------------------------------------------------------------------------
-- The code derived by Hutton/Wright in "Calculating an exceptional
-- machine" is not structurally recursive. However, it is terminating.
------------------------------------------------------------------------

module NotStructurallyRecursive where

open import Data.Nat
open import NotStructurallyRecursive.Lemmas
open import Relation.Binary.PropositionalEquality

data Expr : Set where
  val : ℕ -> Expr
  _⊕_ : Expr -> Expr -> Expr

data Cont : Set where
  STOP :                 Cont
  ADD  : ℕ    -> Cont -> Cont
  EVAL : Expr -> Cont -> Cont

-- Sizes of expressions and continuations, used for the termination
-- proof.

sizeE : Expr -> ℕ
sizeE (val n)   = 1
sizeE (e₁ ⊕ e₂) = 3 + sizeE e₁ + sizeE e₂

sizeC : Cont -> ℕ
sizeC STOP       = 0
sizeC (ADD  n c) = 1 + sizeC c
sizeC (EVAL e c) = 2 + sizeE e + sizeC c

-- The following mutually recursive functions originally were not
-- structurally recursive, but after adding suitable measure functions
-- they are. The equality proofs are used to make it possible to
-- phrase the arguments to recursive applications in the right way.

mutual

  eval : forall (e : Expr) (c : Cont) s -> s ≡ sizeE e + sizeC c -> ℕ
  eval (val n)   c zero    ()
  eval (val n)   c (suc s) eq = exec c n s (cong pred eq)
  eval (e₁ ⊕ e₂) c zero    ()
  eval (e₁ ⊕ e₂) c (suc s) eq = eval e₁ (EVAL e₂ c) s lem
    where lem = lemma₁ (sizeE e₁) (sizeE e₂) (sizeC c) eq

  exec : forall (c : Cont) (n : ℕ) s -> s ≡ sizeC c -> ℕ
  exec STOP         n _       _  = n
  exec (ADD m c₁)   n zero    ()
  exec (ADD m c₁)   n (suc s) eq = exec c₁ (m + n) s (cong pred eq)
  exec (EVAL e₁ c₂) n zero    ()
  exec (EVAL e₁ c₂) n (suc s) eq = eval e₁ (ADD n c₂) s lem
    where lem = lemma₂ (sizeE e₁) (sizeC c₂) eq

run : Expr -> ℕ
run e = eval e STOP _ refl