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.

5 files changed, 65 insertions, 35 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index f95d025e4..8cafb5f3a 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;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 074122b03..6dbc22395 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 5bb8ceb1a..2a454400f 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 c809e4791..03bd8426f 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 29c991837..082ed7ed0 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