Use elabFile completely instead of rebuilding it partially

4 files changed, 42 insertions, 42 deletions

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