-- {-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)


module Escape
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

  {{ Var : Set }} -- term variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}


  {{  Κ : Set }}   -- proof term constants

  where


open import SyntaxRew 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }} -- unification variables

  {{ Κ }}    -- proof term constants


open import LogRel
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }} -- unification variables

  {{ Κ }}    -- proof term constants

open import BigSem
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants
  
  {{ Var }}  -- variables
  {{ decEqVar }} -- unification variables

  {{ Κ }}    -- proof term constants


open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (subst ; subst₂ ; sym ; refl ; trans )


import BigSem

-- escape from logrel to bigstep
escape' : {S : Sig} {P : Prog} {G : Go} {e : PT} {e' : MT} →

    e' ≡ inMT e →
    logrel S P · e' (go G) →
    S + P ⟶ e ∷ G

escapedec : {S : Sig} {P : Prog} {A : T} {e e₁ : PT } {D₁ : De} →

    logreldec S P · (inMT e₁) D₁ (inMT e) (go (at A)) →
    logrelced S P · (inMT e₁) D₁ →  
    S + P - e₁ ∷ D₁ ⟶ e ∷ A


{-# TERMINATING #-}
-- proof on simultaneous structural induction on derivations

--
-- Part 1
--

escape' eq (ldecide ldec lced)
  with inMT-PT' eq
... | e'' , refl 
  with pt ldec
... | x , refl = escape' eq (lift-ldecide-pt ldec lced)

escape' eq (l∃R log wfM)
  with inMT-PT' eq
escape' eq (l∃R log wfM) | symbP x , ()
escape' eq (l∃R log wfM) | (e'' apP e''') , ()
escape' {e = symbP x₁} () (l∃R log wfM) | < x , e'' >P , refl
escape' {e = e apP e₁} () (l∃R log wfM) | < x , e'' >P , refl
escape' {e = < x₁ , e >P} refl (l∃R log wfM) | < x , e'' >P , eq'
  with injective-inMT eq'
... | refl = ∃R (escape' refl log) wfM
escape' {e = lamP x₁ e} () (l∃R log wfM) | < x , e'' >P , refl 
escape' eq (l∃R log wfM) | lamP x e'' , ()


escape' eq (l⇒R log)
  with inMT-PT' eq
escape' eq (l⇒R {e = e} log) | symbP x , ()
escape' eq (l⇒R {e = e} log) | (e'' apP e''') , ()
escape' eq (l⇒R {e = e} log) | < x , e'' >P , ()
escape' {e = symbP x₁} () (l⇒R {e = .(inMT e'')} log) | lamP x e'' , refl 
escape' {e = e apP e₁} () (l⇒R {e = .(inMT e'')} log) | lamP x e'' , refl 
escape' {e = < x₁ , e >P} () (l⇒R {e = .(inMT e'')} log) | lamP x e'' , refl
escape' {e = lamP x₁ e} eq (l⇒R {e = .(inMT e'')} log) | lamP x e'' , refl
  with injective-inMT eq
... | refl = ⇒R (escape' refl log)

escape' eq (l∀R log)
  with inMT-PT' eq
... | e'' , eq'
  with injective-inMT (trans eq' eq)
... | refl 
  = ∀R (escape'
       (subst (λ x → (x [ _ / _ ]MT) ≡ (inMT (_ [ _ / _ ]PT))) eq' (sym (inMT-[/]-dist)))
       log)

    
escape' eq (logrefl x)
  with inMT-PT' eq
... | e' , eq'
  with injective-inMT (trans eq' eq)
escape' eq (logrefl x) | symbP x₁ , () | refl
escape' eq (logrefl x) | (e' apP e'') , () | refl 
escape' eq (logrefl x) | < x₁ , e' >P , () | refl
escape' eq (logrefl x) | lamP x₁ e' , () | refl

--
-- Part 2
-- 

escapedec (linit eq refl) lced
  with injective-inMT eq
... | refl = init

escapedec (l⇒L log ldec) lced
  with pt ldec
escapedec (l⇒L log ldec) lced | symbP _ , ()
escapedec (l⇒L log ldec) lced | (e apP e₁) , eq
  with inspect-apM eq
... | _ , eq'
  with inMT-PT' eq'
... | e' , refl = ⇒L (escape' refl log) (escapedec ldec (l⇒L⁻ lced log))
escapedec (l⇒L log ldec) lced | < _ , _ >P , ()
escapedec (l⇒L log ldec) lced | lamP _ _ , ()


escapedec (l∀L ldec wfM) lced
  with pt ldec
... | e , eq
  with injective-inMT eq 
... | refl = ∀L (escapedec ldec (logced-subst (lced-∀inv lced) wfM)) wfM


-- escape from logrel to bigstep
escape : {S : Sig} {P : Prog} {G : Go} {e : PT}  →

    logrel S P · (inMT e) (go G) →
    S + P ⟶ e ∷ G

escape = escape' refl