From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jul 2017 13:38:22 +0200
Subject: More precise type for universe entries.

We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
---
 interp/declare.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 154793a32d..f95d025e42 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -63,8 +63,12 @@ let cache_variable ((sp,_),o) =
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
       let univs = Global.push_named_def (id,de) in
+      let poly = match de.const_entry_universes with
+      | Monomorphic_const_entry _ -> false
+      | Polymorphic_const_entry _ -> true
+      in
       Explicit, de.const_entry_opaque,
-      de.const_entry_polymorphic, univs in
+      poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -237,22 +241,29 @@ let declare_constant_common id cst =
 
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
+  let univs =
+    if poly then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let is_poly de = match de.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
+  in
   let export = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
         export_seff ||
         not de.const_entry_opaque ||
-        de.const_entry_polymorphic ->
+        is_poly de ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
           Safe_typing.empty_private_constants <> seff
-- 
cgit v1.2.3


From 3c6679676c3963b7c3ec7c1eadbf24ae70311408 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 14 Jul 2017 15:43:40 +0200
Subject: More precise type of entries capturing their lack of side-effects.

We sprinkle a few GADTs in the kernel in order to statically ensure that
entries are pure, so that we get stronger invariants.
---
 interp/declare.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index f95d025e42..8cafb5f3a6 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -184,7 +184,7 @@ let discharge_constant ((sp, kn), obj) =
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
   ConstantEntry
-    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+    (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -220,7 +220,7 @@ let declare_constant_common id cst =
   List.iter (fun (c,ce,role) ->
       (* handling of private_constants just exported *)
       let o = inConstant {
-        cst_decl = ConstantEntry (false, ce);
+        cst_decl = ConstantEntry (PureEntry, ce);
         cst_hyps = [] ;
         cst_kind = IsProof Theorem;
         cst_locl = false;
@@ -270,7 +270,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
     | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry (export,cd);
+    cst_decl = ConstantEntry (EffectEntry export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
-- 
cgit v1.2.3


From 3fcf0930874d7200f2503ac7084b1d6669d59540 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Jul 2017 17:46:15 +0200
Subject: Remove a horrendous hack in Declare to retrieve exported
 side-effects.

Instead of relying on a mutable state in the object pushed on the libstack,
we export an API in the kernel that exports the side-effects of a given
entry in the global environment.
---
 interp/declare.ml | 80 ++++++++++++++++++++++++++-----------------------------
 1 file changed, 38 insertions(+), 42 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 8cafb5f3a6..d82b8f2158 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -106,10 +106,7 @@ type constant_obj = {
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
-  mutable cst_exported : Safe_typing.exported_private_constant list;
-  (* mutable: to avoid change the libobject API, since cache_function
-   * does not return an updated object *)
-  mutable cst_was_seff : bool
+  cst_was_seff : bool;
 }
 
 type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
@@ -150,15 +147,13 @@ let cache_constant ((sp,kn), obj) =
   let _,dir,_ = repr_kn kn in
   let kn' =
     if obj.cst_was_seff then begin
-      obj.cst_was_seff <- false;  
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     end else
       let () = check_exists sp in
-      let kn', exported = Global.add_constant dir id obj.cst_decl in
-      obj.cst_exported <- exported;
-      kn' in
+      Global.add_constant dir id obj.cst_decl
+  in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
@@ -179,7 +174,7 @@ let discharge_constant ((sp, kn), obj) =
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
-  Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
+  Some { obj with cst_was_seff = false; cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
@@ -191,14 +186,13 @@ let dummy_constant cst = {
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
-  cst_exported = [];
-  cst_was_seff = cst.cst_was_seff;
+  cst_was_seff = false;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
-  declare_object_full { (default_object "CONSTANT") with
+let (inConstant : constant_obj -> obj) =
+  declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -209,31 +203,14 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
 
+let update_tables c =
+  declare_constant_implicits c;
+  Heads.declare_head (EvalConstRef c);
+  Notation.declare_ref_arguments_scope (ConstRef c)
+
 let declare_constant_common id cst =
-  let update_tables c =
-(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
-    declare_constant_implicits c;
-    Heads.declare_head (EvalConstRef c);
-    Notation.declare_ref_arguments_scope (ConstRef c) in
   let o = inConstant cst in
   let _, kn as oname = add_leaf id o in
-  List.iter (fun (c,ce,role) ->
-      (* handling of private_constants just exported *)
-      let o = inConstant {
-        cst_decl = ConstantEntry (PureEntry, ce);
-        cst_hyps = [] ;
-        cst_kind = IsProof Theorem;
-        cst_locl = false;
-        cst_exported = [];
-        cst_was_seff = true; } in
-      let id = Label.to_id (pi3 (Constant.repr3 c)) in
-      ignore(add_leaf id o);
-      update_tables c;
-      let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
-      match role with
-      | Safe_typing.Subproof -> ()
-      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
-    (outConstant o).cst_exported;
   pull_to_head oname;
   let c = Global.constant_of_delta_kn kn in
   update_tables c;
@@ -258,23 +235,42 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
   in
-  let export = (* We deal with side effects *)
+  let in_section = Lib.sections_are_opened () in
+  let export, decl = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
         export_seff ||
         not de.const_entry_opaque ||
         is_poly de ->
-          let bo = de.const_entry_body in
-          let _, seff = Future.force bo in
-          Safe_typing.empty_private_constants <> seff
-    | _ -> false
+      (** This globally defines the side-effects in the environment. We mark
+          exported constants as being side-effect not to redeclare them at
+          caching time. *)
+      let cd, export = Global.export_private_constants ~in_section cd in
+      export, ConstantEntry (PureEntry, cd)
+    | _ -> [], ConstantEntry (EffectEntry, cd)
+  in
+  let iter_eff (c, cd, role) =
+    let o = inConstant {
+      cst_decl = ConstantEntry (PureEntry, cd);
+      cst_hyps = [] ;
+      cst_kind = IsProof Theorem;
+      cst_locl = false;
+      cst_was_seff = true
+    } in
+    let id = Label.to_id (pi3 (Constant.repr3 c)) in
+    ignore(add_leaf id o);
+    update_tables c;
+    let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
+    match role with
+    | Safe_typing.Subproof -> ()
+    | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
   in
+  let () = List.iter iter_eff export in
   let cst = {
-    cst_decl = ConstantEntry (EffectEntry export,cd);
+    cst_decl = decl;
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
-    cst_exported = [];
     cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
-- 
cgit v1.2.3


From ce830b204ad52f8b3655d2cb4672662120d83101 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Jul 2017 00:05:03 +0200
Subject: Further simplication: do not recreate entries for side-effects.

This is actually useless, the code does not depend on the value of the
entry for side-effects.
---
 interp/declare.ml | 29 ++++++++++++-----------------
 1 file changed, 12 insertions(+), 17 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index d82b8f2158..70f422b514 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -102,11 +102,12 @@ let declare_variable id obj =
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
-  cst_decl : global_declaration;
+  cst_decl : global_declaration option;
+  (** [None] when the declaration is a side-effect and has already been defined
+      in the global environment. *)
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
-  cst_was_seff : bool;
 }
 
 type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
@@ -146,13 +147,14 @@ let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' =
-    if obj.cst_was_seff then begin
+    match obj.cst_decl with
+    | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    end else
+    | Some decl ->
       let () = check_exists sp in
-      Global.add_constant dir id obj.cst_decl
+      Global.add_constant dir id decl
   in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -174,19 +176,14 @@ let discharge_constant ((sp, kn), obj) =
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
-  Some { obj with cst_was_seff = false; cst_hyps = new_hyps; cst_decl = new_decl; }
+  Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = 
-  ConstantEntry
-    (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
-
 let dummy_constant cst = {
-  cst_decl = dummy_constant_entry;
+  cst_decl = None;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
-  cst_was_seff = false;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
@@ -249,13 +246,12 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
       export, ConstantEntry (PureEntry, cd)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
-  let iter_eff (c, cd, role) =
+  let iter_eff (c, role) =
     let o = inConstant {
-      cst_decl = ConstantEntry (PureEntry, cd);
+      cst_decl = None;
       cst_hyps = [] ;
       cst_kind = IsProof Theorem;
       cst_locl = false;
-      cst_was_seff = true
     } in
     let id = Label.to_id (pi3 (Constant.repr3 c)) in
     ignore(add_leaf id o);
@@ -267,11 +263,10 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
   in
   let () = List.iter iter_eff export in
   let cst = {
-    cst_decl = decl;
+    cst_decl = Some decl;
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
-    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
-- 
cgit v1.2.3