From: Anders Mörtberg <andersmortberg@gmail.com>
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