yurug/coq — pull request #2 by Janno (2014-11-27 16:07:55+00:00)
Title: Mtac2 - Mmatching matches

UPDATE: Pull request now fixed. It's all Github's fault, I swear!

This patch adds 3 new constructors to the Mtac2 datatype:
1. Mdestcase : forall {A} (a : A), Mtac2 Case
2. Mconstrs : forall {A : Type} (a : A), Mtac2 (list dyn)
3. Mmakecase : forall (C : Case), Mtac2 dyn
where dyn are dynamic values and Case is a weakly-typed record representing a Coq match.

Mconstrs returns the list of constructors for a datatype. The type signature seems weird on first glance, but we need to account for parametrized and indexed datatypes, so our argument won't be of type Type, but rather of some type .... -> Type.

Mdestcase and Mmakecase are very straightforward: the former one takes a value (hopefully a match) and constructs an equivalent Case record (if possible). The latter reverts the process, but returns a dynamic value. (We forget some types on the way, so for now this is all we can do).