From: Rafaël Bocquet <rafael.bocquet@ens.fr>
Date: Thu, 7 Jul 2016 15:34:29 +0000 (+0200)
Subject: Speed up conv
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=280f99caa1f97b5d63b388e8fe68b305b5f68a37;p=cubicaltt.git

Speed up conv
---

diff --git a/Eval.hs b/Eval.hs
index ef330da..740682c 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -791,19 +791,12 @@ isCompSystem ns ts = and [ conv ns (getFace alpha beta) (getFace beta alpha)
     where getFace a b = face (ts ! a) (b `minus` a)
 
 instance Convertible Val where
-  conv ns u v | u == v    = True
-              | otherwise =
+  conv ns u v =
     let j = fresh (u,v)
     in case (u,v) of
       (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
         let v@(VVar n _) = mkVarNice ns x (eval e a)
         in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u')
-      (Ter (Lam x a u) e,u') ->
-        let v@(VVar n _) = mkVarNice ns x (eval e a)
-        in conv (n:ns) (eval (upd (x,v) e) u) (app u' v)
-      (u',Ter (Lam x a u) e) ->
-        let v@(VVar n _) = mkVarNice ns x (eval e a)
-        in conv (n:ns) (app u' v) (eval (upd (x,v) e) u)
       (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv ns e e'
       (Ter (Sum p _ _) e,Ter (Sum p' _ _) e')         -> (p == p') && conv ns e e'
       (Ter (HSum p _ _) e,Ter (HSum p' _ _) e')       -> (p == p') && conv ns e e'
@@ -821,8 +814,6 @@ instance Convertible Val where
       (VPCon c v us phis,VPCon c' v' us' phis') ->
         (c == c') && conv ns (v,us,phis) (v',us',phis')
       (VPair u v,VPair u' v')    -> conv ns u u' && conv ns v v'
-      (VPair u v,w)              -> conv ns u (fstVal w) && conv ns v (sndVal w)
-      (w,VPair u v)              -> conv ns (fstVal w) u && conv ns (sndVal w) v
       (VFst u,VFst u')           -> conv ns u u'
       (VSnd u,VSnd u')           -> conv ns u u'
       (VApp u v,VApp u' v')      -> conv ns u u' && conv ns v v'
@@ -831,8 +822,6 @@ instance Convertible Val where
       (VVar x _, VVar x' _)      -> x == x'
       (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c'
       (VPath i a,VPath i' a')    -> conv ns (a `swap` (i,j)) (a' `swap` (i',j))
-      (VPath i a,p')             -> conv ns (a `swap` (i,j)) (p' @@ j)
-      (p,VPath i' a')            -> conv ns (p @@ j) (a' `swap` (i',j))
       (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
       (VComp a u ts,VComp a' u' ts')      -> conv ns (a,u,ts) (a',u',ts')
       (VHComp a u ts,VHComp a' u' ts')    -> conv ns (a,u,ts) (a',u',ts')
@@ -841,6 +830,17 @@ instance Convertible Val where
       (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
       (VUnGlueElem u ts,VUnGlueElem u' ts')    -> conv ns (u,ts) (u',ts')
       (VCompU u es,VCompU u' es')              -> conv ns (u,es) (u',es')
+      _ | u == v -> True
+      (Ter (Lam x a u) e,u') ->
+        let v@(VVar n _) = mkVarNice ns x (eval e a)
+        in conv (n:ns) (eval (upd (x,v) e) u) (app u' v)
+      (u',Ter (Lam x a u) e) ->
+        let v@(VVar n _) = mkVarNice ns x (eval e a)
+        in conv (n:ns) (app u' v) (eval (upd (x,v) e) u)
+      (VPair u v,w)              -> conv ns u (fstVal w) && conv ns v (sndVal w)
+      (w,VPair u v)              -> conv ns (fstVal w) u && conv ns (sndVal w) v
+      (VPath i a,p')             -> conv ns (a `swap` (i,j)) (p' @@ j)
+      (p,VPath i' a')            -> conv ns (p @@ j) (a' `swap` (i',j))
       _                                        -> False
 
 instance Convertible Ctxt where