From 0e520d3fd675bcebb5751bd1a0c304033f4f7782 Mon Sep 17 00:00:00 2001 From: FrigoEU Date: Thu, 1 Aug 2019 17:38:09 +0200 Subject: Improved typeOf searching and handling of Top and Basis --- src/elaborate.sig | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/elaborate.sig') diff --git a/src/elaborate.sig b/src/elaborate.sig index d60cff42..03359814 100644 --- a/src/elaborate.sig +++ b/src/elaborate.sig @@ -47,4 +47,10 @@ signature ELABORATE = sig val incremental : bool ref val verbose : bool ref + val dopen: ElabEnv.env + -> { str: int + , strs: string list + , sgn: Elab.sgn } + -> (Elab.decl list * ElabEnv.env) + end -- cgit v1.2.3 From 053783525d8365b8a498ac38942d44f4669d6a54 Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Tue, 10 Dec 2019 20:21:35 +0100 Subject: First version of calculateFileState --- src/elaborate.sig | 14 +++++ src/lsp.sml | 149 +++++++++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 150 insertions(+), 13 deletions(-) (limited to 'src/elaborate.sig') diff --git a/src/elaborate.sig b/src/elaborate.sig index 03359814..88ea068f 100644 --- a/src/elaborate.sig +++ b/src/elaborate.sig @@ -53,4 +53,18 @@ signature ELABORATE = sig , sgn: Elab.sgn } -> (Elab.decl list * ElabEnv.env) + val elabSgn: (ElabEnv.env * Disjoint.env) + -> Source.sgn + -> (Elab.sgn * Disjoint.goal list) + + datatype constraint = + Disjoint of Disjoint.goal + | TypeClass of ElabEnv.env * Elab.con * Elab.exp option ref * ErrorMsg.span + + val elabStr: (ElabEnv.env * Disjoint.env) + -> Source.str + -> (Elab.str * Elab.sgn * constraint list) + + val subSgn: ElabEnv.env -> ErrorMsg.span -> Elab.sgn -> Elab.sgn -> unit + end diff --git a/src/lsp.sml b/src/lsp.sml index cff30d5e..89a0e4b2 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -1,3 +1,5 @@ +structure C = Compiler + fun trim (s: substring): substring = Substring.dropr (fn c => c = #" " orelse c = #"\n" orelse c = #"\r") @@ -327,22 +329,143 @@ type fileState = , decls : Elab.decl list } type state = - { rootUri : LspSpec.documentUri + { urpPath : string , fileStates : fileState SM.map } val stateRef = ref (NONE: state option) +fun scanDir (f: string -> bool) (path: string) = + let + val dir = OS.FileSys.openDir path + fun doScanDir acc = + case OS.FileSys.readDir dir of + NONE => (OS.FileSys.closeDir dir; acc) + | SOME fname => + (if f fname + then doScanDir (fname :: acc) + else doScanDir acc) + in + doScanDir [] + end + (* Throws Fail if can't init *) fun initState (initParams: LspSpec.initializeParams): state = - { rootUri = case #rootUri initParams of - NONE => raise Fail "Failed to initialize: no rootUri" - | SOME a => a - , fileStates = SM.empty - } + let + val rootPath = case #rootUri initParams of + NONE => raise Fail "No rootdir found" + | SOME a => #path a + val foundUrps = scanDir (fn fname => OS.Path.ext fname = SOME "urp") rootPath + in + { urpPath = case foundUrps of + [] => raise Fail ("No .urp files found in path " ^ rootPath) + | one :: [] => one + | many => raise Fail ("Found multiple .urp files in path " ^ rootPath) + , fileStates = SM.empty + } + end + +fun addSgnToEnv (env: ElabEnv.env) (sgn: Source.sgn_item list) (fileName: string) (addUnprefixed: bool): ElabEnv.env = + let + val moduleName = C.moduleOf fileName + val (sgn, gs) = Elaborate.elabSgn (env, Disjoint.empty) (Source.SgnConst sgn, { file = fileName + , first = ErrorMsg.dummyPos + , last = ErrorMsg.dummyPos }) + val () = case gs of + [] => () + | _ => (app (fn (_, env, _, c1, c2) => + Print.prefaces "Unresolved" + [("c1", ElabPrint.p_con env c1), + ("c2", ElabPrint.p_con env c2)]) gs; + raise Fail ("Unresolved disjointness constraints in " ^ moduleName ^ " at " ^ fileName)) (* TODO Not sure if this is needed for all signatures or only for Basis *) + val (env', n) = ElabEnv.pushStrNamed env moduleName sgn + val (_, env') = if addUnprefixed + then Elaborate.dopen env' {str = n, strs = [], sgn = sgn} + else ([], env) + in + env' + end + fun calculateFileState (state: state) (fileName: string): fileState = - { envOfPreviousModules = ElabEnv.empty - , decls = [] - } + let + (* TODO Optim: cache parsed urp file? *) + val () = if (OS.Path.ext fileName = SOME "ur") + then () + else raise Fail ("Can only handle .ur files for now") + val () = Elaborate.unifyMore := true + val job = valOf (C.run (C.transform C.parseUrp "parseUrp") (#urpPath state)) + fun entryInUrpToFileName (entry: string) (ext: string) = (#urpPath state) ^ "/" ^ entry ^ ext + val modulesBeforeAndAfterThisFile = + List.partition (fn entry => entryInUrpToFileName entry ".ur" = fileName) (#sources job) + val () = case #2 modulesBeforeAndAfterThisFile of + [] => + (* Module we're handling should always be in here *) + raise Fail ("Couldn't find file " ^ fileName ^ " referenced in .urp file at " ^ (#urpPath state)) + | _ => () + val parsedUrss = List.map (fn entry => + let + val fileName = entryInUrpToFileName entry ".urs" + in + { fileName = fileName + , parsed = + if OS.FileSys.access (fileName, []) + then raise (Fail ("Couldn't find an .urs file for " ^ fileName)) + else valOf (C.run (C.transform C.parseUrs "parseUrs") fileName)} + end) + (#1 modulesBeforeAndAfterThisFile) + val parsedBasisUrs = valOf (C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "basis.urs")) + val parsedTopUrs = valOf (C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "top.urs")) + 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 (parsedUr: Source.decl list) = + valOf (C.run (C.transform C.parseUr "parseUr") fileName) + val (parsedUrs: (Source.sgn_item list) option) = + if OS.FileSys.access (fileName ^ "s", []) then + SOME (valOf (C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s"))) + else + NONE + val (str, sgn', gs) = + Elaborate.elabStr + (envBeforeThisFile, Disjoint.empty) + (Source.StrConst parsedUr, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) + + (* TODO definitily not sure about this one, just copied from "top" processing *) + val () = case gs of + [] => () + | _ => app (fn Elaborate.Disjoint (loc, env, denv, c1, c2) => + (case Disjoint.prove env denv (c1, c2, loc) of + [] => () + | _ => + (Print.prefaces "Unresolved constraint in top.ur" + [("loc", Print.PD.string (ErrorMsg.spanToString loc)), + ("c1", ElabPrint.p_con env c1), + ("c2", ElabPrint.p_con env c2)]; + raise Fail "Unresolved constraint in top.ur")) + | Elaborate.TypeClass (env, c, r, loc) => + () + (* let *) + (* val c = normClassKey env c *) + (* in *) + (* case resolveClass env c of *) + (* SOME e => r := SOME e *) + (* | NONE => expError env (Unresolvable (loc, c)) *) + (* end *) + ) gs + val (sgn, gs) = Elaborate.elabSgn + (envBeforeThisFile, Disjoint.empty) + ( Source.SgnConst (case parsedUrs of NONE => [] | SOME a => a) + , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) + val () = case gs of [] => () | _ => raise Fail ("Unresolved disjointness constraints in " ^ fileName) (* TODO not sure? *) + val () = Elaborate.subSgn envBeforeThisFile ErrorMsg.dummySpan sgn' sgn + in + { envOfPreviousModules = envBeforeThisFile + , decls = case str of + (Elab.StrConst decls, _) => decls + | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration") + } + end fun serverLoop () = let @@ -383,9 +506,9 @@ fun serverLoop () = , textDocument_didOpen = fn didOpenParams => let val path = #path (#uri (#textDocument didOpenParams)) - val fileState = calculateFileState state (path) + val fileState = calculateFileState state path in - stateRef := SOME { rootUri = #rootUri state + stateRef := SOME { urpPath = #urpPath state , fileStates = SM.insert ( #fileStates state , path , fileState) @@ -395,9 +518,9 @@ fun serverLoop () = , textDocument_didSave = fn didSaveParams => let val path = #path (#uri (#textDocument didSaveParams)) - val fileState = calculateFileState state (path) + val fileState = calculateFileState state path in - stateRef := SOME { rootUri = #rootUri state + stateRef := SOME { urpPath = #urpPath state , fileStates = SM.insert ( #fileStates state , path , fileState) -- 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.sig') 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