Tune Lem pretty-printing

In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 8cef266e..8214bf49 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -4,6 +4,14 @@ open import Sail_values
 open import Prompt_monad
 open import {isabelle} `Prompt_monad_lemmas`
 
+val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
+declare isabelle target_rep function (>>=) = infix `\<bind>`
+let inline ~{isabelle} (>>=) = bind
+
+val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
+declare isabelle target_rep function (>>) = infix `\<then>`
+let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n
+
 val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let rec iter_aux i f xs = match xs with
   | x :: xs -> f i x >> iter_aux (i + 1) f xs