diff options
| author | Thomas Bauereiss | 2018-02-23 19:38:40 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-26 13:30:21 +0000 |
| commit | 30ba876d4c465d9a6cf2eba4eb1ac4c3dbc7ed22 (patch) | |
| tree | f08e199bb2cc932928296ba2fcdb5bd50d1f7d75 /src/process_file.ml | |
| parent | f100cf44857926030361ef66cff795169c29fdbc (diff) | |
Add/generate Isabelle lemmas about the monad lifting
Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle. In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 80cfdccb..a447061b 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,6 +48,9 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open PPrint +open Pretty_print_common + let opt_lem_sequential = ref false let opt_lem_mwords = ref false @@ -243,7 +246,22 @@ let output_lem filename libs defs = "Sail_values"; operators_module ] @ monad_modules - in + in + let isa_thy_name = String.capitalize filename ^ "_lemmas" in + let isa_lemmas = + separate hardline [ + string ("theory " ^ isa_thy_name); + string " imports"; + string " Sail.Sail_values_extras"; + string " Sail.State_extras"; + string (" " ^ String.capitalize filename); + string "begin"; + string ""; + State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs; + string ""; + string "end" + ] ^^ hardline + in let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in let ((o,_, _) as ext_o) = @@ -253,7 +271,11 @@ let output_lem filename libs defs = (o, base_imports @ (String.capitalize types_module :: libs)) defs generated_line); close_output_with_check ext_ot; - close_output_with_check ext_o + close_output_with_check ext_o; + let ((ol, _, _) as ext_ol) = + open_output_with_check_unformatted (isa_thy_name ^ ".thy") in + print ol isa_lemmas; + close_output_with_check ext_ol let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () |