Rename schToCol -> Schema.toCollage, and refactor. #148

statebox · Aug 23, 2019 · cad5118 · cad5118
1 parent f969b85
commit cad5118
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 17 deletions.
diff --git a/src/Language/CQL/Instance/Presentation.hs b/src/Language/CQL/Instance/Presentation.hs
@@ -47,7 +47,8 @@ import qualified Data.Set              as Set
 import           Data.Void
 import           Language.CQL.Collage  (Collage(..), typeOfCol)
 import           Language.CQL.Common   (Err, MultiTyMap, TyMap, type (+), section, sepTup, intercalate)
-import           Language.CQL.Schema   (Schema, schToCol)
+import           Language.CQL.Schema   (Schema)
+import qualified Language.CQL.Schema   as Schema (toCollage)
 import           Language.CQL.Term     as Term
 import           Prelude               hiding (EQ)
 
@@ -88,6 +89,6 @@ toCollage
 toCollage sch (Presentation gens' sks' eqs') =
   Collage (Set.union e1 e2) (ctys schcol) (cens schcol) (csyms schcol) (cfks schcol) (catts schcol) gens' sks'
   where
-    schcol = schToCol sch
+    schcol = Schema.toCollage sch
     e1 = Set.map (\(   EQ (l,r)) -> (Map.empty, EQ (upp l, upp r))) $ eqs'
     e2 = Set.map (\(g, EQ (l,r)) -> (g,         EQ (upp l, upp r))) $ ceqs schcol
diff --git a/src/Language/CQL/Mapping.hs b/src/Language/CQL/Mapping.hs
@@ -105,7 +105,7 @@ 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
-toMorphism (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 (Schema.toCollage src') (Schema.toCollage dst') ens' fks' atts' Map.empty Map.empty
 
 -- | Checks well-typedness of underlying theory.
 typecheckMapping

diff --git a/src/Language/CQL/Schema.hs b/src/Language/CQL/Schema.hs
@@ -39,12 +39,14 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 
 module Language.CQL.Schema where
 import           Control.DeepSeq
+import           Data.Bifunctor        (second)
 import           Data.List             (nub)
 import           Data.Map.Strict       as Map
 import           Data.Maybe
 import           Data.Set              as Set
 import           Data.Typeable
 import           Data.Void
+import           Control.Arrow ((***))
 import           Language.CQL.Collage (Collage(..), typeOfCol)
 import           Language.CQL.Common
 import           Language.CQL.Options
@@ -98,26 +100,29 @@ typecheckSchema
   :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att])
   => Schema var ty sym en fk att
   -> Err ()
-typecheckSchema t = typeOfCol $ schToCol  t
+typecheckSchema = typeOfCol . toCollage
 
 -- | Converts a schema to a collage.
-schToCol
+toCollage
   :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att])
-  => Schema var ty sym en fk att
+  => Schema        var  ty sym en fk att
   -> Collage (() + var) ty sym en fk att Void Void
-schToCol (Schema ts ens' fks' atts' path_eqs' obs_eqs' _) =
-  Collage (Set.union e3 $ Set.union e1 e2) (ctys tscol)
-    ens' (csyms tscol) fks' atts' Map.empty Map.empty
+toCollage (Schema ts ens' fks' atts' path_eqs' obs_eqs' _) =
+  Collage (eqs1 <> eqs2 <> eqs3) (ctys tscol) ens' (csyms tscol) fks' atts' Map.empty Map.empty
   where
     tscol = tsToCol ts
-    e1 = Set.map (\(en, EQ (l,r))->(Map.fromList [(Left (),Right en)], EQ (upp l, upp r))) path_eqs'
-    e2 = Set.map (\(en, EQ (l,r))->(Map.fromList [(Left (),Right en)], EQ (upp l, upp r))) obs_eqs'
-    e3 = Set.map (\(g,EQ (l,r))->(up1Ctx g, EQ (upp l, upp r))) $ ceqs tscol
 
-up1Ctx :: (Ord var) => Ctx var (ty+Void) -> Ctx (()+var) (ty+x)
-up1Ctx g = Map.map (\x -> case x of
-  Left ty -> Left ty
-  Right v -> absurd v) $ Map.mapKeys Right g
+    eqs1 = Set.map (unitCtx *** uppEQ) path_eqs'
+    eqs2 = Set.map (unitCtx *** uppEQ) obs_eqs'
+    eqs3 = Set.map (up1Ctx  *** uppEQ) (ceqs tscol)
+
+    unitCtx en = Map.singleton (Left ()) (Right en)
+
+up1Ctx
+  :: (Ord var)
+  => Ctx var      (ty+Void)
+  -> Ctx (()+var) (ty+x)
+up1Ctx ctx = second absurd <$> Map.mapKeys Right ctx
 
 typesideToSchema :: Typeside var ty sym -> Schema var ty sym Void Void Void
 typesideToSchema ts'' = Schema ts'' Set.empty Map.empty Map.empty Set.empty Set.empty $ \x _ -> absurd x
@@ -306,7 +311,7 @@ evalSchemaRaw ops ty t a' = do
   (a :: [Schema var ty sym En Fk Att]) <- doImports a'
   r <- evalSchemaRaw' ty t a
   o <- toOptions ops $ schraw_options t
-  p <- createProver (schToCol r) o
+  p <- createProver (toCollage r) o
   pure $ SchemaEx $ Schema ty (ens r) (fks r) (atts r) (path_eqs r) (obs_eqs r) (mkProver p)
   where
     mkProver p en (EQ (l,r)) = prove p (Map.fromList [(Left (),Right en)]) (EQ (upp l, upp r))

diff --git a/src/Language/CQL/Term.hs b/src/Language/CQL/Term.hs
@@ -367,6 +367,13 @@ instance Up x (x + y) where
 instance Up y (x + y) where
   upgr = Right
 
+uppEQ
+  :: ( Up var var', Up ty  ty' , Up sym sym', Up en en'
+     , Up fk  fk' , Up att att', Up gen gen', Up sk sk' )
+  => EQ var  ty  sym  en  fk  att  gen  sk
+  -> EQ var' ty' sym' en' fk' att' gen' sk'
+uppEQ (EQ (l,r)) = EQ (upp l, upp r)
+
 --------------------------------------------------------------------------------------------------------------------
 -- Theories