Today I was inspired by this comment of @herbelin to try and embed a programming language that supports pattern matching of product types in Coq using the PHOAS method. And of course, this needs to come with some reasonable notations.
So, I’m starting with a simple PHOAS encoding of lambda calculus with products types, that can be pattern matched in
From Ltac2 Require Import Ltac2. Section term. Variable X : Type. Inductive prod_pattern := leaf | ppair (l r : prod_pattern). Fixpoint p2p p : Type := match p with | leaf => X | ppair l r => p2p l * p2p r end. Inductive term : Type := | Var (x : X) | App (x y : term) | Prod (x y : term) | Lam p (f : p2p p -> term).
Now I want to create some notations for this, such as
[λ (a, (b, c)), a b]. This notation should elaborate to
Lam (ppair leaf (ppair leaf leaf)) (fun '(a, (b, c)) => a b). This is a bit of a problem though, because the
(a , (b, c)) part of the notation needs to generate both
ppair leaf (ppair leaf leaf) and the real Coq pattern
'(a, (b, c)). This is problematic, because
patterns need to be applicative in Coq, and cannot be computed within the notation. I came up with a solution using Ltac that converts a nested products to
Ltac to_pattern x := match x with | (?x , ?y) => let a := to_pattern x in let b := to_pattern y in constr:(ppair a b) | _ => constr:(leaf) end. Notation "[ 'λ' pat , k ]" := (Lam ltac:(let r := to_pattern pat in exact r) (fun pat => k)) (at level 0, pat pattern, only parsing).
Crazily, this actually almost works! The only problem is that when the
ltac part gets evaluated, the system tries to resolve the
binders in the pattern, and errors out:
Definition test := [λ (a, (b, c)) , App (Var a) (Var b)]. (* The variable a was not found in the current environment. *)
This can be solved by introducing some bogus variables:
Section test. Variable a b c d e f : X. Definition test := [λ (a, (b, c)) , App (Var a) (Var b)]. End test. Print test. (* test = Lam (ppair leaf (ppair leaf leaf)) (fun '(a, (b, _)) => App (Var a) (Var b)) : term *)
I tried if Ltac2 may be better suited for this problem because it appears to be working on preterms, but something as simple as the following already errors out:
Notation "[[ 'λ' pat , k ]]" := (Lam ltac2:(exact leaf) (fun pat => k)) (at level 0, pat pattern, only parsing). Check [[λ a, Var a]]. (* Missing notation term for variable k, probably an ill-typed expression *)
Does anybody have a better solution for this problem?