From 7efd7c0af92dcba3b6ce66c388250c0800fd68b0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 3 Jul 2025 16:44:24 +0200
Subject: [PATCH 01/58] New command "deindex PATH"
It deindex all constants whose path is a suffix of PATH.
Question: what are useful CLI args for deindex? E.g.
- a list of filenames
- a .pkg file (or the fact that it must use the .pkg file)
- a user-provided PATH like it is now?
Moreover notice that there is currently no check that PATH is a well-formed
PATH and A.B matches A.BC as a prefix.
---
src/cli/lambdapi.ml | 22 +++++++++++++++++-
src/tool/indexing.ml | 54 +++++++++++++++++++++++++++++++++++++------
src/tool/indexing.mli | 1 +
3 files changed, 69 insertions(+), 8 deletions(-)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index af1c5cf48..8fb85bc9b 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -112,6 +112,14 @@ let index_cmd cfg add_only rules files dbpath_opt =
Tool.Indexing.dump ~dbpath () in
Error.handle_exceptions run
+let deindex_cmd cfg path dbpath_opt =
+ Config.init cfg;
+ let run () =
+ Tool.Indexing.deindex_path path ;
+ let dbpath = Option.get Path.default_dbpath dbpath_opt in
+ Tool.Indexing.dump ~dbpath () in
+ Error.handle_exceptions run
+
end
(** Running the main type-checking mode. *)
@@ -488,6 +496,11 @@ let path_in_url : string option CLT.t =
"The path in the URL accepted by the server." in
Arg.(value & opt (some string) None & info ["url"] ~docv:"String" ~doc)
+let path_prefix : string CLT.t =
+ let doc =
+ "The prefix path of the constants to de-index." in
+ Arg.(required & pos 0 (some string) None & info [] ~docv:"PATH" ~doc)
+
let header_file_arg : string option CLT.t =
let doc =
"html file holding the header of the web page of the server." in
@@ -500,6 +513,13 @@ let index_cmd =
Cmdliner.Term.(const LPSearchMain.index_cmd $ Config.full
$ add_only_arg $ rules_arg $ files $ custom_dbpath)
+let deindex_cmd =
+ let doc =
+ "De-index all constants whose path is a suffix of the given path." in
+ Cmd.v (Cmd.info "deindex" ~doc ~man:man_pkg_file)
+ Cmdliner.Term.(const LPSearchMain.deindex_cmd $ Config.full
+ $ path_prefix $ custom_dbpath)
+
let search_cmd =
let doc = "Run a search query against the index." in
Cmd.v (Cmd.info "search" ~doc ~man:man_pkg_file)
@@ -522,7 +542,7 @@ let _ =
[ check_cmd ; parse_cmd ; export_cmd ; lsp_server_cmd
; decision_tree_cmd ; help_cmd ; version_cmd
; Init.cmd ; Install.install_cmd ; Install.uninstall_cmd
- ; index_cmd ; search_cmd ; websearch_cmd ]
+ ; index_cmd ; deindex_cmd ; search_cmd ; websearch_cmd ]
in
let doc = "A type-checker for the lambdapi-calculus modulo rewriting." in
let sdocs = Manpage.s_common_options in
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 57bcc4e2d..bac773853 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -3,6 +3,10 @@ open Common open Pos
type sym_name = Common.Path.t * string
+let is_path_prefix patt p =
+ let string_of_path x = Format.asprintf "%a" Common.Path.pp x in
+ Lplib.String.is_prefix patt (string_of_path p)
+
let name_of_sym s = (s.sym_path, s.sym_name)
(* discrimination tree *)
@@ -145,6 +149,38 @@ let insert_name (namemap,index) name v =
| Some l -> l in
Lplib.Extra.StrMap.add name (v::vs) namemap, index
+let rec remove_index ~what =
+ function
+ | Leaf l ->
+ let l' = List.filter what l in
+ (match l' with
+ | [] -> Choice []
+ | _::_ -> Leaf l')
+ | Choice l ->
+ Choice (List.filter_map (remove_node ~what) l)
+
+and remove_node ~what =
+ function
+ | IHOLE i ->
+ (match remove_index ~what i with
+ | Choice [] -> None
+ | i' -> Some (IHOLE i'))
+ | IRigid (r,i) ->
+ (match remove_index ~what i with
+ | Choice [] -> None
+ | i' -> Some (IRigid (r,i')))
+
+let remove_from_name_index ~what i =
+ Lplib.Extra.StrMap.filter_map
+ (fun _ l ->
+ let f x = if what x then Some x else None in
+ match List.filter_map f l with
+ | [] -> None
+ | l' -> Some l') i
+
+let remove ~what (dbname, index) =
+ remove_from_name_index ~what dbname, remove_index ~what index
+
let rec search_index ~generalize index stack =
match index,stack with
| Leaf vs, [] -> vs
@@ -330,6 +366,10 @@ module DB = struct
let db' = Index.insert_name (Lazy.force !db) k v in
db := lazy db'
+ let remove ~what =
+ let db' = Index.remove ~what (Lazy.force !db) in
+ db := lazy db'
+
let set_of_list ~generalize k l =
ItemSet.of_list
(List.map
@@ -569,6 +609,10 @@ let index_sign sign =
rules)
rules
+let deindex_path path =
+ DB.remove
+ ~what:(fun (((sym_path,_),_),_) -> not (is_path_prefix path sym_path))
+
(* let's flatten the interface *)
include DB
@@ -626,12 +670,8 @@ module QueryLanguage = struct
(fun _ positions1 positions2 -> Some (positions1 @ positions2))
let filter set f =
- let f ((p',_),_) _ =
- match f with
- | Path p ->
- let string_of_path x = Format.asprintf "%a" Common.Path.pp x in
- Lplib.String.is_prefix p (string_of_path p') in
- ItemSet.filter f set
+ let g ((p',_),_) _ = let Path p = f in is_path_prefix p p' in
+ ItemSet.filter g set
let answer_query ~mok ss env =
let rec aux =
@@ -707,4 +747,4 @@ let _ =
assert (transform_ascii_to_unicode " forall x, y" = " Π x, y");
assert (transform_ascii_to_unicode "forall x, y" = "Π x, y");
assert (transform_ascii_to_unicode "forall.x, y" = "Π.x, y");
- assert (transform_ascii_to_unicode "((forall x, y" = "((Π x, y")
\ No newline at end of file
+ assert (transform_ascii_to_unicode "((forall x, y" = "((Π x, y")
diff --git a/src/tool/indexing.mli b/src/tool/indexing.mli
index 63ee8febb..c0068156a 100644
--- a/src/tool/indexing.mli
+++ b/src/tool/indexing.mli
@@ -4,6 +4,7 @@ open Core
val empty : unit -> unit
val load_rewriting_rules: string list -> unit
val index_sign : Sign.t -> unit
+val deindex_path : string -> unit
val dump : dbpath:string -> unit -> unit
(* search command used by cli *)
From a4c58fff91e49eb6a3483516919c99d22199f8b4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 4 Jul 2025 11:23:56 +0200
Subject: [PATCH 02/58] Added new filter Q | "regexp"
---
src/parsing/lpParser.mly | 3 +++
src/parsing/searchQuerySyntax.ml | 1 +
src/tool/indexing.ml | 14 +++++++++++---
3 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
index 4f229ce23..1b6dddd11 100644
--- a/src/parsing/lpParser.mly
+++ b/src/parsing/lpParser.mly
@@ -502,5 +502,8 @@ search_query:
else
Format.asprintf "%a.%a" Core.Print.path p Core.Print.uid n in
SearchQuerySyntax.QFilter (q,Path path) }
+ | q=search_query VBAR s=STRINGLIT
+ { let re = Str.regexp s in
+ SearchQuerySyntax.QFilter (q,RegExp re) }
%%
diff --git a/src/parsing/searchQuerySyntax.ml b/src/parsing/searchQuerySyntax.ml
index ab32e66ba..078545ba0 100644
--- a/src/parsing/searchQuerySyntax.ml
+++ b/src/parsing/searchQuerySyntax.ml
@@ -16,6 +16,7 @@ type op =
| Union
type filter =
| Path of string
+ | RegExp of Str.regexp
type query =
| QBase of base_query
| QOpp of query * op * query
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index bac773853..ec4da202c 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -3,9 +3,14 @@ open Common open Pos
type sym_name = Common.Path.t * string
+let string_of_path x = Format.asprintf "%a" Common.Path.pp x
+
let is_path_prefix patt p =
- let string_of_path x = Format.asprintf "%a" Common.Path.pp x in
- Lplib.String.is_prefix patt (string_of_path p)
+ Lplib.String.is_prefix patt (string_of_path p)
+
+let re_matches_sym_name re (p,name) =
+ (* CSC: fix me *)
+ Str.string_match re (string_of_path p ^ "." ^ name) 0
let name_of_sym s = (s.sym_path, s.sym_name)
@@ -670,7 +675,10 @@ module QueryLanguage = struct
(fun _ positions1 positions2 -> Some (positions1 @ positions2))
let filter set f =
- let g ((p',_),_) _ = let Path p = f in is_path_prefix p p' in
+ let g ((p',_ as name),_) _ =
+ match f with
+ | Path p -> is_path_prefix p p'
+ | RegExp re -> re_matches_sym_name re name in
ItemSet.filter g set
let answer_query ~mok ss env =
From b87fc34d220acdc1c433d49b3bc31213f6bfc281 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Sun, 6 Jul 2025 19:18:09 +0200
Subject: [PATCH 03/58] Use tail recursive functions in a few places
Now the query 'concl >= _ | ".*vsum.*"' terminates on the medium-sized HOL
light extraction
---
src/tool/indexing.ml | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index ec4da202c..30a86db55 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -14,6 +14,10 @@ let re_matches_sym_name re (p,name) =
let name_of_sym s = (s.sym_path, s.sym_name)
+(* Tail recursive implementation of List.append for
+ OCaml < 5.1 *)
+let (@) l1 l2 = List.rev_append (List.rev l1) l2
+
(* discrimination tree *)
(* substitution trees would be best *)
@@ -376,8 +380,9 @@ module DB = struct
db := lazy db'
let set_of_list ~generalize k l =
+ (* rev_map is used because it is tail recursive *)
ItemSet.of_list
- (List.map
+ (List.rev_map
(fun (i,pos) ->
i, List.map (fun x -> generalize,k,x) pos) l)
From 52ec33c0d5456164f3994e5bfbb93ea9a17cda1b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Sun, 6 Jul 2025 19:18:18 +0200
Subject: [PATCH 04/58] More issues
---
TODO.md | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/TODO.md b/TODO.md
index a1364e94e..53a0e70da 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,22 @@ TODO
Index and search
----------------
+* After "Number of results: 3" there is a missing CRLF
+
+* why type only supports? =
+ also doc is wrong, but I suppose code is wrong
+
+* concl = _
+ justifications include the following that are not expected
+ $0.[V#] occurs inside the spine of the type and
+ $0.[V#] occurs inside the hypothesis of the type and
+ $0.[V#] occurs as the exact hypothesis of the type and
+ $0.[V#] occurs as the exact conclusion of the type and
+ $0.[V#] occurs inside the conclusion of the type and
+
+* CLI interface: it tries to render way too many results
+ and it takes ages
+
* Too many results found?
anywhere >= (Π x: _, (= _ V# V#))
From 40f3efbc33611f67f3566049096ca6094e01c220 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Sun, 6 Jul 2025 20:54:57 +0200
Subject: [PATCH 05/58] Bug fixed: too many justifications returned
a query like 'concl = _' was returning justifications of the form
_ found in hypothesis
Now only really relevant justifications are returned
Signed-off-by: Claudio Sacerdoti Coen
---
TODO.md | 18 ++++++++++--------
src/tool/indexing.ml | 25 +++++++++++++------------
2 files changed, 23 insertions(+), 20 deletions(-)
diff --git a/TODO.md b/TODO.md
index 53a0e70da..d0fa28c97 100644
--- a/TODO.md
+++ b/TODO.md
@@ -9,14 +9,6 @@ Index and search
* why type only supports? =
also doc is wrong, but I suppose code is wrong
-* concl = _
- justifications include the following that are not expected
- $0.[V#] occurs inside the spine of the type and
- $0.[V#] occurs inside the hypothesis of the type and
- $0.[V#] occurs as the exact hypothesis of the type and
- $0.[V#] occurs as the exact conclusion of the type and
- $0.[V#] occurs inside the conclusion of the type and
-
* CLI interface: it tries to render way too many results
and it takes ages
@@ -36,3 +28,13 @@ anywhere >= (Π x: _, (= _ x x))
* alignments with same name ==> automatic preference?
* better pagination
+
+Performance improvements
+------------------------
+
+* see if compressing the index yields a significant gain
+
+* currently in a query like 'concl = _' it builds an extremely large matching set
+ and THEN it filters out the justifications that have Concl Exact; maybe we
+ could save a lot of time anticipating the filtrage
+
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 30a86db55..3a525e0a2 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -646,17 +646,18 @@ module QueryLanguage = struct
| _, _ -> false
let filter_constr constr _ positions =
- match constr with
- | QType wherep ->
- List.exists
- (function
- | _,_,Type where -> match_where wherep where
- | _ -> false) positions
- | QXhs (insp,sidep) ->
- List.exists
- (function
- | _,_,Xhs (ins,side) -> match_opt insp ins && match_opt sidep side
- | _ -> false) positions
+ Option.map (fun x -> [x])
+ (match constr with
+ | QType wherep ->
+ List.find_opt
+ (function
+ | _,_,Type where -> match_where wherep where
+ | _ -> false) positions
+ | QXhs (insp,sidep) ->
+ List.find_opt
+ (function
+ | _,_,Xhs (ins,side) -> match_opt insp ins && match_opt sidep side
+ | _ -> false) positions)
let answer_base_query ~mok ss env =
function
@@ -665,7 +666,7 @@ module QueryLanguage = struct
let res = search_pterm ~generalize ~mok ss env patt in
(match constr with
| None -> res
- | Some constr -> ItemSet.filter (filter_constr constr) res)
+ | Some constr -> ItemSet.filter_map (filter_constr constr) res)
let perform_op =
function
From 02489efe14a4963d0b6d67cd65707ec2efdc3392 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Mon, 7 Jul 2025 00:00:12 +0200
Subject: [PATCH 06/58] Issue understood
---
TODO.md | 18 +++++++++++++-----
1 file changed, 13 insertions(+), 5 deletions(-)
diff --git a/TODO.md b/TODO.md
index d0fa28c97..c1dcf73c9 100644
--- a/TODO.md
+++ b/TODO.md
@@ -12,11 +12,6 @@ Index and search
* CLI interface: it tries to render way too many results
and it takes ages
-* Too many results found?
-
-anywhere >= (Π x: _, (= _ V# V#))
-anywhere >= (Π x: _, (= _ x x))
-
* html tags in textual output :-(
* would it be more reasonable to save the normalization rules
@@ -38,3 +33,16 @@ Performance improvements
and THEN it filters out the justifications that have Concl Exact; maybe we
could save a lot of time anticipating the filtrage
+Misleading output
+-----------------
+
++ Too many results found?
+
+anywhere >= (Π x: _, (= _ V# V#))
+anywhere >= (Π x: _, (= _ x x))
+
+NO, it's ok, but the output is misleading. The second form is equivalent
+to the first that is equivalent to (_ -> (= _ V# V#)) that is what it is
+found. However it shows the pattern saying that " (Π x: _, (= _ x x))" was
+found, that is the misleading thing.
+
From a01c625f1e159b1865599b1b7fff6d4a1e58d1e2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Mon, 7 Jul 2025 17:09:00 +0200
Subject: [PATCH 07/58] Showing mapping to Coq files in search results
1. during indexing using --source=PATH one can add indexing information
mapping LP identifiers to Coq identifiers and locations
2. when the search results are shown, the Coq code is also printed if
the LP identifier is found in the map in point 1
The code to generate the file used in 1 should belong to HOL2DK. Right now
we have hacked some best-effort shell script that we will commit in the
HOL2DK_indexing repository
---
TODO.md | 10 +++
src/cli/lambdapi.ml | 10 ++-
src/common/pos.ml | 40 ++++++---
src/tool/indexing.ml | 191 ++++++++++++++++++++++++++++--------------
src/tool/indexing.mli | 1 +
5 files changed, 174 insertions(+), 78 deletions(-)
diff --git a/TODO.md b/TODO.md
index c1dcf73c9..80c9b5236 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,16 @@ TODO
Index and search
----------------
+* generate mappings from LP to V automatically with HOL2DK and find
+ what to do with manually written files; also right now there are
+ mappings that are lost and mappings that are confused in a many-to-one
+ relation
+
+* document new features, e.g. -sources (and find better
+ terminology), deindex
+
+* remove should remove also from source index
+
* After "Number of results: 3" there is a missing CRLF
* why type only supports? =
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 8fb85bc9b..fd8141983 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -95,7 +95,7 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
Tool.Websearch.start ~header ss ~port ~dbpath ~path_in_url () in
Error.handle_exceptions run
-let index_cmd cfg add_only rules files dbpath_opt =
+let index_cmd cfg add_only rules files source dbpath_opt =
Config.init cfg;
let run () =
if not add_only then Tool.Indexing.empty ();
@@ -108,6 +108,7 @@ let index_cmd cfg add_only rules files dbpath_opt =
Tool.Indexing.load_rewriting_rules rules;
Tool.Indexing.index_sign (no_wrn Compile.compile_file file) in
List.iter handle files;
+ Option.iter Tool.Indexing.parse_source_map source;
let dbpath = Option.get Path.default_dbpath dbpath_opt in
Tool.Indexing.dump ~dbpath () in
Error.handle_exceptions run
@@ -491,6 +492,11 @@ let custom_dbpath : string option CLT.t =
"Path to the search DB file." in
Arg.(value & opt (some string) None & info ["db"] ~docv:"PATH" ~doc)
+let source_file : string option CLT.t =
+ let doc =
+ "Path to the mapping to additional sources." in
+ Arg.(value & opt (some string) None & info ["sources"] ~docv:"PATH" ~doc)
+
let path_in_url : string option CLT.t =
let doc =
"The path in the URL accepted by the server." in
@@ -511,7 +517,7 @@ let index_cmd =
let doc = "Index the given files." in
Cmd.v (Cmd.info "index" ~doc ~man:man_pkg_file)
Cmdliner.Term.(const LPSearchMain.index_cmd $ Config.full
- $ add_only_arg $ rules_arg $ files $ custom_dbpath)
+ $ add_only_arg $ rules_arg $ files $ source_file $ custom_dbpath)
let deindex_cmd =
let doc =
diff --git a/src/common/pos.ml b/src/common/pos.ml
index 788dba866..00dc0f989 100644
--- a/src/common/pos.ml
+++ b/src/common/pos.ml
@@ -144,11 +144,14 @@ let make_pos : Lexing.position * Lexing.position -> 'a -> 'a loc =
file at position [pos]. [sep] is the separator replacing each newline
(e.g. " \n"). [delimiters] is a pair of delimiters used to wrap the
"unknown location" message returned when the position does not refer to a
- file. [escape] is used to escape the file contents.*)
+ file. [escape] is used to escape the file contents.
+
+ The value -1 for end_col is to be interpreted as "at the end of line". *)
let print_file_contents :
escape:(string -> string) ->
- delimiters:(string*string) -> popt Lplib.Base.pp =
- fun ~escape ~delimiters:(db,de) ppf pos ->
+ delimiters:(string*string) -> complain_if_location_unknown:bool ->
+ popt Lplib.Base.pp =
+ fun ~escape ~delimiters:(db,de) ~complain_if_location_unknown ppf pos ->
match pos with
| Some { fname=Some fname; start_line; start_col; end_line; end_col } ->
(* WARNING: do not try to understand the following code!
@@ -156,7 +159,10 @@ let print_file_contents :
(* ignore the lines before the start_line *)
let ch = open_in fname in
- let out = Buffer.create ((end_line - start_line) * 80 + end_col + 1) in
+ let out =
+ Buffer.create
+ ((end_line - start_line) * 80 +
+ (if end_col = -1 then 80 else end_col) + 1) in
for i = 0 to start_line - 2 do
ignore (input_line ch)
done ;
@@ -189,20 +195,32 @@ let print_file_contents :
(* identify what the end_line is and how many UTF8 codepoints to keep *)
let endl,end_col =
if start_line = end_line then
- startstr, end_col - start_col
+ if end_col = -1 then
+ startstr, -1
+ else
+ startstr, end_col - start_col
else input_line ch, end_col in
(* keep the first end_col UTF8 codepoints of the end_line *)
assert (String.is_valid_utf_8 endl);
let bytepos = ref 0 in
- for i = 0 to end_col - 1 do
- let uchar = String.get_utf_8_uchar endl !bytepos in
- assert (Uchar.utf_decode_is_valid uchar) ;
- bytepos := !bytepos + Uchar.utf_decode_length uchar
- done ;
+ let i = ref 0 in
+ (try
+ while !i <= end_col -1 || end_col = -1 do
+ let uchar = String.get_utf_8_uchar endl !bytepos in
+ assert (Uchar.utf_decode_is_valid uchar) ;
+ bytepos := !bytepos + Uchar.utf_decode_length uchar ;
+ incr i
+ done
+ with
+ Invalid_argument _ -> () (* End of line reached *)) ;
let str = String.sub endl 0 !bytepos in
Buffer.add_string out (escape str) ;
close_in ch ;
string ppf (Buffer.contents out)
- | None | Some {fname=None} -> string ppf (db ^ "unknown location" ^ de)
+ | None | Some {fname=None} ->
+ if complain_if_location_unknown then
+ string ppf (db ^ "unknown location" ^ de)
+ else
+ string ppf ""
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 3a525e0a2..f078b9193 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -18,6 +18,17 @@ let name_of_sym s = (s.sym_path, s.sym_name)
OCaml < 5.1 *)
let (@) l1 l2 = List.rev_append (List.rev l1) l2
+let dump_to ~filename i =
+ let ch = open_out_bin filename in
+ Marshal.to_channel ch i [] ;
+ close_out ch
+
+let restore_from ~filename =
+ let ch = open_in_bin filename in
+ let i = Marshal.from_channel ch in
+ close_in ch ;
+ i
+
(* discrimination tree *)
(* substitution trees would be best *)
@@ -219,17 +230,6 @@ let search ~generalize (_,index) term =
let locate_name (namemap,_) name =
match Lplib.Extra.StrMap.find_opt name namemap with None -> [] | Some l -> l
-let dump_to ~filename i =
- let ch = open_out_bin filename in
- Marshal.to_channel ch i [] ;
- close_out ch
-
-let restore_from ~filename =
- let ch = open_in_bin filename in
- let i = Marshal.from_channel ch in
- close_in ch ;
- i
-
end
module DB = struct
@@ -283,8 +283,99 @@ module DB = struct
m) empty l
end
+ module Sym_nameMap =
+ Map.Make(struct type t = sym_name let compare = compare end)
+
type answer = ((*generalized:*)bool * term * position) list
+ (* disk persistence *)
+
+ let the_dbpath : string ref = ref Path.default_dbpath
+
+ let rwpaths = ref []
+
+ let restore_from_disk () =
+ try restore_from ~filename:!the_dbpath
+ with Sys_error msg ->
+ Common.Error.wrn None "%s.\n\
+ Type \"lambdapi index --help\" to learn how to create the index." msg ;
+ Sym_nameMap.empty, Index.empty
+
+ (* The persistent database *)
+ let db :
+ ((string * string * int * int) Sym_nameMap.t *
+ (item * position list) Index.db) Lazy.t ref =
+ ref (lazy (restore_from_disk ()))
+
+ let empty () = db := lazy (Sym_nameMap.empty,Index.empty)
+
+ let insert k v =
+ let sidx,idx = Lazy.force !db in
+ let db' = sidx, Index.insert idx k v in
+ db := lazy db'
+
+ let insert_name k v =
+ let sidx,idx = Lazy.force !db in
+ let db' = sidx, Index.insert_name idx k v in
+ db := lazy db'
+
+ let remove ~what =
+ let sidx,idx = Lazy.force !db in
+ let db' = sidx,Index.remove ~what idx in
+ db := lazy db'
+
+ let set_of_list ~generalize k l =
+ (* rev_map is used because it is tail recursive *)
+ ItemSet.of_list
+ (List.rev_map
+ (fun (i,pos) ->
+ i, List.map (fun x -> generalize,k,x) pos) l)
+
+ let search ~generalize k =
+ set_of_list ~generalize k
+ (Index.search ~generalize (snd (Lazy.force !db)) k)
+
+ let dump ~dbpath () =
+ dump_to ~filename:dbpath (Lazy.force !db)
+
+ let locate_name name =
+ let k = Term.mk_Wild (* dummy, unused *) in
+ set_of_list ~generalize:false k
+ (Index.locate_name (snd (Lazy.force !db)) name)
+
+ let parse_source_map filename =
+ let sidx,idx = Lazy.force !db in
+ let sidx = ref sidx in
+ let ch = open_in filename in
+ (try
+ while true do
+ let line = input_line ch in
+ match String.split_on_char ' ' line with
+ | [fname; start_line; end_line; sourceid; lpid] ->
+ let rec sym_name_of =
+ function
+ | [] -> assert false
+ | [name] -> [],name
+ | hd::tl -> let path,name = sym_name_of tl in hd::path,name in
+ let lpid = sym_name_of (String.split_on_char '.' lpid) in
+ let start_line = int_of_string start_line in
+ let end_line = int_of_string end_line in
+ sidx :=
+ Sym_nameMap.add lpid (sourceid,fname,start_line,end_line) !sidx
+ | _ ->
+ raise
+ (Common.Error.Fatal(None,"wrong file format for source map file"))
+ done ;
+ with
+ | Failure _ as exn ->
+ close_in ch;
+ raise
+ (Common.Error.Fatal(None,"wrong file format for source map file: " ^
+ Printexc.to_string exn))
+ | End_of_file -> close_in ch) ;
+ db := lazy (!sidx,idx)
+
+
type ho_pp = { run : 'a. 'a Lplib.Base.pp -> 'a Lplib.Base.pp }
let identity_escaper : ho_pp =
@@ -296,6 +387,15 @@ module DB = struct
Format.pp_print_string fmt res
}
+ let source_infos_of_sym_name sym_name =
+ match Sym_nameMap.find_opt sym_name (fst (Lazy.force !db)) with
+ | None -> None, None
+ | Some (sourceid, fname, start_line, end_line) ->
+ let start_col = 0 in
+ let end_col = -1 in (* to the end of line *)
+ Some sourceid,
+ Some { fname=Some fname; start_line; start_col; end_line; end_col }
+
let generic_pp_of_position_list ~escaper ~sep =
Lplib.List.pp
(fun ppf position ->
@@ -323,14 +423,25 @@ module DB = struct
Lplib.Base.out fmt "Nothing found"
else
Lplib.List.pp
- (fun ppf (((p,n),pos),(positions : answer)) ->
- Lplib.Base.out ppf "%s%a.%s%s%s@%s%s%a%s%s%s%a%s%s%s@."
+ (fun ppf (((p,n) as sym_name,pos),(positions : answer)) ->
+ let sourceid,sourcepos = source_infos_of_sym_name sym_name in
+ Lplib.Base.out ppf "%s%a.%s%s%s@%s%s%a%s%s%s%a%s%a%s%a%s%s%s@."
lisb (escaper.run Core.Print.path) p boldb n bolde
(popt_to_string ~print_dirname:false pos)
separator (generic_pp_of_position_list ~escaper ~sep) positions
separator preb codeb
- (Common.Pos.print_file_contents ~escape ~delimiters)
- pos codee pree lise)
+ (Common.Pos.print_file_contents ~escape ~delimiters
+ ~complain_if_location_unknown:true) pos
+ separator
+ (fun ppf opt ->
+ match opt with
+ | None -> Lplib.Base.string ppf ""
+ | Some sourceid ->
+ Lplib.Base.string ppf ("Translated to " ^ sourceid)) sourceid
+ separator
+ (Common.Pos.print_file_contents ~escape ~delimiters
+ ~complain_if_location_unknown:false) sourcepos
+ codee pree lise)
"" fmt l
let html_of_item_list =
@@ -349,56 +460,6 @@ module DB = struct
let html_of_results_list from fmt l =
Lplib.Base.out fmt "%a" from html_of_item_list l
- (* disk persistence *)
-
- let the_dbpath : string ref = ref Path.default_dbpath
-
- let rwpaths = ref []
-
- let restore_from_disk () =
- try Index.restore_from ~filename:!the_dbpath
- with Sys_error msg ->
- Common.Error.wrn None "%s.\n\
- Type \"lambdapi index --help\" to learn how to create the index." msg ;
- Index.empty
-
- let db : (item * position list) Index.db Lazy.t ref =
- ref (lazy (restore_from_disk ()))
-
- let empty () = db := lazy Index.empty
-
- let insert k v =
- let db' = Index.insert (Lazy.force !db) k v in
- db := lazy db'
-
- let insert_name k v =
- let db' = Index.insert_name (Lazy.force !db) k v in
- db := lazy db'
-
- let remove ~what =
- let db' = Index.remove ~what (Lazy.force !db) in
- db := lazy db'
-
- let set_of_list ~generalize k l =
- (* rev_map is used because it is tail recursive *)
- ItemSet.of_list
- (List.rev_map
- (fun (i,pos) ->
- i, List.map (fun x -> generalize,k,x) pos) l)
-
- let search ~generalize k =
- set_of_list ~generalize k
- (Index.search ~generalize (Lazy.force !db) k)
-
- let dump ~dbpath () =
- the_dbpath := dbpath;
- Index.dump_to ~filename:dbpath (Lazy.force !db)
-
- let locate_name name =
- let k = Term.mk_Wild (* dummy, unused *) in
- set_of_list ~generalize:false k
- (Index.locate_name (Lazy.force !db) name)
-
end
exception Overloaded of string * DB.answer DB.ItemSet.t
diff --git a/src/tool/indexing.mli b/src/tool/indexing.mli
index c0068156a..62b1937b4 100644
--- a/src/tool/indexing.mli
+++ b/src/tool/indexing.mli
@@ -4,6 +4,7 @@ open Core
val empty : unit -> unit
val load_rewriting_rules: string list -> unit
val index_sign : Sign.t -> unit
+val parse_source_map : string -> unit (* the name of the file *)
val deindex_path : string -> unit
val dump : dbpath:string -> unit -> unit
From 0a4b1d6df4558fbe8ad500886acb37aaf8d4f808 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Mon, 7 Jul 2025 18:18:50 +0200
Subject: [PATCH 08/58] unindex also removes from source map
---
TODO.md | 2 --
src/tool/indexing.ml | 15 +++++++++------
2 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/TODO.md b/TODO.md
index 80c9b5236..56dab35b9 100644
--- a/TODO.md
+++ b/TODO.md
@@ -12,8 +12,6 @@ Index and search
* document new features, e.g. -sources (and find better
terminology), deindex
-* remove should remove also from source index
-
* After "Number of results: 3" there is a missing CRLF
* why type only supports? =
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index f078b9193..e241fb5aa 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -319,10 +319,15 @@ module DB = struct
let db' = sidx, Index.insert_name idx k v in
db := lazy db'
- let remove ~what =
+ let remove path =
let sidx,idx = Lazy.force !db in
- let db' = sidx,Index.remove ~what idx in
- db := lazy db'
+ let keep sym_path = not (is_path_prefix path sym_path) in
+ let idx =
+ Index.remove
+ ~what:(fun (((sym_path,_),_),_) -> keep sym_path ) idx in
+ let sidx =
+ Sym_nameMap.filter (fun (sym_path,_) _ -> keep sym_path) sidx in
+ db := lazy (sidx,idx)
let set_of_list ~generalize k l =
(* rev_map is used because it is tail recursive *)
@@ -680,9 +685,7 @@ let index_sign sign =
rules)
rules
-let deindex_path path =
- DB.remove
- ~what:(fun (((sym_path,_),_),_) -> not (is_path_prefix path sym_path))
+let deindex_path path = DB.remove path
(* let's flatten the interface *)
include DB
From 15bfaef074119f02db109c0a76f15016eceab65d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Mon, 7 Jul 2025 18:43:45 +0200
Subject: [PATCH 09/58] Regular expressions now match substrings by default
It used to match only prefixes of strings, which was quite weird
---
src/tool/indexing.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index e241fb5aa..4cdfd5f43 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -9,8 +9,10 @@ let is_path_prefix patt p =
Lplib.String.is_prefix patt (string_of_path p)
let re_matches_sym_name re (p,name) =
- (* CSC: fix me *)
- Str.string_match re (string_of_path p ^ "." ^ name) 0
+ try
+ ignore (Str.search_forward re (string_of_path p ^ "." ^ name) 0) ;
+ true
+ with Not_found -> false
let name_of_sym s = (s.sym_path, s.sym_name)
From 4e7a4cfeac37acc4bc533c487a9be93979f9563a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Tue, 8 Jul 2025 13:47:47 +0200
Subject: [PATCH 10/58] Fail when trying to index the same constant twice.
Note: there's no easy way to implement the same check for rules.
However it is unlikely to index twice a file that contains only
rewriting rules.
---
src/tool/indexing.ml | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 4cdfd5f43..e784ec1d4 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -4,13 +4,14 @@ open Common open Pos
type sym_name = Common.Path.t * string
let string_of_path x = Format.asprintf "%a" Common.Path.pp x
+let string_of_sym_name (p,n) = string_of_path p ^ "." ^ n
let is_path_prefix patt p =
Lplib.String.is_prefix patt (string_of_path p)
-let re_matches_sym_name re (p,name) =
+let re_matches_sym_name re sym_name =
try
- ignore (Str.search_forward re (string_of_path p ^ "." ^ name) 0) ;
+ ignore (Str.search_forward re (string_of_sym_name sym_name) 0) ;
true
with Not_found -> false
@@ -658,6 +659,11 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
let index_sym sym =
let qname = name_of_sym sym in
(* Name *)
+ if List.exists (fun ((sn,_),_) -> sn=qname)
+ (DB.ItemSet.bindings (DB.locate_name (snd qname)))
+ then
+ raise
+ (Common.Error.Fatal(None,string_of_sym_name qname ^ " already indexed")) ;
DB.insert_name (snd qname) ((qname,sym.sym_decl_pos),[Name]) ;
(* Type + InType *)
let typ = Timed.(!(sym.Core.Term.sym_type)) in
From 9b59ee2937077cf33dc11e4673af26b00f69f56b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Tue, 8 Jul 2025 15:13:00 +0200
Subject: [PATCH 11/58] Fixed: Plac _ can occur in the r.h.s. of rewriting
rules
E.g. in last rewriting rule in tests/OK/coercions.lp
---
TODO.md | 7 +++++++
src/tool/indexing.ml | 29 +++++++++++++++++++++++++----
2 files changed, 32 insertions(+), 4 deletions(-)
diff --git a/TODO.md b/TODO.md
index 56dab35b9..4a9d0e376 100644
--- a/TODO.md
+++ b/TODO.md
@@ -32,6 +32,13 @@ Index and search
* better pagination
+* Command.handle_require_as: require as X <== what should we do with the renaming?
+
+* Compile.compile_with: where it calls link we must index all the signature
+ Sign.add_rules + Sign.add_symbol
+
+* check the semantics of indexing the Plac _ as variables
+
Performance improvements
------------------------
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index e784ec1d4..563994114 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -90,7 +90,13 @@ let rec node_of_stack t s v =
(* Let-ins are expanded during indexing *)
node_of_stack (subst bind bod) s v
| Meta _ -> assert false
- | Plac _ -> assert false (* not for meta-closed terms *)
+ | Plac _ ->
+ (* this may happen in a rewriting rule that uses a _ in the r.h.s.
+ that is NOT instantiated; the rule is meant to open a proof
+ obligation.
+
+ Tentative implementation: a placeholder is seen as a variable *)
+ IRigid(IVar, index_of_stack s v)
| Wild -> assert false (* used only by tactics and reduction *)
| TRef _ -> assert false (* destroyed by unfold *)
| Bvar _ -> assert false
@@ -114,7 +120,14 @@ let rec match_rigid r term =
| IAbst, Abst(t1,bind) -> let _, t2 = unbind bind in [t1;t2]
| IProd, Prod(t1,bind) -> let _, t2 = unbind bind in [t1;t2]
| _, LLet (_typ, bod, bind) -> match_rigid r (subst bind bod)
- | _, (Meta _ | Plac _ | Wild | TRef _) -> assert false
+ | IVar, Plac _ ->
+ (* this may happen in a rewriting rule that uses a _ in the r.h.s.
+ that is NOT instantiated; the rule is meant to open a proof
+ obligation.
+
+ Tentative implementation: a placeholder is seen as a variable *)
+ []
+ | _, (Meta _ | Wild | TRef _) -> assert false
| _, _ -> raise NoMatch
(* match anything with a flexible term *)
@@ -559,7 +572,14 @@ let rec is_flexible t =
| Appl(t,_) -> is_flexible t
| LLet(_,_,b) -> let _, t = unbind b in is_flexible t
| Vari _ | Type | Kind | Symb _ | Prod _ | Abst _ -> false
- | Meta _ | Plac _ | Wild | TRef _ | Bvar _ -> assert false
+ | Plac _ ->
+ (* this may happen in a rewriting rule that uses a _ in the r.h.s.
+ that is NOT instantiated; the rule is meant to open a proof
+ obligation
+
+ Tentative implementation: a placeholder is seen as a variable *)
+ false
+ | Meta _ | Wild | TRef _ | Bvar _ -> assert false
let enter =
DB.(function
@@ -589,6 +609,7 @@ let subterms_to_index ~is_spine t =
| Vari _
| Type
| Kind
+ | Plac _
| Symb _ -> []
| Abst(t,b) ->
let _, t2 = unbind b in
@@ -613,7 +634,7 @@ let subterms_to_index ~is_spine t =
let _, t3 = unbind b in
aux ~where:(enter where) t1 @ aux ~where:(enter where) t2 @
aux ~where:(enter where) t3
- | Meta _ | Plac _ | Wild | TRef _ -> assert false
+ | Meta _ | Wild | TRef _ -> assert false
in aux ~where:(if is_spine then Spine Exact else Conclusion Exact) t
let insert_rigid t v =
From dc5b98bf1d6794bddeed9b6b148e750358fba528 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Tue, 8 Jul 2025 15:13:40 +0200
Subject: [PATCH 12/58] add_rule reimplemented as a special case of add_rules
---
src/core/sign.ml | 22 +++++++---------------
1 file changed, 7 insertions(+), 15 deletions(-)
diff --git a/src/core/sign.ml b/src/core/sign.ml
index 52376289e..9f36eb147 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -327,21 +327,6 @@ let read =
let open Stdlib in let r = ref (dummy ()) in fun n ->
Debug.(record_time Reading (fun () -> r := read n)); !r
-(** [add_rule sign sym r] adds the new rule [r] to the symbol [sym]. When the
- rule does not correspond to a symbol of signature [sign], it is stored in
- its dependencies. /!\ does not update the decision tree or the critical
- pairs. *)
-let add_rule : t -> sym_rule -> unit = fun sign (sym,r) ->
- sym.sym_rules := !(sym.sym_rules) @ [r];
- if sym.sym_path <> sign.sign_path then
- let sm = Path.Map.find sym.sym_path !(sign.sign_deps) in
- let f = function
- | None -> Some([r],None)
- | Some(rs,n) -> Some(rs@[r],n)
- in
- let sm = StrMap.update sym.sym_name f sm in
- sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps)
-
(** [add_rules sign sym rs] adds the new rules [rs] to the symbol [sym]. When
the rules do not correspond to a symbol of signature [sign], they are
stored in its dependencies. /!\ does not update the decision tree or the
@@ -357,6 +342,13 @@ let add_rules : t -> sym -> rule list -> unit = fun sign sym rs ->
let sm = StrMap.update sym.sym_name f sm in
sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps)
+(** [add_rule sign sym r] adds the new rule [r] to the symbol [sym]. When the
+ rule does not correspond to a symbol of signature [sign], it is stored in
+ its dependencies. /!\ does not update the decision tree or the critical
+ pairs. *)
+let add_rule : t -> sym_rule -> unit = fun sign (sym,r) ->
+ add_rules sign sym [r]
+
(** [add_notation sign sym nota] changes the notation of [sym] to [nota] in
the signature [sign]. *)
let add_notation : t -> sym -> float notation -> unit = fun sign sym nota ->
From c7bf80b44fd41d9752048738e7a19af5ea2ba2bb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Tue, 8 Jul 2025 19:02:28 +0200
Subject: [PATCH 13/58] The local development is now non-permanently indexed
1. we used a Timed.ref to update the indexes with the local development
(i.e. just the files that have been required, not the others) so that it
is possible to query the local development
2. when doing "require ... as Foo" the user can use Foo.X in the queries;
(but not regular expressions involving Foo, but that seems reasonable)
We have introduced some "hakish" code here and there to be reviewed. In
particular:
1. we store in Common/Mode if we are running LSP
2. we detected that the current LSP buffer has "fname" set to an URI
"file:///". We use this feature to distinguish between the buffer
and the filesystem so that, when showing query results to the user,
if the text comes from the buffer we can retrieve it
3. we use a finely tuned combination of Stdlib.ref/Timed.ref to "remember"
things that would be forgotten. E.g.:
a) we remember the LSP buffer content *after* the end of the compilation
b) we remember the index *after* the end of the indexing of a single
file
4. we used a maison stream-like representation of file contents to be able
to retrieve the text to be shown to the user both from the filesystem
or from strings (i.e. the content of the LSP buffer)
5. since indexing is now performed even during compilation when things
enter a signature in LSP mode, we created a huge circular dependency
in the modules that we break using multiple callbacks and Stdlib.ref
that are set here and there. Maybe one can do (much) better.
In particular pure now depends on tool.
---
TODO.md | 7 +++---
src/cli/lambdapi.ml | 7 ++++--
src/common/mode.ml | 4 ++++
src/common/pos.ml | 31 +++++++++++++++---------
src/core/sign.ml | 7 +++++-
src/handle/compile.ml | 1 +
src/pure/dune | 2 +-
src/pure/pure.ml | 1 +
src/tool/indexing.ml | 55 ++++++++++++++++++++++++++++++++++++-------
src/tool/indexing.mli | 5 ++++
10 files changed, 92 insertions(+), 28 deletions(-)
create mode 100644 src/common/mode.ml
diff --git a/TODO.md b/TODO.md
index 4a9d0e376..1f6123258 100644
--- a/TODO.md
+++ b/TODO.md
@@ -32,10 +32,9 @@ Index and search
* better pagination
-* Command.handle_require_as: require as X <== what should we do with the renaming?
-
-* Compile.compile_with: where it calls link we must index all the signature
- Sign.add_rules + Sign.add_symbol
+* document require ... as Foo: using Foo.X in the query already
+ works (pure magic!); of course it does not work when using
+ regular expressions [ check before! ]
* check the semantics of indexing the Plac _ as variables
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index fd8141983..3606827d2 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -104,7 +104,7 @@ let index_cmd cfg add_only rules files source dbpath_opt =
let time = Time.save () in
let handle file =
Console.reset_default ();
- Time.restore time;
+ Tool.Indexing.preserving_index Time.restore time;
Tool.Indexing.load_rewriting_rules rules;
Tool.Indexing.index_sign (no_wrn Compile.compile_file file) in
List.iter handle files;
@@ -210,7 +210,10 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
(** Running the LSP server. *)
let lsp_server_cmd : Config.t -> bool -> string -> unit =
fun cfg standard_lsp lsp_log_file ->
- let run _ = Config.init cfg; Lsp.Lp_lsp.main standard_lsp lsp_log_file in
+ let run _ =
+ Config.init cfg;
+ Common.Mode.lsp_mod := true ;
+ Lsp.Lp_lsp.main standard_lsp lsp_log_file in
Error.handle_exceptions run
(** Printing a decision tree. *)
diff --git a/src/common/mode.ml b/src/common/mode.ml
new file mode 100644
index 000000000..54ddbcb96
--- /dev/null
+++ b/src/common/mode.ml
@@ -0,0 +1,4 @@
+(** [lsp_mod] indicates whether we are executing the LSP server.
+ Constants and rules are indexed automatically only in LSP mode
+ and not in check mode *)
+let lsp_mod = Stdlib.ref false
diff --git a/src/common/pos.ml b/src/common/pos.ml
index 00dc0f989..0c11ec816 100644
--- a/src/common/pos.ml
+++ b/src/common/pos.ml
@@ -140,35 +140,44 @@ let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =
let make_pos : Lexing.position * Lexing.position -> 'a -> 'a loc =
fun lps elt -> in_pos (locate lps) elt
-(** [print_file_contents escape sep delimiters pos] prints the contents of the
- file at position [pos]. [sep] is the separator replacing each newline
+(** [print_file_contents parse_file escape sep delimiters pos] prints the
+ contents of the file at position [pos]. The [parse_file] function
+ takes in input [pos.fname] (that in reality may be a filename or
+ a URI, e.g. when the text comes from LSP) and it returns both a stream
+ of lines provided by a function that raises End_of_file if the file
+ content is terminated, and a function to close the resources when
+ we are done with the stream.
+ [sep] is the separator replacing each newline
(e.g. " \n"). [delimiters] is a pair of delimiters used to wrap the
"unknown location" message returned when the position does not refer to a
file. [escape] is used to escape the file contents.
The value -1 for end_col is to be interpreted as "at the end of line". *)
let print_file_contents :
- escape:(string -> string) ->
+ parse_file:(string -> (unit -> string) * (unit -> unit)) ->
+ escape:(string -> string) ->
delimiters:(string*string) -> complain_if_location_unknown:bool ->
popt Lplib.Base.pp =
- fun ~escape ~delimiters:(db,de) ~complain_if_location_unknown ppf pos ->
+ fun ~parse_file ~escape ~delimiters:(db,de) ~complain_if_location_unknown
+ ppf pos ->
match pos with
| Some { fname=Some fname; start_line; start_col; end_line; end_col } ->
(* WARNING: do not try to understand the following code!
It's dangerous for your health! *)
- (* ignore the lines before the start_line *)
- let ch = open_in fname in
+ let input_line,finish = parse_file fname in
let out =
Buffer.create
((end_line - start_line) * 80 +
(if end_col = -1 then 80 else end_col) + 1) in
+
+ (* ignore the lines before the start_line *)
for i = 0 to start_line - 2 do
- ignore (input_line ch)
+ ignore (input_line ())
done ;
(* skip the first start_col UTF8 codepoints of the start_line *)
- let startl = input_line ch in
+ let startl = input_line () in
assert (String.is_valid_utf_8 startl);
let bytepos = ref 0 in
for i = 0 to start_col - 1 do
@@ -188,7 +197,7 @@ let print_file_contents :
(* add the lines in between the start_line and the end_line *)
for i = 0 to end_line - start_line - 2 do
- Buffer.add_string out (escape (input_line ch)) ;
+ Buffer.add_string out (escape (input_line ())) ;
Buffer.add_string out "\n"
done ;
@@ -199,7 +208,7 @@ let print_file_contents :
startstr, -1
else
startstr, end_col - start_col
- else input_line ch, end_col in
+ else input_line (), end_col in
(* keep the first end_col UTF8 codepoints of the end_line *)
assert (String.is_valid_utf_8 endl);
@@ -217,7 +226,7 @@ let print_file_contents :
let str = String.sub endl 0 !bytepos in
Buffer.add_string out (escape str) ;
- close_in ch ;
+ finish () ;
string ppf (Buffer.contents out)
| None | Some {fname=None} ->
if complain_if_location_unknown then
diff --git a/src/core/sign.ml b/src/core/sign.ml
index 9f36eb147..2889d8918 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -219,6 +219,9 @@ let unlink : t -> unit = fun sign ->
let f s cps = unlink_sym s; List.iter unlink_cp_pos cps in
SymMap.iter f !(sign.sign_cp_pos)
+let add_symbol_callback = Stdlib.ref (fun _ -> ())
+let add_rules_callback = Stdlib.ref (fun _ _ -> ())
+
(** [add_symbol sign expo prop mstrat opaq name pos typ impl notation] adds in
the signature [sign] a symbol with name [name], exposition [expo],
property [prop], matching strategy [strat], opacity [opaq], type [typ],
@@ -233,6 +236,7 @@ let add_symbol : t -> expo -> prop -> match_strat -> bool -> strloc ->
(cleanup typ) (minimize_impl impl)
in
sign.sign_symbols := StrMap.add name.elt sym !(sign.sign_symbols);
+ if Stdlib.(!Common.Mode.lsp_mod) then Stdlib.(!add_symbol_callback sym) ;
sym
(** [strip_private sign] removes private symbols from signature [sign]. *)
@@ -340,7 +344,8 @@ let add_rules : t -> sym -> rule list -> unit = fun sign sym rs ->
| Some(rs',n) -> Some(rs'@rs,n)
in
let sm = StrMap.update sym.sym_name f sm in
- sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps)
+ sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps) ;
+ if Stdlib.(!Common.Mode.lsp_mod) then Stdlib.(!add_rules_callback sym rs)
(** [add_rule sign sym r] adds the new rule [r] to the symbol [sym]. When the
rule does not correspond to a symbol of signature [sign], it is stored in
diff --git a/src/handle/compile.ml b/src/handle/compile.ml
index 79706c6cd..d43a6fce3 100644
--- a/src/handle/compile.ml
+++ b/src/handle/compile.ml
@@ -79,6 +79,7 @@ let rec compile_with :
we need to explicitly update the decision tree of their symbols
because it is not done in linking which normally follows loading. *)
Ghost.iter (fun s -> Tree.update_dtree s []);
+ if Stdlib.(!Common.Mode.lsp_mod) then Tool.Indexing.index_sign sign ;
sign
end
diff --git a/src/pure/dune b/src/pure/dune
index 82aca4a9a..dce63ea6e 100644
--- a/src/pure/dune
+++ b/src/pure/dune
@@ -2,5 +2,5 @@
(name pure)
(public_name lambdapi.pure)
(modules :standard)
- (libraries camlp-streams lambdapi.handle lambdapi.core)
+ (libraries camlp-streams lambdapi.handle lambdapi.core lambdapi.tool)
(flags -w +3))
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index e8876593a..474dd506b 100644
--- a/src/pure/pure.ml
+++ b/src/pure/pure.ml
@@ -62,6 +62,7 @@ type state = Time.t * Sig_state.t
let parse_text :
fname:string -> string -> Command.t list * (Pos.pos * string) option =
fun ~fname s ->
+ Stdlib.(Tool.Indexing.lsp_input := (fname,s)) ;
let parse_string =
if Filename.check_suffix fname dk_src_extension then
Parser.Dk.parse_string
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 563994114..ec4982a32 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -1,5 +1,8 @@
open Core open Term
open Common open Pos
+open Timed
+
+let lsp_input = Stdlib.ref ("","")
type sym_name = Common.Path.t * string
@@ -306,12 +309,12 @@ module DB = struct
(* disk persistence *)
- let the_dbpath : string ref = ref Path.default_dbpath
+ let the_dbpath : string Stdlib.ref = Stdlib.ref Path.default_dbpath
- let rwpaths = ref []
+ let rwpaths = Stdlib.ref []
let restore_from_disk () =
- try restore_from ~filename:!the_dbpath
+ try restore_from ~filename:Stdlib.(!the_dbpath)
with Sys_error msg ->
Common.Error.wrn None "%s.\n\
Type \"lambdapi index --help\" to learn how to create the index." msg ;
@@ -323,6 +326,12 @@ module DB = struct
(item * position list) Index.db) Lazy.t ref =
ref (lazy (restore_from_disk ()))
+ let preserving_index f x =
+ let saved_db = !db in
+ let res = f x in
+ db := saved_db ;
+ res
+
let empty () = db := lazy (Sym_nameMap.empty,Index.empty)
let insert k v =
@@ -436,6 +445,22 @@ module DB = struct
pp_inside inside pp_side side))
sep
+ (* given a filename/URI it returns the stream of lines
+ and a function to close the resources *)
+ let parse_file fname =
+ if String.starts_with ~prefix:"file:///" fname then
+ (assert (fst Stdlib.(!lsp_input) = fname) ;
+ let text = snd Stdlib.(!lsp_input) in
+ let lines = ref (String.split_on_char '\n' text) in
+ (fun () ->
+ match !lines with
+ | [] -> raise End_of_file
+ | he::tl -> lines := tl ; he),
+ (fun () -> ()))
+ else
+ let ch = open_in fname in
+ (fun () -> input_line ch), (fun () -> close_in ch)
+
let generic_pp_of_item_list ~escape ~escaper ~separator ~sep ~delimiters
~lis:(lisb,lise) ~pres:(preb,pree)
~bold:(boldb,bolde) ~code:(codeb,codee) fmt l
@@ -451,7 +476,7 @@ module DB = struct
(popt_to_string ~print_dirname:false pos)
separator (generic_pp_of_position_list ~escaper ~sep) positions
separator preb codeb
- (Common.Pos.print_file_contents ~escape ~delimiters
+ (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
~complain_if_location_unknown:true) pos
separator
(fun ppf opt ->
@@ -460,7 +485,7 @@ module DB = struct
| Some sourceid ->
Lplib.Base.string ppf ("Translated to " ^ sourceid)) sourceid
separator
- (Common.Pos.print_file_contents ~escape ~delimiters
+ (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
~complain_if_location_unknown:false) sourcepos
codee pree lise)
"" fmt l
@@ -535,7 +560,7 @@ let load_meta_rules () =
match elt with
Parsing.Syntax.P_rules r -> rules := List.rev_append r !rules
| _ -> ())
- cmdstream) !DB.rwpaths ;
+ cmdstream) Stdlib.(!DB.rwpaths) ;
let rules = List.rev !rules in
let handle_rule map r =
let (s,r) = check_rule r in
@@ -670,6 +695,12 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
let rhs = rule.rhs in
let get_inside = function | DB.Conclusion ins -> ins | _ -> assert false in
let filename = Option.get rule_pos.fname in
+ let filename =
+ if String.starts_with ~prefix:"file:///" filename then
+ let n = String.length "file://" in
+ String.sub filename n (String.length filename - n)
+ else
+ filename in
let path = Library.path_of_file Parsing.LpLexer.escape filename in
let rule_name = (path,Common.Pos.to_string ~print_fname:false rule_pos) in
index_term_and_subterms ~is_spine:false lhs
@@ -677,6 +708,10 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
index_term_and_subterms ~is_spine:false rhs
(fun where -> ((rule_name,Some rule_pos),[Xhs(get_inside where,Rhs)]))
+let _ =
+ Stdlib.(Core.Sign.add_rules_callback :=
+ fun sym rules -> List.iter (index_rule sym) rules)
+
let index_sym sym =
let qname = name_of_sym sym in
(* Name *)
@@ -695,8 +730,10 @@ let index_sym sym =
(* Rules *)
List.iter (index_rule sym) Timed.(!(sym.Core.Term.sym_rules))
+let _ = Stdlib.(Core.Sign.add_symbol_callback := index_sym)
+
let load_rewriting_rules rwrules =
- DB.rwpaths := rwrules
+ Stdlib.(DB.rwpaths := rwrules)
let index_sign sign =
(*Console.set_flag "print_domains" true ;
@@ -833,13 +870,13 @@ module UserLevelQueries = struct
fail (Format.asprintf "Error: %s@." (Printexc.to_string exn))
let search_cmd_html ss ~from ~how_many s ~dbpath =
- the_dbpath := dbpath;
+ Stdlib.(the_dbpath := dbpath);
search_cmd_gen ss ~from ~how_many
~fail:(fun x -> "" ^ x ^ "")
~pp_results:(html_of_results_list from) ~title_tag:("
","
") s
let search_cmd_txt ss s ~dbpath =
- the_dbpath := dbpath;
+ Stdlib.(the_dbpath := dbpath);
search_cmd_gen ss ~from:0 ~how_many:999999
~fail:(fun x -> Common.Error.fatal_no_pos "%s" x)
~pp_results:pp_results_list ~title_tag:("","") s
diff --git a/src/tool/indexing.mli b/src/tool/indexing.mli
index 62b1937b4..60aca95ba 100644
--- a/src/tool/indexing.mli
+++ b/src/tool/indexing.mli
@@ -8,6 +8,11 @@ val parse_source_map : string -> unit (* the name of the file *)
val deindex_path : string -> unit
val dump : dbpath:string -> unit -> unit
+val preserving_index : ('a -> 'b) -> 'a -> 'b
+
+(* set by lsp; used to print the query results *)
+val lsp_input : ((*uri*)string * (*text*)string) ref
+
(* search command used by cli *)
val search_cmd_txt: Sig_state.sig_state -> string -> dbpath:string -> string
From 60f9e017a00ea5b50a96a5b71ba099abccc3c419 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 16:53:14 +0200
Subject: [PATCH 14/58] Websearch switched to rocq{Lexer,Parser}
- doc and welcome page of websearch to be updated with the new syntax
- in "lambdapi search" and VScode -> and forall cannot be used any more
- the new syntax allows all the LP syntax plus:
t ::= ... | forall binders, t | exists binders, t | fun binders => t
| t -> t
- the binders used in the new entries allow also "x ... z : t" that is
currently rejected by LP (but it is allowed in Coq)
TODO: but for exists, all the Coq's stdlib notations are NOT in place
(e.g. arithmetic/logic connectives, numbers, ...). How should we add them?
Maybe one possible path is to have "special" notation files that can be fed
to websearch when it starts. As for rewriting rules for normalization, the
notation files are supposed to add notation to symbols that have NOT been
put in the environment. It may be feasible: the file that calls Pratter
already uses our find_sym to resolve symbols!
---
src/parsing/dune | 2 +
src/parsing/parser.ml | 95 ++++++++-----
src/parsing/rocqLexer.ml | 227 +++++++++++++++++++++++++++++++
src/parsing/rocqParser.mly | 269 +++++++++++++++++++++++++++++++++++++
src/tool/indexing.ml | 4 +-
5 files changed, 562 insertions(+), 35 deletions(-)
create mode 100644 src/parsing/rocqLexer.ml
create mode 100644 src/parsing/rocqParser.mly
diff --git a/src/parsing/dune b/src/parsing/dune
index dbd73fc61..81a91d7a1 100644
--- a/src/parsing/dune
+++ b/src/parsing/dune
@@ -8,6 +8,8 @@
(menhir (flags --explain --external-tokens LpLexer) (modules lpParser))
+(menhir (flags --explain --external-tokens RocqLexer) (modules rocqParser))
+
(ocamllex dkLexer)
(menhir (flags --explain --external-tokens DkTokens) (modules dkParser))
diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml
index bc4824fb6..30ff1abad 100644
--- a/src/parsing/parser.ml
+++ b/src/parsing/parser.ml
@@ -29,39 +29,15 @@ module type PARSER = sig
which comes from file [f] ([f] can be anything). *)
end
-module Lp :
-sig
- include PARSER
-
- val parse_term : in_channel -> Syntax.p_term Stream.t
- (** [parse inchan] returns a stream of terms parsed from
- channel [inchan]. Terms are parsed lazily and the channel is
- closed once all entries are parsed. *)
-
- val parse_term_file : string -> Syntax.p_term Stream.t
- (** [parse_file fname] returns a stream of parsed terms of file
- [fname]. Terms are parsed lazily. *)
-
- val parse_term_string : string -> string -> Syntax.p_term Stream.t
- (** [parse_term_string f s] returns a stream of parsed terms from string [s]
- which comes from file [f] ([f] can be anything). *)
-
- val parse_rwpatt_string : string -> string -> Syntax.p_rw_patt Stream.t
- (** [parse_rwpatt_string f s] returns a stream of parsed rewrite pattern
- specifications from string [s] which comes from file [f] ([f] can be
- anything). *)
-
- val parse_search_query_string :
- string -> string -> SearchQuerySyntax.query Stream.t
- (** [parse_search_query_string f s] returns a stream of parsed terms from
- string [s] which comes from file [f] ([f] can be anything). *)
-
- val parse_qid : string -> Core.Term.qident
- end
-= struct
-
+module Aux(Lexer :
+ sig
+ type token
+ val get_token :
+ Sedlexing.lexbuf -> unit -> token * Lexing.position * Lexing.position
+ end) =
+struct
let stream_of_lexbuf :
- grammar_entry:(LpLexer.token,'b) MenhirLib.Convert.traditional ->
+ grammar_entry:(Lexer.token,'b) MenhirLib.Convert.traditional ->
?inchan:in_channel -> ?fname:string -> Sedlexing.lexbuf ->
(* Input channel passed as parameter to be closed at the end of stream. *)
'a Stream.t =
@@ -71,7 +47,7 @@ sig
MenhirLib.Convert.Simplified.traditional2revised
grammar_entry
in
- let token = LpLexer.token lb in
+ let token = Lexer.get_token lb in
let generator _ =
try Some(parse token)
with
@@ -97,6 +73,41 @@ sig
let parse_string ~grammar_entry fname s =
stream_of_lexbuf ~grammar_entry ~fname (Sedlexing.Utf8.from_string s)
+end
+
+module Lp :
+sig
+ include PARSER
+
+ val parse_term : in_channel -> Syntax.p_term Stream.t
+ (** [parse inchan] returns a stream of terms parsed from
+ channel [inchan]. Terms are parsed lazily and the channel is
+ closed once all entries are parsed. *)
+
+ val parse_term_file : string -> Syntax.p_term Stream.t
+ (** [parse_file fname] returns a stream of parsed terms of file
+ [fname]. Terms are parsed lazily. *)
+
+ val parse_term_string : string -> string -> Syntax.p_term Stream.t
+ (** [parse_term_string f s] returns a stream of parsed terms from string [s]
+ which comes from file [f] ([f] can be anything). *)
+
+ val parse_rwpatt_string : string -> string -> Syntax.p_rw_patt Stream.t
+ (** [parse_rwpatt_string f s] returns a stream of parsed rewrite pattern
+ specifications from string [s] which comes from file [f] ([f] can be
+ anything). *)
+
+ val parse_search_query_string :
+ string -> string -> SearchQuerySyntax.query Stream.t
+ (** [parse_search_query_string f s] returns a stream of parsed terms from
+ string [s] which comes from file [f] ([f] can be anything). *)
+
+ val parse_qid : string -> Core.Term.qident
+ end
+= struct
+ include Aux(struct type token = LpLexer.token
+ let get_token = LpLexer.token end)
+
let parse_term = parse ~grammar_entry:LpParser.term_alone
let parse_term_string = parse_string ~grammar_entry:LpParser.term_alone
let parse_rwpatt_string =
@@ -115,6 +126,24 @@ sig
end
+module Rocq :
+sig
+ val parse_search_query_string :
+ string -> string -> SearchQuerySyntax.query Stream.t
+ (** [parse_search_query_string f s] returns a stream of parsed terms from
+ string [s] which comes from file [f] ([f] can be anything). *)
+end
+= struct
+ include Aux(struct type token = RocqLexer.token
+ let get_token = RocqLexer.token end)
+
+ let parse_string ~grammar_entry fname s =
+ stream_of_lexbuf ~grammar_entry ~fname (Sedlexing.Utf8.from_string s)
+
+ let parse_search_query_string =
+ parse_string ~grammar_entry:RocqParser.search_query_alone
+end
+
(** Parsing dk syntax. *)
module Dk : PARSER = struct
diff --git a/src/parsing/rocqLexer.ml b/src/parsing/rocqLexer.ml
new file mode 100644
index 000000000..6f0b2537e
--- /dev/null
+++ b/src/parsing/rocqLexer.ml
@@ -0,0 +1,227 @@
+(** Lexer for Lambdapi syntax, using Sedlex, a Utf8 lexer generator. *)
+
+open Lplib
+open Sedlexing
+open Common open Pos
+
+let remove_first : Sedlexing.lexbuf -> string = fun lb ->
+ Utf8.sub_lexeme lb 1 (lexeme_length lb - 1)
+
+let remove_last : Sedlexing.lexbuf -> string = fun lb ->
+ Utf8.sub_lexeme lb 0 (lexeme_length lb - 1)
+
+let remove_ends : Sedlexing.lexbuf -> string = fun lb ->
+ Utf8.sub_lexeme lb 1 (lexeme_length lb - 2)
+
+exception SyntaxError of strloc
+
+let syntax_error : Lexing.position * Lexing.position -> string -> 'a =
+ fun pos msg -> raise (SyntaxError (Pos.make_pos pos msg))
+
+let fail : Sedlexing.lexbuf -> string -> 'a = fun lb msg ->
+ syntax_error (Sedlexing.lexing_positions lb) msg
+
+let invalid_character : Sedlexing.lexbuf -> 'a = fun lb ->
+ fail lb "Invalid character"
+
+(** Tokens. *)
+type token =
+ (* end of file *)
+ | EOF
+
+ (* keywords in alphabetical order *)
+ | GENERALIZE
+ | IN
+ | LET
+ | RULE
+ | TYPE_QUERY
+ | TYPE_TERM
+
+ (* other tokens *)
+ | INT of string
+ | STRINGLIT of string
+
+ (* symbols *)
+ | ARROW
+ | ASSIGN
+ | BACKQUOTE
+ | COMMA
+ | COLON
+ | DOT
+ | EXISTS
+ | FORALL
+ | FUN
+ | LAMBDA
+ | L_PAREN
+ | L_SQ_BRACKET
+ | PI
+ | R_PAREN
+ | R_SQ_BRACKET
+ | SEMICOLON
+ | THICKARROW
+ | UNDERSCORE
+ | VBAR
+
+ (* identifiers *)
+ | UID of string
+ | UID_EXPL of string
+ | UID_META of int
+ | UID_PATT of string
+ | QID of Path.t (* in reverse order *)
+ | QID_EXPL of Path.t (* in reverse order *)
+
+(** Some regexp definitions. *)
+let space = [%sedlex.regexp? Chars " \t\n\r"]
+let digit = [%sedlex.regexp? '0' .. '9']
+let nat = [%sedlex.regexp? Plus digit]
+let int = [%sedlex.regexp? nat | '-', nat]
+let float = [%sedlex.regexp? int, '.', Plus digit]
+let oneline_comment = [%sedlex.regexp? "//", Star (Compl ('\n' | '\r'))]
+let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
+
+(** Identifiers.
+
+ There are two kinds of identifiers: regular identifiers and escaped
+ identifiers of the form ["{|...|}"].
+
+ Modulo those surrounding brackets, escaped identifiers allow to use as
+ identifiers keywords or filenames that are not regular identifiers.
+
+ An escaped identifier denoting a filename or directory is unescaped before
+ accessing to it. Hence, the module ["{|a b|}"] refers to the file ["a b"].
+
+ Identifiers need to be normalized so that an escaped identifier, once
+ unescaped, is not regular. To this end, every identifier of the form
+ ["{|s|}"] with s regular, is understood as ["s"] (function
+ [remove_useless_escape] below).
+
+ Finally, identifiers must not be empty, so that we can use the empty string
+ for the path of ghost signatures. *)
+
+(** Unqualified regular identifiers are any non-empty sequence of characters
+ not among: *)
+let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|/"]
+let regid = [%sedlex.regexp? '/' | Plus (Compl forbidden_letter)]
+
+let is_regid : string -> bool = fun s ->
+ let lb = Utf8.from_string s in
+ match%sedlex lb with
+ | regid, eof -> true
+ | _ -> false
+
+(** Unqualified escaped identifiers are any non-empty sequence of characters
+ (except "|}") between "{|" and "|}". *)
+let notbars = [%sedlex.regexp? Star (Compl '|')]
+let escid = [%sedlex.regexp?
+ "{|", notbars, '|', Star ('|' | Compl (Chars "|}"), notbars, '|'), '}']
+
+(** [escape s] converts a string [s] into an escaped identifier if it is not
+ regular. We do not check whether [s] contains ["|}"]. FIXME? *)
+let escape s = if is_regid s then s else Escape.escape s
+
+(** [remove_useless_escape s] replaces escaped regular identifiers by their
+ unescape form. *)
+let remove_useless_escape : string -> string = fun s ->
+ let s' = Escape.unescape s in if is_regid s' then s' else s
+
+(** Lexer. *)
+let rec token lb =
+ match%sedlex lb with
+
+ (* end of file *)
+ | eof -> EOF
+
+ (* spaces *)
+ | space -> token lb
+
+ (* comments *)
+ | oneline_comment -> token lb
+ | "/*" -> comment token 0 lb
+
+ (* keywords *)
+ | "exists" -> EXISTS (* in Coq *)
+ | "forall" -> FORALL (* in Coq *)
+ | "fun" -> FUN (* in Coq *)
+ | "generalize" -> GENERALIZE
+ | "in" -> IN
+ | "let" -> LET
+ | "rule" -> RULE
+ | "type" -> TYPE_QUERY
+ | "TYPE" -> TYPE_TERM
+
+ (* other tokens *)
+ | int -> INT(Utf8.lexeme lb)
+ | string -> STRINGLIT(Utf8.sub_lexeme lb 1 (lexeme_length lb - 2))
+
+ (* symbols *)
+ | 0x2254 (* ≔ *) -> ASSIGN
+ | 0x2192 (* → *) -> ARROW (* not in Coq! *)
+ | "->" -> ARROW (* in Coq *)
+ | "=>" -> THICKARROW (* in Coq *)
+ | '`' -> BACKQUOTE
+ | ',' -> COMMA
+ | ':' -> COLON
+ | '.' -> DOT
+ | 0x03bb (* λ *) -> LAMBDA (* not in Coq! *)
+ | '(' -> L_PAREN
+ | '[' -> L_SQ_BRACKET
+ | 0x03a0 (* Π *) -> PI
+ | ')' -> R_PAREN
+ | ']' -> R_SQ_BRACKET
+ | ';' -> SEMICOLON
+ | '|' -> VBAR
+ | '_' -> UNDERSCORE
+
+ (* identifiers *)
+ | regid -> UID(Utf8.lexeme lb)
+ | escid -> UID(remove_useless_escape(Utf8.lexeme lb))
+ | '@', regid -> UID_EXPL(remove_first lb)
+ | '@', escid -> UID_EXPL(remove_useless_escape(remove_first lb))
+ | '?', nat -> UID_META(int_of_string(remove_first lb))
+ | '$', regid -> UID_PATT(remove_first lb)
+ | '$', escid -> UID_PATT(remove_useless_escape(remove_first lb))
+ | '$', nat -> UID_PATT(remove_first lb)
+
+ | regid, '.' -> qid false [remove_last lb] lb
+ | escid, '.' -> qid false [remove_useless_escape(remove_last lb)] lb
+ | '@', regid, '.' -> qid true [remove_ends lb] lb
+ | '@', escid, '.' -> qid true [remove_useless_escape(remove_ends lb)] lb
+
+ (* invalid character *)
+ | _ -> invalid_character lb
+
+and qid expl ids lb =
+ match%sedlex lb with
+ | oneline_comment -> qid expl ids lb
+ | "/*" -> comment (qid expl ids) 0 lb
+ | regid, '.' -> qid expl (remove_last lb :: ids) lb
+ | escid, '.' -> qid expl (remove_useless_escape(remove_last lb) :: ids) lb
+ | regid ->
+ if expl then QID_EXPL(Utf8.lexeme lb :: ids)
+ else QID(Utf8.lexeme lb :: ids)
+ | escid ->
+ if expl then QID_EXPL(remove_useless_escape (Utf8.lexeme lb) :: ids)
+ else QID(remove_useless_escape (Utf8.lexeme lb) :: ids)
+ | _ ->
+ fail lb ("Invalid identifier: \""
+ ^ String.concat "." (List.rev (Utf8.lexeme lb :: ids)) ^ "\".")
+
+and comment next i lb =
+ match%sedlex lb with
+ | eof -> fail lb "Unterminated comment."
+ | "*/" -> if i=0 then next lb else comment next (i-1) lb
+ | "/*" -> comment next (i+1) lb
+ | any -> comment next i lb
+ | _ -> invalid_character lb
+
+(** [token buf] is a lexing function on buffer [buf] that can be passed to
+ a parser. *)
+let token : lexbuf -> unit -> token * Lexing.position * Lexing.position =
+ fun lb () -> try with_tokenizer token lb () with
+ | Sedlexing.MalFormed -> fail lb "Not Utf8 encoded file"
+ | Sedlexing.InvalidCodepoint k ->
+ fail lb ("Invalid Utf8 code point " ^ string_of_int k)
+
+let token =
+ let r = ref (EOF, Lexing.dummy_pos, Lexing.dummy_pos) in fun lb () ->
+ Debug.(record_time Lexing (fun () -> r := token lb ())); !r
diff --git a/src/parsing/rocqParser.mly b/src/parsing/rocqParser.mly
new file mode 100644
index 000000000..4b0524ad7
--- /dev/null
+++ b/src/parsing/rocqParser.mly
@@ -0,0 +1,269 @@
+(** Lambdapi parser, using the parser generator Menhir. *)
+
+%{
+ open Lplib
+ open Common open Pos
+ open Syntax
+ open Core
+
+ let qid_of_path lps = function
+ | [] -> assert false
+ | id::mp -> make_pos lps (List.rev mp, id)
+
+ let make_abst startpos ps t endpos =
+ if ps = [] then t else make_pos (startpos,endpos) (P_Abst(ps,t))
+
+ let make_prod startpos ps t endpos =
+ if ps = [] then t else make_pos (startpos,endpos) (P_Prod(ps,t))
+
+ exception Error
+%}
+
+
+// end of file
+
+%token EOF
+
+// keywords in alphabetical order
+
+%token GENERALIZE
+%token IN
+%token LET
+%token RULE
+%token TYPE_QUERY
+%token TYPE_TERM
+
+// other tokens
+
+%token INT
+%token STRINGLIT
+
+// symbols
+
+%token ARROW
+%token ASSIGN
+%token BACKQUOTE
+%token COMMA
+%token COLON
+%token DOT
+%token EXISTS
+%token FORALL
+%token FUN
+%token LAMBDA
+%token L_PAREN
+%token L_SQ_BRACKET
+%token PI
+%token R_PAREN
+%token R_SQ_BRACKET
+%token SEMICOLON
+%token THICKARROW
+%token UNDERSCORE
+%token VBAR
+
+// identifiers
+
+%token UID
+%token UID_EXPL
+%token UID_META
+%token UID_PATT
+%token QID
+%token QID_EXPL
+
+// types
+
+%start search_query_alone
+
+%%
+
+search_query_alone:
+ | q=search_query EOF
+ { q }
+
+uid: s=UID { make_pos $sloc s}
+
+param_list:
+ | x=param { ([x], None, false) }
+ | L_PAREN xs=param+ COLON a=term R_PAREN { (xs, Some(a), false) }
+ | L_SQ_BRACKET xs=param+ a=preceded(COLON, term)? R_SQ_BRACKET
+ { (xs, a, true) }
+
+fun_param_list:
+ | x=param { ([x], None, false) }
+ | L_PAREN xs=param+ COLON a=term R_PAREN { (xs, Some(a), false) }
+
+param:
+ | s=uid { Some s }
+ | UNDERSCORE { None }
+
+term:
+ | t=bterm { t }
+ | t=saterm { t }
+ | t=saterm u=bterm { make_pos $sloc (P_Appl(t,u)) }
+ | t=saterm ARROW u=term { make_pos $sloc (P_Arro(t, u)) }
+
+bterm:
+ | BACKQUOTE q=term_id b=binder
+ { let b = make_pos $loc(b) (P_Abst(fst b, snd b)) in
+ make_pos $sloc (P_Appl(q, b)) }
+ | EXISTS b=rocqbinder(COMMA)
+ { {(List.fold_right
+ (fun bin res ->
+ Pos.none (P_Appl(
+ Pos.none (P_Iden(Pos.none ([],"∃"), false)),
+ Pos.none (P_Abst([bin], res)))))
+ (fst b)
+ (snd b))
+ with pos = Some (Pos.locate $sloc) }
+ } (* in Coq *)
+ | FORALL b=rocqbinder(COMMA)
+ { make_pos $sloc (P_Prod(fst b, snd b)) } (* in Coq *)
+ | PI b=binder
+ { make_pos $sloc (P_Prod(fst b, snd b)) } (* not in Coq! *)
+ | LAMBDA b=binder
+ { make_pos $sloc (P_Abst(fst b, snd b)) } (* not in Coq! *)
+ | FUN b=rocqbinder(THICKARROW)
+ { make_pos $sloc (P_Abst(fst b, snd b)) } (* in Coq *)
+ | LET x=uid a=param_list* b=preceded(COLON, term)? ASSIGN t=term IN u=term
+ { make_pos $sloc (P_LLet(x, a, b, t, u)) }
+
+saterm:
+ | t=saterm u=aterm { make_pos $sloc (P_Appl(t,u)) }
+ | t=aterm { t }
+
+aterm:
+ | ti=term_id { ti }
+ | UNDERSCORE { make_pos $sloc P_Wild }
+ | TYPE_TERM { make_pos $sloc P_Type }
+ | s=UID_META ts=env?
+ { let i = make_pos $loc(s) s
+ and ts = match ts with None -> [||] | Some ts -> Array.of_list ts in
+ make_pos $sloc (P_Meta(i,ts)) }
+ | s=UID_PATT e=env?
+ { let i = if s = "_" then None else Some(make_pos $loc(s) s) in
+ make_pos $sloc (P_Patt(i, Option.map Array.of_list e)) }
+ | L_PAREN t=term R_PAREN { make_pos $sloc (P_Wrap(t)) }
+ | L_SQ_BRACKET t=term R_SQ_BRACKET { make_pos $sloc (P_Expl(t)) }
+ | n=INT { make_pos $sloc (P_NLit n) }
+ | s=STRINGLIT { make_pos $sloc (P_SLit s) }
+
+env: DOT L_SQ_BRACKET ts=separated_list(SEMICOLON, term) R_SQ_BRACKET { ts }
+
+term_id:
+ | i=qid { make_pos $sloc (P_Iden(i, false)) }
+ | i=qid_expl { make_pos $sloc (P_Iden(i, true)) }
+
+qid:
+ | s=UID { make_pos $sloc ([], s) }
+ | p=QID { qid_of_path $sloc p }
+
+qid_expl:
+ | s=UID_EXPL { make_pos $sloc ([], s) }
+ | p=QID_EXPL { qid_of_path $sloc p }
+
+binder:
+ | ps=param_list+ COMMA t=term { (ps, t) }
+ | p=param COLON a=term COMMA t=term { ([[p], Some a, false], t) }
+
+rocqbinder(terminator):
+ | ps=fun_param_list+ a=preceded(COLON, term)? terminator t=term
+ { if a = None then
+ (ps, t)
+ else if List.for_all (fun (_,typ,_) -> typ = None) ps then
+ (List.map (fun (v,_,b) -> v,a,b) ps, t)
+ else
+ raise Error
+ }
+
+maybe_generalize:
+ | g = GENERALIZE?
+ { g <> None }
+
+where:
+ | u = UID g=maybe_generalize
+ { g, match u with
+ | "=" -> Some SearchQuerySyntax.Exact
+ | ">" -> Some SearchQuerySyntax.Inside
+ | "≥"
+ | ">=" -> None
+ | _ ->
+ LpLexer.syntax_error $sloc
+ "Only \">\", \"=\", \"≥\" and \">=\" accepted"
+ }
+
+asearch_query:
+ (* "type" is a keyword... *)
+ | TYPE_QUERY gw=where t=aterm
+ { let g,w = gw in
+ if w <> None then
+ LpLexer.syntax_error $sloc
+ "Only \"≥\" and \">=\" accepted for \"type\""
+ else
+ SearchQuerySyntax.QBase(QSearch(t,g,Some (QType None))) }
+ | RULE gw=where t=aterm
+ { let g,w = gw in
+ SearchQuerySyntax.QBase(QSearch(t,g,Some (QXhs(w,None)))) }
+ | k=UID gw=where t=aterm
+ { let open SearchQuerySyntax in
+ let g,w = gw in
+ match k,t.elt with
+ | "name",P_Iden(id,false) ->
+ assert (fst id.elt = []) ;
+ if w <> Some Exact then
+ LpLexer.syntax_error $sloc
+ "Only \"=\" accepted for \"name\""
+ else if g = true then
+ LpLexer.syntax_error $sloc
+ "\"generalize\" cannot be used with \"name\""
+ else
+ QBase(QName (snd id.elt))
+ | "name",_ ->
+ LpLexer.syntax_error $sloc "Path prefix expected after \"name:\""
+ | "anywhere",_ ->
+ if w <> None then
+ LpLexer.syntax_error $sloc
+ "Only \"≥\" and \">=\" accepted for \"anywhere\""
+ else
+ QBase(QSearch(t,g,None))
+ | "spine",_ ->
+ QBase(QSearch(t,g,Some (QType (Some (Spine w)))))
+ | "concl",_ ->
+ QBase(QSearch(t,g,Some (QType (Some (Conclusion w)))))
+ | "hyp",_ ->
+ QBase(QSearch(t,g,Some (QType (Some (Hypothesis w)))))
+ | "lhs",_ ->
+ QBase(QSearch(t,g,Some (QXhs(w,Some Lhs))))
+ | "rhs",_ ->
+ QBase(QSearch(t,g,Some (QXhs(w,Some Rhs))))
+ | _,_ ->
+ LpLexer.syntax_error $sloc ("Unknown keyword: " ^ k)
+ }
+ | L_PAREN q=search_query R_PAREN
+ { q }
+
+csearch_query:
+ | q=asearch_query
+ { q }
+ | q1=csearch_query COMMA q2=asearch_query
+ { SearchQuerySyntax.QOpp (q1,SearchQuerySyntax.Intersect,q2) }
+
+ssearch_query:
+ | q=csearch_query
+ { q }
+ | q1=ssearch_query SEMICOLON q2=csearch_query
+ { SearchQuerySyntax.QOpp (q1,SearchQuerySyntax.Union,q2) }
+
+search_query:
+ | q=ssearch_query
+ { q }
+ | q=search_query VBAR qid=qid
+ { let p,n = qid.elt in
+ let path =
+ if p = [] then n
+ else
+ Format.asprintf "%a.%a" Core.Print.path p Core.Print.uid n in
+ SearchQuerySyntax.QFilter (q,Path path) }
+ | q=search_query VBAR s=STRINGLIT
+ { let re = Str.regexp s in
+ SearchQuerySyntax.QFilter (q,RegExp re) }
+
+%%
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index ec4982a32..d9050d9a3 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -841,9 +841,8 @@ module UserLevelQueries = struct
let search_cmd_gen ss ~from ~how_many ~fail ~pp_results
~title_tag:(hb,he) s =
- let s = transform_ascii_to_unicode s in
try
- let pstream = Parsing.Parser.Lp.parse_search_query_string "LPSearch" s in
+ let pstream = Parsing.Parser.Rocq.parse_search_query_string "LPSearch" s in
let pq = Stream.next pstream in
let mok _ = None in
let items = ItemSet.bindings (answer_query ~mok ss [] pq) in
@@ -876,6 +875,7 @@ module UserLevelQueries = struct
~pp_results:(html_of_results_list from) ~title_tag:("
","
") s
let search_cmd_txt ss s ~dbpath =
+ let s = transform_ascii_to_unicode s in
Stdlib.(the_dbpath := dbpath);
search_cmd_gen ss ~from:0 ~how_many:999999
~fail:(fun x -> Common.Error.fatal_no_pos "%s" x)
From 94b610afff1553520eb5655c4df2ccf6bec73e62 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 16:54:03 +0200
Subject: [PATCH 15/58] ...
---
TODO.md | 2 ++
1 file changed, 2 insertions(+)
diff --git a/TODO.md b/TODO.md
index 1f6123258..3b118d225 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,8 @@ TODO
Index and search
----------------
+* add notations for Coq stdlib to websearch (using Pratter?)
+
* generate mappings from LP to V automatically with HOL2DK and find
what to do with manually written files; also right now there are
mappings that are lost and mappings that are confused in a many-to-one
From cecd16f6737c9441750408cc1ef9e8635943a708 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 17:17:27 +0200
Subject: [PATCH 16/58] Updated
---
TODO.md | 65 ++++++++++++++++++++++++++++++++++++++-------------------
1 file changed, 43 insertions(+), 22 deletions(-)
diff --git a/TODO.md b/TODO.md
index 3b118d225..431f3f017 100644
--- a/TODO.md
+++ b/TODO.md
@@ -11,34 +11,46 @@ Index and search
mappings that are lost and mappings that are confused in a many-to-one
relation
-* document new features, e.g. -sources (and find better
- terminology), deindex
+* normalize queries when given as commands in lambdapi
+
+* syntactic sugar for regular expressions / way to write a regular
+ expression - only query efficiently
+ (concl = _ | "regexpr")
+
+* CLI interface: it tries to render way too many results
+ and it takes ages
-* After "Number of results: 3" there is a missing CRLF
+* after "Number of results: 3" there is a missing CRLF
* why type only supports? =
also doc is wrong, but I suppose code is wrong
-* CLI interface: it tries to render way too many results
- and it takes ages
+* check the semantics of indexing the Plac _ as variables
-* html tags in textual output :-(
+* when disambiguating an identifier, after rewriting one could be
+ left with just one id (not working now)
+
+Think about
+-----------
+
+* alignments with same name ==> automatic preference?
* would it be more reasonable to save the normalization rules
when the index is created and apply them as default when searching,
in particular when searching as a lambdapi command?
-* normalize queries when given as commands in lambdapi
+* package management
-* alignments with same name ==> automatic preference?
+* update index / deindex (it should work at package level)
-* better pagination
+* more external sources when showing query results, including Git repos
-* document require ... as Foo: using Foo.X in the query already
- works (pure magic!); of course it does not work when using
- regular expressions [ check before! ]
+* VS code integration: right now lambdapi works on the current development
+ mixed with remote, but different sets of rewriting rules would make sense;
+ should it instead only work with the current development and dispatch
+ queries via VS code to a remote websearch?
-* check the semantics of indexing the Plac _ as variables
+* ranking
Performance improvements
------------------------
@@ -49,16 +61,25 @@ Performance improvements
and THEN it filters out the justifications that have Concl Exact; maybe we
could save a lot of time anticipating the filtrage
-Misleading output
------------------
+Documentation
+-------------
-+ Too many results found?
+* document new features, e.g. -sources (and find better
+ terminology), deindex
+
+* document Coq syntax in websearch
+
+* document require ... as Foo: using Foo.X in the query already
+ works (pure magic!); of course it does not work when using
+ regular expressions [ check before! ]
-anywhere >= (Π x: _, (= _ V# V#))
-anywhere >= (Π x: _, (= _ x x))
+* Misleading output for:
-NO, it's ok, but the output is misleading. The second form is equivalent
-to the first that is equivalent to (_ -> (= _ V# V#)) that is what it is
-found. However it shows the pattern saying that " (Π x: _, (= _ x x))" was
-found, that is the misleading thing.
+ anywhere >= (Π x: _, (= _ V# V#))
+ anywhere >= (Π x: _, (= _ x x))
+ Are there too many results? NO, it's ok, but the output is misleading.
+ The second form is equivalent
+ to the first that is equivalent to (_ -> (= _ V# V#)) that is what it is
+ found. However it shows the pattern saying that " (Π x: _, (= _ x x))" was
+ found, that is the misleading thing.
From caa4f000e8d6856dc8a2aba373c8189ce9926452 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 17:36:42 +0200
Subject: [PATCH 17/58] ...
---
TODO.md | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/TODO.md b/TODO.md
index 431f3f017..7258ade19 100644
--- a/TODO.md
+++ b/TODO.md
@@ -21,9 +21,7 @@ Index and search
and it takes ages
* after "Number of results: 3" there is a missing CRLF
-
-* why type only supports? =
- also doc is wrong, but I suppose code is wrong
+* also after "Please rewrite the query ... following:"
* check the semantics of indexing the Plac _ as variables
@@ -64,6 +62,10 @@ Performance improvements
Documentation
-------------
+* fix the doc: not only "anywhere" but also "type" can be paired
+ only with ">="; maybe make it explicit that to match exactly the
+ type of a constant one should use "spine ="
+
* document new features, e.g. -sources (and find better
terminology), deindex
From 8de1444ddb7f52ad4bee653a6cbb6bc00ae0c4c4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 17:40:34 +0200
Subject: [PATCH 18/58] ...
---
TODO.md | 22 ++++++++++------------
1 file changed, 10 insertions(+), 12 deletions(-)
diff --git a/TODO.md b/TODO.md
index 7258ade19..e9ee7d9be 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,14 +4,13 @@ TODO
Index and search
----------------
-* add notations for Coq stdlib to websearch (using Pratter?)
+* after "Number of results: 3" there is a missing CRLF
+* also after "Please rewrite the query ... following:"
-* generate mappings from LP to V automatically with HOL2DK and find
- what to do with manually written files; also right now there are
- mappings that are lost and mappings that are confused in a many-to-one
- relation
+* when disambiguating an identifier, after rewriting one could be
+ left with just one id (not working now)
-* normalize queries when given as commands in lambdapi
+* add notations for Coq stdlib to websearch (using Pratter?)
* syntactic sugar for regular expressions / way to write a regular
expression - only query efficiently
@@ -20,13 +19,12 @@ Index and search
* CLI interface: it tries to render way too many results
and it takes ages
-* after "Number of results: 3" there is a missing CRLF
-* also after "Please rewrite the query ... following:"
-
-* check the semantics of indexing the Plac _ as variables
+* normalize queries when given as commands in lambdapi
-* when disambiguating an identifier, after rewriting one could be
- left with just one id (not working now)
+* generate mappings from LP to V automatically with HOL2DK and find
+ what to do with manually written files; also right now there are
+ mappings that are lost and mappings that are confused in a many-to-one
+ relation
Think about
-----------
From f8c1059da490fa265a0d0cfd9967f8ab14607cc2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 17:51:45 +0200
Subject: [PATCH 19/58] Fix missing \n
---
TODO.md | 3 ---
src/tool/indexing.ml | 6 +++---
2 files changed, 3 insertions(+), 6 deletions(-)
diff --git a/TODO.md b/TODO.md
index e9ee7d9be..ccd6b0fc2 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,9 +4,6 @@ TODO
Index and search
----------------
-* after "Number of results: 3" there is a missing CRLF
-* also after "Please rewrite the query ... following:"
-
* when disambiguating an identifier, after rewriting one could be
left with just one id (not working now)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index d9050d9a3..a38113bf6 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -849,17 +849,17 @@ module UserLevelQueries = struct
let resultsno = List.length items in
let _,items = Lplib.List.cut items from in
let items,_ = Lplib.List.cut items how_many in
- Format.asprintf "%sNumber of results: %d%s%a@."
+ Format.asprintf "%sNumber of results: %d%s@.%a@."
hb resultsno he pp_results items
with
| Stream.Failure ->
- fail (Format.asprintf "Syntax error: a query was expected")
+ fail (Format.asprintf "Syntax error: a query was expected@.")
| Common.Error.Fatal(_,msg) ->
fail (Format.asprintf "Error: %s@." msg)
| Overloaded(name,res) ->
fail (Format.asprintf
"Overloaded symbol %s. Please rewrite the query replacing %s \
- with a fully qualified identifier among the following: %a"
+ with a fully qualified identifier among the following:@.%a@."
name name pp_results (ItemSet.bindings res))
| Stack_overflow ->
fail
From d4ab72d976e0da3b4cd7c9d9f12cd54da5b0cc88 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 18:48:22 +0200
Subject: [PATCH 20/58] Search results from CLI are now printed line-by-line
(streamed)
---
TODO.md | 4 ++--
src/cli/lambdapi.ml | 4 ++--
src/handle/query.ml | 2 +-
src/tool/indexing.ml | 38 +++++++++++++++++++++-----------------
src/tool/indexing.mli | 3 ++-
5 files changed, 28 insertions(+), 23 deletions(-)
diff --git a/TODO.md b/TODO.md
index ccd6b0fc2..f4928d1fd 100644
--- a/TODO.md
+++ b/TODO.md
@@ -13,8 +13,8 @@ Index and search
expression - only query efficiently
(concl = _ | "regexpr")
-* CLI interface: it tries to render way too many results
- and it takes ages
+* CLI interface: use colors? be aware of redirections over files / more
+ / less
* normalize queries when given as commands in lambdapi
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 3606827d2..ab21f6021 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -35,8 +35,8 @@ let search_cmd cfg rules require s dbpath_opt =
Tool.Indexing.load_rewriting_rules rules ;
let ss = sig_state_of_require require in
let dbpath = Option.get Path.default_dbpath dbpath_opt in
- out Format.std_formatter "%s@."
- (Tool.Indexing.search_cmd_txt ss s ~dbpath) in
+ out Format.std_formatter "%a@."
+ (Tool.Indexing.search_cmd_txt ss ~dbpath) s in
Error.handle_exceptions run
let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
diff --git a/src/handle/query.ml b/src/handle/query.ml
index b07dc77c7..faf5dd4c4 100644
--- a/src/handle/query.ml
+++ b/src/handle/query.ml
@@ -177,7 +177,7 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
match elt with
| P_query_search s ->
let dbpath = Path.default_dbpath in
- return string (Tool.Indexing.search_cmd_txt ss s ~dbpath)
+ return (Tool.Indexing.search_cmd_txt ss ~dbpath) s
| P_query_debug(_,_)
| P_query_verbose(_)
| P_query_flag(_,_)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index a38113bf6..7b2913886 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -471,7 +471,7 @@ module DB = struct
Lplib.List.pp
(fun ppf (((p,n) as sym_name,pos),(positions : answer)) ->
let sourceid,sourcepos = source_infos_of_sym_name sym_name in
- Lplib.Base.out ppf "%s%a.%s%s%s@%s%s%a%s%s%s%a%s%a%s%a%s%s%s@."
+ Lplib.Base.out ppf "%s%a.%s%s%s@%s%s%a%s%s%s%a%s%a%s%a%s%s%s%s@."
lisb (escaper.run Core.Print.path) p boldb n bolde
(popt_to_string ~print_dirname:false pos)
separator (generic_pp_of_position_list ~escaper ~sep) positions
@@ -487,7 +487,7 @@ module DB = struct
separator
(Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
~complain_if_location_unknown:false) sourcepos
- codee pree lise)
+ codee pree lise separator)
"" fmt l
let html_of_item_list =
@@ -840,46 +840,50 @@ module UserLevelQueries = struct
Str.global_replace (Str.regexp "\\bforall\\b") "Π" s
let search_cmd_gen ss ~from ~how_many ~fail ~pp_results
- ~title_tag:(hb,he) s =
+ ~title_tag:(hb,he) fmt s =
try
let pstream = Parsing.Parser.Rocq.parse_search_query_string "LPSearch" s in
let pq = Stream.next pstream in
let mok _ = None in
- let items = ItemSet.bindings (answer_query ~mok ss [] pq) in
+ let items = answer_query ~mok ss [] pq in
+ let items = ItemSet.bindings items in
let resultsno = List.length items in
let _,items = Lplib.List.cut items from in
let items,_ = Lplib.List.cut items how_many in
- Format.asprintf "%sNumber of results: %d%s@.%a@."
+ Lplib.Base.out fmt "%sNumber of results: %d%s@.%a@."
hb resultsno he pp_results items
with
| Stream.Failure ->
- fail (Format.asprintf "Syntax error: a query was expected@.")
+ Lplib.Base.out fmt "%s"
+ (fail (Format.asprintf "Syntax error: a query was expected@."))
| Common.Error.Fatal(_,msg) ->
- fail (Format.asprintf "Error: %s@." msg)
+ Lplib.Base.out fmt "%s" (fail (Format.asprintf "Error: %s@." msg))
| Overloaded(name,res) ->
- fail (Format.asprintf
+ Lplib.Base.out fmt "%s" (fail (Format.asprintf
"Overloaded symbol %s. Please rewrite the query replacing %s \
with a fully qualified identifier among the following:@.%a@."
- name name pp_results (ItemSet.bindings res))
+ name name pp_results (ItemSet.bindings res)))
| Stack_overflow ->
- fail
+ Lplib.Base.out fmt "%s" (fail
(Format.asprintf
- "Error: too many results. Please refine your query.@." )
+ "Error: too many results. Please refine your query.@." ))
| exn ->
- fail (Format.asprintf "Error: %s@." (Printexc.to_string exn))
+ Lplib.Base.out fmt "%s"
+ (fail (Format.asprintf "Error: %s@." (Printexc.to_string exn)))
let search_cmd_html ss ~from ~how_many s ~dbpath =
Stdlib.(the_dbpath := dbpath);
- search_cmd_gen ss ~from ~how_many
- ~fail:(fun x -> "" ^ x ^ "")
- ~pp_results:(html_of_results_list from) ~title_tag:("
","
") s
+ Format.asprintf "%a"
+ (search_cmd_gen ss ~from ~how_many
+ ~fail:(fun x -> "" ^ x ^ "")
+ ~pp_results:(html_of_results_list from) ~title_tag:("
","
")) s
- let search_cmd_txt ss s ~dbpath =
+ let search_cmd_txt ss ~dbpath fmt s =
let s = transform_ascii_to_unicode s in
Stdlib.(the_dbpath := dbpath);
search_cmd_gen ss ~from:0 ~how_many:999999
~fail:(fun x -> Common.Error.fatal_no_pos "%s" x)
- ~pp_results:pp_results_list ~title_tag:("","") s
+ ~pp_results:pp_results_list ~title_tag:("","") fmt s
end
diff --git a/src/tool/indexing.mli b/src/tool/indexing.mli
index 60aca95ba..0f83152b6 100644
--- a/src/tool/indexing.mli
+++ b/src/tool/indexing.mli
@@ -14,7 +14,8 @@ val preserving_index : ('a -> 'b) -> 'a -> 'b
val lsp_input : ((*uri*)string * (*text*)string) ref
(* search command used by cli *)
-val search_cmd_txt: Sig_state.sig_state -> string -> dbpath:string -> string
+val search_cmd_txt:
+ Sig_state.sig_state -> dbpath:string -> string Lplib.Base.pp
(* search command used by websearch *)
val search_cmd_html:
From 821b2340fec1fa19655f2176678c72b3fb259cde Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 10 Jul 2025 19:13:11 +0200
Subject: [PATCH 21/58] Use colors for textual output
---
TODO.md | 3 ---
src/tool/indexing.ml | 8 ++++++--
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/TODO.md b/TODO.md
index f4928d1fd..4a637c252 100644
--- a/TODO.md
+++ b/TODO.md
@@ -13,9 +13,6 @@ Index and search
expression - only query efficiently
(concl = _ | "regexpr")
-* CLI interface: use colors? be aware of redirections over files / more
- / less
-
* normalize queries when given as commands in lambdapi
* generate mappings from LP to V automatically with HOL2DK and find
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 7b2913886..58c119143 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -496,10 +496,14 @@ module DB = struct
~lis:("
","
") ~pres:("
","
") ~bold:("","")
~code:("","")
- let pp_item_list =
+ let pp_item_list fmt l =
generic_pp_of_item_list ~escape:(fun x -> x) ~escaper:identity_escaper
~separator:"\n" ~sep:" and\n" ~delimiters:("","")
- ~lis:("* ","") ~pres:("","") ~bold:("","") ~code:("","")
+ ~lis:("* ","") ~pres:("","")
+ ~bold:(if Stdlib.(!Common.Mode.lsp_mod) || Unix.isatty Unix.stdout then
+ ("[0;36m","[0m")
+ else ("",""))
+ ~code:("","") fmt l
let pp_results_list fmt l = pp_item_list fmt l
From 20c5c68942b90c7fa3e677a8e2b40436b7273d16 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 09:21:24 +0200
Subject: [PATCH 22/58] ...
---
TODO.md | 3 +++
1 file changed, 3 insertions(+)
diff --git a/TODO.md b/TODO.md
index 4a637c252..6709a5298 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,9 @@ TODO
Index and search
----------------
+* @abdelghani include git sub-repos and automatize the generation
+ of the file to output Coq sources
+
* when disambiguating an identifier, after rewriting one could be
left with just one id (not working now)
From ef93bcae76fc512d1f0b5bbf210036aca36eca76 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 09:29:55 +0200
Subject: [PATCH 23/58] ...
---
TODO.md | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/TODO.md b/TODO.md
index 6709a5298..6214e2438 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,8 +4,9 @@ TODO
Index and search
----------------
-* @abdelghani include git sub-repos and automatize the generation
- of the file to output Coq sources
+* @abdelghani include in HOL2DK_indexing git sub-repos of
+ coq-hol-light-real-with-N and coq-hol-light
+ and automatize the generation of the file to output Coq sources
* when disambiguating an identifier, after rewriting one could be
left with just one id (not working now)
From d1efd6550acbf01c7594eb05e1eb2c543e502af0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 09:43:17 +0200
Subject: [PATCH 24/58] ...
---
TODO.md | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/TODO.md b/TODO.md
index 6214e2438..1004f42e9 100644
--- a/TODO.md
+++ b/TODO.md
@@ -8,6 +8,14 @@ Index and search
coq-hol-light-real-with-N and coq-hol-light
and automatize the generation of the file to output Coq sources
+* @abdelghani
+ - use lplib/color.ml in place of our color management of the
+ output [ but do not lose our code to check if we are
+ in lsp_mode or targeting a tty ]
+ - "Overloaded symbol prod. Please rewrite the query replacing..."
+ is printed in red but the following lines are also in red
+ (i.e. black color is not restored)
+
* when disambiguating an identifier, after rewriting one could be
left with just one id (not working now)
From 18154ae02a77689edecf5cc585341ba5de07563b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 09:56:05 +0200
Subject: [PATCH 25/58] ...
---
TODO.md | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/TODO.md b/TODO.md
index 1004f42e9..db9016258 100644
--- a/TODO.md
+++ b/TODO.md
@@ -16,6 +16,12 @@ Index and search
is printed in red but the following lines are also in red
(i.e. black color is not restored)
+* @abdelghani
+ - commit the very nice new look&feel of websearch
+ - (maybe?) allow an --add-examples=FNAME to include in the
+ generated webpage an HTML snippet (e.g. with examples or
+ additional infos for that instance)
+
* when disambiguating an identifier, after rewriting one could be
left with just one id (not working now)
From 790dc093dfdc80e4c0d257ccb21c2e6ff091f4b4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 10:09:36 +0200
Subject: [PATCH 26/58] Overloading is now detected up to normalization rules
- this basically removes ALL overloaded problems from the HOL export
- the code is written so that the two normalized symbols may be
unequal (in the sense of =) but have the same path. Maybe one should
investigate why this is necessary, but for the time being it is safe
to ignore. [ We are probably comparing a real symbol with a bogus one
or even two bogus ones that differ ]
---
TODO.md | 3 ---
src/tool/indexing.ml | 56 +++++++++++++++++++++++++++++++++-----------
2 files changed, 42 insertions(+), 17 deletions(-)
diff --git a/TODO.md b/TODO.md
index db9016258..7c14b5935 100644
--- a/TODO.md
+++ b/TODO.md
@@ -22,9 +22,6 @@ Index and search
generated webpage an HTML snippet (e.g. with examples or
additional infos for that instance)
-* when disambiguating an identifier, after rewriting one could be
- left with just one id (not working now)
-
* add notations for Coq stdlib to websearch (using Pratter?)
* syntactic sugar for regular expressions / way to write a regular
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 58c119143..1b99c7809 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -514,25 +514,51 @@ end
exception Overloaded of string * DB.answer DB.ItemSet.t
+let normalize_fun = ref (fun _ -> assert false)
+
+let mk_bogus_sym mp name pos =
+ Core.Term.create_sym mp Core.Term.Public Core.Term.Defin Core.Term.Sequen
+ false (Common.Pos.make pos name) None Core.Term.mk_Type []
+
+let elim_duplicates_up_to_normalization res =
+ let resl = DB.ItemSet.bindings res in
+ let norm =
+ List.map
+ (fun ((((mp,name),sympos),l) as inp) ->
+ let s = mk_bogus_sym mp name sympos in
+ match !normalize_fun (Core.Term.mk_Symb s) with
+ | Symb {sym_path ; sym_name ; _} ->
+ (((sym_path,sym_name),sympos), l)
+ | _ -> inp) resl in
+ let res = List.sort (fun ((x,_),_) ((y,_),_) -> compare x y) norm in
+ let res =
+ let rec uniq =
+ function
+ | [] | [_] as l -> l
+ | ((x,_),_)::(((y,_),_)::_ as l) when x=y -> uniq l
+ | i::l -> i::uniq l in
+ uniq res in
+ DB.ItemSet.of_list res
+
let find_sym ~prt ~prv sig_state ({elt=(mp,name); pos} as s) =
- let pos,mp =
- match mp with
- [] ->
- let res = DB.locate_name name in
- if DB.ItemSet.cardinal res > 1 then
- raise (Overloaded (name,res)) ;
- (match DB.ItemSet.choose_opt res with
- | None -> Common.Error.fatal pos "Unknown symbol %s." name
- | Some (((mp,_),sympos),[_,_,DB.Name]) -> sympos,mp
- | Some _ -> assert false) (* locate only returns DB.Name*)
- | _::_ -> None,mp
- in
try
Core.Sig_state.find_sym ~prt ~prv sig_state s
with
Common.Error.Fatal _ ->
- Core.Term.create_sym mp Core.Term.Public Core.Term.Defin Core.Term.Sequen
- false (Common.Pos.make pos name) None Core.Term.mk_Type []
+ let pos,mp =
+ match mp with
+ [] ->
+ let res_orig = DB.locate_name name in
+ let res = elim_duplicates_up_to_normalization res_orig in
+ if DB.ItemSet.cardinal res > 1 then
+ raise (Overloaded (name,res_orig)) ;
+ (match DB.ItemSet.choose_opt res with
+ | None -> Common.Error.fatal pos "Unknown symbol %s." name
+ | Some (((mp,_),sympos),[_,_,DB.Name]) -> sympos,mp
+ | Some _ -> assert false) (* locate only returns DB.Name*)
+ | _::_ -> None,mp
+ in
+ mk_bogus_sym mp name pos
module QNameMap =
Map.Make(struct type t = sym_name let compare = Stdlib.compare end)
@@ -585,6 +611,8 @@ let normalize typ =
with Not_found -> Core.Tree_type.empty_dtree in
Core.Eval.snf ~dtree ~tags:[`NoExpand] [] typ
+let _ = normalize_fun := normalize
+
let search_pterm ~generalize ~mok ss env pterm =
let env =
("V#",(new_var "V#",Term.mk_Type,None))::env in
From 6d0ed69e3f76a9e38576937b958c731595a1b672 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 14:51:34 +0200
Subject: [PATCH 27/58] Bug fixed: after normalization in elim duplicates the
wrong name was kept
Example: Real was no longer found because it must become R and not Real
---
src/tool/indexing.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 1b99c7809..58d291f19 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -545,7 +545,7 @@ let find_sym ~prt ~prv sig_state ({elt=(mp,name); pos} as s) =
Core.Sig_state.find_sym ~prt ~prv sig_state s
with
Common.Error.Fatal _ ->
- let pos,mp =
+ let pos,mp,name =
match mp with
[] ->
let res_orig = DB.locate_name name in
@@ -554,9 +554,9 @@ let find_sym ~prt ~prv sig_state ({elt=(mp,name); pos} as s) =
raise (Overloaded (name,res_orig)) ;
(match DB.ItemSet.choose_opt res with
| None -> Common.Error.fatal pos "Unknown symbol %s." name
- | Some (((mp,_),sympos),[_,_,DB.Name]) -> sympos,mp
+ | Some (((mp,name),sympos),[_,_,DB.Name]) -> sympos,mp,name
| Some _ -> assert false) (* locate only returns DB.Name*)
- | _::_ -> None,mp
+ | _::_ -> None,mp,name
in
mk_bogus_sym mp name pos
From 8b593054bab2b762a27a73780da25c3b9d7fa0c6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 16:55:40 +0200
Subject: [PATCH 28/58] Multiple --require are now allowed
In particular one can require (and open) theory_hol.lp and then
require (and open) a notation.lp file to add infix notation.
---
TODO.md | 5 +++++
src/cli/lambdapi.ml | 24 ++++++++++++++----------
src/tool/indexing.ml | 7 +++++--
src/tool/indexing.mli | 1 +
4 files changed, 25 insertions(+), 12 deletions(-)
diff --git a/TODO.md b/TODO.md
index 7c14b5935..c3b55cbe2 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,6 +4,9 @@ TODO
Index and search
----------------
+* @abdelghani test if search in vscode still works once that
+ you have repaired lsp :-)
+
* @abdelghani include in HOL2DK_indexing git sub-repos of
coq-hol-light-real-with-N and coq-hol-light
and automatize the generation of the file to output Coq sources
@@ -69,6 +72,8 @@ Performance improvements
Documentation
-------------
+* fix the doc: --require can now be repeated
+
* fix the doc: not only "anywhere" but also "type" can be paired
only with ">="; maybe make it explicit that to match exactly the
type of a constant one should use "spine ="
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index ab21f6021..e65061865 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -20,19 +20,22 @@ module CLT = Cmdliner.Term
module LPSearchMain =
struct
-let sig_state_of_require =
- function
- None -> Core.Sig_state.dummy
- | Some req ->
- (* Search for a package from the current working directory. *)
- Package.apply_config (Filename.concat (Sys.getcwd()) ".") ;
- Core.Sig_state.of_sign
- (Compile.compile (Parsing.Parser.path_of_string req))
+let sig_state_of_require l =
+ (* Search for a package from the current working directory. *)
+ Package.apply_config (Filename.concat (Sys.getcwd()) ".") ;
+ List.fold_left
+ (fun ss req ->
+ Handle.Command.handle Compile.compile ss
+ (Pos.none
+ (Parsing.Syntax.P_require
+ (true, [Pos.none (Parsing.Parser.path_of_string req)]))))
+ Core.Sig_state.dummy l
let search_cmd cfg rules require s dbpath_opt =
Config.init cfg;
let run () =
Tool.Indexing.load_rewriting_rules rules ;
+ Tool.Indexing.force_meta_rules_loading () ;
let ss = sig_state_of_require require in
let dbpath = Option.get Path.default_dbpath dbpath_opt in
out Format.std_formatter "%a@."
@@ -43,6 +46,7 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
Config.init cfg;
let run () =
Tool.Indexing.load_rewriting_rules rules ;
+ Tool.Indexing.force_meta_rules_loading () ;
let ss = sig_state_of_require require in
let header = match header_file with
| None ->
@@ -485,10 +489,10 @@ let rules_arg : string list CLT.t =
multiple times to fetch rules from multiple files." in
Arg.(value & opt_all string [] & info ["rules"] ~docv:"FILENAME" ~doc)
-let require_arg : string option CLT.t =
+let require_arg : string list CLT.t =
let doc =
"LP file to be required before starting the search engine." in
- Arg.(value & opt (some string) None & info ["require"] ~docv:"PATH" ~doc)
+ Arg.(value & opt_all string [] & info ["require"] ~docv:"PATH" ~doc)
let custom_dbpath : string option CLT.t =
let doc =
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 58d291f19..c707a308a 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -605,6 +605,8 @@ let load_meta_rules () =
let meta_rules = lazy (load_meta_rules ())
+let force_meta_rules_loading () = ignore (Lazy.force meta_rules)
+
let normalize typ =
let dtree sym =
try QNameMap.find (name_of_sym sym) (Lazy.force meta_rules)
@@ -616,11 +618,12 @@ let _ = normalize_fun := normalize
let search_pterm ~generalize ~mok ss env pterm =
let env =
("V#",(new_var "V#",Term.mk_Type,None))::env in
+ Dream.log "QUERY before scoping: %a@." Parsing.Pretty.term pterm ;
let query =
Parsing.Scope.scope_search_pattern ~find_sym ~mok ss env pterm in
- Dream.log "QUERY before: %a" Core.Print.term query ;
+ Dream.log "QUERY before normalize: %a" Core.Print.term query ;
let query = normalize query in
- Dream.log "QUERY after: %a" Core.Print.term query ;
+ Dream.log "QUERY to be executed: %a" Core.Print.term query ;
DB.search ~generalize query
let rec is_flexible t =
diff --git a/src/tool/indexing.mli b/src/tool/indexing.mli
index 0f83152b6..b927ac01d 100644
--- a/src/tool/indexing.mli
+++ b/src/tool/indexing.mli
@@ -3,6 +3,7 @@ open Core
(* indexing *)
val empty : unit -> unit
val load_rewriting_rules: string list -> unit
+val force_meta_rules_loading: unit -> unit
val index_sign : Sign.t -> unit
val parse_source_map : string -> unit (* the name of the file *)
val deindex_path : string -> unit
From 7ff31c7bef81d647138c29f5ae74e17dda3d27aa Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 17:31:48 +0200
Subject: [PATCH 29/58] Added support for /\ \/ ~ to the Rocq lexer
---
TODO.md | 2 ++
src/parsing/rocqLexer.ml | 5 +++++
2 files changed, 7 insertions(+)
diff --git a/TODO.md b/TODO.md
index c3b55cbe2..a8ff05d16 100644
--- a/TODO.md
+++ b/TODO.md
@@ -72,6 +72,8 @@ Performance improvements
Documentation
-------------
+* document the Coq syntax: ~ /\ \/ -> forall exists =
+
* fix the doc: --require can now be repeated
* fix the doc: not only "anywhere" but also "type" can be paired
diff --git a/src/parsing/rocqLexer.ml b/src/parsing/rocqLexer.ml
index 6f0b2537e..4c9396da7 100644
--- a/src/parsing/rocqLexer.ml
+++ b/src/parsing/rocqLexer.ml
@@ -172,6 +172,11 @@ let rec token lb =
| '|' -> VBAR
| '_' -> UNDERSCORE
+ (* rocq identifiers *)
+ | "\\/" -> UID("∨")
+ | "/\\" -> UID("∧")
+ | "~" -> UID("¬")
+
(* identifiers *)
| regid -> UID(Utf8.lexeme lb)
| escid -> UID(remove_useless_escape(Utf8.lexeme lb))
From 1f7259eb653534d74466ca97692206669408057b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Fri, 11 Jul 2025 17:38:27 +0200
Subject: [PATCH 30/58] ..
---
TODO.md | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/TODO.md b/TODO.md
index a8ff05d16..b581701e2 100644
--- a/TODO.md
+++ b/TODO.md
@@ -25,8 +25,6 @@ Index and search
generated webpage an HTML snippet (e.g. with examples or
additional infos for that instance)
-* add notations for Coq stdlib to websearch (using Pratter?)
-
* syntactic sugar for regular expressions / way to write a regular
expression - only query efficiently
(concl = _ | "regexpr")
@@ -41,7 +39,14 @@ Index and search
Think about
-----------
-* alignments with same name ==> automatic preference?
+* what notations for Coq should websearch know about;
+ right now they are in:
+ - notation.lp file
+ problem: if you want to add a lot of them, you need to
+ require the definitions first (without requiring all the
+ library...)
+ - hard-coded lexing tokens in rocqLexer, e.g. /\ mapped to
+ the corresponding Unicode character
* would it be more reasonable to save the normalization rules
when the index is created and apply them as default when searching,
@@ -72,7 +77,7 @@ Performance improvements
Documentation
-------------
-* document the Coq syntax: ~ /\ \/ -> forall exists =
+* document the Coq syntax: ~ /\ \/ -> = forall exists fun
* fix the doc: --require can now be repeated
@@ -83,8 +88,6 @@ Documentation
* document new features, e.g. -sources (and find better
terminology), deindex
-* document Coq syntax in websearch
-
* document require ... as Foo: using Foo.X in the query already
works (pure magic!); of course it does not work when using
regular expressions [ check before! ]
From 9c8d0031c9b1adba5bc443b2a427c33ceb6dfcdf Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Wed, 16 Jul 2025 16:27:33 +0200
Subject: [PATCH 31/58] New pratter API
---
src/parsing/pratt.ml | 47 ++++++++++++++++++++------------------------
1 file changed, 21 insertions(+), 26 deletions(-)
diff --git a/src/parsing/pratt.ml b/src/parsing/pratt.ml
index 2091a7397..04383f891 100644
--- a/src/parsing/pratt.ml
+++ b/src/parsing/pratt.ml
@@ -21,27 +21,26 @@ end = struct
open Lplib
open Pos
- let is_op : Sig_state.find_sym -> Sig_state.t -> Env.t -> p_term
- -> (Pratter.fixity * float) option =
- fun find_sym ss env t ->
+ let ops (find_sym: Sig_state.find_sym) (ss: Sig_state.t) (env: Env.t)
+ (t: p_term) : (Pratter.fixity * float * p_term) list =
match t.elt with
| P_Iden({elt=(mp, s); _} as id, false) ->
- let open Option.Monad in
- let* sym =
+ let sym =
try (* Look if [id] is in [env]... *)
if mp <> [] then raise Not_found;
- ignore (Env.find s env); None
+ ignore (Env.find s env); []
with Not_found -> (* ... or look into the signature *)
- Some(find_sym ~prt:true ~prv:true ss id)
+ [find_sym ~prt:true ~prv:true ss id]
in
- (match Timed.(!(sym.sym_nota)) with
- | Term.Infix(assoc, prio) -> Some(Pratter.Infix assoc, prio)
- | Term.Prefix(prio) | Succ(Prefix(prio)) ->
- Some(Pratter.Prefix, prio)
- | Term.Postfix(prio) | Succ(Postfix(prio)) ->
- Some(Pratter.Postfix, prio)
- | _ -> None)
- | _ -> None
+ List.concat_map (fun (sym: Term.sym) ->
+ match Timed.(!(sym.sym_nota)) with
+ | Term.Infix(assoc, prio) -> [Pratter.Infix assoc, prio, t]
+ | Term.Prefix(prio) | Succ(Prefix(prio)) ->
+ [Pratter.Prefix, prio, t]
+ | Term.Postfix(prio) | Succ(Postfix(prio)) ->
+ [Pratter.Postfix, prio, t]
+ | _ -> []) sym
+ | _ -> []
let appl : p_term -> p_term -> p_term = fun t u ->
Pos.make (Pos.cat t.pos u.pos) (P_Appl(t, u))
@@ -54,18 +53,14 @@ end = struct
Sig_state.t -> Env.t -> p_term -> p_term =
fun ?(find_sym=Sig_state.find_sym) st env t ->
let h, args = Syntax.p_get_args t in
- let strm = Stream.of_list (h :: args) in
- let is_op = is_op find_sym st env in
- match Pratter.expression ~is_op ~appl strm with
+ let ops = ops find_sym st env in
+ let p = Pratter.expression ~ops ~appl ~token:Fun.id in
+ match Pratter.run p (List.to_seq (h :: args)) with
| Ok e -> e
- | Error `TooFewArguments ->
+ | Error `Too_few_arguments ->
Error.fatal t.pos "Malformed application in \"%a\"" Pretty.term t
- | Error `OpConflict (t, u) ->
- Error.fatal t.pos "Operator conflict between \"%a\" and \"%a\""
- Pretty.term t Pretty.term u
- | Error `UnexpectedInfix t ->
- Error.fatal t.pos "Unexpected infix operator \"%a\"" Pretty.term t
- | Error `UnexpectedPostfix t ->
- Error.fatal t.pos "Unexpected postfix operator \"%a\"" Pretty.term t
+ | Error `Op_conflict (t) ->
+ Error.fatal t.pos "Operator conflict on \"%a\""
+ Pretty.term t
end
include Pratt
From f1d288638e82a75063e5e242f8eff1b028a87828 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
Date: Thu, 17 Jul 2025 10:38:21 +0200
Subject: [PATCH 32/58] fix sig_state_of_require: the ghost signature needs to
be open
---
src/cli/lambdapi.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index a76623194..0815a56c6 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -29,7 +29,7 @@ let sig_state_of_require l =
(Pos.none
(Parsing.Syntax.P_require
(Some false, [Pos.none (Parsing.Parser.path_of_string req)]))))
- Core.Sig_state.dummy l
+ (Sig_state.open_sign Core.Sig_state.dummy Sign.Ghost.sign) l
let search_cmd cfg rules require s dbpath_opt =
Config.init cfg;
From e19588d067a2038ccdcfb15e0b7ea567a3f4efcc Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen
Date: Thu, 17 Jul 2025 15:46:50 +0200
Subject: [PATCH 33/58] Reverted commit that was due to Sig_state.dummy not
respecting the invariants
---
src/cli/lambdapi.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 48008f93b..803120631 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -29,7 +29,7 @@ let sig_state_of_require l =
(Pos.none
(Parsing.Syntax.P_require
(Some false, [Pos.none (Parsing.Parser.path_of_string req)]))))
- (Sig_state.open_sign Core.Sig_state.dummy Sign.Ghost.sign) l
+ Core.Sig_state.dummy l
let search_cmd cfg rules require s dbpath_opt =
Config.init cfg;
From 3ebc4cff3e007c07976954754fdc13815ed0e2e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
Date: Thu, 17 Jul 2025 17:15:34 +0200
Subject: [PATCH 34/58] fix comments (lambdapi -> rocq)
---
src/parsing/rocqLexer.ml | 2 +-
src/parsing/rocqParser.mly | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/parsing/rocqLexer.ml b/src/parsing/rocqLexer.ml
index 4c9396da7..3040e0c8c 100644
--- a/src/parsing/rocqLexer.ml
+++ b/src/parsing/rocqLexer.ml
@@ -1,4 +1,4 @@
-(** Lexer for Lambdapi syntax, using Sedlex, a Utf8 lexer generator. *)
+(** Lexer for Rocq syntax, using Sedlex, a Utf8 lexer generator. *)
open Lplib
open Sedlexing
diff --git a/src/parsing/rocqParser.mly b/src/parsing/rocqParser.mly
index 4b0524ad7..d783487c3 100644
--- a/src/parsing/rocqParser.mly
+++ b/src/parsing/rocqParser.mly
@@ -1,4 +1,4 @@
-(** Lambdapi parser, using the parser generator Menhir. *)
+(** Rocq parser, using the parser generator Menhir. *)
%{
open Lplib
From 9a0de11d2980b813c4fe08bbc91b2b65eabb0a25 Mon Sep 17 00:00:00 2001
From: Abdelghani Alidra
Date: Thu, 28 Aug 2025 12:38:36 +0200
Subject: [PATCH 35/58] document deindex
---
CHANGES.md | 5 +++++
doc/options.rst | 9 +++++++++
2 files changed, 14 insertions(+)
diff --git a/CHANGES.md b/CHANGES.md
index 7e7cf7f28..445c4c878 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -5,6 +5,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
## Unreleased
+### Added
+
+- CLI command `deindex` to remove constants from the index.
+
+
### Changed
- `simplify` now fails if the goal cannot be simplified.
diff --git a/doc/options.rst b/doc/options.rst
index bab6c2c89..c367d0daf 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -11,6 +11,7 @@ The available commands are:
* ``check``: check the correctness of input files.
* ``decision-tree``: output the decision tree of a symbol as a Dot graph (see :doc:`dtrees`)
+* ``deindex``: remove constants from the search index given a prefix path
* ``export``: translate the input file to other formats.
* ``help``: display the main help message.
* ``index``: create an index of symbols and rules of input files.
@@ -88,6 +89,14 @@ decision-tree
* ``--ghost`` print the decision tree of a ghost symbol. Ghost symbols are symbols used internally that cannot be used in the concrete syntax.
+deindex
+-------
+
+* ``--path`` : indicates the suffix of the paths of the symbols to be removed from the index.
+ The path must be dot (`.`) separated.
+ For insrance, if symbol `tests.OK.natural.N` is indexed, `lambdapi deindex --path tests.OK.natural`
+ will remove it (together with all the symbols whose path starts with `tests.OK.natural.N`) from the index.
+
export
------
From 2c5480c495a631f7ca2fcb79e9538d9bf982493f Mon Sep 17 00:00:00 2001
From: Abdelghani Alidra
Date: Thu, 28 Aug 2025 12:58:55 +0200
Subject: [PATCH 36/58] documented current dev indexing
---
CHANGES.md | 1 +
doc/queries.rst | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/CHANGES.md b/CHANGES.md
index 445c4c878..f374b9d3a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
### Added
- CLI command `deindex` to remove constants from the index.
+- Indexing of symbols from current development (as well as currently required files) and their deindexing when files are closed are now automatically supported.
### Changed
diff --git a/doc/queries.rst b/doc/queries.rst
index ad537c618..682677cbc 100644
--- a/doc/queries.rst
+++ b/doc/queries.rst
@@ -111,7 +111,7 @@ beginning, the timeout is set to 2s.
------------------
Runs a query between double quotes against the index file
-``~/.LPSearch.db``. See :doc:`query_language` for the query language
+``~/.LPSearch.db`` updated with current development and required files. See :doc:`query_language` for the query language
specification.
::
From 43a4ef12ff58bcb7a9b2f3209c209f3457225df1 Mon Sep 17 00:00:00 2001
From: Abdelghani Alidra
Date: Thu, 28 Aug 2025 13:10:12 +0200
Subject: [PATCH 37/58] update doc of deindex
---
doc/options.rst | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/doc/options.rst b/doc/options.rst
index c367d0daf..2a93786b9 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -93,7 +93,7 @@ deindex
-------
* ``--path`` : indicates the suffix of the paths of the symbols to be removed from the index.
- The path must be dot (`.`) separated.
+ The path must be dot (`.`) and is not checked for well formness (i.e. A.B matches A.BC).
For insrance, if symbol `tests.OK.natural.N` is indexed, `lambdapi deindex --path tests.OK.natural`
will remove it (together with all the symbols whose path starts with `tests.OK.natural.N`) from the index.
From 0f9cf9f8889c0389be4bd5bab8657b7898d74953 Mon Sep 17 00:00:00 2001
From: Abdelghani Alidra
Date: Fri, 29 Aug 2025 09:52:14 +0200
Subject: [PATCH 38/58] document filtering with regexp
---
CHANGES.md | 2 +-
doc/query_language.rst | 8 ++++++--
2 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index f374b9d3a..873f6df5a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -9,7 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
- CLI command `deindex` to remove constants from the index.
- Indexing of symbols from current development (as well as currently required files) and their deindexing when files are closed are now automatically supported.
-
+- Added filtering of search results using regular expressions.
### Changed
diff --git a/doc/query_language.rst b/doc/query_language.rst
index 1016f8e5b..b30625145 100644
--- a/doc/query_language.rst
+++ b/doc/query_language.rst
@@ -7,7 +7,7 @@ Queries can be expressed according to the following syntax:
Q ::= B | Q,Q | Q;Q | Q|PATH
B ::= WHERE HOW GENERALIZE? PATTERN
- PATH ::= << string >>
+ PATH ::= << string >> | "<< RegExp>>"
WHERE ::= name | anywhere | rule | lhs | rhs | type | concl | hyp | spine
HOW ::= > | = | >= | ≥
GENERALIZE ::= generalize
@@ -22,7 +22,7 @@ where
The semantics of the query language is the following:
-* a query ``Q`` is either a base query ``B``, the conjunction ``Q1,Q2`` of two queries ``Q1`` and ``Q2``, their disjunction ``Q1;Q2`` or the query ``Q|PATH`` that behaves as ``Q``, but only keeps the results whose path is a suffix of ``PATH`` (that must be a valid path prefix)
+* a query ``Q`` is either a base query ``B``, the conjunction ``Q1,Q2`` of two queries ``Q1`` and ``Q2``, their disjunction ``Q1;Q2`` or the query ``Q|PATH`` that behaves as ``Q``, but only keeps the results whose path is a suffix of ``PATH`` (that must be a valid path prefix) or matches the regular expression between double quotes (``""``)
* a base query ``name = ID`` looks for symbols with name ``ID`` in the library.
The identifier ``ID`` must not be qualified.
* a base query ``WHERE HOW GENERALIZE? PATTERN`` looks in the library for occurrences of the pattern ``PATTERN`` **up to normalization rules** and, if ``generalize`` is specified, also **up to generalization** of the pattern. The normalization rules are library specific and are employed during indexing. They can be used, for example, to remove the clutter associated to encodings, to align concepts by mapping symbols to cross-library standard ones, or to standardize the shape of statements to improve recall (e.g. replacing occurrence of ``x > y`` with ``y < x``).
@@ -53,5 +53,9 @@ Examples:
in a module whose path is a suffix of ``math.arithmetics``. The query
can return ``plus_O : ∀x: nat. plus x O = x`` where ``plus_O`` has
fully qualified name ``math.arithmetics.addition.plus``
+ * ``concl > plus | "*.arithmetics"``
+ searches for theorems having an hypothesis containing ``plus`` and located
+ in a module whose path matches ``*.arithmetics``. The query
+ can return ``math.arithmetics.addition.plus`` and ``mathematics.arithmetics.addition.plus``
* ``name = nat ; name = NAT``
searches for symbols named either ``nat`` or ``NAT``
From 14d88974f8d031403181813e0e7a7df6e02228e5 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Mon, 1 Sep 2025 13:21:55 +0200
Subject: [PATCH 39/58] document Rocq support
---
CHANGES.md | 1 +
doc/options.rst | 3 +++
doc/query_language.rst | 6 +++---
src/cli/lambdapi.ml | 8 +++-----
4 files changed, 10 insertions(+), 8 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 873f6df5a..804d71023 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
- CLI command `deindex` to remove constants from the index.
- Indexing of symbols from current development (as well as currently required files) and their deindexing when files are closed are now automatically supported.
- Added filtering of search results using regular expressions.
+- Added support for basic Rocq syntax for writing search queries (fun, forall, exists, /\ and ~)
### Changed
diff --git a/doc/options.rst b/doc/options.rst
index 2a93786b9..f0eb34395 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -183,6 +183,9 @@ index
* ``--db `` tells lambdapi to index symbols and rules in ```` instead of ``~/.LPSearch.db``.
+* ``--source`` indicates the path to the file containing the mapping to additional sources (for instance, Rocq sources corresponding to indexed ones).
+ These sources will also be displayed by the websearch engine when showing the results.
+
install/uninstall
-----------------
diff --git a/doc/query_language.rst b/doc/query_language.rst
index b30625145..537916db1 100644
--- a/doc/query_language.rst
+++ b/doc/query_language.rst
@@ -11,7 +11,7 @@ Queries can be expressed according to the following syntax:
WHERE ::= name | anywhere | rule | lhs | rhs | type | concl | hyp | spine
HOW ::= > | = | >= | ≥
GENERALIZE ::= generalize
- PATTERN ::= << term possibly containing placeholders _ (for terms) and V# (for variable occurrences >>
+ PATTERN ::= << term possibly containing placeholders _ (for terms) and V# (for variable occurrences) >>
where
@@ -19,6 +19,8 @@ where
* parentheses can be used as usual to force a different precedence order
* ``anywhere`` can be paired only with ``>=`` and ``name`` can be paired only with ``>=`` and no ``generalize``
* a pattern should be wrapped in parentheses, unless it is atomic (e.g. an identifier or a placeholder)
+* a pattern is expressed using the Lambdapi terms syntax. Additionaly, the search engine allows the use of a basic Rocq syntax to express terms.
+ Specifically, ``fun``, ``forall``, ``exists``, ``/\`` and ``~`` are supported to express terms inside the pattern.
The semantics of the query language is the following:
@@ -42,8 +44,6 @@ The semantics of the query language is the following:
* ``=`` the pattern must match the whole position
* ``>`` the pattern must match a strict subterm of the position
-Note that for commodity, ``forall`` and ``->`` can be used inside the query instead of the Unicode characters ``Π`` and ``→`` respectively.
-
Examples:
* ``hyp = (nat → bool) , hyp >= (list nat)``
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 803120631..c89feea33 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -67,11 +67,9 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
query language specification to learn about the query language.
The query language also uses the
- Lambdapi terms syntax. with the possibility to use,
- for commodity,
- \"forall\" and \"->\" instead of \"Π\" and \"→\" respectively
- (results are displayed with the Unicode symbols
- \"Π\" and \"→\" though).
+ Lambdapi terms syntax.
+ while supporting a subset of the Rocq syntax (specificaly,
+ terms using fun, forall, exists, /\ and ~ are allowed)
In particular, the following constructors can come handy for
writing queries:
From 2b88b50f8df48811591c22dd59464543c8859ad0 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Mon, 1 Sep 2025 13:51:53 +0200
Subject: [PATCH 40/58] document multiple --require flag and disambiguating
overloaded symbols
---
CHANGES.md | 6 +++++-
doc/options.rst | 4 ++--
src/cli/lambdapi.ml | 2 +-
3 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 804d71023..77b005896 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -10,7 +10,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
- CLI command `deindex` to remove constants from the index.
- Indexing of symbols from current development (as well as currently required files) and their deindexing when files are closed are now automatically supported.
- Added filtering of search results using regular expressions.
-- Added support for basic Rocq syntax for writing search queries (fun, forall, exists, /\ and ~)
+- Added support for basic Rocq syntax for writing search queries (fun, forall, exists, /\ and ~).
+- Allow the `--require` flag to be used multiple times with the `search` and `websearch` commands.
+- Ambiguity due to overloaded symbols is now solved by normalisation.
+
+
### Changed
diff --git a/doc/options.rst b/doc/options.rst
index f0eb34395..4d8459a7e 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -45,7 +45,7 @@ The ``index`` command generates the file ``~/.LPSearch.db`` if ``$HOME`` is defi
**Remark on search:**
-The command ``search`` takes as argument a query and runs it against the index file ``~/.LPSearch.db``. It is also possible to normalize terms in the query wrt some rules by using ``--rules`` options. It is advised to use the same set of rules previously used during indexing. It is also possible to pass via ``--require`` a file to be required and opened before performing the query, e.g. to specify implicit arguments for symbols. See :doc:`query_language` for the specification of the query language.
+The command ``search`` takes as argument a query and runs it against the index file ``~/.LPSearch.db``. It is also possible to normalize terms in the query wrt some rules by using ``--rules`` options. It is advised to use the same set of rules previously used during indexing. It is also possible to pass via ``--require`` files to be required and opened before performing the query, e.g. to specify implicit arguments for symbols. See :doc:`query_language` for the specification of the query language.
**Common flags:**
@@ -203,7 +203,7 @@ search
* ``--rules `` tells lambdapi to normalize terms in the query using the rules given in the file ````. Several files can be specified by using several ``--rules`` options. In these files, symbols must be fully qualified but no ``require`` command is needed. Moreover, the rules do not need to preserve typing. On the other hand, right hand-side of rules must contain implicit arguments. It is advised to use the same set of rules previously used during indexing.
-* ``--require `` requires and open ```` when starting the search engine. The file can be used for example to specify implicit arguments for symbols used in the queries.
+* ``--require `` requires and opens ```` when starting the search engine. The files can be used for example to specify implicit arguments for symbols used in the queries.
* ``--db `` tells lambdapi to search in ```` instead of ``~/.LPSearch.db``.
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index c89feea33..829fdafcf 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -489,7 +489,7 @@ let rules_arg : string list CLT.t =
let require_arg : string list CLT.t =
let doc =
- "LP file to be required before starting the search engine." in
+ "LP files to be required before starting the search engine." in
Arg.(value & opt_all string [] & info ["require"] ~docv:"PATH" ~doc)
let custom_dbpath : string option CLT.t =
From d868fb4a560de9468248c2bee97de0d6ca9e63e8 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Mon, 1 Sep 2025 14:36:04 +0200
Subject: [PATCH 41/58] update CHANGES.md with search improvements
---
CHANGES.md | 3 +++
1 file changed, 3 insertions(+)
diff --git a/CHANGES.md b/CHANGES.md
index 77b005896..7b55d257f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -13,6 +13,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
- Added support for basic Rocq syntax for writing search queries (fun, forall, exists, /\ and ~).
- Allow the `--require` flag to be used multiple times with the `search` and `websearch` commands.
- Ambiguity due to overloaded symbols is now solved by normalisation.
+- Added streaming of results in command line search.
+- Supporting `Plac` in rewriting rules.
+- Fixed Stack_overflow exception due large number of search results.
From 74712037ad3df1d6a349387ce25b96cac606c276 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Thu, 16 Oct 2025 19:00:11 +0200
Subject: [PATCH 42/58] use Lplib.Color instead of hand made coloring in
indexing
---
src/cli/lambdapi.ml | 2 +-
src/lplib/color.ml | 2 ++
src/tool/indexing.ml | 62 +++++++++++++++++++++++++-------------------
3 files changed, 38 insertions(+), 28 deletions(-)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 829fdafcf..0e8aae406 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -67,7 +67,7 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
query language specification to learn about the query language.
The query language also uses the
- Lambdapi terms syntax.
+ Lambdapi terms syntax.
while supporting a subset of the Rocq syntax (specificaly,
terms using fun, forall, exists, /\ and ~ are allowed)
In particular, the following constructors can come handy for
diff --git a/src/lplib/color.ml b/src/lplib/color.ml
index 4d316926a..d4068d221 100644
--- a/src/lplib/color.ml
+++ b/src/lplib/color.ml
@@ -75,6 +75,8 @@ let blu fmt = colorize Blu fmt
let mag fmt = colorize Mag fmt
let cya fmt = colorize Cya fmt
+let default (fmt:('a, 'b, 'c, 'd, 'e, 'f) format6) = fmt
+
(** [g_or_r cond fmt] colors the format [fmt] in green if [cond] is [true] and
in red otherwise. *)
let g_or_r cond = if cond then gre else red
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 5603e41f9..54dc822ac 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -463,47 +463,55 @@ module DB = struct
let generic_pp_of_item_list ~escape ~escaper ~separator ~sep ~delimiters
~lis:(lisb,lise) ~pres:(preb,pree)
- ~bold:(boldb,bolde) ~code:(codeb,codee) fmt l
- =
+ ~bold:(boldb,bolde) ~code:(codeb,codee) ?(colorizer=Lplib.Color.default)
+ fmt l =
if l = [] then
Lplib.Base.out fmt "Nothing found"
else
- Lplib.List.pp
- (fun ppf (((p,n) as sym_name,pos),(positions : answer)) ->
- let sourceid,sourcepos = source_infos_of_sym_name sym_name in
- Lplib.Base.out ppf "%s%a.%s%s%s@%s%s%a%s%s%s%a%s%a%s%a%s%s%s%s@."
- lisb (escaper.run Core.Print.path) p boldb n bolde
- (popt_to_string ~print_dirname:false pos)
- separator (generic_pp_of_position_list ~escaper ~sep) positions
- separator preb codeb
- (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
- ~complain_if_location_unknown:true) pos
- separator
- (fun ppf opt ->
- match opt with
- | None -> Lplib.Base.string ppf ""
- | Some sourceid ->
- Lplib.Base.string ppf ("Translated to " ^ sourceid)) sourceid
- separator
- (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
- ~complain_if_location_unknown:false) sourcepos
- codee pree lise separator)
+ Lplib.List.pp (fun ppf (((p,n) as sym_name,pos),(positions : answer)) ->
+ let sourceid,sourcepos = source_infos_of_sym_name sym_name in
+ (* let n_pp = (Lplib.Color.red "%s") n in *)
+ Lplib.Base.out ppf
+ ("%s%a.%s"
+ ^^
+ (colorizer "%s")
+ ^^ "%s@%s%s%a%s%s%s%a%s%a%s%a%s%s%s%s@.")
+ lisb (escaper.run Core.Print.path) p boldb n bolde
+ (popt_to_string ~print_dirname:false pos)
+ separator (generic_pp_of_position_list ~escaper ~sep) positions
+ separator preb codeb
+ (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
+ ~complain_if_location_unknown:true) pos
+ separator
+ (fun ppf opt ->
+ match opt with
+ | None -> Lplib.Base.string ppf ""
+ | Some sourceid ->
+ Lplib.Base.string ppf ("Translated to " ^ sourceid)) sourceid
+ separator
+ (Common.Pos.print_file_contents ~parse_file ~escape ~delimiters
+ ~complain_if_location_unknown:false) sourcepos
+ codee pree lise separator)
"" fmt l
let html_of_item_list =
generic_pp_of_item_list ~escape:Dream.html_escape ~escaper:html_escaper
~separator:" \n" ~sep:" and \n" ~delimiters:("
","
")
~lis:("
","
") ~pres:("
","
") ~bold:("","")
- ~code:("","")
+ ~code:("","") ~colorizer: Lplib.Color.default
let pp_item_list fmt l =
generic_pp_of_item_list ~escape:(fun x -> x) ~escaper:identity_escaper
~separator:"\n" ~sep:" and\n" ~delimiters:("","")
~lis:("* ","") ~pres:("","")
- ~bold:(if Stdlib.(!Common.Mode.lsp_mod) || Unix.isatty Unix.stdout then
- ("[0;36m","[0m")
- else ("",""))
- ~code:("","") fmt l
+ ~bold:("","")
+ ~code:("","")
+ ~colorizer:
+ (if Stdlib.(!Common.Mode.lsp_mod) || Unix.isatty Unix.stdout then
+ Lplib.Color.red
+ else
+ Lplib.Color.default)
+ fmt l
let pp_results_list fmt l = pp_item_list fmt l
From 107d6900e0fcf55f393a54d85769a70515a8a7fb Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Thu, 6 Nov 2025 16:18:31 +0100
Subject: [PATCH 43/58] fix color of error messages: specifically Overloaded
symbol prod. Please rewrite the query replacing...
---
src/cli/config.ml | 2 +-
src/cli/lambdapi.ml | 2 +-
src/common/error.ml | 27 +++++++++++++++------------
src/handle/command.ml | 6 +++---
src/handle/tactic.ml | 6 +++---
src/lsp/lp_doc.ml | 2 +-
src/lsp/lp_lsp.ml | 2 +-
src/pure/pure.ml | 12 ++++++------
src/tool/indexing.ml | 19 ++++++++++---------
9 files changed, 41 insertions(+), 37 deletions(-)
diff --git a/src/cli/config.ml b/src/cli/config.ml
index 14240aaab..788e15709 100644
--- a/src/cli/config.ml
+++ b/src/cli/config.ml
@@ -109,7 +109,7 @@ let map_dir : (Path.t * string) list CLT.t =
let path : Path.t Arg.conv =
let parse (s: string) : (Path.t, [>`Msg of string]) result =
try Ok(Parser.path_of_string s)
- with Error.Fatal(_,s) -> Error(`Msg(s))
+ with Error.Fatal(_,s, _) -> Error(`Msg(s))
in
let print fmt p = Path.pp fmt p in
Arg.conv (parse, print)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 0e8aae406..9382dfd23 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -288,7 +288,7 @@ let qident : qident CLT.t =
let qident : qident Arg.conv =
let parse (s: string): (qident, [>`Msg of string]) result =
try Ok(Parser.qident_of_string s)
- with Fatal(_,s) -> Error(`Msg(s))
+ with Fatal(_,s,_) -> Error(`Msg(s))
in
let print fmt qid = Pretty.qident fmt (Pos.none qid) in
Arg.conv (parse, print)
diff --git a/src/common/error.ml b/src/common/error.ml
index 40cad8fe5..4073aae52 100644
--- a/src/common/error.ml
+++ b/src/common/error.ml
@@ -37,7 +37,7 @@ let no_wrn : ('a -> 'b) -> 'a -> 'b = fun f x ->
cases where positions are expected [Some None] may be used to indicate the
abscence of a position. This may happen when terms are generated (e.g., by
a form of desugaring). *)
-exception Fatal of Pos.popt option * string
+exception Fatal of Pos.popt option * string * string
(** [fatal_str fmt] may be called an arbitrary number of times to build up the
error message of the [fatal] or [fatal_no_pos] functions prior to calling
@@ -46,16 +46,19 @@ exception Fatal of Pos.popt option * string
let fatal_msg : 'a outfmt -> 'a =
fun fmt -> out Format.str_formatter fmt
-(** [fatal popt fmt] raises the [Fatal(popt,msg)] exception, in which [msg] is
- built from the format [fmt] (provided the necessary arguments). *)
+(** [fatal popt fmt] raises the [Fatal(popt,msg,more)] exception, in which [msg] is
+ built from the format [fmt] (provided the necessary arguments).
+ [more] continues the error message and is printed in normal format instead of
+ red color*)
+
let fatal : Pos.popt -> ('a,'b) koutfmt -> 'a = fun pos fmt ->
- let cont _ = raise (Fatal(Some(pos), Format.flush_str_formatter ())) in
+ let cont _ = raise (Fatal(Some(pos), Format.flush_str_formatter (), "")) in
Format.kfprintf cont Format.str_formatter fmt
(** [fatal_no_pos fmt] is similar to [fatal _ fmt], but it is used to raise an
error that has no precise attached source code position. *)
-let fatal_no_pos : ('a,'b) koutfmt -> 'a = fun fmt ->
- let cont _ = raise (Fatal(None, Format.flush_str_formatter ())) in
+let fatal_no_pos : ?more:string -> ('a,'b) koutfmt -> 'a = fun ?(more="") fmt ->
+ let cont _ = raise (Fatal(None, Format.flush_str_formatter (), more)) in
Format.kfprintf cont Format.str_formatter fmt
(** [handle_exceptions f] runs [f ()] in an exception handler and handles both
@@ -64,15 +67,15 @@ let fatal_no_pos : ('a,'b) koutfmt -> 'a = fun fmt ->
[1] (indicating failure). Hence, [handle_exceptions] should only be called
by the main program logic, not by the internals. *)
let handle_exceptions : (unit -> unit) -> unit = fun f ->
- let exit_with : type a b. (a,b) koutfmt -> a = fun fmt ->
+ let exit_with : type a b. string -> (a,b) koutfmt -> a = fun cnt fmt ->
Color.update_with_color Format.err_formatter;
- Format.kfprintf (fun _ -> exit 1) Format.err_formatter
+ Format.kfprintf (fun _ -> Color.update_with_color Format.err_formatter;(Format.kfprintf (fun _ -> exit 1) Format.err_formatter "%s" cnt)) Format.err_formatter
(Color.red (fmt ^^ "@."))
in
try f () with
- | Fatal(None, msg) -> exit_with "%s" msg
- | Fatal(Some(p), msg) -> exit_with "[%a] %s" Pos.pp p msg
+ | Fatal(None, msg, cnt) -> exit_with cnt "%s" msg
+ | Fatal(Some(p), msg, cnt) -> exit_with cnt "[%a] %s" Pos.pp p msg
| e ->
- exit_with "Uncaught [%s].\n%s"
+ exit_with "" "Uncaught [%s].\n%s"
(Printexc.to_string e)
- (Printexc.get_backtrace())
+ (Printexc.get_backtrace())
\ No newline at end of file
diff --git a/src/handle/command.ml b/src/handle/command.ml
index c8cad76cc..8d48e2ef6 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -623,9 +623,9 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
ss
with
| Timeout as e -> raise e
- | Fatal(Some(Some(_)),_) as e -> raise e
- | Fatal(None ,m) -> fatal pos "Error on command.@.%s" m
- | Fatal(Some(None) ,m) -> fatal pos "Error on command.@.%s" m
+ | Fatal(Some(Some(_)),_, _) as e -> raise e
+ | Fatal(None ,m, _) -> fatal pos "Error on command.@.%s" m
+ | Fatal(Some(None) ,m, _) -> fatal pos "Error on command.@.%s" m
| e ->
fatal pos "Uncaught exception: %s." (Printexc.to_string e)
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
index 55a4711c4..aae8319a1 100644
--- a/src/handle/tactic.ml
+++ b/src/handle/tactic.ml
@@ -665,12 +665,12 @@ let rec handle :
| P_tac_try tactic ->
begin
try handle ss sym_pos prv ps tactic
- with Fatal(_, _s) -> ps
+ with Fatal(_, _s, _) -> ps
end
| P_tac_orelse(t1,t2) ->
begin
try handle ss sym_pos prv ps t1
- with Fatal(_, _s) -> handle ss sym_pos prv ps t2
+ with Fatal(_, _s, _) -> handle ss sym_pos prv ps t2
end
| P_tac_repeat t ->
begin
@@ -679,7 +679,7 @@ let rec handle :
let ps = handle ss sym_pos prv ps t in
if List.length ps.proof_goals < nb_goals then ps
else handle ss sym_pos prv ps tac
- with Fatal(_, _s) -> ps
+ with Fatal(_, _s, _) -> ps
end
| P_tac_and(t1,t2) ->
let ps = handle ss sym_pos prv ps t1 in
diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index 2eecef981..d3390d418 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -131,7 +131,7 @@ let new_doc ~uri ~version ~text =
assert(String.is_prefix "file://" uri);
let path = String.sub uri 7 (String.length uri - 7) in
Some(Pure.initial_state path), []
- with Error.Fatal(_pos, msg) ->
+ with Error.Fatal(_pos, msg, _) ->
let loc : Pos.pos =
{
fname = Some(uri);
diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml
index ec48b398e..28d5f83c3 100644
--- a/src/lsp/lp_lsp.ml
+++ b/src/lsp/lp_lsp.ml
@@ -58,7 +58,7 @@ let do_check_text ofmt ~doc =
let doc, diags =
try
Lp_doc.check_text ~doc
- with Common.Error.Fatal(_pos, msg) ->
+ with Common.Error.Fatal(_pos, msg, _) ->
let loc : Pos.pos =
{
fname = Some(doc.uri);
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index 0b31e013e..e2b6dbaa3 100644
--- a/src/pure/pure.ml
+++ b/src/pure/pure.ml
@@ -73,9 +73,9 @@ let parse_text :
Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) (parse_string fname s);
List.rev Stdlib.(!cmds), None
with
- | Fatal(Some(Some(pos)), msg) -> List.rev Stdlib.(!cmds), Some(pos, msg)
- | Fatal(Some(None) , _ ) -> assert false
- | Fatal(None , _ ) -> assert false
+ | Fatal(Some(Some(pos)), msg, _) -> List.rev Stdlib.(!cmds), Some(pos, msg)
+ | Fatal(Some(None) , _ , _) -> assert false
+ | Fatal(None , _ , _) -> assert false
type proof_finalizer = Sig_state.t -> Proof.proof_state -> Sig_state.t
@@ -170,7 +170,7 @@ let handle_command : state -> Command.t -> command_result =
(t, ss, d.pdata_state, d.pdata_finalize, d.pdata_prv, d.pdata_sym_pos)
in
Cmd_Proof(ps, d.pdata_proof, d.pdata_sym_pos, d.pdata_end_pos)
- with Fatal(Some p,m) ->
+ with Fatal(Some p,m, _) ->
Cmd_Error(Some p, Pos.popt_to_string p ^ " " ^ m)
let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
@@ -179,13 +179,13 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
let ps, qres = Handle.Tactic.handle ss sym_pos prv (ps, None) tac n in
let qres = Option.map (fun f -> f ()) qres in
Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres)
- with Fatal(Some p,m) ->
+ with Fatal(Some p,m, _) ->
Tac_Error(Some p, Pos.popt_to_string p ^ " " ^ m)
let end_proof : proof_state -> command_result =
fun (_, ss, ps, finalize, _, _) ->
try Cmd_OK((Time.save (), finalize ss ps), None)
- with Fatal(Some p,m) ->
+ with Fatal(Some p,m, _) ->
Cmd_Error(Some p, Pos.popt_to_string p ^ " " ^ m)
let get_symbols : state -> Term.sym Extra.StrMap.t =
diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml
index 54dc822ac..1a3eb62d6 100644
--- a/src/tool/indexing.ml
+++ b/src/tool/indexing.ml
@@ -394,14 +394,14 @@ module DB = struct
Sym_nameMap.add lpid (sourceid,fname,start_line,end_line) !sidx
| _ ->
raise
- (Common.Error.Fatal(None,"wrong file format for source map file"))
+ (Common.Error.Fatal(None,"wrong file format for source map file", ""))
done ;
with
| Failure _ as exn ->
close_in ch;
raise
(Common.Error.Fatal(None,"wrong file format for source map file: " ^
- Printexc.to_string exn))
+ Printexc.to_string exn, ""))
| End_of_file -> close_in ch) ;
db := lazy (!sidx,idx)
@@ -762,7 +762,7 @@ let index_sym sym =
(DB.ItemSet.bindings (DB.locate_name (snd qname)))
then
raise
- (Common.Error.Fatal(None,string_of_sym_name qname ^ " already indexed")) ;
+ (Common.Error.Fatal(None,string_of_sym_name qname ^ " already indexed", "")) ;
DB.insert_name (snd qname) ((qname,sym.sym_decl_pos),[Name]) ;
(* Type + InType *)
let typ = Timed.(!(sym.Core.Term.sym_type)) in
@@ -882,7 +882,7 @@ module UserLevelQueries = struct
let s = Str.global_replace (Str.regexp_string " -> ") " → " s in
Str.global_replace (Str.regexp "\\bforall\\b") "Π" s
- let search_cmd_gen ss ~from ~how_many ~fail ~pp_results
+ let search_cmd_gen ss ~from ~how_many ~(fail:(?more:string -> string -> string)) ~pp_results
~title_tag:(hb,he) fmt s =
try
let pstream = Parsing.Parser.Rocq.parse_search_query_string "LPSearch" s in
@@ -899,13 +899,14 @@ module UserLevelQueries = struct
| Stream.Failure ->
Lplib.Base.out fmt "%s"
(fail (Format.asprintf "Syntax error: a query was expected@."))
- | Common.Error.Fatal(_,msg) ->
+ | Common.Error.Fatal(_,msg, _) ->
Lplib.Base.out fmt "%s" (fail (Format.asprintf "Error: %s@." msg))
| Overloaded(name,res) ->
Lplib.Base.out fmt "%s" (fail (Format.asprintf
"Overloaded symbol %s. Please rewrite the query replacing %s \
- with a fully qualified identifier among the following:@.%a@."
- name name pp_results (ItemSet.bindings res)))
+ with a fully qualified identifier among the following:@."
+ name name)
+ ~more:(Format.asprintf "%a@." pp_results (ItemSet.bindings res)))
| Stack_overflow ->
Lplib.Base.out fmt "%s" (fail
(Format.asprintf
@@ -918,14 +919,14 @@ module UserLevelQueries = struct
Stdlib.(the_dbpath := dbpath);
Format.asprintf "%a"
(search_cmd_gen ss ~from ~how_many
- ~fail:(fun x -> "" ^ x ^ "")
+ ~fail:(fun ?more x -> "" ^ x ^ "" ^ (Option.value more ~default:""))
~pp_results:(html_of_results_list from) ~title_tag:("
","
")) s
let search_cmd_txt ss ~dbpath fmt s =
let s = transform_ascii_to_unicode s in
Stdlib.(the_dbpath := dbpath);
search_cmd_gen ss ~from:0 ~how_many:999999
- ~fail:(fun x -> Common.Error.fatal_no_pos "%s" x)
+ ~fail:(fun ?more x -> Common.Error.fatal_no_pos ?more "%s" x)
~pp_results:pp_results_list ~title_tag:("","") fmt s
end
From 4a4896505eeb4a0fd5add1600825425abeb33061 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Thu, 6 Nov 2025 19:42:27 +0100
Subject: [PATCH 44/58] read header of websearch page from file
---
dune-project | 2 ++
src/cli/lambdapi.ml | 44 +++++----------------------------------
src/tool/description.html | 38 +++++++++++++++++++++++++++++++++
src/tool/dune | 13 +++++++++++-
4 files changed, 57 insertions(+), 40 deletions(-)
create mode 100644 src/tool/description.html
diff --git a/dune-project b/dune-project
index 6e69ec795..24e32cc7b 100644
--- a/dune-project
+++ b/dune-project
@@ -9,6 +9,7 @@
(license CECILL-2.1)
(using menhir 2.0)
+(using dune_site 0.1)
(package
(name lambdapi)
@@ -47,4 +48,5 @@ systems: Dedukti, Coq, HRS, CPF.")
(lwt_ppx (>= 1))
(uri (>= 1.1))
)
+ (sites (share server_resources))
)
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 9382dfd23..5c25ba612 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -50,45 +50,11 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
let ss = sig_state_of_require require in
let header = match header_file with
| None ->
- "
-
-
- The search button answers the query. Read the
- query language specification to learn about the query language.
- The query language also uses the
- Lambdapi terms syntax.
- while supporting a subset of the Rocq syntax (specificaly,
- terms using fun, forall, exists, /\ and ~ are allowed)
- In particular, the following constructors can come handy for
- writing queries:
-
-
-
an anonymous functionλ (x:A) y z,t
- mapping x, y
- and z (of type A for x) to t.
-
a dependent product
- forall (x:A) y z,T
-
-
a non-dependent product A -> T
- (syntactic sugar for forall x:A,T when
- x does not occur in T)
-
-
- "
+ let themes_locations : string list = Tool.Mysites.Sites.server_resources in
+ let file = match themes_locations with
+ | [] -> assert false
+ | x :: _ -> x in
+ Lplib.String.string_of_file (file ^ "/default/description.html")
| Some file -> Lplib.String.string_of_file file in
let dbpath = Option.get Path.default_dbpath dbpath_opt in
let path_in_url = match path_in_url with
diff --git a/src/tool/description.html b/src/tool/description.html
new file mode 100644
index 000000000..ea4e7e04a
--- /dev/null
+++ b/src/tool/description.html
@@ -0,0 +1,38 @@
+
+
+
+ The search button answers the query. Read the
+ query language specification to learn about the query language.
+ The query language also uses the
+ Lambdapi terms syntax.
+ while supporting a subset of the Rocq syntax (specificaly,
+ terms using fun, forall, exists, /\ and ~ are allowed)
+ In particular, the following constructors can come handy for
+ writing queries:
+
+
+
an anonymous functionλ (x:A) y z,t
+ mapping x, y
+ and z (of type A for x) to t.
+
a dependent product
+ forall (x:A) y z,T
+
+
a non-dependent product A -> T
+ (syntactic sugar for forall x:A,T when
+ x does not occur in T)
+
+
\ No newline at end of file
diff --git a/src/tool/dune b/src/tool/dune
index d3cc83495..ac46dc70a 100644
--- a/src/tool/dune
+++ b/src/tool/dune
@@ -2,10 +2,21 @@
(name tool)
(public_name lambdapi.tool)
(modules :standard)
- (libraries lambdapi.parsing lambdapi.core dream unix)
+ (libraries lambdapi.parsing lambdapi.core dream unix dune-site)
(preprocess (pps lwt_ppx)))
(rule
(targets websearch.ml)
(deps websearch.eml.ml)
(action (run dream_eml %{deps} --workspace %{workspace_root})))
+
+(install
+ (section (site (lambdapi server_resources)))
+ (files
+ (description.html as default/description.html)
+ )
+)
+
+(generate_sites_module
+ (module mysites)
+ (sites lambdapi))
From f3f5a35a68d63d44bdceaff45b30077951178a28 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Fri, 7 Nov 2025 09:12:18 +0100
Subject: [PATCH 45/58] move the default html header to ressources
---
TODO.md | 12 ------------
{src/tool => ressources}/description.html | 0
ressources/dune | 23 +++++++++++++++++++++++
src/cli/dune | 2 +-
src/cli/lambdapi.ml | 2 +-
src/tool/dune | 13 +------------
6 files changed, 26 insertions(+), 26 deletions(-)
rename {src/tool => ressources}/description.html (100%)
create mode 100644 ressources/dune
diff --git a/TODO.md b/TODO.md
index b581701e2..187cb0c9a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -4,23 +4,11 @@ TODO
Index and search
----------------
-* @abdelghani test if search in vscode still works once that
- you have repaired lsp :-)
-
* @abdelghani include in HOL2DK_indexing git sub-repos of
coq-hol-light-real-with-N and coq-hol-light
and automatize the generation of the file to output Coq sources
* @abdelghani
- - use lplib/color.ml in place of our color management of the
- output [ but do not lose our code to check if we are
- in lsp_mode or targeting a tty ]
- - "Overloaded symbol prod. Please rewrite the query replacing..."
- is printed in red but the following lines are also in red
- (i.e. black color is not restored)
-
-* @abdelghani
- - commit the very nice new look&feel of websearch
- (maybe?) allow an --add-examples=FNAME to include in the
generated webpage an HTML snippet (e.g. with examples or
additional infos for that instance)
diff --git a/src/tool/description.html b/ressources/description.html
similarity index 100%
rename from src/tool/description.html
rename to ressources/description.html
diff --git a/ressources/dune b/ressources/dune
new file mode 100644
index 000000000..2f4367a8e
--- /dev/null
+++ b/ressources/dune
@@ -0,0 +1,23 @@
+(library
+ (name ressources)
+ ; (public_name lambdapi.tool)
+ (modules :standard)
+ (libraries lambdapi.parsing lambdapi.core dream unix dune-site)
+ (preprocess (pps lwt_ppx))
+)
+
+; (rule
+; (targets websearch.ml)
+; (deps websearch.eml.ml)
+; (action (run dream_eml %{deps} --workspace %{workspace_root})))
+
+(install
+ (section (site (lambdapi server_resources)))
+ (files
+ (description.html as default/description.html)
+ )
+)
+
+(generate_sites_module
+ (module mysites)
+ (sites lambdapi))
diff --git a/src/cli/dune b/src/cli/dune
index 572d1a1e6..b6692f1c2 100644
--- a/src/cli/dune
+++ b/src/cli/dune
@@ -4,4 +4,4 @@
(modes byte native)
(modules :standard)
(libraries cmdliner lambdapi.lsp lambdapi.tool lambdapi.handle
- lambdapi.export unix))
+ lambdapi.export unix ressources))
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index 5c25ba612..cb40228ef 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -50,7 +50,7 @@ let websearch_cmd cfg rules port require header_file dbpath_opt path_in_url =
let ss = sig_state_of_require require in
let header = match header_file with
| None ->
- let themes_locations : string list = Tool.Mysites.Sites.server_resources in
+ let themes_locations : string list = Ressources.Mysites.Sites.server_resources in
let file = match themes_locations with
| [] -> assert false
| x :: _ -> x in
diff --git a/src/tool/dune b/src/tool/dune
index ac46dc70a..e94761262 100644
--- a/src/tool/dune
+++ b/src/tool/dune
@@ -8,15 +8,4 @@
(rule
(targets websearch.ml)
(deps websearch.eml.ml)
- (action (run dream_eml %{deps} --workspace %{workspace_root})))
-
-(install
- (section (site (lambdapi server_resources)))
- (files
- (description.html as default/description.html)
- )
-)
-
-(generate_sites_module
- (module mysites)
- (sites lambdapi))
+ (action (run dream_eml %{deps} --workspace %{workspace_root})))
\ No newline at end of file
From c331b1fe70708c658f82439c7bbd24dd51f895e4 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA
Date: Mon, 10 Nov 2025 11:23:51 +0100
Subject: [PATCH 46/58] update dependencies and description header
---
dune-project | 1 +
lambdapi.opam | 1 +
ressources/description.html | 153 +++++++++++++++++++++++++++---------
3 files changed, 118 insertions(+), 37 deletions(-)
diff --git a/dune-project b/dune-project
index 24e32cc7b..9f81fd377 100644
--- a/dune-project
+++ b/dune-project
@@ -47,6 +47,7 @@ systems: Dedukti, Coq, HRS, CPF.")
(odoc :with-doc)
(lwt_ppx (>= 1))
(uri (>= 1.1))
+ (dune-site (>= 3.15))
)
(sites (share server_resources))
)
diff --git a/lambdapi.opam b/lambdapi.opam
index 2e65966cd..c6af8dded 100644
--- a/lambdapi.opam
+++ b/lambdapi.opam
@@ -38,6 +38,7 @@ depends: [
"odoc" {with-doc}
"lwt_ppx" {>= "1"}
"uri" {>= "1.1"}
+ "dune-site" {>= "3.15"}
]
build: [
["dune" "subst"] {dev}
diff --git a/ressources/description.html b/ressources/description.html
index ea4e7e04a..f148cef5a 100644
--- a/ressources/description.html
+++ b/ressources/description.html
@@ -1,38 +1,117 @@
+
-
-
- The search button answers the query. Read the
- query language specification to learn about the query language.
- The query language also uses the
- Lambdapi terms syntax.
- while supporting a subset of the Rocq syntax (specificaly,
- terms using fun, forall, exists, /\ and ~ are allowed)
- In particular, the following constructors can come handy for
- writing queries:
-
-
-
an anonymous functionλ (x:A) y z,t
- mapping x, y
- and z (of type A for x) to t.
-
a dependent product
- forall (x:A) y z,T
-
-
a non-dependent product A -> T
- (syntactic sugar for forall x:A,T when
- x does not occur in T)
+ The search button answers the query. Read the
+ query language specification to learn about the query language.
+ The query language also uses the
+ Lambdapi terms syntax.
+ while supporting a subset of the Rocq syntax (specificaly,
+ terms using fun, forall, exists, /\ and ~ are allowed)
+ In particular, the following constructors can come handy for
+ writing queries:
+
+
+
an anonymous functionλ (x:A) y z,t
+ mapping x, y
+ and z (of type A for x) to t.
+
a dependent product
+ forall (x:A) y z,T
+
+
a non-dependent product A -> T
+ (syntactic sugar for forall x:A,T when
+ x does not occur in T)