From 19b0f79b555223a6a3980413f1aa403e8b92a303 Mon Sep 17 00:00:00 2001 From: Stefan Berghofer Date: Mon, 10 Apr 2017 18:05:54 +0200 Subject: [PATCH] Added support for generic number literals to Isabelle printer --- drivers/isabelle-common.gen | 1 - lib/isabelle/Why3_BV.thy.2016 | 48 +++++---------------------------- lib/isabelle/Why3_BV.thy.2016-1 | 48 +++++---------------------------- src/printer/isabelle.ml | 10 ++++--- 4 files changed, 19 insertions(+), 88 deletions(-) diff --git a/drivers/isabelle-common.gen b/drivers/isabelle-common.gen index 2860cbed9..17a1c82ae 100644 --- a/drivers/isabelle-common.gen +++ b/drivers/isabelle-common.gen @@ -6,7 +6,6 @@ valid "Finished Why3 theory" fail "\\*\\*\\* \\(.*\\)$" "\\1" time "why3cpulimit time : %s s" -transformation "eliminate_literal" transformation "eliminate_epsilon" transformation "eliminate_if_fmla" transformation "eliminate_let_fmla" diff --git a/lib/isabelle/Why3_BV.thy.2016 b/lib/isabelle/Why3_BV.thy.2016 index 26cc0fad9..cfacc11c5 100644 --- a/lib/isabelle/Why3_BV.thy.2016 +++ b/lib/isabelle/Why3_BV.thy.2016 @@ -365,8 +365,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -563,8 +561,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -761,8 +757,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -959,8 +953,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -1039,27 +1031,14 @@ why3_vc eq_sub_bv_def why3_end -definition rliteral_8 :: "'a::len0 word" where - "rliteral_8 = 2 ^ 8 - 1" - -definition rliteral_16 :: "'a::len0 word" where - "rliteral_16 = 2 ^ 16 - 1" - -definition rliteral_32 :: "'a::len0 word" where - "rliteral_32 = 2 ^ 32 - 1" - - why3_open "bv/BVConverter_32_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_32 - -why3_vc rliteral_axiom by (simp add: rliteral_32_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_32_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1071,13 +1050,10 @@ why3_open "bv/BVConverter_16_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_16 - -why3_vc rliteral_axiom by (simp add: rliteral_16_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1089,13 +1065,10 @@ why3_open "bv/BVConverter_8_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1107,13 +1080,10 @@ why3_open "bv/BVConverter_16_32.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_16 - -why3_vc rliteral_axiom by (simp add: rliteral_16_def) why3_vc toSmall_to_uint using assms - by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def) + by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1125,13 +1095,10 @@ why3_open "bv/BVConverter_8_32.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1143,13 +1110,10 @@ why3_open "bv/BVConverter_8_16.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) diff --git a/lib/isabelle/Why3_BV.thy.2016-1 b/lib/isabelle/Why3_BV.thy.2016-1 index d75bd54b1..6cc52d41b 100644 --- a/lib/isabelle/Why3_BV.thy.2016-1 +++ b/lib/isabelle/Why3_BV.thy.2016-1 @@ -365,8 +365,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -563,8 +561,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -761,8 +757,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -959,8 +953,6 @@ why3_vc Nth_bv_is_nth2 using assms by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def) -why3_vc tqtaxiom using to_uint_bounds [of i] by auto - why3_vc to_uint_size_bv by (simp add: size_bv_def) why3_vc to_uint_zeros by simp @@ -1039,27 +1031,14 @@ why3_vc eq_sub_bv_def why3_end -definition rliteral_8 :: "'a::len0 word" where - "rliteral_8 = 2 ^ 8 - 1" - -definition rliteral_16 :: "'a::len0 word" where - "rliteral_16 = 2 ^ 16 - 1" - -definition rliteral_32 :: "'a::len0 word" where - "rliteral_32 = 2 ^ 32 - 1" - - why3_open "bv/BVConverter_32_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_32 - -why3_vc rliteral_axiom by (simp add: rliteral_32_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_32_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1071,13 +1050,10 @@ why3_open "bv/BVConverter_16_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_16 - -why3_vc rliteral_axiom by (simp add: rliteral_16_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1089,13 +1065,10 @@ why3_open "bv/BVConverter_8_64.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1107,13 +1080,10 @@ why3_open "bv/BVConverter_16_32.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_16 - -why3_vc rliteral_axiom by (simp add: rliteral_16_def) why3_vc toSmall_to_uint using assms - by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def) + by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1125,13 +1095,10 @@ why3_open "bv/BVConverter_8_32.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) @@ -1143,13 +1110,10 @@ why3_open "bv/BVConverter_8_16.xml" constants toBig = ucast toSmall = ucast - rliteral = rliteral_8 - -why3_vc rliteral_axiom by (simp add: rliteral_8_def) why3_vc toSmall_to_uint using assms - by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def) + by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial) why3_vc toBig_to_uint by (simp add: uint_up_ucast is_up) diff --git a/src/printer/isabelle.ml b/src/printer/isabelle.ml index 1c441da12..cece2bc48 100644 --- a/src/printer/isabelle.ml +++ b/src/printer/isabelle.ml @@ -200,8 +200,7 @@ let rec print_term info defs fmt t = match t.t_node with let number_format = { Number.long_int_support = true; Number.extra_leading_zeros_support = true; - Number.dec_int_support = Number.Number_custom - ""; + Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; Number.bin_int_support = Number.Number_unsupported; @@ -223,7 +222,12 @@ let rec print_term info defs fmt t = match t.t_node with ")); Number.def_real_support = Number.Number_unsupported; } in - Number.print number_format fmt c + begin match c with + | Number.ConstInt _ -> + fprintf fmt "%a" + (Number.print number_format) c (print_ty info) (t_type t) + | _ -> Number.print number_format fmt c + end | Tif (f, t1, t2) -> print_app print_const (print_term info defs) fmt ("HOL.If", [f; t1; t2]) | Tlet (t1, tb) -> -- GitLab