-- {-# OPTIONS --allow-unsolved-metas #-} 
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)


module Fundamental

  {{ Α : Set }} -- Alpha, type-level constants
  {{ C : Set }} -- C, term-level constants

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

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

  where


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

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

  {{ Κ }} -- proof term symbols

import SmlSem
open SmlSem
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

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

  {{ Κ }} -- proof term symbols
  using ( _+_⊢_∣_~>_∣_ ; sdec ; s∃R ; s⇒R ; s∀R ;
    _+_⊢_∣_~_∷_~>_∣_ ; unif ; s⇒L ; s∀L ;
    smldec-val-prog ;
    view-C ; view-C-dec )

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

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

  {{ Κ }} -- proof term symbols

 
open import Relation.Binary.PropositionalEquality
open import Data.Product using (∃ ; ∃₂ ; ∃! ; _×_ ; _,_ )

{-# TERMINATING #-}
fundamental : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {ê ê' : MT}  →
  S + P ⊢ Γ ∣ ê ~> Γ' ∣ ê' → logrel S P Γ' ê' ê

fundamentaldec : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {ê : MT} {e e' : MT} {D : De} →

  S + P ⊢ Γ ∣ ê ~ e' ∷ D ~> Γ' ∣ e →
  logrelced S P Γ e' D →
  logreldec S P Γ' e' D e ê

-- sdec cases
fundamental (sdec {C = C} smldec κ∷DinP)
  with view-C-dec {C = C} refl smldec
... | e' , θ' , refl , smldec' = lift-ldecide (fundamentaldec smldec'
  (subst (λ x → logrelced _ _ _ _ x) unit-ε-De (ldecide⁻ {θ = ε} κ∷DinP (smldec-val-prog smldec'))))
  (subst (λ x → logrelced _ _ _ _ x) unit-ε-De  (ldecide⁻ κ∷DinP (smldec-val-prog smldec')))

-- s∃R case
fundamental (s∃R {C = C} {x} sml)
  with view-C {C = C} refl sml
... | e' , θ' , refl , sml'
  with view-C {C = < var x , ● >} refl sml'
... | M , θ'' , refl , sml''
  with θ'' {X = x}
... | M' , wfP = lift-∃R {C = C} (fundamental sml'') (wfP here)

-- s⇒R case
fundamental (s⇒R {C = C} {κ = κ} sml) 
  with view-C {C = C} refl sml
... | e' , θ' , refl , sml' 
  with view-C {C = lam κ ● } refl sml'
... | e'' , θ'' , refl , sml'' = lift-⇒R (fundamental sml'')  


-- s∀R cases
fundamental (s∀R {C = C} sml)
  with view-C {C = C} refl sml
... | e' , θ' , refl , sml'
  = lift-∀R (fundamental sml')

--
-- Part 2
--
open import Function


fundamentaldec (unif σ eq z) lced = lift-linit eq lced


fundamentaldec (s⇒L {C = C} smldec) lced
  with view-C-dec {C = C} refl smldec
... | e , θ , refl , smldec'
  with fundamentaldec smldec (l⇒L⁻ lced (logrefl (logced-val-prog lced)))
... | ldec
--  with θ {x}
    = lift-⇒L (logrefl (logced-val-prog lced)) ldec

fundamentaldec (s∀L {C = C} {x = x} smldec) lced
  with view-C-dec {C = C} refl smldec
... | e , θ , refl , smldec'
  with fundamentaldec smldec' (lced-∀inv lced)
... | ldec
  with θ {x}
... | M , wfP = lift-∀L' ( logdec-subst ldec) (wfP here)