PRFA.tp6c
MPRI PRFA (2-7-2) — Exercise session 6 — Meta-programming (SOLUTIONS)
REMINDER — Syntax of match goal
Ltac my_assumption :=
match goal with
| H : ?A |- ?A ⇒ apply H
end.
Goal ∀ P Q R, P → Q → R → P.
Proof.
intros.
my_assumption.
Qed.
EXERCISE
Define a tactic to perform split repeatedly on goals of the shape A × B
but not on any other kinds of goals (for instance it should not solve True).
For instance, on (nat × bool) × (unit × bool) it should yield 4 subgoals.
Hint: You will need split and match goal or lazymatch goal and idtac.
Try it on these goals.
Goal nat × bool.
Proof.
splits. (* 2 goals *)
Abort.
Goal nat × (bool × unit) × (unit × nat × bool) × unit.
Proof.
splits. (* 7 goals *)
Abort.
NEW TACTIC — clear
It is possible to *forget* about hypotheses using the clear tactic as
follows.
It is sometimes useful before applying the induction tactic to get rid of
something in the generated induction hypothesis.
Goal ∀ P Q R, P → Q → R → P.
Proof.
intros P Q R p q r.
clear Q p q.
Fail clear P. (* Cannot get rid of something used elsewhere. *)
clear. (* Without arguments it clears everything it can *)
exfalso.
clear.
Abort.
EXERCISE
Prove the following by induction on n.
In particular, don't use lia, we want you to use the induction hypothesis.
Goal ∀ n, n mod 14 = 7 → n - n = 0.
Proof.
intros n hn.
clear hn. (* Note that without this, the IH is useless *)
induction n.
- reflexivity.
- cbn. eauto.
Qed.
Proof.
intros n hn.
clear hn. (* Note that without this, the IH is useless *)
induction n.
- reflexivity.
- cbn. eauto.
Qed.
Matching on the type of an expression
The same way we can match on the goal, we can match the type of an expression
using the type of construct.
Ltac handle_hyp h :=
lazymatch type of h with
| (?A × ?B)%type ⇒ destruct h
| nat ⇒ induction h
| _ ⇒ idtac
end.
Goal ∀ (n : nat × nat), fst n = snd n.
Proof.
intro n.
handle_hyp n.
handle_hyp n.
Abort.
NEW TACTIC — fresh
Not all tactics operate on goals, some are used to produce values, or even
names (as in variable names).
This is the case of the fresh tactic which you can use to get a *fresh*
name (as in not used in the currrent context) to give to a newly introduced
variable.
Goal ∀ n m k, n + m - k = m + n - k.
Proof.
let N := fresh in
intro N. (* Here it chooses H, not very cool, we can guide naming a bit *)
let N := fresh "n" in
intro N. (* We suggested n and it stick with it. *)
let N := fresh "n" in
intro N. (* This time, n was already taken, so it chose n0 instead *)
let na := fresh H in
destruct H as [| na]. (* This time we suggested to use the name of H *)
(* It picked H0 *)
Abort.
EXERCISE — Forward reasoning
A very useful tactic that should be part of the standard library, but is not,
is the fwd tactic.
Given H : P → Q, fwd H will yield two goals:
Note that there shouldn't be anything else appearing in the goal.
- one where P must be proven
- and one where H has been replaced by H : Q
Ltac fwd h :=
match type of h with
| ?P → _ ⇒
let h' := fresh in
assert (h' : P) ; [| specialize (h h') ; clear h' ]
end.
Try on the following goal, do not use apply
Goal ∀ P Q R, (P → Q → R) → (P → Q) → P → R.
Proof.
intros P Q R h1 h2 h3.
fwd h2. 1: assumption.
fwd h1. 1: assumption.
fwd h1. 1: assumption.
assumption.
Qed.
Proof.
intros P Q R h1 h2 h3.
fwd h2. 1: assumption.
fwd h1. 1: assumption.
fwd h1. 1: assumption.
assumption.
Qed.
EXERCISE (Harder)
Try to generalise the code for fwd so that you can also provide a tactic.
If H : P → Q then forward_gen H tac will also apply tac to try and
solve the goal P first.
Ltac forward_gen h tac :=
match type of h with
| ?P → _ ⇒
let h' := fresh in
assert (h' : P) ; [ tac | specialize (h h') ; clear h' ]
end.
We define handy notations
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
Goal ∀ P Q R, (P → Q → R) → (P → Q) → P → R.
Proof.
intros P Q R h1 h2 h3.
forward h2 by assumption.
do 2 forward h1 by assumption.
assumption.
Qed.
From PRFA Require Import MetaCoqPrelude.
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
Goal ∀ P Q R, (P → Q → R) → (P → Q) → P → R.
Proof.
intros P Q R h1 h2 h3.
forward h2 by assumption.
do 2 forward h1 by assumption.
assumption.
Qed.
From PRFA Require Import MetaCoqPrelude.
Print Assumptions
In Coq, you have a very useful command which can tell you on which axiom a
given lemma depends.
See how it works below.
Axiom LEM : ∀ (P : Prop), P ∨ ¬ P.
Axiom funext : ∀ A B (f g : A → B), (∀ x, f x = g x) → f = g.
Lemma foo :
(fun n ⇒ n + 0) = (fun n ⇒ n).
Proof.
apply funext. intro. rewrite <- plus_n_O. reflexivity.
Qed.
Print Assumptions foo. (* Only funext is listed. *)
We will now try to implement our own Print Assumptions using MetaCoq.
For this, we need to be able to manipulate not only the term but also its
environment to be able to check its dependencies.
For instance, if we inspect foo above, we need to know that funext is
indeed referring to an axiom, and this information is not contained within
foo itself.
We can use $quote_rec to get both the term and its dependencies as follows:
Definition foo_env :=
let (env, _) := q_foo in env.
Compute lookup_constant foo_env (MPfile ["Peano"; "Init"; "Coq"], "plus_n_O").
This time, cst_body := None. It's an axiom.
To give you inspiration for the rest here is the (deep) identity function on
term.
Fixpoint identity (t : term) :=
match t with
| tRel n ⇒ tRel n
| tVar id ⇒ tVar id
| tEvar ev args ⇒ tEvar ev (map identity args)
| tSort s ⇒ tSort s
| tCast t kind v ⇒ tCast (identity t) kind (identity v)
| tProd na ty body ⇒ tProd na (identity ty) (identity body)
| tLambda na ty body ⇒ tLambda na (identity ty) (identity body)
| tLetIn na def def_ty body ⇒ tLetIn na (identity def) (identity def_ty) (identity body)
| tApp f args ⇒ tApp (identity f) (map identity args)
| tConst c u ⇒ tConst c u
| tInd ind u ⇒ tInd ind u
| tConstruct ind idx u ⇒ tConstruct ind idx u
| tCase ind p discr brs ⇒
let p' := map_predicate id identity identity p in
let brs' := map_branches identity brs in
tCase ind p' (identity discr) brs'
| tProj proj t ⇒ tProj proj (identity t)
| tFix mfix idx ⇒ tFix (map (map_def identity identity) mfix) idx
| tCoFix mfix idx ⇒ tCoFix (map (map_def identity identity) mfix) idx
| tInt i ⇒ tInt i
| tFloat f ⇒ tFloat f
| tArray u arr def ty ⇒ tArray u (map identity arr) (identity def) (identity ty)
end.
EXERCISE
Define a Coq function assumptions : global_env × term → list kername
such that Compute assumptions ($quote_rec f) returns the list of
assumptions (axioms) that f depends on, including recursively.
Note: You cannot convince Coq that it is terminating, so we'll deactivate
termination checking. That's ok when meta-programming.
Hint: You may use the flat_map function too.
Unset Guard Checking.
Section assums.
Context (env : global_env).
Fixpoint assms (t : term) :=
match t with
| tConst c u ⇒
match lookup_constant env c with
| Some body ⇒
match body.(cst_body) with
| None ⇒ [c]
| Some c ⇒ assms c
end
| _ ⇒ []
end
| tRel _ | tVar _ | tSort _ | tInd _ _ | tConstruct _ _ _ | tInt _ | tFloat _ ⇒ []
| tEvar ev args ⇒ flat_map assms args
| tCast t kind v ⇒ assms t ++ assms v
| tProd na ty body ⇒ assms ty ++ assms body
| tLambda na ty body ⇒ assms ty ++ assms body
| tLetIn na def def_ty body ⇒ assms def ++ assms def_ty ++ assms body
| tApp f args ⇒ assms f ++ flat_map assms args
| tCase ci type_info discr branches ⇒
assms discr ++ flat_map (fun b ⇒ assms b.(bbody)) branches
| tProj proj t ⇒ assms t
| tFix mfix idx ⇒ flat_map (fun d ⇒ assms d.(dbody)) mfix
| tCoFix mfix idx ⇒ flat_map (fun d ⇒ assms d.(dbody)) mfix
| tArray u arr def ty ⇒ flat_map assms arr ++ assms def ++ assms ty
end.
End assums.
Set Guard Checking.
Definition assumptions p :=
assms p.1 p.2.
Compute assumptions ($quote_rec 0).
Compute assumptions ($quote_rec foo).
Definition bar : nat :=
let x := foo in
139.
Compute assumptions ($quote_rec bar).
Module test.
Require Import Classical.
Lemma DNE P : ~~ P → P.
Proof.
tauto.
Qed.
End test.
Compute assumptions ($quote_rec test.DNE).
Definition more_deps :=
(bar, test.DNE, LEM).
Compute assumptions ($quote_rec more_deps).
ALTERNATIVE
Definition assum_fold env : fold_handler (list kername) :=
fun t a k ⇒
match t with
| tConst c u ⇒
match lookup_constant env c with
| Some body ⇒
match body.(cst_body) with
| None ⇒ c :: a
| Some c ⇒ k a c
end
| _ ⇒ []
end
| _ ⇒ k a t
end.
Definition assumptions_alt p : list kername :=
tm_fold (assum_fold p.1) [] p.2.
Compute assumptions_alt ($quote_rec 0).
Compute assumptions_alt ($quote_rec foo).
Compute assumptions_alt ($quote_rec bar).
Compute assumptions_alt ($quote_rec test.DNE).
Compute assumptions_alt ($quote_rec more_deps).
fun t a k ⇒
match t with
| tConst c u ⇒
match lookup_constant env c with
| Some body ⇒
match body.(cst_body) with
| None ⇒ c :: a
| Some c ⇒ k a c
end
| _ ⇒ []
end
| _ ⇒ k a t
end.
Definition assumptions_alt p : list kername :=
tm_fold (assum_fold p.1) [] p.2.
Compute assumptions_alt ($quote_rec 0).
Compute assumptions_alt ($quote_rec foo).
Compute assumptions_alt ($quote_rec bar).
Compute assumptions_alt ($quote_rec test.DNE).
Compute assumptions_alt ($quote_rec more_deps).
EXERCISE
Define a function which replaces any subterm of the form a × b + c with
muladd a b c defined below.
Hint: You can use u == v to check whether u and v are equal terms
(it returns a boolean).
Definition muladd a b c :=
a × b + c.
Fixpoint fold_muladd (t : term) :=
match t with
| tApp p ([ tApp m [ a ; b ] ; c ] as args) ⇒
if (p == $quote plus) && (m == $quote mult)
then tApp ($quote muladd) [ fold_muladd a ; fold_muladd b ; fold_muladd c ]
else tApp (fold_muladd p) (map fold_muladd args)
| tApp f args ⇒ tApp (fold_muladd f) (map fold_muladd args)
| tRel n ⇒ tRel n
| tVar id ⇒ tVar id
| tEvar ev args ⇒ tEvar ev (map fold_muladd args)
| tSort s ⇒ tSort s
| tCast t kind v ⇒ tCast (fold_muladd t) kind (fold_muladd v)
| tProd na ty body ⇒ tProd na (fold_muladd ty) (fold_muladd body)
| tLambda na ty body ⇒ tLambda na (fold_muladd ty) (fold_muladd body)
| tLetIn na def def_ty body ⇒ tLetIn na (fold_muladd def) (fold_muladd def_ty) (fold_muladd body)
| tConst c u ⇒ tConst c u
| tInd ind u ⇒ tInd ind u
| tConstruct ind idx u ⇒ tConstruct ind idx u
| tCase ind p discr brs ⇒
let p' := map_predicate id fold_muladd fold_muladd p in
let brs' := map_branches fold_muladd brs in
tCase ind p' (fold_muladd discr) brs'
| tProj proj t ⇒ tProj proj (fold_muladd t)
| tFix mfix idx ⇒ tFix (map (map_def fold_muladd fold_muladd) mfix) idx
| tCoFix mfix idx ⇒ tCoFix (map (map_def fold_muladd fold_muladd) mfix) idx
| tInt i ⇒ tInt i
| tFloat f ⇒ tFloat f
| tArray u arr def ty ⇒ tArray u (map fold_muladd arr) (fold_muladd def) (fold_muladd ty)
end.
Check $unquote (fold_muladd ($quote (3 × 2 + 5))).
Check $unquote (fold_muladd ($quote (1 + (3 × 2 + 5)))).
Check $unquote (fold_muladd ($quote ((9 × 2 + 0) × (1 + (3 × 2 + 5)) + 1 + (3 × 2 + 5)))).
ALTERNATIVE VERSION
Definition muladd_handler : tm_handler :=
fun t k ⇒
match t with
| tApp p [ tApp m [ a ; b ] ; c ] ⇒
if (p == $quote plus) && (m == $quote mult)
then k (tApp ($quote muladd) [ a ; b ; c ])
else k t
| _ ⇒ k t
end.
Definition fold_muladd_alt :=
transform muladd_handler.
Check $unquote (fold_muladd_alt ($quote (3 × 2 + 5))).
Check $unquote (fold_muladd_alt ($quote (1 + (3 × 2 + 5)))).
Check $unquote (fold_muladd_alt ($quote ((9 × 2 + 0) × (1 + (3 × 2 + 5)) + 1 + (3 × 2 + 5)))).
fun t k ⇒
match t with
| tApp p [ tApp m [ a ; b ] ; c ] ⇒
if (p == $quote plus) && (m == $quote mult)
then k (tApp ($quote muladd) [ a ; b ; c ])
else k t
| _ ⇒ k t
end.
Definition fold_muladd_alt :=
transform muladd_handler.
Check $unquote (fold_muladd_alt ($quote (3 × 2 + 5))).
Check $unquote (fold_muladd_alt ($quote (1 + (3 × 2 + 5)))).
Check $unquote (fold_muladd_alt ($quote ((9 × 2 + 0) × (1 + (3 × 2 + 5)) + 1 + (3 × 2 + 5)))).
Let's go back to Ltac for a bit
EXERCISE
Expand the my_tauto tactic below so that it solves the following goals.
Ltac my_tauto :=
lazymatch goal with
| h : ?P |- ?P ⇒ exact h
| |- True ⇒ constructor
| |- _ ∧ _ ⇒ split ; my_tauto
| |- _ → _ ⇒ intro ; my_tauto
| h : False |- _ ⇒ destruct h
| h : _ ∧ _ |- _ ⇒ destruct h ; my_tauto
| h : _ ∨ _ |- _ ⇒ destruct h ; my_tauto
| h1 : ?P → ?Q, h2 : ?P |- _ ⇒ specialize (h1 h2) ; my_tauto
| |- _ ∨ _ ⇒ (left ; my_tauto) || (right ; my_tauto)
end.
Section Tauto.
Variables (P Q R : Prop).
Goal P → True ∧ True.
Proof.
my_tauto.
Qed.
Goal P → P.
Proof.
my_tauto.
Qed.
Goal P → (P → R) → R.
Proof.
my_tauto.
Qed.
Goal False ∨ True.
Proof.
my_tauto.
Qed.
Goal (P ∨ Q ∨ False) ∧ (P → Q) → True ∧ (R ∨ Q).
Proof.
my_tauto.
Qed.
End Tauto.
Some more MetaCoq
EXERCISE
Write a command reify that turns a Coq expression of type nat into an
expression of the following datatype.
Expressions that do not start with + or × are refied as constants.
Inductive arith :=
| aPlus : arith → arith → arith
| aTimes : arith → arith → arith
| aConst : nat → arith.
Fixpoint reify (t : term) :=
match t with
| tApp c [ u ; v ] ⇒
if c == $quote plus then tApp ($quote aPlus) [ reify u ; reify v ]
else if c == $quote mult then tApp ($quote aTimes) [ reify u ; reify v ]
else tApp ($quote aConst) [t]
| _n ⇒ tApp ($quote aConst) [t]
end.
Goal 4 × (9 + 12) + (3 + 1 × 7) = 2.
Proof.
match goal with
| [ |- ?L = _ ] ⇒
let x := eval cbv in $unquote (reify ($quote L)) in
pose x
end.
Abort.
ADVANCED EXERCISE
Write a meta-program that takes a definition potentially using an axioms and
a proof of said axiom to produce a new definition, equal to the original one
expcet that uses of the axioms are replaced by the proof.
The axiom to be replaced is going to be given as a kername, like those
collected by assumptions.
You don't actually have to verify that the constant is indeed an axiom.
Hint: You will need eq_constant.
Definition instantiate_axiom ax prf :=
transform (fun t k ⇒
match t with
| tConst c u ⇒
if eq_constant ax c then prf
else k t
| _ ⇒ k t
end
).
Axiom mystery : nat.
Definition what :=
mystery × 3.
Compute $unquote (instantiate_axiom ($name mystery) ($quote 10) ($Quote what)).
ADVANCED EXERCISE
A slightly harder version would be to turn a definition using axioms to one
assuming these axioms with an implication.
For instance, for the foo defined above which uses funext, we would expect
something of the following type.
(∀ A B (f g : A → B), (∀ x, f x = g x) → f = g) →
(fun n ⇒ n + 0) = (fun n ⇒ n)
Hint: You can use assumptions and lookup_constant to get the type of a
constant, and lift0 1 t to weaken t by adding one new variable in the
context.
Definition replace_const_lift c u :=
transform_nb (fun nb t k ⇒
match t with
| tConst c' ui ⇒
if eq_constant c c' then (lift0 nb u)
else k nb t
| _ ⇒ k nb t
end
) 0.
Definition unaxiom p :=
let axs := assumptions p in
fold_left (fun t ax ⇒
match lookup_constant p.1 ax with
| Some body ⇒
let ty := body.(cst_type) in
tLam "ax" ty (replace_const_lift ax (tRel 0) t)
| None ⇒ t (* Something wrong, so we just let go *)
end
) axs p.2.
Eval simpl in $unquote (unaxiom ($Quote_rec what)).
Axiom unkown : bool.
Axiom random : nat → nat.
Definition test f :=
if unkown then what else random (f 9).
Eval simpl in $unquote (unaxiom ($Quote_rec test)).
NOTE
This is not recursive! It could be fixed by modifying replace_const_lift
further by also performing lookup_constant and going though constants.
This might have the undesired side effect of unfolding all constants though
so we'll just accept this simple solution for now.
ADVANCED EXERCISE — Deriving
We promised MetaCoq could be used to derive automatically certain things.
Let's see how this can be done by automatically deriving update functions for
a record.
We assume that there is no dependency between the fields, otherwise it's
unclear what an update function should do.
This exercise is hard, so it makes sense to make some assumptions first
such as the absence of parameters (like in triple below) or of local
definitions (like in trap below).
Don't hesitate to ask questions if you are stuck.
We'll start with a few record definitions, together with one example of an
update function, don't hesitate to write your own and quote them to understand
what you need to write.
Record point3D := {
px : nat ;
py : nat ;
pz : nat
}.
Record Zalt := {
num : nat ;
positive : bool
}.
Record triple A B C := {
p1 : A ;
p2 : B ;
p3 : C
}.
Record trap := {
v1 : nat ;
v2 := 10 ^ v1 ;
v3 : nat
}.
We write an update for num by hand.
Definition upd_num (f : nat → nat) (x : Zalt) :=
match x with
| Build_Zalt num positive ⇒ Build_Zalt (f num) positive
end.
match x with
| Build_Zalt num positive ⇒ Build_Zalt (f num) positive
end.
NOTE
There are other ways to write it, but this one might be the easiest to
automate.
Now we can look at how it is quoted.
We use $Quote rather than $quote to unfold the constant upd_num when
quoting it. Otherwise we would get some tConst which is not as informative.
Below is a meta-program that gives you the definition of an inductive.
Hint: It may be useful to you later, perhaps no as-is, but with some
modification to also get the argument of tInd.
Definition get_inductive {A} (ind : A) :=
t <- tmQuote ind ;;
match t with
| tInd ind _ ⇒
let kn := ind.(inductive_mind) in
tmQuoteInductive kn
| _ ⇒ tmFail "Not an inductive type"
end.
t <- tmQuote ind ;;
match t with
| tInd ind _ ⇒
let kn := ind.(inductive_mind) in
tmQuoteInductive kn
| _ ⇒ tmFail "Not an inductive type"
end.
We use it like this to define Zalt_def to inspect at our leisure.
This now contains the definition of Zalt.
You may compare the information you see in here with what appeared in
q_upd_num. It might be useful to copy paste them to better compare.
Print Zalt_def.
SOME TOOLS
To help you build the derive_updates meta-program, we'll give you some
useful tools.
Also check out the following useful constructs:
If you plan to handle parameters:
Handy concatenation notation.
- tmMkDefinition takes a string and a term and produces a definition using that name (if fresh, otherwise it fails) and unquoting the given term.
- tmFreshName takes a string and will return a new string that is fresh in the current environment, based on the given one (typically by adding a number at the end).
- it_mkLambda_or_LetIn takes c : context and t : term and produces a new λ-abstraction with body t and quantifying over c. Basically it does the right thing by inserting as many tLam as necessary.
- subst l 0 t will substitute the variables of t using the terms provided in l. For this exercise, you can provide garbage (just some random tRel k will suffice), what matters is the number of terms you provide. Providing 3 will reduce tRel 5 to tRel 2.
To debug we recommend you use the following in place of tmMkDefinition
mkr 3 2 will produce [ tRel 4 ; tRel 3 ; tRel 2 ]
Extract the name from aname or use d as default.
Definition get_name (a : aname) d :=
match a.(binder_name) with
| nNamed na ⇒ na
| nAnon ⇒ d
end.
Definition has_body (c : context_decl) :=
match c.(decl_body) with
| Some _ ⇒ true
| None ⇒ false
end.
Fixpoint mkargs_aux nargs n args i {struct i} :=
match i, n with
| 0, _ ⇒ []
| S i, Some (S n) ⇒
let l := mkargs_aux nargs (Some n) (tl args) i in
if hd true args then l else tRel i :: l
| S i, Some 0 ⇒
let l := mkargs_aux nargs None (tl args) i in
if hd true args then l else tApp (tRel (S nargs)) [ tRel i ] :: l
| S i, None ⇒
let l := mkargs_aux nargs None (tl args) i in
if hd true args then l else tRel i :: l
end.
Definition mkargs nargs n args :=
let l := rev_map has_body args in
mkargs_aux nargs n l nargs.
Definition from_arg ind npar params args cargs n (a : context_decl) :=
match a.(decl_body) with
| Some _ ⇒ None
| None ⇒
let nargs := List.length args in
let ty := subst (mkr (nargs - S n) 0) 0 a.(decl_type) in
let nparams := List.length params in
let t :=
it_mkLambda_or_LetIn params (
tLam "f" (tImpl ty ty) (
tLam "x" (mkApps (tInd ind []) (mkr nparams 1)) (
tCase
{| ci_ind := ind ; ci_npar := npar ; ci_relevance := Relevant |}
{|
puinst := [] ;
pparams := mkr nparams 2 ;
pcontext := [
{| binder_name := nNamed "x"; binder_relevance := Relevant |}
] ;
preturn := mkApps (tInd ind []) (mkr nparams 3)
|}
(tRel 0)
[
{|
bcontext := args ;
bbody := tApp (tConstruct ind 0 []) (mkr nparams 5 ++ mkargs nargs (Some (nargs - S n)) cargs)
|}
]
)
)
)
in
Some (a.(decl_name), t)
end.
Definition from_ctor ind npar params (b : constructor_body) :=
let args := map decl_name b.(cstr_args) in
mapi (from_arg ind npar params args b.(cstr_args)) b.(cstr_args).
Fixpoint def_list dn (l : list (option (aname × term))) :=
match l with
| Some (n, q) :: l ⇒
na <- tmFreshName ("upd_" # get_name n dn) ;;
tmMkDefinition na q ;;
def_list dn l
| None :: l ⇒ def_list dn l
| [] ⇒ tmReturn tt
end.
Fixpoint debug_def_list dn (l : list (option (aname × term))) :=
match l with
| Some (n, q) :: l ⇒
na <- tmFreshName ("debug_" # get_name n dn) ;;
tmDebugDefinition na q ;;
debug_def_list dn l
| None :: l ⇒ debug_def_list dn l
| [] ⇒ tmReturn tt
end.
Definition from_mind (def_list : ident → list (option (aname × term)) → TemplateMonad unit) ind mind :=
match mind.(ind_finite) with
| BiFinite ⇒
match mind.(ind_bodies) with
| [ oib ] ⇒
match oib.(ind_ctors) with
| [ cstr ] ⇒
let upd_funs := from_ctor ind mind.(ind_npars) mind.(ind_params) cstr in
let default_name := string_of_kername ind.(inductive_mind) in
def_list default_name upd_funs
| _ ⇒ tmFail "A record should have exactly one constructor"
end
| _ ⇒ tmFail "Expecting only one record (not mutually defined)"
end
| _ ⇒ tmFail "Not a record"
end.
Definition get_inductive' {A} (ind : A) :=
t <- tmQuote ind ;;
match t with
| tInd ind _ ⇒
let kn := ind.(inductive_mind) in
q <- tmQuoteInductive kn ;;
tmReturn (ind, q)
| _ ⇒ tmFail "Not an inductive type"
end.
Definition derive_updates {A} (ind : A) :=
'(ind, mib) <- get_inductive' ind ;;
from_mind def_list ind mib.
Definition debug_derive_updates {A} (ind : A) :=
'(ind, mib) <- get_inductive' ind ;;
from_mind debug_def_list ind mib.
MetaCoq Run (derive_updates point3D).
MetaCoq Run (derive_updates Zalt).
Fail MetaCoq Run (derive_updates nat).
MetaCoq Run (derive_updates triple).
MetaCoq Run (derive_updates trap).
Arguments upd_p1 {A B C}.
Arguments upd_p2 {A B C}.
Arguments upd_p3 {A B C}.
match a.(binder_name) with
| nNamed na ⇒ na
| nAnon ⇒ d
end.
Definition has_body (c : context_decl) :=
match c.(decl_body) with
| Some _ ⇒ true
| None ⇒ false
end.
Fixpoint mkargs_aux nargs n args i {struct i} :=
match i, n with
| 0, _ ⇒ []
| S i, Some (S n) ⇒
let l := mkargs_aux nargs (Some n) (tl args) i in
if hd true args then l else tRel i :: l
| S i, Some 0 ⇒
let l := mkargs_aux nargs None (tl args) i in
if hd true args then l else tApp (tRel (S nargs)) [ tRel i ] :: l
| S i, None ⇒
let l := mkargs_aux nargs None (tl args) i in
if hd true args then l else tRel i :: l
end.
Definition mkargs nargs n args :=
let l := rev_map has_body args in
mkargs_aux nargs n l nargs.
Definition from_arg ind npar params args cargs n (a : context_decl) :=
match a.(decl_body) with
| Some _ ⇒ None
| None ⇒
let nargs := List.length args in
let ty := subst (mkr (nargs - S n) 0) 0 a.(decl_type) in
let nparams := List.length params in
let t :=
it_mkLambda_or_LetIn params (
tLam "f" (tImpl ty ty) (
tLam "x" (mkApps (tInd ind []) (mkr nparams 1)) (
tCase
{| ci_ind := ind ; ci_npar := npar ; ci_relevance := Relevant |}
{|
puinst := [] ;
pparams := mkr nparams 2 ;
pcontext := [
{| binder_name := nNamed "x"; binder_relevance := Relevant |}
] ;
preturn := mkApps (tInd ind []) (mkr nparams 3)
|}
(tRel 0)
[
{|
bcontext := args ;
bbody := tApp (tConstruct ind 0 []) (mkr nparams 5 ++ mkargs nargs (Some (nargs - S n)) cargs)
|}
]
)
)
)
in
Some (a.(decl_name), t)
end.
Definition from_ctor ind npar params (b : constructor_body) :=
let args := map decl_name b.(cstr_args) in
mapi (from_arg ind npar params args b.(cstr_args)) b.(cstr_args).
Fixpoint def_list dn (l : list (option (aname × term))) :=
match l with
| Some (n, q) :: l ⇒
na <- tmFreshName ("upd_" # get_name n dn) ;;
tmMkDefinition na q ;;
def_list dn l
| None :: l ⇒ def_list dn l
| [] ⇒ tmReturn tt
end.
Fixpoint debug_def_list dn (l : list (option (aname × term))) :=
match l with
| Some (n, q) :: l ⇒
na <- tmFreshName ("debug_" # get_name n dn) ;;
tmDebugDefinition na q ;;
debug_def_list dn l
| None :: l ⇒ debug_def_list dn l
| [] ⇒ tmReturn tt
end.
Definition from_mind (def_list : ident → list (option (aname × term)) → TemplateMonad unit) ind mind :=
match mind.(ind_finite) with
| BiFinite ⇒
match mind.(ind_bodies) with
| [ oib ] ⇒
match oib.(ind_ctors) with
| [ cstr ] ⇒
let upd_funs := from_ctor ind mind.(ind_npars) mind.(ind_params) cstr in
let default_name := string_of_kername ind.(inductive_mind) in
def_list default_name upd_funs
| _ ⇒ tmFail "A record should have exactly one constructor"
end
| _ ⇒ tmFail "Expecting only one record (not mutually defined)"
end
| _ ⇒ tmFail "Not a record"
end.
Definition get_inductive' {A} (ind : A) :=
t <- tmQuote ind ;;
match t with
| tInd ind _ ⇒
let kn := ind.(inductive_mind) in
q <- tmQuoteInductive kn ;;
tmReturn (ind, q)
| _ ⇒ tmFail "Not an inductive type"
end.
Definition derive_updates {A} (ind : A) :=
'(ind, mib) <- get_inductive' ind ;;
from_mind def_list ind mib.
Definition debug_derive_updates {A} (ind : A) :=
'(ind, mib) <- get_inductive' ind ;;
from_mind debug_def_list ind mib.
MetaCoq Run (derive_updates point3D).
MetaCoq Run (derive_updates Zalt).
Fail MetaCoq Run (derive_updates nat).
MetaCoq Run (derive_updates triple).
MetaCoq Run (derive_updates trap).
Arguments upd_p1 {A B C}.
Arguments upd_p2 {A B C}.
Arguments upd_p3 {A B C}.
Test that it works
If you manage to execute those lines, it's very likely that it does, but
better safe than sorry.