simple stack compiler&decompiler :)

Compiler.agda

{-# OPTIONS --without-K --safe #-}

module Compiler where

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

infixr 5 _∷_
{-# BUILTIN LIST List #-}

pattern [_]                     z =                     z ∷ []
pattern [_,_]                 y z =                 y ∷ z ∷ []
pattern [_,_,_]             x y z =             x ∷ y ∷ z ∷ []
pattern [_,_,_,_]         w x y z =         w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_]     v w x y z =     v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

infixr 5 _++_

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =            ys
(x ∷ xs) ++ ys  = x ∷ (xs ++ ys)

reverse : ∀ {A : Set} → List A → List A
reverse      []  = []
reverse (x ∷ xs) = reverse xs ++ [ x ]

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 4 _≡_

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans refl refl  =  refl

cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

module ≡-Reasoning {A : Set} where
  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs =
  begin
    ([] ++ ys) ++ zs
  ≡⟨⟩
    ys ++ zs
  ≡⟨⟩
    [] ++ (ys ++ zs)
  ∎
++-assoc (x ∷ xs) ys zs =
  begin
    (x ∷ xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ (xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ ((xs ++ ys) ++ zs)
  ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
    x ∷ (xs ++ (ys ++ zs))
  ≡⟨⟩
    x ∷ xs ++ (ys ++ zs)
  ∎

++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-identityʳ [] =
  begin
    [] ++ []
  ≡⟨⟩
    []
  ∎
++-identityʳ (x ∷ xs) =
  begin
    (x ∷ xs) ++ []
  ≡⟨⟩
    x ∷ (xs ++ [])
  ≡⟨ cong (x ∷_) (++-identityʳ xs) ⟩
    x ∷ xs
  ∎

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-distrib [] ys =
  begin
    reverse ([] ++ ys)
  ≡⟨⟩
    reverse ys
  ≡⟨ sym (++-identityʳ (reverse ys)) ⟩
    reverse ys ++ []
  ≡⟨⟩
    reverse ys ++ reverse []
  ∎
reverse-++-distrib (x ∷ xs) ys =
  begin
    reverse ((x ∷ xs) ++ ys)
  ≡⟨⟩
    reverse (x ∷ (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨⟩
    reverse ys ++ reverse (x ∷ xs)
  ∎

shunt : ∀ {A : Set} → List A → List A → List A
shunt      []  ys = ys
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)

shunt-reverse : ∀ {A : Set} (xs ys : List A) → shunt xs ys ≡ reverse xs ++ ys
shunt-reverse      []  ys = refl
shunt-reverse (x ∷ xs) ys =
  begin
    shunt (x ∷ xs) ys
  ≡⟨⟩
    shunt xs (x ∷ ys)
  ≡⟨ shunt-reverse xs (x ∷ ys) ⟩
    reverse xs ++ (x ∷ ys)
  ≡⟨⟩
    reverse xs ++ ([ x ] ++ ys)
  ≡⟨ sym (++-assoc (reverse xs ) [ x ] ys) ⟩
    (reverse xs ++ [ x ]) ++ ys
  ≡⟨⟩
    reverse (x ∷ xs) ++ ys
  ∎

fast-reverse : ∀ {A : Set} → List A → List A
fast-reverse xs = shunt xs []

fast-reverse-reverses : ∀ {A : Set} (xs : List A) → fast-reverse xs ≡ reverse xs
fast-reverse-reverses xs =
  begin
    fast-reverse xs
  ≡⟨⟩
    shunt xs []
  ≡⟨ shunt-reverse xs [] ⟩
    reverse xs ++ []
  ≡⟨ ++-identityʳ (reverse xs) ⟩
    reverse xs
  ∎

reverse-inv : ∀ {A : Set} → (xs : List A) → reverse (reverse xs) ≡ xs
reverse-inv [] = refl
reverse-inv (x ∷ xs) =
  begin
    reverse (reverse xs ++ [ x ])
  ≡⟨ reverse-++-distrib (reverse xs) [ x ]  ⟩
    reverse (reverse [ x ]) ++ reverse (reverse xs)
  ≡⟨⟩
    [ x ] ++ reverse (reverse xs)
  ≡⟨ cong ([ x ] ++_) (reverse-inv xs) ⟩
    [ x ] ++ xs
  ≡⟨⟩
    x ∷ xs
  ∎

fast-reverse-inv : ∀ {A : Set} → (xs : List A) → fast-reverse (fast-reverse xs) ≡ xs
fast-reverse-inv xs =
  begin
    fast-reverse (fast-reverse xs)
  ≡⟨ cong fast-reverse (fast-reverse-reverses xs) ⟩
    fast-reverse (reverse xs)
  ≡⟨ fast-reverse-reverses (reverse xs) ⟩
    reverse (reverse xs)
  ≡⟨ reverse-inv xs ⟩
    xs
  ∎

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc k) + n = suc (k + n)

_-_ : ℕ → ℕ → ℕ
m - zero = m
zero - suc n = zero
suc m - suc n = m - n

infixl 6 _+_ _-_
{-# BUILTIN NATURAL ℕ #-}

module Expr where
  data Expr : Set where
    nat : ℕ → Expr
    add : Expr → Expr → Expr
    sub : Expr → Expr → Expr

  eval : Expr → ℕ
  eval (nat e) = e
  eval (add e₁ e₂) = eval e₁ + eval e₂
  eval (sub e₁ e₂) = eval e₁ - eval e₂

module Program where
  data Command : Set where
    nat : ℕ → Command
    add : Command
    sub : Command

  Program = List Command

  eval : (program : Program) → (stack : List ℕ) → List ℕ
  eval         []             stack  = stack
  eval (nat n ∷ p)            stack  = eval p (n ∷ stack)
  eval (add   ∷ p) (n₁ ∷ n₂ ∷ stack) = eval p ((n₁ + n₂) ∷ stack)
  eval (sub   ∷ p) (n₁ ∷ n₂ ∷ stack) = eval p ((n₁ - n₂) ∷ stack)
  eval _ _ = []

open Expr
open Program

compile : (expr : Expr) → Program
compile (nat n)     =                             [ Command.nat n ]
compile (add e₁ e₂) = compile e₂ ++ compile e₁ ++ [ Command.add   ]
compile (sub e₁ e₂) = compile e₂ ++ compile e₁ ++ [ Command.sub   ]

correct : (e : Expr) → (program : Program) → (stack : List ℕ)
          → Program.eval (compile e ++ program) stack
          ≡ Program.eval program (Expr.eval e ∷ stack)
correct (nat _)     program stack = refl
correct (add e₁ e₂) program stack =
  begin
    Program.eval (compile (add e₁ e₂) ++ program) stack
  ≡⟨⟩
    Program.eval ((compile e₂ ++ compile e₁ ++ [ Command.add ]) ++ program) stack
  ≡⟨ cong₂ Program.eval (++-assoc (compile e₂) (compile e₁ ++ [ Command.add ]) program) refl ⟩
    Program.eval (compile e₂ ++ (compile e₁ ++ [ Command.add ]) ++ program) stack
  ≡⟨ correct e₂ ((compile e₁ ++ [ Command.add ]) ++ program) stack ⟩
    Program.eval ((compile e₁ ++ [ Command.add ]) ++ program) (Expr.eval e₂ ∷ stack)
  ≡⟨ cong₂ Program.eval (++-assoc (compile e₁) [ Command.add ] program) refl ⟩
    Program.eval (compile e₁ ++ ([ Command.add ] ++ program)) (Expr.eval e₂ ∷ stack)
  ≡⟨ correct e₁ ( [ Command.add ] ++ program) (Expr.eval e₂ ∷ stack) ⟩
    Program.eval ([ Command.add ] ++ program) (Expr.eval e₁ ∷ Expr.eval e₂ ∷ stack)
  ≡⟨⟩
    Program.eval (Command.add ∷ program) (Expr.eval e₁ ∷ Expr.eval e₂ ∷ stack)
  ≡⟨⟩
    Program.eval program ((Expr.eval e₁ + Expr.eval e₂) ∷ stack)
  ≡⟨⟩
    Program.eval program (Expr.eval (add e₁ e₂) ∷ stack)
  ∎
correct (sub e₁ e₂) program stack =
  begin
    Program.eval (compile (sub e₁ e₂) ++ program) stack
  ≡⟨⟩
    Program.eval ((compile e₂ ++ compile e₁ ++ [ Command.sub ]) ++ program) stack
  ≡⟨ cong₂ Program.eval (++-assoc (compile e₂) (compile e₁ ++ [ Command.sub ]) program) refl ⟩
    Program.eval (compile e₂ ++ (compile e₁ ++ [ Command.sub ]) ++ program) stack
  ≡⟨ correct e₂ ((compile e₁ ++ [ Command.sub ]) ++ program) stack ⟩
    Program.eval ((compile e₁ ++ [ Command.sub ]) ++ program) (Expr.eval e₂ ∷ stack)
  ≡⟨ cong₂ Program.eval (++-assoc (compile e₁) [ Command.sub ] program) refl ⟩
    Program.eval (compile e₁ ++ ([ Command.sub ] ++ program)) (Expr.eval e₂ ∷ stack)
  ≡⟨ correct e₁ ([ Command.sub ] ++ program) (Expr.eval e₂ ∷ stack) ⟩
    Program.eval ([ Command.sub ] ++ program) (Expr.eval e₁ ∷ Expr.eval e₂ ∷ stack)
  ≡⟨⟩
    Program.eval (Command.sub ∷ program) (Expr.eval e₁ ∷ Expr.eval e₂ ∷ stack)
  ≡⟨⟩
    Program.eval program ((Expr.eval e₁ - Expr.eval e₂) ∷ stack)
  ≡⟨⟩
    Program.eval program (Expr.eval (sub e₁ e₂) ∷ stack)
  ∎

correct_nil : (e : Expr) → Program.eval (compile e) [] ≡ [ Expr.eval e ]
correct_nil e =
  begin
    Program.eval (compile e) []
  ≡⟨ cong₂ Program.eval (sym (++-identityʳ (compile e))) refl ⟩
    Program.eval (compile e ++ []) []
  ≡⟨ correct e [] [] ⟩
    [ Expr.eval e ]
  ∎

data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A → Maybe A

decompile : (program : Program) → (stack : List Expr) → Maybe Expr
decompile []                         [ expr ] = Just expr
decompile (nat n ∷ program)            stack  = decompile program (Expr.nat n     ∷ stack)
decompile (add   ∷ program) (e₁ ∷ e₂ ∷ stack) = decompile program (Expr.add e₁ e₂ ∷ stack)
decompile (sub   ∷ program) (e₁ ∷ e₂ ∷ stack) = decompile program (Expr.sub e₁ e₂ ∷ stack)
decompile                _                 _  = Nothing

decompile-compile : (e : Expr) → (p : Program) → (stack : List Expr)
                  → decompile ((compile e) ++ p) stack
                  ≡ decompile p (e ∷ stack)
decompile-compile (nat _) p stack = refl
decompile-compile (add e₁ e₂) p stack =
  begin
    decompile ((compile e₂ ++ compile e₁ ++ [ add ]) ++ p) stack
  ≡⟨ cong₂ decompile (++-assoc (compile e₂) (compile e₁ ++ [ add ]) p ) refl ⟩
    decompile (compile e₂ ++ (compile e₁ ++ [ add ]) ++ p) stack
  ≡⟨ decompile-compile e₂ ((compile e₁ ++ [ add ]) ++ p) stack ⟩
    decompile ((compile e₁ ++ [ add ]) ++ p) (e₂ ∷ stack)
  ≡⟨ cong₂ decompile (++-assoc (compile e₁) [ add ] p) refl ⟩
    decompile (compile e₁ ++ ([ add ] ++ p)) (e₂ ∷ stack)
  ≡⟨  decompile-compile e₁ ([ add ] ++ p) (e₂ ∷ stack) ⟩
    decompile ([ add ] ++ p) (e₁ ∷ e₂ ∷ stack)
  ≡⟨⟩
    decompile p ((add e₁ e₂) ∷ stack)
  ∎
decompile-compile (sub e₁ e₂) p stack =
  begin
    decompile ((compile e₂ ++ compile e₁ ++ [ sub ]) ++ p) stack
  ≡⟨ cong₂ decompile (++-assoc (compile e₂) (compile e₁ ++ [ sub ]) p ) refl ⟩
    decompile (compile e₂ ++ (compile e₁ ++ [ sub ]) ++ p) stack
  ≡⟨ decompile-compile e₂ ((compile e₁ ++ [ sub ]) ++ p) stack ⟩
    decompile ((compile e₁ ++ [ sub ]) ++ p) (e₂ ∷ stack)
  ≡⟨ cong₂ decompile (++-assoc (compile e₁) [ sub ] p) refl ⟩
    decompile (compile e₁ ++ ([ sub ] ++ p)) (e₂ ∷ stack)
  ≡⟨  decompile-compile e₁ ([ sub ] ++ p) (e₂ ∷ stack) ⟩
    decompile ([ sub ] ++ p) (e₁ ∷ e₂ ∷ stack)
  ≡⟨⟩
    decompile p ((sub e₁ e₂) ∷ stack)
  ∎

decompile-correct : (e : Expr) → decompile (compile e) [] ≡ Just e
decompile-correct (nat n) = refl
decompile-correct (add e₁ e₂) =
  begin
    decompile (compile e₂ ++ compile e₁ ++ [ add ]) []
  ≡⟨ decompile-compile e₂ (compile e₁ ++ [ add ]) [] ⟩
    decompile (compile e₁ ++ [ add ]) [ e₂ ]
  ≡⟨ decompile-compile e₁ [ add ] [ e₂ ] ⟩
    Just (add e₁ e₂)
  ∎
decompile-correct (sub e₁ e₂) =
  begin
    decompile (compile e₂ ++ compile e₁ ++ [ sub ]) []
  ≡⟨ decompile-compile e₂ (compile e₁ ++ [ sub ]) [] ⟩
    decompile (compile e₁ ++ [ sub ]) [ e₂ ]
  ≡⟨ decompile-compile e₁ [ sub ] [ e₂ ] ⟩
    Just (sub e₁ e₂)
  ∎