Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.

TODO fix interface on knowing_parameters to avoid useless array allocations.

5 files changed, 59 insertions, 23 deletions

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 8b7230c3b..a68888c8c 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -132,11 +132,10 @@ let type_of_constant_in env cst =
   let ar = constant_type_in env cst in
     type_of_constant_knowing_parameters_arity env ar [||]
 
-let judge_of_constant_knowing_parameters env (kn,u as cst) jl =
+let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
-  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+  let ty, cu = type_of_constant_knowing_parameters env cst args in
   let () = check_constraints cu env in
     ty
 
@@ -278,13 +277,14 @@ let judge_of_cast env c ct k expected_type =
    the App case of execute; from this constraints, the expected
    dynamic constraints of the form u<=v are enforced *)
 
-(* let judge_of_inductive_knowing_parameters env ind jl = *)
-(*   let c = mkInd ind in *)
-(*   let (mib,mip) = lookup_mind_specif env ind in *)
-(*   check_args env c mib.mind_hyps; *)
-(*   let paramstyp = Array.map (fun j -> j.uj_type) jl in *)
-(*   let t =  in *)
-(*   make_judge c t *)
+let judge_of_inductive_knowing_parameters env (ind,u as indu) args =
+  let (mib,mip) as spec = lookup_mind_specif env ind in
+  check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+  let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters 
+    env (spec,u) args
+  in
+    check_constraints cst env;
+    t
 
 let judge_of_inductive env (ind,u as indu) =
   let (mib,mip) = lookup_mind_specif env ind in
@@ -382,7 +382,21 @@ let rec execute env cstr =
     (* Lambda calculus operators *)
     | App (f,args) ->
         let argst = execute_array env args in
-	let ft = execute env f in
+	let ft =
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+	      let args = Array.map (fun t -> lazy t) argst in
+		judge_of_inductive_knowing_parameters env ind args
+	    | Const cst ->
+		(* Sort-polymorphism of constant *)
+	      let args = Array.map (fun t -> lazy t) argst in
+	      judge_of_constant_knowing_parameters env cst args
+	    | _ ->
+		(* No sort-polymorphism *)
+		execute env f
+	in
+
 	  judge_of_apply env f ft args argst
 
     | Lambda (name,c1,c2) ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9862ffd3e..64a6f1e17 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -237,6 +237,11 @@ let constrained_type_of_inductive env ((mib,mip),u as pind) =
   let cst = instantiate_inductive_constraints mib subst in
     (ty, cst)
 
+let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
+  let ty, subst = type_of_inductive_gen env pind args in
+  let cst = instantiate_inductive_constraints mib subst in
+    (ty, cst)
+
 let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
   fst (type_of_inductive_gen env mip args)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a403003e2..a23d170f5 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -44,10 +44,13 @@ val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context
 val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
+val constrained_type_of_inductive_knowing_parameters : 
+  env -> mind_specif puniverses -> types Lazy.t array -> types constrained
 
 val type_of_inductive : env -> mind_specif puniverses -> types
 
-val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
+val type_of_inductive_knowing_parameters : 
+  env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
 
 val elim_sorts : mind_specif -> sorts_family list
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 63bd40681..0a89a0bfd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -632,7 +632,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
 
 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
   let b = 
-    if cv_pb = CUMUL then leq_constr_univs univs t1 t2 
+    if cv_pb == CUMUL then leq_constr_univs univs t1 t2 
     else eq_constr_univs univs t1 t2
   in
     if b then Constraint.empty
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09e2fb1d5..9428ace38 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -314,19 +314,21 @@ let judge_of_cast env cj k tj =
    the App case of execute; from this constraints, the expected
    dynamic constraints of the form u<=v are enforced *)
 
-(* let judge_of_inductive_knowing_parameters env ind jl = *)
-(*   let c = mkInd ind in *)
-(*   let (mib,mip) = lookup_mind_specif env ind in *)
-(*   check_args env c mib.mind_hyps; *)
-(*   let paramstyp = Array.map (fun j -> j.uj_type) jl in *)
-(*   let t =  in *)
-(*   make_judge c t *)
+let judge_of_inductive_knowing_parameters env (ind,u as indu) args =
+  let c = mkIndU indu in
+  let (mib,mip) as spec = lookup_mind_specif env ind in
+  check_hyps_inclusion env c mib.mind_hyps;
+  let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters 
+    env (spec,u) args
+  in
+    check_constraints cst env;
+    make_judge c t
 
 let judge_of_inductive env (ind,u as indu) =
   let c = mkIndU indu in
-  let (mib,mip) = lookup_mind_specif env ind in
+  let (mib,mip) as spec = lookup_mind_specif env ind in
   check_hyps_inclusion env c mib.mind_hyps;
-  let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
+  let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in
     check_constraints cst env;
     (make_judge c t)
 
@@ -424,7 +426,19 @@ let rec execute env cstr =
     (* Lambda calculus operators *)
     | App (f,args) ->
         let jl = execute_array env args in
-	let j = execute env f in
+	let j =
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+	      let args = Array.map (fun j -> lazy j.uj_type) jl in
+		judge_of_inductive_knowing_parameters env ind args
+	    | Const cst ->
+		(* Sort-polymorphism of constant *)
+	      judge_of_constant_knowing_parameters env cst jl
+	    | _ ->
+		(* No sort-polymorphism *)
+		execute env f
+	in
 	  judge_of_apply env j jl
 
     | Lambda (name,c1,c2) ->