diff options
| author | Jon French | 2018-06-11 15:25:02 +0100 |
|---|---|---|
| committer | Jon French | 2018-06-11 15:25:02 +0100 |
| commit | 826e94548a86a88d8fefeb1edef177c02bf5d68d (patch) | |
| tree | fc9a5484440e030cc479101c5cab345c1c77468e /src/state.ml | |
| parent | 5717bb3d0cef5932cb2b33bc66b3b2f0c0552164 (diff) | |
| parent | 4336409f923c10a8c5e4acc91fa7e6ef5551a88f (diff) | |
Merge branch 'sail2' into mappings
(involved some manual tinkering with gitignore, type_check, riscv)
Diffstat (limited to 'src/state.ml')
| -rw-r--r-- | src/state.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/state.ml b/src/state.ml index ab63747c..c591f753 100644 --- a/src/state.ml +++ b/src/state.ml @@ -366,11 +366,11 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id = remove_leading_underscores (string_of_id id) in let id' = remove_trailing_underscores id in separate_map hardline string [ - "lemma liftS_read_reg_" ^ id ^ "[simp]:"; + "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\""; " by (auto simp: liftState_read_reg_readS register_defs)"; ""; - "lemma liftS_write_reg_" ^ id ^ "[simp]:"; + "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; " by (auto simp: liftState_write_reg_updateS register_defs)" ] @@ -510,5 +510,5 @@ let generate_regstate_defs mwords defs = defs let add_regstate_defs mwords env (Defs defs) = - let reg_defs, env = check env (generate_regstate_defs mwords defs) in + let reg_defs, env = Type_error.check env (generate_regstate_defs mwords defs) in env, append_ast (Defs defs) reg_defs |