First iteration of more detailed elaboration caching

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)