1 files changed, 78 insertions, 54 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a084504dcb..9aa688fc71 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,29 +22,35 @@ open Declarations
 open Environ
 open Entries
 open Typeops
+open Fast_typeops
 
-let constrain_type env j cst1 = function
-  | `None ->
-      make_polymorphic_if_constant_for_ind env j, cst1
+let debug = false
+let prerr_endline =
+  if debug then prerr_endline else fun _ -> ()
+
+let constrain_type env j poly = function
+  | `None -> j.uj_type
   | `Some t ->
-      let (tj,cst2) = infer_type env t in
-      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-      assert (eq_constr t tj.utj_val);
-      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
-      NonPolymorphicType t, cstrs
-  | `SomeWJ (t, tj, cst2) ->
-      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-      assert (eq_constr t tj.utj_val);
-      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
-      NonPolymorphicType t, cstrs
+      let tj = infer_type env t in
+      let _ = judge_of_cast env j DEFAULTcast tj in
+	assert (eq_constr t tj.utj_val);
+	t
+  | `SomeWJ (t, tj) ->
+      let tj = infer_type env t in
+      let _ = judge_of_cast env j DEFAULTcast tj in
+	assert (eq_constr t tj.utj_val);
+	t
 
 let map_option_typ = function None -> `None | Some x -> `Some x
 
-let translate_local_assum env t =
-  let (j,cst) = infer env t in
-  let t = Typeops.assumption_of_judgment env j in
-    (t,cst)
-
+let local_constrain_type env j = function
+  | None ->
+      j.uj_type
+  | Some t ->
+      let tj = infer_type env t in
+      let _ = judge_of_cast env j DEFAULTcast tj in
+      assert (eq_constr t tj.utj_val);
+      t
 
 (* Insertion of constants and parameters in environment. *)
 
@@ -59,19 +65,19 @@ let handle_side_effects env body side_eff =
         if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
-      | Const c' when eq_constant c c' -> mkRel i
+      | Const (c', _) when eq_constant c c' -> mkRel i
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
     let fix_body (c,cb) t =
       match cb.const_body with
       | Undef _ -> assert false
       | Def b ->
           let b = Mod_subst.force_constr b in
-          let b_ty = Typeops.type_of_constant_type env cb.const_type in
+          let b_ty = cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkLetIn (cname c, b, b_ty, t)
       | OpaqueDef b -> 
           let b = Opaqueproof.force_proof b in
-          let b_ty = Typeops.type_of_constant_type env cb.const_type in
+          let b_ty = cb.const_type in
           let t = sub c 1 (Vars.lift 1 t) in
           mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
     List.fold_right fix_body cbl t
@@ -86,46 +92,50 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
   
-let infer_declaration env dcl =
+let infer_declaration env kn dcl =
   match dcl with
-  | ParameterEntry (ctx,t,nl) ->
-      let j, cst = infer env t in
+  | ParameterEntry (ctx,poly,(t,uctx),nl) ->
+      let env = push_context uctx env in
+      let j = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, NonPolymorphicType t, cst, false, ctx
+      Undef nl, t, None, poly, Future.from_val uctx, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
+      let env = push_context c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
-      let tyj, tycst = infer_type env typ in
+      let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
           let body = handle_side_effects env body side_eff in
-          let j, cst = infer env body in
+          let j = infer env body in
           let j = hcons_j j in
-          let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
+          let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, cst) in
+          j.uj_val, Univ.empty_constraint) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      let typ = NonPolymorphicType typ in
-      def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
+      def, typ, None, c.const_entry_polymorphic, Future.from_val c.const_entry_universes,
+	c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
+      let env = push_context c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let body, side_eff = Future.join body in
       let body = handle_side_effects env body side_eff in
-      let j, cst = infer env body in
+      let j = infer env body in
       let j = hcons_j j in
-      let typ, cst = constrain_type env j cst (map_option_typ typ) in
+      let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in
       feedback_completion_typecheck feedback_id;
       let def = Def (Mod_subst.from_val j.uj_val) in
-      def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+      def, typ, None, c.const_entry_polymorphic,
+        Future.from_val c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx
 
-let global_vars_set_constant_type env = function
-  | NonPolymorphicType t -> global_vars_set env t
-  | PolymorphicArity (ctx,_) ->
-      Context.fold_rel_context
-        (fold_rel_declaration
-	  (fun t c -> Id.Set.union (global_vars_set env t) c))
-      ctx ~init:Id.Set.empty
+(* let global_vars_set_constant_type env = function *)
+(*   | NonPolymorphicType t -> global_vars_set env t *)
+(*   | PolymorphicArity (ctx,_) -> *)
+(*       Context.fold_rel_context *)
+(*         (fold_rel_declaration *)
+(* 	  (fun t c -> Id.Set.union (global_vars_set env t) c)) *)
+(*       ctx ~init:Id.Set.empty *)
 
 let record_aux env s1 s2 =
   let v =
@@ -137,7 +147,7 @@ let record_aux env s1 s2 =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
+let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -152,12 +162,14 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
-        let ids_typ = global_vars_set_constant_type env typ in
+        let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
             let vars = global_vars_set env (Opaqueproof.force_proof lc) in
+            (* we force so that cst are added to the env immediately after *)
+            ignore(Future.join univs);
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
@@ -174,38 +186,50 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
+  let tps = 
+    match proj with
+    | None -> Cemitcodes.from_val (compile_constant_body env def)
+    | Some pb ->
+      Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
+  in
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_body_code = Cemitcodes.from_val (compile_constant_body env def);
-    const_constraints = cst;
+    const_proj = proj;
+    const_body_code = tps;
+    const_polymorphic = poly;
+    const_universes = univs;
     const_inline_code = inline_code }
 
+
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =
-  build_constant_declaration kn env (infer_declaration env ce)
+  build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+
+let translate_local_assum env t =
+  let j = infer env t in
+  let t = Typeops.assumption_of_judgment env j in
+    t
 
 let translate_recipe env kn r =
-  let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
-  build_constant_declaration kn env (def,typ,cst,inline_code,hyps)
+  build_constant_declaration kn env (Cooking.cook_constant env r)
 
 let translate_local_def env id centry =
-  let def,typ,cst,inline_code,ctx =
-    infer_declaration env (DefinitionEntry centry) in
-  let typ = type_of_constant_type env typ in
-  def, typ, cst
+  let def,typ,proj,poly,univs,inline_code,ctx =
+    infer_declaration env None (DefinitionEntry centry) in
+  def, typ, univs
 
 (* Insertion of inductive types. *)