diff options
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) | _ -> |