Misc comments and formatting. #148

statebox · Aug 22, 2019 · f882abd · f882abd
1 parent 0bce9fd
commit f882abd
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 28 deletions.
diff --git a/src/Language/CQL/Instance.hs b/src/Language/CQL/Instance.hs
@@ -98,9 +98,9 @@ data InstanceEx :: * where
     -> InstanceEx
 
 
--- | Converts an algebra into a presentation: adds one equation per fact in the algebra
--- and one generator per element.  Presentations in this form are called saturated because
--- they are maximally large without being redundant.  @I(fk.x) = I(fk)(I(x))@
+-- | Converts an algebra into a presentation: adds one equation per fact in the algebra,
+--   and one generator per element.  Presentations in this form are called saturated because
+--   they are maximally large without being redundant.  @I(fk.x) = I(fk)(I(x))@
 algebraToPresentation :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Ord y, Ord x)
   => Algebra var ty sym en fk att gen sk x y
   -> Presentation var ty sym en fk att x y
@@ -240,7 +240,7 @@ initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra
     nf'''' (Left g)          = Sk $ MkTalgGen $ Left   g
     nf'''' (Right (gt, att)) = Sk $ MkTalgGen $ Right (gt, att)
 
-    --repr'''' :: TalgGen en fk att gen sk -> Term Void ty sym en fk att gen sk
+    repr'''' :: TalgGen en fk att gen sk -> Term Void ty sym en fk att gen sk
     repr'''' (MkTalgGen (Left g))         = Sk g
     repr'''' (MkTalgGen (Right (x, att))) = Att att $ upp x
 
@@ -417,12 +417,12 @@ evalInstanceRaw' sch (InstExpRaw' _ gens0 eqs' _ _) is = do
       rest <- transEq gens' sks' eqs''
       pure $ Set.insert (EQ (lhs', rhs')) rest
 
-    --transPath :: forall en fk gen . [String] -> RawTerm -> Err (Term Void Void Void en fk Void Gen Void)
+    transPath :: forall var' ty' sym' en' att'. [String] -> RawTerm -> Err (Term var' ty' sym' en' fk att' String Sk)
     transPath gens' (RawApp x [])  | elem  x gens' = pure $ Gen x
     transPath gens' (RawApp x [a]) | elem' x (Map.keys $ sch_fks sch) = Fk (fromJust $ cast x) <$> transPath gens' a
     transPath _ x = Left $ "cannot type " ++ show x
 
-    --transTerm :: forall ty sym en fk att Gen Sk . [String] -> [String] -> RawTerm -> Err (Term Void ty sym en fk att Gen Sk)
+    transTerm :: [String] -> [String] -> RawTerm -> Err (Term Void ty sym en fk att Gen Sk)
     transTerm gens' _    (RawApp x [])  | elem  x gens' = pure $ Gen x
     transTerm _     sks' (RawApp x [])  | elem  x sks'  = pure $ Sk  x
     transTerm gens' _    (RawApp x [a]) | elem' x (Map.keys $ sch_fks  sch) = Fk  (fromJust $ cast x) <$> transPath gens' a
@@ -462,22 +462,26 @@ evalInstanceRaw ops ty' t is = do
 
 -- | The empty instance on a schema has no data, so the types of its generators and carriers are 'Void'.
 emptyInstance :: Schema var ty sym en fk att -> Instance var ty sym en fk att Void Void Void Void
-emptyInstance ts'' = Instance ts''
+emptyInstance ts'' =
+  Instance
+    ts''
     (Presentation Map.empty Map.empty Set.empty)
     (const undefined)
     (Algebra ts''
       (const Set.empty) (const undefined) (const undefined) (const undefined)
       (const Set.empty) (const undefined) (const undefined)
       Set.empty)
 
--- | Pivots an instance. The returned schema will not have strings as fks etc, so it will be impossible to write a literal on it, at least for now. 
--- (Java CQL hacks around this by landing on String.)
-pivot :: forall var ty sym en fk att gen sk x y
+-- | Pivot an instance. The returned schema will not have strings as fks etc, so it will be impossible to write a literal on it, at least for now. 
+--   (Java CQL hacks around this by landing on String.)
+pivot
+  :: forall var ty sym en fk att gen sk x y
    . (MultiTyMap '[Show, Ord, Typeable] '[var, ty, sym, en, fk, att, gen, sk, x, y])
-  => Instance  var ty sym     en      fk      att                    gen  sk  x  y
-  -> (Schema   var ty sym (x, en) (x, fk) (x, att)
-  ,  Instance  var ty sym (x, en) (x, fk) (x, att)  (x, en) y (x, en)  y
-  ,  Mapping   var ty sym (x, en) (x, fk) (x, att)      en  fk att)
+  => Instance   var ty sym     en      fk      att                    gen  sk  x  y
+  -> ( Schema   var ty sym (x, en) (x, fk) (x, att)
+     , Instance var ty sym (x, en) (x, fk) (x, att)  (x, en) y  (x, en)           y
+     , Mapping  var ty sym (x, en) (x, fk) (x, att)      en  fk att
+     )
 pivot (Instance sch _ idp (Algebra _ ens _ fk fn tys nnf rep2'' teqs)) = (sch', inst, mapp)
   where
     sch'_ens  = Set.fromList [  (x, en)                                | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en)]
@@ -536,7 +540,6 @@ pivot (Instance sch _ idp (Algebra _ ens _ fk fn tys nnf rep2'' teqs)) = (sch',
       Fk (_, f) a  -> Fk f $ instToInst a
       Gen (x, _)   -> upp $ fn x
 
--- coproducts, etc
 
 ---------------------------------------------------------------------------------------------------------------
 -- Functorial data migration
@@ -551,7 +554,6 @@ subs (Mapping _ _ ens' fks' atts') (Presentation gens' sks' eqs') = Presentation
     gens'' = Map.map (\k -> ens' ! k) gens'
     eqs''  = Set.map (\(EQ (l, r)) -> EQ (changeEn fks' atts' l, changeEn fks' atts' r)) eqs'
 
-
 changeEn
   :: (Ord k1, Ord k2, Eq var)
   => Map k1 (Term () Void Void en1 fk Void Void Void)

diff --git a/src/Language/CQL/Instance/Algebra.hs b/src/Language/CQL/Instance/Algebra.hs
@@ -86,8 +86,8 @@ data Algebra var ty sym en fk att gen sk x y
 instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData x, NFData y)
   => NFData (Algebra var ty sym en fk att gen sk x y)
   where
-    rnf (Algebra s0 e0 nf0 nf02 repr0 ty0 nf1 repr1 eqs1) = deepseq s0 $ f e0 $ deepseq nf0 $ deepseq repr0
-      $ w ty0 $ deepseq nf1 $ deepseq repr1 $ deepseq nf02 $ rnf eqs1
+    rnf (Algebra s0 e0 nf0 nf02 repr0 ty0 nf1 repr1 eqs1) =
+      deepseq s0 $ f e0 $ deepseq nf0 $ deepseq repr0 $ w ty0 $ deepseq nf1 $ deepseq repr1 $ deepseq nf02 $ rnf eqs1
       where
         f g = deepseq (Set.map (rnf . g) $ Schema.ens s0)
         w g = deepseq (Set.map (rnf . g) $ tys (typeside s0))
@@ -111,7 +111,6 @@ evalSchTerm alg x term = case term of
   Sym f as -> Sym f $ fmap (evalSchTerm alg x) as
   _        -> error "Impossibility in evalSchTerm, please report.  Given a term of non-type sort."
 
-
 -- | Helper to convert terms in the 'Collage' of entity sort into terms with 'Void's in the attribute etc slots.
 --   Morally, 'Collage' should store two or more classes of equation, but having to convert like this is relatively rare.
 --   Indeed, 'IP.satisfiesSchema' itself is redundant; a properly functioning CQL would not generate unsatisfying

diff --git a/src/Language/CQL/Term.hs b/src/Language/CQL/Term.hs
@@ -268,7 +268,7 @@ occurs h x = case x of
   Sym h' as -> h == HSym h' || any (occurs h) as
 
 -- | If there is one, finds an equation of the form empty |- @gen/sk = term@,
--- where @gen@ does not occur in @term@.
+--   where @gen@ does not occur in @term@.
 findSimplifiableEqs
   :: (Eq ty, Eq sym, Eq en, Eq fk, Eq att, Eq gen, Eq sk)
   => Theory var ty sym en fk att gen sk
@@ -280,13 +280,14 @@ findSimplifiableEqs = procEqs . Set.toList
     g (Gen y)    t = if occurs (HGen y) t then Nothing else Just (HGen y, t)
     g (Sym _ []) _ = Nothing
     g _ _          = Nothing
-    procEqs []  = Nothing
+
+    procEqs []                             = Nothing
     procEqs ((m, _):tl) | not (Map.null m) = procEqs tl
-    procEqs ((_, EQ (lhs, rhs)):tl) = case g lhs rhs of
-      Nothing -> case g rhs lhs of
-        Nothing -> procEqs tl
-        Just y  -> Just y
-      Just   y -> Just y
+    procEqs ((_, EQ (lhs, rhs)):tl)        = case g lhs rhs of
+                                               Nothing -> case g rhs lhs of
+                                                 Nothing -> procEqs tl
+                                                 Just y  -> Just y
+                                               Just   y -> Just y
 
 -- | Replaces a symbol by a term in a term.
 replace'
@@ -343,7 +344,8 @@ simplifyTheoryStep eqs = case findSimplifiableEqs eqs of
 class Up x y where
   upgr :: x -> y
 
-upp :: (Up var var', Up ty ty', Up sym sym', Up en en', Up fk fk', Up att att', Up gen gen', Up sk sk')
+upp
+  :: (Up var var', Up ty ty', Up sym sym', Up en en', Up fk fk', Up att att', Up gen gen', Up sk sk')
   => Term var  ty  sym  en  fk  att  gen  sk
   -> Term var' ty' sym' en' fk' att' gen' sk'
 upp (Var v  ) = Var $ upgr v
@@ -374,8 +376,9 @@ type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en
 type Ctx k v = Map k v
 
 -- Our own pair type for pretty printing purposes
+-- | This type indicates that the two terms are equal.
 newtype EQ var ty sym en fk att gen sk
-  = EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord,Eq)
+  = EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord, Eq)
 
 instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (EQ var ty sym en fk att gen sk) where
   show (EQ (lhs,rhs)) = show lhs ++ " = " ++ show rhs