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') 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