module BoolExpr where

open import Bool
open import PropositionalLogic

{-
We define the type of Boolean expression, cf Figure 3.1 in Pierce:
-}

data BoolExpr : Set where
  True          : BoolExpr
  False         : BoolExpr
  If_then_else_ : BoolExpr → BoolExpr → BoolExpr → BoolExpr

ex : BoolExpr
ex = If True then False else False

{-
We then define the value of a Boolean expression
-}

val : BoolExpr → Bool
val True                    = true
val False                   = false
val (If t₁ then t₂ else t₃) = if (val t₁) then (val t₂) else (val t₃)

{-
We finally map a Boolean value to a Boolean expression ("quote" in the terminology of LISP).
-}

quot : Bool → BoolExpr
quot true  = True
quot false = False

{-
We can now define the "normal form" of a Boolean expression:
-}

nf : BoolExpr → BoolExpr
nf b = quot (val b)

Nf : BoolExpr → Set
Nf True = ⊤
Nf False = ⊤
Nf (If t then t₁ else t₂) = ⊥

quot-is-Nf : (b : Bool) → Nf (quot b)
quot-is-Nf true = <>
quot-is-Nf false = <>

nf-is-Nf : (b : BoolExpr) → Nf (nf b)
nf-is-Nf b = quot-is-Nf (val b)

{-
Exercise: implement the principle of induction on Boolean expressions! Hint: See Pierce 3.3, p 36.
-}