From: Simon Huber <hubsim@gmail.com>
Date: Thu, 27 Apr 2017 20:05:13 +0000 (+0200)
Subject: Don't use smart-constructors when normalizing values
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e32fc4aad9f46b203a248e6a2dcd77a9767b0f89;p=cubicaltt.git

Don't use smart-constructors when normalizing values
---

diff --git a/Eval.hs b/Eval.hs
index 2681214..16011f5 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -942,23 +942,23 @@ instance Normal Val where
     VPCon n u us phis   -> VPCon n (normal ns u) (normal ns us) phis
     VPathP a u0 u1      -> VPathP (normal ns a) (normal ns u0) (normal ns u1)
     VPLam i u           -> VPLam i (normal ns u)
-    VComp u v vs        -> compLine (normal ns u) (normal ns v) (normal ns vs)
-    VHComp u v vs       -> hComp (normal ns u) (normal ns v) (normal ns vs)
-    VGlue u equivs      -> glue (normal ns u) (normal ns equivs)
-    VGlueElem u us      -> glueElem (normal ns u) (normal ns us)
-    VUnGlueElem u us    -> unglueElem (normal ns u) (normal ns us)
-    VUnGlueElemU e u us -> unGlueU (normal ns e) (normal ns u) (normal ns us)
+    VComp u v vs        -> VComp (normal ns u) (normal ns v) (normal ns vs)
+    VHComp u v vs       -> VHComp (normal ns u) (normal ns v) (normal ns vs)
+    VGlue u equivs      -> VGlue (normal ns u) (normal ns equivs)
+    VGlueElem u us      -> VGlueElem (normal ns u) (normal ns us)
+    VUnGlueElem u us    -> VUnGlueElem (normal ns u) (normal ns us)
+    VUnGlueElemU e u us -> VUnGlueElemU (normal ns e) (normal ns u) (normal ns us)
     VCompU a ts         -> VCompU (normal ns a) (normal ns ts)
-    VVar x t            -> VVar x t -- (normal ns t)
-    VFst t              -> fstVal (normal ns t)
-    VSnd t              -> sndVal (normal ns t)
+    VVar x t            -> VVar x (normal ns t)
+    VFst t              -> VFst (normal ns t)
+    VSnd t              -> VSnd (normal ns t)
     VSplit u t          -> VSplit (normal ns u) (normal ns t)
-    VApp u v            -> app (normal ns u) (normal ns v)
+    VApp u v            -> VApp (normal ns u) (normal ns v)
     VAppFormula u phi   -> VAppFormula (normal ns u) (normal ns phi)
     VId a u v           -> VId (normal ns a) (normal ns u) (normal ns v)
     VIdPair u us        -> VIdPair (normal ns u) (normal ns us)
-    VIdJ a u c d x p    -> idJ (normal ns a) (normal ns u) (normal ns c)
-                               (normal ns d) (normal ns x) (normal ns p)
+    VIdJ a u c d x p    -> VIdJ (normal ns a) (normal ns u) (normal ns c)
+                                (normal ns d) (normal ns x) (normal ns p)
     _                   -> v
 
 instance Normal (Nameless a) where