aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.ml46
-rw-r--r--grammar/grammar.mllib2
-rw-r--r--grammar/q_constr.ml42
-rw-r--r--grammar/q_coqast.ml447
-rw-r--r--grammar/q_util.ml412
-rw-r--r--grammar/tacextend.ml424
-rw-r--r--grammar/vernacextend.ml49
7 files changed, 67 insertions, 35 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index cc378ceda6..a3c94c5d4f 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -13,7 +13,7 @@ open Q_util
open Egramml
open Compat
-let loc = Loc.ghost
+let loc = CompatLoc.ghost
let default_loc = <:expr< Loc.ghost >>
let mk_extraarg prefix s =
@@ -314,10 +314,10 @@ EXTEND
genarg:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let t, g = interp_entry_name false None e "" in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let t, g = interp_entry_name false None e sep in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| s = STRING ->
if String.length s > 0 && Util.is_letter s.[0] then
Lexer.add_keyword s;
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index afb8ac4e66..7d91550df4 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,10 +1,10 @@
Coq_config
Pp_control
-Compat
Flags
Pp
Loc
+Compat
Errors
CList
CArray
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index 8943b2b638..5d46897c60 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -13,7 +13,7 @@ open Compat
open Pcaml
open PcamlSig
-let loc = Loc.ghost
+let loc = CompatLoc.ghost
let dloc = <:expr< Loc.ghost >>
let apply_ref f l =
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3d39d13d7f..cbbc9e1871 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -20,7 +20,7 @@ let anti loc x =
expl_anti loc <:expr< $lid:purge_str x$ >>
(* We don't give location for tactic quotation! *)
-let loc = Loc.ghost
+let loc = CompatLoc.ghost
let dloc = <:expr< Loc.ghost >>
@@ -41,16 +41,21 @@ let mlexpr_of_qualid qid =
<:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
let mlexpr_of_reference = function
- | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
- | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+ | Libnames.Qualid (loc,qid) ->
+ let loc = of_coqloc loc in <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
+ | Libnames.Ident (loc,id) ->
+ let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
-let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
+let mlexpr_of_located f (loc,x) =
+ let loc = of_coqloc loc in
+ <:expr< ($dloc$, $f x$) >>
let mlexpr_of_loc loc = <:expr< $dloc$ >>
let mlexpr_of_by_notation f = function
| Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >>
| Misctypes.ByNotation (loc,s,sco) ->
+ let loc = of_coqloc loc in
<:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
let mlexpr_of_intro_pattern = function
@@ -135,24 +140,36 @@ let mlexpr_of_binder_kind = function
let rec mlexpr_of_constr = function
| Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
+ let loc = of_coqloc loc in
anti loc (string_of_id id)
| Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
| Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
| Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Constrexpr.CProdN (loc,l,a) -> <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list
+ | Constrexpr.CProdN (loc,l,a) ->
+ let loc = of_coqloc loc in
+ <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list
(mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
- | Constrexpr.CLambdaN (loc,l,a) -> <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
+ | Constrexpr.CLambdaN (loc,l,a) ->
+ let loc = of_coqloc loc in
+ <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
| Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Constrexpr.CAppExpl (loc,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
- | Constrexpr.CApp (loc,a,l) -> <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
+ | Constrexpr.CAppExpl (loc,a,l) ->
+ let loc = of_coqloc loc in
+ <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+ | Constrexpr.CApp (loc,a,l) ->
+ let loc = of_coqloc loc in
+ <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
| Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Constrexpr.CHole (loc, None) -> <:expr< Constrexpr.CHole $dloc$ None >>
+ | Constrexpr.CHole (loc, None) ->
+ let loc = of_coqloc loc in
+ <:expr< Constrexpr.CHole $dloc$ None >>
| Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
| Constrexpr.CNotation(_,ntn,(subst,substl,[])) ->
<:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$
($mlexpr_of_list mlexpr_of_constr subst$,
$mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
| Constrexpr.CPatVar (loc,n) ->
+ let loc = of_coqloc loc in
<:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
| _ -> failwith "mlexpr_of_constr: TODO"
@@ -211,6 +228,7 @@ let mlexpr_of_may_eval f = function
| Genredexpr.ConstrEval (r,c) ->
<:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
| Genredexpr.ConstrContext ((loc,id),c) ->
+ let loc = of_coqloc loc in
let id = mlexpr_of_ident id in
<:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >>
| Genredexpr.ConstrTypeOf c ->
@@ -427,6 +445,7 @@ let rec mlexpr_of_atomic_tactic = function
and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| Tacexpr.TacAtom (loc,t) ->
+ let loc = of_coqloc loc in
<:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >>
| Tacexpr.TacThen (t1,[||],t2,[||]) ->
<:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>>
@@ -489,11 +508,15 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| _ -> failwith "Quotation of tactic expressions: TODO"
and mlexpr_of_tactic_arg = function
- | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
+ | Tacexpr.MetaIdArg (loc,true,id) ->
+ let loc = of_coqloc loc in
+ anti loc id
| Tacexpr.MetaIdArg (loc,false,id) ->
- <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
+ let loc = of_coqloc loc in
+ <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
| Tacexpr.TacCall (loc,t,tl) ->
- <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
+ let loc = of_coqloc loc in
+ <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
| Tacexpr.Tacexp t ->
<:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >>
| Tacexpr.ConstrMayEval c ->
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 895584703a..eee84c38db 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -14,27 +14,27 @@ let mlexpr_of_list f l =
List.fold_right
(fun e1 e2 ->
let e1 = f e1 in
- let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+ let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< [$e1$ :: $e2$] >>)
- l (let loc = Loc.ghost in <:expr< [] >>)
+ l (let loc = CompatLoc.ghost in <:expr< [] >>)
let mlexpr_of_pair m1 m2 (a1,a2) =
let e1 = m1 a1 and e2 = m2 a2 in
- let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+ let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< ($e1$, $e2$) >>
let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
- let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
+ let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
<:expr< ($e1$, $e2$, $e3$) >>
let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)=
let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in
- let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in
+ let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in
<:expr< ($e1$, $e2$, $e3$, $e4$) >>
(* We don't give location for tactic quotation! *)
-let loc = Loc.ghost
+let loc = CompatLoc.ghost
let mlexpr_of_bool = function
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index f38479ac90..ce97ee78e2 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -29,9 +29,10 @@ let rec make_patt = function
let rec make_when loc = function
| [] -> <:expr< True >>
| GramNonTerminal(loc',t,_,Some p)::l ->
+ let loc' = of_coqloc loc' in
let p = Names.string_of_id p in
let l = make_when loc l in
- let loc = Loc.merge loc' loc in
+ let loc = CompatLoc.merge loc' loc in
let t = mlexpr_of_argtype loc' t in
<:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
| _::l -> make_when loc l
@@ -39,8 +40,9 @@ let rec make_when loc = function
let rec make_let e = function
| [] -> e
| GramNonTerminal(loc,t,_,Some p)::l ->
+ let loc = of_coqloc loc in
let p = Names.string_of_id p in
- let loc = Loc.merge loc (MLast.loc_of_expr e) in
+ let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
let e = make_let e l in
let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
<:expr< let $lid:p$ = $v$ in $e$ >>
@@ -70,6 +72,7 @@ let make_fun_clauses loc s l =
let rec make_args = function
| [] -> <:expr< [] >>
| GramNonTerminal(loc,t,_,Some p)::l ->
+ let loc = of_coqloc loc in
let p = Names.string_of_id p in
<:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
| _::l -> make_args l
@@ -77,8 +80,9 @@ let rec make_args = function
let rec make_eval_tactic e = function
| [] -> e
| GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag ->
+ let loc = of_coqloc loc in
let p = Names.string_of_id p in
- let loc = Loc.merge loc (MLast.loc_of_expr e) in
+ let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
let e = make_eval_tactic e l in
<:expr< let $lid:p$ = $lid:p$ in $e$ >>
| _::l -> make_eval_tactic e l
@@ -86,17 +90,20 @@ let rec make_eval_tactic e = function
let rec make_fun e = function
| [] -> e
| GramNonTerminal(loc,_,_,Some p)::l ->
+ let loc = of_coqloc loc in
let p = Names.string_of_id p in
<:expr< fun $lid:p$ -> $make_fun e l$ >>
| _::l -> make_fun e l
let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
| GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
- | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >>
+ | GramNonTerminal (loc,nt,_,sopt) ->
+ let loc = of_coqloc loc in <:expr< None >>
let make_prod_item = function
| GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
| GramNonTerminal (loc,nt,g,sopt) ->
+ let loc = of_coqloc loc in
<:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
$mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
@@ -106,8 +113,9 @@ let mlexpr_of_clause =
let rec make_tags loc = function
| [] -> <:expr< [] >>
| GramNonTerminal(loc',t,_,Some p)::l ->
+ let loc' = of_coqloc loc' in
let l = make_tags loc l in
- let loc = Loc.merge loc' loc in
+ let loc = CompatLoc.merge loc' loc in
let t = mlexpr_of_argtype loc' t in
<:expr< [ $t$ :: $l$ ] >>
| _::l -> make_tags loc l
@@ -221,12 +229,12 @@ EXTEND
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let t, g = interp_entry_name false None e "" in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let t, g = interp_entry_name false None e sep in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| s = STRING ->
- if s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal.");
+ if s = "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
GramTerminal s
] ]
;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index db8c51386a..3550e75e3b 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -20,8 +20,9 @@ open Compat
let rec make_let e = function
| [] -> e
| GramNonTerminal(loc,t,_,Some p)::l ->
+ let loc = of_coqloc loc in
let p = Names.string_of_id p in
- let loc = Loc.merge loc (MLast.loc_of_expr e) in
+ let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
let e = make_let e l in
<:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
| _::l -> make_let e l
@@ -83,7 +84,7 @@ EXTEND
rule:
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
->
- if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty.");
+ if s = "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
(Some s,l,<:expr< fun () -> $e$ >>)
| "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
(None,l,<:expr< fun () -> $e$ >>)
@@ -92,10 +93,10 @@ EXTEND
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let t, g = interp_entry_name false None e "" in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let t, g = interp_entry_name false None e sep in
- GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
+ GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| s = STRING ->
GramTerminal s
] ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-14 13:10:27 +0000