From 968cd36942d7b80023618a13fb8e1f93db0cdd61 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 11 May 2018 12:12:16 +0100
Subject: Add Boolean short-circuiting to state monad

---
 src/gen_lib/state.lem   | 6 ++++++
 src/pretty_print_lem.ml | 5 +++--
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'src')

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) ^/^
-- 
cgit v1.2.3