Inductifs avec polymorphisme de sorte (version initiale)

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

4 files changed, 79 insertions, 45 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 68342e706d..b99ada7693 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -367,21 +367,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 
-	in let resj = apply_rec env 1 fj args in
-	  (*
-	    let apply_one_arg (floc,tycon,jl) c =
-	    let (dom,rng) = split_tycon floc env isevars tycon in
-	    let cj = pretype dom env isevars lvar c in
-	    let rng_tycon =
-	    option_app (subst1 cj.uj_val) rng in
-	    let argloc = loc_of_rawconstr c in
-	    (join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
-	    let _,_,jl =
-	    List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in
-	    let jl = List.rev jl in
-	    let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in
-	  *)
-	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+	in 
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+	let resj =
+	  match kind_of_term resj.uj_val with
+	  | App (f,args) when isInd f ->
+	      let sigma = evars_of !isevars in
+	      let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in
+	      let s = snd (splay_arity env sigma t) in
+	      on_judgment_type (set_inductive_level env s) resj
+		(* Rem: no need to send sigma: no head evar, it's an arity *)
+	  | _ -> resj in
+	inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RLambda(loc,name,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 715f54731c..776f1313f0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,11 +18,6 @@ open Environ
 open Typeops
 open Declarations
 
-let outsort env sigma t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
-    | Sort s -> s
-    | _ -> anomaly "Retyping: found a type of type which is not a sort"
-
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -38,9 +33,9 @@ let rec subst_type env sigma typ = function
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env ar =
     match kind_of_term (whd_betadeltaiota env sigma ar) with
-      | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
-      | Sort s -> s
-      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
+    | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
+    | Sort s -> s
+    | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
 
 let typeur sigma metamap =
@@ -78,7 +73,10 @@ let typeur sigma metamap =
          subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args)->
+    | App(f,args) when isInd f ->
+	let t = type_of_applied_inductive env (destInd f) args in
+        strip_outer_cast (subst_type env sigma t (Array.to_list args))
+    | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Cast (c,_, t) -> t
@@ -95,12 +93,17 @@ let typeur sigma metamap =
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when
               Environ.engagement env = Some ImpredicativeSet -> s
-          | Type _ as s, Prop Pos -> s
-	  | _, (Type u2 as s) -> s (*Type Univ.dummy_univ*))
+          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.base_univ)
+	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
+	  | Prop Null, (Type _ as s) -> s
+	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+    | App(f,args) when isInd f ->
+	let t = type_of_applied_inductive env (destInd f) args in
+        sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
-    | _ -> outsort env sigma (type_of env t)
+    | _ -> decomp_sort env sigma (type_of env t)
 
   and sort_family_of env t =
     match kind_of_term t with
@@ -112,16 +115,31 @@ let typeur sigma metamap =
        family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ ->
         anomaly "sort_of: Not a type (1)"
-    | _ -> family_of_sort (outsort env sigma (type_of env t))
+    | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
+
+  and type_of_applied_inductive env ind args =
+    let specif = lookup_mind_specif env ind in
+    let t = Inductive.type_of_inductive specif in
+    if is_small_inductive specif then
+      (* No polymorphism *)
+      t
+    else
+      (* Retyping constructor with the actual arguments *)
+      let env',llc,ls0 = constructor_instances env specif ind args in
+      let lls = Array.map (Array.map (sort_of env')) llc in
+      let ls = Array.map max_inductive_sort lls in
+      set_inductive_level env (find_inductive_level env specif ind ls0 ls) t
 
-  in type_of, sort_of, sort_family_of
+  in type_of, sort_of, sort_family_of, type_of_applied_inductive
 
-let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c
-let get_sort_of env sigma t = let _,f,_ = typeur sigma [] in f env t
-let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c
+let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
+let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
+let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
+let type_of_applied_inductive env sigma ind args =
+  let _,_,_,f = typeur sigma [] in f env ind args
 
 let get_type_of_with_meta env sigma metamap = 
-  let f,_,_ = typeur sigma metamap in f env
+  let f,_,_,_ = typeur sigma metamap in f env
 
 (* Makes an assumption from a constr *)
 let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index f0c01a56ec..8631f55453 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Names
 open Term
 open Evd
 open Environ
@@ -32,3 +33,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
 
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
+
+val type_of_applied_inductive : env -> evar_map -> inductive -> 
+  constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 38febedaa5..85e75586b7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -91,7 +91,11 @@ let rec execute env evd cstr =
 	let j = execute env evd f in
         let jl = execute_array env evd args in
 	let (j,_) = judge_of_apply env j jl in
-	j
+	if isInd f then
+	  (* Sort-polymorphism of inductive types *)
+	  adjust_inductive_level env evd (destInd f) args j
+	else
+	  j
 	    
     | Lambda (name,c1,c2) -> 
         let j = execute env evd c1 in
@@ -133,17 +137,28 @@ and execute_recdef env evd (names,lar,vdef) =
   let _ = type_fixpoint env1 names lara vdefj in
   (names,lara,vdefv)
 
-and execute_array env evd v =
-  let jl = execute_list env evd (Array.to_list v) in
-  Array.of_list jl
-
-and execute_list env evd = function
-  | [] -> 
-      []
-  | c::r -> 
-      let j = execute env evd c in 
-      let jr = execute_list env evd r in
-      j::jr
+and execute_array env evd = Array.map (execute env evd)
+
+and execute_list env evd = List.map (execute env evd)
+
+and adjust_inductive_level env evd ind args j =
+  let specif = lookup_mind_specif env ind in
+  if is_small_inductive specif then
+    (* No polymorphism *)
+    j
+  else
+    (* Retyping constructor with the actual arguments *)
+    let env',llc,ls0 = constructor_instances env specif ind args in
+    let llj = Array.map (execute_array env' evd) llc in
+    let ls =
+      Array.map (fun lj ->
+	let ls =
+	  Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj
+	in
+	max_inductive_sort ls) llj
+    in
+    let s = find_inductive_level env specif ind ls0 ls in
+    on_judgment_type (set_inductive_level env s) j
 
 let mcheck env evd c t =
   let sigma = Evd.evars_of evd in