aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml8
-rw-r--r--parsing/g_constr.ml466
-rw-r--r--parsing/g_prim.ml426
-rw-r--r--parsing/g_vernac.ml420
4 files changed, 62 insertions, 58 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c8fe96f74..49bf267db 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -313,13 +313,13 @@ let interp_entry forpat e = match e with
| ETBinderList (true, _) -> assert false
| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
-let constr_expr_of_name (loc,na) = Loc.tag ~loc @@ match na with
+let constr_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
| Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
- | Name id -> CRef (Ident (loc,id), None)
+ | Name id -> CRef (Ident (Loc.tag ?loc id), None)
-let cases_pattern_expr_of_name (loc,na) = Loc.tag ~loc @@ match na with
+let cases_pattern_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
| Anonymous -> CPatAtom None
- | Name id -> CPatAtom (Some (Ident (loc,id)))
+ | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
type 'r env = {
constrs : 'r list;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e6c82c894..45585d9ce 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -33,12 +33,12 @@ let _ = List.iter CLexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) ->
- let loc = Loc.merge (constr_loc c) (constr_loc ty)
- in Loc.tag ~loc @@ CCast(c, CastConv ty)
+ let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
+ in Loc.tag ?loc @@ CCast(c, CastConv ty)
let binder_of_name expl (loc,na) =
CLocalAssum ([loc, na], Default expl,
- Loc.tag ~loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
+ Loc.tag ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
let binders_of_names l =
List.map (binder_of_name Explicit) l
@@ -51,7 +51,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
let _ = Option.map (fun (aloc,_) ->
- CErrors.user_err ~loc:aloc
+ CErrors.user_err ?loc:aloc
~hdr:"Constr:mk_cofixb"
(Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
let ty = match tyc with
@@ -131,7 +131,7 @@ GEXTEND Gram
[ [ id = Prim.ident -> id ] ]
;
Prim.name:
- [ [ "_" -> (!@loc, Anonymous) ] ]
+ [ [ "_" -> Loc.tag ~loc:!@loc Anonymous ] ]
;
global:
[ [ r = Prim.reference -> r ] ]
@@ -183,13 +183,13 @@ GEXTEND Gram
| "90" RIGHTA [ ]
| "10" LEFTA
[ f=operconstr; args=LIST1 appl_arg -> Loc.tag ~loc:(!@loc) @@ CApp((None,f),args)
- | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:(!@loc) @@ CAppExpl((None,f,i),args)
+ | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),args)
| "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
let args = List.map (fun x -> Loc.tag @@ CRef (Ident x,None), None) args in
- Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ~loc:locid @@ CPatVar id),args) ]
+ Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ?loc:locid @@ CPatVar id),args) ]
| "9"
[ ".."; c = operconstr LEVEL "0"; ".." ->
- Loc.tag ~loc:(!@loc) @@ CAppExpl ((None, Ident (!@loc,ldots_var),None),[c]) ]
+ Loc.tag ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ]
| "8" [ ]
| "1" LEFTA
[ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
@@ -236,10 +236,10 @@ GEXTEND Gram
| "let"; id=name; bl = binders; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
let ty,c1 = match ty, c1 with
- | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ~loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+ | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
| _, _ -> ty, c1 in
- Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ~loc:(constr_loc c1) bl c1,
- Option.map (mkCProdN ~loc:(fst ty) bl) (snd ty), c2)
+ Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
+ Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2)
| "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
let fixp = mk_single_fix fx in
let (li,id) = match snd fixp with
@@ -254,14 +254,18 @@ GEXTEND Gram
Loc.tag ~loc:!@loc @@ CLetTuple (lb,po,c1,c2)
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
- Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+ Loc.tag ~loc:!@loc @@
+ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
- Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+ Loc.tag ~loc:!@loc @@
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
- Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+ Loc.tag ~loc:!@loc @@
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -270,7 +274,7 @@ GEXTEND Gram
;
appl_arg:
[ [ id = lpar_id_coloneq; c=lconstr; ")" ->
- (c,Some (!@loc,ExplByName id))
+ (c,Some (Loc.tag ~loc:!@loc @@ ExplByName id))
| c=operconstr LEVEL "9" -> (c,None) ] ]
;
atomic_constr:
@@ -345,7 +349,7 @@ GEXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
;
mult_pattern:
- [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (!@loc,pl) ] ]
+ [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ]
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
@@ -364,7 +368,7 @@ GEXTEND Gram
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
- [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> !@loc, CPatOr (p::pl) ]
+ [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> Loc.tag ~loc:!@loc @@ CPatOr (p::pl) ]
| "99" RIGHTA [ ]
| "11" LEFTA
[ p = pattern; "as"; id = ident ->
@@ -374,21 +378,21 @@ GEXTEND Gram
(match p with
| _, CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
| loc, CPatCstr (r, None, l2) ->
- CErrors.user_err ~loc ~hdr:"compound_pattern"
+ 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."))
+ ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
+ (Pp.str "Such pattern cannot have arguments."))
|"@"; r = Prim.reference; lp = LIST0 NEXT ->
- !@loc, CPatCstr (r, Some lp, []) ]
+ Loc.tag ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
| "1" LEFTA
- [ c = pattern; "%"; key=IDENT -> !@loc, CPatDelimiters (key,c) ]
+ [ c = pattern; "%"; key=IDENT -> Loc.tag ~loc:!@loc @@ CPatDelimiters (key,c) ]
| "0"
[ r = Prim.reference -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
| "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
- | "_" -> !@loc, CPatAtom None
+ | "_" -> Loc.tag ~loc:!@loc @@ CPatAtom None
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
| _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
@@ -401,7 +405,7 @@ GEXTEND Gram
Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
| _ -> p
in
- !@loc, CPatCast (p, ty)
+ Loc.tag ~loc:!@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) ] ]
;
@@ -411,7 +415,7 @@ GEXTEND Gram
(fun na -> CLocalAssum (na::nal,Default Implicit,c))
| nal=LIST1 name; "}" ->
(fun na -> CLocalAssum (na::nal,Default Implicit,
- Loc.tag ~loc:(Loc.merge (fst na) !@loc) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+ Loc.tag ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
| ":"; c=lconstr; "}" ->
(fun na -> CLocalAssum ([na],Default Implicit,c))
] ]
@@ -424,7 +428,7 @@ GEXTEND Gram
] ]
;
impl_name_head:
- [ [ id = impl_ident_head -> (!@loc,Name id) ] ]
+ [ [ id = impl_ident_head -> (Loc.tag ~loc:!@loc @@ Name id) ] ]
;
binders_fixannot:
[ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
@@ -444,7 +448,7 @@ GEXTEND Gram
| id = name; idl = LIST0 name; bl = binders ->
binders_of_names (id::idl) @ bl
| id1 = name; ".."; id2 = name ->
- [CLocalAssum ([id1;(!@loc,Name ldots_var);id2],
+ [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2],
Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
| bl = closed_binder; bl' = binders ->
bl@bl'
@@ -490,17 +494,17 @@ GEXTEND Gram
] ]
;
typeclass_constraint:
- [ [ "!" ; c = operconstr LEVEL "200" -> (!@loc, Anonymous), true, c
+ [ [ "!" ; c = operconstr LEVEL "200" -> (Loc.tag ~loc:!@loc Anonymous), true, c
| "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
id, expl, c
| iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
- (!@loc, iid), expl, c
+ (Loc.tag ~loc:!@loc iid), expl, c
| c = operconstr LEVEL "200" ->
- (!@loc, Anonymous), false, c
+ (Loc.tag ~loc:!@loc Anonymous), false, c
] ]
;
type_cstr:
- [ [ c=OPT [":"; c=lconstr -> c] -> (!@loc,c) ] ]
+ [ [ c=OPT [":"; c=lconstr -> c] -> Loc.tag ~loc:!@loc c ] ]
;
END;;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index ed6a8df4e..d94c5e963 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -44,13 +44,13 @@ GEXTEND Gram
[ [ LEFTQMARK; id = ident -> id ] ]
;
pattern_identref:
- [ [ id = pattern_ident -> (!@loc, id) ] ]
+ [ [ id = pattern_ident -> Loc.tag ~loc:!@loc id ] ]
;
var: (* as identref, but interpret as a term identifier in ltac *)
- [ [ id = ident -> (!@loc, id) ] ]
+ [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
;
identref:
- [ [ id = ident -> (!@loc, id) ] ]
+ [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
;
field:
[ [ s = FIELD -> Id.of_string s ] ]
@@ -61,8 +61,8 @@ GEXTEND Gram
] ]
;
fullyqualid:
- [ [ id = ident; (l,id')=fields -> !@loc,id::List.rev (id'::l)
- | id = ident -> !@loc,[id]
+ [ [ id = ident; (l,id')=fields -> Loc.tag ~loc:!@loc @@ id::List.rev (id'::l)
+ | id = ident -> Loc.tag ~loc:!@loc [id]
] ]
;
basequalid:
@@ -71,13 +71,13 @@ GEXTEND Gram
] ]
;
name:
- [ [ IDENT "_" -> (!@loc, Anonymous)
- | id = ident -> (!@loc, Name id) ] ]
+ [ [ IDENT "_" -> Loc.tag ~loc:!@loc Anonymous
+ | id = ident -> Loc.tag ~loc:!@loc @@ Name id ] ]
;
reference:
[ [ id = ident; (l,id') = fields ->
- Qualid (!@loc, local_make_qualid (l@[id]) id')
- | id = ident -> Ident (!@loc,id)
+ Qualid (Loc.tag ~loc:!@loc @@ local_make_qualid (l@[id]) id')
+ | id = ident -> Ident (Loc.tag ~loc:!@loc id)
] ]
;
by_notation:
@@ -88,15 +88,15 @@ GEXTEND Gram
| ntn = by_notation -> Misctypes.ByNotation ntn ] ]
;
qualid:
- [ [ qid = basequalid -> !@loc, qid ] ]
+ [ [ qid = basequalid -> Loc.tag ~loc:!@loc qid ] ]
;
ne_string:
[ [ s = STRING ->
- if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
+ if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s
] ]
;
ne_lstring:
- [ [ s = ne_string -> (!@loc, s) ] ]
+ [ [ s = ne_string -> Loc.tag ~loc:!@loc s ] ]
;
dirpath:
[ [ id = ident; l = LIST0 field ->
@@ -106,7 +106,7 @@ GEXTEND Gram
[ [ s = STRING -> s ] ]
;
lstring:
- [ [ s = string -> (!@loc, s) ] ]
+ [ [ s = string -> (Loc.tag ~loc:!@loc s) ] ]
;
integer:
[ [ i = INT -> my_int_of_string (!@loc) i
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7a3a2ace1..c8101875d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -102,7 +102,7 @@ GEXTEND Gram
;
located_vernac:
- [ [ v = vernac -> !@loc, v ] ]
+ [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ]
;
END
@@ -542,8 +542,8 @@ GEXTEND Gram
starredidentref:
[ [ i = identref -> SsSingl i
| i = identref; "*" -> SsFwdClose(SsSingl i)
- | "Type" -> SsSingl (!@loc, Id.of_string "Type")
- | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+ | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")
+ | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]]
;
ssexpr:
[ "35"
@@ -720,7 +720,7 @@ GEXTEND Gram
;
argument_spec: [
[ b = OPT "!"; id = name ; s = OPT scope ->
- snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s
+ snd id, not (Option.is_empty b), Option.map (fun x -> Loc.tag ~loc:!@loc x) s
]
];
(* List of arguments implicit status, scope, modifiers *)
@@ -733,7 +733,7 @@ GEXTEND Gram
| "/" -> [`Slash]
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+ | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
| Some _, Some _ -> error "scope declared twice" in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -741,7 +741,7 @@ GEXTEND Gram
implicit_status = NotImplicit}) items
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+ | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
| Some _, Some _ -> error "scope declared twice" in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -749,7 +749,7 @@ GEXTEND Gram
implicit_status = Implicit}) items
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+ | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
| Some _, Some _ -> error "scope declared twice" in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -782,7 +782,7 @@ GEXTEND Gram
[ [ name = pidentref; sup = OPT binders ->
(let ((loc,id),l) = name in ((loc, Name id),l)),
(Option.default [] sup)
- | -> ((!@loc, Anonymous), None), [] ] ]
+ | -> ((Loc.tag ~loc:!@loc Anonymous), None), [] ] ]
;
hint_info:
[ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
@@ -1149,8 +1149,8 @@ GEXTEND Gram
| IDENT "only"; IDENT "parsing" -> SetOnlyParsing
| IDENT "compat"; s = STRING ->
SetCompatVersion (Coqinit.get_compat_version s)
- | IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
- s2 = OPT [s = STRING -> (!@loc,s)] ->
+ | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s];
+ s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] ->
begin match s1, s2 with
| (_,k), Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 17:16:19 +0000