From 562694cbb5beb31906610b7eabf42a56087673b5 Mon Sep 17 00:00:00 2001 From: FrigoEU Date: Sun, 7 Jul 2019 17:55:02 +0200 Subject: First iteration of more detailed elaboration caching --- src/elaborate.sml | 26 +++++++++++++++++++------- src/errormsg.sig | 4 ++++ src/errormsg.sml | 21 ++++++++++++++++++++- src/mod_db.sig | 4 +++- src/mod_db.sml | 47 +++++++++++++++++++++++++++++++++++++++++------ 5 files changed, 87 insertions(+), 15 deletions(-) diff --git a/src/elaborate.sml b/src/elaborate.sml index 97b36a0b..3547d784 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2800,7 +2800,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) end) -and elabSgn (env, denv) (sgn, loc) = +and elabSgn (env, denv) (sgn, loc): (L'.sgn * D.goal list) = case sgn of L.SgnConst sgis => let @@ -4165,6 +4165,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = | NONE => let val () = if !verbose then TextIO.print ("CHECK: " ^ x ^ "\n") else () + val () = ErrorMsg.startElabStructure x val () = if x = "Basis" then raise Fail "Not allowed to redefine structure 'Basis'" @@ -4206,7 +4207,13 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = L'.StrFun _ => () | _ => strError env (FunctorRebind loc)) | _ => (); - Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; + Option.map (fn tm => ModDb.insert (dNew, + tm, + ErrorMsg.stopElabStructureAndGetErrored x, + case sgno of + NONE => true + | SOME sgn => false + )) tmo; ([dNew], (env', denv', gs' @ gs)) end) @@ -4221,6 +4228,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = end | NONE => let + val () = ErrorMsg.startElabStructure x + val (sgn', gs') = elabSgn (env, denv) sgn val (env', n) = E.pushStrNamed env x sgn' @@ -4239,7 +4248,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = epreface ("item", p_sgn_item env sgi))) | _ => raise Fail "FFI signature isn't SgnConst"; - Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; + Option.map (fn tm => ModDb.insert (dNew, tm, ErrorMsg.stopElabStructureAndGetErrored x, false)) tmo; ([dNew], (env', denv, enD gs' @ gs)) end) @@ -4735,6 +4744,8 @@ fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env fun elabFile basis basis_tm topStr topSgn top_tm env file = let val () = ModDb.snapshot () + val () = ErrorMsg.resetStructureTracker () + val () = mayDelay := true val () = delayedUnifs := [] @@ -4756,7 +4767,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (env', basis_n) = E.pushStrNamed env "Basis" sgn in - ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm); + ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm, false, false); (* TODO: also check for errors? *) (basis_n, env', sgn) end | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) => @@ -4815,7 +4826,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (env', top_n) = E.pushStrNamed env' "Top" topSgn in - ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm); + ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm, false, false); (* TODO: also check for errors? *) (top_n, env', topSgn, topStr) end | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) => @@ -5099,9 +5110,10 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = (); if ErrorMsg.anyErrors () then - ModDb.revert () + () else - (); + ModDb.flagAllOk (); + (*Print.preface("File", ElabPrint.p_file env file);*) diff --git a/src/errormsg.sig b/src/errormsg.sig index 92425842..b4a508d9 100644 --- a/src/errormsg.sig +++ b/src/errormsg.sig @@ -48,6 +48,10 @@ signature ERROR_MSG = sig val posOf : int -> pos val spanOf : int * int -> span + val startElabStructure : string -> unit + val stopElabStructureAndGetErrored : string -> bool (* Did the module elab encounter errors? *) + + val resetStructureTracker: unit -> unit val resetErrors : unit -> unit val anyErrors : unit -> bool val error : string -> unit diff --git a/src/errormsg.sml b/src/errormsg.sml index 8f3c93b1..eee20768 100644 --- a/src/errormsg.sml +++ b/src/errormsg.sml @@ -88,12 +88,31 @@ fun spanOf (pos1, pos2) = {file = !file, val errors = ref false +val structuresCurrentlyElaborating: ((string * bool) list) ref = ref nil + +fun startElabStructure s = + structuresCurrentlyElaborating := ((s, false) :: !structuresCurrentlyElaborating) +fun stopElabStructureAndGetErrored s = + let + val errored = + case List.find (fn x => #1 x = s) (!structuresCurrentlyElaborating) of + NONE => false + | SOME tup => #2 tup + val () = structuresCurrentlyElaborating := + (List.filter (fn x => #1 x <> s) (!structuresCurrentlyElaborating)) + in + errored + end +fun resetStructureTracker () = + structuresCurrentlyElaborating := [] fun resetErrors () = errors := false fun anyErrors () = !errors fun error s = (TextIO.output (TextIO.stdErr, s); TextIO.output1 (TextIO.stdErr, #"\n"); - errors := true) + errors := true; + structuresCurrentlyElaborating := + List.map (fn (s, e) => (s, true)) (!structuresCurrentlyElaborating)) fun errorAt (span : span) s = (TextIO.output (TextIO.stdErr, #file span); TextIO.output (TextIO.stdErr, ":"); diff --git a/src/mod_db.sig b/src/mod_db.sig index 8f78f2c2..f4bf661a 100644 --- a/src/mod_db.sig +++ b/src/mod_db.sig @@ -30,12 +30,14 @@ signature MOD_DB = sig val reset : unit -> unit - val insert : Elab.decl * Time.time -> unit + val insert : Elab.decl * Time.time * bool (* hasErrors *) * bool (* hasInference *) -> unit (* Here's a declaration, including the modification timestamp of the file it came from. * We might invalidate other declarations that depend on this one, if the timestamp has changed. *) val lookup : Source.decl -> Elab.decl option + val flagAllOk : unit -> unit + (* Allow undoing to snapshots after failed compilations. *) val snapshot : unit -> unit val revert : unit -> unit diff --git a/src/mod_db.sml b/src/mod_db.sml index 2d6b285b..53bcdc7e 100644 --- a/src/mod_db.sml +++ b/src/mod_db.sml @@ -42,7 +42,10 @@ structure IM = IntBinaryMap type oneMod = {Decl : decl, When : Time.time, - Deps : SS.set} + Deps : SS.set, + HasErrors: bool, + HasInference: bool + } val byName = ref (SM.empty : oneMod SM.map) val byId = ref (IM.empty : string IM.map) @@ -50,7 +53,25 @@ val byId = ref (IM.empty : string IM.map) fun reset () = (byName := SM.empty; byId := IM.empty) -fun insert (d, tm) = +fun printByName (bn: oneMod SM.map): unit = + (TextIO.print ("Contents of ModDb.byName: \n"); + List.app (fn tup => + let + val name = #1 tup + val m = #2 tup + val renderedDeps = String.concatWith ", " (SS.listItems (#Deps m)) + val renderedMod = + " " ^ name + ^ ". Stored at : " ^ Time.toString (#When m) + ^", HasErrors: " ^ Bool.toString (#HasErrors m) + ^", HasInference: " ^ Bool.toString (#HasInference m) + ^". Deps: " ^ renderedDeps ^"\n" + in + TextIO.print renderedMod + end) + (SM.listItemsi bn)) + +fun insert (d, tm, hasErrors, hasInference) = let val xn = case #1 d of @@ -73,7 +94,10 @@ fun insert (d, tm) = let fun doMod (n', deps) = case IM.find (!byId, n') of - NONE => deps + NONE => raise Fail ("ModDb: Trying to make dep tree but couldn't find module " ^ Int.toString n') + (* This should probably throw: *) + (* Trying to add a dep for a module but can't find the dep... *) + (* That will always cause a hole in the dependency tree and cause problems down the line *) | SOME x' => SS.union (deps, SS.add (case SM.find (!byName, x') of @@ -118,8 +142,12 @@ fun insert (d, tm) = x, {Decl = d, When = tm, - Deps = deps}); + Deps = deps, + HasErrors = hasErrors, + HasInference = hasInference + }); byId := IM.insert (!byId, n, x) + (* printByName (!byName) *) end end end @@ -130,7 +158,7 @@ fun lookup (d : Source.decl) = (case SM.find (!byName, x) of NONE => NONE | SOME r => - if tm = #When r then + if tm = #When r andalso not (#HasErrors r) andalso not (#HasInference r) then SOME (#Decl r) else NONE) @@ -138,7 +166,7 @@ fun lookup (d : Source.decl) = (case SM.find (!byName, x) of NONE => NONE | SOME r => - if tm = #When r then + if tm = #When r andalso not (#HasErrors r) andalso not (#HasInference r) then SOME (#Decl r) else NONE) @@ -147,6 +175,13 @@ fun lookup (d : Source.decl) = val byNameBackup = ref (!byName) val byIdBackup = ref (!byId) +fun flagAllOk () = byName := SM.map (fn r => { Decl = #Decl r + , When = #When r + , Deps = #Deps r + , HasErrors = #HasErrors r + , HasInference = false + }) (!byName) + fun snapshot () = (byNameBackup := !byName; byIdBackup := !byId) fun revert () = (byName := !byNameBackup; byId := !byIdBackup) -- cgit v1.2.3