Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 49 insertions, 48 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 6f2385392..d96107755 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -179,15 +179,14 @@ let ast_to_global loc c =
     | ("CONST", [sp]) ->
 	let ref = ConstRef (ast_to_sp sp) in
 	RRef (loc, ref), implicits_of_global ref
-    | ("EVAR", [(Num (_,ev))]) ->
-	let ref = EvarRef ev in
-	RRef (loc, ref), implicits_of_global ref
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
 	RRef (loc, ref), implicits_of_global ref
     | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) ->
 	let ref = ConstructRef ((ast_to_sp sp,ti),n) in
 	RRef (loc, ref), implicits_of_global ref
+    | ("EVAR", [(Num (_,ev))]) ->
+	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
 	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index ca5033a20..41f6f1818 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -15,9 +15,9 @@ open Termast
 
 exception Non_closed_number
 
-let ast_O = ast_of_ref ast_of_rawconstr glob_O
-let ast_S = ast_of_ref ast_of_rawconstr glob_S
-let ast_myvar = ast_of_ref ast_of_rawconstr glob_My_special_variable_nat
+let ast_O = ast_of_ref glob_O
+let ast_S = ast_of_ref glob_S
+let ast_myvar = ast_of_ref glob_My_special_variable_nat
   
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 let nat_of_int n dloc =
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index eb6b20719..2577ef9be 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -329,7 +329,6 @@ let print_name qid =
       | IndRef (sp,_) -> print_inductive sp
       | ConstructRef ((sp,_),_) -> print_inductive sp
       | VarRef sp -> print_section_variable sp
-      | EvarRef n -> [< 'sTR "?"; 'iNT n; 'fNL >]
   with Not_found -> 
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3d72f4adc..0a7a73966 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -74,35 +74,23 @@ let stringopt_of_name = function
   | Name id -> Some (string_of_id id)
   | Anonymous -> None
 
-let ast_of_constant_ref pr (sp,ids) =
-  let a = ope("CONST", [path_section dummy_loc sp]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_constant_ref sp =
+  ope("CONST", [path_section dummy_loc sp])
 
-let ast_of_existential_ref pr  (ev,ids) =
-  let a = ope("EVAR", [num ev]) in
-  if !print_arguments or !print_evar_arguments then
-    ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_existential_ref ev =
+  ope("EVAR", [num ev])
 
-let ast_of_constructor_ref pr  (((sp,tyi),n) as cstr_sp,ids) =
-  let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_constructor_ref ((sp,tyi),n) =
+  ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n])
 
-let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
-  let a = ope("MUTIND",	[path_section dummy_loc sp; num tyi]) in
-  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
-  else a
+let ast_of_inductive_ref (sp,tyi) =
+  ope("MUTIND", [path_section dummy_loc sp; num tyi])
 
-let ast_of_ref pr r =
-  (* TODO gérer le ctxt *)
-  let ctxt = [||] in match r with
-  | ConstRef sp -> ast_of_constant_ref pr (sp,ctxt)
-  | IndRef sp -> ast_of_inductive_ref pr (sp,ctxt)
-  | ConstructRef sp -> ast_of_constructor_ref pr (sp,ctxt)
+let ast_of_ref = function
+  | ConstRef sp -> ast_of_constant_ref sp
+  | IndRef sp -> ast_of_inductive_ref sp
+  | ConstructRef sp -> ast_of_constructor_ref sp
   | VarRef sp -> ast_of_ident (basename sp)
-  | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
@@ -112,21 +100,18 @@ let ast_of_qualid p =
 (**********************************************************************)
 (* conversion of patterns                                             *)
 
-let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt)
-
 let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
   | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
-  | PatCstr(loc,cstr,args,Name id) ->
+  | PatCstr(loc,(cstrsp,_),args,Name id) ->
       let args = List.map ast_of_cases_pattern args in
       ope("PATTAS",
 	  [nvar (string_of_id id);
-	   ope("PATTCONSTRUCT",
-	       (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)])
-  | PatCstr(loc,cstr,args,Anonymous) ->
+	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)])
+  | PatCstr(loc,(cstrsp,_),args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor_ref ast_of_ident (adapt cstr))::
-	  List.map ast_of_cases_pattern args)
+	  (ast_of_constructor_ref cstrsp)
+	  :: List.map ast_of_cases_pattern args)
 	
 let ast_dependent na aty =
   match na with
@@ -188,8 +173,9 @@ let ast_of_app impl f args =
 *)
 
 let rec ast_of_raw = function
-  | RRef (_,ref) -> ast_of_ref ast_of_raw ref
+  | RRef (_,ref) -> ast_of_ref ref
   | RVar (_,id) -> ast_of_ident id
+  | REvar (_,n) -> ast_of_existential_ref n
   | RMeta (_,n) -> ope("META",[num n])
   | RApp (_,f,args) ->
       let (f,args) =
@@ -197,8 +183,7 @@ let rec ast_of_raw = function
       let astf = ast_of_raw f in
       let astargs = List.map ast_of_raw args in
       (match f with 
-	 | RRef (_,(EvarRef _ as ref)) ->
-	     ast_of_ref ast_of_raw ref (* we drop args *)
+	 | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
 	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
 
 	 | RVar (_,id) ->
@@ -317,19 +302,37 @@ let ast_of_constr at_top env t =
   ast_of_raw 
     (Detyping.detype avoid (names_of_rel_context env) t')
 
-let ast_of_constant env    = ast_of_constant_ref (ast_of_constr false env)
+let ast_of_constant env (sp,ids) =
+  let a = ast_of_constant_ref sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_existential env = ast_of_existential_ref (ast_of_constr false env)
+let ast_of_existential env (ev,ids) =
+  let a = ast_of_existential_ref ev in
+  if !print_arguments or !print_evar_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_inductive env   = ast_of_inductive_ref (ast_of_constr false env)
+let ast_of_constructor env (cstr_sp,ids) =
+  let a = ast_of_constructor_ref cstr_sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
-let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env)
+let ast_of_inductive env (ind_sp,ids) =
+  let a = ast_of_inductive_ref ind_sp in
+  if !print_arguments then
+    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
+  else a
 
 let rec ast_of_pattern env = function
-  | PRef ref -> ast_of_ref (fun c -> ast_of_raw (Detyping.detype [] env c)) ref
+  | PRef ref -> ast_of_ref ref
 
   | PVar id -> ast_of_ident id
 
+  | PEvar n -> ast_of_existential_ref n
+
   | PRel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> ast_of_ident id
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 4b689ead0..1d6ee2208 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -26,7 +26,7 @@ val ast_of_constant     : env -> constant -> Coqast.t
 val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t
 val ast_of_inductive    : env -> inductive -> Coqast.t
-val ast_of_ref          : ('a -> Coqast.t) -> global_reference -> Coqast.t
+val ast_of_ref          : global_reference -> Coqast.t
 val ast_of_qualid       : qualid -> Coqast.t
 
 (* For debugging *)