diff options
| author | Thomas Bauereiss | 2018-05-11 12:12:16 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-11 12:12:16 +0100 |
| commit | 968cd36942d7b80023618a13fb8e1f93db0cdd61 (patch) | |
| tree | b1aed696b8954e1f61c12d94298c308f46dba2af /src | |
| parent | ff18bac6654a73cedf32a45ee406fe3e74ae3efd (diff) | |
Add Boolean short-circuiting to state monad
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/state.lem | 6 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 5 |
2 files changed, 9 insertions, 2 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 6bc304a8..f69f59c1 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -28,6 +28,12 @@ end declare {isabelle} termination_argument foreachS = automatic +val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let and_boolS l r = l >>$= (fun l -> if l then r else returnS false) + +val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let or_boolS l r = l >>$= (fun l -> if l then returnS true else r) + val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e let bool_of_bitU_fail = function | B0 -> returnS false diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c3e96d57..332d5681 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -629,7 +629,8 @@ let doc_exp_lem, doc_let_lem = | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> - let call = doc_id_lem (append_id f "M") in + let suffix = if !opt_sequential then "S" else "M" in + let call = doc_id_lem (append_id f suffix) in wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "foreach", _) -> @@ -869,7 +870,7 @@ let doc_exp_lem, doc_let_lem = (string "end"))) | E_try (e, pexps) -> if effectful (effect_of e) then - let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in + let try_catch = if ctxt.early_ret then appendS "try_catchR" else "try_catch" in wrap_parens (group ((separate space [string try_catch; expY e; string "(function "]) ^/^ (separate_map (break 1) (doc_case ctxt) pexps) ^/^ |