aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml62
-rw-r--r--kernel/cbytecodes.mli17
-rw-r--r--kernel/cbytegen.ml689
-rw-r--r--kernel/cbytegen.mli29
-rw-r--r--kernel/cemitcodes.ml424
-rw-r--r--kernel/cemitcodes.mli14
-rw-r--r--kernel/cinstr.mli43
-rw-r--r--kernel/clambda.ml853
-rw-r--r--kernel/clambda.mli27
-rw-r--r--kernel/csymtable.ml65
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/environ.ml10
-rw-r--r--kernel/kernel.mllib3
-rw-r--r--kernel/mod_typing.ml27
-rw-r--r--kernel/nativelambda.ml17
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/retroknowledge.ml10
-rw-r--r--kernel/retroknowledge.mli26
-rw-r--r--kernel/subtyping.ml9
-rw-r--r--kernel/univ.ml44
-rw-r--r--kernel/univ.mli10
-rw-r--r--kernel/vmvalues.ml11
22 files changed, 1567 insertions, 827 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 9febc6449b..aa6c49bc79 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -45,6 +45,55 @@ type reloc_table = (tag * int) array
type annot_switch =
{ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+let rec eq_structured_constant c1 c2 = match c1, c2 with
+| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_sorts _, _ -> false
+| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
+| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
+| Const_bn (t1, a1), Const_bn (t2, a2) ->
+ Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2
+| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
+
+let rec hash_structured_constant c =
+ let open Hashset.Combine in
+ match c with
+ | Const_sorts s -> combinesmall 1 (Sorts.hash s)
+ | Const_ind i -> combinesmall 2 (ind_hash i)
+ | Const_proj p -> combinesmall 3 (Constant.hash p)
+ | Const_b0 t -> combinesmall 4 (Int.hash t)
+ | Const_bn (t, a) ->
+ let fold h c = combine h (hash_structured_constant c) in
+ let h = Array.fold_left fold 0 a in
+ combinesmall 5 (combine (Int.hash t) h)
+ | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+ | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
+
+let eq_annot_switch asw1 asw2 =
+ let eq_ci ci1 ci2 =
+ eq_ind ci1.ci_ind ci2.ci_ind &&
+ Int.equal ci1.ci_npar ci2.ci_npar &&
+ CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
+ in
+ let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
+ eq_ci asw1.ci asw2.ci &&
+ CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
+ (asw1.tailcall : bool) == asw2.tailcall
+
+let hash_annot_switch asw =
+ let open Hashset.Combine in
+ let h1 = Constr.case_info_hash asw.ci in
+ let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+ let h3 = if asw.tailcall then 1 else 0 in
+ combine3 h1 h2 h3
+
module Label =
struct
type t = int
@@ -301,16 +350,3 @@ and pp_bytecodes c =
pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
| i :: c ->
pp_instr i ++ fnl () ++ pp_bytecodes c
-
-(*spiwack: moved this type in this file because I needed it for
- retroknowledge which can't depend from cbytegen *)
-type block =
- | Bconstr of constr
- | Bstrconst of structured_constant
- | Bmakeblock of int * block array
- | Bconstruct_app of int * int * int * block array
- (* tag , nparams, arity *)
- | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
- (* spiwack: compilation given by a function *)
- (* compilation function (see get_vm_constant_dynamic_info in
- retroknowledge.mli for more info) , argument array *)
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 5d37a5840b..c8fbb27a99 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -41,6 +41,12 @@ type reloc_table = (tag * int) array
type annot_switch =
{ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+val eq_structured_constant : structured_constant -> structured_constant -> bool
+val hash_structured_constant : structured_constant -> int
+
+val eq_annot_switch : annot_switch -> annot_switch -> bool
+val hash_annot_switch : annot_switch -> int
+
module Label :
sig
type t = int
@@ -165,14 +171,3 @@ type comp_env = {
val pp_bytecodes : bytecodes -> Pp.t
val pp_fv_elem : fv_elem -> Pp.t
-
-(*spiwack: moved this here because I needed it for retroknowledge *)
-type block =
- | Bconstr of constr
- | Bstrconst of structured_constant
- | Bmakeblock of int * block array
- | Bconstruct_app of int * int * int * block array
- (** tag , nparams, arity *)
- | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
- (** compilation function (see get_vm_constant_dynamic_info in
- retroknowledge.mli for more info) , argument array *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5dab2932d7..3104d57514 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -14,6 +14,8 @@ open Util
open Names
open Cbytecodes
open Cemitcodes
+open Cinstr
+open Clambda
open Constr
open Declarations
open Pre_env
@@ -96,7 +98,7 @@ module Config = struct
let stack_safety_margin = 15
end
-type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
+type argument = ArgLambda of lambda | ArgUniv of Univ.Level.t
let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty }
let push_fv d e = {
@@ -356,13 +358,6 @@ let cont_cofix arity =
Kreturn (arity+2) ]
-(*i Global environment *)
-
-let global_env = ref empty_env
-
-let set_global_env env = global_env := env
-
-
(* Code of closures *)
let fun_code = ref []
@@ -370,31 +365,8 @@ let init_fun_code () = fun_code := []
(* Compilation of constructors and inductive types *)
-
-(* Limitation due to OCaml's representation of non-constant
- constructors: limited to 245 + 1 (0 tag) cases. *)
-
-exception TooLargeInductive of Id.t
-
-let max_nb_const = 0x1000000
-let max_nb_block = 0x1000000 + last_variant_tag - 1
-
-let str_max_constructors =
- Format.sprintf
- " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
-
-let check_compilable ib =
-
- if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then
- raise (TooLargeInductive ib.mind_typename)
-
(* Inv: arity > 0 *)
-let const_bn tag args =
- if tag < last_variant_tag then Const_bn(tag, args)
- else
- Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
-
(*
If [tag] hits the OCaml limitation for non constant constructors, we switch to
another representation for the remaining constructors:
@@ -415,126 +387,9 @@ let code_makeblock ~stack_size ~arity ~tag cont =
Kpush :: nest_block tag arity cont
end
-(* [code_construct] compiles an abstracted constructor dropping parameters and
- updates [fun_code] *)
-(* Inv : nparam + arity > 0 *)
-let code_construct tag nparams arity cont =
- let f_cont =
- add_pop nparams
- (if Int.equal arity 0 then
- [Kconst (Const_b0 tag); Kreturn 0]
- else if tag < last_variant_tag then
- [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
- else
- nest_block tag arity [Kreturn 0])
- in
- let lbl = Label.create() in
- (* No need to grow the stack here, as the function does not push stuff. *)
- 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
-
-let rec str_const c =
- match kind c with
- | Sort s -> Bstrconst (Const_sorts s)
- | Cast(c,_,_) -> str_const c
- | App(f,args) ->
- begin
- match kind f with
- | Construct(((kn,j),i),u) ->
- begin
- let oib = lookup_mind kn !global_env in
- let oip = oib.mind_packets.(j) in
- let () = check_compilable oip in
- let tag,arity = oip.mind_reloc_tbl.(i-1) in
- let nparams = oib.mind_nparams in
- 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
- 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
- a processor number (a caml number actually) *)
- try
- try
- Bstrconst (Retroknowledge.get_vm_constant_static_info
- (!global_env).retroknowledge
- 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
- 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
- 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
- during the execution *)
- let rargs = Array.sub args nparams arity in
- let b_args = Array.map str_const rargs in
- Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
- (!global_env).retroknowledge
- f),
- b_args)
- with Not_found ->
- (* 3/ if no special behavior is available, then the compiler
- falls back to the normal behavior *)
- if Int.equal arity 0 then Bstrconst(Const_b0 tag)
- else
- let rargs = Array.sub args nparams arity in
- let b_args = Array.map str_const rargs in
- try
- let sc_args = Array.map get_strcst b_args in
- Bstrconst(const_bn tag sc_args)
- with Not_found ->
- Bmakeblock(tag,b_args)
- 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
- Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
- (!global_env).retroknowledge
- f),
- b_args)
- with Not_found ->
- Bconstruct_app(tag, nparams, arity, b_args)
- end
- | _ -> Bconstr c
- end
- | 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 *)
- try
- Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
- (!global_env).retroknowledge
- c),
- [| |])
- with Not_found ->
- let oib = lookup_mind kn !global_env in
- let oip = oib.mind_packets.(j) in
- let () = check_compilable oip in
- let num,arity = oip.mind_reloc_tbl.(i-1) in
- let nparams = oib.mind_nparams in
- if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
- else Bconstruct_app(num,nparams,arity,[||])
- end
- | _ -> Bconstr c
+let compile_structured_constant reloc sc sz cont =
+ set_max_stack_size sz;
+ Kconst sc :: cont
(* compiling application *)
let comp_args comp_expr reloc args sz cont =
@@ -545,9 +400,10 @@ let comp_args comp_expr reloc args sz cont =
done;
!c
-(* Precondition: args not empty *)
let comp_app comp_fun comp_arg reloc f args sz cont =
let nargs = Array.length args in
+ if Int.equal nargs 0 then comp_fun reloc f sz cont
+ else
match is_tailcall cont with
| Some k ->
comp_args comp_arg reloc args sz
@@ -593,112 +449,105 @@ let rec get_alias env kn =
| BCalias kn' -> get_alias env kn'
| _ -> 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
+ cont
+ else
+ Kareconst (n, else_lbl)::cont
+
(* sz is the size of the local stack *)
-let rec compile_constr reloc c sz cont =
+let rec compile_lam env reloc lam sz cont =
set_max_stack_size sz;
- match kind c with
- | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
- | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
- | 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
- | Ind (ind,u) ->
- let bcst = Bstrconst (Const_ind ind) in
+ match lam with
+ | Lrel(_, i) -> pos_rel i reloc sz :: cont
+
+ | Lval v -> compile_structured_constant reloc v sz cont
+
+ | Lproj (n,kn,arg) ->
+ compile_lam env reloc arg sz (Kproj (n,kn) :: cont)
+
+ | Lvar id -> pos_named id reloc :: cont
+
+ | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont
+
+ | Lind (ind,u) ->
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 (Sorts.Prop _) | Construct _ ->
- compile_str_cst reloc (str_const c) sz cont
- | Sort (Sorts.Type u) ->
+ compile_structured_constant reloc (Const_ind ind) sz cont
+ else comp_app compile_structured_constant compile_universe reloc
+ (Const_ind ind) (Univ.Instance.to_array u) sz cont
+
+ | Lsort (Sorts.Prop _ as s) ->
+ compile_structured_constant reloc (Const_sorts s) sz cont
+ | Lsort (Sorts.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
+ let u,s = Universe.compact u 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 (Sorts.Type uglob))) sz cont
+ if List.is_empty s then
+ compile_structured_constant reloc (Const_sorts (Sorts.Type u)) sz cont
else
let compile_get_univ reloc idx sz cont =
set_max_stack_size sz;
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
+ comp_app compile_structured_constant compile_get_univ reloc
+ (Const_type u) (Array.of_list s) sz cont
end
- | LetIn(_,xb,_,body) ->
- 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 =
- Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
- compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
- | Lambda _ ->
- let params, body = Term.decompose_lam c in
- let arity = List.length params in
- let r_fun = comp_env_fun arity in
- let lbl_fun = Label.create() in
- let cont_fun =
- ensure_stack_capacity (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
- match kind f with
- | Construct _ -> compile_str_cst reloc (str_const c) 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
+
+ | Llet (id,def,body) ->
+ compile_lam env reloc def sz
+ (Kpush ::
+ compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont))
+
+ | Lprod (dom,codom) ->
+ let cont1 =
+ Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in
+ compile_lam env reloc codom sz cont1
+
+ | Llam (ids,body) ->
+ let arity = Array.length ids in
+ let r_fun = comp_env_fun arity in
+ let lbl_fun = Label.create() in
+ let cont_fun =
+ ensure_stack_capacity (compile_lam env 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)
+
+ | Lapp (f, args) ->
+ begin match f with
+ | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont
+ | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont
+ end
+
+ | Lfix ((rec_args, init), (decl, types, bodies)) ->
+ let ndef = Array.length types in
let rfv = ref empty_fv in
let lbl_types = Array.make ndef Label.no in
let lbl_bodies = Array.make ndef Label.no in
- (* Compilation des types *)
+ (* Compiling types *)
let env_type = comp_env_fix_type rfv in
for i = 0 to ndef - 1 do
let fcode =
- ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop]
+ ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop]
in
- let lbl,fcode = label_code fcode in
- lbl_types.(i) <- lbl;
+ let lbl,fcode = label_code fcode in
+ lbl_types.(i) <- lbl;
fun_code := [Ksequence(fcode,!fun_code)]
done;
(* Compiling bodies *)
for i = 0 to ndef - 1 do
- let params,body = Term.decompose_lam rec_bodies.(i) in
- let arity = List.length params in
+ let params,body = decompose_Llam bodies.(i) in
+ let arity = Array.length params in
let env_body = comp_env_fix ndef i arity rfv in
- let cont1 =
- ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity]
+ let cont1 =
+ ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity]
in
let lbl = Label.create () in
lbl_bodies.(i) <- lbl;
@@ -709,8 +558,9 @@ let rec compile_constr reloc c sz cont =
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
+
+ | Lcofix(init, (decl,types,bodies)) ->
+ let ndef = Array.length types in
let lbl_types = Array.make ndef Label.no in
let lbl_bodies = Array.make ndef Label.no in
(* Compiling types *)
@@ -718,22 +568,22 @@ let rec compile_constr reloc c sz cont =
let env_type = comp_env_cofix_type ndef rfv in
for i = 0 to ndef - 1 do
let fcode =
- ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop]
+ ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop]
in
- let lbl,fcode = label_code fcode in
- lbl_types.(i) <- lbl;
+ let lbl,fcode = label_code fcode in
+ lbl_types.(i) <- lbl;
fun_code := [Ksequence(fcode,!fun_code)]
done;
(* Compiling bodies *)
for i = 0 to ndef - 1 do
- let params,body = Term.decompose_lam rec_bodies.(i) in
- let arity = List.length params in
+ let params,body = decompose_Llam bodies.(i) in
+ let arity = Array.length params in
let env_body = comp_env_cofix ndef arity rfv in
let lbl = Label.create () in
let comp arity =
(* 4 stack slots are needed to update the cofix when forced *)
set_max_stack_size (arity + 4);
- compile_constr env_body body (arity+1) (cont_cofix arity)
+ compile_lam env env_body body (arity+1) (cont_cofix arity)
in
let cont = ensure_stack_capacity comp arity in
lbl_bodies.(i) <- lbl;
@@ -744,33 +594,34 @@ let rec compile_constr reloc c sz cont =
compile_fv reloc fv.fv_rev sz
(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
- | Case(ci,t,a,branchs) ->
+
+ | Lcase(ci,rtbl,t,a,branches) ->
let ind = ci.ci_ind in
- let mib = lookup_mind (fst ind) !global_env in
+ let mib = lookup_mind (fst ind) env in
let oib = mib.mind_packets.(snd ind) in
- let () = check_compilable oib in
- let tbl = oib.mind_reloc_tbl in
let lbl_consts = Array.make oib.mind_nb_constant Label.no in
let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+ let nconst = Array.length branches.constant_branches in
let nblock = min nallblock (last_variant_tag + 1) in
let lbl_blocks = Array.make nblock Label.no in
let neblock = max 0 (nallblock - last_variant_tag) in
let lbl_eblocks = Array.make neblock Label.no in
- let branch1,cont = make_branch cont in
- (* Compiling return type *)
+ let branch1, cont = make_branch cont in
+ (* Compilation of the return type *)
let fcode =
- ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop]
+ ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop]
in
let lbl_typ,fcode = label_code fcode in
fun_code := [Ksequence(fcode,!fun_code)];
- (* Compiling branches *)
+ (* Compilation of the branches *)
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
- | _ -> sz+3, Kjump, false
+ match branch1 with
+ | Kreturn k ->
+ assert (Int.equal k sz) ;
+ sz, branch1, true
+ | Kbranch _ -> sz+3, Kjump, false
+ | _ -> assert false
in
let c = ref cont in
@@ -781,29 +632,26 @@ let rec compile_constr reloc c sz cont =
Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
lbl_blocks.(last_variant_tag) <- lbl_b;
c := code_b
- end;
-
- (* Compiling regular constructor branches *)
- for i = 0 to Array.length tbl - 1 do
- let tag, arity = tbl.(i) in
- 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;
- c := code_b
- else
- let args, body = Term.decompose_lam branchs.(i) in
- let nargs = List.length args in
-
- let code_b =
- if Int.equal nargs arity then
- compile_constr (push_param arity sz_b reloc)
- body (sz_b+arity) (add_pop arity (branch :: !c))
- else
- let sz_appterm = if is_tailcall then sz_b + arity else arity in
- compile_constr reloc branchs.(i) (sz_b+arity)
- (Kappterm(arity,sz_appterm) :: !c) in
- let code_b =
+ end;
+
+ (* Compilation of constant branches *)
+ for i = nconst - 1 downto 0 do
+ let aux =
+ compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c)
+ in
+ let lbl_b,code_b = label_code aux in
+ lbl_consts.(i) <- lbl_b;
+ c := code_b
+ done;
+ (* -1 for accu branch *)
+ for i = nallblock - 2 downto 0 do
+ let tag = i + 1 in
+ let (ids, body) = branches.nonconstant_branches.(i) in
+ let arity = Array.length ids in
+ let code_b =
+ compile_lam env (push_param arity sz_b reloc)
+ body (sz_b+arity) (add_pop arity (branch::!c)) in
+ let code_b =
if tag < last_variant_tag then begin
set_max_stack_size (sz_b + arity);
Kpushfields arity :: code_b
@@ -812,15 +660,15 @@ let rec compile_constr reloc c sz cont =
set_max_stack_size (sz_b + arity + 1);
Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b
end
- in
- let lbl_b,code_b = label_code code_b in
- if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
+ in
+ let lbl_b, code_b = label_code code_b in
+ if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
- c := code_b
+ c := code_b
done;
let annot =
- {ci = ci; rtbl = tbl; tailcall = is_tailcall;
+ {ci = ci; rtbl = rtbl; tailcall = is_tailcall;
max_stack_size = !max_stack_size - sz}
in
@@ -839,38 +687,50 @@ let rec compile_constr reloc c sz cont =
| Kbranch lbl -> Kpush_retaddr lbl :: !c
| _ -> !c
in
- compile_constr reloc a sz
- (try
- let entry = mkInd 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 =
- set_max_stack_size sz;
- match sc with
- | Bconstr c -> compile_constr reloc c sz cont
- | Bstrconst sc -> Kconst sc :: cont
- | Bmakeblock(tag,args) ->
- let arity = Array.length args in
- let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
- comp_args compile_str_cst reloc args sz cont
- | Bconstruct_app(tag,nparams,arity,args) ->
- 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)
- compile_str_cst reloc () args sz cont
- | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont
+ compile_lam env reloc a sz code_sw
+
+ | Lmakeblock (tag,args) ->
+ let arity = Array.length args in
+ let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
+ comp_args (compile_lam env) reloc args sz cont
+
+ | Lprim (kn, ar, op, args) ->
+ op_compilation env ar op kn reloc args sz cont
+
+ | Luint v ->
+ (match v with
+ | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont
+ | UintDigits ds ->
+ let nargs = Array.length ds in
+ if Int.equal nargs 31 then
+ let (escape,labeled_cont) = make_branch cont in
+ let else_lbl = Label.create() in
+ comp_args (compile_lam env) reloc ds sz
+ ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
+ else
+ let code_construct cont = (* spiwack: variant of the global code_construct
+ which handles dynamic compilation of
+ integers *)
+ 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
+ let lbl = Label.create() in
+ fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
+ Kclosure(lbl,0) :: cont
+ in
+ comp_app (fun _ _ _ cont -> code_construct cont)
+ (compile_lam env) reloc () ds sz cont
+ | UintDecomp t ->
+ let escape_lbl, labeled_cont = label_code cont in
+ compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
(* spiwack : compilation of constants with their arguments.
Makes a special treatment with 31-bit integer addition *)
and compile_get_global reloc (kn,u) sz cont =
set_max_stack_size sz;
- let kn = get_alias !global_env kn in
if Univ.Instance.is_empty u then
Kgetglobal kn :: cont
else
@@ -880,41 +740,67 @@ and compile_get_global reloc (kn,u) sz cont =
and compile_universe reloc uni sz cont =
set_max_stack_size sz;
match Univ.Level.var_index uni with
- | None -> Kconst (Const_univ_level uni) :: cont
+ | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont
| Some idx -> pos_universe_var idx reloc sz :: cont
-and compile_const reloc kn u args sz cont =
+and compile_constant env reloc kn u args sz cont =
set_max_stack_size sz;
+ if Univ.Instance.is_empty u then
+ (* normal compilation *)
+ comp_app (fun _ _ sz cont ->
+ compile_get_global reloc (kn,u) sz cont)
+ (compile_lam env) reloc () args sz cont
+ else
+ let compile_arg reloc constr_or_uni sz cont =
+ match constr_or_uni with
+ | ArgLambda t -> compile_lam env reloc t 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 ArgLambda args.(i-lu))
+ in
+ comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+ compile_arg reloc () all 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)
+ 2/ if they are, uses the "op" instruction to execute
+ 3/ if at least one is not, branches to the normal behavior:
+ Kgetglobal (get_alias !global_env kn) *)
+and op_compilation env n op =
+ 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]*)
+ 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)];
+ Kclosure(lbl, 0)::cont
+ in
+ fun kn reloc 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
- falls back on its normal behavior *)
- try
- Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
- (mkConstU (kn,u)) reloc args sz cont
- with Not_found ->
- if Int.equal nargs 0 then
- compile_get_global reloc (kn,u) sz cont
- else
- 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
+ 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
+ assert (n < 4);
+ comp_args (compile_lam env) 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 < 4 and non-tailcall cont*)
+ compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont))))
+ else
+ comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
+ (compile_lam env) reloc () args sz cont
+
let is_univ_copy max u =
let u = Univ.Instance.to_array u in
@@ -937,33 +823,29 @@ let dump_bytecodes init code fvs =
prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
fnl ())
-let compile fail_on_error ?universes:(universes=0) env c =
- set_global_env env;
+let compile ~fail_on_error ?universes:(universes=0) env c =
init_fun_code ();
Label.reset_label_counter ();
let cont = [Kstop] in
try
let reloc, init_code =
if Int.equal universes 0 then
+ let lam = lambda_of_constr ~optimize:true env c in
let reloc = empty_comp_env () in
- reloc, ensure_stack_capacity (compile_constr reloc c 0) cont
+ reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont
else
(* We are going to generate a lambda, but merge the universe closure
* with the function closure if it exists.
*)
+ let lam = lambda_of_constr ~optimize:true env c in
+ let params, body = decompose_Llam lam in
+ let arity = Array.length params in
let reloc = empty_comp_env () in
- let arity , body =
- match kind c with
- | Lambda _ ->
- let params, body = Term.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 =
- ensure_stack_capacity (compile_constr r_fun body full_arity)
+ ensure_stack_capacity (compile_lam env r_fun body full_arity)
[Kreturn full_arity]
in
fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
@@ -978,15 +860,12 @@ let compile fail_on_error ?universes:(universes=0) env c =
(if !Flags.dump_bytecode then
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
- with TooLargeInductive tname ->
+ with TooLargeInductive msg ->
let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else
- (fun x -> Feedback.msg_warning x) in
- (Pp.(fn
- (str "Cannot compile code for virtual machine as it uses inductive " ++
- Id.print tname ++ str str_max_constructors));
- None)
+ (fun x -> Feedback.msg_warning x) in
+ fn msg; None
-let compile_constant_body fail_on_error env univs = 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
@@ -1001,65 +880,13 @@ let compile_constant_body fail_on_error env univs = function
let con= Constant.make1 (Constant.canonical kn') in
Some (BCalias (get_alias env con))
| _ ->
- let res = compile fail_on_error ~universes:instance_size 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 = BCalias (Constant.make1 (Constant.canonical 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
- cont
- else
- Kareconst (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
- Const_b0
- (Array.fold_left
- (fun temp_i -> fun t -> match kind t with
- | Construct ((_,d),_) -> 2*temp_i+d-1
- | _ -> raise NotClosed)
- 0 args
- )
-
-(* this function is used for the compilation of the constructor of
- 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
- let nargs = Array.length args in
- 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
- ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
- else
- let code_construct cont = (* spiwack: variant of the global code_construct
- which handles dynamic compilation of
- integers *)
- 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
- let lbl = Label.create() in
- fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
- Kclosure(lbl,0) :: cont
- in
- if Int.equal 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 =
@@ -1097,47 +924,3 @@ let op2_compilation op =
comp_app (fun _ _ _ cont -> code_construct normal cont)
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)
- 2/ if they are, uses the "op" instruction to execute
- 3/ if at least one is not, branches to the normal behavior:
- Kgetglobal (get_alias !global_env kn) *)
-let op_compilation n op =
- 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]*)
- 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)];
- Kclosure(lbl, 0)::cont
- in
- fun kn fc reloc args sz cont ->
- if not fc then raise Not_found else
- let nargs = Array.length args in
- 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
- (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*)
- compile_get_global reloc kn sz (Kapply n::labeled_cont))))
- else if Int.equal nargs 0 then
- code_construct reloc kn sz cont
- else
- 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 =
- if not fc then
- raise Not_found
- else
- let escape_lbl, labeled_cont = label_code cont in
- (Kisconst escape_lbl)::Kdecompint31::labeled_cont
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index c117d3fb57..99f2a3c01a 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,38 +13,13 @@ open Declarations
open Pre_env
(** Should only be used for monomorphic terms *)
-val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
+val compile : fail_on_error:bool ->
?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
(** init, fun, fv *)
-val compile_constant_body : bool ->
+val compile_constant_body : fail_on_error:bool ->
env -> constant_universes -> constant_def -> body_code option
(** Shortcut of the previous function used during module strengthening *)
val compile_alias : Names.Constant.t -> body_code
-
-(** spiwack: this function contains the information needed to perform
- the static compilation of int31 (trying and obtaining
- a 31-bit integer in processor representation at compile time) *)
-val compile_structured_int31 : bool -> constr array ->
- structured_constant
-
-(** this function contains the information needed to perform
- the dynamic compilation of int31 (trying and obtaining a
- 31-bit integer in processor representation at runtime when
- it failed at compile time *)
-val dynamic_int31_compilation : bool -> comp_env ->
- block array ->
- int -> bytecodes -> bytecodes
-
-(*spiwack: template for the compilation n-ary operation, invariant: n>=1.
- works as follow: checks if all the arguments are non-pointers
- if they are applies the operation (second argument) if not
- all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
- constr array -> int -> bytecodes-> bytecodes
-
-(*spiwack: compiling function to insert dynamic decompilation before
- matching integers (in case they are in processor representation) *)
-val int31_escape_before_match : bool -> bytecodes -> bytecodes
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index eeea19c12b..856b0b465c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,18 +10,51 @@
machine, Oct 2004 *)
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
+open Names
open Term
open Cbytecodes
open Copcodes
open Mod_subst
+type emitcodes = String.t
+
+external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+
(* Relocation information *)
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
| Reloc_getglobal of Names.Constant.t
-type patch = reloc_info * int
+let eq_reloc_info r1 r2 = match r1, r2 with
+| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
+| Reloc_annot _, _ -> false
+| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2
+| Reloc_const _, _ -> false
+| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
+| Reloc_getglobal _, _ -> false
+
+let hash_reloc_info r =
+ let open Hashset.Combine in
+ match r with
+ | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
+ | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
+ | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+
+module RelocTable = Hashtbl.Make(struct
+ type t = reloc_info
+ let equal = eq_reloc_info
+ let hash = hash_reloc_info
+end)
+
+(** We use arrays for on-disk representation. On 32-bit machines, this means we
+ can only have a maximum amount of about 4.10^6 relocations, which seems
+ quite a lot, but potentially reachable if e.g. compiling big proofs. This
+ would prevent VM computing with these terms on 32-bit architectures. Maybe
+ we should use a more robust data structure? *)
+type patches = {
+ reloc_infos : (reloc_info * int array) array;
+}
let patch_char4 buff pos c1 c2 c3 c4 =
Bytes.unsafe_set buff pos c1;
@@ -29,40 +62,48 @@ let patch_char4 buff pos c1 c2 c3 c4 =
Bytes.unsafe_set buff (pos + 2) c3;
Bytes.unsafe_set buff (pos + 3) c4
-let patch buff (pos, n) =
+let patch1 buff pos n =
patch_char4 buff pos
(Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16))
(Char.unsafe_chr (n asr 24))
-(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
-let patch_int buff patches =
+let patch_int buff reloc =
(* copy code *before* patching because of nested evaluations:
the code we are patching might be called (and thus "concurrently" patched)
and results in wrong results. Side-effects... *)
let buff = Bytes.of_string buff in
- let () = List.iter (fun p -> patch buff p) patches in
- (* Note: we follow the apporach suggested by Gabriel Scherer in
- PR#136 here, and use unsafe as we own buff.
+ let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in
+ let () = CArray.iter iter reloc in
+ buff
- The crux of the question that avoids defining emitcodes just as a
- Byte.t is the call to hcons in to_memory below. Even if disabling
- this optimization has no visible time impact, test data shows
- that the optimization is indeed triggered quite often so we
- choose ugliness over altering the semantics.
-
- Handle with care.
- *)
- Bytes.unsafe_to_string buff
+let patch buff pl f =
+ (** Order seems important here? *)
+ let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
+ let buff = patch_int buff reloc in
+ tcode_of_code buff (Bytes.length buff)
(* Buffering of bytecode *)
-let out_buffer = ref(Bytes.create 1024)
-and out_position = ref 0
+type label_definition =
+ Label_defined of int
+ | Label_undefined of (int * int) list
-let out_word b1 b2 b3 b4 =
- let p = !out_position in
- if p >= Bytes.length !out_buffer then begin
- let len = Bytes.length !out_buffer in
+type env = {
+ mutable out_buffer : Bytes.t;
+ mutable out_position : int;
+ mutable label_table : label_definition array;
+ (* le ieme element de la table = Label_defined n signifie que l'on a
+ deja rencontrer le label i et qu'il est a l'offset n.
+ = Label_undefined l signifie que l'on a
+ pas encore rencontrer ce label, le premier entier indique ou est l'entier
+ a patcher dans la string, le deuxieme son origine *)
+ reloc_info : int list RelocTable.t;
+}
+
+let out_word env b1 b2 b3 b4 =
+ let p = env.out_position in
+ if p >= Bytes.length env.out_buffer then begin
+ let len = Bytes.length env.out_buffer in
let new_len =
if len <= Sys.max_string_length / 2
then 2 * len
@@ -71,260 +112,240 @@ let out_word b1 b2 b3 b4 =
then invalid_arg "String.create" (* Pas la bonne exception .... *)
else Sys.max_string_length in
let new_buffer = Bytes.create new_len in
- Bytes.blit !out_buffer 0 new_buffer 0 len;
- out_buffer := new_buffer
+ Bytes.blit env.out_buffer 0 new_buffer 0 len;
+ env.out_buffer <- new_buffer
end;
- patch_char4 !out_buffer p (Char.unsafe_chr b1)
+ patch_char4 env.out_buffer p (Char.unsafe_chr b1)
(Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
- out_position := p + 4
+ env.out_position <- p + 4
-let out opcode =
- out_word opcode 0 0 0
+let out env opcode =
+ out_word env opcode 0 0 0
-let out_int n =
- out_word n (n asr 8) (n asr 16) (n asr 24)
+let out_int env n =
+ out_word env n (n asr 8) (n asr 16) (n asr 24)
(* Handling of local labels and backpatching *)
-type label_definition =
- Label_defined of int
- | Label_undefined of (int * int) list
-
-let label_table = ref ([| |] : label_definition array)
-(* le ieme element de la table = Label_defined n signifie que l'on a
- deja rencontrer le label i et qu'il est a l'offset n.
- = Label_undefined l signifie que l'on a
- pas encore rencontrer ce label, le premier entier indique ou est l'entier
- a patcher dans la string, le deuxieme son origine *)
-
-let extend_label_table needed =
- let new_size = ref(Array.length !label_table) in
+let extend_label_table env needed =
+ let new_size = ref(Array.length env.label_table) in
while needed >= !new_size do new_size := 2 * !new_size done;
let new_table = Array.make !new_size (Label_undefined []) in
- Array.blit !label_table 0 new_table 0 (Array.length !label_table);
- label_table := new_table
-
-let backpatch (pos, orig) =
- let displ = (!out_position - orig) asr 2 in
- Bytes.set !out_buffer pos @@ Char.unsafe_chr displ;
- Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
- Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
- Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
-
-let define_label lbl =
- if lbl >= Array.length !label_table then extend_label_table lbl;
- match (!label_table).(lbl) with
+ Array.blit env.label_table 0 new_table 0 (Array.length env.label_table);
+ env.label_table <- new_table
+
+let backpatch env (pos, orig) =
+ let displ = (env.out_position - orig) asr 2 in
+ Bytes.set env.out_buffer pos @@ Char.unsafe_chr displ;
+ Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+ Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+ Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
+
+let define_label env lbl =
+ if lbl >= Array.length env.label_table then extend_label_table env lbl;
+ match (env.label_table).(lbl) with
Label_defined _ ->
raise(Failure "CEmitcode.define_label")
| Label_undefined patchlist ->
- List.iter backpatch patchlist;
- (!label_table).(lbl) <- Label_defined !out_position
+ List.iter (fun p -> backpatch env p) patchlist;
+ (env.label_table).(lbl) <- Label_defined env.out_position
-let out_label_with_orig orig lbl =
- if lbl >= Array.length !label_table then extend_label_table lbl;
- match (!label_table).(lbl) with
+let out_label_with_orig env orig lbl =
+ if lbl >= Array.length env.label_table then extend_label_table env lbl;
+ match (env.label_table).(lbl) with
Label_defined def ->
- out_int((def - orig) asr 2)
+ out_int env ((def - orig) asr 2)
| Label_undefined patchlist ->
(* spiwack: patchlist is supposed to be non-empty all the time
thus I commented that out. If there is no problem I suggest
removing it for next release (cur: 8.1) *)
(*if patchlist = [] then *)
- (!label_table).(lbl) <-
- Label_undefined((!out_position, orig) :: patchlist);
- out_int 0
+ (env.label_table).(lbl) <-
+ Label_undefined((env.out_position, orig) :: patchlist);
+ out_int env 0
-let out_label l = out_label_with_orig !out_position l
+let out_label env l = out_label_with_orig env env.out_position l
(* Relocation information *)
-let reloc_info = ref ([] : (reloc_info * int) list)
+let enter env info =
+ let pos = env.out_position in
+ let old = try RelocTable.find env.reloc_info info with Not_found -> [] in
+ RelocTable.replace env.reloc_info info (pos :: old)
-let enter info =
- reloc_info := (info, !out_position) :: !reloc_info
+let slot_for_const env c =
+ enter env (Reloc_const c);
+ out_int env 0
-let slot_for_const c =
- enter (Reloc_const c);
- out_int 0
+let slot_for_annot env a =
+ enter env (Reloc_annot a);
+ out_int env 0
-let slot_for_annot a =
- enter (Reloc_annot a);
- out_int 0
-
-let slot_for_getglobal p =
- enter (Reloc_getglobal p);
- out_int 0
+let slot_for_getglobal env p =
+ enter env (Reloc_getglobal p);
+ out_int env 0
(* Emission of one instruction *)
-let emit_instr = function
- | Klabel lbl -> define_label lbl
+let emit_instr env = function
+ | Klabel lbl -> define_label env lbl
| Kacc n ->
- if n < 8 then out(opACC0 + n) else (out opACC; out_int n)
+ if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n)
| Kenvacc n ->
if n >= 1 && n <= 4
- then out(opENVACC1 + n - 1)
- else (out opENVACC; out_int n)
+ then out env(opENVACC1 + n - 1)
+ else (out env opENVACC; out_int env n)
| Koffsetclosure ofs ->
if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out (opOFFSETCLOSURE0 + ofs / 2)
- else (out opOFFSETCLOSURE; out_int ofs)
+ then out env (opOFFSETCLOSURE0 + ofs / 2)
+ else (out env opOFFSETCLOSURE; out_int env ofs)
| Kpush ->
- out opPUSH
+ out env opPUSH
| Kpop n ->
- out opPOP; out_int n
+ out env opPOP; out_int env n
| Kpush_retaddr lbl ->
- out opPUSH_RETADDR; out_label lbl
+ out env opPUSH_RETADDR; out_label env lbl
| Kapply n ->
- if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n)
+ if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
| Kappterm(n, sz) ->
- if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz)
- else (out opAPPTERM; out_int n; out_int sz)
+ if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
+ else (out env opAPPTERM; out_int env n; out_int env sz)
| Kreturn n ->
- out opRETURN; out_int n
+ out env opRETURN; out_int env n
| Kjump ->
- out opRETURN; out_int 0
+ out env opRETURN; out_int env 0
| Krestart ->
- out opRESTART
+ out env opRESTART
| Kgrab n ->
- out opGRAB; out_int n
+ out env opGRAB; out_int env n
| Kgrabrec(rec_arg) ->
- out opGRABREC; out_int rec_arg
+ out env opGRABREC; out_int env rec_arg
| Kclosure(lbl, n) ->
- out opCLOSURE; out_int n; out_label lbl
+ out env opCLOSURE; out_int env n; out_label env lbl
| Kclosurerec(nfv,init,lbl_types,lbl_bodies) ->
- out opCLOSUREREC;out_int (Array.length lbl_bodies);
- out_int nfv; out_int init;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_types;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_bodies
+ out env opCLOSUREREC;out_int env (Array.length lbl_bodies);
+ out_int env nfv; out_int env init;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_types;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_bodies
| Kclosurecofix(nfv,init,lbl_types,lbl_bodies) ->
- out opCLOSURECOFIX;out_int (Array.length lbl_bodies);
- out_int nfv; out_int init;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_types;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_bodies
+ out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies);
+ out_int env nfv; out_int env init;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_types;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_bodies
| Kgetglobal q ->
- out opGETGLOBAL; slot_for_getglobal q
+ out env opGETGLOBAL; slot_for_getglobal env q
| Kconst (Const_b0 i) ->
if i >= 0 && i <= 3
- then out (opCONST0 + i)
- else (out opCONSTINT; out_int i)
+ then out env (opCONST0 + i)
+ else (out env opCONSTINT; out_int env i)
| Kconst c ->
- out opGETGLOBAL; slot_for_const c
+ out env opGETGLOBAL; slot_for_const env c
| Kmakeblock(n, t) ->
if Int.equal n 0 then invalid_arg "emit_instr : block size = 0"
- else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
- else (out opMAKEBLOCK; out_int n; out_int t)
+ else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t)
+ else (out env opMAKEBLOCK; out_int env n; out_int env t)
| Kmakeprod ->
- out opMAKEPROD
+ out env opMAKEPROD
| Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
- out opMAKESWITCHBLOCK;
- out_label typlbl; out_label swlbl;
- slot_for_annot annot;out_int sz
+ out env opMAKESWITCHBLOCK;
+ out_label env typlbl; out_label env swlbl;
+ slot_for_annot env annot;out_int env sz
| Kswitch (tbl_const, tbl_block) ->
let lenb = Array.length tbl_block in
let lenc = Array.length tbl_const in
assert (lenb < 0x100 && lenc < 0x1000000);
- out opSWITCH;
- out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
-(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
- let org = !out_position in
- Array.iter (out_label_with_orig org) tbl_const;
- Array.iter (out_label_with_orig org) tbl_block
+ out env opSWITCH;
+ out_word env lenc (lenc asr 8) (lenc asr 16) (lenb);
+(* out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) tbl_const;
+ Array.iter (out_label_with_orig env org) tbl_block
| Kpushfields n ->
- out opPUSHFIELDS;out_int n
+ out env opPUSHFIELDS;out_int env n
| Kfield n ->
- if n <= 1 then out (opGETFIELD0+n)
- else (out opGETFIELD;out_int n)
+ if n <= 1 then out env (opGETFIELD0+n)
+ else (out env opGETFIELD;out_int env n)
| Ksetfield n ->
- if n <= 1 then out (opSETFIELD0+n)
- else (out opSETFIELD;out_int n)
+ if n <= 1 then out env (opSETFIELD0+n)
+ else (out env opSETFIELD;out_int env n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
- | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
- | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size
+ | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p)
+ | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
(* spiwack *)
- | Kbranch lbl -> out opBRANCH; out_label lbl
- | Kaddint31 -> out opADDINT31
- | Kaddcint31 -> out opADDCINT31
- | Kaddcarrycint31 -> out opADDCARRYCINT31
- | Ksubint31 -> out opSUBINT31
- | Ksubcint31 -> out opSUBCINT31
- | Ksubcarrycint31 -> out opSUBCARRYCINT31
- | Kmulint31 -> out opMULINT31
- | Kmulcint31 -> out opMULCINT31
- | Kdiv21int31 -> out opDIV21INT31
- | Kdivint31 -> out opDIVINT31
- | Kaddmuldivint31 -> out opADDMULDIVINT31
- | Kcompareint31 -> out opCOMPAREINT31
- | Khead0int31 -> out opHEAD0INT31
- | Ktail0int31 -> out opTAIL0INT31
- | Kisconst lbl -> out opISCONST; out_label lbl
- | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
- | Kcompint31 -> out opCOMPINT31
- | Kdecompint31 -> out opDECOMPINT31
- | Klorint31 -> out opORINT31
- | Klandint31 -> out opANDINT31
- | Klxorint31 -> out opXORINT31
+ | Kbranch lbl -> out env opBRANCH; out_label env lbl
+ | Kaddint31 -> out env opADDINT31
+ | Kaddcint31 -> out env opADDCINT31
+ | Kaddcarrycint31 -> out env opADDCARRYCINT31
+ | Ksubint31 -> out env opSUBINT31
+ | Ksubcint31 -> out env opSUBCINT31
+ | Ksubcarrycint31 -> out env opSUBCARRYCINT31
+ | Kmulint31 -> out env opMULINT31
+ | Kmulcint31 -> out env opMULCINT31
+ | Kdiv21int31 -> out env opDIV21INT31
+ | Kdivint31 -> out env opDIVINT31
+ | Kaddmuldivint31 -> out env opADDMULDIVINT31
+ | Kcompareint31 -> out env opCOMPAREINT31
+ | Khead0int31 -> out env opHEAD0INT31
+ | Ktail0int31 -> out env opTAIL0INT31
+ | Kisconst lbl -> out env opISCONST; out_label env lbl
+ | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl
+ | Kcompint31 -> out env opCOMPINT31
+ | Kdecompint31 -> out env opDECOMPINT31
+ | Klorint31 -> out env opORINT31
+ | Klandint31 -> out env opANDINT31
+ | Klxorint31 -> out env opXORINT31
(*/spiwack *)
| Kstop ->
- out opSTOP
+ out env opSTOP
(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
-let rec emit insns remaining = match insns with
+let rec emit env insns remaining = match insns with
| [] ->
(match remaining with
[] -> ()
- | (first::rest) -> emit first rest)
+ | (first::rest) -> emit env first rest)
(* Peephole optimizations *)
| Kpush :: Kacc n :: c ->
- if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
- emit c remaining
+ if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n);
+ emit env c remaining
| Kpush :: Kenvacc n :: c ->
if n >= 1 && n <= 4
- then out(opPUSHENVACC1 + n - 1)
- else (out opPUSHENVACC; out_int n);
- emit c remaining
+ then out env(opPUSHENVACC1 + n - 1)
+ else (out env opPUSHENVACC; out_int env n);
+ emit env c remaining
| Kpush :: Koffsetclosure ofs :: c ->
if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
- else (out opPUSHOFFSETCLOSURE; out_int ofs);
- emit c remaining
+ then out env(opPUSHOFFSETCLOSURE0 + ofs / 2)
+ else (out env opPUSHOFFSETCLOSURE; out_int env ofs);
+ emit env c remaining
| Kpush :: Kgetglobal id :: c ->
- out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
+ out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining
| Kpush :: Kconst (Const_b0 i) :: c ->
if i >= 0 && i <= 3
- then out (opPUSHCONST0 + i)
- else (out opPUSHCONSTINT; out_int i);
- emit c remaining
+ then out env (opPUSHCONST0 + i)
+ else (out env opPUSHCONSTINT; out_int env i);
+ emit env c remaining
| Kpush :: Kconst const :: c ->
- out opPUSHGETGLOBAL; slot_for_const const;
- emit c remaining
+ out env opPUSHGETGLOBAL; slot_for_const env const;
+ emit env c remaining
| Kpop n :: Kjump :: c ->
- out opRETURN; out_int n; emit c remaining
+ out env opRETURN; out_int env n; emit env c remaining
| Ksequence(c1,c2)::c ->
- emit c1 (c2::c::remaining)
+ emit env c1 (c2::c::remaining)
(* Default case *)
| instr :: c ->
- emit_instr instr; emit c remaining
+ emit_instr env instr; emit env c remaining
(* Initialization *)
-let init () =
- out_position := 0;
- label_table := Array.make 16 (Label_undefined []);
- reloc_info := []
-
-type emitcodes = String.t
-
-let length = String.length
-
-type to_patch = emitcodes * (patch list) * fv
+type to_patch = emitcodes * patches * fv
(* Substitution *)
let rec subst_strcst s sc =
@@ -334,17 +355,21 @@ let rec subst_strcst s sc =
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
-let subst_patch s (ri,pos) =
+let subst_reloc s ri =
match ri with
| Reloc_annot a ->
let (kn,i) = a.ci.ci_ind in
let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
- (Reloc_annot {a with ci = ci},pos)
- | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
+ Reloc_annot {a with ci = ci}
+ | Reloc_const sc -> Reloc_const (subst_strcst s sc)
+ | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
+
+let subst_patches subst p =
+ let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
+ { reloc_infos = infos; }
let subst_to_patch s (code,pl,fv) =
- code,List.rev_map (subst_patch s) pl,fv
+ code, subst_patches s pl, fv
type body_code =
| BCdefined of to_patch
@@ -381,16 +406,23 @@ let repr_body_code = function
| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
- init();
- emit init_code [];
- emit fun_code [];
+ let env = {
+ out_buffer = Bytes.create 1024;
+ out_position = 0;
+ label_table = Array.make 16 (Label_undefined []);
+ reloc_info = RelocTable.create 91;
+ } in
+ emit env init_code [];
+ emit env fun_code [];
(** Later uses of this string are all purely functional *)
- let code = Bytes.sub_string !out_buffer 0 !out_position in
+ let code = Bytes.sub_string env.out_buffer 0 env.out_position in
let code = CString.hcons code in
- let reloc = List.rev !reloc_info in
+ let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in
+ let reloc = RelocTable.fold fold env.reloc_info [] in
+ let reloc = { reloc_infos = CArray.of_list reloc } in
Array.iter (fun lbl ->
(match lbl with
Label_defined _ -> assert true
| Label_undefined patchlist ->
- assert (patchlist = []))) !label_table;
+ assert (patchlist = []))) env.label_table;
(code, reloc, fv)
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index fee45aafd8..03920dc1a3 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -6,20 +6,12 @@ type reloc_info =
| Reloc_const of structured_constant
| Reloc_getglobal of Constant.t
-type patch = reloc_info * int
-
-(* A virer *)
-val subst_patch : Mod_subst.substitution -> patch -> patch
-
+type patches
type emitcodes
-val length : emitcodes -> int
-
-val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes
-
-type to_patch = emitcodes * (patch list) * fv
+val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode
-val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
+type to_patch = emitcodes * patches * fv
type body_code =
| BCdefined of to_patch
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
new file mode 100644
index 0000000000..2d9ec6050e
--- /dev/null
+++ b/kernel/cinstr.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Names
+open Constr
+open Cbytecodes
+
+(** This file defines the lambda code for the bytecode compiler. It has been
+extracted from Clambda.ml because of the retroknowledge architecture. *)
+
+type uint =
+ | UintVal of Uint31.t
+ | UintDigits of lambda array
+ | UintDecomp of lambda
+
+and lambda =
+ | Lrel of Name.t * int
+ | Lvar of Id.t
+ | Lprod of lambda * lambda
+ | Llam of Name.t array * lambda
+ | Llet of Name.t * lambda * lambda
+ | Lapp of lambda * lambda array
+ | Lconst of pconstant
+ | Lprim of pconstant * int (* arity *) * instruction * lambda array
+ | Lcase of case_info * reloc_table * lambda * lambda * lam_branches
+ | Lfix of (int array * int) * fix_decl
+ | Lcofix of int * fix_decl
+ | Lmakeblock of int * lambda array
+ | Lval of structured_constant
+ | Lsort of Sorts.t
+ | Lind of pinductive
+ | Lproj of int * Constant.t * lambda
+ | Luint of uint
+
+and lam_branches =
+ { constant_branches : lambda array;
+ nonconstant_branches : (Name.t array * lambda) array }
+
+and fix_decl = Name.t array * lambda array * lambda array
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
new file mode 100644
index 0000000000..636ed35107
--- /dev/null
+++ b/kernel/clambda.ml
@@ -0,0 +1,853 @@
+open Util
+open Names
+open Esubst
+open Term
+open Constr
+open Declarations
+open Cbytecodes
+open Cinstr
+open Pre_env
+open Pp
+
+let pr_con sp = str(Names.Label.to_string (Constant.label sp))
+
+(** Printing **)
+
+let pp_names ids =
+ prlist_with_sep (fun _ -> brk(1,1)) Name.print (Array.to_list ids)
+
+let pp_rel name n =
+ Name.print name ++ str "##" ++ int n
+
+let pp_sort s =
+ match Sorts.family s with
+ | InSet -> str "Set"
+ | InProp -> str "Prop"
+ | InType -> str "Type"
+
+let rec pp_lam lam =
+ match lam with
+ | Lrel (id,n) -> pp_rel id n
+ | Lvar id -> Id.print id
+ | Lprod(dom,codom) -> hov 1
+ (str "forall(" ++
+ pp_lam dom ++
+ str "," ++ spc() ++
+ pp_lam codom ++
+ str ")")
+ | Llam(ids,body) -> hov 1
+ (str "(fun " ++
+ pp_names ids ++
+ str " =>" ++
+ spc() ++
+ pp_lam body ++
+ str ")")
+ | Llet(id,def,body) -> hov 0
+ (str "let " ++
+ Name.print id ++
+ str ":=" ++
+ pp_lam def ++
+ str " in" ++
+ spc() ++
+ pp_lam body)
+ | Lapp(f, args) -> hov 1
+ (str "(" ++ pp_lam f ++ spc() ++
+ prlist_with_sep spc pp_lam (Array.to_list args) ++
+ str")")
+ | Lconst (kn,_) -> pr_con kn
+ | Lcase(_ci, _rtbl, t, a, branches) ->
+ let ic = ref (-1) in
+ let ib = ref 0 in
+ v 0 (str"<" ++ pp_lam t ++ str">" ++ cut() ++
+ str "Case" ++ spc () ++ pp_lam a ++ spc() ++ str "of" ++ cut() ++
+ v 0
+ ((prlist_with_sep (fun _ -> str "")
+ (fun c ->
+ cut () ++ str "| " ++
+ int (incr ic; !ic) ++ str " => " ++ pp_lam c)
+ (Array.to_list branches.constant_branches)) ++
+ (prlist_with_sep (fun _ -> str "")
+ (fun (ids,c) ->
+ cut () ++ str "| " ++
+ int (incr ib; !ib) ++ str " " ++
+ pp_names ids ++ str " => " ++ pp_lam c)
+ (Array.to_list branches.nonconstant_branches)))
+ ++ cut() ++ str "end")
+ | Lfix((t,i),(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in
+ hov 1
+ (str"fix " ++ int i ++ spc() ++ str"{" ++
+ v 0
+ (prlist_with_sep spc
+ (fun (na,i,ty,bd) ->
+ Name.print na ++ str"/" ++ int i ++ str":" ++
+ pp_lam ty ++ cut() ++ str":=" ++
+ pp_lam bd) (Array.to_list fixl)) ++
+ str"}")
+
+ | Lcofix (i,(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+ hov 1
+ (str"cofix " ++ int i ++ spc() ++ str"{" ++
+ v 0
+ (prlist_with_sep spc
+ (fun (na,ty,bd) ->
+ Name.print na ++ str":" ++ pp_lam ty ++
+ cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++
+ str"}")
+ | Lmakeblock(tag, args) ->
+ hov 1
+ (str "(makeblock " ++ int tag ++ spc() ++
+ prlist_with_sep spc pp_lam (Array.to_list args) ++
+ str")")
+ | Lval _ -> str "values"
+ | Lsort s -> pp_sort s
+ | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
+ | Lprim((kn,_u),ar,op,args) ->
+ hov 1
+ (str "(PRIM " ++ pr_con kn ++ spc() ++
+ prlist_with_sep spc pp_lam (Array.to_list args) ++
+ str")")
+ | Lproj(i,kn,arg) ->
+ hov 1
+ (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg
+ ++ str ")")
+ | Luint _ ->
+ str "(uint)"
+
+(*s Constructors *)
+
+let mkLapp f args =
+ if Array.length args = 0 then f
+ else
+ match f with
+ | Lapp(f', args') -> Lapp (f', Array.append args' args)
+ | _ -> Lapp(f, args)
+
+let mkLlam ids body =
+ if Array.length ids = 0 then body
+ else
+ match body with
+ | Llam(ids', body) -> Llam(Array.append ids ids', body)
+ | _ -> Llam(ids, body)
+
+let decompose_Llam lam =
+ match lam with
+ | Llam(ids,body) -> ids, body
+ | _ -> [||], lam
+
+(*s Operators on substitution *)
+let subst_id = subs_id 0
+let lift = subs_lift
+let liftn = subs_liftn
+let cons v subst = subs_cons([|v|], subst)
+let shift subst = subs_shft (1, subst)
+
+(* A generic map function *)
+
+let rec map_lam_with_binders g f n lam =
+ match lam with
+ | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
+ | Lprod(dom,codom) ->
+ let dom' = f n dom in
+ let codom' = f n codom in
+ if dom == dom' && codom == codom' then lam else Lprod(dom',codom')
+ | Llam(ids,body) ->
+ let body' = f (g (Array.length ids) n) body in
+ if body == body' then lam else mkLlam ids body'
+ | Llet(id,def,body) ->
+ let def' = f n def in
+ let body' = f (g 1 n) body in
+ if body == body' && def == def' then lam else Llet(id,def',body')
+ | Lapp(fct,args) ->
+ let fct' = f n fct in
+ let args' = Array.smartmap (f n) args in
+ if fct == fct' && args == args' then lam else mkLapp fct' args'
+ | Lcase(ci,rtbl,t,a,branches) ->
+ let const = branches.constant_branches in
+ let nonconst = branches.nonconstant_branches in
+ let t' = f n t in
+ let a' = f n a in
+ let const' = Array.smartmap (f n) const in
+ let on_b b =
+ let (ids,body) = b in
+ let body' = f (g (Array.length ids) n) body in
+ if body == body' then b else (ids,body') in
+ let nonconst' = Array.smartmap on_b nonconst in
+ let branches' =
+ if const == const' && nonconst == nonconst' then
+ branches
+ else
+ { constant_branches = const';
+ nonconstant_branches = nonconst' }
+ in
+ if t == t' && a == a' && branches == branches' then lam else
+ Lcase(ci,rtbl,t',a',branches')
+ | Lfix(init,(ids,ltypes,lbodies)) ->
+ let ltypes' = Array.smartmap (f n) ltypes in
+ let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+ if ltypes == ltypes' && lbodies == lbodies' then lam
+ else Lfix(init,(ids,ltypes',lbodies'))
+ | Lcofix(init,(ids,ltypes,lbodies)) ->
+ let ltypes' = Array.smartmap (f n) ltypes in
+ let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+ if ltypes == ltypes' && lbodies == lbodies' then lam
+ else Lcofix(init,(ids,ltypes',lbodies'))
+ | Lmakeblock(tag,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then lam else Lmakeblock(tag,args')
+ | Lprim(kn,ar,op,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then lam else Lprim(kn,ar,op,args')
+ | Lproj(i,kn,arg) ->
+ let arg' = f n arg in
+ if arg == arg' then lam else Lproj(i,kn,arg')
+ | Luint u ->
+ let u' = map_uint g f n u in
+ if u == u' then lam else Luint u'
+
+and map_uint g f n u =
+ match u with
+ | UintVal _ -> u
+ | UintDigits(args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then u else UintDigits(args')
+ | UintDecomp(a) ->
+ let a' = f n a in
+ if a == a' then u else UintDecomp(a')
+
+(*s Lift and substitution *)
+
+
+let rec lam_exlift el lam =
+ match lam with
+ | Lrel(id,i) ->
+ let i' = reloc_rel i el in
+ if i == i' then lam else Lrel(id,i')
+ | _ -> map_lam_with_binders el_liftn lam_exlift el lam
+
+let lam_lift k lam =
+ if k = 0 then lam
+ else lam_exlift (el_shft k el_id) lam
+
+let lam_subst_rel lam id n subst =
+ match expand_rel n subst with
+ | Inl(k,v) -> lam_lift k v
+ | Inr(n',_) ->
+ if n == n' then lam
+ else Lrel(id, n')
+
+let rec lam_exsubst subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+ | _ -> map_lam_with_binders liftn lam_exsubst subst lam
+
+let lam_subst_args subst args =
+ if is_subs_id subst then args
+ else Array.smartmap (lam_exsubst subst) args
+
+(** Simplification of lambda expression *)
+
+(* [simplify subst lam] simplify the expression [lam_subst subst lam] *)
+(* that is : *)
+(* - Reduce [let] is the definition can be substituted i.e: *)
+(* - a variable (rel or identifier) *)
+(* - a constant *)
+(* - a structured constant *)
+(* - a function *)
+(* - Transform beta redex into [let] expression *)
+(* - Move arguments under [let] *)
+(* Invariant : Terms in [subst] are already simplified and can be *)
+(* substituted *)
+
+let can_subst lam =
+ match lam with
+ | Lrel _ | Lvar _ | Lconst _
+ | Lval _ | Lsort _ | Lind _ | Llam _ -> true
+ | _ -> false
+
+let rec simplify subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+
+ | Llet(id,def,body) ->
+ let def' = simplify subst def in
+ if can_subst def' then simplify (cons def' subst) body
+ else
+ let body' = simplify (lift subst) body in
+ if def == def' && body == body' then lam
+ else Llet(id,def',body')
+
+ | Lapp(f,args) ->
+ begin match simplify_app subst f subst args with
+ | Lapp(f',args') when f == f' && args == args' -> lam
+ | lam' -> lam'
+ end
+
+ | _ -> map_lam_with_binders liftn simplify subst lam
+
+and simplify_app substf f substa args =
+ match f with
+ | Lrel(id, i) ->
+ begin match lam_subst_rel f id i substf with
+ | Llam(ids, body) ->
+ reduce_lapp
+ subst_id (Array.to_list ids) body
+ substa (Array.to_list args)
+ | f' -> mkLapp f' (simplify_args substa args)
+ end
+ | Llam(ids, body) ->
+ reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args)
+ | Llet(id, def, body) ->
+ let def' = simplify substf def in
+ if can_subst def' then
+ simplify_app (cons def' substf) body substa args
+ else
+ Llet(id, def', simplify_app (lift substf) body (shift substa) args)
+ | Lapp(f, args') ->
+ let args = Array.append
+ (lam_subst_args substf args') (lam_subst_args substa args) in
+ simplify_app substf f subst_id args
+ | _ -> mkLapp (simplify substf f) (simplify_args substa args)
+
+and simplify_args subst args = Array.smartmap (simplify subst) args
+
+and reduce_lapp substf lids body substa largs =
+ match lids, largs with
+ | id::lids, a::largs ->
+ let a = simplify substa a in
+ if can_subst a then
+ reduce_lapp (cons a substf) lids body substa largs
+ else
+ let body = reduce_lapp (lift substf) lids body (shift substa) largs in
+ Llet(id, a, body)
+ | [], [] -> simplify substf body
+ | _::_, _ ->
+ Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body)
+ | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
+
+
+
+
+(* [occurrence kind k lam]:
+ If [kind] is [true] return [true] if the variable [k] does not appear in
+ [lam], return [false] if the variable appear one time and not
+ under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
+ If [kind] is [false] return [false] if the variable does not appear in [lam]
+ else raise [Not_found]
+*)
+
+let rec occurrence k kind lam =
+ match lam with
+ | Lrel (_,n) ->
+ if n = k then
+ if kind then false else raise Not_found
+ else kind
+ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind
+ | Lprod(dom, codom) ->
+ occurrence k (occurrence k kind dom) codom
+ | Llam(ids,body) ->
+ let _ = occurrence (k+Array.length ids) false body in kind
+ | Llet(_,def,body) ->
+ occurrence (k+1) (occurrence k kind def) body
+ | Lapp(f, args) ->
+ occurrence_args k (occurrence k kind f) args
+ | Lprim(_,_,_,args) | Lmakeblock(_,args) ->
+ occurrence_args k kind args
+ | Lcase(_ci,_rtbl,t,a,branches) ->
+ let kind = occurrence k (occurrence k kind t) a in
+ let r = ref kind in
+ Array.iter (fun c -> r := occurrence k kind c && !r) branches.constant_branches;
+ let on_b (ids,c) =
+ r := occurrence (k+Array.length ids) kind c && !r
+ in
+ Array.iter on_b branches.nonconstant_branches;
+ !r
+ | Lfix(_,(ids,ltypes,lbodies))
+ | Lcofix(_,(ids,ltypes,lbodies)) ->
+ let kind = occurrence_args k kind ltypes in
+ let _ = occurrence_args (k+Array.length ids) false lbodies in
+ kind
+ | Lproj(_,_,arg) ->
+ occurrence k kind arg
+ | Luint u -> occurrence_uint k kind u
+
+and occurrence_args k kind args =
+ Array.fold_left (occurrence k) kind args
+
+and occurrence_uint k kind u =
+ match u with
+ | UintVal _ -> kind
+ | UintDigits args -> occurrence_args k kind args
+ | UintDecomp t -> occurrence k kind t
+
+let occur_once lam =
+ try let _ = occurrence 1 true lam in true
+ with Not_found -> false
+
+(* [remove_let lam] remove let expression in [lam] if the variable is *)
+(* used at most once time in the body, and does not appear under *)
+(* a lambda or a fix or a cofix *)
+
+let rec remove_let subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+ | Llet(id,def,body) ->
+ let def' = remove_let subst def in
+ if occur_once body then remove_let (cons def' subst) body
+ else
+ let body' = remove_let (lift subst) body in
+ if def == def' && body == body' then lam else Llet(id,def',body')
+ | _ -> map_lam_with_binders liftn remove_let subst lam
+
+
+(*s Translation from [constr] to [lambda] *)
+
+(* Translation of constructor *)
+
+(* Limitation due to OCaml's representation of non-constant
+ constructors: limited to 245 + 1 (0 tag) cases. *)
+
+exception TooLargeInductive of Pp.t
+
+let max_nb_const = 0x1000000
+let max_nb_block = 0x1000000 + last_variant_tag - 1
+
+let str_max_constructors =
+ Format.sprintf
+ " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
+
+let check_compilable ib =
+
+ if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then
+ let msg =
+ Pp.(str "Cannot compile code for virtual machine as it uses inductive "
+ ++ Id.print ib.mind_typename ++ str str_max_constructors)
+ in
+ raise (TooLargeInductive msg)
+
+let is_value lc =
+ match lc with
+ | Lval _ -> true
+ | _ -> false
+
+let get_value lc =
+ match lc with
+ | Lval v -> v
+ | _ -> raise Not_found
+
+let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n)
+
+let make_args start _end =
+ Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
+
+(* Translation of constructors *)
+let expand_constructor tag nparams arity =
+ let ids = Array.make (nparams + arity) Anonymous in
+ if arity = 0 then mkLlam ids (mkConst_b0 tag)
+ else
+ let args = make_args arity 1 in
+ Llam(ids, Lmakeblock (tag, args))
+
+let makeblock tag nparams arity args =
+ let nargs = Array.length args in
+ if nparams > 0 || nargs < arity then
+ mkLapp (expand_constructor tag nparams arity) args
+ else
+ (* The constructor is fully applied *)
+ if arity = 0 then mkConst_b0 tag
+ else
+ if Array.for_all is_value args then
+ if tag < last_variant_tag then
+ Lval(Cbytecodes.Const_bn(tag, Array.map get_value args))
+ else
+ let args = Array.map get_value args in
+ let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in
+ Lval(Cbytecodes.Const_bn(last_variant_tag, args))
+ else Lmakeblock(tag, args)
+
+
+(* Compiling constants *)
+
+let rec get_alias env kn =
+ let cb = lookup_constant kn env in
+ let tps = cb.const_body_code in
+ match tps with
+ | None -> kn
+ | Some tps ->
+ (match Cemitcodes.force tps with
+ | Cemitcodes.BCalias kn' -> get_alias env kn'
+ | _ -> kn)
+
+(* Compilation of primitive *)
+
+let _h = Name(Id.of_string "f")
+
+(*
+let expand_prim kn op arity =
+ let ids = Array.make arity Anonymous in
+ let args = make_args arity 1 in
+ Llam(ids, prim kn op args)
+*)
+
+let compile_prim n op kn fc args =
+ if not fc then raise Not_found
+ else
+ Lprim(kn, n, op, args)
+
+ (*
+ let (nparams, arity) = CPrimitives.arity op in
+ let expected = nparams + arity in
+ if Array.length args >= expected then prim kn op args
+ else mkLapp (expand_prim kn op expected) args
+*)
+
+(*i Global environment *)
+
+let get_names decl =
+ let decl = Array.of_list decl in
+ Array.map fst decl
+
+
+(* Rel Environment *)
+module Vect =
+struct
+ type 'a t = {
+ mutable elems : 'a array;
+ mutable size : int;
+ }
+
+ let make n a = {
+ elems = Array.make n a;
+ size = 0;
+ }
+
+ let extend v =
+ if v.size = Array.length v.elems then
+ let new_size = min (2*v.size) Sys.max_array_length in
+ if new_size <= v.size then raise (Invalid_argument "Vect.extend");
+ let new_elems = Array.make new_size v.elems.(0) in
+ Array.blit v.elems 0 new_elems 0 (v.size);
+ v.elems <- new_elems
+
+ let push v a =
+ extend v;
+ v.elems.(v.size) <- a;
+ v.size <- v.size + 1
+
+ let popn v n =
+ v.size <- max 0 (v.size - n)
+
+ let pop v = popn v 1
+
+ let get_last v n =
+ if v.size <= n then raise
+ (Invalid_argument "Vect.get:index out of bounds");
+ v.elems.(v.size - n - 1)
+
+end
+
+let dummy_lambda = Lrel(Anonymous, 0)
+
+let empty_args = [||]
+
+module Renv =
+struct
+
+ type constructor_info = tag * int * int (* nparam nrealargs *)
+
+ type t = {
+ global_env : env;
+ name_rel : Name.t Vect.t;
+ construct_tbl : (constructor, constructor_info) Hashtbl.t;
+ }
+
+ let make env = {
+ global_env = env;
+ name_rel = Vect.make 16 Anonymous;
+ construct_tbl = Hashtbl.create 111
+ }
+
+ let push_rel env id = Vect.push env.name_rel id
+
+ let push_rels env ids =
+ Array.iter (push_rel env) ids
+
+ let pop env = Vect.pop env.name_rel
+
+ let popn env n =
+ for _i = 1 to n do pop env done
+
+ let get env n =
+ Lrel (Vect.get_last env.name_rel (n-1), n)
+
+ let get_construct_info env c =
+ try Hashtbl.find env.construct_tbl c
+ with Not_found ->
+ let ((mind,j), i) = c in
+ let oib = lookup_mind mind env.global_env in
+ let oip = oib.mind_packets.(j) in
+ check_compilable oip;
+ let tag,arity = oip.mind_reloc_tbl.(i-1) in
+ let nparams = oib.mind_nparams in
+ let r = (tag, nparams, arity) in
+ Hashtbl.add env.construct_tbl c r;
+ r
+end
+
+open Renv
+
+let rec lambda_of_constr env c =
+ match Constr.kind c with
+ | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
+ | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar")
+
+ | Cast (c, _, _) -> lambda_of_constr env c
+
+ | Rel i -> Renv.get env i
+
+ | Var id -> Lvar id
+
+ | Sort s -> Lsort s
+ | Ind ind -> Lind ind
+
+ | Prod(id, dom, codom) ->
+ let ld = lambda_of_constr env dom in
+ Renv.push_rel env id;
+ let lc = lambda_of_constr env codom in
+ Renv.pop env;
+ Lprod(ld, Llam([|id|], lc))
+
+ | Lambda _ ->
+ let params, body = decompose_lam c in
+ let ids = get_names (List.rev params) in
+ Renv.push_rels env ids;
+ let lb = lambda_of_constr env body in
+ Renv.popn env (Array.length ids);
+ mkLlam ids lb
+
+ | LetIn(id, def, _, body) ->
+ let ld = lambda_of_constr env def in
+ Renv.push_rel env id;
+ let lb = lambda_of_constr env body in
+ Renv.pop env;
+ Llet(id, ld, lb)
+
+ | App(f, args) -> lambda_of_app env f args
+
+ | Const _ -> lambda_of_app env c empty_args
+
+ | Construct _ -> lambda_of_app env c empty_args
+
+ | Case(ci,t,a,branches) ->
+ let ind = ci.ci_ind in
+ let mib = lookup_mind (fst ind) env.global_env in
+ let oib = mib.mind_packets.(snd ind) in
+ let () = check_compilable oib in
+ let rtbl = oib.mind_reloc_tbl in
+
+
+ (* translation of the argument *)
+ let la = lambda_of_constr env a in
+ let entry = mkInd ind in
+ let la =
+ try
+ Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge
+ entry la
+ with Not_found -> la
+ in
+ (* translation of the type *)
+ let lt = lambda_of_constr env t in
+ (* translation of branches *)
+ let consts = Array.make oib.mind_nb_constant dummy_lambda in
+ let blocks = Array.make oib.mind_nb_args ([||],dummy_lambda) in
+ for i = 0 to Array.length rtbl - 1 do
+ let tag, arity = rtbl.(i) in
+ let b = lambda_of_constr env branches.(i) in
+ if arity = 0 then consts.(tag) <- b
+ else
+ let b =
+ match b with
+ | Llam(ids, body) when Array.length ids = arity -> (ids, body)
+ | _ ->
+ let ids = Array.make arity Anonymous in
+ let args = make_args arity 1 in
+ let ll = lam_lift arity b in
+ (ids, mkLapp ll args)
+ in blocks.(tag-1) <- b
+ done;
+ let branches =
+ { constant_branches = consts;
+ nonconstant_branches = blocks }
+ in
+ Lcase(ci, rtbl, lt, la, branches)
+
+ | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
+ let ltypes = lambda_of_args env 0 type_bodies in
+ Renv.push_rels env names;
+ let lbodies = lambda_of_args env 0 rec_bodies in
+ Renv.popn env (Array.length names);
+ Lfix(rec_init, (names, ltypes, lbodies))
+
+ | CoFix(init,(names,type_bodies,rec_bodies)) ->
+ let ltypes = lambda_of_args env 0 type_bodies in
+ Renv.push_rels env names;
+ let lbodies = lambda_of_args env 0 rec_bodies in
+ Renv.popn env (Array.length names);
+ Lcofix(init, (names, ltypes, lbodies))
+
+ | Proj (p,c) ->
+ let kn = Projection.constant p in
+ let cb = lookup_constant kn env.global_env in
+ let pb = Option.get cb.const_proj in
+ let n = pb.proj_arg in
+ let lc = lambda_of_constr env c in
+ Lproj (n,kn,lc)
+
+and lambda_of_app env f args =
+ match Constr.kind f with
+ | Const (kn,u as c) ->
+ let kn = get_alias env.global_env kn 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
+ (* We delay the compilation of arguments to avoid an exponential behavior *)
+ let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge
+ (mkConstU (kn,u)) in
+ let args = lambda_of_args env 0 args in
+ f args
+ with Not_found ->
+ let cb = lookup_constant kn env.global_env in
+ begin match cb.const_body with
+ | Def csubst when cb.const_inline_code ->
+ lambda_of_app env (Mod_subst.force_constr csubst) args
+ | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args)
+ end)
+ | Construct (c,_) ->
+ let tag, nparams, arity = Renv.get_construct_info env c in
+ let nargs = Array.length args in
+ if Int.equal (nparams + arity) nargs then (* fully applied *)
+ (* 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.
+ 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
+ a processor number (a caml number actually) *)
+ try
+ try
+ Retroknowledge.get_vm_constant_static_info
+ env.global_env.retroknowledge
+ 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
+ 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
+ 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
+ during the execution *)
+ let rargs = Array.sub args nparams arity in
+ let args = lambda_of_args env nparams rargs in
+ Retroknowledge.get_vm_constant_dynamic_info
+ env.global_env.retroknowledge
+ f args
+ with Not_found ->
+ (* 3/ if no special behavior is available, then the compiler
+ falls back to the normal behavior *)
+ let args = lambda_of_args env nparams args in
+ makeblock tag 0 arity args
+ else
+ let args = lambda_of_args env nparams args in
+ (* spiwack: tries first to apply the run-time compilation
+ behavior of the constructor, as in 2/ above *)
+ (try
+ (Retroknowledge.get_vm_constant_dynamic_info
+ env.global_env.retroknowledge
+ f) args
+ with Not_found ->
+ if nparams <= nargs then (* got all parameters *)
+ makeblock tag 0 arity args
+ else (* still expecting some parameters *)
+ makeblock tag (nparams - nargs) arity empty_args)
+ | _ ->
+ let f = lambda_of_constr env f in
+ let args = lambda_of_args env 0 args in
+ mkLapp f args
+
+and lambda_of_args env start args =
+ let nargs = Array.length args in
+ if start < nargs then
+ Array.init (nargs - start)
+ (fun i -> lambda_of_constr env args.(start + i))
+ else empty_args
+
+
+
+
+(*********************************)
+
+
+let optimize_lambda lam =
+ let lam = simplify subst_id lam in
+ remove_let subst_id lam
+
+let lambda_of_constr ~optimize genv c =
+ let env = Renv.make genv in
+ let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in
+ Renv.push_rels env (Array.of_list ids);
+ let lam = lambda_of_constr env c in
+ let lam = if optimize then optimize_lambda lam else lam in
+ if !Flags.dump_lambda then
+ Feedback.msg_debug (pp_lam lam);
+ lam
+
+(** Retroknowledge, to be removed once we move to primitive machine integers *)
+let compile_structured_int31 fc args =
+ if not fc then raise Not_found else
+ Luint (UintVal
+ (Uint31.of_int (Array.fold_left
+ (fun temp_i -> fun t -> match kind t with
+ | Construct ((_,d),_) -> 2*temp_i+d-1
+ | _ -> raise NotClosed)
+ 0 args)))
+
+let dynamic_int31_compilation fc args =
+ if not fc then raise Not_found else
+ Luint (UintDigits args)
+
+(* We are relying here on the tags of digits constructors *)
+let digits_from_uint i =
+ let d0 = mkConst_b0 0 in
+ let d1 = mkConst_b0 1 in
+ let digits = Array.make 31 d0 in
+ for k = 0 to 30 do
+ if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
+ digits.(30-k) <- d1
+ done;
+ digits
+
+let int31_escape_before_match fc t =
+ if not fc then
+ raise Not_found
+ else
+ match t with
+ | Luint (UintVal i) ->
+ let digits = digits_from_uint i in
+ Lmakeblock (1, digits)
+ | Luint (UintDigits args) ->
+ Lmakeblock (1,args)
+ | Luint (UintDecomp _) ->
+ assert false
+ | _ -> Luint (UintDecomp t)
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
new file mode 100644
index 0000000000..89b7fd8e3b
--- /dev/null
+++ b/kernel/clambda.mli
@@ -0,0 +1,27 @@
+open Names
+open Cinstr
+
+exception TooLargeInductive of Pp.t
+
+val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda
+
+val decompose_Llam : lambda -> Name.t array * lambda
+
+val get_alias : Pre_env.env -> Constant.t -> Constant.t
+
+val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda
+
+(** spiwack: this function contains the information needed to perform
+ the static compilation of int31 (trying and obtaining
+ a 31-bit integer in processor representation at compile time) *)
+val compile_structured_int31 : bool -> Constr.t array -> lambda
+
+(** this function contains the information needed to perform
+ the dynamic compilation of int31 (trying and obtaining a
+ 31-bit integer in processor representation at runtime when
+ it failed at compile time *)
+val dynamic_int31_compilation : bool -> lambda array -> lambda
+
+(*spiwack: compiling function to insert dynamic decompilation before
+ matching integers (in case they are in processor representation) *)
+val int31_escape_before_match : bool -> lambda -> lambda
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 2bbb867cd4..236d83576d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -14,7 +14,6 @@
open Util
open Names
-open Constr
open Vmvalues
open Cemitcodes
open Cbytecodes
@@ -25,7 +24,6 @@ open Cbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
-external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
(*******************)
@@ -56,61 +54,12 @@ let set_global v =
(* table pour les structured_constant et les annotations des switchs *)
-let rec eq_structured_constant c1 c2 = match c1, c2 with
-| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
-| Const_ind _, _ -> false
-| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
-| Const_proj _, _ -> false
-| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
-| Const_b0 _, _ -> false
-| Const_bn (t1, a1), Const_bn (t2, a2) ->
- Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| Const_bn _, _ -> false
-| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
-| Const_univ_level _ , _ -> false
-| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
-| Const_type _ , _ -> false
-
-let rec hash_structured_constant c =
- let open Hashset.Combine in
- match c with
- | Const_sorts s -> combinesmall 1 (Sorts.hash s)
- | Const_ind i -> combinesmall 2 (ind_hash i)
- | Const_proj p -> combinesmall 3 (Constant.hash p)
- | Const_b0 t -> combinesmall 4 (Int.hash t)
- | Const_bn (t, a) ->
- let fold h c = combine h (hash_structured_constant c) in
- let h = Array.fold_left fold 0 a in
- combinesmall 5 (combine (Int.hash t) h)
- | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
- | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
-
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
let equal = eq_structured_constant
let hash = hash_structured_constant
end)
-let eq_annot_switch asw1 asw2 =
- let eq_ci ci1 ci2 =
- eq_ind ci1.ci_ind ci2.ci_ind &&
- Int.equal ci1.ci_npar ci2.ci_npar &&
- Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
- in
- let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
- eq_ci asw1.ci asw2.ci &&
- Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
- (asw1.tailcall : bool) == asw2.tailcall
-
-let hash_annot_switch asw =
- let open Hashset.Combine in
- let h1 = Constr.case_info_hash asw.ci in
- let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
- let h3 = if asw.tailcall then 1 else 0 in
- combine3 h1 h2 h3
-
module AnnotTable = Hashtbl.Make (struct
type t = annot_switch
let equal = eq_annot_switch
@@ -205,19 +154,17 @@ and slot_for_fv env fv =
assert false
and eval_to_patch env (buff,pl,fv) =
- let patch = function
- | Reloc_annot a, pos -> (pos, slot_for_annot a)
- | Reloc_const sc, pos -> (pos, slot_for_str_cst sc)
- | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn)
+ let slots = function
+ | Reloc_annot a -> slot_for_annot a
+ | Reloc_const sc -> slot_for_str_cst sc
+ | Reloc_getglobal kn -> slot_for_getglobal env kn
in
- let patches = List.map_left patch pl in
- let buff = patch_int buff patches in
+ let tc = patch buff pl slots in
let vm_env = Array.map (slot_for_fv env) fv in
- let tc = tcode_of_code buff (length buff) in
eval_tcode tc vm_env
and val_of_constr env c =
- match compile true env c with
+ match compile ~fail_on_error:true env c with
| Some v -> eval_to_patch env (to_memory v)
| None -> assert false
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5b9e1a1414..cb7f0ecef3 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -219,7 +219,7 @@ type ('ty,'a) functorize =
type with_declaration =
| WithMod of Id.t list * ModPath.t
- | WithDef of Id.t list * constr Univ.in_universe_context
+ | WithDef of Id.t list * (constr * Univ.AUContext.t option)
type module_alg_expr =
| MEident of ModPath.t
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 738ecc6e1f..fe5a7dfb57 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -468,7 +468,7 @@ type unsafe_type_judgment = types punsafe_type_judgment
(*s Compilation of global declaration *)
-let compile_constant_body = Cbytegen.compile_constant_body false
+let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false
exception Hyp_not_found
@@ -560,7 +560,7 @@ let dispatch =
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 (Cbytegen.op_compilation n op kn);
+ vm_compiling = Some (Clambda.compile_prim n op kn);
native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
}
in
@@ -599,13 +599,13 @@ fun rk value field ->
in
{ empty_reactive_info with
vm_decompile_const = Some int31_decompilation;
- vm_before_match = Some Cbytegen.int31_escape_before_match;
+ 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 Cbytegen.compile_structured_int31;
- vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation;
+ 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;
}
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 749854b8cd..370185a721 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -23,8 +23,9 @@ Declareops
Retroknowledge
Conv_oracle
Pre_env
-Cbytegen
+Clambda
Nativelambda
+Cbytegen
Nativecode
Nativelib
Environ
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b7eb481ee3..6b89a1da03 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -73,13 +73,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
any implementations of parameters and opaques terms,
as long as they have the right type *)
let c', univs, ctx' =
- match cb.const_universes with
- | Monomorphic_const _ ->
- (** We do not add the deferred constraints of the body in the
- environment, because they do not appear in the type of the
- definition. Any inconsistency will be raised at a later stage
- when joining the environment. *)
- let env' = Environ.push_context ~strict:true ctx env' in
+ match cb.const_universes, ctx with
+ | Monomorphic_const _, None ->
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
@@ -91,11 +86,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let c' = Mod_subst.force_constr cs in
c, Reduction.infer_conv env' (Environ.universes env') c c'
in
- let ctx = Univ.ContextSet.of_context ctx in
- c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
- | Polymorphic_const uctx ->
- let inst, ctx = Univ.abstract_universes ctx in
- let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+ c', Monomorphic_const Univ.ContextSet.empty, cst
+ | Polymorphic_const uctx, Some ctx ->
let () =
if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
@@ -116,7 +108,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
in
if not (Univ.Constraint.is_empty cst) then
error_incorrect_with_constraint lab;
- c, Polymorphic_const ctx, Univ.ContextSet.empty
+ c, Polymorphic_const ctx, Univ.Constraint.empty
+ | _ -> error_incorrect_with_constraint lab
in
let def = Def (Mod_subst.from_val c') in
(* let ctx' = Univ.UContext.make (newus, cst) in *)
@@ -225,11 +218,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
let check_with env mp (sign,alg,reso,cst) = function
- |WithDef(idl,c) ->
+ |WithDef(idl, (c, ctx)) ->
let struc = destr_nofunctor sign in
- let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
- NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
+ let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in
+ let wd' = WithDef (idl, (c', ctx)) in
+ NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 29b3e59da8..dfe9d025e4 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -83,9 +83,9 @@ let get_const_prefix env c =
(* A generic map function *)
-let map_lam_with_binders g f n lam =
+let rec map_lam_with_binders g f n lam =
match lam with
- | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
+ | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _
| Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
| Lprod(dom,codom) ->
let dom' = f n dom in
@@ -134,6 +134,19 @@ let map_lam_with_binders g f n lam =
| Lmakeblock(prefix,cn,tag,args) ->
let args' = Array.smartmap (f n) args in
if args == args' then lam else Lmakeblock(prefix,cn,tag,args')
+ | Luint u ->
+ let u' = map_uint g f n u in
+ if u == u' then lam else Luint u'
+
+and map_uint g f n u =
+ match u with
+ | UintVal _ -> u
+ | UintDigits(prefix,c,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then u else UintDigits(prefix,c,args')
+ | UintDecomp(prefix,c,a) ->
+ let a' = f n a in
+ if a == a' then u else UintDecomp(prefix,c,a')
(*s Lift and substitution *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index da7042713f..68f53c3556 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -918,7 +918,6 @@ let dest_prod_assum env =
| LetIn (x,b,t,c) ->
let d = LocalDef (x,b,t) in
prodec_rec (push_rel d env) (Context.Rel.add d l) c
- | Cast (c,_,_) -> prodec_rec env l c
| _ ->
let rty' = whd_all env rty in
if Constr.equal rty' rty then l, rty
@@ -936,7 +935,6 @@ let dest_lam_assum env =
| LetIn (x,b,t,c) ->
let d = LocalDef (x,b,t) in
lamec_rec (push_rel d env) (Context.Rel.add d l) c
- | Cast (c,_,_) -> lamec_rec env l c
| _ -> l,rty
in
lamec_rec env Context.Rel.empty
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 88cf93acc9..24d022d698 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -102,20 +102,18 @@ module Reactive = Map.Make (EntryOrd)
type reactive_info = {(*information required by the compiler of the VM *)
vm_compiling :
(*fastcomputation flag -> continuation -> result *)
- (bool -> Cbytecodes.comp_env -> constr array ->
- int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+ (bool -> Cinstr.lambda array -> Cinstr.lambda)
option;
vm_constant_static :
(*fastcomputation flag -> constructor -> args -> result*)
- (bool->constr array->Cbytecodes.structured_constant)
+ (bool -> constr array -> Cinstr.lambda)
option;
vm_constant_dynamic :
(*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
- (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
- Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+ (bool -> Cinstr.lambda array -> Cinstr.lambda)
option;
(* fastcomputation flag -> cont -> result *)
- vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+ vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
(* tag (= compiled int for instance) -> result *)
vm_decompile_const : (int -> constr) option;
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index e4d78ba14f..134b4b4f7b 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -82,9 +82,8 @@ val initial_retroknowledge : retroknowledge
and the continuation cont of the bytecode compilation
returns the compilation of id in cont if it has a specific treatment
or raises Not_found if id should be compiled as usual *)
-val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env ->
- constr array ->
- int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
+val get_vm_compiling_info : retroknowledge -> entry ->
+ Cinstr.lambda array -> Cinstr.lambda
(*Given an identifier id (usually Construct _)
and its argument array, returns a function that tries an ad-hoc optimisated
compilation (in the case of the 31-bit integers it means compiling them
@@ -93,8 +92,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env ->
CBytecodes.NotClosed if the term is not a closed constructor pattern
(a constant for the compiler) *)
val get_vm_constant_static_info : retroknowledge -> entry ->
- constr array ->
- Cbytecodes.structured_constant
+ constr array -> Cinstr.lambda
(*Given an identifier id (usually Construct _ )
its argument array and a continuation, returns the compiled version
@@ -102,16 +100,14 @@ val get_vm_constant_static_info : retroknowledge -> entry ->
31-bit integers, that would be the dynamic compilation into integers)
or raises Not_found if id should be compiled as usual *)
val get_vm_constant_dynamic_info : retroknowledge -> entry ->
- Cbytecodes.comp_env ->
- Cbytecodes.block array ->
- int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
+ Cinstr.lambda array -> Cinstr.lambda
(** Given a type identifier, this function is used before compiling a match
over this type. In the case of 31-bit integers for instance, it is used
to add the instruction sequence which would perform a dynamic decompilation
in case the argument of the match is not in coq representation *)
-val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
- -> Cbytecodes.bytecodes
+val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda
+ -> Cinstr.lambda
(** Given a type identifier, this function is used by pretyping/vnorm.ml to
recover the elements of that type from their compiled form if it's non
@@ -148,20 +144,18 @@ val find : retroknowledge -> field -> entry
type reactive_info = {(*information required by the compiler of the VM *)
vm_compiling :
(*fastcomputation flag -> continuation -> result *)
- (bool->Cbytecodes.comp_env->constr array ->
- int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+ (bool -> Cinstr.lambda array -> Cinstr.lambda)
option;
vm_constant_static :
(*fastcomputation flag -> constructor -> args -> result*)
- (bool->constr array->Cbytecodes.structured_constant)
+ (bool -> constr array -> Cinstr.lambda)
option;
vm_constant_dynamic :
(*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
- (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
- Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+ (bool -> Cinstr.lambda array -> Cinstr.lambda)
option;
(* fastcomputation flag -> cont -> result *)
- vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+ vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
(* tag (= compiled int for instance) -> result *)
vm_decompile_const : (int -> constr) option;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d0d5cb1d56..e95d5d2b57 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -118,6 +118,15 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let env = check_polymorphic_instance error env auctx auctx' in
env, Univ.make_abstract_instance auctx'
| Cumulative_ind cumi, Cumulative_ind cumi' ->
+ (** Currently there is no way to control variance of inductive types, but
+ just in case we require that they are in a subtyping relation. *)
+ let () =
+ let v = ACumulativityInfo.variance cumi in
+ let v' = ACumulativityInfo.variance cumi' in
+ if not (Array.for_all2 Variance.check_subtype v' v) then
+ CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++
+ str " is not compatible with the one of " ++ KerName.print kn2)
+ in
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
let env = check_polymorphic_instance error env auctx auctx' in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 080bb7ad48..c42b667492 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -266,7 +266,7 @@ struct
module Expr =
struct
type t = Level.t * int
-
+
(* Hashing of expressions *)
module ExprHash =
struct
@@ -487,7 +487,40 @@ struct
| [] -> cons a l
in
List.fold_right (fun a acc -> aux a acc) u []
-
+
+ (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
+ [p], -1 if not found *)
+ let rec max_var_pred p u =
+ let open Level in
+ match u with
+ | [] -> -1
+ | (v, _) :: u ->
+ match var_index v with
+ | Some i when p i -> max i (max_var_pred p u)
+ | _ -> max_var_pred p u
+
+ let rec remap_var u i j =
+ let open Level in
+ match u with
+ | [] -> []
+ | (v, incr) :: u when var_index v = Some i ->
+ (Level.var j, incr) :: remap_var u i j
+ | _ :: u -> remap_var u i j
+
+ let rec compact u max_var i =
+ if i >= max_var then (u,[]) else
+ let j = max_var_pred (fun j -> j < i) u in
+ if Int.equal i (j+1) then
+ let (u,s) = compact u max_var (i+1) in
+ (u, i :: s)
+ else
+ let (u,s) = compact (remap_var u i j) max_var (i+1) in
+ (u, j+1 :: s)
+
+ let compact u =
+ let max_var = max_var_pred (fun _ -> true) u in
+ compact u max_var 0
+
(* Returns the formal universe that is greater than the universes u and v.
Used to type the products. *)
let sup x y = merge_univs x y
@@ -726,6 +759,13 @@ struct
| Invariant, _ | _, Invariant -> Invariant
| Covariant, Covariant -> Covariant
+ let check_subtype x y = match x, y with
+ | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+ | Irrelevant, Covariant -> false
+ | (Covariant | Invariant), Covariant -> true
+ | (Irrelevant | Covariant), Invariant -> false
+ | Invariant, Invariant -> true
+
let pr = function
| Irrelevant -> str "*"
| Covariant -> str "+"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 77ebf5a11b..74d1bfd3a8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -125,6 +125,13 @@ sig
val for_all : (Level.t * int -> bool) -> t -> bool
val map : (Level.t * int -> 'a) -> t -> 'a list
+
+ (** [compact u] remaps local variables in [u] such that their indices become
+ consecutive. It returns the new universe and the mapping.
+ Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
+ [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+ *)
+ val compact : t -> t * int list
end
type universe = Universe.t
@@ -246,6 +253,9 @@ sig
A'] as opposed to [A' <= A]. *)
type t = Irrelevant | Covariant | Invariant
+ (** [check_subtype x y] holds if variance [y] is also an instance of [x] *)
+ val check_subtype : t -> t -> bool
+
val sup : t -> t -> t
val pr : t -> Pp.t
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec18..2d8a1d9761 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,6 +8,7 @@
open Names
open Sorts
open Cbytecodes
+open Univ
(*******************************************)
(* Initalization of the abstract machine ***)
@@ -189,11 +190,11 @@ let rec whd_accu a stk =
| i when Int.equal i type_atom_tag ->
begin match stk with
| [Zapp args] ->
- let u = ref (Obj.obj (Obj.field at 0)) in
- for i = 0 to nargs args - 1 do
- u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
- done;
- Vsort (Type !u)
+ let args = Array.init (nargs args) (arg args) in
+ let u = Obj.obj (Obj.field at 0) in
+ let inst = Instance.of_array (Array.map uni_lvl_val args) in
+ let u = Univ.subst_instance_universe inst u in
+ Vsort (Type u)
| _ -> assert false
end
| i when i <= max_atom_tag ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 23:06:17 +0000