Skip to content

Commit

Permalink
Rename Morphism-related functions for clarity. #148
Browse files Browse the repository at this point in the history
  • Loading branch information
@epost
epost committed Aug 14, 2019
1 parent 9690d64 commit bd16d92
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 32 deletions.
14 changes: 7 additions & 7 deletions src/Language/CQL/Mapping.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ import qualified Data.Set as Set
import Data.Typeable
import Data.Void
import Language.CQL.Common
import Language.CQL.Morphism (Morphism(..), trans, trans', typeOfMor)
import Language.CQL.Morphism (Morphism(..), translate, translate', typeOfMor)
import Language.CQL.Schema as Schema
import Language.CQL.Term
import Prelude hiding (EQ)
Expand Down Expand Up @@ -125,16 +125,16 @@ validateMapping m@(Mapping src' dst' ens' _ _) = do
where
validateObsEq :: (en, EQ () ty sym en fk att Void Void) -> Err ()
validateObsEq (enx, EQ (l,r)) = let
l' = trans (mapToMor m) l
r' = trans (mapToMor m) r :: Term () ty sym en' fk' att' Void Void
l' = translate (mapToMor m) l
r' = translate (mapToMor m) r :: Term () ty sym en' fk' att' Void Void
en' = ens' ! enx
in if eq dst' en' (EQ (l', r'))
then pure ()
else Left $ show l ++ " = " ++ show r ++ " translates to " ++ show l' ++ " = " ++ show r' ++ " which is not provable"
validatePathEq :: (en, EQ () Void Void en fk Void Void Void) -> Err ()
validatePathEq (enx, EQ (l,r)) = let
l' = trans' (mapToMor m) l
r' = trans' (mapToMor m) r :: Term () Void Void en' fk' Void Void Void
l' = translate' (mapToMor m) l
r' = translate' (mapToMor m) r :: Term () Void Void en' fk' Void Void Void
en' = ens' ! enx
in if eq dst' en' (EQ (upp l', upp r'))
then pure ()
Expand Down Expand Up @@ -187,8 +187,8 @@ composeMapping
composeMapping (Mapping s t e f a) m2@(Mapping s' t' e' _ _) =
if t == s'
then let e'' = Map.fromList [ (k, e' ! v) | (k, v) <- Map.toList e ]
f'' = Map.fromList [ (k, trans' (mapToMor m2) v) | (k, v) <- Map.toList f ]
a'' = Map.fromList [ (k, trans (mapToMor m2) v) | (k, v) <- Map.toList a ]
f'' = Map.fromList [ (k, translate' (mapToMor m2) v) | (k, v) <- Map.toList f ]
a'' = Map.fromList [ (k, translate (mapToMor m2) v) | (k, v) <- Map.toList a ]
in pure $ Mapping s t' e'' f'' a''
else Left $ "Source and target schemas do not match: " ++ show t ++ " and " ++ show s'

Expand Down
30 changes: 15 additions & 15 deletions src/Language/CQL/Morphism.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,39 +79,39 @@ checkDoms' mor = do
s sk = if Map.member sk $ m_sks mor then pure () else Left $ "No sk mapping for " ++ show sk

-- | Translates a term along a morphism.
trans'
translate'
:: forall var var' ty sym en fk att gen sk en' fk' att' gen' sk'
. TyMap Ord '[gen, sk, fk, var, att, var']
=> Morphism var ty sym en fk att gen sk en' fk' att' gen' sk'
-> Term var' Void Void en fk Void gen Void
-> Term var' Void Void en' fk' Void gen' Void
trans' _ (Var x) = Var x
trans' mor (Fk f a) = let
x = trans' mor a :: Term var' Void Void en' fk' Void gen' Void
y = upp (m_fks mor ! f) :: Term () Void Void en' fk' Void gen' Void
translate' _ (Var x) = Var x
translate' mor (Fk f a) = let
x = translate' mor a :: Term var' Void Void en' fk' Void gen' Void
y = upp (m_fks mor ! f) :: Term () Void Void en' fk' Void gen' Void
in subst y x
trans' mor (Gen g) = upp $ m_gens mor ! g
trans' _ (Sym _ _) = undefined
trans' _ (Att _ _) = undefined
trans' _ (Sk _ ) = undefined
translate' mor (Gen g) = upp $ m_gens mor ! g
translate' _ (Sym _ _) = undefined
translate' _ (Att _ _) = undefined
translate' _ (Sk _ ) = undefined

-- | Translates a term along a morphism.
trans
translate
:: forall var var' ty sym en fk att gen sk en' fk' att' gen' sk'
. TyMap Ord '[gen, sk, fk, var, att, var']
=> Morphism var ty sym en fk att gen sk en' fk' att' gen' sk'
-> Term var' ty sym en fk att gen sk
-> Term var' ty sym en' fk' att' gen' sk'
trans mor term = case term of
translate mor term = case term of
Var x -> Var x
Sym f xs -> Sym f $ Prelude.map (trans mor) xs
Sym f xs -> Sym f (translate mor <$> xs)
Gen g -> upp $ m_gens mor ! g
Sk s -> upp $ m_sks mor ! s
Att f a -> subst (upp $ (m_atts mor) ! f) $ trans mor a
Att f a -> subst (upp $ m_atts mor ! f) $ translate mor a
Fk f a -> subst (upp y) x
where
x = trans mor a :: Term var' ty sym en' fk' att' gen' sk'
y = m_fks mor ! f :: Term () Void Void en' fk' Void Void Void
x = translate mor a :: Term var' ty sym en' fk' att' gen' sk'
y = m_fks mor ! f :: Term () Void Void en' fk' Void Void Void


typeOfMor
Expand Down
20 changes: 10 additions & 10 deletions src/Language/CQL/Transform.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ import Data.Void
import Language.CQL.Common
import Language.CQL.Instance as I
import Language.CQL.Mapping as M
import Language.CQL.Morphism (Morphism(..), trans, trans', typeOfMor)
import Language.CQL.Morphism (Morphism(..), translate, translate', typeOfMor)
import Language.CQL.Options
import Language.CQL.Query
import Language.CQL.Schema as S
Expand Down Expand Up @@ -95,7 +95,7 @@ typecheckTransform
:: (MultiTyMap '[Show, Ord, Typeable, NFData] '[sym, en, fk, att], MultiTyMap '[Show, Ord, NFData] '[var, ty, gen, sk, x, y, gen', sk', x', y'])
=> Transform var ty sym en fk att gen sk x y gen' sk' x' y'
-> Err ()
typecheckTransform m = typeOfMor $ transToMor m
typecheckTransform m = typeOfMor $ toMorphism m

validateTransform
:: forall var ty sym en fk att gen sk x y gen' sk' x' y' -- need forall
Expand All @@ -107,17 +107,17 @@ validateTransform m@(Transform src' dst' _ _) =
where
f :: (EQ Void ty sym en fk att gen sk) -> Err () -- need type signature
f (EQ (l, r)) = let
l' = trans (transToMor m) l
r' = trans (transToMor m) r :: Term Void ty sym en fk att gen' sk'
l' = translate (toMorphism m) l
r' = translate (toMorphism m) r :: Term Void ty sym en fk att gen' sk'
in if dp dst' (EQ (l', r'))
then pure ()
else Left $ show l ++ " = " ++ show r ++ " translates to " ++ show l' ++ " = " ++ show r' ++ " which is not provable"

transToMor
toMorphism
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, gen, sk, en', fk', att', gen', sk'])
=> Transform var ty sym en' fk' att' gen sk x1 y1 gen' sk' x2 y2
-> Morphism var ty sym en' fk' att' gen sk en' fk' att' gen' sk'
transToMor (Transform src' dst' gens' sks') =
toMorphism (Transform src' dst' gens' sks') =
Morphism (presToCol (I.schema src') (pres src'))
(presToCol (I.schema src') (pres dst'))
ens0 fks0 atts0 gens' sks'
Expand Down Expand Up @@ -195,8 +195,8 @@ composeTransform (Transform s t f a) m2@(Transform s' t' _ _)
| t == s' = pure $ Transform s t' f'' a''
| otherwise = Left $ "Source and target instances do not match: " ++ show t ++ " and " ++ show s'
where
f'' = Map.fromList [ (k, trans' (transToMor m2) v) | (k, v) <- Map.toList f ]
a'' = Map.fromList [ (k, trans (transToMor m2) v) | (k, v) <- Map.toList a ]
f'' = Map.fromList [ (k, translate' (toMorphism m2) v) | (k, v) <- Map.toList f ]
a'' = Map.fromList [ (k, translate (toMorphism m2) v) | (k, v) <- Map.toList a ]

evalSigmaTrans
:: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk, en', fk', att', gen', sk', x', y'])
Expand Down Expand Up @@ -252,8 +252,8 @@ evalDeltaTrans m h o = do
j <- evalDeltaInst m (dstT h) o
pure $ Transform i j (gens' i) (sks' i)
where
gens' i = mapWithKey (\(_,x) en' -> Gen (en', nf (algebra $ dstT h) $ trans' (transToMor h) $ repr (algebra $ srcT h) x)) $ I.gens $ pres i
sks' i = mapWithKey (\y _ -> upp $ nf'' (algebra $ dstT h) $ trans (transToMor h) $ repr' (algebra $ srcT h) y) $ I.sks $ pres i
gens' i = mapWithKey (\(_,x) en' -> Gen (en', nf (algebra $ dstT h) $ translate' (toMorphism h) $ repr (algebra $ srcT h) x)) $ I.gens $ pres i
sks' i = mapWithKey (\y _ -> upp $ nf'' (algebra $ dstT h) $ translate (toMorphism h) $ repr' (algebra $ srcT h) y) $ I.sks $ pres i

---------------------------------------------------------------------------------------------------------
-- Raw literals
Expand Down

0 comments on commit bd16d92

Please sign in to comment.