From: Anders Mörtberg Date: Fri, 4 Dec 2015 00:57:58 +0000 (-0500) Subject: Add VCompU to normal and conv X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=59f3630a7cd6bbdc6c45fc8e9f5fc66acfffa48f;p=cubicaltt.git Add VCompU to normal and conv --- 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