Skip to content

Commit b155e73

Browse files
marcoshmarcosh
authored
Merge pull request #155 from statebox/148/ever-more-cleanup
Ever more refactoring. #148
2 parents d537da6 + cd8a8f9 commit b155e73

File tree

7 files changed

+101
-84
lines changed

7 files changed

+101
-84
lines changed

‎src/Language/CQL/Collage.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ import Data.Map.Strict as Map hiding (foldr, size)
4646
import Data.Set as Set hiding (foldr, size)
4747
import Data.Void
4848
import Language.CQL.Common
49-
import Language.CQL.Term (Ctx, EQ(..), Head(..), Term(..), occsTerm, upp)
49+
import Language.CQL.Term (Ctx, EQ, EQF(..), Head(..), Term(..), occsTerm, upp)
5050
import qualified Language.CQL.Term as T (simplifyTheory)
5151
import Prelude hiding (EQ)
5252

‎src/Language/CQL/Instance/Algebra.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ import qualified Data.Set as Set
4949
import Data.Void
5050
import Language.CQL.Common (intercalate, mapl, section, MultiTyMap, TyMap, type (+))
5151
import Language.CQL.Schema as Schema
52-
import Language.CQL.Term (EQ(..), Head(HSk), Term(..), subst, upp, replaceRepeatedly, simplifyTheory)
52+
import Language.CQL.Term (EQ, Head(HSk), Term(..), subst, upp, replaceRepeatedly, simplifyTheory)
5353
import Language.CQL.Typeside as Typeside
5454
import Prelude hiding (EQ)
5555
import qualified Text.Tabular as T

‎src/Language/CQL/Instance/Presentation.hs

+3-2
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,8 @@ import qualified Data.Set as Set
4747
import Data.Void
4848
import Language.CQL.Collage (Collage(..), typeOfCol)
4949
import Language.CQL.Common (Err, MultiTyMap, TyMap, type (+), section, sepTup, intercalate)
50-
import Language.CQL.Schema (Schema, schToCol)
50+
import Language.CQL.Schema (Schema)
51+
import qualified Language.CQL.Schema as Schema (toCollage)
5152
import Language.CQL.Term as Term
5253
import Prelude hiding (EQ)
5354

@@ -88,6 +89,6 @@ toCollage
8889
toCollage sch (Presentation gens' sks' eqs') =
8990
Collage (Set.union e1 e2) (ctys schcol) (cens schcol) (csyms schcol) (cfks schcol) (catts schcol) gens' sks'
9091
where
91-
schcol = schToCol sch
92+
schcol = Schema.toCollage sch
9293
e1 = Set.map (\( EQ (l,r)) -> (Map.empty, EQ (upp l, upp r))) $ eqs'
9394
e2 = Set.map (\(g, EQ (l,r)) -> (g, EQ (upp l, upp r))) $ ceqs schcol

‎src/Language/CQL/Mapping.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ toMorphism
105105
:: MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, en', fk', att']
106106
=> Mapping var ty sym en fk att en' fk' att'
107107
-> Morphism var ty sym en fk att Void Void en' fk' att' Void Void
108-
toMorphism (Mapping src' dst' ens' fks' atts') = Morphism (schToCol src') (schToCol dst') ens' fks' atts' Map.empty Map.empty
108+
toMorphism (Mapping src' dst' ens' fks' atts') = Morphism (Schema.toCollage src') (Schema.toCollage dst') ens' fks' atts' Map.empty Map.empty
109109

110110
-- | Checks well-typedness of underlying theory.
111111
typecheckMapping

‎src/Language/CQL/Morphism.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ import Data.Set as Set hiding (foldr, size)
4646
import Data.Void
4747
import Language.CQL.Collage (Collage(..))
4848
import Language.CQL.Common
49-
import Language.CQL.Term (Ctx, Term(..), EQ(..), subst, upp)
49+
import Language.CQL.Term (Ctx, Term(..), EQ, EQF(..), subst, upp)
5050
import Prelude hiding (EQ)
5151

5252
-- | A morphism between 'Collage's.

‎src/Language/CQL/Schema.hs

+24-17
Original file line numberDiff line numberDiff line change
@@ -38,13 +38,17 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.
3838
{-# LANGUAGE UndecidableInstances #-}
3939

4040
module Language.CQL.Schema where
41+
42+
import Control.Arrow ((***))
4143
import Control.DeepSeq
44+
import Data.Bifunctor (second)
4245
import Data.List (nub)
4346
import Data.Map.Strict as Map
4447
import Data.Maybe
4548
import Data.Set as Set
4649
import Data.Typeable
4750
import Data.Void
51+
4852
import Language.CQL.Collage (Collage(..), typeOfCol)
4953
import Language.CQL.Common
5054
import Language.CQL.Options
@@ -88,36 +92,39 @@ instance TyMap Show '[var, ty, sym, en, fk, att]
8892
, section "observation_equations " $ unlines $ eqs'' obs_eqs'
8993
]
9094
where
91-
fks'' = (\(k,(s,t)) -> show k ++ " : " ++ show s ++ " -> " ++ show t) <$> Map.toList fks'
92-
atts'' = (\(k,(s,t)) -> show k ++ " : " ++ show s ++ " -> " ++ show t) <$> Map.toList atts'
93-
eqs'' x = (\(en,EQ (l,r)) -> "forall x : " ++ show en ++ " . " ++ show (mapVar "x" l) ++ " = " ++ show (mapVar "x" r)) <$> Set.toList x
95+
fks'' = (\(k,(s,t)) -> show k ++ " : " ++ show s ++ " -> " ++ show t) <$> Map.toList fks'
96+
atts'' = (\(k,(s,t)) -> show k ++ " : " ++ show s ++ " -> " ++ show t) <$> Map.toList atts'
97+
eqs'' x = (\(en,EQ (l,r)) -> "forall x : " ++ show en ++ " . " ++ show (mapTermVar (const "x") l) ++ " = " ++ show (mapTermVar (const "x") r)) <$> Set.toList x
9498

9599
-- | Checks that the underlying theory is well-sorted.
96100
-- I.e. rule out "1" = one kind of errors.
97101
typecheckSchema
98102
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att])
99103
=> Schema var ty sym en fk att
100104
-> Err ()
101-
typecheckSchema t = typeOfCol $ schToCol t
105+
typecheckSchema = typeOfCol . toCollage
102106

103107
-- | Converts a schema to a collage.
104-
schToCol
108+
toCollage
105109
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att])
106-
=> Schema var ty sym en fk att
110+
=> Schema var ty sym en fk att
107111
-> Collage (() + var) ty sym en fk att Void Void
108-
schToCol (Schema ts ens' fks' atts' path_eqs' obs_eqs' _) =
109-
Collage (Set.union e3 $ Set.union e1 e2) (ctys tscol)
110-
ens' (csyms tscol) fks' atts' Map.empty Map.empty
112+
toCollage (Schema ts ens' fks' atts' path_eqs' obs_eqs' _) =
113+
Collage (eqs1 <> eqs2 <> eqs3) (ctys tscol) ens' (csyms tscol) fks' atts' Map.empty Map.empty
111114
where
112115
tscol = tsToCol ts
113-
e1 = Set.map (\(en, EQ (l,r))->(Map.fromList [(Left (),Right en)], EQ (upp l, upp r))) path_eqs'
114-
e2 = Set.map (\(en, EQ (l,r))->(Map.fromList [(Left (),Right en)], EQ (upp l, upp r))) obs_eqs'
115-
e3 = Set.map (\(g,EQ (l,r))->(up1Ctx g, EQ (upp l, upp r))) $ ceqs tscol
116116

117-
up1Ctx :: (Ord var) => Ctx var (ty+Void) -> Ctx (()+var) (ty+x)
118-
up1Ctx g = Map.map (\x -> case x of
119-
Left ty -> Left ty
120-
Right v -> absurd v) $ Map.mapKeys Right g
117+
eqs1 = Set.map (unitCtx *** fmap upp) path_eqs'
118+
eqs2 = Set.map (unitCtx *** fmap upp) obs_eqs'
119+
eqs3 = Set.map (up1Ctx *** fmap upp) (ceqs tscol)
120+
121+
unitCtx en = Map.singleton (Left ()) (Right en)
122+
123+
up1Ctx
124+
:: (Ord var)
125+
=> Ctx var (ty+Void)
126+
-> Ctx (()+var) (ty+x)
127+
up1Ctx = (second absurd <$>) . Map.mapKeys Right
121128

122129
typesideToSchema :: Typeside var ty sym -> Schema var ty sym Void Void Void
123130
typesideToSchema ts'' = Schema ts'' Set.empty Map.empty Map.empty Set.empty Set.empty $ \x _ -> absurd x
@@ -306,7 +313,7 @@ evalSchemaRaw ops ty t a' = do
306313
(a :: [Schema var ty sym En Fk Att]) <- doImports a'
307314
r <- evalSchemaRaw' ty t a
308315
o <- toOptions ops $ schraw_options t
309-
p <- createProver (schToCol r) o
316+
p <- createProver (toCollage r) o
310317
pure $ SchemaEx $ Schema ty (ens r) (fks r) (atts r) (path_eqs r) (obs_eqs r) (mkProver p)
311318
where
312319
mkProver p en (EQ (l,r)) = prove p (Map.fromList [(Left (),Right en)]) (EQ (upp l, upp r))

‎src/Language/CQL/Term.hs

+70-61
Original file line numberDiff line numberDiff line change
@@ -49,14 +49,6 @@ import Data.Void
4949
import Language.CQL.Common
5050
import Prelude hiding (EQ)
5151

52-
data RawTerm = RawApp String [RawTerm]
53-
deriving Eq
54-
55-
instance Show RawTerm where
56-
show (RawApp sym az) = show sym ++ "(" ++ (intercalate "," . fmap show $ az) ++ ")"
57-
58-
--------------------------------------------------------------------------------------------
59-
-- Terms
6052

6153
data Term var ty sym en fk att gen sk
6254
-- | Variable.
@@ -86,48 +78,40 @@ data Head ty sym en fk att gen sk
8678
| HSk sk
8779
deriving (Eq, Ord)
8880

89-
instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] =>
90-
NFData (Term var ty sym en fk att gen sk) where
91-
rnf x = case x of
92-
Var v -> rnf v
93-
Sym f a -> let _ = rnf f in rnf a
94-
Fk f a -> let _ = rnf f in rnf a
95-
Att f a -> let _ = rnf f in rnf a
96-
Gen a -> rnf a
97-
Sk a -> rnf a
98-
99-
instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] =>
100-
NFData (EQ var ty sym en fk att gen sk) where
101-
rnf (EQ (x, y)) = deepseq x $ rnf y
102-
103-
104-
instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] =>
105-
Show (Term var ty sym en fk att gen sk)
106-
where
107-
show x = case x of
108-
Var v -> show' v
109-
Gen g -> show' g
110-
Sk s -> show' s
111-
Fk fk a -> show' a ++ "." ++ show' fk
112-
Att att a -> show' a ++ "." ++ show' att
113-
Sym sym [] -> show' sym
114-
Sym sym az -> show' sym ++ "(" ++ (intercalate "," . fmap show' $ az) ++ ")"
115-
where
116-
117-
show' :: Show a => a -> String
118-
show' = dropQuotes . show
81+
deriving instance TyMap Eq '[var, sym, fk, att, gen, sk] => Eq (Term var ty sym en fk att gen sk)
11982

12083
deriving instance TyMap Ord '[var, ty, sym, en, fk, att, gen, sk] => Ord (Term var ty sym en fk att gen sk)
12184

122-
instance (Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk)
123-
=> Show (Head ty sym en fk att gen sk) where
85+
instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] => NFData (Term var ty sym en fk att gen sk) where
86+
rnf x = case x of
87+
Var v -> rnf v
88+
Sym f a -> let _ = rnf f in rnf a
89+
Fk f a -> let _ = rnf f in rnf a
90+
Att f a -> let _ = rnf f in rnf a
91+
Gen a -> rnf a
92+
Sk a -> rnf a
93+
94+
instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (Term var ty sym en fk att gen sk) where
95+
show x = case x of
96+
Var v -> show' v
97+
Gen g -> show' g
98+
Sk s -> show' s
99+
Fk fk a -> show' a ++ "." ++ show' fk
100+
Att att a -> show' a ++ "." ++ show' att
101+
Sym sym [] -> show' sym
102+
Sym sym az -> show' sym ++ "(" ++ (intercalate "," . fmap show' $ az) ++ ")"
103+
104+
instance TyMap Show '[ty, sym, en, fk, att, gen, sk] => Show (Head ty sym en fk att gen sk) where
124105
show x = case x of
125106
HSym sym -> show' sym
126107
HFk fk -> show' fk
127108
HAtt att -> show' att
128109
HGen gen -> show' gen
129110
HSk sk -> show' sk
130111

112+
show' :: Show a => a -> String
113+
show' = dropQuotes . show
114+
131115
-- | Maps functions through a term.
132116
mapTerm
133117
:: (var -> var')
@@ -150,8 +134,11 @@ mapTerm v t r e f a g s x = case x of
150134
where
151135
mt = mapTerm v t r e f a g s
152136

153-
mapVar :: var -> Term () ty sym en fk att gen sk -> Term var ty sym en fk att gen sk
154-
mapVar v = mapTerm (const v) id id id id id id id
137+
mapTermVar
138+
:: (var -> var')
139+
-> Term var ty sym en fk att gen sk
140+
-> Term var' ty sym en fk att gen sk
141+
mapTermVar f = mapTerm f id id id id id id id
155142

156143
-- | The number of variable and symbol occurrences in a term.
157144
size :: Term var ty sym en fk att gen sk -> Integer
@@ -208,7 +195,7 @@ hasTypeType'' t = case t of
208195
Fk _ _ -> False
209196

210197
----------------------------------------------------------------------------------------------------------
211-
-- Substitution and simplification of theories
198+
-- Substitution and simplification on terms
212199

213200
-- | Experimental
214201
subst2
@@ -268,6 +255,41 @@ occurs h x = case x of
268255
Att h' a -> h == HAtt h' || occurs h a
269256
Sym h' as -> h == HSym h' || any (occurs h) as
270257

258+
259+
--------------------------------------------------------------------------------------------------------------------
260+
-- Equality, especially on Terms
261+
262+
-- | A value of this type means the lhs and rhs are equal.
263+
-- One reason for its existence is to allow pretty-printing.
264+
type EQ var ty sym en fk att gen sk = EQF (Term var ty sym en fk att gen sk)
265+
266+
newtype EQF a = EQ (a, a)
267+
268+
instance Functor EQF where
269+
fmap f (EQ (l, r)) = EQ (f l, f r)
270+
271+
instance (Show a) => Show (EQF a) where
272+
show (EQ (lhs, rhs)) = show lhs ++ " = " ++ show rhs
273+
274+
deriving instance (Ord a) => Ord (EQF a)
275+
276+
deriving instance (Eq a) => Eq (EQF a)
277+
278+
instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk] => NFData (EQ var ty sym en fk att gen sk) where
279+
rnf (EQ (x, y)) = deepseq x $ rnf y
280+
281+
hasTypeType' :: EQ Void ty sym en fk att gen sk -> Bool
282+
hasTypeType' (EQ (lhs, _)) = hasTypeType lhs
283+
284+
285+
--------------------------------------------------------------------------------------------------------------------
286+
-- Theories
287+
288+
type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
289+
290+
-- TODO wrap Map class to throw an error (or do something less ad hoc) if a key is ever inserted twice
291+
type Ctx k v = Map k v
292+
271293
-- | If there is one, finds an equation of the form @empty |- gen/sk = term@,
272294
-- where @gen@ does not occur in @term@.
273295
findSimplifiableEq
@@ -367,23 +389,10 @@ instance Up x (x + y) where
367389
instance Up y (x + y) where
368390
upgr = Right
369391

370-
--------------------------------------------------------------------------------------------------------------------
371-
-- Theories
372-
373-
type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en fk att gen sk)
374-
375-
-- TODO wrap Map class to throw an error (or do something less ad hoc) if a key is ever put twice
376-
type Ctx k v = Map k v
377-
378-
-- Our own pair type for pretty printing purposes
379-
-- | This type indicates that the two terms are equal.
380-
newtype EQ var ty sym en fk att gen sk
381-
= EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord, Eq)
382-
383-
instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (EQ var ty sym en fk att gen sk) where
384-
show (EQ (lhs,rhs)) = show lhs ++ " = " ++ show rhs
392+
--------------------------------------------------------------------------------
385393

386-
deriving instance TyMap Eq '[var, sym, fk, att, gen, sk] => Eq (Term var ty sym en fk att gen sk)
394+
data RawTerm = RawApp String [RawTerm]
395+
deriving Eq
387396

388-
hasTypeType' :: EQ Void ty sym en fk att gen sk -> Bool
389-
hasTypeType' (EQ (lhs, _)) = hasTypeType lhs
397+
instance Show RawTerm where
398+
show (RawApp sym az) = show sym ++ "(" ++ (intercalate "," . fmap show $ az) ++ ")"

0 commit comments

Comments
 (0)