diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-12 20:11:01 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:19 +0200 |
commit | 846b74275511bd89c2f3abe19245133050d2199c (patch) | |
tree | 24e4c838d440e7ce6104bca95c8eb4b7baa321ec /interp | |
parent | e57074289193b0f0184f3c7143d8ab7e0edd5112 (diff) |
[constrexpr] Make patterns use Loc.located for location information
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrexpr_ops.ml | 41 | ||||
-rw-r--r-- | interp/constrextern.ml | 52 | ||||
-rw-r--r-- | interp/constrintern.ml | 114 | ||||
-rw-r--r-- | interp/modintern.ml | 11 | ||||
-rw-r--r-- | interp/notation.ml | 8 | ||||
-rw-r--r-- | interp/topconstr.ml | 24 |
6 files changed, 117 insertions, 133 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a592b4cff..3ba5d985f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -59,31 +59,31 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with let eq_located f (_, x) (_, y) = f x y -let rec cases_pattern_expr_eq p1 p2 = +let rec cases_pattern_expr_eq (l1, p1) (l2, p2) = if p1 == p2 then true else match p1, p2 with - | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) -> + | CPatAlias(a1,i1), CPatAlias(a2,i2) -> Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 - | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) -> + | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> eq_reference c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 - | CPatAtom(_,r1), CPatAtom(_,r2) -> + | CPatAtom(r1), CPatAtom(r2) -> Option.equal eq_reference r1 r2 - | CPatOr (_, a1), CPatOr (_, a2) -> + | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 - | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) -> + | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> String.equal n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 - | CPatPrim(_,i1), CPatPrim(_,i2) -> + | CPatPrim i1, CPatPrim i2 -> prim_token_eq i1 i2 - | CPatRecord (_, l1), CPatRecord (_, l2) -> + | CPatRecord l1, CPatRecord l2 -> let equal (r1, e1) (r2, e2) = eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 in List.equal equal l1 l2 - | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) -> + | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> String.equal s1 s2 && cases_pattern_expr_eq e1 e2 | _ -> false @@ -183,7 +183,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal (eq_located Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 -and branch_expr_eq (_, p1, e1) (_, p2, e2) = +and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && constr_expr_eq e1 e2 @@ -252,22 +252,9 @@ let constr_loc = function | CPrim (loc,_) -> loc | CDelimiters (loc,_,_) -> loc -let cases_pattern_expr_loc = function - | CPatAlias (loc,_,_) -> loc - | CPatCstr (loc,_,_,_) -> loc - | CPatAtom (loc,_) -> loc - | CPatOr (loc,_) -> loc - | CPatNotation (loc,_,_,_) -> loc - | CPatRecord (loc, _) -> loc - | CPatPrim (loc,_) -> loc - | 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 cases_pattern_expr_loc (l,_) = l + +let raw_cases_pattern_expr_loc (l, _) = l let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) @@ -330,7 +317,7 @@ let expand_binders mkC loc bl c = let c = CCases (loc, LetPatternStyle, None, [(e,None,None)], - [(loc1, [(loc1,[p])], c)]) + [(loc1, ([(loc1,[p])], c))]) in (ni :: env, mkC loc ([id],Default Explicit,ty) c) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 59b8b4e5b..7a229856e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -148,11 +148,11 @@ let insert_delimiters e = function let insert_pat_delimiters loc p = function | None -> p - | Some sc -> CPatDelimiters (loc,sc,p) + | Some sc -> Loc.tag ~loc @@ CPatDelimiters (sc,p) let insert_pat_alias loc p = function | Anonymous -> p - | Name id -> CPatAlias (loc,p,id) + | Name id -> Loc.tag ~loc @@ CPatAlias (p,id) (**********************************************************************) (* conversion of references *) @@ -178,7 +178,7 @@ let extern_reference loc vars l = !my_extern_reference loc vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else @@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args = let rec impls_fit l = function |[],t -> Some (List.rev_append l t) |_,[] -> None - |h::t,CPatAtom(_,None)::tt when is_status_implicit h -> impls_fit l (t,tt) + |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt) |h::_,_ when is_status_implicit h -> None |_::t,hh::tt -> impls_fit (hh::l) (t,tt) in let rec aux = function @@ -237,7 +237,7 @@ let expand_curly_brackets loc mknot ntn l = mknot (loc,!ntn',l) let destPrim = function CPrim(_,t) -> Some t | _ -> None -let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None +let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn @@ -267,15 +267,15 @@ let make_notation loc ntn (terms,termlists,binders as subst) = destPrim terms let make_pat_notation loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then CPatNotation (loc,ntn,subst,args) else + if not (List.is_empty termlists) then (loc, CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),args)) - (fun (loc,p) -> CPatPrim (loc,p)) + (fun (loc,ntn,l) -> Loc.tag ~loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,p) -> Loc.tag ~loc @@ CPatPrim p) destPatPrim terms let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l) + if List.is_empty l then Loc.tag ~loc @@ CPatAtom (Some qid) else Loc.tag ~loc @@ CPatCstr (qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in @@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) + Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | None -> raise No_match | Some key -> let loc = cases_pattern_loc pat in - insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na + insert_pat_alias loc (insert_pat_delimiters loc (Loc.tag ~loc @@ CPatPrim p) key) na with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> match pat with - | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id))) - | PatVar (loc,Anonymous) -> CPatAtom (loc, None) + | PatVar (loc,Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None | PatCstr(loc,cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = @@ -327,24 +327,24 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | Some c :: q -> match args with | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc + | (_loc, CPatAtom(None)) :: tail -> ip q tail acc (* we don't want to have 'x = _' in our patterns *) | head :: tail -> ip q tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in - CPatRecord(loc, List.rev (ip projs args [])) + Loc.tag ~loc @@ CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, c, None, args) - else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) + then Loc.tag ~loc @@ CPatCstr (c, None, args) + else Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - |Some true_args -> CPatCstr (loc, c, None, true_args) - |None -> CPatCstr (loc, c, Some full_args, []) + | Some true_args -> Loc.tag ~loc @@ CPatCstr (c, None, true_args) + | None -> Loc.tag ~loc @@ CPatCstr (c, Some full_args, []) in insert_pat_alias loc p na and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -401,8 +401,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function let p = apply_notation_to_pattern loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias loc p na - | PatVar (loc,Anonymous) -> CPatAtom (loc, None) - | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id))) + | PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None + | PatVar (loc,Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id))) with No_match -> extern_notation_pattern allscopes vars t rules @@ -422,7 +422,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), []) + Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -430,7 +430,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> - insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key + insert_pat_delimiters Loc.ghost (Loc.tag @@ CPatPrim p) key with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -440,8 +440,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args) - |None -> CPatCstr (Loc.ghost, c, Some args, []) + |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args) + |None -> Loc.tag @@ CPatCstr (c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -868,7 +868,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = - (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], + Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf..6bf6772c6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -230,7 +230,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 -> @@ -430,17 +430,16 @@ 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 rec free_vars_of_pat il (loc, pt) = match pt with + | CPatCstr (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) -> + | CPatAtom ro -> begin match ro with | Some (Ident (loc, i)) -> (loc, i) :: il | Some _ | None -> il end - | CPatNotation (loc, n, l1, l2) -> + | CPatNotation (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") @@ -988,10 +987,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 else Int.equal 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(Loc.ghost,None)::out) + then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(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(Loc.ghost,None)::out) + then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -1194,14 +1193,14 @@ let alias_of als = match als.alias_ids with *) -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) - | 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 rec subst_pat_iterator y t (loc, p) = match p with + | RCPatAtom id -> + begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end + | RCPatCstr (id,l1,l2) -> + Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) + | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a) + | RCPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl) let drop_notations_pattern looked_for = (* At toplevel, Constructors and Inductives are accepted, in recursive calls @@ -1250,46 +1249,46 @@ let drop_notations_pattern looked_for = let (_,argscs) = find_remaining_scopes [] pats g in Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) with Not_found -> None - and in_pat top scopes = function - | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id) - | CPatRecord (loc, l) -> + and in_pat top scopes (loc, pt) = match pt with + | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id) + | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in + sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in begin match sorted_fields with - | None -> RCPatAtom (loc, None) + | None -> Loc.tag ~loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = if !asymmetric_patterns then pl else - let pars = List.make n (CPatAtom (loc, None)) in + let pars = List.make n (loc, CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with - |Some (a,b,c) -> RCPatCstr(loc, a, b, c) + |Some (a,b,c) -> (loc, RCPatCstr(a, b, c)) |None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, head, None, pl) -> + | CPatCstr (head, None, pl) -> begin match drop_syndef top scopes head pl with - | Some (a,b,c) -> RCPatCstr(loc, a, b, c) + | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, Some expl_pl, pl) -> + | CPatCstr (r, Some expl_pl, pl) -> let g = try locate (snd (qualid_of_reference r)) with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) - RCPatCstr (loc, g, List.map (in_pat false scopes) pl, []) + Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) else (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) (* but not scopes in expl_pl *) 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)],[]),[]) + Loc.tag ~loc @@ RCPatCstr (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) - | CPatNotation (_,"( _ )",([a],[]),[]) -> + | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a - | CPatNotation (loc, ntn, fullargs,extrargs) -> + | CPatNotation (ntn, fullargs,extrargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in let ((ids',c),df) = Notation.interp_notation loc ntn scopes in let (ids',idsl',_) = split_by_type ids' in @@ -1297,18 +1296,17 @@ let drop_notations_pattern looked_for = let substlist = make_subst idsl' argsl in let subst = make_subst ids' args in in_not top loc scopes (subst,substlist) extrargs c - | CPatDelimiters (loc, key, e) -> + | CPatDelimiters (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) - | CPatAtom (loc, Some id) -> + | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes) + | CPatAtom Some id -> begin match drop_syndef top scopes id [] with - |Some (a,b,c) -> RCPatCstr (loc, a, b, c) - |None -> RCPatAtom (loc, Some (find_pattern_variable id)) + | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c) + | None -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id)) end - | CPatAtom (loc,None) -> RCPatAtom (loc,None) - | CPatOr (loc, pl) -> - RCPatOr (loc,List.map (in_pat top scopes) pl) + | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None + | CPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl) | CPatCast _ -> assert false and in_pat_sc scopes x = in_pat false (x,snd scopes) @@ -1322,17 +1320,17 @@ let drop_notations_pattern looked_for = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then RCPatAtom (loc,Some id) else + if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id) end | NRef g -> ensure_kind top loc g; let (_,argscs) = find_remaining_scopes [] args g in - RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args) + Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - RCPatCstr (loc, g, + Loc.tag ~loc @@ RCPatCstr (g, List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> @@ -1351,7 +1349,7 @@ let drop_notations_pattern looked_for = anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NHole _ -> let () = assert (List.is_empty args) in - RCPatAtom (loc, None) + Loc.tag ~loc @@ RCPatAtom None | t -> error_invalid_pattern_notation ~loc () in in_pat true @@ -1363,10 +1361,10 @@ let rec intern_pat genv aliases pat = (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in match pat with - | RCPatAlias (loc, p, id) -> + | loc, RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in intern_pat genv aliases' p - | RCPatCstr (loc, head, expl_pl, pl) -> + | loc, RCPatCstr (head, expl_pl, pl) -> if !asymmetric_patterns then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in @@ -1378,13 +1376,13 @@ let rec intern_pat genv aliases pat = 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) -> + | loc, RCPatAtom (Some id) -> let aliases = merge_aliases aliases id in (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)]) - | RCPatAtom (loc, None) -> + | loc, RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in (ids, [asubst, PatVar (loc, alias_of aliases)]) - | RCPatOr (loc, pl) -> + | loc, RCPatOr pl -> assert (not (List.is_empty pl)); let pl' = List.map (intern_pat genv aliases) pl in let (idsl,pl') = List.split pl' in @@ -1402,21 +1400,21 @@ let rec intern_pat genv aliases pat = 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,_,_) -> +let rec check_no_patcast (loc, pt) = match pt with + | CPatCast (_,_) -> 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) -> + | 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) -> + | CPatOr pl -> List.iter check_no_patcast pl - | CPatNotation(_,_,subst,pl) -> + | CPatNotation(_,subst,pl) -> check_no_patcast_subst subst; List.iter check_no_patcast pl - | CPatRecord(_,prl) -> + | CPatRecord prl -> List.iter (fun (_,p) -> check_no_patcast p) prl | CPatAtom _ | CPatPrim _ -> () @@ -1441,7 +1439,7 @@ let intern_ind_pattern genv scopes pat = with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc in match no_not with - | RCPatCstr (loc, head, expl_pl, pl) -> + | loc, RCPatCstr (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 @@ -1784,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (ids,List.flatten mpl') (* Expands a pattern-matching clause [lhs => rhs] *) - and intern_eqn n env (loc,lhs,rhs) = + and intern_eqn n env (loc,(lhs,rhs)) = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; diff --git a/interp/modintern.ml b/interp/modintern.ml index d4ade7058..166711659 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -65,17 +65,16 @@ let transl_with_decl env = function let ctx = Evd.evar_context_universe_context ectx in WithDef (fqid,(c,ctx)) -let loc_of_module = function - | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc +let loc_of_module (l, _) = l (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind = function +let rec interp_module_ast env kind (loc, m) = match m with | CMident qid -> - let (mp,kind) = lookup_module_or_modtype kind qid in + let (mp,kind) = lookup_module_or_modtype kind (loc,qid) in (MEident mp, kind) - | CMapply (_,me1,me2) -> + | CMapply (me1,me2) -> let me1',kind1 = interp_module_ast env kind me1 in let me2',kind2 = interp_module_ast env ModAny me2 in let mp2 = match me2' with @@ -85,7 +84,7 @@ let rec interp_module_ast env kind = function if kind2 == ModType then error_application_to_module_type (loc_of_module me2); (MEapply (me1',mp2), kind1) - | CMwith (loc,me,decl) -> + | CMwith (me,decl) -> let me,kind = interp_module_ast env kind me in if kind == Module then error_incorrect_with_in_module loc; let decl = transl_with_decl env decl in diff --git a/interp/notation.ml b/interp/notation.ml index 90ac7f729..04711808b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -472,11 +472,11 @@ let interp_prim_token = (** [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,[],[]) + | GVar (loc,id) -> Loc.tag ~loc @@ RCPatAtom (Some id) + | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None) + | GRef (loc,g,_) -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[]) | GApp (loc,GRef (_,g,_),l) -> - looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) + looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[]) | _ -> raise Not_found let interp_prim_token_cases_pattern_expr loc looked_for p = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index d3142e7f0..172caa2ca 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -43,22 +43,22 @@ let is_constructor id = (Nametab.locate_extended (qualid_of_ident id))) with Not_found -> false -let rec cases_pattern_fold_names f a = function - | CPatRecord (_, l) -> +let rec cases_pattern_fold_names f a pt = match snd pt with + | CPatRecord l -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (_,pat,id) -> f id a - | CPatOr (_,patl) -> + | CPatAlias (pat,id) -> f id a + | CPatOr (patl) -> List.fold_left (cases_pattern_fold_names f) a patl - | CPatCstr (_,_,patl1,patl2) -> + | CPatCstr (_,patl1,patl2) -> List.fold_left (cases_pattern_fold_names f) (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,_,(patl,patll),patl') -> + | 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 + | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat + | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a - | CPatCast (loc,_,_) -> + | CPatCast ((loc,_),_) -> CErrors.user_err ~loc ~hdr:"cases_pattern_fold_names" (Pp.strbrk "Casts are not supported here.") @@ -125,7 +125,7 @@ let fold_constr_expr_with_binders g f n acc = function let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in - List.fold_right (fun (loc,patl,rhs) acc -> + List.fold_right (fun (loc,(patl,rhs)) acc -> let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (loc,nal,(ona,po),b,c) -> @@ -230,9 +230,9 @@ let map_constr_expr_with_binders g f e = function | CPrim _ | CRef _ as x -> x | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> - let bl = List.map (fun (loc,patl,rhs) -> + let bl = List.map (fun (loc,(patl,rhs)) -> let ids = ids_of_pattern_list patl in - (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in + (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in let ids = ids_of_cases_tomatch a in let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) |