diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 7 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
2 files changed, 9 insertions, 2 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 9eb59319..87c9af39 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -212,3 +212,10 @@ let barrier bk = Barrier bk (Done ()) val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e let footprint _ = Footprint (Done ()) + +(* Define a type synonym that also takes the register state as a type parameter, + in order to make switching to the state monad without changing generated + definitions easier, see also lib/hol/prompt_monad.lem. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 332d5681..36794348 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1455,8 +1455,8 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) ] 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 + string ("type MR 'a 'r = base_monadR register_value regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = base_monad register_value regstate 'a " ^ exc_typ); hardline ] ]); (print defs_file) |