From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/nativevalues.ml | 118 ++++++++++++++++++++++++------------------------- 1 file changed, 59 insertions(+), 59 deletions(-) (limited to 'kernel/nativevalues.ml') diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df30..066dfc39 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,14 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t) | Afix of t array * t array * rec_pos * int (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t - | Aprod of name * t * (t -> t) + | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of existential * t - | Aproj of constant * accumulator + | Aevar of Evar.t * t * t array + | Aproj of Constant.t * accumulator let accumulate_tag = 0 -let accumulate_code (k:accumulator) (x:t) = - let o = Obj.repr k in - let osize = Obj.size o in - let r = Obj.new_block accumulate_tag (osize + 1) in - for i = 0 to osize - 1 do - Obj.set_field r i (Obj.field o i) - done; - Obj.set_field r osize (Obj.repr x); - (Obj.obj r:t) - -let rec accumulate (x:t) = - accumulate_code (Obj.magic accumulate) x - -let mk_accu_gen rcode (a:atom) = -(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *) - let r = Obj.new_block 0 3 in - Obj.set_field r 0 (Obj.field (Obj.magic rcode) 0); - Obj.set_field r 1 (Obj.field (Obj.magic rcode) 1); - Obj.set_field r 2 (Obj.magic a); - (Obj.magic r:t);; - -let mk_accu (a:atom) = mk_accu_gen accumulate a +(** Unique pointer used to drive the accumulator function *) +let ret_accu = Obj.repr (ref ()) + +type accu_val = { mutable acc_atm : atom; acc_arg : Obj.t list } + +let mk_accu (a : atom) : t = + let rec accumulate data x = + if x == ret_accu then Obj.repr data + else + let data = { data with acc_arg = x :: data.acc_arg } in + let ans = Obj.repr (accumulate data) in + let () = Obj.set_tag ans accumulate_tag in + ans + in + let acc = { acc_atm = a; acc_arg = [] } in + let ans = Obj.repr (accumulate acc) in + (** FIXME: use another representation for accumulators, this causes naked + pointers. *) + let () = Obj.set_tag ans accumulate_tag in + (Obj.obj ans : t) + +let get_accu (k : accumulator) = + (Obj.magic k : Obj.t -> accu_val) ret_accu let mk_rel_accu i = mk_accu (Arel i) @@ -111,6 +115,7 @@ let mk_ind_accu ind u = mk_accu (Aind (ind,Univ.Instance.of_array u)) let mk_sort_accu s u = + let open Sorts in match s with | Prop _ -> mk_accu (Asort s) | Type s -> @@ -130,39 +135,34 @@ let mk_prod_accu s dom codom = let mk_meta_accu mv ty = mk_accu (Ameta (mv,ty)) -let mk_evar_accu ev ty = - mk_accu (Aevar (ev,ty)) +let mk_evar_accu ev ty args = + mk_accu (Aevar (ev,ty,args)) let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) let atom_of_accu (k:accumulator) = - (Obj.magic (Obj.field (Obj.magic k) 2) : atom) + (get_accu k).acc_atm let set_atom_of_accu (k:accumulator) (a:atom) = - Obj.set_field (Obj.magic k) 2 (Obj.magic a) + (get_accu k).acc_atm <- a let accu_nargs (k:accumulator) = - let nargs = Obj.size (Obj.magic k) - 3 in -(* if nargs < 0 then Format.eprintf "nargs = %i\n" nargs; *) - assert (nargs >= 0); - nargs + List.length (get_accu k).acc_arg let args_of_accu (k:accumulator) = - let nargs = accu_nargs k in - let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in - let t = Array.init nargs f in - Array.to_list t + let acc = (get_accu k).acc_arg in + (Obj.magic (Array.of_list acc) : t array) let is_accu x = let o = Obj.repr x in Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag let mk_fix_accu rec_pos pos types bodies = - mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos)) + mk_accu (Afix(types,bodies,rec_pos, pos)) let mk_cofix_accu pos types norm = - mk_accu_gen accumulate (Acofix(types,norm,pos,(Obj.magic 0 : t))) + mk_accu (Acofix(types,norm,pos,(Obj.magic 0 : t))) let upd_cofix (cofix :t) (cofix_fun : t) = let atom = atom_of_accu (Obj.magic cofix) in @@ -177,11 +177,10 @@ let force_cofix (cofix : t) = let atom = atom_of_accu accu in match atom with | Acofix(typ,norm,pos,f) -> - let f = ref f in - let args = List.rev (args_of_accu accu) in - List.iter (fun x -> f := !f x) args; - let v = !f (Obj.magic ()) in - set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); + let args = args_of_accu accu in + let f = Array.fold_right (fun arg f -> f arg) args f in + let v = f (Obj.magic ()) in + set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); v | Acofixe(_,_,_,v) -> v | _ -> cofix @@ -200,7 +199,7 @@ let mk_block tag args = (* Two instances of dummy_value should not be pointer equal, otherwise comparing them as terms would succeed *) let dummy_value : unit -> t = - fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed") + fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.") let cast_accu v = (Obj.magic v:accumulator) @@ -334,6 +333,7 @@ let l_or accu x y = if is_int x && is_int y then no_check_l_or x y else accu x y +[@@@ocaml.warning "-37"] type coq_carry = | Caccu of t | C0 of t @@ -430,7 +430,7 @@ let addmuldiv accu x y z = if is_int x && is_int y && is_int z then no_check_addmuldiv x y z else accu x y z - +[@@@ocaml.warning "-34"] type coq_bool = | Baccu of t | Btrue @@ -491,12 +491,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) -- cgit v1.2.3