From 0fbe8d310392deb63ebff0e25b0b3e4931c4d66f Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Wed, 9 Apr 2025 15:37:27 -0400
Subject: [PATCH] hey this works

---
 Bytecode/Basic.lean | 95 ++++++++++++++++++---------------------------
 1 file changed, 38 insertions(+), 57 deletions(-)

diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean
index aebaa8f..d4fff5f 100644
--- a/Bytecode/Basic.lean
+++ b/Bytecode/Basic.lean
@@ -1,5 +1,7 @@
 import Batteries.Data.Rat.Basic
 import Batteries.Control.Lawful.MonadLift
+-- THIS GETS ME LawfulMonad (OptionT m)! YES
+import Batteries.Control.OptionT
 
 inductive Ast
 | lit (n : Rat)
@@ -27,73 +29,52 @@ def Ast.interpret : Ast → Rat
 
 #eval Ast.interpret <| 3/2 + 0.5
 
-inductive Op
-| push (n : Rat)
-| add
-| sub
-| mul
-| div
-  deriving Repr
-
--- TODO: prove that the stack manip is all good throughout
-def Op.pop_push : Op → Nat × Nat
-| push _ => (0, 1)
-| _ => (2, 1)
-
-abbrev Ops := Array Op
-
-def pushM (x : α) : StateM (Array α) Unit :=
-  modify <| (·.push x)
-
-def popM? : StateM (Array α) (Option α) := do
-  let top ← Array.back? <$> get
-  modify Array.pop
-  return top
-
 abbrev M := OptionT (StateM (Array Rat))
-instance : LawfulMonad M := sorry
 
-def Op.action (op : Op) : M Unit := do
-  match op with
-  | .push n => pushM n
-  | .add => pushM <| (← popM?) + (← popM?)
-  | .sub => pushM <| (← popM?) - (← popM?)
-  | .mul => pushM <| (← popM?) * (← popM?)
-  | .div => pushM <| (← popM?) / (← popM?)
+def M.push (n : Rat) : M Unit := modify (·.push n)
 
-def Ops.action (ops : Ops) : M Unit := ops.forM Op.action
+def M.pop : M Rat := OptionT.mk do
+  let top ← getModify Array.pop
+  return top.back?
 
-def Ops.run (ops : Ops) : Option Rat :=
-  (do
-    ops.action
-    popM?
-  ).run #[] |>.fst
+abbrev M.op (l r : M Unit) (f : Rat → Rat → Rat) : M Unit := do
+  l
+  let l ← pop
+  r
+  let r ← pop
+  push (f l r)
 
-def Ast.compile : Ast → Ops
-| .lit n => #[.push n]
-| .add l r => l.compile ++ r.compile ++ #[.add]
-| .sub l r => l.compile ++ r.compile ++ #[.sub]
-| .mul l r => l.compile ++ r.compile ++ #[.mul]
--- Note that l and r are flipped here. compilation!
-| .div l r => r.compile ++ l.compile ++ #[.div]
 
-#eval (3/2 + 0.5 : Ast) |>.compile.run
+def Ast.compile : Ast → M Unit
+| lit n   => M.push n
+| add l r => M.op l.compile r.compile (·+·)
+| sub l r => M.op l.compile r.compile (·-·)
+| mul l r => M.op l.compile r.compile (·*·)
+| div l r => M.op l.compile r.compile (·/·)
+
+def M.run (m : M Unit) : Option Rat :=
+  OptionT.run (do m; pop) #[] |>.fst
+
+#eval Ast.compile (3/2 + 0.5) |>.run
 
 @[simp]
-theorem Ops.append_action (a b : Ops)
-    : (a ++ b).action = (do a.action; b.action) := by
-  rw [action]
-  exact Array.forM_append
+theorem M.push_pop : (do push x; pop) = pure x := by
+  funext xs
+  -- what on earth
+  simp only [bind, OptionT.bind, OptionT.mk, StateT.bind, push, modify, modifyGet,
+    MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, OptionT.lift, StateT.modifyGet, pure,
+    StateT.pure, pop, getModify, Array.pop_push, Array.back?_push, OptionT.pure]
 
-@[simp]
-theorem Ops.push_action (ops : Ops) (op : Op)
-    : action (ops.push op) = (do ops.action; op.action) := by
-  rw [Array.push_eq_append, append_action]
-  have : op.action = action #[op] := by simp [action]
-  rw [this]
+-- instance : LawfulMonad M where
+--   map_const := rfl
+--   id_map {a} x := by
+--     simp [Functor.map, OptionT.bind, OptionT.mk, StateT.instLawfulMonad]
 
 theorem Ast.compile_sound (ast : Ast)
-    : ast.compile.run = some ast.interpret := by
+    : ast.compile = M.push ast.interpret := by
   induction ast
   · rfl
-  simp [compile]
+  repeat (
+    simp only [M.op, compile, interpret, *]
+    repeat rw [←bind_assoc, M.push_pop, pure_bind]
+  )