aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--kernel/environ.ml35
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/nativecode.ml217
-rw-r--r--kernel/nativeinstr.mli1
-rw-r--r--kernel/nativelambda.ml18
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/nativevalues.ml222
-rw-r--r--kernel/nativevalues.mli71
-rw-r--r--kernel/primitives.ml91
-rw-r--r--kernel/primitives.mli39
-rw-r--r--kernel/retroknowledge.ml26
-rw-r--r--kernel/retroknowledge.mli16
13 files changed, 669 insertions, 71 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index c56982d99..1e2764997 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -62,6 +62,7 @@ Cbytecodes
Copcodes
Cemitcodes
Nativevalues
+Primitives
Nativeinstr
Future
Opaqueproof
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5a40b1c2a..be0b65d91 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -477,8 +477,11 @@ let register =
(* subfunction which adds the compiling information of an
int31 operation which has a specific vm instruction (associates
it to the name of the coq definition in the reactive retroknowledge) *)
- let add_int31_op retroknowledge v n op kn =
- add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+ let add_int31_op retroknowledge v n op prim kn =
+ let rk =
+ add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+ in
+ add_native_compiling_info rk v (Nativelambda.compile_prim prim kn)
in
let add_int31_before_match rk v =
@@ -490,16 +493,16 @@ let register =
fun env field value ->
(* subfunction which shortens the (very often use) registration of binary
operators to the reactive retroknowledge. *)
- let add_int31_binop_from_const op =
+ let add_int31_binop_from_const op prim =
match kind_of_term value with
| Const kn -> retroknowledge add_int31_op env value 2
- op kn
+ op prim kn
| _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
in
- let add_int31_unop_from_const op =
+ let add_int31_unop_from_const op prim =
match kind_of_term value with
| Const kn -> retroknowledge add_int31_op env value 1
- op kn
+ op prim kn
| _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
in
(* subfunction which completes the function constr_of_int31 above
@@ -531,33 +534,47 @@ fun env field value ->
(add_int31_before_match
(retroknowledge add_int31c env i31c) value)
| KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
+ Primitives.Int31add
| KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
+ Primitives.Int31addc
| KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
+ Primitives.Int31addcarryc
| KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
+ Primitives.Int31sub
| KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
+ Primitives.Int31subc
| KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const
- Cbytecodes.Ksubcarrycint31
+ Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
| KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
+ Primitives.Int31mul
| KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
+ Primitives.Int31mulc
| KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
(match kind_of_term value with
| Const kn ->
retroknowledge add_int31_op env value 3
- Cbytecodes.Kdiv21int31 kn
+ Cbytecodes.Kdiv21int31 Primitives.Int31div21 kn
| _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
| KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
+ Primitives.Int31div
| KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
(match kind_of_term value with
| Const kn ->
retroknowledge add_int31_op env value 3
- Cbytecodes.Kaddmuldivint31 kn
+ Cbytecodes.Kaddmuldivint31 Primitives.Int31addmuldiv kn
| _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
| KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
+ Primitives.Int31compare
| KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
+ Primitives.Int31head0
| KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
+ Primitives.Int31tail0
| KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31
+ Primitives.Int31lor
| KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31
+ Primitives.Int31land
| KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31
+ Primitives.Int31lxor
| _ -> env.retroknowledge
in
Retroknowledge.add_field retroknowledge_with_reactive_info field value
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 3267b7e75..0d0adf9a7 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -13,6 +13,7 @@ Cbytecodes
Copcodes
Cemitcodes
Nativevalues
+Primitives
Nativeinstr
Opaqueproof
Declareops
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c4ede775e..c8572eec3 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -12,6 +12,7 @@ open Context
open Declarations
open Util
open Nativevalues
+open Primitives
open Nativeinstr
open Nativelambda
open Pre_env
@@ -255,14 +256,32 @@ type primitive =
| Mk_rel of int
| Mk_var of identifier
| Is_accu
+ | Is_int
| Cast_accu
| Upd_cofix
| Force_cofix
| Mk_uint
+ | Mk_int
+ | Mk_bool
+ | Val_to_int
| Mk_I31_accu
| Decomp_uint
| Mk_meta
| Mk_evar
+ | MLand
+ | MLle
+ | MLlt
+ | MLinteq
+ | MLlsl
+ | MLlsr
+ | MLland
+ | MLlor
+ | MLlxor
+ | MLadd
+ | MLsub
+ | MLmul
+ | MLmagic
+ | Coq_primitive of Primitives.t * (prefix * constant) option
let eq_primitive p1 p2 =
match p1, p2 with
@@ -284,29 +303,49 @@ let eq_primitive p1 p2 =
| _ -> false
let primitive_hash = function
-| Mk_prod -> 1
-| Mk_sort -> 2
-| Mk_ind -> 3
-| Mk_const -> 4
-| Mk_sw -> 5
-| Mk_fix (r, i) ->
- let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in
- combinesmall 6 (combine h (Int.hash i))
-| Mk_cofix i ->
- combinesmall 7 (Int.hash i)
-| Mk_rel i ->
- combinesmall 8 (Int.hash i)
-| Mk_var id ->
- combinesmall 9 (Id.hash id)
-| Is_accu -> 10
-| Cast_accu -> 11
-| Upd_cofix -> 12
-| Force_cofix -> 13
-| Mk_uint -> 14
-| Mk_I31_accu -> 15
-| Decomp_uint -> 16
-| Mk_meta -> 17
-| Mk_evar -> 18
+ | Mk_prod -> 1
+ | Mk_sort -> 2
+ | Mk_ind -> 3
+ | Mk_const -> 4
+ | Mk_sw -> 5
+ | Mk_fix (r, i) ->
+ let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in
+ combinesmall 6 (combine h (Int.hash i))
+ | Mk_cofix i ->
+ combinesmall 7 (Int.hash i)
+ | Mk_rel i ->
+ combinesmall 8 (Int.hash i)
+ | Mk_var id ->
+ combinesmall 9 (Id.hash id)
+ | Is_accu -> 10
+ | Is_int -> 11
+ | Cast_accu -> 12
+ | Upd_cofix -> 13
+ | Force_cofix -> 14
+ | Mk_uint -> 15
+ | Mk_int -> 16
+ | Mk_bool -> 17
+ | Val_to_int -> 18
+ | Mk_I31_accu -> 19
+ | Decomp_uint -> 20
+ | Mk_meta -> 21
+ | Mk_evar -> 22
+ | MLand -> 23
+ | MLle -> 24
+ | MLlt -> 25
+ | MLinteq -> 26
+ | MLlsl -> 27
+ | MLlsr -> 28
+ | MLland -> 29
+ | MLlor -> 30
+ | MLlxor -> 31
+ | MLadd -> 32
+ | MLsub -> 33
+ | MLmul -> 34
+ | MLmagic -> 35
+ | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim)
+ | Coq_primitive (prim, Some (prefix,kn)) ->
+ combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
type mllambda =
| MLlocal of lname
@@ -828,6 +867,113 @@ let merge_branches t =
Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
Array.of_list (to_list newt)
+
+type prim_aux =
+ | PAprim of string * constant * Primitives.t * prim_aux array
+ | PAml of mllambda
+
+let add_check cond args =
+ let aux cond a =
+ match a with
+ | PAml(MLint _) -> cond
+ | PAml ml ->
+ (* FIXME: use explicit equality function *)
+ if List.mem ml cond then cond else ml::cond
+ | _ -> cond
+ in
+ Array.fold_left aux cond args
+
+let extract_prim ml_of l =
+ let decl = ref [] in
+ let cond = ref [] in
+ let rec aux l =
+ match l with
+ | Lprim(prefix,kn,p,args) ->
+ let args = Array.map aux args in
+ cond := add_check !cond args;
+ PAprim(prefix,kn,p,args)
+ | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l)
+ | _ ->
+ let x = fresh_lname Anonymous in
+ decl := (x,ml_of l)::!decl;
+ PAml (MLlocal x) in
+ let res = aux l in
+ (!decl, !cond, res)
+
+let app_prim p args = MLapp(MLprimitive p, args)
+
+let to_int v =
+ match v with
+ | MLapp(MLprimitive Mk_uint, t) ->
+ begin match t.(0) with
+ | MLuint i -> MLint (Uint31.to_int i)
+ | _ -> MLapp(MLprimitive Val_to_int, [|v|])
+ end
+ | MLapp(MLprimitive Mk_int, t) -> t.(0)
+ | _ -> MLapp(MLprimitive Val_to_int, [|v|])
+
+let of_int v =
+ match v with
+ | MLapp(MLprimitive Val_to_int, t) -> t.(0)
+ | _ -> MLapp(MLprimitive Mk_int,[|v|])
+
+let compile_prim decl cond paux =
+(*
+ let args_to_int args =
+ for i = 0 to Array.length args - 1 do
+ args.(i) <- to_int args.(i)
+ done;
+ args in
+ *)
+ let rec opt_prim_aux paux =
+ match paux with
+ | PAprim(prefix, kn, op, args) ->
+ let args = Array.map opt_prim_aux args in
+ app_prim (Coq_primitive(op,None)) args
+(*
+ TODO: check if this inling was useful
+ begin match op with
+ | Int31lt ->
+ if Sys.word_size = 64 then
+ app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|]
+ else app_prim (Coq_primitive (Primitives.Int31lt,None)) args
+ | Int31le ->
+ if Sys.word_size = 64 then
+ app_prim Mk_bool [|(app_prim MLle (args_to_int args))|]
+ else app_prim (Coq_primitive (Primitives.Int31le, None)) args
+ | Int31lsl -> of_int (mk_lsl (args_to_int args))
+ | Int31lsr -> of_int (mk_lsr (args_to_int args))
+ | Int31land -> of_int (mk_land (args_to_int args))
+ | Int31lor -> of_int (mk_lor (args_to_int args))
+ | Int31lxor -> of_int (mk_lxor (args_to_int args))
+ | Int31add -> of_int (mk_add (args_to_int args))
+ | Int31sub -> of_int (mk_sub (args_to_int args))
+ | Int31mul -> of_int (mk_mul (args_to_int args))
+ | _ -> app_prim (Coq_primitive(op,None)) args
+ end *)
+ | PAml ml -> ml
+ and naive_prim_aux paux =
+ match paux with
+ | PAprim(prefix, kn, op, args) ->
+ app_prim (Coq_primitive(op, Some (prefix, kn))) (Array.map naive_prim_aux args)
+ | PAml ml -> ml in
+
+ let compile_cond cond paux =
+ match cond with
+ | [] -> opt_prim_aux paux
+ | [c1] ->
+ MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux)
+ | c1::cond ->
+ let cond =
+ List.fold_left
+ (fun ml c -> app_prim MLland [| ml; to_int c|])
+ (app_prim MLland [|to_int c1; MLint 0 |]) cond in
+ let cond = app_prim MLmagic [|cond|] in
+ MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in
+ let add_decl decl body =
+ List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in
+ add_decl decl (compile_cond cond paux)
+
let rec ml_of_lam env l t =
match t with
| Lrel(id ,i) -> get_rel env id i
@@ -858,6 +1004,9 @@ let merge_branches t =
| Lapp(f,args) ->
MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
| Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c))
+ | Lprim _ ->
+ let decl,cond,paux = extract_prim (ml_of_lam env l) t in
+ compile_prim decl cond paux
| Lcase (annot,p,a,bs) ->
(* let predicate_uid fv_pred = compilation of p
let rec case_uid fv a_uid =
@@ -1482,14 +1631,36 @@ let pp_mllam fmt l =
| Mk_var id ->
Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
| Is_accu -> Format.fprintf fmt "is_accu"
+ | Is_int -> Format.fprintf fmt "is_int"
| Cast_accu -> Format.fprintf fmt "cast_accu"
| Upd_cofix -> Format.fprintf fmt "upd_cofix"
| Force_cofix -> Format.fprintf fmt "force_cofix"
| Mk_uint -> Format.fprintf fmt "mk_uint"
+ | Mk_int -> Format.fprintf fmt "mk_int"
+ | Mk_bool -> Format.fprintf fmt "mk_bool"
+ | Val_to_int -> Format.fprintf fmt "val_to_int"
| Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu"
| Decomp_uint -> Format.fprintf fmt "decomp_uint"
| Mk_meta -> Format.fprintf fmt "mk_meta_accu"
| Mk_evar -> Format.fprintf fmt "mk_evar_accu"
+ | MLand -> Format.fprintf fmt "(&&)"
+ | MLle -> Format.fprintf fmt "(<=)"
+ | MLlt -> Format.fprintf fmt "(<)"
+ | MLinteq -> Format.fprintf fmt "(==)"
+ | MLlsl -> Format.fprintf fmt "(lsl)"
+ | MLlsr -> Format.fprintf fmt "(lsr)"
+ | MLland -> Format.fprintf fmt "(land)"
+ | MLlor -> Format.fprintf fmt "(lor)"
+ | MLlxor -> Format.fprintf fmt "(lxor)"
+ | MLadd -> Format.fprintf fmt "(+)"
+ | MLsub -> Format.fprintf fmt "(-)"
+ | MLmul -> Format.fprintf fmt "( * )"
+ | MLmagic -> Format.fprintf fmt "Obj.magic"
+ | Coq_primitive (op,None) ->
+ Format.fprintf fmt "no_check_%s" (Primitives.to_string op)
+ | Coq_primitive (op, Some (prefix,kn)) ->
+ Format.fprintf fmt "%s %a" (Primitives.to_string op)
+ pp_mllam (MLglobal (Gconstant (prefix,kn)))
in
Format.fprintf fmt "@[%a@]" pp_mllam l
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index bba011475..13d61841f 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -29,6 +29,7 @@ and lambda =
| Llet of name * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of prefix * constant
+ | Lprim of prefix * constant * Primitives.t * lambda array
| Lcase of annot_sw * lambda * lambda * lam_branches
(* annotations, term being matched, accu, branches *)
| Lif of lambda * lambda * lambda
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f6fb25ab0..631349c07 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -101,6 +101,9 @@ let map_lam_with_binders g f n lam =
let fct' = f n fct in
let args' = Array.smartmap (f n) args in
if fct == fct' && args == args' then lam else mkLapp fct' args'
+ | Lprim(prefix,kn,op,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then lam else Lprim(prefix,kn,op,args')
| Lcase(annot,t,a,br) ->
let t' = f n t in
let a' = f n a in
@@ -297,7 +300,7 @@ let rec occurence k kind lam =
occurence (k+1) (occurence k kind def) body
| Lapp(f, args) ->
occurence_args k (occurence k kind f) args
- | Lmakeblock(_,_,_,args) ->
+ | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
occurence_args k kind args
| Lcase(_,t,a,br) ->
let kind = occurence k (occurence k kind t) a in
@@ -626,6 +629,12 @@ and lambda_of_app env sigma f args =
| Const kn ->
let kn = get_allias !global_env kn in
let cb = lookup_constant kn !global_env in
+ (try
+ let prefix = get_const_prefix !global_env kn in
+ let args = lambda_of_args env sigma 0 args in
+ Retroknowledge.get_native_compiling_info
+ (!global_env).retroknowledge (mkConst kn) prefix args
+ with Not_found ->
begin match cb.const_body with
| Def csubst ->
if cb.const_inline_code then
@@ -641,7 +650,7 @@ and lambda_of_app env sigma f args =
| OpaqueDef _ | Undef _ ->
let prefix = get_const_prefix !global_env kn in
mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
- end
+ end)
| Construct c ->
let tag, nparams, arity = Renv.get_construct_info env c in
let expected = nparams + arity in
@@ -726,3 +735,8 @@ let before_match_int31 fc prefix c t =
| Luint (UintVal i) -> assert false
| Luint (UintDigits (prefix,c,args)) -> assert false
| _ -> Luint (UintDecomp (prefix,c,t))
+
+let compile_prim prim kn fc prefix args =
+ if not fc then raise Not_found
+ else
+ Lprim(prefix, kn, prim, args)
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 8ff0d727c..afebf8087 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -37,3 +37,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
val before_match_int31 : bool -> prefix -> constructor -> lambda -> lambda
+val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array ->
+ lambda
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 7f2785cf9..ab56c4be0 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -222,6 +222,8 @@ let dummy_value : unit -> t =
let cast_accu v = (Obj.magic v:accumulator)
let mk_int (x : int) = (Obj.magic x : t)
+(* Coq's booleans are reversed... *)
+let mk_bool (b : bool) = (Obj.magic (not b) : t)
let mk_uint (x : Uint31.t) = (Obj.magic x : t)
type block
@@ -260,7 +262,223 @@ let is_int (x:t) =
let o = Obj.repr x in
Obj.is_int o
-let to_int (x:t) = (Obj.magic x : int)
+let val_to_int (x:t) = (Obj.magic x : int)
+
+let to_uint (x:t) = (Obj.magic x : Uint31.t)
+let of_uint (x: Uint31.t) = (Obj.magic x : t)
+
+let no_check_head0 x =
+ of_uint (Uint31.head0 (to_uint x))
+
+let head0 accu x =
+ if is_int x then no_check_head0 x
+ else accu x
+
+let no_check_tail0 x =
+ of_uint (Uint31.tail0 (to_uint x))
+
+let tail0 accu x =
+ if is_int x then no_check_tail0 x
+ else accu x
+
+let no_check_add x y =
+ of_uint (Uint31.add (to_uint x) (to_uint y))
+
+let add accu x y =
+ if is_int x && is_int y then no_check_add x y
+ else accu x y
+
+let no_check_sub x y =
+ of_uint (Uint31.sub (to_uint x) (to_uint y))
+
+let sub accu x y =
+ if is_int x && is_int y then no_check_sub x y
+ else accu x y
+
+let no_check_mul x y =
+ of_uint (Uint31.mul (to_uint x) (to_uint y))
+
+let mul accu x y =
+ if is_int x && is_int y then no_check_mul x y
+ else accu x y
+
+let no_check_div x y =
+ of_uint (Uint31.div (to_uint x) (to_uint y))
+
+let div accu x y =
+ if is_int x && is_int y then no_check_div x y
+ else accu x y
+
+let no_check_rem x y =
+ of_uint (Uint31.rem (to_uint x) (to_uint y))
+
+let rem accu x y =
+ if is_int x && is_int y then no_check_rem x y
+ else accu x y
+
+let no_check_l_sr x y =
+ of_uint (Uint31.l_sr (to_uint x) (to_uint y))
+
+let l_sr accu x y =
+ if is_int x && is_int y then no_check_l_sr x y
+ else accu x y
+
+let no_check_l_sl x y =
+ of_uint (Uint31.l_sl (to_uint x) (to_uint y))
+
+let l_sl accu x y =
+ if is_int x && is_int y then no_check_l_sl x y
+ else accu x y
+
+let no_check_l_and x y =
+ of_uint (Uint31.l_and (to_uint x) (to_uint y))
+
+let l_and accu x y =
+ if is_int x && is_int y then no_check_l_and x y
+ else accu x y
+
+let no_check_l_xor x y =
+ of_uint (Uint31.l_xor (to_uint x) (to_uint y))
+
+let l_xor accu x y =
+ if is_int x && is_int y then no_check_l_xor x y
+ else accu x y
+
+let no_check_l_or x y =
+ of_uint (Uint31.l_or (to_uint x) (to_uint y))
+
+let l_or accu x y =
+ if is_int x && is_int y then no_check_l_or x y
+ else accu x y
+
+type coq_carry =
+ | Caccu of t
+ | C0 of t
+ | C1 of t
+
+type coq_pair =
+ | Paccu of t
+ | PPair of t * t
+
+let mkCarry b i =
+ if b then (Obj.magic (C1(of_uint i)):t)
+ else (Obj.magic (C0(of_uint i)):t)
+
+let no_check_addc x y =
+ let s = Uint31.add (to_uint x) (to_uint y) in
+ mkCarry (Uint31.lt s (to_uint x)) s
+
+let addc accu x y =
+ if is_int x && is_int y then no_check_addc x y
+ else accu x y
+
+let no_check_subc x y =
+ let s = Uint31.sub (to_uint x) (to_uint y) in
+ mkCarry (Uint31.lt (to_uint x) (to_uint y)) s
+
+let subc accu x y =
+ if is_int x && is_int y then no_check_subc x y
+ else accu x y
+
+let no_check_addCarryC x y =
+ let s =
+ Uint31.add (Uint31.add (to_uint x) (to_uint y))
+ (Uint31.of_int 1) in
+ mkCarry (Uint31.le s (to_uint x)) s
+
+let addCarryC accu x y =
+ if is_int x && is_int y then no_check_addCarryC x y
+ else accu x y
+
+let no_check_subCarryC x y =
+ let s =
+ Uint31.sub (Uint31.sub (to_uint x) (to_uint y))
+ (Uint31.of_int 1) in
+ mkCarry (Uint31.le (to_uint x) (to_uint y)) s
+
+let subCarryC accu x y =
+ if is_int x && is_int y then no_check_subCarryC x y
+ else accu x y
+
+let of_pair (x, y) =
+ (Obj.magic (PPair(of_uint x, of_uint y)):t)
+
+let no_check_mulc x y =
+ of_pair(Uint31.mulc (to_uint x) (to_uint y))
+
+let mulc accu x y =
+ if is_int x && is_int y then no_check_mulc x y
+ else accu x y
+
+let no_check_diveucl x y =
+ let i1, i2 = to_uint x, to_uint y in
+ of_pair(Uint31.div i1 i2, Uint31.rem i1 i2)
+
+let diveucl accu x y =
+ if is_int x && is_int y then no_check_diveucl x y
+ else accu x y
+
+let no_check_div21 x y z =
+ let i1, i2, i3 = to_uint x, to_uint y, to_uint z in
+ of_pair (Uint31.div21 i1 i2 i3)
+
+let div21 accu x y z =
+ if is_int x && is_int y && is_int z then no_check_div21 x y z
+ else accu x y z
+
+let no_check_addMulDiv x y z =
+ let p, i, j = to_uint x, to_uint y, to_uint z in
+ let p' = Uint31.to_int p in
+ of_uint (Uint31.l_or
+ (Uint31.l_sl i p)
+ (Uint31.l_sr j (Uint31.of_int (31 - p'))))
+
+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
+
+
+type coq_bool =
+ | Baccu of t
+ | Btrue
+ | Bfalse
+
+type coq_cmp =
+ | CmpAccu of t
+ | CmpEq
+ | CmpLt
+ | CmpGt
+
+let no_check_eq x y =
+ mk_bool (Uint31.equal (to_uint x) (to_uint y))
+
+let eq accu x y =
+ if is_int x && is_int y then no_check_eq x y
+ else accu x y
+
+let no_check_lt x y =
+ mk_bool (Uint31.lt (to_uint x) (to_uint y))
+
+let lt accu x y =
+ if is_int x && is_int y then no_check_lt x y
+ else accu x y
+
+let no_check_le x y =
+ mk_bool (Uint31.le (to_uint x) (to_uint y))
+
+let le accu x y =
+ if is_int x && is_int y then no_check_le x y
+ else accu x y
+
+let no_check_compare x y =
+ match Uint31.compare (to_uint x) (to_uint y) with
+ | x when x < 0 -> (Obj.magic CmpLt:t)
+ | 0 -> (Obj.magic CmpEq:t)
+ | _ -> (Obj.magic CmpGt:t)
+
+let compare accu x y =
+ if is_int x && is_int y then no_check_compare x y
+ else accu x y
let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
let bohcnv = Array.init 256 (fun i -> i -
@@ -340,7 +558,7 @@ let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
let decomp_uint c v =
if is_int v then
let r = ref c in
- let v = to_int v in
+ let v = val_to_int v in
for i = 30 downto 0 do
r := (!r) (mk_int ((v lsr i) land 1));
done;
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 821b23168..9b0ce8e82 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -73,7 +73,7 @@ val force_cofix : t -> t
val mk_const : tag -> t
val mk_block : tag -> t array -> t
-
+val mk_bool : bool -> t
val mk_int : int -> t
val mk_uint : Uint31.t -> t
@@ -112,5 +112,74 @@ val is_accu : t -> bool
val str_encode : 'a -> string
val str_decode : string -> 'a
+(** Support for machine integers *)
+
+val val_to_int : t -> int
+val is_int : t -> bool
+
+(* function with check *)
+val head0 : t -> t -> t
+val tail0 : t -> t -> t
+
+val add : t -> t -> t -> t
+val sub : t -> t -> t -> t
+val mul : t -> t -> t -> t
+val div : t -> t -> t -> t
+val rem : t -> t -> t -> t
+
+val l_sr : t -> t -> t -> t
+val l_sl : t -> t -> t -> t
+val l_and : t -> t -> t -> t
+val l_xor : t -> t -> t -> t
+val l_or : t -> t -> t -> t
+
+val addc : t -> t -> t -> t
+val subc : t -> t -> t -> t
+val addCarryC : t -> t -> t -> t
+val subCarryC : t -> t -> t -> t
+
+val mulc : t -> t -> t -> t
+val diveucl : t -> t -> t -> t
+
+val div21 : t -> t -> t -> t -> t
+val addMulDiv : t -> t -> t -> t -> t
+
+val eq : t -> t -> t -> t
+val lt : t -> t -> t -> t
+val le : t -> t -> t -> t
+val compare : t -> t -> t -> t
+
+(* Function without check *)
+val no_check_head0 : t -> t
+val no_check_tail0 : t -> t
+
+val no_check_add : t -> t -> t
+val no_check_sub : t -> t -> t
+val no_check_mul : t -> t -> t
+val no_check_div : t -> t -> t
+val no_check_rem : t -> t -> t
+
+val no_check_l_sr : t -> t -> t
+val no_check_l_sl : t -> t -> t
+val no_check_l_and : t -> t -> t
+val no_check_l_xor : t -> t -> t
+val no_check_l_or : t -> t -> t
+
+val no_check_addc : t -> t -> t
+val no_check_subc : t -> t -> t
+val no_check_addCarryC : t -> t -> t
+val no_check_subCarryC : t -> t -> t
+
+val no_check_mulc : t -> t -> t
+val no_check_diveucl : t -> t -> t
+
+val no_check_div21 : t -> t -> t -> t
+val no_check_addMulDiv : t -> t -> t -> t
+
+val no_check_eq : t -> t -> t
+val no_check_lt : t -> t -> t
+val no_check_le : t -> t -> t
+val no_check_compare : t -> t -> t
+
val mk_I31_accu : t
val decomp_uint : t -> t -> t
diff --git a/kernel/primitives.ml b/kernel/primitives.ml
new file mode 100644
index 000000000..64c486220
--- /dev/null
+++ b/kernel/primitives.ml
@@ -0,0 +1,91 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type t =
+ | Int31head0
+ | Int31tail0
+ | Int31add
+ | Int31sub
+ | Int31mul
+ | Int31div
+ | Int31mod
+(*
+ | Int31lsr
+ | Int31lsl
+ *)
+ | Int31land
+ | Int31lor
+ | Int31lxor
+ | Int31addc
+ | Int31subc
+ | Int31addcarryc
+ | Int31subcarryc
+ | Int31mulc
+ | Int31diveucl
+ | Int31div21
+ | Int31addmuldiv
+ | Int31eq
+ | Int31lt
+ | Int31le
+ | Int31compare
+
+let hash = function
+ | Int31head0 -> 1
+ | Int31tail0 -> 2
+ | Int31add -> 3
+ | Int31sub -> 4
+ | Int31mul -> 5
+ | Int31div -> 6
+ | Int31mod -> 7
+(*
+ | Int31lsr -> 8
+ | Int31lsl -> 9
+ *)
+ | Int31land -> 10
+ | Int31lor -> 11
+ | Int31lxor -> 12
+ | Int31addc -> 13
+ | Int31subc -> 14
+ | Int31addcarryc -> 15
+ | Int31subcarryc -> 16
+ | Int31mulc -> 17
+ | Int31diveucl -> 18
+ | Int31div21 -> 19
+ | Int31addmuldiv -> 20
+ | Int31eq -> 21
+ | Int31lt -> 22
+ | Int31le -> 23
+ | Int31compare -> 24
+
+let to_string = function
+ | Int31head0 -> "head0"
+ | Int31tail0 -> "tail0"
+ | Int31add -> "add"
+ | Int31sub -> "sub"
+ | Int31mul -> "mul"
+ | Int31div -> "div"
+ | Int31mod -> "mod"
+(*
+ | Int31lsr -> "l_sr"
+ | Int31lsl -> "l_sl"
+ *)
+ | Int31land -> "l_and"
+ | Int31lor -> "l_or"
+ | Int31lxor -> "l_xor"
+ | Int31addc -> "addc"
+ | Int31subc -> "subc"
+ | Int31addcarryc -> "addcarryc"
+ | Int31subcarryc -> "subcarryc"
+ | Int31mulc -> "mulc"
+ | Int31diveucl -> "diveucl"
+ | Int31div21 -> "div21"
+ | Int31addmuldiv -> "addmuldiv"
+ | Int31eq -> "eq"
+ | Int31lt -> "lt"
+ | Int31le -> "le"
+ | Int31compare -> "compare"
diff --git a/kernel/primitives.mli b/kernel/primitives.mli
new file mode 100644
index 000000000..1b70a9be8
--- /dev/null
+++ b/kernel/primitives.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type t =
+ | Int31head0
+ | Int31tail0
+ | Int31add
+ | Int31sub
+ | Int31mul
+ | Int31div
+ | Int31mod
+(*
+ | Int31lsr
+ | Int31lsl
+ *)
+ | Int31land
+ | Int31lor
+ | Int31lxor
+ | Int31addc
+ | Int31subc
+ | Int31addcarryc
+ | Int31subcarryc
+ | Int31mulc
+ | Int31diveucl
+ | Int31div21
+ | Int31addmuldiv
+ | Int31eq
+ | Int31lt
+ | Int31le
+ | Int31compare
+
+val hash : t -> int
+
+val to_string : t -> string
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index f4b57d085..466380f2d 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -130,9 +130,8 @@ type reactive_end = {(*information required by the compiler of the VM *)
vm_decompile_const : (int -> Term.constr) option;
native_compiling :
- (bool->Cbytecodes.comp_env->constr array ->
- int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
- option;
+ (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
+ Nativeinstr.lambda) option;
native_constant_static :
(bool -> constr array -> Nativeinstr.lambda) option;
@@ -142,9 +141,8 @@ type reactive_end = {(*information required by the compiler of the VM *)
Nativeinstr.lambda array -> Nativeinstr.lambda) option;
native_before_match : (bool -> Nativeinstr.prefix -> constructor ->
- Nativeinstr.lambda -> Nativeinstr.lambda) option;
+ Nativeinstr.lambda -> Nativeinstr.lambda) option
- native_decompile_const : (int -> Term.constr) option
}
@@ -186,7 +184,6 @@ let empty_reactive_end =
native_constant_static = None;
native_constant_dynamic = None;
native_before_match = None;
- native_decompile_const = None
}
@@ -270,12 +267,6 @@ let get_native_before_match_info knowledge key =
| None -> raise Not_found
| Some f -> f knowledge.flags.fastcomputation
-let get_native_decompile_constant_info knowledge key =
- match (Reactive.find key knowledge.reactive).native_decompile_const
- with
- | None -> raise Not_found
- | Some f -> f
-
(* functions manipulating reactive knowledge *)
let add_vm_compiling_info knowledge value nfo =
{knowledge with reactive =
@@ -376,16 +367,5 @@ let add_native_before_match_info knowledge value nfo =
knowledge.reactive
}
-let add_native_decompile_constant_info knowledge value nfo =
- {knowledge with reactive =
- try
- Reactive.add value
- {(Reactive.find value (knowledge.reactive)) with native_decompile_const = Some nfo}
- knowledge.reactive
- with Not_found ->
- Reactive.add value {empty_reactive_end with native_decompile_const = Some nfo}
- knowledge.reactive
- }
-
let clear_info knowledge value =
{knowledge with reactive = Reactive.remove value knowledge.reactive}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 644fb7074..30d824a9b 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -118,9 +118,8 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
-val get_native_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env ->
- constr array ->
- int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
+val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix ->
+ Nativeinstr.lambda array -> Nativeinstr.lambda
val get_native_constant_static_info : retroknowledge -> entry ->
constr array -> Nativeinstr.lambda
@@ -134,8 +133,6 @@ val get_native_before_match_info : retroknowledge -> entry ->
Nativeinstr.prefix -> constructor ->
Nativeinstr.lambda -> Nativeinstr.lambda
-val get_native_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
-
(** the following functions are solely used in Pre_env and Environ to implement
the functions register and unregister (and mem) of Environ *)
val add_field : retroknowledge -> field -> entry -> retroknowledge
@@ -167,9 +164,9 @@ val add_vm_decompile_constant_info : retroknowledge -> entry ->
(int -> constr) -> retroknowledge
val add_native_compiling_info : retroknowledge-> entry ->
- (bool -> Cbytecodes.comp_env -> constr array -> int ->
- Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
- retroknowledge
+ (bool -> Nativeinstr.prefix ->
+ Nativeinstr.lambda array -> Nativeinstr.lambda) ->
+ retroknowledge
val add_native_constant_static_info : retroknowledge -> entry ->
(bool -> constr array ->
@@ -187,9 +184,6 @@ val add_native_before_match_info : retroknowledge -> entry ->
Nativeinstr.lambda -> Nativeinstr.lambda) ->
retroknowledge
-val add_native_decompile_constant_info : retroknowledge -> entry ->
- (int -> constr) -> retroknowledge
-
val clear_info : retroknowledge-> entry -> retroknowledge
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 11:29:47 +0000