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.
---
 kernel/entries.ml      |  7 +++++--
 kernel/safe_typing.ml  | 10 +++++-----
 kernel/term_typing.ml  | 30 +++++++++++++++++++-----------
 kernel/term_typing.mli |  2 +-
 4 files changed, 30 insertions(+), 19 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3fa25c142a..a1ccbdbc1b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -64,6 +64,10 @@ type mutual_inductive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
+type constant_universes_entry =
+  | Monomorphic_const_entry of Univ.universe_context
+  | Polymorphic_const_entry of Univ.universe_context
+
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -71,8 +75,7 @@ type 'a definition_entry = {
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
-  const_entry_polymorphic : bool;
-  const_entry_universes   : Univ.universe_context;
+  const_entry_universes   : constant_universes_entry;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ed4c7d57ad..074122b03f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,12 +382,12 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = 
-    match Term_typing.translate_local_def senv.revstruct senv.env id de with
-    | c, typ, Monomorphic_const ctx -> c, typ, ctx
-    | _, _, Polymorphic_const _ -> assert false
+  let open Entries in
+  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let poly = match de.Entries.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
   in
-  let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cf82d54ec1..9102234657 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,8 +251,8 @@ let infer_declaration ~trust env kn dcl =
       delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
-		       const_entry_polymorphic = false} as c) ->
-      let env = push_context ~strict:true c.const_entry_universes env in
+		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
+      let env = push_context ~strict:true univs env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -271,7 +271,7 @@ let infer_declaration ~trust env kn dcl =
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None,
-      (Monomorphic_const c.const_entry_universes),
+      (Monomorphic_const univs),
       c.const_entry_inline_code, c.const_entry_secctx
 
   (** Other definitions have to be processed immediately. *)
@@ -279,18 +279,22 @@ let infer_declaration ~trust env kn dcl =
       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, ctx), side_eff = Future.join body in
-      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+      let poly, univs = match c.const_entry_universes with
+      | Monomorphic_const_entry univs -> false, univs
+      | Polymorphic_const_entry univs -> true, univs
+      in
+      let univsctx = Univ.ContextSet.of_context univs in
       let body, ctx, _ = inline_side_effects env body
         (Univ.ContextSet.union univsctx ctx) side_eff in
-      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
-      let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
+      let env = push_context_set ~strict:(not poly) ctx env in
+      let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs =
         abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
       in      
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+           if not poly then (* Old-style polymorphism *)
              make_polymorphic_if_constant_for_ind env j
            else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
         | Some t ->
@@ -461,11 +465,12 @@ let translate_constant mb env kn ce =
     (infer_declaration ~trust:mb env (Some kn) ce)
 
 let constant_entry_of_side_effect cb u =
-  let poly, univs =
+  let univs =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, ctx
+    | Monomorphic_const uctx ->
+      Monomorphic_const_entry uctx
     | Polymorphic_const auctx -> 
-      true, Univ.AUContext.repr auctx
+      Polymorphic_const_entry (Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
@@ -478,7 +483,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_feedback = None;
     const_entry_type =
       (match cb.const_type with RegularArity t -> Some t | _ -> None);
-    const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -592,6 +596,10 @@ let translate_local_def mb env id centry =
            env ids_def ids_typ context_ids in
        record_aux env ids_typ ids_def expr
   end;
+  let univs = match univs with
+  | Monomorphic_const ctx -> ctx
+  | Polymorphic_const _ -> assert false
+  in
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 77d126074f..29c9918373 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -15,7 +15,7 @@ open Entries
 type side_effects
 
 val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
-  constant_def * types * constant_universes
+  constant_def * types * Univ.universe_context
 
 val translate_local_assum : env -> types -> types
 
-- 
cgit v1.2.3


From 9961577dfbb93f0b691c355ba99822665def037f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jul 2017 17:00:48 +0200
Subject: Using a record type for Cooking.result.

---
 kernel/cooking.ml     | 22 +++++++++++-----
 kernel/cooking.mli    | 11 +++++---
 kernel/term_typing.ml | 71 ++++++++++++++++++++++++++++++++++++---------------
 3 files changed, 74 insertions(+), 30 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 95822fac68..63614e20f7 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -151,9 +151,14 @@ let abstract_constant_body =
 type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
-type result =
-  constant_def * constant_type * projection_body option * 
-    constant_universes * inline * Context.Named.t option
+type result = {
+  cook_body : constant_def;
+  cook_type : constant_type;
+  cook_proj : projection_body option;
+  cook_universes : constant_universes;
+  cook_inline : inline;
+  cook_context : Context.Named.t option;
+}
 
 let on_body ml hy f = function
   | Undef _ as x -> x
@@ -254,9 +259,14 @@ let cook_constant ~hcons env { from = cb; info } =
     | Polymorphic_const auctx -> 
       Polymorphic_const (AUContext.union abs_ctx auctx)
   in
-    (body, typ, Option.map projection cb.const_proj, 
-     univs, cb.const_inline_code, 
-     Some const_hyps)
+  {
+    cook_body = body;
+    cook_type = typ;
+    cook_proj = Option.map projection cb.const_proj;
+    cook_universes = univs;
+    cook_inline = cb.const_inline_code;
+    cook_context = Some const_hyps;
+  }
 
 (* let cook_constant_key = Profile.declare_profile "cook_constant" *)
 (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 79a028d760..f386fd9362 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -16,9 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
-type result =
-  constant_def * constant_type * projection_body option * 
-    constant_universes * inline * Context.Named.t option
+type result = {
+  cook_body : constant_def;
+  cook_type : constant_type;
+  cook_proj : projection_body option;
+  cook_universes : constant_universes;
+  cook_inline : inline;
+  cook_context : Context.Named.t option;
+}
 
 val cook_constant : hcons:bool -> env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9102234657..c809e4791c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -243,7 +243,14 @@ let infer_declaration ~trust env kn dcl =
       in
       let c = Typeops.assumption_of_judgment env j in
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
-	Undef nl, RegularArity t, None, univs, false, ctx
+      {
+        Cooking.cook_body = Undef nl;
+        cook_type = RegularArity t;
+        cook_proj = None;
+        cook_universes = univs;
+        cook_inline = false;
+        cook_context = ctx;
+      }
 
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
       so we delay the typing and hash consing of its body.
@@ -270,9 +277,14 @@ let infer_declaration ~trust env kn dcl =
           feedback_completion_typecheck feedback_id;
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, RegularArity typ, None,
-      (Monomorphic_const univs),
-      c.const_entry_inline_code, c.const_entry_secctx
+      {
+        Cooking.cook_body = def;
+        cook_type = RegularArity typ;
+        cook_proj = None;
+        cook_universes = Monomorphic_const univs;
+        cook_inline = c.const_entry_inline_code;
+        cook_context = c.const_entry_secctx;
+      }
 
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
@@ -308,7 +320,14 @@ let infer_declaration ~trust env kn dcl =
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
-	def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_proj = None;
+        cook_universes = univs;
+        cook_inline = c.const_entry_inline_code;
+        cook_context = c.const_entry_secctx;
+      }
 
   | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
     let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
@@ -328,8 +347,14 @@ let infer_declaration ~trust env kn dcl =
         Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
     in
     let term, typ = pb.proj_eta in
-      Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
-      univs, false, None
+    {
+      Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
+      cook_type = RegularArity typ;
+      cook_proj = Some pb;
+      cook_universes = univs;
+      cook_inline = false;
+      cook_context = None;
+    }
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
@@ -353,7 +378,9 @@ let record_aux env s_ty s_bo suggested_expr =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
+let build_constant_declaration kn env result =
+  let open Cooking in
+  let typ = result.cook_type in
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -380,7 +407,8 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
   (* 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
-    match ctx with
+    let def = result.cook_body in
+    match result.cook_context with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
@@ -423,9 +451,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
+  let univs = result.cook_universes in
   let tps = 
     let res =
-      match proj with
+      match result.cook_proj with
       | None -> compile_constant_body env univs def
       | Some pb ->
 	(* The compilation of primitive projections is a bit tricky, because
@@ -438,10 +467,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
 	  { const_hyps = hyps;
 	    const_body = def;
 	    const_type = typ;
-	    const_proj = proj;
+	    const_proj = result.cook_proj;
 	    const_body_code = None;
 	    const_universes = univs;
-	    const_inline_code = inline_code;
+	    const_inline_code = result.cook_inline;
 	    const_typing_flags = Environ.typing_flags env;
 	    }
 	in
@@ -452,10 +481,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_proj = proj;
+    const_proj = result.cook_proj;
     const_body_code = tps;
     const_universes = univs;
-    const_inline_code = inline_code;
+    const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
 (*s Global and local constant declaration. *)
@@ -579,11 +608,11 @@ let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
 let translate_local_def mb env id centry =
-  let def,typ,proj,univs,inline_code,ctx =
-    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
-  let typ = type_of_constant_type env typ in
-  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
-    match def with
+  let open Cooking in
+  let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
+  let typ = type_of_constant_type env decl.cook_type in
+  if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
+    match decl.cook_body with
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
@@ -596,11 +625,11 @@ let translate_local_def mb env id centry =
            env ids_def ids_typ context_ids in
        record_aux env ids_typ ids_def expr
   end;
-  let univs = match univs with
+  let univs = match decl.cook_universes with
   | Monomorphic_const ctx -> ctx
   | Polymorphic_const _ -> assert false
   in
-  def, typ, univs
+  decl.cook_body, typ, univs
 
 (* Insertion of inductive types. *)
 
-- 
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.
---
 kernel/safe_typing.ml  | 22 +++++++++++++++-------
 kernel/safe_typing.mli |  9 ++++++---
 kernel/term_typing.ml  | 45 ++++++++++++++++++++++++++++++---------------
 kernel/term_typing.mli | 18 +++++++++++-------
 4 files changed, 62 insertions(+), 32 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 074122b03f..6dbc223952 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -383,7 +383,8 @@ let safe_push_named d env =
 
 let push_named_def (id,de) senv =
   let open Entries in
-  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let trust = Term_typing.SideEffects senv.revstruct in
+  let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in
   let poly = match de.Entries.const_entry_universes with
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
@@ -492,12 +493,17 @@ let add_field ((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 : bool -> private_constants effect_entry
+| PureEntry : unit effect_entry
+
 type global_declaration =
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+                  (* bool: export private constants *)
+  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constants Entries.constant_entry * private_constant_role
+  constant * unit Entries.constant_entry * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -526,10 +532,10 @@ let add_constant dir l decl senv =
   let no_section = DirPath.is_empty dir in
   let seff_to_export, decl =
     match decl with
-    | ConstantEntry (true, ce) ->
+    | ConstantEntry (EffectEntry true, ce) ->
         let exports, ce =
           Term_typing.export_side_effects senv.revstruct senv.env ce in
-        exports, ConstantEntry (false, ce)
+        exports, ConstantEntry (PureEntry, ce)
     | _ -> [], decl
   in
   let senv =
@@ -538,8 +544,10 @@ let add_constant dir l decl senv =
   let senv =
     let cb = 
       match decl with
-      | ConstantEntry (export_seff,ce) ->
-        Term_typing.translate_constant senv.revstruct senv.env kn ce
+      | ConstantEntry (EffectEntry _, ce) ->
+        Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) 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 senv.env kn r in
         if no_section then Declareops.hcons_const_body cb else cb in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5bb8ceb1a5..2a454400fd 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -94,13 +94,16 @@ val push_named_def :
 
 (** Insertion of global axioms or definitions *)
 
+type 'a effect_entry =
+| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *)
+| PureEntry : unit effect_entry
+
 type global_declaration =
-                  (* bool: export private constants *)
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constants Entries.constant_entry * private_constant_role
+  constant * unit Entries.constant_entry * private_constant_role
 
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c809e4791c..03bd8426fe 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -77,6 +77,10 @@ end
 
 type side_effects = SideEffects.t
 
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
 let uniq_seff_rev = SideEffects.repr
 let uniq_seff l = List.rev (SideEffects.repr l)
 
@@ -232,7 +236,7 @@ let abstract_constant_universes abstract uctx =
     let sbst, auctx = Univ.abstract_universes uctx in
     sbst, Polymorphic_const auctx
 
-let infer_declaration ~trust env kn dcl =
+let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context ~strict:(not poly) uctx env in
@@ -264,15 +268,22 @@ let infer_declaration ~trust env kn dcl =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
-          let body, uctx, signatures =
-            inline_side_effects env body uctx side_eff in
-          let valid_signatures = check_signatures trust signatures in
-	  let env = push_context_set uctx env in
-          let j =
+          let j, uctx = match trust with
+          | Pure ->
+            let env = push_context_set uctx env in
+            let j = infer env body in
+            let _ = judge_of_cast env j DEFAULTcast tyj in
+            j, uctx
+          | SideEffects trust ->
+            let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in
+            let valid_signatures = check_signatures trust signatures in
+            let env = push_context_set uctx env in
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
             let j = infer env body in
-            unzip ectx j in
-          let _ = judge_of_cast env j DEFAULTcast tyj in
+            let j = unzip ectx j in
+            let _ = judge_of_cast env j DEFAULTcast tyj in
+            j, uctx
+          in
           let c = hcons_constr j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
@@ -296,8 +307,11 @@ let infer_declaration ~trust env kn dcl =
       | Polymorphic_const_entry univs -> true, univs
       in
       let univsctx = Univ.ContextSet.of_context univs in
-      let body, ctx, _ = inline_side_effects env body
-        (Univ.ContextSet.union univsctx ctx) side_eff in
+      let ctx = Univ.ContextSet.union univsctx ctx in
+      let body, ctx, _ = match trust with
+      | Pure -> body, ctx, []
+      | SideEffects _ -> inline_side_effects env body ctx side_eff
+      in
       let env = push_context_set ~strict:(not poly) ctx env in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs =
@@ -507,7 +521,7 @@ let constant_entry_of_side_effect cb u =
     | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
-    const_entry_body = Future.from_val (pt, empty_seff);
+    const_entry_body = Future.from_val (pt, ());
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type =
@@ -530,17 +544,18 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects constant_entry * side_effect_role
+  constant * constant_body * unit constant_entry * side_effect_role
 
 let export_side_effects mb env ce =
   match ce with
-  | ParameterEntry _ | ProjectionEntry _ -> [], ce
+  | ParameterEntry e -> [], ParameterEntry e
+  | ProjectionEntry e -> [], ProjectionEntry e
   | DefinitionEntry c ->
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
         const_entry_body = Future.chain ~pure:true body
-          (fun (b_ctx, _) -> b_ctx, empty_seff) } in
+          (fun (b_ctx, _) -> b_ctx, ()) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
         with Not_found -> true in 
@@ -580,7 +595,7 @@ let export_side_effects mb env ce =
            let env, cbs =
              List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
                let ce = constant_entry_of_side_effect ocb u in
-               let cb = translate_constant mb env kn ce in
+               let cb = translate_constant Pure env kn ce in
                (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
              (env,[]) cbs in
            translate_seff sl rest (cbs @ acc) env
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 29c9918373..082ed7ed0d 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,7 +14,11 @@ open Entries
 
 type side_effects
 
-val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
+val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
   constant_def * types * Univ.universe_context
 
 val translate_local_assum : env -> types -> types
@@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-  structure_body -> env -> constant -> side_effects constant_entry ->
+  'a trust -> env -> constant -> 'a constant_entry ->
     constant_body
 
 type side_effect_role =
@@ -51,7 +55,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects constant_entry * side_effect_role
+  constant * constant_body * unit constant_entry * side_effect_role
   
 (* Given a constant entry containing side effects it exports them (either
  * by re-checking them or trusting them).  Returns the constant bodies to
@@ -59,10 +63,10 @@ type exported_side_effect =
  * needs to be translated as usual after this step. *)
 val export_side_effects :
   structure_body -> env -> side_effects constant_entry ->
-    exported_side_effect list * side_effects constant_entry
+    exported_side_effect list * unit constant_entry
 
 val constant_entry_of_side_effect :
-  constant_body -> seff_env -> side_effects constant_entry
+  constant_body -> seff_env -> unit constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -71,8 +75,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:structure_body -> env -> constant option -> 
-  side_effects constant_entry -> Cooking.result
+val infer_declaration : trust:'a trust -> env -> constant option -> 
+  'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
-- 
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.
---
 kernel/safe_typing.ml  | 26 +++++++++++---------------
 kernel/safe_typing.mli |  8 ++++++--
 2 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6dbc223952..ccd6e9cf97 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -494,11 +494,10 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type 'a effect_entry =
-| EffectEntry : bool -> private_constants effect_entry
+| EffectEntry : private_constants effect_entry
 | PureEntry : unit effect_entry
 
 type global_declaration =
-                  (* bool: export private constants *)
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
@@ -527,24 +526,21 @@ let add_constant_aux no_section senv (kn, cb) =
   in
   senv''
 
+let export_private_constants ~in_section ce senv =
+  let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
+  let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in
+  let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in
+  let no_section = not in_section in
+  let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+  (ce, exported), senv
+
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let no_section = DirPath.is_empty dir in
-  let seff_to_export, decl =
-    match decl with
-    | ConstantEntry (EffectEntry true, ce) ->
-        let exports, ce =
-          Term_typing.export_side_effects senv.revstruct senv.env ce in
-        exports, ConstantEntry (PureEntry, ce)
-    | _ -> [], decl
-  in
-  let senv =
-    List.fold_left (add_constant_aux no_section) senv
-      (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
   let senv =
     let cb = 
       match decl with
-      | ConstantEntry (EffectEntry _, ce) ->
+      | ConstantEntry (EffectEntry, ce) ->
         Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce
       | ConstantEntry (PureEntry, ce) ->
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
@@ -552,7 +548,7 @@ let add_constant dir l decl senv =
         let cb = Term_typing.translate_recipe senv.env kn r in
         if no_section then Declareops.hcons_const_body cb else cb in
     add_constant_aux no_section senv (kn, cb) in
-  (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
+  kn, senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2a454400fd..7152261078 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -95,7 +95,7 @@ val push_named_def :
 (** Insertion of global axioms or definitions *)
 
 type 'a effect_entry =
-| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *)
+| EffectEntry : private_constants effect_entry
 | PureEntry : unit effect_entry
 
 type global_declaration =
@@ -105,11 +105,15 @@ type global_declaration =
 type exported_private_constant = 
   constant * unit Entries.constant_entry * private_constant_role
 
+val export_private_constants : in_section:bool ->
+  private_constants Entries.constant_entry ->
+  (unit Entries.constant_entry * exported_private_constant list) safe_transformer
+
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
 val add_constant :
   DirPath.t -> Label.t -> global_declaration ->
-    (constant * exported_private_constant list) safe_transformer
+    constant safe_transformer
 
 (** Adding an inductive type *)
 
-- 
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.
---
 kernel/safe_typing.ml  | 6 +++---
 kernel/safe_typing.mli | 2 +-
 kernel/term_typing.ml  | 6 +++---
 kernel/term_typing.mli | 5 +----
 4 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ccd6e9cf97..04051f2e23 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -502,7 +502,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * unit Entries.constant_entry * private_constant_role
+  constant * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -528,8 +528,8 @@ let add_constant_aux no_section senv (kn, cb) =
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
-  let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in
-  let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in
+  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let no_section = not in_section in
   let senv = List.fold_left (add_constant_aux no_section) senv bodies in
   (ce, exported), senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7152261078..148fdca678 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -103,7 +103,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * unit Entries.constant_entry * private_constant_role
+  constant * private_constant_role
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.constant_entry ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 03bd8426fe..23c5b6f58e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -544,7 +544,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * unit constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
 
 let export_side_effects mb env ce =
   match ce with
@@ -596,7 +596,7 @@ let export_side_effects mb env ce =
              List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
                let ce = constant_entry_of_side_effect ocb u in
                let cb = translate_constant Pure env kn ce in
-               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) 
              (env,[]) cbs in
            translate_seff sl rest (cbs @ acc) env
         | Some sl, cbs :: rest ->
@@ -604,7 +604,7 @@ let export_side_effects mb env ce =
            let cbs = List.map turn_direct cbs in
            let env = List.fold_left push_seff env cbs in
            let ecbs = List.map (fun (kn,cb,u,r) ->
-             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+             kn, cb, r) cbs in
            translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
      in
        translate_seff trusted seff [] env
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 082ed7ed0d..5914c4a954 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -55,7 +55,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * unit constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
   
 (* Given a constant entry containing side effects it exports them (either
  * by re-checking them or trusting them).  Returns the constant bodies to
@@ -65,9 +65,6 @@ val export_side_effects :
   structure_body -> env -> side_effects constant_entry ->
     exported_side_effect list * unit constant_entry
 
-val constant_entry_of_side_effect :
-  constant_body -> seff_env -> unit constant_entry
-
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
 
-- 
cgit v1.2.3


From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 18 Jul 2017 18:16:43 +0200
Subject: Statically ensuring that inlined entries out of the kernel have no
 effects.

This was an easy to prove property that I somehow overlooked.
---
 kernel/safe_typing.mli | 2 +-
 kernel/term_typing.ml  | 2 +-
 kernel/term_typing.mli | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 148fdca678..752fdd793e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
   Environ.env -> Constr.constr -> private_constants -> Constr.constr
 val inline_private_constants_in_definition_entry :
-  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+  Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
 val universes_of_private : private_constants -> Univ.universe_context_set list
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 23c5b6f58e..ed53df01f1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -654,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), empty_seff);
+      (body, ctx'), ());
 }
 
 let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 5914c4a954..24153343e7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr
     redexes. *)
 
 val inline_entry_side_effects :
-  env -> side_effects definition_entry -> side_effects definition_entry
+  env -> side_effects definition_entry -> unit definition_entry
 (** Same as {!inline_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
-- 
cgit v1.2.3


From 906b48ff401f22be6059a6cdde8723b858102690 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Jul 2017 14:05:52 +0200
Subject: Avoiding a variable shadowing in the kernel.

This ought to ease the understanding of the code.
---
 kernel/term_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ed53df01f1..43c099712a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -274,9 +274,9 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
             let j = infer env body in
             let _ = judge_of_cast env j DEFAULTcast tyj in
             j, uctx
-          | SideEffects trust ->
+          | SideEffects mb ->
             let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in
-            let valid_signatures = check_signatures trust signatures in
+            let valid_signatures = check_signatures mb signatures in
             let env = push_context_set uctx env in
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
             let j = infer env body in
-- 
cgit v1.2.3