From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Apr 2017 12:13:04 +0200 Subject: Adding a fold_glob_constr_with_binders combinator. Binding generalizable_vars_of_glob_constr, occur_glob_constr, free_glob_vars, and bound_glob_vars on it. Most of the functions of which it factorizes the code were bugged with respect to bindings in the return clause of "match" and in either the types or the bodies of "fix/cofix". --- interp/implicit_quantifiers.ml | 56 +----------------------------------------- 1 file changed, 1 insertion(+), 55 deletions(-) (limited to 'interp') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 7f11c0a3b6..d6749e918f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -131,61 +131,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp if Id.List.mem_assoc id vs then vs else (id, loc) :: vs else vs - | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> - let vs' = vars bound vs ty in - let bound' = add_name_to_ids bound na in - vars bound' vs' c - | GLetIn (loc,na,b,ty,c) -> - let vs' = vars bound vs b in - let vs'' = Option.fold_left (vars bound) vs' ty in - let bound' = add_name_to_ids bound na in - vars bound' vs'' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bound vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in - List.fold_left (vars_pattern bound) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 b in - let bound' = List.fold_left add_name_to_ids bound nal in - vars bound' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 c in - let vs3 = vars bound vs2 b1 in - vars bound vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound' = Array.fold_right Id.Set.add idl bound in - let vars_fix i vs fid = - let vs1,bound1 = - List.fold_left - (fun (vs,bound) (na,k,bbd,bty) -> - let vs' = vars_option bound vs bbd in - let vs'' = vars bound vs' bty in - let bound' = add_name_to_ids bound na in - (vs'',bound') - ) - (vs,bound') - bl.(i) - in - let vs2 = vars bound1 vs1 tyl.(i) in - vars bound1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bound vs c in - (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bound vs (loc,idl,p,c) = - let bound' = List.fold_right Id.Set.add idl bound in - vars bound' vs c - - and vars_option bound vs = function None -> vs | Some p -> vars bound vs p - - and vars_return_type bound vs (na,tyopt) = - let bound' = add_name_to_ids bound na in - vars_option bound' vs tyopt + | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vars = List.rev (vars bound [] rt) in List.iter (fun (id, loc) -> -- cgit v1.2.3 From e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 5 May 2017 18:12:55 +0200 Subject: Remove dead code and unused open. --- interp/implicit_quantifiers.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'interp') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index d6749e918f..19c872b310 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -19,7 +19,6 @@ open Typeclasses_errors open Pp open Libobject open Nameops -open Misctypes open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li | [] -> bdvars, l in aux bound l binders -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs = function | GVar (loc,id) -> -- cgit v1.2.3 From a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 May 2017 03:00:04 +0200 Subject: Typo in comments of constrintern. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3f99a3c7c0..b57a046796 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -900,7 +900,7 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) -(** {6 Elemtary bricks } *) +(** {6 Elementary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl -- cgit v1.2.3 From b643916aed4093eb7f21116aaef726cab561bc27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 15 May 2017 01:10:54 +0200 Subject: [interp] [ast] Make raw_cases_pattern_expr private. The type `raw_cases_pattern_expr` is used only in the interpretation of notation patterns. Indeed, this should be a private type thus we make it local to `Constrintern`; it makes no sense to expose it in the public AST. The patch is routine, except for the case used to interpret primitives in patterns. We now return a `glob_constr` representing the raw pattern, instead of the private raw pattern type. This could be further refactored but have opted to be conservative here. This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754 , see the commentaries there for more information about `raw_cases_pattern_expr`. --- interp/constrexpr_ops.ml | 6 ------ interp/constrexpr_ops.mli | 1 - interp/constrintern.ml | 36 +++++++++++++++++++++++++++++++----- interp/notation.ml | 25 +++++++++++++------------ interp/notation.mli | 4 +++- 5 files changed, 47 insertions(+), 25 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a592b4cff8..542f9feaf6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function | CPatDelimiters (loc,_,_) -> loc | CPatCast(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 | CLocalAssum ((loc,_)::_,_,t) | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f6d97e107d..b547288e3f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool val constr_loc : constr_expr -> Loc.t val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t -val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t val local_binders_loc : local_binder_expr list -> Loc.t (** {6 Constructors}*) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3f99a3c7c0..b183418009 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -900,6 +900,21 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) +(** Private internalization patterns *) +type raw_cases_pattern_expr = + | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t + | RCPatCstr of Loc.t * Globnames.global_reference + * raw_cases_pattern_expr list * raw_cases_pattern_expr list + (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) + | RCPatAtom of Loc.t * Id.t option + | RCPatOr of Loc.t * raw_cases_pattern_expr list + +let raw_cases_pattern_expr_loc = function + | RCPatAlias (loc,_,_) -> loc + | RCPatCstr (loc,_,_,_) -> loc + | RCPatAtom (loc,_) -> loc + | RCPatOr (loc,_) -> loc + (** {6 Elemtary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] @@ -1198,8 +1213,8 @@ let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal 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) + 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) @@ -1216,6 +1231,14 @@ let drop_notations_pattern looked_for = let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in + (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + let rec rcp_of_glob = function + | GVar (loc,id) -> RCPatAtom (loc,Some id) + | GHole (loc,_,_,_) -> RCPatAtom (loc,None) + | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[]) + | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[]) + | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ") + in let rec drop_syndef top scopes re pats = let (loc,qid) = qualid_of_reference re in try @@ -1285,8 +1308,9 @@ let drop_notations_pattern looked_for = let (argscs1,_) = find_remaining_scopes expl_pl pl g in RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) - when Bigint.is_strictly_pos p -> - fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes) + when Bigint.is_strictly_pos p -> + let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in + rcp_of_glob pat | CPatNotation (_,"( _ )",([a],[]),[]) -> in_pat top scopes a | CPatNotation (loc, ntn, fullargs,extrargs) -> @@ -1299,7 +1323,9 @@ let drop_notations_pattern looked_for = in_not top loc scopes (subst,substlist) extrargs c | CPatDelimiters (loc, key, e) -> in_pat top (None,find_delimiters_scope loc key::snd scopes) e - | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes) + | CPatPrim (loc,p) -> + let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in + rcp_of_glob pat | CPatAtom (loc, Some id) -> begin match drop_syndef top scopes id [] with diff --git a/interp/notation.ml b/interp/notation.ml index 6aa6f54c05..7be2fe0f01 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -444,16 +444,20 @@ let notation_of_prim_token = function | Numeral n -> "- "^(to_string (neg n)) | String _ -> raise Not_found -let find_prim_token g loc p sc = +let find_prim_token check_allowed loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (Notation_ops.glob_constr_of_notation_constr loc c),df + let pat = Notation_ops.glob_constr_of_notation_constr loc c in + check_allowed pat; + pat, df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in check_required_module loc sc spdir; - g (interp ()), ((dirpath (fst spdir),DirPath.empty),"") + let pat = interp () in + check_allowed pat; + pat, ((dirpath (fst spdir),DirPath.empty),"") let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in @@ -466,20 +470,17 @@ let interp_prim_token_gen g loc p local_scopes = | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token = - interp_prim_token_gen (fun x -> x) + interp_prim_token_gen (fun _ -> ()) -(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) - -let rec rcp_of_glob looked_for = function - | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_,_) -> RCPatAtom (loc,None) - | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) +let rec check_allowed_ref_in_pat looked_for = function + | GVar _ | GHole _ -> () + | GRef (_,g,_) -> looked_for g | GApp (loc,GRef (_,g,_),l) -> - looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) + looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l | _ -> raise Not_found let interp_prim_token_cases_pattern_expr loc looked_for p = - interp_prim_token_gen (rcp_of_glob looked_for) loc p + interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p let 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 2e92a00a8c..300480ff1c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) + +(* This function returns a glob_const representing a pattern *) val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> - local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) + local_scopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) -- cgit v1.2.3 From e4ca8679e6700cfd6563890eb7d9e4ee59bede57 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 15 May 2017 02:25:52 +0200 Subject: [interp] Rework check for casts inside patterns. 1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast in a pattern is not a fatal error. We move this check to the internalization function, which is the logical place to raise it, removing a bit boilerplate code. --- interp/constrintern.ml | 51 +++++++++++++++----------------------------------- 1 file changed, 15 insertions(+), 36 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b183418009..405d63dfe7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1335,8 +1335,21 @@ let drop_notations_pattern looked_for = | CPatAtom (loc,None) -> RCPatAtom (loc,None) | CPatOr (loc, pl) -> RCPatOr (loc,List.map (in_pat top scopes) pl) - | CPatCast _ -> - assert false + | CPatCast (loc,_,_) -> + (* We raise an error if the pattern contains a cast, due to + current restrictions on casts in patterns. Cast in patterns + are supportted only in local binders and only at top + level. In fact, they are currently eliminated by the + parser. The only reason why they are in the + [cases_pattern_expr] type is that the parser needs to factor + the "(c : t)" notation with user defined notations (such as + the pair). In the long term, we will try to support such + casts everywhere, and use them to print the domains of + lambdas in the encoding of match in constr. This check is + here and not in the parser because it would require + duplicating the levels of the [pattern] rule. *) + CErrors.user_err ~loc ~hdr:"drop_notations_pattern" + (Pp.strbrk "Casts are not supported in this pattern.") and in_pat_sc scopes x = in_pat false (x,snd scopes) and in_not top loc scopes (subst,substlist as fullsubst) args = function | NVar id -> @@ -1418,40 +1431,7 @@ let rec intern_pat genv aliases pat = check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a - bit ad-hoc, and is due to current restrictions on casts in patterns. We - support them only in local binders and only at top level. In fact, they are - currently eliminated by the parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor the "(c : t)" - notation with user defined notations (such as the pair). In the long term, we - will try to support such casts everywhere, and use them to print the domains - of lambdas in the encoding of match in constr. We put this check here and not - in the parser because it would require to duplicate the levels of the - [pattern] rule. *) -let rec check_no_patcast = function - | CPatCast (loc,_,_) -> - CErrors.user_err ~loc ~hdr:"check_no_patcast" - (Pp.strbrk "Casts are not supported here.") - | CPatDelimiters(_,_,p) - | CPatAlias(_,p,_) -> check_no_patcast p - | CPatCstr(_,_,opl,pl) -> - Option.iter (List.iter check_no_patcast) opl; - List.iter check_no_patcast pl - | CPatOr(_,pl) -> - List.iter check_no_patcast pl - | CPatNotation(_,_,subst,pl) -> - check_no_patcast_subst subst; - List.iter check_no_patcast pl - | CPatRecord(_,prl) -> - List.iter (fun (_,p) -> check_no_patcast p) prl - | CPatAtom _ | CPatPrim _ -> () - -and check_no_patcast_subst (pl,pll) = - List.iter check_no_patcast pl; - List.iter (List.iter check_no_patcast) pll - let intern_cases_pattern genv scopes aliases pat = - check_no_patcast pat; intern_pat genv aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) @@ -1460,7 +1440,6 @@ let _ = fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p let intern_ind_pattern genv scopes pat = - check_no_patcast pat; let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat -- cgit v1.2.3 From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 14 May 2017 00:10:57 +0200 Subject: Fixing a bug with nested "as" clauses in "match". --- interp/constrintern.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c916fcd886..80de11e3ee 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -947,17 +947,6 @@ let find_remaining_scopes pl1 pl2 ref = 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 merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids @ ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) - idspl (ids,[Id.Map.empty,[]]) - (* @return the first variable that occurs twice in a pattern naive n^2 algo *) @@ -1212,6 +1201,17 @@ let alias_of als = match als.alias_ids with *) +let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 + +let product_of_cases_patterns aliases idspl = + List.fold_right (fun (ids,pl) (ids',ptaill) -> + (ids @ ids', + (* Cartesian prod of the or-pats for the nth arg and the tail args *) + List.flatten ( + List.map (fun (subst,p) -> + List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl))) + idspl (aliases.alias_ids,[aliases.alias_map,[]]) + let rec subst_pat_iterator y t p = match p with | RCPatAtom (_,id) -> begin match id with Some x when Id.equal x y -> t | _ -> p end @@ -1376,7 +1376,7 @@ let drop_notations_pattern looked_for = let rec intern_pat genv aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in - let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in + let (ids',pll) = product_of_cases_patterns aliases (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 @@ -1466,7 +1466,7 @@ let intern_ind_pattern genv scopes pat = let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in (with_letin, - match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias (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) @@ -1796,7 +1796,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and intern_multiple_pattern env n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in check_number_of_pattern loc n pl; - product_of_cases_patterns [] idsl_pll + product_of_cases_patterns empty_alias idsl_pll (* Expands a disjunction of multiple pattern *) and intern_disjunctive_multiple_pattern env loc n mpl = -- cgit v1.2.3 From 00964706efe8f6b13e38b57ddb45fac516feb958 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 13 May 2017 23:31:08 +0200 Subject: Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters). We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour. --- interp/constrintern.ml | 35 ++++++----------------------------- 1 file changed, 6 insertions(+), 29 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 80de11e3ee..4e76fe9aae 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -432,31 +432,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il = - function - | CPatCstr (loc, c, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in - List.fold_left free_vars_of_pat il l2 - | CPatAtom (loc, ro) -> - begin match ro with - | Some (Ident (loc, i)) -> (loc, i) :: il - | Some _ | None -> il - end - | CPatNotation (loc, n, l1, l2) -> - let il = List.fold_left free_vars_of_pat il (fst l1) in - List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) - | _ -> anomaly (str "free_vars_of_pat") - -let intern_local_pattern intern lvar env p = - List.fold_left - (fun env (loc, i) -> - let bk = Default Implicit in - let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in - let n = Name i in - let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in - env) - env (free_vars_of_pat [] p) - type binder_data = | BDRawDef of (Loc.t * glob_binder) | BDPattern of @@ -490,13 +465,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in - let env = intern_local_pattern intern lvar env p in - let cp = + let il,cp = match !intern_cases_pattern_fwd (None,env.scopes) p with - | (_, [(_, cp)]) -> cp + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err_loc (loc,"",str "Unsupported nested \"as\" clause."); + il,cp | _ -> assert false in - let il = List.map snd (free_vars_of_pat [] p) in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) let intern_generalization intern env lvar loc bk ak c = -- cgit v1.2.3