open import Relation.Binary.PropositionalEquality

data ∃ {A : Set} (B : A → Set) : Set where
     _,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x

infixl 8  _∨_
data _∨_ (P Q : Set) : Set where
  or-introl : P → P ∨ Q
  or-intror : Q → P ∨ Q

or-elimination : {A B C : Set} → A ∨ B → (A → C) → (B → C) → C
or-elimination (or-introl x) ac bc = ac x
or-elimination (or-intror x) ac bc = bc x

data Term : Set where
  true : Term
  false : Term
  if_then_else_ : Term → Term → Term → Term
  zero : Term
  succ : Term → Term
  pred : Term → Term
  iszero : Term → Term

infix 30 if_then_else_

data Type : Set where
  Bool : Type
  Nat : Type

data _∷_ : Term → Type → Set where
  t-True : true ∷ Bool
  t-False : false ∷ Bool
  t-If : {t₁ t₂ t₃ : Term} {T : Type} →
    t₁ ∷ Bool → t₂ ∷ T → t₃ ∷ T →
      if t₁ then t₂ else t₃ ∷ T
  t-Zero : zero ∷ Nat
  t-Succ : {t₁ : Term} →
    t₁ ∷ Nat → (succ t₁) ∷ Nat
  t-Pred : {t₁ : Term} →
    t₁ ∷ Nat → (pred t₁) ∷ Nat
  t-IsZero : {t₁ : Term} →
    iszero t₁ ∷ Bool

data is-nval : Term → Set where
  nval-zero : is-nval zero
  nval-succ : {t : Term} → is-nval t → is-nval (succ t)
  nval-pred : {t : Term} → is-nval t → is-nval (pred t)

data is-bval : Term → Set where
  bval-true : is-bval true
  bval-false : is-bval false

data is-value : Term → Set where
  val-true : is-value true
  val-false : is-value false
  val-zero : is-value zero
  val-succ : {nv : Term} → is-nval nv → is-value (succ nv)


data _⟶_ : Term → Term → Set where
  e-IfTrue : {t₂ t₃ : Term} →
    if true then t₂ else t₃ ⟶ t₂
  e-IfFalse : {t₂ t₃ : Term} →
    if false then t₂ else t₃ ⟶ t₃
  e-If : {t₁ t₁′ t₂ t₃ : Term} →
    t₁ ⟶ t₁′
      →
    if t₁ then t₂ else t₃ ⟶ if t₁′ then t₂ else t₃

  e-Succ : {t₁ t₁′ : Term} →
    t₁ ⟶ t₁′
      →
    succ t₁ ⟶ succ t₁′
  e-PredZero :
    pred zero ⟶ zero
  e-PredSucc : {nv₁ : Term} →
    is-nval nv₁
      →
    pred (succ nv₁) ⟶ pred nv₁
  e-IsZeroZero :
    iszero zero ⟶ true
  e-IsZeroSucc : {nv₁ : Term} →
    is-nval nv₁
      →
    iszero (succ nv₁) ⟶ false
  e-IsZero : {t₁ t₁′ : Term} →
    t₁ ⟶ t₁′
      →
    iszero t₁ ⟶ iszero t₁′

-- reverse-true : {R : Type} → true ∷ R → R ≡ Bool
-- reverse-true t-true = refl

normal-form-bool : {v : Term} → v ∷ Bool → is-value v → (v ≡ true) ∨ (v ≡ false)
normal-form-bool t-True is-value-v = or-introl refl
normal-form-bool t-False is-value-v = or-intror refl
normal-form-bool (t-If v-bool v-bool₁ v-bool₂) ()
normal-form-bool t-IsZero ()

normal-form-nat : {v : Term} → v ∷ Nat → is-value v → is-nval v
normal-form-nat t-Zero isval-v = nval-zero
normal-form-nat (t-Succ vnat) (val-succ x) = nval-succ x
normal-form-nat (t-Pred vnat) ()
normal-form-nat (t-If vnat vnat₁ vnat₂) ()


progress : {t : Term} {T : Type} → t ∷ T → is-value t ∨ ∃ \(t′ : Term) → t ⟶ t′
progress t-True = or-introl val-true
progress t-False = or-introl val-false
progress (t-If t1bool t₂t t₃t) = or-elimination (progress t1bool)
  (λ x → or-intror (value-case t1bool x))
  (λ x → or-intror (prog-case t1bool x))
  where
    value-case : {t₁ t₂ t₃ : Term} → t₁ ∷ Bool → is-value t₁ → ∃ \(t′ : Term) → (if t₁ then t₂ else t₃) ⟶ t′
    value-case {t₁}{t₂}{t₃} t₁bool is-value-t1 = or-elimination (normal-form-bool t₁bool is-value-t1)
      true-case
      false-case
      where
        true-case : {t₁ t₂ t₃ : Term} → t₁ ≡ true → ∃ \(t′ : Term) → (if t₁ then t₂ else t₃) ⟶ t′
        true-case {_}{t₂}{_} refl = t₂ , e-IfTrue
        false-case : {t₁ t₂ t₃ : Term} → t₁ ≡ false → ∃ \(t′ : Term) → (if t₁ then t₂ else t₃) ⟶ t′
        false-case {_}{_}{t₃} refl = t₃ , e-IfFalse
    prog-case : {t₁ t₂ t₃ : Term} → t₁ ∷ Bool → ∃ (_⟶_ t₁) → ∃ \(t′ : Term) → (if t₁ then t₂ else t₃) ⟶ t′
    prog-case {t₁}{t₂}{t₃} t1bool₁ (x₁ , x) = (if x₁ then t₂ else t₃) , (e-If x)
progress t-Zero = or-introl val-zero
progress (t-Succ case) = {!!}
progress (t-Pred case) = {!!}
progress t-IsZero = {!!}