From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/vm.ml | 601 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 601 insertions(+) create mode 100644 kernel/vm.ml (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml new file mode 100644 index 00000000..c8be979e --- /dev/null +++ b/kernel/vm.ml @@ -0,0 +1,601 @@ +open Obj +open Names +open Term +open Conv_oracle +open Cbytecodes + + +external set_drawinstr : unit -> unit = "coq_set_drawinstr" + +(******************************************) +(* Fonctions en plus du module Obj ********) +(******************************************) + +external offset_closure : t -> int -> t = "coq_offset_closure" +external offset : t -> int = "coq_offset" +let first o = (offset_closure o (offset o)) +let last o = (field o (size o - 1)) + +let accu_tag = 0 + +(*******************************************) +(* Initalisation de la machine abstraite ***) +(*******************************************) + +external init_vm : unit -> unit = "init_coq_vm" + +let _ = init_vm () + +external transp_values : unit -> bool = "get_coq_transp_value" +external set_transp_values : bool -> unit = "coq_set_transp_value" + +(*******************************************) +(* Le code machine ************************) +(*******************************************) + +type tcode +let tcode_of_obj v = ((obj v):tcode) +let fun_code v = tcode_of_obj (field (repr v) 0) + +external mkAccuCode : int -> tcode = "coq_makeaccu" +external mkPopStopCode : int -> tcode = "coq_pushpop" +external mkAccuCond : int -> tcode = "coq_accucond" + +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 = + let len = Array.length !popstop_tbl in + if i < len then !popstop_tbl.(i) + else + begin + popstop_tbl := + Array.init (i+10) + (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j); + !popstop_tbl.(i) + end + +let stop = popstop_code 0 + +(******************************************************) +(* Types de donnees abstraites et fonctions associees *) +(******************************************************) + +(* Values of the abstract machine *) +let val_of_obj v = ((obj v):values) +let crasy_val = (val_of_obj (repr 0)) + + +(* Functions *) +type vfun +(* v = [Tc | c | fv1 | ... | fvn ] *) +(* ^ *) +(* [Tc | (Restart : c) | v | a1 | ... an] *) +(* ^ *) + +(* Products *) +type vprod +(* [0 | dom : codom] *) +(* ^ *) +let dom : vprod -> values = fun p -> val_of_obj (field (repr p) 0) +let codom : vprod -> vfun = fun p -> (obj (field (repr p) 1)) + +(* Arguments *) +type arguments +(* arguments = [_ | _ | _ | a1 | ... | an] *) +(* ^ *) +let nargs : arguments -> int = fun args -> (size (repr args)) - 2 + +let unsafe_arg : arguments -> int -> values = + fun args i -> val_of_obj (field (repr args) (i+2)) + +let arg args i = + if 0 <= i && i < (nargs args) then unsafe_arg args i + else raise (Invalid_argument + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i))) + +(* Fixpoints *) +type vfix + +(* [Tc|c0|Ti|c1|...|Ti|cn|fv1|...|fvn| [ct0|...|ctn]] *) +(* ^ *) +type vfix_block + +let fix_init : vfix -> int = fun vf -> (offset (repr vf)/2) + +let block_of_fix : vfix -> vfix_block = fun vf -> obj (first (repr vf)) + +let fix_block_type : vfix_block -> tcode array = + fun fb -> (obj (last (repr fb))) + +let fix_block_ndef : vfix_block -> int = + fun fb -> size (last (repr fb)) + +let fix_ndef vf = fix_block_ndef (block_of_fix vf) + +let unsafe_fb_code : vfix_block -> int -> tcode = + fun fb i -> tcode_of_obj (field (repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 + +let rec_args vf = + let fb = block_of_fix vf in + let size = fix_block_ndef fb in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = fix_init f1, fix_init f2 in + (* Verification du point de depart *) + if i1 = i2 then + let fb1,fb2 = block_of_fix f1, block_of_fix f2 in + let n = fix_block_ndef fb1 in + (* Verification du nombre de definition *) + if n = fix_block_ndef fb2 then + (* Verification des arguments recursifs *) + try + for i = 0 to n - 1 do + if not (unsafe_rec_arg fb1 i = unsafe_rec_arg fb2 i) then + raise FALSE + done; + true + with FALSE -> false + else false + else false + +(* Partials applications of Fixpoints *) +type vfix_app +let fix : vfix_app -> vfix = + fun vfa -> ((obj (field (repr vfa) 1)):vfix) +let args_of_fix : vfix_app -> arguments = + fun vfa -> ((magic vfa) : arguments) + +(* CoFixpoints *) +type vcofix +type vcofix_block +let cofix_init : vcofix -> int = fun vcf -> (offset (repr vcf)/2) + +let block_of_cofix : vcofix -> vcofix_block = fun vcf -> obj (first (repr vcf)) + +let cofix_block_ndef : vcofix_block -> int = + fun fb -> size (last (repr fb)) + +let cofix_ndef vcf= cofix_block_ndef (block_of_cofix vcf) + +let cofix_block_type : vcofix_block -> tcode array = + fun cfb -> (obj (last (repr cfb))) + +let check_cofix cf1 cf2 = + cofix_init cf1 = cofix_init cf2 && + cofix_ndef cf1 = cofix_ndef cf2 + +let cofix_arity c = int_tcode c 1 + +let unsafe_cfb_code : vcofix_block -> int -> tcode = + fun cfb i -> tcode_of_obj (field (repr cfb) (2 * i)) + +(* Partials applications of CoFixpoints *) +type vcofix_app +let cofix : vcofix_app -> vcofix = + fun vcfa -> ((obj (field (repr vcfa) 1)):vcofix) +let args_of_cofix : vcofix_app -> arguments = + fun vcfa -> ((magic vcfa) : arguments) + +(* Blocks *) +type vblock (* la representation Ocaml *) +let btag : vblock -> int = fun b -> tag (repr b) +let bsize : vblock -> int = fun b -> size (repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then + val_of_obj (field (repr b) i) + else raise (Invalid_argument "Vm.bfield") + +(* Accumulators and atoms *) + +type accumulator +(* [Ta | accumulate | at | a1 | ... | an ] *) + +type inv_rel_key = int + +type id_key = inv_rel_key tableKey + +type vstack = values array + +type vm_env + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +(* Ne pas changer ce type sans modifier le code C *) +type atom = + | Aid of id_key + | Aiddef of id_key * values + | Aind of inductive + | Afix_app of accumulator * vfix_app + | Aswitch of accumulator * vswitch + +let atom_of_accu : accumulator -> atom = + fun a -> ((obj (field (repr a) 1)) : atom) + +let args_of_accu : accumulator -> arguments = + fun a -> ((magic a) : arguments) + +let nargs_of_accu a = nargs (args_of_accu a) + +(* Les zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix_app + | Zswitch of vswitch + +type stack = zipper list + +type whd = + | Vsort of sorts + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix + | Vfix_app of vfix_app + | Vcofix of vcofix + | Vcofix_app of vcofix_app + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack +(* Les atomes sont forcement Aid Aiddef Aind *) + +(**********************************************) +(* Constructeurs ******************************) +(**********************************************) +(* obj_of_atom : atom -> t *) +let obj_of_atom : atom -> t = + fun a -> + let res = Obj.new_block accu_tag 2 in + set_field res 0 (repr accumulate); + set_field res 1 (repr a); + res + +(* obj_of_str_const : structured_constant -> t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_b0 tag -> repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = new_block tag len in + for i = 0 to len - 1 do + set_field res i (obj_of_str_const args.(i)) + done; + res + +let val_of_obj o = ((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 idkey_tbl = Hashtbl.create 31 + +let val_of_idkey key = + try Hashtbl.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + Hashtbl.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) +let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) + +let val_of_named id = val_of_idkey (VarKey id) +let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) + +let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_constant_def n c v = + let res = Obj.new_block accu_tag 2 in + set_field res 0 (repr (mkAccuCond n)); + set_field res 1 (repr (Aiddef(ConstKey c, v))); + val_of_obj res + + + +(*************************************************) +(* Destructors ***********************************) +(*************************************************) + + +let rec whd_accu a stk = + let stk = + if nargs_of_accu a = 0 then stk + else Zapp (args_of_accu a) :: stk in + let at = atom_of_accu a in + match at with + | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk) + | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk) + | Aswitch(a,sw) -> whd_accu a (Zswitch sw :: stk) + +external kind_of_closure : t -> int = "coq_kind_of_closure" + +let whd_val : values -> whd = + fun v -> + let o = repr v in + if is_int o then Vconstr_const (obj o) + else + let tag = tag o in + if tag = accu_tag then + if is_accumulate (fun_code o) then whd_accu (obj o) [] + else + if size o = 1 then Vsort(obj (field o 0)) + else Vprod(obj o) + else + if tag = closure_tag || tag = infix_tag then + match kind_of_closure o with + | 0 -> Vfun(obj o) + | 1 -> Vfix(obj o) + | 2 -> Vfix_app(obj o) + | 3 -> Vcofix(obj o) + | 4 -> Vcofix_app(obj o) + | 5 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work" + else Vconstr_block(obj o) + + + +(************************************************) +(* La machine abstraite *************************) +(************************************************) + + +(* gestion de la pile *) +external push_ra : tcode -> unit = "coq_push_ra" +external push_val : values -> unit = "coq_push_val" +external push_arguments : arguments -> unit = "coq_push_arguments" +external push_vstack : vstack -> unit = "coq_push_vstack" + + +(* interpreteur *) +external interprete : tcode -> values -> vm_env -> int -> values = + "coq_interprete_ml" + +let apply_arguments vf vargs = + let n = nargs vargs in + if n = 0 then vf + else + begin + push_ra stop; + push_arguments vargs; + interprete (fun_code vf) vf (magic vf) (n - 1) + end + +let apply_vstack vf vstk = + let n = Array.length vstk in + if n = 0 then vf + else + begin + push_ra stop; + push_vstack vstk; + interprete (fun_code vf) vf (magic vf) (n - 1) + end + +let apply_fix_app vfa arg = + let vf = fix vfa in + let vargs = args_of_fix vfa in + push_ra stop; + push_val arg; + push_arguments vargs; + interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs) + +external set_forcable : unit -> unit = "coq_set_forcable" +let force_cofix v = + match whd_val v with + | Vcofix _ | Vcofix_app _ -> + push_ra stop; + set_forcable (); + interprete (fun_code v) (magic v) (magic v) 0 + | _ -> v + +let apply_switch sw arg = + let arg = force_cofix arg in + let tc = sw.sw_annot.tailcall in + if tc then + (push_ra stop;push_vstack sw.sw_stk) + else + (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + interprete sw.sw_code arg sw.sw_env 0 + +let is_accu v = + is_block (repr v) && tag (repr v) = accu_tag && + fun_code v == accumulate + +let rec whd_stack v stk = + match stk with + | [] -> whd_val v + | Zapp a :: stkt -> whd_stack (apply_arguments v a) stkt + | Zfix fa :: stkt -> + if is_accu v then whd_accu (magic v) stk + else whd_stack (apply_fix_app fa v) stkt + | Zswitch sw :: stkt -> + if is_accu v then whd_accu (magic v) stk + else whd_stack (apply_switch sw v) stkt + +let rec force_whd v stk = + match whd_stack v stk with + | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk + | res -> res + + + +(* Function *) +external closure_arity : vfun -> int = "coq_closure_arity" + +(* [apply_rel v k arity] applique la valeurs [v] aux arguments + [k],[k+1], ... , [k+arity-1] *) +let mkrel_vstack k arity = + let max = k + arity - 1 in + Array.init arity (fun i -> val_of_rel (max - i)) + +let body_of_vfun k vf = + let vargs = mkrel_vstack k 1 in + apply_vstack (magic 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_vstack (magic vf1) vargs in + let v2 = apply_vstack (magic vf2) vargs in + arity, v1, v2 + + +(* Fix *) +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 jump_grabrec c = offset_tcode c 2 +let jump_grabrecrestart c = offset_tcode c 3 + +let bodies_of_fix k vf = + let fb = block_of_fix vf in + let ndef = fix_block_ndef fb in + (* Construction de l' environnement des corps des points fixes *) + let e = dup (repr fb) in + for i = 0 to ndef - 1 do + set_field e (2 * i) (repr (relaccu_code (k + i))) + done; + let fix_body i = + let c = jump_grabrec (unsafe_fb_code fb i) in + let res = Obj.new_block closure_tag 2 in + set_field res 0 (repr c); + set_field res 1 (offset_closure e (2*i)); + ((obj res) : vfun) + in Array.init ndef fix_body + +let types_of_fix vf = + let fb = block_of_fix vf in + let type_code = fix_block_type fb in + let type_val c = interprete c crasy_val (magic fb) 0 in + Array.map type_val type_code + + +(* CoFix *) +let jump_cograb c = offset_tcode c 2 +let jump_cograbrestart c = offset_tcode c 3 + +let bodies_of_cofix k vcf = + let cfb = block_of_cofix vcf in + let ndef = cofix_block_ndef cfb in + (* Construction de l' environnement des corps des cofix *) + let e = dup (repr cfb) in + for i = 0 to ndef - 1 do + set_field e (2 * i) (repr (relaccu_code (k + i))) + done; + let cofix_body i = + let c = unsafe_cfb_code cfb i in + let arity = int_tcode c 1 in + if arity = 0 then + begin + push_ra stop; + interprete (jump_cograbrestart c) crasy_val + (obj (offset_closure e (2*i))) 0 + end + else + let res = Obj.new_block closure_tag 2 in + set_field res 0 (repr (jump_cograb c)); + set_field res 1 (offset_closure e (2*i)); + ((obj res) : values) + in Array.init ndef cofix_body + +let types_of_cofix vcf = + let cfb = block_of_cofix vcf in + let type_code = cofix_block_type cfb in + let type_val c = interprete c crasy_val (magic cfb) 0 in + Array.map type_val type_code + +(* Switch *) + +let eq_tbl sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + +let case_info sw = sw.sw_annot.ci + +let type_of_switch sw = + push_vstack sw.sw_stk; + interprete sw.sw_type_code crasy_val sw.sw_env 0 + +let branch_arg k (tag,arity) = + if arity = 0 then ((magic tag):values) + else + let b = new_block tag arity in + for i = 0 to arity - 1 do + set_field b i (repr (val_of_rel (k+i))) + done; + val_of_obj b + + +let branch_of_switch k sw = + let eval_branch (_,arity as ta) = + let arg = branch_arg k ta in + let v = apply_switch sw arg in + (arity, v) + in + Array.map eval_branch sw.sw_annot.rtbl + + + + + + + + + + + + + + + + + + + + + + + + + + -- cgit v1.2.3