Adapt universe polymorphic branch to new handling of futures for delayed proofs.

13 files changed, 61 insertions, 45 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3d580d713..5fa01e5db 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -213,7 +213,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs = Future.from_val (UContext.union abs_ctx (Future.force cb.const_universes)) in
+  let univs = UContext.union abs_ctx cb.const_universes in
     (body, typ, Option.map projection cb.const_proj, 
      cb.const_polymorphic, univs, cb.const_inline_code, 
      Some const_hyps)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 9c7344f89..b8dfe63d3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -61,7 +61,7 @@ type constant_def =
   | Def of constr Mod_subst.substituted
   | OpaqueDef of Opaqueproof.opaque
 
-type constant_universes = Univ.universe_context Future.computation
+type constant_universes = Univ.universe_context
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 8806bba45..4363ec442 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -43,11 +43,20 @@ let body_of_constant cb = match cb.const_body with
   | OpaqueDef o -> Some (Opaqueproof.force_proof o)
 
 let constraints_of_constant cb = Univ.Constraint.union 
-  (Univ.UContext.constraints (Future.force cb.const_universes))
+  (Univ.UContext.constraints cb.const_universes)
   (match cb.const_body with
   | Undef _ -> Univ.empty_constraint
   | Def c -> Univ.empty_constraint
-  | OpaqueDef o -> Opaqueproof.force_constraints o)
+  | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o))
+
+let universes_of_constant cb = 
+  match cb.const_body with
+  | Undef _ | Def _ -> cb.const_universes
+  | OpaqueDef o -> Opaqueproof.force_constraints o
+
+let universes_of_polymorphic_constant cb = 
+  if cb.const_polymorphic then universes_of_constant cb
+  else Univ.UContext.empty
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -139,11 +148,7 @@ let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_universes =
-      if Future.is_val cb.const_universes then
-        Future.from_val
-          (Univ.hcons_universe_context (Future.force cb.const_universes))
-      else (* FIXME: Why not? *) cb.const_universes }
+    const_universes = Univ.hcons_universe_context cb.const_universes }
 
 (** {6 Inductive types } *)
 
@@ -265,7 +270,6 @@ let hcons_mind mib =
 (** {6 Stm machinery } *)
 
 let join_constant_body cb =
-  ignore(Future.join cb.const_universes);
   match cb.const_body with
   | OpaqueDef o -> Opaqueproof.join_opaque o
   | _ -> ()
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 9f5197668..6c43bffa9 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -30,6 +30,12 @@ val constant_has_body : constant_body -> bool
 
 val body_of_constant : constant_body -> Term.constr option
 val constraints_of_constant : constant_body -> Univ.constraints
+val universes_of_constant : constant_body -> Univ.universe_context
+
+(** Return the universe context, in case the definition is polymorphic, otherwise
+    the context is empty. *)
+
+val universes_of_polymorphic_constant : constant_body -> Univ.universe_context
 
 val is_opaque : constant_body -> bool
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index a161a6fcb..001a1e4b3 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -63,7 +63,7 @@ type definition_entry = {
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
-  const_entry_universes   : Univ.universe_context Future.computation;
+  const_entry_universes   : Univ.universe_context;
   const_entry_proj        : projection option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ede655702..dd4237b22 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -207,7 +207,7 @@ let add_constant kn cb env =
   add_constant_key kn cb (no_link_info ()) env
 
 let universes_of cb = 
-  Future.force cb.const_universes
+  cb.const_universes
 
 let universes_and_subst_of cb u =
   let univs = universes_of cb in
@@ -234,7 +234,7 @@ let constant_type env (kn,u) =
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then Future.force cb.const_universes
+    if cb.const_polymorphic then cb.const_universes
     else Univ.UContext.empty
 
 type const_evaluation_result = NoBody | Opaque | IsProj
@@ -283,7 +283,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in
+      let subst = Univ.make_universe_subst u cb.const_universes in
 	map_regular_arity (subst_univs_constr subst) cb.const_type
     else cb.const_type
 
@@ -293,7 +293,7 @@ let constant_value_in env (kn,u) =
     | Def l_body -> 
       let b = Mod_subst.force_constr l_body in
 	if cb.const_polymorphic then
-	  let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in
+	  let subst = Univ.make_universe_subst u cb.const_universes in
 	    subst_univs_constr subst b
 	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b20fe9671..cab3276c3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,8 +72,8 @@ let rec check_with_def env struc (idl,c) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let env' = Environ.add_constraints 
-	(Univ.UContext.constraints (Future.force cb.const_universes)) env' in
+      let ccst = Declareops.constraints_of_constant cb in
+      let env' = Environ.add_constraints ccst env' in
       let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j = Typeops.infer env' c in
@@ -84,10 +84,9 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	| Def cs ->
 	  let cst = Reduction.infer_conv env' (Environ.universes env') c
 	    (Mod_subst.force_constr cs) in
-	  let cst = 
+	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
 	    if cb.const_polymorphic then cst
-	    else (*FIXME MS: computed above *)
-	      (Univ.UContext.constraints (Future.force cb.const_universes)) +++ cst 
+	    else ccst +++ cst 
 	  in
             c, cst
       in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 673b12b2c..73d5c5db2 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 type cooking_info = { 
   modlist : work_list; 
   abstract : Context.named_context in_universe_context } 
-type proofterm = (constr * Univ.constraints) Future.computation
+type proofterm = (constr * Univ.universe_context) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
@@ -99,7 +99,7 @@ let force_constraints = function
   | NoIndirect(_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       match !get_univ dp i with
-      | None -> Univ.Constraint.empty
+      | None -> Univ.UContext.empty
       | Some u -> Future.force u
 
 let get_constraints = function
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 71f491754..fee15e405 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -19,7 +19,7 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.constraints) Future.computation
+type proofterm = (constr * Univ.universe_context) Future.computation
 type opaque
 
 (** From a [proofterm] to some [opaque]. *)
@@ -31,9 +31,9 @@ val turn_indirect : opaque -> opaque
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor configured below. *)
 val force_proof : opaque -> constr
-val force_constraints : opaque -> Univ.constraints
+val force_constraints : opaque -> Univ.universe_context
 val get_proof : opaque -> Term.constr Future.computation
-val get_constraints : opaque -> Univ.constraints Future.computation option
+val get_constraints : opaque -> Univ.universe_context Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -66,7 +66,7 @@ val set_indirect_creator :
 val set_indirect_opaque_accessor :
   (DirPath.t -> int -> Term.constr Future.computation) -> unit
 val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.constraints Future.computation option) -> unit
+  (DirPath.t -> int -> Univ.universe_context Future.computation option) -> unit
 val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
 val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
 val reset_indirect_creator : unit -> unit
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 35577239b..deabf1bcf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -298,11 +298,11 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let c = match c with
-    | Def c -> Mod_subst.force_constr c
-    | OpaqueDef o -> Opaqueproof.force_proof o
+  let c, univs = match c with
+    | Def c -> Mod_subst.force_constr c, univs
+    | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o
     | _ -> assert false in
-  let senv' = push_context (Future.join de.Entries.const_entry_universes) senv in
+  let senv' = push_context univs senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
@@ -332,9 +332,15 @@ let globalize_constant_universes cb =
   if cb.const_polymorphic then
     Now Univ.Constraint.empty
   else
-    (match Future.peek_val cb.const_universes with
-    | Some c -> Now (Univ.UContext.constraints c)
-    | None -> Later (Future.chain ~pure:true cb.const_universes Univ.UContext.constraints))
+    match cb.const_body with
+    | (Undef _ | Def _) -> Now (Univ.UContext.constraints cb.const_universes)
+    | OpaqueDef lc ->
+      match Opaqueproof.get_constraints lc with
+      | None -> Now (Univ.UContext.constraints cb.const_universes)
+      | Some fc ->
+        match Future.peek_val fc with
+        | None -> Later (Future.chain ~pure:true fc Univ.UContext.constraints)
+        | Some c -> Now (Univ.UContext.constraints c)
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
@@ -751,7 +757,7 @@ let import lib cst vodigest senv =
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.add_constraints mb.mod_constraints senv.env in
-  let env = Environ.add_constraints cst env in
+  let env = Environ.push_context cst env in
   (mp, lib.comp_natsymbs),
   { senv with
     env =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ad2148ead..5b5457c38 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -140,7 +140,7 @@ val export :
     module_path * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
-val import : compiled_library -> Univ.constraints -> vodigest ->
+val import : compiled_library -> Univ.universe_context -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
 (** {6 Safe typing judgments } *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 56e94ba0d..61420d7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -308,7 +308,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let u1 = inductive_instance mind1 in
       let arity1,cst1 = constrained_type_of_inductive env 
 	((mind1,mind1.mind_packets.(i)),u1) in
-      let cst2 = UContext.constraints (Future.force cb2.const_universes) in
+      let cst2 = Declareops.constraints_of_constant cb2 in 
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, arity1, typ2) in
@@ -323,7 +323,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
       let u1 = inductive_instance mind1 in
       let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let cst2 = UContext.constraints (Future.force cb2.const_universes) in
+      let cst2 = Declareops.constraints_of_constant cb2 in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = Constraint.union cst (Constraint.union cst1 cst2) in
       let error = NotConvertibleTypeField (env, ty1, ty2) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 27ab90aa5..780c14a20 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -89,7 +89,7 @@ let handle_side_effects env body side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 		mkLetIn (cname c, b, b_ty, t)
 	    else 
-	      let univs = Future.force cb.const_universes in
+	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
       | OpaqueDef b -> 
           let b = Opaqueproof.force_proof b in
@@ -99,7 +99,7 @@ let handle_side_effects env body side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
 	    else
-	      let univs = Future.force cb.const_universes in
+	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
     in
       List.fold_right fix_body cbl t
@@ -120,10 +120,10 @@ let infer_declaration env kn dcl =
       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, RegularArity t, None, poly, Future.from_val uctx, false, ctx
+      Undef nl, RegularArity t, None, poly, uctx, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true } as c) ->
-      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
+      let env = push_context c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -133,12 +133,13 @@ let infer_declaration env kn dcl =
           let j = hcons_j j in
           let _typ = constrain_type env j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, Univ.empty_constraint) in
+          j.uj_val, Univ.UContext.empty) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes,
+      def, RegularArity typ, None, c.const_entry_polymorphic, 
+	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
   | DefinitionEntry c ->
-      let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *)
+      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
@@ -211,7 +212,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         | 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);
+            ignore(Opaqueproof.force_constraints lc);
             !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;