Skip to content

Commit

Permalink
Improve naming and qualification of Morphism-related functions. #148
Browse files Browse the repository at this point in the history
  • Loading branch information
epost committed Aug 14, 2019
1 parent bd16d92 commit 8cd7f65
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 17 deletions.
23 changes: 12 additions & 11 deletions src/Language/CQL/Mapping.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,8 @@ import qualified Data.Set as Set
import Data.Typeable
import Data.Void
import Language.CQL.Common
import Language.CQL.Morphism (Morphism(..), translate, translate', typeOfMor)
import Language.CQL.Morphism (Morphism(..), translate, translate')
import Language.CQL.Morphism as Morphism (typeOf)
import Language.CQL.Schema as Schema
import Language.CQL.Term
import Prelude hiding (EQ)
Expand Down Expand Up @@ -100,18 +101,18 @@ getFks = fks
getAtts :: Mapping var ty sym en fk att en' fk' att' -> Map att (Term () ty sym en' fk' att' Void Void)
getAtts = atts

mapToMor
toMorphism
:: MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, en', fk', att']
=> Mapping var ty sym en fk att en' fk' att'
-> Morphism var ty sym en fk att Void Void en' fk' att' Void Void
mapToMor (Mapping src' dst' ens' fks' atts') = Morphism (schToCol src') (schToCol dst') ens' fks' atts' Map.empty Map.empty
toMorphism (Mapping src' dst' ens' fks' atts') = Morphism (schToCol src') (schToCol dst') ens' fks' atts' Map.empty Map.empty

-- | Checks well-typedness of underlying theory.
typecheckMapping
:: (MultiTyMap '[Show, Ord, NFData] '[var, ty], MultiTyMap '[Show, Ord, Typeable, NFData] '[sym, en, fk, att, en', fk', att'])
=> Mapping var ty sym en fk att en' fk' att'
-> Err ()
typecheckMapping m = typeOfMor $ mapToMor m
typecheckMapping m = Morphism.typeOf $ toMorphism m

-- | Given @F@ checks that each @S |- p = q -> T |- F p = F q@.
validateMapping
Expand All @@ -125,16 +126,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' = translate (mapToMor m) l
r' = translate (mapToMor m) r :: Term () ty sym en' fk' att' Void Void
l' = translate (toMorphism m) l
r' = translate (toMorphism 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' = translate' (mapToMor m) l
r' = translate' (mapToMor m) r :: Term () Void Void en' fk' Void Void Void
l' = translate' (toMorphism m) l
r' = translate' (toMorphism 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 @@ -186,9 +187,9 @@ composeMapping
-> Err (Mapping var ty sym en fk att en'' fk'' att'')
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, translate' (mapToMor m2) v) | (k, v) <- Map.toList f ]
a'' = Map.fromList [ (k, translate (mapToMor m2) v) | (k, v) <- Map.toList a ]
then let e'' = Map.fromList [ (k, e' ! v) | (k, v) <- Map.toList e ]
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 ]
in pure $ Mapping s t' e'' f'' a''
else Left $ "Source and target schemas do not match: " ++ show t ++ " and " ++ show s'

Expand Down
5 changes: 2 additions & 3 deletions src/Language/CQL/Morphism.hs
Original file line number Diff line number Diff line change
Expand Up @@ -113,13 +113,12 @@ translate mor term = case term of
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
typeOf
:: forall var ty sym en fk att gen sk en' fk' att' gen' sk'
. (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk, en', fk', att', gen', sk'])
=> Morphism var ty sym en fk att gen sk en' fk' att' gen' sk'
-> Err ()
typeOfMor mor = do
typeOf mor = do
checkDoms' mor
mapM_ typeOfMorEns $ Map.toList $ m_ens mor
mapM_ typeOfMorFks $ Map.toList $ m_fks mor
Expand Down
7 changes: 4 additions & 3 deletions src/Language/CQL/Transform.hs
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,9 @@ import Data.Typeable
import Data.Void
import Language.CQL.Common
import Language.CQL.Instance as I
import Language.CQL.Mapping as M
import Language.CQL.Morphism (Morphism(..), translate, translate', typeOfMor)
import Language.CQL.Mapping as M hiding (toMorphism)
import Language.CQL.Morphism (Morphism(..), translate, translate')
import Language.CQL.Morphism as Morphism (typeOf)
import Language.CQL.Options
import Language.CQL.Query
import Language.CQL.Schema as S
Expand Down Expand Up @@ -95,7 +96,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 $ toMorphism m
typecheckTransform m = Morphism.typeOf $ toMorphism m

validateTransform
:: forall var ty sym en fk att gen sk x y gen' sk' x' y' -- need forall
Expand Down

0 comments on commit 8cd7f65

Please sign in to comment.