diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 94009f619..d6e4a9190 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -1,17 +1,7 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* v.Fleche.Doc.ast) doc.Fleche.Doc.nodes in - let slist = Coq.Ast.grab_definitions f ast in + let slist = Fleche.Lang.Ast.grab_definitions f ast in let msg = LSP.mk_reply ~id ~result:(`List slist) in LIO.send_json ofmt msg @@ -192,9 +184,11 @@ let do_hover ofmt ~id params = let do_completion ofmt ~id params = let uri, _ = get_docTextPosition params in let doc = Hashtbl.find doc_table uri in - let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in + let f _loc id = + `Assoc [ ("label", `String Fleche.Lang.Ast.Id.(to_string id)) ] + in let ast = List.map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes in - let clist = Coq.Ast.grab_definitions f ast in + let clist = Fleche.Lang.Ast.grab_definitions f ast in let result = `List clist in let msg = LSP.mk_reply ~id ~result in LIO.send_json ofmt msg @@ -319,25 +313,9 @@ let lsp_main log_file std vo_load_path ml_include_path = let debug_oc = open_out log_file in LIO.debug_fmt := F.formatter_of_out_channel debug_oc; - (* Dedukti stuff *) - let lvl_to_severity (lvl : Feedback.level) = - match lvl with - | Feedback.Debug -> 5 - | Feedback.Info -> 4 - | Feedback.Notice -> 3 - | Feedback.Warning -> 2 - | Feedback.Error -> 1 - in - - let fb_handler, fb_queue = - let q = ref [] in - ( (fun Feedback.{ contents; _ } -> - match contents with - | Message (lvl, loc, msg) -> - let lvl = lvl_to_severity lvl in - q := (loc, lvl, msg) :: !q - | _ -> ()) - , q ) + let msg_handler, msg_queue = + let q : Fleche.Lang.Message.t list ref = ref [] in + ((fun (loc, lvl, msg) -> q := (loc, lvl, msg) :: !q), q) in Fleche.Io.CallBack.set (lsp_cb oc); @@ -347,10 +325,10 @@ let lsp_main log_file std vo_load_path ml_include_path = let debug = Fleche.Debug.backtraces in let state = - ( Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin }) + ( Fleche.Lang.Init.(init { msg_handler; debug; load_module; load_plugin }) , vo_load_path , ml_include_path - , fb_queue ) + , msg_queue ) in memo_read_from_disk (); diff --git a/coq/ast.ml b/coq/ast.ml index f1384a76a..f1bc18742 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -4,8 +4,6 @@ type t = Vernacexpr.vernac_control let hash x = Serlib.Ser_vernacexpr.hash_vernac_control x let compare x y = Serlib.Ser_vernacexpr.compare_vernac_control x y -let to_coq x = x -let of_coq x = x let loc { CAst.loc; _ } = loc (* Printer is very fiddly w.r.t. state, especially when used for debug, so we @@ -75,3 +73,38 @@ let grab_definitions f nodes = let marshal_in ic : t = Marshal.from_channel ic let marshal_out oc v = Marshal.to_channel oc v [] + +module Internal = struct + let to_coq x = x + let of_coq x = x +end + +(* Structure inference *) +module View = struct + type ast = t + + type t = + (* This could be also extracted from the interpretation *) + | Open of unit + | End of unit + | Require of + { prefix : Libnames.qualid option + ; refs : Libnames.qualid list + } + | Other + + let kind ast = + match ast.CAst.v.Vernacexpr.expr with + | Vernacexpr.VernacStartTheoremProof _ -> Open () + | Vernacexpr.VernacEndProof _ -> End () + | Vernacexpr.VernacRequire (prefix, _export, module_refs) -> + let refs = List.map fst module_refs in + Require { prefix; refs } + | _ -> Other +end + +module Id = Names.Id + +module QualId = struct + type t = Libnames.qualid +end diff --git a/coq/ast.mli b/coq/ast.mli index c4bdca512..3fba0745c 100644 --- a/coq/ast.mli +++ b/coq/ast.mli @@ -1,11 +1,46 @@ type t -val loc : t -> Loc.t option +(* Single identifier *) +module Id : sig + type t + + val to_string : t -> string +end + +(* Qualified Identifier *) +module QualId : sig + type t +end + +(* Comparison / hash functions *) val hash : t -> int val compare : t -> t -> int -val to_coq : t -> Vernacexpr.vernac_control -val of_coq : Vernacexpr.vernac_control -> t +val loc : t -> Loc.t option val print : t -> Pp.t -val grab_definitions : (Loc.t -> Names.Id.t -> 'a) -> t list -> 'a list +val grab_definitions : (Loc.t -> Id.t -> 'a) -> t list -> 'a list val marshal_in : in_channel -> t val marshal_out : out_channel -> t -> unit + +(* Analysis on AST / Structure inference *) +module View : sig + type ast = t + + type t = + (* This could be also extracted from the interpretation *) + | Open of unit + | End of unit + | Require of + { prefix : QualId.t option + ; refs : QualId.t list + } + | Other + + val kind : ast -> t +end + +(* This can't be used outside of the [Coq] library, and will be gone once we + functiorialize the interface *) +module Internal : sig + val to_coq : t -> Vernacexpr.vernac_control + val of_coq : Vernacexpr.vernac_control -> t +end diff --git a/coq/init.ml b/coq/init.ml index 6fa4119f4..85c3f246b 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -18,16 +18,15 @@ (* Low-level, internal Coq initialization *) (**************************************************************************) -type coq_opts = - { fb_handler : Feedback.feedback -> unit - (** callback to handle async feedback *) +type opts = + { msg_handler : Message.t -> unit (** callback to handle async feedback *) ; load_module : string -> unit (** callback to load cma/cmo files *) ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) } -let coq_init opts = +let init opts = (* Core Coq initialization *) Lib.init (); Global.set_impredicative_set false; @@ -41,7 +40,22 @@ let coq_init opts = (**************************************************************************) (* Initialize logging. *) - ignore (Feedback.add_feeder opts.fb_handler); + let lvl_to_severity (lvl : Feedback.level) = + match lvl with + | Feedback.Debug -> 5 + | Feedback.Info -> 4 + | Feedback.Notice -> 3 + | Feedback.Warning -> 2 + | Feedback.Error -> 1 + in + + let fb_handler = function + | Feedback.{ contents = Message (lvl, loc, msg); _ } -> + let lvl = lvl_to_severity lvl in + opts.msg_handler (loc, lvl, msg) + | _ -> () + in + ignore (Feedback.add_feeder fb_handler); (* SerAPI plugins *) let load_plugin = opts.load_plugin in @@ -61,7 +75,7 @@ let coq_init opts = (**************************************************************************) (* Add root state!! *) (**************************************************************************) - Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq + Vernacstate.freeze_interp_state ~marshallable:false |> State.Internal.of_coq (* End of initialization *) @@ -90,33 +104,44 @@ let loadpath_from_coqproject () : Loadpath.vo_path list = (List.map (fun f -> to_vo_loadpath f.thing true) r_includes) (* Inits the context for a document *) -let doc_init ~root_state ~vo_load_path ~ml_include_path ~libname ~require_libs = - (* Lsp.Io.log_error "init" "starting"; *) - Vernacstate.unfreeze_interp_state (State.to_coq root_state); - - (* This should go away in Coq itself *) - Safe_typing.allow_delayed_constants := true; - let load_objs libs = - let rq_file (dir, from, exp) = - let mp = Libnames.qualid_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently - (Vernacentries.vernac_require mfrom exp) - [ (mp, Vernacexpr.ImportAll) ] +module Doc = struct + type require_decl = + string * string option * Vernacexpr.export_with_cats option + + type env = + { vo_load_path : Loadpath.vo_path list + ; ml_load_path : string list + ; requires : require_decl list + } + + let make ~root_state ~env ~name = + (* Lsp.Io.log_error "init" "starting"; *) + Vernacstate.unfreeze_interp_state (State.Internal.to_coq root_state); + + (* This should go away in Coq itself *) + Safe_typing.allow_delayed_constants := true; + let load_objs libs = + let rq_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently + (Vernacentries.vernac_require mfrom exp) + [ (mp, Vernacexpr.ImportAll) ] + in + List.(iter rq_file (rev libs)) in - List.(iter rq_file (rev libs)) - in - (* Set load path; important, this has to happen before we declare the library - below as [Declaremods/Library] will infer the module name by looking at the - load path! *) - List.iter Mltop.add_ml_dir ml_include_path; - List.iter Loadpath.add_vo_path vo_load_path; - List.iter Loadpath.add_vo_path (loadpath_from_coqproject ()); - Declaremods.start_library libname; + (* Set load path; important, this has to happen before we declare the + library below as [Declaremods/Library] will infer the module name by + looking at the load path! *) + List.iter Mltop.add_ml_dir env.ml_load_path; + List.iter Loadpath.add_vo_path env.vo_load_path; + List.iter Loadpath.add_vo_path (loadpath_from_coqproject ()); + Declaremods.start_library name; - (* Import initial libraries. *) - load_objs require_libs; + (* Import initial libraries. *) + load_objs env.requires; - (* We return the state at this point! *) - Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq + (* We return the state at this point! *) + Vernacstate.freeze_interp_state ~marshallable:false |> State.Internal.of_coq +end diff --git a/coq/init.mli b/coq/init.mli index 310452415..77a674278 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -18,22 +18,25 @@ (* Low-level, internal Coq initialization *) (**************************************************************************) -type coq_opts = - { fb_handler : Feedback.feedback -> unit - (** callback to handle async feedback *) +type opts = + { msg_handler : Message.t -> unit (** callback to handle async feedback *) ; load_module : string -> unit (** callback to load cma/cmo files *) ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) } -val coq_init : coq_opts -> State.t +val init : opts -> State.t -val doc_init : - root_state:State.t - -> vo_load_path:Loadpath.vo_path list - -> ml_include_path:string list - -> libname:Names.DirPath.t - -> require_libs: - (string * string option * Vernacexpr.export_with_cats option) list - -> State.t +module Doc : sig + type require_decl = + string * string option * Vernacexpr.export_with_cats option + + type env = + { vo_load_path : Loadpath.vo_path list + ; ml_load_path : string list + ; requires : require_decl list + } + + val make : root_state:State.t -> env:env -> name:Names.DirPath.t -> State.t +end diff --git a/coq/internal.ml b/coq/internal.ml new file mode 100644 index 000000000..cb58c40f1 --- /dev/null +++ b/coq/internal.ml @@ -0,0 +1,23 @@ +module type Conv = sig + type t + + module Internal : sig + type coq + + val of_coq : coq -> t + val to_coq : t -> coq + end +end + +module Make (S : sig + type coq +end) : Conv with type Internal.coq = S.coq = struct + module Internal = struct + type coq = S.coq + + let of_coq x = x + let to_coq x = x + end + + type t = S.coq +end diff --git a/coq/interp.ml b/coq/interp.ml index 784bbb1ae..7790109f7 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -30,9 +30,9 @@ let get_feedback fb_queue = type 'a interp_result = 'a Info.t Protect.R.t let coq_interp ~st cmd = - let st = State.to_coq st in - let cmd = Ast.to_coq cmd in - Vernacinterp.interp ~st cmd |> State.of_coq + let st = State.Internal.to_coq st in + let cmd = Ast.Internal.to_coq cmd in + Vernacinterp.interp ~st cmd |> State.Internal.of_coq let interp ~st ~fb_queue cmd = Protect.eval cmd ~f:(fun cmd -> diff --git a/coq/parse.ml b/coq/parse.ml new file mode 100644 index 000000000..a206a9d25 --- /dev/null +++ b/coq/parse.ml @@ -0,0 +1,42 @@ +module State = Internal.Make (struct + type coq = Vernacstate.Parser.t +end) + +module Proof_mode = Internal.Make (struct + type coq = Pvernac.proof_mode +end) + +module Parsable = struct + type t = Pcoq.Parsable.t + + let make = Pcoq.Parsable.make +end + +let parse st mode ps = + let st = State.Internal.to_coq st in + let mode = Option.map Proof_mode.Internal.to_coq mode in + Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps + |> Option.map Ast.Internal.of_coq + +(* Error recovery heuristic *) + +(* Read the input stream until a dot or a "end of proof" token is encountered *) +let parse_to_terminator : unit Pcoq.Entry.t = + (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *) + let rec dot st = + match Gramlib.LStream.next st with + | Tok.KEYWORD ("." | "..." | "Qed" | "Defined" | "Admitted") | Tok.BULLET _ + -> () + | Tok.EOI -> () + | _ -> dot st + in + Pcoq.Entry.of_parser "Coqtoplevel.dot" { parser_fun = dot } + +(* If an error occurred while parsing, we try to read the input until a dot + token is encountered. We assume that when a lexer error occurs, at least one + char was eaten *) + +let rec discard_to_dot ps = + try Pcoq.Entry.parse parse_to_terminator ps with + | CLexer.Error.E _ -> discard_to_dot ps + | e when CErrors.noncritical e -> () diff --git a/coq/parse.mli b/coq/parse.mli new file mode 100644 index 000000000..bb32267ff --- /dev/null +++ b/coq/parse.mli @@ -0,0 +1,15 @@ +module State : Internal.Conv with type Internal.coq = Vernacstate.Parser.t + +module Parsable : sig + type t + + val make : ?loc:Loc.t -> char Gramlib.Stream.t -> t +end + +module Proof_mode : Internal.Conv with type Internal.coq = Pvernac.proof_mode + +(** The main entry: reads an vernac command or a tactic (depending on the proof + mode) *) +val parse : State.t -> Proof_mode.t option -> Parsable.t -> Ast.t option + +val discard_to_dot : Parsable.t -> unit diff --git a/coq/protect.ml b/coq/protect.ml index cd3b2b619..814b023b4 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -1,3 +1,5 @@ +type error = Loc.t option * Pp.t + module R = struct type 'a t = | Completed of ('a, Loc.t option * Pp.t) result diff --git a/coq/protect.mli b/coq/protect.mli index 4b9b8ee74..9b07860a2 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -1,6 +1,8 @@ +type error = Loc.t option * Pp.t + module R : sig type 'a t = - | Completed of ('a, Loc.t option * Pp.t) result + | Completed of ('a, error) result | Interrupted (* signal sent, eval didn't complete *) end diff --git a/coq/state.ml b/coq/state.ml index a25703c2f..251c33637 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -1,5 +1,11 @@ type t = Vernacstate.t +module Proof = struct + type proof = Vernacstate.LemmaStack.t + + let get ~st = st.Vernacstate.lemmas +end + let any_out oc (a : Summary.Frozen.any) = (* let (Summary.Frozen.Any (tag, _value)) = a in *) (* let name = Summary.Dyn.repr tag in *) @@ -52,19 +58,25 @@ let _marshal_in ic = let shallow = Marshal.from_channel ic in { Vernacstate.parsing; system; lemmas; program; opaques; shallow } -let marshal_in ic : t = Marshal.from_channel ic -let marshal_out oc st = Marshal.to_channel oc st [] -let of_coq x = x -let to_coq x = x +module Marshal = struct + let read ic : t = Marshal.from_channel ic + let write oc st = Marshal.to_channel oc st [] +end + +module Internal = struct + let of_coq x = x + let to_coq x = x +end + let compare x y = compare x y let mode ~st = Option.map (fun _ -> Vernacinterp.get_default_proof_mode ()) st.Vernacstate.lemmas + |> Option.map Parse.Proof_mode.Internal.of_coq -let parsing ~st = st.Vernacstate.parsing -let lemmas ~st = st.Vernacstate.lemmas +let parsing ~st = st.Vernacstate.parsing |> Parse.State.Internal.of_coq let drop_proofs ~st = let open Vernacstate in diff --git a/coq/state.mli b/coq/state.mli index 47f125247..95ef2985c 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -1,14 +1,25 @@ type t -val marshal_in : in_channel -> t -val marshal_out : out_channel -> t -> unit -val of_coq : Vernacstate.t -> t -val to_coq : t -> Vernacstate.t val compare : t -> t -> int -val mode : st:t -> Pvernac.proof_mode option -val parsing : st:t -> Vernacstate.Parser.t -val lemmas : st:t -> Vernacstate.LemmaStack.t option +val mode : st:t -> Parse.Proof_mode.t option +val parsing : st:t -> Parse.State.t val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b +module Proof : sig + type proof = Vernacstate.LemmaStack.t + + val get : st:t -> proof option +end + (* Error recovery *) val drop_proofs : st:t -> t + +module Marshal : sig + val read : in_channel -> t + val write : out_channel -> t -> unit +end + +module Internal : sig + val of_coq : Vernacstate.t -> t + val to_coq : t -> Vernacstate.t +end diff --git a/fleche/doc.ml b/fleche/doc.ml index c784c790e..e86714357 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -1,11 +1,9 @@ (************************************************************************) -(* Coq Language Server Protocol *) -(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) -(* Copyright 2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Flèche Document Manager *) +(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -(* Status: Experimental *) -(************************************************************************) (* open Lsp_util * module LSP = Lsp.Base *) @@ -13,8 +11,8 @@ (* [node list] is a very crude form of a meta-data map "loc -> data" , where for now [data] is only the goals. *) type node = - { ast : Coq.Ast.t (** Ast of node *) - ; state : Coq.State.t (** (Full) State of node *) + { ast : Lang.Ast.t (** Ast of node *) + ; state : Lang.State.t (** (Full) State of node *) ; memo_info : string } @@ -25,7 +23,7 @@ type t = { uri : string ; version : int ; contents : string - ; root : Coq.State.t + ; root : Lang.State.t ; nodes : node list } @@ -33,11 +31,11 @@ type t = * LSP.mk_diagnostics ~uri:doc.uri ~version:doc.version [pos, 1, msg, None] *) let mk_doc state = - let root_state, vo_load_path, ml_include_path, _ = state in - let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in - let require_libs = [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] in - Coq.Init.doc_init ~root_state ~vo_load_path ~ml_include_path ~libname - ~require_libs + let root_state, vo_load_path, ml_load_path, _ = state in + let requires = [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] in + let env = { Lang.Init.Doc.vo_load_path; ml_load_path; requires } in + let name = Names.(DirPath.make [ Id.of_string "foo" ]) in + Lang.Init.Doc.make ~root_state ~env ~name let create ~state ~uri ~version ~contents = { uri; contents; version; root = mk_doc state; nodes = [] } @@ -46,63 +44,41 @@ let create ~state ~uri ~version ~contents = (* let close_doc _modname = () *) let parse_stm ~st ps = - let mode = Coq.State.mode ~st in - let st = Coq.State.parsing ~st in + let mode = Lang.State.mode ~st in + let st = Lang.State.parsing ~st in let parse ps = (* Coq is missing this, so we add it here. Note that this MUST run inside coq_protect *) Control.check_for_interrupt (); - Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps - |> Option.map Coq.Ast.of_coq - in - Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps - -(* Read the input stream until a dot or a "end of proof" token is encountered *) -let parse_to_terminator : unit Pcoq.Entry.t = - (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *) - let rec dot st = - match Gramlib.LStream.next st with - | Tok.KEYWORD ("." | "..." | "Qed" | "Defined" | "Admitted") | Tok.BULLET _ - -> () - | Tok.EOI -> () - | _ -> dot st + Lang.Parse.(parse st mode) ps in - Pcoq.Entry.of_parser "Coqtoplevel.dot" { parser_fun = dot } - -(* If an error occurred while parsing, we try to read the input until a dot - token is encountered. We assume that when a lexer error occurs, at least one - char was eaten *) - -let rec discard_to_dot ps = - try Pcoq.Entry.parse parse_to_terminator ps with - | CLexer.Error.E _ -> discard_to_dot ps - | e when CErrors.noncritical e -> () + Stats.record ~kind:Stats.Kind.Parsing ~f:(Lang.Protect.eval ~f:parse) ps (* Gross hack *) let proof_st = ref None let register_hack_proof_recover ast st = - match (Coq.Ast.to_coq ast).CAst.v.Vernacexpr.expr with - | Vernacexpr.VernacStartTheoremProof _ -> + match Lang.Ast.View.kind ast with + | Open () -> proof_st := Some st; () | _ -> () (* Simple heuristic for Qed. *) -let state_recovery_heuristic st v = - match (Coq.Ast.to_coq v).CAst.v.Vernacexpr.expr with +let state_recovery_heuristic st ast = + match Lang.Ast.View.kind ast with (* Drop the top proof state if we reach a faulty Qed. *) - | Vernacexpr.VernacEndProof _ -> + | End () -> let st = Option.default st !proof_st in - Io.Log.error "recovery" (Memo.input_info (v, st)); + Io.Log.error "recovery" (Memo.input_info (ast, st)); proof_st := None; - Coq.State.drop_proofs ~st + Lang.State.drop_proofs ~st | _ -> st type process_action = | EOF | Skip - | Process of Coq.Ast.t + | Process of Lang.Ast.t (* Make each fb a diag *) let _pp_located fmt (_loc, pp) = Pp.pp_with fmt pp @@ -113,15 +89,14 @@ let pp_words fmt w = else Format.fprintf fmt "%.2f Mw" (w /. (1024.0 *. 1024.0)) let mk_diag ?(extra = []) range severity message = - let range = Types.to_range range in - let message = Pp.string_of_ppcmds message in + let range = Lang.Loc.to_range range in + let message = Lang.Pp.to_string message in Types.Diagnostic.{ range; severity; message; extra } (* modular error diagnostic generation *) let mk_error_diagnostic ~loc ~msg ~ast = - match (Coq.Ast.to_coq ast).v with - | Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } -> - let refs = List.map fst module_refs in + match Lang.Ast.View.kind ast with + | Require { prefix; refs } -> let extra = [ Types.Diagnostic.Extra.FailedRequire { prefix; refs } ] in mk_diag ~extra loc 1 msg | _ -> mk_diag loc 1 msg @@ -130,6 +105,16 @@ let feed_to_diag ~loc (range, severity, message) = let range = Option.default loc range in mk_diag range severity message +let send_processing_diag ~uri ~version loc diags = + let proc_diag = mk_diag loc 3 (Lang.Pp.str "Processing") in + Io.Report.diagnostics ~uri ~version (proc_diag :: diags) + +let print_parsing_debug_info loc ast = + let line = (Lang.Loc.to_range loc).start.line in + let line = "[l: " ^ string_of_int line ^ "] " in + Io.Log.error "coq" + ("parsed sentence: " ^ line ^ Lang.Pp.to_string (Lang.Ast.print ast)) + let process_feedback ~loc fbs = List.map (feed_to_diag ~loc) fbs let interp_and_info ~parsing_time ~st ~fb_queue ast = @@ -153,24 +138,24 @@ let interp_and_info ~parsing_time ~st ~fb_queue ast = (* XXX: Imperative problem *) let process_and_parse ~uri ~version ~fb_queue doc = - let loc = Loc.initial (InFile { dirpath = None; file = uri }) in + let loc = Lang.Loc.initial ~uri in let doc_handle = - Pcoq.Parsable.make ~loc Gramlib.Stream.(of_string doc.contents) + Lang.Parse.Parsable.make ~loc Gramlib.Stream.(of_string doc.contents) in let rec stm doc st diags = if Debug.parsing then Io.Log.error "coq" "parsing sentence"; (* Parsing *) let action, diags, parsing_time = match parse_stm ~st doc_handle with - | Coq.Protect.R.Interrupted, time -> (EOF, diags, time) - | Coq.Protect.R.Completed res, time -> ( + | Lang.Protect.R.Interrupted, time -> (EOF, diags, time) + | Lang.Protect.R.Completed res, time -> ( match res with | Ok None -> (EOF, diags, time) | Ok (Some ast) -> (Process ast, diags, time) | Error (loc, msg) -> let loc = Option.get loc in let diags = mk_diag loc 1 msg :: diags in - discard_to_dot doc_handle; + Lang.Parse.discard_to_dot doc_handle; (Skip, diags, time)) in (* Execution *) @@ -180,27 +165,22 @@ let process_and_parse ~uri ~version ~fb_queue doc = | Skip -> stm doc st diags (* We interpret the command now *) | Process ast -> ( - let loc = Coq.Ast.loc ast |> Option.get in + let loc = Lang.Ast.loc ast |> Option.get in (* XXX Eager update! *) - (if Config.eager_diagnostics then - let proc_diag = mk_diag loc 3 (Pp.str "Processing") in - Io.Report.diagnostics ~uri ~version (proc_diag :: diags)); - (if Debug.parsing then - let line = "[l: " ^ string_of_int loc.Loc.line_nb ^ "] " in - Io.Log.error "coq" - ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast))); + if Config.eager_diagnostics then + send_processing_diag ~uri ~version loc diags; + if Debug.parsing then print_parsing_debug_info loc ast; register_hack_proof_recover ast st; - (* memory is disabled as it is quite slow and misleading *) let res, memo_info = interp_and_info ~parsing_time ~st ~fb_queue ast in match res with - | Coq.Protect.R.Interrupted -> + | Lang.Protect.R.Interrupted -> (* Exit *) (doc, st, diags) - | Coq.Protect.R.Completed res -> ( + | Lang.Protect.R.Completed res -> ( match res with | Ok { res = state; feedback } -> - (* let goals = Coq.State.goals *) - let ok_diag = mk_diag loc 3 (Pp.str "OK") in + (* let goals = Lang.State.goals *) + let ok_diag = mk_diag loc 3 (Lang.Pp.str "OK") in let diags = if Config.ok_diag then ok_diag :: diags else diags in let fb_diags = process_feedback ~loc feedback in let diags = fb_diags @ diags in diff --git a/fleche/doc.mli b/fleche/doc.mli index 39928a21d..9de6494f5 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -1,26 +1,15 @@ (************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* data" , where for now [data] is only the goals. *) type node = - { ast : Coq.Ast.t (** Ast of node *) - ; state : Coq.State.t (** (Full) State of node *) + { ast : Lang.Ast.t (** Ast of node *) + ; state : Lang.State.t (** (Full) State of node *) ; memo_info : string } @@ -28,12 +17,12 @@ type t = { uri : string ; version : int ; contents : string - ; root : Coq.State.t + ; root : Lang.State.t ; nodes : node list } val create : - state:Coq.State.t * Loadpath.vo_path list * string list * _ + state:Lang.State.t * Loadpath.vo_path list * string list * _ -> uri:string -> version:int -> contents:string @@ -42,5 +31,5 @@ val create : val check : ofmt:Format.formatter -> doc:t - -> fb_queue:Coq.Message.t list ref - -> t * Coq.State.t * Types.Diagnostic.t list + -> fb_queue:Lang.Message.t list ref + -> t * Lang.State.t * Types.Diagnostic.t list diff --git a/fleche/info.ml b/fleche/info.ml index 316640fa6..6b6d7af78 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -1,25 +1,16 @@ (************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* t -> bool - val gt_range : ?loc:Loc.t -> t -> bool + val in_range : ?loc:Lang.Loc.t -> t -> bool + val gt_range : ?loc:Lang.Loc.t -> t -> bool type offset_table = string @@ -53,7 +44,7 @@ module LineCol : Point with type t = int * int = struct match loc with | None -> false | Some loc -> - let r = Types.to_range loc in + let r = Lang.Loc.to_range loc in let line1 = r.start.line in let col1 = r.start.character in let line2 = r._end.line in @@ -71,7 +62,7 @@ module LineCol : Point with type t = int * int = struct match loc with | None -> false | Some loc -> - let r = Types.to_range loc in + let r = Lang.Loc.to_range loc in let line1 = r.start.line in let col1 = r.start.character in let line2 = r._end.line in @@ -90,12 +81,16 @@ module Offset : Point with type t = int = struct let in_range ?loc point = match loc with | None -> false - | Some loc -> loc.Loc.bp <= point && point < loc.ep + | Some loc -> + let loc = Lang.Loc.to_range loc in + loc.start.offset <= point && point < loc._end.offset let gt_range ?loc point = match loc with | None -> false - | Some loc -> point < loc.Loc.bp + | Some loc -> + let loc = Lang.Loc.to_range loc in + point < loc.start.offset let to_offset off _ = off let to_string off = string_of_int off @@ -126,7 +121,7 @@ module Make (P : Point) : S with module P := P = struct match l with | [] -> prev | node :: xs -> ( - let loc = Coq.Ast.loc node.Doc.ast in + let loc = Lang.Ast.loc node.Doc.ast in match approx with | Exact -> if P.in_range ?loc point then Some node else find None xs | PickPrev -> @@ -157,7 +152,7 @@ module Make (P : Point) : S with module P := P = struct let ppx env sigma x = (* Jscoq_util.pp_opt *) Printer.pr_ltype_env env sigma x in - let lemmas = Coq.State.lemmas ~st in + let lemmas = Lang.State.Proof.get ~st in Option.cata (reify_goals ppx) None lemmas let goals ~doc ~point approx = @@ -179,7 +174,7 @@ module Make (P : Point) : S with module P := P = struct let completion ~doc ~point prefix = find ~doc ~point Exact |> obind (fun node -> - Coq.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix -> + Lang.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix -> to_qualid prefix |> obind (fun p -> Nametab.completion_canditates p diff --git a/fleche/info.mli b/fleche/info.mli index 855bf2f30..346669408 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -1,26 +1,17 @@ (************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* t -> bool - val gt_range : ?loc:Loc.t -> t -> bool + val in_range : ?loc:Lang.Loc.t -> t -> bool + val gt_range : ?loc:Lang.Loc.t -> t -> bool (** [to_offset] will help to resolve a position from for example (line,col) to an offset, but in some case requires a lookup method. *) diff --git a/fleche/lang.ml b/fleche/lang.ml new file mode 100644 index 000000000..18b6da270 --- /dev/null +++ b/fleche/lang.ml @@ -0,0 +1,78 @@ +(* XXX: ejgallego, do we start lines at 0? *) +module Point = struct + type t = + { line : int + ; character : int + ; offset : int + } +end + +module Range = struct + type t = + { start : Point.t + ; _end : Point.t + } +end + +module Loc = struct + include Loc + + type offset = int * int * int * int * int * int + + let initial ~uri = Loc.initial (InFile { dirpath = None; file = uri }) + + let offset (l1 : Loc.t) (l2 : Loc.t) = + let line_offset = l2.line_nb - l1.line_nb in + let bol_offset = l2.bol_pos - l1.bol_pos in + let line_last_offset = l2.line_nb_last - l1.line_nb_last in + let bol_last_offset = l2.bol_pos_last - l1.bol_pos_last in + let bp_offset = l2.bp - l1.bp in + let ep_offset = l2.ep - l1.ep in + ( line_offset + , bol_offset + , line_last_offset + , bol_last_offset + , bp_offset + , ep_offset ) + + let apply_offset + ( line_offset + , bol_offset + , line_last_offset + , bol_last_offset + , bp_offset + , ep_offset ) (loc : Loc.t) = + { loc with + line_nb = loc.line_nb + line_offset + ; bol_pos = loc.bol_pos + bol_offset + ; line_nb_last = loc.line_nb_last + line_last_offset + ; bol_pos_last = loc.bol_pos_last + bol_last_offset + ; bp = loc.bp + bp_offset + ; ep = loc.ep + ep_offset + } + + let to_range (p : Loc.t) : Range.t = + let Loc.{ line_nb; line_nb_last; bol_pos; bol_pos_last; bp; ep; _ } = p in + let start_line = line_nb - 1 in + let start_col = bp - bol_pos in + let end_line = line_nb_last - 1 in + let end_col = ep - bol_pos_last in + Range. + { start = { line = start_line; character = start_col; offset = bp } + ; _end = { line = end_line; character = end_col; offset = ep } + } +end + +module Pp = struct + include Pp + + let to_string = string_of_ppcmds +end + +module Message = Coq.Message +module Init = Coq.Init +module Ast = Coq.Ast +module Parse = Coq.Parse +module State = Coq.State +module Protect = Coq.Protect +module Interp = Coq.Interp diff --git a/fleche/lang.mli b/fleche/lang.mli new file mode 100644 index 000000000..b6d154920 --- /dev/null +++ b/fleche/lang.mli @@ -0,0 +1 @@ +include Lang_intf.S diff --git a/fleche/lang_intf.ml b/fleche/lang_intf.ml new file mode 100644 index 000000000..1c8333fd5 --- /dev/null +++ b/fleche/lang_intf.ml @@ -0,0 +1,196 @@ +(************************************************************************) +(* Flèche Document Manager *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +module type S = sig + (* XXX: ejgallego, do we start lines at 0? *) + module Point : sig + type t = + { line : int + ; character : int + ; offset : int + } + end + + module Range : sig + type t = + { start : Point.t + ; _end : Point.t + } + end + + (* Remove in favor of Range directly (however that's a bit annoying due to + thep pervasive occurence of native locs usually; moreover a loc in Coq + includes the file / dirpath *) + module Loc : sig + type t + + (* Difference between two locs *) + type offset + + val initial : uri:string -> t + val offset : t -> t -> offset + val apply_offset : offset -> t -> t + val to_range : t -> Range.t + end + + module Pp : sig + type t + + val to_string : t -> string + val str : string -> t + end + + module Message : sig + type t = Loc.t option * int * Pp.t + end + + module Ast : sig + type t + + (* Single identifier *) + module Id : sig + type t + + val to_string : t -> string + end + + (* Qualified Identifier *) + module QualId : sig + type t + end + + val hash : t -> int + val loc : t -> Loc.t option + val compare : t -> t -> int + val print : t -> Pp.t + val grab_definitions : (Loc.t -> Id.t -> 'a) -> t list -> 'a list + + module View : sig + type ast = t + + type t = + (* This could be also extracted from the interpretation *) + | Open of unit + | End of unit + | Require of + { prefix : QualId.t option + ; refs : QualId.t list + } + | Other + + val kind : ast -> t + end + + val marshal_in : in_channel -> t + val marshal_out : out_channel -> t -> unit + end + + module Parse : sig + module State : sig + type t + end + + module Parsable : sig + type t + + val make : ?loc:Loc.t -> char Gramlib.Stream.t -> t + end + + module Proof_mode : sig + type t + end + + val parse : State.t -> Proof_mode.t option -> Parsable.t -> Ast.t option + val discard_to_dot : Parsable.t -> unit + end + + module State : sig + type t + + val compare : t -> t -> int + val mode : st:t -> Parse.Proof_mode.t option + val parsing : st:t -> Parse.State.t + val drop_proofs : st:t -> t + val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b + + module Proof : sig + type proof = Vernacstate.LemmaStack.t + + val get : st:t -> proof option + end + + module Marshal : sig + val read : in_channel -> t + val write : out_channel -> t -> unit + end + end + + module Protect : sig + type error = Loc.t option * Pp.t + + module R : sig + type 'a t = + | Completed of ('a, error) result + | Interrupted (* signal sent, eval didn't complete *) + end + + val eval : f:('i -> 'o) -> 'i -> 'o R.t + + (** Update the loc stored in the result, this is used by our cache-aware + location *) + val map_loc : f:(Loc.t -> Loc.t) -> 'a R.t -> 'a R.t + end + + module Interp : sig + module Info : sig + type 'a t = + { res : 'a + ; feedback : Message.t list + } + end + + type 'a interp_result = 'a Info.t Protect.R.t + + val interp : + st:State.t + -> fb_queue:Message.t list ref + -> Ast.t + -> State.t interp_result + + val marshal_in : (in_channel -> 'a) -> in_channel -> 'a interp_result + + val marshal_out : + (out_channel -> 'a -> unit) -> out_channel -> 'a interp_result -> unit + end + + module Init : sig + type opts = + { msg_handler : Message.t -> unit + (** callback to handle async messages from the lange engine *) + ; load_module : string -> unit (** callback to load cma/cmo files *) + ; load_plugin : Mltop.PluginSpec.t -> unit + (** callback to load findlib packages *) + ; debug : bool (** Enable Coq Debug mode *) + } + + val init : opts -> State.t + + module Doc : sig + type require_decl = + string * string option * Vernacexpr.export_with_cats option + + type env = + { vo_load_path : Loadpath.vo_path list + ; ml_load_path : string list + ; requires : require_decl list + } + + val make : + root_state:State.t -> env:env -> name:Names.DirPath.t -> State.t + end + end +end diff --git a/fleche/memo.ml b/fleche/memo.ml index 5327c5448..4a6f98390 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -1,3 +1,10 @@ +(************************************************************************) +(* Flèche Document Manager *) +(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + module CS = Stats module Stats = struct @@ -17,23 +24,23 @@ end (* This requires a ppx likely as to ignore the CAst location *) module VernacInput = struct - type t = Coq.Ast.t * Coq.State.t + type t = Lang.Ast.t * Lang.State.t let equal (v1, st1) (v2, st2) = - if Coq.Ast.compare v1 v2 = 0 then - if Coq.State.compare st1 st2 = 0 then true else false + if Lang.Ast.compare v1 v2 = 0 then + if Lang.State.compare st1 st2 = 0 then true else false else false - let hash (v, st) = Hashtbl.hash (Coq.Ast.hash v, st) + let hash (v, st) = Hashtbl.hash (Lang.Ast.hash v, st) let marshal_out oc (v, st) = - Coq.Ast.marshal_out oc v; - Coq.State.marshal_out oc st; + Lang.Ast.marshal_out oc v; + Lang.State.Marshal.write oc st; () let marshal_in ic = - let v = Coq.Ast.marshal_in ic in - let st = Coq.State.marshal_in ic in + let v = Lang.Ast.marshal_in ic in + let st = Lang.State.Marshal.read ic in (v, st) end @@ -60,22 +67,22 @@ module CacheStats = struct end let input_info (v, st) = - Format.asprintf "stm: %d | st %d" (Coq.Ast.hash v) (Hashtbl.hash st) + Format.asprintf "stm: %d | st %d" (Lang.Ast.hash v) (Hashtbl.hash st) module HC = Hashtbl.Make (VernacInput) module Result = struct (* We store the location as to compute an offset for cached results *) - type t = Loc.t * Coq.State.t Coq.Interp.interp_result + type t = Lang.Loc.t * Lang.State.t Lang.Interp.interp_result (* XXX *) let marshal_in ic : t = let loc = Marshal.from_channel ic in - (loc, Coq.Interp.marshal_in Coq.State.marshal_in ic) + (loc, Lang.Interp.marshal_in Lang.State.Marshal.read ic) let marshal_out oc (loc, t) = Marshal.to_channel oc loc []; - Coq.Interp.marshal_out Coq.State.marshal_out oc t + Lang.Interp.marshal_out Lang.State.Marshal.write oc t end type cache = Result.t HC.t @@ -86,44 +93,13 @@ let in_cache st stm = let kind = CS.Kind.Hashing in CS.record ~kind ~f:(HC.find_opt !cache) (stm, st) -(* XXX: Move elsewhere *) -let loc_offset (l1 : Loc.t) (l2 : Loc.t) = - let line_offset = l2.line_nb - l1.line_nb in - let bol_offset = l2.bol_pos - l1.bol_pos in - let line_last_offset = l2.line_nb_last - l1.line_nb_last in - let bol_last_offset = l2.bol_pos_last - l1.bol_pos_last in - let bp_offset = l2.bp - l1.bp in - let ep_offset = l2.ep - l1.ep in - ( line_offset - , bol_offset - , line_last_offset - , bol_last_offset - , bp_offset - , ep_offset ) - -let loc_apply_offset - ( line_offset - , bol_offset - , line_last_offset - , bol_last_offset - , bp_offset - , ep_offset ) (loc : Loc.t) = - { loc with - line_nb = loc.line_nb + line_offset - ; bol_pos = loc.bol_pos + bol_offset - ; line_nb_last = loc.line_nb_last + line_last_offset - ; bol_pos_last = loc.bol_pos_last + bol_last_offset - ; bp = loc.bp + bp_offset - ; ep = loc.ep + ep_offset - } - let adjust_offset ~stm_loc ~cached_loc res = - let offset = loc_offset cached_loc stm_loc in - let f = loc_apply_offset offset in - Coq.Protect.map_loc ~f res + let offset = Lang.Loc.offset cached_loc stm_loc in + let f = Lang.Loc.apply_offset offset in + Lang.Protect.map_loc ~f res let interp_command ~st ~fb_queue stm : _ Stats.t = - let stm_loc = Coq.Ast.loc stm |> Option.get in + let stm_loc = Lang.Ast.loc stm |> Option.get in match in_cache st stm with | Some (cached_loc, res), time -> if Debug.cache then Io.Log.error "coq" "cache hit"; @@ -135,15 +111,15 @@ let interp_command ~st ~fb_queue stm : _ Stats.t = CacheStats.miss (); let kind = CS.Kind.Exec in let res, time_interp = - CS.record ~kind ~f:(Coq.Interp.interp ~st ~fb_queue) stm + CS.record ~kind ~f:(Lang.Interp.interp ~st ~fb_queue) stm in let time = time_hash +. time_interp in match res with - | Coq.Protect.R.Interrupted as res -> + | Lang.Protect.R.Interrupted as res -> (* Don't cache interruptions *) fb_queue := []; Stats.make ~time res - | Coq.Protect.R.Completed _ as res -> + | Lang.Protect.R.Completed _ as res -> let () = HC.add !cache (stm, st) (stm_loc, res) in let time = time_hash +. time_interp in Stats.make ~time res) diff --git a/fleche/memo.mli b/fleche/memo.mli index fccb391ae..fa57dd6e3 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -1,3 +1,10 @@ +(************************************************************************) +(* Flèche Document Manager *) +(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + module Stats : sig type 'a t = { res : 'a @@ -8,13 +15,13 @@ module Stats : sig end (* debug *) -val input_info : Coq.Ast.t * Coq.State.t -> string +val input_info : Lang.Ast.t * Lang.State.t -> string val interp_command : - st:Coq.State.t - -> fb_queue:Coq.Message.t list ref - -> Coq.Ast.t - -> Coq.State.t Coq.Interp.interp_result Stats.t + st:Lang.State.t + -> fb_queue:Lang.Message.t list ref + -> Lang.Ast.t + -> Lang.State.t Lang.Interp.interp_result Stats.t val mem_stats : unit -> int val load_from_disk : file:string -> unit diff --git a/fleche/types.ml b/fleche/types.ml index b60b6e1fb..8bea6c499 100644 --- a/fleche/types.ml +++ b/fleche/types.ml @@ -15,48 +15,19 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -(* XXX: ejgallego, do we start lines at 0? *) -module Point = struct - type t = - { line : int - ; character : int - ; offset : int - } -end - -module Range = struct - type t = - { start : Point.t - ; _end : Point.t - } -end - module Diagnostic = struct module Extra = struct type t = | FailedRequire of - { prefix : Libnames.qualid option - ; refs : Libnames.qualid list + { prefix : Lang.Ast.QualId.t option + ; refs : Lang.Ast.QualId.t list } end type t = - { range : Range.t + { range : Lang.Range.t ; severity : int ; message : string ; extra : Extra.t list } end - -let to_range (p : Loc.t) : Range.t = - let Loc.{ line_nb; line_nb_last; bol_pos; bol_pos_last; bp; ep; _ } = p in - let start_line = line_nb - 1 in - let start_col = bp - bol_pos in - let end_line = line_nb_last - 1 in - let end_col = ep - bol_pos_last in - Range. - { start = { line = start_line; character = start_col; offset = bp } - ; _end = { line = end_line; character = end_col; offset = ep } - } - -let to_orange = Option.map to_range diff --git a/fleche/types.mli b/fleche/types.mli index 756e6cb59..ac7e112cd 100644 --- a/fleche/types.mli +++ b/fleche/types.mli @@ -15,39 +15,19 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -module Point : sig - type t = - { line : int - ; character : int - ; offset : int - } -end - -module Range : sig - type t = - { start : Point.t - ; _end : Point.t - } -end - module Diagnostic : sig module Extra : sig type t = | FailedRequire of - { prefix : Libnames.qualid option - ; refs : Libnames.qualid list + { prefix : Lang.Ast.QualId.t option + ; refs : Lang.Ast.QualId.t list } end type t = - { range : Range.t + { range : Lang.Range.t ; severity : int ; message : string ; extra : Extra.t list } end - -(** XXX specific to Coq *) -val to_range : Loc.t -> Range.t - -val to_orange : Loc.t option -> Range.t option diff --git a/lsp/base.ml b/lsp/base.ml index cffd56c46..dc432d860 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -47,7 +47,7 @@ let mk_event m p = let json_of_thm thm = let open Proofs in match thm with | None -> `Null | Some thm -> `Assoc [ "goals", `List List.(map json_of_goal thm.t_goals) ] *) -let mk_range { Fleche.Types.Range.start; _end } : J.t = +let mk_range { Fleche.Lang.Range.start; _end } : J.t = `Assoc [ ( "start" , `Assoc @@ -60,7 +60,7 @@ let mk_range { Fleche.Types.Range.start; _end } : J.t = (* let mk_diagnostic ((p : Pos.pos), (lvl : int), (msg : string), (thm : Proofs.theorem option)) : J.json = *) let mk_diagnostic - ( (r : Fleche.Types.Range.t) + ( (r : Fleche.Lang.Range.t) , (lvl : int) , (msg : string) , (_thm : unit option) ) : J.t = diff --git a/lsp/base.mli b/lsp/base.mli index 502d2e99f..08c8269bd 100644 --- a/lsp/base.mli +++ b/lsp/base.mli @@ -15,14 +15,14 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -val mk_range : Fleche.Types.Range.t -> Yojson.Basic.t +val mk_range : Fleche.Lang.Range.t -> Yojson.Basic.t val mk_reply : id:int -> result:Yojson.Basic.t -> Yojson.Basic.t (* val mk_diagnostic : Range.t * int * string * unit option -> Yojson.Basic.t *) val mk_diagnostics : uri:string -> version:int - -> (Fleche.Types.Range.t * int * string * unit option) list + -> (Fleche.Lang.Range.t * int * string * unit option) list -> Yojson.Basic.t val std_protocol : bool ref