Utilisation de global_reference dans rawconstr

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

7 files changed, 37 insertions, 23 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 4591be556d..f7c1a88d1c 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -107,13 +107,14 @@ let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
   if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
   else a
 
-let ast_of_ref pr = function
-  | RConst (sp,ctxt) -> ast_of_constant_ref pr (sp,ctxt)
-  | RInd (ind,ctxt) -> ast_of_inductive_ref pr (ind,ctxt)
-  | RConstruct (cstr,ctxt) -> ast_of_constructor_ref pr (cstr,ctxt)
-  | RVar id -> ast_of_ident id
-  | REVar (ev,ctxt) -> ast_of_existential_ref pr (ev,ctxt)
-
+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)
+  | VarRef sp -> ast_of_ident (basename sp)
+  | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt)
 
 
 (**********************************************************************)
@@ -156,12 +157,14 @@ let explicitize =
     | [] -> List.rev lastimplargs
   in exprec 1 []
 
+(*
 let implicit_of_ref = function
-  | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
-  | RInd (indid,_) -> inductive_implicits_list indid
-  | RConst (sp,_) -> constant_implicits_list sp
-  | RVar id -> (try (implicits_of_var id) with _ -> []) (* et FW? *)
+  | ConstructRef sp -> constructor_implicits_list sp
+  | IndRef sp -> inductive_implicits_list sp
+  | ConstRef sp -> constant_implicits_list sp
+  | VarRef sp -> (try implicits_of_var sp with _ -> [])
   | _ -> []
+*)
 
 let rec skip_coercion dest_ref (f,args as app) =
   if !print_coercions then app
@@ -201,6 +204,7 @@ let ast_of_app impl f args =
 
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ast_of_raw ref
+  | RVar (_,id) -> ast_of_ident id
   | RMeta (_,n) -> ope("META",[num n])
   | RApp (_,f,args) ->
       let (f,args) =
@@ -208,7 +212,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 (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
 	 | _           -> ast_of_app [] astf astargs)
   | RBinder (_,BProd,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
@@ -329,6 +333,8 @@ let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env)
 let rec ast_of_pattern env = function
   | PRef ref -> ast_of_ref (fun c -> ast_of_raw (Detyping.detype [] env c)) ref
 
+  | PVar id -> ast_of_ident id
+
   | PRel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> ast_of_ident id
@@ -345,7 +351,7 @@ let rec ast_of_pattern env = function
       let astf = ast_of_pattern env f in
       let astargs = List.map (ast_of_pattern env) args in
       (match f with 
-	 | PRef ref -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | PRef ref -> ast_of_app (implicits_of_global ref) astf astargs
 	 | _        -> ast_of_app [] astf astargs)
 
   | PSoApp (n,args) ->
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 4e62177a97..1674ed9fe1 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -30,6 +30,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
 
 (* For debugging *)
 val print_implicits : bool ref
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 84041fb329..d68d8ec742 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -330,7 +330,7 @@ let check_number_of_regular_eqns eqns =
 (* Functions to deal with matrix factorization *)
 let occur_rawconstr id =
   let rec occur = function
-    | RRef (loc,RVar id) -> true
+    | RVar (loc,id') -> id = id'
     | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
     | RBinder (loc,bk,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RCases (loc,prinfo,tyopt,tml,pl) ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 306f2b8ce2..a452cf645e 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -137,11 +137,11 @@ let coercion_exists coe =
   with Not_found -> false
 
 let coe_of_reference = function
-  | RConst (sp,l) -> NAM_Constant sp
-  | RInd (ind_sp,l) -> NAM_Inductive ind_sp
-  | RConstruct (cstr_sp,l) -> NAM_Constructor cstr_sp
-  | RVar id  -> NAM_Var id
-  | _ -> raise Not_found
+  | ConstRef sp -> NAM_Constant sp
+  | IndRef sp -> NAM_Inductive sp
+  | ConstructRef sp -> NAM_Constructor sp
+  | VarRef sp  -> NAM_Var (basename sp)
+  | EvarRef _ -> raise Not_found
 
 let coercion_params r =
   let _,coe_info = coercion_info (coe_of_reference r) in
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index ab9410cc64..342161cb44 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -52,8 +52,10 @@ val class_info_from_index : int -> cl_typ * cl_info_typ
 val coercion_exists : coe_typ -> bool
 val coercion_info : coe_typ -> (int * coe_info_typ)
 val coercion_info_from_index : int -> coe_typ * coe_info_typ
-val coercion_params : 
-  'a array reference -> int (* raise [Not_found] if not a coercion *)
+
+(* [coercion_params] raises [Not_found] if not a coercion *)
+val coercion_params : global_reference -> int
+
 val constructor_at_head : constr -> cl_typ * int
 
 (* raises [Not_found] if not convertible to a class *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f1a28f63b7..7e933a2131 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,7 +32,8 @@ type 'ctxt reference =
 
 (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
-  | RRef of loc * rawconstr array reference
+  | RRef of loc * global_reference
+  | RVar of loc * identifier
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
@@ -62,6 +63,7 @@ let dummy_loc = (0,0)
 
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
+  | RVar (loc,_) -> loc
   | RMeta (loc,_) -> loc
   | RApp (loc,_,_) -> loc
   | RBinder (loc,_,_,_,_) -> loc
@@ -76,3 +78,5 @@ let loc_of_rawconstr = function
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 
 
+
+
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 58ebbf353d..b0f6615b96 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -30,7 +30,8 @@ type 'ctxt reference =
   | REVar of int * 'ctxt
 
 type rawconstr = 
-  | RRef of loc * rawconstr array reference
+  | RRef of loc * global_reference
+  | RVar of loc * identifier
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr