use MultiTyMap #121

statebox · Nov 24, 2018 · 8e86a8c · 8e86a8c
1 parent 3743982
commit 8e86a8c
Show file tree

Hide file tree

Showing 8 changed files with 65 additions and 67 deletions.
diff --git a/src/Language/Common.hs b/src/Language/Common.hs
@@ -19,8 +19,8 @@
 {-# LANGUAGE UndecidableInstances  #-}
 
 module Language.Common where
+
 import           Control.Arrow   (left)
-import           Control.DeepSeq
 import           Data.Char
 import           Data.Foldable   as Foldable (foldl, toList)
 import           Data.Kind
@@ -114,10 +114,6 @@ type family TyMap (f :: * -> Constraint) (xs :: [*]) :: Constraint
 type instance TyMap f '[] = ()
 type instance TyMap f (t ': ts) = (f t, TyMap f ts)
 
-type family ShowOrdNFDataN (xs :: [*]) :: Constraint
-type instance ShowOrdNFDataN '[] = ()
-type instance ShowOrdNFDataN (t ': ts) = (Show t, Ord t, NFData t, ShowOrdNFDataN ts)
-
-type family ShowOrdTypeableNFDataN (xs :: [*]) :: Constraint
-type instance ShowOrdTypeableNFDataN '[] = ()
-type instance ShowOrdTypeableNFDataN (t ': ts) = (Show t, Ord t, Typeable t, NFData t, ShowOrdTypeableNFDataN ts)
+type family MultiTyMap (fs :: [* -> Constraint]) (xs :: [*]) :: Constraint
+type instance MultiTyMap '[] _ = ()
+type instance MultiTyMap (f : fs) xs = (TyMap f xs, MultiTyMap fs xs)
diff --git a/src/Language/Instance.hs b/src/Language/Instance.hs
@@ -43,7 +43,7 @@ import qualified Text.Tabular.AsciiArt as Ascii
 
 -- | Checks that an instance presentation is a well-formed theory.
 typecheckPresentation
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Schema var ty sym en fk att
   -> Presentation var ty sym en fk att gen sk
   -> Err ()
@@ -108,7 +108,7 @@ down1 _        = error "Anomaly: please report.  Function name: down1."
 
 -- | Checks that an instance satisfies its schema.
 checkSatisfaction
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk, x, y])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y])
   => Instance var ty sym en fk att gen sk x y
   -> Err ()
 checkSatisfaction (Instance sch pres' dp' alg) = do
@@ -205,13 +205,13 @@ instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk]
 data InstanceEx :: * where
   InstanceEx
     :: forall var ty sym en fk att gen sk x y
-    .  (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk, x, y])
+    .  (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y])
     => Instance var ty sym en fk att gen sk x y
     -> InstanceEx
 
 -- | Converts an instance to a presentation.
 instToCol
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Schema var ty sym en fk att
   -> Presentation var ty sym en fk att gen sk
   -> Collage (()+var) ty sym en fk att gen sk
@@ -225,7 +225,7 @@ instToCol sch (Presentation gens' sks' eqs') =
 
 
 -- | Converts an instance into a presentation: adds one equation per fact in the algebra.
-algebraToPresentation :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk], Ord y, Ord 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
 algebraToPresentation (alg@(Algebra sch en' _ _ ty' _ _ _)) = Presentation gens' sks' eqs'
@@ -247,7 +247,7 @@ reify :: (Ord x, Ord en) => (en -> Set x) -> Set en -> [(x, en)]
 reify f s = concat $ Set.toList $ Set.map (\en'-> Set.toList $ Set.map (\x->(x,en')) $ f en') $ s
 
 initialInstance
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Presentation var ty sym en fk att gen sk -> (EQ (()+var) ty sym en fk att gen sk -> Bool)
   -> Schema var ty sym en fk att
   -> Instance var ty sym en fk att gen sk (Carrier en fk gen) (TalgGen en fk att gen sk)
@@ -256,7 +256,7 @@ initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra p dp' sch
 
 
 initialAlgebra
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Presentation var ty sym en fk att gen sk
   -> (EQ (()+var) ty sym en fk att gen sk -> Bool)
   -> Schema var ty sym en fk att
@@ -309,7 +309,7 @@ fromListAccum ((k,v):kvs) = Map.insert k op (fromListAccum kvs)
     r  = fromListAccum kvs
 
 assembleSks
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Map en (Set (Carrier en fk gen))
   -> Map ty (Set (TalgGen en fk att gen sk))
@@ -322,7 +322,7 @@ assembleSks col ens' = unionWith Set.union sks' $ fromListAccum gens'
 -- | Inlines type-algebra equations of the form @gen = term@.
 -- The hard work is delegtated to functions from the Term module.
 simplifyAlg
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk, x, y])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y])
   => Algebra var ty sym en fk att gen sk x y
   -> Algebra var ty sym en fk att gen sk x y
 simplifyAlg
@@ -356,7 +356,7 @@ deriving instance TyMap Ord '[en, fk, att, gen, sk] => Ord (TalgGen en fk att ge
 
 deriving instance TyMap Eq '[en, fk, att, gen, sk] => Eq (TalgGen en fk att gen sk)
 
-assembleGens :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
+assembleGens :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Eq en)
  => Collage var ty sym en fk att gen sk -> [Carrier en fk gen] -> Map en (Set (Carrier en fk gen))
 assembleGens col [] = Map.fromList $ Prelude.map (\x -> (x,Set.empty)) $ Set.toList $ cens col
 assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
@@ -365,7 +365,7 @@ assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
        s = fromJust $ Map.lookup t m
 
 close
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Eq en)
   => Collage var  ty   sym  en fk att  gen sk
   -> (EQ     var  ty   sym  en fk att  gen sk    -> Bool)
   -> [Term   Void Void Void en fk Void gen Void]
@@ -375,7 +375,7 @@ close col dp' =
     y f x = let z = f x in if x == z then x else y f z
 
 close1m
-  :: (Foldable t, ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (Foldable t, MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => (EQ var ty sym en fk att gen sk -> Bool)
   -> Collage var ty sym en fk att gen sk
   -> t (Term Void Void Void en fk Void gen Void)
@@ -387,7 +387,7 @@ dedup :: (EQ var ty sym en fk att gen sk -> Bool)
                -> [Term Void Void Void en fk Void gen Void]
 dedup dp' = nubBy (\x y -> dp' (EQ (upp x, upp y)))
 
-close1 :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk], Eq en)
+close1 :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk], Eq en)
  => Collage var ty sym en fk att gen sk -> (EQ var ty sym en fk att gen sk -> Bool) -> Term Void Void Void en fk Void gen Void -> [ (Term Void Void Void en fk Void gen Void) ]
 close1 col _ e = e:(fmap (\(x,_) -> Fk x e) l)
  where t = typeOf col e
@@ -478,7 +478,7 @@ split'' ens2 tys2 ((w, ei):tl) =
           else Left $ "Not an entity or type: " ++ show ei
 
 evalInstanceRaw'
-  :: forall var ty sym en fk att . (ShowOrdNFDataN '[var, ty, sym, en, fk, att], Typeable ty, Typeable sym, Typeable en, Typeable fk, Typeable att)
+  :: forall var ty sym en fk att . (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att], Typeable ty, Typeable sym, Typeable en, Typeable fk, Typeable att)
   => Schema var ty sym en fk att
   -> InstExpRaw'
   -> [Presentation var ty sym en fk att Gen Sk]
@@ -527,7 +527,7 @@ evalInstanceRaw' sch (InstExpRaw' _ gens0 eqs' _ _) is = do
                                                                             Nothing -> Left $ "Cannot type: " ++ v
 
 evalInstanceRaw
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att])
   => Options
   -> Schema var ty sym en fk att
   -> InstExpRaw'
@@ -569,7 +569,7 @@ emptyInstance ts'' = Instance ts''
 -- Functorial data migration
 
 subs
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq en')
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq en')
   => Mapping var ty sym en fk att en' fk' att'
   -> Presentation var ty sym en  fk  att  gen sk
   -> Presentation var ty sym en' fk' att' gen sk
@@ -608,7 +608,7 @@ changeEn' fks' atts' t = case t of
   Att h _ -> absurd h
 
 evalSigmaInst
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq x, Eq y, Eq en')
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, en', fk', att', gen, sk], Eq x, Eq y, Eq en')
   => Mapping var ty sym en fk att en' fk' att'
   -> Instance var ty sym en fk att gen sk x y -> Options
   -> Err (Instance var ty sym en' fk' att' gen sk (Carrier en' fk' gen) (TalgGen en' fk' att' gen sk))
@@ -653,7 +653,7 @@ evalDeltaAlgebra (Mapping src' _ ens' fks0 atts0)
 
 
 evalDeltaInst
-  :: forall var ty sym en fk att gen sk x y en' fk' att' . (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk, x, y, en', fk', att'])
+  :: forall var ty sym en fk att gen sk x y en' fk' att' . (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk, x, y, en', fk', att'])
   => Mapping var ty sym en fk att en' fk' att'
   -> Instance var ty sym en' fk' att' gen sk x y -> Options
   -> Err (Instance var ty sym en fk att (en,x) y (en,x) y)

diff --git a/src/Language/Mapping.hs b/src/Language/Mapping.hs
@@ -79,22 +79,22 @@ getAtts :: Mapping var ty sym en fk att en' fk' att' -> Map att (Term () ty   sy
 getAtts = atts
 
 mapToMor
-  :: ShowOrdNFDataN '[var, ty, sym, en, fk, att, en', fk', att']
+  :: 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
 
 -- | Checks well-typedness of underlying theory.
 typecheckMapping
-  :: (ShowOrdNFDataN '[var, ty], ShowOrdTypeableNFDataN '[sym, en, fk, att, en', fk', att'])
+  :: (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
 
 -- | Given @F@ checks that each @S |- p = q  ->  T |- F p = F q@.
 validateMapping
   :: forall  var ty sym en fk att en' fk' att'
-  . (ShowOrdNFDataN '[var, ty], ShowOrdTypeableNFDataN '[sym, en, fk, att, en', fk', att'])
+  . (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 ()
 validateMapping (m@(Mapping src' dst' ens' _ _)) = do
@@ -145,7 +145,7 @@ instance Deps MappingExp where
 
 data MappingEx :: * where
   MappingEx
-    :: forall var ty sym en fk att en' fk' att' . (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, en', fk', att'])
+    :: forall var ty sym en fk att en' fk' att' . (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att'])
     => Mapping var ty sym en fk att en' fk' att'
     -> MappingEx
 
@@ -158,7 +158,7 @@ instance NFData MappingEx where
 -- Operations
 
 composeMapping
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, en', fk', att', en', fk', att', en'', fk'', att''])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att', en', fk', att', en'', fk'', att''])
   =>      Mapping var ty sym en  fk  att  en'  fk'  att'
   ->      Mapping var ty sym en' fk' att' en'' fk'' att''
   -> Err (Mapping var ty sym en  fk  att  en'' fk'' att'')
@@ -185,7 +185,7 @@ data MappingExpRaw' =
 } deriving (Eq, Show)
 
 evalMappingRaw'
-  :: forall var ty sym en fk att en' fk' att' . (ShowOrdNFDataN '[var, ty], ShowOrdTypeableNFDataN '[sym, en, fk, att, en', fk', att'])
+  :: forall var ty sym en fk att en' fk' att' . (MultiTyMap '[Show, Ord, NFData] '[var, ty], MultiTyMap '[Show, Ord, Typeable, NFData] '[sym, en, fk, att, en', fk', att'])
   => Schema var ty sym en fk att -> Schema var ty sym en' fk' att'
   -> MappingExpRaw'
   -> [Mapping var ty sym en fk att en' fk' att']
@@ -272,7 +272,7 @@ evalMappingRaw' src' dst' (MappingExpRaw' _ _ ens0 fks0 atts0 _ _) is = do
       Nothing       -> Left $ "Not in target schema/typeside: " ++ show ty
 
 evalMappingRaw
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, en', fk', att'])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att'])
   => Schema var ty sym en  fk  att
   -> Schema var ty sym en' fk' att'
   -> MappingExpRaw'

diff --git a/src/Language/Prover.hs b/src/Language/Prover.hs
@@ -16,6 +16,8 @@
 {-# LANGUAGE UndecidableInstances  #-}
 
 module Language.Prover where
+
+import           Control.DeepSeq
 import           Data.Rewriting.CriticalPair as CP
 import           Data.Rewriting.Rule         as R
 import           Data.Rewriting.Rules        as Rs
@@ -45,7 +47,7 @@ proverStringToName m = case sOps m prover_name of
   x            -> Left $ "Not a prover: " ++ x
 
 createProver
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Options
   -> Err (Prover var ty sym en fk att gen sk)
@@ -72,7 +74,7 @@ freeProver col = if Set.size (ceqs col) == 0
 
 -- | A prover for weakly orthogonal theories: http://hackage.haskell.org/package/term-rewriting
 orthProver
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Options
   -> Err (Prover var ty sym en fk att gen sk)

diff --git a/src/Language/Schema.hs b/src/Language/Schema.hs
@@ -69,13 +69,13 @@ instance TyMap Show '[var, ty, sym, en, fk, att]
       eqs'' x = Prelude.map (\(en,EQ (l,r)) -> "forall x : " ++ show en ++ " . " ++ show (mapVar "x" l) ++ " = " ++ show (mapVar "x" r)) $ Set.toList x
 
 typecheckSchema
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att])
+  :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att])
   => Schema var ty sym en fk att
   -> Err ()
 typecheckSchema t = typeOfCol $ schToCol  t
 
 schToCol
-  :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att])
+  :: (MultiTyMap '[Show, Ord, NFData] '[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' _) =
@@ -141,7 +141,7 @@ instance Deps SchemaExp where
 
 data SchemaEx :: * where
   SchemaEx
-    :: forall var ty sym en fk att . (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att])
+    :: forall var ty sym en fk att . (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att])
     => Schema var ty sym en fk att
     -> SchemaEx
 
@@ -174,7 +174,7 @@ type Fk = String
 type Att = String
 
 evalSchemaRaw'
-  :: (Show var, Ord var, ShowOrdTypeableNFDataN '[ty, sym])
+  :: (Show var, Ord var, MultiTyMap '[Show, Ord, Typeable, NFData] '[ty, sym])
   => Typeside var ty sym -> SchemaExpRaw'
   -> [Schema var ty sym En Fk Att]
   -> Err (Schema var ty sym En Fk Att)
@@ -264,7 +264,7 @@ evalSchemaRaw' (x@(Typeside _ _ _ _)) (SchemaExpRaw' _ ens'x fks'x atts'x peqs o
 
 
 evalSchemaRaw
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym])
   => Options
   -> Typeside var ty sym
   -> SchemaExpRaw'