Modification messages d'erreurs, possibilité de n'importe quel constr dans les instances de références

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

5 files changed, 71 insertions, 49 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index dcc0177a2d..ad4e07dc87 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -125,11 +125,25 @@ let dbize_ctxt ctxt =
       (function
 	 | Nvar (loc,s) ->
 	     (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *)
-	     VAR (ident_of_nvar loc s)
+	     RRef (loc, RVar (ident_of_nvar loc s))
 	 | _ -> anomaly "Bad ast for local ctxt of a global reference") ctxt
   in
   Array.of_list l
 
+let dbize_constr_ctxt =
+  Array.map
+    (function
+       | VAR id ->
+	   (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *)
+	   RRef (dummy_loc, RVar id)
+       | _ -> anomaly "Bad ast for local ctxt of a global reference")
+
+let dbize_rawconstr_ctxt =
+  Array.map
+    (function
+       | RRef (_, RVar id) -> VAR id
+       | _ -> anomaly "Bad ast for local ctxt of a global reference")
+
 let dbize_global loc = function
   | ("CONST", sp::ctxt) -> 
       RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
@@ -145,10 +159,11 @@ let dbize_global loc = function
 		      [< 'sTR "Bad ast for this global a reference">])
 
 let ref_from_constr = function
-  | DOPN (Const sp,ctxt) -> RConst (sp, ctxt)
-  | DOPN (Evar ev,ctxt) -> REVar (ev, ctxt) 
-  | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j), ctxt)
-  | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), ctxt)
+  | DOPN (Const sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt)
+  | DOPN (Evar ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) 
+  | DOPN (MutConstruct (spi,j),ctxt) -> 
+      RConstruct ((spi,j), dbize_constr_ctxt ctxt)
+  | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), dbize_constr_ctxt ctxt)
   | VAR id -> RVar id  (* utilisé pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
@@ -630,10 +645,10 @@ let ctxt_of_ids ids =
   Array.of_list (List.map (function id -> VAR id) ids)
 
 let rec pat_of_ref metas vars = function
-  | RConst (sp,ctxt) -> RConst (sp, ctxt)
-  | RInd (ip,ctxt) -> RInd (ip, ctxt)
-  | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt)
-  | REVar (n,ctxt) -> REVar (n, ctxt)
+  | RConst (sp,ctxt) -> RConst (sp, dbize_rawconstr_ctxt ctxt)
+  | RInd (ip,ctxt) -> RInd (ip, dbize_rawconstr_ctxt ctxt)
+  | RConstruct(cp,ctxt) ->RConstruct(cp, dbize_rawconstr_ctxt ctxt)
+  | REVar (n,ctxt) -> REVar (n, dbize_rawconstr_ctxt ctxt)
   | RAbst _ -> error "pattern_of_rawconstr: not implemented"
   | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index bad9c38667..5a4f8ae5bd 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -119,16 +119,17 @@ let fprtype a =
 (* For compatibility *)
 let fterm0 = fprterm_env
 
-let pr_constant cst = gentermpr (ast_of_constant cst)
-let pr_existential ev = gentermpr (ast_of_existential ev)
-let pr_inductive ind = gentermpr (ast_of_inductive ind)
-let pr_constructor cstr = gentermpr (ast_of_constructor cstr)
+let pr_constant env cst = gentermpr (ast_of_constant (unitize_env env) cst)
+let pr_existential env ev = gentermpr (ast_of_existential (unitize_env env) ev)
+let pr_inductive env ind = gentermpr (ast_of_inductive (unitize_env env) ind)
+let pr_constructor env cstr =
+  gentermpr (ast_of_constructor (unitize_env env) cstr)
 
 open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
-  | ConstNode sp -> pr_constant (sp,[||])
-  | IndNode sp -> pr_inductive (sp,[||])
-  | CstrNode sp -> pr_constructor (sp,[||])
+  | ConstNode sp -> pr_constant (Global.context()) (sp,[||])
+  | IndNode sp -> pr_inductive (Global.context()) (sp,[||])
+  | CstrNode sp -> pr_constructor (Global.context()) (sp,[||])
   | VarNode id -> print_id id
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index d6e785c8f4..75ac36c081 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -22,10 +22,10 @@ val prtype          : typed_type -> std_ppcmds
 val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
 val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
 
-val pr_constant     : constant -> std_ppcmds
-val pr_existential  : existential -> std_ppcmds
-val pr_constructor  : constructor -> std_ppcmds
-val pr_inductive    : inductive -> std_ppcmds
+val pr_constant     : 'a assumptions -> constant -> std_ppcmds
+val pr_existential  : 'a assumptions -> existential -> std_ppcmds
+val pr_constructor  : 'a assumptions -> constructor -> std_ppcmds
+val pr_inductive    : 'a assumptions -> inductive -> std_ppcmds
 val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
 val pr_pattern_env  : 'a assumptions -> constr_pattern -> std_ppcmds
diff --git a/parsing/termast.ml b/parsing/termast.ml
index f4b7071932..9adc75473f 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -86,48 +86,44 @@ let stringopt_of_name = function
   | Name id -> Some (string_of_id id)
   | Anonymous -> None
 
-let ast_of_constant_ref (sp,ids) =
+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::(List.map ast_of_ident ids))
+  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
   else a
 
-let ast_of_constant (ev,ids) = ast_of_constant_ref (ev,ids_of_ctxt ids)
-
-let ast_of_existential_ref (ev,ids) =
+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::(List.map ast_of_ident ids))
+    ope("INSTANCE",a::(array_map_to_list pr ids))
   else a
 
-let ast_of_existential (ev,ids) = ast_of_existential_ref (ev,ids_of_ctxt ids)
-
-let ast_of_constructor_ref (((sp,tyi),n) as cstr_sp,ids) =
+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::(List.map ast_of_ident ids))
+  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
   else a
 
-let ast_of_constructor (ev,ids) = ast_of_constructor_ref (ev,ids_of_ctxt ids)
-
-let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) =
+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::(List.map ast_of_ident ids))
+  if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids))
   else a
 
-let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt)
-
-let ast_of_ref = function
-  | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_ctxt ctxt)
+let ast_of_ref pr = function
+  | RConst (sp,ctxt) -> ast_of_constant_ref pr (sp,ctxt)
   | RAbst (sp) ->
       ope("ABST", (path_section dummy_loc sp)
 	    ::(List.map ast_of_ident (* on triche *) []))
-  | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt)
-  | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt 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 (ev,ids_of_ctxt ctxt)
+  | REVar (ev,ctxt) -> ast_of_existential_ref pr (ev,ctxt)
+
+
 
 (**********************************************************************)
 (* 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 "_"
@@ -135,10 +131,12 @@ let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
       let args = List.map ast_of_cases_pattern args in
       ope("PATTAS",
 	  [nvar (string_of_id id);
-	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstr)::args)])
+	   ope("PATTCONSTRUCT",
+	       (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)])
   | PatCstr(loc,cstr,args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor_ref cstr)::List.map ast_of_cases_pattern args)
+	  (ast_of_constructor_ref ast_of_ident (adapt cstr))::
+	  List.map ast_of_cases_pattern args)
 	
 let ast_dependent na aty =
   match na with
@@ -205,7 +203,7 @@ let ast_of_app impl f args =
 *)
 
 let rec ast_of_raw = function
-  | RRef (_,ref) -> ast_of_ref ref
+  | RRef (_,ref) -> ast_of_ref ast_of_raw ref
   | RMeta (_,n) -> ope("META",[num n])
   | RApp (_,f,args) ->
       let (f,args) =
@@ -737,8 +735,16 @@ let ast_of_constr at_top env t =
   with Detyping.StillDLAM ->
     old_bdize at_top env t'
 
+let ast_of_constant env    = ast_of_constant_ref (ast_of_constr false env)
+
+let ast_of_existential env = ast_of_existential_ref (ast_of_constr false env)
+
+let ast_of_inductive env   = ast_of_inductive_ref (ast_of_constr false env)
+
+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 ref
+  | PRef ref -> ast_of_ref (ast_of_constr false env) ref
   | PRel n ->
       (try match fst (lookup_rel n env) with
 	 | Name id   -> ast_of_ident id
diff --git a/parsing/termast.mli b/parsing/termast.mli
index e0b8069d93..7961ee7fbd 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -25,10 +25,10 @@ val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
 i*)
 
-val ast_of_constant     : constant -> Coqast.t
-val ast_of_existential  : existential -> Coqast.t
-val ast_of_constructor  : constructor -> Coqast.t
-val ast_of_inductive    : inductive -> Coqast.t
+val ast_of_constant     : unit assumptions -> constant -> Coqast.t
+val ast_of_existential  : unit assumptions -> existential -> Coqast.t
+val ast_of_constructor  : unit assumptions -> constructor -> Coqast.t
+val ast_of_inductive    : unit assumptions -> inductive -> Coqast.t
 
 (* For debugging *)
 val print_implicits : bool ref