reintroduced Convertible typeclass; fixed conv for formulas

diff --git a/CTT.hs b/CTT.hs
index 84d487743d1f4a6b8275ee959f8ad48b9f9a75b3..ed9f56bcc88f3907f08a07435d6205f94916be0d 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -151,18 +151,18 @@ mapEnv f g e = case e of
   Def ts e      -> Def ts (mapEnv f g e)
   Sub e (i,phi) -> Sub (mapEnv f g e) (i,g phi)
 
+valAndFormulaOfEnv :: Env -> ([Val],[Formula])
+valAndFormulaOfEnv rho = case rho of
+  Empty -> ([],[])
+  Pair rho (_,u) -> let (us,phis) in (u:us,phis)
+  Sub rho (_,phi) -> let (us,phis) in (us,phi:phis)
+  Def _ rho -> valAndFormulaOfEnv rho
+
 valOfEnv :: Env -> [Val]
-valOfEnv Empty            = []
-valOfEnv (Pair env (_,v)) = v : valOfEnv env
-valOfEnv (Def _ env)      = valOfEnv env
-valOfEnv (Sub env _)      = valOfEnv env
+valOfEnv = valAndFormulaOfEnv . fst
 
 formulaOfEnv :: Env -> [Formula]
-formulaOfEnv e = case e of
-  Empty           -> []
-  Pair rho _      -> formulaOfEnv rho
-  Def _ rho       -> formulaOfEnv rho
-  Sub rho (_,phi) -> phi : formulaOfEnv rho
+formulaOfEnv = valAndFormulaOfEnv . snd
 
 domainEnv :: Env -> [Name]
 domainEnv rho = case rho of

diff --git a/Eval.hs b/Eval.hs
index 6d387d1e596b1d3dfb10d8e48869575aaa9a99e3..49b2e579c9007bc9fdb9345acad7bd9db374dbb1 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -265,51 +265,74 @@ comps _ _ _ _ = error "comps: different lengths of types and values"
 -------------------------------------------------------------------------------
 -- | Conversion
 
-conv :: Int -> Val -> Val -> Bool
-conv k u v | u == v    = True
-           | otherwise = let j = fresh (u,v) in case (u,v) of
-  (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
-    let v = mkVar k (eval e a)
-    in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u')
-  (Ter (Lam x a u) e,u') ->
-    let v = mkVar k (eval e a)
-    in conv (k+1) (eval (Pair e (x,v)) u) (app u' v)
-  (u',Ter (Lam x a u) e) ->
-    let v = mkVar k (eval e a)
-    in conv (k+1) (app u' v) (eval (Pair e (x,v)) u)
-  (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && convEnv k e e'
-  (Ter (Sum p _) e,Ter (Sum p' _) e')     -> (p == p') && convEnv k e e'
-  (Ter (Undef p) e,Ter (Undef p') e')     -> (p == p') && convEnv k e e'
-  (VPi u v,VPi u' v') ->
-    let w = mkVar k u
-    in conv k u u' && conv (k+1) (app v w) (app v' w)
-  (VSigma u v,VSigma u' v') ->
-    let w = mkVar k u
-    in conv k u u' && conv (k+1) (app v w) (app v' w)
-  (VCon c us,VCon c' us')   -> (c == c') && and (zipWith (conv k) us us')
-  (VSPair u v,VSPair u' v') -> conv k u u' && conv k v v'
-  (VSPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
-  (w,VSPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
-  (VFst u,VFst u')          -> conv k u u'
-  (VSnd u,VSnd u')          -> conv k u u'
-  (VApp u v,VApp u' v')     -> conv k u u' && conv k v v'
-  (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
-  (VVar x _, VVar x' _)     -> x == x'
-  (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
-  (VPath i a,VPath i' a') -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
-  (VPath i a,p') -> conv k (a `swap` (i,j)) (p' @@ j)
-  (p,VPath i' a')              -> conv k (p @@ j) (a' `swap` (i',j))
-  (VTrans p u,v) | isIndep k j (p @@ j) -> conv k u v
-  (u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v
-  (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
-  (VAppFormula u x,VAppFormula u' x') -> conv k u u' && (x == x')
-  -- VAppformula
-  -- VTrans
-  -- VComp
-  _                         -> False
-
-convEnv :: Int -> Env -> Env -> Bool
-convEnv k e e' = and $ zipWith (conv k) (valOfEnv e) (valOfEnv e')
-
-isIndep :: Int -> Name -> Val -> Bool
+
+class Convertible a where
+  conv   :: Int -> a -> a -> Bool
+
+isIndep :: (Nominal a, Convertible a) => Int -> Name -> a -> Bool
 isIndep k i u = conv k u (u `face` (i ~> 0))
+
+instance Convertible Val where
+  conv k u v | u == v    = True
+             | otherwise = let j = fresh (u,v) in case (u,v) of
+    (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
+      let v = mkVar k (eval e a)
+      in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u')
+    (Ter (Lam x a u) e,u') ->
+      let v = mkVar k (eval e a)
+      in conv (k+1) (eval (Pair e (x,v)) u) (app u' v)
+    (u',Ter (Lam x a u) e) ->
+      let v = mkVar k (eval e a)
+      in conv (k+1) (app u' v) (eval (Pair e (x,v)) u)
+    (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && conv k e e'
+    (Ter (Sum p _) e,Ter (Sum p' _) e')     -> (p == p') && conv k e e'
+    (Ter (Undef p) e,Ter (Undef p') e')     -> (p == p') && conv k e e'
+    (VPi u v,VPi u' v') ->
+      let w = mkVar k u
+      in conv k u u' && conv (k+1) (app v w) (app v' w)
+    (VSigma u v,VSigma u' v') ->
+      let w = mkVar k u
+      in conv k u u' && conv (k+1) (app v w) (app v' w)
+    (VCon c us,VCon c' us')   -> (c == c') && conv k us us'
+    (VSPair u v,VSPair u' v') -> conv k u u' && conv k v v'
+    (VSPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
+    (w,VSPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
+    (VFst u,VFst u')          -> conv k u u'
+    (VSnd u,VSnd u')          -> conv k u u'
+    (VApp u v,VApp u' v')     -> conv k u u' && conv k v v'
+    (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
+    (VVar x _, VVar x' _)     -> x == x'
+    (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
+    (VPath i a,VPath i' a')    -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
+    (VPath i a,p')             -> conv k (a `swap` (i,j)) (p' @@ j)
+    (p,VPath i' a')            -> conv k (p @@ j) (a' `swap` (i',j))
+    (VTrans p u,v) | isIndep k j (p @@ j) -> conv k u v
+    (u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v
+    (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
+    (VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
+    -- VComp
+    _                         -> False
+
+instance Convertible Env where
+  conv k e e' =
+    and $ zipWith (conv k) (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
+
+instance Convertible () where conv _ _ _ = True
+
+instance (Convertible a, Convertible b) => Convertible (a, b) where
+  conv k (u, v) (u', v') = conv k u u' && conv k v v'
+
+instance (Convertible a, Convertible b, Convertible c)
+      => Convertible (a, b, c) where
+  conv k (u, v, w) (u', v', w') = conv k (u,(v,w)) (u',(v',w'))
+
+instance (Convertible a,Convertible b,Convertible c,Convertible d)
+      => Convertible (a,b,c,d) where
+  conv k (u,v,w,x) (u',v',w',x') = conv k (u,v,(w,x)) (u',v',(w',x'))
+
+instance Convertible a => Convertible [a] where
+  conv k us us' = length us == length us' &&
+                  and [conv k u u' | (u,u') <- zip us us']
+
+instance Convertible Formula where
+  conv _ phi psi = sort (invFormula phi 1) == sort (invFormula psi 1)