Imported Upstream version 8.5~beta3+dfsg

1 files changed, 197 insertions, 69 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 07fab06a..1f7cc3c7 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -91,18 +91,20 @@ open Pre_env
 (* In Cfxe_t accumulators, we need to store [fcofixi] for testing         *)
 (* conversion of cofixpoints (which is intentional).                      *)
 
+type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
 
 let empty_fv = { size= 0;  fv_rev = [] }
 
 let fv r = !(r.in_env)
 
-let empty_comp_env ()=
-  { nb_stack = 0;
+let empty_comp_env ?(univs=0) ()=
+  { nb_uni_stack = univs;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
     offset = 0;
-    in_env = ref empty_fv;
+    in_env = ref empty_fv
   }
 
 (*i Creation functions for comp_env *)
@@ -110,8 +112,9 @@ let empty_comp_env ()=
 let rec add_param 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;
+let comp_env_fun ?(univs=0) arity =
+  { nb_uni_stack = univs ;
+    nb_stack = arity;
     in_stack = add_param arity 0 [];
     nb_rec = 0;
     pos_rec = [];
@@ -120,8 +123,9 @@ let comp_env_fun arity =
   }
 
 
-let comp_env_fix_type rfv =
-  { nb_stack = 0;
+let comp_env_fix_type  rfv =
+  { nb_uni_stack = 0;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
@@ -134,7 +138,8 @@ let comp_env_fix ndef curr_pos arity rfv =
    for i = ndef downto 1 do
      prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
    done;
-   { nb_stack = arity;
+   { nb_uni_stack = 0;
+     nb_stack = arity;
      in_stack = add_param arity 0 [];
      nb_rec = ndef;
      pos_rec = !prec;
@@ -143,7 +148,8 @@ let comp_env_fix ndef curr_pos arity rfv =
    }
 
 let comp_env_cofix_type ndef rfv =
-  { nb_stack = 0;
+  { nb_uni_stack = 0;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
@@ -156,7 +162,8 @@ let comp_env_cofix ndef arity rfv =
    for i = 1 to ndef do
      prec := Kenvacc i :: !prec
    done;
-   { nb_stack = arity;
+   { nb_uni_stack = 0;
+     nb_stack = arity;
      in_stack = add_param arity 0 [];
      nb_rec = ndef;
      pos_rec = !prec;
@@ -168,7 +175,7 @@ let comp_env_cofix ndef arity rfv =
 let push_param n sz r =
   { r with
     nb_stack = r.nb_stack + n;
-    in_stack = add_param n sz r.in_stack }
+    in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack }
 
 (* [push_local sz r] add a new variable on the stack at position [sz] *)
 let push_local sz r =
@@ -176,8 +183,6 @@ let push_local sz r =
     nb_stack = r.nb_stack + 1;
     in_stack = (sz + 1) :: r.in_stack }
 
-
-
 (*i Compilation of variables *)
 let find_at f l =
   let rec aux n = function
@@ -214,6 +219,22 @@ let pos_rel i r sz =
 	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
 	Kenvacc(r.offset + pos)
 
+let pos_universe_var i r sz =
+  if i < r.nb_uni_stack then
+    Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
+  else
+    let env = !(r.in_env) in
+    let f = function
+      | FVuniv_var u -> Int.equal i u
+      | _ -> false
+    in
+    try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+    with Not_found ->
+      let pos = env.size in
+      let db = FVuniv_var i in
+      r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+      Kenvacc(r.offset + pos)
+
 (*i  Examination of the continuation *)
 
 (* Discard all instructions up to the next label.                        *)
@@ -459,8 +480,9 @@ let rec str_const c =
               end
 	| _ -> Bconstr c
       end
-  | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct (((kn,j),i),u) ->  
+  | Ind (ind,u) when Univ.Instance.is_empty u ->
+    Bstrconst (Const_ind ind)
+  | Construct (((kn,j),i),_) ->
       begin
       (* spiwack: tries first to apply the run-time compilation
            behavior of the constructor, as in 2/ above *)
@@ -513,6 +535,7 @@ let compile_fv_elem reloc fv sz cont =
   match fv with
   | FVrel i -> pos_rel i reloc sz :: cont
   | FVnamed id -> pos_named id reloc :: cont
+  | FVuniv_var i -> pos_universe_var i reloc sz :: cont
 
 let rec compile_fv reloc l sz cont =
   match l with
@@ -524,39 +547,71 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env (kn,u as p) =
+let rec get_alias env kn =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     match tps with
-    | None -> p
+    | None -> kn
     | Some tps ->
        (match Cemitcodes.force tps with
-	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
-	| _ -> p)
-
-(* Compiling expressions *)
+	| BCalias kn' -> get_alias env kn'
+	| _ -> kn)
 
+(* sz is the size of the local stack *)
 let rec compile_constr reloc c sz cont =
   match kind_of_term c with
   | 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
+  | Proj (p,c) ->
+     let kn = Projection.constant p in
+     let cb = lookup_constant kn !global_env in
+     let pb = Option.get cb.const_proj in
+     let n = pb.proj_arg in
+     compile_constr reloc c sz (Kproj (n,kn) :: 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,u) -> compile_const reloc kn u [||] sz cont
-  | Sort _  | Ind _ | Construct _ ->
+  | Ind (ind,u) ->
+     let bcst = Bstrconst (Const_ind ind) in
+    if Univ.Instance.is_empty u then
+      compile_str_cst reloc bcst sz cont
+    else
+      comp_app compile_str_cst compile_universe reloc
+	   bcst
+	   (Univ.Instance.to_array u)
+	   sz
+	   cont
+  | Sort (Prop _) | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
-
+  | Sort (Type u) ->
+     (* We separate global and local universes in [u]. The former will be part
+        of the structured constant, while the later (if any) will be applied as
+        arguments. *)
+     let open Univ in begin
+      let levels = Universe.levels u in
+      let global_levels =
+	LSet.filter (fun x -> Level.var_index x = None) levels
+      in
+      let local_levels =
+	List.map_filter (fun x -> Level.var_index x)
+	  (LSet.elements levels)
+      in
+      (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
+      let uglob =
+	LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
+      in
+      if local_levels = [] then
+	compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont
+      else
+	let compile_get_univ reloc idx sz cont =
+	  compile_fv_elem reloc (FVuniv_var idx) sz cont
+	in
+        comp_app compile_str_cst compile_get_univ reloc
+	  (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+    end
   | LetIn(_,xb,_,body) ->
       compile_constr reloc xb sz
 	(Kpush ::
@@ -665,7 +720,9 @@ 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 (Int.equal 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
@@ -747,8 +804,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 u -> fun args -> fun sz -> fun cont ->
+and compile_get_global reloc (kn,u) sz cont =
+  let kn = get_alias !global_env kn in
+  if Univ.Instance.is_empty u then
+    Kgetglobal kn :: cont
+  else
+    comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+      compile_universe reloc () (Univ.Instance.to_array u) sz cont
+
+and compile_universe reloc uni sz cont =
+  match Univ.Level.var_index uni with
+  | None -> Kconst (Const_univ_level uni) :: cont
+  | Some idx -> pos_universe_var idx reloc sz :: cont
+
+and compile_const reloc kn u args sz 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
@@ -758,30 +827,85 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_allias !global_env (kn, u)) :: cont
+      compile_get_global reloc (kn,u) sz cont
     else
-      comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
-        compile_constr reloc () args sz cont
-
-let compile fail_on_error env c =
+      if Univ.Instance.is_empty u then
+        (* normal compilation *)
+        comp_app (fun _ _ sz cont ->
+            compile_get_global reloc (kn,u) sz cont)
+          compile_constr reloc () args sz cont
+      else
+        let compile_arg reloc constr_or_uni sz cont =
+          match constr_or_uni with
+          | ArgConstr cst -> compile_constr reloc cst sz cont
+          | ArgUniv uni -> compile_universe reloc uni sz cont
+        in
+	let u = Univ.Instance.to_array u in
+	let lu = Array.length u in
+	let all =
+	  Array.init (lu + Array.length args) 
+	    (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu))
+	in
+        comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+          compile_arg reloc () all sz cont
+
+let is_univ_copy max u =
+  let u = Univ.Instance.to_array u in
+  if Array.length u = max then
+    Array.fold_left_i (fun i acc u ->
+        if acc then
+          match Univ.Level.var_index u with
+          | None -> false
+          | Some l -> l = i
+        else false) true u
+  else
+    false
+
+let dump_bytecodes init code fvs =
+  let open Pp in
+    (str "code =" ++ fnl () ++
+     pp_bytecodes init ++ fnl () ++
+     pp_bytecodes code ++ fnl () ++
+     str "fv = " ++
+     prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
+     fnl ())
+
+let compile fail_on_error ?universes:(universes=0) env c =
   set_global_env env;
   init_fun_code ();
   Label.reset_label_counter ();
-  let reloc = empty_comp_env () in
-  try 
-    let init_code = compile_constr reloc c 0 [Kstop] in
+  let cont = [Kstop] in
+  try
+    let reloc, init_code =
+      if Int.equal universes 0 then
+        let reloc = empty_comp_env () in
+        reloc, compile_constr reloc c 0 cont
+      else
+        (* We are going to generate a lambda, but merge the universe closure
+         * with the function closure if it exists.
+         *)
+        let reloc = empty_comp_env () in
+        let arity , body =
+          match kind_of_term c with
+          | Lambda _ ->
+            let params, body = decompose_lam c in
+            List.length params , body
+          | _ -> 0 , c
+        in
+        let full_arity = arity + universes in
+        let r_fun = comp_env_fun ~univs:universes arity in
+        let lbl_fun = Label.create () in
+        let cont_fun =
+          compile_constr r_fun body full_arity [Kreturn full_arity]
+        in
+        fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
+        let fv = fv r_fun in
+        reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont)
+    in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
-(*  draw_instr init_code;
-  draw_instr !fun_code;
-  Format.print_string "fv = ";
-  List.iter (fun v ->
-    match v with
-    | 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();  *)
-      Some (init_code,!fun_code, Array.of_list fv)
+    (if !Flags.dump_bytecode then
+      Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+    Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
     let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
       (Pp.(fn
@@ -789,28 +913,33 @@ let compile fail_on_error env c =
 	    Id.print tname ++ str str_max_constructors));
        None)
 
-let compile_constant_body fail_on_error env = function
+let compile_constant_body fail_on_error env univs = function
   | Undef _ | OpaqueDef _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
+      let instance_size =
+        match univs with
+        | None -> 0
+        | Some univ -> Univ.UContext.size univ
+      in
       match kind_of_term body with
-	| Const (kn',u) ->
+	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      Some (BCallias (get_allias env (con,u)))
+	      Some (BCalias (get_alias env con))
 	| _ ->
-	    let res = compile fail_on_error env body in
+	    let res = compile fail_on_error ~universes:instance_size env body in
 	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias kn = BCalias (constant_of_kn (canonical_con kn))
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
 
 let make_areconst n else_lbl cont =
-  if n <=0 then
+  if n <= 0 then
     cont
   else
     Kareconst (n, else_lbl)::cont
@@ -867,7 +996,7 @@ let op2_compilation op =
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
-          (*Kgetglobal (get_allias !global_env kn):: *)
+          (*Kgetglobal (get_alias !global_env kn):: *)
           normal::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
      in
@@ -886,7 +1015,7 @@ let op2_compilation op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = 2 and non-tailcall cont*)
-           (*Kgetglobal (get_allias !global_env kn):: *)
+           (*Kgetglobal (get_alias !global_env kn):: *)
            normal::
            Kapply 2::labeled_cont)))
   else if nargs=0 then
@@ -900,16 +1029,16 @@ let op2_compilation op =
   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:
-      Kgetglobal (get_allias !global_env kn) *)
+      Kgetglobal (get_alias !global_env kn) *)
 let op_compilation n op =
-  let code_construct kn cont =
+  let code_construct reloc kn sz cont =
      let f_cont =
          let else_lbl = Label.create () in
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          Kgetglobal (get_allias !global_env kn)::
-          Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
+          compile_get_global reloc kn sz (
+            Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
      in
      let lbl = Label.create () in
      fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
@@ -926,12 +1055,11 @@ let op_compilation n op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = n and non-tailcall cont*)
-           Kgetglobal (get_allias !global_env kn)::
-           Kapply n::labeled_cont)))
+           compile_get_global reloc kn sz (Kapply n::labeled_cont))))
   else if Int.equal nargs 0 then
-    code_construct kn cont
+    code_construct reloc kn sz cont
   else
-    comp_app (fun _ _ _ cont -> code_construct kn cont)
+    comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
       compile_constr reloc () args sz cont
 
 let int31_escape_before_match fc cont =