Don't use interfaces anymore for ModDb validity, but check for undetermined unif vars

4 files changed, 54 insertions, 36 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 3547d784..1c76250f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4209,10 +4209,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                            | _ => ();
                          Option.map (fn tm => ModDb.insert (dNew,
                                                             tm,
-                                                            ErrorMsg.stopElabStructureAndGetErrored x,
-                                                            case sgno of
-                                                                NONE => true
-                                                              | SOME sgn => false
+                                                            ErrorMsg.stopElabStructureAndGetErrored x
                                                             )) tmo;
                          ([dNew], (env', denv', gs' @ gs))
                      end)
@@ -4248,7 +4245,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, ErrorMsg.stopElabStructureAndGetErrored x, false)) tmo;
+                         Option.map (fn tm => ModDb.insert (dNew, tm, ErrorMsg.stopElabStructureAndGetErrored x)) tmo;
                          ([dNew], (env', denv, enD gs' @ gs))
                      end)
 
@@ -4767,7 +4764,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, false, false); (* TODO: also check for errors? *)
+                    ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm, false); (* TODO: also check for errors? *)
                     (basis_n, env', sgn)
                 end
               | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) =>
@@ -4826,7 +4823,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, false, false); (* TODO: also check for errors? *)
+                    ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm, false); (* TODO: also check for errors? *)
                     (top_n, env', topSgn, topStr)
                 end
               | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) =>
@@ -5109,12 +5106,6 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
         else
             ();
 
-        if ErrorMsg.anyErrors () then
-            ()
-        else
-            ModDb.flagAllOk ();
-        
-
         (*Print.preface("File", ElabPrint.p_file env file);*)
 
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index bfa40265..cb7c8a77 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -435,10 +435,12 @@ val () = (Globals.setResetTime ();
                                                                 wrs = [Socket.sockDesc sock],
                                                                 exs = [],
                                                                 timeout = SOME (Time.fromSeconds 1)}))) then
-                     (app (fn arg => send (sock, arg ^ "\n")) args;
+                     (TextIO.print "Using daemon\n";
+                      app (fn arg => send (sock, arg ^ "\n")) args;
                       send (sock, "\n");
                       OS.Process.exit (wait ()))
                  else
                      (OS.FileSys.remove socket;
                       raise OS.SysErr ("", NONE))
-             end handle OS.SysErr _ => OS.Process.exit (oneRun args))
+             end handle OS.SysErr _ =>
+                        OS.Process.exit (oneRun args))
diff --git a/src/mod_db.sig b/src/mod_db.sig
index f4bf661a..c45fd203 100644
--- a/src/mod_db.sig
+++ b/src/mod_db.sig
@@ -30,14 +30,12 @@
 signature MOD_DB = sig
     val reset : unit -> unit
 
-    val insert : Elab.decl * Time.time * bool (* hasErrors *) * bool (* hasInference *) -> unit
+    val insert : Elab.decl * Time.time * bool (* hasErrors *) -> 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 53bcdc7e..2e2b9c6c 100644
--- a/src/mod_db.sml
+++ b/src/mod_db.sml
@@ -43,8 +43,7 @@ structure IM = IntBinaryMap
 type oneMod = {Decl : decl,
                When : Time.time,
                Deps : SS.set,
-               HasErrors: bool,
-               HasInference: bool
+               HasErrors: bool
               }
 
 val byName = ref (SM.empty : oneMod SM.map)
@@ -59,19 +58,43 @@ fun printByName (bn: oneMod SM.map): unit =
                   let
                       val name = #1 tup
                       val m = #2 tup
-                      val renderedDeps = String.concatWith ", " (SS.listItems (#Deps m))
+                      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) =
+fun printById (bi: string IM.map): unit =
+    (TextIO.print ("Contents of ModDb.byId: \n");
+     List.app (fn tup =>
+                  let
+                      val i = #1 tup
+                      val name = #2 tup
+                  in
+                      TextIO.print ("  " ^  Int.toString i ^": "^ name ^"\n")
+                  end)
+              (IM.listItemsi bi))
+
+fun dContainsUndeterminedUnif d =
+    ElabUtil.Decl.exists
+        {kind = fn _ => false,
+         con = fn _ => false,
+         exp = fn e => case e of
+                           EUnif (ref NONE) => true 
+                         | _ => false,
+         sgn_item = fn _ => false,
+         sgn = fn _ => false,
+         str = fn _ => false,
+         decl = fn _ => false}
+        d
+
+fun insert (d, tm, hasErrors) =
     let
         val xn =
             case #1 d of
@@ -83,10 +106,13 @@ fun insert (d, tm, hasErrors, hasInference) =
             NONE => ()
           | SOME (x, n) =>
             let
+                (* Keep module when it's file didn't change and it was OK before *)
                 val skipIt =
                     case SM.find (!byName, x) of
                         NONE => false
                       | SOME r => #When r = tm
+                                  andalso not (#HasErrors r)
+                                  andalso not (dContainsUndeterminedUnif (#Decl r))
             in
                 if skipIt then
                     ()
@@ -94,8 +120,16 @@ fun insert (d, tm, hasErrors, hasInference) =
                     let
                         fun doMod (n', deps) =
                             case IM.find (!byId, n') of
-                                NONE => raise Fail ("ModDb: Trying to make dep tree but couldn't find module " ^ Int.toString n')
-                              (* This should probably throw: *)
+                                NONE =>
+                                (TextIO.print ("MISSED_DEP: " ^ Int.toString n' ^"\n");
+                                 deps)
+                                (* raise Fail ("ModDb: Trying to make dep tree but couldn't find module " ^ Int.toString n') *)
+                              (* I feel like this should throw, but the dependency searching algorithm *)
+                              (* is not 100% precise. I encountered problems in json.urs: *)
+                              (*   datatype r = Rec of M.t r *)
+                              (* M is the structure passed to the Recursive functor, so this is not an external dependency *)
+                              (* I'm just not sure how to filter these out yet *)
+                              (* I still think this should 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' =>
@@ -143,11 +177,11 @@ fun insert (d, tm, hasErrors, hasInference) =
                                              {Decl = d,
                                               When = tm,
                                               Deps = deps,
-                                              HasErrors = hasErrors,
-                                              HasInference = hasInference
+                                              HasErrors = hasErrors
                                             });
                         byId := IM.insert (!byId, n, x)
                         (* printByName (!byName) *)
+                        (* printById (!byId) *)
                     end
             end
     end
@@ -158,7 +192,7 @@ fun lookup (d : Source.decl) =
         (case SM.find (!byName, x) of
              NONE => NONE
            | SOME r =>
-             if tm = #When r andalso not (#HasErrors r) andalso not (#HasInference r) then
+             if tm = #When r andalso not (#HasErrors r) andalso not (dContainsUndeterminedUnif (#Decl r)) then
                  SOME (#Decl r)
              else
                  NONE)
@@ -166,7 +200,7 @@ fun lookup (d : Source.decl) =
         (case SM.find (!byName, x) of
              NONE => NONE
            | SOME r =>
-             if tm = #When r andalso not (#HasErrors r) andalso not (#HasInference r) then
+             if tm = #When r andalso not (#HasErrors r) andalso not (dContainsUndeterminedUnif (#Decl r)) then
                  SOME (#Decl r)
              else
                  NONE)
@@ -175,13 +209,6 @@ 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)