module stlc.proof.termination where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open import Data.List
open import Data.List.Properties

open import stlc.catComb.eval
open import stlc.catComb.compile renaming (catCombValueToMachineValue to toValue)
open import stlc.step
open import machine.eval (CAM→) hiding (Config)
open import stlc.monad.impl

appInstruction-step : ∀ {i e₁ e₂} → CAM→ ⟨ APP ∷ [] ∣ cur i e₁ , e₂ ∣ [] ⟩ ⟨ i ∣ e₁ , e₂ ∣ [] ⟩
appInstruction-step {i} {e₁} {e₂} rewrite sym (cong ⟨_∣ e₁ , e₂ ∣ [] ⟩ (++-identityʳ i)) = app-step

case1Instruction-step : ∀ {f g e₁ e₂} → CAM→ ⟨ CASE f g ∷ [] ∣ e₁ , L e₂ ∣ [] ⟩ ⟨ f ∣ e₁ , e₂ ∣ [] ⟩
case1Instruction-step {f = f} {e₁ = e₁} {e₂ = e₂} rewrite sym (cong ⟨_∣ e₁ , e₂ ∣ [] ⟩ (++-identityʳ f)) = case1-step

case2Instruction-step : ∀ {f g e₁ e₂} → CAM→ ⟨ CASE f g ∷ [] ∣ e₁ , R e₂ ∣ [] ⟩ ⟨ g ∣ e₁ , e₂ ∣ [] ⟩
case2Instruction-step {g = g} {e₁ = e₁} {e₂ = e₂} rewrite sym (cong ⟨_∣ e₁ , e₂ ∣ [] ⟩ (++-identityʳ g)) = case2-step

it1Instruction-step : ∀ {x r e} → CAM→ ⟨ IT x r ∷ [] ∣ e , [] ∣ [] ⟩ ⟨ x ∣ e ∣ [] ⟩
it1Instruction-step {x} {e = e} rewrite sym (cong ⟨_∣ e ∣ [] ⟩ (++-identityʳ x)) = it1-step

appendOneInstruction : ∀ {i i₁ i₂ e₁ e₂ s₁ s₂} → CAM→ ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ → CAM→ ⟨ i₁ ++ [ i ] ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ++ [ i ] ∣ e₂ ∣ s₂ ⟩
appendOneInstruction unit-step = unit-step
appendOneInstruction nat-step = nat-step
appendOneInstruction skip-step = skip-step
appendOneInstruction fst-step = fst-step
appendOneInstruction snd-step = snd-step
appendOneInstruction push-step = push-step
appendOneInstruction swap-step = swap-step
appendOneInstruction pair-step = pair-step
appendOneInstruction cur-step = cur-step
appendOneInstruction {i} (app-step {i₁} {i₂}) rewrite ++-assoc i₂ i₁ [ i ] = app-step
--- COPRODUCT ---
appendOneInstruction inl-step = inl-step
appendOneInstruction inr-step = inr-step
appendOneInstruction {i₃} (case1-step {i₁} {i = i}) rewrite ++-assoc i₁ i [ i₃ ] = case1-step
appendOneInstruction {i₃} (case2-step {i₂ = i₂} {i}) rewrite ++-assoc i₂ i [ i₃ ] = case2-step
--- LIST OBJECT ---
appendOneInstruction nil-step = nil-step
appendOneInstruction c-step = c-step
appendOneInstruction {i₁} (it1-step {i} {x = x}) rewrite ++-assoc x i [ i₁ ] = it1-step
appendOneInstruction {i₁} (it2-step {i} {r = r}) rewrite ++-assoc r i [ i₁ ] = it2-step

appendInstructions : ∀ {i₁ i₂ i' e₁ e₂ s₁ s₂} → CAM→ ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ → CAM→ ⟨ i₁ ++ i' ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ++ i' ∣ e₂ ∣ s₂ ⟩
appendInstructions {i₁} {i₂} {[]} x rewrite ++-identityʳ i₁ | ++-identityʳ i₂ = x
appendInstructions {i₁} {i₂} {i ∷ i'} x rewrite sym (++-assoc i₁ [ i ] i') | sym (++-assoc i₂ [ i ] i') = appendInstructions (appendOneInstruction x)

splitInstructions : ∀ {i₁ i₂ i₃ e₁ e₂ e₃ s₁ s₂ s₃} → CAM→* ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ [] ∣ e₂ ∣ s₂ ⟩ → CAM→* ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ ⟨ i₃ ∣ e₃ ∣ s₃ ⟩ → CAM→* ⟨ i₁ ++ i₂ ∣ e₁ ∣ s₁ ⟩ ⟨ i₃ ∣ e₃ ∣ s₃ ⟩
splitInstructions {[]} refl x = x
splitInstructions {_ ∷ _} (trans x xs) y = trans (splitInstructions x y) (appendInstructions xs)

stackAppendOneValue-step : ∀ {i₁ i₂ e₁ e₂ s₁ s₂ s'} → CAM→ ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ → CAM→ ⟨ i₁ ∣ e₁ ∣ s₁ ++ [ s' ] ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ++ [ s' ] ⟩
stackAppendOneValue-step unit-step = unit-step
stackAppendOneValue-step nat-step = nat-step
stackAppendOneValue-step skip-step = skip-step
--- PRODUCT ---
stackAppendOneValue-step fst-step = fst-step
stackAppendOneValue-step snd-step = snd-step
stackAppendOneValue-step push-step = push-step
stackAppendOneValue-step swap-step = swap-step
stackAppendOneValue-step pair-step = pair-step
--- EXPONENTIAL ---
stackAppendOneValue-step cur-step = cur-step
stackAppendOneValue-step app-step = app-step
--- COPRODUCT ---
stackAppendOneValue-step inl-step = inl-step
stackAppendOneValue-step inr-step = inr-step
stackAppendOneValue-step case1-step = case1-step
stackAppendOneValue-step case2-step = case2-step
--- LIST OBJECT ---
stackAppendOneValue-step nil-step = nil-step
stackAppendOneValue-step c-step = c-step
stackAppendOneValue-step it1-step = it1-step
stackAppendOneValue-step it2-step = it2-step

stackAppendOneValue-tr : ∀ {i₁ i₂ e₁ e₂ s₁ s₂ s'} → CAM→* ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ → CAM→* ⟨ i₁ ∣ e₁ ∣ s₁ ++ [ s' ] ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ++ [ s' ] ⟩
stackAppendOneValue-tr refl = refl
stackAppendOneValue-tr (trans x x₁) = trans (stackAppendOneValue-tr x) (stackAppendOneValue-step x₁)

stackAppendValues : ∀ {s₁ s₂ s' i₁ i₂ e₁ e₂} → CAM→* ⟨ i₁ ∣ e₁ ∣ s₁ ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ⟩ → CAM→* ⟨ i₁ ∣ e₁ ∣ s₁ ++ s' ⟩ ⟨ i₂ ∣ e₂ ∣ s₂ ++ s' ⟩
stackAppendValues {s₁} {s₂} {[]} x rewrite ++-identityʳ s₁ | ++-identityʳ s₂ = x
stackAppendValues {s₁} {s₂} {s ∷ s'} x rewrite sym (++-assoc s₁ [ s ] s') | sym (++-assoc s₂ [ s ] s') = stackAppendValues (stackAppendOneValue-tr x)

catCombEval→machineEval : ∀ {A B s t} {f : CatComb A B} → ⟨ f ∣ s ⟩= t → CAM→* ⟨ code f ∣ toValue s ∣ [] ⟩ ⟨ [] ∣ toValue t ∣ [] ⟩
catCombEval→machineEval ev-unit = trans refl unit-step
catCombEval→machineEval ev-nat = trans refl nat-step
catCombEval→machineEval ev-id = trans refl skip-step
catCombEval→machineEval (ev-comp f₁ f₂) with catCombEval→machineEval f₁ | catCombEval→machineEval f₂
... | x | y = splitInstructions x y
--- PRODUCT ---
catCombEval→machineEval (ev-pair f₁ f₂) with catCombEval→machineEval f₁ | catCombEval→machineEval f₂
... | x | y = trans (splitInstructions (stackAppendValues x) (trans (splitInstructions (stackAppendValues y) (trans refl pair-step)) swap-step)) push-step
catCombEval→machineEval ev-p1 = trans refl fst-step
catCombEval→machineEval ev-p2 = trans refl snd-step
--- EXPONENTIAL
catCombEval→machineEval ev-cur = trans refl cur-step
catCombEval→machineEval (ev-app f) with catCombEval→machineEval f
... | x = trans x appInstruction-step
--- COPRODUCT ---
catCombEval→machineEval (ev-copair1 f) = trans (catCombEval→machineEval f) case1Instruction-step
catCombEval→machineEval (ev-copair2 f) = trans (catCombEval→machineEval f) case2Instruction-step
catCombEval→machineEval ev-i1 = trans refl inl-step
catCombEval→machineEval ev-i2 = trans refl inr-step
--- LIST OBJECT ---
catCombEval→machineEval ev-nil = trans refl nil-step
catCombEval→machineEval ev-cons = trans refl c-step
catCombEval→machineEval (ev-it-nil f) = trans (catCombEval→machineEval f) it1Instruction-step
catCombEval→machineEval (ev-it-cons f g) with catCombEval→machineEval f | catCombEval→machineEval g
... | x | y = trans (splitInstructions (stackAppendValues x) (trans (trans (splitInstructions y refl) pair-step) pair-step)) it2-step
--- MONAD ---
catCombEval→machineEval (ev-ret {m = exception} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-ret {m = state} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-ret {m = nondeterminism} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-ret {m = continuation} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-bind {s = exception} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-bind {s = state} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-bind {s = nondeterminism} x) = catCombEval→machineEval x
catCombEval→machineEval (ev-bind {s = continuation} x) = catCombEval→machineEval x