diff options
| author | Thomas Bauereiss | 2018-02-14 19:45:07 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-15 20:11:21 +0000 |
| commit | 737ec26cf494affb346504c482e9b91127b68636 (patch) | |
| tree | 30bcac2487eb2294952624aa25321a0299c6e2e7 /src/pretty_print_lem.ml | |
| parent | 9883998c6de1a0421eacb4f4c352b0aa8c4a1b5c (diff) | |
Rebase state monad onto prompt monad
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 88ad8065..730cf4a8 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1423,12 +1423,12 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) separate empty (List.map doc_def_lem statedefs); hardline; hardline; register_refs; hardline; - if !opt_sequential then + (* if !opt_sequential then concat [ string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline; string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline; ] - else + else *) concat [ string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline; string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline |