Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 150 insertions, 147 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 72113425..e7859962 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -80,71 +80,71 @@ open Pre_env
 (*  [a1] est mis a jour :                                                 *)
 (*  a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ]     *)
 (* Le cycle est cree ...                                                  *)
-   
+
 (* On conserve la fct de cofix pour la conversion                         *)
-   
-    
+
+
 let empty_fv = { size= 0;  fv_rev = [] }
-  
+
 let fv r = !(r.in_env)
-   
-let empty_comp_env ()= 
-  { nb_stack = 0; 
+
+let empty_comp_env ()=
+  { nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
-    offset = 0; 
+    offset = 0;
     in_env = ref empty_fv;
-  } 
+  }
 
 (*i Creation functions for comp_env *)
 
 let rec add_param n sz l =
-  if n = 0 then l else add_param (n - 1) sz (n+sz::l) 
-   
-let comp_env_fun arity = 
-  { nb_stack = arity; 
+  if n = 0 then l else add_param (n - 1) sz (n+sz::l)
+
+let comp_env_fun arity =
+  { nb_stack = arity;
     in_stack = add_param arity 0 [];
     nb_rec = 0;
     pos_rec = [];
-    offset = 1; 
-    in_env = ref empty_fv 
-  } 
-    
+    offset = 1;
+    in_env = ref empty_fv
+  }
 
-let comp_env_type rfv = 
-  { nb_stack = 0; 
+
+let comp_env_type rfv =
+  { nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
-    offset = 1; 
-    in_env = rfv 
+    offset = 1;
+    in_env = rfv
   }
-   
+
 let comp_env_fix ndef curr_pos arity rfv =
    let prec = ref [] in
    for i = ndef downto 1 do
-     prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec 
+     prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
    done;
-   { nb_stack = arity; 
+   { nb_stack = arity;
      in_stack = add_param arity 0 [];
-     nb_rec = ndef; 
+     nb_rec = ndef;
      pos_rec = !prec;
      offset = 2 * (ndef - curr_pos - 1)+1;
-     in_env = rfv 
-   } 
+     in_env = rfv
+   }
 
 let comp_env_cofix ndef arity rfv =
    let prec = ref [] in
    for i = 1 to ndef do
      prec := Kenvacc i :: !prec
    done;
-   { nb_stack = arity; 
+   { nb_stack = arity;
      in_stack = add_param arity 0 [];
-     nb_rec = ndef; 
+     nb_rec = ndef;
      pos_rec = !prec;
      offset = ndef+1;
-     in_env = rfv 
+     in_env = rfv
    }
 
 (* [push_param ] ajoute les parametres de fonction dans la pile *)
@@ -155,15 +155,15 @@ let push_param n sz r =
 
 (* [push_local e sz] ajoute une nouvelle variable dans la pile a la *)
 (* position [sz]                                                    *)
-let push_local sz r = 
-  { r with 
+let push_local sz r =
+  { r with
     nb_stack = r.nb_stack + 1;
     in_stack = (sz + 1) :: r.in_stack }
 
 
 
 (*i Compilation of variables *)
-let find_at el l = 
+let find_at el l =
   let rec aux n = function
     | [] -> raise Not_found
     | hd :: tl -> if hd = el then n else aux (n+1) tl
@@ -178,12 +178,12 @@ let pos_named id r =
     r.in_env := { size = pos+1; fv_rev =  cid:: env.fv_rev};
     Kenvacc (r.offset + pos)
 
-let pos_rel i r sz = 
+let pos_rel i r sz =
   if i <= r.nb_stack then
     Kacc(sz - (List.nth r.in_stack (i-1)))
   else
     let i = i - r.nb_stack in
-    if i <= r.nb_rec then 
+    if i <= r.nb_rec then
       try List.nth r.pos_rec (i-1)
       with _ -> assert false
     else
@@ -223,7 +223,7 @@ let label_code = function
    when executed, branches to the continuation or performs what the
    continuation performs. We avoid generating branches to returns. *)
 (* spiwack: make_branch was only used once. Changed it back to the ZAM
-      one to match the appropriate semantics (old one avoided the 
+      one to match the appropriate semantics (old one avoided the
       introduction of an unconditional branch operation, which seemed
       appropriate for the 31-bit integers' code). As a memory, I leave
       the former version in this comment.
@@ -259,7 +259,7 @@ let rec is_tailcall = function
   | _ -> None
 
 (* Extention of the continuation *)
-	
+
 (* Add a Kpop n instruction in front of a continuation *)
 let rec add_pop n = function
   | Kpop m :: cont -> add_pop (n+m) cont
@@ -269,9 +269,9 @@ let rec add_pop n = function
 let add_grab arity lbl cont =
   if arity = 1 then Klabel lbl :: cont
   else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont
- 
+
 let add_grabrec rec_arg arity lbl cont =
-  if arity = 1 then 
+  if arity = 1 then
     Klabel lbl :: Kgrabrec 0 :: Krestart :: cont
   else
     Krestart :: Klabel lbl :: Kgrabrec rec_arg ::
@@ -288,11 +288,11 @@ let cont_cofix arity =
     Kacc 2;
     Kfield 1;
     Kfield 0;
-    Kmakeblock(2, cofix_evaluated_tag); 
+    Kmakeblock(2, cofix_evaluated_tag);
     Kpush;        (*  stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
     Kacc 2;
     Ksetfield 1;  (*   ai = [At|accumulate|[Cfxe_t|fcofix|res]|args]      *)
-                  (*  stk = res::ai::args::ra::...                        *)   
+                  (*  stk = res::ai::args::ra::...                        *)
     Kacc 0;       (* accu = res                                           *)
     Kreturn (arity+2) ]
 
@@ -315,24 +315,24 @@ let init_fun_code () = fun_code := []
 let code_construct tag nparams arity cont =
   let f_cont =
       add_pop nparams
-      (if arity = 0 then 
+      (if arity = 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
        else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
-    in 
+    in
     let lbl = Label.create() in
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
     Kclosure(lbl,0) :: cont
 
 let get_strcst = function
   | Bstrconst sc -> sc
-  | _ -> raise Not_found 
+  | _ -> raise Not_found
 
 
-let rec str_const c = 
+let rec str_const c =
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
-  | Cast(c,_,_) -> str_const c 
-  | App(f,args) -> 
+  | Cast(c,_,_) -> str_const c
+  | App(f,args) ->
       begin
 	match kind_of_term f with
 	| Construct((kn,j),i) -> (* arnaud: Construct(((kn,j),i) as cstr) -> *)
@@ -345,32 +345,32 @@ let rec str_const c =
               (* spiwack: *)
               (* 1/ tries to compile the constructor in an optimal way,
                     it is supposed to work only if the arguments are
-                    all fully constructed, fails with Cbytecodes.NotClosed. 
+                    all fully constructed, fails with Cbytecodes.NotClosed.
                     it can also raise Not_found when there is no special
-                    treatment for this constructor 
-                    for instance: tries to to compile an integer of the 
-                        form I31 D1 D2 ... D31 to [D1D2...D31] as 
+                    treatment for this constructor
+                    for instance: tries to to compile an integer of the
+                        form I31 D1 D2 ... D31 to [D1D2...D31] as
                         a processor number (a caml number actually) *)
-              try 
+              try
 		try
-		  Bstrconst (Retroknowledge.get_vm_constant_static_info 
+		  Bstrconst (Retroknowledge.get_vm_constant_static_info
                                               (!global_env).retroknowledge
                                               (kind_of_term f) args)
                 with NotClosed ->
-		  (* 2/ if the arguments are not all closed (this is 
-                        expectingly (and it is currently the case) the only 
-                        reason why this exception is raised) tries to 
+		  (* 2/ if the arguments are not all closed (this is
+                        expectingly (and it is currently the case) the only
+                        reason why this exception is raised) tries to
                         give a clever, run-time behavior to the constructor.
                         Raises Not_found if there is no special treatment
                         for this integer.
                         this is done in a lazy fashion, using the constructor
                         Bspecial because it needs to know the continuation
                         and such, which can't be done at this time.
-                        for instance, for int31: if one of the digit is 
+                        for instance, for int31: if one of the digit is
                             not closed, it's not impossible that the number
                             gets fully instanciated at run-time, thus to ensure
                             uniqueness of the representation in the vm
-                            it is necessary to try and build a caml integer 
+                            it is necessary to try and build a caml integer
                             during the execution *)
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
@@ -385,16 +385,16 @@ let rec str_const c =
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
-		  try 
+		  try
 		    let sc_args = Array.map get_strcst b_args in
 		    Bstrconst(Const_bn(num, sc_args))
 		  with Not_found ->
 		    Bmakeblock(num,b_args)
-	    else  
+	    else
               let b_args = Array.map str_const args in
 	     (* spiwack: tries first to apply the run-time compilation
                 behavior of the constructor, as in 2/ above *)
-	      try 
+	      try
 		Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
                                            (kind_of_term f)),
@@ -407,7 +407,7 @@ let rec str_const c =
   | Ind ind -> Bstrconst (Const_ind ind)
   | Construct ((kn,j),i) ->  (*arnaud: Construct ((kn,j),i as cstr) ->  *)
       begin
-      (* spiwack: tries first to apply the run-time compilation 
+      (* spiwack: tries first to apply the run-time compilation
            behavior of the constructor, as in 2/ above *)
       try
 	Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
@@ -415,7 +415,7 @@ let rec str_const c =
                                            (kind_of_term c)),
                          [| |])
       with Not_found ->
-	let oib = lookup_mind kn !global_env in 
+	let oib = lookup_mind kn !global_env in
 	let oip = oib.mind_packets.(j) in
 	let num,arity = oip.mind_reloc_tbl.(i-1) in
 	let nparams = oib.mind_nparams in
@@ -426,17 +426,17 @@ let rec str_const c =
 
 (* compilation des applications *)
 let comp_args comp_expr reloc args sz cont =
-  let nargs_m_1 = Array.length args - 1 in  
+  let nargs_m_1 = Array.length args - 1 in
   let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
   for i = 1 to nargs_m_1 do
     c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
-  done; 
+  done;
   !c
-  
+
 let comp_app comp_fun comp_arg reloc f args sz cont =
   let nargs = Array.length args in
   match is_tailcall cont with
-  | Some k -> 
+  | Some k ->
       comp_args comp_arg reloc args sz
 	(Kpush ::
 	 comp_fun reloc f (sz + nargs)
@@ -445,14 +445,14 @@ let comp_app comp_fun comp_arg reloc f args sz cont =
       if nargs < 4 then
 	comp_args comp_arg reloc args sz
 	  (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont)))
-      else 
+      else
 	let lbl,cont1 = label_code cont in
 	Kpush_retaddr lbl ::
 	(comp_args comp_arg reloc args (sz + 3)
 	   (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
 
 (* Compilation des variables libres *)
-  
+
 let compile_fv_elem reloc fv sz cont =
   match fv with
   | FVrel i -> pos_rel i reloc sz :: cont
@@ -463,7 +463,7 @@ let rec compile_fv reloc l sz cont =
   | [] -> cont
   | [fvn] -> compile_fv_elem reloc fvn sz cont
   | fvn :: tl ->
-      compile_fv_elem reloc fvn sz 
+      compile_fv_elem reloc fvn sz
 	(Kpush :: compile_fv reloc tl (sz + 1) cont)
 
 (* compilation des constantes *)
@@ -474,14 +474,14 @@ let rec get_allias env kn =
   | BCallias kn' -> get_allias env kn'
   | _ -> kn
 
-  
+
 (* compilation des expressions *)
- 
+
 let rec compile_constr reloc c sz cont =
   match kind_of_term c with
   | Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta")
   | Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar")
- 
+
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
   | Rel i -> pos_rel i reloc sz :: cont
@@ -489,13 +489,13 @@ let rec compile_constr reloc c sz cont =
   | Const kn -> compile_const reloc kn [||] sz cont
   | Sort _  | Ind _ | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
-  
+
   | LetIn(_,xb,_,body) ->
-      compile_constr reloc xb sz 
-	(Kpush :: 
+      compile_constr reloc xb sz
+	(Kpush ::
 	(compile_constr (push_local sz reloc) body (sz+1) (add_pop 1 cont)))
   | Prod(id,dom,codom) ->
-      let cont1 = 
+      let cont1 =
 	Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
       compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
   | Lambda _ ->
@@ -503,18 +503,18 @@ let rec compile_constr reloc c sz cont =
       let arity = List.length params in
       let r_fun = comp_env_fun arity in
       let lbl_fun = Label.create() in
-      let cont_fun = 
+      let cont_fun =
 	compile_constr r_fun body arity [Kreturn arity] in
       fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
       let fv = fv r_fun in
       compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
- 
-  | App(f,args) -> 
-      begin 
+
+  | App(f,args) ->
+      begin
 	match kind_of_term f with
 	| Construct _ -> compile_str_cst reloc (str_const c) sz cont
         | Const kn -> compile_const reloc kn args sz cont
-	| _ -> comp_app compile_constr compile_constr reloc f args sz cont 
+	| _ -> comp_app compile_constr compile_constr reloc f args sz cont
       end
   | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) ->
       let ndef = Array.length type_bodies in
@@ -524,10 +524,10 @@ let rec compile_constr reloc c sz cont =
       (* Compilation des types *)
       let env_type = comp_env_type rfv in
       for i = 0 to ndef - 1 do
-	let lbl,fcode = 
-	  label_code 
-	    (compile_constr env_type type_bodies.(i) 0 [Kstop]) in 
-	lbl_types.(i) <- lbl; 
+	let lbl,fcode =
+	  label_code
+	    (compile_constr env_type type_bodies.(i) 0 [Kstop]) in
+	lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compilation des corps *)
@@ -535,7 +535,7 @@ let rec compile_constr reloc c sz cont =
 	let params,body = decompose_lam rec_bodies.(i) in
 	let arity = List.length params in
 	let env_body = comp_env_fix ndef i arity rfv in
-	let cont1 = 
+	let cont1 =
 	  compile_constr env_body body arity [Kreturn arity] in
 	let lbl = Label.create () in
 	lbl_bodies.(i) <- lbl;
@@ -543,9 +543,9 @@ let rec compile_constr reloc c sz cont =
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       let fv = !rfv in
-      compile_fv reloc fv.fv_rev sz 
+      compile_fv reloc fv.fv_rev sz
 	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
-  
+
   | CoFix(init,(_,type_bodies,rec_bodies)) ->
       let ndef = Array.length type_bodies in
       let lbl_types = Array.create ndef Label.no in
@@ -554,10 +554,10 @@ let rec compile_constr reloc c sz cont =
       let rfv = ref empty_fv in
       let env_type = comp_env_type rfv in
       for i = 0 to ndef - 1 do
-	let lbl,fcode = 
-	  label_code 
+	let lbl,fcode =
+	  label_code
 	    (compile_constr env_type type_bodies.(i) 0 [Kstop]) in
-	lbl_types.(i) <- lbl; 
+	lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compilation des corps *)
@@ -566,17 +566,17 @@ let rec compile_constr reloc c sz cont =
 	let arity = List.length params in
 	let env_body = comp_env_cofix ndef arity rfv in
 	let lbl = Label.create () in
-	let cont1 = 
+	let cont1 =
 	  compile_constr env_body body (arity+1) (cont_cofix arity) in
-	let cont2 = 
+	let cont2 =
 	  add_grab (arity+1) lbl cont1 in
 	lbl_bodies.(i) <- lbl;
 	fun_code := [Ksequence(cont2,!fun_code)];
       done;
       let fv = !rfv in
-      compile_fv reloc fv.fv_rev sz 
+      compile_fv reloc fv.fv_rev sz
 	(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
-  
+
   | Case(ci,t,a,branchs) ->
       let ind = ci.ci_ind in
       let mib = lookup_mind (fst ind) !global_env in
@@ -586,20 +586,20 @@ let rec compile_constr reloc c sz cont =
       let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in
       let branch1,cont = make_branch cont in
       (* Compilation du type *)
-      let lbl_typ,fcode = 	
+      let lbl_typ,fcode =
 	label_code (compile_constr reloc t sz [Kpop sz; Kstop])
       in fun_code := [Ksequence(fcode,!fun_code)];
-      (* Compilation des branches *) 
+      (* Compilation des branches *)
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
-	match branch1 with 
+	match branch1 with
 	| Kreturn k -> assert (k = sz); sz, branch1, true
 	| _ -> sz+3, Kjump, false
       in
       let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
      (* Compilation de la branche accumulate *)
-      let lbl_accu, code_accu = 
-	label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) 
+      let lbl_accu, code_accu =
+	label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont)
       in
       lbl_blocks.(0) <- lbl_accu;
       let c = ref code_accu in
@@ -607,14 +607,14 @@ let rec compile_constr reloc c sz cont =
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
 	if arity = 0 then
-	  let lbl_b,code_b = 
+	  let lbl_b,code_b =
 	    label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
-	  lbl_consts.(tag) <- lbl_b; 
+	  lbl_consts.(tag) <- lbl_b;
 	  c := code_b
-	else 
+	else
 	  let args, body = decompose_lam branchs.(i) in
 	  let nargs = List.length args in
-	  let lbl_b,code_b = 
+	  let lbl_b,code_b =
 	    label_code(
 	    if nargs = arity then
 	      Kpushfields arity ::
@@ -622,7 +622,7 @@ let rec compile_constr reloc c sz cont =
 		body (sz_b+arity) (add_pop arity (branch :: !c))
 	    else
 	      let sz_appterm = if is_tailcall then sz_b + arity else arity in
-	      Kpushfields arity :: 
+	      Kpushfields arity ::
 	      compile_constr reloc branchs.(i) (sz_b+arity)
 		(Kappterm(arity,sz_appterm) :: !c))
 	  in
@@ -630,21 +630,21 @@ let rec compile_constr reloc c sz cont =
 	  c := code_b
       done;
       c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
-      let code_sw = 
- 	match branch1 with 
-        (* spiwack : branch1 can't be a lbl anymore it's a Branch instead 
+      let code_sw =
+ 	match branch1 with
+        (* spiwack : branch1 can't be a lbl anymore it's a Branch instead
 	| Klabel lbl -> Kpush_retaddr lbl ::  !c *)
         | Kbranch lbl -> Kpush_retaddr lbl ::  !c
-	| _ -> !c 
+	| _ -> !c
       in
-      compile_constr reloc a sz 
-      (try 
+      compile_constr reloc a sz
+      (try
 	let entry = Term.Ind ind in
 	Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
 	                                       entry code_sw
       with Not_found ->
 	code_sw)
-       
+
 and compile_str_cst reloc sc sz cont =
   match sc with
   | Bconstr c -> compile_constr reloc c sz cont
@@ -655,25 +655,25 @@ and compile_str_cst reloc sc sz cont =
   | Bconstruct_app(tag,nparams,arity,args) ->
       if Array.length args = 0 then code_construct tag nparams arity cont
       else
-	comp_app 
-	  (fun _ _ _ cont -> code_construct tag nparams arity cont) 
+	comp_app
+	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
 	  compile_str_cst reloc () args sz cont
   | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont
 
 
-(* spiwack : compilation of constants with their arguments. 
+(* spiwack : compilation of constants with their arguments.
    Makes a special treatment with 31-bit integer addition *)
 and compile_const =
-(*arnaud:  let code_construct kn cont = 
-     let f_cont = 
+(*arnaud:  let code_construct kn cont =
+     let f_cont =
          let else_lbl = Label.create () in
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           Kaddint31:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
           Kgetglobal (get_allias !global_env kn)::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
-     in 
-     let lbl = Label.create () in 
+     in
+     let lbl = Label.create () in
      fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
   in *)
@@ -685,14 +685,14 @@ and compile_const =
   try
     Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
                   (kind_of_term (mkConst kn)) reloc args sz cont
-  with Not_found -> 
+  with Not_found ->
     if nargs = 0 then
       Kgetglobal (get_allias !global_env kn) :: cont
     else
-      comp_app (fun _ _ _ cont -> 
+      comp_app (fun _ _ _ cont ->
                    Kgetglobal (get_allias !global_env kn) :: cont)
         compile_constr reloc () args sz cont
-      
+
 let compile env c =
   set_global_env env;
   init_fun_code ();
@@ -723,8 +723,11 @@ let compile_constant_body env body opaque boxed =
 	BCdefined(true, to_patch)
       else
 	match kind_of_term body with
-	| Const kn' -> BCallias (get_allias env kn')
-	| _ -> 
+	| Const kn' ->
+	    (* we use the canonical name of the constant*)
+	    let con= constant_of_kn (canonical_con kn') in
+	      BCallias (get_allias env con)
+	| _ ->
 	    let res = compile env body in
 	    let to_patch = to_memory res in
 	    BCdefined (false, to_patch)
@@ -743,9 +746,9 @@ let make_areconst n else_lbl cont =
 (* try to compile int31 as a const_b0. Succeed if all the arguments are closed
    fails otherwise by raising NotClosed*)
 let compile_structured_int31 fc args =
-  if not fc then raise Not_found else 
+  if not fc then raise Not_found else
   Const_b0
-    (Array.fold_left 
+    (Array.fold_left
        (fun temp_i -> fun t -> match kind_of_term t with
           | Construct (_,d) -> 2*temp_i+d-1
           | _ -> raise NotClosed)
@@ -753,7 +756,7 @@ let compile_structured_int31 fc args =
     )
 
 (* this function is used for the compilation of the constructor of
-   the int31, it is used when it appears not fully applied, or 
+   the int31, it is used when it appears not fully applied, or
    applied to at least one non-closed digit *)
 let dynamic_int31_compilation fc reloc args sz cont =
   if not fc then raise Not_found else
@@ -761,32 +764,32 @@ let dynamic_int31_compilation fc reloc args sz cont =
       if nargs = 31 then
 	let (escape,labeled_cont) = make_branch cont in
 	let else_lbl = Label.create() in
-	  comp_args compile_str_cst reloc args sz 
+	  comp_args compile_str_cst reloc args sz
             ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
-      else 
+      else
 	let code_construct cont = (* spiwack: variant of the global code_construct
-                                     which handles dynamic compilation of 
+                                     which handles dynamic compilation of
                                      integers *)
-          let f_cont = 
+          let f_cont =
             let else_lbl = Label.create () in
 	      [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl);
                Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0]
-	  in 
+	  in
 	  let lbl = Label.create() in
 	    fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
 	    Kclosure(lbl,0) :: cont
-	in 
+	in
 	  if nargs = 0 then
 	    code_construct cont
 	  else
 	    comp_app (fun _ _ _ cont -> code_construct cont)
               compile_str_cst reloc () args sz cont
-       
+
 (*(* template compilation for 2ary operation, it probably possible
    to make a generic such function with arity abstracted *)
 let op2_compilation op =
   let code_construct normal cont =  (*kn cont =*)
-     let f_cont = 
+     let f_cont =
          let else_lbl = Label.create () in
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
@@ -795,7 +798,7 @@ let op2_compilation op =
           normal::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
      in
-     let lbl = Label.create () in 
+     let lbl = Label.create () in
      fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
   in
@@ -805,8 +808,8 @@ let op2_compilation op =
   if nargs=2 then (*if it is a fully applied addition*)
     let (escape, labeled_cont) = make_branch cont in
     let else_lbl = Label.create () in
-      comp_args compile_constr reloc args sz 
-	(Kisconst else_lbl::(make_areconst 1  else_lbl 
+      comp_args compile_constr reloc args sz
+	(Kisconst else_lbl::(make_areconst 1  else_lbl
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = 2 and non-tailcall cont*)
@@ -820,14 +823,14 @@ let op2_compilation op =
       compile_constr reloc () args sz cont *)
 
 (*template for n-ary operation, invariant: n>=1,
-  the operations does the following : 
-  1/ checks if all the arguments are constants (i.e. non-block values) 
+  the operations does the following :
+  1/ checks if all the arguments are constants (i.e. non-block values)
   2/ if they are, uses the "op" instruction to execute
-  3/ if at least one is not, branches to the normal behavior: 
+  3/ if at least one is not, branches to the normal behavior:
       Kgetglobal (get_allias !global_env kn) *)
 let op_compilation n op =
-  let code_construct kn cont = 
-     let f_cont = 
+  let code_construct kn cont =
+     let f_cont =
          let else_lbl = Label.create () in
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
@@ -835,7 +838,7 @@ let op_compilation n op =
           Kgetglobal (get_allias !global_env kn)::
           Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
      in
-     let lbl = Label.create () in 
+     let lbl = Label.create () in
      fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
      Kclosure(lbl, 0)::cont
   in
@@ -845,8 +848,8 @@ let op_compilation n op =
   if nargs=n then (*if it is a fully applied addition*)
     let (escape, labeled_cont) = make_branch cont in
     let else_lbl = Label.create () in
-      comp_args compile_constr reloc args sz 
-	(Kisconst else_lbl::(make_areconst (n-1) else_lbl 
+      comp_args compile_constr reloc args sz
+	(Kisconst else_lbl::(make_areconst (n-1) else_lbl
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = n and non-tailcall cont*)