Improvements and new features for indexing

CHANGES.md

@@ -7,6 +7,15 @@ 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.
+- Added filtering of search results using regular expressions.
+- 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.
 - Decimal numbers can now be qualified by a module path so that one can use the decimal notation with different types in the same file.
 
 ### Changed
@@ -17,6 +26,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Syntax: do not identify {|a|} and a when a is a regular identifier anymore.
 - Dedukti export: translate a module path A.B.C to C, and check that C is a valid module name in Dedukti.
 - LSP server: Position of the error is removed from diagnostics when the error occurs in the file currently open in the editor.
+- Syntax of search query is modified as follows : `in` is used instead of `|` (filtering). `with` is used instead of `,` (conjunction). `|` is used instead of `;` (disjunction)
 
 ### Fixed
 

TODO.md

@@ -4,19 +4,89 @@ TODO
 Index and search
 ----------------
 
-* Too many results found?
+* @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
 
-anywhere >= (Π x: _, (= _ V# V#))
-anywhere >= (Π x: _, (= _ x x))
+* @abdelghani
+  - (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)
 
-* html tags in textual output :-(
+* syntactic sugar for regular expressions / way to write a regular
+  expression - only query efficiently
+    (concl = _ | "regexpr")
+
+* normalize queries when given as commands in lambdapi
+
+* 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
+-----------
+
+* 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,
   in particular when searching as a lambdapi command?
 
-* normalize queries when given as commands in lambdapi
+* package management
+
+* update index / deindex (it should work at package level)
+
+* more external sources when showing query results, including Git repos
+
+* 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?
+
+* ranking
+
+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
+
+Documentation
+-------------
+
+* document the Coq syntax:  ~ /\ \/ -> = forall exists fun
+
+* 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 ="
+
+* document new features, e.g. -sources (and find better
+  terminology), deindex
+
+* 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! ]
+
+* Misleading output for:
 
-* alignments with same name ==> automatic preference?
+  anywhere >= (Π x: _, (= _ V# V#))
+  anywhere >= (Π x: _, (= _ x x))
 
-* better pagination
+  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.

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.
@@ -44,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:**
 
@@ -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 prefix of symbol paths to be removed from the index.
+  That prefix is not checked for well-formedness (i.e. A.B matches A.BC).
+  For instance, `lambdapi deindex --path tests.OK.natural`` removes from the index all the symbols
+  whose path starts with `tests.OK.natural` like `tests.OK.natural.N`.
+
 export
 ------
 
@@ -174,6 +183,9 @@ index
 
 * ``--db <FILE.db>`` tells lambdapi to index symbols and rules in ``<FILE.db>`` 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
 -----------------
 
@@ -191,7 +203,7 @@ search
 
 * ``--rules <LPSearch.lp>`` tells lambdapi to normalize terms in the query using the rules given in the file ``<LPSearch.lp>``. 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 <FILE.lp>`` requires and open ``<FILE.lp>`` when starting the search engine. The file can be used for example to specify implicit arguments for symbols used in the queries.
+* ``--require <FILE.lp>`` requires and opens ``<FILE.lp>`` when starting the search engine. The file can be used for example to specify implicit arguments for symbols used in the queries.
 
 * ``--db <FILE.db>`` tells lambdapi to search in ``<FILE.db>`` instead of ``~/.LPSearch.db``.
 

doc/queries.rst

@@ -109,8 +109,10 @@ beginning, the timeout is set to 2s.
 ``search``
 ------------------
 
-Runs a query between double quotes against the index file
-``~/.LPSearch.db``. See :doc:`query_language` for the query language
+Runs a query between double quotes against the index file updated
+with the assets defined in the file under development including the
+assets imported by the `require` commands.
+See :doc:`query_language` for the query language
 specification.
 
 ::

doc/query_language.rst

@@ -7,7 +7,7 @@ Queries can be expressed according to the following syntax:
 
    Q ::= B | Q with Q | Q|Q | Q in PATH
    B ::= WHERE HOW GENERALIZE? PATTERN
-   PATH ::= << string >>
+   PATH ::= <identifier> | "<regexp>"
    WHERE ::= name | anywhere | rule | lhs | rhs | type | concl | hyp | spine
    HOW ::= > | = | >= | ≥
    GENERALIZE ::= generalize
@@ -19,10 +19,12 @@ 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:
 
-* a query ``Q`` is either a base query ``B``, the conjunction ``Q1 with Q2`` of two queries ``Q1`` and ``Q2``, their disjunction ``Q1 | Q2`` or the query ``Q in 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 with Q2`` of two queries ``Q1`` and ``Q2``, their disjunction ``Q1 | Q2`` or the query ``Q IN 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``).
@@ -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) with hyp >= (list nat)``
@@ -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``

dune-project

@@ -46,6 +46,7 @@ systems: Dedukti, Coq, HRS, CPF.")
   (odoc :with-doc)
   (lwt_ppx (>= 1))
   (uri (>= 1.1))
+  (dune-site (>= 3.15))
   (ppx_inline_test (>= v0.17))
  )
  (sites (share server_resources))

lambdapi.opam

@@ -40,6 +40,7 @@ depends: [
   "odoc" {with-doc}
   "lwt_ppx" {>= "1"}
   "uri" {>= "1.1"}
+  "dune-site" {>= "3.15"}
   "ppx_inline_test"
 ]
 build: [

ressources/description.html

@@ -0,0 +1,117 @@
+<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.5.0/css/all.min.css">
+
+<style>
+    .snippet {
+      border: 1px solid grey;  /* Bordure grise */
+      color: red;              /* Texte en rouge */
+      padding: 0 3px 0 3px;           /* Espace autour du texte à l'intérieur de la bordure */
+      line-height: 1.6;
+    }
+    code {
+      font-family: "Courier New", Courier, monospace;
+      background-color:rgb(8, 8, 8);
+      padding: 2px 4px;
+      border-radius: 4px;
+      color:rgb(43, 230, 52);
+      font-size: 1.3em;
+      white-space: normal;
+    }
+    #description {
+      margin-top: 10px;
+      padding: 10px;
+      background-color: #f0f0f0;
+      border: 1px solid #ccc;
+    }
+    button {
+      width: 100%;
+      cursor: pointer;
+      /* margin-top: 10px; */
+      /* padding: 10px; */
+      background-color: #f0f0f0;
+      border: 1px solid #ccc;
+    }
+    .header {
+      position: relative; /* Conteneur pour les liens */
+      width: 100%;
+      height: 80px;
+      background-color: #f1f1f1;
+    }
+    .top-right-link {
+      position: absolute;
+      top: 10px;
+      right: 10px;
+      text-decoration: none;
+      background-color: #007BFF;
+      color: white;
+      padding: 10px 20px;
+      border-radius: 5px;
+      font-size: 18px;
+      text-align: center;
+    }
+    .top-right-link span {
+      display: block;
+      font-size: 12px;
+    }
+    .top-right-link:hover {
+        background-color: #0056b3;
+    }
+    .top-left-link {
+      position: absolute;
+      top: 10px;
+      left: 10px;
+      text-decoration: none;
+      background-color: #007BFF;
+      color: white;
+      padding: 10px 20px;
+      border-radius: 5px;
+      font-size: 18px;
+      text-align: center;
+    }
+    .top-left-link span {
+      display: block;
+      font-size: 12px;
+    }
+    .top-left-link:hover {
+        background-color: #0056b3;
+    }
+</style>
+
+<div class="header">
+    <a href="https://github.com/Deducteam/lambdapi/issues/new" target="_blank" class="top-right-link"><span>Something went wrong?</span>Open an issue</a>
+    <a href="https://github.com/Deducteam/lambdapi/discussions/1214" target="_blank" class="top-left-link"><span>Like this tool?</span>Join the discussion</a>
+    <h1 style="text-align: center;"><a href="https://github.com/Deducteam/lambdapi">LambdaPi</a> Search Engine</h1>
+</div>
+
+<div id="descriptionSection" style="display: %%HIDE_DESCRIPTION%%;">
+
+
+  <p>
+      The <b>search</b> button answers the query. Read the <a href=
+      \"https://lambdapi.readthedocs.io/en/latest/query_language.html\">
+      query language specification</a> to learn about the query language.
+      <br>The query language also uses the <a
+      href=\"https://lambdapi.readthedocs.io/en/latest/terms.html\">
+      Lambdapi terms syntax</a>.<br>
+      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:<br>
+  </p>
+  <ul>
+      <li>an anonymous function<span class=\"snippet\">λ (x:A) y z,t</span>
+      mapping <span class=\"snippet\">x</span>, <span class=\"snippet\">y
+      </span> and <span class=\"snippet\">z</span> (of type <span class=\"
+      snippet\">A</span> for <span class=\"snippet\">x</span>) to <span
+      class=\"snippet\">t</span>.</li>
+      <li>a dependent product
+        <span class=\"snippet\">forall (x:A) y z,T</span>
+      </li>
+      <li>a non-dependent product <span class=\"snippet\">A -> T</span>
+        (syntactic sugar for <span class=\"snippet\">forall x:A,T</span> when
+        <span class=\"snippet\">x</span> does not occur in <span class=
+        \"snippet\">T</span>)</li>
+  </ul>
+
+</div>
+
+</script>

ressources/dune

@@ -0,0 +1,19 @@
+(library
+ (name ressources)
+ (public_name lambdapi.ressources)
+ (modules :standard)
+ (libraries lambdapi.parsing lambdapi.core dream unix dune-site)
+ (preprocess (pps lwt_ppx))
+)
+
+(install
+ (section (site (lambdapi server_resources)))
+ (files
+  (description.html as default/description.html)
+  (lambdapi.ico as default/lambdapi.ico)
+ )
+)
+
+(generate_sites_module
+ (module mysites)
+ (sites lambdapi))

src/cli/config.ml

@@ -109,7 +109,7 @@ let map_dir : (Path.t * string) list CLT.t =
   let mod_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, err_desc) -> Error(`Msg(s ^ "\n" ^ err_desc))
     in
     let print fmt p = Path.pp fmt p in
     Arg.conv (parse, print)

src/cli/dune

@@ -4,5 +4,4 @@
  (modes byte native)
  (modules :standard)
  (libraries cmdliner lambdapi.lsp lambdapi.tool lambdapi.handle
-            lambdapi.export unix)           
-)
+            lambdapi.export unix ressources))