[fleche] Store document environment in [Doc.t]

compiler/compile.ml

@@ -30,8 +30,9 @@ let compile_file ~cc file =
   | Error _ -> ()
   | Ok uri -> (
     let workspace = workspace_of_uri ~io ~workspaces ~uri in
+    let env = Doc.Env.make ~init:root_state ~workspace in
     let raw = Util.input_all file in
-    let () = Theory.create ~io ~root_state ~workspace ~uri ~raw ~version:1 in
+    let () = Theory.create ~io ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io with
     | None -> ()
     | Some (_, doc) ->

controller/lsp_core.ml

@@ -251,8 +251,9 @@ let do_open ~io ~(state : State.t) params =
     |> Lsp.Doc.TextDocumentItem.of_yojson |> Result.get_ok
   in
   let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in
-  let root_state, workspace = State.workspace_of_uri ~uri ~state in
-  Fleche.Theory.create ~io ~root_state ~workspace ~uri ~raw:text ~version
+  let init, workspace = State.workspace_of_uri ~uri ~state in
+  let env = Fleche.Doc.Env.make ~init ~workspace in
+  Fleche.Theory.create ~io ~env ~uri ~raw:text ~version
 
 let do_change ~ofn ~io params =
   let uri, version = Helpers.get_uri_version params in

fleche/doc.ml

@@ -201,18 +201,35 @@ module Completion = struct
     | _ -> false
 end
 
-(* Private. A doc is a list of nodes for now. The first element in the list is
-   assumed to be the tip of the document. The initial document is the empty
-   list. *)
+(** Enviroment external to the document, this includes for now the [init] Coq
+    state and the [workspace], which are used to build the first state of the
+    document, usually by importing the prelude and other libs implicitly. *)
+module Env = struct
+  type t =
+    { init : Coq.State.t
+    ; workspace : Coq.Workspace.t
+    }
+
+  let make ~init ~workspace = { init; workspace }
+end
+
+(** A Flèche document is basically a [node list], which is a crude form of a
+    meta-data map [Range.t -> data], where for now [data] is the contents of
+    [Node.t]. *)
 type t =
-  { uri : Lang.LUri.File.t
-  ; version : int
-  ; contents : Contents.t
-  ; toc : Lang.Range.t CString.Map.t
-  ; root : Coq.State.t
-  ; nodes : Node.t list
-  ; diags_dirty : bool  (** Used to optimize `eager_diagnostics` *)
+  { uri : Lang.LUri.File.t  (** [uri] of the document *)
+  ; version : int  (** [version] of the document *)
+  ; contents : Contents.t  (** [contents] of the document *)
+  ; nodes : Node.t list  (** List of document nodes *)
   ; completed : Completion.t
+        (** Status of the document, usually either completed, suspended, or
+            waiting for some IO / external event *)
+  ; toc : Lang.Range.t CString.Map.t  (** table of contents *)
+  ; env : Env.t  (** External document enviroment *)
+  ; root : Coq.State.t
+        (** [root] contains the first state document state, obtained by applying
+            a workspace to Coq's initial state *)
+  ; diags_dirty : bool  (** internal field *)
   }
 
 (* Flatten the list of document asts *)
@@ -257,11 +274,11 @@ let process_init_feedback ~stats range state messages =
   else []
 
 (* Memoized call to [Coq.Init.doc_init] *)
-let mk_doc root_state workspace uri = Memo.Init.eval (root_state, workspace, uri)
+let mk_doc ~env ~uri = Memo.Init.eval (env.Env.init, env.workspace, uri)
 
-let create ~state ~workspace ~uri ~version ~contents =
+let create ~env ~uri ~version ~contents =
   let () = Stats.reset () in
-  let { Coq.Protect.E.r; feedback } = mk_doc state workspace uri in
+  let { Coq.Protect.E.r; feedback } = mk_doc ~env ~uri in
   Coq.Protect.R.map r ~f:(fun root ->
       let init_loc = init_loc ~uri in
       let lines = contents.Contents.lines in
@@ -277,18 +294,19 @@ let create ~state ~workspace ~uri ~version ~contents =
       ; contents
       ; toc
       ; version
-      ; root
       ; nodes
-      ; diags_dirty
       ; completed = Stopped init_range
+      ; root
+      ; env
+      ; diags_dirty
       })
 
-let create ~state ~workspace ~uri ~version ~raw =
+let create ~env ~uri ~version ~raw =
   match Contents.make ~uri ~raw with
   | Error e -> Coq.Protect.R.error (Pp.str e)
-  | Ok contents -> create ~state ~workspace ~uri ~version ~contents
+  | Ok contents -> create ~env ~uri ~version ~contents
 
-let create_failed_permanent ~state ~uri ~version ~raw =
+let create_failed_permanent ~env ~uri ~version ~raw =
   Contents.make ~uri ~raw
   |> Contents.R.map ~f:(fun contents ->
          let lines = contents.Contents.lines in
@@ -298,10 +316,11 @@ let create_failed_permanent ~state ~uri ~version ~raw =
          ; contents
          ; toc = CString.Map.empty
          ; version
-         ; root = state
+         ; root = env.Env.init
          ; nodes = []
          ; diags_dirty = true
          ; completed = FailedPermanent range
+         ; env
          })
 
 let recover_up_to_offset ~init_range doc offset =
@@ -342,6 +361,7 @@ let bump_version ~init_range ~version ~contents doc =
   (* Important: uri, root remain the same *)
   let uri = doc.uri in
   let root = doc.root in
+  let env = doc.env in
   { uri
   ; version
   ; root
@@ -350,6 +370,7 @@ let bump_version ~init_range ~version ~contents doc =
   ; toc
   ; diags_dirty = true (* EJGA: Is it worth to optimize this? *)
   ; completed
+  ; env
   }
 
 let bump_version ~version ~(contents : Contents.t) doc =

fleche/doc.mli

@@ -58,18 +58,35 @@ module Completion : sig
   val is_completed : t -> bool
 end
 
+(** Enviroment external to the document, this includes for now the [init] Coq
+    state and the [workspace], which are used to build the first state of the
+    document, usually by importing the prelude and other libs implicitly. *)
+module Env : sig
+  type t = private
+    { init : Coq.State.t
+    ; workspace : Coq.Workspace.t
+    }
+
+  val make : init:Coq.State.t -> workspace:Coq.Workspace.t -> t
+end
+
 (** A Flèche document is basically a [node list], which is a crude form of a
     meta-data map [Range.t -> data], where for now [data] is the contents of
     [Node.t]. *)
 type t = private
-  { uri : Lang.LUri.File.t
-  ; version : int
-  ; contents : Contents.t
-  ; toc : Lang.Range.t CString.Map.t
-  ; root : Coq.State.t
-  ; nodes : Node.t list
-  ; diags_dirty : bool
+  { uri : Lang.LUri.File.t  (** [uri] of the document *)
+  ; version : int  (** [version] of the document *)
+  ; contents : Contents.t  (** [contents] of the document *)
+  ; nodes : Node.t list  (** List of document nodes *)
   ; completed : Completion.t
+        (** Status of the document, usually either completed, suspended, or
+            waiting for some IO / external event *)
+  ; toc : Lang.Range.t CString.Map.t  (** table of contents *)
+  ; env : Env.t  (** External document enviroment *)
+  ; root : Coq.State.t
+        (** [root] contains the first state document state, obtained by applying
+            a workspace to Coq's initial state *)
+  ; diags_dirty : bool  (** internal field *)
   }
 
 (** Return the list of all asts in the doc *)
@@ -80,8 +97,7 @@ val diags : t -> Lang.Diagnostic.t list
 
 (** Create a new Coq document, this is cached! *)
 val create :
-     state:Coq.State.t
-  -> workspace:Coq.Workspace.t
+     env:Env.t
   -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string
@@ -113,7 +129,7 @@ val save : doc:t -> (unit, Loc.t) Coq.Protect.E.t
 
 (** This is internal, to workaround the Coq multiple-docs problem *)
 val create_failed_permanent :
-     state:Coq.State.t
+     env:Env.t
   -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string

fleche/theory.ml

@@ -232,10 +232,9 @@ let send_error_permanent_fail ~io ~uri ~version message =
   let d = Lang.Diagnostic.{ range; severity = 1; message; extra = None } in
   Io.Report.diagnostics ~io ~uri ~version [ d ]
 
-let create ~io ~root_state ~workspace ~uri ~raw ~version =
-  let r = Doc.create ~state:root_state ~workspace ~uri ~raw ~version in
+let handle_create ~io ~uri ~version r =
   match r with
-  | Completed (Result.Ok doc) ->
+  | Coq.Protect.R.Completed (Result.Ok doc) ->
     Handle.create ~uri ~doc;
     Check.schedule ~uri
   | Completed (Result.Error (Anomaly (_, msg)))
@@ -250,6 +249,10 @@ let create ~io ~root_state ~workspace ~uri ~raw ~version =
     send_error_permanent_fail ~io ~uri ~version (Pp.str message)
   | Interrupted -> ()
 
+let create ~io ~env ~uri ~raw ~version =
+  let r = Doc.create ~env ~uri ~raw ~version in
+  handle_create ~io ~uri ~version r
+
 (* Set this to false for < 8.17, we could parse the version but not worth it. *)
 let sane_coq_base_version = true
 
@@ -265,7 +268,7 @@ let sane_coq_version =
 (* Can't wait for the day this goes away *)
 let tainted = ref false
 
-let create ~io ~root_state ~workspace ~uri ~raw ~version =
+let create ~io ~env ~uri ~raw ~version =
   if !tainted && not sane_coq_version then (
     (* Error due to Coq bug *)
     let message =
@@ -276,13 +279,13 @@ let create ~io ~root_state ~workspace ~uri ~raw ~version =
        instructions on how to install a fixed branch for earlier Coq versions."
     in
     Io.Report.message ~io ~lvl:1 ~message;
-    (match Doc.create_failed_permanent ~state:root_state ~uri ~raw ~version with
+    (match Doc.create_failed_permanent ~env ~uri ~raw ~version with
     | Contents.R.Error _e -> ()
     | Ok doc -> Handle.create ~uri ~doc);
     send_error_permanent_fail ~io ~uri ~version (Pp.str message))
   else (
     tainted := true;
-    create ~io ~root_state ~workspace ~uri ~raw ~version)
+    create ~io ~env ~uri ~raw ~version)
 
 let change ~io ~(doc : Doc.t) ~version ~raw =
   let uri = doc.uri in

fleche/theory.mli

@@ -25,8 +25,7 @@ end
 (** Create a document inside a theory *)
 val create :
      io:Io.CallBack.t
-  -> root_state:Coq.State.t
-  -> workspace:Coq.Workspace.t
+  -> env:Doc.Env.t
   -> uri:Lang.LUri.File.t
   -> raw:string
   -> version:int