Term transformation helper function

[gabrielhdt]

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.

[francoisthire]

Should it be called LpMeta? 😁

[fblanqui]

Why not using parse_string instead?

[gabrielhdt]

Well we don't have a parse_term yet, we can only parse complete commands (unless we use

lambdapi/tests/rewriting.ml

Line 6 in c1337fd

let parse_term s =

)

[fblanqui]

Which equality is used here?

[gabrielhdt]

I use syntactic equality (the infamous Rewrite.eq): we don't want to use convertibility since we want to make sure that a rewrite step is done.

[fblanqui]

@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]

@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.

[gabrielhdt]

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.

[fblanqui]

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.

[gabrielhdt]

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.