From f22205ee06f9170a74dc8cefba2b42deeaeb246b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 16:04:52 +0200
Subject: Make explicit the delayed computation of opaque bodies in
 Term_typing.

We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.

This commit is mostly moving code around, this should be 1:1 semantically.
---
 kernel/safe_typing.ml  |  28 ++++++----
 kernel/term_typing.ml  | 142 +++++++++++++++++++++++--------------------------
 kernel/term_typing.mli |  14 ++---
 3 files changed, 94 insertions(+), 90 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fc55720583..4dbc009324 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -767,22 +767,24 @@ let export_side_effects mb env (b_ctx, eff) =
               let kn = eff.seff_constant in
                let ce = constant_entry_of_side_effect eff in
                let open Entries in
-               let open Term_typing in
                let cb = match ce with
                | DefinitionEff ce ->
-                Term_typing.translate_constant Pure env kn (DefinitionEntry ce)
+                Term_typing.translate_constant env kn (DefinitionEntry ce)
                | OpaqueEff ce ->
-                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
-                Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce)
+                Term_typing.translate_constant env kn (OpaqueEntry ce)
                in
-              let map cu =
-                let (c, u) = Future.force cu in
+              let map ctx = match ce with
+              | OpaqueEff e ->
+                let body = Future.force e.Entries.opaque_entry_body in
+                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+                let (c, u) = Term_typing.check_delayed handle ctx body in
                 let () = match u with
                 | Opaqueproof.PrivateMonomorphic ctx
                 | Opaqueproof.PrivatePolymorphic (_, ctx) ->
                   assert (Univ.ContextSet.is_empty ctx)
                 in
                 c
+              | _ -> assert false
               in
                let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
@@ -824,15 +826,23 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
-      | ConstantEntry (EffectEntry, ce) ->
+      | ConstantEntry (EffectEntry, Entries.OpaqueEntry e) ->
         let handle env body eff =
           let body, uctx, signatures = inline_side_effects env body eff in
           let trusted = check_signatures senv.revstruct signatures in
           body, uctx, trusted
         in
-        Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
+        let cb = Term_typing.translate_constant senv.env kn (Entries.OpaqueEntry e) in
+        let ctx = match cb.const_body with
+        | OpaqueDef ctx -> ctx
+        | _ -> assert false
+        in
+        let map pf = Term_typing.check_delayed handle ctx pf in
+        let pf = Future.chain e.Entries.opaque_entry_body map in
+        { cb with const_body = OpaqueDef pf }
       | ConstantEntry (PureEntry, ce) ->
-        Term_typing.translate_constant Term_typing.Pure senv.env kn ce
+        let cb = Term_typing.translate_constant senv.env kn ce in
+        map_constant (fun _ -> assert false) cb
     in
   let senv =
     let senv, cb, delayed_cst = match cb.const_body with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f70b2960cf..1e0db8026f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -29,10 +29,6 @@ module NamedDecl = Context.Named.Declaration
 type 'a effect_handler =
   env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
-type _ trust =
-| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
-
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
     let open Context.Rel.Declaration in
@@ -64,7 +60,11 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       Feedback.feedback ~id:state_id Feedback.Complete)
 
-let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
+type typing_context =
+| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option
+| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
+
+let infer_declaration (type a) env (dcl : a constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -118,25 +118,10 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   | OpaqueEntry ({ opaque_entry_type = typ;
                        opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
       let env = push_context_set ~strict:true univs env in
-      let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
-      let proofterm =
-        Future.chain body begin fun ((body,uctx),side_eff) ->
-          (* don't redeclare universes which are declared for the type *)
-          let uctx = Univ.ContextSet.diff uctx univs in
-          let SideEffects handle = trust in
-          let (body, uctx', valid_signatures) = handle env body side_eff in
-          let uctx = Univ.ContextSet.union uctx uctx' in
-          let env = push_context_set uctx env in
-          let body,env,ectx = skip_trusted_seff valid_signatures body env in
-          let j = Typeops.infer env body in
-          let j = unzip ectx j in
-          let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
-          let c = j.uj_val in
-          feedback_completion_typecheck feedback_id;
-          c, Opaqueproof.PrivateMonomorphic uctx
-      end in
-      let def = OpaqueDef proofterm in
+      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef context in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
@@ -150,26 +135,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 
   | OpaqueEntry ({ opaque_entry_type = typ;
                        opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
-      let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
       let env = push_context ~strict:false uctx env in
       let tj = Typeops.infer_type env typ in
       let sbst, auctx = Univ.abstract_universes nas uctx in
       let usubst = Univ.make_instance_subst sbst in
-      let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
-        let SideEffects handle = trust in
-        let body, ctx', _ = handle env body side_eff in
-        let ctx = Univ.ContextSet.union ctx ctx' in
-        (** [ctx] must contain local universes, such that it has no impact
-            on the rest of the graph (up to transitivity). *)
-        let env = push_subgraph ctx env in
-        let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
-        let j = Typeops.infer env body in
-        let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
-        let def = Vars.subst_univs_level_constr usubst j.uj_val in
-        let () = feedback_completion_typecheck feedback_id in
-        def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
-      end in
-      let def = OpaqueDef proofterm in
+      let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef context in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
       {
         Cooking.cook_body = def;
@@ -184,7 +156,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      let Pure = trust in
       let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry ctx ->
         let env = push_context_set ~strict:true ctx env in
@@ -218,25 +189,29 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
+let check_section_variables env declared_set typ body =
+  let ids_typ = global_vars_set env typ in
+  let ids_def = global_vars_set env body in
+  let inferred_set = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
+  if not (Id.Set.subset inferred_set declared_set) then
+    let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
+    let n = List.length l in
+    let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
+    let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
+    let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
+    user_err Pp.(prlist str
+        ["The following section "; (String.plural n "variable"); " ";
+        (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
+        missing_vars ++ str "." ++ fnl () ++ fnl () ++
+        str "You can either update your proof to not depend on " ++ missing_vars ++
+        str ", or you can update your Proof line from" ++ fnl () ++
+        str "Proof using " ++ declared_vars ++ fnl () ++
+        str "to" ++ fnl () ++
+        str "Proof using " ++ inferred_vars)
+
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
-  let check declared_set inferred_set =
-    if not (Id.Set.subset inferred_set declared_set) then
-      let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
-      let n = List.length l in
-      let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
-      let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
-      let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
-      user_err Pp.(prlist str
-         ["The following section "; (String.plural n "variable"); " ";
-          (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
-         missing_vars ++ str "." ++ fnl () ++ fnl () ++
-         str "You can either update your proof to not depend on " ++ missing_vars ++
-         str ", or you can update your Proof line from" ++ fnl () ++
-         str "Proof using " ++ declared_vars ++ fnl () ++
-         str "to" ++ fnl () ++
-         str "Proof using " ++ inferred_vars) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
@@ -265,22 +240,10 @@ let build_constant_declaration env result =
         (* We use the declared set and chain a check of correctness *)
         declared,
         match def with
-        | Undef _ | Primitive _ as x -> x (* nothing to check *)
+        | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set env typ in
-            let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
-            check declared inferred;
-            x
-        | OpaqueDef lc -> (* In this case we can postpone the check *)
-          let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
-          let kont c =
-            let ids_typ = global_vars_set env typ in
-            let ids_def = global_vars_set env c in
-            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
-            check declared inferred
-          in
-          OpaqueDef (iter kont lc)
+          let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
+          x
   in
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
@@ -297,11 +260,42 @@ let build_constant_declaration env result =
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
+let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with
+| MonoTyCtx (env, tyj, univs, declared, feedback_id) ->
+  let ((body, uctx), side_eff) = body in
+  (* don't redeclare universes which are declared for the type *)
+  let uctx = Univ.ContextSet.diff uctx univs in
+  let (body, uctx', valid_signatures) = handle env body side_eff in
+  let uctx = Univ.ContextSet.union uctx uctx' in
+  let env = push_context_set uctx env in
+  let body,env,ectx = skip_trusted_seff valid_signatures body env in
+  let j = Typeops.infer env body in
+  let j = unzip ectx j in
+  let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
+  let c = j.uj_val in
+  let () = check_section_variables env declared tyj.utj_val body in
+  feedback_completion_typecheck feedback_id;
+  c, Opaqueproof.PrivateMonomorphic uctx
+| PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) ->
+  let ((body, ctx), side_eff) = body in
+  let body, ctx', _ = handle env body side_eff in
+  let ctx = Univ.ContextSet.union ctx ctx' in
+  (** [ctx] must contain local universes, such that it has no impact
+      on the rest of the graph (up to transitivity). *)
+  let env = push_subgraph ctx env in
+  let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
+  let j = Typeops.infer env body in
+  let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+  let () = check_section_variables env declared tj.utj_val body in
+  let def = Vars.subst_univs_level_constr usubst j.uj_val in
+  let () = feedback_completion_typecheck feedback_id in
+  def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
+
 (*s Global and local constant declaration. *)
 
-let translate_constant mb env _kn ce =
+let translate_constant env _kn ce =
   build_constant_declaration env
-    (infer_declaration ~trust:mb env ce)
+    (infer_declaration env ce)
 
 let translate_local_assum env t =
   let j = Typeops.infer env t in
@@ -336,7 +330,7 @@ let translate_local_def env _id centry =
     const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
     const_entry_inline_code = false;
   } in
-  let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
+  let decl = infer_declaration env (DefinitionEntry centry) in
   let typ = decl.cook_type in
   let () = match decl.cook_universes with
   | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ef01ece185..f82312245b 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,9 +22,7 @@ open Entries
 type 'a effect_handler =
   env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
-type _ trust =
-| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
+type typing_context
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * Sorts.relevance * types
@@ -32,15 +30,17 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  'a trust -> env -> Constant.t -> 'a constant_entry ->
-    Opaqueproof.proofterm constant_body
+  env -> Constant.t -> 'a constant_entry ->
+    typing_context constant_body
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
+val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes)
+
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Opaqueproof.proofterm Cooking.result
+val infer_declaration : env ->
+  'a constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
-- 
cgit v1.2.3


From 1f2a3fe97be66fd3201b9c98e5744953d4149b91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:04:25 +0200
Subject: Cleaning up the previous code by ensuring statically invariants on
 opaque proofs.

We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
---
 kernel/entries.ml      |  9 +++---
 kernel/safe_typing.ml  | 48 ++++++++++-------------------
 kernel/safe_typing.mli |  3 +-
 kernel/term_typing.ml  | 84 +++++++++++++++++++++++++-------------------------
 kernel/term_typing.mli | 10 ++++--
 5 files changed, 71 insertions(+), 83 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 1e6bc14935..8c4bd16ae3 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -102,11 +102,10 @@ type 'a const_entry_body = 'a proof_output Future.computation
 (** Dummy wrapper type discriminable from unit *)
 type 'a seff_wrap = { seff_wrap : 'a }
 
-type _ constant_entry =
-  | DefinitionEntry : definition_entry -> unit constant_entry
-  | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry
-  | ParameterEntry : parameter_entry -> unit constant_entry
-  | PrimitiveEntry : primitive_entry -> unit constant_entry
+type constant_entry =
+  | DefinitionEntry : definition_entry -> constant_entry
+  | ParameterEntry : parameter_entry -> constant_entry
+  | PrimitiveEntry : primitive_entry -> constant_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4dbc009324..43aafac809 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -299,13 +299,6 @@ let lift_constant c =
   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 =
@@ -585,7 +578,8 @@ type 'a effect_entry =
 | PureEntry : unit effect_entry
 
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
@@ -765,17 +759,14 @@ let export_side_effects mb env (b_ctx, eff) =
           if Int.equal sl 0 then
             let env, cb =
               let kn = eff.seff_constant in
-               let ce = constant_entry_of_side_effect eff in
-               let open Entries in
-               let cb = match ce with
-               | DefinitionEff ce ->
+              let ce = constant_entry_of_side_effect eff in
+              let open Entries in
+              let cb = match ce with
+              | DefinitionEff ce ->
                 Term_typing.translate_constant env kn (DefinitionEntry ce)
-               | OpaqueEff ce ->
-                Term_typing.translate_constant env kn (OpaqueEntry ce)
-               in
-              let map ctx = match ce with
-              | OpaqueEff e ->
-                let body = Future.force e.Entries.opaque_entry_body in
+              | OpaqueEff ce ->
+                let cb, ctx = Term_typing.translate_opaque env kn ce in
+                let body = Future.force ce.Entries.opaque_entry_body in
                 let handle _env c () = (c, Univ.ContextSet.empty, 0) in
                 let (c, u) = Term_typing.check_delayed handle ctx body in
                 let () = match u with
@@ -783,10 +774,8 @@ let export_side_effects mb env (b_ctx, eff) =
                 | Opaqueproof.PrivatePolymorphic (_, ctx) ->
                   assert (Univ.ContextSet.is_empty ctx)
                 in
-                c
-              | _ -> assert false
+                { cb with const_body = OpaqueDef c }
               in
-               let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
@@ -826,23 +815,18 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
-      | ConstantEntry (EffectEntry, Entries.OpaqueEntry e) ->
+      | OpaqueEntry ce ->
         let handle env body eff =
           let body, uctx, signatures = inline_side_effects env body eff in
           let trusted = check_signatures senv.revstruct signatures in
           body, uctx, trusted
         in
-        let cb = Term_typing.translate_constant senv.env kn (Entries.OpaqueEntry e) in
-        let ctx = match cb.const_body with
-        | OpaqueDef ctx -> ctx
-        | _ -> assert false
-        in
+        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
         let map pf = Term_typing.check_delayed handle ctx pf in
-        let pf = Future.chain e.Entries.opaque_entry_body map in
+        let pf = Future.chain ce.Entries.opaque_entry_body map in
         { cb with const_body = OpaqueDef pf }
-      | ConstantEntry (PureEntry, ce) ->
-        let cb = Term_typing.translate_constant senv.env kn ce in
-        map_constant (fun _ -> assert false) cb
+      | ConstantEntry ce ->
+        Term_typing.translate_constant senv.env kn ce
     in
   let senv =
     let senv, cb, delayed_cst = match cb.const_body with
@@ -870,7 +854,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
 
   let senv =
     match decl with
-    | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
+    | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) ->
       if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b55293f1c..6e5c9c55ae 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -78,7 +78,8 @@ type 'a effect_entry =
 | PureEntry : unit effect_entry
 
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1e0db8026f..f85b3db413 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -64,7 +64,7 @@ type typing_context =
 | MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option
 | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
 
-let infer_declaration (type a) env (dcl : a constant_entry) =
+let infer_declaration env (dcl : constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -112,47 +112,6 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_relevance = Sorts.Relevant;
       }
 
-  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
-      let env = push_context_set ~strict:true univs env in
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let tyj = Typeops.infer_type env typ in
-      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      {
-        Cooking.cook_body = def;
-        cook_type = tyj.utj_val;
-        cook_universes = Monomorphic univs;
-        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Similar case for polymorphic entries. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let env = push_context ~strict:false uctx env in
-      let tj = Typeops.infer_type env typ in
-      let sbst, auctx = Univ.abstract_universes nas uctx in
-      let usubst = Univ.make_instance_subst sbst in
-      let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-      {
-        Cooking.cook_body = def;
-        cook_type = typ;
-        cook_universes = Polymorphic auctx;
-        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
@@ -189,6 +148,43 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
+(** Definition is opaque (Qed), so we delay the typing of its body. *)
+let infer_opaque env = function
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
+      let env = push_context_set ~strict:true univs env in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let tyj = Typeops.infer_type env typ in
+      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      {
+        Cooking.cook_body = def;
+        cook_type = tyj.utj_val;
+        cook_universes = Monomorphic univs;
+        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let env = push_context ~strict:false uctx env in
+      let tj = Typeops.infer_type env typ in
+      let sbst, auctx = Univ.abstract_universes nas uctx in
+      let usubst = Univ.make_instance_subst sbst in
+      let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_universes = Polymorphic auctx;
+        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
 let check_section_variables env declared_set typ body =
   let ids_typ = global_vars_set env typ in
   let ids_def = global_vars_set env body in
@@ -297,6 +293,10 @@ let translate_constant env _kn ce =
   build_constant_declaration env
     (infer_declaration env ce)
 
+let translate_opaque env _kn ce =
+  let def, ctx = infer_opaque env ce in
+  build_constant_declaration env def, ctx
+
 let translate_local_assum env t =
   let j = Typeops.infer env t in
   let t = Typeops.assumption_of_judgment env j in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index f82312245b..c9f6d66e36 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,8 +30,12 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  env -> Constant.t -> 'a constant_entry ->
-    typing_context constant_body
+  env -> Constant.t -> constant_entry ->
+    'a constant_body
+
+val translate_opaque :
+  env -> Constant.t -> 'a opaque_entry ->
+    unit constant_body * typing_context
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
@@ -40,7 +44,7 @@ val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (C
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : env ->
-  'a constant_entry -> typing_context Cooking.result
+  constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
-- 
cgit v1.2.3


From 60596e870bcb481673fd3108fc1b6478df5a2621 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:37:42 +0200
Subject: Split the function used to declare side-effects from the standard
 one.

This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
---
 kernel/entries.ml      |  3 ---
 kernel/safe_typing.ml  | 40 ++++++++++++++++++++++++++++------------
 kernel/safe_typing.mli | 17 ++++++++++-------
 3 files changed, 38 insertions(+), 22 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8c4bd16ae3..046ea86872 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,9 +99,6 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-(** Dummy wrapper type discriminable from unit *)
-type 'a seff_wrap = { seff_wrap : 'a }
-
 type constant_entry =
   | DefinitionEntry : definition_entry -> constant_entry
   | ParameterEntry : parameter_entry -> constant_entry
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 43aafac809..d2a7703648 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -572,11 +572,6 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
 
 let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
-(** Insertion of constants and parameters in environment *)
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
 | ConstantEntry : Entries.constant_entry -> global_declaration
 | OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
@@ -811,9 +806,9 @@ let export_private_constants ce senv =
   let senv = List.fold_left add_constant_aux senv bodies in
   (ce, exported), senv
 
-let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
+let add_constant l decl senv =
   let kn = Constant.make2 senv.modpath l in
-    let cb = 
+    let cb =
       match decl with
       | OpaqueEntry ce ->
         let handle env body eff =
@@ -859,10 +854,31 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  let eff : a = match side_effect with
-  | PureEntry -> ()
-  | EffectEntry ->
-    let body, univs = match cb.const_body with
+  kn, senv
+
+let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
+  let kn = Constant.make2 senv.modpath l in
+    let cb =
+      match decl with
+      | OpaqueEff ce ->
+        let handle _env body () = body, Univ.ContextSet.empty, 0 in
+        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
+        let map pf = Term_typing.check_delayed handle ctx pf in
+        let pf = Future.chain ce.Entries.opaque_entry_body map in
+        { cb with const_body = OpaqueDef pf }
+      | DefinitionEff ce ->
+        Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
+    in
+  let senv, cb, body = match cb.const_body with
+  | Def _ as const_body -> senv, { cb with const_body }, const_body
+  | OpaqueDef c ->
+    let senv, o = push_opaque_proof c senv in
+    senv, { cb with const_body = OpaqueDef o }, cb.const_body
+  | Undef _ | Primitive _ -> assert false
+  in
+  let senv = add_constant_aux senv (kn, cb) in
+  let eff =
+    let body, univs = match body with
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
     | OpaqueDef o ->
@@ -884,7 +900,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
       seff_constant = kn;
       seff_body = cb;
     } in
-    { Entries.seff_wrap = SideEffects.add eff empty_private_constants }
+    SideEffects.add eff empty_private_constants
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e5c9c55ae..c60e7e893f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,24 +73,27 @@ val is_joined_environment : safe_environment -> bool
 
 (** Insertion of global axioms or definitions *)
 
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
 | ConstantEntry : Entries.constant_entry -> global_declaration
 | OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+
 type exported_private_constant = Constant.t
 
 val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a certificate of its validity *)
+(** returns the main constant *)
 val add_constant :
-  side_effect:'a effect_entry -> Label.t -> global_declaration ->
-    (Constant.t * 'a) safe_transformer
+  Label.t -> global_declaration -> Constant.t safe_transformer
+
+(** Similar to add_constant but also returns a certificate *)
+val add_private_constant :
+  Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer
 
 (** Adding an inductive type *)
 
-- 
cgit v1.2.3


From 221db99a7809cad8f613baa2038fbbd8fb27a691 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 6 Jul 2019 17:30:58 +0200
Subject: Ensure that side-effect declarations reaching the kernel are forced.

---
 kernel/safe_typing.ml  | 72 +++++++++++++++++++++-----------------------------
 kernel/safe_typing.mli |  2 +-
 2 files changed, 31 insertions(+), 43 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d2a7703648..659f9cd1c4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -693,7 +693,7 @@ let check_signatures curmb sl =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 let constant_entry_of_side_effect eff =
   let cb = eff.seff_body in
@@ -712,7 +712,7 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEff {
-    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_body = p;
     opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
@@ -730,6 +730,25 @@ let constant_entry_of_side_effect eff =
 let export_eff eff =
   (eff.seff_constant, eff.seff_body)
 
+let is_empty_private = function
+| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx
+| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx
+
+let empty_private univs = match univs with
+| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
+
+(* Special function to call when the body of an opaque definition is provided.
+  It performs the type-checking of the body immediately. *)
+let translate_direct_opaque env kn ce =
+  let cb, ctx = Term_typing.translate_opaque env kn ce in
+  let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in
+  let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+  let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in
+  (* No constraints can be generated, we set it empty everywhere *)
+  let () = assert (is_empty_private u) in
+  { cb with const_body = OpaqueDef c }
+
 let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
@@ -760,16 +779,7 @@ let export_side_effects mb env (b_ctx, eff) =
               | DefinitionEff ce ->
                 Term_typing.translate_constant env kn (DefinitionEntry ce)
               | OpaqueEff ce ->
-                let cb, ctx = Term_typing.translate_opaque env kn ce in
-                let body = Future.force ce.Entries.opaque_entry_body in
-                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
-                let (c, u) = Term_typing.check_delayed handle ctx body in
-                let () = match u with
-                | Opaqueproof.PrivateMonomorphic ctx
-                | Opaqueproof.PrivatePolymorphic (_, ctx) ->
-                  assert (Univ.ContextSet.is_empty ctx)
-                in
-                { cb with const_body = OpaqueDef c }
+                translate_direct_opaque env kn ce
               in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
@@ -791,10 +801,7 @@ let export_private_constants ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
-    let local = match c.const_universes with
-    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
-    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
-    in
+    let local = empty_private c.const_universes in
     let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
     senv, (kn, { c with const_body = OpaqueDef o })
   | Def _ | Undef _ | Primitive _ as body ->
@@ -861,39 +868,20 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
     let cb =
       match decl with
       | OpaqueEff ce ->
-        let handle _env body () = body, Univ.ContextSet.empty, 0 in
-        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
-        let map pf = Term_typing.check_delayed handle ctx pf in
-        let pf = Future.chain ce.Entries.opaque_entry_body map in
-        { cb with const_body = OpaqueDef pf }
+        translate_direct_opaque senv.env kn ce
       | DefinitionEff ce ->
         Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
     in
-  let senv, cb, body = match cb.const_body with
-  | Def _ as const_body -> senv, { cb with const_body }, const_body
+  let senv, dcb = match cb.const_body with
+  | Def _ as const_body -> senv, { cb with const_body }
   | OpaqueDef c ->
-    let senv, o = push_opaque_proof c senv in
-    senv, { cb with const_body = OpaqueDef o }, cb.const_body
+    let local = empty_private cb.const_universes in
+    let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in
+    senv, { cb with const_body = OpaqueDef o }
   | Undef _ | Primitive _ -> assert false
   in
-  let senv = add_constant_aux senv (kn, cb) in
+  let senv = add_constant_aux senv (kn, dcb) in
   let eff =
-    let body, univs = match body with
-    | (Primitive _ | Undef _) -> assert false
-    | Def c -> (Def c, cb.const_universes)
-    | OpaqueDef o ->
-      let (b, delayed) = Future.force o in
-      match cb.const_universes, delayed with
-      | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
-        OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) ->
-        (* Upper layers enforce that there are no internal constraints *)
-        let () = assert (Univ.ContextSet.is_empty ctx) in
-        OpaqueDef b, Polymorphic auctx
-      | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
-        assert false
-    in
-    let cb = { cb with const_body = body; const_universes = univs } in
     let from_env = CEphemeron.create senv.revstruct in
     let eff = {
       from_env = from_env;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c60e7e893f..ec86495db8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ type global_declaration =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 type exported_private_constant = Constant.t
 
-- 
cgit v1.2.3