------------------------------------------------------------------------
-- The abstract syntax is a set, and the semantics is propositional
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Atom

module Propositional (atoms : χ-atoms) where

open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (const)

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J

open import Cancellation  atoms
open import Chi           atoms
open import Deterministic atoms

open χ-atoms atoms

-- Exp has decidable equality.

mutual

  _≟_ : Decidable-equality Exp
  apply e₁₁ e₂₁  apply e₁₂ e₂₂ with e₁₁  e₁₂
  ... | no  e₁₁≢e₁₂ = no (e₁₁≢e₁₂  proj₁  cancel-apply)
  ... | yes e₁₁≡e₁₂ = ⊎-map (cong₂ apply e₁₁≡e₁₂)
                            (_∘ proj₂  cancel-apply)
                            (e₂₁  e₂₂)


  lambda x₁ e₁  lambda x₂ e₂ with x₁ V.≟ x₂
  ... | no  x₁≢x₂ = no (x₁≢x₂  proj₁  cancel-lambda)
  ... | yes x₁≡x₂ = ⊎-map (cong₂ lambda x₁≡x₂)
                          (_∘ proj₂  cancel-lambda)
                          (e₁  e₂)

  case e₁ bs₁  case e₂ bs₂ with e₁  e₂
  ... | no  e₁≢e₂ = no (e₁≢e₂  proj₁  cancel-case)
  ... | yes e₁≡e₂ = ⊎-map (cong₂ case e₁≡e₂)
                          (_∘ proj₂  cancel-case)
                          (bs₁ ≟-B⋆ bs₂)

  rec x₁ e₁  rec x₂ e₂ with x₁ V.≟ x₂
  ... | no  x₁≢x₂ = no (x₁≢x₂  proj₁  cancel-rec)
  ... | yes x₁≡x₂ = ⊎-map (cong₂ rec x₁≡x₂)
                          (_∘ proj₂  cancel-rec)
                          (e₁  e₂)

  var x₁  var x₂ = ⊎-map (cong var) (_∘ cancel-var) (x₁ V.≟ x₂)

  const c₁ es₁  const c₂ es₂ with c₁ C.≟ c₂
  ... | no  c₁≢c₂ = no (c₁≢c₂  proj₁  cancel-const)
  ... | yes c₁≡c₂ = ⊎-map (cong₂ const c₁≡c₂)
                          (_∘ proj₂  cancel-const)
                          (es₁ ≟-⋆ es₂)

  apply _ _   lambda _ _ = no  ())
  apply _ _   case _ _   = no  ())
  apply _ _   rec _ _    = no  ())
  apply _ _   var _      = no  ())
  apply _ _   const _ _  = no  ())
  lambda _ _  apply _ _  = no  ())
  lambda _ _  case _ _   = no  ())
  lambda _ _  rec _ _    = no  ())
  lambda _ _  var _      = no  ())
  lambda _ _  const _ _  = no  ())
  case _ _    apply _ _  = no  ())
  case _ _    lambda _ _ = no  ())
  case _ _    rec _ _    = no  ())
  case _ _    var _      = no  ())
  case _ _    const _ _  = no  ())
  rec _ _     apply _ _  = no  ())
  rec _ _     lambda _ _ = no  ())
  rec _ _     case _ _   = no  ())
  rec _ _     var _      = no  ())
  rec _ _     const _ _  = no  ())
  var _       apply _ _  = no  ())
  var _       lambda _ _ = no  ())
  var _       case _ _   = no  ())
  var _       rec _ _    = no  ())
  var _       const _ _  = no  ())
  const _ _   apply _ _  = no  ())
  const _ _   lambda _ _ = no  ())
  const _ _   case _ _   = no  ())
  const _ _   rec _ _    = no  ())
  const _ _   var _      = no  ())

  _≟-B_ : Decidable-equality Br
  branch c₁ xs₁ e₁ ≟-B branch c₂ xs₂ e₂ with c₁ C.≟ c₂
  ... | no  c₁≢c₂ = no (c₁≢c₂  proj₁  cancel-branch)
  ... | yes c₁≡c₂ with List.Dec._≟_ V._≟_ xs₁ xs₂
  ...   | no  xs₁≢xs₂ = no (xs₁≢xs₂  proj₁  proj₂  cancel-branch)
  ...   | yes xs₁≡xs₂ = ⊎-map (cong₂ (uncurry branch)
                                     (cong₂ _,_ c₁≡c₂ xs₁≡xs₂))
                              (_∘ proj₂  proj₂  cancel-branch)
                              (e₁  e₂)

  _≟-⋆_ : Decidable-equality (List Exp)
  []         ≟-⋆ []         = yes refl
  (e₁  es₁) ≟-⋆ (e₂  es₂) with e₁  e₂
  ... | no  e₁≢e₂ = no (e₁≢e₂  List.cancel-∷-head)
  ... | yes e₁≡e₂ = ⊎-map (cong₂ _∷_ e₁≡e₂)
                          (_∘ List.cancel-∷-tail)
                          (es₁ ≟-⋆ es₂)

  []      ≟-⋆ (_  _) = no  ())
  (_  _) ≟-⋆ []      = no  ())

  _≟-B⋆_ : Decidable-equality (List Br)
  []         ≟-B⋆ []         = yes refl
  (b₁  bs₁) ≟-B⋆ (b₂  bs₂) with b₁ ≟-B b₂
  ... | no  b₁≢b₂ = no (b₁≢b₂  List.cancel-∷-head)
  ... | yes b₁≡b₂ = ⊎-map (cong₂ _∷_ b₁≡b₂)
                          (_∘ List.cancel-∷-tail)
                          (bs₁ ≟-B⋆ bs₂)

  []      ≟-B⋆ (_  _) = no  ())
  (_  _) ≟-B⋆ []      = no  ())

-- Exp is a set.

Exp-set : Is-set Exp
Exp-set = decidable⇒set _≟_

-- An alternative definition of the semantics.

data Lookup′ (c : Const) : List Br  List Var  Exp  Set where
  here  :  {c′ xs xs′ e e′ bs} 
          c  c′  xs  xs′  e  e′ 
          Lookup′ c (branch c′ xs′ e′  bs) xs e
  there :  {c′ xs′ e′ bs xs e} 
          c  c′  Lookup′ c bs xs e 
          Lookup′ c (branch c′ xs′ e′  bs) xs e

infixr 5 _∷_
infix  4 _[_←_]↦′_

data _[_←_]↦′_ (e : Exp) : List Var  List Exp  Exp  Set where
  []  :  {e′}  e  e′  e [ []  [] ]↦′ e′
  _∷_ :  {x xs e′ es′ e″ e‴} 
        e‴  e″ [ x  e′ ]  e [ xs  es′ ]↦′ e″ 
        e [ x  xs  e′  es′ ]↦′ e‴

infix 4 _⟶′_ _⟶⋆′_

mutual

  data _⟶′_ : Exp  Exp  Set where
    apply  :  {e₁ e₂ x e v₂ v} 
             e₁ ⟶′ lambda x e  e₂ ⟶′ v₂  e [ x  v₂ ] ⟶′ v 
             apply e₁ e₂ ⟶′ v
    case   :  {e bs c es xs e′ e″ v} 
             e ⟶′ const c es  Lookup′ c bs xs e′ 
             e′ [ xs  es ]↦′ e″  e″ ⟶′ v 
             case e bs ⟶′ v
    rec    :  {x e v}  e [ x  rec x e ] ⟶′ v  rec x e ⟶′ v
    lambda :  {x x′ e e′} 
             x  x′  e  e′  lambda x e ⟶′ lambda x′ e′
    const  :  {c c′ es vs} 
             c  c′  es ⟶⋆′ vs  const c es ⟶′ const c′ vs

  data _⟶⋆′_ : List Exp  List Exp  Set where
    []  : [] ⟶⋆′ []
    _∷_ :  {e es v vs}  e ⟶′ v  es ⟶⋆′ vs  e  es ⟶⋆′ v  vs

-- The alternative definition is isomorphic to the other one.

Lookup↔Lookup′ :  {c bs xs e}  Lookup c bs xs e  Lookup′ c bs xs e
Lookup↔Lookup′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to :  {c bs xs e}  Lookup c bs xs e  Lookup′ c bs xs e
  to here          = here refl refl refl
  to (there p₁ p₂) = there p₁ (to p₂)

  from :  {c bs xs e}  Lookup′ c bs xs e  Lookup c bs xs e
  from (here refl refl refl) = here
  from (there p₁ p₂)         = there p₁ (from p₂)

  from∘to :  {c bs xs e} (p : Lookup c bs xs e)  from (to p)  p
  from∘to here          = refl
  from∘to (there p₁ p₂) rewrite from∘to p₂ = refl

  to∘from :  {c bs xs e} (p : Lookup′ c bs xs e)  to (from p)  p
  to∘from (here refl refl refl) = refl
  to∘from (there p₁ p₂)         rewrite to∘from p₂ = refl

↦↔↦′ :  {e xs es e′}  e [ xs  es ]↦ e′  e [ xs  es ]↦′ e′
↦↔↦′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to :  {e xs es e′}  e [ xs  es ]↦ e′  e [ xs  es ]↦′ e′
  to []    = [] refl
  to ( p) = refl  to p

  from :  {e xs es e′}  e [ xs  es ]↦′ e′  e [ xs  es ]↦ e′
  from ([] refl)  = []
  from (refl  p) =  from p

  from∘to :  {e xs es e′} (p : e [ xs  es ]↦ e′)  from (to p)  p
  from∘to []    = refl
  from∘to ( p) rewrite from∘to p = refl

  to∘from :  {e xs es e′} (p : e [ xs  es ]↦′ e′)  to (from p)  p
  to∘from ([] refl)  = refl
  to∘from (refl  p) rewrite to∘from p = refl

⟶↔⟶′ :  {e v}  e  v  e ⟶′ v
⟶↔⟶′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  mutual

    to :  {e v}  e  v  e ⟶′ v
    to (apply p q r)  = apply (to p) (to q) (to r)
    to (case p q r s) = case (to p) (_↔_.to Lookup↔Lookup′ q)
                             (_↔_.to ↦↔↦′ r) (to s)
    to (rec p)        = rec (to p)
    to lambda         = lambda refl refl
    to (const ps)     = const refl (to⋆ ps)

    to⋆ :  {e v}  e ⟶⋆ v  e ⟶⋆′ v
    to⋆ []       = []
    to⋆ (p  ps) = to p  to⋆ ps

  mutual

    from :  {e v}  e ⟶′ v  e  v
    from (apply p q r)      = apply (from p) (from q) (from r)
    from (case p q r s)     = case (from p) (_↔_.from Lookup↔Lookup′ q)
                                   (_↔_.from ↦↔↦′ r) (from s)
    from (rec p)            = rec (from p)
    from (lambda refl refl) = lambda
    from (const refl ps)    = const (from⋆ ps)

    from⋆ :  {e v}  e ⟶⋆′ v  e ⟶⋆ v
    from⋆ []       = []
    from⋆ (p  ps) = from p  from⋆ ps

  mutual

    from∘to :  {e v} (p : e  v)  from (to p)  p
    from∘to (apply p q r)  rewrite from∘to p | from∘to q | from∘to r
                           = refl
    from∘to (case p q r s) rewrite from∘to p
                                 | _↔_.left-inverse-of Lookup↔Lookup′ q
                                 | _↔_.left-inverse-of ↦↔↦′ r
                                 | from∘to s = refl
    from∘to (rec p)        rewrite from∘to p = refl
    from∘to lambda         = refl
    from∘to (const ps)     rewrite from⋆∘to⋆ ps = refl

    from⋆∘to⋆ :  {e v} (ps : e ⟶⋆ v)  from⋆ (to⋆ ps)  ps
    from⋆∘to⋆ []       = refl
    from⋆∘to⋆ (p  ps) rewrite from∘to p | from⋆∘to⋆ ps = refl

  mutual

    to∘from :  {e v} (p : e ⟶′ v)  to (from p)  p
    to∘from (apply p q r)      rewrite to∘from p | to∘from q | to∘from r
                               = refl
    to∘from (case p q r s)     rewrite to∘from p
                                     | _↔_.right-inverse-of
                                         Lookup↔Lookup′ q
                                     | _↔_.right-inverse-of ↦↔↦′ r
                                     | to∘from s = refl
    to∘from (rec p)            rewrite to∘from p = refl
    to∘from (lambda refl refl) = refl
    to∘from (const refl ps)    rewrite to⋆∘from⋆ ps = refl

    to⋆∘from⋆ :  {e v} (ps : e ⟶⋆′ v)  to⋆ (from⋆ ps)  ps
    to⋆∘from⋆ []       = refl
    to⋆∘from⋆ (p  ps) rewrite to∘from p | to⋆∘from⋆ ps = refl

-- The alternative semantics is deterministic.

Lookup′-deterministic :
   {c bs xs₁ xs₂ e₁ e₂} 
  Lookup′ c bs xs₁ e₁  Lookup′ c bs xs₂ e₂ 
  xs₁  xs₂ × e₁  e₂
Lookup′-deterministic p q =
  Lookup-deterministic
    (_↔_.from Lookup↔Lookup′ p) (_↔_.from Lookup↔Lookup′ q) refl

↦′-deterministic :
   {e xs es e₁ e₂} 
  e [ xs  es ]↦′ e₁  e [ xs  es ]↦′ e₂  e₁  e₂
↦′-deterministic p q =
  ↦-deterministic (_↔_.from ↦↔↦′ p) (_↔_.from ↦↔↦′ q)

⟶′-deterministic :  {e v₁ v₂}  e ⟶′ v₁  e ⟶′ v₂  v₁  v₂
⟶′-deterministic p q =
  ⟶-deterministic (_↔_.from ⟶↔⟶′ p) (_↔_.from ⟶↔⟶′ q)

-- The alternative semantics is proof-irrelevant.

Lookup′-proof-irrelevant :
   {c bs xs e}  Proof-irrelevant (Lookup′ c bs xs e)
Lookup′-proof-irrelevant (here p₁ p₂ p₃) (here q₁ q₂ q₃)
    rewrite _⇔_.to set⇔UIP C.Name-set p₁ q₁
          | _⇔_.to set⇔UIP (decidable⇒set (List.Dec._≟_ V._≟_)) p₂ q₂
          | _⇔_.to set⇔UIP Exp-set p₃ q₃
    = refl
Lookup′-proof-irrelevant (there p₁ p₂) (there q₁ q₂)
  rewrite _⇔_.to propositional⇔irrelevant
            (¬-propositional ext) p₁ q₁
        | Lookup′-proof-irrelevant p₂ q₂
  = refl

Lookup′-proof-irrelevant (here c≡c′ _ _) (there c≢c′ _) =
  ⊥-elim (c≢c′ c≡c′)
Lookup′-proof-irrelevant (there c≢c′ _) (here c≡c′ _ _) =
  ⊥-elim (c≢c′ c≡c′)

↦′-proof-irrelevant :
   {e xs es e′}  Proof-irrelevant (e [ xs  es ]↦′ e′)
↦′-proof-irrelevant ([] p) ([] q)
  rewrite _⇔_.to set⇔UIP Exp-set p q
  = refl
↦′-proof-irrelevant (p₁  p₂) (q₁  q₂)
  with ↦′-deterministic p₂ q₂
... | refl rewrite _⇔_.to set⇔UIP Exp-set p₁ q₁
                 | ↦′-proof-irrelevant p₂ q₂
  = refl

mutual

  ⟶′-proof-irrelevant :  {e v}  Proof-irrelevant (e ⟶′ v)
  ⟶′-proof-irrelevant (apply p₁ p₂ p₃) (apply q₁ q₂ q₃)
    with ⟶′-deterministic p₁ q₁
  ... | refl rewrite ⟶′-proof-irrelevant p₁ q₁
                with ⟶′-deterministic p₂ q₂
  ... | refl rewrite ⟶′-proof-irrelevant p₂ q₂
                   | ⟶′-proof-irrelevant p₃ q₃
             = refl
  ⟶′-proof-irrelevant (case p₁ p₂ p₃ p₄) (case q₁ q₂ q₃ q₄)
    with ⟶′-deterministic p₁ q₁
  ... | refl rewrite ⟶′-proof-irrelevant p₁ q₁
                with Lookup′-deterministic p₂ q₂
  ... | refl , refl rewrite Lookup′-proof-irrelevant p₂ q₂
                       with ↦′-deterministic p₃ q₃
  ... | refl rewrite ↦′-proof-irrelevant p₃ q₃
                   | ⟶′-proof-irrelevant p₄ q₄
    = refl
  ⟶′-proof-irrelevant (rec p) (rec q)
    rewrite ⟶′-proof-irrelevant p q
    = refl
  ⟶′-proof-irrelevant (lambda p₁ p₂) (lambda q₁ q₂)
    rewrite _⇔_.to set⇔UIP V.Name-set p₁ q₁
          | _⇔_.to set⇔UIP Exp-set p₂ q₂
          = refl
  ⟶′-proof-irrelevant (const p ps) (const q qs)
    rewrite _⇔_.to set⇔UIP C.Name-set p q
          | ⟶⋆′-proof-irrelevant ps qs
    = refl

  ⟶⋆′-proof-irrelevant :  {es vs}  Proof-irrelevant (es ⟶⋆′ vs)
  ⟶⋆′-proof-irrelevant []       []       = refl
  ⟶⋆′-proof-irrelevant (p  ps) (q  qs)
    rewrite ⟶′-proof-irrelevant p q
          | ⟶⋆′-proof-irrelevant ps qs
    = refl

-- The semantics is propositional.

⟶-propositional :  {e v}  Is-proposition (e  v)
⟶-propositional {e} {v} =    $⟨ ⟶′-proof-irrelevant 
  Proof-irrelevant (e ⟶′ v)  ↝⟨ _⇔_.from propositional⇔irrelevant 
  Is-proposition (e ⟶′ v)    ↝⟨ H-level.respects-surjection (_↔_.surjection $ inverse ⟶↔⟶′) 1 ⟩□
  Is-proposition (e  v)