Skip to content

Commit

Permalink
Misc comments and formatting. #148
Browse files Browse the repository at this point in the history
  • Loading branch information
epost committed Aug 22, 2019
1 parent 0bce9fd commit f882abd
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 28 deletions.
34 changes: 18 additions & 16 deletions src/Language/CQL/Instance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -98,9 +98,9 @@ data InstanceEx :: * where
-> InstanceEx


-- | Converts an algebra into a presentation: adds one equation per fact in the algebra
-- and one generator per element. Presentations in this form are called saturated because
-- they are maximally large without being redundant. @I(fk.x) = I(fk)(I(x))@
-- | Converts an algebra into a presentation: adds one equation per fact in the algebra,
-- and one generator per element. Presentations in this form are called saturated because
-- they are maximally large without being redundant. @I(fk.x) = I(fk)(I(x))@
algebraToPresentation :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Ord y, Ord x)
=> Algebra var ty sym en fk att gen sk x y
-> Presentation var ty sym en fk att x y
Expand Down Expand Up @@ -240,7 +240,7 @@ initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra
nf'''' (Left g) = Sk $ MkTalgGen $ Left g
nf'''' (Right (gt, att)) = Sk $ MkTalgGen $ Right (gt, att)

--repr'''' :: TalgGen en fk att gen sk -> Term Void ty sym en fk att gen sk
repr'''' :: TalgGen en fk att gen sk -> Term Void ty sym en fk att gen sk
repr'''' (MkTalgGen (Left g)) = Sk g
repr'''' (MkTalgGen (Right (x, att))) = Att att $ upp x

Expand Down Expand Up @@ -417,12 +417,12 @@ evalInstanceRaw' sch (InstExpRaw' _ gens0 eqs' _ _) is = do
rest <- transEq gens' sks' eqs''
pure $ Set.insert (EQ (lhs', rhs')) rest

--transPath :: forall en fk gen . [String] -> RawTerm -> Err (Term Void Void Void en fk Void Gen Void)
transPath :: forall var' ty' sym' en' att'. [String] -> RawTerm -> Err (Term var' ty' sym' en' fk att' String Sk)
transPath gens' (RawApp x []) | elem x gens' = pure $ Gen x
transPath gens' (RawApp x [a]) | elem' x (Map.keys $ sch_fks sch) = Fk (fromJust $ cast x) <$> transPath gens' a
transPath _ x = Left $ "cannot type " ++ show x

--transTerm :: forall ty sym en fk att Gen Sk . [String] -> [String] -> RawTerm -> Err (Term Void ty sym en fk att Gen Sk)
transTerm :: [String] -> [String] -> RawTerm -> Err (Term Void ty sym en fk att Gen Sk)
transTerm gens' _ (RawApp x []) | elem x gens' = pure $ Gen x
transTerm _ sks' (RawApp x []) | elem x sks' = pure $ Sk x
transTerm gens' _ (RawApp x [a]) | elem' x (Map.keys $ sch_fks sch) = Fk (fromJust $ cast x) <$> transPath gens' a
Expand Down Expand Up @@ -462,22 +462,26 @@ evalInstanceRaw ops ty' t is = do

-- | The empty instance on a schema has no data, so the types of its generators and carriers are 'Void'.
emptyInstance :: Schema var ty sym en fk att -> Instance var ty sym en fk att Void Void Void Void
emptyInstance ts'' = Instance ts''
emptyInstance ts'' =
Instance
ts''
(Presentation Map.empty Map.empty Set.empty)
(const undefined)
(Algebra ts''
(const Set.empty) (const undefined) (const undefined) (const undefined)
(const Set.empty) (const undefined) (const undefined)
Set.empty)

-- | Pivots an instance. The returned schema will not have strings as fks etc, so it will be impossible to write a literal on it, at least for now.
-- (Java CQL hacks around this by landing on String.)
pivot :: forall var ty sym en fk att gen sk x y
-- | Pivot an instance. The returned schema will not have strings as fks etc, so it will be impossible to write a literal on it, at least for now.
-- (Java CQL hacks around this by landing on String.)
pivot
:: forall var ty sym en fk att gen sk x y
. (MultiTyMap '[Show, Ord, Typeable] '[var, ty, sym, en, fk, att, gen, sk, x, y])
=> Instance var ty sym en fk att gen sk x y
-> (Schema var ty sym (x, en) (x, fk) (x, att)
, Instance var ty sym (x, en) (x, fk) (x, att) (x, en) y (x, en) y
, Mapping var ty sym (x, en) (x, fk) (x, att) en fk att)
=> Instance var ty sym en fk att gen sk x y
-> ( Schema var ty sym (x, en) (x, fk) (x, att)
, Instance var ty sym (x, en) (x, fk) (x, att) (x, en) y (x, en) y
, Mapping var ty sym (x, en) (x, fk) (x, att) en fk att
)
pivot (Instance sch _ idp (Algebra _ ens _ fk fn tys nnf rep2'' teqs)) = (sch', inst, mapp)
where
sch'_ens = Set.fromList [ (x, en) | en <- Set.toList (Schema.ens sch), x <- Set.toList (ens en)]
Expand Down Expand Up @@ -536,7 +540,6 @@ pivot (Instance sch _ idp (Algebra _ ens _ fk fn tys nnf rep2'' teqs)) = (sch',
Fk (_, f) a -> Fk f $ instToInst a
Gen (x, _) -> upp $ fn x

-- coproducts, etc

---------------------------------------------------------------------------------------------------------------
-- Functorial data migration
Expand All @@ -551,7 +554,6 @@ subs (Mapping _ _ ens' fks' atts') (Presentation gens' sks' eqs') = Presentation
gens'' = Map.map (\k -> ens' ! k) gens'
eqs'' = Set.map (\(EQ (l, r)) -> EQ (changeEn fks' atts' l, changeEn fks' atts' r)) eqs'


changeEn
:: (Ord k1, Ord k2, Eq var)
=> Map k1 (Term () Void Void en1 fk Void Void Void)
Expand Down
5 changes: 2 additions & 3 deletions src/Language/CQL/Instance/Algebra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ data Algebra var ty sym en fk att gen sk x y
instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData x, NFData y)
=> NFData (Algebra var ty sym en fk att gen sk x y)
where
rnf (Algebra s0 e0 nf0 nf02 repr0 ty0 nf1 repr1 eqs1) = deepseq s0 $ f e0 $ deepseq nf0 $ deepseq repr0
$ w ty0 $ deepseq nf1 $ deepseq repr1 $ deepseq nf02 $ rnf eqs1
rnf (Algebra s0 e0 nf0 nf02 repr0 ty0 nf1 repr1 eqs1) =
deepseq s0 $ f e0 $ deepseq nf0 $ deepseq repr0 $ w ty0 $ deepseq nf1 $ deepseq repr1 $ deepseq nf02 $ rnf eqs1
where
f g = deepseq (Set.map (rnf . g) $ Schema.ens s0)
w g = deepseq (Set.map (rnf . g) $ tys (typeside s0))
Expand All @@ -111,7 +111,6 @@ evalSchTerm alg x term = case term of
Sym f as -> Sym f $ fmap (evalSchTerm alg x) as
_ -> error "Impossibility in evalSchTerm, please report. Given a term of non-type sort."


-- | Helper to convert terms in the 'Collage' of entity sort into terms with 'Void's in the attribute etc slots.
-- Morally, 'Collage' should store two or more classes of equation, but having to convert like this is relatively rare.
-- Indeed, 'IP.satisfiesSchema' itself is redundant; a properly functioning CQL would not generate unsatisfying
Expand Down
21 changes: 12 additions & 9 deletions src/Language/CQL/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -268,7 +268,7 @@ occurs h x = case x of
Sym h' as -> h == HSym h' || any (occurs h) as

-- | If there is one, finds an equation of the form empty |- @gen/sk = term@,
-- where @gen@ does not occur in @term@.
-- where @gen@ does not occur in @term@.
findSimplifiableEqs
:: (Eq ty, Eq sym, Eq en, Eq fk, Eq att, Eq gen, Eq sk)
=> Theory var ty sym en fk att gen sk
Expand All @@ -280,13 +280,14 @@ findSimplifiableEqs = procEqs . Set.toList
g (Gen y) t = if occurs (HGen y) t then Nothing else Just (HGen y, t)
g (Sym _ []) _ = Nothing
g _ _ = Nothing
procEqs [] = Nothing

procEqs [] = Nothing
procEqs ((m, _):tl) | not (Map.null m) = procEqs tl
procEqs ((_, EQ (lhs, rhs)):tl) = case g lhs rhs of
Nothing -> case g rhs lhs of
Nothing -> procEqs tl
Just y -> Just y
Just y -> Just y
procEqs ((_, EQ (lhs, rhs)):tl) = case g lhs rhs of
Nothing -> case g rhs lhs of
Nothing -> procEqs tl
Just y -> Just y
Just y -> Just y

-- | Replaces a symbol by a term in a term.
replace'
Expand Down Expand Up @@ -343,7 +344,8 @@ simplifyTheoryStep eqs = case findSimplifiableEqs eqs of
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')
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'
upp (Var v ) = Var $ upgr v
Expand Down Expand Up @@ -374,8 +376,9 @@ type Theory var ty sym en fk att gen sk = Set (Ctx var (ty+en), EQ var ty sym en
type Ctx k v = Map k v

-- Our own pair type for pretty printing purposes
-- | This type indicates that the two terms are equal.
newtype EQ var ty sym en fk att gen sk
= EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord,Eq)
= EQ (Term var ty sym en fk att gen sk, Term var ty sym en fk att gen sk) deriving (Ord, Eq)

instance TyMap Show '[var, ty, sym, en, fk, att, gen, sk] => Show (EQ var ty sym en fk att gen sk) where
show (EQ (lhs,rhs)) = show lhs ++ " = " ++ show rhs
Expand Down

0 comments on commit f882abd

Please sign in to comment.