diff options
| -rw-r--r-- | lib/isabelle/Hoare.thy | 2 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 36 | ||||
| -rw-r--r-- | lib/isabelle/ROOT | 11 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy (renamed from lib/isabelle/Sail_operators_mwords_lemmas.thy) | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy (renamed from lib/isabelle/Prompt_monad_lemmas.thy) | 6 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy (renamed from lib/isabelle/State_lemmas.thy) | 28 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy (renamed from lib/isabelle/State_monad_lemmas.thy) | 6 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_values_lemmas.thy (renamed from lib/isabelle/Sail_values_lemmas.thy) | 12 | ||||
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 18 | ||||
| -rw-r--r-- | src/gen_lib/sail2_prompt.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail2_string.lem | 14 |
11 files changed, 81 insertions, 58 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 9271e2fa..5c77c5e7 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -1,6 +1,6 @@ theory Hoare imports - State_lemmas + Sail2_state_lemmas "HOL-Eisbach.Eisbach_Tools" begin diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index b10dde78..56591140 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,8 +1,11 @@ -THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ - Sail_operators_mwords.thy Sail_operators_bitlists.thy \ - State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy -EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ - Sail_operators_mwords_lemmas.thy Hoare.thy +THYS = Sail2_instr_kinds.thy Sail2_values.thy Sail2_operators.thy \ + Sail2_operators_mwords.thy Sail2_operators_bitlists.thy \ + Sail2_state_monad.thy Sail2_state.thy Sail2_state_lifting.thy \ + Sail2_prompt_monad.thy Sail2_prompt.thy \ + Sail2_string.thy +EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ + Sail2_prompt_monad_lemmas.thy \ + Sail2_operators_mwords_lemmas.thy Hoare.thy RISCV_DIR = ../../riscv @@ -24,34 +27,37 @@ manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex make -C $(RISCV_DIR) Riscv_duopod.thy isabelle build -d manual Sail-Manual -Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem +Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy +Sail2_values.thy: ../../src/gen_lib/sail2_values.lem Sail2_instr_kinds.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy +Sail2_operators.thy: ../../src/gen_lib/sail2_operators.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_operators.thy Prompt.thy +Sail2_operators_mwords.thy: ../../src/gen_lib/sail2_operators_mwords.lem Sail2_operators.thy Sail2_prompt.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy Prompt.thy +Sail2_operators_bitlists.thy: ../../src/gen_lib/sail2_operators_bitlists.lem Sail2_operators.thy Sail2_prompt.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy +Sail2_prompt_monad.thy: ../../src/gen_lib/sail2_prompt_monad.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_lemmas.thy +Sail2_prompt.thy: ../../src/gen_lib/sail2_prompt.lem Sail2_prompt_monad.thy Sail2_prompt_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy +Sail2_state_monad.thy: ../../src/gen_lib/sail2_state_monad.lem Sail2_values.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy +Sail2_state.thy: ../../src/gen_lib/sail2_state.lem Sail2_prompt.thy Sail2_state_monad.thy Sail2_state_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy +Sail2_state_lifting.thy: ../../src/gen_lib/sail2_state_lifting.lem Sail2_prompt.thy Sail2_state.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + +Sail2_string.thy: ../../src/gen_lib/sail2_string.lem Sail2_operators_mwords.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index 1f3ba3ff..545e47c4 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -3,10 +3,11 @@ session "Sail" = "LEM" + sessions "HOL-Eisbach" theories [document = false] - Sail_values_lemmas - Prompt - State_lemmas - Sail_operators_mwords_lemmas - Sail_operators_bitlists + Sail2_values_lemmas + Sail2_prompt + Sail2_state_lemmas + Sail2_operators_mwords_lemmas + Sail2_operators_bitlists + Sail2_string Hoare document_files "root.tex" diff --git a/lib/isabelle/Sail_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index 22c35e1f..ae8802f2 100644 --- a/lib/isabelle/Sail_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -1,5 +1,5 @@ -theory "Sail_operators_mwords_lemmas" - imports Sail_operators_mwords +theory Sail2_operators_mwords_lemmas + imports Sail2_operators_mwords begin lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 7a3a108d..08c9b33c 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -1,7 +1,7 @@ -theory Prompt_monad_lemmas +theory Sail2_prompt_monad_lemmas imports - Prompt_monad - Sail_values_lemmas + Sail2_prompt_monad + Sail2_values_lemmas begin notation bind (infixr "\<bind>" 54) diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index cf5e4dbf..124722ab 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -1,5 +1,5 @@ -theory State_lemmas - imports State State_lifting +theory Sail2_state_lemmas + imports Sail2_state Sail2_state_lifting begin lemma All_liftState_dom: "liftState_dom (r, m)" @@ -220,41 +220,57 @@ qed lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto lemma and_boolM_simps[simp]: - "and_boolM (return b) y = (if b then y else return False)" + "and_boolM (return b) (return c) = return (b \<and> c)" "and_boolM x (return True) = x" "and_boolM x (return False) = x \<bind> (\<lambda>_. return False)" "\<And>x y z. and_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. and_boolM (y r) z))" by (auto simp: and_boolM_def) +lemma and_boolM_return_if: + "and_boolM (return b) y = (if b then y else return False)" + by (auto simp: and_boolM_def) + lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y] lemma or_boolM_simps[simp]: - "or_boolM (return b) y = (if b then return True else y)" + "or_boolM (return b) (return c) = return (b \<or> c)" "or_boolM x (return True) = x \<bind> (\<lambda>_. return True)" "or_boolM x (return False) = x" "\<And>x y z. or_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. or_boolM (y r) z))" by (auto simp: or_boolM_def) +lemma or_boolM_return_if: + "or_boolM (return b) y = (if b then return True else y)" + by (auto simp: or_boolM_def) + lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y] lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto lemma and_boolS_simps[simp]: - "and_boolS (returnS b) y = (if b then y else returnS False)" + "and_boolS (returnS b) (returnS c) = returnS (b \<and> c)" "and_boolS x (returnS True) = x" "and_boolS x (returnS False) = bindS x (\<lambda>_. returnS False)" "\<And>x y z. and_boolS (bindS x y) z = (bindS x (\<lambda>r. and_boolS (y r) z))" by (auto simp: and_boolS_def) +lemma and_boolS_returnS_if: + "and_boolS (returnS b) y = (if b then y else returnS False)" + by (auto simp: and_boolS_def) + lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] lemma or_boolS_simps[simp]: - "or_boolS (returnS b) y = (if b then returnS True else y)" + "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)" "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)" "or_boolS x (returnS False) = x" "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))" by (auto simp: or_boolS_def) +lemma or_boolS_returnS_if: + "or_boolS (returnS b) y = (if b then returnS True else y)" + by (auto simp: or_boolS_def) + lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] end diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index e0d684ba..b705de4c 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -1,7 +1,7 @@ -theory State_monad_lemmas +theory Sail2_state_monad_lemmas imports - State_monad - Sail_values_lemmas + Sail2_state_monad + Sail2_values_lemmas begin (*context diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index dd008695..b50d8942 100644 --- a/lib/isabelle/Sail_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -1,5 +1,5 @@ -theory Sail_values_lemmas - imports Sail_values +theory Sail2_values_lemmas + imports Sail2_values begin lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) @@ -57,10 +57,10 @@ lemma bool_of_bitU_bitU_of_bool[simp]: "bool_of_bitU (bitU_of_bool x) = Some x" by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+ -abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict instance_Sail_values_BitU_Sail_values_bitU_dict" -lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def -abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict" -lemmas BC_mword_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_def +abbreviation "BC_bitU_list \<equiv> instance_Sail2_values_Bitvector_list_dict instance_Sail2_values_BitU_Sail2_values_bitU_dict" +lemmas BC_bitU_list_def = instance_Sail2_values_Bitvector_list_dict_def instance_Sail2_values_BitU_Sail2_values_bitU_dict_def +abbreviation "BC_mword \<equiv> instance_Sail2_values_Bitvector_Machine_word_mword_dict" +lemmas BC_mword_defs = instance_Sail2_values_Bitvector_Machine_word_mword_dict_def access_mword_def access_mword_inc_def access_mword_dec_def (*update_mword_def update_mword_inc_def update_mword_dec_def*) subrange_list_def subrange_list_inc_def subrange_list_dec_def diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 0c83ebea..6cd90a9a 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -1,8 +1,8 @@ (*<*) theory Manual imports - Sail.State_lemmas - Sail.Sail_operators_mwords_lemmas + Sail.Sail2_state_lemmas + Sail.Sail2_operators_mwords_lemmas Sail.Hoare Riscv_duopod.Riscv_duopod_lemmas begin @@ -183,7 +183,7 @@ Vectors in Sail are mapped to lists in Isabelle, except for bitvectors, which ar Both increasing and decreasing indexing order are supported by having two versions for each operation that involves indexing, such as @{term update_list_inc} and @{term update_list_dec}, or @{term subrange_list_inc} and @{term subrange_list_dec}. These operations are defined in the -theory @{theory Sail_values}, while @{theory Sail_values_lemmas} provides simplification rules +theory @{theory Sail2_values}, while @{theory Sail2_values_lemmas} provides simplification rules such as @{lemma "access_list_inc xs i = xs ! nat i" by auto} \\ @@ -209,7 +209,7 @@ into multiple clauses with concrete bitvector lengths. This is not enabled by d so Sail generates Lem definitions using bit lists unless the @{verbatim "-lem_mwords"} command line flag is used. -The theory @{theory Sail_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides +The theory @{theory Sail2_values} defines a (Lem) typeclass @{verbatim Bitvector}, which provides an interface to some basic bitvector operations and has instantiations for both bit lists and machine words. It is mainly intended for internal use in the Sail library,\<^footnote>\<open>Lem typeclasses are not very convenient to use in Isabelle, as they get translated to dictionaries that have to be passed to functions @@ -219,7 +219,7 @@ representations. For use in Sail specifications, wrappers are defined in the th right theory is automatically added to the generated files, depending on which bitvector representation is used. Hence, bitvector operations can be referred to in the Sail source code using uniform names, e.g.~@{term add_vec}, @{term update_vec_dec}, or @{term subrange_vec_inc}. -The theory @{theory Sail_operators_mwords_lemmas} sets up simplification rules that relate these +The theory @{theory Sail2_operators_mwords_lemmas} sets up simplification rules that relate these operations to the native operations in Isabelle, e.g. @{lemma "add_vec l r = l + r" by simp} \\ @@ -235,8 +235,8 @@ for integration with relaxed memory models. For the sequential case, we use a s exceptions and nondeterminism). The generated definitions use the free monad, and the sequential case is supported via a lifting -to the state monad defined in the theory @{theory State}. Simplification rules are set up in the -theory @{theory State_lemmas}, allowing seamless reasoning about the generated definitions in terms +to the state monad defined in the theory @{theory Sail2_state}. Simplification rules are set up in the +theory @{theory Sail2_state_lemmas}, allowing seamless reasoning about the generated definitions in terms of the state monad.\<close> subsubsection \<open>State Monad \label{sec:state-monad}\<close> @@ -308,7 +308,7 @@ instances.\<close> subsubsection \<open>Free Monad \label{sec:free-monad}\<close> -text \<open>In addition to the state monad, the theory @{theory Prompt_monad} defines a free monad of an +text \<open>In addition to the state monad, the theory @{theory Sail2_prompt_monad} defines a free monad of an effect datatype. A monadic expression either returns a pure value @{term a}, denoted @{term "Done a"}, or it has an effect. The latter can be a failure or an exception, or an effect together with a continuation. For example, @{term \<open>Read_reg ''PC'' k\<close>} represents a request to @@ -383,7 +383,7 @@ register state record: Sail aims to generate Isabelle definitions that can be used with either the state or the free monad. To achieve this, the definitions are generated using the free monad, and a lifting to the state monad is provided together with simplification rules. These include generic simplification rules -(proved in the theory @{theory State_lemmas}) such as +(proved in the theory @{theory Sail2_state_lemmas}) such as @{thm [display] liftState_return[where r = "(get_regval, set_regval)"] liftState_bind[where r = "(get_regval, set_regval)"] diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem index 434df843..08a47052 100644 --- a/src/gen_lib/sail2_prompt.lem +++ b/src/gen_lib/sail2_prompt.lem @@ -2,7 +2,7 @@ open import Pervasives_extra (*open import Sail_impl_base*) open import Sail2_values open import Sail2_prompt_monad -open import {isabelle} `Prompt_monad_lemmas` +open import {isabelle} `Sail2_prompt_monad_lemmas` val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e declare isabelle target_rep function (>>=) = infix `\<bind>` diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem index a54ffa65..3374d800 100644 --- a/src/gen_lib/sail2_string.lem +++ b/src/gen_lib/sail2_string.lem @@ -30,10 +30,8 @@ let string_append = stringAppend ***********************************************) val maybeIntegerOfString : string -> maybe integer - +let maybeIntegerOfString _ = Nothing (* TODO FIXME *) declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Some (Nat_big_num.of_int i))` -declare isabelle target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) -declare hol target_rep function maybeIntegerOfString = `maybeIntegerOfString` (* TODO FIXME *) (*********************************************** * end stuff that should be in Lem Num_extra * @@ -65,10 +63,12 @@ let rec n_leading_spaces s = (* match len with * (\* | 0 -> 0 *\) * (\* | 1 -> *\) - * | len -> *) match nth s 0 with - | #' ' -> 1 + (n_leading_spaces (string_sub s 1 (len - 1))) - | _ -> 0 - end + * | len -> *) + (* Isabelle generation for pattern matching on characters + is currently broken, so use an if-expression *) + if nth s 0 = #' ' + then 1 + (n_leading_spaces (string_sub s 1 (len - 1))) + else 0 (* end *) let opt_spc_matches_prefix s = |