From d5eb827f89b71de9aadb1fd26477f44d20f95330 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 27 Nov 2008 10:40:29 -0500
Subject: Remove unnecessary lifts in ElabEnv.pushCRel

---
 src/elab_env.sml  |  4 ++--
 src/elaborate.sml | 26 ++++++++++++++++++++++----
 2 files changed, 24 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/elab_env.sml b/src/elab_env.sml
index 05da56db..3acb855d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -268,7 +268,7 @@ fun pushCRel (env : env) x k =
     in
         {renameC = SM.insert (renameC, x, Rel' (0, k)),
          relC = (x, k) :: #relC env,
-         namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
+         namedC = #namedC env,
 
          datatypes = #datatypes env,
          constructors = #constructors env,
@@ -283,7 +283,7 @@ fun pushCRel (env : env) x k =
          renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
                             | Named' (n, c) => Named' (n, lift c)) (#renameE env),
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
-         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+         namedE = #namedE env,
 
          renameSgn = #renameSgn env,
          sgn = #sgn env,
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e3d76ed6..86ae6067 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -875,12 +875,19 @@
              []
          else
              let
+                 (*val befor = Time.now ()
+                 val old1 = c1
+                 val old2 = c2*)
                  val (c1, gs1) = hnormCon (env, denv) c1
                  val (c2, gs2) = hnormCon (env, denv) c2
              in
                  let
                      val gs3 = unifyCons'' (env, denv) c1 c2
                  in
+                     (*prefaces "unifyCons'" [("c1", p_con env old1),
+                                            ("c2", p_con env old2),
+                                            ("t", PD.string (LargeReal.toString (Time.toReal
+                                                                                 (Time.- (Time.now (), befor)))))];*)
                      gs1 @ gs2 @ gs3
                  end
                  handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
@@ -906,7 +913,16 @@
                  err CExplicitness
              else
                  (unifyKinds d1 d2;
-                  unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
+                  let
+                      val denv' = D.enter denv
+                      (*val befor = Time.now ()*)
+                      val env' = E.pushCRel env x1 d1
+                  in
+                      (*TextIO.print ("E.pushCRel: "
+                                    ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
+                                    ^ "\n");*)
+                      unifyCons' (env', denv') r1 r2
+                  end)
            | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
 
            | (L'.CRel n1, L'.CRel n2) =>
@@ -1478,6 +1494,7 @@ val makeInstantiable =
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
         (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
+        (*val befor = Time.now ()*)
 
         val r = case e of
             L.EAnnot (e, t) =>
@@ -1770,7 +1787,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
             end
     in
         (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
-                            ("t", PD.string (LargeInt.toString (Time.toMilliseconds (Time.- (Time.now (), befor)))))];*)
+                            ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*)
         r
     end
 
@@ -2913,6 +2930,7 @@ fun wildifyStr env (str, sgn) =
 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
     let
         (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
+        (*val befor = Time.now ()*)
 
         val r = 
             case d of
@@ -3293,8 +3311,8 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
         (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
     in
         (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
-                             ("t", PD.string (LargeInt.toString (Time.toMilliseconds
-                                                                     (Time.- (Time.now (), befor)))))];*)
+                             ("t", PD.string (LargeReal.toString (Time.toReal
+                                                                      (Time.- (Time.now (), befor)))))];*)
 
         r
     end
-- 
cgit v1.2.3