MAJ pour fusion avec pretyping

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

10 files changed, 62 insertions, 34 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
index b31f2f6b79..b12e6e9930 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -20,7 +20,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : constr;
+  evar_concl : typed_type;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 62378f921e..036443f129 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -23,7 +23,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : constr;
+  evar_concl : typed_type;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 819dfcf841..37ffa5ca12 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -82,7 +82,8 @@ let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+  instantiate_constr (ids_of_sign hyps) (body_of_type info.evar_concl)
+    (Array.to_list args)
 
 let existential_value sigma c =
   let (n,args) = destEvar c in
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 9c2ffedb2f..26dc2b6170 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -234,4 +234,5 @@ let lookup_id id env =
 
 type 'b assumptions = (typed_type,'b) env
 type context = (typed_type,typed_type) env
+type var_context = typed_type signature
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index c67ab11d8f..af8dbe086f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -83,4 +83,5 @@ val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 
 type 'b assumptions = (typed_type,'b) env
 type context = (typed_type,typed_type) env
+type var_context = typed_type signature
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index db992769dd..eaef2dafc0 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -28,6 +28,7 @@ type type_error =
       * typed_type array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
+  | CantFindCaseType of constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -41,7 +42,7 @@ let error_not_type k env c =
   raise (TypeError (k, context env, NotAType c))
 
 let error_assumption k env c =
-    raise (TypeError (k, context env, BadAssumption c))
+  raise (TypeError (k, context env, BadAssumption c))
 
 let error_reference_variables k env id =
   raise (TypeError (k, context env, ReferenceVariables id))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index fae63666c1..23fed99f3e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -30,6 +30,7 @@ type type_error =
       * typed_type array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
+  | CantFindCaseType of constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 65406f2798..f20c5d213a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -175,6 +175,15 @@ let type_inst_construct env sigma i mind =
   with Induc -> 
     error_not_inductive CCI env mind
 
+let type_of_existential env sigma c =
+  let (ev,args) = destEvar c in
+  let evi = Evd.map sigma ev in
+  let hyps = get_globals (context evi.Evd.evar_env) in
+  let id = id_of_string ("?" ^ string_of_int ev) in
+  check_hyps id env sigma hyps;
+  instantiate_type (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
+
+
 (* Case. *)
 
 let rec sort_of_arity env sigma c =
@@ -338,14 +347,23 @@ let type_of_case env sigma pj cj lfj =
 
 (* Prop and Set *)
 
-let type_of_prop_or_set cts =
-  { uj_val = DOP0(Sort(Prop cts));
+let judge_of_prop =
+  { uj_val = DOP0(Sort prop);
+    uj_type = DOP0(Sort type_0);
+    uj_kind = DOP0(Sort type_1) }
+
+let judge_of_set =
+  { uj_val = DOP0(Sort spec);
     uj_type = DOP0(Sort type_0);
     uj_kind = DOP0(Sort type_1) }
 
+let make_judge_of_prop_contents = function
+  | Null -> judge_of_prop
+  | Pos -> judge_of_set
+
 (* Type of Type(i). *)
 
-let type_of_type u =
+let make_judge_of_type u =
   let (uu,uuu,c) = super_super u in
   { uj_val = DOP0 (Sort (Type u));
     uj_type = DOP0 (Sort (Type uu));
@@ -447,7 +465,7 @@ let apply_rel_list env sigma nocheck argjl funj =
  which may contain the CoFix variables. These occurrences of CoFix variables
  are not considered *)
 
-let noccur_with_meta lc n m term = 
+let noccur_with_meta n m term = 
   let rec occur_rec n = function
     | Rel p -> if n<=p & p<n+m then raise Occur
     | VAR _ -> ()
@@ -455,7 +473,7 @@ let noccur_with_meta lc n m term =
 	(match strip_outer_cast cl.(0) with
            | DOP0 (Meta _) -> ()
 	   | _ -> Array.iter (occur_rec n) cl)
-    | DOPN(Const sp, cl) when Spset.mem sp lc -> ()
+    | DOPN(Evar _, _) -> ()
     | DOPN(op,cl) -> Array.iter (occur_rec n) cl
     | DOPL(_,cl) -> List.iter (occur_rec n) cl
     | DOP0(_) -> ()
@@ -587,7 +605,7 @@ let is_subterm env sigma lcx mind_recvec n lst c =
 (* Auxiliary function: it checks a condition f depending on a deBrujin
    index for a certain number of abstractions *)
 
-let rec check_subterm_rec_meta env sigma lc vectn k def = 
+let rec check_subterm_rec_meta env sigma vectn k def = 
   (k < 0) or
   (let nfi = Array.length vectn in 
    (* check fi does not appear in the k+1 first abstractions, 
@@ -595,7 +613,7 @@ let rec check_subterm_rec_meta env sigma lc vectn k def =
    let rec check_occur n def = 
      (match strip_outer_cast def with
 	| DOP2(Lambda,a,DLAM(_,b)) -> 
-	    if noccur_with_meta lc n nfi a then
+	    if noccur_with_meta n nfi a then
               if n = k+1 then (a,b) else check_occur (n+1) b
             else 
 	      error "Bad occurrence of recursive call"
@@ -613,7 +631,7 @@ let rec check_subterm_rec_meta env sigma lc vectn k def =
    *)
    let rec check_rec_call n lst t = 
      (* n gives the index of the recursive variable *)
-     (noccur_with_meta lc (n+k+1) nfi t) or 
+     (noccur_with_meta (n+k+1) nfi t) or 
      (* no recursive call in the term *)
      (match whd_betadeltaiota_stack env sigma t [] with 
 	| (Rel p,l) -> 
@@ -726,7 +744,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
 the inductive-decreasing index 
 the function checks the convertibility of ti with Ai *)
 
-let check_fix env sigma lc = function
+let check_fix env sigma = function
   | DOPN(Fix(nvect,j),vargs) -> 
       let nbfix = let nv = Array.length vargs in 
       if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
@@ -742,7 +760,7 @@ let check_fix env sigma lc = function
 	let check_type i = 
 	  try
 	    let _ = 
-	      check_subterm_rec_meta env sigma lc nvect nvect.(i) vdefs.(i) in 
+	      check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in 
 	    ()
 	  with UserError (s,str) ->
 	    error_ill_formed_rec_body CCI env str lna i vdefs 
@@ -756,7 +774,7 @@ let check_fix env sigma lc = function
 let mind_nparams env i =
   let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
 
-let check_guard_rec_meta env sigma lc nbfix def deftype = 
+let check_guard_rec_meta env sigma nbfix def deftype = 
   let rec codomain_is_coind c  =
     match whd_betadeltaiota env sigma (strip_outer_cast c) with
       | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b 
@@ -771,7 +789,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
   let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
   let vlra = lvlra.(tyi) in  
   let rec check_rec_call alreadygrd n vlra  t = 
-    if noccur_with_meta lc n nbfix t then
+    if noccur_with_meta n nbfix t then
       true 
     else 
       match whd_betadeltaiota_stack env sigma t [] with 
@@ -781,7 +799,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
              if n <= p && p < n+nbfix then
 	       (* recursive call *)
                if alreadygrd then
-		 if List.for_all (noccur_with_meta lc n nbfix) l then
+		 if List.for_all (noccur_with_meta n nbfix) l then
 		   true
 		 else 
 		   error "Nested recursive occurrences"
@@ -820,19 +838,21 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
                                (process_args_of_constr lr lrar)
 				 
                        |  _::lrar  -> 
-                            if (noccur_with_meta lc n nbfix t) 
+                            if (noccur_with_meta n nbfix t) 
                             then (process_args_of_constr lr lrar)
                             else error "Recursive call inside a non-recursive argument of constructor")
             in (process_args_of_constr realargs lra)
 		 
 		 
 	| (DOP2(Lambda,a,DLAM(_,b)),[]) -> 
-            if (noccur_with_meta lc n nbfix a) then
+            if (noccur_with_meta n nbfix a) then
               check_rec_call alreadygrd (n+1)  vlra b
             else 
 	      error "Recursive call in the type of an abstraction"
 	      
 	| (DOPN(CoFix(j),vargs),l) -> 
+          if  (List.for_all (noccur_with_meta n nbfix) l)
+          then 
             let nbfix = let nv = Array.length vargs in 
             if nv < 2 then
               error "Ill-formed recursive definition" 
@@ -845,18 +865,19 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
             let (lna,vdefs) = decomp_DLAMV_name la ldef in
             let vlna = Array.of_list lna 
             in 
-	    if (array_for_all (noccur_with_meta lc n nbfix) varit) then
+	    if (array_for_all (noccur_with_meta n nbfix) varit) then
               (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
               &&
               (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
             else 
 	      error "Recursive call in the type of a declaration"
-		
+	  else error "Unguarded recursive call"
+
 	| (DOPN(MutCase _,_) as mc,l) -> 
             let (_,p,c,vrest) = destCase mc in
-            if (noccur_with_meta lc n nbfix p) then
-              if (noccur_with_meta lc n nbfix c) then
-		if (List.for_all (noccur_with_meta lc n nbfix) l) then
+            if (noccur_with_meta n nbfix p) then
+              if (noccur_with_meta n nbfix c) then
+		if (List.for_all (noccur_with_meta n nbfix) l) then
 		  (array_for_all (check_rec_call alreadygrd n vlra) vrest)
 		else 
 		  error "Recursive call in the argument of a function defined by cases"        
@@ -873,7 +894,7 @@ let check_guard_rec_meta env sigma lc nbfix def deftype =
 (* The  function which checks that the whole block of definitions 
    satisfies the guarded condition *)
 
-let check_cofix env sigma lc f = 
+let check_cofix env sigma f = 
   match f with
     | DOPN(CoFix(j),vargs) -> 
 	let nbfix = let nv = Array.length vargs in 
@@ -890,7 +911,7 @@ let check_cofix env sigma lc f =
 	let check_type i = 
 	  try 
 	    let _ = 
-	      check_guard_rec_meta env sigma lc nbfix vdefs.(i) varit.(i) in 
+	      check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in 
 	    ()
 	  with UserError (s,str) -> 
 	    error_ill_formed_rec_body CCI env str lna i vdefs 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 45db129741..1e602e0397 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -32,6 +32,8 @@ val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type
 
 val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr
 
+val type_of_existential : unsafe_env -> 'a evar_map -> constr -> typed_type
+
 val type_of_case : unsafe_env -> 'a evar_map 
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment
@@ -40,9 +42,9 @@ val type_case_branches :
   unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
     -> constr * constr array * constr 
 
-val type_of_prop_or_set : contents -> unsafe_judgment
+val make_judge_of_prop_contents : contents -> unsafe_judgment
 
-val type_of_type : universe -> unsafe_judgment * constraints
+val make_judge_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
   unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
@@ -60,8 +62,8 @@ val apply_rel_list :
   unsafe_env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
-val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
+val check_fix : unsafe_env -> 'a evar_map -> constr -> unit
+val check_cofix : unsafe_env -> 'a evar_map -> constr -> unit
 
 val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 27b50dceba..db3d00302e 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -79,20 +79,20 @@ let rec execute mf env cstr =
           error "General Fixpoints not allowed";
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
-        check_fix env Evd.empty Spset.empty fix;
+        check_fix env Evd.empty fix;
 	(make_judge fix larv.(i), cst)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
         let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
-        check_cofix env Evd.empty Spset.empty cofix;
+        check_cofix env Evd.empty cofix;
 	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
-	(type_of_prop_or_set c, cst0)
+	(make_judge_of_prop_contents c, cst0)
 
     | IsSort (Type u) ->
-	type_of_type u
+	make_judge_of_type u
 	  
     | IsAppL (f,args) ->
 	let (j,cst1) = execute mf env f in