From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/cbytegen.ml | 780 ++++++++++++++++++++--------------------------------- 1 file changed, 297 insertions(+), 483 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b1fc0c85..e2c535e9 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -356,13 +382,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 +389,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 +411,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_of_term c with - | Sort s -> Bstrconst (Const_sorts s) - | Cast(c,_,_) -> str_const c - | App(f,args) -> - begin - match kind_of_term 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 +424,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 @@ -571,6 +451,7 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont | FVuniv_var i -> pos_universe_var i reloc sz :: cont + | FVevar evk -> pos_evar evk reloc :: cont let rec compile_fv reloc l sz cont = match l with @@ -593,112 +474,111 @@ 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_of_term 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 + + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem reloc (FVevar evk) sz cont + else + (** Arguments are reversed in evar instances *) + let args = Array.copy args in + let () = Array.rev args in + comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz 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 + 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_sort s) sz cont + | Lsort (Sorts.Type u) -> + (* We represent universes as a global constant with local universes + "compacted", i.e. as [u arg0 ... argn] where we will substitute (after + evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *) + let u,s = Univ.compact_univ u in + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont else - comp_app compile_str_cst compile_universe reloc - bcst - (Univ.Instance.to_array u) - sz - cont - | Sort (Prop _) | Construct _ -> - compile_str_cst reloc (str_const c) sz cont - | Sort (Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in - (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m - in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont - else - let compile_get_univ reloc idx sz cont = - 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_sort (Sorts.Type u)) (Array.of_list s) sz cont + + | 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 - | 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 = 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_of_term 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 + + | 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 = 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 +589,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 +599,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 = 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 +625,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 +663,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 = 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 +691,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 +718,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 +771,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 +854,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_of_term c with - | Lambda _ -> - let params, body = decompose_lam c in - List.length params , body - | _ -> 0 , c - in let full_arity = arity + universes in let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in let cont_fun = - 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,87 +891,32 @@ 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 -> - let fn = if fail_on_error then CErrors.errorlabstrm "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) - -let compile_constant_body fail_on_error env univs = function + 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 + fn msg; None + +let compile_constant_body ~fail_on_error env univs = function | Undef _ | OpaqueDef _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in let instance_size = match univs with - | None -> 0 - | Some univ -> Univ.UContext.size univ + | Monomorphic_const _ -> 0 + | Polymorphic_const univ -> Univ.AUContext.size univ in - match kind_of_term body with + match kind body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con kn') in + 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_of_kn (canonical_con kn)) - -(* spiwack: additional function which allow different part of compilation of the - 31-bit integers *) - -let make_areconst n else_lbl cont = - if n <= 0 then - 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_of_term 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 +let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) (*(* template compilation for 2ary operation, it probably possible to make a generic such function with arity abstracted *) @@ -1097,47 +955,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 -- cgit v1.2.3