modules Indrec, Tacentries, Hiddentac

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

11 files changed, 115 insertions, 18 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index db5458211d..96fe8d5846 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -110,7 +110,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     let (lpar,auxlargs) = array_chop auxnpar largs in 
     if not (array_for_all (noccur_bet n ntypes) auxlargs) then
       raise (InductiveError (NonPos n));
-    let auxlc = mis_lc env mispeci 
+    let auxlc = mis_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
     if auxntyp <> 1 then raise (InductiveError (NonPos n));
     let lrecargs = array_map_to_list (check_param_pos n) lpar in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d9a11fe478..ceb8fa0deb 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -56,6 +56,7 @@ val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
+val is_recursive : int list -> recarg list array -> bool
 val mis_is_recursive : mind_specif -> bool
 
 val mind_nth_type_packet : 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 0cdc50c562..07c5525263 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -60,10 +60,28 @@ let const_abst_opt_value env c =
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
 
-let mis_lc env mis =
+let mis_lc mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
     (Array.to_list mis.mis_args)
 
+let mis_lc_without_abstractions mis = 
+  let rec strip_DLAM = function
+    | (DLAM (n,c1)) -> strip_DLAM c1 
+    | (DLAMV (n,v)) -> v
+    | _ -> assert false
+  in 
+  strip_DLAM (mis_lc mis)
+
+let mis_type_mconstructs mispec =
+  let specif = mis_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) 
+  and make_Ck k = DOPN(MutConstruct((mispec.mis_sp,mispec.mis_tyi),k+1),
+		       mispec.mis_args) in
+  (Array.init nconstr make_Ck, 
+   sAPPVList specif (list_tabulate make_Ik ntypes))
+
 (* Existentials. *)
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
@@ -83,3 +101,14 @@ let existential_value sigma c =
 	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
     | Evar_empty ->
 	anomaly "a defined existential with no body"
+
+let mis_arity' mis =
+  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
+  and largs = Array.to_list mis.mis_args in 
+  { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs;
+    typ = mis.mis_mip.mind_arity.typ }
+
+let mis_arity mispec =
+  let { body = b; typ = t } = mis_arity' mispec in
+  DOP2 (Cast, b, DOP0 (Sort t))
+
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 27bd8191ec..ba5a072a1e 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -24,5 +24,10 @@ val existential_type : 'a evar_map -> constr -> constr
 
 val const_abst_opt_value : unsafe_env -> constr -> constr option
 
-val mis_lc : unsafe_env -> mind_specif -> constr
+val mis_arity : mind_specif -> constr
+
+val mis_lc : mind_specif -> constr
+val mis_lc_without_abstractions : mind_specif -> constr array
+
+val mis_type_mconstructs : mind_specif -> constr array * constr array
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1a1ea5bbb4..0d4557efc6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -310,9 +310,8 @@ let fold_commands cl env sigma c =
 
 let abstract_scheme env (locc,a,ta) t =
   let na = named_hd env ta Anonymous in
-  if occur_meta ta then
-    error "cannot find a type for the generalisation"
-  else if occur_meta a then 
+  if occur_meta ta then error "cannot find a type for the generalisation";
+  if occur_meta a then 
     DOP2(Lambda,ta,DLAM(na,t))
   else 
     DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t))
diff --git a/kernel/term.ml b/kernel/term.ml
index 4694a75a25..543c41baa8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -52,6 +52,11 @@ type sorts =
 let mk_Set  = Prop Pos
 let mk_Prop = Prop Null
 
+let print_sort = function
+  | Prop Pos -> [< 'sTR "Set" >]
+  | Prop Null -> [< 'sTR "Prop" >]
+  | Type _ -> [< 'sTR "Type" >]
+
 type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
diff --git a/kernel/term.mli b/kernel/term.mli
index 5f8cfefc01..823917ea5f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Pp
 open Names
 open Generic
 (*i*)
@@ -39,6 +40,8 @@ type sorts =
 val mk_Set  : sorts
 val mk_Prop : sorts
 
+val print_sort : sorts -> std_ppcmds
+
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating the generic terms (type [term], 
   see \refsec{generic_terms}) on the above operators, themselves instanciated
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c072a368b4..db992769dd 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -26,6 +26,8 @@ type type_error =
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
+  | NotInductive of constr
+  | MLCase of string * constr * constr * constr * constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -71,4 +73,8 @@ let error_ill_formed_rec_body k env str lna i vdefs =
 let error_ill_typed_rec_body k env i lna vdefj vargs =
   raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
+let error_not_inductive k env c =
+  raise (TypeError (k, context env, NotInductive c))
 
+let error_ml_case k env mes c ct br brt =
+  raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 961a1b2511..fae63666c1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -28,6 +28,8 @@ type type_error =
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
+  | NotInductive of constr
+  | MLCase of string * constr * constr * constr * constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -72,3 +74,8 @@ val error_ill_typed_rec_body  :
   path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> 'b
 
+val error_not_inductive : path_kind -> unsafe_env -> constr -> 'a
+
+val error_ml_case : path_kind -> unsafe_env -> 
+  string -> constr -> constr -> constr -> constr -> 'a
+
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 010dde8e27..65406f2798 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -150,6 +150,31 @@ let type_mconstructs env sigma mind =
   let mis = lookup_mind_specif redmind env in 
   mis_type_mconstructs mis
 
+let mis_type_mconstruct i mispec =
+  let specif = instantiate_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in 
+  if i > nconstr then error "Not enough constructors in the type";
+  sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+
+let type_mconstruct env sigma i mind =
+  let redmind = check_mrectype_spec env sigma mind in
+  let (sp,tyi,args) = destMutInd redmind in
+  let mispec = lookup_mind_specif redmind env in 
+  mis_type_mconstruct i mispec
+
+let type_inst_construct env sigma i mind = 
+  try 
+    let (mI,largs) = find_mrectype env sigma mind in 
+    let mispec = lookup_mind_specif mI env in 
+    let nparams = mis_nparams mispec in 
+    let tc = mis_type_mconstruct i mispec in
+    let (globargs,_) = list_chop nparams largs in
+    hnf_prod_applist env sigma "Typing.type_construct" tc globargs
+  with Induc -> 
+    error_not_inductive CCI env mind
+
 (* Case. *)
 
 let rec sort_of_arity env sigma c =
@@ -221,8 +246,10 @@ let is_correct_arity env sigma kelim (c,p) =
 	   (fun s -> make_arity_dep env sigma (DOP0(Sort s)) t ind) kelim)
 	@(List.map 
 	    (fun s -> make_arity_nodep env sigma (DOP0(Sort s)) t) kelim)
-      in error_elim_arity CCI env ind listarity c p pt kinds
-  in srec 
+      in 
+      error_elim_arity CCI env ind listarity c p pt kinds
+  in 
+  srec 
 
 let cast_instantiate_arity mis =
   let tty = instantiate_arity mis in
@@ -291,15 +318,12 @@ let type_case_branches env sigma ct pt p c =
 let check_branches_message env sigma (c,ct) (explft,lft) = 
   let n = Array.length explft 
   and expn = Array.length lft in
-  let rec check_conv i = 
-    if not (i = n) then
-      if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
-	error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
-	  (nf_betaiota env sigma explft.(i))
-      else 
-	check_conv (i+1) 
-  in
-  if n<>expn then error_number_branches CCI env c ct expn else check_conv 0
+  if n<>expn then error_number_branches CCI env c ct expn;
+  for i = 0 to n-1 do
+    if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
+      error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
+	(nf_betaiota env sigma explft.(i))
+  done
 
 let type_of_case env sigma pj cj lfj =
   let lft = Array.map (fun j -> j.uj_type) lfj in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cb7f97ec57..45db129741 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 (*i*)
@@ -66,3 +65,22 @@ val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
 
 val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
+
+val type_one_branch_dep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr -> constr 
+
+val type_one_branch_nodep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr 
+
+val make_arity_dep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
+
+val make_arity_nodep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr 
+
+val find_case_dep_nparams :
+  unsafe_env -> 'a evar_map -> constr * constr ->
+    constr * constr list ->
+      constr -> bool * (int * constr list * constr list) 
+
+val type_inst_construct : unsafe_env -> 'a evar_map -> int -> constr -> constr