Skip to content

Commit 667a1bb

Browse files
epostepost
committed
Move Collage into its own separate module. #148 
1 parent 8cd7f65 commit 667a1bb

File tree

7 files changed

+240
-182
lines changed

7 files changed

+240
-182
lines changed

‎src/Language/CQL/Collage.hs

+226
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,226 @@
1+
{-
2+
SPDX-License-Identifier: AGPL-3.0-only
3+
4+
This file is part of `statebox/cql`, the categorical query language.
5+
6+
Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
7+
8+
This program is free software: you can redistribute it and/or modify
9+
it under the terms of the GNU Affero General Public License as published by
10+
the Free Software Foundation, either version 3 of the License, or
11+
(at your option) any later version.
12+
13+
This program is distributed in the hope that it will be useful,
14+
but WITHOUT ANY WARRANTY; without even the implied warranty of
15+
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16+
GNU Affero General Public License for more details.
17+
18+
You should have received a copy of the GNU Affero General Public License
19+
along with this program. If not, see <https://www.gnu.org/licenses/>.
20+
-}
21+
{-# LANGUAGE AllowAmbiguousTypes #-}
22+
{-# LANGUAGE DataKinds #-}
23+
{-# LANGUAGE DuplicateRecordFields #-}
24+
{-# LANGUAGE ExplicitForAll #-}
25+
{-# LANGUAGE FlexibleContexts #-}
26+
{-# LANGUAGE FlexibleInstances #-}
27+
{-# LANGUAGE GADTs #-}
28+
{-# LANGUAGE ImpredicativeTypes #-}
29+
{-# LANGUAGE IncoherentInstances #-}
30+
{-# LANGUAGE InstanceSigs #-}
31+
{-# LANGUAGE LiberalTypeSynonyms #-}
32+
{-# LANGUAGE MultiParamTypeClasses #-}
33+
{-# LANGUAGE RankNTypes #-}
34+
{-# LANGUAGE ScopedTypeVariables #-}
35+
{-# LANGUAGE StandaloneDeriving #-}
36+
{-# LANGUAGE TypeOperators #-}
37+
{-# LANGUAGE TypeSynonymInstances #-}
38+
{-# LANGUAGE UndecidableInstances #-}
39+
40+
module Language.CQL.Collage where
41+
42+
import Control.DeepSeq (NFData)
43+
import Data.Map.Merge.Strict
44+
import Data.Map.Strict as Map hiding (foldr, size)
45+
import Data.Set as Set hiding (foldr, size)
46+
import Data.Void
47+
import Language.CQL.Common
48+
import Language.CQL.Term (Head(..), Term(..), simplifyFix, occsTerm, upp)
49+
import Language.CQL.Term (EQ(..), Ctx)
50+
import Prelude hiding (EQ)
51+
52+
data Collage var ty sym en fk att gen sk
53+
= Collage
54+
{ ceqs :: Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
55+
, ctys :: Set ty
56+
, cens :: Set en
57+
, csyms :: Map sym ([ty],ty)
58+
, cfks :: Map fk (en, en)
59+
, catts :: Map att (en, ty)
60+
, cgens :: Map gen en
61+
, csks :: Map sk ty
62+
} deriving (Eq, Show)
63+
64+
--------------------------------------------------------------------------------
65+
66+
occs
67+
:: (Ord sym, Ord fk, Ord att, Ord gen, Ord sk)
68+
=> Collage var ty sym en fk att gen sk
69+
-> Map (Head ty sym en fk att gen sk) Int
70+
occs col = foldr (\(_, EQ (lhs, rhs)) x -> m x $ m (occsTerm lhs) $ occsTerm rhs) Map.empty $ ceqs col
71+
where
72+
m = merge preserveMissing preserveMissing $ zipWithMatched (\_ x y -> x + y)
73+
74+
--------------------------------------------------------------------------------
75+
76+
-- | Simplify a collage by replacing symbols of the form @gen/sk = term@, yielding also a
77+
-- translation function from the old theory to the new, encoded as a list of (symbol, term) pairs.
78+
simplify
79+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
80+
=> Collage var ty sym en fk att gen sk
81+
-> (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)])
82+
simplify (Collage ceqs' ctys' cens' csyms' cfks' catts' cgens' csks' )
83+
= (Collage ceqs'' ctys' cens' csyms' cfks' catts' cgens'' csks'', f)
84+
where
85+
(ceqs'', f) = simplifyFix ceqs' []
86+
cgens'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HGen x) $ fmap fst f) $ Map.toList cgens'
87+
csks'' = Map.fromList $ Prelude.filter (\(x,_) -> notElem (HSk x) $ fmap fst f) $ Map.toList csks'
88+
89+
--------------------------------------------------------------------------------
90+
91+
eqsAreGround :: Collage var ty sym en fk att gen sk -> Bool
92+
eqsAreGround col = Prelude.null [ x | x <- Set.toList $ ceqs col, not $ Map.null (fst x) ]
93+
94+
fksFrom :: Eq en => Collage var ty sym en fk att gen sk -> en -> [(fk,en)]
95+
fksFrom sch en' = f $ Map.assocs $ cfks sch
96+
where f [] = []
97+
f ((fk,(en1,t)):l) = if en1 == en' then (fk,t) : (f l) else f l
98+
99+
attsFrom :: Eq en => Collage var ty sym en fk att gen sk -> en -> [(att,ty)]
100+
attsFrom sch en' = f $ Map.assocs $ catts sch
101+
where f [] = []
102+
f ((fk,(en1,t)):l) = if en1 == en' then (fk,t) : (f l) else f l
103+
104+
-- | Gets the type of a term that is already known to be well-typed.
105+
typeOf
106+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
107+
=> Collage var ty sym en fk att gen sk
108+
-> Term Void Void Void en fk Void gen Void
109+
-> en
110+
typeOf col e = case typeOf' col Map.empty (upp e) of
111+
Left _ -> error "Impossible in typeOf, please report."
112+
Right x -> case x of
113+
Left _ -> error "Impossible in typeOf, please report."
114+
Right y -> y
115+
116+
checkDoms
117+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
118+
=> Collage var ty sym en fk att gen sk
119+
-> Err ()
120+
checkDoms col = do
121+
mapM_ f $ Map.elems $ csyms col
122+
mapM_ g $ Map.elems $ cfks col
123+
mapM_ h $ Map.elems $ catts col
124+
mapM_ isEn $ Map.elems $ cgens col
125+
mapM_ isTy $ Map.elems $ csks col
126+
where
127+
f (t1,t2) = do { mapM_ isTy t1 ; isTy t2 }
128+
g (e1,e2) = do { isEn e1 ; isEn e2 }
129+
h (e ,t ) = do { isEn e ; isTy t }
130+
isEn x = if Set.member x $ cens col
131+
then pure ()
132+
else Left $ "Not an entity: " ++ show x
133+
isTy x = if Set.member x $ ctys col
134+
then pure ()
135+
else Left $ "Not a type: " ++ show x
136+
137+
typeOfCol
138+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
139+
=> Collage var ty sym en fk att gen sk
140+
-> Err ()
141+
typeOfCol col = do
142+
checkDoms col
143+
mapM_ (typeOfEq' col) $ Set.toList $ ceqs col
144+
145+
--------------------------------------------------------------------------------
146+
147+
typeOf'
148+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
149+
=> Collage var ty sym en fk att gen sk
150+
-> Ctx var (ty + en)
151+
-> Term var ty sym en fk att gen sk
152+
-> Err (ty + en)
153+
typeOf' _ ctx (Var v) = note ("Unbound variable: " ++ show v) $ Map.lookup v ctx
154+
typeOf' col _ (Gen g) = case Map.lookup g $ cgens col of
155+
Nothing -> Left $ "Unknown generator: " ++ show g
156+
Just t -> Right $ Right t
157+
typeOf' col _ (Sk s) = case Map.lookup s $ csks col of
158+
Nothing -> Left $ "Unknown labelled null: " ++ show s
159+
Just t -> Right $ Left t
160+
typeOf' col ctx xx@(Fk f a) = case Map.lookup f $ cfks col of
161+
Nothing -> Left $ "Unknown foreign key: " ++ show f
162+
Just (s, t) -> do s' <- typeOf' col ctx a
163+
if (Right s) == s' then pure $ Right t else Left $ "Expected argument to have entity " ++
164+
show s ++ " but given " ++ show s' ++ " in " ++ (show xx)
165+
typeOf' col ctx xx@(Att f a) = case Map.lookup f $ catts col of
166+
Nothing -> Left $ "Unknown attribute: " ++ show f
167+
Just (s, t) -> do s' <- typeOf' col ctx a
168+
if (Right s) == s' then pure $ Left t else Left $ "Expected argument to have entity " ++
169+
show s ++ " but given " ++ show s' ++ " in " ++ (show xx)
170+
typeOf' col ctx xx@(Sym f a) = case Map.lookup f $ csyms col of
171+
Nothing -> Left $ "Unknown function symbol: " ++ show f
172+
Just (s, t) -> do s' <- mapM (typeOf' col ctx) a
173+
if length s' == length s
174+
then if (Left <$> s) == s'
175+
then pure $ Left t
176+
else Left $ "Expected arguments to have types " ++
177+
show s ++ " but given " ++ show s' ++ " in " ++ (show $ xx)
178+
else Left $ "Expected argument to have arity " ++
179+
show (length s) ++ " but given " ++ show (length s') ++ " in " ++ (show $ xx)
180+
181+
typeOfEq'
182+
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
183+
=> Collage var ty sym en fk att gen sk
184+
-> (Ctx var (ty + en), EQ var ty sym en fk att gen sk)
185+
-> Err (ty + en)
186+
typeOfEq' col (ctx, EQ (lhs, rhs)) = do
187+
lhs' <- typeOf' col ctx lhs
188+
rhs' <- typeOf' col ctx rhs
189+
if lhs' == rhs'
190+
then Right lhs'
191+
else Left $ "Equation lhs has type " ++ show lhs' ++ " but rhs has type " ++ show rhs'
192+
193+
--------------------------------------------------------------------------------
194+
195+
-- | Initialize a mapping of sorts to bools for sort inhabition check.
196+
initGround :: (Ord ty, Ord en) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool)
197+
initGround col = (me', mt')
198+
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
201+
me' = Prelude.foldr (\(_, en) m -> Map.insert en True m) me $ Map.toList $ cgens col
202+
mt' = Prelude.foldr (\(_, ty) m -> Map.insert ty True m) mt $ Map.toList $ csks col
203+
204+
-- | Applies one layer of symbols to the sort to boolean inhabitation map.
205+
closeGround :: (Ord ty, Ord en) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool) -> (Map en Bool, Map ty Bool)
206+
closeGround col (me, mt) = (me', mt'')
207+
where
208+
mt''= Prelude.foldr (\(_, (tys,ty)) m -> if and ((!) mt' <$> tys) then Map.insert ty True m else m) mt' $ Map.toList $ csyms col
209+
mt' = Prelude.foldr (\(_, (en, ty)) m -> if (!) me' en then Map.insert ty True m else m) mt $ Map.toList $ catts col
210+
me' = Prelude.foldr (\(_, (en, _ )) m -> if (!) me en then Map.insert en True m else m) me $ Map.toList $ cfks col
211+
212+
-- | Does a fixed point of closeGround.
213+
iterGround :: (MultiTyMap '[Show, Ord, NFData] '[ty, en]) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool) -> (Map en Bool, Map ty Bool)
214+
iterGround col r = if r == r' then r else iterGround col r'
215+
where r' = closeGround col r
216+
217+
-- | Gets the inhabitation map for the sorts of a collage.
218+
computeGround :: (MultiTyMap '[Show, Ord, NFData] '[ty, en]) => Collage var ty sym en fk att gen sk -> (Map en Bool, Map ty Bool)
219+
computeGround col = iterGround col $ initGround col
220+
221+
-- | True iff all sorts in a collage are inhabited.
222+
allSortsInhabited :: (MultiTyMap '[Show, Ord, NFData] '[ty, en]) => Collage var ty sym en fk att gen sk -> Bool
223+
allSortsInhabited col = t && f
224+
where (me, mt) = computeGround col
225+
t = and $ Map.elems me
226+
f = and $ Map.elems mt

‎src/Language/CQL/Instance.hs

+1
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ import Data.Set (Set)
4949
import qualified Data.Set as Set
5050
import Data.Typeable hiding (typeOf)
5151
import Data.Void
52+
import Language.CQL.Collage (Collage(..), attsFrom, fksFrom, typeOf, typeOfCol)
5253
import Language.CQL.Common (elem', intercalate, fromListAccum, mapl, section, sepTup, toMapSafely, Deps(..), Err, Kind(INSTANCE), MultiTyMap, TyMap, type (+))
5354
import Language.CQL.Mapping as Mapping
5455
import Language.CQL.Options

‎src/Language/CQL/Morphism.hs

+2-1
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,9 @@ import Data.Map.Strict as Map hiding (foldr, size)
4444
import Data.Maybe
4545
import Data.Set as Set hiding (foldr, size)
4646
import Data.Void
47+
import Language.CQL.Collage (Collage(..))
4748
import Language.CQL.Common
48-
import Language.CQL.Term (Collage(..), Ctx, Term(..), EQ(..), subst, upp)
49+
import Language.CQL.Term (Ctx, Term(..), EQ(..), subst, upp)
4950
import Prelude hiding (EQ)
5051

5152

‎src/Language/CQL/Prover.hs

+5-3
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,8 @@ import Data.Rewriting.Rules as Rs
4747
import Data.Rewriting.Term as T
4848
import Data.Set as Set
4949
import Language.CQL.Common
50+
import Language.CQL.Collage as Collage (simplify)
51+
import Language.CQL.Collage
5052
import Language.CQL.Options as O hiding (Prover)
5153
import Language.CQL.Term as S
5254
import Prelude hiding (EQ)
@@ -130,7 +132,7 @@ orthProver col ops = if isDecreasing eqs1 || allow_nonTerm
130132
else Left $ "Rewriting Error: not orthogonal. Pairs are " ++ show (findCps eqs2)
131133
else Left "Rewriting Error: not size decreasing"
132134
where
133-
(col', f) = simplifyCol col
135+
(col', f) = Collage.simplify col
134136

135137
p _ (EQ (lhs', rhs')) = nf (convert' lhs') == nf (convert' rhs')
136138

@@ -272,7 +274,7 @@ kbProver col ops = if allSortsInhabited col || allow_empty
272274
in pure $ Prover col p'
273275
else Left "Completion Error: contains uninhabited sorts"
274276
where
275-
(col', f) = simplifyCol col
277+
(col', f) = Collage.simplify col
276278
p ctx (EQ (lhs', rhs')) = normaliseTerm (completed ctx lhs' rhs') (convert col ctx lhs') == normaliseTerm (completed ctx lhs' rhs') (convert col ctx rhs')
277279
completed g l r = completePure defaultConfig $ addGoal defaultConfig (initState col') (toGoal g l r)
278280
allow_empty = bOps ops Allow_Empty_Sorts_Unsafe
@@ -297,7 +299,7 @@ congProver col = if eqsAreGround col'
297299
hidden = decide rules'
298300
rules' = fmap (\(_, EQ (l, r)) -> (convertCong l, convertCong r)) $ Set.toList $ ceqs col
299301
doProof l r = hidden (convertCong l) (convertCong r)
300-
(col', f) = simplifyCol col
302+
(col', f) = Collage.simplify col
301303

302304
convertCong
303305
:: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])

‎src/Language/CQL/Schema.hs

+1
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ import Data.Maybe
4545
import Data.Set as Set
4646
import Data.Typeable
4747
import Data.Void
48+
import Language.CQL.Collage (Collage(..), typeOfCol)
4849
import Language.CQL.Common
4950
import Language.CQL.Options
5051
import Language.CQL.Prover

0 commit comments

Comments
 (0)