Deducteam
Term transformation helper function
Introduce a function that allows to rewrite a term with a specific set of rewrite rules. In particular, it may be used to implement tactics that transform terms.
@gabrielhdt How do you plan to introduce in LP the rules you want to use? If I remember well, dkmeta takes as argument some file f_in.dk and some set of rules R (in another file rules.dk?), and generate a new file f_out.dk obtained from f_in.dk by replacing every term by its normal form wrt R. @francoisthire Is it right?
@gabrielhdt How do you plan to introduce in LP the rules you want to use? If I remember well, dkmeta takes as argument some file f_in.dk and some set of rules R (in another file rules.dk?), and generate a new file f_out.dk obtained from f_in.dk by replacing every term by its normal form wrt R. @francoisthire Is it right?
IMO the first step is to provide a convenient caml API, so that we may write rules in ocaml (possibly using parse_string or whatever).
Then we may provide a binary. In the case of a binary, we may provide a file containing only rewrite rules which are evaluated after the evaluation of the input, so that the rewrite rules are scoped with the signature state of the input. We can also provide lambdapi code as command line arguments, if we have few rewrite rules (à la lisp, we could invoke echo ... | lpmeta --eval 'rule impd A (λ _, $B.[]) ↪ imp A $B.[];'). Regarding input and output, IMHO the cleanest way is to implement a filter that reads on stdin and writes on stdout.
I'll try to use these features on https://github.com/Deducteam/personoj/tree/devel/proofs/psnj_toolbox soon enough, so we may have a practical feedback.
We may also be more general, and allow to evaluate any command once the input is parsed. This would allow for instance to declare a symbol abst and a rewrite rule λ x: $a, $t.[x] ↪ abst $a (λ y: $a, $t.[y]).
Edit: this will obviously not work since the rule is non terminating
A possible implementation of LpMeta may behave as specified by the following test file https://github.com/Deducteam/personoj/blob/48d580f39975292ae8ad5af9136f19b56a324b44/proofs/psnj_toolbox/test/qfo/qfo.t where the binary lpmeta is called psnj qfo (for historical reasons, it should be changed). The synopsis is
lpmeta [--e LP] [--eval LP] [--load FILE] [--meta-eval LPM] [-m LPM] [--meta-load MFILE]
to evaluate the lambdapi commands LP (in the order they appear), evaluate the lambdapi file FILE, read and parse standard input, evaluate meta rewrite rules LPM, evaluate meta rewrite rules in file MFILE and finally normalise the types of the command given on standard input and print them to standard output.
Gabriel, do you want to rewrite dk files only, or lp files also? If you want to rewrite dk files only, there is something easy to do now that lambdapi can generate dk files: we could add an option --normalize-with file and use the rules defined in file to normalize the terms before outputing them. If needed, we could also add an unsafe modifier for the rule command for not checking SR.
Well for the moment it's rather only an API, so it allows to rewrite terms, and not file or signature. But rewriting files or signature should only depend on the printer used, right? So I'd say that it is orthogonal. The updated version of the specification of the previously mentioned tool psnj meta is here, it rewrites the type of symbol declarations with respect to a set of rewrite rules.