From eba0e54f6ecef38b451ef84a978b9ab55699ccf8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Sep 2018 21:02:48 +0200
Subject: Move side-effect typing into Safe_env.

This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.
---
 kernel/term_typing.mli | 42 ++++++++----------------------------------
 1 file changed, 8 insertions(+), 34 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ab25090b00..3dc498ca1c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,53 +14,27 @@ open Environ
 open Declarations
 open Entries
 
-type side_effects
+(** Handlers are used to manage side-effects. The ['a] type stands for the type
+    of side-effects, and it is parametric because they are only defined later
+    on. Handlers inline the provided side-effects into the term, and return
+    the set of additional global constraints that need to be added for the term
+    to be well typed. *)
+type 'a effect_handler =
+  env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
 type _ trust =
 | Pure : unit trust
-| SideEffects : structure_body -> side_effects trust
+| SideEffects : 'a effect_handler -> 'a trust
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * types
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> side_effects proof_output
-
-val inline_side_effects : env -> constr -> side_effects -> constr
-(** Returns the term where side effects have been turned into let-ins or beta
-    redexes. *)
-
-val inline_entry_side_effects :
-  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. *)
-
-val empty_seff : side_effects
-val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects
-val concat_seff : side_effects -> side_effects -> side_effects
-(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
-    [e1] must be more recent than those of [e2]. *)
-val uniq_seff : side_effects -> side_eff list
-(** Return the list of individual side-effects in the order of their
-    creation. *)
-
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-type exported_side_effect = 
-  Constant.t * 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
- * be pushed in the safe_env by safe typing.  The main constant entry
- * needs to be translated as usual after this step. *)
-val export_side_effects :
-  structure_body -> env -> side_effects definition_entry ->
-    exported_side_effect list * unit definition_entry
-
 val translate_mind :
   env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-- 
cgit v1.2.3


From d24125537710202cc15a8d6a7352072bd6c77cba Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Sep 2018 13:22:01 +0200
Subject: Explicitly merge contexts in side-effect universe handling.

Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
---
 kernel/term_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 3dc498ca1c..faf434c142 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -20,7 +20,7 @@ open Entries
     the set of additional global constraints that need to be added for the term
     to be well typed. *)
 type 'a effect_handler =
-  env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
+  env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
 type _ trust =
 | Pure : unit trust
-- 
cgit v1.2.3