Imported Upstream version 8.5~beta1+dfsg

1 files changed, 67 insertions, 57 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 56008749..d6c160c3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.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        *)
@@ -50,7 +50,7 @@ open Pre_env
 (* Access to these variables is performed by the [Koffsetclosure n]       *)
 (* instruction that shifts the environment pointer of [n] fields.         *)
 
-(* This allows to represent mutual fixpoints in just one block.           *)
+(* This allows representing mutual fixpoints in just one block.           *)
 (* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint    *)
 (* types. They are used in conversion tests (which requires that          *)
 (* fixpoint types must be convertible). Their environment is the one of   *)
@@ -108,7 +108,7 @@ let empty_comp_env ()=
 (*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)
+  if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
 
 let comp_env_fun arity =
   { nb_stack = arity;
@@ -179,16 +179,17 @@ let push_local sz r =
 
 
 (*i Compilation of variables *)
-let find_at el l =
+let find_at f l =
   let rec aux n = function
     | [] -> raise Not_found
-    | hd :: tl -> if hd = el then n else aux (n+1) tl
+    | hd :: tl -> if f hd then n else aux (n + 1) tl
   in aux 1 l
 
 let pos_named id r =
   let env = !(r.in_env) in
   let cid = FVnamed id in
-  try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
+  let f = function FVnamed id' -> Id.equal id id' | _ -> false in
+  try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
   with Not_found ->
     let pos = env.size in
     r.in_env := { size = pos+1; fv_rev =  cid:: env.fv_rev};
@@ -206,7 +207,8 @@ let pos_rel i r sz =
       let i = i - r.nb_rec in
       let db = FVrel(i) in
       let env = !(r.in_env) in
-      try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
+      let f = function FVrel j -> Int.equal i j | _ -> false in
+      try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
       with Not_found ->
 	let pos = env.size in
 	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
@@ -219,7 +221,7 @@ let pos_rel i r sz =
 (* non-terminating instruction (branch, raise, return, appterm)          *)
 (* in front of it.                                                       *)
 
-let rec discard_dead_code cont = cont
+let discard_dead_code cont = cont
 (*function
     [] -> []
   | (Klabel _ | Krestart ) :: _ as cont -> cont
@@ -280,14 +282,14 @@ let rec is_tailcall = function
 let rec add_pop n = function
   | Kpop m :: cont -> add_pop (n+m) cont
   | Kreturn m:: cont -> Kreturn (n+m) ::cont
-  | cont -> if n = 0 then cont else Kpop n :: cont
+  | cont -> if Int.equal n 0 then cont else Kpop n :: cont
 
 let add_grab arity lbl cont =
-  if arity = 1 then Klabel lbl :: cont
+  if Int.equal 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 Int.equal arity 1 && rec_arg < arity then
     Klabel lbl :: Kgrabrec 0 :: Krestart :: cont
   else
     Krestart :: Klabel lbl :: Kgrabrec rec_arg ::
@@ -331,7 +333,7 @@ let init_fun_code () = fun_code := []
 let code_construct tag nparams arity cont =
   let f_cont =
       add_pop nparams
-      (if arity = 0 then
+      (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
        else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
     in
@@ -351,13 +353,13 @@ let rec str_const c =
   | App(f,args) ->
       begin
 	match kind_of_term f with
-	| Construct((kn,j),i) -> 
+	| Construct(((kn,j),i),u) -> 
             begin
 	    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
-	    if nparams + arity = Array.length args then
+	    if Int.equal (nparams + arity) (Array.length args) then
               (* spiwack: *)
               (* 1/ tries to compile the constructor in an optimal way,
                     it is supposed to work only if the arguments are
@@ -371,7 +373,7 @@ let rec str_const c =
 		try
 		  Bstrconst (Retroknowledge.get_vm_constant_static_info
                                               (!global_env).retroknowledge
-                                              (kind_of_term f) args)
+                                              f args)
                 with NotClosed ->
 		  (* 2/ if the arguments are not all closed (this is
                         expectingly (and it is currently the case) the only
@@ -392,12 +394,12 @@ let rec str_const c =
 		  let b_args = Array.map str_const rargs in
 		  Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
-                                           (kind_of_term f)),
+                                           f),
                            b_args)
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
 		      falls back to the normal behavior *)
-		if arity = 0 then Bstrconst(Const_b0 num)
+		if Int.equal arity 0 then Bstrconst(Const_b0 num)
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
@@ -413,7 +415,7 @@ let rec str_const c =
 	      try
 		Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
                                            (!global_env).retroknowledge
-                                           (kind_of_term f)),
+                                           f),
                          b_args)
 	      with Not_found ->
 	        Bconstruct_app(num, nparams, arity, b_args)
@@ -421,21 +423,21 @@ let rec str_const c =
 	| _ -> Bconstr c
       end
   | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct ((kn,j),i) ->  
+  | Construct (((kn,j),i),u) ->  
       begin
       (* 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
                                            (!global_env).retroknowledge
-                                           (kind_of_term c)),
+                                           c),
                          [| |])
       with Not_found ->
 	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
-	if nparams + arity = 0 then Bstrconst(Const_b0 num)
+	if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
 	else Bconstruct_app(num,nparams,arity,[||])
       end
   | _ -> Bconstr c
@@ -484,25 +486,33 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env kn =
-  let tps = (lookup_constant kn env).const_body_code in
-  match Cemitcodes.force tps with
-  | BCallias kn' -> get_allias env kn'
-  | _ -> kn
-
+let rec get_allias env (kn,u as p) =
+  let cb = lookup_constant kn env in
+  let tps = cb.const_body_code in
+    (match Cemitcodes.force tps with
+    | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+    | _ -> p)
 
 (* Compiling 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")
+  | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
+  | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
+  | Proj (p,c) -> 
+    (* compile_const reloc p [|c|] sz cont *)
+    let kn = Projection.constant p in
+    let cb = lookup_constant kn !global_env in
+      (* TODO: better representation of projections *)
+    let pb = Option.get cb.const_proj in
+    let args = Array.make pb.proj_npars mkProp in
+      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
   | Rel i -> pos_rel i reloc sz :: cont
   | Var id -> pos_named id reloc :: cont
-  | Const kn -> compile_const reloc kn [||] sz cont
+  | Const (kn,u) -> compile_const reloc kn u [||] sz cont
   | Sort _  | Ind _ | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
 
@@ -529,14 +539,14 @@ let rec compile_constr reloc c sz cont =
       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
+        | Const (kn,u) -> compile_const reloc kn u 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
       let rfv = ref empty_fv in
-      let lbl_types = Array.create ndef Label.no in
-      let lbl_bodies = Array.create ndef Label.no in
+      let lbl_types = Array.make ndef Label.no in
+      let lbl_bodies = Array.make ndef Label.no in
       (* Compilation des types *)
       let env_type = comp_env_fix_type rfv in
       for i = 0 to ndef - 1 do
@@ -564,8 +574,8 @@ let rec compile_constr reloc c sz cont =
 
   | CoFix(init,(_,type_bodies,rec_bodies)) ->
       let ndef = Array.length type_bodies in
-      let lbl_types = Array.create ndef Label.no in
-      let lbl_bodies = Array.create ndef Label.no in
+      let lbl_types = Array.make ndef Label.no in
+      let lbl_bodies = Array.make ndef Label.no in
       (* Compiling types *)
       let rfv = ref empty_fv in
       let env_type = comp_env_cofix_type ndef rfv in
@@ -598,8 +608,8 @@ let rec compile_constr reloc c sz cont =
       let mib = lookup_mind (fst ind) !global_env in
       let oib = mib.mind_packets.(snd ind) in
       let tbl = oib.mind_reloc_tbl in
-      let lbl_consts = Array.create oib.mind_nb_constant Label.no in
-      let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in
+      let lbl_consts = Array.make oib.mind_nb_constant Label.no in
+      let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in
       let branch1,cont = make_branch cont in
       (* Compiling return type *)
       let lbl_typ,fcode =
@@ -609,7 +619,7 @@ let rec compile_constr reloc c sz cont =
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
 	match branch1 with
-	| Kreturn k -> assert (k = sz); sz, branch1, true
+	| Kreturn k -> assert (Int.equal k sz); sz, branch1, true
 	| _ -> sz+3, Kjump, false
       in
       let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -622,7 +632,7 @@ let rec compile_constr reloc c sz cont =
       (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
-	if arity = 0 then
+	if Int.equal arity 0 then
 	  let lbl_b,code_b =
 	    label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
 	  lbl_consts.(tag) <- lbl_b;
@@ -632,7 +642,7 @@ let rec compile_constr reloc c sz cont =
 	  let nargs = List.length args in
 	  let lbl_b,code_b =
 	    label_code(
-	    if nargs = arity then
+	    if Int.equal nargs arity then
 	      Kpushfields arity ::
 	      compile_constr (push_param arity sz_b reloc)
 		body (sz_b+arity) (add_pop arity (branch :: !c))
@@ -655,7 +665,7 @@ let rec compile_constr reloc c sz cont =
       in
       compile_constr reloc a sz
       (try
-	let entry = Term.Ind ind in
+	let entry = mkInd ind in
 	Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
 	                                       entry code_sw
       with Not_found ->
@@ -669,7 +679,7 @@ and compile_str_cst reloc sc sz cont =
       let nargs = Array.length args in
       comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if Array.length args = 0 then code_construct tag nparams arity cont
+      if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
       else
 	comp_app
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -680,20 +690,20 @@ and compile_str_cst reloc sc sz cont =
 (* spiwack : compilation of constants with their arguments.
    Makes a special treatment with 31-bit integer addition *)
 and compile_const =
-  fun reloc-> fun  kn -> fun args -> fun sz -> fun cont ->
+  fun reloc-> fun  kn u -> fun args -> fun sz -> fun cont ->
   let nargs = Array.length args in
   (* spiwack: checks if there is a specific way to compile the constant
               if there is not, Not_found is raised, and the function
               falls back on its normal behavior *)
   try
     Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
-                  (kind_of_term (mkConst kn)) reloc args sz cont
+                  (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
-    if nargs = 0 then
-      Kgetglobal (get_allias !global_env kn) :: cont
+    if Int.equal nargs 0 then
+      Kgetglobal (get_allias !global_env (kn, u)) :: cont
     else
       comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env kn) :: cont)
+                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
 let compile env c =
@@ -708,7 +718,7 @@ let compile env c =
   Format.print_string "fv = ";
   List.iter (fun v ->
     match v with
-    | FVnamed id -> Format.print_string ((string_of_id id)^"; ")
+    | FVnamed id -> Format.print_string ((Id.to_string id)^"; ")
     | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv;  Format
     .print_string "\n";
   Format.print_flush();  *)
@@ -717,12 +727,12 @@ let compile env c =
 let compile_constant_body env = function
   | Undef _ | OpaqueDef _ -> BCconstant
   | Def sb ->
-      let body = Declarations.force sb in
+      let body = Mod_subst.force_constr sb in
       match kind_of_term body with
-	| Const kn' ->
+	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      BCallias (get_allias env con)
+	      BCallias (get_allias env (con,u))
 	| _ ->
 	    let res = compile env body in
 	    let to_patch = to_memory res in
@@ -730,7 +740,7 @@ let compile_constant_body env = function
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias kn = BCallias (constant_of_kn (canonical_con kn))
+let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
@@ -749,7 +759,7 @@ let compile_structured_int31 fc args =
   Const_b0
     (Array.fold_left
        (fun temp_i -> fun t -> match kind_of_term t with
-          | Construct (_,d) -> 2*temp_i+d-1
+          | Construct ((_,d),_) -> 2*temp_i+d-1
           | _ -> raise NotClosed)
        0 args
     )
@@ -760,7 +770,7 @@ let compile_structured_int31 fc args =
 let dynamic_int31_compilation fc reloc args sz cont =
   if not fc then raise Not_found else
     let nargs = Array.length args in
-      if nargs = 31 then
+      if Int.equal 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
@@ -778,7 +788,7 @@ let dynamic_int31_compilation fc reloc args sz cont =
 	    fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
 	    Kclosure(lbl,0) :: cont
 	in
-	  if nargs = 0 then
+	  if Int.equal nargs 0 then
 	    code_construct cont
 	  else
 	    comp_app (fun _ _ _ cont -> code_construct cont)
@@ -844,7 +854,7 @@ let op_compilation n op =
   fun kn fc reloc args sz cont ->
   if not fc then raise Not_found else
   let nargs = Array.length args in
-  if nargs=n then (*if it is a fully applied addition*)
+  if Int.equal 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
@@ -854,7 +864,7 @@ let op_compilation n op =
            (* works as comp_app with nargs = n and non-tailcall cont*)
            Kgetglobal (get_allias !global_env kn)::
            Kapply n::labeled_cont)))
-  else if nargs=0 then
+  else if Int.equal nargs 0 then
     code_construct kn cont
   else
     comp_app (fun _ _ _ cont -> code_construct kn cont)