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

7 files changed, 67 insertions, 35 deletions

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