Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active July 21, 2019 01:24
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Lysxia/6a9025aeec5f89f36728da1426a3c9dd to your computer and use it in GitHub Desktop.
Save Lysxia/6a9025aeec5f89f36728da1426a3c9dd to your computer and use it in GitHub Desktop.
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