1 files changed, 475 insertions, 84 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index de2a890fb5..df9e253135 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -59,6 +59,7 @@
    etc.
 *)
 
+open CErrors
 open Util
 open Names
 open Declarations
@@ -167,6 +168,12 @@ let is_initial senv =
 
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
 
+let constant_of_delta_kn_senv senv kn =
+  Mod_subst.constant_of_deltas_kn senv.paramresolver senv.modresolver kn
+
+let mind_of_delta_kn_senv senv kn =
+  Mod_subst.mind_of_deltas_kn senv.paramresolver senv.modresolver kn
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
@@ -185,7 +192,24 @@ let set_engagement c senv =
     engagement = Some c }
 
 let set_typing_flags c senv =
-  { senv with env = Environ.set_typing_flags c senv.env }
+  let env = Environ.set_typing_flags c senv.env in
+  if env == senv.env then senv
+  else { senv with env }
+
+let set_indices_matter indices_matter senv =
+  set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
+
+let set_share_reduction b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with share_reduction = b } senv
+
+let set_VM b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with enable_VM = b } senv
+
+let set_native_compiler b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with enable_native_compiler = b } senv
 
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
@@ -209,59 +233,88 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-type private_constant = Entries.side_effect
-type private_constants = Term_typing.side_effects
-
-type private_constant_role = Term_typing.side_effect_role =
-  | Subproof
-  | Schema of inductive * string
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
+  eff      : Entries.side_eff list;
+}
 
-let empty_private_constants = Term_typing.empty_seff
-let add_private = Term_typing.add_seff
-let concat_private = Term_typing.concat_seff
-let mk_pure_proof = Term_typing.mk_pure_proof
-let inline_private_constants_in_constr = Term_typing.inline_side_effects
-let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants = Term_typing.uniq_seff
+module SideEffects :
+sig
+  type t
+  val repr : t -> side_effect list
+  val empty : t
+  val add : side_effect -> t -> t
+  val concat : t -> t -> t
+end =
+struct
+
+module SeffOrd = struct
+open Entries
+type t = side_effect
+let compare e1 e2 =
+  let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
+  List.compare cmp e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+  if SeffSet.mem x es.elts then es
+  else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+  List.fold_right add xes.seff yes
+
+end
+
+type private_constants = SideEffects.t
+
+let side_effects_of_private_constants l =
+  let ans = List.rev (SideEffects.repr l) in
+  List.map_append (fun { eff; _ } -> eff) ans
+
+let empty_private_constants = SideEffects.empty
+let add_private mb eff effs =
+  let from_env = CEphemeron.create mb in
+  SideEffects.add { eff; from_env } effs
+let concat_private = SideEffects.concat
+
+let make_eff env cst r =
+  let open Entries in
+  let cbo = Environ.lookup_constant cst env.env in
+  {
+    seff_constant = cst;
+    seff_body = cbo;
+    seff_env = get_opaque_body env.env cbo;
+    seff_role = r;
+  }
 
 let private_con_of_con env c =
-  let cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+  let open Entries in
+  let eff = [make_eff env c Subproof] in
+  add_private env.revstruct eff empty_private_constants
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEscheme(
-      List.map (fun (i,c) ->
-        let cbo = Environ.lookup_constant c env.env in
-        i, c, cbo, get_opaque_body env.env cbo) cl,
-      kind) }
+  let open Entries in
+  let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
+  add_private env.revstruct eff empty_private_constants
 
 let universes_of_private eff =
-  let open Declarations in
-  List.fold_left
-    (fun acc { Entries.eff } ->
-       match eff with
-       | Entries.SEscheme (l,s) ->
-         List.fold_left
-           (fun acc (_,_,cb,c) ->
-              let acc = match c with
-                | `Nothing -> acc
-                | `Opaque (_, ctx) -> ctx :: acc
-              in
-              match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-           )
-           acc l
-       | Entries.SEsubproof (c, cb, e) ->
-         match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-    )
-    [] (Term_typing.uniq_seff eff)
+  let open Entries in
+  let fold acc eff =
+    let acc = match eff.seff_env with
+    | `Nothing -> acc
+    | `Opaque (_, ctx) -> ctx :: acc
+    in
+    match eff.seff_body.const_universes with
+    | Monomorphic_const ctx -> ctx :: acc
+    | Polymorphic_const _ -> acc
+  in
+  List.fold_left fold [] (side_effects_of_private_constants eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -283,7 +336,6 @@ let add_constraints_list cst senv =
   List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
 let push_context_set poly ctx = add_constraints (Now (poly,ctx))
-let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
 
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
@@ -449,7 +501,7 @@ type generic_name =
   | M (** name already known, cf the mod_mp field *)
   | MT (** name already known, cf the mod_mp field *)
 
-let add_field ((l,sfb) as field) gn senv =
+let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
   let mlabs,olabs = match sfb with
     | SFBmind mib ->
       let l = labels_of_mib mib in
@@ -459,8 +511,18 @@ let add_field ((l,sfb) as field) gn senv =
     | SFBmodule _ | SFBmodtype _ ->
       check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
-  let cst = constraints_of_sfb senv.env sfb in
-  let senv = add_constraints_list cst senv in
+  let senv =
+    if is_include then
+      (* Universes and constraints were added when the included module
+         was defined eg in [Include F X.] (one of the trickier
+         versions of Include) the constraints on the fields are
+         exactly those of the fields of F which was defined
+         separately. *)
+      senv
+    else
+      let cst = constraints_of_sfb senv.env sfb in
+      add_constraints_list cst senv
+  in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
     | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -488,12 +550,12 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  Constant.t * private_constant_role
+  Constant.t * Entries.side_effect_role
 
-let add_constant_aux no_section senv (kn, cb) =
-  let l = pi3 (Constant.repr3 kn) in
+let add_constant_aux ~in_section senv (kn, cb) =
+  let l = Constant.label kn in
   let cb, otab = match cb.const_body with
-    | OpaqueDef lc when no_section ->
+    | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       let od, otab =
@@ -512,28 +574,241 @@ let add_constant_aux no_section senv (kn, cb) =
   in
   senv''
 
+let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
+
+let inline_side_effects env body side_eff =
+  let open Entries in
+  let open Constr in
+  (** First step: remove the constants that are still in the environment *)
+  let filter { eff = se; from_env = mb } =
+    let map e = (e.seff_constant, e.seff_body, e.seff_env) in
+    let cbl = List.map map se in
+    let not_exists (c,_,_) =
+      try ignore(Environ.lookup_constant c env); false
+      with Not_found -> true in
+    let cbl = List.filter not_exists cbl in
+    (cbl, mb)
+  in
+  (* CAVEAT: we assure that most recent effects come first *)
+  let side_eff = List.map filter (SideEffects.repr side_eff) in
+  let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
+  let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+  let side_eff = List.rev side_eff in
+  (** Most recent side-effects first in side_eff *)
+  if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
+  else
+    (** Second step: compute the lifts and substitutions to apply *)
+    let cname c = Name (Label.to_id (Constant.label c)) in
+    let fold (subst, var, ctx, args) (c, cb, b) =
+      let (b, opaque) = match cb.const_body, b with
+      | Def b, _ -> (Mod_subst.force_constr b, false)
+      | OpaqueDef _, `Opaque (b,_) -> (b, true)
+      | _ -> assert false
+      in
+      match cb.const_universes with
+      | Monomorphic_const univs ->
+        (** Abstract over the term at the top of the proof *)
+        let ty = cb.const_type in
+        let subst = Cmap_env.add c (Inr var) subst in
+        let ctx = Univ.ContextSet.union ctx univs in
+        (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
+      | Polymorphic_const _ ->
+        (** Inline the term to emulate universe polymorphism *)
+        let subst = Cmap_env.add c (Inl b) subst in
+        (subst, var, ctx, args)
+    in
+    let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, Univ.ContextSet.empty, []) side_eff in
+    (** Third step: inline the definitions *)
+    let rec subst_const i k t = match Constr.kind t with
+    | Const (c, u) ->
+      let data = try Some (Cmap_env.find c subst) with Not_found -> None in
+      begin match data with
+      | None -> t
+      | Some (Inl b) ->
+        (** [b] is closed but may refer to other constants *)
+        subst_const i k (Vars.subst_instance_constr u b)
+      | Some (Inr n) ->
+        mkRel (k + n - i)
+      end
+    | Rel n ->
+      (** Lift free rel variables *)
+      if n <= k then t
+      else mkRel (n + len - i - 1)
+    | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
+    in
+    let map_args i (na, b, ty, opaque) =
+      (** Both the type and the body may mention other constants *)
+      let ty = subst_const (len - i - 1) 0 ty in
+      let b = subst_const (len - i - 1) 0 b in
+      (na, b, ty, opaque)
+    in
+    let args = List.mapi map_args args in
+    let body = subst_const 0 0 body in
+    let fold_arg (na, b, ty, opaque) accu =
+      if opaque then mkApp (mkLambda (na, ty, accu), [|b|])
+      else mkLetIn (na, b, ty, accu)
+    in
+    let body = List.fold_right fold_arg args body in
+    (body, ctx, sigs)
+
+let inline_private_constants_in_definition_entry env ce =
+  let open Entries in
+  { ce with
+  const_entry_body = Future.chain
+    ce.const_entry_body (fun ((body, ctx), side_eff) ->
+      let body, ctx',_ = inline_side_effects env body side_eff in
+      let ctx' = Univ.ContextSet.union ctx ctx' in
+      (body, ctx'), ());
+  }
+
+let inline_private_constants_in_constr env body side_eff =
+  pi1 (inline_side_effects env body side_eff)
+
+let rec is_nth_suffix n l suf =
+  if Int.equal n 0 then l == suf
+  else match l with
+  | [] -> false
+  | _ :: l -> is_nth_suffix (pred n) l suf
+
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct.
+   Returns the number of effects that can be trusted. *)
+let check_signatures curmb sl =
+  let is_direct_ancestor accu (mb, how_many) =
+    match accu with
+    | None -> None
+    | Some (n, curmb) ->
+        try
+          let mb = CEphemeron.get mb in
+          if is_nth_suffix how_many mb curmb
+          then Some (n + how_many, mb)
+          else None
+        with CEphemeron.InvalidKey -> None in
+  let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
+  match sl with
+  | None -> 0
+  | Some (n, _) -> n
+
+
+let constant_entry_of_side_effect cb u =
+  let open Entries in
+  let univs =
+    match cb.const_universes with
+    | Monomorphic_const uctx ->
+      Monomorphic_const_entry uctx
+    | Polymorphic_const auctx ->
+      Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
+  in
+  let pt =
+    match cb.const_body, u with
+    | OpaqueDef _, `Opaque (b, c) -> b, c
+    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    | _ -> assert false in
+  DefinitionEntry {
+    const_entry_body = Future.from_val (pt, ());
+    const_entry_secctx = None;
+    const_entry_feedback = None;
+    const_entry_type = Some cb.const_type;
+    const_entry_universes = univs;
+    const_entry_opaque = Declareops.is_opaque cb;
+    const_entry_inline_code = cb.const_inline_code }
+
+let turn_direct orig =
+  let open Entries in
+  let cb = orig.seff_body in
+  if Declareops.is_opaque cb then
+    let p = match orig.seff_env with
+    | `Opaque (b, c) -> (b, c)
+    | _ -> assert false
+    in
+    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
+    let cb = { cb with const_body } in
+    { orig with seff_body = cb }
+  else orig
+
+let export_eff eff =
+  let open Entries in
+  (eff.seff_constant, eff.seff_body, eff.seff_role)
+
+let export_side_effects mb env c =
+  let open Entries in
+      let body = c.const_entry_body in
+      let _, eff = Future.force body in
+      let ce = { c with
+        Entries.const_entry_body = Future.chain body
+          (fun (b_ctx, _) -> b_ctx, ()) } in
+      let not_exists e =
+        try ignore(Environ.lookup_constant e.seff_constant env); false
+        with Not_found -> true in
+      let aux (acc,sl) { eff = se; from_env = mb } =
+        let cbl = List.filter not_exists se in
+        if List.is_empty cbl then acc, sl
+        else cbl :: acc, (mb,List.length cbl) :: sl in
+      let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
+      let trusted = check_signatures mb signatures in
+      let push_seff env eff =
+        let { seff_constant = kn; seff_body = cb ; _ } = eff in
+        let env = Environ.add_constant kn cb env in
+        match cb.const_universes with
+        | Polymorphic_const _ -> env
+        | Monomorphic_const ctx ->
+          let ctx = match eff.seff_env with
+          | `Nothing -> ctx
+          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          in
+          Environ.push_context_set ~strict:true ctx env
+      in
+      let rec translate_seff sl seff acc env =
+        match seff with
+        | [] -> List.rev acc, ce
+        | cbs :: rest ->
+          if Int.equal sl 0 then
+           let env, cbs =
+             List.fold_left (fun (env,cbs) eff ->
+              let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
+               let ce = constant_entry_of_side_effect ocb u in
+               let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
+               let eff = { eff with
+                seff_body = cb;
+                seff_env = `Nothing;
+               } in
+               (push_seff env eff, export_eff eff :: cbs))
+             (env,[]) cbs in
+           translate_seff 0 rest (cbs @ acc) env
+          else
+           let cbs_len = List.length cbs in
+           let cbs = List.map turn_direct cbs in
+           let env = List.fold_left push_seff env cbs in
+           let ecbs = List.map export_eff cbs in
+           translate_seff (sl - cbs_len) rest (ecbs @ acc) env
+     in
+       translate_seff trusted seff [] env
+
 let export_private_constants ~in_section ce senv =
-  let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
+  let exported, ce = 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, _, 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
+  let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_constant dir l decl senv =
-  let kn = Constant.make3 senv.modpath dir l in
-  let no_section = DirPath.is_empty dir in
+let add_constant ~in_section l decl senv =
+  let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
       match decl with
       | ConstantEntry (EffectEntry, ce) ->
-        Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce
+        let handle env body eff =
+          let body, uctx, signatures = inline_side_effects env body eff in
+          let trusted = check_signatures senv.revstruct signatures in
+          body, uctx, trusted
+        in
+        Term_typing.translate_constant (Term_typing.SideEffects handle) 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
-    add_constant_aux no_section senv (kn, cb) in
+        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+        if in_section then cb else Declareops.hcons_const_body cb in
+    add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
 (** Insertion of inductive types *)
@@ -546,9 +821,9 @@ let check_mind mie lab =
     (* The label and the first inductive type name should match *)
     assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
 
-let add_mind dir l mie senv =
+let add_mind l mie senv =
   let () = check_mind mie l in
-  let kn = MutInd.make3 senv.modpath dir l in
+  let kn = MutInd.make2 senv.modpath l in
   let mib = Term_typing.translate_mind senv.env kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
@@ -781,13 +1056,13 @@ let add_include me is_module inl senv =
   let add senv ((l,elem) as field) =
     let new_name = match elem with
       | SFBconst _ ->
-        C (Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp_sup l))
+        C (Mod_subst.constant_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmind _ ->
-	I (Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp_sup l))
+        I (Mod_subst.mind_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmodule _ -> M
       | SFBmodtype _ -> MT
     in
-    add_field field new_name senv
+    add_field ~is_include:true field new_name senv
   in
   resolver, List.fold_left add senv str
 
@@ -801,6 +1076,8 @@ type compiled_library = {
   comp_natsymbs : Nativecode.symbols
 }
 
+let module_of_library lib = lib.comp_mod
+
 type native_library = Nativecode.global list
 
 let get_library_native_symbols senv dir =
@@ -896,12 +1173,8 @@ let typing senv = Typeops.infer (env_of_senv senv)
 
 (** {6 Retroknowledge / native compiler } *)
 
-(** universal lifting, used for the "get" operations mostly *)
-let retroknowledge f senv =
-  Environ.retroknowledge f (env_of_senv senv)
-
-let register field value by_clause senv =
-  (* todo : value closed, by_clause safe, by_clause of the proper type*)
+let register field value senv =
+  (* todo : value closed *)
   (* spiwack : updates the safe_env with the information that the register
      action has to be performed (again) when the environment is imported *)
   { senv with
@@ -914,16 +1187,12 @@ let register field value by_clause senv =
 but it is meant to become a replacement for environ.register *)
 let register_inline kn senv =
   let open Environ in
-  let open Pre_env in
   if not (evaluable_constant kn senv.env) then
     CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected");
-  let env = pre_env senv.env in
-  let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
+  let env = senv.env in
+  let cb = lookup_constant kn env in
   let cb = {cb with const_inline_code = true} in
-  let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in
-  let new_globals = { env.env_globals with env_constants = new_constants } in
-  let env = { env with env_globals = new_globals } in
-  { senv with env = env_of_pre_env env }
+  let env = add_constant kn cb env in { senv with env}
 
 let add_constraints c =
   add_constraints
@@ -950,6 +1219,128 @@ loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
 
-let set_strategy e k l = { e with env =
+let set_strategy k l e = { e with env =
    (Environ.set_oracle e.env
       (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
+
+(** Register retroknowledge hooks *)
+
+open Retroknowledge
+
+(* the Environ.register function synchronizes the proactive and reactive
+   retroknowledge. *)
+let dispatch =
+
+  (* subfunction used for static decompilation of int31 (after a vm_compute,
+     see pretyping/vnorm.ml for more information) *)
+  let constr_of_int31 =
+    let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
+                                    digit of i and adds 1 to it
+                                    (nth_digit_plus_one 1 3 = 2) *)
+      if Int.equal (i land (1 lsl n)) 0 then
+        1
+      else
+        2
+    in
+      fun ind -> fun digit_ind -> fun tag ->
+        let array_of_int i =
+          Array.init 31 (fun n -> Constr.mkConstruct
+                           (digit_ind, nth_digit_plus_one i (30-n)))
+        in
+        (* We check that no bit above 31 is set to one. This assertion used to
+        fail in the VM, and led to conversion tests failing at Qed. *)
+        assert (Int.equal (tag lsr 31) 0);
+        Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag)
+  in
+
+  (* subfunction which dispatches the compiling information of an
+     int31 operation which has a specific vm instruction (associates
+     it to the name of the coq definition in the reactive retroknowledge) *)
+  let int31_op n op prim kn =
+    { empty_reactive_info with
+      vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *)
+      native_compiling = Some (Nativelambda.compile_prim prim kn);
+    }
+  in
+
+fun rk value field ->
+  (* subfunction which shortens the (very common) dispatch of operations *)
+  let int31_op_from_const n op prim =
+    match value with
+      | GlobRef.ConstRef kn -> int31_op n op prim kn
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
+  in
+  let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
+  let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
+  match field with
+    | KInt31 Int31Type ->
+        let int31bit =
+          (* invariant : the type of bits is registered, otherwise the function
+             would raise Not_found. The invariant is enforced in safe_typing.ml *)
+          match field with
+          | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits)
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
+        in
+        let i31bit_type =
+          match int31bit with
+          | GlobRef.IndRef i31bit_type -> i31bit_type
+          |  _ -> anomaly ~label:"Environ.register"
+              (Pp.str "Int31Bits should be an inductive type.")
+        in
+        let int31_decompilation =
+          match value with
+          | GlobRef.IndRef i31t ->
+              constr_of_int31 i31t i31bit_type
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "should be an inductive type.")
+        in
+        { empty_reactive_info with
+          vm_decompile_const = Some int31_decompilation;
+          vm_before_match = Some Clambda.int31_escape_before_match;
+          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
+        }
+    | KInt31 Int31Constructor ->
+        { empty_reactive_info with
+          vm_constant_static = Some Clambda.compile_structured_int31;
+          vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
+          native_constant_static = Some Nativelambda.compile_static_int31;
+          native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
+        }
+    | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31
+                                                          CPrimitives.Int31add
+    | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31
+                                                           CPrimitives.Int31addc
+    | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
+                                                                CPrimitives.Int31addcarryc
+    | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31
+                                                           CPrimitives.Int31sub
+    | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31
+                                                            CPrimitives.Int31subc
+    | KInt31 Int31MinusCarryC -> int31_binop_from_const
+                                        Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
+    | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31
+                                                           CPrimitives.Int31mul
+    | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31
+                                                           CPrimitives.Int31mulc
+    | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
+                                                           CPrimitives.Int31div21
+    | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31
+                                                         CPrimitives.Int31diveucl
+    | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
+                                                         CPrimitives.Int31addmuldiv
+    | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31
+                                                             CPrimitives.Int31compare
+    | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31
+                                                          CPrimitives.Int31head0
+    | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31
+                                                          CPrimitives.Int31tail0
+    | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31
+                                                         CPrimitives.Int31lor
+    | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31
+                                                          CPrimitives.Int31land
+    | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31
+                                                          CPrimitives.Int31lxor
+    | _ -> empty_reactive_info
+
+let _ = Hook.set Retroknowledge.dispatch_hook dispatch