From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Feb 2018 01:02:17 +0100 Subject: Primitive integers This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux Co-authored-by: Benjamin Grégoire Co-authored-by: Vincent Laporte --- kernel/nativecode.ml | 198 ++++++++++++++++++++------------------------------- 1 file changed, 78 insertions(+), 120 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 482a2f3a3c..c32bdb85d6 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -14,7 +14,6 @@ open Constr open Declarations open Util open Nativevalues -open Nativeinstr open Nativelambda open Environ @@ -286,8 +285,6 @@ type primitive = | Mk_int | Mk_bool | Val_to_int - | Mk_I31_accu - | Decomp_uint | Mk_meta | Mk_evar | MLand @@ -305,7 +302,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option + | Coq_primitive of CPrimitives.t * (prefix * pconstant) option let eq_primitive p1 p2 = match p1, p2 with @@ -351,29 +348,27 @@ let primitive_hash = function | 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 (CPrimitives.hash prim) - | Coq_primitive (prim, Some (prefix,kn)) -> - combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) - | Mk_proj -> 38 - | MLarrayget -> 39 - | Mk_empty_instance -> 40 + | Mk_meta -> 19 + | Mk_evar -> 20 + | MLand -> 21 + | MLle -> 22 + | MLlt -> 23 + | MLinteq -> 24 + | MLlsl -> 25 + | MLlsr -> 26 + | MLland -> 27 + | MLlor -> 28 + | MLlxor -> 29 + | MLadd -> 30 + | MLsub -> 31 + | MLmul -> 32 + | MLmagic -> 33 + | Coq_primitive (prim, None) -> combinesmall 34 (CPrimitives.hash prim) + | Coq_primitive (prim, Some (prefix,(kn,_))) -> + combinesmall 35 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) + | Mk_proj -> 36 + | MLarrayget -> 37 + | Mk_empty_instance -> 38 type mllambda = | MLlocal of lname @@ -389,7 +384,7 @@ type mllambda = | MLconstruct of string * constructor * mllambda array (* prefix, constructor name, arguments *) | MLint of int - | MLuint of Uint31.t + | MLuint of Uint63.t | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array @@ -455,7 +450,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLint i1, MLint i2 -> Int.equal i1 i2 | MLuint i1, MLuint i2 -> - Uint31.equal i1 i2 + Uint63.equal i1 i2 | MLsetref (id1, ml1), MLsetref (id2, ml2) -> String.equal id1 id2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 @@ -534,7 +529,7 @@ let rec hash_mllambda gn n env t = | MLint i -> combinesmall 11 i | MLuint i -> - combinesmall 12 (Uint31.to_int i) + combinesmall 12 (Uint63.hash i) | MLsetref (id, ml) -> let hid = String.hash id in let hml = hash_mllambda gn n env ml in @@ -947,9 +942,10 @@ let merge_branches t = Array.iter (fun (c,args,body) -> insert (c,args) body newt) t; Array.of_list (to_list newt) +let app_prim p args = MLapp(MLprimitive p, args) -type prim_aux = - | PAprim of string * Constant.t * CPrimitives.t * prim_aux array +type prim_aux = + | PAprim of string * pconstant * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -962,97 +958,67 @@ let add_check cond args = | _ -> 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 = + 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) + 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 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 = +let cast_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|]) + | MLint _ -> v + | _ -> MLapp(MLprimitive Val_to_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 inlining 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 (CPrimitives.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 (CPrimitives.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 = + let args = Array.map opt_prim_aux args in + app_prim (Coq_primitive(op,None)) args + | 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 + app_prim (Coq_primitive(op, Some (prefix,kn))) (Array.map naive_prim_aux args) + | PAml ml -> ml + in - let compile_cond cond paux = + let compile_cond cond paux = match cond with - | [] -> opt_prim_aux paux + | [] -> opt_prim_aux paux | [c1] -> - MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) + 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 cond = + List.fold_left + (fun ml c -> app_prim MLland [| ml; cast_to_int c|]) + (app_prim MLland [| cast_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) + + (* The optimizations done for checking if integer values are closed are valid + only on 64-bit architectures. So on 32-bit architectures, we fall back to less optimized checks. *) + if max_int = 1073741823 (* 32-bits *) then + add_decl decl (naive_prim_aux paux) + else + add_decl decl (compile_cond cond paux) let ml_of_instance instance u = let ml_of_level l = @@ -1089,6 +1055,11 @@ let ml_of_instance instance u = | Llam(ids,body) -> let lnames,env = push_rels env ids in MLlam(lnames, ml_of_lam env l body) + | Lrec(id,body) -> + let ids,body = decompose_Llam body in + let lname, env = push_rel env id in + let lnames, env = push_rels env ids in + MLletrec([|lname, lnames, ml_of_lam env l body|], MLlocal lname) | Llet(id,def,body) -> let def = ml_of_lam env l def in let lname, env = push_rel env id in @@ -1101,8 +1072,8 @@ let ml_of_instance instance u = mkMLapp (MLglobal(Gconstant (prefix, c))) args | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> - let decl,cond,paux = extract_prim (ml_of_lam env l) t in - compile_prim decl cond paux + 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 = @@ -1311,18 +1282,7 @@ let ml_of_instance instance u = | Lconstruct (prefix, (cn,u)) -> let uargs = ml_of_instance env.env_univ u in mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs - | Luint v -> - (match v with - | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) - | UintDigits (prefix,cn,ds) -> - let c = MLglobal (Gconstruct (prefix, cn)) in - let ds = Array.map (ml_of_lam env l) ds in - let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in - MLapp(i31, ds) - | UintDecomp (prefix,cn,t) -> - let c = MLglobal (Gconstruct (prefix, cn)) in - let t = ml_of_lam env l t in - MLapp (MLprimitive Decomp_uint, [|c;t|])) + | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> @@ -1646,7 +1606,7 @@ let pp_mllam fmt l = Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" (string_of_construct prefix c) pp_cargs args | MLint i -> pp_int fmt i - | MLuint i -> Format.fprintf fmt "(Uint31.of_int %a)" pp_int (Uint31.to_int i) + | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i) | MLsetref (s, body) -> Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body | MLsequence(l1,l2) -> @@ -1766,8 +1726,6 @@ let pp_mllam fmt l = | 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 "(&&)" @@ -1787,9 +1745,9 @@ let pp_mllam fmt l = | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) - | Coq_primitive (op, Some (prefix,kn)) -> + | Coq_primitive (op, Some (prefix,(c,_))) -> Format.fprintf fmt "%s %a" (CPrimitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix, kn))) + pp_mllam (MLglobal (Gconstant (prefix,c))) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -1903,7 +1861,7 @@ let compile_constant env sigma prefix ~interactive con cb = let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); - let is_lazy = is_lazy env prefix t in + let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix -- cgit v1.2.3