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

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Binary using (Decidable)

module LF

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

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


  where


mutual 
  data t : Set where
    const : C → t
    var : Var → t
    apt : t → t → t
    lamt : T → t → t

  data T : Set where
    tconst : Α → T
    apT : T → t → T
    PiT : T → T → T

data K : Set where
  type : K
  o : K
  PiK : T → K → K


-- Signatures
data Sig : Set where
  · : Sig
  _,_∷T_ : Sig → C → T → Sig
  _,_∷K_ : Sig → Α → K → Sig

-- Contexts
data Ctx : Set where
  · : Ctx
  _,_∷_ : Ctx → Var → T → Ctx







data _∷_∈_ : Var → T → Ctx → Set where
  here : {Γ : Ctx} { A : T} { X : Var } → X ∷ A ∈ (Γ , X ∷ A)
  there : {Γ : Ctx} {A B : T} {X Y : Var} → X ∷ A ∈ Γ → X ∷ A ∈ (Γ , Y ∷ B)



-- Well-formedness
postulate _+_⊢_∷_ : Sig → Ctx → t → T → Set

postulate wf-var : {S : Sig} {Γ : Ctx} {x : Var} {A : T} → x ∷ A ∈ Γ → S + Γ ⊢ var x ∷ A

postulate _+_⊢_∷T_ : Sig → Ctx → T → K → Set

postulate _+_⊢_≡T_∷_ : Sig → Ctx → T → T → K → Set



data ⊢_ : Sig → Set where
  ·-wfsig : ⊢ ·
  ,∷-wfctx-c : ∀ {S} {c : C} {A : T}  → ⊢ S → S + · ⊢ ( const c ) ∷ A → ⊢ ( S , c ∷T A )
  ,∷-wfctx-o : ∀ {S} {a : Α}  → ⊢ S → S + · ⊢ ( tconst a ) ∷T o → ⊢ ( S , a ∷K o )
  ,∷-wfctx-type : ∀ {S} {a : Α}  → ⊢ S → S + · ⊢ ( tconst a ) ∷T type → ⊢ ( S , a ∷K type )

data _⊢_ : Sig → Ctx → Set where
  ·-wfctx : ∀ {S} → ⊢ S → S ⊢ ·
  ,∷-wfctx : ∀ {S Γ y A} → S ⊢ Γ → S ⊢ (Γ , y ∷ A)
  


open import Data.Product 

-- simultaneoust subst
Θ : Sig → Ctx → Ctx → Set
Θ S Γ Γ' = ∀ {X} → Σ t (λ M → ∀ {A} → X ∷ A ∈ Γ → S + Γ' ⊢ M ∷ A)  


weaken' : ∀ {S} {Γ Γ'} {A B} {X Y} {M} →
         (X ∷ A ∈ (Γ , Y ∷ B) → S + Γ' ⊢ M ∷ A) →
         (X ∷ A ∈ Γ → S + Γ' ⊢ M ∷ A)
weaken' wf X∷A∈Γ = wf (there X∷A∈Γ)

weaken : ∀ {S} {Γ Γ'} {B} {Y} →
  Θ S (Γ , Y ∷ B) Γ' →
  Θ S Γ Γ'
weaken θ {X}
  with θ {X}
weaken θ {X} | M , snd = M , weaken' snd




open import Relation.Nullary

_[_/_]T : T → t → Var → T
_[_/_]t : t → t → Var → t


tconst a [ M / x ]T = tconst a
apT A N [ M / x ]T = apT (A [ M / x ]T) (N [ M / x ]t)
PiT A B [ M / x ]T = PiT (A [ M / x ]T) (B [ M / x ]T)

const c [ M / x ]t = const c
var y [ M / x ]t with decEqVar x y
(var y [ M / x ]t) | yes p = M
(var y [ M / x ]t) | no ¬p = var y
apt N₁ N₂ [ M / x ]t = apt (N₁ [ M / x ]t) (N₂ [ M / x ]t)
lamt A N [ M / x ]t = lamt (A [ M / x ]T) (N [ M / x ]t)

-- substitution


_Θt_ : ∀ {S Γ Γ'} → Θ S Γ Γ' → t → t 
_ΘT_ : ∀ {S Γ Γ'} → Θ S Γ Γ' → T → T

θ ΘT tconst a = tconst a
θ ΘT apT A M = apT (θ ΘT A) (θ Θt M)
θ ΘT PiT A B = PiT (θ ΘT A) (θ ΘT B)

θ Θt const c = const c
θ Θt var x
  with θ {X = x} 
... | t , res = t
θ Θt apt M₁ M₂ =  apt (θ Θt M₁)  (θ Θt M₂)
θ Θt lamt A M = lamt A (θ Θt M)


ε : ∀ {S Γ} → Θ S Γ Γ -- empty subst
ε {X = X} = var X , λ x → wf-var x

_Θ∘_ : ∀ {S Γ Γ' Γ'' } → Θ S Γ Γ' → Θ S Γ' Γ'' → Θ S Γ Γ'' -- empty subst
(θ Θ∘ θ') {X} with θ {X = X}
(θ Θ∘ θ') {X} | M , wf = (θ' Θt M) , {!!}

postulate unit-ε-t : {M : t} → ε Θt M ≡ M -- empty subst over types
postulate unit-ε-T : {A : T} → ε ΘT A ≡ A -- empty subst over terms



{-

[/]T-dist : {A : T} {M : t} {x : Var} {θ : Θ} →
  (θ ΘT (A [ M / x ]T)) ≡ (θ ΘT A) [ (θ Θt M) / x ]T

[/]t-dist : {N M : t} {x : Var} {θ : Θ} →
  (θ Θt (N [ M / x ]t)) ≡ (θ Θt N) [ (θ Θt M) / x ]t



[/]T-dist {tconst a} {M} {x} {θ} = refl
[/]T-dist {apT A x₁} {M} {x} {θ} = cong₂ apT [/]T-dist [/]t-dist
[/]T-dist {PiT A A₁} {M} {x} {θ} = cong₂ PiT [/]T-dist [/]T-dist


[/]t-dist {const c} {M} {x} {θ} = refl
[/]t-dist {uvar X} {M} {x} {θ} = {!!}
[/]t-dist {var y} {M} {x} {θ} with decEqVar x y
[/]t-dist {var y} {M} {.y} {θ} | yes refl = {!!}
... | no ¬p = {!!}
[/]t-dist {apt N₁ N₂} {M} {x} {θ} = {!!}
[/]t-dist {lamt y N} {M} {x} {θ} = {!!}

-}




{- implicit validity -}
impl-val-ctx : {S : Sig} {Γ : Ctx} {A A' : T} {L : K} →
  S + Γ ⊢ A ≡T A' ∷ L →
  S ⊢ Γ

impl-val-ctx = {!!}


lf-subst-ty : {S : Sig} {Γ : Ctx} {A B : T} {x : Var} {M N : t} →

              S + Γ , x ∷ B ⊢ M ∷ A →
              S + Γ ⊢ ( M [ N / x ]t ) ∷ (A [ N / x ]T)

lf-subst-ty = {!!}



trm-weaken-sig : {S : Sig} {Γ : Ctx} {M : t} {c : C} {A B : T} →
  S + Γ ⊢ M ∷ B →
  ⊢ (S , c ∷T A) →
  (S , c ∷T A) + Γ ⊢  M ∷ B
trm-weaken-sig = {!!}