diff options
| author | Pierre-Marie Pédrot | 2017-07-26 21:27:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-27 01:39:24 +0200 |
| commit | f204058d329fa78b506f4c3b3c4f97ecce504d4b (patch) | |
| tree | 97ab8dee9941ddfaced5059456b6864d3beb3cac /theories | |
| parent | c9e7d7f1ceb22667e77a4ee49a4afc2cce6f9a2c (diff) | |
Adding necessary primitives to do pattern-matching over constr.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init.v | 4 | ||||
| -rw-r--r-- | theories/Ltac2.v | 1 | ||||
| -rw-r--r-- | theories/Pattern.v | 30 |
3 files changed, 35 insertions, 0 deletions
diff --git a/theories/Init.v b/theories/Init.v index c0a73576d3..803e48e352 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -27,6 +27,7 @@ Ltac2 Type constant. Ltac2 Type inductive. Ltac2 Type constructor. Ltac2 Type projection. +Ltac2 Type pattern. Ltac2 Type constr. Ltac2 Type message. @@ -56,3 +57,6 @@ Ltac2 Type exn ::= [ Not_focussed ]. Ltac2 Type exn ::= [ Not_found ]. (** Used when something is missing. *) + +Ltac2 Type exn ::= [ Match_failure ]. +(** Used to signal a pattern didn't match a term. *) diff --git a/theories/Ltac2.v b/theories/Ltac2.v index 0d6c8f232a..9aaee850cd 100644 --- a/theories/Ltac2.v +++ b/theories/Ltac2.v @@ -15,4 +15,5 @@ Require Ltac2.Array. Require Ltac2.Message. Require Ltac2.Constr. Require Ltac2.Control. +Require Ltac2.Pattern. Require Ltac2.Std. 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 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ltac2.Init. + +Ltac2 Type t := pattern. + +Ltac2 Type context. + +Ltac2 @ external matches : t -> 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. *) |