Skip to content

Commit f969b85

Browse files
epostepost
authored
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
1 parent d911bab commit f969b85

File tree

9 files changed

+609
-433
lines changed

9 files changed

+609
-433
lines changed

‎src/Language/CQL.hs

+20-20
Original file line numberDiff line numberDiff line change
@@ -42,23 +42,24 @@ module Language.CQL where
4242
import Control.Concurrent
4343
import Control.DeepSeq
4444
import Control.Exception
45-
import Data.List (nub)
46-
import qualified Data.Map.Strict as Map
45+
import Data.List (nub)
46+
import qualified Data.Map.Strict as Map
4747
import Data.Maybe
4848
import Data.Typeable
49-
import Language.CQL.Common as C
49+
import Language.CQL.Common as C
5050
import Language.CQL.Graph
51-
import Language.CQL.Instance as I
52-
import Language.CQL.Mapping as M
51+
import Language.CQL.Instance as I
52+
import qualified Language.CQL.Instance.Presentation as IP
53+
import Language.CQL.Mapping as M
5354
import Language.CQL.Options
54-
import Language.CQL.Parser.Program (parseProgram)
55-
import Language.CQL.Program as P
56-
import Language.CQL.Query as Q
57-
import Language.CQL.Schema as S
58-
import Language.CQL.Term as Term
59-
import Language.CQL.Transform as Tr
60-
import Language.CQL.Typeside as T
61-
import Prelude hiding (EQ, exp)
55+
import Language.CQL.Parser.Program (parseProgram)
56+
import Language.CQL.Program as P
57+
import Language.CQL.Query as Q
58+
import Language.CQL.Schema as S
59+
import Language.CQL.Term as Term
60+
import Language.CQL.Transform as Tr
61+
import Language.CQL.Typeside as T
62+
import Prelude hiding (EQ, exp)
6263
import System.IO.Unsafe
6364

6465
-- | Times out a computation after @i@ microseconds.
@@ -88,7 +89,7 @@ timeout' i p = unsafePerformIO $ do
8889
class Typecheck e e' where
8990
typecheck :: Types -> e -> Err e'
9091

91-
-- | Checks that e.g. in @sigma F I@ that @F : S -> T and I : S-Inst@.
92+
-- | Checks that e.g. in @sigma F I@ that @F : S -> T@ and @I : S-Inst@.
9293
-- Checking that @S@ is well-formed is done by 'validate'.
9394
typecheckCqlProgram :: [(String,Kind)] -> Prog -> Types -> Err Types
9495
typecheckCqlProgram [] _ x = pure x
@@ -319,11 +320,9 @@ instance Evalable SchemaExp SchemaEx where
319320
getOptions = getOptionsSchema
320321

321322
instance Evalable InstanceExp InstanceEx where
322-
323-
-- | Calls @checkSatisfaction@.
324323
validate (InstanceEx x) = do
325-
typecheckPresentation (schema x) (pres x)
326-
checkSatisfaction x
324+
IP.typecheck (schema x) (pres x)
325+
I.satisfiesSchema x
327326
eval prog env exp = do
328327
i <- evalInstance prog env exp
329328
o' <- toOptions (other env) $ getOptions exp
@@ -359,6 +358,7 @@ getOptions' e = case e of
359358
ExpM e' -> getOptions e'
360359
ExpT e' -> getOptions e'
361360
ExpQ e' -> getOptions e'
361+
362362
------------------------------------------------------------------------------------------------------------
363363

364364
evalTypeside :: Prog -> Env -> TypesideExp -> Err TypesideEx
@@ -382,8 +382,8 @@ evalTransform p env (TransformId s) = do
382382
(InstanceEx i) <- evalInstance p env s
383383
pure $ TransformEx $ Transform i i (h i) (g i)
384384
where
385-
h i = foldr (\(gen,_) m -> Map.insert gen (Gen gen) m) Map.empty $ Map.toList $ I.gens $ pres i
386-
g i = foldr (\(sk ,_) m -> Map.insert sk (Sk sk) m) Map.empty $ Map.toList $ I.sks $ pres i
385+
h i = foldr (\(gen,_) m -> Map.insert gen (Gen gen) m) Map.empty $ Map.toList $ IP.gens $ pres i
386+
g i = foldr (\(sk ,_) m -> Map.insert sk (Sk sk) m) Map.empty $ Map.toList $ IP.sks $ pres i
387387

388388
evalTransform p env (TransformComp f g) = do
389389
(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

+25-9
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.
3333
{-# LANGUAGE RankNTypes #-}
3434
{-# LANGUAGE ScopedTypeVariables #-}
3535
{-# LANGUAGE StandaloneDeriving #-}
36+
{-# LANGUAGE TupleSections #-}
3637
{-# LANGUAGE TypeOperators #-}
3738
{-# LANGUAGE TypeSynonymInstances #-}
3839
{-# LANGUAGE UndecidableInstances #-}
@@ -45,18 +46,18 @@ import Data.Map.Strict as Map hiding (foldr, size)
4546
import Data.Set as Set hiding (foldr, size)
4647
import Data.Void
4748
import Language.CQL.Common
48-
import Language.CQL.Term (Head(..), Term(..), simplifyFix, occsTerm, upp)
49-
import Language.CQL.Term (EQ(..), Ctx)
49+
import Language.CQL.Term (Ctx, EQ(..), Head(..), Term(..), occsTerm, upp)
50+
import qualified Language.CQL.Term as T (simplifyTheory)
5051
import Prelude hiding (EQ)
5152

5253
data Collage var ty sym en fk att gen sk
5354
= Collage
5455
{ ceqs :: Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
5556
, ctys :: Set ty
5657
, cens :: Set en
57-
, csyms :: Map sym ([ty],ty)
58-
, cfks :: Map fk (en, en)
59-
, catts :: Map att (en, ty)
58+
, csyms :: Map sym ([ty], ty)
59+
, cfks :: Map fk (en , en)
60+
, catts :: Map att (en , ty)
6061
, cgens :: Map gen en
6162
, csks :: Map sk ty
6263
} deriving (Eq, Show)
@@ -80,9 +81,9 @@ simplify
8081
=> Collage var ty sym en fk att gen sk
8182
-> (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)])
8283
simplify (Collage ceqs' ctys' cens' csyms' cfks' catts' cgens' csks' )
83-
= (Collage ceqs'' ctys' cens' csyms' cfks' catts' cgens'' csks'', f)
84+
= (Collage ceqs'' ctys' cens' csyms' cfks' catts' cgens'' csks'', f)
8485
where
85-
(ceqs'', f) = simplifyFix ceqs' []
86+
(ceqs'', f) = T.simplifyTheory ceqs' []
8687
cgens'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HGen x) $ fmap fst f) $ Map.toList cgens'
8788
csks'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HSk x) $ fmap fst f) $ Map.toList csks'
8889

@@ -101,6 +102,21 @@ attsFrom sch en' = f $ Map.assocs $ catts sch
101102
where f [] = []
102103
f ((fk,(en1,t)):l) = if en1 == en' then (fk,t) : (f l) else f l
103104

105+
-- TODO Carrier is duplicated here from Instance.Algebra (Carrier) because it is used in assembleGens.
106+
type Carrier en fk gen = Term Void Void Void en fk Void gen Void
107+
108+
assembleGens
109+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
110+
=> Collage var ty sym en fk att gen sk
111+
-> [Carrier en fk gen]
112+
-> Map en (Set (Carrier en fk gen))
113+
assembleGens col [] = Map.fromList $ mapl (, Set.empty) $ cens col
114+
assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
115+
where
116+
m = assembleGens col tl
117+
t = typeOf col e
118+
s = m ! t
119+
104120
-- | Gets the type of a term that is already known to be well-typed.
105121
typeOf
106122
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
@@ -196,8 +212,8 @@ typeOfEq' col (ctx, EQ (lhs, rhs)) = do
196212
initGround :: (Ord ty, Ord en) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool)
197213
initGround col = (me', mt')
198214
where
199-
me = Map.fromList $ Prelude.map (\en -> (en, False)) $ Set.toList $ cens col
200-
mt = Map.fromList $ Prelude.map (\ty -> (ty, False)) $ Set.toList $ ctys col
215+
me = Map.fromList $ fmap (\en -> (en, False)) $ Set.toList $ cens col
216+
mt = Map.fromList $ fmap (\ty -> (ty, False)) $ Set.toList $ ctys col
201217
me' = Prelude.foldr (\(_, en) m -> Map.insert en True m) me $ Map.toList $ cgens col
202218
mt' = Prelude.foldr (\(_, ty) m -> Map.insert ty True m) mt $ Map.toList $ csks col
203219

0 commit comments

Comments
 (0)