------------------------------------------------------------------------
-- Some χ program combinators
------------------------------------------------------------------------

module Combinators where

open import Equality.Propositional
open import Prelude hiding (if_then_else_; not; const)
open import Tactic.By

open import Equality.Decision-procedures equality-with-J
import Nat equality-with-J as Nat

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Constants      χ-ℕ-atoms
open import Deterministic  χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms
open import Reasoning      χ-ℕ-atoms
open import Termination    χ-ℕ-atoms
open import Values         χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

import Coding.Instances.Nat

------------------------------------------------------------------------
-- A non-terminating expression

loop : Exp
loop = rec v-x (var v-x)

loop-closed : Closed loop
loop-closed =
  Closed′-closed-under-rec $
  Closed′-closed-under-var (inj₁ refl)

¬loop⇓ : ¬ Terminates loop
¬loop⇓ (_ , p) = lemma p
  where
  lemma :  {w}  ¬ loop  w
  lemma (rec p) with v-x V.≟ v-x
  ... | no  x≢x = x≢x refl
  ... | yes _   = lemma p

------------------------------------------------------------------------
-- Natural numbers

-- Equality of natural numbers.

private

  equal-ℕ′ : Exp
  equal-ℕ′ =
    rec v-equal (lambda v-m (lambda v-n (case (var v-m) branches)))
    module Equal-ℕ where
    zero-branches =
      branch c-zero [] (const c-true []) 
      branch c-suc (v-n  []) (const c-false []) 
      []

    suc-branches =
      branch c-zero [] (const c-false []) 
      branch c-suc (v-n  []) (
        apply (apply (var v-equal) (var v-m)) (var v-n)) 
      []

    branches =
      branch c-zero [] (case (var v-n) zero-branches) 
      branch c-suc (v-m  []) (case (var v-n) suc-branches) 
      []

equal-ℕ : Exp  Exp  Exp
equal-ℕ e₁ e₂ = apply (apply equal-ℕ′ e₁) e₂

equal-ℕ-closed :
   {xs e₁ e₂} 
  Closed′ xs e₁  Closed′ xs e₂  Closed′ xs (equal-ℕ e₁ e₂)
equal-ℕ-closed {xs} cl-e₁ cl-e₂ =
  Closed′-closed-under-apply
    (Closed′-closed-under-apply
       (from-⊎ (closed′? equal-ℕ′ xs))
       cl-e₁)
    cl-e₂

equal-ℕ-correct :
   m n 
  equal-ℕ  m   n  
   Prelude.if m Nat.≟ n then true else false 
equal-ℕ-correct m n =
  equal-ℕ  m   n                                ⟶⟨⟩

  apply (apply equal-ℕ′  m )  n                 ⟶⟨ apply (apply (rec lambda) (rep⇓rep m) lambda) (rep⇓rep n) 

  case ( m  [ v-n   n  ])
    (branches [ v-equal  equal-ℕ′ ]B⋆
              [ v-m   m  ]B⋆ [ v-n   n  ]B⋆)  ≡⟨ by (subst-rep m) ⟩⟶

  case  m 
    (branches [ v-equal  equal-ℕ′ ]B⋆
              [ v-m   m  ]B⋆ [ v-n   n  ]B⋆)  ⇓⟨ lemma m n ⟩■

   Prelude.if m Nat.≟ n then true else false 
  where
  open Equal-ℕ

  lemma :
     m n 
    case  m 
      (branches [ v-equal  equal-ℕ′ ]B⋆
                [ v-m   m  ]B⋆ [ v-n   n  ]B⋆)
      
     Prelude.if m Nat.≟ n then true else false 
  lemma zero zero =
    case  zero 
      (branches [ v-equal  equal-ℕ′ ]B⋆
                [ v-m   zero  ]B⋆ [ v-n   zero  ]B⋆)  ⟶⟨ _⇓_.case (rep⇓rep zero) here [] 

    case  zero  zero-branches                             ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (true  Bool)) ⟩■

     true  Bool 

  lemma zero (suc n) =
    case  zero 
      (branches [ v-equal  equal-ℕ′ ]B⋆
                [ v-m   zero  ]B⋆ [ v-n   suc n  ]B⋆)  ⟶⟨ case (rep⇓rep zero) here [] 

    case  suc n  zero-branches                             ⇓⟨ case (rep⇓rep (suc n)) (there  ()) here) ( [])
                                                                     (rep⇓rep (false  Bool)) ⟩■
     false  Bool 

  lemma (suc m) zero =
    case  suc m 
      (branches [ v-equal  equal-ℕ′ ]B⋆
                [ v-m   suc m  ]B⋆ [ v-n   zero  ]B⋆)     ⟶⟨ case (rep⇓rep (suc m)) (there  ()) here) ( []) 

    case  zero 
      (suc-branches [ v-equal  equal-ℕ′ ]B⋆ [ v-m   m  ]B⋆
                    [ v-n   zero  ]B⋆)                       ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (false  Bool)) ⟩■

     false  Bool 

  lemma (suc m) (suc n) =
    case  suc m 
      (branches [ v-equal  equal-ℕ′ ]B⋆
                [ v-m   suc m  ]B⋆ [ v-n   suc n  ]B⋆)    ⟶⟨ case (rep⇓rep (suc m)) (there  ()) here) ( []) 

    case ( suc n  [ v-m   m  ])
      (suc-branches [ v-equal  equal-ℕ′ ]B⋆ [ v-m   m  ]B⋆
                    [ v-n   suc n  ]B⋆)                      ≡⟨ by (subst-rep (suc n)) ⟩⟶

    case  suc n 
      (suc-branches [ v-equal  equal-ℕ′ ]B⋆ [ v-m   m  ]B⋆
                    [ v-n   suc n  ]B⋆)                      ⟶⟨ case (rep⇓rep (suc n)) (there  ()) here) ( []) 

    apply (apply equal-ℕ′ ( m  [ v-n   n  ]))  n         ≡⟨ by (subst-rep m) ⟩⟶

    apply (apply equal-ℕ′  m )  n                           ⟶⟨⟩

    equal-ℕ  m   n                                          ⇓⟨ equal-ℕ-correct m n 

     Prelude.if m Nat.≟ n then true else false                ≡⟨ by lem ⟩⟶

     Prelude.if suc m Nat.≟ suc n then true else false        ■⟨ rep-value (Prelude.if suc m Nat.≟ suc n then true else false) 
    where
    lem : Prelude.if m Nat.≟ n then true else false 
          Prelude.if suc m Nat.≟ suc n then true else false
    lem with m Nat.≟ n
    ... | yes _ = refl
    ... | no  _ = refl

private

  equal-ℕ-correct′ :
     m n {v} 
    equal-ℕ  m   n   v 
    v   Prelude.if m Nat.≟ n then true else false 
  equal-ℕ-correct′ m n p =
    ⇓-deterministic p (equal-ℕ-correct m n)

-- Membership of a list of natural numbers.

private

  member′ : Exp
  member′ =
    lambda v-x body
    module Member where
    cons-branches =
      branch c-true [] (const c-true []) 
      branch c-false [] (apply (var v-member) (var v-xs)) 
      []

    branches =
      branch c-nil [] (const c-false []) 
      branch c-cons (v-y  v-xs  []) (
        case (equal-ℕ (var v-x) (var v-y))
          cons-branches) 
      []

    body = rec v-member (lambda v-xs (case (var v-xs) branches))

    body-closed :  {xs}  Closed′ (v-x  xs) body
    body-closed {xs} = from-⊎ (closed′? body (v-x  xs))

member : Exp  Exp  Exp
member m ns = apply (apply member′ m) ns

member-closed :
   {xs m ns} 
  Closed′ xs m  Closed′ xs ns  Closed′ xs (member m ns)
member-closed cl-m cl-ns =
  Closed′-closed-under-apply
    (Closed′-closed-under-apply
       (Closed′-closed-under-lambda Member.body-closed)
       cl-m)
    cl-ns

member-correct :
   m ns 
  member  m   ns  
   Prelude.if V.member m ns then true else false 
member-correct m ns =
  member  m   ns                                                    ⟶⟨⟩

  apply (apply member′  m )  ns                                     ⟶⟨ apply (apply lambda (rep⇓rep m) (rec lambda)) (rep⇓rep ns) 

  case  ns 
    (branches [ v-x   m  ]B⋆ [ v-member  body [ v-x   m  ] ]B⋆)  ⇓⟨ lemma ns ⟩■

   Prelude.if V.member m ns then true else false 
  where
  open Member

  lemma :
     ns 
    case  ns  (branches [ v-x   m  ]B⋆
                             [ v-member  body [ v-x   m  ] ]B⋆)
      
     Prelude.if V.member m ns then true else false 
  lemma [] =
    case  []  List  
      (branches [ v-x   m  ]B⋆
                [ v-member  body [ v-x   m  ] ]B⋆)           ⇓⟨ case (rep⇓rep ([]  List )) here [] (const []) ⟩■

     false  Bool 

  lemma (n  ns) =
    case  n List.∷ ns 
      (branches [ v-x   m  ]B⋆
                [ v-member  body [ v-x   m  ] ]B⋆)         ⟶⟨ case (rep⇓rep (n List.∷ ns)) (there  ()) here) (  []) 

    case (equal-ℕ   m  [ v-member  body [ v-x   m  ] ]
                          [ v-xs   ns  ] [ v-y   n  ] 
                   n )
      (cons-branches [ v-x   m  ]B⋆
                     [ v-member  body [ v-x   m  ] ]B⋆
                     [ v-xs   ns  ]B⋆ [ v-y   n  ]B⋆)    ≡⟨ ⟨by⟩ (substs-rep m ((v-y ,  n )  (v-xs ,  ns ) 
                                                                                      (v-member , body [ v-x   m  ])  [])) ⟩⟶
    case (equal-ℕ  m   n )
      ( cons-branches [ v-x   m  ]B⋆ 
                       [ v-member  body [ v-x   m  ] ]B⋆
                       [ v-xs   ns  ]B⋆ [ v-y   n  ]B⋆)  ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _  m  (from-⊎ (v-x ∈?-B⋆ cons-branches))) ⟩⟶

    case (equal-ℕ  m   n )
       cons-branches [ v-member  body [ v-x   m  ] ]B⋆
                      [ v-xs   ns  ]B⋆ [ v-y   n  ]B⋆   ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _ _
                                                                          λ { (._ , ._ , ._ , inj₁ refl        , const _ ()        , _)
                                                                            ; (._ , ._ , ._ , inj₂ (inj₁ refl) , y∈FV[body[x←m]ns] , _) 
                                                                              Closed′-closed-under-apply
                                                                                (Closed′-closed-under-subst body-closed (rep-closed m))
                                                                                (rep-closed ns)
                                                                                v-y  ()) y∈FV[body[x←m]ns]
                                                                            ; (_ , _ , _ , (inj₂ (inj₂ ())) , _) }) ⟩⟶
    case (equal-ℕ  m   n )
      (cons-branches [ v-member  body [ v-x   m  ] ]B⋆
                     [ v-xs   ns  ]B⋆)                      ⇓⟨ lemma′ (m Nat.≟ n) (equal-ℕ-correct m n) ⟩■

     Prelude.if V.member m (n  ns) then true else false 
    where
    lemma′ :
      (m≟n : Dec (m  n)) 
      equal-ℕ  m   n 
        
       Prelude.if m≟n then true else false  
      case (equal-ℕ  m   n )
        (cons-branches [ v-member  body [ v-x   m  ] ]B⋆
                       [ v-xs   ns  ]B⋆)
        
       Prelude.if V.member m (n  ns) then true else false 
    lemma′ (yes m≡n) hyp =
      case (equal-ℕ  m   n )
        (cons-branches [ v-member  body [ v-x   m  ] ]B⋆
                       [ v-xs   ns  ]B⋆)                    ⟶⟨ case hyp here [] 

       true  Bool                                           ≡⟨ cong ⌜_⌝ lem ⟩⟶

       Prelude.if V.member m (n  ns) then true else false   ■⟨ rep-value (Prelude.if V.member m (n  ns) then true else false) 
      where
      lem : true  Prelude.if V.member m (n  ns) then true else false
      lem with m Nat.≟ n
      ... | yes _   = refl
      ... | no  m≢n = ⊥-elim (m≢n m≡n)

    lemma′ (no m≢n) hyp =
      case (equal-ℕ  m   n )
        (cons-branches [ v-member  body [ v-x   m  ] ]B⋆
                       [ v-xs   ns  ]B⋆)                    ⟶⟨ case hyp (there  ()) here) [] 

      apply (body [ v-x   m  ] [ v-xs   ns  ])  ns     ≡⟨ by (subst-closed v-x  ns 
                                                                        (Closed′-closed-under-subst body-closed (rep-closed m))) ⟩⟶

      apply (body [ v-x   m  ])  ns                       ⟶⟨ apply (rec lambda) (rep⇓rep ns) 

      case  ns 
        (branches [ v-x   m  ]B⋆
                  [ v-member  body [ v-x   m  ] ]B⋆)       ⇓⟨ lemma ns 

       Prelude.if V.member m      ns  then true else false   ≡⟨ cong ⌜_⌝ lem ⟩⟶

       Prelude.if V.member m (n  ns) then true else false   ■⟨ rep-value (Prelude.if V.member m (n  ns) then true else false) 
      where
      lem : Prelude.if V.member m      ns  then true else false 
            Prelude.if V.member m (n  ns) then true else false
      lem with m Nat.≟ n
      ... | yes m≡n = ⊥-elim (m≢n m≡n)
      ... | no  _   with V.member m ns
      ...   | yes _ = refl
      ...   | no  _ = refl

------------------------------------------------------------------------
-- Booleans

-- If-then-else.

infix 5 if_then_else_

if_then_else_ : Exp  Exp  Exp  Exp
if c then t else f =
  case c (branch c-true  [] t 
          branch c-false [] f 
          [])

if-then-else-closed :
   {xs c t f} 
  Closed′ xs c  Closed′ xs t  Closed′ xs f 
  Closed′ xs (if c then t else f)
if-then-else-closed c-cl t-cl f-cl =
  Closed′-closed-under-case
    c-cl
    λ where
      (inj₁ refl)         t-cl
      (inj₂ (inj₁ refl))  f-cl
      (inj₂ (inj₂ ()))

if-then-else-correct :
   {A : Set}  cA : Rep A Consts  {e₁ e₂ e₃}
  (b₁ : Bool) (v₂ v₃ : A) 
  e₁   b₁   e₂   v₂   e₃   v₃  
  if e₁ then e₂ else e₃   Prelude.if b₁ then v₂ else v₃ 
if-then-else-correct true  _ _ e₁⇓ e₂⇓ e₃⇓ = case e₁⇓ here [] e₂⇓
if-then-else-correct false _ _ e₁⇓ e₂⇓ e₃⇓ =
  case e₁⇓ (there  ()) here) [] e₃⇓

-- Negation of booleans.

not : Exp  Exp
not e = if e then  false  Bool  else  true  Bool 

not-closed :  {xs e}  Closed′ xs e  Closed′ xs (not e)
not-closed cl-e =
  if-then-else-closed
    cl-e
    (Closed→Closed′ (from-⊎ (closed?  false  Bool )))
    (Closed→Closed′ (from-⊎ (closed?  true   Bool )))

not-correct :  {e} b  e   b   not e   Prelude.not b 
not-correct b e⇓ =
  if-then-else-correct b false true
    e⇓ (rep⇓rep (false  Bool)) (rep⇓rep (true  Bool))

-- Conjunction.

and : Exp  Exp  Exp
and e₁ e₂ = if e₁ then e₂ else  false  Bool 

and-closed :
   {xs e₁ e₂}  Closed′ xs e₁  Closed′ xs e₂  Closed′ xs (and e₁ e₂)
and-closed cl-e₁ cl-e₂ =
  if-then-else-closed
    cl-e₁
    cl-e₂
    (Closed→Closed′ (from-⊎ (closed?  false  Bool )))

and-correct :
   {e₁ e₂} b₁ b₂ 
  e₁   b₁   e₂   b₂  
  and e₁ e₂   b₁  b₂ 
and-correct b₁ b₂ e₁⇓ e₂⇓ =
  if-then-else-correct b₁ b₂ false e₁⇓ e₂⇓ (rep⇓rep (false  Bool))

-- Disjunction.

or : Exp  Exp  Exp
or e₁ e₂ = if e₁ then  true  Bool  else e₂

or-closed :
   {xs e₁ e₂}  Closed′ xs e₁  Closed′ xs e₂  Closed′ xs (or e₁ e₂)
or-closed cl-e₁ cl-e₂ =
  if-then-else-closed
    cl-e₁
    (Closed→Closed′ (from-⊎ (closed?  true  Bool )))
    cl-e₂

or-correct :
   {e₁ e₂} b₁ b₂ 
  e₁   b₁   e₂   b₂  
  or e₁ e₂   b₁  b₂ 
or-correct b₁ b₂ e₁⇓ e₂⇓ =
  if-then-else-correct b₁ true b₂ e₁⇓ (rep⇓rep (true  Bool)) e₂⇓

-- Equality of booleans.

equal-Bool : Exp  Exp  Exp
equal-Bool e₁ e₂ =
  if e₁ then e₂ else not e₂

equal-Bool-closed :
   {xs e₁ e₂} 
  Closed′ xs e₁  Closed′ xs e₂  Closed′ xs (equal-Bool e₁ e₂)
equal-Bool-closed cl-e₁ cl-e₂ =
  if-then-else-closed cl-e₁ cl-e₂ (not-closed cl-e₂)

equal-Bool-correct :
   {e₁ e₂} b₁ b₂ 
  e₁   b₁   e₂   b₂  
  equal-Bool e₁ e₂   Prelude.if b₁ Bool.≟ b₂ then true else false 
equal-Bool-correct {e₁} {e₂} b₁ b₂ e₁⇓ e₂⇓ =
  equal-Bool e₁ e₂                                  ⇓⟨ if-then-else-correct b₁ b₂ (Prelude.not b₂) e₁⇓ e₂⇓ (not-correct b₂ e₂⇓) 
   Prelude.if b₁ then b₂ else Prelude.not b₂      ≡⟨ cong ⌜_⌝ (lemma b₁ b₂) ⟩⟶
   Prelude.if b₁ Bool.≟ b₂ then true else false   ■⟨ rep-value (Prelude.if b₁ Bool.≟ b₂ then true else false) 
  where
  lemma :
     b₁ b₂ 
    Prelude.if b₁ then b₂ else Prelude.not b₂ 
    Prelude.if b₁ Bool.≟ b₂ then true else false
  lemma true  true  = refl
  lemma true  false = refl
  lemma false true  = refl
  lemma false false = refl

-- An internal decoding function for booleans.

decode-Bool : Exp  Exp
decode-Bool e =
  case e
    (branch c-const (v-c  v-es  [])
       (equal-ℕ (var v-c)  c-true )  [])

decode-Bool-closed :
   {xs e}  Closed′ xs e  Closed′ xs (decode-Bool e)
decode-Bool-closed cl-e =
  Closed′-closed-under-case
    cl-e
    λ where
      (inj₁ refl)  equal-ℕ-closed
                      (Closed′-closed-under-var
                         (from-⊎ (V.member v-c (v-c  v-es  _))))
                      (Closed→Closed′ (rep-closed c-true))
      (inj₂ ())

decode-Bool-correct :
   {e} (b : Bool) 
  e    b   Exp   decode-Bool e   b 
decode-Bool-correct true e⇓ =
  case e⇓ here (  []) (equal-ℕ-correct c-true c-true)
decode-Bool-correct false e⇓ =
  case e⇓ here (  []) (equal-ℕ-correct c-false c-true)