Last active
July 21, 2019 01:24
-
-
Save Lysxia/6a9025aeec5f89f36728da1426a3c9dd to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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