use MultiTyMap #121

statebox · Nov 28, 2018 · 6404855 · 6404855
1 parent ffb2d54
commit 6404855
Show file tree

Hide file tree

Showing 9 changed files with 73 additions and 80 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
@@ -122,10 +122,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
@@ -107,7 +107,7 @@ down1 _        = error "Anomaly: please report.  Function name: down1."
 
 -- | Checks that an instance satisfies its schema.
 checkSatisfaction
-  :: (Show ty, Show sym, Show en, Show fk, Show att, Show gen, Show sk, Ord x)
+  :: (MultiTyMap '[Show] '[var, ty, sym, en, fk, att, gen, sk, x, y], Eq x)
   => Instance var ty sym en fk att gen sk x y
   -> Err ()
 checkSatisfaction (Instance sch pres' dp' alg) = do
@@ -173,7 +173,7 @@ instance (NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData gen, N
 
 -- | 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 ()
@@ -187,7 +187,7 @@ eqs0 (Presentation _ _ x) = x
 
 -- | Converts a presentation to a collage.
 presToCol
-  :: (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
@@ -227,15 +227,15 @@ instance TyMap NFData '[var, ty, sym, en, fk, att, gen, sk, x, y]
 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 algebra into a presentation: adds one equation per fact in the algebra
 -- and one generator per element.  Presentations in this form are called saturated because
 -- they are maximally large without being redundant.  @I(fk.x) = I(fk)(I(x))@
-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'
@@ -258,7 +258,7 @@ reify f s = concat $ Set.toList $ Set.map (\en'-> Set.toList $ Set.map (\x->(x,e
 -- Needs to have satisfaction checked.
 saturatedInstance
   :: forall var ty sym en fk att gen sk
-  .  (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 (Instance var ty sym en fk att gen sk gen (Either sk (gen, att)))
@@ -321,7 +321,7 @@ newtype TalgGen en fk att gen sk = MkTalgGen (Either sk (Carrier en fk gen, att)
 -- The term model is constructed by repeatedly adding news terms to the empty model
 -- until a fixedpoint is reached.
 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
@@ -358,7 +358,7 @@ initialInstance p dp' sch = Instance sch p dp'' $ initialAlgebra
 
 
 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))
@@ -371,7 +371,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
@@ -398,7 +398,7 @@ deriving instance TyMap Ord '[en, fk, att, gen, sk] => Ord (TalgGen en fk att ge
 
 deriving instance TyMap Eq '[fk, att, gen, sk] => Eq (TalgGen en fk att gen sk)
 
-assembleGens :: (ShowOrdNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+assembleGens :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => 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
@@ -407,7 +407,7 @@ assembleGens col (e:tl) = Map.insert t (Set.insert e s) m
        s = m ! t
 
 close
-  :: (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
   -> (EQ     var  ty   sym  en fk att  gen sk    -> Bool)
   -> [Term   Void Void Void en fk Void gen Void]
@@ -417,7 +417,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)
@@ -429,7 +429,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])
+close1 :: (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, gen, sk])
  => 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
@@ -511,7 +511,7 @@ split'' ens2 tys2 ((w, ei):tl) =
           else Left $ "Not an entity or type: " ++ show ei
 
 evalInstanceRaw'
-  :: forall var ty sym en fk att . (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Typeable ty, Typeable sym, Typeable en, Typeable fk, Typeable att)
+  :: forall var ty sym en fk att . (MultiTyMap '[Ord, Typeable] '[ty, sym, en, fk, att])
   => Schema var ty sym en fk att
   -> InstExpRaw'
   -> [Presentation var ty sym en fk att Gen Sk]
@@ -551,7 +551,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'
@@ -590,7 +590,7 @@ emptyInstance ts'' = Instance ts''
       Set.empty)
 
 pivot
-  :: (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
   -> (Schema   var ty sym x (x, fk) (x, att)
   ,   Instance var ty sym x (x, fk) (x, att) x sk x  y
@@ -632,7 +632,7 @@ pivot (Instance sch (Presentation _ sks _) _ (Algebra _ ens _ fk _ tys nnf _ teq
 -- Functorial data migration
 
 subs
-  :: (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord en', Ord fk', Ord att', Ord gen, Ord sk)
+  :: (MultiTyMap '[Ord] '[ty, sym, en, fk, att, en', fk', att', gen, sk])
   => 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
@@ -671,7 +671,7 @@ changeEn' fks' atts' t = case t of
   Att h _ -> absurd h
 
 evalSigmaInst
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, en', fk', att', gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att', gen, sk])
   => 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))
@@ -712,10 +712,7 @@ evalDeltaAlgebra (Mapping src' _ ens' fks0 atts0)
 
 
 evalDeltaInst
-  :: forall var ty sym en fk att gen sk x y en' fk' att'
-  . (Ord ty, Ord sym, Ord en, Ord fk, Ord att, Ord x, Ord y, Ord var,
-     Show var, Show ty, Show sym, Show en, Show fk, Show att, Show x, Show y,
-     NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, NFData x, NFData y)
+  :: forall var ty sym en fk att gen sk x y en' fk' att' . (MultiTyMap '[Show, Ord, NFData] '[var, ty, sym, en, fk, att, x, y])
   => 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
@@ -144,7 +144,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
 
 -- | Compose two mappings.
 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'')
@@ -186,7 +186,7 @@ data MappingExpRaw' =
 
 -- | Does the hard work of @evalMappingRaw@.
 evalMappingRaw'
-  :: forall var ty sym en fk att en' fk' att' . (ShowOrdTypeableNFDataN '[sym, en, fk, att, en', fk', att'])
+  :: forall var ty sym en fk att en' fk' att' . (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']
@@ -274,7 +274,7 @@ evalMappingRaw' src' dst' (MappingExpRaw' _ _ ens0 fks0 atts0 _ _) is = do
 
 -- | Evaluates a literal into a mapping.  Does not typecheck or validate.
 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.List
 import           Data.Map
 import           Data.Maybe
@@ -62,7 +64,7 @@ data Prover var ty sym en fk att gen sk = Prover
 
 -- | Create a prover from a collage and user-provided options.
 createProver
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, 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)
@@ -98,7 +100,7 @@ freeProver col | Set.size (ceqs col) == 0 = return $ Prover col p
 -- without empty sorts and without non-trivial critical pairs (rule overlaps).
 -- Runs the rules non deterministically to get a unique normal form.
 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)
@@ -189,7 +191,7 @@ data Precedence = Precedence !Bool !(Maybe Int) !Int
   deriving (Eq, Ord)
 
 prec
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Head        ty sym en fk att gen sk
   -> Precedence
@@ -201,7 +203,7 @@ prec col c = Precedence p q r -- trace (show (p,q,r)) $
     r = negate (Map.findWithDefault 0 c $ occs col)
 
 toTweeConst
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Head        ty sym en fk att gen sk
   -> Constant (Head ty sym en fk att gen sk)
@@ -216,7 +218,7 @@ toTweeConst col c = Constant (prec col c) c arr sz Nothing
       HSym s -> length $ fst $ (csyms col) ! s
 
 convert
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Ctx var (ty+en)
   -> S.Term var ty sym en fk att gen sk
@@ -231,7 +233,7 @@ convert col ctx x = case x of
 
 initState
   :: forall                     var  ty  sym  en  fk  att  gen  sk
-  .  (ShowOrdTypeableNFDataN '[       var, ty, sym, en, fk, att, gen, sk])
+  .  (MultiTyMap '[Show, Ord, Typeable, NFData] '[       var, ty, sym, en, fk, att, gen, sk])
   => Collage                    var  ty  sym  en  fk  att  gen  sk
   -> State (Extended (Constant (Head ty  sym  en  fk  att  gen  sk)))
 initState col = Set.foldr (\z s -> addAxiom defaultConfig s (toAxiom z)) initialState $ ceqs col
@@ -244,7 +246,7 @@ initState col = Set.foldr (\z s -> addAxiom defaultConfig s (toAxiom z)) initial
 -- critical pairs (rule overlaps) are detected.
 kbProver
   :: forall                     var  ty  sym  en  fk  att  gen  sk
-  .  (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  .  (MultiTyMap '[Show, Ord, Typeable, 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)
@@ -267,7 +269,7 @@ kbProver col ops = if allSortsInhabited col || allow_empty
 -- how much of the congruence graph gets preserved between calls; the code we have could re-run
 -- building the congruence graph on each call to eq.
 congProver
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => Collage var ty sym en fk att gen sk
   -> Err (Prover var ty sym en fk att gen sk)
 congProver col = if eqsAreGround col'
@@ -281,7 +283,7 @@ congProver col = if eqsAreGround col'
     (col', f) = simplifyCol col
 
 convertCong
-  :: (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, gen, sk])
+  :: (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, gen, sk])
   => S.Term var ty sym en fk att gen sk
   -> Language.Internal.Term (Head ty sym en fk att gen sk)
 convertCong x = case x of

diff --git a/src/Language/Query.hs b/src/Language/Query.hs
@@ -21,6 +21,7 @@ module Language.Query where
 import           Control.DeepSeq
 import           Data.Map.Strict as Map
 import           Data.Set        as Set
+import           Data.Typeable
 import           Data.Void
 import           Language.Common
 import           Language.Schema
@@ -56,7 +57,7 @@ instance (NFData var, NFData ty, NFData sym, NFData en, NFData fk, NFData att, N
 data QueryEx :: * where
   QueryEx
     :: forall var ty sym en fk att en' fk' att'
-    .  (ShowOrdTypeableNFDataN '[var, ty, sym, en, fk, att, en', fk', att'])
+    .  (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym, en, fk, att, en', fk', att'])
     => Query var ty sym en fk att en' fk' att' -> QueryEx
 
 instance NFData QueryEx where