declarations eliminations / debuggae inductifs (debut)

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

9 files changed, 43 insertions, 28 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9dc0ca365..433a2c1d9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -128,7 +128,14 @@ let extract nparams c =
   with UserError _ -> raise (InductiveError BadEntry)
 
 let check_params nparams params c = 
-  if not (fst (extract nparams c) = params) then 
+  let eparams = fst (extract nparams c) in
+  try
+    List.iter2 
+      (fun (n1,t1) (n2,t2) ->
+	 if n1 <> n2 || strip_outer_cast t1 <> strip_outer_cast t2 then
+	   raise (InductiveError BadEntry))
+      eparams params
+  with Invalid_argument _ ->
     raise (InductiveError BadEntry)
 
 let mind_extract_and_check_params mie =
@@ -146,7 +153,6 @@ let mind_check_lc params mie =
   let check_lc (_,_,_,lc) =
     let (lna,c) = decomp_all_DLAMV_name lc in
     Array.iter (check_params nparams params) c;
-    if not (List.length lna = ntypes) then
-      raise (InductiveError BadEntry)
+    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
   in
   List.iter check_lc mie.mind_entry_inds
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 706646245..a12c6803a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -930,8 +930,8 @@ let type_fixpoint env sigma lna lar vdefj =
   assert (Array.length lar = lt);
   try
     conv_forall2_i
-      (fun i e def ar -> 
-	 try conv_leq e def (lift lt ar) 
+      (fun i env sigma def ar -> 
+	 try conv_leq env sigma def (lift lt ar) 
 	 with NotConvertible -> raise (IllBranch i))
       env sigma
       (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
diff --git a/lib/util.ml b/lib/util.ml
index b96eca3ae..8410367f9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -133,6 +133,8 @@ let list_fold_left_i f =
   in 
   it_list_f 
 
+let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
+
 let list_for_all_i p = 
   let rec for_all_p i = function
     | [] -> true 
diff --git a/lib/util.mli b/lib/util.mli
index b26d6a1d7..e0de343df 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -53,6 +53,7 @@ val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_index : 'a -> 'a list -> int
+val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
diff --git a/library/declare.ml b/library/declare.ml
index 31749152c..550843267 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Generic
@@ -171,7 +172,8 @@ let declare_mind mie =
     | (id,_,_,_)::_ -> id
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let _ = add_leaf id CCI (in_inductive mie) in ()
+  let sp = add_leaf id CCI (in_inductive mie) in
+  sp
 
 
 (* Test and access functions. *)
@@ -280,19 +282,20 @@ let mind_path = function
 
 (* Eliminations. *)
 
-let declare_eliminations sp =
-  let env = Global.env () in
-  let sigma = Evd.empty in
-  let mindid = basename sp in
-  let mind = global_reference (kind_of_path sp) mindid in
-  let redmind = minductype_spec env sigma mind in
-  let mindstr = string_of_id mindid in
+let declare_eliminations sp i =
+  let oper = MutInd (sp,i) in
+  let ids = ids_of_sign (Global.var_context()) in
+  let mind = DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) in
+  let mispec = Global.lookup_mind_specif mind in 
+  let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     declare_constant (id_of_string na)
       ({ const_entry_body = c; const_entry_type = None },
-       NeverDischarge,false)
+       NeverDischarge, false);
+    pPNL [< 'sTR na; 'sTR " is defined" >]
   in
-  let mispec = Global.lookup_mind_specif redmind in 
+  let env = Global.env () in
+  let sigma = Evd.empty in
   let elim_scheme = 
     strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in
   let npars = mis_nparams mispec in
diff --git a/library/declare.mli b/library/declare.mli
index 4fe7767fd..f5c2dff07 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -28,9 +28,9 @@ val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
 
-val declare_mind : mutual_inductive_entry -> unit
+val declare_mind : mutual_inductive_entry -> section_path
 
-val declare_eliminations : section_path -> unit
+val declare_eliminations : section_path -> int -> unit
 
 val make_strength : string list -> strength
 val make_strength_0 : unit -> strength
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 0e062f6c9..f12f5edec 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -121,7 +121,7 @@ let implicit_args_msg sp mipv =
           [< (implicit_args_id mip.mind_typename (list_of_implicits imps));
              prvecti 
 	       (fun j idc ->
-		  let imps = constructor_implicits ((sp,i),j) in
+		  let imps = constructor_implicits ((sp,i),succ j) in
                   (implicit_args_id idc (list_of_implicits imps)))
                mip.mind_consnames 
           >])
@@ -245,7 +245,7 @@ let print_leaf_entry with_values sep (spopt,lobj) =
 	  hOV 0 [< 'sTR"Fw constant " ; 
 		   'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
 
-    | (sp,"MUTUALINDUCTIVE") ->
+    | (sp,"INDUCTIVE") ->
 	let mib = Global.lookup_mind sp in
 	if kind_of_path sp = CCI then
 	  [< print_mutual sp mib; 'fNL >]
@@ -369,7 +369,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
                if (head_const typ.body) = const then
                  fn (print_basename sp) hyps typ.body;
                crible_rec rest
-	   | (sp,"MUTUALINDUCTIVE") -> 
+	   | (sp,"INDUCTIVE") -> 
                let mib = Global.lookup_mind sp in 
                (match const with 
 		  | (DOPN(MutInd(sp',tyi),_)) -> 
@@ -490,11 +490,11 @@ let print_local_context () =
                [< print_last_const rest;
                   'sTR(print_basename sp) ;'sTR" = ";
                   print_typed_recipe (val_0,typ) >]
-           | "MUTUALINDUCTIVE" -> 
+           | "INDUCTIVE" -> 
                let mib = Global.lookup_mind sp in 
                [< print_last_const rest;print_mutual sp mib; 'fNL >]
-           |  "VARIABLE" ->  [< >]
-           |  _          ->  print_last_const rest)
+           | "VARIABLE" ->  [< >]
+           | _          ->  print_last_const rest)
     | (sp,Lib.ClosedSection _)::rest -> print_last_const rest
     | _ -> [< >]
   in 
@@ -583,7 +583,7 @@ let print_extraction () =
 		  (match cont with 
 		     | Some(t,_) -> fprint_var (string_of_id name) t
                      | _         -> [< >]) >]
-	   | (sp,"MUTUALINDUCTIVE") ->
+	   | (sp,"INDUCTIVE") ->
 	       [< print_rec rest; 
 		  (try 
 		     [< print_extracted_mutual sp ; 'fNL >] 
@@ -626,7 +626,7 @@ let print_extracted_context () =
 		     [< 'sTR (s ^" ==> "); fprint_recipe d; 'fNL >]
 		   with Not_found -> 
 		     [< >]) >]
-	   | "MUTUALINDUCTIVE" -> 
+	   | "INDUCTIVE" -> 
 	       [< print_last_constants rest; 
 		  try print_extracted_mutual sp with Not_found -> [<>] >]
 	   | "VARIABLE" -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ce0d13e8..217acdb0a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -153,8 +153,11 @@ let build_mutual lparams lnamearconstrs finite =
       mind_entry_inds = mispecvec }
     in
     States.unfreeze fs;
-    declare_mind mie;
-    pPNL(minductive_message lrecnames)
+    let sp = declare_mind mie in
+    pPNL(minductive_message lrecnames);
+    for i = 0 to List.length mispecvec - 1 do
+      declare_eliminations sp i
+    done
   with e ->
     States.unfreeze fs; raise e
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ecbd1a91c..e35e9f6ba 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -20,7 +20,7 @@ let set_batch_mode () = batch_mode := true
 
 let remove_top_ml () = Mltop.remove ()
 
-let inputstate = ref "tactics.coq"
+let inputstate = ref "barestate.coq"
 let set_inputstate s = inputstate:= s
 let inputstate () =if !inputstate <> "" then intern_state !inputstate