Boxing Env to prevent Show conflicts with newer versions of haskell packages

diff --git a/CTT.hs b/CTT.hs
index c7eb5ed83dd27ad97e050a93240878967b017a16..3bc9e4cdd64f9bbe5a6586df3385623cd52f5609 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -251,28 +251,29 @@ instance Eq Ctxt where
 -- lists. This is more efficient because acting on an environment now
 -- only need to affect the lists and not the whole context.
 -- The last list is the list of opaque names
-type Env = (Ctxt,[Val],[Formula],Nameless (Set Ident))
+newtype Env = Env (Ctxt,[Val],[Formula],Nameless (Set Ident))
+  deriving (Eq)
 
 emptyEnv :: Env
-emptyEnv = (Empty,[],[],Nameless Set.empty)
+emptyEnv = Env (Empty,[],[],Nameless Set.empty)
 
 def :: Decls -> Env -> Env
-def (MutualDecls m ds) (rho,vs,fs,Nameless os) = (Def m ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds)))
-def (OpaqueDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.insert n os))
-def (TransparentDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.delete n os))
-def TransparentAllDecl (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless Set.empty)
+def (MutualDecls m ds) (Env (rho,vs,fs,Nameless os)) = Env (Def m ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds)))
+def (OpaqueDecl n) (Env (rho,vs,fs,Nameless os)) = Env (rho,vs,fs,Nameless (Set.insert n os))
+def (TransparentDecl n) (Env (rho,vs,fs,Nameless os)) = Env (rho,vs,fs,Nameless (Set.delete n os))
+def TransparentAllDecl (Env (rho,vs,fs,Nameless os)) = Env (rho,vs,fs,Nameless Set.empty)
 
 defWhere :: Decls -> Env -> Env
-defWhere (MutualDecls m ds) (rho,vs,fs,Nameless os) = (Def m ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds)))
+defWhere (MutualDecls m ds) (Env (rho,vs,fs,Nameless os)) = Env (Def m ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds)))
 defWhere (OpaqueDecl _) rho = rho
 defWhere (TransparentDecl _) rho = rho
 defWhere TransparentAllDecl rho = rho
 
 sub :: (Name,Formula) -> Env -> Env
-sub (i,phi) (rho,vs,fs,os) = (Sub i rho,vs,phi:fs,os)
+sub (i,phi) (Env (rho,vs,fs,os)) = Env (Sub i rho,vs,phi:fs,os)
 
 upd :: (Ident,Val) -> Env -> Env
-upd (x,v) (rho,vs,fs,Nameless os) = (Upd x rho,v:vs,fs,Nameless (Set.delete x os))
+upd (x,v) (Env (rho,vs,fs,Nameless os)) = Env (Upd x rho,v:vs,fs,Nameless (Set.delete x os))
 
 upds :: [(Ident,Val)] -> Env -> Env
 upds xus rho = foldl (flip upd) rho xus
@@ -284,10 +285,10 @@ subs :: [(Name,Formula)] -> Env -> Env
 subs iphis rho = foldl (flip sub) rho iphis
 
 mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
-mapEnv f g (rho,vs,fs,os) = (rho,map f vs,map g fs,os)
+mapEnv f g (Env (rho,vs,fs,os)) = Env (rho,map f vs,map g fs,os)
 
 valAndFormulaOfEnv :: Env -> ([Val],[Formula])
-valAndFormulaOfEnv (_,vs,fs,_) = (vs,fs)
+valAndFormulaOfEnv (Env (_,vs,fs,_)) = (vs,fs)
 
 valOfEnv :: Env -> [Val]
 valOfEnv = fst . valAndFormulaOfEnv
@@ -296,7 +297,7 @@ formulaOfEnv :: Env -> [Formula]
 formulaOfEnv = snd . valAndFormulaOfEnv
 
 domainEnv :: Env -> [Name]
-domainEnv (rho,_,_,_) = domCtxt rho
+domainEnv (Env (rho,_,_,_)) = domCtxt rho
   where domCtxt rho = case rho of
           Empty      -> []
           Upd _ e    -> domCtxt e
@@ -306,11 +307,11 @@ domainEnv (rho,_,_,_) = domCtxt rho
 -- Extract the context from the environment, used when printing holes
 contextOfEnv :: Env -> [String]
 contextOfEnv rho = case rho of
-  (Empty,_,_,_)               -> []
-  (Upd x e,VVar n t:vs,fs,os) -> (n ++ " : " ++ show t) : contextOfEnv (e,vs,fs,os)
-  (Upd x e,v:vs,fs,os)        -> (x ++ " = " ++ show v) : contextOfEnv (e,vs,fs,os)
-  (Def _ _ e,vs,fs,os)        -> contextOfEnv (e,vs,fs,os)
-  (Sub i e,vs,phi:fs,os)      -> (show i ++ " = " ++ show phi) : contextOfEnv (e,vs,fs,os)
+  Env (Empty,_,_,_)               -> []
+  Env (Upd x e,VVar n t:vs,fs,os) -> (n ++ " : " ++ show t) : contextOfEnv (Env (e,vs,fs,os))
+  Env (Upd x e,v:vs,fs,os)        -> (x ++ " = " ++ show v) : contextOfEnv (Env (e,vs,fs,os))
+  Env (Def _ _ e,vs,fs,os)        -> contextOfEnv (Env (e,vs,fs,os))
+  Env (Sub i e,vs,phi:fs,os)      -> (show i ++ " = " ++ show phi) : contextOfEnv (Env (e,vs,fs,os))
 
 --------------------------------------------------------------------------------
 -- | Pretty printing
@@ -325,19 +326,19 @@ showEnv b e =
       par   x = if b then parens x else x
       com     = if b then comma else PP.empty
       showEnv1 e = case e of
-        (Upd x env,u:us,fs,os)   ->
-          showEnv1 (env,us,fs,os) <+> names x <+> showVal1 u <> com
-        (Sub i env,us,phi:fs,os) ->
-          showEnv1 (env,us,fs,os) <+> names (show i) <+> text (show phi) <> com
-        (Def _ _ env,vs,fs,os)   -> showEnv1 (env,vs,fs,os)
-        _                        -> showEnv b e
+        Env (Upd x env,u:us,fs,os)   ->
+          showEnv1 (Env (env,us,fs,os)) <+> names x <+> showVal1 u <> com
+        Env (Sub i env,us,phi:fs,os) ->
+          showEnv1 (Env (env,us,fs,os)) <+> names (show i) <+> text (show phi) <> com
+        Env (Def _ _ env,vs,fs,os)   -> showEnv1 (Env (env,vs,fs,os))
+        _                            -> showEnv b e
   in case e of
-    (Empty,_,_,_)            -> PP.empty
-    (Def _ _ env,vs,fs,os)   -> showEnv b (env,vs,fs,os)
-    (Upd x env,u:us,fs,os)   ->
-      par $ showEnv1 (env,us,fs,os) <+> names x <+> showVal1 u
-    (Sub i env,us,phi:fs,os) ->
-      par $ showEnv1 (env,us,fs,os) <+> names (show i) <+> text (show phi)
+    Env (Empty,_,_,_)            -> PP.empty
+    Env (Def _ _ env,vs,fs,os)   -> showEnv b (Env (env,vs,fs,os))
+    Env (Upd x env,u:us,fs,os)   ->
+      par $ showEnv1 (Env (env,us,fs,os)) <+> names x <+> showVal1 u
+    Env (Sub i env,us,phi:fs,os) ->
+      par $ showEnv1 (Env (env,us,fs,os)) <+> names (show i) <+> text (show phi)
 
 instance Show Loc where
   show = render . showLoc

diff --git a/Eval.hs b/Eval.hs
index 16011f5fbdfb429b781cae0d7da1ad3d90291e72..e013605f3a2bac0846eb581b6c8be31d638a15ee 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -16,30 +16,30 @@ import CTT
 -- Lookup functions
 
 look :: String -> Env -> Val
-look x (Upd y rho,v:vs,fs,os) | x == y = v
-                              | otherwise = look x (rho,vs,fs,os)
-look x r@(Def _ decls rho,vs,fs,Nameless os) = case lookup x decls of
+look x (Env (Upd y rho,v:vs,fs,os)) | x == y = v
+                                    | otherwise = look x (Env (rho,vs,fs,os))
+look x r@(Env (Def _ decls rho,vs,fs,Nameless os)) = case lookup x decls of
   Just (_,t) -> eval r t
-  Nothing    -> look x (rho,vs,fs,Nameless os)
-look x (Sub _ rho,vs,_:fs,os) = look x (rho,vs,fs,os)
-look x (Empty,_,_,_) = error $ "look: not found " ++ show x
+  Nothing    -> look x (Env (rho,vs,fs,Nameless os))
+look x (Env (Sub _ rho,vs,_:fs,os)) = look x (Env (rho,vs,fs,os))
+look x (Env (Empty,_,_,_)) = error $ "look: not found " ++ show x
 
 lookType :: String -> Env -> Val
-lookType x (Upd y rho,v:vs,fs,os)
-  | x /= y        = lookType x (rho,vs,fs,os)
+lookType x (Env (Upd y rho,v:vs,fs,os))
+  | x /= y        = lookType x (Env (rho,vs,fs,os))
   | VVar _ a <- v = a
   | otherwise     = error ""
-lookType x r@(Def _ decls rho,vs,fs,os) = case lookup x decls of
+lookType x r@(Env (Def _ decls rho,vs,fs,os)) = case lookup x decls of
   Just (a,_) -> eval r a
-  Nothing -> lookType x (rho,vs,fs,os)
-lookType x (Sub _ rho,vs,_:fs,os) = lookType x (rho,vs,fs,os)
-lookType x (Empty,_,_,_)                  = error $ "lookType: not found " ++ show x
+  Nothing -> lookType x (Env (rho,vs,fs,os))
+lookType x (Env (Sub _ rho,vs,_:fs,os)) = lookType x (Env (rho,vs,fs,os))
+lookType x (Env (Empty,_,_,_))          = error $ "lookType: not found " ++ show x
 
 lookName :: Name -> Env -> Formula
-lookName i (Upd _ rho,v:vs,fs,os) = lookName i (rho,vs,fs,os)
-lookName i (Def _ _ rho,vs,fs,os) = lookName i (rho,vs,fs,os)
-lookName i (Sub j rho,vs,phi:fs,os) | i == j    = phi
-                                    | otherwise = lookName i (rho,vs,fs,os)
+lookName i (Env (Upd _ rho,v:vs,fs,os)) = lookName i (Env (rho,vs,fs,os))
+lookName i (Env (Def _ _ rho,vs,fs,os)) = lookName i (Env (rho,vs,fs,os))
+lookName i (Env (Sub j rho,vs,phi:fs,os)) | i == j    = phi
+                                          | otherwise = lookName i (Env (rho,vs,fs,os))
 lookName i _ = error $ "lookName: not found " ++ show i
 
 
@@ -51,6 +51,11 @@ instance Nominal Ctxt where
   act e _   = e
   swap e _  = e
 
+instance Nominal Env where
+  support (Env (rho,vs,fs,os)) = support (rho,vs,fs,os)
+  act (Env (rho,vs,fs,os)) iphi = Env $ act (rho,vs,fs,os) iphi
+  swap (Env (rho,vs,fs,os)) ij = Env $ swap (rho,vs,fs,os) ij
+
 instance Nominal Val where
   support v = case v of
     VU                      -> []
@@ -157,7 +162,7 @@ instance Nominal Val where
 -- The evaluator
 
 eval :: Env -> Ter -> Val
-eval rho@(_,_,_,Nameless os) v = case v of
+eval rho@(Env (_,_,_,Nameless os)) v = case v of
   U                   -> VU
   App r s             -> app (eval rho r) (eval rho s)
   Var i
@@ -833,6 +838,10 @@ isCompSystem ns ts = and [ conv ns (getFace alpha beta) (getFace beta alpha)
                          | (alpha,beta) <- allCompatible (keys ts) ]
     where getFace a b = face (ts ! a) (b `minus` a)
 
+instance Convertible Env where
+  conv ns (Env (rho1,vs1,fs1,os1)) (Env (rho2,vs2,fs2,os2)) =
+      conv ns (rho1,vs1,fs1,os1) (rho2,vs2,fs2,os2)
+
 instance Convertible Val where
   conv ns u v | u == v    = True
               | otherwise =
@@ -927,6 +936,9 @@ instance Convertible (Nameless a) where
 class Normal a where
   normal :: [String] -> a -> a
 
+instance Normal Env where
+  normal ns (Env (rho,vs,fs,os)) = Env (normal ns (rho,vs,fs,os))
+
 instance Normal Val where
   normal ns v = case v of
     VU                  -> VU