Hi everyone !
(this is a bit of a follow-up from https://coq.discourse.group/t/use-notations-to-define-an-embedded-language-inside-coq/703 but with a more specific problem)
I’m using the Coq notations (an custom expressions) to embed a small functional language (like STLC). I struggle with the definition of a function that takes an argument.
To make the language more user-friendly I would like the notations to allow for arbitrary names of arguments, that would then be substituted by the notation system to the actual internal representation of variables (in my case, integers).
A simple example would be:
Notation "'fun' f ( x ) = t" :=
(let x := (fvar 0) in
(lambda_function t))
(in custom expr, f ident, x ident, t custom expr)
This works nicely for substituting x with fvar 0 (free variable 0) inside the term lambda_function t that would otherwise contain an unbounded reference to x.
However I have a problem when several functions are nested: I should be able to assign a different number to each argument. What I want is technically the following:
... (let x:= (fvar [fresh_number computed using t]) in ...
But the problem I have is that t contains unbounded references to x so I cannot use the functions that I have for computation of free variables.
On exponential way of doing it is to temporarily set x to 0 in t, compute the free variables, take the max, and set set x back to max + 1:
Notation "'fun' ( x ) => t" :=
(let t0 := (let x := (fvar 0) in t) in
let fresh := (max (free_vars t0)) + 1 in
let x := (fvar fresh) in
lambda_function t)
(in custom expr, x ident, t custom expr).
Where t0 is a temporary t[x → (fvar 0)] that is used for computing the free variables and then discarded.
So my question is the following: what options would you suggest I could use to deal with this ?
I was thinking of using a random number (does not seem a good idea), compute a number from the string identifier of the argument x (no idea how to do that), compute a number from the level of recursion of the parsing (if that’s possible) or use some Ltac2 subst magic that I do not understand.
Thank you very much !