Imported Upstream version 8.5~beta1+dfsg

1 files changed, 355 insertions, 199 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index b8818950..0ebff440 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,11 +20,12 @@
 (* This file defines the type of environments on which the
    type-checker works, together with simple related functions *)
 
+open Errors
 open Util
 open Names
-open Sign
-open Univ
 open Term
+open Context
+open Vars
 open Declarations
 open Pre_env
 
@@ -36,20 +37,33 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
+let oracle env = env.env_conv_oracle
+let set_oracle env o = { env with env_conv_oracle = o }
 
 let empty_named_context_val = empty_named_context_val
 
 let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
+
+let type_in_type env = env.env_stratification.env_type_in_type
+
+let is_impredicative_set env = 
+  match engagement env with
+  | Some ImpredicativeSet -> true
+  | _ -> false
+
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
 let named_context_val env = env.env_named_context,env.env_named_vals
 let rel_context env = env.env_rel_context
+let opaque_tables env = env.indirect_pterms
+let set_opaque_tables env indirect_pterms = { env with indirect_pterms }
 
 let empty_context env =
-  env.env_rel_context = empty_rel_context
-  && env.env_named_context = empty_named_context
+  match env.env_rel_context, env.env_named_context with
+  | [], [] -> true
+  | _ -> false
 
 (* Rel context *)
 let lookup_rel n env =
@@ -64,10 +78,10 @@ let nb_rel env = env.env_nb_rel
 
 let push_rel = push_rel
 
-let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
+let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 let fold_rel_context f env ~init =
@@ -92,21 +106,29 @@ let named_vals_of_val = snd
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
 let map_named_val f (ctxt,ctxtv) =
-  let ctxt =
-    List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in
-  (ctxt,ctxtv)
+  let rec map ctx = match ctx with
+  | [] -> []
+  | (id, body, typ) :: rem ->
+    let body' = Option.smartmap f body in
+    let typ' = f typ in
+    let rem' = map rem in
+    if body' == body && typ' == typ && rem' == rem then ctx
+    else (id, body', typ') :: rem'
+  in
+  (map ctxt, ctxtv)
 
 let empty_named_context = empty_named_context
 
 let push_named = push_named
+let push_named_context = List.fold_right push_named
 let push_named_context_val = push_named_context_val
 
 let val_of_named_context ctxt =
   List.fold_right push_named_context_val ctxt empty_named_context_val
 
 
-let lookup_named id env = Sign.lookup_named id env.env_named_context
-let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt
+let lookup_named id env = Context.lookup_named id env.env_named_context
+let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt
 
 let eq_named_context_val c1 c2 =
    c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2)
@@ -134,6 +156,12 @@ let reset_with_named_context (ctxt,ctxtv) env =
 
 let reset_context = reset_with_named_context empty_named_context_val
 
+let pop_rel_context n env =
+  let ctxt = env.env_rel_context in
+  { env with
+    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_nb_rel = env.env_nb_rel - n }
+
 let fold_named_context f env ~init =
   let rec fold_right env =
     match env.env_named_context with
@@ -145,77 +173,210 @@ let fold_named_context f env ~init =
   in fold_right env
 
 let fold_named_context_reverse f ~init env =
-  Sign.fold_named_context_reverse f ~init:init (named_context env)
+  Context.fold_named_context_reverse f ~init:init (named_context env)
+
+
+(* Universe constraints *)
+
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then
+    env
+  else
+    let s = env.env_stratification in
+    { env with env_stratification =
+      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+
+let check_constraints c env =
+  Univ.check_constraints c env.env_stratification.env_universes
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = Some c } }
+
+let set_type_in_type env =
+  { env with env_stratification =
+    { env.env_stratification with env_type_in_type = true } }
+
+let push_constraints_to_env (_,univs) env =
+  add_constraints univs env
+
+let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
+let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
 
 (* Global constants *)
 
 let lookup_constant = lookup_constant
 
-let add_constant kn cs env =
+let no_link_info = NotLinked
+
+let add_constant_key kn cb linkinfo env =
   let new_constants =
-    Cmap_env.add kn (cs,ref None) env.env_globals.env_constants in
+    Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
+let add_constant kn cb env =
+  add_constant_key kn cb no_link_info env
+
+let constraints_of cb u =
+  let univs = cb.const_universes in
+    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
+
+let map_regular_arity f = function
+  | RegularArity a as ar -> 
+    let a' = f a in 
+      if a' == a then ar else RegularArity a'
+  | TemplateArity _ -> assert false
+
 (* constant_type gives the type of a constant *)
-let constant_type env kn =
+let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-    cb.const_type
+    if cb.const_polymorphic then
+      let csts = constraints_of cb u in
+	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+    else cb.const_type, Univ.Constraint.empty
 
-type const_evaluation_result = NoBody | Opaque
+let constant_context env kn =
+  let cb = lookup_constant kn env in
+    if cb.const_polymorphic then cb.const_universes
+    else Univ.UContext.empty
+
+type const_evaluation_result = NoBody | Opaque | IsProj
 
 exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env kn =
+let constant_value env (kn,u) =
+  let cb = lookup_constant kn env in
+    if cb.const_proj = None then
+      match cb.const_body with
+      | Def l_body -> 
+	if cb.const_polymorphic then
+	  let csts = constraints_of cb u in
+	    (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
+	else Mod_subst.force_constr l_body, Univ.Constraint.empty
+      | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+      | Undef _ -> raise (NotEvaluableConst NoBody)
+    else raise (NotEvaluableConst IsProj)
+
+let constant_opt_value env cst =
+  try Some (constant_value env cst)
+  with NotEvaluableConst _ -> None
+
+let constant_value_and_type env (kn, u) =
+  let cb = lookup_constant kn env in
+    if cb.const_polymorphic then
+      let cst = constraints_of cb u in
+      let b' = match cb.const_body with
+	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
+	| OpaqueDef _ -> None
+	| Undef _ -> None
+      in
+	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
+    else 
+      let b' = match cb.const_body with
+	| Def l_body -> Some (Mod_subst.force_constr l_body)
+	| OpaqueDef _ -> None
+	| Undef _ -> None
+      in b', cb.const_type, Univ.Constraint.empty
+
+(* These functions should be called under the invariant that [env] 
+   already contains the constraints corresponding to the constant 
+   application. *)
+
+(* constant_type gives the type of a constant *)
+let constant_type_in env (kn,u) =
+  let cb = lookup_constant kn env in
+    if cb.const_polymorphic then
+      map_regular_arity (subst_instance_constr u) cb.const_type
+    else cb.const_type
+
+let constant_value_in env (kn,u) =
   let cb = lookup_constant kn env in
   match cb.const_body with
-    | Def l_body -> Declarations.force l_body
+    | Def l_body -> 
+      let b = Mod_subst.force_constr l_body in
+	subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
 
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
+let constant_opt_value_in env cst =
+  try Some (constant_value_in env cst)
   with NotEvaluableConst _ -> None
 
 (* A global const is evaluable if it is defined and not opaque *)
-let evaluable_constant cst env =
-  try let _  = constant_value env cst in true
-  with NotEvaluableConst _ -> false
+let evaluable_constant kn env =
+  let cb = lookup_constant kn env in
+    match cb.const_body with
+    | Def _ -> true
+    | OpaqueDef _ -> false
+    | Undef _ -> false
+
+let polymorphic_constant cst env =
+  (lookup_constant cst env).const_polymorphic
+
+let polymorphic_pconstant (cst,u) env =
+  if Univ.Instance.is_empty u then false
+  else polymorphic_constant cst env
+
+let template_polymorphic_constant cst env =
+  match (lookup_constant cst env).const_type with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pconstant (cst,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_constant cst env
+
+let lookup_projection cst env =
+  match (lookup_constant (Projection.constant cst) env).const_proj with 
+  | Some pb -> pb
+  | None -> anomaly (Pp.str "lookup_projection: constant is not a projection")
+
+let is_projection cst env =
+  match (lookup_constant cst env).const_proj with 
+  | Some _ -> true
+  | None -> false
 
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
+
+let polymorphic_ind (mind,i) env =
+  (lookup_mind mind env).mind_polymorphic
+
+let polymorphic_pind (ind,u) env =
+  if Univ.Instance.is_empty u then false
+  else polymorphic_ind ind env
+
+let template_polymorphic_ind (mind,i) env =
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with 
+  | TemplateArity _ -> true
+  | RegularArity _ -> false
+
+let template_polymorphic_pind (ind,u) env =
+  if not (Univ.Instance.is_empty u) then false
+  else template_polymorphic_ind ind env
   
-let add_mind kn mib env =
-  let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+let add_mind_key kn mind_key env =
+  let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
 	env_inductives = new_inds } in
   { env with env_globals = new_globals }
 
-(* Universe constraints *)
-
-let add_constraints c env =
-  if is_empty_constraint c then
-    env
-  else
-    let s = env.env_stratification in
-    { env with env_stratification =
-      { s with env_universes = merge_constraints c s.env_universes } }
-
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
+let add_mind kn mib env =
+  let li = ref no_link_info in add_mind_key kn (mib, li) env
 
 (* Lookup of section variables *)
+
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
-  Sign.vars_of_named_context cmap.const_hyps
+  Context.vars_of_named_context cmap.const_hyps
 
 let lookup_inductive_variables (kn,i) env =
   let mis = lookup_mind kn env in
-  Sign.vars_of_named_context mis.mind_hyps
+  Context.vars_of_named_context mis.mind_hyps
 
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
@@ -224,10 +385,11 @@ let lookup_constructor_variables (ind,_) env =
 
 let vars_of_global env constr =
   match kind_of_term constr with
-      Var id -> [id]
-    | Const kn -> lookup_constant_variables kn env
-    | Ind ind -> lookup_inductive_variables ind env
-    | Construct cstr -> lookup_constructor_variables cstr env
+      Var id -> Id.Set.singleton id
+    | Const (kn, _) -> lookup_constant_variables kn env
+    | Ind (ind, _) -> lookup_inductive_variables ind env
+    | Construct (cstr, _) -> lookup_constructor_variables cstr env
+    (** FIXME: is Proj missing? *)
     | _ -> raise Not_found
 
 let global_vars_set env constr =
@@ -235,54 +397,54 @@ let global_vars_set env constr =
     let acc =
       match kind_of_term c with
       | Var _ | Const _ | Ind _ | Construct _ ->
-	  List.fold_right Idset.add (vars_of_global env c) acc
+	  Id.Set.union (vars_of_global env c) acc
       | _ ->
 	  acc in
     fold_constr filtrec acc c
   in
-    filtrec Idset.empty constr
+    filtrec Id.Set.empty constr
 
 
 (* [keep_hyps env ids] keeps the part of the section context of [env] which
    contains the variables of the set [ids], and recursively the variables
    contained in the types of the needed variables. *)
 
+let really_needed env needed =
+  Context.fold_named_context_reverse
+    (fun need (id,copt,t) ->
+      if Id.Set.mem id need then
+        let globc =
+          match copt with
+            | None -> Id.Set.empty
+            | Some c -> global_vars_set env c in
+        Id.Set.union
+          (global_vars_set env t)
+          (Id.Set.union globc need)
+      else need)
+    ~init:needed
+    (named_context env)
+
 let keep_hyps env needed =
-  let really_needed =
-    Sign.fold_named_context_reverse
-      (fun need (id,copt,t) ->
-        if Idset.mem id need then
-          let globc =
-	    match copt with
-	      | None -> Idset.empty
-	      | Some c -> global_vars_set env c in
-	  Idset.union
-            (global_vars_set env t)
-	    (Idset.union globc need)
-        else need)
-      ~init:needed
-      (named_context env) in
-  Sign.fold_named_context
+  let really_needed = really_needed env needed in
+  Context.fold_named_context
     (fun (id,_,_ as d) nsign ->
-      if Idset.mem id really_needed then add_named_decl d nsign
+      if Id.Set.mem id really_needed then add_named_decl d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
 
 (* Modules *)
 
-let add_modtype ln mtb env =
-  let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
-  let new_globals =
-    { env.env_globals with
-	env_modtypes = new_modtypes } in
+let add_modtype mtb env =
+  let mp = mtb.mod_mp in
+  let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
+  let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
   { env with env_globals = new_globals }
 
-let shallow_add_module mp mb env =
+let shallow_add_module mb env =
+  let mp = mb.mod_mp in
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
-  let new_globals =
-    { env.env_globals with
-	env_modules = new_mods } in
+  let new_globals = { env.env_globals with env_modules = new_mods } in
   { env with env_globals = new_globals }
 
 let lookup_module mp env =
@@ -315,11 +477,11 @@ let compile_constant_body = Cbytegen.compile_constant_body
 
 exception Hyp_not_found
 
-let rec apply_to_hyp (ctxt,vals) id f =
+let apply_to_hyp (ctxt,vals) id f =
   let rec aux rtail ctxt vals =
     match ctxt, vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if idc = id then
+	if Id.equal idc id then
 	  (f ctxt d rtail)::ctxt, v::vals
 	else
 	  let ctxt',vals' = aux (d::rtail) ctxt vals in
@@ -328,11 +490,11 @@ let rec apply_to_hyp (ctxt,vals) id f =
     | _, _ -> assert false
   in aux [] ctxt vals
 
-let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   let rec aux ctxt vals =
     match ctxt,vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if idc = id then
+	if Id.equal idc id then
 	  let sign = ctxt,vals in
 	  push_named_context_val (f d sign) sign
 	else
@@ -346,7 +508,7 @@ let insert_after_hyp (ctxt,vals) id d check =
   let rec aux ctxt vals =
     match  ctxt, vals with
     | (idc,c,ct)::ctxt', v::vals' ->
-	if idc = id then begin
+	if Id.equal idc id then begin
 	  check ctxt;
 	  push_named_context_val d (ctxt,vals)
 	end else
@@ -359,18 +521,22 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
-  List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
-      if List.mem id ids then
-	(ctxt,vals)
-      else
-	let nd = check_context d in
-	let nv = check_value v in
-	  (nd::ctxt,(id',nv)::vals))
-		     ctxt vals ([],[])
-
-
-
-
+  let rec remove_hyps ctxt vals = match ctxt, vals with
+  | [], [] -> [], []
+  | d :: rctxt, (nid, v) :: rvals ->
+    let (id, _, _) = d in
+    let ans = remove_hyps rctxt rvals in
+    if Id.Set.mem id ids then ans
+    else
+      let (rctxt', rvals') = ans in
+      let d' = check_context d in
+      let v' = check_value v in
+      if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then
+        ctxt, vals
+      else (d' :: rctxt', (nid, v') :: rvals')
+  | _ -> assert false
+  in
+  remove_hyps ctxt vals
 
 (*spiwack: the following functions assemble the pieces of the retroknowledge
    note that the "consistent" register function is available in the module
@@ -385,35 +551,23 @@ let retroknowledge f env =
 let registered env field =
     retroknowledge mem env field
 
-(* spiwack: this unregistration function is not in operation yet. It should
-            not be used *)
-(* this unregistration function assumes that no "constr" can hold two different
-   places in the retroknowledge. There is no reason why it shouldn't be true,
-   but in case someone needs it, remember to add special branches to the
-   unregister function *)
-let unregister env field =
-  match field with
-    | KInt31 (_,Int31Type) ->
-	(*there is only one matching kind due to the fact that Environ.env
-          is abstract, and that the only function which add elements to the
-          retroknowledge is Environ.register which enforces this shape *)
-	(match retroknowledge find env field with
-	   | Ind i31t -> let i31c = Construct (i31t, 1) in
-	     {env with retroknowledge =
-		 remove (retroknowledge clear_info env i31c) field}
-	   | _ -> assert false)
-    |_ -> {env with retroknowledge =
-	   try
-	     remove (retroknowledge clear_info env
-                       (retroknowledge find env field)) field
-	   with Not_found ->
-	     retroknowledge remove env field}
-
+let register_one env field entry =
+  { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry }
 
+(* [register env field entry] may register several fields when needed *)
+let register env field entry =
+  match field with
+    | KInt31 (grp, Int31Type) ->
+        let i31c = match kind_of_term entry with
+                     | Ind i31t -> mkConstructUi (i31t, 1)
+		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
+	in
+        register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
+    | field -> register_one env field entry
 
 (* the Environ.register function syncrhonizes the proactive and reactive
    retroknowledge. *)
-let register =
+let dispatch =
 
   (* subfunction used for static decompilation of int31 (after a vm_compute,
      see pretyping/vnorm.ml for more information) *)
@@ -421,7 +575,7 @@ let register =
     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 (land) i ((lsl) 1 n) = 0 then
+      if Int.equal (i land (1 lsl n)) 0 then
         1
       else
         2
@@ -434,92 +588,94 @@ let register =
 	  mkApp(mkConstruct(ind, 1), array_of_int tag)
   in
 
-  (* subfunction which adds the information bound to the constructor of
-     the int31 type to the reactive retroknowledge *)
-  let add_int31c retroknowledge c =
-    let rk = add_vm_constant_static_info retroknowledge c
-                                         Cbytegen.compile_structured_int31
-    in
-    add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation
-  in
-
-  (* subfunction which adds the compiling information of an
+  (* 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 add_int31_op retroknowledge v n op kn =
-    add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+  let int31_op n op prim kn =
+    { empty_reactive_info with
+      vm_compiling = Some (Cbytegen.op_compilation n op kn);
+      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
+    }
   in
 
-fun env field value ->
-  (* subfunction which shortens the (very often use) registration of binary
-     operators to the reactive retroknowledge. *)
-  let add_int31_binop_from_const op =
-    match value with
-      | Const kn ->  retroknowledge add_int31_op env value 2
-	                               op kn
-      | _ -> anomaly "Environ.register: should be a constant"
-  in
-  let add_int31_unop_from_const op =
-    match value with
-      | Const kn ->  retroknowledge add_int31_op env value 1
-	                               op kn
-      | _ -> anomaly "Environ.register: should be a constant"
-  in
-  (* subfunction which completes the function constr_of_int31 above
-     by performing the actual retroknowledge operations *)
-  let add_int31_decompilation_from_type rk =
-    (* 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 (grp, Int31Type) ->
-	  (match Retroknowledge.find rk (KInt31 (grp,Int31Bits)) with
-	    | Ind i31bit_type ->
-		(match value with
-		  | Ind i31t ->
-		      Retroknowledge.add_vm_decompile_constant_info rk
-		               value (constr_of_int31 i31t i31bit_type)
-		  | _ -> anomaly "Environ.register: should be an inductive type")
-	    | _ -> anomaly "Environ.register: Int31Bits should be an inductive type")
-      | _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field"
+fun rk value field ->
+  (* subfunction which shortens the (very common) dispatch of operations *)
+  let int31_op_from_const n op prim =
+    match kind_of_term value with
+      | Const kn ->  int31_op n op prim kn
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
-  {env with retroknowledge =
-  let retroknowledge_with_reactive_info =
+  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 i31c = match value with
-                     | Ind i31t -> (Construct (i31t, 1))
-		     | _ -> anomaly "Environ.register: should be an inductive type"
-	in
-	add_int31_decompilation_from_type
-	  (add_vm_before_match_info
-	     (retroknowledge add_int31c env i31c)
-	     value Cbytegen.int31_escape_before_match)
-    | KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
-    | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
-    | KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
-    | KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
-    | KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
-    | KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const
-	                                           Cbytecodes.Ksubcarrycint31
-    | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
-    | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
-    | KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
-                                (match value with
-				 | Const kn ->
-				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kdiv21int31 kn
-				 | _ -> anomaly "Environ.register: should be a constant")
-    | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
-    | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
-                                (match value with
-				 | Const kn ->
-				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kaddmuldivint31 kn
-				 | _ -> anomaly "Environ.register: should be a constant")
-    | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
-    | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
-    | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
-    | _ -> env.retroknowledge
-  in
-  Retroknowledge.add_field retroknowledge_with_reactive_info field value
-  }
+    | KInt31 (grp, 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 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "add_int31_decompilation_from_type called with an abnormal field")
+        in
+        let i31bit_type =
+          match kind_of_term int31bit with
+          | Ind (i31bit_type,_) -> i31bit_type
+          |  _ -> anomaly ~label:"Environ.register"
+              (Pp.str "Int31Bits should be an inductive type")
+        in
+        let int31_decompilation =
+          match kind_of_term value with
+          | Ind (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 Cbytegen.int31_escape_before_match;
+          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
+        }
+    | KInt31 (_, Int31Constructor) ->
+        { empty_reactive_info with
+          vm_constant_static = Some Cbytegen.compile_structured_int31;
+          vm_constant_dynamic = Some Cbytegen.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
+							  Primitives.Int31add
+    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
+							   Primitives.Int31addc
+    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
+								Primitives.Int31addcarryc
+    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
+							   Primitives.Int31sub
+    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
+							    Primitives.Int31subc
+    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
+	                                Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
+    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
+							   Primitives.Int31mul
+    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
+							   Primitives.Int31mulc
+    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
+                                                           Primitives.Int31div21
+    | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
+							 Primitives.Int31diveucl
+    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
+                                                         Primitives.Int31addmuldiv
+    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
+							     Primitives.Int31compare
+    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
+							  Primitives.Int31head0
+    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
+							  Primitives.Int31tail0
+    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
+							 Primitives.Int31lor
+    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
+							  Primitives.Int31land
+    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
+							  Primitives.Int31lxor
+    | _ -> empty_reactive_info
+
+let _ = Hook.set Retroknowledge.dispatch_hook dispatch