From 6a3bbbaa22b9e4a1edf907ab0a9eb196d83a8b38 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 6 Jul 2019 16:07:20 -0400 Subject: Fix subsignature checking for mutually recursive types --- src/elaborate.sml | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index 51d00bd8..97b36a0b 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3284,12 +3284,27 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = SOME env end - val env = E.pushCNamedAs env x1 n1 k' NONE - val env = if n1 = n2 then - env - else - (cparts (n2, n1); - E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))) + fun dt_pusher (dts1, dts2, env) = + case (dts1, dts2) of + ((x1, n1, xs1, _) :: dts1', (x2, n2, xs2, _) :: dts2') => + let + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 + + val env = E.pushCNamedAs env x1 n1 k' NONE + val env = if n1 = n2 then + env + else + (cparts (n2, n1); + E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))) + in + dt_pusher (dts1', dts2', env) + end + | _ => env + val env = case #1 sgi1All of + L'.SgiDatatype dts1 => dt_pusher (dts1, dts2, env) + | _ => env + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 fun xncBad ((x1, _, t1), (x2, _, t2)) = String.compare (x1, x2) <> EQUAL -- cgit v1.2.3 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(-) (limited to 'src/elaborate.sml') 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 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(-) (limited to 'src/elaborate.sml') 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 From 2a7c54badfcd4e30105a0127b25975000ff09bbb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 18 Sep 2019 13:51:13 -0400 Subject: Disallow wildcards in signatures (should help with #174) --- src/elab_err.sig | 2 ++ src/elab_err.sml | 6 ++++++ src/elaborate.sml | 35 ++++++++++++++++++++++++++--------- tests/wildsig.ur | 7 +++++++ 4 files changed, 41 insertions(+), 9 deletions(-) create mode 100644 tests/wildsig.ur (limited to 'src/elaborate.sml') diff --git a/src/elab_err.sig b/src/elab_err.sig index acf137df..fc80fcac 100644 --- a/src/elab_err.sig +++ b/src/elab_err.sig @@ -29,6 +29,7 @@ signature ELAB_ERR = sig datatype kind_error = UnboundKind of ErrorMsg.span * string + | KDisallowedWildcard of ErrorMsg.span val kindError : ElabEnv.env -> kind_error -> unit @@ -47,6 +48,7 @@ signature ELAB_ERR = sig | DuplicateField of ErrorMsg.span * string | ProjBounds of Elab.con * int | ProjMismatch of Elab.con * Elab.kind + | CDisallowedWildcard of ErrorMsg.span val conError : ElabEnv.env -> con_error -> unit diff --git a/src/elab_err.sml b/src/elab_err.sml index 385caca3..bbe1c160 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -40,11 +40,14 @@ val p_kind = P.p_kind datatype kind_error = UnboundKind of ErrorMsg.span * string + | KDisallowedWildcard of ErrorMsg.span fun kindError env err = case err of UnboundKind (loc, s) => ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) + | KDisallowedWildcard loc => + ErrorMsg.errorAt loc "Wildcard not allowed in signature" datatype kunify_error = KOccursCheckFailed of kind * kind @@ -76,6 +79,7 @@ datatype con_error = | DuplicateField of ErrorMsg.span * string | ProjBounds of con * int | ProjMismatch of con * kind + | CDisallowedWildcard of ErrorMsg.span fun conError env err = case err of @@ -101,6 +105,8 @@ fun conError env err = (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; eprefaces' [("Constructor", p_con env c), ("Kind", p_kind env k)]) + | CDisallowedWildcard loc => + ErrorMsg.errorAt loc "Wildcard not allowed in signature" datatype cunify_error = CKind of kind * kind * E.env * kunify_error diff --git a/src/elaborate.sml b/src/elaborate.sml index 97b36a0b..6ffb7716 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -260,6 +260,19 @@ end + (* Wildcards are disallowed inside signatures. + * We use a flag to indicate when we are in a signature, + * with a helper function for entering this mode and properly backing out afterward. *) + val inSignature = ref false + fun enterSignature f = + let + val inS = !inSignature + in + inSignature := true; + (f () handle ex => (inSignature := inS; raise ex)) + before inSignature := inS + end + fun elabKind env (k, loc) = case k of L.KType => (L'.KType, loc) @@ -268,7 +281,7 @@ | L.KRecord k => (L'.KRecord (elabKind env k), loc) | L.KUnit => (L'.KUnit, loc) | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) - | L.KWild => kunif env loc + | L.KWild => if !inSignature then (kindError env (KDisallowedWildcard loc); kerror) else kunif env loc | L.KVar s => (case E.lookupK env s of NONE => @@ -531,11 +544,15 @@ end | L.CWild k => - let - val k' = elabKind env k - in - (cunif env (loc, k'), k', []) - end + if !inSignature then + (conError env (CDisallowedWildcard loc); + (cerror, kerror, [])) + else + let + val k' = elabKind env k + in + (cunif env (loc, k'), k', []) + end fun kunifsRemain k = case k of @@ -4146,7 +4163,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = | L.DSgn (x, sgn) => let - val (sgn', gs') = elabSgn (env, denv) sgn + val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn) val (env', n) = E.pushSgnNamed env x sgn' in ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) @@ -4171,7 +4188,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = else () - val formal = Option.map (elabSgn (env, denv)) sgno + val formal = enterSignature (fn () => Option.map (elabSgn (env, denv)) sgno) val (str', sgn', gs') = case formal of @@ -4221,7 +4238,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = end | NONE => let - val (sgn', gs') = elabSgn (env, denv) sgn + val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn) val (env', n) = E.pushStrNamed env x sgn' diff --git a/tests/wildsig.ur b/tests/wildsig.ur new file mode 100644 index 00000000..336772a7 --- /dev/null +++ b/tests/wildsig.ur @@ -0,0 +1,7 @@ +signature S = sig + val x : _ +end + +structure M : S = struct + val x = 7 +end -- cgit v1.2.3 From 3f8929c83b451837fcd9dc9475534c0e78967ab2 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 18 Sep 2019 15:33:35 -0400 Subject: Signatures should be allowed to use wildcards for kinds associated with concrete constructors --- src/elaborate.sml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index 6ffb7716..c6825150 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2577,7 +2577,14 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = let val k' = case ko of NONE => kunif env loc - | SOME k => elabKind env k + | SOME k => + case #1 k of + L.KWild => kunif env loc + (* Why duplicate this case of elabKind here? + * To avoid flagging a disallowed wildcard in + * a signature, since we are guaranteed to + * resolve this kind locally during elaboration. *) + | _ => elabKind env k val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') @@ -4756,6 +4763,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val () = mayDelay := true val () = delayedUnifs := [] val () = delayedExhaustives := [] + val () = inSignature := false val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan) val (basis_n, env', sgn) = -- cgit v1.2.3 From abf8a0434cb1c1ab22a50182ffdc6cf0c4645523 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 20 Sep 2019 13:39:07 -0400 Subject: Laxer wildcard restriction for signatures --- src/elaborate.sml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index c6825150..fbbde303 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -264,14 +264,16 @@ * We use a flag to indicate when we are in a signature, * with a helper function for entering this mode and properly backing out afterward. *) val inSignature = ref false - fun enterSignature f = + fun enterSignature' b f = let val inS = !inSignature in - inSignature := true; + inSignature := b; (f () handle ex => (inSignature := inS; raise ex)) before inSignature := inS end + fun enterSignature f = enterSignature' true f + fun exitSignature f = enterSignature' false f fun elabKind env (k, loc) = case k of @@ -2577,14 +2579,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = let val k' = case ko of NONE => kunif env loc - | SOME k => - case #1 k of - L.KWild => kunif env loc - (* Why duplicate this case of elabKind here? - * To avoid flagging a disallowed wildcard in - * a signature, since we are guaranteed to - * resolve this kind locally during elaboration. *) - | _ => elabKind env k + | SOME k => exitSignature (fn () => elabKind env k) + (* Waive wildcard restriction within translation + * of kind annotation. The kind of [c] will allow + * us to resolve it fully. *) val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') -- cgit v1.2.3 From c388a91762e9dd9aef2eb097963af020c0e452f8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 21 Sep 2019 08:33:09 -0400 Subject: Desugaring of SQL constraints uses wildcards, so allow that even in signatures --- src/elaborate.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index fbbde303..9718ccad 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2734,7 +2734,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val ct = (L'.CApp (ct, c'), loc) val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) - val (pe', pet, gs'') = elabExp (env', denv) pe + val (pe', pet, gs'') = exitSignature (fn () => elabExp (env', denv) pe) val gs'' = List.mapPartial (fn Disjoint x => SOME x | _ => NONE) gs'' @@ -2742,7 +2742,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val pst = (L'.CApp (pst, c'), loc) val pst = (L'.CApp (pst, pkey), loc) - val (ce', cet, gs''') = elabExp (env', denv) ce + val (ce', cet, gs''') = exitSignature (fn () => elabExp (env', denv) ce) val gs''' = List.mapPartial (fn Disjoint x => SOME x | _ => NONE) gs''' -- cgit v1.2.3 From 25b0685cefe772c73562665a4cc8d2d40e5ff600 Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Wed, 11 Dec 2019 13:58:01 +0100 Subject: Use elabFile completely instead of rebuilding it partially --- src/compiler.sml | 2 +- src/elaborate.sig | 5 +++- src/elaborate.sml | 4 ++- src/lsp.sml | 73 ++++++++++++++++++++++++++----------------------------- 4 files changed, 42 insertions(+), 42 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/compiler.sml b/src/compiler.sml index fab939f9..ab7b86b4 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1283,7 +1283,7 @@ val elaborate = { in Elaborate.elabFile basis (OS.FileSys.modTime basisF) topStr topSgn (if Time.< (tm1, tm2) then tm2 else tm1) - ElabEnv.empty file + ElabEnv.empty (fn env => env) file end, print = ElabPrint.p_file ElabEnv.empty } diff --git a/src/elaborate.sig b/src/elaborate.sig index 88ea068f..d6747241 100644 --- a/src/elaborate.sig +++ b/src/elaborate.sig @@ -29,7 +29,10 @@ signature ELABORATE = sig val elabFile : Source.sgn_item list -> Time.time -> Source.decl list -> Source.sgn_item list -> Time.time - -> ElabEnv.env -> Source.file -> Elab.file + -> ElabEnv.env + -> (ElabEnv.env -> ElabEnv.env) (* Adapt env after stdlib but before elaborate *) + -> Source.file + -> Elab.file val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option diff --git a/src/elaborate.sml b/src/elaborate.sml index d5e190fa..85234775 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4760,7 +4760,7 @@ and elabStr (env, denv) (str, loc) = fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env -fun elabFile basis basis_tm topStr topSgn top_tm env file = +fun elabFile basis basis_tm topStr topSgn top_tm env changeEnv file = let val () = ModDb.snapshot () val () = ErrorMsg.resetStructureTracker () @@ -4857,6 +4857,8 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} + val env' = changeEnv env' + fun elabDecl' x = (resetKunif (); resetCunif (); diff --git a/src/lsp.sml b/src/lsp.sml index 34209231..b5a92683 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -417,9 +417,7 @@ end structure SM = BinaryMapFn(SK) type fileState = - { envOfPreviousModules : ElabEnv.env - , decls : Elab.decl list - } + { decls : Elab.decl list } type state = { urpPath : string , fileStates : fileState SM.map @@ -498,6 +496,8 @@ fun calculateFileState (state: state) (fileName: string): (fileState option * Ls then () else raise Fail ("Can only handle .ur files for now") val () = Elaborate.unifyMore := true + (* To reuse Basis and Top *) + val () = Elaborate.incremental := true (* Parsing .urp *) val job = case C.run (C.transform C.parseUrp "parseUrp") (#urpPath state) of NONE => raise LspError (InternalError ("Couldn't parse .urp file at " ^ (#urpPath state))) @@ -531,28 +531,35 @@ fun calculateFileState (state: state) (fileName: string): (fileState option * Ls } end) modulesBeforeThisFile - (* Parsing Basis and Top .urs *) + (* Parsing Basis and Top *) + val basisF = Settings.libFile "basis.urs" + val topF = Settings.libFile "top.urs" + val topF' = Settings.libFile "top.ur" + + val tm1 = OS.FileSys.modTime topF + val tm2 = OS.FileSys.modTime topF' + val parsedBasisUrs = - case C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "basis.urs") of - NONE => raise LspError (InternalError ("Failed to parse basis.urs file at " ^ (Settings.libFile "basis.urs"))) + case C.run (C.transform C.parseUrs "parseUrs") basisF of + NONE => raise LspError (InternalError ("Failed to parse basis.urs file at " ^ basisF)) | SOME a => a val parsedTopUrs = - case C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "top.urs") of - NONE => raise LspError (InternalError ("Failed to parse top.urs file at " ^ (Settings.libFile "top.urs"))) + case C.run (C.transform C.parseUrs "parseUrs") topF of + NONE => raise LspError (InternalError ("Failed to parse top.urs file at " ^ topF)) | SOME a => a - (* Building env with previous .urs files *) - val envWithStdLib = - addSgnToEnv - (addSgnToEnv ElabEnv.empty parsedBasisUrs (Settings.libFile "basis.urs") true) - parsedTopUrs (Settings.libFile "top.urs") true - val envBeforeThisFile = List.foldl (fn (sgn, env) => addSgnToEnv env (#parsed sgn) (#fileName sgn) false) envWithStdLib parsedUrss + val parsedTopUr = + case C.run (C.transform C.parseUr "parseUr") topF' of + NONE => raise LspError (InternalError ("Failed to parse top.ur file at " ^ topF')) + | SOME a => a + (* Parsing .ur and .urs of current file *) - val (parsedUrs: (Source.sgn_item list) option) = + val (parsedUrs: Source.sgn option) = (if OS.FileSys.access (fileName ^ "s", []) then case C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s") of NONE => NONE - | SOME a => SOME a + | SOME a => SOME ( Source.SgnConst a + , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) else NONE) handle ex => NONE val () = ErrorMsg.resetErrors () @@ -562,34 +569,22 @@ fun calculateFileState (state: state) (fileName: string): (fileState option * Ls case parsedUrO of NONE => (* Parse error *) (NONE, List.map errorToDiagnostic (ErrorMsg.readErrorLog ())) | SOME parsedUr => - (* .ur file found -> typecheck *) + (* Parsing of .ur succeeded *) let - val (str, sgn', gs) = - Elaborate.elabStr - (envBeforeThisFile, Disjoint.empty) - (Source.StrConst parsedUr, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) - val () = - (* .urs file found -> check and compare with .ur file *) - (case parsedUrs of - NONE => () - | SOME parsedUrs => - let - val (sgn, gs) = Elaborate.elabSgn - (envBeforeThisFile, Disjoint.empty) - ( Source.SgnConst parsedUrs - , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}); - in - Elaborate.subSgn envBeforeThisFile ErrorMsg.dummySpan sgn' sgn - end) + val loc = {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos} + val res = Elaborate.elabFile + parsedBasisUrs tm1 parsedTopUr parsedTopUrs tm2 ElabEnv.empty + (* Adding urs's of previous modules to env *) + (fn envB => List.foldl (fn (sgn, env) => addSgnToEnv env (#parsed sgn) (#fileName sgn) false) envB parsedUrss) + [( Source.DStr (C.moduleOf fileName, parsedUrs, NONE, (Source.StrConst parsedUr, loc), false) + , loc )] (* report back errors (as Diagnostics) *) val errors = ErrorMsg.readErrorLog () - val decls = case str of - (Elab.StrConst decls, _) => decls + val decls = case List.last res of + (Elab.DStr (_, _, _, (Elab.StrConst decls, _)), _) => decls | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration") in - (SOME { envOfPreviousModules = envBeforeThisFile - , decls = decls - }, + (SOME { decls = decls }, List.map errorToDiagnostic errors) end end -- cgit v1.2.3 From ef4e0c207abd0e41badf7bf0052b498eb6c01d43 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 7 Feb 2020 10:34:21 -0500 Subject: Fix signature matching of an imported datatype vs. a fresh datatype --- src/elab_print.sml | 5 ++++- src/elaborate.sml | 12 +++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elab_print.sml b/src/elab_print.sml index 8a6a651a..637164f4 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -546,7 +546,10 @@ fun p_datatype env (x, n, xs, cons) = val env = E.pushCNamedAs env x n k NONE val env = foldl (fn (x, env) => E.pushCRel env x k) env xs in - box [string x, + box [(if !debug then + string (x ^ "_" ^ Int.toString n) + else + string x), p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", diff --git a/src/elaborate.sml b/src/elaborate.sml index 85234775..e975cabe 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3325,8 +3325,14 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = | _ => env val env = case #1 sgi1All of L'.SgiDatatype dts1 => dt_pusher (dts1, dts2, env) - | _ => env - + | _ => foldl (fn ((x2, n2, xs2, _), env) => + let + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs2 + in + E.pushCNamedAs env x2 n2 k' NONE + end) env dts2 + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 fun xncBad ((x1, _, t1), (x2, _, t2)) = String.compare (x1, x2) <> EQUAL @@ -4229,7 +4235,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = L'.StrFun _ => () | _ => strError env (FunctorRebind loc)) | _ => (); - Option.map (fn tm => ModDb.insert (dNew, + Option.app (fn tm => ModDb.insert (dNew, tm, ErrorMsg.stopElabStructureAndGetErrored x )) tmo; -- cgit v1.2.3