31 lines
840 B
Text
31 lines
840 B
Text
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 #[α] #[β]
|
||
| 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 : Array Type → Type
|
||
| ⟨[]⟩ => Unit
|
||
| ⟨[t]⟩ => t
|
||
| ⟨t::ts⟩ => t × Stack ⟨ts⟩
|
||
|
||
#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
|
||
| seq a b, s => b.run (a.run s)
|
||
|
||
#eval Op.push 1 >> Op.call Nat.succ |>.run ()
|
||
|
||
def main : IO Unit :=
|
||
IO.println s!"Hello, world!"
|