diff options
| -rw-r--r-- | interp/constrexpr_ops.ml | 23 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 4 | ||||
| -rw-r--r-- | interp/constrextern.ml | 37 | ||||
| -rw-r--r-- | interp/constrintern.ml | 579 | ||||
| -rw-r--r-- | interp/notation.ml | 4 | ||||
| -rw-r--r-- | interp/notation.mli | 4 | ||||
| -rw-r--r-- | interp/topconstr.ml | 13 | ||||
| -rw-r--r-- | intf/constrexpr.mli | 16 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 10 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 9 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 17 |
12 files changed, 355 insertions, 363 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 18f0a38d4..27cebf9e6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -13,6 +13,7 @@ open Nameops open Libnames open Misctypes open Term +open Glob_term open Mod_subst open Constrexpr open Decl_kinds @@ -57,15 +58,20 @@ let constr_loc = function let cases_pattern_expr_loc = function | CPatAlias (loc,_,_) -> loc - | CPatCstr (loc,_,_) -> loc - | CPatCstrExpl (loc,_,_) -> loc + | CPatCstr (loc,_,_,_) -> loc | CPatAtom (loc,_) -> loc | CPatOr (loc,_) -> loc - | CPatNotation (loc,_,_) -> loc + | CPatNotation (loc,_,_,_) -> loc | CPatRecord (loc, _) -> loc | CPatPrim (loc,_) -> loc | CPatDelimiters (loc,_,_) -> loc +let raw_cases_pattern_expr_loc = function + | RCPatAlias (loc,_,_) -> loc + | RCPatCstr (loc,_,_,_) -> loc + | RCPatAtom (loc,_) -> loc + | RCPatOr (loc,_) -> loc + let local_binder_loc = function | LocalRawAssum ((loc,_)::_,_,t) | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t) @@ -140,3 +146,14 @@ let coerce_to_name = function | a -> Errors.user_err_loc (constr_loc a,"coerce_to_name", str "This expression should be a name.") + +let rec raw_cases_pattern_expr_of_glob_constr looked_for = function + | GVar (loc,id) -> RCPatAtom (loc,Some id) + | GHole (loc,_) -> RCPatAtom (loc,None) + | GRef (loc,g) -> + looked_for g; + RCPatCstr (loc, g,[],[]) + | GApp (loc,GRef (_,g),l) -> + looked_for g; + RCPatCstr (loc, g,[],List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l) + | _ -> raise Not_found diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 161320626..d3e32da46 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -19,6 +19,7 @@ open Constrexpr val constr_loc : constr_expr -> loc val cases_pattern_expr_loc : cases_pattern_expr -> loc +val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> loc val local_binders_loc : local_binder list -> loc @@ -50,3 +51,6 @@ val names_of_local_assums : local_binder list -> name located list (** Does not take let binders into account *) val names_of_local_binders : local_binder list -> name located list + +val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit) + -> Glob_term.glob_constr -> raw_cases_pattern_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7537e7d0b..9ac030136 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -169,10 +169,9 @@ let rec check_same_pattern p1 p2 = match p1, p2 with | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 -> check_same_pattern a1 a2 - | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 -> - List.iter2 check_same_pattern a1 a2 - | CPatCstrExpl(_,c1,a1), CPatCstrExpl(_,c2,a2) when c1=c2 -> - List.iter2 check_same_pattern a1 a2 + | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when c1=c2 -> + let () = List.iter2 check_same_pattern a1 a2 in + List.iter2 check_same_pattern b1 b2 | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> () | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> () | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> @@ -321,21 +320,21 @@ let make_notation loc ntn (terms,termlists,binders as subst) = destPrim terms let make_pat_notation loc ntn (terms,termlists as subst) = - if termlists <> [] then CPatNotation (loc,ntn,subst) else + if termlists <> [] then CPatNotation (loc,ntn,subst,[]) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]))) + (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),[])) (fun (loc,p) -> CPatPrim (loc,p)) destPatPrim terms let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l) + if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l) let add_patt_for_params ind l = Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (dummy_loc,None)) l -let drop_implicits_in_patt ind args = - let impl_st = extract_impargs_data (implicits_of_global (IndRef ind)) in +let drop_implicits_in_patt cst args = + let impl_st = extract_impargs_data (implicits_of_global cst) in let rec impls_fit l = function |[],t -> Some (List.rev_append l t) |_,[] -> None @@ -367,7 +366,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp -> let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstrExpl (loc, c, add_patt_for_params (fst cstrsp) args) + CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) | _ -> try if !Flags.raw_print or !print_no_symbol then raise No_match; @@ -410,13 +409,13 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in if !Topconstr.oldfashion_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, c, args) - else CPatCstrExpl (loc, c, add_patt_for_params (fst cstrsp) args) + then CPatCstr (loc, c, [], args) + else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) else let full_args = add_patt_for_params (fst cstrsp) args in - match drop_implicits_in_patt (fst cstrsp) full_args with - |Some true_args -> CPatCstr (loc, c, true_args) - |None -> CPatCstrExpl (loc, c, full_args) + match drop_implicits_in_patt (ConstructRef cstrsp) full_args with + |Some true_args -> CPatCstr (loc, c, [], true_args) + |None -> CPatCstr (loc, c, full_args, []) in insert_pat_alias loc p na and apply_notation_to_pattern loc ((subst,substlist),more_args) (tmp_scope, scopes as allscopes) vars = function @@ -483,7 +482,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference dummy_loc vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstrExpl (dummy_loc, c, add_patt_for_params ind args) + CPatCstr (dummy_loc, c, add_patt_for_params ind args, []) else try if !Flags.raw_print or !print_no_symbol then raise No_match; @@ -500,9 +499,9 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = with No_match -> let c = extern_reference dummy_loc vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - match drop_implicits_in_patt ind args with - |Some true_args -> CPatCstr (dummy_loc, c, true_args) - |None -> CPatCstrExpl (dummy_loc, c, args) + match drop_implicits_in_patt (IndRef ind) args with + |Some true_args -> CPatCstr (dummy_loc, c, [], true_args) + |None -> CPatCstr (dummy_loc, c, args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 304712675..f6513fd0d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -176,7 +176,7 @@ let explain_internalization_error e = let error_bad_inductive_type loc = user_err_loc (loc,"",str - "This should be an inductive type applied to names or \"_\".") + "This should be an inductive type applied to patterns.") let error_parameter_not_implicit loc = user_err_loc (loc,"", str @@ -248,7 +248,7 @@ let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | CPatNotation (_,"{ _ }",([a],[])) :: l -> + | CPatNotation (_,"{ _ }",([a],[]),[]) :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -744,6 +744,10 @@ let interp_reference vars r = (vars,[]) [] r in r +(**********************************************************************) +(** {5 Cases } *) + +(** {6 Elemtary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl @@ -757,12 +761,21 @@ let rec simple_adjust_scopes n scopes = | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes let find_remaining_scopes pl1 pl2 ref = - snd (list_chop (List.length pl1) - (simple_adjust_scopes (List.length pl1 + List.length pl2) - (find_arguments_scope ref))) - -(**********************************************************************) -(* Cases *) + let impls_st = implicits_of_global ref in + let len_pl1 = List.length pl1 in + let len_pl2 = List.length pl2 in + let impl_list = if len_pl1 = 0 + then select_impargs_size len_pl2 impls_st + else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in + let allscs = find_arguments_scope ref in + let scope_list = list_skipn_at_least len_pl1 allscs in + let rec aux = function + |[],l -> l + |_,[] -> [] + |h::t,_::tt when is_status_implicit h -> aux (t,tt) + |_::t,h::tt -> h :: aux (t,tt) + in ((try list_firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), + simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) let product_of_cases_patterns ids idspl = List.fold_right (fun (ids,pl) (ids',ptaill) -> @@ -779,7 +792,9 @@ let simple_product_of_cases_patterns pl = List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)) pl [[],[]] -(* Check linearity of pattern-matching *) +(* @return the first variable that occurs twice in a pattern + +naive n2 algo *) let rec has_duplicate = function | [] -> None | x::l -> if List.mem x l then (Some x) else has_duplicate l @@ -804,246 +819,77 @@ let check_or_pat_variables loc ids idsl = user_err_loc (loc, "", str "The components of this disjunctive pattern must bind the same variables.") -(** @param with_params says if _ for params were asked to the user. +(** Use only when params were NOT asked to the user. @return if letin are included *) -let check_constructor_length env loc cstr with_params pl pl0 = +let check_constructor_length env loc cstr len_pl pl0 = let nargs = Inductiveops.mis_constructor_nargs cstr in - let n = List.length pl + List.length pl0 in + let n = len_pl + List.length pl0 in if n = nargs then false else (n = (fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr) || (error_wrong_numarg_constructor_loc loc env cstr - (if with_params then nargs else nargs - (Inductiveops.inductive_nparams (fst cstr)))) + (nargs - (Inductiveops.inductive_nparams (fst cstr)))) -let add_implicits_check_length nargs impls_st len_pl1 pl2 fail = +let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if len_pl1 = 0 then select_impargs_size (List.length pl2) impls_st - else snd (list_chop len_pl1 (select_stronger_impargs impls_st)) in + else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in let rec aux i = function |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in - if args_len = nargs then l - else fail (nargs - List.length impl_list + i) - |imp::q,l when is_status_implicit imp -> CPatAtom(dummy_loc,None):: aux i (q,l) - |il,[] -> fail (remaining_args (len_pl1+i) il) - |_::q,hh::tt -> hh::aux (succ i) (q,tt) + ((if args_len = nargs then false + else args_len = nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) + ,l) + |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp + then let (b,out) = aux i (q,[]) in (b,RCPatAtom(dummy_loc,None)::out) + else fail (remaining_args (len_pl1+i) il) + |imp::q,(hh::tt as l) -> if is_status_implicit imp + then let (b,out) = aux i (q,l) in (b,RCPatAtom(dummy_loc,None)::out) + else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) -let add_implicits_check_constructor_length env loc c idslpl1 pl2 = +let add_implicits_check_constructor_length env loc c len_pl1 pl2 = let nargs = Inductiveops.mis_constructor_nargs c in - let len_pl1 = List.length idslpl1 in + let nargs' = (fst (Inductiveops.inductive_nargs (fst c))) + + Inductiveops.constructor_nrealhyps c in let impls_st = implicits_of_global (ConstructRef c) in - add_implicits_check_length nargs impls_st len_pl1 pl2 - (error_wrong_numarg_constructor_loc loc env c) + add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c) + nargs nargs' impls_st len_pl1 pl2 -(** @return if the letin are include *) -let check_ind_length env loc ind pl pl0 = - let (mib,mip) = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - let nargs = mip.Declarations.mind_nrealargs + nparams in - let n = List.length pl + List.length pl0 in - if n = nargs then false else - let nparams', nrealargs' = inductive_nargs_env env ind in - let nargs' = nrealargs' + nparams' in - n = nargs' || - (error_wrong_numarg_inductive_loc loc env ind nargs) - -let add_implicits_check_ind_length env loc c idslpl1 pl2 = +let add_implicits_check_ind_length env loc c len_pl1 pl2 = let (mib,mip) = Global.lookup_inductive c in let nparams = mib.Declarations.mind_nparams in let nargs = mip.Declarations.mind_nrealargs + nparams in - let len_pl1 = List.length idslpl1 in + let nparams', nrealargs' = inductive_nargs_env env c in let impls_st = implicits_of_global (IndRef c) in - add_implicits_check_length nargs impls_st len_pl1 pl2 - (error_wrong_numarg_inductive_loc loc env c) -(* Manage multiple aliases *) + add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c) + nargs (nrealargs' + nparams') impls_st len_pl1 pl2 - (* [merge_aliases] returns the sets of all aliases encountered at this - point and a substitution mapping extra aliases to the first one *) -let merge_aliases (ids,asubst as _aliases) id = - ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst - -let alias_of = function - | ([],_) -> Anonymous - | (id::_,_) -> Name id - -let message_redundant_alias (id1,id2) = - if_warn msg_warning - (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) - -(* Expanding notations *) - -let rec subst_pat_iterator y t (subst,p) = match p with - | PatVar (_,id) as x -> - if id = Name y then t else [subst,x] - | PatCstr (loc,id,l,alias) -> - let l' = List.map (fun a -> (subst_pat_iterator y t ([],a))) l in - let pl = simple_product_of_cases_patterns l' in - List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl - -(** @raise NotEnoughArguments only in the case of [subst_cases_pattern] thanks to - preconditions in other cases. *) +(** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin then fst (Inductiveops.inductive_nargs ind) else Inductiveops.inductive_nparams ind in - if nparams > List.length args then error_not_enough_arguments loc; + assert (nparams <= List.length args); let params,args = list_chop nparams args in List.iter (function PatVar(_,Anonymous) -> () | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params; args -let subst_cases_pattern loc alias intern fullsubst env a = - let rec aux alias (subst,substlist as fullsubst) = function - | NVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = List.assoc id subst in - intern {env with scopes=subscopes@env.scopes; - tmp_scope = scopt} ([],[]) a - with Not_found -> - if id = ldots_var then [], [[], PatVar (loc,Name id)] else - anomaly ("Unbound pattern notation variable: "^(string_of_id id)) - (* - (* Happens for local notation joint with inductive/fixpoint defs *) - if aliases <> ([],[]) then - anomaly "Pattern notation without constructors"; - [[id],[]], PatVar (loc,Name id) - *) - end - | NRef (ConstructRef c) -> - ([],[[], PatCstr (loc,c, [], alias)]) - | NApp (NRef (ConstructRef cstr),args) -> - let idslpll = List.map (aux Anonymous fullsubst) args in - let ids',pll = product_of_cases_patterns [] idslpll in - let pl' = List.map (fun (asubst,pl) -> - asubst,PatCstr (loc,cstr,chop_params_pattern loc (fst cstr) pl false,alias)) pll in - ids', pl' - | NList (x,_,iter,terminator,lassoc) -> - (try - (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = List.assoc x substlist in - let termin = aux Anonymous fullsubst terminator in - let idsl,v = - List.fold_right (fun a (tids,t) -> - let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in - let pll = List.map (subst_pat_iterator ldots_var t) u in - tids@uids, List.flatten pll) - (if lassoc then List.rev l else l) termin in - idsl, List.map (fun ((asubst, pl) as x) -> - match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v - with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | NHole _ -> ([],[[], PatVar (loc,Anonymous)]) - | t -> error_invalid_pattern_notation loc - in aux alias fullsubst a - -let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = function - | NVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = List.assoc id subst in - intern_ind_patt {env with scopes=subscopes@env.scopes; - tmp_scope = scopt} a - with Not_found -> - anomaly ("Unbound pattern notation variable: "^(string_of_id id)) - end - | NRef (IndRef c) -> - false, (c, []) - | NApp (NRef (IndRef ind),args) -> - let idslpll = List.map (subst_cases_pattern loc Anonymous intern fullsubst env) args in - begin - match product_of_cases_patterns [] idslpll with - |_,[_,pl]-> - let pl' = chop_params_pattern loc ind pl false in - false, (ind,pl') - |_ -> error_invalid_pattern_notation loc - end - | t -> error_invalid_pattern_notation loc - - -(* Differentiating between constructors and matching variables *) -type pattern_qualid_kind = - | ConstrPat of constructor * (identifier list * - ((identifier * identifier) list * cases_pattern) list) list - | VarPat of identifier - -let find_at_head looked_for add_params ref f pats env = - let (loc,qid) = qualid_of_reference ref in - let gref = - try locate_extended qid - with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in - match gref with - | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with - | NRef g -> - let cstr = looked_for g in - assert (vars=[]); - cstr,add_params cstr, pats - | NApp (NRef g,args) -> - let cstr = looked_for g in - let nvars = List.length vars in - if List.length pats < nvars then error_not_enough_arguments loc; - let pats1,pats2 = list_chop nvars pats in - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in - let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in - cstr, idspl1, pats2 - | _ -> raise Not_found) - - | TrueGlobal r -> - let rec unf = function - | ConstRef cst -> - let v = Environ.constant_value (Global.env()) cst in - unf (global_of_constr v) - | g -> - let cstr = looked_for g in - Dumpglob.add_glob loc r; - cstr, add_params cstr, pats - in unf r - -let find_constructor add_params = - find_at_head (function ConstructRef cstr -> cstr |_ -> raise Not_found) - (function (ind,_ as c) -> match add_params with - |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c - then fst (Inductiveops.inductive_nargs ind) - else Inductiveops.inductive_nparams ind in - Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))]) - |None -> []) - +let find_constructor loc add_params ref = + let cstr = (function ConstructRef cstr -> cstr + |IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.") + |_ -> anomaly "unexpected global_reference in pattern") ref in + cstr, (function (ind,_ as c) -> match add_params with + |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c + then fst (Inductiveops.inductive_nargs ind) + else Inductiveops.inductive_nparams ind in + Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))]) + |None -> []) cstr let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) -let maybe_constructor add_params ref f env = - try - let c,idspl1,pl2 = find_constructor add_params ref f [] env in - assert (pl2 = []); - ConstrPat (c,idspl1) - with - (* patt var does not exists globally *) - | InternalizationError _ -> VarPat (find_pattern_variable ref) - (* patt var also exists globally but does not satisfy preconditions *) - | (Environ.NotEvaluableConst _ | Not_found) -> - if_warn msg_warning (str "pattern " ++ pr_reference ref ++ - str " is understood as a pattern variable"); - VarPat (find_pattern_variable ref) - -let mustbe_constructor loc add_params ref f patl env = - try find_constructor add_params ref f patl env - with (Environ.NotEvaluableConst _ | Not_found) -> - raise (InternalizationError (loc,NotAConstructor ref)) - -let mustbe_inductive loc ref f patl env = - try find_at_head (function IndRef ind -> ind|_ -> raise Not_found) (function _ -> []) ref f patl env - with (Environ.NotEvaluableConst _ | Not_found| - InternalizationError (_,NotAConstructor _)) -> - error_bad_inductive_type loc - let sort_fields mode loc l completer = (*mode=false if pattern and true if constructor*) match l with @@ -1133,124 +979,225 @@ let sort_fields mode loc l completer = Some (nparams, base_constructor, List.rev (clean_list sorted_indexed_pattern 0 [])) -let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = - let intern_pat = intern_cases_pattern genv in +(** {6 Manage multiple aliases} *) + + (* [merge_aliases] returns the sets of all aliases encountered at this + point and a substitution mapping extra aliases to the first one *) +let merge_aliases (ids,asubst as _aliases) id = + ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst + +let alias_of = function + | ([],_) -> Anonymous + | (id::_,_) -> Name id + +let message_redundant_alias (id1,id2) = + if_warn msg_warning + (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) + +(** {6 Expanding notations } + + @returns a raw_case_pattern_expr : + - no notations and syntactic definition + - global reference and identifeir instead of reference + +*) + +let rec subst_pat_iterator y t p = match p with + | RCPatAtom (_,id) -> + begin match id with Some x when x = y -> t |_ -> p end + | RCPatCstr (loc,id,l1,l2) -> + RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) + | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) + | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) + +let drop_notations_pattern looked_for = + let rec drop_syndef env re pats = + let (loc,qid) = qualid_of_reference re in + try + match locate_extended qid with + |SynDef sp -> + let (vars,a) = Syntax_def.search_syntactic_definition sp in + (match a with + | NRef g -> + looked_for g; + let () = assert (vars = []) in + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g, [], List.map2 (in_pat_sc env) argscs pats) + | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *) + looked_for g; + let () = assert (vars = []) in + let (argscs,_) = find_remaining_scopes pats [] g in + Some (g, List.map2 (in_pat_sc env) argscs pats, []) + | NApp (NRef g,args) -> + looked_for g; + let nvars = List.length vars in + if List.length pats < nvars then error_not_enough_arguments loc; + let pats1,pats2 = list_chop nvars pats in + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in + let idspl1 = List.map (in_not loc env (subst,[]) []) args in + let (_,argscs) = find_remaining_scopes pats1 pats2 g in + Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2) + | _ -> raise Not_found) + |TrueGlobal g -> + looked_for g; + Dumpglob.add_glob loc g; + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g,[],List.map2 (fun x -> in_pat {env with tmp_scope = x}) argscs pats) + with Not_found -> None + and in_pat env = function + | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat env p, id) + | CPatRecord (loc, l) -> + let sorted_fields = + sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in + begin match sorted_fields with + | None -> RCPatAtom (loc, None) + | Some (_, head, pl) -> + match drop_syndef env head pl with + |Some (a,b,c) -> RCPatCstr(loc, a, b, c) + |None -> raise (InternalizationError (loc,NotAConstructor head)) + end + | CPatCstr (loc, head, [], pl) -> + begin + match drop_syndef env head pl with + | Some (a,b,c) -> RCPatCstr(loc, a, b, c) + | None -> raise (InternalizationError (loc,NotAConstructor head)) + end + | CPatCstr (loc, r, expl_pl, pl) -> + let g = try + (locate (snd (qualid_of_reference r))) + with Not_found -> + raise (InternalizationError (loc,NotAConstructor r)) in + let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in + RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl) + | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) + when Bigint.is_strictly_pos p -> + fst (Notation.interp_prim_token_cases_pattern_expr loc looked_for (Numeral (Bigint.neg p)) + (env.tmp_scope,env.scopes)) + | CPatNotation (_,"( _ )",([a],[]),[]) -> + in_pat env a + | CPatNotation (loc, ntn, fullargs,extrargs) -> + let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in + let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in + let (ids',idsl',_) = split_by_type ids' in + Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in + let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in + in_not loc env (subst,substlist) extrargs c + | CPatDelimiters (loc, key, e) -> + in_pat {env with scopes=find_delimiters_scope loc key::env.scopes; + tmp_scope = None} e + | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc looked_for p + (env.tmp_scope,env.scopes)) + | CPatAtom (loc, Some id) -> + begin + match drop_syndef env id [] with + |Some (a,b,c) -> RCPatCstr (loc, a, b, c) + |None -> RCPatAtom (loc, Some (find_pattern_variable id)) + end + | CPatAtom (loc,None) -> RCPatAtom (loc,None) + | CPatOr (loc, pl) -> + RCPatOr (loc,List.map (in_pat env) pl) + and in_pat_sc env x = in_pat {env with tmp_scope = x} + and in_not loc env (subst,substlist as fullsubst) args = function + | NVar id -> + assert (args = []); + begin + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = List.assoc id subst in + in_pat {env with scopes=subscopes@env.scopes; + tmp_scope = scopt} a + with Not_found -> + if id = ldots_var then RCPatAtom (loc,Some id) else + anomaly ("Unbound pattern notation variable: "^(string_of_id id)) + end + | NRef g -> + looked_for g; + let (_,argscs) = find_remaining_scopes [] args g in + RCPatCstr (loc, g, [], List.map2 (in_pat_sc env) argscs args) + | NApp (NRef g,pl) -> + looked_for g; + let (argscs1,argscs2) = find_remaining_scopes pl args g in + RCPatCstr (loc, g, + List.map2 (fun x -> in_not loc {env with tmp_scope = x} fullsubst []) argscs1 pl, + List.map2 (in_pat_sc env) argscs2 args) + | NList (x,_,iter,terminator,lassoc) -> + let () = assert (args = []) in + (try + (* All elements of the list are in scopes (scopt,subscopes) *) + let (l,(scopt,subscopes)) = List.assoc x substlist in + let termin = in_not loc env fullsubst [] terminator in + List.fold_right (fun a t -> + let u = in_not loc env ((x,(a,(scopt,subscopes)))::subst,substlist) [] iter in + subst_pat_iterator ldots_var t u) + (if lassoc then List.rev l else l) termin + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | NHole _ -> let () = assert (args = []) in RCPatAtom (loc,None) + | t -> error_invalid_pattern_notation loc + in in_pat + +let rec intern_pat genv (ids,asubst as aliases) pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = - let argscs2 = find_remaining_scopes idslpl1 pl2 (ConstructRef c) in - let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in + let idslpl2 = List.map (intern_pat genv ([],[])) pl2 in let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in match pat with - | CPatAlias (loc, p, id) -> + | RCPatAlias (loc, p, id) -> let aliases' = merge_aliases aliases id in - intern_pat env aliases' p - | CPatRecord (loc, l) -> - let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in - let self_patt = - match sorted_fields with - | None -> CPatAtom (loc, None) - | Some (_, head, pl) -> CPatCstr(loc, head, pl) - in - intern_pat env aliases self_patt - | CPatCstr (loc, head, pl) -> + intern_pat genv aliases' p + | RCPatCstr (loc, head, expl_pl, pl) -> if !oldfashion_patterns then - let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat pl env in - let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in - intern_cstr_with_all_args loc c with_letin idslpl1 pl2 + let c,idslpl1 = find_constructor loc (if expl_pl = [] then Some (List.length pl) else None) head in + let with_letin = + check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in + intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl) else - let c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat pl env in - let pl2' = add_implicits_check_constructor_length genv loc c idslpl1 pl2 in - intern_cstr_with_all_args loc c false idslpl1 pl2' - | CPatCstrExpl (loc, head, pl) -> - let c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat pl env in - let with_letin = check_constructor_length genv loc c true idslpl1 pl2 in - intern_cstr_with_all_args loc c with_letin idslpl1 pl2 - | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[])) - when Bigint.is_strictly_pos p -> - intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p))) - | CPatNotation (_,"( _ )",([a],[])) -> - intern_pat env aliases a - | CPatNotation (loc, ntn, fullargs) -> - let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in - let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in - let (ids',idsl',_) = split_by_type ids' in - Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in - let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in - let ids'',pl = - subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist) - env c - in ids@ids'', pl - | CPatPrim (loc, p) -> - let a = alias_of aliases in - let (c,_) = Notation.interp_prim_token_cases_pattern loc p a - (env.tmp_scope,env.scopes) in - (ids,[asubst,c]) - | CPatDelimiters (loc, key, e) -> - intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes; - tmp_scope = None} aliases e - | CPatAtom (loc, Some head) -> - (match maybe_constructor (if !oldfashion_patterns then Some 0 else None) - head intern_pat env with - | ConstrPat (c,idspl) -> - if !oldfashion_patterns then - let with_letin = check_constructor_length genv loc c false idspl [] in - intern_cstr_with_all_args loc c with_letin idspl [] - else - let pl2 = add_implicits_check_constructor_length genv loc c idspl [] in - intern_cstr_with_all_args loc c false idspl pl2 - | VarPat id -> - let ids,asubst = merge_aliases aliases id in - (ids,[asubst, PatVar (loc,alias_of (ids,asubst))])) - | CPatAtom (loc, None) -> + let c,idslpl1 = find_constructor loc None head in + let with_letin, pl2 = + add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in + intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) + | RCPatAtom (loc, Some id) -> + let ids,asubst = merge_aliases aliases id in + (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]) + | RCPatAtom (loc, None) -> (ids,[asubst, PatVar (loc,alias_of aliases)]) - | CPatOr (loc, pl) -> + | RCPatOr (loc, pl) -> assert (pl <> []); - let pl' = List.map (intern_pat env aliases) pl in + let pl' = List.map (intern_pat genv aliases) pl in let (idsl,pl') = List.split pl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -let rec intern_ind_pattern genv env pat = - let intern_ind_with_all_args loc c idslpl1 pl2 = - let argscs2 = find_remaining_scopes idslpl1 pl2 (IndRef c) in - let idslpl2 = List.map2 (fun x -> intern_cases_pattern genv {env with tmp_scope = x} ([],[])) argscs2 pl2 in - match product_of_cases_patterns [] (idslpl1@idslpl2) with - |_,[_,pl] -> - (c,chop_params_pattern loc c pl false) - |_ -> error_bad_inductive_type loc - in - match pat with - | CPatCstr (loc, head, pl) -> - let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) pl env in - let pl2' = add_implicits_check_ind_length genv loc c idslpl1 pl2 in - false,intern_ind_with_all_args loc c idslpl1 pl2' - | CPatCstrExpl (loc, head, pl) -> - let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) pl env in - let with_letin = check_ind_length genv loc c idslpl1 pl2 in - with_letin,intern_ind_with_all_args loc c idslpl1 pl2 - | CPatNotation (_,"( _ )",([a],[])) -> - intern_ind_pattern genv env a - | CPatNotation (loc, ntn, fullargs) -> - let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in - let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in - let (ids',idsl',_) = split_by_type ids' in - Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in - let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in - subst_ind_pattern loc (intern_ind_pattern genv) (intern_cases_pattern genv) (subst,substlist) - env c - | CPatDelimiters (loc, key, e) -> - intern_ind_pattern genv {env with scopes=find_delimiters_scope loc key::env.scopes; - tmp_scope = None} e - | CPatAtom (loc, Some head) -> - let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) [] env in - let with_letin = check_ind_length genv loc c idslpl1 pl2 in - with_letin,intern_ind_with_all_args loc c idslpl1 pl2 - | x -> error_bad_inductive_type (cases_pattern_expr_loc x) +let intern_cases_pattern genv env aliases pat = + intern_pat genv aliases + (drop_notations_pattern (function ConstructRef _ -> () |_ -> raise Not_found) env pat) + +let intern_ind_pattern genv env pat = + let no_not = + try + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () |_ -> raise Not_found) env pat + with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc + in + match no_not with + | RCPatCstr (loc, head,expl_pl, pl) -> + let c = (function IndRef ind -> ind + |_ -> error_bad_inductive_type loc) head in + let with_letin, pl2 = add_implicits_check_ind_length genv loc c + (List.length expl_pl) pl in + let idslpl1 = List.rev_map (intern_pat genv ([],[])) expl_pl in + let idslpl2 = List.map (intern_pat genv ([],[])) pl2 in + (with_letin, + match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + |_,[_,pl] -> + (c,chop_params_pattern loc c pl with_letin) + |_ -> error_bad_inductive_type loc) + | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x) (**********************************************************************) (* Utilities for application *) diff --git a/interp/notation.ml b/interp/notation.ml index 2430b980c..a76ede48c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -372,8 +372,8 @@ let interp_prim_token_gen g loc p local_scopes = let interp_prim_token = interp_prim_token_gen (fun x -> x) -let interp_prim_token_cases_pattern loc p name = - interp_prim_token_gen (cases_pattern_of_glob_constr name) loc p +let interp_prim_token_cases_pattern_expr loc looked_for p = + interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p let rec interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in diff --git a/interp/notation.mli b/interp/notation.mli index 7629d86e7..3f66f993a 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -84,8 +84,8 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : loc -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern : loc -> prim_token -> name -> - local_scopes -> cases_pattern * (notation_location * scope_name option) +val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token -> + local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 9b3c00bf2..bc9d3b851 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -47,7 +47,8 @@ let error_invalid_pattern_notation loc = let ids_of_cases_indtype = let rec vars_of ids = function (* We deal only with the regular cases *) - | (CPatCstr (_,_,l)|CPatCstrExpl (_, _, l)|CPatNotation (_,_,(l,[]))) -> List.fold_left vars_of [] l + | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) -> + List.fold_left vars_of (List.fold_left vars_of [] l2) l1 (* assume the ntn is applicative and does not instantiate the head !! *) | CPatDelimiters(_,_,c) -> vars_of ids c | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids @@ -69,10 +70,14 @@ let rec cases_pattern_fold_names f a = function | CPatRecord (_, l) -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l | CPatAlias (_,pat,id) -> f id a - | CPatCstr (_,_,patl) | CPatCstrExpl (_,_,patl) | CPatOr (_,patl) -> + | CPatOr (_,patl) -> List.fold_left (cases_pattern_fold_names f) a patl - | CPatNotation (_,_,(patl,patll)) -> - List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll) + | CPatCstr (_,_,patl1,patl2) -> + List.fold_left (cases_pattern_fold_names f) + (List.fold_left (cases_pattern_fold_names f) a patl1) patl2 + | CPatNotation (_,_,(patl,patll),patl') -> + List.fold_left (cases_pattern_fold_names f) + (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a 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 diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ee8ec009d..323da812d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -198,7 +198,7 @@ let extend_constr_notation (n,assoc,ntn,rules) = let e = interp_constr_entry_key false (ETConstr (n,())) in let nb = extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules in (* Add the notation in cases_pattern *) - let mkact loc env = CPatNotation (loc,ntn,env) in + let mkact loc env = CPatNotation (loc,ntn,env,[]) in let e = interp_constr_entry_key true (ETConstr (n,())) in let nb' = extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rules in diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ca462a702..f53cab6c6 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -344,12 +344,14 @@ GEXTEND Gram | "9" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with - | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) + | CPatAtom (_, Some r) -> CPatCstr (loc, r, [], lp) + | CPatCstr (_, r, l1, l2) -> CPatCstr (loc, r, l1 , l2@lp) + | CPatNotation (_, n, s, l) -> CPatNotation (loc, n , s, l@lp) | _ -> Errors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", - Pp.str "Constructor expected.")) + Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST1 NEXT -> - CPatCstrExpl (loc, r, lp) ] + CPatCstr (loc, r, lp, []) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] | "0" @@ -359,7 +361,7 @@ GEXTEND Gram | "("; p = pattern LEVEL "200"; ")" -> (match p with CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CPatNotation(loc,"( _ )",([p],[])) + CPatNotation(loc,"( _ )",([p],[]),[]) | _ -> p) | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (loc, String s) ] ] diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 6d3a5be39..a067440cb 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -96,10 +96,11 @@ let rec add_vars_of_simple_pattern globs = function (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) -> - List.fold_left add_vars_of_simple_pattern globs pl - | CPatNotation(_,_,(pl,pll)) -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) + | CPatCstr (_,_,pl1,pl2) -> + List.fold_left add_vars_of_simple_pattern + (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + | CPatNotation(_,_,(pl,pll),pl') -> + List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs | _ -> globs diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2e3ce2103..78a2fd759 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -174,19 +174,24 @@ let rec pr_patt sep inh p = str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec | CPatAlias (_,p,id) -> pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las - | CPatCstr (_,c,[]) -> pr_reference c, latom - | CPatCstr (_,c,args) -> + | CPatCstr (_,c,[],[]) -> pr_reference c, latom + | CPatCstr (_,c,[],args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstrExpl (_,c,args) -> + | CPatCstr (_,c,args,[]) -> str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + | CPatCstr (_,c,expl_args,extra_args) -> + surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) + ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp | CPatAtom (_,None) -> str "_", latom | CPatAtom (_,Some r) -> pr_reference r, latom | CPatOr (_,pl) -> hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator - | CPatNotation (_,"( _ )",([p],[])) -> + | CPatNotation (_,"( _ )",([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,(l,ll)) -> - pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) + | CPatNotation (_,s,(l,ll),args) -> + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in + (if args=[]||prec_less l_not (lapp,L) then strm_not else surround strm_not) + ++ prlist (pr_patt spc (lapp,L)) args, if args<>[] then lapp else l_not | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in |