From b2953849b999d1c3b42c0f494b234f2a93ac7754 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 14 Jun 2012 22:16:29 +0000 Subject: Internalization of pattern is done in two phases. First Notations, syntactic definitions, primitive entries are tackled to build raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns are internalized as cases_pattern or applied inductive (dealing with implicit args, or_pattern refactoring, aliases). It is more uniform, it allows notations for non fully applied constructors but : - It does not raise a warning when an identifier is also a global_reference different than a constructor. - It looks for implicit arguments twice. (because finding scopes of arguments asks for implicit arguments). - It does not deal anymore with constants that evaluates to constructor. (This one is voluntary, dealing with implicit & notations is already a hell full of bugs so what will be next step ? Any terms that computes to a pattern ???) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7 --- intf/constrexpr.mli | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f6d274abb..605be512c 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -35,13 +35,25 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string +type raw_cases_pattern_expr = + | RCPatAlias of loc * raw_cases_pattern_expr * identifier + | RCPatCstr of loc * Globnames.global_reference + * raw_cases_pattern_expr list * raw_cases_pattern_expr list + (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + | RCPatAtom of loc * identifier option + | RCPatOr of loc * raw_cases_pattern_expr list + type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier - | CPatCstr of loc * reference * cases_pattern_expr list - | CPatCstrExpl of loc * reference * cases_pattern_expr list + | CPatCstr of loc * reference + * cases_pattern_expr list * cases_pattern_expr list + (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) | CPatAtom of loc * reference option | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_notation_substitution + * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents + (notation n applied with substitution l1) + applied to arguments l2 *) | CPatPrim of loc * prim_token | CPatRecord of loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr -- cgit v1.2.3