Assorted formatting, refactoring, commenting. #148

src/Language/CQL.hs

@@ -89,7 +89,7 @@ timeout' i p = unsafePerformIO $ do
 class Typecheck e e' where
   typecheck :: Types -> e -> Err e'
 
--- | Checks that e.g. in @sigma F I@ that @F : S -> T and I : S-Inst@.
+-- | Checks that e.g. in @sigma F I@ that @F : S -> T@ and @I : S-Inst@.
 -- Checking that @S@ is well-formed is done by 'validate'.
 typecheckCqlProgram :: [(String,Kind)] -> Prog -> Types -> Err Types
 typecheckCqlProgram [] _ x = pure x
@@ -360,6 +360,7 @@ getOptions' e = case e of
   ExpM  e' -> getOptions e'
   ExpT  e' -> getOptions e'
   ExpQ  e' -> getOptions e'
+
 ------------------------------------------------------------------------------------------------------------
 
 evalTypeside :: Prog -> Env -> TypesideExp -> Err TypesideEx

src/Language/CQL/Collage.hs

@@ -55,9 +55,9 @@ data Collage var ty sym en fk att gen sk
   { ceqs  :: Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
   , ctys  :: Set ty
   , cens  :: Set en
-  , csyms :: Map sym ([ty],ty)
-  , cfks  :: Map fk (en, en)
-  , catts :: Map att (en, ty)
+  , csyms :: Map sym ([ty], ty)
+  , cfks  :: Map fk  (en  , en)
+  , catts :: Map att (en  , ty)
   , cgens :: Map gen en
   , csks  :: Map sk ty
   } deriving (Eq, Show)
@@ -81,7 +81,7 @@ simplify
   =>  Collage var ty sym en fk att gen sk
   -> (Collage var ty sym en fk att gen sk, [(Head ty sym en fk att gen sk, Term var ty sym en fk att gen sk)])
 simplify (Collage ceqs'  ctys' cens' csyms' cfks' catts' cgens'  csks'    )
-  =         (Collage ceqs'' ctys' cens' csyms' cfks' catts' cgens'' csks'', f)
+  =      (Collage ceqs'' ctys' cens' csyms' cfks' catts' cgens'' csks'', f)
   where
     (ceqs'', f) = simplifyFix ceqs' []
     cgens''     = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HGen x) $ fmap fst f) $ Map.toList cgens'
@@ -109,7 +109,7 @@ assembleGens
  => Collage var ty sym en fk att gen sk
  -> [Carrier en fk gen]
  -> Map en (Set (Carrier en fk gen))
-assembleGens col []     = Map.fromList $ fmap (, Set.empty) $ Set.toList $ cens col
+assembleGens col []     = Map.fromList $ mapl (, Set.empty) $ cens col
 assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
   where
     m = assembleGens col tl
@@ -211,8 +211,8 @@ typeOfEq' col (ctx, EQ (lhs, rhs)) = do
 initGround :: (Ord ty, Ord en) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool)
 initGround col = (me', mt')
   where
-    me  = Map.fromList $ Prelude.map (\en -> (en, False)) $ Set.toList $ cens col
-    mt  = Map.fromList $ Prelude.map (\ty -> (ty, False)) $ Set.toList $ ctys col
+    me  = Map.fromList $ fmap (\en -> (en, False))              $ Set.toList $ cens  col
+    mt  = Map.fromList $ fmap (\ty -> (ty, False))              $ Set.toList $ ctys  col
     me' = Prelude.foldr (\(_, en) m -> Map.insert en True m) me $ Map.toList $ cgens col
     mt' = Prelude.foldr (\(_, ty) m -> Map.insert ty True m) mt $ Map.toList $ csks  col
 

src/Language/CQL/Instance.hs

@@ -67,12 +67,17 @@ import qualified Text.Tabular.AsciiArt as Ascii
 --------------------------------------------------------------------------------------------------------------------
 -- Algebras
 
--- | An algebra (model) of a schema.  For entities, consists of a carrier set, evaluation function
--- (nf), and its "inverse" repr.  For types, consists of a generating set of labelled nulls,
--- evaluation function (nf'), and its "inverse" repr', as well as a set of equations (the so-called type algebra).
--- The Eq instance is not defined because for now we define instance equality to be based on equations.
--- x: type of Carrier
--- y: type of generators for type algebra presentation
+-- | An algebra (model) of a 'Schema'.
+--
+--   * For entities, consists of a carrier set, evaluation function @nf@, and its "inverse" @repr@.
+--
+--   * For types, consists of a generating set of labelled nulls, evaluation function @nf'@, and its "inverse" @repr'@,
+--     as well as a set of equations (the so-called type algebra).
+--
+-- The @Eq@ instance is not defined because for now we define instance equality to be based on equations.
+--
+-- @x@: type of Carrier
+-- @y@: type of generators for type algebra presentation
 data Algebra var ty sym en fk att gen sk x y
   = Algebra
   { aschema :: Schema var ty sym en fk att
@@ -186,7 +191,7 @@ data Instance var ty sym en fk att gen sk x y
   = Instance
   { schema  :: Schema       var  ty sym en fk att
   , pres    :: Presentation var  ty sym en fk att gen sk
-  , dp      :: EQ           Void ty sym en fk att gen sk -> Bool
+  , dp      :: EQ           Void ty sym en fk att gen sk     -> Bool
   , algebra :: Algebra      var  ty sym en fk att gen sk x y
   }
 
@@ -198,7 +203,8 @@ freeTalg (Instance _ _ _ (Algebra _ _ _ _ _ _ _ _ teqs)) = Prelude.null teqs
 -- | Just syntactic equality of the theory for now.
 instance TyMap Eq '[var, ty, sym, en, fk, att, gen, sk, x, y]
   => Eq (Instance var ty sym en fk att gen sk x y) where
-  (==) (Instance schema' (Presentation gens' sks' eqs') _ _) (Instance schema'' (Presentation gens'' sks'' eqs'') _ _)
+  (==) (Instance schema'  (Presentation gens'  sks'  eqs' ) _ _)
+       (Instance schema'' (Presentation gens'' sks'' eqs'') _ _)
     = (schema' == schema'') && (gens' == gens'') && (sks' == sks'') && (eqs' == eqs'')
 
 instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk, x, y]
@@ -242,8 +248,8 @@ reify f s = concat $ Set.toList $ Set.map (\en'-> Set.toList $ Set.map (, en') $
 saturatedInstance
   :: forall var ty sym en fk att gen sk
   .  (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
-  => Schema var ty sym en fk att
-  -> Presentation var ty sym en fk att gen sk
+  => Schema        var ty sym en fk att
+  -> Presentation  var ty sym en fk att gen sk
   -> Err (Instance var ty sym en fk att gen sk gen (Either sk (gen, att)))
 saturatedInstance sch (Presentation gens sks eqs) = do
   (fks, atts) <- foldM procEq (Map.empty, Map.empty) eqs
@@ -252,7 +258,7 @@ saturatedInstance sch (Presentation gens sks eqs) = do
   let alg = Algebra sch (Set.fromList . gens') (nf1 fks) (nf2 fks) Gen (Set.fromList . sks' atts) (nf' atts) repr' Set.empty
   pure $ Instance sch (Presentation gens sks eqs) (\(EQ (l, r)) -> l == r) alg
   where
-    --checkTotality :: Map (gen, fk) gen -> Err ()
+    checkTotality :: Map (gen, fk) gen -> Err ()
     checkTotality fks =
       mapM_ (\en -> if   List.null (fksMissing en fks)
                     then pure ()
@@ -294,7 +300,11 @@ saturatedInstance sch (Presentation gens sks eqs) = do
 ---------------------------------------------------------------------------------------------------------------
 -- Initial algebras
 
+-- | The carrier for the initial algebra of an instance; they are just terms.
+--   Made into a separate type so this could be changed; cql-java for example just uses natural numbers as the carrier.
 type Carrier en fk gen = Term Void Void Void en fk Void gen Void
+
+-- | The generating labelled nulls for the type algebra of the associated instance.
 newtype TalgGen en fk att gen sk = MkTalgGen (Either sk (Carrier en fk gen, att))
 
 -- | Computes an initial instance (minimal model of a presentation).

src/Language/CQL/Morphism.hs

@@ -49,17 +49,17 @@ import           Language.CQL.Common
 import           Language.CQL.Term     (Ctx, Term(..), EQ(..), subst, upp)
 import           Prelude               hiding (EQ)
 
-
+-- | A morphism between 'Collage's.
 data Morphism var ty sym en fk att gen sk en' fk' att' gen' sk'
-  = Morphism {
-    m_src  :: Collage (()+var) ty sym en fk att gen sk
+  = Morphism
+  { m_src  :: Collage (()+var) ty sym en  fk  att  gen  sk
   , m_dst  :: Collage (()+var) ty sym en' fk' att' gen' sk'
   , m_ens  :: Map en  en'
-  , m_fks  :: Map fk  (Term () Void Void en' fk' Void Void Void)
-  , m_atts :: Map att (Term () ty   sym  en' fk' att' Void Void)
+  , m_fks  :: Map fk  (Term ()   Void Void en' fk' Void Void Void)
+  , m_atts :: Map att (Term ()   ty   sym  en' fk' att' Void Void)
   , m_gens :: Map gen (Term Void Void Void en' fk' Void gen' Void)
-  , m_sks  :: Map sk  (Term Void  ty   sym  en' fk' att'  gen' sk')
-}
+  , m_sks  :: Map sk  (Term Void ty   sym  en' fk' att' gen' sk')
+  }
 
 -- | Checks totality of the morphism mappings.
 checkDoms'
@@ -111,8 +111,8 @@ translate mor term = case term of
   Att f a  -> subst (upp $ m_atts mor ! f) $ translate mor a
   Fk  f a  -> subst (upp y) x
     where
-      x = translate mor a :: Term var' ty sym  en' fk' att' gen' sk'
-      y = m_fks mor ! f   :: Term () Void Void en' fk' Void Void Void
+      x = translate mor a :: Term var' ty   sym  en' fk' att' gen' sk'
+      y = m_fks mor ! f   :: Term ()   Void Void en' fk' Void Void Void
 
 typeOf
   :: forall var ty sym en fk att gen sk en' fk' att' gen' sk'
@@ -159,7 +159,6 @@ typeOf mor  = do
     typeOfMorSks (e,e') = Left $ "Bad null mapping " ++ show e ++ " -> " ++ show e'
 
 
--- I've given up on non string based error handling for now
 typeOf'
   :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk

src/Language/CQL/Prover.hs

@@ -264,20 +264,22 @@ initState col = Set.foldr (\z s -> addAxiom defaultConfig s (toAxiom z)) initial
 -- lhs -> rhs where the lhs is larger than the rhs, adding additional equations whenever
 -- critical pairs (rule overlaps) are detected.
 kbProver
-  :: forall                     var  ty  sym  en  fk  att  gen  sk
+  :: forall var  ty  sym  en  fk  att  gen  sk
   .  (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Options
   -> Err (Prover var ty sym en fk att gen sk)
-kbProver col ops = if allSortsInhabited col || allow_empty
-      then let p' ctx (EQ (l, r)) = p ctx $ EQ (replaceRepeatedly f l, replaceRepeatedly f r)
-           in pure $ Prover col p'
-      else Left "Completion Error: contains uninhabited sorts"
+kbProver col ops =
+  if allSortsInhabited col || allow_empty
+  then let p' ctx (EQ (l, r)) = p ctx $ EQ (replaceRepeatedly f l, replaceRepeatedly f r)
+       in pure $ Prover col p'
+  else Left "Completion Error: contains uninhabited sorts"
   where
-    (col', f) = Collage.simplify col
+    (col', f)               = Collage.simplify col
     p ctx (EQ (lhs', rhs')) = normaliseTerm (completed ctx lhs' rhs') (convert col ctx lhs') == normaliseTerm (completed ctx lhs' rhs') (convert col ctx rhs')
-    completed g l r = completePure defaultConfig $ addGoal defaultConfig (initState col') (toGoal g l r)
-    allow_empty = bOps ops Allow_Empty_Sorts_Unsafe
+    completed g l r         = completePure defaultConfig $ addGoal defaultConfig (initState col') (toGoal g l r)
+    allow_empty             = bOps ops Allow_Empty_Sorts_Unsafe
+
     toGoal :: Ctx var (ty+en) -> S.Term var ty sym en fk att gen sk -> S.Term var ty sym en fk att gen sk -> Goal (Extended (Constant (Head ty sym en fk att gen sk)))
     toGoal ctx lhs0 rhs0 = goal 0 "" $ convert col ctx lhs0 :=: convert col ctx rhs0
 

src/Language/CQL/Term.hs

@@ -344,7 +344,8 @@ 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')
-  => Term var ty sym en fk att gen sk -> Term var' ty' sym' en' fk' att' gen' 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
 upp (Sym f a) = Sym (upgr f) $ fmap upp a
 upp (Fk  f a) = Fk  (upgr f) $      upp a