1 files changed, 122 insertions, 70 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index be4c0e1ecc..c9acd168e8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -69,7 +69,7 @@ let type_of_type u =
     mkType uu
 
 let type_of_sort = function
-  | Prop c -> type1
+  | Prop | Set -> type1
   | Type u -> type_of_type u
 
 (*s Type of a de Bruijn index. *)
@@ -91,7 +91,8 @@ let type_of_variable env id =
 (* Checks if a context of variables can be instantiated by the
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+  let conv env a b = conv env ?evars a b in
   Context.Named.fold_outside
     (fun d1 () ->
       let open Context.Named.Declaration in
@@ -118,14 +119,14 @@ let check_hyps_inclusion env f c sign =
 (* Type of constants *)
 
 
-let type_of_constant env (kn,u as cst) =
+let type_of_constant env (kn,_u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   let ty, cu = constant_type env cst in
   let () = check_constraints cu env in
     ty
 
-let type_of_constant_in env (kn,u as cst) =
+let type_of_constant_in env (kn,_u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   constant_type_in env cst
@@ -142,7 +143,7 @@ let type_of_constant_in env (kn,u as cst) =
   and no upper constraint exists on the sort $s$, we don't need to compute $s$
 *)
 
-let type_of_abstraction env name var ty =
+let type_of_abstraction _env name var ty =
   mkProd (name, var, ty)
 
 (* Type of an application. *)
@@ -150,39 +151,52 @@ let type_of_abstraction env name var ty =
 let make_judgev c t = 
   Array.map2 make_judge c t
 
+let rec check_empty_stack = function
+| [] -> true
+| CClosure.Zupdate _ :: s -> check_empty_stack s
+| _ -> false
+
 let type_of_apply env func funt argsv argstv =
+  let open CClosure in
   let len = Array.length argsv in
-  let rec apply_rec i typ = 
-    if Int.equal i len then typ
-    else 
-      (match kind (whd_all env typ) with
-      | Prod (_,c1,c2) ->
-	let arg = argsv.(i) and argt = argstv.(i) in
-	  (try
-	     let () = conv_leq false env argt c1 in
-	       apply_rec (i+1) (subst1 arg c2)
-	   with NotConvertible ->
-	     error_cant_apply_bad_type env
-	       (i+1,c1,argt)
-	       (make_judge func funt)
-	       (make_judgev argsv argstv))
-	    
+  let infos = create_clos_infos all env in
+  let tab = create_tab () in
+  let rec apply_rec i typ =
+    if Int.equal i len then term_of_fconstr typ
+    else
+      let typ, stk = whd_stack infos tab typ [] in
+      (** The return stack is known to be empty *)
+      let () = assert (check_empty_stack stk) in
+      match fterm_of typ with
+      | FProd (_, c1, c2, e) ->
+        let arg = argsv.(i) in
+        let argt = argstv.(i) in
+        let c1 = term_of_fconstr c1 in
+        begin match conv_leq false env argt c1 with
+        | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+        | exception NotConvertible ->
+          error_cant_apply_bad_type env
+            (i+1,c1,argt)
+            (make_judge func funt)
+            (make_judgev argsv argstv)
+        end
       | _ ->
-	error_cant_apply_not_functional env 
-	  (make_judge func funt)
-	  (make_judgev argsv argstv))
-  in apply_rec 0 funt
+        error_cant_apply_not_functional env
+          (make_judge func funt)
+          (make_judgev argsv argstv)
+  in
+  apply_rec 0 (inject funt)
 
 (* Type of product *)
 
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
     (* Product rule (s,Prop,Prop) *)
-    | (_,       Prop Null)  -> rangsort
+    | (_,       Prop)  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop _,  Prop Pos) -> rangsort
+    | ((Prop | Set),  Set) -> rangsort
     (* Product rule (Type,Set,?) *)
-    | (Type u1, Prop Pos) ->
+    | (Type u1, Set) ->
         if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
@@ -190,9 +204,9 @@ let sort_of_product env domsort rangsort =
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
+    | (Set,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Null, Type _)  -> rangsort
+    | (Prop, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
     | (Type u1, Type u2) -> Type (Universe.sup u1 u2)
 
@@ -204,7 +218,7 @@ let sort_of_product env domsort rangsort =
 
   where j.uj_type is convertible to a sort s2
 *)
-let type_of_product env name s1 s2 =
+let type_of_product env _name s1 s2 =
   let s = sort_of_product env s1 s2 in
     mkSort s
 
@@ -221,7 +235,7 @@ let check_cast env c ct k expected_type =
   try
     match k with
     | VMcast ->
-      vm_conv CUMUL env ct expected_type
+      Vconv.vm_conv CUMUL env ct expected_type
     | DEFAULTcast ->
       default_conv ~l2r:false CUMUL env ct expected_type
     | REVERTcast ->
@@ -247,7 +261,7 @@ let check_cast env c ct k expected_type =
    dynamic constraints of the form u<=v are enforced *)
 
 let type_of_inductive_knowing_parameters env (ind,u as indu) args =
-  let (mib,mip) as spec = lookup_mind_specif env ind in
+  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
@@ -264,7 +278,7 @@ let type_of_inductive env (ind,u as indu) =
 
 (* Constructors. *)
 
-let type_of_constructor env (c,u as cu) =
+let type_of_constructor env (c,_u as cu) =
   let () =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
@@ -285,7 +299,7 @@ let check_branch_types env (ind,u) c ct lft explft =
     | Invalid_argument _ ->
         error_number_branches env (make_judge c ct) (Array.length explft)
 
-let type_of_case env ci p pt c ct lf lft =
+let type_of_case env ci p pt c ct _lf lft =
   let (pind, _ as indspec) =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct) in
@@ -296,13 +310,13 @@ let type_of_case env ci p pt c ct lf lft =
   rslty
 
 let type_of_projection env p c ct =
-  let pb = lookup_projection p env in
+  let pty = lookup_projection p env in
   let (ind,u), args =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(MutInd.equal pb.proj_ind (fst ind));
-  let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
+  assert(eq_ind (Projection.inductive p) ind);
+  let ty = Vars.subst_instance_constr u pty in
   substl (c :: CList.rev args) ty
       
 
@@ -319,6 +333,52 @@ let check_fixpoint env lna lar vdef vdeft =
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar
 
+(* Global references *)
+
+let type_of_global_in_context env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    cb.Declarations.const_type, univs
+  | IndRef ind ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+    Inductive.type_of_inductive env (specif, inst), univs
+  | ConstructRef cstr ->
+    let (mib,_ as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
+
+(* Build a fresh instance for a given context, its associated substitution and
+   the instantiated constraints. *)
+
+let constr_of_global_in_context env r =
+  let open GlobRef in
+  match r with
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    mkConstU (c, Univ.make_abstract_instance univs), univs
+  | IndRef ind ->
+    let (mib,_) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkIndU (ind, Univ.make_abstract_instance univs), univs
+  | ConstructRef cstr ->
+    let (mib,_) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
+
 (************************************************************************)
 (************************************************************************)
 
@@ -399,7 +459,7 @@ let rec execute env cstr =
         let lft = execute_array env lf in
           type_of_case env ci p pt c ct lf lft
 
-    | Fix ((vn,i as vni),recdef) ->
+    | Fix ((_vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
         check_fix env fix; fix_ty
@@ -431,7 +491,15 @@ and execute_recdef env (names,lar,vdef) i =
 and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
+
+let check_wellformed_universes env c =
+  let univs = universes_of_constr c in
+  try UGraph.check_declared_universes (universes env) univs
+  with UGraph.UndeclaredLevel u ->
+    error_undeclared_universe env u
+
 let infer env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
     make_judge constr t
 
@@ -449,42 +517,36 @@ let type_judgment env {uj_val=c; uj_type=t} =
   {utj_val = c; utj_type = s }
 
 let infer_type env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
 let infer_v env cv =
+  let () = Array.iter (check_wellformed_universes env) cv in
   let jv = execute_array env cv in
     make_judgev cv jv
 
 (* Typing of several terms. *)
 
-let infer_local_decl env id = function
-  | Entries.LocalDefEntry c ->
-      let t = execute env c in
-      RelDecl.LocalDef (Name id, c, t)
-  | Entries.LocalAssumEntry c ->
-      let t = execute env c in
-      RelDecl.LocalAssum (Name id, check_assumption env c t)
-
-let infer_local_decls env decls =
-  let rec inferec env = function
-  | (id, d) :: l ->
-      let (env, l) = inferec env l in
-      let d = infer_local_decl env id d in
-        (push_rel d env, Context.Rel.add d l)
-  | [] -> (env, Context.Rel.empty)
-  in
-  inferec env decls
+let check_context env rels =
+  let open Context.Rel.Declaration in
+  Context.Rel.fold_outside (fun d env ->
+    match d with
+      | LocalAssum (_,ty) ->
+        let _ = infer_type env ty in
+        push_rel d env
+      | LocalDef (_,bd,ty) ->
+        let j1 = infer env bd in
+        let _ = infer_type env ty in
+        conv_leq false env j1.uj_type ty;
+        push_rel d env)
+    rels ~init:env
 
 let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1
 let judge_of_type u = make_judge (mkType u) (type_of_type u)
 
-let judge_of_prop_contents = function
-  | Null -> judge_of_prop
-  | Pos -> judge_of_set
-
 let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
 
 let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
@@ -509,7 +571,7 @@ let judge_of_product env x varj outj =
   make_judge (mkProd (x, varj.utj_val, outj.utj_val))
              (mkSort (sort_of_product env varj.utj_type outj.utj_type))
 
-let judge_of_letin env name defj typj j =
+let judge_of_letin _env name defj typj j =
   make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val))
              (subst1 defj.uj_val j.uj_type)
 
@@ -528,13 +590,3 @@ let judge_of_case env ci pj cj lfj =
   let lf, lft = dest_judgev lfj in
   make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
              (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
-
-let type_of_projection_constant env (p,u) =
-  let cst = Projection.constant p in
-  let cb = lookup_constant cst env in
-  match cb.const_proj with
-  | Some pb ->
-    if Declareops.constant_is_polymorphic cb then
-      Vars.subst_instance_constr u pb.proj_type
-    else pb.proj_type
-  | None -> raise (Invalid_argument "type_of_projection: not a projection")