From d0d7026ab9dbf30926bf2b77513e5977c5153b73 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 30 May 2024 11:52:00 +0200 Subject: [PATCH] [petanque] Return extra premise information. We now return the file where the premise is defined, as well as its position and text. --- CHANGES.md | 5 + compiler/compile.ml | 6 +- {fleche => coq}/compat.ml | 8 ++ {fleche => coq}/compat.mli | 9 ++ coq/glob.ml | 190 ++++++++++++++++++++++++++++++ coq/glob.mli | 30 +++++ coq/library_file.ml | 31 ++++- coq/library_file.mli | 10 +- petanque/agent.ml | 74 +++++++++++- petanque/agent.mli | 15 ++- petanque/json_shell/jAgent.ml | 10 ++ petanque/json_shell/protocol.ml | 2 +- petanque/test/basic_api.ml | 4 +- petanque/test/json_api.ml | 25 +++- petanque/test/json_api_failure.ml | 2 +- 15 files changed, 401 insertions(+), 20 deletions(-) rename {fleche => coq}/compat.ml (93%) rename {fleche => coq}/compat.mli (79%) create mode 100644 coq/glob.ml create mode 100644 coq/glob.mli diff --git a/CHANGES.md b/CHANGES.md index 427075ba..9a73963a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -168,6 +168,11 @@ - [petanque] Return basic goal information after `run_tac`, so we avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego, #733) + - [coq] Add support for reading glob files metadata (@ejgallego, + #735) + - [petanque] Return extra premise information: file name, position, + raw_text, using the above support for reading .glob files + (@ejgallego, #735) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/compiler/compile.ml b/compiler/compile.ml index 9bbfa342..263817d0 100644 --- a/compiler/compile.ml +++ b/compiler/compile.ml @@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) = let file = Lang.LUri.File.to_string_file doc.uri in let file = Filename.remove_extension file ^ ".diags" in let diags = Fleche.Doc.diags doc in - Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags + Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags (** Return: exit status for file: @@ -47,9 +47,7 @@ let compile_file ~cc file : int = let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in let files = Coq.Files.make () in let env = Doc.Env.make ~init:root_state ~workspace ~files in - let raw = - Fleche.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) - in + let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in match Theory.Check.maybe_check ~io ~token with | None -> 102 diff --git a/fleche/compat.ml b/coq/compat.ml similarity index 93% rename from fleche/compat.ml rename to coq/compat.ml index d20d7f0b..ea4561c3 100644 --- a/fleche/compat.ml +++ b/coq/compat.ml @@ -105,6 +105,14 @@ module Result = struct let ( let+ ) r f = map f r let ( let* ) r f = bind r f end + + let split = function + | Ok (x1, x2) -> (Ok x1, Ok x2) + | Error err -> (Error err, Error err) + + let pp pp_r pp_e fmt = function + | Ok r -> Format.fprintf fmt "@[Ok: @[%a@]@]" pp_r r + | Error e -> Format.fprintf fmt "@[Error: @[%a@]@]" pp_e e end let format_to_file ~file ~f x = diff --git a/fleche/compat.mli b/coq/compat.mli similarity index 79% rename from fleche/compat.mli rename to coq/compat.mli index fa1a01a0..fc56a00c 100644 --- a/fleche/compat.mli +++ b/coq/compat.mli @@ -25,4 +25,13 @@ module Result : sig val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t end + + val split : ('a * 'b, 'e) t -> ('a, 'e) t * ('b, 'e) t + + val pp : + (Format.formatter -> 'r -> unit) + -> (Format.formatter -> 'e -> unit) + -> Format.formatter + -> ('r, 'e) Result.t + -> unit end diff --git a/coq/glob.ml b/coq/glob.ml new file mode 100644 index 00000000..6c9eb714 --- /dev/null +++ b/coq/glob.ml @@ -0,0 +1,190 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* "Ill-formed file: " ^ s + | Outdated -> "Outdated .glob file" +end + +module Info = struct + type t = + { kind : string + ; offset : int * int + } +end + +(* This is taken from coqdoc/glob_file.ml , we should share this code, but no + cycles ATM *) +module Coq = struct + module Entry_type = struct + type t = + | Library + | Module + | Definition + | Inductive + | Constructor + | Lemma + | Record + | Projection + | Instance + | Class + | Method + | Variable + | Axiom + | TacticDefinition + | Abbreviation + | Notation + | Section + | Binder + + let of_string = function + | "def" + | "coe" + | "subclass" + | "canonstruc" + | "fix" + | "cofix" + | "ex" + | "scheme" -> Definition + | "prf" | "thm" -> Lemma + | "ind" | "variant" | "coind" -> Inductive + | "constr" -> Constructor + | "indrec" | "rec" | "corec" -> Record + | "proj" -> Projection + | "class" -> Class + | "meth" -> Method + | "inst" -> Instance + | "var" -> Variable + | "defax" | "prfax" | "ax" -> Axiom + | "abbrev" | "syndef" -> Abbreviation + | "not" -> Notation + | "lib" -> Library + | "mod" | "modtype" -> Module + | "tac" -> TacticDefinition + | "sec" -> Section + | "binder" -> Binder + | s -> invalid_arg ("type_of_string:" ^ s) + end + + let read_dp ic = + let line = input_line ic in + let n = String.length line in + match line.[0] with + | 'F' -> + let lib_name = String.sub line 1 (n - 1) in + Ok lib_name + | _ -> Error (Error.Ill_formed "lib name not found in header") + + let correct_file vfile ic = + let s = input_line ic in + if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then + Error (Error.Ill_formed "DIGEST ill-formed") + else + let s = String.sub s 7 (String.length s - 7) in + match (vfile, s) with + | None, "NO" -> read_dp ic + | Some _, "NO" -> Error (Ill_formed "coming from .v file but no digest") + | None, _ -> Error (Ill_formed "digest but .v source file not available") + | Some vfile, s -> + if s = Digest.to_hex (Digest.file vfile) then + (* XXX Read F line *) + read_dp ic + else Error Outdated + + let parse_ref line = + try + (* Disable for now *) + if false then + let add_ref _ _ _ _ _ = () in + Scanf.sscanf line "R%d:%d %s %s %s %s" (fun loc1 loc2 lib_dp sp id ty -> + for loc = loc1 to loc2 do + add_ref loc lib_dp sp id (Entry_type.of_string ty); + (* Also add an entry for each module mentioned in [lib_dp], * to + use in interpolation. *) + ignore + (List.fold_right + (fun thisPiece priorPieces -> + let newPieces = + match priorPieces with + | "" -> thisPiece + | _ -> thisPiece ^ "." ^ priorPieces + in + add_ref loc "" "" newPieces Entry_type.Library; + newPieces) + (Str.split (Str.regexp_string ".") lib_dp) + "") + done) + with _ -> () + + let parse_def line : _ Result.t = + try + Scanf.sscanf line "%s %d:%d %s %s" + (fun kind loc1 loc2 section_path name -> + Ok (name, section_path, kind, (loc1, loc2))) + with Scanf.Scan_failure err -> Error err + + let process_line dp map line = + match line.[0] with + | 'R' -> + let _reference = parse_ref line in + map + | _ -> ( + match parse_def line with + | Error _ -> map + | Ok (name, section_path, kind, offset) -> + let section_path = + if String.equal "<>" section_path then "" else section_path ^ "." + in + let name = dp ^ "." ^ section_path ^ name in + let info = { Info.kind; offset } in + DefMap.add name info map) + + let read_glob vfile inc = + match correct_file vfile inc with + | Error e -> Error (Error.to_string e) + | Ok dp -> ( + let map = ref DefMap.empty in + try + while true do + let line = input_line inc in + let n = String.length line in + if n > 0 then map := process_line dp !map line + done; + assert false + with End_of_file -> Ok !map) +end + +(* Glob file that was read and parsed successfully *) +type t = Info.t DefMap.t + +let open_file file = + if Sys.file_exists file then + let vfile = Filename.remove_extension file ^ ".v" in + Compat.Ocaml_414.In_channel.with_open_text file (Coq.read_glob (Some vfile)) + else Error (Format.asprintf "Cannot open file: %s" file) + +let get_info map name = + match DefMap.find_opt name map with + | Some info -> Ok info + | None -> Error (Format.asprintf "definition %s not found in glob table" name) diff --git a/coq/glob.mli b/coq/glob.mli new file mode 100644 index 00000000..83376443 --- /dev/null +++ b/coq/glob.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* (t, string) Result.t + +module Info : sig + type t = + { kind : string + ; offset : int * int + } +end + +val get_info : t -> string -> (Info.t, string) Result.t diff --git a/coq/library_file.ml b/coq/library_file.ml index 352e7c86..b932edd8 100644 --- a/coq/library_file.ml +++ b/coq/library_file.ml @@ -31,7 +31,7 @@ let iter_constructors indsp u fn env nconstr = fn (Names.GlobRef.ConstructRef (indsp, i)) typ done -let ind_handler fn prefix (id, _) = +let ind_handler fn prefix (id, (_obj : DeclareInd.Internal.inductive_obj)) = let open Names in let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in let mind = Global.mind_of_delta_kn kn in @@ -84,8 +84,26 @@ let constructor_info (gref : Names.GlobRef.t) = let belongs_to_lib dps dp = List.exists (fun p -> Libnames.is_dirpath_prefix_of p dp) dps -let toc dps : _ list = - let res = ref [] in +module Entry = struct + type t = + { name : string + ; typ : Constr.t + ; file : string + } +end + +let try_locate_absolute_library dir = + let f = Loadpath.try_locate_absolute_library in + CErrors.to_result ~f dir + +let find_v_file dir = + match try_locate_absolute_library dir with + (* EJGA: we want to improve this as to pass the error to the client *) + | Error _ -> "error when trying to locate the .v file" + | Ok file -> file + +let toc dps : Entry.t list = + let res : Entry.t list ref = ref [] in let obj_action = let fn_c (cst : Names.Constant.t) (_ : Decls.logical_kind) (typ : Constr.t) = @@ -94,7 +112,8 @@ let toc dps : _ list = (* let () = F.eprintf "cst found: %s@\n%!" (Names.Constant.to_string cst) in *) let name = Names.Constant.to_string cst in - res := (name, typ) :: !res + let file = find_v_file cst_dp in + res := { name; typ; file } :: !res else () in (* We do nothing for inductives, note this is called both on constructors @@ -103,7 +122,9 @@ let toc dps : _ list = match constructor_info gref with | None -> () | Some (ind_dp, name) -> - if belongs_to_lib dps ind_dp then res := (name, typ) :: !res + if belongs_to_lib dps ind_dp then + let file = find_v_file ind_dp in + res := { name; typ; file } :: !res in obj_action fn_c fn_i in diff --git a/coq/library_file.mli b/coq/library_file.mli index 5795ee14..a93fd482 100644 --- a/coq/library_file.mli +++ b/coq/library_file.mli @@ -7,6 +7,14 @@ type t (** Logical path of the library *) val name : t -> Names.DirPath.t +module Entry : sig + type t = + { name : string + ; typ : Constr.t + ; file : string + } +end + (** [toc libs] Returns the list of constants and inductives found on .vo libraries [libs], as pairs of [name, typ]. Note that the constants are returned in the order they appear on the file. @@ -24,7 +32,7 @@ val toc : token:Limits.Token.t -> st:State.t -> t list - -> ((string * Constr.t) list, Loc.t) Protect.E.t + -> (Entry.t list, Loc.t) Protect.E.t (** Recovers the list of loaded libraries for state [st] *) val loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t diff --git a/petanque/agent.ml b/petanque/agent.ml index 2fba9fb6..4102db48 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -88,7 +88,7 @@ let io = let read_raw ~uri = let file = Lang.LUri.File.to_string_file uri in - try Ok Fleche.Compat.Ocaml_414.In_channel.(with_open_text file input_all) + try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all) with Sys_error err -> Error err let find_thm ~(doc : Fleche.Doc.t) ~thm = @@ -113,7 +113,7 @@ let init ~token ~debug ~root = let init = init_coq ~debug in Fleche.Io.CallBack.set io; let dir = Lang.LUri.File.to_string_file root in - (let open Fleche.Compat.Result.O in + (let open Coq.Compat.Result.O in let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in let files = Coq.Files.make () in Fleche.Doc.Env.make ~init ~workspace ~files) @@ -177,9 +177,77 @@ let goals ~token ~st = in Coq.Protect.E.map ~f (Fleche.Info.Goals.goals ~token ~st) |> protect_to_result +module Premise = struct + type t = + { full_name : string + (* should be a Coq DirPath, but let's go step by step *) + ; file : string (* file (in FS format) where the premise is found *) + ; kind : (string, string) Result.t (* type of object *) + ; range : (Lang.Range.t, string) Result.t (* a range if known *) + ; offset : (int * int, string) Result.t + (* a offset in the file if known (from .glob files) *) + ; raw_text : (string, string) Result.t (* raw text of the premise *) + } +end + +module Memo = struct + module H = Hashtbl.Make (CString) + + let table_glob = H.create 1000 + + let open_file glob = + match H.find_opt table_glob glob with + | Some g -> g + | None -> + let g = Coq.Glob.open_file glob in + H.add table_glob glob g; + g + + let table_source = H.create 1000 + + let input_source file = + match H.find_opt table_source file with + | Some res -> res + | None -> + if Sys.file_exists file then ( + let res = + Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all) + in + H.add table_source file res; + res) + else + let res = Error "source file is not available" in + H.add table_source file res; + res +end + +let info_of ~glob ~name = + let open Coq.Compat.Result.O in + let* g = Memo.open_file glob in + let+ { Coq.Glob.Info.kind; offset } = Coq.Glob.get_info g name in + (kind, offset) + +let raw_of ~file ~offset = + match offset with + | Ok (bp, ep) -> + let open Coq.Compat.Result.O in + let* c = Memo.input_source file in + if String.length c < ep then Error "offset out of bounds" + else Ok (String.sub c bp (ep - bp + 1)) + | Error err -> Error ("offset information is not available: " ^ err) + +let to_premise (p : Coq.Library_file.Entry.t) : Premise.t = + let { Coq.Library_file.Entry.name; typ = _; file } = p in + let file = Filename.(remove_extension file ^ ".v") in + let glob = Filename.(remove_extension file ^ ".glob") in + let range = Error "not implemented yet" in + let kind, offset = info_of ~glob ~name |> Coq.Compat.Result.split in + let raw_text = raw_of ~file ~offset in + { full_name = name; file; kind; range; offset; raw_text } + let premises ~token ~st = (let open Coq.Protect.E.O in let* all_libs = Coq.Library_file.loaded ~token ~st in let+ all_premises = Coq.Library_file.toc ~token ~st all_libs in - List.map fst all_premises) + List.map to_premise all_premises) |> protect_to_result diff --git a/petanque/agent.mli b/petanque/agent.mli index 7e4782e8..18a3152d 100644 --- a/petanque/agent.mli +++ b/petanque/agent.mli @@ -78,7 +78,20 @@ val goals : -> st:State.t -> string Coq.Goals.reified_pp option R.t +module Premise : sig + type t = + { full_name : string + (* should be a Coq DirPath, but let's go step by step *) + ; file : string (* file (in FS format) where the premise is found *) + ; kind : (string, string) Result.t (* type of object *) + ; range : (Lang.Range.t, string) Result.t (* a range if known *) + ; offset : (int * int, string) Result.t + (* a offset in the file if known (from .glob files) *) + ; raw_text : (string, string) Result.t (* raw text of the premise *) + } +end + (** Return the list of defined constants and inductives for a given state. For now we just return their fully qualified name, but more options are of course possible. *) -val premises : token:Coq.Limits.Token.t -> st:State.t -> string list R.t +val premises : token:Coq.Limits.Token.t -> st:State.t -> Premise.t list R.t diff --git a/petanque/json_shell/jAgent.ml b/petanque/json_shell/jAgent.ml index 0688ef58..d69ecb82 100644 --- a/petanque/json_shell/jAgent.ml +++ b/petanque/json_shell/jAgent.ml @@ -33,3 +33,13 @@ end module Goals = struct type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson] end + +module Lang = struct + module Range = struct + type t = Lsp.JLang.Range.t [@@deriving yojson] + end +end + +module Premise = struct + type t = [%import: Petanque.Agent.Premise.t] [@@deriving yojson] +end diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml index 06707d3a..a3c0defb 100644 --- a/petanque/json_shell/protocol.ml +++ b/petanque/json_shell/protocol.ml @@ -166,7 +166,7 @@ module Premises = struct end module Response = struct - type t = string list [@@deriving yojson] + type t = Premise.t list [@@deriving yojson] end module Handler = struct diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index 9b5ed231..19219ada 100644 --- a/petanque/test/basic_api.ml +++ b/petanque/test/basic_api.ml @@ -21,7 +21,7 @@ let start ~token = Petanque.Agent.trace_ref := trace; Petanque.Agent.message_ref := message; (* Will this work on Windows? *) - let open Fleche.Compat.Result.O in + let open Coq.Compat.Result.O in let root, uri = prepare_paths () in let* env = Agent.init ~token ~debug ~root in Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons" @@ -31,7 +31,7 @@ let extract_st (st : _ Agent.Run_result.t) = | Proof_finished st | Current_state st -> st let main () = - let open Fleche.Compat.Result.O in + let open Coq.Compat.Result.O in let token = Coq.Limits.create_atomic () in let r ~st ~tac = let st = extract_st st in diff --git a/petanque/test/json_api.ml b/petanque/test/json_api.ml index 4357e536..6deb7dc9 100644 --- a/petanque/test/json_api.ml +++ b/petanque/test/json_api.ml @@ -17,8 +17,28 @@ let extract_st (st : Protocol.RunTac.Response.t) = match st with | Proof_finished st | Current_state st -> st +let pp_offset fmt (bp, ep) = Format.fprintf fmt "(%d,%d)" bp ep + +let pp_res_str = + Coq.Compat.Result.pp Format.pp_print_string Format.pp_print_string + +let pp_premise fmt + { Petanque.Agent.Premise.full_name + ; kind + ; file + ; range = _ + ; offset + ; raw_text + } = + Format.( + fprintf fmt + "@[{ name = %s;@ file = %s;@ kind = %a;@ offset = %a;@ raw_text = %a}@]@\n" + full_name file pp_res_str kind + (Coq.Compat.Result.pp pp_offset pp_print_string) + offset pp_res_str raw_text) + let run (ic, oc) = - let open Fleche.Compat.Result.O in + let open Coq.Compat.Result.O in let debug = false in let module S = Client.S (struct let ic = ic @@ -34,7 +54,8 @@ let run (ic, oc) = let root, uri = prepare_paths () in let* env = S.init { debug; root } in let* st = S.start { env; uri; thm = "rev_snoc_cons" } in - let* _premises = S.premises { st } in + let* premises = S.premises { st } in + Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises); let* st = S.run_tac { st; tac = "induction l." } in let* st = r ~st ~tac:"-" in let* st = r ~st ~tac:"reflexivity." in diff --git a/petanque/test/json_api_failure.ml b/petanque/test/json_api_failure.ml index 7e2e1eff..71bce482 100644 --- a/petanque/test/json_api_failure.ml +++ b/petanque/test/json_api_failure.ml @@ -18,7 +18,7 @@ let extract_st (st : Protocol.RunTac.Response.t) = | Proof_finished st | Current_state st -> st let run (ic, oc) = - let open Fleche.Compat.Result.O in + let open Coq.Compat.Result.O in let debug = false in let module S = Client.S (struct let ic = ic