diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:07 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:07 +0000 |
| commit | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (patch) | |
| tree | e1be15920daf8b2e5ae788f57e772e79ddaacd30 | |
| parent | 621625757d04bdb19075d92e764749d0a1393ce3 (diff) | |
Moved Compat to parsing. This permits to break the dependency of the
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.
This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
45 files changed, 518 insertions, 306 deletions
diff --git a/.gitignore b/.gitignore index 570342784..c3669497f 100644 --- a/.gitignore +++ b/.gitignore @@ -110,7 +110,7 @@ g_*.ml ide/project_file.ml lib/pp.ml -lib/compat.ml +parsing/compat.ml grammar/q_util.ml grammar/q_constr.ml grammar/q_coqast.ml diff --git a/Makefile.common b/Makefile.common index 654a71527..8fa2e5b76 100644 --- a/Makefile.common +++ b/Makefile.common @@ -81,7 +81,7 @@ SRCDIRS:=\ # Order is relevent here because kernel and checker contain files # with the same name -CHKSRCDIRS:= checker lib config kernel +CHKSRCDIRS:= checker lib config kernel parsing ########################################################################### # tools @@ -225,7 +225,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc COQENVCMO:=lib/clib.cma\ - lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/loc.cmo lib/errors.cmo + lib/loc.cmo lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo diff --git a/checker/check.mllib b/checker/check.mllib index c12b5953a..c93051fa1 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,9 +1,9 @@ Coq_config Pp_control -Compat Flags Pp Loc +Compat Segmenttree Unicodetable Unicode diff --git a/checker/checker.ml b/checker/checker.ml index a75aed533..976030ef5 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -274,7 +274,12 @@ let rec explain_exn = function (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) - | Loc.Exc_located (loc,exc) -> + | Loc.Exc_located (loc, exc) -> + hov 0 ((if loc = Loc.ghost then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ explain_exn exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) diff --git a/dev/printers.mllib b/dev/printers.mllib index 703aa9616..f06530442 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,10 +1,10 @@ Coq_config Pp_control +Loc Compat Flags Pp -Loc Segmenttree Unicodetable Unicode @@ -110,6 +110,7 @@ Declaremods Tok Lexer Ppextend +Pputils Genarg Constrexpr_ops Notation_ops diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index cc378ceda..a3c94c5d4 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 afb8ac4e6..7d91550df 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 8943b2b63..5d46897c6 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 3d39d13d7..cbbc9e187 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 895584703..eee84c38d 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 f38479ac9..ce97ee78e 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 db8c51386..3550e75e3 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 ] ] diff --git a/intf/extend.mli b/intf/extend.mli index ca40eb744..d66f29ba7 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -10,8 +10,17 @@ type side = Left | Right +type gram_assoc = NonA | RightA | LeftA + +type gram_position = + | First + | Last + | Before of string + | After of string + | Level of string + type production_position = - | BorderProd of side * Compat.gram_assoc option + | BorderProd of side * gram_assoc option | InternalProd type production_level = diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index dfa03a4d7..31c1643d2 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -185,7 +185,7 @@ type grammar_tactic_prod_item_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level | SetLevel of int - | SetAssoc of Compat.gram_assoc + | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version | SetFormat of string located diff --git a/lib/lib.mllib b/lib/lib.mllib index a7d56c666..f557bd7d7 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,6 +1,5 @@ Xml_lexer Xml_parser -Compat Loc Errors Bigint diff --git a/lib/loc.ml b/lib/loc.ml index 58a328823..57c928bbc 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -6,24 +6,62 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp +(* Locations management *) -include Compat.Loc -(* Locations management *) +type t = { + fname : string; (** filename *) + line_nb : int; (** start line number *) + bol_pos : int; (** position of the beginning of start line *) + line_nb_last : int; (** end line number *) + bol_pos_last : int; (** position of the beginning of end line *) + bp : int; (** start position *) + ep : int; (** end position *) +} + +exception Exc_located of t * exn + +let create fname line_nb bol_pos (bp, ep) = { + fname = fname; line_nb = line_nb; bol_pos = bol_pos; + line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } + +let make_loc (bp, ep) = { + fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + bp = bp; ep = ep; } + +let ghost = { + fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + bp = 0; ep = 0; } -let dummy_loc = Compat.Loc.ghost -let join_loc = Compat.Loc.merge -let make_loc = Compat.make_loc -let unloc = Compat.unloc +let merge loc1 loc2 = + if loc1.bp < loc2.bp then + if loc1.ep < loc2.ep then { + fname = loc1.fname; + line_nb = loc1.line_nb; + bol_pos = loc1.bol_pos; + line_nb_last = loc2.line_nb_last; + bol_pos_last = loc2.bol_pos_last; + bp = loc1.bp; ep = loc2.ep; } + else loc1 + else if loc2.ep < loc1.ep then { + fname = loc2.fname; + line_nb = loc2.line_nb; + bol_pos = loc2.bol_pos; + line_nb_last = loc1.line_nb_last; + bol_pos_last = loc1.bol_pos_last; + bp = loc2.bp; ep = loc1.ep; } + else loc2 + +let unloc loc = (loc.bp, loc.ep) + +let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep) + +let raise loc e = raise (Exc_located (loc, e)) + +let dummy_loc = ghost +let join_loc = merge type 'a located = t * 'a 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 - -let pr_located pr (loc, x) = - if Flags.do_beautify () && loc <> dummy_loc then - let (b, e) = unloc loc in - Pp.comment b ++ pr x ++ Pp.comment e - else pr x diff --git a/lib/loc.mli b/lib/loc.mli index c1cbdb64d..0b6ba544d 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -8,21 +8,37 @@ (** {5 Basic types} *) -type t = Compat.Loc.t +type t exception Exc_located of t * exn type 'a located = t * 'a +(** Embed a location in a type *) (** {5 Location manipulation} *) (** This is inherited from CAMPL4/5. *) +val create : string -> int -> int -> (int * int) -> t +(** Create a location from a filename, a line number, a position of the + beginning of the line and a pair of start and end position *) + val unloc : t -> int * int +(** Return the start and end position of a location *) + val make_loc : int * int -> t +(** Make a location out of its start and end position *) + val ghost : t +(** Dummy location *) + val merge : t -> t -> t + val raise : t -> exn -> 'a +(** Raise a located exception *) + +val represent : t -> (string * int * int * int * int) +(** Return the arguments given in [create] *) (** {5 Location utilities} *) @@ -32,9 +48,6 @@ val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit val down_located : ('a -> 'b) -> 'a located -> 'b (** Projects out a located object *) -val pr_located : ('a -> Pp.std_ppcmds) -> 'a located -> Pp.std_ppcmds -(** Prints an object surrounded by its commented location *) - (** {5 Backward compatibility} *) val dummy_loc : t diff --git a/lib/compat.ml4 b/parsing/compat.ml4 index 3c26285bf..9a7c75bcc 100644 --- a/lib/compat.ml4 +++ b/parsing/compat.ml4 @@ -12,26 +12,45 @@ IFDEF CAMLP5 THEN -module Loc = struct +module CompatLoc = struct include Ploc - exception Exc_located = Exc let ghost = dummy let merge = encl end -let make_loc = Loc.make_unlined -let unloc loc = (Loc.first_pos loc, Loc.last_pos loc) +exception Exc_located = Ploc.Exc + +let of_coqloc loc = + let (fname, lnb, pos, bp, ep) = Loc.represent loc in + Ploc.make_loc fname lnb pos (bp, ep) "" + +let to_coqloc loc = + Loc.create (Ploc.file_name loc) (Ploc.line_nb loc) + (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) + +let make_loc = Ploc.make_unlined ELSE -module Loc = Camlp4.PreCast.Loc +module CompatLoc = Camlp4.PreCast.Loc + +exception Exc_located = CompatLoc.Exc_located + +let of_coqloc loc = + let (fname, lnb, pos, bp, ep) = Loc.represent loc in + CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false) + +let to_coqloc loc = + Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc) + (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc) -let make_loc (start,stop) = - Loc.of_tuple ("", 0, 0, start, 0, 0, stop, false) -let unloc loc = (Loc.start_off loc, Loc.stop_off loc) +let make_loc (start, stop) = + CompatLoc.of_tuple ("", 0, 0, start, 0, 0, stop, false) END +let (!@) = to_coqloc + (** Misc module emulation *) IFDEF CAMLP5 THEN @@ -53,22 +72,58 @@ END (** Grammar auxiliary types *) IFDEF CAMLP5 THEN -type gram_assoc = Gramext.g_assoc = NonA | RightA | LeftA -type gram_position = Gramext.position = - | First - | Last - | Before of string - | After of string - | Like of string (** dont use it, not in camlp4 *) - | Level of string + +let to_coq_assoc = function +| Gramext.RightA -> Extend.RightA +| Gramext.LeftA -> Extend.LeftA +| Gramext.NonA -> Extend.NonA + +let of_coq_assoc = function +| Extend.RightA -> Gramext.RightA +| Extend.LeftA -> Gramext.LeftA +| Extend.NonA -> Gramext.NonA + +let of_coq_position = function +| Extend.First -> Gramext.First +| Extend.Last -> Gramext.Last +| Extend.Before s -> Gramext.Before s +| Extend.After s -> Gramext.After s +| Extend.Level s -> Gramext.Level s + +let to_coq_position = function +| Gramext.First -> Extend.First +| Gramext.Last -> Extend.Last +| Gramext.Before s -> Extend.Before s +| Gramext.After s -> Extend.After s +| Gramext.Level s -> Extend.Level s +| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *) + ELSE -type gram_assoc = PcamlSig.Grammar.assoc = NonA | RightA | LeftA -type gram_position = PcamlSig.Grammar.position = - | First - | Last - | Before of string - | After of string - | Level of string + +let to_coq_assoc = function +| PcamlSig.Grammar.RightA -> Extend.RightA +| PcamlSig.Grammar.LeftA -> Extend.LeftA +| PcamlSig.Grammar.NonA -> Extend.NonA + +let of_coq_assoc = function +| Extend.RightA -> PcamlSig.Grammar.RightA +| Extend.LeftA -> PcamlSig.Grammar.LeftA +| Extend.NonA -> PcamlSig.Grammar.NonA + +let of_coq_position = function +| Extend.First -> PcamlSig.Grammar.First +| Extend.Last -> PcamlSig.Grammar.Last +| Extend.Before s -> PcamlSig.Grammar.Before s +| Extend.After s -> PcamlSig.Grammar.After s +| Extend.Level s -> PcamlSig.Grammar.Level s + +let to_coq_position = function +| PcamlSig.Grammar.First -> Extend.First +| PcamlSig.Grammar.Last -> Extend.Last +| PcamlSig.Grammar.Before s -> Extend.Before s +| PcamlSig.Grammar.After s -> Extend.After s +| PcamlSig.Grammar.Level s -> Extend.Level s + END @@ -88,7 +143,7 @@ end ELSE module type LexerSig = - Camlp4.Sig.Lexer with module Loc = Loc and type Token.t = Tok.t + Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t END @@ -104,9 +159,9 @@ module type GrammarSig = sig type action = Gramext.g_action type production_rule = symbol list * action type single_extend_statment = - string option * gram_assoc option * production_rule list + string option * Gramext.g_assoc option * production_rule list type extend_statment = - gram_position option * single_extend_statment list + Gramext.position option * single_extend_statment list val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> parsable -> 'a @@ -123,9 +178,9 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct type action = Gramext.g_action type production_rule = symbol list * action type single_extend_statment = - string option * gram_assoc option * production_rule list + string option * Gramext.g_assoc option * production_rule list type extend_statment = - gram_position option * single_extend_statment list + Gramext.position option * single_extend_statment list let action = Gramext.action let entry_create = Entry.create let entry_parse = Entry.parse @@ -142,7 +197,7 @@ ELSE module type GrammarSig = sig include Camlp4.Sig.Grammar.Static - with module Loc = Loc and type Token.t = Tok.t + with module Loc = CompatLoc and type Token.t = Tok.t type 'a entry = 'a Entry.t type action = Action.t type parsable @@ -162,7 +217,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let parsable s = s let action = Action.mk let entry_create = Entry.mk - let entry_parse e s = parse e (*FIXME*)Loc.ghost s + let entry_parse e s = parse e (*FIXME*)CompatLoc.ghost s let entry_print ft x = Entry.print ft x let srules' = srules (entry_create "dummy") end diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ade579c69..8f1fda02b 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -184,10 +184,14 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = let symbs = make_constr_prod_item assoc n forpat pt in let pure_sublevels = pure_sublevels level symbs in let needed_levels = register_empty_levels forpat pure_sublevels in + let map_level (pos, ass1, name, ass2) = + (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in + let needed_levels = List.map map_level needed_levels in let pos,p4assoc,name,reinit = find_position forpat assoc level in let nb_decls = List.length needed_levels + 1 in List.iter (prepare_empty_levels forpat) needed_levels; - grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])]); + grammar_extend entry reinit (Option.map of_coq_position pos, + [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]); nb_decls) 0 rules let extend_constr_notation (n,assoc,ntn,rules) = @@ -211,7 +215,7 @@ let get_tactic_entry n = else if n = 5 then weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then - weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n)) + weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -234,7 +238,8 @@ let add_tactic_entry (key,lev,prods,tac) = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule (mkact key tac) prods in synchronize_level_positions (); - grammar_extend entry None (pos,[(None, None, List.rev [rules])]); + grammar_extend entry None (Option.map of_coq_position pos, + [(None, None, List.rev [rules])]); 1 (**********************************************************************) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 918a36084..0bd8d1990 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -33,7 +33,7 @@ type grammar_constr_prod_item = concat with last parsed list if true *) type notation_grammar = - int * gram_assoc option * notation * grammar_constr_prod_item list list + int * Extend.gram_assoc option * notation * grammar_constr_prod_item list list (** Adding notations *) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index c74f36907..735a31f21 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -19,7 +19,7 @@ let make_generic_action (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil = let rec make env = function | [] -> - Gram.action (fun loc -> f loc env) + Gram.action (fun loc -> f (to_coqloc loc) env) | None :: tl -> (* parse a non-binding item *) Gram.action (fun _ -> make env tl) | Some (p, t) :: tl -> (* non-terminal *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 64a8c54ea..1f7a85c8e 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -138,7 +138,7 @@ GEXTEND Gram | id = METAIDENT -> id_of_string id ] ] ; Prim.name: - [ [ "_" -> (loc, Anonymous) ] ] + [ [ "_" -> (!@loc, Anonymous) ] ] ; global: [ [ r = Prim.reference -> r ] ] @@ -159,54 +159,54 @@ GEXTEND Gram ; constr: [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global -> CAppExpl(loc,(None,f),[]) ] ] + | "@"; f=global -> CAppExpl(!@loc,(None,f),[]) ] ] ; operconstr: [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - CCast(loc,c1, CastVM c2) + CCast(!@loc,c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> - CCast(loc,c1, CastVM c2) + CCast(!@loc,c1, CastVM c2) | c1 = operconstr; ":";c2 = binder_constr -> - CCast(loc,c1, CastConv c2) + CCast(!@loc,c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv c2) + CCast(!@loc,c1, CastConv c2) | c1 = operconstr; ":>" -> - CCast(loc,c1, CastCoerce) ] + CCast(!@loc,c1, CastCoerce) ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) + [ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args) + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> let args = List.map (fun x -> CRef (Ident x), None) args in - CApp(loc,(None,CPatVar(locid,(true,id))),args) ] + CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAppExpl (loc,(None,Ident (loc,ldots_var)),[c]) ] + CAppExpl (!@loc,(None,Ident (!@loc,ldots_var)),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - CApp(loc,(Some (List.length args+1),CRef f),args@[c,None]) + CApp(!@loc,(Some (List.length args+1),CRef f),args@[c,None]) | c=operconstr; ".("; "@"; f=global; args=LIST0 (operconstr LEVEL "9"); ")" -> - CAppExpl(loc,(Some (List.length args+1),f),args@[c]) - | c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] + CAppExpl(!@loc,(Some (List.length args+1),f),args@[c]) + | c=operconstr; "%"; key=IDENT -> CDelimiters (!@loc,key,c) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c | "("; c = operconstr LEVEL "200"; ")" -> (match c with CPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CNotation(loc,"( _ )",([c],[],[])) + CNotation(!@loc,"( _ )",([c],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c | "`{"; c = operconstr LEVEL "200"; "}" -> - CGeneralization (loc, Implicit, None, c) + CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> - CGeneralization (loc, Explicit, None, c) + CGeneralization (!@loc, Explicit, None, c) ] ] ; forall: @@ -216,9 +216,9 @@ GEXTEND Gram [ [ "fun" -> () ] ] ; record_declaration: - [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (loc, None, fs) + [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) -(* CRecord (loc, Some c, fs) *) +(* CRecord (!@loc, Some c, fs) *) ] ] ; record_field_declaration: @@ -227,65 +227,65 @@ GEXTEND Gram ; binder_constr: [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> - mkCProdN loc bl c + mkCProdN (!@loc) bl c | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - mkCLambdaN loc bl c + mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> let loc1 = Loc.merge (local_binders_loc bl) (constr_loc c1) in - CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) + CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in let (li,id) = match fixp with CFix(_,id,_) -> id | CCoFix(_,id,_) -> id | _ -> assert false in - CLetIn(loc,(li,Name id),fixp,c) + CLetIn(!@loc,(li,Name id),fixp,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CLetTuple (loc,lb,po,c1,c2) + 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, [(!@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, [(!@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, [(!@loc, [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> - CIf (loc, c, po, b1, b2) + CIf (!@loc, c, po, b1, b2) | c=fix_constr -> c ] ] ; appl_arg: [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - (c,Some (loc,ExplByName id)) + (c,Some (!@loc,ExplByName id)) | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: [ [ g=global -> CRef g - | s=sort -> CSort (loc,s) - | n=INT -> CPrim (loc, Numeral (Bigint.of_string n)) - | s=string -> CPrim (loc, String s) - | "_" -> CHole (loc, None) - | id=pattern_ident -> CPatVar(loc,(false,id)) ] ] + | s=sort -> CSort (!@loc,s) + | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) + | s=string -> CPrim (!@loc, String s) + | "_" -> CHole (!@loc, None) + | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ] ; fix_constr: [ [ fx1=single_fix -> mk_single_fix fx1 | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; "for"; id=identref -> - mk_fix(loc,kw,id,dcl1::dcls) + mk_fix(!@loc,kw,id,dcl1::dcls) ] ] ; single_fix: - [ [ kw=fix_kw; dcl=fix_decl -> (loc,kw,dcl) ] ] + [ [ kw=fix_kw; dcl=fix_decl -> (!@loc,kw,dcl) ] ] ; fix_kw: [ [ "fix" -> true @@ -298,7 +298,7 @@ GEXTEND Gram ; match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ] + br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ] ; case_item: [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] @@ -322,11 +322,11 @@ 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,pl) ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; - "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] + "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ] ; recordpattern: [ [ id = global; ":="; pat = pattern -> (id, pat) ] ] @@ -334,42 +334,42 @@ GEXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] + [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ] | "99" RIGHTA [ ] | "10" LEFTA [ p = pattern; "as"; id = ident -> - CPatAlias (loc, p, id) ] + CPatAlias (!@loc, p, id) ] | "9" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with - | CPatAtom (_, Some r) -> CPatCstr (loc, r, [], lp) - | CPatCstr (_, r, l1, l2) -> CPatCstr (loc, r, l1 , l2@lp) - | CPatNotation (_, n, s, l) -> CPatNotation (loc, n , s, l@lp) + | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp) + | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) + | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) | _ -> Errors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST1 NEXT -> - CPatCstr (loc, r, lp, []) ] + CPatCstr (!@loc, r, lp, []) ] | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] + [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ] | "0" - [ r = Prim.reference -> CPatAtom (loc,Some r) - | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (loc, pat) - | "_" -> CPatAtom (loc,None) + [ r = Prim.reference -> CPatAtom (!@loc,Some r) + | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat) + | "_" -> CPatAtom (!@loc,None) | "("; p = pattern LEVEL "200"; ")" -> (match p with CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CPatNotation(loc,"( _ )",([p],[]),[]) + CPatNotation(!@loc,"( _ )",([p],[]),[]) | _ -> p) - | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n)) - | s = string -> CPatPrim (loc, String s) ] ] + | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n)) + | s = string -> CPatPrim (!@loc, String s) ] ] ; impl_ident_tail: - [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None)) + [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None)) | idl=LIST1 name; ":"; c=lconstr; "}" -> (fun id -> LocalRawAssum (id::idl,Default Implicit,c)) | idl=LIST1 name; "}" -> - (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))) + (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None))) | ":"; c=lconstr; "}" -> (fun id -> LocalRawAssum ([id],Default Implicit,c)) ] ] @@ -383,7 +383,7 @@ GEXTEND Gram ; binders_fixannot: [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot -> - (assum (loc, Name id) :: fst bl), snd bl + (assum (!@loc, Name id) :: fst bl), snd bl | f = fixannot -> [], f | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl | -> [], (None, CStructRec) @@ -399,8 +399,8 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(loc,Name ldots_var);id2], - Default Explicit,CHole (loc,None))] + [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2], + Default Explicit,CHole (!@loc,None))] | bl = closed_binder; bl' = binders -> bl@bl' ] ] @@ -409,7 +409,7 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))] + [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None))] | bl = closed_binder -> bl ] ] ; closed_binder: @@ -420,15 +420,15 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (Loc.merge (constr_loc t) loc,c, CastConv t))] + [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] + [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [LocalRawAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> [LocalRawAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) + List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> @@ -436,17 +436,17 @@ GEXTEND Gram ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c + [ [ "!" ; c = operconstr LEVEL "200" -> (!@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, iid), expl, c | c = operconstr LEVEL "200" -> - (loc, Anonymous), false, c + (!@loc, Anonymous), false, c ] ] ; type_cstr: - [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ] + [ [ c=OPT [":"; c=lconstr -> c] -> (!@loc,c) ] ] ; END;; diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 6506af0a1..7b4628938 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Constrexpr open Tacexpr open Misctypes @@ -84,20 +85,20 @@ GEXTEND Gram | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> - TacArg (loc,TacExternal (loc,com,req,la)) - | st = simple_tactic -> TacAtom (loc,st) - | a = may_eval_arg -> TacArg(loc,a) + TacArg (!@loc,TacExternal (!@loc,com,req,la)) + | st = simple_tactic -> TacAtom (!@loc,st) + | a = may_eval_arg -> TacArg(!@loc,a) | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(loc,MetaIdArg (loc,false,id)) + TacArg(!@loc,MetaIdArg (!@loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(loc,ConstrMayEval(ConstrTerm c)) + TacArg(!@loc,ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacArg(loc,IntroPattern ipat) + TacArg(!@loc,IntroPattern ipat) | r = reference; la = LIST0 tactic_arg -> - TacArg(loc,TacCall (loc,r,la)) ] + TacArg(!@loc,TacCall (!@loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a - | a = tactic_atom -> TacArg (loc,a) ] ] + | a = tactic_atom -> TacArg (!@loc,a) ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: @@ -118,7 +119,7 @@ GEXTEND Gram | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (loc,true,id) + | id = METAIDENT -> MetaIdArg (!@loc,true,id) | "()" -> TacVoid ] ] ; may_eval_arg: @@ -126,7 +127,7 @@ GEXTEND Gram | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ] ; fresh_id: - [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ] + [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -141,9 +142,9 @@ GEXTEND Gram | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (loc,true,id) + [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id) | n = integer -> Integer n - | r = reference -> TacCall (loc,r,[]) + | r = reference -> TacCall (!@loc,r,[]) | "()" -> TacVoid ] ] ; match_key: diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 55f4a77fb..e868bc77c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Names open Libnames open Tok @@ -44,13 +45,13 @@ GEXTEND Gram [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: - [ [ id = pattern_ident -> (loc, id) ] ] + [ [ id = pattern_ident -> (!@loc, id) ] ] ; var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> (loc,id) ] ] + [ [ id = ident -> (!@loc, id) ] ] ; identref: - [ [ id = ident -> (loc,id) ] ] + [ [ id = ident -> (!@loc, id) ] ] ; field: [ [ s = FIELD -> id_of_string s ] ] @@ -61,8 +62,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,id::List.rev (id'::l) + | id = ident -> !@loc,[id] ] ] ; basequalid: @@ -71,32 +72,32 @@ GEXTEND Gram ] ] ; name: - [ [ IDENT "_" -> (loc, Anonymous) - | id = ident -> (loc, Name id) ] ] + [ [ IDENT "_" -> (!@loc, Anonymous) + | id = ident -> (!@loc, Name id) ] ] ; reference: [ [ id = ident; (l,id') = fields -> - Qualid (loc, local_make_qualid (l@[id]) id') - | id = ident -> Ident (loc,id) + Qualid (!@loc, local_make_qualid (l@[id]) id') + | id = ident -> Ident (!@loc,id) ] ] ; by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ] + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (!@loc, s, sc) ] ] ; smart_global: [ [ c = reference -> Misctypes.AN c | ntn = by_notation -> Misctypes.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> loc, qid ] ] + [ [ qid = basequalid -> !@loc, qid ] ] ; ne_string: [ [ s = STRING -> - if s="" then Errors.user_err_loc(loc,"",Pp.str"Empty string."); s + if s="" then Errors.user_err_loc(!@loc, "", Pp.str"Empty string."); s ] ] ; ne_lstring: - [ [ s = ne_string -> (loc,s) ] ] + [ [ s = ne_string -> (!@loc, s) ] ] ; dirpath: [ [ id = ident; l = LIST0 field -> @@ -106,11 +107,11 @@ GEXTEND Gram [ [ s = STRING -> s ] ] ; integer: - [ [ i = INT -> my_int_of_string loc i - | "-"; i = INT -> - my_int_of_string loc i ] ] + [ [ i = INT -> my_int_of_string (!@loc) i + | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] ; natural: - [ [ i = INT -> my_int_of_string loc i ] ] + [ [ i = INT -> my_int_of_string (!@loc) i ] ] ; bigint: (* Negative numbers are dealt with specially *) [ [ i = INT -> (Bigint.of_string i) ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index d6592397a..eee6d3ce6 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Constrexpr open Vernacexpr open Locality @@ -113,6 +114,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f62be2f5c..b21711d32 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -218,7 +218,7 @@ GEXTEND Gram [ [ id = identref -> AI id (* This is used in quotations *) - | id = METAIDENT -> MetaId (loc,id) ] ] + | id = METAIDENT -> MetaId (!@loc, id) ] ] ; open_constr: [ [ c = constr -> ((),c) ] ] @@ -260,37 +260,37 @@ GEXTEND Gram [ [ l = LIST0 simple_intropattern -> l ]] ; disjunctive_intropattern: - [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc - | "()" -> loc,IntroOrAndPattern [[]] - | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]] + [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> !@loc,IntroOrAndPattern tc + | "()" -> !@loc,IntroOrAndPattern [[]] + | "("; si = simple_intropattern; ")" -> !@loc,IntroOrAndPattern [[si]] | "("; si = simple_intropattern; ","; tc = LIST1 simple_intropattern SEP "," ; ")" -> - loc,IntroOrAndPattern [si::tc] + !@loc,IntroOrAndPattern [si::tc] | "("; si = simple_intropattern; "&"; tc = LIST1 simple_intropattern SEP "&" ; ")" -> (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]] - in loc,pairify (si::tc) ] ] + in !@loc,pairify (si::tc) ] ] ; naming_intropattern: - [ [ prefix = pattern_ident -> loc, IntroFresh prefix - | "?" -> loc, IntroAnonymous - | id = ident -> loc, IntroIdentifier id - | "*" -> loc, IntroForthcoming true - | "**" -> loc, IntroForthcoming false ] ] + [ [ prefix = pattern_ident -> !@loc, IntroFresh prefix + | "?" -> !@loc, IntroAnonymous + | id = ident -> !@loc, IntroIdentifier id + | "*" -> !@loc, IntroForthcoming true + | "**" -> !@loc, IntroForthcoming false ] ] ; simple_intropattern: [ [ pat = disjunctive_intropattern -> pat | pat = naming_intropattern -> pat - | "_" -> loc, IntroWildcard - | "->" -> loc, IntroRewrite true - | "<-" -> loc, IntroRewrite false ] ] + | "_" -> !@loc, IntroWildcard + | "->" -> !@loc, IntroRewrite true + | "<-" -> !@loc, IntroRewrite false ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> @@ -402,13 +402,13 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit,CHole (loc, None)) + [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; fixdecl: [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; - ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] + ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ] ; fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> Some id @@ -416,7 +416,7 @@ GEXTEND Gram ; cofixdecl: [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" -> - (loc,id,bl,None,ty) ] ] + (!@loc, id, bl, None, ty) ] ] ; bindings_with_parameters: [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; @@ -459,7 +459,7 @@ GEXTEND Gram msg_warning (strbrk msg); Some id | IDENT "_eqn" -> let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in - msg_warning (strbrk msg); Some (loc, IntroAnonymous) + msg_warning (strbrk msg); Some (!@loc, IntroAnonymous) | -> None ] ] ; as_name: @@ -558,10 +558,10 @@ GEXTEND Gram (* Begin compatibility *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAssert (None,Some (loc,IntroIdentifier id),c) + TacAssert (None,Some (!@loc,IntroIdentifier id),c) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAssert (Some tac,Some (loc,IntroIdentifier id),c) + TacAssert (Some tac,Some (!@loc,IntroIdentifier id),c) (* End compatibility *) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> @@ -674,7 +674,7 @@ GEXTEND Gram | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl) (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl -> - let p,cl = merge_occurrences loc cl oc in + let p,cl = merge_occurrences (!@loc) cl oc in TacChange (p,c,cl) ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6d82a6504..0519bee8c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -94,8 +94,8 @@ GEXTEND Gram [ [ prfcom = default_command_entry -> prfcom ] ] ; locality: - [ [ IDENT "Local" -> locality_flag := Some (loc,true) - | IDENT "Global" -> locality_flag := Some (loc,false) + [ [ IDENT "Local" -> locality_flag := Some (!@loc,true) + | IDENT "Global" -> locality_flag := Some (!@loc,false) | -> locality_flag := None ] ] ; noedit_mode: @@ -127,7 +127,7 @@ GEXTEND Gram VernacSolve(g,tac,use_dft_tac)) ] ] ; located_vernac: - [ [ v = vernac -> loc, v ] ] + [ [ v = vernac -> !@loc, v ] ] ; END @@ -299,7 +299,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CHole (loc, None) ] ] + | -> CHole (!@loc, None) ] ] ; (* Inductive schemes *) scheme: @@ -336,19 +336,19 @@ GEXTEND Gram ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t)) + t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t)) | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> fun id -> - (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) + (oc,DefExpr (id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with | CCast(_,b, (CastConv t|CastVM t)) -> - (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) + (None,DefExpr(id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | _ -> - (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ] + (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id,CHole (loc, None))) + [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -365,9 +365,9 @@ GEXTEND Gram constructor_type: [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> - fun l id -> (coe <> None,(id,mkCProdN loc l c)) + fun l id -> (coe <> None,(id,mkCProdN (!@loc) l c)) | -> - fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] + fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None)))) ] -> t l ]] ; @@ -489,7 +489,7 @@ 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 -> CMapply (!@loc,me1,me2) ] ] ; module_expr_atom: @@ -505,9 +505,9 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me) + | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me) | mty = module_type; "with"; decl = with_declaration -> - CMwith (loc,mty,decl) + CMwith (!@loc,mty,decl) ] ] ; END @@ -589,17 +589,17 @@ 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, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) 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, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) 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, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items ] -> l ] SEP ","; @@ -677,7 +677,7 @@ GEXTEND Gram ; argument_spec: [ [ b = OPT "!"; id = name ; s = OPT scope -> - snd id, b <> None, Option.map (fun x -> loc, x) s + snd id, b <> None, Option.map (fun x -> !@loc, x) s ] ]; strategy_level: @@ -691,7 +691,7 @@ GEXTEND Gram [ [ name = identref; sup = OPT binders -> (let (loc,id) = name in (loc, Name id)), (Option.default [] sup) - | -> (loc, Anonymous), [] ] ] + | -> (!@loc, Anonymous), [] ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] @@ -1039,7 +1039,7 @@ GEXTEND Gram SetOnlyParsing Flags.Current | IDENT "compat"; s = STRING -> SetOnlyParsing (Coqinit.get_compat_version s) - | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s + | IDENT "format"; s = [s = STRING -> (!@loc,s)] -> SetFormat s | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) @@ -1057,6 +1057,6 @@ GEXTEND Gram [ [ s = ne_string -> TacTerm s | nt = IDENT; po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ] + ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] ; END diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 37d2b332d..29b3579f0 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Pp open Errors open Util @@ -44,14 +45,14 @@ GEXTEND Gram xml: [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml; "<"; "/"; ctag = IDENT; ">" -> - check_tags loc otag ctag; - XmlTag (loc,ctag,attrs,l) + check_tags (!@loc) otag ctag; + XmlTag (!@loc,ctag,attrs,l) | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" -> - XmlTag (loc,tag,attrs,[]) + XmlTag (!@loc,tag,attrs,[]) ] ] ; attr: - [ [ name = IDENT; "="; data = STRING -> (name, (loc, data)) ] ] + [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ] ; END diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index dc120bd6d..ca5c20c71 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -100,7 +100,7 @@ module Error = struct end open Error -let err loc str = Loc.raise (make_loc loc) (Error.E str) +let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) @@ -172,7 +172,7 @@ let lookup_utf8 cs = | None -> EmptyStream let unlocated f x = - try f x with Loc.Exc_located (_,exc) -> raise exc + try f x with Loc.Exc_located (_, exc) -> raise exc let check_keyword str = let rec loop_symb = parser @@ -538,7 +538,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc let current_location_table = ref (loct_create ()) -type location_table = (int, Loc.t) Hashtbl.t +type location_table = (int, CompatLoc.t) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t let location_function n = loct_func !current_location_table n @@ -596,10 +596,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *) module M_ = Camlp4.ErrorHandler.Register (Error) -module Loc = Loc +module Loc = CompatLoc module Token = struct include Tok (* Cf. tok.ml *) - module Loc = Loc + module Loc = CompatLoc module Error = Camlp4.Struct.EmptyError module Filter = struct type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t diff --git a/parsing/lexer.mli b/parsing/lexer.mli index e5b8ebb11..0e53bd615 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -12,7 +12,7 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool -val location_function : int -> Loc.t +(* val location_function : int -> Loc.t *) (** for coqdoc *) type location_table diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 98ba1f762..2f0851164 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,4 +1,5 @@ Tok +Compat Lexer Extrawit Pcoq diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 04b5e4673..b14822b8a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -28,6 +28,7 @@ let warning_verbose = ref true IFDEF CAMLP5 THEN open Gramext ELSE +open PcamlSig.Grammar open G END @@ -210,7 +211,7 @@ let rec remove_grammars n = (match !camlp4_state with | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove" | ByGrammar(g,reinit,ext)::t -> - grammar_delete g reinit ext; + grammar_delete g (Option.map of_coq_assoc reinit) ext; camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -422,7 +423,7 @@ module Vernac_ = GEXTEND Gram main_entry: - [ [ a = vernac -> Some (loc,a) | EOI -> None ] ] + [ [ a = vernac -> Some (!@loc, a) | EOI -> None ] ] ; END @@ -446,23 +447,23 @@ let main_entry = Vernac_.main_entry let constr_level = string_of_int let default_levels = - [200,RightA,false; - 100,RightA,false; - 99,RightA,true; - 10,RightA,false; - 9,RightA,false; - 8,RightA,true; - 1,LeftA,false; - 0,RightA,false] + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.RightA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] let default_pattern_levels = - [200,RightA,true; - 100,RightA,false; - 99,RightA,true; - 10,LeftA,false; - 9,RightA,false; - 1,LeftA,false; - 0,RightA,false] + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.LeftA,false; + 9,Extend.RightA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] let level_stack = ref [(default_levels, default_pattern_levels)] @@ -472,19 +473,19 @@ let level_stack = (* first LeftA, then RightA and NoneA together *) let admissible_assoc = function - | LeftA, Some (RightA | NonA) -> false - | RightA, Some LeftA -> false + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false + | Extend.RightA, Some Extend.LeftA -> false | _ -> true let create_assoc = function - | None -> RightA + | None -> Extend.RightA | Some a -> a let error_level_assoc p current expected = let pr_assoc = function - | LeftA -> str "left" - | RightA -> str "right" - | NonA -> str "non" in + | Extend.LeftA -> str "left" + | Extend.RightA -> str "right" + | Extend.NonA -> str "non" in errorlabstrm "" (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ @@ -518,18 +519,18 @@ let find_position_gen forpat ensure assoc lev = let assoc = create_assoc assoc in if !init = None then (* Create the entry *) - (if !after = None then Some First - else Some (After (constr_level (Option.get !after)))), + (if !after = None then Some Extend.First + else Some (Extend.After (constr_level (Option.get !after)))), Some assoc, Some (constr_level n), None else (* The reinit flag has been updated *) - Some (Level (constr_level n)), None, None, !init + Some (Extend.Level (constr_level n)), None, None, !init with (* Nothing has changed *) Exit -> level_stack := current :: !level_stack; (* Just inherit the existing associativity and name (None) *) - Some (Level (constr_level n)), None, None, None + Some (Extend.Level (constr_level n)), None, None, None let remove_levels n = level_stack := List.skipn n !level_stack @@ -561,8 +562,8 @@ let synchronize_level_positions () = (* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) let camlp4_assoc = function - | Some NonA | Some RightA -> RightA - | None | Some LeftA -> LeftA + | Some Extend.NonA | Some Extend.RightA -> Extend.RightA + | None | Some Extend.LeftA -> Extend.LeftA (* [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of @@ -577,20 +578,20 @@ let adjust_level assoc from = function | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) (* Compute production name on the right side *) (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> + | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) -> Some None (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some RightA)) -> + | (NumLevel n,BorderProd (Right,Some Extend.RightA)) -> Some (Some (n,true)) (* Compute production name on the left side *) (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some NonA)) -> None + | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None (* If the expected assoc is the current one, set to SELF *) | (NumLevel n,BorderProd (Left,Some a)) when a = camlp4_assoc assoc -> None (* Otherwise, force the level, n or n-1, according to expected assoc *) | (NumLevel n,BorderProd (Left,Some a)) -> - if a = LeftA then Some (Some (n,true)) else Some None + if a = Extend.LeftA then Some (Some (n,true)) else Some None (* None means NEXT *) | (NextLevel,_) -> Some None (* Compute production name elsewhere *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 682474c51..e9b504e05 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -290,15 +290,15 @@ val interp_entry_name : bool (** true to fail on unknown entry *) -> val find_position : bool (** true if for creation in pattern entry; false if in constr entry *) -> - gram_assoc option -> int option -> - gram_position option * gram_assoc option * string option * - (** for reinitialization: *) gram_assoc option + Extend.gram_assoc option -> int option -> + Extend.gram_position option * Extend.gram_assoc option * string option * + (** for reinitialization: *) Extend.gram_assoc option val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> - (gram_position option * gram_assoc option * - string option * gram_assoc option) list + (Extend.gram_position option * Extend.gram_assoc option * + string option * Extend.gram_assoc option) list val remove_levels : int -> unit diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index e8e81c472..a3052320c 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -10,6 +10,7 @@ (* arnaud: veiller à l'aspect tutorial des commentaires *) +open Compat open Pp open Tok open Decl_expr @@ -189,7 +190,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Constrexpr.CRef (Libnames.Ident (loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -202,7 +203,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Constrexpr.CRef (Libnames.Ident (loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 303932484..160ca1b4c 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -104,7 +104,7 @@ open Genarg open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global)) +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 77c6dc493..0dceecf4f 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) +open Compat open Util open Term open Names @@ -145,7 +146,7 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> loc, g ]] + [ [ g = Vernac.rec_definition -> !@loc, g ]] ; END diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1d03716d0..25ea991e7 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -13,6 +13,7 @@ open Pp open Names open Nameops open Libnames +open Pputils open Ppextend open Constrexpr open Constrexpr_ops @@ -102,7 +103,7 @@ let pr_com_at n = if Flags.do_beautify() && n <> 0 then comment n else mt() -let pr_with_comments loc pp = Loc.pr_located (fun x -> x) (loc,pp) +let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) @@ -137,12 +138,12 @@ let pr_opt_type_spc pr = function let pr_lident (loc,id) = if loc <> Loc.ghost then let (b,_) = Loc.unloc loc in - Loc.pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) + pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) else pr_id id let pr_lname = function (loc,Name id) -> pr_lident (loc,id) - | lna -> Loc.pr_located pr_name lna + | lna -> pr_located pr_name lna let pr_or_var pr = function | ArgArg x -> pr x diff --git a/printing/pputils.ml b/printing/pputils.ml new file mode 100644 index 000000000..0c54c6181 --- /dev/null +++ b/printing/pputils.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +let pr_located pr (loc, x) = + if Flags.do_beautify () && loc <> Loc.ghost then + let (b, e) = Loc.unloc loc in + Pp.comment b ++ pr x ++ Pp.comment e + else pr x diff --git a/printing/pputils.mli b/printing/pputils.mli new file mode 100644 index 000000000..bac2815fa --- /dev/null +++ b/printing/pputils.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds +(** Prints an object surrounded by its commented location *) + diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 748e5297b..3553373fb 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,13 +9,12 @@ open Pp open Names -let pr_located = Loc.pr_located - -open Compat +(* open Compat *) open Errors open Util open Extend open Vernacexpr +open Pputils open Ppconstr open Pptactic open Libnames @@ -28,8 +27,8 @@ let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (loc,id) = if loc <> Loc.ghost then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) + let (b,_) = Loc.unloc loc in + pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) else pr_id id let string_of_fqid fqid = @@ -39,8 +38,8 @@ let pr_fqid fqid = str (string_of_fqid fqid) let pr_lfqid (loc,fqid) = if loc <> Loc.ghost then - let (b,_) = unloc loc in - pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) + let (b,_) = Loc.unloc loc in + pr_located pr_fqid (Loc.make_loc (b,b+String.length(string_of_fqid fqid)),fqid) else pr_fqid fqid @@ -319,7 +318,7 @@ let pr_onescheme (idop,schem) = let begin_of_inductive = function [] -> 0 - | (_,((loc,_),_))::_ -> fst (unloc loc) + | (_,((loc,_),_))::_ -> fst (Loc.unloc loc) let pr_class_rawexpr = function | FunClass -> str"Funclass" diff --git a/printing/printing.mllib b/printing/printing.mllib index 2de798aa4..6d6e1bba6 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,3 +1,4 @@ +Pputils Ppconstr Printer Pptactic diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index d1e379cca..c6e694902 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -44,6 +44,11 @@ let explain_exn_default = function hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ Errors.print_no_anomaly exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in + hov 0 ((if loc = Loc.ghost then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ Errors.print_no_anomaly exc) | EvaluatedError (msg,None) -> msg | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise (* Otherwise, not handled here *) @@ -110,6 +115,9 @@ let rec process_vernac_interp_error = function Some (process_vernac_interp_error exc)) | Loc.Exc_located (loc,exc) -> Loc.Exc_located (loc,process_vernac_interp_error exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in + Loc.Exc_located (loc, process_vernac_interp_error exc) | exc -> exc diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 8bfcfea6a..bd426b6fd 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -292,8 +292,13 @@ let eval_call c = | Errors.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner - | Loc.Exc_located (loc, inner) when loc = Loc.ghost -> None, pr_exn inner - | Loc.Exc_located (loc, inner) -> Some (Loc.unloc loc), pr_exn inner + | Loc.Exc_located (loc, inner) -> + let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in + loc, pr_exn inner + | Compat.Exc_located (loc, inner) -> + let loc = Compat.to_coqloc loc in + let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in + loc, pr_exn inner | e -> None, pr_exn e in let interruptible f x = diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a665dc373..d406bf8d9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -24,7 +24,6 @@ open Vernacexpr open Pcoq open Libnames open Tok -open Lexer open Egramml open Egramcoq open Notation @@ -33,7 +32,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = add_keyword s +let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with @@ -159,7 +158,7 @@ let pr_grammar = function (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format (loc,str) = +let parse_format ((loc, str) : lstring) = let str = " "^str in let l = String.length str in let push_token a = function @@ -334,7 +333,7 @@ let rec interp_list_parser hd = function (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = is_ident x in + let norm = Lexer.is_ident x in if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'" else x @@ -342,7 +341,7 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when is_ident x -> + | String x :: sl when Lexer.is_ident x -> NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl @@ -643,12 +642,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in distribute [GramConstrNonTerminal (typ, Some m)] ll | Terminal s -> - distribute [GramConstrTerminal (terminal s)] ll + distribute [GramConstrTerminal (Lexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [terminal s] + (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in match List.assoc x etyps with diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 74ed231d1..7e301ba0e 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -291,6 +291,12 @@ let print_toplevel_error exc = (print_highlight_location top_buffer loc, ie) else ((mt ()) (* print_command_location top_buffer dloc *), ie) + | Compat.Exc_located (loc, ie) -> + let loc = Compat.to_coqloc loc in + if valid_buffer_loc top_buffer dloc loc then + (print_highlight_location top_buffer loc, ie) + else + ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) | _ -> |