Still more Cleanup. #148 (#154)

* Move assembleGens from Instance into Collage. #148

* Move Presentation into its own module Instance.Presentation. #148

* Clean up code in and around Instance.Presentation. #148

* Assorted formatting, refactoring, commenting. #148

* Rename checkSatisfaction -> I.satisfiesSchema, typecheckPresentation -> IP.typecheck. #148

* in Presentation, rename eqs0 to eqs and fully qualify as IP.eqs. #148

* Move Algebra into its own module Instance.Algebra. #148

* Instance.hs: move satisfiesSchema down a bit. #148

* Rename presToCol to IP.toCollage. #148

* Remove duplicate simplifyAlg and rename to A.simplify. #148

* Rename Term.simplifyFix to Term.simplifyTheory. #148

* Term.hs: Rename findSimplifiable -> findSimplifiableEqs. #148

* Term.hs: Introduce Theory type alias. #148

* Misc comments and formatting. #148

* Instance.hs: Use Carrier type alias where it fits. #148

* Clean up leftovers from moving Carrier and TalgGen into Algebra. #148

* Term.hs: move Head directly under Term. #148

* Term.hs: rename replace' -> replace. #148

* Simplify and clean up findSimplifiableEq. #148

src/Language/CQL.hs

@@ -42,23 +42,24 @@ module Language.CQL where
 import Control.Concurrent
 import Control.DeepSeq
 import Control.Exception
-import Data.List (nub)
-import qualified Data.Map.Strict as Map
+import Data.List  (nub)
+import qualified Data.Map.Strict  as Map
 import Data.Maybe
 import Data.Typeable
-import Language.CQL.Common as C
+import Language.CQL.Common  as C
 import Language.CQL.Graph
-import Language.CQL.Instance as I
-import Language.CQL.Mapping as M
+import Language.CQL.Instance as I
+import qualified Language.CQL.Instance.Presentation as IP
+import Language.CQL.Mapping as M
 import Language.CQL.Options
-import Language.CQL.Parser.Program (parseProgram)
-import Language.CQL.Program as P
-import Language.CQL.Query as Q
-import Language.CQL.Schema as S
-import Language.CQL.Term as Term
-import Language.CQL.Transform as Tr
-import Language.CQL.Typeside as T
-import Prelude hiding (EQ, exp)
+import Language.CQL.Parser.Program  (parseProgram)
+import Language.CQL.Program  as P
+import Language.CQL.Query  as Q
+import Language.CQL.Schema  as S
+import Language.CQL.Term  as Term
+import Language.CQL.Transform  as Tr
+import Language.CQL.Typeside  as T
+import Prelude  hiding (EQ, exp)
 import System.IO.Unsafe
 
 -- | Times out a computation after @i@ microseconds.
@@ -88,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
@@ -319,11 +320,9 @@ instance Evalable SchemaExp SchemaEx where
  getOptions = getOptionsSchema
 
 instance Evalable InstanceExp InstanceEx where
-
- -- | Calls @checkSatisfaction@.
  validate (InstanceEx x) = do
- typecheckPresentation (schema x) (pres x)
- checkSatisfaction x
+ IP.typecheck (schema x) (pres x)
+ I.satisfiesSchema x
  eval prog env exp = do
  i <- evalInstance prog env exp
  o' <- toOptions (other env) $ getOptions exp
@@ -359,6 +358,7 @@ getOptions' e = case e of
  ExpM e' -> getOptions e'
  ExpT e' -> getOptions e'
  ExpQ e' -> getOptions e'
+
 ------------------------------------------------------------------------------------------------------------
 
 evalTypeside :: Prog -> Env -> TypesideExp -> Err TypesideEx
@@ -382,8 +382,8 @@ evalTransform p env (TransformId s) = do
  (InstanceEx i) <- evalInstance p env s
  pure $ TransformEx $ Transform i i (h i) (g i)
  where
- h i = foldr (\(gen,_) m -> Map.insert gen (Gen gen) m) Map.empty $ Map.toList $ I.gens $ pres i
- g i = foldr (\(sk ,_) m -> Map.insert sk (Sk sk) m) Map.empty $ Map.toList $ I.sks $ pres i
+ h i = foldr (\(gen,_) m -> Map.insert gen (Gen gen) m) Map.empty $ Map.toList $ IP.gens $ pres i
+ g i = foldr (\(sk ,_) m -> Map.insert sk (Sk sk) m) Map.empty $ Map.toList $ IP.sks $ pres i
 
 evalTransform p env (TransformComp f g) = do
  (TransformEx (f' :: Transform var ty sym en fk att gen sk x y gen' sk' x' y' )) <- evalTransform p env f

src/Language/CQL/Collage.hs

@@ -33,6 +33,7 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -45,18 +46,18 @@ import Data.Map.Strict as Map hiding (foldr, size)
 import Data.Set as Set hiding (foldr, size)
 import Data.Void
 import Language.CQL.Common
-import Language.CQL.Term (Head(..), Term(..), simplifyFix, occsTerm, upp)
-import  Language.CQL.Term (EQ(..), Ctx)
+import Language.CQL.Term (Ctx, EQ(..), Head(..), Term(..), occsTerm, upp)
+import qualified Language.CQL.Term as T (simplifyTheory)
 import Prelude hiding (EQ)
 
 data Collage var ty sym en fk att gen sk
  = Collage
  { 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)
@@ -80,9 +81,9 @@ 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' []
+ (ceqs'', f) = T.simplifyTheory ceqs' []
  cgens'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HGen x) $ fmap fst f) $ Map.toList cgens'
  csks'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HSk x) $ fmap fst f) $ Map.toList csks'
 
@@ -101,6 +102,21 @@ attsFrom sch en' = f $ Map.assocs $ catts sch
  where f [] = []
  f ((fk,(en1,t)):l) = if en1 == en' then (fk,t) : (f l) else f l
 
+-- TODO Carrier is duplicated here from Instance.Algebra (Carrier) because it is used in assembleGens.
+type Carrier en fk gen = Term Void Void Void en fk Void gen Void
+
+assembleGens
+ :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
+ => Collage var ty sym en fk att gen sk
+ -> [Carrier en fk gen]
+ -> Map en (Set (Carrier en fk gen))
+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
+ t = typeOf col e
+ s = m ! t
+
 -- | Gets the type of a term that is already known to be well-typed.
 typeOf
  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
@@ -196,8 +212,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