Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Indexing and search for LambdaPi (Deducteam#982)
This PR adds: - indexing and search commands in the CLI, as queries and provided by a webserver - a query language to compose basic queries - new options --no-sr-check, --rules, --port - the record type Eval.config is extended with a new field allowing to specify which dtree to use for each symbol The last two modifications allow to later implement something similar to [dkmeta](https://github.com/Deducteam/dkmeta) in lambdapi. TODO: - [x] CI fails with ocaml < 4.14.1 - [x] update CHANGES.md - [x] update AUTHORS.md - [x] @fblanqui test locate/search/search-query commands (VSCode is broken again for me) - [x] update emacs and vscode - [x] doc --no-sr-check - [ ] @fblanqui reorganize options.rst with a section for each command ? - [x] @sacerdot add examples in doc/query_language.rst - [x] update comments of modified functions - [x] make sanity_check - [x] update BNF - [x] update doc of command line arguments - [x] update doc of lambdapi queries - [x] add comment in doc that results of search may be not well typed - [x] fix hard-coded string "LPSearch" in parse_term_string in lambdapi.ml: I have nothing better to put there, it stays like that - [x] fix hard-coded Indexing.dbpath and meta-rules file - [x] add option --meta-rules for reading file LPSearch.lp - [x] rename command resolve by locate - [x] put keywords in alphabetic order - [x] replace assert false by fatal whenever possible - [x] in lambdapi.ml, locate_cmd should take an identifier and not a string - [x] replace LPSearch.dk by LPSearch.lp - [x] when reading LPSearch.lp, fail if an identifier is not qualified - [x] allow the search query in the middle of a proof, using the variables of the proof context; turn metavariables into patterns? - [x] be sure to quote all dedukti/lambdapi snippets that are pasted to the web page - [x] add cli/query command for the query language - [x] remove "search" in favour of the query language? (maybe yes) same for locate? (probably not) - [x] allow to start the webserver on a different port - [x] rename the webserver to websearch - [x] branch the query language doc to the main doc - [x] test indexing and search on lambdapi files (in particular test path restriction of the query language) index file: - define a default place for the index files, for instance ~/.lambdapi/LPSearch.db and ~/.lambdapi/LPSearch.lp - better: use dune site for use opam compatible places future work (not for this PR): - [ ] remove fix in pos.ml for handling Deducteam#1001 - [ ] add rules to undo HOL encoding - [x] add a query language - [ ] more WHEN/HOW specifications? (e.g. in conclusion or spine) - [x] more precise matching information (in particular: in conclusion/hypothesis) - [ ] even more precise information: in conclusion of hypothesis - [x] for more precise results, allow a variant of index-matching where an IHOLE can be matched only by an IVar; this "undoes" the "modus ponens" step used during indexing - [ ] order search results according to precision of the matching (larger patterns) or other criteria ----------------------------------------- commits: * Scoping functions generalized over symbol identifiers * First index/search cli-commands implemented - lambdapi index FILES creates a LPSearch.db index file in current dir - lambdapi resolve name resolves the name using the index - lambdapi search interactively asks for queries resolved using the index; the query are term patterns (use _ for holes) * New Dedukti queries search and resolve To be fixed: - where/when to write LPSearch.db * DB made lazy and loaded from disk when needed The path "LPSearch.db" in the current dir is still hard-coded * Debugging code removed * TO BE REVISED: added parser for terms - used for "lambdapi search term" - a functor would be more appropriate to allow to parse more grammar entries uniformly * Interface minimized * Preliminary work to index more E.g. to index the body, to index subterms, etc. * added is_vari * Indexing subterms of types of symbols * Bug fixed: "lambdapi index" was adding to the index The fix empties the index just before. * fix line lengths for make sanity_check to pass * add option --no-sr-check * Ready to index rules as well * Implemented meta-rewriting rules - for now used only on the type of constants to be indexed - the rules can be untyped and be defined on symbols not declare yet * Lhs/Rhs of rules indexed * Code refactoring - Pure has no references - DB manages the global reference - Code outside is high level code to index signatures and process queries * Disable warnings during compilation * Semantics of matching during indexing changed - patterns $_.[...] are now the placeholders both in queries and in types/rules - when going under a pi, variables are turned into placeholders KNOWN BUG: variables should be turned into placeholders only in spines * BUG FIXED: replace vars with placeholders in spine only * dbpath/rwpath hardcoded * lambdapi index --add adds the file to the index WARNING: it does not check if the files was already added * resolve renamed to locate everywhere * warning improved * sanity * update doc and bnf * Do not expand during normalization + better flexibility check * LPSearch.dk to undo the encoding * Line commented out by mistake * Duplicated code generalized * Code simplified and ready to be generalized - subterms_to_index now returns pairs where/what - used also to index the whole term * item type refined to have more informations on the location * Locate/search queries now return a set in place of a list This is a preliminary step to define a query language based on operations on sets. * BUG fixed - introduced by last commit - find_sym must be the identity of qualified names, as it used to be * New option holes_in_index to search (defaults to false) - when holes_in_index is false, search behaves as if the indexed symbols where applied to prove the current goal, i.e. pi-quantifications in the spine are eliminated using holes (~metavariables) * For lhs/rhs it makes no sense to handle them as spines - pi-generalization is disabled for lhs/rhs - the position information degenerates to Exact/Inside * Doc fixed * Added V# as a pattern that matches only variables. * Check that all assert false must remain so + code cleanup * Restore alphabetic order * lamdapi cli: accept only non-qualified identifiers for locate * LPSearch.dk => LPSearch.lp (with change of syntax) * Allow to use variables in scope in searches during a proof. * Allow meta-variables in search patterns WARNING: meta-variables seem to be bugged/unusable in lambdapi at the moment. This feature cannot be tested * Removed unused field problem This is some hand-made cherry-picking from the main branch, to avoid several conflicts * lambdapi webserver implemented * Nice printing of snippets in HTML * Localize symbol declarations In case of definitions, only the declaration part is localized * webserver documented * added dream and lwt_ppx dependencies * Fix --help for locate/search I finally understood how to have mandatory positional arguments with cmdliner * deref generalized to accomodate plain text * Enable code snippets for textual search as well * Painful code factorization between txt/html queries * hide function * code cleanup * - rename holes_in_index in generalize - update BNF script and grammar - add temporary fix for Deducteam#1001 - fix code in tests/kernel.ml and tests/rewriting.ml * details * remove version constraints on lwt_ppx and dream * Definition of a basic query language * Add path to Xhs * reformatted * syntax fixed * Code refactoring (big change) An ItemSet is now a map from items (i.e. sym_name * pos) to a list of positions. The base query involved in the position is not recorded yet. The next step is to add it in order to understand the output in case of union/intersection. * fix doc * WiP: syntax for the query language - name: id - XXX: pattern - "," and ";" for conjunction/disjunction - "|" for filtering * Bug fixed: arguments swapped in search query filtering * Bug fix + WiP in query language - WiP: more syntax allowed - Bug fix: filtering was expecting only one position after base query, which is not an invariant * New syntax for search queries: :/=/~ for the position to match * Only "type:" makes sense: "type=" and "type~" don't * Record the base queries in the answer * Pretty-print terms without fully qualifying identifiers on demand. Used to print query patterns * allow to specify generalization in base queries * print when the term occurs potentially generalized * Link to the github * document the query language * more checks that make sense * doc improved * form improved * search-query cli command added and documented * search-query query added Untested: VSCode is broken again for me Warning: I am following a non-orthodox approach to avoid polluting LambdaPI code everywhere. The query takes a string that is later scoped/handled by my code * query commands documented * BNF updated automatically * add doc for --no-sr-check * update editors * SEARCHQUERY -> SEARCH_QUERY * update auhors * HTML-escaping of snippets * Complete and improved html escaping It uses an higher-order polymorphic pretty-printer * More readable output * webserver renamed to websearch * Add --port option to websearch * deref -> print_file_contents * detail * fix index_cmd * --rules option to index * Escaping fixed * Keep the query to remember what you asked for * Allow qualified path prefixes * document --rules * Show something when the list of results is empty * Use =, >, >= and its unicode variant for positions * Improved error reporting in websearch * a few examples added to the doc * fix LPSearch db file name * update doc queries * Bug fixed: locs are in UTF8 codepoint, not chars! * Improved error message * Queries with overloaded symbols now fail The previous behavior was to pick a random interpretation and issue a warning about that. Now we fail and tell the user to use locate to disambiguate the symbol by hand * Red color for all query types * handle_exception used for all commands * Avoid blank lines in HTML output * one end-line was missing * only search_query left, renamed to search * One reference to locate was still there * match ==> anywhere * update editors and doc * update bnf * update CHANGES.md * pos.ml: comment assert String.is_valid_utf_8 * update emacs files * update vscode syntax file * add utf8 string functions missing in ocaml < 4.14.1 * update doc for --rules * indentation * add missing functions in Bytes for OCaml < 4.14.1 * Check for no implicit terms in rhs of indexing rules * detail * doc: add example of index rules * fix doc * add uchar.ml * update vscode json files --------- Co-authored-by: Frédéric Blanqui <frederic.blanqui@inria.fr>
- Loading branch information
