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.
---
 tactics/declare.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 61321cd605..719430e71c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -259,17 +259,17 @@ let define_constant ~side_effect ~name cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = Entries.DefinitionEntry (cast_proof_entry de) in
-      export, ConstantEntry (PureEntry, cd), false
+      export, ConstantEntry cd, false
     else
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
       let de = cast_opaque_proof_entry de in
-      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false
+      [], OpaqueEntry de, false
   | ParameterEntry e ->
-    [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+    [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
   | PrimitiveEntry e ->
-    [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
+    [], ConstantEntry (Entries.PrimitiveEntry e), false
   in
   let kn, eff = Global.add_constant ~side_effect name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
-- 
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.
---
 tactics/abstract.ml   |  8 +++++---
 tactics/declare.ml    | 45 +++++++++++++++++++++++++++++++++------------
 tactics/declare.mli   |  2 +-
 tactics/ind_tables.ml | 13 +++++++++++--
 4 files changed, 50 insertions(+), 18 deletions(-)

(limited to 'tactics')

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index edeb27ab88..03ab0a1c13 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -149,9 +149,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     let (_, info) = CErrors.push src in
     iraise (e, info)
   in
+  let body, effs = Future.force const.Declare.proof_entry_body in
+  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+  let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in
+  let cd = { const with Declare.proof_entry_opaque = opaque } in
   let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -172,8 +175,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
-  let effs = Evd.concat_side_effects eff
-      (snd (Future.force const.Declare.proof_entry_body)) in
+  let effs = Evd.concat_side_effects eff effs in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 719430e71c..c9da88988f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -204,7 +204,11 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-let cast_opaque_proof_entry e =
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
+let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry) =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -218,8 +222,15 @@ let cast_opaque_proof_entry e =
         Id.Set.empty, Id.Set.empty
       else
         let ids_typ = global_vars_set env typ in
-        let (pf, _), eff = Future.force e.proof_entry_body in
-        let env = Safe_typing.push_private_constants env eff in
+        let pf, env = match entry with
+        | PureEntry ->
+          let (pf, _), () = Future.force e.proof_entry_body in
+          pf, env
+        | EffectEntry ->
+          let (pf, _), eff = Future.force e.proof_entry_body in
+          let env = Safe_typing.push_private_constants env eff in
+          pf, env
+        in
         let vars = global_vars_set env pf in
         ids_typ, vars
     in
@@ -247,7 +258,7 @@ let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-let define_constant ~side_effect ~name cd =
+let define_constant ~name cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let export, decl, unsafe = match cd with
   | DefinitionEntry de ->
@@ -264,34 +275,44 @@ let define_constant ~side_effect ~name cd =
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
-      let de = cast_opaque_proof_entry de in
+      let de = cast_opaque_proof_entry EffectEntry de in
       [], OpaqueEntry de, false
   | ParameterEntry e ->
     [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
   | PrimitiveEntry e ->
     [], ConstantEntry (Entries.PrimitiveEntry e), false
   in
-  let kn, eff = Global.add_constant ~side_effect name decl in
+  let kn = Global.add_constant name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
-  kn, eff, export
+  kn, export
 
 let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
   let () = check_exists name in
-  let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in
+  let kn, export = define_constant ~name cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd =
-  let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in
-  let () = assert (CList.is_empty export) in
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+  let kn, eff =
+    let de =
+      if not de.proof_entry_opaque then
+        let body, () = Future.force de.proof_entry_body in
+        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+        DefinitionEff (cast_proof_entry de)
+      else
+        let de = cast_opaque_proof_entry PureEntry de in
+        OpaqueEff de
+    in
+    Global.add_private_constant name de
+  in
   let () = register_constant kn kind local in
   let seff_roles = match role with
   | None -> Cmap.empty
   | Some r -> Cmap.singleton kn r
   in
-  let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in
+  let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
 (** Declaration of section variables and local definitions *)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index f4bfdb1547..a6c1374a77 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -78,7 +78,7 @@ val declare_private_constant
   -> ?local:import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
-  -> Evd.side_effects constant_entry
+  -> unit proof_entry
   -> Constant.t * Evd.side_effects
 
 (** Since transparent constants' side effects are globally declared, we
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 54393dce00..3f824a94bf 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,8 +124,17 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = Declare.definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
+  let entry = {
+    Declare.proof_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty), ());
+    proof_entry_secctx = None;
+    proof_entry_type = None;
+    proof_entry_universes = univs;
+    proof_entry_opaque = false;
+    proof_entry_inline_code = false;
+    proof_entry_feedback = None;
+  } in
+  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id
-- 
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.

---
 tactics/declare.ml | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index c9da88988f..63a93d3dc3 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -204,11 +204,11 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
-| PureEntry : unit effect_entry
+type ('a, 'b) effect_entry =
+| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
+| PureEntry : (unit, Constr.constr) effect_entry
 
-let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry) =
+let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -238,12 +238,24 @@ let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry
     Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
   | Some hyps -> hyps
   in
+  let (body, univs : b * _) = match entry with
+  | PureEntry ->
+    let (body, uctx), () = Future.force e.proof_entry_body in
+    let univs = match e.proof_entry_universes with
+    | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx')
+    | Polymorphic_entry _ ->
+      assert (Univ.ContextSet.is_empty uctx);
+      e.proof_entry_universes
+    in
+    body, univs
+  | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
+  in
   {
-    opaque_entry_body = e.proof_entry_body;
+    opaque_entry_body = body;
     opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
-    opaque_entry_universes = e.proof_entry_universes;
+    opaque_entry_universes = univs;
   }
 
 let get_roles export eff =
-- 
cgit v1.2.3


From 593e784250eca0f38479109395a5fbc605f2c3c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Oct 2019 16:00:00 +0200
Subject: Simplify future forcing in Declare.

---
 tactics/declare.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 63a93d3dc3..7d32f1a7e8 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -310,8 +310,6 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let kn, eff =
     let de =
       if not de.proof_entry_opaque then
-        let body, () = Future.force de.proof_entry_body in
-        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
         DefinitionEff (cast_proof_entry de)
       else
         let de = cast_opaque_proof_entry PureEntry de in
-- 
cgit v1.2.3