{-# OPTIONS --guardedness #-}
module Language.Nested where

open import Language.Values using
    ( Value; int; bool
    ; ValueType; tint; tbool
    ; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
    ; s; s'; s''
    ; st; st'; st''
    ; b; b₁; b₂
    ; z; z₁; z₂
    )

open import Data.Integer using (ℤ; _+_; +_)
open import Data.Nat using (ℕ; suc)
open import Data.Bool using (Bool; true; false)
open import Data.List using (List; _∷_; []; length)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (Σ; _×_; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data Instruction : Set where
    pushint : ℤ → Instruction
    pushbool : Bool → Instruction
    add : Instruction

    loop : ℕ → List Instruction → Instruction
    break : Instruction

Program : Set
Program = List Instruction

Env : Set
Env = List (List Instruction)

variable
    i : Instruction
    is is' is'' : Program
    S S' S'' : Env
    n : ℕ

Triple : Set
Triple = List Value × Program × Env

data _⇒_ : Triple → Triple → Set where
    pushint-eval : ( s , (pushint z ∷ is) , S ) ⇒ ( ((int z) ∷ s) , is , S )
    pushbool-eval : ( s , (pushbool b ∷ is) , S ) ⇒ ( ((bool b) ∷ s) , is , S )
    add-eval : ( (int z₁ ∷ int z₂ ∷ s) , (add ∷ is), S ) ⇒ ( ((int (z₁ + z₂)) ∷ s) , is , S )

    loop-eval⁰ : (s , loop 0 is' ∷ is , S) ⇒ (s , is , S)
    loop-evalⁿ : (s , loop (suc n) is' ∷ is , S) ⇒ (s , is' , (loop n is' ∷ is) ∷ S)
    break-evalᶠ : (bool false ∷ s , break ∷ is , is' ∷ S) ⇒ (s , is , is' ∷ S)
    break-evalᵗ : (bool true ∷ s , break ∷ is , (loop n is'' ∷ is') ∷ S) ⇒ (s , is' , S)

    empty-eval : (s , [] , is' ∷ S) ⇒ (s , is' , S)

infixr 30 _thenᵉ_
data _⇒*_ : Triple → Triple → Set where
    doneᵉ : ( s , [] , []  ) ⇒* ( s , [] , [] )
    _thenᵉ_ : ( s , is , S ) ⇒ ( s' , is' , S' ) →
             ( s' , is' , S' ) ⇒* ( s'' , is'' , S'' ) →
             ( s , is , S ) ⇒* ( s'' , is'' , S'' )

StackType : Set
StackType = List ValueType

variable
    F F' F'' : List (List ValueType)
    σ σ' σ'' : StackType
    mst : Maybe StackType

interleaved mutual
    data _⊢⟨_⟩_↦_ : StackType → Maybe StackType → Instruction → StackType → Set
    data _⊢⟨_⟩_↦*_ : StackType → Maybe StackType → Program → StackType → Set

    data _⊢⟨_⟩_↦_ where
        pushint-t : st ⊢⟨ mst ⟩ (pushint z) ↦ (tint ∷ st)
        pushbool-t : st ⊢⟨ mst ⟩ (pushbool b) ↦ (tbool ∷ st)
        add-t : (tint ∷ tint ∷ st) ⊢⟨ mst ⟩ add ↦ (tint ∷ st)

        loop-t : st ⊢⟨ just st ⟩ is ↦* st →
                 st ⊢⟨ mst ⟩ loop n is ↦ st
        break-t : (tbool ∷ st) ⊢⟨ just st ⟩ break ↦ st

    infixr 30 _thenᵗ_
    data _⊢⟨_⟩_↦*_ where
        doneᵗ-just : st ⊢⟨ just st ⟩ [] ↦* st
        doneᵗ-nothing : st ⊢⟨ nothing ⟩ [] ↦* st
        _thenᵗ_ : st ⊢⟨ mst ⟩ i ↦ st' →
                  st' ⊢⟨ mst ⟩ is ↦* st'' →
                  st ⊢⟨ mst ⟩ (i ∷ is) ↦* st''

_⊢_↦|_ : StackType → Program → StackType → Set
_⊢_↦|_ st is st' = st ⊢⟨ nothing ⟩ is ↦* st'

basict₄ : [] ⊢ (pushint (+ 1) ∷ loop 3 (pushint (+ 2) ∷ add ∷ []) ∷ pushint (+ 1) ∷ add ∷ []) ↦| (tint ∷ [])
basict₄ = pushint-t thenᵗ loop-t (pushint-t thenᵗ add-t thenᵗ doneᵗ-just) thenᵗ pushint-t thenᵗ add-t thenᵗ doneᵗ-nothing

data _⊢_↦*_ : StackType → (Program × Env) → StackType → Set where
    program-typed-flat : st ⊢⟨ nothing ⟩ is ↦* st' →
                         st ⊢ (is , []) ↦* st'
    program-typed-rec : ∀ {stˡ} →
                        st ⊢⟨ just st' ⟩ is ↦* st' →
                        st' ⊢ (loop n is'' ∷ is' , S) ↦* stˡ →
                        st ⊢ (is , (loop n is'' ∷ is') ∷ S) ↦* stˡ

skip-loop-continuation : st ⊢ (loop n is ∷ is' , S) ↦* st' →
                         st ⊢ (is' , S) ↦* st'
skip-loop-continuation (program-typed-flat (loop-t _ thenᵗ rest)) = (program-typed-flat rest)
skip-loop-continuation (program-typed-rec (loop-t _ thenᵗ rest) frames) = (program-typed-rec rest frames)

preservation : ∀ {stˡ} →
               (s , is , S) ⇒ (s' , is' , S') →
               ⟦ st ⟧ˢ s →
               st ⊢ (is , S) ↦* stˡ →
               Σ StackType (λ st' → ⟦ st' ⟧ˢ s' × st' ⊢ (is' , S') ↦* stˡ)
preservation pushint-eval ⟦st⟧ (program-typed-flat (pushint-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
preservation pushint-eval ⟦st⟧ (program-typed-rec (pushint-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
preservation pushbool-eval ⟦st⟧ (program-typed-flat (pushbool-t thenᵗ rest)) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-flat rest))
preservation pushbool-eval ⟦st⟧ (program-typed-rec (pushbool-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-rec rest frames))
preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-flat (add-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-rec (add-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
preservation loop-eval⁰ ⟦st⟧ (program-typed-flat ((loop-t _) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-flat rest))
preservation loop-eval⁰ ⟦st⟧ (program-typed-rec ((loop-t _) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest) frames)
preservation loop-evalⁿ ⟦st⟧ (program-typed-flat ((loop-t loopt) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-flat (loop-t loopt thenᵗ rest))))
preservation loop-evalⁿ ⟦st⟧ (program-typed-rec ((loop-t loopt) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-rec (loop-t loopt thenᵗ rest) frames)))
preservation break-evalᵗ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , skip-loop-continuation frames)
preservation break-evalᶠ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest frames))
preservation empty-eval ⟦st⟧ (program-typed-rec (doneᵗ-just) frames) = (_ , ⟦st⟧ , frames)

progress : ∀ {stˡ} →
           st ⊢ (is , S) ↦* stˡ →
           ⟦ st ⟧ˢ s →
           (Σ Triple ((s , is , S) ⇒_)) ⊎ (is ≡ [] × S ≡ [] × ⟦ stˡ ⟧ˢ s)
progress (program-typed-flat (pushint-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushint-eval)
progress (program-typed-rec (pushint-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushint-eval)
progress (program-typed-flat (pushbool-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushbool-eval)
progress (program-typed-rec (pushbool-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushbool-eval)
progress (program-typed-flat (add-t thenᵗ rest)) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
progress (program-typed-rec (add-t thenᵗ rest) frames) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
progress {is = loop 0 is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
progress {is = loop 0 is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
progress {is = loop (suc n) is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
progress {is = loop (suc n) is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
progress {s = bool true ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᵗ)
progress {s = bool false ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᶠ)
progress {is = []} (program-typed-rec (doneᵗ-just) frames) ⟦st⟧ = inj₁ (_ , empty-eval)
progress {is = []} (program-typed-flat (doneᵗ-nothing)) ⟦st⟧ = inj₂ (refl , refl , ⟦st⟧)

{-# TERMINATING #-} -- evaluation always terminates, but proving it is tedious
static-dynamic-help : ∀ {stˡ} →
                      st ⊢ (is , S) ↦* stˡ →
                      ⟦ st ⟧ˢ s →
                      Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , S) ⇒* (sˡ , [] , []))
static-dynamic-help {s = s} frames ⟦st⟧
    with progress frames ⟦st⟧
...   | inj₁ ((s' , is' , S') , is⇒is') =
        let (st' , (⟦st'⟧ , frames')) = preservation is⇒is' ⟦st⟧ frames in
        let (sˡ , (⟦stˡ⟧ , is'⇒*[])) = static-dynamic-help frames' ⟦st'⟧ in
        (sˡ , (⟦stˡ⟧ , is⇒is' thenᵉ is'⇒*[]))
...   | inj₂ (refl , refl , ⟦stˡ⟧) = (s , (⟦stˡ⟧ , doneᵉ))


static-dynamic : ∀ {stˡ} →
                 st ⊢ is ↦| stˡ →
                 ⟦ st ⟧ˢ s →
                 Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , []) ⇒* (sˡ , [] , []))
static-dynamic st⊢is↦|stˡ = static-dynamic-help (program-typed-flat st⊢is↦|stˡ)

-- Copied from Flat.agda

open import Data.Nat.Show using () renaming (show to showℕ)
open import Data.Integer.Show using () renaming (show to showℤ)
open import Data.Bool.Show using () renaming (show to showBool)
open import Data.String using (String; _++_)
open import Data.Product using (proj₁)

stackToString : List Value → String
stackToString [] = "[]"
stackToString (int i ∷ s) = showℤ i ++ " :: " ++ stackToString s
stackToString (bool b ∷ s) = showBool b ++ " :: " ++ stackToString s

open import IO
open import Level using (0ℓ)

main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic basict₄ ⟦⟧ˢ-empty))))