Mem

LeanBoogie/Boog.lean

@@ -1,6 +1,8 @@
 import Std
 import Aesop
 
+namespace Boogie
+
 open Std (HashSet HashMap)
 
 /-

LeanBoogie/BoogieDsl.lean

@@ -3,7 +3,7 @@ import Std
 import Qq
 import LeanBoogie.Boog
 
-namespace Boog
+namespace Boogie
 open Lean Elab Meta Qq
 open Std (HashSet HashMap)
 

LeanBoogie/ITree/Mem.lean

@@ -0,0 +1,21 @@
+import LeanBoogie.ITree.ITree
+import LeanBoogie.ITree.Eutt
+import LeanBoogie.ITree.Monad
+
+/-
+  # Memory effects
+-/
+
+example : Ans = Int := rfl -- currently our ITrees have the answer type hardcoded as Int.
+
+/-- Memory events: Reading or writing of a variable. -/
+inductive MemEv
+| read  : String        -> MemEv
+| write : String -> Int -> MemEv
+
+abbrev Mem : Type -> Type := ITree MemEv
+
+def Mem.set (a : String) (b : Int) : Mem Unit := .vis (.write a b) (fun _unit => .ret ())
+def Mem.get (v : String)           : Mem Int  := .vis (.read v) (fun ans => .ret ans)
+
+-- TODO: interpreting memory events away into the boogie state monad.

LeanBoogie/ITree/Monad.lean

@@ -1,6 +1,10 @@
 import LeanBoogie.ITree.ITree
 import LeanBoogie.ITree.Eutt
 
+/-
+  # `ITree` forms a monad
+-/
+
 def ITree.pure (a : A) : ITree E A := .ret a
 
 def ITree.bind (ta : ITree E A) (tb : A -> ITree E B) : ITree E B :=
@@ -15,3 +19,15 @@ instance : Monad (ITree E) where
   bind := ITree.bind
 
 #check LawfulMonad
+
+/- ## Helpers for writing imperative programs -/
+
+def ITree.skip : ITree E Unit := .ret ()
+def ITree.seq (a b : ITree E Unit) : ITree E Unit := bind a (fun () => b)
+def ITree.trigger (e : E) : ITree E Int := .vis e (fun ans => .ret ans)
+
+def ITree.ite (c : ITree E Bool) (t e : ITree E Unit) : ITree E Unit
+  := bind c (fun c => if c then t else e)
+
+abbrev ITree.ifthen (c : ITree E Bool) (t : ITree E Unit) : ITree E Unit
+  := ite c t skip