From 59f3630a7cd6bbdc6c45fc8e9f5fc66acfffa48f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 3 Dec 2015 19:57:58 -0500 Subject: [PATCH] Add VCompU to normal and conv --- Eval.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Eval.hs b/Eval.hs index 63e816a..e70b53c 100644 --- a/Eval.hs +++ b/Eval.hs @@ -252,6 +252,7 @@ inferType v = case v of ty -> error $ "inferType: expected IdP type for " ++ show v ++ ", got " ++ show ty VComp a _ _ -> a @@ One + VUnGlueElemU _ b es -> compUniv b es _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -764,6 +765,8 @@ instance Convertible Val where (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v isos,VGlue v' isos') -> conv ns (v,isos) (v',isos') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') + (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' + (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') _ -> False instance Convertible Ctxt where @@ -826,6 +829,8 @@ instance Normal Val where VSplit u t -> VSplit (normal ns u) (normal ns t) VApp u v -> app (normal ns u) (normal ns v) VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi) + VCompU u es -> compUniv (normal ns u) (normal ns es) + VUnGlueElemU u b es -> unGlueU (normal ns u) (normal ns b) (normal ns es) _ -> v instance Normal Ctxt where -- 2.34.1