diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 546 |
1 files changed, 26 insertions, 520 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 51101f88e..352ea74a4 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,47 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Sorts -open Constr open Cbytecodes +open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" -(******************************************) -(* Utility Functions about Obj ************) -(******************************************) - -external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" -external offset : Obj.t -> int = "coq_offset" - -(*******************************************) -(* Initalization of the abstract machine ***) -(*******************************************) - -external init_vm : unit -> unit = "init_coq_vm" - -let _ = init_vm () - -(*******************************************) -(* Machine code *** ************************) -(*******************************************) - -type tcode -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) - -external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" -external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -external int_tcode : tcode -> int -> int = "coq_int_tcode" - -external accumulate : unit -> tcode = "accumulate_code" -let accumulate = accumulate () - -external is_accumulate : tcode -> bool = "coq_is_accumulate_code" - let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = @@ -62,106 +28,6 @@ let popstop_code i = let stop = popstop_code 0 -(******************************************************) -(* Abstract data types and utility functions **********) -(******************************************************) - -(* Values of the abstract machine *) -let val_of_obj v = ((Obj.obj v):values) -let crazy_val = (val_of_obj (Obj.repr 0)) - -(* Abstract data *) -type vprod -type vfun -type vfix -type vcofix -type vblock -type arguments - -type vm_env -type vstack = values array - -type vswitch = { - sw_type_code : tcode; - sw_code : tcode; - sw_annot : annot_switch; - sw_stk : vstack; - sw_env : vm_env - } - -(* Representation of values *) -(* + Products : *) -(* - vprod = 0_[ dom | codom] *) -(* dom : values, codom : vfun *) -(* *) -(* + Functions have two representations : *) -(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) -(* C:tcode, fvi : values *) -(* Remark : a function and its environment is the same value. *) -(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) -(* *) -(* + Fixpoints : *) -(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) -(* One single block to represent all of the fixpoints, each fixpoint *) -(* is the pointer to the field holding the pointer to its code, and *) -(* the infix tag is used to know where the block starts. *) -(* - Partial application follows the scheme of partially applied *) -(* functions. Note: only fixpoints not having been applied to its *) -(* recursive argument are coded this way. When the rec. arg. is *) -(* applied, either it's a constructor and the fix reduces, or it's *) -(* and the fix is coded as an accumulator. *) -(* *) -(* + Cofixpoints : see cbytegen.ml *) -(* *) -(* + vblock's encode (non constant) constructors as in Ocaml, but *) -(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) -(* accumulators. *) -(* *) -(* + vm_env is the type of the machine environments (i.e. a function or *) -(* a fixpoint) *) -(* *) -(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) -(* - representation of [accu] : tag_[....] *) -(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) -(* -- 10_[accu|proj name] : a projection blocked by an accu *) -(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 12_[accu|vswitch] : a match blocked by an accu *) -(* -- 13_[fcofix] : a cofix function *) -(* -- 14_[fcofix|val] : a cofix function, val represent the value *) -(* of the function applied to arg1 ... argn *) -(* The [arguments] type, which is abstracted as an array, represents : *) -(* tag[ _ | _ |v1|... | vn] *) -(* Generally the first field is a code pointer. *) - -(* Do not edit this type without editing C code, especially "coq_values.h" *) - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(* Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix*arguments (* Possibly empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up = values - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t (************************************************) (* Abstract machine *****************************) @@ -178,389 +44,72 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" - - (* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) (* Apply a value to arguments contained in [vargs] *) let apply_arguments vf vargs = let n = nargs vargs in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end (* Apply value [vf] to an array of argument values [varray] *) let apply_varray vf varray = let n = Array.length varray in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; (* The fun code of [vf] will make sure we have enough stack, so we put 0 here. *) push_vstack varray 0; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(*************************************************) -(* Destructors ***********************************) -(*************************************************) - -let uni_lvl_val (v : values) : Univ.Level.t = - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - CErrors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr ++ str ".") - -let rec whd_accu a stk = - let stk = - if Int.equal (Obj.size a) 2 then stk - else Zapp (Obj.obj a) :: stk in - let at = Obj.field a 1 in - match Obj.tag at with - | i when Int.equal i type_atom_tag -> - begin match stk with - | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) - | _ -> assert false - end - | i when i <= max_atom_tag -> - Vatom_stk(Obj.magic at, stk) - | i when Int.equal i proj_tag -> - let zproj = Zproj (Obj.obj (Obj.field at 0)) in - whd_accu (Obj.field at 1) (zproj :: stk) - | i when Int.equal i fix_app_tag -> - let fa = Obj.field at 1 in - let zfix = - Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in - whd_accu (Obj.field at 0) (zfix :: stk) - | i when Int.equal i switch_tag -> - let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in - whd_accu (Obj.field at 0) (zswitch :: stk) - | i when Int.equal i cofix_tag -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcfx, to_up, None) - | [Zapp args] -> Vcofix(vcfx, to_up, Some args) - | _ -> assert false - end - | i when Int.equal i cofix_evaluated_tag -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcofix, res, None) - | [Zapp args] -> Vcofix(vcofix, res, Some args) - | _ -> assert false - end - | tg -> - CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") - -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" - -let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in - if Obj.is_int o then Vconstr_const (Obj.obj o) - else - let tag = Obj.tag o in - if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) - else - if tag = Obj.closure_tag || tag = Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) - else - Vconstr_block(Obj.obj o) - -(**********************************************) -(* Constructors *******************************) -(**********************************************) - -let obj_of_atom : atom -> Obj.t = - fun a -> - let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); - Obj.set_field res 1 (Obj.repr a); - res - -(* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> Obj.repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p - | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res - | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) - -let val_of_obj o = ((Obj.obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let atom_of_proj kn v = - let r = Obj.new_block proj_tag 2 in - Obj.set_field r 0 (Obj.repr kn); - Obj.set_field r 1 (Obj.repr v); - ((Obj.obj r) : atom) - -let val_of_proj kn v = - val_of_atom (atom_of_proj kn v) - -module IdKeyHash = -struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal - open Hashset.Combine - let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) - | VarKey id -> combinesmall 2 (Id.hash id) - | RelKey i -> combinesmall 3 (Int.hash i) -end - -module KeyTable = Hashtbl.Make(IdKeyHash) - -let idkey_tbl = KeyTable.create 31 - -let val_of_idkey key = - try KeyTable.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - KeyTable.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) - -let val_of_named id = val_of_idkey (VarKey id) - -let val_of_constant c = val_of_idkey (ConstKey c) - -external val_of_annot_switch : annot_switch -> values = "%identity" - +(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) - -(*************************************************) -(** Operations manipulating data types ***********) -(*************************************************) - -(* Functions over products *) - -let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) -let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) - -(* Functions over vfun *) - -external closure_arity : vfun -> int = "coq_closure_arity" - -let body_of_vfun k vf = +let reduce_fun k vf = let vargs = mkrel_vstack k 1 in - apply_varray (Obj.magic vf) vargs + apply_varray vf vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_varray (Obj.magic vf1) vargs in - let v2 = apply_varray (Obj.magic vf2) vargs in + let v1 = apply_varray vf1 vargs in + let v2 = apply_varray vf2 vargs in arity, v1, v2 -(* Functions over fixpoint *) - -let first o = (offset_closure o (offset o)) -let last o = (Obj.field o (Obj.size o - 1)) - -let current_fix vf = - (offset (Obj.repr vf) / 2) - -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = first (Obj.repr vf) in - let size = Obj.size (last fb) in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = current_fix f1, current_fix f2 in - (* Checking starting point *) - if i1 = i2 then - let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in - let n = Obj.size (last fb1) in - (* Checking number of definitions *) - if n = Obj.size (last fb2) then - (* Checking recursive arguments *) - try - for i = 0 to n - 1 do - if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i - then raise FALSE - done; - true - with FALSE -> false - else false - else false - (* Functions over vfix *) -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" - -let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; - ref (Array.init len mkAccuCode) - -let relaccu_code i = - let len = Array.length !relaccu_tbl in - if i < len then !relaccu_tbl.(i) - else - begin - realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; - relaccu_tbl := - Array.init nl - (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); - !relaccu_tbl.(i) - end let reduce_fix k vf = - let fb = first (Obj.repr vf) in + let fb = first_fix vf in (* computing types *) - let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let fc_typ = fix_types fb in let ndef = Array.length fc_typ in - let et = offset_closure fb (2*(ndef - 1)) in + let et = offset_closure_fix fb (2*(ndef - 1)) in let ftyp = Array.map - (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in + (fun c -> interprete c crazy_val et 0) fc_typ in (* Construction of the environment of fix bodies *) - let e = Obj.dup fb in - for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) - done; - let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); - Obj.set_field res 1 (offset_closure e (2*i)); - ((Obj.obj res) : vfun) in - (Array.init ndef fix_body, ftyp) - -(* Functions over vcofix *) - -let get_fcofix vcf i = - match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with - | Vcofix(vcfi, _, _) -> vcfi - | _ -> assert false - -let current_cofix vcf = - let ndef = Obj.size (last (Obj.repr vcf)) in - let rec find_cofix pos = - if pos < ndef then - if get_fcofix vcf pos == vcf then pos - else find_cofix (pos+1) - else raise Not_found in - try find_cofix 0 - with Not_found -> assert false - -let check_cofix vcf1 vcf2 = - (current_cofix vcf1 = current_cofix vcf2) && - (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + (mk_fix_body k ndef fb, ftyp) let reduce_cofix k vcf = - let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let fc_typ = cofix_types vcf in let ndef = Array.length fc_typ in let ftyp = (* Evaluate types *) - Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in + Array.map (fun c -> interprete c crazy_val (cofix_env vcf) 0) fc_typ in (* Construction of the environment of cofix bodies *) - let e = Obj.dup (Obj.repr vcf) in - for i = 0 to ndef - 1 do - Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) - done; - - let cofix_body i = - let vcfi = get_fcofix vcf i in - let c = Obj.field (Obj.repr vcfi) 0 in - Obj.set_field e 0 c; - let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); - Obj.set_field self 1 (Obj.repr atom); - apply_varray (Obj.obj e) [|Obj.obj self|] in - (Array.init ndef cofix_body, ftyp) - - -(* Functions over vblock *) - -let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) -let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) - else invalid_arg "Vm.bfield" - - -(* Functions over vswitch *) - -let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl - -let case_info sw = sw.sw_annot.ci + (mk_cofix_body apply_varray k ndef vcf, ftyp) let type_of_switch sw = (* The fun code of types will make sure we have enough stack, so we put 0 @@ -568,20 +117,6 @@ let type_of_switch sw = push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 -let branch_arg k (tag,arity) = - if Int.equal arity 0 then ((Obj.magic tag):values) - else - let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 - else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); - b,1 in - for i = ofs to ofs + arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; - val_of_obj b - let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then @@ -603,8 +138,8 @@ let branch_of_switch k sw = (* t = a stk --> t v *) let rec apply_stack a stk v = match stk with - | [] -> apply_varray a [|v|] - | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v + | [] -> apply_varray (fun_of_val a) [|v|] + | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v | Zfix(f,args) :: stk -> let a,stk = @@ -615,7 +150,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args+ nargs args') in a, stk | _ -> @@ -623,7 +158,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) in a, stk in apply_stack a stk v @@ -634,50 +169,21 @@ let apply_whd k whd = let v = val_of_rel k in match whd with | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false - | Vfun f -> body_of_vfun k f + | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; push_val v; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0 + interprete (fix_code f) (fix_val f) (fix_env f) 0 | Vfix(f, Some args) -> push_ra stop; push_val v; push_arguments args; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) | Vcofix(_,to_up,_) -> push_ra stop; push_val v; - interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 + interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let rec pr_atom a = - Pp.(match a with - | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Constant.print c - | RelKey i -> str "#" ++ int i - | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") -and pr_whd w = - Pp.(match w with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" - | Vuniv_level _ -> assert false) -and pr_stack stk = - Pp.(match stk with - | [] -> str "[]" - | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) -and pr_zipper z = - Pp.(match z with - | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") |