Ensure statically that declarations built by Term_typing are direct.

This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.

8 files changed, 106 insertions, 111 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d879f4ee95..9b6e37251f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -155,8 +155,8 @@ let abstract_constant_body c (hyps, subst) =
 type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
-type result = {
-  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index ffd4e51ffc..b022e2ac09 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -17,8 +17,8 @@ type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cook
 
 type inline = bool
 
-type result = {
-  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
@@ -27,7 +27,7 @@ type result = {
   cook_context : Constr.named_context option;
 }
 
-val cook_constant : hcons:bool -> recipe -> result
+val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result
 val cook_constr : Opaqueproof.cooking_info -> constr -> constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 57059300b8..423a416ca4 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -100,6 +100,10 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
+let force_direct = function
+| Direct (_, cu) -> Future.force cu
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index d47c0bbb3c..8b6e8a1c8f 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,6 +39,7 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+val force_direct : opaque -> (constr * Univ.ContextSet.t)
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 36f1515a8c..a5d8a480ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,27 +228,10 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
-type seff_env =
-  [ `Nothing
-  (* The proof term and its universes.
-     Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.ContextSet.t ]
-
-let get_opaque_body env cbo =
-  match cbo.const_body with
-  | Undef _ -> assert false
-  | Primitive _ -> assert false
-  | Def _ -> `Nothing
-  | OpaqueDef opaque ->
-      `Opaque
-        (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
-         Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : Opaqueproof.opaque Declarations.constant_body;
-  seff_env : seff_env;
+  seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body;
   seff_role : Entries.side_effect_role;
 }
 
@@ -288,39 +271,38 @@ type private_constants = SideEffects.t
 let side_effects_of_private_constants l =
   List.rev (SideEffects.repr l)
 
+(* Only used to push in an Environ.env. *)
+let lift_constant c =
+  let body = match c.const_body with
+  | OpaqueDef _ -> Undef None
+  | Def _ | Undef _ | Primitive _ as body -> body
+  in
+  { c with const_body = body }
+
+let map_constant f c =
+  let body = match c.const_body with
+  | OpaqueDef o -> OpaqueDef (f o)
+  | Def _ | Undef _ | Primitive _ as body -> body
+  in
+  { c with const_body = body }
+
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
     try ignore(Environ.lookup_constant eff.seff_constant env); env
-    with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+    with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
   in
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
 let concat_private = SideEffects.concat
 
-let private_constant env role cst =
-  (** The constant must be the last entry of the safe environment *)
-  let () = match env.revstruct with
-  | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
-  | _ -> assert false
-  in
-  let from_env = CEphemeron.create env.revstruct in
-  let cbo = Environ.lookup_constant cst env.env in
-  let eff = {
-    from_env = from_env;
-    seff_constant = cst;
-    seff_body = cbo;
-    seff_env = get_opaque_body env.env cbo;
-    seff_role = role;
-  } in
-  SideEffects.add eff empty_private_constants
-
 let universes_of_private eff =
   let fold acc eff =
-    let acc = match eff.seff_env with
-    | `Nothing -> acc
-    | `Opaque (_, ctx) -> ctx :: acc
+    let acc = match eff.seff_body.const_body with
+    | Def _ -> acc
+    | OpaqueDef (_, ctx) -> ctx :: acc
+    | Primitive _ | Undef _ -> assert false
     in
     match eff.seff_body.const_universes with
     | Monomorphic ctx -> ctx :: acc
@@ -565,7 +547,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -598,7 +579,7 @@ let inline_side_effects env body side_eff =
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
   let filter e =
-    let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+    let cb = (e.seff_constant, e.seff_body) in
     try ignore (Environ.lookup_constant e.seff_constant env); None
     with Not_found -> Some (cb, e.from_env)
   in
@@ -612,10 +593,10 @@ let inline_side_effects env body side_eff =
   else
     (** Second step: compute the lifts and substitutions to apply *)
     let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
-    let fold (subst, var, ctx, args) (c, cb, b) =
-      let (b, opaque) = match cb.const_body, b with
-      | Def b, _ -> (Mod_subst.force_constr b, false)
-      | OpaqueDef _, `Opaque (b,_) -> (b, true)
+    let fold (subst, var, ctx, args) (c, cb) =
+      let (b, opaque) = match cb.const_body with
+      | Def b -> (Mod_subst.force_constr b, false)
+      | OpaqueDef (b, _) -> (b, true)
       | _ -> assert false
       in
       match cb.const_universes with
@@ -701,7 +682,8 @@ let check_signatures curmb sl =
   | Some (n, _) -> n
 
 
-let constant_entry_of_side_effect cb u =
+let constant_entry_of_side_effect eff =
+  let cb = eff.seff_body in
   let open Entries in
   let univs =
     match cb.const_universes with
@@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u =
       Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
-    match cb.const_body, u with
-    | OpaqueDef _, `Opaque (b, c) -> b, c
-    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    match cb.const_body with
+    | OpaqueDef (b, c) -> b, c
+    | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
     const_entry_body = Future.from_val (pt, ());
@@ -724,18 +706,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
-let turn_direct orig =
-  let cb = orig.seff_body in
-  if Declareops.is_opaque cb then
-    let p = match orig.seff_env with
-    | `Opaque (b, c) -> (b, c)
-    | _ -> assert false
-    in
-    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
-    let cb = { cb with const_body } in
-    { orig with seff_body = cb }
-  else orig
-
 let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
@@ -756,13 +726,14 @@ let export_side_effects mb env c =
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
         let { seff_constant = kn; seff_body = cb ; _ } = eff in
-        let env = Environ.add_constant kn cb env in
+        let env = Environ.add_constant kn (lift_constant cb) env in
         match cb.const_universes with
         | Polymorphic _ -> env
         | Monomorphic ctx ->
-          let ctx = match eff.seff_env with
-          | `Nothing -> ctx
-          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          let ctx = match eff.seff_body.const_body with
+          | Def _ -> ctx
+          | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx
+          | Undef _ | Primitive _ -> assert false
           in
           Environ.push_context_set ~strict:true ctx env
       in
@@ -771,35 +742,39 @@ let export_side_effects mb env c =
         | [] -> List.rev acc, ce
         | eff :: rest ->
           if Int.equal sl 0 then
-           let env, cb =
-              let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
-               let ce = constant_entry_of_side_effect ocb u in
+            let env, cb =
+              let kn = eff.seff_constant in
+               let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let eff = { eff with
-                seff_body = cb;
-                seff_env = `Nothing;
-               } in
+               let cb = map_constant Future.force cb in
+               let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
             translate_seff 0 rest (cb :: acc) env
           else
-           let cb = turn_direct eff in
-           let env = push_seff env cb in
-           let ecb = export_eff cb in
+           let env = push_seff env eff in
+           let ecb = export_eff eff in
            translate_seff (sl - 1) rest (ecb :: acc) env
      in
        translate_seff trusted seff [] env
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+  let bodies = List.map map exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
+let add_recipe ~in_section l r senv =
+  let kn = Constant.make2 senv.modpath l in
+  let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let senv = add_constant_aux ~in_section senv (kn, cb) in
+  kn, senv
+
 let add_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
-  let senv =
     let cb = 
       match decl with
       | ConstantEntry (EffectEntry, ce) ->
@@ -811,9 +786,9 @@ let add_constant ?role ~in_section l decl senv =
         Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
       | ConstantEntry (PureEntry, ce) ->
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
-      | GlobalRecipe r ->
-        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
-        if in_section then cb else Declareops.hcons_const_body cb in
+    in
+  let senv =
+    let cb = map_constant Opaqueproof.create cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -824,7 +799,16 @@ let add_constant ?role ~in_section l decl senv =
   in
   let eff = match role with
   | None -> empty_private_constants
-  | Some role -> private_constant senv role kn
+  | Some role ->
+    let cb = map_constant Future.force cb in
+    let from_env = CEphemeron.create senv.revstruct in
+    let eff = {
+      from_env = from_env;
+      seff_constant = kn;
+      seff_body = cb;
+      seff_role = role;
+    } in
+    SideEffects.add eff empty_private_constants
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b9a68663d3..36ca3d8c47 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -88,7 +88,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -103,6 +102,9 @@ val add_constant :
   ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * private_constants) safe_transformer
 
+val add_recipe :
+  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
+
 (** Adding an inductive type *)
 
 val add_mind :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index faa4411e92..9e33b431fc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -154,7 +154,7 @@ the polymorphic case
           let c = Constr.hcons j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
-      let def = OpaqueDef (Opaqueproof.create proofterm) in
+      let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
@@ -207,7 +207,7 @@ the polymorphic case
       in
       let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
-	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+        if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration _kn env result =
+let build_constant_declaration ~force ~iter env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -271,11 +271,8 @@ let build_constant_declaration _kn env result =
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let vars =
-              global_vars_set env
-                (Opaqueproof.force_proof (opaque_tables env) lc) in
-            (* we force so that cst are added to the env immediately after *)
-            ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
+            let (lc, _) = force lc in
+            let vars = global_vars_set env lc in
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
@@ -296,11 +293,14 @@ let build_constant_declaration _kn env result =
             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 env typ in
-              let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
-              check declared inferred) lc) in
+          let kont c =
+            let ids_typ = global_vars_set env typ in
+            let ids_def = global_vars_set env c in
+            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            check declared inferred
+          in
+          OpaqueDef (iter kont lc)
+  in
   let univs = result.cook_universes in
   let tps = 
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
@@ -318,8 +318,10 @@ let build_constant_declaration _kn env result =
 
 (*s Global and local constant declaration. *)
 
-let translate_constant mb env kn ce =
-  build_constant_declaration kn env
+let translate_constant mb env _kn ce =
+  let force cu = Future.force cu in
+  let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
+  build_constant_declaration ~force ~iter env
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
@@ -327,8 +329,10 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     j.uj_val, t
 
-let translate_recipe ~hcons env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
+let translate_recipe ~hcons env _kn r =
+  let force o = Opaqueproof.force_direct o in
+  let iter k o = Opaqueproof.iter_direct_opaque k o in
+  build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r)
 
 let translate_local_def env _id centry =
   let open Cooking in
@@ -351,8 +355,7 @@ let translate_local_def env _id centry =
     | Def _ -> ()
     | OpaqueDef lc ->
        let ids_typ = global_vars_set env typ in
-       let ids_def = global_vars_set env
-         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let ids_def = global_vars_set env (fst (Future.force lc)) in
        record_aux env ids_typ ids_def
   end;
   let () = match decl.cook_universes with
@@ -362,8 +365,7 @@ let translate_local_def env _id centry =
   let c = match decl.cook_body with
   | Def c -> Mod_subst.force_constr c
   | OpaqueDef o ->
-    let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
-    let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+    let (p, cst) = Future.force o in
     (** Let definitions are ensured to have no extra constraints coming from
         the body by virtue of the typing of [Entries.section_def_entry]. *)
     let () = assert (Univ.ContextSet.is_empty cst) in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 01b69b2b66..a046d26ea9 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,14 +33,16 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
-    Opaqueproof.opaque constant_body
+    Opaqueproof.proofterm constant_body
 
 val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Cooking.result
+  'a constant_entry -> Opaqueproof.proofterm Cooking.result
 
 val build_constant_declaration :
-  Constant.t -> env -> Cooking.result -> Opaqueproof.opaque constant_body
+  force:('a -> constr * 'b) ->
+  iter:((constr -> unit) -> 'a -> 'a) ->
+  env -> 'a Cooking.result -> 'a constant_body