summaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativevalues.ml')
-rw-r--r--kernel/nativevalues.ml118
1 files changed, 59 insertions, 59 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
-open Names
-open CErrors
+
open Util
+open CErrors
+open Names
+open Constr
(** This module defines the representation of values internally used by
the native compiler *)
@@ -51,42 +54,43 @@ type atom =
| Arel of int
| Aconstant of pconstant
| Aind of pinductive
- | Asort of sorts
- | Avar of identifier
+ | Asort of Sorts.t
+ | Avar of Id.t
| Acase of annot_sw * accumulator * t * (t -> 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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 04:49:15 +0000