ajout des inductifs (sans types singletons pour l'instant)

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

10 files changed, 365 insertions, 24 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5cd8cc801c..3608e969fe 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -223,3 +223,4 @@ type unsafe_judgment = {
 let cast_of_judgment = function
   | { uj_val = DOP2 (Cast,_,_) as c } -> c
   | { uj_val = c; uj_type = ty } -> mkCast c ty
+
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 82da97329a..0988ae1972 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,8 +1,13 @@
 
 (* $Id$ *)
 
+open Util
+open Generic
+open Term
 open Inductive
+open Sign
 open Environ
+open Instantiate
 open Reduction
 
 let mind_check_arities env mie =
@@ -11,3 +16,230 @@ let mind_check_arities env mie =
   in
   List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
 
+let sort_of_arity env c =
+  let rec sort_of ar =
+    match whd_betadeltaiota env ar with
+      | DOP0 (Sort s) -> s
+      | DOP2 (Prod, _, DLAM (_, c)) -> sort_of c
+      | _ -> error "not an arity"
+  in
+  sort_of c
+
+let allowed_sorts issmall isunit = function
+  | Type _ -> 
+      [prop;spec;types]
+  | Prop Pos -> 
+      if issmall then [prop;spec;types] else [prop;spec]
+  | Prop Null -> 
+      if isunit then [prop;spec] else [prop]
+
+let is_small_type t = is_small t.typ
+
+let failwith_non_pos_vect n ntypes v =
+  for i = 0 to Array.length v - 1 do
+    for k = n to n + ntypes - 1 do
+      if not (noccurn k v.(i)) then raise (InductiveError (NonPos (k-n+1)))
+    done
+  done;
+  anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
+
+let check_correct_par env nparams ntypes n l largs =
+  if Array.length largs < nparams then raise (InductiveError (NotEnoughArgs l));
+  let (lpar,largs') = array_chop nparams largs in
+  for k = 0 to nparams - 1 do
+    if not ((Rel (n-k-1))= whd_betadeltaiotaeta env lpar.(k)) then
+      raise (InductiveError (NonPar (k+1,l)))
+  done;
+  if not (array_for_all (noccur_bet n ntypes) largs') then 
+    failwith_non_pos_vect n ntypes largs'
+
+let abstract_mind_lc env ntyps npars lc = 
+  let lC = decomp_DLAMV ntyps lc in
+  if npars = 0 then 
+    lC 
+  else 
+    let make_abs = 
+      list_tabulate
+	(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps 
+    in 
+    Array.map (compose (nf_beta env) (substl make_abs)) lC
+
+let decomp_par n c = snd (decompose_prod_n n c)
+      
+let listrec_mconstr env ntypes nparams i indlc =
+  (* check the inductive types occur positively in C *)
+  let rec check_pos n c = 
+    match whd_betadeltaiota env c with 
+      | DOP2(Prod,b,DLAM(na,d)) -> 
+          if not (noccur_bet n ntypes b) then raise (InductiveError (NonPos n));
+	  check_pos (n+1) d
+      | x -> 
+	  (match ensure_appl x with 
+             | DOPN(AppL,cl) -> 
+                 let hd = array_hd cl 
+		 and largs = array_tl cl in
+                 (match hd with 
+                    | Rel k -> 
+			check_correct_par env nparams ntypes n (k-n+1) largs;
+                        if k >= n && k<n+ntypes then 
+			  Mrec(n+ntypes-k-1) 
+                        else if noccur_bet n ntypes x then 
+			  if (n-nparams) <= k & k <= (n-1) 
+			  then Param(n-1-k)
+                          else Norec
+			else 
+			  raise (InductiveError (NonPos n))
+                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                        if (noccur_bet n ntypes x) then
+                          Norec
+                        else 
+			  Imbr(sp,i,imbr_positive n mi largs)
+                    | err -> 
+			if noccur_bet n ntypes x then Norec
+			else raise (InductiveError (NonPos n)))
+             | _ -> anomaly "check_pos")
+	  
+  and imbr_positive n mi largs = 
+    let mispeci = lookup_mind_specif mi env in
+    let auxnpar = mis_nparams mispeci in
+    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 
+    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
+    (* The abstract imbricated inductive type with parameters substituted *)
+    let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
+    let newidx = n + auxntyp in
+    let _ = 
+      (* fails if the inductive type occurs non positively *)
+      (* when substituted *) 
+      Array.map 
+	(function c -> 
+	   let c' = hnf_prod_appvect env "is_imbr_pos" c 
+		      (Array.map (lift auxntyp) lpar) in 
+	   check_construct false newidx c') 
+	auxlcvect
+    in 
+    lrecargs
+
+  (* The function check_param_pos is exactly the same as check_pos, but
+     with an extra case for traversing abstractions, like in Marseille's
+     contribution about bisimulations:
+     
+     CoInductive strong_eq:process->process->Prop:=
+       str_eq:(p,q:process)((a:action)(p':process)(transition p a p')->
+          (Ex [q':process] (transition q a q')/\(strong_eq p' q')))->
+             ((a:action)(q':process)(transition q a q')->
+          (Ex [p':process] (transition p a p')/\(strong_eq p' q')))->
+          (strong_eq p q).
+
+     Abstractions may occur in imbricated recursive ocurrences, but I am
+     not sure if they make sense in a form of constructor. This is why I
+     chose to duplicated the code.  Eduardo 13/7/99. *)
+  and check_param_pos n c = 
+    match whd_betadeltaiota env c with 
+      (* The extra case *)
+      | DOP2(Lambda,b,DLAM(na,d)) -> 
+          if noccur_bet n ntypes b
+          then check_param_pos (n+1) d
+          else raise (InductiveError (NonPos n))
+      (******************)
+      | DOP2(Prod,b,DLAM(na,d)) -> 
+          if (noccur_bet n ntypes b) 
+          then check_param_pos (n+1) d
+          else raise (InductiveError (NonPos n))
+      | x -> 
+	  (match ensure_appl x with 
+             | DOPN(AppL,cl) -> 
+                 let hd = array_hd cl 
+		 and largs = array_tl cl in 
+		 (match hd with 
+                    | Rel k -> 
+                        check_correct_par env nparams ntypes n (k-n+1) largs;
+			if k >= n & k<n+ntypes then 
+			  Mrec(n+ntypes-k-1) 
+                        else if noccur_bet n ntypes x then 
+			  if (n-nparams) <= k & k <= (n-1)
+                          then Param(n-1-k)
+                          else Norec
+			else raise (InductiveError (NonPos n))
+                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                        if (noccur_bet n ntypes x) 
+                        then Norec
+                        else Imbr(sp,i,imbr_positive n mi largs)
+                    | err -> if noccur_bet n ntypes x then Norec
+		      else raise (InductiveError (NonPos n)))
+             | _ -> anomaly "check_param_pos")
+  
+  (* check the inductive types occur positively in the products of C, if
+     checkhd=true, also check the head corresponds to a constructor of
+     the ith type *) 
+
+  and check_construct check = 
+    let rec check_constr_rec lrec n c = 
+      match whd_betadeltaiota env c with
+        | DOP2(Prod,b,DLAM(na,d)) -> 
+            let recarg = (check_pos n b) in 
+	    check_constr_rec (recarg::lrec) (n+1) d 
+	| x -> 
+	    (match ensure_appl x with 
+               | DOPN(AppL,cl) ->
+                   let hd = array_hd cl 
+                   and largs = array_tl cl in 
+                   if check then 
+                     (match hd with 
+			| Rel k -> 
+			    check_correct_par env nparams ntypes n (k-n+1) largs;
+                            if k = n+ntypes-i then 
+			      List.rev lrec 
+                            else 
+			      raise (InductiveError (NonPos n))
+                        | _ -> raise (InductiveError (NonPos n)))
+                   else 
+                     if array_for_all (noccur_bet n ntypes) largs 
+                     then List.rev lrec 
+                     else raise (InductiveError (NonPos n)) 
+	       | _ -> anomaly "ensure_appl should return an AppL") 
+    in check_constr_rec []
+  in
+  let (lna,lC) = decomp_DLAMV_name ntypes indlc in
+  Array.map
+    (fun c ->
+       (* try *)
+       check_construct true (1+nparams) (decomp_par nparams c)
+       (* with InductiveError err -> 
+	    explain_ind_err (ntypes-i+1) lna nparams c err *))
+    lC
+    
+let is_recursive listind =
+  let rec one_is_rec rvec = 
+    List.exists (function Mrec(i) -> List.mem i listind 
+                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Norec -> false
+                   | Param _ -> false) rvec
+  in 
+  array_exists one_is_rec
+
+let cci_inductive env env_ar kind nparams finite inds =
+  let ntypes = List.length inds in
+  let one_packet i (id,ar,cnames,issmall,isunit,lc) =
+    let recargs = listrec_mconstr env_ar ntypes nparams i lc in
+    let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
+    let kelim = allowed_sorts issmall isunit (sort_of_arity env ar.body) in
+    { mind_consnames = Array.of_list cnames;
+      mind_typename = id;
+      mind_lc = lc;
+      mind_arity  = ar;
+      mind_kelim = kelim;
+      mind_listrec = recargs;
+      mind_finite = finite }
+  in
+  let packets = Array.of_list (list_map_i one_packet 1 inds) in
+  { mind_kind = kind;
+    mind_ntypes = ntypes;
+    mind_hyps = get_globals (context env);
+    mind_packets = packets;
+    mind_singl = None;
+    mind_nparams = nparams }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8723ec3c65..ebb1e1f679 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 (*i*)
+open Names
+open Term
 open Inductive
 open Environ
 (*i*)
@@ -10,3 +12,11 @@ open Environ
    inductive types are some arities. *)
 
 val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit
+
+val sort_of_arity : 'a unsafe_env -> constr -> sorts
+
+val cci_inductive : 
+  'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> 
+    (identifier * typed_type * identifier list * bool * bool * constr) list ->
+      mutual_inductive_body
+
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 6302badc22..9b4c1ae710 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -8,6 +8,7 @@ open Generic
 open Term
 open Sign
 open Constant
+open Inductive
 open Evd
 open Environ
 
@@ -101,3 +102,8 @@ let const_abst_opt_value env c =
     | DOPN(Abst sp,_) ->
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
+
+let mis_lc env mis =
+  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
+    (Array.to_list mis.mis_args)
+
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 0bcdabf6d2..73d6de1b12 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Names
 open Term
+open Inductive
 open Environ
 (*i*)
 
@@ -21,3 +22,6 @@ val const_or_ex_value : 'a unsafe_env -> constr -> constr
 val const_or_ex_type : 'a unsafe_env -> constr -> constr
 
 val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
+
+val mis_lc : 'a unsafe_env -> mind_specif -> constr
+
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7e81089453..77331bf5a2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1306,7 +1306,13 @@ let is_type_arity env =
       | _ -> false
   in 
   srec 
-    
+
+let is_info_type env t =
+  let s = t.typ in
+  (s = Prop Pos) ||
+  (s <> Prop Null && 
+   try info_arity env t.body with IsType -> true)
+
 let is_info_cast_type env c = 
   match c with  
     | DOP2(Cast,c,t) -> 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index c9cafccec4..6e6c243c76 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -104,6 +104,7 @@ val is_info_arity : 'c unsafe_env -> constr -> bool
 val is_info_sort : 'c unsafe_env -> constr -> bool
 val is_logic_arity : 'c unsafe_env -> constr -> bool
 val is_type_arity : 'c unsafe_env -> constr -> bool
+val is_info_type : 'c unsafe_env -> typed_type -> bool
 val is_info_cast_type : 'c unsafe_env -> constr -> bool
 val contents_of_cast_type : 'c unsafe_env -> constr -> contents
 val poly_args : 'a unsafe_env -> constr -> int list
diff --git a/kernel/term.ml b/kernel/term.ml
index 94ce20615e..46bcebcd84 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -59,6 +59,8 @@ type 'a judge = { body : constr; typ : 'a }
 type typed_type = sorts judge
 type typed_term = typed_type judge
 
+let make_typed t s = { body = t; typ = s }
+
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
 let body_of_type ty = ty.body
diff --git a/kernel/term.mli b/kernel/term.mli
index 0af1cf6133..0fc2a5e8f0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -56,6 +56,8 @@ type 'a judge = { body : constr; typ : 'a }
 type typed_type = sorts judge
 type typed_term = typed_type judge
 
+val make_typed : constr -> sorts -> typed_type
+
 val typed_app : (constr -> constr) -> typed_type -> typed_type
 
 val body_of_type : typed_type -> constr
diff --git a/kernel/typing.ml b/kernel/typing.ml
index b9ef2893a2..1366738689 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -16,6 +16,8 @@ open Type_errors
 open Typeops
 open Indtypes
 
+type judgment = unsafe_judgment
+
 (* Fonctions temporaires pour relier la forme castée de la forme jugement *)
 
 let tjudge_of_cast env = function
@@ -232,6 +234,23 @@ let unsafe_type_of env c =
 let unsafe_type_of_type env c = 
   let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
 
+(* Typing of several terms. *)
+
+let safe_machine_l env cl =
+  let type_one (env,l) c =
+    let (j,u) = safe_machine env c in
+    (set_universes u env, j::l)
+  in
+  List.fold_left type_one (env,[]) cl
+
+let safe_machine_v env cv =
+  let type_one (env,l) c =
+    let (j,u) = safe_machine env c in
+    (set_universes u env, j::l)
+  in
+  let env',l = Array.fold_left type_one (env,[]) cv in
+  (env', Array.of_list l)
+ 
 
 (*s Safe environments. *)
 
@@ -307,39 +326,97 @@ let add_parameter sp c env =
 
 (* Insertion of inductive types. *)
 
-let check_type_constructs env_params univ nparams lc =
-  let check_one env c =
-    let (_,c) = decompose_prod_n nparams c in
-    let (j,u) = safe_machine env c in
-    match whd_betadeltaiota env j.uj_type with
-      | DOP0 (Sort (Type uc)) -> set_universes (enforce_geq univ uc u) env
-      | _ -> error "Type of Constructor not well-formed"
+(* [for_all_prods p env c] checks a boolean condition [p] on all types
+   appearing in products in front of [c]. The boolean condition [p] is a 
+   function taking a value of type [typed_type] as argument. *)
+
+let rec for_all_prods p env c =
+  match whd_betadeltaiota env c with
+    | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> 
+	(p (make_typed t s)) &&
+	(let ty = { body = t; typ = s } in
+	 let env' = Environ.push_rel (name,ty) env in
+	 for_all_prods p env' c)
+    | DOP2(Prod, b, DLAM(name,c)) -> 
+	let (jb,u) = unsafe_machine env b in
+	let var = assumption_of_judgement env jb in
+	(p var) &&
+	(let env' = Environ.push_rel (name,var) (set_universes u env) in
+	 for_all_prods p env' c)
+    | _ -> true
+
+let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
+
+let enforce_type_constructor env univ j =
+  match whd_betadeltaiota env j.uj_type with
+    | DOP0 (Sort (Type uc)) -> 
+	let u = universes env in
+	set_universes (enforce_geq univ uc u) env
+    | _ -> error "Type of Constructor not well-formed"
+
+let type_one_constructor env_ar env_par nparams ar c =
+  let (jc,u) = safe_machine env_ar c in
+  let env = set_universes u env_ar in
+  let env' = match sort_of_arity env_ar ar with
+    | Type u -> enforce_type_constructor env u jc
+    | Prop _ -> env 
   in
-  Array.fold_left check_one env_params lc
-
-let check_prop_constructs env_ar lc =
-  let check_one c = 
-    let (j,_) = safe_machine env_ar c in
-    match whd_betadeltaiota env_ar j.uj_type with
-      | DOP0 (Sort _) -> cast_of_judgment j
-      | _ -> error "The type of a constructor must be a type"
+  let (_,c) = decompose_prod_n nparams jc.uj_val in
+  let issmall = is_small_type env_par c in
+  (env', (issmall,jc))
+
+let logic_constr env c =
+  for_all_prods (fun t -> not (is_info_type env t)) env c
+
+let logic_arity env c =
+  for_all_prods 
+    (fun t -> (not (is_info_type env t)) or (is_small_type env t.body)) env c
+
+let is_unit env_par nparams ar spec =
+  match decomp_all_DLAMV_name spec with
+    | (_,[|c|]) ->
+	(let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) &&
+	(let (_,c') = decompose_prod_n nparams c in logic_constr env_par c')
+    | _ -> false
+
+let type_one_inductive env_ar env_par nparams (id,ar,cnames,spec) =
+  let (lna,vc) = decomp_all_DLAMV_name spec in
+  let (env',(issmall,jlc)) = 
+    List.fold_left 
+      (fun (env,(small,jl)) c -> 
+	 let (env',(sm,jc)) = type_one_constructor env env_par nparams ar c in
+	 (env', (small && sm,jc::jl)))
+      (env_ar,(true,[])) (Array.to_list vc)
   in
-  Array.map check_one lc
+  let castlc = List.map cast_of_judgment jlc in
+  let spec' = put_DLAMSV lna (Array.of_list castlc) in
+  let isunit = is_unit env_par nparams ar spec in
+  let (_,tyar) = lookup_var id env' in
+  (env', (id,tyar,cnames,issmall,isunit,spec'))
 
 let add_mind sp mie env =
   mind_check_names mie;
   mind_check_arities env mie;
   let params = mind_extract_and_check_params mie in
+  let nparams = mie.mind_entry_nparams in
   mind_check_lc params mie;
-  let env_arities = 
-    push_rels 
-      (List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds) env 
+  let types_sign = 
+    List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
   in
+  let env_arities = push_rels types_sign env in
   let env_params = push_rels params env_arities in
-  (* ICI *)
-  env_arities
-
-type judgment = unsafe_judgment
+  let env_arities',inds =
+    List.fold_left 
+      (fun (env,inds) ind -> 
+	 let (env',ind') = type_one_inductive env env_params nparams ind in
+	 (env',ind'::inds))
+      (env_arities,[]) mie.mind_entry_inds
+  in
+  let kind = kind_of_path sp in
+  let mib = 
+    cci_inductive env env_arities' kind nparams mie.mind_entry_finite inds
+  in
+  add_mind sp mib (set_universes (universes env_arities') env)
 
 
 (*s Machines with information. *)