From bc67c873a23309d2ef9e8365e0a9b7f8f15577ca Mon Sep 17 00:00:00 2001 From: FrigoEU Date: Mon, 29 Jul 2019 11:09:28 +0200 Subject: Don't use interfaces anymore for ModDb validity, but check for undetermined unif vars --- src/elaborate.sml | 17 ++++----------- src/main.mlton.sml | 6 ++++-- src/mod_db.sig | 4 +--- src/mod_db.sml | 63 ++++++++++++++++++++++++++++++++++++++---------------- 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) -- cgit v1.2.3