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

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

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

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))

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