From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 18 Aug 2020 13:07:54 +0200 Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo --- kernel/cbytecodes.ml | 166 --------- kernel/cbytecodes.mli | 78 ---- kernel/cbytegen.ml | 934 ----------------------------------------------- kernel/cbytegen.mli | 31 -- kernel/cemitcodes.ml | 497 ------------------------- kernel/cemitcodes.mli | 46 --- kernel/clambda.ml | 833 ------------------------------------------ kernel/clambda.mli | 45 --- kernel/csymtable.ml | 226 ------------ kernel/csymtable.mli | 22 -- kernel/declarations.ml | 2 +- kernel/declareops.ml | 2 +- kernel/dune | 2 +- kernel/genOpcodeFiles.ml | 6 +- kernel/kernel.mllib | 12 +- kernel/mod_typing.ml | 4 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 4 +- kernel/term_typing.ml | 8 +- kernel/vconv.ml | 2 +- kernel/vm.ml | 2 +- kernel/vmbytecodes.ml | 166 +++++++++ kernel/vmbytecodes.mli | 78 ++++ kernel/vmbytegen.ml | 934 +++++++++++++++++++++++++++++++++++++++++++++++ kernel/vmbytegen.mli | 31 ++ kernel/vmemitcodes.ml | 497 +++++++++++++++++++++++++ kernel/vmemitcodes.mli | 46 +++ kernel/vmlambda.ml | 833 ++++++++++++++++++++++++++++++++++++++++++ kernel/vmlambda.mli | 45 +++ kernel/vmsymtable.ml | 226 ++++++++++++ kernel/vmsymtable.mli | 22 ++ 31 files changed, 2901 insertions(+), 2901 deletions(-) delete mode 100644 kernel/cbytecodes.ml delete mode 100644 kernel/cbytecodes.mli delete mode 100644 kernel/cbytegen.ml delete mode 100644 kernel/cbytegen.mli delete mode 100644 kernel/cemitcodes.ml delete mode 100644 kernel/cemitcodes.mli delete mode 100644 kernel/clambda.ml delete mode 100644 kernel/clambda.mli delete mode 100644 kernel/csymtable.ml delete mode 100644 kernel/csymtable.mli create mode 100644 kernel/vmbytecodes.ml create mode 100644 kernel/vmbytecodes.mli create mode 100644 kernel/vmbytegen.ml create mode 100644 kernel/vmbytegen.mli create mode 100644 kernel/vmemitcodes.ml create mode 100644 kernel/vmemitcodes.mli create mode 100644 kernel/vmlambda.ml create mode 100644 kernel/vmlambda.mli create mode 100644 kernel/vmsymtable.ml create mode 100644 kernel/vmsymtable.mli (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml deleted file mode 100644 index 74405a0105..0000000000 --- a/kernel/cbytecodes.ml +++ /dev/null @@ -1,166 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* str "FVnamed(" ++ Id.print id ++ str ")" - | FVrel i -> str "Rel(" ++ int i ++ str ")" - | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" - | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")" - -let rec pp_instr i = - match i with - | Klabel _ | Ksequence _ -> assert false - | Kacc n -> str "acc " ++ int n - | Kenvacc n -> str "envacc " ++ int n - | Koffsetclosure n -> str "offsetclosure " ++ int n - | Kpush -> str "push" - | Kpop n -> str "pop " ++ int n - | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl - | Kapply n -> str "apply " ++ int n - | Kappterm(n, m) -> - str "appterm " ++ int n ++ str ", " ++ int m - | Kreturn n -> str "return " ++ int n - | Kjump -> str "jump" - | Krestart -> str "restart" - | Kgrab n -> str "grab " ++ int n - | Kgrabrec n -> str "grabrec " ++ int n - | Kclosure(lbl, n) -> - str "closure " ++ pp_lbl lbl ++ str ", " ++ int n - | Kclosurerec(fv,init,lblt,lblb) -> - h 1 (str "closurerec " ++ - int fv ++ str ", " ++ int init ++ - str " types = " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ - str " bodies = " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kclosurecofix (fv,init,lblt,lblb) -> - h 1 (str "closurecofix " ++ - int fv ++ str ", " ++ int init ++ - str " types = " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ - str " bodies = " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal idu -> str "getglobal " ++ Constant.print idu - | Kconst sc -> - str "const " ++ pp_struct_const sc - | Kmakeblock(n, m) -> - str "makeblock " ++ int n ++ str ", " ++ int m - | Kmakeprod -> str "makeprod" - | Kmakeswitchblock(lblt,lbls,_,sz) -> - str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++ - pp_lbl lbls ++ str ", " ++ int sz - | Kswitch(lblc,lblb) -> - h 1 (str "switch " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblc) ++ - str " | " ++ - prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kpushfields n -> str "pushfields " ++ int n - | Kfield n -> str "field " ++ int n - | Ksetfield n -> str "setfield " ++ int n - - | Kstop -> str "stop" - - | Kbranch lbl -> str "branch " ++ pp_lbl lbl - - | Kproj p -> str "proj " ++ Projection.Repr.print p - - | Kensurestackcapacity size -> str "growstack " ++ int size - - | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ - (match id with Some (id,_u) -> Constant.print id | None -> str "") - - | Kcamlprim (op, lbl) -> - str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ - pp_lbl lbl - - | Kareint n -> str "areint " ++ int n - -and pp_bytecodes c = - match c with - | [] -> str "" - | Klabel lbl :: c -> - str "L" ++ int lbl ++ str ":" ++ fnl () ++ - pp_bytecodes c - | Ksequence (l1, l2) :: c -> - pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c - | i :: c -> - pp_instr i ++ fnl () ++ pp_bytecodes c diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli deleted file mode 100644 index b703058fb7..0000000000 --- a/kernel/cbytecodes.mli +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* t - val reset_label_counter : unit -> unit - end - -type instruction = - | Klabel of Label.t - | Kacc of int (** accu = sp[n] *) - | Kenvacc of int (** accu = coq_env[n] *) - | Koffsetclosure of int (** accu = &coq_env[n] *) - | Kpush (** sp = accu :: sp *) - | Kpop of int (** sp = skipn n sp *) - | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) - | Kapply of int (** number of arguments (arguments on top of stack) *) - | Kappterm of int * int (** number of arguments, slot size *) - | Kreturn of int (** slot size *) - | Kjump - | Krestart - | Kgrab of int (** number of arguments *) - | Kgrabrec of int (** rec arg *) - | Kclosure of Label.t * int (** label, number of free variables *) - | Kclosurerec of int * int * Label.t array * Label.t array - (** nb fv, init, lbl types, lbl bodies *) - | Kclosurecofix of int * int * Label.t array * Label.t array - (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of Constant.t - | Kconst of structured_constant - | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 - ** is accu, all others are popped from - ** the top of the stack *) - | Kmakeprod - | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kswitch of Label.t array * Label.t array (** consts,blocks *) - | Kpushfields of int - | Kfield of int (** accu = accu[n] *) - | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) - | Kstop - | Ksequence of bytecodes * bytecodes - | Kproj of Projection.Repr.t - | Kensurestackcapacity of int - - | Kbranch of Label.t (** jump to label, is it needed ? *) - | Kprim of CPrimitives.t * pconstant option - | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int - -and bytecodes = instruction list - -val pp_bytecodes : bytecodes -> Pp.t - -type fv_elem = - FVnamed of Id.t -| FVrel of int -| FVuniv_var of int -| FVevar of Evar.t - -type fv = fv_elem array - -val pp_fv_elem : fv_elem -> Pp.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml deleted file mode 100644 index bacc308e1f..0000000000 --- a/kernel/cbytegen.ml +++ /dev/null @@ -1,934 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* *) -(* type = [Ct1 | .... | Ctn] *) -(* Ci is the code pointer of the i-th body *) -(* At runtime, a fixpoint environment (which is the same as the fixpoint *) -(* itself) is a pointer to the field holding its code pointer. *) -(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint *) -(* and de Bruijn [1] the last one. *) -(* Access to these variables is performed by the [Koffsetclosure n] *) -(* instruction that shifts the environment pointer of [n] fields. *) - -(* This allows representing mutual fixpoints in just one block. *) -(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *) -(* types. They are used in conversion tests (which requires that *) -(* fixpoint types must be convertible). Their environment is the one of *) -(* the last fixpoint : *) -(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) -(* ^ *) - -(* Representation of mutual cofix : *) -(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) -(* ... *) -(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) -(* *) -(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *) -(* ^ *) -(* ... *) -(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) -(* ^ *) -(* The [ai] blocks are functions that accumulate their arguments: *) -(* ai arg1 argp ---> *) -(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) -(* If such a block is matched against, we have to force evaluation, *) -(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) -(* (note that [ai'] is a pointer to the closure, passed as argument) *) -(* Once evaluation is completed [ai'] is updated with the result: *) -(* ai' <-- *) -(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) -(* This representation is nice because the application of the cofix is *) -(* evaluated only once (it simulates a lazy evaluation) *) -(* Moreover, when cofix don't have arguments, it is possible to create *) -(* a cycle, e.g.: *) -(* cofix one := cons 1 one *) -(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) -(* fcofix1 = [clos_t | code | a1] *) -(* The result of evaluating [a1] is [cons_t | 1 | a1]. *) -(* When [a1] is updated : *) -(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) -(* The cycle is created ... *) -(* *) -(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) -(* conversion of cofixpoints (which is intentional). *) - -module Fv_elem = -struct -type t = fv_elem - -let compare e1 e2 = match e1, e2 with -| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 -| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 -| FVrel _, FVnamed _ -> 1 -| FVrel r1, FVrel r2 -> Int.compare r1 r2 -| FVrel _, (FVuniv_var _ | FVevar _) -> -1 -| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var _, (FVnamed _ | FVrel _) -> 1 -| FVuniv_var _, FVevar _ -> -1 -| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 -| FVevar e1, FVevar e2 -> Evar.compare e1 e2 - -end - -module FvMap = Map.Make(Fv_elem) - -(*spiwack: both type have been moved from Cbytegen because I needed then - for the retroknowledge *) -type vm_env = { - size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) - fv_fwd : int FvMap.t; (* reverse mapping *) - } - - -type comp_env = { - arity : int; (* arity of the current function, 0 if none *) - nb_uni_stack : int ; (* number of universes on the stack, *) - (* universes are always at the bottom. *) - nb_stack : int; (* number of variables on the stack *) - in_stack : int Range.t; (* position in the stack *) - nb_rec : int; (* number of mutually recursive functions *) - pos_rec : instruction list; (* instruction d'acces pour les variables *) - (* de point fix ou de cofix *) - offset : int; - in_env : vm_env ref (* The free variables of the expression *) - } - -module Config = struct - let stack_threshold = 256 (* see byterun/coq_memory.h *) - let stack_safety_margin = 15 -end - -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 = { - size = e.size + 1; - fv_rev = d :: e.fv_rev; - fv_fwd = FvMap.add d e.size e.fv_fwd; -} - -let fv r = !(r.in_env) - -let empty_comp_env ()= - { arity = 0; - nb_uni_stack = 0; - nb_stack = 0; - in_stack = Range.empty; - nb_rec = 0; - pos_rec = []; - offset = 0; - in_env = ref empty_fv - } - -(* Maximal stack size reached during the current function body. Used to - reallocate the stack if we lack space. *) -let max_stack_size = ref 0 - -let set_max_stack_size stack_size = - if stack_size > !max_stack_size then - max_stack_size := stack_size - -let ensure_stack_capacity f x = - let old = !max_stack_size in - max_stack_size := 0; - let code = f x in - let used_safe = - !max_stack_size + Config.stack_safety_margin - in - max_stack_size := old; - if used_safe > Config.stack_threshold then - Kensurestackcapacity used_safe :: code - else code - -(*i Creation functions for comp_env *) - -let rec add_param n sz l = - if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l) - -let comp_env_fun ?(univs=0) arity = - { arity; - nb_uni_stack = univs ; - nb_stack = arity; - in_stack = add_param arity 0 Range.empty; - nb_rec = 0; - pos_rec = []; - offset = 1; - in_env = ref empty_fv - } - - -let comp_env_fix_type rfv = - { arity = 0; - nb_uni_stack = 0; - nb_stack = 0; - in_stack = Range.empty; - nb_rec = 0; - pos_rec = []; - offset = 1; - in_env = rfv - } - -let comp_env_fix ndef curr_pos arity rfv = - let prec = ref [] in - for i = ndef downto 1 do - prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec - done; - { arity; - nb_uni_stack = 0; - nb_stack = arity; - in_stack = add_param arity 0 Range.empty; - nb_rec = ndef; - pos_rec = !prec; - offset = 2 * (ndef - curr_pos - 1)+1; - in_env = rfv - } - -let comp_env_cofix_type ndef rfv = - { arity = 0; - nb_uni_stack = 0; - nb_stack = 0; - in_stack = Range.empty; - nb_rec = 0; - pos_rec = []; - offset = 1+ndef; - in_env = rfv - } - -let comp_env_cofix ndef arity rfv = - let prec = ref [] in - for i = 1 to ndef do - prec := Kenvacc i :: !prec - done; - { arity; - nb_uni_stack = 0; - nb_stack = arity; - in_stack = add_param arity 0 Range.empty; - nb_rec = ndef; - pos_rec = !prec; - offset = ndef+1; - in_env = rfv - } - -(* [push_param ] add function parameters on the stack *) -let push_param n sz r = - { r with - nb_stack = r.nb_stack + n; - in_stack = add_param n sz r.in_stack } - -(* [push_local sz r] add a new variable on the stack at position [sz] *) -let push_local sz r = - { r with - nb_stack = r.nb_stack + 1; - in_stack = Range.cons (sz + 1) r.in_stack } - -(*i Compilation of variables *) -let find_at fv env = FvMap.find fv env.fv_fwd - -let pos_named id r = - let env = !(r.in_env) in - let cid = FVnamed id in - try Kenvacc(r.offset + find_at cid env) - with Not_found -> - let pos = env.size in - r.in_env := push_fv cid env; - Kenvacc (r.offset + pos) - -let pos_rel i r sz = - if i <= r.nb_stack then - Kacc(sz - (Range.get r.in_stack (i-1))) - else - let i = i - r.nb_stack in - if i <= r.nb_rec then - try List.nth r.pos_rec (i-1) - with (Failure _|Invalid_argument _) -> assert false - else - let i = i - r.nb_rec in - let db = FVrel(i) in - let env = !(r.in_env) in - try Kenvacc(r.offset + find_at db env) - with Not_found -> - let pos = env.size in - r.in_env := push_fv db env; - Kenvacc(r.offset + pos) - -let pos_universe_var i r sz = - (* Compilation of a universe variable can happen either at toplevel (the - current closure correspond to a constant and has local universes) or in a - local closure (which has no local universes). *) - if r.nb_uni_stack != 0 then - (* Universe variables are represented by De Bruijn levels (not indices), - starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] - with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access - the last universe. *) - Kacc (sz - r.arity - (r.nb_uni_stack - i)) - else - let env = !(r.in_env) in - let db = FVuniv_var i in - try Kenvacc (r.offset + find_at db env) - with Not_found -> - let pos = env.size in - r.in_env := push_fv db env; - Kenvacc(r.offset + pos) - -let pos_evar evk r = - let env = !(r.in_env) in - let cid = FVevar evk in - try Kenvacc(r.offset + find_at cid env) - with Not_found -> - 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. *) -(* This function is to be applied to the continuation before adding a *) -(* non-terminating instruction (branch, raise, return, appterm) *) -(* in front of it. *) - -let discard_dead_code cont = cont -(*function - [] -> [] - | (Klabel _ | Krestart ) :: _ as cont -> cont - | _ :: cont -> discard_dead_code cont -*) - -(* Return a label to the beginning of the given continuation. *) -(* If the sequence starts with a branch, use the target of that branch *) -(* as the label, thus avoiding a jump to a jump. *) - -let label_code = function - | Klabel lbl :: _ as cont -> (lbl, cont) - | Kbranch lbl :: _ as cont -> (lbl, cont) - | cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont) - -(* Return a branch to the continuation. That is, an instruction that, - when executed, branches to the continuation or performs what the - continuation performs. We avoid generating branches to returns. *) -(* spiwack: make_branch was only used once. Changed it back to the ZAM - one to match the appropriate semantics (old one avoided the - introduction of an unconditional branch operation, which seemed - appropriate for the 31-bit integers' code). As a memory, I leave - the former version in this comment. -let make_branch cont = - match cont with - | (Kreturn _ as return) :: cont' -> return, cont' - | Klabel lbl as b :: _ -> b, cont - | _ -> let b = Klabel(Label.create()) in b,b::cont -*) - -let rec make_branch_2 lbl n cont = - function - Kreturn m :: _ -> (Kreturn (n + m), cont) - | Klabel _ :: c -> make_branch_2 lbl n cont c - | Kpop m :: c -> make_branch_2 lbl (n + m) cont c - | _ -> - match lbl with - Some lbl -> (Kbranch lbl, cont) - | None -> let lbl = Label.create() in (Kbranch lbl, Klabel lbl :: cont) - -let make_branch cont = - match cont with - (Kbranch _ as branch) :: _ -> (branch, cont) - | (Kreturn _ as return) :: _ -> (return, cont) - | Klabel lbl :: _ -> make_branch_2 (Some lbl) 0 cont cont - | _ -> make_branch_2 (None) 0 cont cont - -(* Check if we're in tailcall position *) - -let rec is_tailcall = function - | Kreturn k :: _ -> Some k - | Klabel _ :: c -> is_tailcall c - | _ -> None - -(* Extension of the continuation *) - -(* Add a Kpop n instruction in front of a continuation *) -let rec add_pop n = function - | Kpop m :: cont -> add_pop (n+m) cont - | Kreturn m:: cont -> Kreturn (n+m) ::cont - | cont -> if Int.equal n 0 then cont else Kpop n :: cont - -let add_grab arity lbl cont = - if Int.equal arity 1 then Klabel lbl :: cont - else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont - -let add_grabrec rec_arg arity lbl cont = - if Int.equal arity 1 && rec_arg < arity then - Klabel lbl :: Kgrabrec 0 :: Krestart :: cont - else - Krestart :: Klabel lbl :: Kgrabrec rec_arg :: - Krestart :: Kgrab (arity - 1) :: cont - -(* continuation of a cofix *) - -let cont_cofix arity = - (* accu = res *) - (* stk = ai::args::ra::... *) - (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *) - [ Kpush; - Kpush; (* stk = res::res::ai::args::ra::... *) - Kacc 2; - Kfield 1; - Kfield 0; - Kmakeblock(2, cofix_evaluated_tag); - Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*) - Kacc 2; - Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *) - (* stk = res::ai::args::ra::... *) - Kacc 0; (* accu = res *) - Kreturn (arity+2) ] - - -(* Code of closures *) -let fun_code = ref [] - -let init_fun_code () = fun_code := [] - -(* Compilation of constructors and inductive types *) - - -(* -If [tag] hits the OCaml limitation for non constant constructors, we switch to -another representation for the remaining constructors: -[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args] - -We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation. - *) - -let nest_block tag arity cont = - Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) :: - Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont - -let code_makeblock ~stack_size ~arity ~tag cont = - if tag < Obj.last_non_constant_constructor_tag then - Kmakeblock(arity, tag) :: cont - else begin - set_max_stack_size (stack_size + 1); - Kpush :: nest_block tag arity cont - end - -let compile_structured_constant _cenv sc sz cont = - set_max_stack_size sz; - Kconst sc :: cont - -(* compiling application *) -let comp_args comp_expr cenv args sz cont = - let nargs_m_1 = Array.length args - 1 in - let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in - for i = 1 to nargs_m_1 do - c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) - done; - !c - -let comp_app comp_fun comp_arg cenv f args sz cont = - let nargs = Array.length args in - if Int.equal nargs 0 then comp_fun cenv f sz cont - else - match is_tailcall cont with - | Some k -> - comp_args comp_arg cenv args sz - (Kpush :: - comp_fun cenv f (sz + nargs) - (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) - | None -> - if nargs <= 4 then - comp_args comp_arg cenv args sz - (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) - else - let lbl,cont1 = label_code cont in - Kpush_retaddr lbl :: - (comp_args comp_arg cenv args (sz + 3) - (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) - -(* Compiling free variables *) - -let compile_fv_elem cenv fv sz cont = - match fv with - | FVrel i -> pos_rel i cenv sz :: cont - | FVnamed id -> pos_named id cenv :: cont - | FVuniv_var i -> pos_universe_var i cenv sz :: cont - | FVevar evk -> pos_evar evk cenv :: cont - -let rec compile_fv cenv l sz cont = - match l with - | [] -> cont - | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont - | fvn :: tl -> - compile_fv_elem cenv fvn sz - (Kpush :: compile_fv cenv tl (sz + 1) cont) - - -(* 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 - | BCalias kn' -> get_alias env kn' - | _ -> kn) - -(* Some primitives are not implemented natively by the VM, but calling OCaml - code instead *) -let is_caml_prim = let open CPrimitives in function - | Arraymake - | Arrayget - | Arraydefault - | Arrayset - | Arraycopy - | Arrayreroot - | Arraylength -> true - | _ -> false - -(* sz is the size of the local stack *) -let rec compile_lam env cenv lam sz cont = - set_max_stack_size sz; - match lam with - | Lrel(_, i) -> pos_rel i cenv sz :: cont - - | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont - - | Lval v -> compile_structured_constant cenv (Const_val v) sz cont - - | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont - - | Lfloat f -> compile_structured_constant cenv (Const_float f) sz cont - - | Lproj (p,arg) -> - compile_lam env cenv arg sz (Kproj p :: cont) - - | Lvar id -> pos_named id cenv :: cont - - | Levar (evk, args) -> - if Array.is_empty args then - compile_fv_elem cenv (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) cenv (FVevar evk) args sz cont - - | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont - - | Lind (ind,u) -> - if Univ.Instance.is_empty u then - compile_structured_constant cenv (Const_ind ind) sz cont - else comp_app compile_structured_constant compile_universe cenv - (Const_ind ind) (Univ.Instance.to_array u) sz cont - - | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) -> - compile_structured_constant cenv (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 cenv idx sz cont = - set_max_stack_size sz; - compile_fv_elem cenv (FVuniv_var idx) sz cont - in - if List.is_empty s then - compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont - else - comp_app compile_structured_constant compile_get_univ cenv - (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont - - | Llet (_id,def,body) -> - compile_lam env cenv def sz - (Kpush :: - compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) - - | Lprod (dom,codom) -> - let cont1 = - Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in - compile_lam env cenv 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 cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) - - | Lapp (f, args) -> - begin match f with - | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont - | _ -> comp_app (compile_lam env) (compile_lam env) cenv 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 - (* Compiling types *) - let env_type = comp_env_fix_type rfv in - for i = 0 to ndef - 1 do - let fcode = - ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] - in - 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_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_lam env env_body body arity) [Kreturn arity] - in - let lbl = Label.create () in - lbl_bodies.(i) <- lbl; - let fcode = add_grabrec rec_args.(i) arity lbl cont1 in - fun_code := [Ksequence(fcode,!fun_code)] - done; - let fv = !rfv in - compile_fv cenv fv.fv_rev sz - (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - - - | 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 *) - let rfv = ref empty_fv in - let env_type = comp_env_cofix_type ndef rfv in - for i = 0 to ndef - 1 do - let fcode = - ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] - in - 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_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_lam env env_body body (arity+1) (cont_cofix arity) - in - let cont = ensure_stack_capacity comp arity in - lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; - done; - let fv = !rfv in - set_max_stack_size (sz + fv.size + ndef + 2); - compile_fv cenv fv.fv_rev sz - (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) - - | Lif(t, bt, bf) -> - let branch, cont = make_branch cont in - let lbl_true = Label.create() in - let lbl_false = Label.create() in - compile_lam env cenv t sz - (Kswitch([|lbl_true;lbl_false|],[||]) :: - Klabel lbl_false :: - compile_lam env cenv bf sz - (branch :: - Klabel lbl_true :: - compile_lam env cenv bt sz cont)) - - | Lcase(ci,rtbl,t,a,branches) -> - let ind = ci.ci_ind in - let mib = lookup_mind (fst ind) env in - let oib = mib.mind_packets.(snd ind) 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 (Obj.last_non_constant_constructor_tag + 1) in - let lbl_blocks = Array.make nblock Label.no in - let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in - let lbl_eblocks = Array.make neblock Label.no in - let branch1, cont = make_branch cont in - (* Compilation of the return type *) - let fcode = - ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] - in - let lbl_typ,fcode = label_code fcode in - fun_code := [Ksequence(fcode,!fun_code)]; - (* 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 - | Kbranch _ -> sz+3, Kjump, false - | _ -> assert false - in - - let c = ref cont in - (* Perform the extra match if needed (too many block constructors) *) - if neblock <> 0 then begin - let lbl_b, code_b = - label_code ( - Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in - lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b; - c := code_b - end; - - (* Compilation of constant branches *) - for i = nconst - 1 downto 0 do - let aux = - compile_lam env cenv 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 cenv) - body (sz_b+arity) (add_pop arity (branch::!c)) in - let code_b = - if tag < Obj.last_non_constant_constructor_tag then begin - set_max_stack_size (sz_b + arity); - Kpushfields arity :: code_b - end - else begin - 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 < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b - else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b; - c := code_b - done; - - let annot = - {rtbl = rtbl; tailcall = is_tailcall; - max_stack_size = !max_stack_size - sz} - in - - (* Compiling branch for accumulators *) - let lbl_accu, code_accu = - set_max_stack_size (sz+3); - label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) - in - lbl_blocks.(0) <- lbl_accu; - - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; - let code_sw = - match branch1 with - (* spiwack : branch1 can't be a lbl anymore it's a Branch instead - | Klabel lbl -> Kpush_retaddr lbl :: !c *) - | Kbranch lbl -> Kpush_retaddr lbl :: !c - | _ -> !c - in - compile_lam env cenv 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) cenv args sz cont - - | Lprim (Some (kn,u), op, args) when is_caml_prim op -> - let arity = CPrimitives.arity op in - let nparams = CPrimitives.nparams op in - let nargs = arity - nparams in - assert (arity = Array.length args && arity <= 4); - let (jump, cont) = make_branch cont in - let lbl_default = Label.create () in - let default = - let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in - let cont = - if Univ.Instance.is_empty u then cont - else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) - in - Klabel lbl_default :: - Kpush :: - if Int.equal nparams 0 then cont - else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) - in - fun_code := [Ksequence(default, !fun_code)]; - comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) - - | Lprim (kn, op, args) -> - comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) - -and compile_get_global cenv (kn,u) sz cont = - set_max_stack_size sz; - if Univ.Instance.is_empty u then - Kgetglobal kn :: cont - else - comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_universe cenv () (Univ.Instance.to_array u) sz cont - -and compile_universe cenv uni sz cont = - set_max_stack_size sz; - match Univ.Level.var_index uni with - | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont - | Some idx -> pos_universe_var idx cenv sz :: cont - -and compile_constant env cenv 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 cenv (kn,u) sz cont) - (compile_lam env) cenv () args sz cont - else - let compile_arg cenv constr_or_uni sz cont = - match constr_or_uni with - | ArgLambda t -> compile_lam env cenv t sz cont - | ArgUniv uni -> compile_universe cenv 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 cenv () all sz cont - -let is_univ_copy max u = - let u = Univ.Instance.to_array u in - if Array.length u = max then - Array.fold_left_i (fun i acc u -> - if acc then - match Univ.Level.var_index u with - | None -> false - | Some l -> l = i - else false) true u - else - false - -let dump_bytecode = ref false - -let dump_bytecodes init code fvs = - let open Pp in - (str "code =" ++ fnl () ++ - pp_bytecodes init ++ fnl () ++ - pp_bytecodes code ++ fnl () ++ - str "fv = " ++ - prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ - fnl ()) - -let compile ~fail_on_error ?universes:(universes=0) env c = - init_fun_code (); - Label.reset_label_counter (); - let cont = [Kstop] in - try - let cenv, init_code = - if Int.equal universes 0 then - let lam = lambda_of_constr ~optimize:true env c in - let cenv = empty_comp_env () in - cenv, ensure_stack_capacity (compile_lam env cenv 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 cenv = empty_comp_env () 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_lam env r_fun body full_arity) - [Kreturn full_arity] - in - fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; - let fv = fv r_fun in - let init_code = - ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) - (Kclosure(lbl_fun,fv.size) :: cont) - in - cenv, init_code - in - let fv = List.rev (!(cenv.in_env).fv_rev) in - (if !dump_bytecode then - Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; - Some (init_code,!fun_code, Array.of_list fv) - with TooLargeInductive msg as exn -> - let _, info = Exninfo.capture exn in - let fn = if fail_on_error then - CErrors.user_err ?loc:None ~info ~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 _ | Primitive _ -> Some BCconstant - | Def sb -> - let body = Mod_subst.force_constr sb in - let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in - 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.make1 (Constant.canonical kn') in - Some (BCalias (get_alias env con)) - | _ -> - 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)) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli deleted file mode 100644 index d5ea2509ef..0000000000 --- a/kernel/cbytegen.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option -(** init, fun, fv *) - -val compile_constant_body : fail_on_error:bool -> - env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def -> - body_code option - -(** Shortcut of the previous function used during module strengthening *) - -val compile_alias : Names.Constant.t -> body_code - -(** Dump the bytecode after compilation (for debugging purposes) *) -val dump_bytecode : bool ref diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml deleted file mode 100644 index ed475dca7e..0000000000 --- a/kernel/cemitcodes.ml +++ /dev/null @@ -1,497 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 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 - | Reloc_proj_name of Projection.Repr.t - | Reloc_caml_prim of CPrimitives.t - -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 -| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 -| Reloc_proj_name _, _ -> false -| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 -| Reloc_caml_prim _, _ -> 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) - | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) - | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) - -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; - Bytes.unsafe_set buff (pos + 1) c2; - Bytes.unsafe_set buff (pos + 2) c3; - Bytes.unsafe_set buff (pos + 3) c4 - -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)) - -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 iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in - let () = CArray.iter iter reloc in - 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 - -(* Buffering of bytecode *) - -type label_definition = - Label_defined of int - | Label_undefined of (int * int) list - -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 - else - if len = Sys.max_string_length - 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 env.out_buffer 0 new_buffer 0 len; - env.out_buffer <- new_buffer - end; - patch_char4 env.out_buffer p (Char.unsafe_chr b1) - (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); - env.out_position <- p + 4 - -let out env opcode = - out_word env opcode 0 0 0 - -let is_immed i = Uint63.le (Uint63.of_int i) Uint63.maxuint31 - -let out_int env n = - out_word env n (n asr 8) (n asr 16) (n asr 24) - -(* Handling of local labels and backpatching *) - -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 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 (fun p -> backpatch env p) patchlist; - (env.label_table).(lbl) <- Label_defined env.out_position - -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 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 *) - (env.label_table).(lbl) <- - Label_undefined((env.out_position, orig) :: patchlist); - out_int env 0 - -let out_label env l = out_label_with_orig env env.out_position l - -(* Relocation information *) - -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 slot_for_const env c = - enter env (Reloc_const c); - out_int env 0 - -let slot_for_annot env a = - enter env (Reloc_annot a); - out_int env 0 - -let slot_for_getglobal env p = - enter env (Reloc_getglobal p); - out_int env 0 - -let slot_for_proj_name env p = - enter env (Reloc_proj_name p); - out_int env 0 - -let slot_for_caml_prim env op = - enter env (Reloc_caml_prim op); - out_int env 0 - -(* Emission of one instruction *) - -let nocheck_prim_op = function - | Int63add -> opADDINT63 - | Int63sub -> opSUBINT63 - | Int63lt -> opLTINT63 - | Int63le -> opLEINT63 - | _ -> assert false - - -let check_prim_op = function - | Int63head0 -> opCHECKHEAD0INT63 - | Int63tail0 -> opCHECKTAIL0INT63 - | Int63add -> opCHECKADDINT63 - | Int63sub -> opCHECKSUBINT63 - | Int63mul -> opCHECKMULINT63 - | Int63div -> opCHECKDIVINT63 - | Int63mod -> opCHECKMODINT63 - | Int63lsr -> opCHECKLSRINT63 - | Int63lsl -> opCHECKLSLINT63 - | Int63land -> opCHECKLANDINT63 - | Int63lor -> opCHECKLORINT63 - | Int63lxor -> opCHECKLXORINT63 - | Int63addc -> opCHECKADDCINT63 - | Int63subc -> opCHECKSUBCINT63 - | Int63addCarryC -> opCHECKADDCARRYCINT63 - | Int63subCarryC -> opCHECKSUBCARRYCINT63 - | Int63mulc -> opCHECKMULCINT63 - | Int63diveucl -> opCHECKDIVEUCLINT63 - | Int63div21 -> opCHECKDIV21INT63 - | Int63addMulDiv -> opCHECKADDMULDIVINT63 - | Int63eq -> opCHECKEQINT63 - | Int63lt -> opCHECKLTINT63 - | Int63le -> opCHECKLEINT63 - | Int63compare -> opCHECKCOMPAREINT63 - | Float64opp -> opCHECKOPPFLOAT - | Float64abs -> opCHECKABSFLOAT - | Float64eq -> opCHECKEQFLOAT - | Float64lt -> opCHECKLTFLOAT - | Float64le -> opCHECKLEFLOAT - | Float64compare -> opCHECKCOMPAREFLOAT - | Float64classify -> opCHECKCLASSIFYFLOAT - | Float64add -> opCHECKADDFLOAT - | Float64sub -> opCHECKSUBFLOAT - | Float64mul -> opCHECKMULFLOAT - | Float64div -> opCHECKDIVFLOAT - | Float64sqrt -> opCHECKSQRTFLOAT - | Float64ofInt63 -> opCHECKFLOATOFINT63 - | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA - | Float64frshiftexp -> opCHECKFRSHIFTEXP - | Float64ldshiftexp -> opCHECKLDSHIFTEXP - | Float64next_up -> opCHECKNEXTUPFLOAT - | Float64next_down -> opCHECKNEXTDOWNFLOAT - | Arraymake -> opISINT_CAML_CALL2 - | Arrayget -> opISARRAY_INT_CAML_CALL2 - | Arrayset -> opISARRAY_INT_CAML_CALL3 - | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> - opISARRAY_CAML_CALL1 - -let emit_instr env = function - | Klabel lbl -> define_label env lbl - | Kacc 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 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 env (opOFFSETCLOSURE0 + ofs / 2) - else (out env opOFFSETCLOSURE; out_int env ofs) - | Kpush -> - out env opPUSH - | Kpop n -> - out env opPOP; out_int env n - | Kpush_retaddr lbl -> - out env opPUSH_RETADDR; out_label env lbl - | Kapply 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 env(opAPPTERM1 + n - 1); out_int env sz) - else (out env opAPPTERM; out_int env n; out_int env sz) - | Kreturn n -> - out env opRETURN; out_int env n - | Kjump -> - out env opRETURN; out_int env 0 - | Krestart -> - out env opRESTART - | Kgrab n -> - out env opGRAB; out_int env n - | Kgrabrec(rec_arg) -> - out env opGRABREC; out_int env rec_arg - | Kclosure(lbl, n) -> - out env opCLOSURE; out_int env n; out_label env lbl - | Kclosurerec(nfv,init,lbl_types,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 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 env opGETGLOBAL; slot_for_getglobal env q - | Kconst (Const_b0 i) when is_immed i -> - if i >= 0 && i <= 3 - then out env (opCONST0 + i) - else (out env opCONSTINT; out_int env i) - | Kconst 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 env(opMAKEBLOCK1 + n - 1); out_int env t) - else (out env opMAKEBLOCK; out_int env n; out_int env t) - | Kmakeprod -> - out env opMAKEPROD - | Kmakeswitchblock(typlbl,swlbl,annot,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 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 env opPUSHFIELDS;out_int env n - | Kfield n -> - if n <= 1 then out env (opGETFIELD0+n) - else (out env opGETFIELD;out_int env n) - | Ksetfield n -> - if n <= 1 then out env (opSETFIELD0+n) - else (out env opSETFIELD;out_int env n) - | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p - | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size - | Kbranch lbl -> out env opBRANCH; out_label env lbl - | Kprim (op,None) -> - out env (nocheck_prim_op op) - - | Kprim(op,Some (q,_u)) -> - out env (check_prim_op op); - slot_for_getglobal env q - - | Kcamlprim (op,lbl) -> - out env (check_prim_op op); - out_label env lbl; - slot_for_caml_prim env op - - | Kareint 1 -> out env opISINT - | Kareint 2 -> out env opAREINT2; - - | Kstop -> out env opSTOP - - | Kareint _ -> assert false - -(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) - -let rec emit env insns remaining = match insns with - | [] -> - (match remaining with - [] -> () - | (first::rest) -> emit env first rest) - (* Peephole optimizations *) - | Kpush :: Kacc n :: c -> - 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 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 env(opPUSHOFFSETCLOSURE0 + ofs / 2) - else (out env opPUSHOFFSETCLOSURE; out_int env ofs); - emit env c remaining - | Kpush :: Kgetglobal id :: c -> - out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining - | Kpush :: Kconst (Const_b0 i) :: c when is_immed i -> - if i >= 0 && i <= 3 - then out env (opPUSHCONST0 + i) - else (out env opPUSHCONSTINT; out_int env i); - emit env c remaining - | Kpush :: Kconst const :: c -> - out env opPUSHGETGLOBAL; slot_for_const env const; - emit env c remaining - | Kpop n :: Kjump :: c -> - out env opRETURN; out_int env n; emit env c remaining - | Ksequence(c1,c2)::c -> - emit env c1 (c2::c::remaining) - (* Default case *) - | instr :: c -> - emit_instr env instr; emit env c remaining - -(* Initialization *) - -type to_patch = emitcodes * patches * fv - -(* Substitution *) -let subst_strcst s sc = - match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ - | Const_float _ -> sc - | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) - -let subst_annot _ (a : annot_switch) = a - -let subst_reloc s ri = - match ri with - | Reloc_annot a -> Reloc_annot (subst_annot s a) - | Reloc_const sc -> Reloc_const (subst_strcst s sc) - | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) - | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) - | Reloc_caml_prim _ -> ri - -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, subst_patches s pl, fv - -type body_code = - | BCdefined of to_patch - | BCalias of Names.Constant.t - | BCconstant - -type to_patch_substituted = -| PBCdefined of to_patch substituted -| PBCalias of Names.Constant.t substituted -| PBCconstant - -let from_val = function -| BCdefined tp -> PBCdefined (from_val tp) -| BCalias cu -> PBCalias (from_val cu) -| BCconstant -> PBCconstant - -let force = function -| PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCalias cu -> BCalias (force subst_constant cu) -| PBCconstant -> BCconstant - -let subst_to_patch_subst s = function -| PBCdefined tp -> PBCdefined (subst_substituted s tp) -| PBCalias cu -> PBCalias (subst_substituted s cu) -| PBCconstant -> PBCconstant - -let repr_body_code = function -| PBCdefined tp -> - let (s, tp) = repr_substituted tp in - (s, BCdefined tp) -| PBCalias cu -> - let (s, cu) = repr_substituted cu in - (s, BCalias cu) -| PBCconstant -> (None, BCconstant) - -let to_memory (init_code, fun_code, fv) = - 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 env.out_buffer 0 env.out_position in - let code = CString.hcons code 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 = []))) env.label_table; - (code, reloc, fv) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli deleted file mode 100644 index c4262f3380..0000000000 --- a/kernel/cemitcodes.mli +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* patches -> (reloc_info -> int) -> Vmvalues.tcode - -type to_patch = emitcodes * patches * fv - -type body_code = - | BCdefined of to_patch - | BCalias of Constant.t - | BCconstant - - -type to_patch_substituted - -val from_val : body_code -> to_patch_substituted - -val force : to_patch_substituted -> body_code - -val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted - -val repr_body_code : - to_patch_substituted -> Mod_subst.substitution list option * body_code - -val to_memory : bytecodes * bytecodes * fv -> to_patch - (** init code, fun code, fv *) diff --git a/kernel/clambda.ml b/kernel/clambda.ml deleted file mode 100644 index 6690a379ce..0000000000 --- a/kernel/clambda.ml +++ /dev/null @@ -1,833 +0,0 @@ -open Util -open Names -open Esubst -open Term -open Constr -open Declarations -open Vmvalues -open Environ -open Pp - -let pr_con sp = str(Names.Label.to_string (Constant.label sp)) - -type lambda = - | Lrel of Name.t * int - | Lvar of Id.t - | Levar of Evar.t * lambda array - | Lprod of lambda * lambda - | Llam of Name.t Context.binder_annot array * lambda - | Llet of Name.t Context.binder_annot * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) - | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lint of int - | Lmakeblock of int * lambda array - | Luint of Uint63.t - | Lfloat of Float64.t - | Lval of structured_values - | Lsort of Sorts.t - | Lind of pinductive - | Lproj of Projection.Repr.t * lambda - -(* We separate branches for constant and non-constant constructors. If the OCaml - limitation on non-constant constructors is reached, remaining branches are - stored in [extra_branches]. *) -and lam_branches = - { constant_branches : lambda array; - nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } -(* extra_branches : (name array * lambda) array } *) - -and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array - -(** Printing **) - -let pr_annot x = Name.print x.Context.binder_name - -let pp_names ids = - prlist_with_sep (fun _ -> brk(1,1)) pr_annot (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" - | InSProp -> str "SProp" - | InType -> str "Type" - -let rec pp_lam lam = - match lam with - | Lrel (id,n) -> pp_rel id n - | Lvar id -> Id.print id - | Levar (evk, args) -> - hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") - | 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 " ++ - pr_annot 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") - | Lif (t, bt, bf) -> - v 0 (str "(if " ++ pp_lam t ++ - cut () ++ str "then " ++ pp_lam bt ++ - cut() ++ str "else " ++ pp_lam bf ++ str ")") - | 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) -> - pr_annot 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) -> - pr_annot 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")") - | Luint i -> str (Uint63.to_string i) - | Lfloat f -> str (Float64.to_string f) - | Lval _ -> str "values" - | Lsort s -> pp_sort s - | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim(Some (kn,_u),_op,args) -> - hov 1 - (str "(PRIM " ++ pr_con kn ++ spc() ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ - str")") - | Lprim(None,op,args) -> - hov 1 - (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ - str")") - | Lproj(p,arg) -> - hov 1 - (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg - ++ str ")") - | Lint i -> - Pp.(str "(int:" ++ int i ++ str ")") - -(*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 map_lam_with_binders g f n lam = - match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ - | Lfloat _ -> lam - | Levar (evk, args) -> - let args' = Array.Smart.map (f n) args in - if args == args' then lam else Levar (evk, args') - | 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.Smart.map (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.Smart.map (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.Smart.map 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') - | Lif(t,bt,bf) -> - let t' = f n t in - let bt' = f n bt in - let bf' = f n bf in - if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') - | Lfix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.Smart.map (f n) ltypes in - let lbodies' = Array.Smart.map (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.Smart.map (f n) ltypes in - let lbodies' = Array.Smart.map (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.Smart.map (f n) args in - if args == args' then lam else Lmakeblock(tag,args') - | Lprim(kn,op,args) -> - let args' = Array.Smart.map (f n) args in - if args == args' then lam else Lprim(kn,op,args') - | Lproj(p,arg) -> - let arg' = f n arg in - if arg == arg' then lam else Lproj(p,arg') - -(*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.Smart.map (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 _ | Luint _ - | Lval _ | Lsort _ | Lind _ -> true - | _ -> false - - -let can_merge_if bt bf = - match bt, bf with - | Llam(_idst,_), Llam(_idsf,_) -> true - | _ -> false - -let merge_if t bt bf = - let (idst,bodyt) = decompose_Llam bt in - let (idsf,bodyf) = decompose_Llam bf in - let nt = Array.length idst in - let nf = Array.length idsf in - let common,idst,idsf = - if nt = nf then idst, [||], [||] - else - if nt < nf then idst,[||], Array.sub idsf nt (nf - nt) - else idsf, Array.sub idst nf (nt - nf), [||] in - Llam(common, - Lif(lam_lift (Array.length common) t, - mkLlam idst bodyt, - mkLlam idsf bodyf)) - - -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 - - | Lif(t,bt,bf) -> - let t' = simplify subst t in - let bt' = simplify subst bt in - let bf' = simplify subst bf in - if can_merge_if bt' bf' then merge_if t' bt' bf' - else - if t == t' && bt == bt' && bf == bf' then lam - else Lif(t',bt',bf') - | _ -> 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.Smart.map (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 _ | Lint _ | Luint _ - | Lfloat _ -> kind - | Levar (_, args) -> - occurrence_args k kind args - | 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 - | Lif (t, bt, bf) -> - let kind = occurrence k kind t in - kind && occurrence k kind bt && occurrence k kind bf - | 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 - -and occurrence_args k kind args = - Array.fold_left (occurrence k) kind args - -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 + Obj.last_non_constant_constructor_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 _ | Lint _ | Luint _ -> true - | _ -> false - -let get_value lc = - match lc with - | Luint i -> val_of_uint i - | Lval v -> v - | Lint i -> val_of_int i - | _ -> raise Not_found - -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 anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) - let ids = Array.make (nparams + arity) anon in - if arity = 0 then mkLlam ids (Lint 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 Lint tag - else - if Array.for_all is_value args then - if tag < Obj.last_non_constant_constructor_tag then - Lval(val_of_block tag (Array.map get_value args)) - else - let args = Array.map get_value args in - let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in - Lval(val_of_block Obj.last_non_constant_constructor_tag args) - else Lmakeblock(tag, args) - -let makearray args def = - try - let p = Array.map get_value args in - Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def)) - with Not_found -> - let ar = Lmakeblock(0, args) in (* build the ocaml array *) - let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *) - Lmakeblock(0,[|kind|]) (* the reference *) - -(* 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 prim kn p args = - Lprim(Some kn, p, args) - -let expand_prim kn op arity = - (* primitives are always Relevant *) - let ids = Array.make arity Context.anonR in - let args = make_args arity 1 in - Llam(ids, prim kn op args) - -let lambda_of_prim kn op args = - let arity = CPrimitives.arity op in - match Int.compare (Array.length args) arity with - | 0 -> prim kn op args - | x when x > 0 -> - let prim_args = Array.sub args 0 arity in - let extra_args = Array.sub args arity (Array.length args - arity) in - mkLapp(prim kn op prim_args) extra_args - | _ -> mkLapp (expand_prim kn op arity) 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 : 'a t) = - 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 : 'a t) n = - v.size <- max 0 (v.size - n) - - let pop v = popn v 1 - - let get_last (v : 'a t) 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.Context.binder_name - - 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 (evk, args) -> - let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in - Levar (evk, args) - - | 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,_iv,a,branches) -> (* XXX handle iv *) - 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 - (* 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 anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) - let ids = Array.make arity anon 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 rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in - 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 lc = lambda_of_constr env c in - Lproj (Projection.repr p,lc) - - | Int i -> Luint i - | Float f -> Lfloat f - | Array(_u, t,def,_ty) -> - let def = lambda_of_constr env def in - makearray (lambda_of_args env 0 t) def - -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 - let cb = lookup_constant kn env.global_env in - begin match cb.const_body with - | Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args) - | 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 nparams < nargs then (* got all parameters *) - let args = lambda_of_args env nparams args in - makeblock tag 0 arity args - else 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 dump_lambda = ref false - -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_annot (rel_context genv) 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 !dump_lambda then - Feedback.msg_debug (pp_lam lam); - lam diff --git a/kernel/clambda.mli b/kernel/clambda.mli deleted file mode 100644 index bd11c2667f..0000000000 --- a/kernel/clambda.mli +++ /dev/null @@ -1,45 +0,0 @@ -open Names -open Constr -open Vmvalues -open Environ - -type lambda = - | Lrel of Name.t * int - | Lvar of Id.t - | Levar of Evar.t * lambda array - | Lprod of lambda * lambda - | Llam of Name.t Context.binder_annot array * lambda - | Llet of Name.t Context.binder_annot * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) - | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lint of int - | Lmakeblock of int * lambda array - | Luint of Uint63.t - | Lfloat of Float64.t - | Lval of structured_values - | Lsort of Sorts.t - | Lind of pinductive - | Lproj of Projection.Repr.t * lambda - -and lam_branches = - { constant_branches : lambda array; - nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } - -and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array - -exception TooLargeInductive of Pp.t - -val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda - -val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda - -val get_alias : env -> Constant.t -> Constant.t - -(** Dump the VM lambda code after compilation (for debugging purposes) *) -val dump_lambda : bool ref diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml deleted file mode 100644 index 185fb9f5a4..0000000000 --- a/kernel/csymtable.ml +++ /dev/null @@ -1,226 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* atom array -> vm_global -> values array -> values = "coq_eval_tcode" - -type global_data = { mutable glob_len : int; mutable glob_val : values array } - -(*******************) -(* Linkage du code *) -(*******************) - -(* Table des globaux *) - -(* [global_data] contient les valeurs des constantes globales - (axiomes,definitions), les annotations des switch et les structured - constant *) -let global_data = { - glob_len = 0; - glob_val = Array.make 4096 crazy_val; -} - -let get_global_data () = Vmvalues.vm_global global_data.glob_val - -let realloc_global_data n = - let n = min (2 * n + 0x100) Sys.max_array_length in - let ans = Array.make n crazy_val in - let src = global_data.glob_val in - let () = Array.blit src 0 ans 0 (Array.length src) in - global_data.glob_val <- ans - -let check_global_data n = - if n >= Array.length global_data.glob_val then realloc_global_data n - -let set_global v = - let n = global_data.glob_len in - check_global_data n; - global_data.glob_val.(n) <- v; - global_data.glob_len <- global_data.glob_len + 1; - n - -(* Initialization of OCaml primitives *) -let parray_make = set_global Vmvalues.parray_make -let parray_get = set_global Vmvalues.parray_get -let parray_get_default = set_global Vmvalues.parray_get_default -let parray_set = set_global Vmvalues.parray_set -let parray_copy = set_global Vmvalues.parray_copy -let parray_reroot = set_global Vmvalues.parray_reroot -let parray_length = set_global Vmvalues.parray_length - -(* table pour les structured_constant et les annotations des switchs *) - -module SConstTable = Hashtbl.Make (struct - type t = structured_constant - let equal = eq_structured_constant - let hash = hash_structured_constant -end) - -module AnnotTable = Hashtbl.Make (struct - type t = annot_switch - let equal = eq_annot_switch - let hash = hash_annot_switch -end) - -module ProjNameTable = Hashtbl.Make (Projection.Repr) - -let str_cst_tbl : int SConstTable.t = SConstTable.create 31 - -let annot_tbl : int AnnotTable.t = AnnotTable.create 31 - (* (annot_switch * int) Hashtbl.t *) - -let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31 - -(*************************************************************) -(*** Mise a jour des valeurs des variables et des constantes *) -(*************************************************************) - -exception NotEvaluated - -let key rk = - match !rk with - | None -> raise NotEvaluated - | Some k -> - try CEphemeron.get k - with CEphemeron.InvalidKey -> raise NotEvaluated - -(************************) -(* traduction des patch *) - -(* slot_for_*, calcul la valeur de l'objet, la place - dans la table global, rend sa position dans la table *) - -let slot_for_str_cst key = - try SConstTable.find str_cst_tbl key - with Not_found -> - let n = set_global (val_of_str_const key) in - SConstTable.add str_cst_tbl key n; - n - -let slot_for_annot key = - try AnnotTable.find annot_tbl key - with Not_found -> - let n = set_global (val_of_annot_switch key) in - AnnotTable.add annot_tbl key n; - n - -let slot_for_caml_prim = - let open CPrimitives in function - | Arraymake -> parray_make - | Arrayget -> parray_get - | Arraydefault -> parray_get_default - | Arrayset -> parray_set - | Arraycopy -> parray_copy - | Arrayreroot -> parray_reroot - | Arraylength -> parray_length - | _ -> assert false - -let slot_for_proj_name key = - try ProjNameTable.find proj_name_tbl key - with Not_found -> - let n = set_global (val_of_proj_name key) in - ProjNameTable.add proj_name_tbl key n; - n - -let rec slot_for_getglobal env kn = - let (cb,(_,rk)) = lookup_constant_key kn env in - try key rk - with NotEvaluated -> -(* Pp.msgnl(str"not yet evaluated");*) - let pos = - match cb.const_body_code with - | None -> set_global (val_of_constant kn) - | Some code -> - match Cemitcodes.force code with - | BCdefined(code,pl,fv) -> - let v = eval_to_patch env (code,pl,fv) in - set_global v - | BCalias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant kn) - in -(*Pp.msgnl(str"value stored at: "++int pos);*) - rk := Some (CEphemeron.create pos); - pos - -and slot_for_fv env fv = - let fill_fv_cache cache id v_of_id env_of_id b = - let v,d = - match b with - | None -> v_of_id id, Id.Set.empty - | Some c -> - val_of_constr (env_of_id id env) c, - Environ.global_vars_set env c in - build_lazy_val cache (v, d); v in - let val_of_rel i = val_of_rel (nb_rel env - i) in - let idfun _ x = x in - match fv with - | FVnamed id -> - let nv = lookup_named_val id env in - begin match force_lazy_val nv with - | None -> - env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun - | Some (v, _) -> v - end - | FVrel i -> - let rv = lookup_rel_val i env in - begin match force_lazy_val rv with - | None -> - env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel - | Some (v, _) -> v - end - | FVevar evk -> val_of_evar evk - | FVuniv_var _idu -> - assert false - -and eval_to_patch env (buff,pl,fv) = - 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 - | Reloc_proj_name p -> slot_for_proj_name p - | Reloc_caml_prim op -> slot_for_caml_prim op - in - let tc = patch buff pl slots in - let vm_env = - (* Beware, this may look like a call to [Array.map], but it's not. - Calling [Array.map f] when the first argument returned by [f] - is a float would lead to [vm_env] being an unboxed Double_array - (Tag_val = Double_array_tag) whereas eval_tcode expects a - regular array (Tag_val = 0). - See test-suite/primitive/float/coq_env_double_array.v - for an actual instance. *) - let a = Array.make (Array.length fv) crazy_val in - Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in - eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env - -and val_of_constr env c = - match compile ~fail_on_error:true env c with - | Some v -> eval_to_patch env (to_memory v) - | None -> assert false - -let set_transparent_const _kn = () (* !?! *) -let set_opaque_const _kn = () (* !?! *) diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli deleted file mode 100644 index e480bfcec1..0000000000 --- a/kernel/csymtable.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* constr -> Vmvalues.values - -val set_opaque_const : Constant.t -> unit -val set_transparent_const : Constant.t -> unit - -val get_global_data : unit -> Vmvalues.vm_global diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7609c1a64d..9c32cd8e0e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -107,7 +107,7 @@ type 'opaque constant_body = { const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def; const_type : types; const_relevance : Sorts.relevance; - const_body_code : Cemitcodes.to_patch_substituted option; + const_body_code : Vmemitcodes.to_patch_substituted option; const_universes : universes; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 326bf0d6ad..b9f434f179 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -116,7 +116,7 @@ let subst_const_body sub cb = const_body = body'; const_type = type'; const_body_code = - Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; + Option.map (Vmemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; diff --git a/kernel/dune b/kernel/dune index 5f7502ef6b..ce6fdc03df 100644 --- a/kernel/dune +++ b/kernel/dune @@ -11,7 +11,7 @@ (modules genOpcodeFiles)) (rule - (targets copcodes.ml) + (targets vmopcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (rule diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 67a672c349..2d74cca44c 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -11,7 +11,7 @@ (** List of opcodes. It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and - [copcodes.ml] files. + [vmopcodes.ml] files. If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c with the arity of the instruction and maybe coq_tcode_of_code. @@ -196,7 +196,7 @@ let pp_coq_instruct_h fmt = let pp_coq_jumptbl_h fmt = pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") -let pp_copcodes_ml fmt = +let pp_vmopcodes_ml fmt = pp_header true fmt; Array.iteri (fun n s -> Format.fprintf fmt "let op%s = %d@.@." s n @@ -210,7 +210,7 @@ let main () = match Sys.argv.(1) with | "enum" -> pp_coq_instruct_h Format.std_formatter | "jump" -> pp_coq_jumptbl_h Format.std_formatter - | "copml" -> pp_copcodes_ml Format.std_formatter + | "copml" -> pp_vmopcodes_ml Format.std_formatter | _ -> usage () | exception Invalid_argument _ -> usage () diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 41388d9f17..d4d7150222 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -15,9 +15,9 @@ Term CPrimitives Mod_subst Vmvalues -Cbytecodes -Copcodes -Cemitcodes +Vmbytecodes +Vmopcodes +Vmemitcodes Opaqueproof Declarations Entries @@ -30,12 +30,12 @@ Primred CClosure Relevanceops Reduction -Clambda +Vmlambda Nativelambda -Cbytegen +Vmbytegen Nativecode Nativelib -Csymtable +Vmsymtable Vm Vconv Nativeconv diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 44b010204b..5873d1f502 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -124,8 +124,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = { cb with const_body = def; const_universes = univs ; - const_body_code = Option.map Cemitcodes.from_val - (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } + const_body_code = Option.map Vmemitcodes.from_val + (Vmbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index 77ef38dfd5..883ad79be5 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -328,7 +328,7 @@ let strengthen_const mp_from l cb resolver = let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } + const_body_code = Some (Vmemitcodes.from_val (Vmbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index b00b96018f..99090f0147 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -395,8 +395,8 @@ let rec get_alias env (kn, u as p) = match tps with | None -> p | Some tps -> - match Cemitcodes.force tps with - | Cemitcodes.BCalias kn' -> get_alias env (kn', u) + match Vmemitcodes.force tps with + | Vmemitcodes.BCalias kn' -> get_alias env (kn', u) | _ -> p let prim env kn p args = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 48567aa564..24aa4ed771 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -283,8 +283,8 @@ let build_constant_declaration env result = let univs = result.cook_universes in let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in let tps = - let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in - Option.map Cemitcodes.from_val res + let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Vmemitcodes.from_val res in { const_hyps = hyps; const_body = def; @@ -343,8 +343,8 @@ let translate_recipe env _kn r = let open Cooking in let result = Cooking.cook_constant r in let univs = result.cook_universes in - let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in - let tps = Option.map Cemitcodes.from_val res in + let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in + let tps = Option.map Vmemitcodes.from_val res in let hyps = Option.get result.cook_context in (* Trust the set of section hypotheses generated by Cooking *) let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f78f0d4d1e..cc2c2c0b4b 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -4,7 +4,7 @@ open Environ open Reduction open Vm open Vmvalues -open Csymtable +open Vmsymtable (* Test la structure des piles *) diff --git a/kernel/vm.ml b/kernel/vm.ml index d8c66bebd2..76954a83d8 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -44,7 +44,7 @@ external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env - "coq_interprete_byte" "coq_interprete_ml" let interprete code v env k = - coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k + coq_interprete code v (get_atom_rel ()) (Vmsymtable.get_global_data ()) env k (* Functions over arguments *) diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml new file mode 100644 index 0000000000..74405a0105 --- /dev/null +++ b/kernel/vmbytecodes.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* str "FVnamed(" ++ Id.print id ++ str ")" + | FVrel i -> str "Rel(" ++ int i ++ str ")" + | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" + | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")" + +let rec pp_instr i = + match i with + | Klabel _ | Ksequence _ -> assert false + | Kacc n -> str "acc " ++ int n + | Kenvacc n -> str "envacc " ++ int n + | Koffsetclosure n -> str "offsetclosure " ++ int n + | Kpush -> str "push" + | Kpop n -> str "pop " ++ int n + | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl + | Kapply n -> str "apply " ++ int n + | Kappterm(n, m) -> + str "appterm " ++ int n ++ str ", " ++ int m + | Kreturn n -> str "return " ++ int n + | Kjump -> str "jump" + | Krestart -> str "restart" + | Kgrab n -> str "grab " ++ int n + | Kgrabrec n -> str "grabrec " ++ int n + | Kclosure(lbl, n) -> + str "closure " ++ pp_lbl lbl ++ str ", " ++ int n + | Kclosurerec(fv,init,lblt,lblb) -> + h 1 (str "closurerec " ++ + int fv ++ str ", " ++ int init ++ + str " types = " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ + str " bodies = " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblb)) + | Kclosurecofix (fv,init,lblt,lblb) -> + h 1 (str "closurecofix " ++ + int fv ++ str ", " ++ int init ++ + str " types = " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ + str " bodies = " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblb)) + | Kgetglobal idu -> str "getglobal " ++ Constant.print idu + | Kconst sc -> + str "const " ++ pp_struct_const sc + | Kmakeblock(n, m) -> + str "makeblock " ++ int n ++ str ", " ++ int m + | Kmakeprod -> str "makeprod" + | Kmakeswitchblock(lblt,lbls,_,sz) -> + str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++ + pp_lbl lbls ++ str ", " ++ int sz + | Kswitch(lblc,lblb) -> + h 1 (str "switch " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblc) ++ + str " | " ++ + prlist_with_sep spc pp_lbl (Array.to_list lblb)) + | Kpushfields n -> str "pushfields " ++ int n + | Kfield n -> str "field " ++ int n + | Ksetfield n -> str "setfield " ++ int n + + | Kstop -> str "stop" + + | Kbranch lbl -> str "branch " ++ pp_lbl lbl + + | Kproj p -> str "proj " ++ Projection.Repr.print p + + | Kensurestackcapacity size -> str "growstack " ++ int size + + | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ + (match id with Some (id,_u) -> Constant.print id | None -> str "") + + | Kcamlprim (op, lbl) -> + str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ + pp_lbl lbl + + | Kareint n -> str "areint " ++ int n + +and pp_bytecodes c = + match c with + | [] -> str "" + | Klabel lbl :: c -> + str "L" ++ int lbl ++ str ":" ++ fnl () ++ + pp_bytecodes c + | Ksequence (l1, l2) :: c -> + pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c + | i :: c -> + pp_instr i ++ fnl () ++ pp_bytecodes c diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli new file mode 100644 index 0000000000..b703058fb7 --- /dev/null +++ b/kernel/vmbytecodes.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* t + val reset_label_counter : unit -> unit + end + +type instruction = + | Klabel of Label.t + | Kacc of int (** accu = sp[n] *) + | Kenvacc of int (** accu = coq_env[n] *) + | Koffsetclosure of int (** accu = &coq_env[n] *) + | Kpush (** sp = accu :: sp *) + | Kpop of int (** sp = skipn n sp *) + | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) + | Kapply of int (** number of arguments (arguments on top of stack) *) + | Kappterm of int * int (** number of arguments, slot size *) + | Kreturn of int (** slot size *) + | Kjump + | Krestart + | Kgrab of int (** number of arguments *) + | Kgrabrec of int (** rec arg *) + | Kclosure of Label.t * int (** label, number of free variables *) + | Kclosurerec of int * int * Label.t array * Label.t array + (** nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix of int * int * Label.t array * Label.t array + (** nb fv, init, lbl types, lbl bodies *) + | Kgetglobal of Constant.t + | Kconst of structured_constant + | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 + ** is accu, all others are popped from + ** the top of the stack *) + | Kmakeprod + | Kmakeswitchblock of Label.t * Label.t * annot_switch * int + | Kswitch of Label.t array * Label.t array (** consts,blocks *) + | Kpushfields of int + | Kfield of int (** accu = accu[n] *) + | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) + | Kstop + | Ksequence of bytecodes * bytecodes + | Kproj of Projection.Repr.t + | Kensurestackcapacity of int + + | Kbranch of Label.t (** jump to label, is it needed ? *) + | Kprim of CPrimitives.t * pconstant option + | Kcamlprim of CPrimitives.t * Label.t + | Kareint of int + +and bytecodes = instruction list + +val pp_bytecodes : bytecodes -> Pp.t + +type fv_elem = + FVnamed of Id.t +| FVrel of int +| FVuniv_var of int +| FVevar of Evar.t + +type fv = fv_elem array + +val pp_fv_elem : fv_elem -> Pp.t diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml new file mode 100644 index 0000000000..1274e3a867 --- /dev/null +++ b/kernel/vmbytegen.ml @@ -0,0 +1,934 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* *) +(* type = [Ct1 | .... | Ctn] *) +(* Ci is the code pointer of the i-th body *) +(* At runtime, a fixpoint environment (which is the same as the fixpoint *) +(* itself) is a pointer to the field holding its code pointer. *) +(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint *) +(* and de Bruijn [1] the last one. *) +(* Access to these variables is performed by the [Koffsetclosure n] *) +(* instruction that shifts the environment pointer of [n] fields. *) + +(* This allows representing mutual fixpoints in just one block. *) +(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *) +(* types. They are used in conversion tests (which requires that *) +(* fixpoint types must be convertible). Their environment is the one of *) +(* the last fixpoint : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^ *) + +(* Representation of mutual cofix : *) +(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) +(* ... *) +(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) +(* *) +(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* ... *) +(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* The [ai] blocks are functions that accumulate their arguments: *) +(* ai arg1 argp ---> *) +(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) +(* If such a block is matched against, we have to force evaluation, *) +(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) +(* Once evaluation is completed [ai'] is updated with the result: *) +(* ai' <-- *) +(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) +(* This representation is nice because the application of the cofix is *) +(* evaluated only once (it simulates a lazy evaluation) *) +(* Moreover, when cofix don't have arguments, it is possible to create *) +(* a cycle, e.g.: *) +(* cofix one := cons 1 one *) +(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) +(* fcofix1 = [clos_t | code | a1] *) +(* The result of evaluating [a1] is [cons_t | 1 | a1]. *) +(* When [a1] is updated : *) +(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) +(* The cycle is created ... *) +(* *) +(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) +(* conversion of cofixpoints (which is intentional). *) + +module Fv_elem = +struct +type t = fv_elem + +let compare e1 e2 = match e1, e2 with +| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 +| FVrel _, FVnamed _ -> 1 +| FVrel r1, FVrel r2 -> Int.compare r1 r2 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 +| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 +| FVuniv_var _, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 + +end + +module FvMap = Map.Make(Fv_elem) + +(*spiwack: both type have been moved from Vmbytegen because I needed then + for the retroknowledge *) +type vm_env = { + size : int; (* longueur de la liste [n] *) + fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (* reverse mapping *) + } + + +type comp_env = { + arity : int; (* arity of the current function, 0 if none *) + nb_uni_stack : int ; (* number of universes on the stack, *) + (* universes are always at the bottom. *) + nb_stack : int; (* number of variables on the stack *) + in_stack : int Range.t; (* position in the stack *) + nb_rec : int; (* number of mutually recursive functions *) + pos_rec : instruction list; (* instruction d'acces pour les variables *) + (* de point fix ou de cofix *) + offset : int; + in_env : vm_env ref (* The free variables of the expression *) + } + +module Config = struct + let stack_threshold = 256 (* see byterun/coq_memory.h *) + let stack_safety_margin = 15 +end + +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 = { + size = e.size + 1; + fv_rev = d :: e.fv_rev; + fv_fwd = FvMap.add d e.size e.fv_fwd; +} + +let fv r = !(r.in_env) + +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 0; + in_env = ref empty_fv + } + +(* Maximal stack size reached during the current function body. Used to + reallocate the stack if we lack space. *) +let max_stack_size = ref 0 + +let set_max_stack_size stack_size = + if stack_size > !max_stack_size then + max_stack_size := stack_size + +let ensure_stack_capacity f x = + let old = !max_stack_size in + max_stack_size := 0; + let code = f x in + let used_safe = + !max_stack_size + Config.stack_safety_margin + in + max_stack_size := old; + if used_safe > Config.stack_threshold then + Kensurestackcapacity used_safe :: code + else code + +(*i Creation functions for comp_env *) + +let rec add_param n sz l = + if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l) + +let comp_env_fun ?(univs=0) arity = + { arity; + nb_uni_stack = univs ; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = ref empty_fv + } + + +let comp_env_fix_type rfv = + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = rfv + } + +let comp_env_fix ndef curr_pos arity rfv = + let prec = ref [] in + for i = ndef downto 1 do + prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec + done; + { arity; + nb_uni_stack = 0; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = ndef; + pos_rec = !prec; + offset = 2 * (ndef - curr_pos - 1)+1; + in_env = rfv + } + +let comp_env_cofix_type ndef rfv = + { arity = 0; + nb_uni_stack = 0; + nb_stack = 0; + in_stack = Range.empty; + nb_rec = 0; + pos_rec = []; + offset = 1+ndef; + in_env = rfv + } + +let comp_env_cofix ndef arity rfv = + let prec = ref [] in + for i = 1 to ndef do + prec := Kenvacc i :: !prec + done; + { arity; + nb_uni_stack = 0; + nb_stack = arity; + in_stack = add_param arity 0 Range.empty; + nb_rec = ndef; + pos_rec = !prec; + offset = ndef+1; + in_env = rfv + } + +(* [push_param ] add function parameters on the stack *) +let push_param n sz r = + { r with + nb_stack = r.nb_stack + n; + in_stack = add_param n sz r.in_stack } + +(* [push_local sz r] add a new variable on the stack at position [sz] *) +let push_local sz r = + { r with + nb_stack = r.nb_stack + 1; + in_stack = Range.cons (sz + 1) r.in_stack } + +(*i Compilation of variables *) +let find_at fv env = FvMap.find fv env.fv_fwd + +let pos_named id r = + let env = !(r.in_env) in + let cid = FVnamed id in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + +let pos_rel i r sz = + if i <= r.nb_stack then + Kacc(sz - (Range.get r.in_stack (i-1))) + else + let i = i - r.nb_stack in + if i <= r.nb_rec then + try List.nth r.pos_rec (i-1) + with (Failure _|Invalid_argument _) -> assert false + else + let i = i - r.nb_rec in + let db = FVrel(i) in + let env = !(r.in_env) in + try Kenvacc(r.offset + find_at db env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv db env; + Kenvacc(r.offset + pos) + +let pos_universe_var i r sz = + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) + else + let env = !(r.in_env) in + let db = FVuniv_var i in + try Kenvacc (r.offset + find_at db env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv db env; + Kenvacc(r.offset + pos) + +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + 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. *) +(* This function is to be applied to the continuation before adding a *) +(* non-terminating instruction (branch, raise, return, appterm) *) +(* in front of it. *) + +let discard_dead_code cont = cont +(*function + [] -> [] + | (Klabel _ | Krestart ) :: _ as cont -> cont + | _ :: cont -> discard_dead_code cont +*) + +(* Return a label to the beginning of the given continuation. *) +(* If the sequence starts with a branch, use the target of that branch *) +(* as the label, thus avoiding a jump to a jump. *) + +let label_code = function + | Klabel lbl :: _ as cont -> (lbl, cont) + | Kbranch lbl :: _ as cont -> (lbl, cont) + | cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont) + +(* Return a branch to the continuation. That is, an instruction that, + when executed, branches to the continuation or performs what the + continuation performs. We avoid generating branches to returns. *) +(* spiwack: make_branch was only used once. Changed it back to the ZAM + one to match the appropriate semantics (old one avoided the + introduction of an unconditional branch operation, which seemed + appropriate for the 31-bit integers' code). As a memory, I leave + the former version in this comment. +let make_branch cont = + match cont with + | (Kreturn _ as return) :: cont' -> return, cont' + | Klabel lbl as b :: _ -> b, cont + | _ -> let b = Klabel(Label.create()) in b,b::cont +*) + +let rec make_branch_2 lbl n cont = + function + Kreturn m :: _ -> (Kreturn (n + m), cont) + | Klabel _ :: c -> make_branch_2 lbl n cont c + | Kpop m :: c -> make_branch_2 lbl (n + m) cont c + | _ -> + match lbl with + Some lbl -> (Kbranch lbl, cont) + | None -> let lbl = Label.create() in (Kbranch lbl, Klabel lbl :: cont) + +let make_branch cont = + match cont with + (Kbranch _ as branch) :: _ -> (branch, cont) + | (Kreturn _ as return) :: _ -> (return, cont) + | Klabel lbl :: _ -> make_branch_2 (Some lbl) 0 cont cont + | _ -> make_branch_2 (None) 0 cont cont + +(* Check if we're in tailcall position *) + +let rec is_tailcall = function + | Kreturn k :: _ -> Some k + | Klabel _ :: c -> is_tailcall c + | _ -> None + +(* Extension of the continuation *) + +(* Add a Kpop n instruction in front of a continuation *) +let rec add_pop n = function + | Kpop m :: cont -> add_pop (n+m) cont + | Kreturn m:: cont -> Kreturn (n+m) ::cont + | cont -> if Int.equal n 0 then cont else Kpop n :: cont + +let add_grab arity lbl cont = + if Int.equal arity 1 then Klabel lbl :: cont + else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont + +let add_grabrec rec_arg arity lbl cont = + if Int.equal arity 1 && rec_arg < arity then + Klabel lbl :: Kgrabrec 0 :: Krestart :: cont + else + Krestart :: Klabel lbl :: Kgrabrec rec_arg :: + Krestart :: Kgrab (arity - 1) :: cont + +(* continuation of a cofix *) + +let cont_cofix arity = + (* accu = res *) + (* stk = ai::args::ra::... *) + (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *) + [ Kpush; + Kpush; (* stk = res::res::ai::args::ra::... *) + Kacc 2; + Kfield 1; + Kfield 0; + Kmakeblock(2, cofix_evaluated_tag); + Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*) + Kacc 2; + Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *) + (* stk = res::ai::args::ra::... *) + Kacc 0; (* accu = res *) + Kreturn (arity+2) ] + + +(* Code of closures *) +let fun_code = ref [] + +let init_fun_code () = fun_code := [] + +(* Compilation of constructors and inductive types *) + + +(* +If [tag] hits the OCaml limitation for non constant constructors, we switch to +another representation for the remaining constructors: +[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args] + +We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation. + *) + +let nest_block tag arity cont = + Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) :: + Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont + +let code_makeblock ~stack_size ~arity ~tag cont = + if tag < Obj.last_non_constant_constructor_tag then + Kmakeblock(arity, tag) :: cont + else begin + set_max_stack_size (stack_size + 1); + Kpush :: nest_block tag arity cont + end + +let compile_structured_constant _cenv sc sz cont = + set_max_stack_size sz; + Kconst sc :: cont + +(* compiling application *) +let comp_args comp_expr cenv args sz cont = + let nargs_m_1 = Array.length args - 1 in + let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in + for i = 1 to nargs_m_1 do + c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c) + done; + !c + +let comp_app comp_fun comp_arg cenv f args sz cont = + let nargs = Array.length args in + if Int.equal nargs 0 then comp_fun cenv f sz cont + else + match is_tailcall cont with + | Some k -> + comp_args comp_arg cenv args sz + (Kpush :: + comp_fun cenv f (sz + nargs) + (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) + | None -> + if nargs <= 4 then + comp_args comp_arg cenv args sz + (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) + else + let lbl,cont1 = label_code cont in + Kpush_retaddr lbl :: + (comp_args comp_arg cenv args (sz + 3) + (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1)))) + +(* Compiling free variables *) + +let compile_fv_elem cenv fv sz cont = + match fv with + | FVrel i -> pos_rel i cenv sz :: cont + | FVnamed id -> pos_named id cenv :: cont + | FVuniv_var i -> pos_universe_var i cenv sz :: cont + | FVevar evk -> pos_evar evk cenv :: cont + +let rec compile_fv cenv l sz cont = + match l with + | [] -> cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont + | fvn :: tl -> + compile_fv_elem cenv fvn sz + (Kpush :: compile_fv cenv tl (sz + 1) cont) + + +(* 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 Vmemitcodes.force tps with + | BCalias kn' -> get_alias env kn' + | _ -> kn) + +(* Some primitives are not implemented natively by the VM, but calling OCaml + code instead *) +let is_caml_prim = let open CPrimitives in function + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> true + | _ -> false + +(* sz is the size of the local stack *) +let rec compile_lam env cenv lam sz cont = + set_max_stack_size sz; + match lam with + | Lrel(_, i) -> pos_rel i cenv sz :: cont + + | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont + + | Lval v -> compile_structured_constant cenv (Const_val v) sz cont + + | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont + + | Lfloat f -> compile_structured_constant cenv (Const_float f) sz cont + + | Lproj (p,arg) -> + compile_lam env cenv arg sz (Kproj p :: cont) + + | Lvar id -> pos_named id cenv :: cont + + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem cenv (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) cenv (FVevar evk) args sz cont + + | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont + + | Lind (ind,u) -> + if Univ.Instance.is_empty u then + compile_structured_constant cenv (Const_ind ind) sz cont + else comp_app compile_structured_constant compile_universe cenv + (Const_ind ind) (Univ.Instance.to_array u) sz cont + + | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) -> + compile_structured_constant cenv (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 cenv idx sz cont = + set_max_stack_size sz; + compile_fv_elem cenv (FVuniv_var idx) sz cont + in + if List.is_empty s then + compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont + else + comp_app compile_structured_constant compile_get_univ cenv + (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont + + | Llet (_id,def,body) -> + compile_lam env cenv def sz + (Kpush :: + compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) + + | Lprod (dom,codom) -> + let cont1 = + Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in + compile_lam env cenv 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 cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) + + | Lapp (f, args) -> + begin match f with + | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont + | _ -> comp_app (compile_lam env) (compile_lam env) cenv 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 + (* Compiling types *) + let env_type = comp_env_fix_type rfv in + for i = 0 to ndef - 1 do + let fcode = + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] + in + 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_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_lam env env_body body arity) [Kreturn arity] + in + let lbl = Label.create () in + lbl_bodies.(i) <- lbl; + let fcode = add_grabrec rec_args.(i) arity lbl cont1 in + fun_code := [Ksequence(fcode,!fun_code)] + done; + let fv = !rfv in + compile_fv cenv fv.fv_rev sz + (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) + + + | 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 *) + let rfv = ref empty_fv in + let env_type = comp_env_cofix_type ndef rfv in + for i = 0 to ndef - 1 do + let fcode = + ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop] + in + 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_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_lam env env_body body (arity+1) (cont_cofix arity) + in + let cont = ensure_stack_capacity comp arity in + lbl_bodies.(i) <- lbl; + fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; + done; + let fv = !rfv in + set_max_stack_size (sz + fv.size + ndef + 2); + compile_fv cenv fv.fv_rev sz + (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) + + | Lif(t, bt, bf) -> + let branch, cont = make_branch cont in + let lbl_true = Label.create() in + let lbl_false = Label.create() in + compile_lam env cenv t sz + (Kswitch([|lbl_true;lbl_false|],[||]) :: + Klabel lbl_false :: + compile_lam env cenv bf sz + (branch :: + Klabel lbl_true :: + compile_lam env cenv bt sz cont)) + + | Lcase(ci,rtbl,t,a,branches) -> + let ind = ci.ci_ind in + let mib = lookup_mind (fst ind) env in + let oib = mib.mind_packets.(snd ind) 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 (Obj.last_non_constant_constructor_tag + 1) in + let lbl_blocks = Array.make nblock Label.no in + let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in + let lbl_eblocks = Array.make neblock Label.no in + let branch1, cont = make_branch cont in + (* Compilation of the return type *) + let fcode = + ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] + in + let lbl_typ,fcode = label_code fcode in + fun_code := [Ksequence(fcode,!fun_code)]; + (* 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 + | Kbranch _ -> sz+3, Kjump, false + | _ -> assert false + in + + let c = ref cont in + (* Perform the extra match if needed (too many block constructors) *) + if neblock <> 0 then begin + let lbl_b, code_b = + label_code ( + Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b; + c := code_b + end; + + (* Compilation of constant branches *) + for i = nconst - 1 downto 0 do + let aux = + compile_lam env cenv 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 cenv) + body (sz_b+arity) (add_pop arity (branch::!c)) in + let code_b = + if tag < Obj.last_non_constant_constructor_tag then begin + set_max_stack_size (sz_b + arity); + Kpushfields arity :: code_b + end + else begin + 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 < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b; + c := code_b + done; + + let annot = + {rtbl = rtbl; tailcall = is_tailcall; + max_stack_size = !max_stack_size - sz} + in + + (* Compiling branch for accumulators *) + let lbl_accu, code_accu = + set_max_stack_size (sz+3); + label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) + in + lbl_blocks.(0) <- lbl_accu; + + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; + let code_sw = + match branch1 with + (* spiwack : branch1 can't be a lbl anymore it's a Branch instead + | Klabel lbl -> Kpush_retaddr lbl :: !c *) + | Kbranch lbl -> Kpush_retaddr lbl :: !c + | _ -> !c + in + compile_lam env cenv 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) cenv args sz cont + + | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + let arity = CPrimitives.arity op in + let nparams = CPrimitives.nparams op in + let nargs = arity - nparams in + assert (arity = Array.length args && arity <= 4); + let (jump, cont) = make_branch cont in + let lbl_default = Label.create () in + let default = + let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = + if Univ.Instance.is_empty u then cont + else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) + in + Klabel lbl_default :: + Kpush :: + if Int.equal nparams 0 then cont + else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) + in + fun_code := [Ksequence(default, !fun_code)]; + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + + | Lprim (kn, op, args) -> + comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) + +and compile_get_global cenv (kn,u) sz cont = + set_max_stack_size sz; + if Univ.Instance.is_empty u then + Kgetglobal kn :: cont + else + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_universe cenv () (Univ.Instance.to_array u) sz cont + +and compile_universe cenv uni sz cont = + set_max_stack_size sz; + match Univ.Level.var_index uni with + | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont + | Some idx -> pos_universe_var idx cenv sz :: cont + +and compile_constant env cenv 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 cenv (kn,u) sz cont) + (compile_lam env) cenv () args sz cont + else + let compile_arg cenv constr_or_uni sz cont = + match constr_or_uni with + | ArgLambda t -> compile_lam env cenv t sz cont + | ArgUniv uni -> compile_universe cenv 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 cenv () all sz cont + +let is_univ_copy max u = + let u = Univ.Instance.to_array u in + if Array.length u = max then + Array.fold_left_i (fun i acc u -> + if acc then + match Univ.Level.var_index u with + | None -> false + | Some l -> l = i + else false) true u + else + false + +let dump_bytecode = ref false + +let dump_bytecodes init code fvs = + let open Pp in + (str "code =" ++ fnl () ++ + pp_bytecodes init ++ fnl () ++ + pp_bytecodes code ++ fnl () ++ + str "fv = " ++ + prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ + fnl ()) + +let compile ~fail_on_error ?universes:(universes=0) env c = + init_fun_code (); + Label.reset_label_counter (); + let cont = [Kstop] in + try + let cenv, init_code = + if Int.equal universes 0 then + let lam = lambda_of_constr ~optimize:true env c in + let cenv = empty_comp_env () in + cenv, ensure_stack_capacity (compile_lam env cenv 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 cenv = empty_comp_env () 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_lam env r_fun body full_arity) + [Kreturn full_arity] + in + fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + let init_code = + ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) + (Kclosure(lbl_fun,fv.size) :: cont) + in + cenv, init_code + in + let fv = List.rev (!(cenv.in_env).fv_rev) in + (if !dump_bytecode then + Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; + Some (init_code,!fun_code, Array.of_list fv) + with TooLargeInductive msg as exn -> + let _, info = Exninfo.capture exn in + let fn = if fail_on_error then + CErrors.user_err ?loc:None ~info ~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 _ | Primitive _ -> Some BCconstant + | Def sb -> + let body = Mod_subst.force_constr sb in + let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in + 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.make1 (Constant.canonical kn') in + Some (BCalias (get_alias env con)) + | _ -> + 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)) diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli new file mode 100644 index 0000000000..aef7ac3d6b --- /dev/null +++ b/kernel/vmbytegen.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option +(** init, fun, fv *) + +val compile_constant_body : fail_on_error:bool -> + env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def -> + body_code option + +(** Shortcut of the previous function used during module strengthening *) + +val compile_alias : Names.Constant.t -> body_code + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml new file mode 100644 index 0000000000..2dfc9a2941 --- /dev/null +++ b/kernel/vmemitcodes.ml @@ -0,0 +1,497 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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 + | Reloc_proj_name of Projection.Repr.t + | Reloc_caml_prim of CPrimitives.t + +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 +| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 +| Reloc_proj_name _, _ -> false +| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 +| Reloc_caml_prim _, _ -> 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) + | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) + | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) + +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; + Bytes.unsafe_set buff (pos + 1) c2; + Bytes.unsafe_set buff (pos + 2) c3; + Bytes.unsafe_set buff (pos + 3) c4 + +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)) + +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 iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in + let () = CArray.iter iter reloc in + 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 + +(* Buffering of bytecode *) + +type label_definition = + Label_defined of int + | Label_undefined of (int * int) list + +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 + else + if len = Sys.max_string_length + 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 env.out_buffer 0 new_buffer 0 len; + env.out_buffer <- new_buffer + end; + patch_char4 env.out_buffer p (Char.unsafe_chr b1) + (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); + env.out_position <- p + 4 + +let out env opcode = + out_word env opcode 0 0 0 + +let is_immed i = Uint63.le (Uint63.of_int i) Uint63.maxuint31 + +let out_int env n = + out_word env n (n asr 8) (n asr 16) (n asr 24) + +(* Handling of local labels and backpatching *) + +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 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 (fun p -> backpatch env p) patchlist; + (env.label_table).(lbl) <- Label_defined env.out_position + +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 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 *) + (env.label_table).(lbl) <- + Label_undefined((env.out_position, orig) :: patchlist); + out_int env 0 + +let out_label env l = out_label_with_orig env env.out_position l + +(* Relocation information *) + +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 slot_for_const env c = + enter env (Reloc_const c); + out_int env 0 + +let slot_for_annot env a = + enter env (Reloc_annot a); + out_int env 0 + +let slot_for_getglobal env p = + enter env (Reloc_getglobal p); + out_int env 0 + +let slot_for_proj_name env p = + enter env (Reloc_proj_name p); + out_int env 0 + +let slot_for_caml_prim env op = + enter env (Reloc_caml_prim op); + out_int env 0 + +(* Emission of one instruction *) + +let nocheck_prim_op = function + | Int63add -> opADDINT63 + | Int63sub -> opSUBINT63 + | Int63lt -> opLTINT63 + | Int63le -> opLEINT63 + | _ -> assert false + + +let check_prim_op = function + | Int63head0 -> opCHECKHEAD0INT63 + | Int63tail0 -> opCHECKTAIL0INT63 + | Int63add -> opCHECKADDINT63 + | Int63sub -> opCHECKSUBINT63 + | Int63mul -> opCHECKMULINT63 + | Int63div -> opCHECKDIVINT63 + | Int63mod -> opCHECKMODINT63 + | Int63lsr -> opCHECKLSRINT63 + | Int63lsl -> opCHECKLSLINT63 + | Int63land -> opCHECKLANDINT63 + | Int63lor -> opCHECKLORINT63 + | Int63lxor -> opCHECKLXORINT63 + | Int63addc -> opCHECKADDCINT63 + | Int63subc -> opCHECKSUBCINT63 + | Int63addCarryC -> opCHECKADDCARRYCINT63 + | Int63subCarryC -> opCHECKSUBCARRYCINT63 + | Int63mulc -> opCHECKMULCINT63 + | Int63diveucl -> opCHECKDIVEUCLINT63 + | Int63div21 -> opCHECKDIV21INT63 + | Int63addMulDiv -> opCHECKADDMULDIVINT63 + | Int63eq -> opCHECKEQINT63 + | Int63lt -> opCHECKLTINT63 + | Int63le -> opCHECKLEINT63 + | Int63compare -> opCHECKCOMPAREINT63 + | Float64opp -> opCHECKOPPFLOAT + | Float64abs -> opCHECKABSFLOAT + | Float64eq -> opCHECKEQFLOAT + | Float64lt -> opCHECKLTFLOAT + | Float64le -> opCHECKLEFLOAT + | Float64compare -> opCHECKCOMPAREFLOAT + | Float64classify -> opCHECKCLASSIFYFLOAT + | Float64add -> opCHECKADDFLOAT + | Float64sub -> opCHECKSUBFLOAT + | Float64mul -> opCHECKMULFLOAT + | Float64div -> opCHECKDIVFLOAT + | Float64sqrt -> opCHECKSQRTFLOAT + | Float64ofInt63 -> opCHECKFLOATOFINT63 + | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA + | Float64frshiftexp -> opCHECKFRSHIFTEXP + | Float64ldshiftexp -> opCHECKLDSHIFTEXP + | Float64next_up -> opCHECKNEXTUPFLOAT + | Float64next_down -> opCHECKNEXTDOWNFLOAT + | Arraymake -> opISINT_CAML_CALL2 + | Arrayget -> opISARRAY_INT_CAML_CALL2 + | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> + opISARRAY_CAML_CALL1 + +let emit_instr env = function + | Klabel lbl -> define_label env lbl + | Kacc 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 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 env (opOFFSETCLOSURE0 + ofs / 2) + else (out env opOFFSETCLOSURE; out_int env ofs) + | Kpush -> + out env opPUSH + | Kpop n -> + out env opPOP; out_int env n + | Kpush_retaddr lbl -> + out env opPUSH_RETADDR; out_label env lbl + | Kapply 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 env(opAPPTERM1 + n - 1); out_int env sz) + else (out env opAPPTERM; out_int env n; out_int env sz) + | Kreturn n -> + out env opRETURN; out_int env n + | Kjump -> + out env opRETURN; out_int env 0 + | Krestart -> + out env opRESTART + | Kgrab n -> + out env opGRAB; out_int env n + | Kgrabrec(rec_arg) -> + out env opGRABREC; out_int env rec_arg + | Kclosure(lbl, n) -> + out env opCLOSURE; out_int env n; out_label env lbl + | Kclosurerec(nfv,init,lbl_types,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 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 env opGETGLOBAL; slot_for_getglobal env q + | Kconst (Const_b0 i) when is_immed i -> + if i >= 0 && i <= 3 + then out env (opCONST0 + i) + else (out env opCONSTINT; out_int env i) + | Kconst 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 env(opMAKEBLOCK1 + n - 1); out_int env t) + else (out env opMAKEBLOCK; out_int env n; out_int env t) + | Kmakeprod -> + out env opMAKEPROD + | Kmakeswitchblock(typlbl,swlbl,annot,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 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 env opPUSHFIELDS;out_int env n + | Kfield n -> + if n <= 1 then out env (opGETFIELD0+n) + else (out env opGETFIELD;out_int env n) + | Ksetfield n -> + if n <= 1 then out env (opSETFIELD0+n) + else (out env opSETFIELD;out_int env n) + | Ksequence _ -> invalid_arg "Vmemitcodes.emit_instr" + | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p + | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size + | Kbranch lbl -> out env opBRANCH; out_label env lbl + | Kprim (op,None) -> + out env (nocheck_prim_op op) + + | Kprim(op,Some (q,_u)) -> + out env (check_prim_op op); + slot_for_getglobal env q + + | Kcamlprim (op,lbl) -> + out env (check_prim_op op); + out_label env lbl; + slot_for_caml_prim env op + + | Kareint 1 -> out env opISINT + | Kareint 2 -> out env opAREINT2; + + | Kstop -> out env opSTOP + + | Kareint _ -> assert false + +(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) + +let rec emit env insns remaining = match insns with + | [] -> + (match remaining with + [] -> () + | (first::rest) -> emit env first rest) + (* Peephole optimizations *) + | Kpush :: Kacc n :: c -> + 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 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 env(opPUSHOFFSETCLOSURE0 + ofs / 2) + else (out env opPUSHOFFSETCLOSURE; out_int env ofs); + emit env c remaining + | Kpush :: Kgetglobal id :: c -> + out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining + | Kpush :: Kconst (Const_b0 i) :: c when is_immed i -> + if i >= 0 && i <= 3 + then out env (opPUSHCONST0 + i) + else (out env opPUSHCONSTINT; out_int env i); + emit env c remaining + | Kpush :: Kconst const :: c -> + out env opPUSHGETGLOBAL; slot_for_const env const; + emit env c remaining + | Kpop n :: Kjump :: c -> + out env opRETURN; out_int env n; emit env c remaining + | Ksequence(c1,c2)::c -> + emit env c1 (c2::c::remaining) + (* Default case *) + | instr :: c -> + emit_instr env instr; emit env c remaining + +(* Initialization *) + +type to_patch = emitcodes * patches * fv + +(* Substitution *) +let subst_strcst s sc = + match sc with + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ + | Const_float _ -> sc + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) + +let subst_annot _ (a : annot_switch) = a + +let subst_reloc s ri = + match ri with + | Reloc_annot a -> Reloc_annot (subst_annot s a) + | Reloc_const sc -> Reloc_const (subst_strcst s sc) + | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) + | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) + | Reloc_caml_prim _ -> ri + +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, subst_patches s pl, fv + +type body_code = + | BCdefined of to_patch + | BCalias of Names.Constant.t + | BCconstant + +type to_patch_substituted = +| PBCdefined of to_patch substituted +| PBCalias of Names.Constant.t substituted +| PBCconstant + +let from_val = function +| BCdefined tp -> PBCdefined (from_val tp) +| BCalias cu -> PBCalias (from_val cu) +| BCconstant -> PBCconstant + +let force = function +| PBCdefined tp -> BCdefined (force subst_to_patch tp) +| PBCalias cu -> BCalias (force subst_constant cu) +| PBCconstant -> BCconstant + +let subst_to_patch_subst s = function +| PBCdefined tp -> PBCdefined (subst_substituted s tp) +| PBCalias cu -> PBCalias (subst_substituted s cu) +| PBCconstant -> PBCconstant + +let repr_body_code = function +| PBCdefined tp -> + let (s, tp) = repr_substituted tp in + (s, BCdefined tp) +| PBCalias cu -> + let (s, cu) = repr_substituted cu in + (s, BCalias cu) +| PBCconstant -> (None, BCconstant) + +let to_memory (init_code, fun_code, fv) = + 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 env.out_buffer 0 env.out_position in + let code = CString.hcons code 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 = []))) env.label_table; + (code, reloc, fv) diff --git a/kernel/vmemitcodes.mli b/kernel/vmemitcodes.mli new file mode 100644 index 0000000000..5c0e103143 --- /dev/null +++ b/kernel/vmemitcodes.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* patches -> (reloc_info -> int) -> Vmvalues.tcode + +type to_patch = emitcodes * patches * fv + +type body_code = + | BCdefined of to_patch + | BCalias of Constant.t + | BCconstant + + +type to_patch_substituted + +val from_val : body_code -> to_patch_substituted + +val force : to_patch_substituted -> body_code + +val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted + +val repr_body_code : + to_patch_substituted -> Mod_subst.substitution list option * body_code + +val to_memory : bytecodes * bytecodes * fv -> to_patch + (** init code, fun code, fv *) diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml new file mode 100644 index 0000000000..332a331a7a --- /dev/null +++ b/kernel/vmlambda.ml @@ -0,0 +1,833 @@ +open Util +open Names +open Esubst +open Term +open Constr +open Declarations +open Vmvalues +open Environ +open Pp + +let pr_con sp = str(Names.Label.to_string (Constant.label sp)) + +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Levar of Evar.t * lambda array + | Lprod of lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of pconstant + | Lprim of pconstant option * CPrimitives.t * lambda array + (* No check if None *) + | Lcase of case_info * reloc_table * lambda * lambda * lam_branches + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lint of int + | Lmakeblock of int * lambda array + | Luint of Uint63.t + | Lfloat of Float64.t + | Lval of structured_values + | Lsort of Sorts.t + | Lind of pinductive + | Lproj of Projection.Repr.t * lambda + +(* We separate branches for constant and non-constant constructors. If the OCaml + limitation on non-constant constructors is reached, remaining branches are + stored in [extra_branches]. *) +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } +(* extra_branches : (name array * lambda) array } *) + +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array + +(** Printing **) + +let pr_annot x = Name.print x.Context.binder_name + +let pp_names ids = + prlist_with_sep (fun _ -> brk(1,1)) pr_annot (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" + | InSProp -> str "SProp" + | InType -> str "Type" + +let rec pp_lam lam = + match lam with + | Lrel (id,n) -> pp_rel id n + | Lvar id -> Id.print id + | Levar (evk, args) -> + hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") + | 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 " ++ + pr_annot 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") + | Lif (t, bt, bf) -> + v 0 (str "(if " ++ pp_lam t ++ + cut () ++ str "then " ++ pp_lam bt ++ + cut() ++ str "else " ++ pp_lam bf ++ str ")") + | 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) -> + pr_annot 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) -> + pr_annot 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")") + | Luint i -> str (Uint63.to_string i) + | Lfloat f -> str (Float64.to_string f) + | Lval _ -> str "values" + | Lsort s -> pp_sort s + | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i + | Lprim(Some (kn,_u),_op,args) -> + hov 1 + (str "(PRIM " ++ pr_con kn ++ spc() ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ + str")") + | Lprim(None,op,args) -> + hov 1 + (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ + str")") + | Lproj(p,arg) -> + hov 1 + (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg + ++ str ")") + | Lint i -> + Pp.(str "(int:" ++ int i ++ str ")") + +(*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 map_lam_with_binders g f n lam = + match lam with + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ + | Lfloat _ -> lam + | Levar (evk, args) -> + let args' = Array.Smart.map (f n) args in + if args == args' then lam else Levar (evk, args') + | 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.Smart.map (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.Smart.map (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.Smart.map 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') + | Lif(t,bt,bf) -> + let t' = f n t in + let bt' = f n bt in + let bf' = f n bf in + if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') + | Lfix(init,(ids,ltypes,lbodies)) -> + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (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.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (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.Smart.map (f n) args in + if args == args' then lam else Lmakeblock(tag,args') + | Lprim(kn,op,args) -> + let args' = Array.Smart.map (f n) args in + if args == args' then lam else Lprim(kn,op,args') + | Lproj(p,arg) -> + let arg' = f n arg in + if arg == arg' then lam else Lproj(p,arg') + +(*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.Smart.map (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 _ | Luint _ + | Lval _ | Lsort _ | Lind _ -> true + | _ -> false + + +let can_merge_if bt bf = + match bt, bf with + | Llam(_idst,_), Llam(_idsf,_) -> true + | _ -> false + +let merge_if t bt bf = + let (idst,bodyt) = decompose_Llam bt in + let (idsf,bodyf) = decompose_Llam bf in + let nt = Array.length idst in + let nf = Array.length idsf in + let common,idst,idsf = + if nt = nf then idst, [||], [||] + else + if nt < nf then idst,[||], Array.sub idsf nt (nf - nt) + else idsf, Array.sub idst nf (nt - nf), [||] in + Llam(common, + Lif(lam_lift (Array.length common) t, + mkLlam idst bodyt, + mkLlam idsf bodyf)) + + +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 + + | Lif(t,bt,bf) -> + let t' = simplify subst t in + let bt' = simplify subst bt in + let bf' = simplify subst bf in + if can_merge_if bt' bf' then merge_if t' bt' bf' + else + if t == t' && bt == bt' && bf == bf' then lam + else Lif(t',bt',bf') + | _ -> 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.Smart.map (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 _ | Lint _ | Luint _ + | Lfloat _ -> kind + | Levar (_, args) -> + occurrence_args k kind args + | 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 + | Lif (t, bt, bf) -> + let kind = occurrence k kind t in + kind && occurrence k kind bt && occurrence k kind bf + | 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 + +and occurrence_args k kind args = + Array.fold_left (occurrence k) kind args + +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 + Obj.last_non_constant_constructor_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 _ | Lint _ | Luint _ -> true + | _ -> false + +let get_value lc = + match lc with + | Luint i -> val_of_uint i + | Lval v -> v + | Lint i -> val_of_int i + | _ -> raise Not_found + +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 anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) + let ids = Array.make (nparams + arity) anon in + if arity = 0 then mkLlam ids (Lint 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 Lint tag + else + if Array.for_all is_value args then + if tag < Obj.last_non_constant_constructor_tag then + Lval(val_of_block tag (Array.map get_value args)) + else + let args = Array.map get_value args in + let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in + Lval(val_of_block Obj.last_non_constant_constructor_tag args) + else Lmakeblock(tag, args) + +let makearray args def = + try + let p = Array.map get_value args in + Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def)) + with Not_found -> + let ar = Lmakeblock(0, args) in (* build the ocaml array *) + let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *) + Lmakeblock(0,[|kind|]) (* the reference *) + +(* 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 Vmemitcodes.force tps with + | Vmemitcodes.BCalias kn' -> get_alias env kn' + | _ -> kn) + +(* Compilation of primitive *) + +let prim kn p args = + Lprim(Some kn, p, args) + +let expand_prim kn op arity = + (* primitives are always Relevant *) + let ids = Array.make arity Context.anonR in + let args = make_args arity 1 in + Llam(ids, prim kn op args) + +let lambda_of_prim kn op args = + let arity = CPrimitives.arity op in + match Int.compare (Array.length args) arity with + | 0 -> prim kn op args + | x when x > 0 -> + let prim_args = Array.sub args 0 arity in + let extra_args = Array.sub args arity (Array.length args - arity) in + mkLapp(prim kn op prim_args) extra_args + | _ -> mkLapp (expand_prim kn op arity) 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 : 'a t) = + 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 : 'a t) n = + v.size <- max 0 (v.size - n) + + let pop v = popn v 1 + + let get_last (v : 'a t) 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.Context.binder_name + + 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 "Vmbytegen.lambda_of_constr: Meta") + | Evar (evk, args) -> + let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in + Levar (evk, args) + + | 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,_iv,a,branches) -> (* XXX handle iv *) + 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 + (* 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 anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) + let ids = Array.make arity anon 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 rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in + 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 lc = lambda_of_constr env c in + Lproj (Projection.repr p,lc) + + | Int i -> Luint i + | Float f -> Lfloat f + | Array(_u, t,def,_ty) -> + let def = lambda_of_constr env def in + makearray (lambda_of_args env 0 t) def + +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 + let cb = lookup_constant kn env.global_env in + begin match cb.const_body with + | Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args) + | 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 nparams < nargs then (* got all parameters *) + let args = lambda_of_args env nparams args in + makeblock tag 0 arity args + else 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 dump_lambda = ref false + +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_annot (rel_context genv) 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 !dump_lambda then + Feedback.msg_debug (pp_lam lam); + lam diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli new file mode 100644 index 0000000000..bd11c2667f --- /dev/null +++ b/kernel/vmlambda.mli @@ -0,0 +1,45 @@ +open Names +open Constr +open Vmvalues +open Environ + +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Levar of Evar.t * lambda array + | Lprod of lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of pconstant + | Lprim of pconstant option * CPrimitives.t * lambda array + (* No check if None *) + | Lcase of case_info * reloc_table * lambda * lambda * lam_branches + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lint of int + | Lmakeblock of int * lambda array + | Luint of Uint63.t + | Lfloat of Float64.t + | Lval of structured_values + | Lsort of Sorts.t + | Lind of pinductive + | Lproj of Projection.Repr.t * lambda + +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } + +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array + +exception TooLargeInductive of Pp.t + +val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda + +val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda + +val get_alias : env -> Constant.t -> Constant.t + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml new file mode 100644 index 0000000000..85f7369654 --- /dev/null +++ b/kernel/vmsymtable.ml @@ -0,0 +1,226 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* atom array -> vm_global -> values array -> values = "coq_eval_tcode" + +type global_data = { mutable glob_len : int; mutable glob_val : values array } + +(*******************) +(* Linkage du code *) +(*******************) + +(* Table des globaux *) + +(* [global_data] contient les valeurs des constantes globales + (axiomes,definitions), les annotations des switch et les structured + constant *) +let global_data = { + glob_len = 0; + glob_val = Array.make 4096 crazy_val; +} + +let get_global_data () = Vmvalues.vm_global global_data.glob_val + +let realloc_global_data n = + let n = min (2 * n + 0x100) Sys.max_array_length in + let ans = Array.make n crazy_val in + let src = global_data.glob_val in + let () = Array.blit src 0 ans 0 (Array.length src) in + global_data.glob_val <- ans + +let check_global_data n = + if n >= Array.length global_data.glob_val then realloc_global_data n + +let set_global v = + let n = global_data.glob_len in + check_global_data n; + global_data.glob_val.(n) <- v; + global_data.glob_len <- global_data.glob_len + 1; + n + +(* Initialization of OCaml primitives *) +let parray_make = set_global Vmvalues.parray_make +let parray_get = set_global Vmvalues.parray_get +let parray_get_default = set_global Vmvalues.parray_get_default +let parray_set = set_global Vmvalues.parray_set +let parray_copy = set_global Vmvalues.parray_copy +let parray_reroot = set_global Vmvalues.parray_reroot +let parray_length = set_global Vmvalues.parray_length + +(* table pour les structured_constant et les annotations des switchs *) + +module SConstTable = Hashtbl.Make (struct + type t = structured_constant + let equal = eq_structured_constant + let hash = hash_structured_constant +end) + +module AnnotTable = Hashtbl.Make (struct + type t = annot_switch + let equal = eq_annot_switch + let hash = hash_annot_switch +end) + +module ProjNameTable = Hashtbl.Make (Projection.Repr) + +let str_cst_tbl : int SConstTable.t = SConstTable.create 31 + +let annot_tbl : int AnnotTable.t = AnnotTable.create 31 + (* (annot_switch * int) Hashtbl.t *) + +let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31 + +(*************************************************************) +(*** Mise a jour des valeurs des variables et des constantes *) +(*************************************************************) + +exception NotEvaluated + +let key rk = + match !rk with + | None -> raise NotEvaluated + | Some k -> + try CEphemeron.get k + with CEphemeron.InvalidKey -> raise NotEvaluated + +(************************) +(* traduction des patch *) + +(* slot_for_*, calcul la valeur de l'objet, la place + dans la table global, rend sa position dans la table *) + +let slot_for_str_cst key = + try SConstTable.find str_cst_tbl key + with Not_found -> + let n = set_global (val_of_str_const key) in + SConstTable.add str_cst_tbl key n; + n + +let slot_for_annot key = + try AnnotTable.find annot_tbl key + with Not_found -> + let n = set_global (val_of_annot_switch key) in + AnnotTable.add annot_tbl key n; + n + +let slot_for_caml_prim = + let open CPrimitives in function + | Arraymake -> parray_make + | Arrayget -> parray_get + | Arraydefault -> parray_get_default + | Arrayset -> parray_set + | Arraycopy -> parray_copy + | Arrayreroot -> parray_reroot + | Arraylength -> parray_length + | _ -> assert false + +let slot_for_proj_name key = + try ProjNameTable.find proj_name_tbl key + with Not_found -> + let n = set_global (val_of_proj_name key) in + ProjNameTable.add proj_name_tbl key n; + n + +let rec slot_for_getglobal env kn = + let (cb,(_,rk)) = lookup_constant_key kn env in + try key rk + with NotEvaluated -> +(* Pp.msgnl(str"not yet evaluated");*) + let pos = + match cb.const_body_code with + | None -> set_global (val_of_constant kn) + | Some code -> + match Vmemitcodes.force code with + | BCdefined(code,pl,fv) -> + let v = eval_to_patch env (code,pl,fv) in + set_global v + | BCalias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant kn) + in +(*Pp.msgnl(str"value stored at: "++int pos);*) + rk := Some (CEphemeron.create pos); + pos + +and slot_for_fv env fv = + let fill_fv_cache cache id v_of_id env_of_id b = + let v,d = + match b with + | None -> v_of_id id, Id.Set.empty + | Some c -> + val_of_constr (env_of_id id env) c, + Environ.global_vars_set env c in + build_lazy_val cache (v, d); v in + let val_of_rel i = val_of_rel (nb_rel env - i) in + let idfun _ x = x in + match fv with + | FVnamed id -> + let nv = lookup_named_val id env in + begin match force_lazy_val nv with + | None -> + env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun + | Some (v, _) -> v + end + | FVrel i -> + let rv = lookup_rel_val i env in + begin match force_lazy_val rv with + | None -> + env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + | Some (v, _) -> v + end + | FVevar evk -> val_of_evar evk + | FVuniv_var _idu -> + assert false + +and eval_to_patch env (buff,pl,fv) = + 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 + | Reloc_proj_name p -> slot_for_proj_name p + | Reloc_caml_prim op -> slot_for_caml_prim op + in + let tc = patch buff pl slots in + let vm_env = + (* Beware, this may look like a call to [Array.map], but it's not. + Calling [Array.map f] when the first argument returned by [f] + is a float would lead to [vm_env] being an unboxed Double_array + (Tag_val = Double_array_tag) whereas eval_tcode expects a + regular array (Tag_val = 0). + See test-suite/primitive/float/coq_env_double_array.v + for an actual instance. *) + let a = Array.make (Array.length fv) crazy_val in + Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in + eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env + +and val_of_constr env c = + match compile ~fail_on_error:true env c with + | Some v -> eval_to_patch env (to_memory v) + | None -> assert false + +let set_transparent_const _kn = () (* !?! *) +let set_opaque_const _kn = () (* !?! *) diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli new file mode 100644 index 0000000000..e480bfcec1 --- /dev/null +++ b/kernel/vmsymtable.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* constr -> Vmvalues.values + +val set_opaque_const : Constant.t -> unit +val set_transparent_const : Constant.t -> unit + +val get_global_data : unit -> Vmvalues.vm_global -- cgit v1.2.3