From 3ecb763c4c9df83bbce2f7f04cfe8cf664a50d39 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 21:47:42 +0200 Subject: [PATCH] [fleche] Store document environment in [Doc.t] This is convenient as we may need to re-create the initial document state when the environment has changed. This patch doesn't fully take advantage of the document env, but it is a prerequisite for the cleanup in #604, in particular to allow a document to recover on `bump` if the init state failed. --- compiler/compile.ml | 3 ++- controller/lsp_core.ml | 5 ++-- fleche/doc.ml | 59 ++++++++++++++++++++++++++++-------------- fleche/doc.mli | 36 +++++++++++++++++++------- fleche/theory.ml | 15 ++++++----- fleche/theory.mli | 3 +-- 6 files changed, 81 insertions(+), 40 deletions(-) diff --git a/compiler/compile.ml b/compiler/compile.ml index 2623d56e..fcb6d423 100644 --- a/compiler/compile.ml +++ b/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) -> diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index e0e34951..f8e8f80f 100644 --- a/controller/lsp_core.ml +++ b/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 diff --git a/fleche/doc.ml b/fleche/doc.ml index 54bcad2c..2c994f5d 100644 --- a/fleche/doc.ml +++ b/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 = diff --git a/fleche/doc.mli b/fleche/doc.mli index 88711422..1eef329e 100644 --- a/fleche/doc.mli +++ b/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 diff --git a/fleche/theory.ml b/fleche/theory.ml index 6a267c30..23a2acf5 100644 --- a/fleche/theory.ml +++ b/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 diff --git a/fleche/theory.mli b/fleche/theory.mli index abaa5857..ff8b60e9 100644 --- a/fleche/theory.mli +++ b/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