aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/texmacspp.ml22
-rw-r--r--interp/constrexpr_ops.ml41
-rw-r--r--interp/constrextern.ml52
-rw-r--r--interp/constrintern.ml114
-rw-r--r--interp/modintern.ml11
-rw-r--r--interp/notation.ml8
-rw-r--r--interp/topconstr.ml24
-rw-r--r--intf/constrexpr.mli43
-rw-r--r--lib/loc.ml4
-rw-r--r--lib/loc.mli17
-rw-r--r--parsing/egramcoq.ml14
-rw-r--r--parsing/g_constr.ml452
-rw-r--r--parsing/g_vernac.ml411
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--printing/ppconstr.ml38
-rw-r--r--printing/ppvernac.ml12
16 files changed, 232 insertions, 233 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e20704b7fb..19be13be78 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -300,32 +300,32 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
end
and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
+and pp_cases_pattern_expr (loc, cpe) =
match cpe with
- | CPatAlias (loc, cpe, id) ->
+ | CPatAlias (cpe, id) ->
xmlApply loc
(xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
[pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, None, cpel2) ->
+ | CPatCstr (ref, None, cpel2) ->
xmlApply loc
(xmlOperator "reference"
~attr:["name", Libnames.string_of_reference ref] loc ::
[Element ("impargs", [], []);
Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatCstr (loc, ref, Some cpel1, cpel2) ->
+ | CPatCstr (ref, Some cpel1, cpel2) ->
xmlApply loc
(xmlOperator "reference"
~attr:["name", Libnames.string_of_reference ref] loc ::
[Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
+ | CPatAtom optr ->
let attrs = match optr with
| None -> []
| Some r -> ["name", Libnames.string_of_reference r] in
xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
+ | CPatOr cpel ->
xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+ | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
xmlApply loc
(xmlOperator "notation" loc ::
[xmlOperator n loc;
@@ -339,8 +339,8 @@ and pp_cases_pattern_expr cpe =
List.map pp_cases_pattern_expr cpel))
subst_rec)]);
Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
+ | CPatPrim tok -> pp_token loc tok
+ | CPatRecord rcl ->
xmlApply loc
(xmlOperator "record" loc ::
List.map (fun (r, cpe) ->
@@ -348,7 +348,7 @@ and pp_cases_pattern_expr cpe =
["reference", Libnames.string_of_reference r],
[pp_cases_pattern_expr cpe]))
rcl)
- | CPatDelimiters (loc, delim, cpe) ->
+ | CPatDelimiters (delim, cpe) ->
xmlApply loc
(xmlOperator "delimiter" ~attr:["name", delim] loc ::
[pp_cases_pattern_expr cpe])
@@ -370,7 +370,7 @@ and pp_case_expr (e, name, pat) =
and pp_branch_expr_list bel =
xmlWith
(List.map
- (fun (_, cpel, e) ->
+ (fun (_, (cpel, e)) ->
let ppcepl =
List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
let ppe = [pp_expr e] in
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff8..3ba5d985f9 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 59b8b4e5b9..7a229856e0 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 d75487ecf3..6bf6772c61 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 d4ade7058a..166711659f 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 90ac7f7296..04711808b7 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 d3142e7f0c..172caa2caa 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)
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..c1de0ce246 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -36,31 +36,33 @@ type prim_token =
| Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
| String of string
-type raw_cases_pattern_expr =
- | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
- | RCPatCstr of Loc.t * Globnames.global_reference
+type raw_cases_pattern_expr_r =
+ | RCPatAlias of raw_cases_pattern_expr * Id.t
+ | RCPatCstr of Globnames.global_reference
* raw_cases_pattern_expr list * raw_cases_pattern_expr list
(** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
- | RCPatAtom of Loc.t * Id.t option
- | RCPatOr of Loc.t * raw_cases_pattern_expr list
+ | RCPatAtom of Id.t option
+ | RCPatOr of raw_cases_pattern_expr list
+and raw_cases_pattern_expr = raw_cases_pattern_expr_r Loc.located
type instance_expr = Misctypes.glob_level list
-type cases_pattern_expr =
- | CPatAlias of Loc.t * cases_pattern_expr * Id.t
- | CPatCstr of Loc.t * reference
+type cases_pattern_expr_r =
+ | CPatAlias of cases_pattern_expr * Id.t
+ | CPatCstr of reference
* cases_pattern_expr list option * cases_pattern_expr list
(** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
- | CPatAtom of Loc.t * reference option
- | CPatOr of Loc.t * cases_pattern_expr list
- | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
+ | CPatAtom of reference option
+ | CPatOr of cases_pattern_expr list
+ | CPatNotation of 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.t * prim_token
- | CPatRecord of Loc.t * (reference * cases_pattern_expr) list
- | CPatDelimiters of Loc.t * string * cases_pattern_expr
- | CPatCast of Loc.t * cases_pattern_expr * constr_expr
+ | CPatPrim of prim_token
+ | CPatRecord of (reference * cases_pattern_expr) list
+ | CPatDelimiters of string * cases_pattern_expr
+ | CPatCast of cases_pattern_expr * constr_expr
+and cases_pattern_expr = cases_pattern_expr_r located
and cases_pattern_notation_substitution =
cases_pattern_expr list * (** for constr subterms *)
@@ -104,7 +106,7 @@ and case_expr = constr_expr (* expression that is being matched
* cases_pattern_expr option (* in-clause *)
and branch_expr =
- Loc.t * cases_pattern_expr list located list * constr_expr
+ (cases_pattern_expr list located list * constr_expr) Loc.located
and binder_expr =
Name.t located list * binder_kind * constr_expr
@@ -144,7 +146,8 @@ type with_declaration_ast =
| CWith_Module of Id.t list located * qualid located
| CWith_Definition of Id.t list located * constr_expr
-type module_ast =
- | CMident of qualid located
- | CMapply of Loc.t * module_ast * module_ast
- | CMwith of Loc.t * module_ast * with_declaration_ast
+type module_ast_r =
+ | CMident of qualid
+ | CMapply of module_ast * module_ast
+ | CMwith of module_ast * with_declaration_ast
+and module_ast = module_ast_r located
diff --git a/lib/loc.ml b/lib/loc.ml
index e373a760cb..39f2d7dfba 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -59,6 +59,10 @@ let join_loc = merge
(** Located type *)
type 'a located = t * 'a
+
+let to_pair x = x
+let tag ?loc x = Option.default ghost loc, x
+
let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
let down_located f (_,a) = f a
diff --git a/lib/loc.mli b/lib/loc.mli
index bb88f86428..fef1d89388 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -18,9 +18,6 @@ type t = {
ep : int; (** end position *)
}
-type 'a located = t * 'a
-(** Embed a location in a type *)
-
(** {5 Location manipulation} *)
(** This is inherited from CAMPL4/5. *)
@@ -54,12 +51,22 @@ val get_loc : Exninfo.info -> t option
val raise : ?loc:t -> exn -> 'a
(** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
-(** {5 Location utilities} *)
+(** {5 Objects with location information } *)
+
+type 'a located = t * 'a
+(** Embed a location in a type *)
+
+(** Warning, this API is experimental *)
+
+val to_pair : 'a located -> t * 'a
+val tag : ?loc:t -> 'a -> 'a located
val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val down_located : ('a -> 'b) -> 'a located -> 'b
+
+(* Current not used *)
val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
-val down_located : ('a -> 'b) -> 'a located -> 'b
(** Projects out a located object *)
(** {5 Backward compatibility} *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 496b200020..a973a539a6 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -318,8 +318,8 @@ let constr_expr_of_name (loc,na) = match na with
| Name id -> CRef (Ident (loc,id), None)
let cases_pattern_expr_of_name (loc,na) = match na with
- | Anonymous -> CPatAtom (loc,None)
- | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
+ | Anonymous -> Loc.tag ~loc @@ CPatAtom None
+ | Name id -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
type 'r env = {
constrs : 'r list;
@@ -342,13 +342,13 @@ match e with
| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
| TTBigint ->
begin match forpat with
- | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
- | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v))
+ | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
+ | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v))
end
| TTReference ->
begin match forpat with
- | ForConstr -> push_constr subst (CRef (v, None))
- | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v))
+ | ForConstr -> push_constr subst (CRef (v, None))
+ | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v))
end
| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
@@ -436,7 +436,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
let invalid = List.exists (fun (_, b) -> not b) env.binders in
let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in
let env = (env.constrs, env.constrlists) in
- CPatNotation (loc, notation, env, [])
+ Loc.tag ~loc @@ CPatNotation (notation, env, [])
let extend_constr state forpat ng =
let n = ng.notgram_level in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f2ed88fea..6ca8134c06 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -120,7 +120,7 @@ let name_colon =
| _ -> err ())
| _ -> err ())
-let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
+let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
@@ -254,14 +254,14 @@ GEXTEND Gram
CLetTuple (!@loc,lb,po,c1,c2)
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
+ CCases (!@loc, LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
+ CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
- CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
+ CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -349,7 +349,7 @@ GEXTEND Gram
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
- "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
+ "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ]
;
record_pattern:
[ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
@@ -364,46 +364,46 @@ GEXTEND Gram
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
- [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
+ [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> !@loc, CPatOr (p::pl) ]
| "99" RIGHTA [ ]
| "11" LEFTA
[ p = pattern; "as"; id = ident ->
- CPatAlias (!@loc, p, id) ]
+ Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ]
| "10" RIGHTA
[ p = pattern; lp = LIST1 NEXT ->
(match p with
- | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
- | CPatCstr (_, r, None, l2) -> CErrors.user_err
- ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
- (Pp.str "Nested applications not supported.")
- | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
- | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
+ | _, CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
+ | loc, CPatCstr (r, None, l2) ->
+ CErrors.user_err ~loc ~hdr:"compound_pattern"
+ (Pp.str "Nested applications not supported.")
+ | _, CPatCstr (r, l1, l2) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
+ | _, CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp)
| _ -> CErrors.user_err
~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
(Pp.str "Such pattern cannot have arguments."))
|"@"; r = Prim.reference; lp = LIST0 NEXT ->
- CPatCstr (!@loc, r, Some lp, []) ]
+ !@loc, CPatCstr (r, Some lp, []) ]
| "1" LEFTA
- [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
+ [ c = pattern; "%"; key=IDENT -> !@loc, CPatDelimiters (key,c) ]
| "0"
- [ r = Prim.reference -> CPatAtom (!@loc,Some r)
- | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
- | "_" -> CPatAtom (!@loc,None)
+ [ r = Prim.reference -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
+ | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
+ | "_" -> !@loc, CPatAtom None
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
- CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CPatNotation(!@loc,"( _ )",([p],[]),[])
+ | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+ Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
| _ -> p)
| "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
let p =
match p with
- CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CPatNotation(!@loc,"( _ )",([p],[]),[])
+ | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+ Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
| _ -> p
in
- CPatCast (!@loc, p, ty)
- | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
- | s = string -> CPatPrim (!@loc, String s) ] ]
+ !@loc, CPatCast (p, ty)
+ | n = INT -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+ | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ]
;
impl_ident_tail:
[ [ "}" -> binder_of_name Implicit
@@ -482,7 +482,7 @@ GEXTEND Gram
| "'"; p = pattern LEVEL "0" ->
let (p, ty) =
match p with
- | CPatCast (_, p, ty) -> (p, Some ty)
+ | _, CPatCast (p, ty) -> (p, Some ty)
| _ -> (p, None)
in
[CLocalPattern (!@loc, p, ty)]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 011565d86a..a43f1127a9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -511,11 +511,11 @@ GEXTEND Gram
(* Module expressions *)
module_expr:
[ [ me = module_expr_atom -> me
- | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2)
+ | me1 = module_expr; me2 = module_expr_atom -> Loc.tag ~loc:!@loc @@ CMapply (me1,me2)
] ]
;
module_expr_atom:
- [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ]
+ [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
@@ -525,11 +525,12 @@ GEXTEND Gram
] ]
;
module_type:
- [ [ qid = qualid -> CMident qid
+ [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid)
| "("; mt = module_type; ")" -> mt
- | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me)
+ | mty = module_type; me = module_expr_atom ->
+ Loc.tag ~loc:!@loc @@ CMapply (mty,me)
| mty = module_type; "with"; decl = with_declaration ->
- CMwith (!@loc,mty,decl)
+ Loc.tag ~loc:!@loc @@ CMwith (mty,decl)
] ]
;
(* Proof using *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d335836dfc..daa5cbb3fb 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -760,7 +760,7 @@ let rec add_args id new_args b =
List.map (fun (b,na,b_option) ->
add_args id new_args b,
na, b_option) cel,
- List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
+ List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc:loc @@ (cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b96..966ba6734f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -252,62 +252,62 @@ let tag_var = tag Tag.variable
let lpator = 100
let lpatrec = 0
- let rec pr_patt sep inh p =
+ let rec pr_patt sep inh (loc, p) =
let (strm,prec) = match p with
- | CPatRecord (_, l) ->
+ | CPatRecord l ->
let pp (c, p) =
pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
in
str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
- | CPatAlias (_, p, id) ->
+ | CPatAlias (p, id) ->
pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
- | CPatCstr (_,c, None, []) ->
+ | CPatCstr (c, None, []) ->
pr_reference c, latom
- | CPatCstr (_, c, None, args) ->
+ | CPatCstr (c, None, args) ->
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, Some args, []) ->
+ | CPatCstr (c, Some args, []) ->
str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, Some expl_args, extra_args) ->
+ | CPatCstr (c, Some 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) ->
+ | CPatAtom (None) ->
str "_", latom
- | CPatAtom (_,Some r) ->
+ | CPatAtom (Some r) ->
pr_reference r, latom
- | CPatOr (_,pl) ->
+ | 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),args) ->
+ | CPatNotation (s,(l,ll),args) ->
let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in
(if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
- | CPatPrim (_,p) ->
+ | CPatPrim p ->
pr_prim_token p, latom
- | CPatDelimiters (_,k,p) ->
+ | CPatDelimiters (k,p) ->
pr_delimiters k (pr_patt mt lsimplepatt p), 1
| CPatCast _ ->
assert false
in
- let loc = cases_pattern_expr_loc p in
+ let loc = cases_pattern_expr_loc (loc, p) in
pr_with_comments loc
(sep() ++ if prec_less prec inh then strm else surround strm)
let pr_patt = pr_patt mt
- let pr_eqn pr (loc,pl,rhs) =
+ let pr_eqn pr (loc,(pl,rhs)) =
let pl = List.map snd pl in
spc() ++ hov 4
(pr_with_comments loc
@@ -397,7 +397,7 @@ let tag_var = tag Tag.variable
| CProdN (loc,[],c) ->
extract_prod_binders c
| CProdN (loc,[[_,Name id],bk,t],
- CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
let bl,c = extract_prod_binders b in
CLocalPattern (loc,p,None) :: bl, c
@@ -413,7 +413,7 @@ let tag_var = tag Tag.variable
| CLambdaN (loc,[],c) ->
extract_lam_binders c
| CLambdaN (loc,[[_,Name id],bk,t],
- CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
let bl,c = extract_lam_binders b in
CLocalPattern (loc,p,None) :: bl, c
@@ -642,7 +642,7 @@ let tag_var = tag Tag.variable
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
+ | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e4a87739b1..2e064454c1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -204,18 +204,18 @@ open Decl_kinds
pr_located pr_qualid qid
let rec pr_module_ast leading_space pr_c = function
- | CMident qid ->
+ | loc, CMident qid ->
if leading_space then
- spc () ++ pr_located pr_qualid qid
+ spc () ++ pr_located pr_qualid (loc, qid)
else
- pr_located pr_qualid qid
- | CMwith (_,mty,decl) ->
+ pr_located pr_qualid (loc,qid)
+ | _loc, CMwith (mty,decl) ->
let m = pr_module_ast leading_space pr_c mty in
let p = pr_with_declaration pr_c decl in
m ++ spc() ++ keyword "with" ++ spc() ++ p
- | CMapply (_,me1,(CMident _ as me2)) ->
+ | _loc, CMapply (me1,(_, CMident _ as me2)) ->
pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
- | CMapply (_,me1,me2) ->
+ | _loc, CMapply (me1,me2) ->
pr_module_ast leading_space pr_c me1 ++ spc() ++
hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 21:00:31 +0000