Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/tcase.v
Last active Jul 21, 2019

Embed
What would you like to do?
Require Import List Arith Ascii String Fin.
Require Import MetaCoq.Template.All.
Import ListNotations MonadNotation.
Set Universe Polymorphism.
Local Open Scope string_scope.
(* Get the [one_inductive_body] from a [mutual_inductive_body].
Fails if there is more than one. *)
Definition get_ind_body (tyDef : mutual_inductive_body)
: TemplateMonad one_inductive_body :=
match ind_bodies tyDef with
| [body] => tmReturn body
| _ => tmFail "Unimplemented (mutually recursive types)"
end.
(* Given a type [u := forall (x1 : X1) .. (xn : Xn), _], construct the
type [fun (x1 : X1) .. (xn : Xn) => f (t x1 .. xn)]. *)
Fixpoint mkLambdaFromProd (f : nat -> term) (u : term) : term :=
match u with
| tProd x ux uf =>
let uf' := mkLambdaFromProd
(fun n => f (S n)) uf in
tLambda x ux uf'
| _ => f O
end.
(* [match x : y return z with ... end]
- [x]: Scrutinee
- [y]: Type of scrutinee
- [z]: "Motive", return type of the [match]
*)
Definition tMatch
(x : term) (y : term) (z : term)
(branch : ident -> term -> nat -> term)
: TemplateMonad term :=
match y with
| tApp (tInd i _ as ti) ys =>
let name := inductive_mind i in
tyDef <- tmQuoteInductive name ;;
tyBody <- get_ind_body tyDef ;;
let params := firstn (ind_npars tyDef) ys in
let motive := mkLambdaFromProd
(fun n => tLambda
nAnon
(mkApps (lift0 n (tApp ti params)) (List.map tRel (rev' (seq 0 n))))
(lift0 n z))
(subst0 (rev' params) (remove_arity (ind_npars tyDef) (ind_type tyBody))) in
let mkBranch : _ -> (nat * term) := fun '(i, t, a) =>
let t' := subst0 (ti :: rev' params) (remove_arity (ind_npars tyDef) t) in
let u := mkLambdaFromProd (fun _ => branch i t' a) t' in
(a, u) in
tmReturn (tCase (i, 0) motive x (List.map mkBranch (ind_ctors tyBody)))
| _ => tmFail "Not matching an inductive"
end.
Definition unitI := mkInd "unit" 0.
Quote Definition unitQ := unit.
Quote Definition ttQ := tt.
Definition testMatch y : TemplateMonad unit :=
tMatch (tRel 0) y unitQ (fun _ _ _ => ttQ) >>= fun t =>
tmUnquote (tLambda nAnon y t) >>= print_nf.
Run TemplateProgram (tmQuote (t 2) >>= testMatch).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.