diff options
| -rw-r--r-- | src/elab_env.sml | 4 | ||||
| -rw-r--r-- | src/elaborate.sml | 26 |
2 files changed, 24 insertions, 6 deletions
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 |