From f204058d329fa78b506f4c3b3c4f97ecce504d4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 26 Jul 2017 21:27:36 +0200 Subject: Adding necessary primitives to do pattern-matching over constr. --- theories/Pattern.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 theories/Pattern.v (limited to 'theories/Pattern.v') diff --git a/theories/Pattern.v b/theories/Pattern.v new file mode 100644 index 0000000000..c2ba4162e8 --- /dev/null +++ b/theories/Pattern.v @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> (ident * constr) list := + "ltac2" "pattern_matches". +(** If the term matches the pattern, returns the bound variables. If it doesn't, + fail with [Match_failure]. Panics if not focussed. *) + +Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) := + "ltac2" "pattern_matches_subterm". +(** Returns a stream of results corresponding to all of the subterms of the term + that matches the pattern as in [matches]. The stream is encoded as a + backtracking value whose last exception is [Match_failure]. The additional + value compared to [matches] is the context of the match, to be filled with + the instantiate function. *) + +Ltac2 @ external instantiate : context -> constr -> constr := + "ltac2" "pattern_instantiate". +(** Fill the hole of a context with the given term. *) -- cgit v1.2.3