From 07335670c4339f9c4ae620088d9352be67a77714 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 17:42:09 +0200 Subject: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml. Indeed OCaml has a similar file and this conflicts, at least in debugger. --- API/API.ml | 2 +- kernel/cPrimitives.ml | 91 +++++++++++++++++++++++++++++++++++++++++++++++++ kernel/cPrimitives.mli | 39 +++++++++++++++++++++ kernel/environ.ml | 34 +++++++++--------- kernel/kernel.mllib | 2 +- kernel/nativecode.ml | 16 ++++----- kernel/nativeinstr.mli | 2 +- kernel/nativelambda.mli | 2 +- kernel/primitives.ml | 91 ------------------------------------------------- kernel/primitives.mli | 39 --------------------- 10 files changed, 159 insertions(+), 159 deletions(-) create mode 100644 kernel/cPrimitives.ml create mode 100644 kernel/cPrimitives.mli delete mode 100644 kernel/primitives.ml delete mode 100644 kernel/primitives.mli diff --git a/API/API.ml b/API/API.ml index c952e123d..1d7a4a4f4 100644 --- a/API/API.ml +++ b/API/API.ml @@ -43,7 +43,7 @@ module Cbytecodes = Cbytecodes (* module Copcodes *) module Cemitcodes = Cemitcodes (* module Nativevalues *) -(* module Primitives *) +(* module CPrimitives *) module Opaqueproof = Opaqueproof module Declareops = Declareops module Retroknowledge = Retroknowledge diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml new file mode 100644 index 000000000..14c11bf10 --- /dev/null +++ b/kernel/cPrimitives.ml @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/cPrimitives.mli b/kernel/cPrimitives.mli new file mode 100644 index 000000000..8cdffb670 --- /dev/null +++ b/kernel/cPrimitives.mli @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* int + +val to_string : t -> string diff --git a/kernel/environ.ml b/kernel/environ.ml index d2c737ab0..621a9931d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -624,39 +624,39 @@ fun rk value field -> native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - Primitives.Int31add + CPrimitives.Int31add | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - Primitives.Int31addc + CPrimitives.Int31addc | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - Primitives.Int31addcarryc + CPrimitives.Int31addcarryc | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - Primitives.Int31sub + CPrimitives.Int31sub | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - Primitives.Int31subc + CPrimitives.Int31subc | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - Primitives.Int31mul + CPrimitives.Int31mul | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - Primitives.Int31mulc + CPrimitives.Int31mulc | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - Primitives.Int31div21 + CPrimitives.Int31div21 | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - Primitives.Int31diveucl + CPrimitives.Int31diveucl | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - Primitives.Int31addmuldiv + CPrimitives.Int31addmuldiv | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - Primitives.Int31compare + CPrimitives.Int31compare | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - Primitives.Int31head0 + CPrimitives.Int31head0 | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - Primitives.Int31tail0 + CPrimitives.Int31tail0 | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - Primitives.Int31lor + CPrimitives.Int31lor | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - Primitives.Int31land + CPrimitives.Int31land | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - Primitives.Int31lxor + CPrimitives.Int31lxor | _ -> empty_reactive_info let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 994634854..917e4f6f1 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -17,7 +17,7 @@ Opaqueproof Declarations Entries Nativevalues -Primitives +CPrimitives Declareops Retroknowledge Conv_oracle diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index da7fcd6f2..e08d913bc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -296,7 +296,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of Primitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * constant) option let eq_primitive p1 p2 = match p1, p2 with @@ -361,9 +361,9 @@ let primitive_hash = function | MLsub -> 33 | MLmul -> 34 | MLmagic -> 35 - | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim) + | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim) | Coq_primitive (prim, Some (prefix,kn)) -> - combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim)) + combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) | Mk_proj -> 38 | MLarrayget -> 39 | Mk_empty_instance -> 40 @@ -921,7 +921,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * Primitives.t * prim_aux array + | PAprim of string * constant * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -988,11 +988,11 @@ let compile_prim decl cond paux = | 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 + 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 (Primitives.Int31le, None)) 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)) @@ -1752,9 +1752,9 @@ let pp_mllam fmt l = | MLarrayget -> Format.fprintf fmt "Array.get" | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> - Format.fprintf fmt "no_check_%s" (Primitives.to_string op) + Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) | Coq_primitive (op, Some (prefix,kn)) -> - Format.fprintf fmt "%s %a" (Primitives.to_string op) + Format.fprintf fmt "%s %a" (CPrimitives.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 cb79877e8..2353470f0 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -30,7 +30,7 @@ and lambda = | Lapp of lambda * lambda array | Lconst of prefix * pconstant | Lproj of prefix * constant (* prefix, projection name *) - | Lprim of prefix * constant * Primitives.t * lambda array + | Lprim of prefix * constant * CPrimitives.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.mli b/kernel/nativelambda.mli index bfa3bf941..156e4f834 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> lambda -val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array -> +val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array -> lambda diff --git a/kernel/primitives.ml b/kernel/primitives.ml deleted file mode 100644 index 14c11bf10..000000000 --- a/kernel/primitives.ml +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 deleted file mode 100644 index 8cdffb670..000000000 --- a/kernel/primitives.mli +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int - -val to_string : t -> string -- cgit v1.2.3