diff options
| -rw-r--r-- | interp/constrintern.ml | 36 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 |
2 files changed, 19 insertions, 21 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f5ad4172c..2e5ec38c8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -424,17 +424,17 @@ let rec subst_pat_iterator y t (subst,p) = match p with let pl = simple_product_of_cases_patterns l' in List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl -let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a = - let rec aux aliases subst = function +let subst_cases_pattern loc alias intern subst scopes a = + let rec aux alias subst = function | AVar id -> begin (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try let (a,(scopt,subscopes)) = List.assoc id subst in - intern (subscopes@scopes) ([],[]) scopt a + intern (subscopes@scopes) ([],[]) scopt a with Not_found -> - if id = ldots_var then [],[[], PatVar (loc,Name id)] else + 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 *) @@ -444,33 +444,34 @@ let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a = *) end | ARef (ConstructRef c) -> - (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)]) + ([],[[], PatCstr (loc,c, [], alias)]) | AApp (ARef (ConstructRef (ind,_ as c)),args) -> let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let _,args = list_chop nparams args in - let idslpll = List.map (aux ([],[]) subst) args in - let ids',pll = product_of_cases_patterns ids idslpll in + let idslpll = List.map (aux Anonymous subst) args in + let ids',pll = product_of_cases_patterns [] idslpll in let pl' = List.map (fun (subst,pl) -> - subst,PatCstr (loc,c,pl,alias_of aliases)) pll in - ids', pl' + subst,PatCstr (loc,c,pl,alias)) pll in + ids', pl' | AList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (a,(scopt,subscopes)) = List.assoc x subst in - let termin = aux ([],[]) subst terminator in + let termin = aux Anonymous subst terminator in let l = decode_patlist_value a in let idsl,v = List.fold_right (fun a (tids,t) -> - let uids,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in + let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) 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 - ids@idsl, v + idsl, List.map (fun ((subst, pl) as x) -> + match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v with Not_found -> anomaly "Inconsistent substitution of recursive notation") | t -> user_err_loc (loc,"",str "Invalid notation for pattern") - in aux aliases subst a - + in aux alias subst a + (* Differentiating between constructors and matching variables *) type pattern_qualid_kind = | ConstrPat of (constructor * cases_pattern list) @@ -565,11 +566,12 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = intern_cases_pattern genv scopes aliases tmp_scope a | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in - let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in if !dump then dump_notation_location (patntn_loc loc args ntn) df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in + let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes c + in ids@ids'', pl | CPatPrim (loc, p) -> let a = alias_of aliases in let (c,df) = Notation.interp_prim_token_cases_pattern loc p a diff --git a/interp/constrintern.mli b/interp/constrintern.mli index edbf9fb62..eac01a92a 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -61,10 +61,6 @@ val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list -val intern_pattern : env -> cases_pattern_expr -> - Names.identifier list * - ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list - (*s Composing internalisation with pretyping *) (* Main interpretation function *) |