ast.compile.run = ast.interpret

Bytecode/Basic.lean

@@ -52,6 +52,8 @@ def Ast.compile : Ast → M Unit
 | mul l r => M.op l.compile r.compile (·*·)
 | div l r => M.op l.compile r.compile (·/·)
 
+#eval (do Ast.compile (3/2 + 0.5); M.pop).run #[]
+
 def M.run (m : M Unit) : Option Rat :=
   OptionT.run (do m; pop) #[] |>.fst
 
@@ -70,7 +72,7 @@ theorem M.push_pop : (do push x; pop) = pure x := by
 --   id_map {a} x := by
 --     simp [Functor.map, OptionT.bind, OptionT.mk, StateT.instLawfulMonad]
 
-theorem Ast.compile_sound (ast : Ast)
+theorem Ast.compile_eq_push_interpret (ast : Ast)
     : ast.compile = M.push ast.interpret := by
   induction ast
   · rfl
@@ -78,3 +80,7 @@ theorem Ast.compile_sound (ast : Ast)
     simp only [M.op, compile, interpret, *]
     repeat rw [←bind_assoc, M.push_pop, pure_bind]
   )
+
+theorem Ast.compile_sound (ast : Ast)
+    : ast.compile.run = ast.interpret := by
+  simp [M.run, compile_eq_push_interpret, M.push_pop, pure, OptionT.pure, StateT.pure]

README.md

@@ -1 +1,5 @@
 # bytecode
+
+proof that an extremely basic bytecode compiler is sound
+
+(maybe todo: main)