module Boolean-Expressions where

-- You can (hopefully) find out how to type a given character in the
-- following way: Place the cursor on the character (in Emacs), type
-- C-u C-x =, and read the line starting "to input:" (if any).

------------------------------------------------------------------------
-- Syntax

data Term : Set where
  true          : Term
  false         : Term
  if_then_else_ : (t₁ t₂ t₃ : Term) → Term

ex : Term
ex = if true then false else true

data Value : Set where
  true false : Value

⌜_⌝ : Value → Term
⌜ true ⌝  = true
⌜ false ⌝ = false

------------------------------------------------------------------------
-- Small-step semantics

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

ex⇉ : ex ⇉ false
ex⇉ = E-IfTrue

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

deterministic : ∀ {t t₁ t₂} → t ⇉ t₁ → t ⇉ t₂ → t₁ ≡ t₂
deterministic E-IfTrue E-IfTrue = refl
deterministic E-IfTrue (E-If ())
deterministic E-IfFalse E-IfFalse = refl
deterministic E-IfFalse (E-If ())
deterministic (E-If ()) E-IfTrue
deterministic (E-If ()) E-IfFalse
deterministic (E-If p) (E-If q) with deterministic p q
deterministic (E-If p) (E-If q) | refl = refl

data Red (t : Term) : Set where
  red : ∀ t′ → t ⇉ t′ → Red t

data ⊥ : Set where

contradiction : {A : Set} → ⊥ → A
contradiction ()

¬_ : Set → Set
¬ A = A → ⊥

NF : Term → Set
NF t = ¬ Red t

values-are-normal : (v : Value) → NF ⌜ v ⌝
values-are-normal true  (red t′ ())
values-are-normal false (red t′ ())

data Is-value : Term → Set where
  is-value : ∀ v → Is-value ⌜ v ⌝

if-reduces : ∀ t₁ t₂ t₃ → Red (if t₁ then t₂ else t₃)
if-reduces t₁ t₂ t₃ = {!!}

normal-forms-are-values : ∀ t → NF t → Is-value t
normal-forms-are-values true                   nf = is-value true
normal-forms-are-values false                  nf = is-value false
normal-forms-are-values (if t then t₁ else t₂) nf =
  contradiction (nf (if-reduces t t₁ t₂))

infixr 5 _∷_ _++_

data _⇉⋆_ : Term → Term → Set where
  []  : ∀ {t} → t ⇉⋆ t
  _∷_ : ∀ {t₁ t₂ t₃} → t₁ ⇉ t₂ → t₂ ⇉⋆ t₃ → t₁ ⇉⋆ t₃

_++_ : ∀ {t₁ t₂ t₃} → t₁ ⇉⋆ t₂ → t₂ ⇉⋆ t₃ → t₁ ⇉⋆ t₃
[]       ++ qs = qs
(p ∷ ps) ++ qs = p ∷ (ps ++ qs)

E-If⋆ : ∀ {t₁ t₁′ t₂ t₃} →
        t₁ ⇉⋆ t₁′ →
        if t₁ then t₂ else t₃ ⇉⋆ if t₁′ then t₂ else t₃
E-If⋆ []       = []
E-If⋆ (p ∷ ps) = E-If p ∷ E-If⋆ ps

uniqueness-of-normal-forms :
  ∀ {t t₁ t₂} →
  t ⇉⋆ t₁ → t ⇉⋆ t₂ → NF t₁ → NF t₂ → t₁ ≡ t₂
uniqueness-of-normal-forms = {!!}

⌜-⌝-injective : ∀ v₁ v₂ → ⌜ v₁ ⌝ ≡ ⌜ v₂ ⌝ → v₁ ≡ v₂
⌜-⌝-injective true  true  eq = refl
⌜-⌝-injective true  false ()
⌜-⌝-injective false true  ()
⌜-⌝-injective false false eq = refl

uniqueness-of-normal-forms′ :
  ∀ {t v₁ v₂} →
  t ⇉⋆ ⌜ v₁ ⌝ → t ⇉⋆ ⌜ v₂ ⌝ → v₁ ≡ v₂
uniqueness-of-normal-forms′ {t} {v₁} {v₂} t⇉⋆v₁ t⇉⋆v₂ =
  ⌜-⌝-injective _ _ lemma
  where
  lemma : ⌜ v₁ ⌝ ≡ ⌜ v₂ ⌝
  lemma = uniqueness-of-normal-forms t⇉⋆v₁ t⇉⋆v₂
            (values-are-normal v₁)
            (values-are-normal v₂)

data _⇓ (t : Term) : Set where
  terminates : ∀ v → t ⇉⋆ ⌜ v ⌝ → t ⇓

prepend-steps : ∀ {t₁ t₂} →  t₁ ⇉⋆ t₂  →  t₂ ⇓  →  t₁ ⇓
prepend-steps = {!!}

termination : ∀ t → t ⇓
termination = {!!}

------------------------------------------------------------------------
-- Big-step semantics

data _⇓_ : Term → Value → Set where
  ⇓-True    : true  ⇓ true
  ⇓-False   : false ⇓ false
  ⇓-IfTrue  : ∀ {t t₁ t₂ v} →
              t ⇓ true → t₁ ⇓ v →
              if t then t₁ else t₂ ⇓ v
  ⇓-IfFalse : ∀ {t t₁ t₂ v} →
              t ⇓ false → t₂ ⇓ v →
              if t then t₁ else t₂ ⇓ v

ex⇓ : if ex then ex else ex ⇓ false
ex⇓ = ⇓-IfFalse (⇓-IfTrue ⇓-True ⇓-False) (⇓-IfTrue ⇓-True ⇓-False)

ex⇉⋆ : if ex then ex else ex ⇉⋆ false
ex⇉⋆ = E-If E-IfTrue ∷ E-IfFalse ∷ E-IfTrue ∷ []

big-to-small : ∀ {t v} → t ⇓ v → t ⇉⋆ ⌜ v ⌝
big-to-small ⇓-True                   = []
big-to-small ⇓-False                  = []
big-to-small (⇓-IfTrue  t⇓true  t₁⇓v) = E-If⋆ (big-to-small t⇓true) ++
                                        E-IfTrue ∷
                                        big-to-small t₁⇓v
big-to-small (⇓-IfFalse {t} {t₁} {t₂} {v}
                        t⇓false t₂⇓v) =
  lemma₁ ++ lemma₂ ∷ lemma₃
  where
  lemma₁ : if t then t₁ else t₂ ⇉⋆ if false then t₁ else t₂
  lemma₁ = E-If⋆ (big-to-small t⇓false)

  lemma₂ : if false then t₁ else t₂ ⇉ t₂
  lemma₂ = E-IfFalse

  lemma₃ : t₂ ⇉⋆ ⌜ v ⌝
  lemma₃ = big-to-small t₂⇓v

value-of-value : ∀ v → ⌜ v ⌝ ⇓ v
value-of-value = {!!}

prepend-step : ∀ {t₁ t₂ v} → t₁ ⇉ t₂ → t₂ ⇓ v → t₁ ⇓ v
prepend-step = {!!}

small-to-big : ∀ {t v} → t ⇉⋆ ⌜ v ⌝ → t ⇓ v
small-to-big = {!!}

------------------------------------------------------------------------
-- Denotational semantics

[if_then_else_]V : Value → Value → Value → Value
[if true  then v₁ else v₂ ]V = v₁
[if false then v₁ else v₂ ]V = v₂

⟦_⟧ : Term → Value
⟦ true                 ⟧ = true
⟦ false                ⟧ = false
⟦ if t then t₁ else t₂ ⟧ = [if ⟦ t ⟧ then ⟦ t₁ ⟧ else ⟦ t₂ ⟧ ]V

⇓-complete : ∀ t → t ⇓ ⟦ t ⟧
⇓-complete t = {!!}

-- Lemma: Uniqueness of normal forms for _⇓_.

⇓-sound : ∀ t v → t ⇓ v → v ≡ ⟦ t ⟧
⇓-sound t v = {!!}