Op GADT

Main.lean

@@ -1,30 +1,35 @@
-inductive Op : (inp out : Array (Type u)) → Type (u+1) where
-| push (a : α)        : Op #[] #[α]
-| pop  {α : Type u}   : Op #[α] #[]
-| dup  {α : Type u}   : Op #[α] #[α, α]
-| swap {α β : Type u} : Op #[α, β] #[β, α]
-| call (f : α → β)    : Op #[α] #[β]
+inductive Op : (inp out : List (Type u)) → Type (u+1) where
+| push (a : α) : Op s (α::s)
+| pop  : Op (α::s) s
+| dup  : Op (α::s) (α::α::s)
+| swap : Op (α::β::s) (β::α::s)
+| call : Op ((α → β)::α::s) (β::s)
 | seq  (a : Op i o) (b : Op o o') : Op i o'
 
-instance : HAndThen (Op i o) (Op o o') (Op i o') where
-  hAndThen a b := Op.seq a (b ())
+abbrev Stack : List Type → Type
+| [] => Unit
+| t::ts => t × Stack ts
 
-abbrev Stack : Array Type → Type
-| ⟨[]⟩ => Unit
-| ⟨[t]⟩ => t
-| ⟨t::ts⟩ => t × Stack ⟨ts⟩
+example : (α × Stack s) = Stack (α::s) := by simp
 
-#reduce (types := true) Stack #[Nat, Int, Int]
+#reduce (types := true) Stack [Nat, Int, Int]
 
 def Op.run : Op i o → Stack i → Stack o
-| push x, () => x
-| pop, _ => ()
-| dup, x => (x, x)
-| swap, (a, b) => (b, a)
-| call f, x => f x
+| push x, t => (x, t)
+| pop, (x, s) => s
+| dup, (x, s) => (x, x, s)
+| swap, (a, b, s) => (b, a, s)
+| call, (f, a, s) => (f a, s)
 | seq a b, s => b.run (a.run s)
 
-#eval Op.push 1 >> Op.call Nat.succ |>.run ()
+def Op.runEmpty (op : Op [] o) : Stack o := op.run ()
+
+#eval  (Op.push 1)
+|>.seq (Op.push 2)
+|>.seq (Op.push Nat.add)
+|>.seq  Op.call
+|>.seq  Op.call
+|>.runEmpty
 
 def main : IO Unit :=
   IO.println s!"Hello, world!"