module Ahmed.Day1 where

open import Agda.Builtin.Sigma
open import Data.Bool
open import Data.Empty
open import Data.Fin
open import Data.Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary

id : {A : Set} → A → A
id {A} x = x

data type : Set where
  bool : type
  _-→_ : type → type → type

data term : Set where
  `_ : ℕ → term
  `true : term
  `false : term
  `if_then_else_ : term → term → term → term
  `λ[_]_ : (τ : type) → (e : term) → term
  _∙_ : term → term → term

data ctx : Set where
  nil : ctx
  cons : ctx → type → ctx

lookup : ctx → ℕ → Maybe type
lookup nil _ = nothing
lookup (cons ctx₁ x) zero = just x 
lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n

data sub : Set where
  nil : sub
  cons : sub → term → sub

subst : term → term → term
subst (` zero) v = v
subst (` suc x) v = ` x
subst `true v = `true
subst `false v = `false
subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)

data value-rel : type → term → Set where 
  v-`true : value-rel bool `true
  v-`false : value-rel bool `false
  v-`λ[_]_ : ∀ {τ₁ τ₂ e} → value-rel (τ₁ -→ τ₂) (`λ[ τ₁ ] e)

data good-subst : ctx → sub → Set where
  nil : good-subst nil nil
  cons : ∀ {ctx τ γ v}
    → good-subst ctx γ
    → value-rel τ v
    → good-subst (cons ctx τ) γ

data step : term → term → Set where
  step-if-e : ∀ {e e' e₁ e₂} → step e e' → step (`if e then e₁ else e₂) (`if e' then e₁ else e₂)
  step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
  step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
  step-`λ-1 : ∀ {e₁ e₁' e₂} → step e₁ e₁' → step (e₁ ∙ e₂) (e₁' ∙ e₂)
  step-`λ-2 : ∀ {τ e₁ e₂ e₂'} → step e₂ e₂' → step ((`λ[ τ ] e₁) ∙ e₂) ((`λ[ τ ] e₁) ∙ e₂')
  step-`λ-β : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)

data steps : ℕ → term → term → Set where
  zero : ∀ {e} → steps zero e e
  suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''

safe : (τ : type) → (e : term) → Set
safe τ e = ∀ {n} → (e' : term) → steps n e e' → (value-rel τ e') ⊎ (∃ λ e'' → step e' e'')

data _⊢_∶_ : ctx → term → type → Set where
  type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
  type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
  type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
    → ctx ⊢ e ∶ bool
    → ctx ⊢ e₁ ∶ τ
    → ctx ⊢ e₂ ∶ τ
    → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
  type-`x : ∀ {ctx x}
    → (p : Is-just (lookup ctx x))
    → ctx ⊢ (` x) ∶ (to-witness p)
  type-`λ : ∀ {ctx τ₁ τ₂ e}
    → (cons ctx τ₁) ⊢ e ∶ τ₂
    → ctx ⊢ (`λ[ τ₁ ] e) ∶ (τ₁ -→ τ₂)
  type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
    → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
    → ctx ⊢ e₂ ∶ τ₂
    → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂

irreducible : term → Set
irreducible e = ¬ (∃ λ e' → step e e')

data term-rel : type → term → Set where
  e-term : ∀ {τ e}
    → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
    → term-rel τ e

type-soundness : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
type-soundness {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → (value-rel τ e') ⊎ (∃ λ e'' → step e' e'')

type-sound : (e : term) → (τ : type) → (p : nil ⊢ e ∶ τ) → type-soundness p
type-sound .`true .bool type-`true .`true zero = inj₁ v-`true
type-sound .`false .bool type-`false .`false zero = inj₁ v-`false
type-sound .(`if _ then _ else _) τ (type-`ifthenelse p p₁ p₂) e' steps = {!   !}
type-sound .(`λ[ _ ] _) .(_ -→ _) (type-`λ p) e' steps = {!   !}
type-sound .(_ ∙ _) τ (type-∙ p p₁) e' steps = {!   !}

_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-rel τ e
  
fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-soundness well-typed → Γ ⊨ e ∶ τ
fundamental {Γ} {e} {τ} well-typed tsound γ good-sub = e-term f
  where
    f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'   
    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (tsound e' steps)

module semantic-type-soundness where
  part1 : (e : term) → (τ : type) → nil ⊢ e ∶ τ → term-rel τ e
  part1 (` x) _ (type-`x ())
  part1 `true bool p = e-term f
    where
      f : {n : ℕ} (e' : term) → steps n `true e' → irreducible e' → value-rel bool e'
      f {.zero} .`true zero irred = v-`true
  part1 `false bool p = e-term f
    where
      f : {n : ℕ} (e' : term) → steps n `false e' → irreducible e' → value-rel bool e'
      f {zero} .`false zero irred = v-`false
  part1 (`λ[ τ₁ ] e) (.τ₁ -→ τ₂) (type-`λ p) = e-term f
    where
      f : {n : ℕ} (e' : term) → steps n (`λ[ τ₁ ] e) e' → irreducible e' → value-rel (τ₁ -→ τ₂) e'
      f .(`λ[ τ₁ ] e) zero irred = v-`λ[_]_
  part1 (`if e then e₁ else e₂) τ (type-`ifthenelse p p₁ p₂) = e-term f
    where
      v : ∀ {n} → (e' : term) → steps n e e' → value-rel bool e' → ∃ (step (`if e then e₁ else e₂))
      v .`true zero v-`true = e₁ , step-if-1
      v .`false zero v-`false = e₂ , step-if-2
      v e' (suc {_} {e''} n step steps) val =
        (`if e'' then e₁ else e₂) , step-if-e step

      f : {n : ℕ} (e' : term) → steps n (`if e then e₁ else e₂) e' → irreducible e' → value-rel τ e'
      f .(`if e then e₁ else e₂) zero irred with part1 e bool p
      f .(`if e then e₁ else e₂) zero irred | e-term f' =
        let
          wtf = v e zero {!   !}
          wtf3 = {! irred ?  !}
          -- wtf2 = v e wtf
          -- wtf3 = irred wtf2
        -- in ⊥-elim wtf3
        in {!   !}
      f e' (suc n (step-if-e step) steps) irred = {!   !}
      f e' (suc n step-if-1 steps) irred with part1 e₁ τ p₁
      f e' (suc n step-if-1 steps) irred | e-term f' = f' e' steps irred
      f e' (suc n step-if-2 steps) irred with part1 e₂ τ p₂
      f e' (suc n step-if-2 steps) irred | e-term f' = f' e' steps irred
  part1 (e₁ ∙ e₂) τ₂ (type-∙ {_} {τ₁} p₁ p₂) = e-term f  
    where
      f : {n : ℕ} (e' : term) → steps n (e₁ ∙ e₂) e' → irreducible e' → value-rel τ₂ e'
      f .(e₁ ∙ e₂) zero irred = {!   !}
      f e' (suc n (step-`λ-1 step) steps) irred with part1 e₁ (τ₁ -→ τ₂) p₁
      f e' (suc _ (step-`λ-1 step) steps) irred | e-term f' = {!    !}
      f e' (suc n (step-`λ-2 step) steps) irred = {!   !}
      f e' (suc n step-`λ-β steps) irred = {!   !}

  part2 : (e : term) → (τ : type) → term-rel τ e → safe τ e 
  part2 e τ (e-term p) .e zero =
    inj₁ (p e zero λ q → {!   !})  
    where
      v : ⊥
      v = {!   !}     
  part2 e τ (e-term p) e' (suc {f} {g} n step steps) = inj₂ ({!   !} , {! step  !})