------------------------------------------------------------------------
-- Encoders and decoders
------------------------------------------------------------------------

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

open import Atom

module Coding (atoms : χ-atoms) where

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

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import Injection equality-with-J using (Injective)
open import List equality-with-J using (foldr)
open import Maybe equality-with-J
open import Monad equality-with-J

open import Chi            atoms
open import Constants      atoms
open import Free-variables atoms
open import Values         atoms

open χ-atoms atoms

------------------------------------------------------------------------
-- General definitions

-- Representation functions.

record Rep {a b} (A : Set a) (B : Set b) : Set (a  b) where
  field
    -- Representation function.
    ⌜_⌝ : A  B

    -- ⌜_⌝ is injective.
    rep-injective : Injective ⌜_⌝

open Rep    public

-- An identity encoder.

id-rep :  {a} {A : Set a}  Rep A A
id-rep = record
  { ⌜_⌝           = id
  ; rep-injective = id
  }

-- Composition of representation functions.

infixr 9 _∘-rep_

_∘-rep_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
          Rep B C  Rep A B  Rep A C
r₁ ∘-rep r₂ = record
  { ⌜_⌝           = R₁.⌜_⌝  R₂.⌜_⌝
  ; rep-injective = λ {x y} 
      R₁.⌜ R₂.⌜ x    R₁.⌜ R₂.⌜ y    ↝⟨ R₁.rep-injective 
      R₂.⌜ x   R₂.⌜ y                 ↝⟨ R₂.rep-injective ⟩□
      x  y                              
  }
  where
  module R₁ = Rep r₁
  module R₂ = Rep r₂

-- Encoder/decoder pairs.

record Code {a b} (A : Set a) (B : Set b) : Set (a  b) where
  field
    -- Encoder.
    code : A  B

    -- Partial decoder.
    decode : B  Maybe A

    -- The decoder must decode encoded values successfully.
    decode∘code :  x  decode (code x)  just x

  -- The encoder is injective.

  code-injective : Injective code
  code-injective {x} {y} eq = ⊎.cancel-inj₂ (
    just x           ≡⟨ by decode∘code 
    decode (code x)  ≡⟨ by eq 
    decode (code y)  ≡⟨ by decode∘code ⟩∎
    just y           )

  -- Encoder/decoder pairs can be turned into representation
  -- functions.

  rep : Rep A B
  rep = record
    { ⌜_⌝           = code
    ; rep-injective = code-injective
    }

open Code    public

-- Converts bijections to encoders.

↔→Code :  {a b} {A : Set a} {B : Set b}  A  B  Code A B
↔→Code A↔B = record
  { code        = to
  ; decode      = λ b  just (from b)
  ; decode∘code = λ a 
      just (from (to a))  ≡⟨ cong just (left-inverse-of a) 
      just a              
  }
  where
  open _↔_ A↔B

-- An identity encoder.

id-code :  {a} {A : Set a}  Code A A
id-code = ↔→Code Bijection.id

-- Composition of encoders.

infixr 9 _∘-code_

_∘-code_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
           Code B C  Code A B  Code A C
c₁ ∘-code c₂ = record
  { code        = C₁.code  C₂.code
  ; decode      = λ c  C₁.decode c >>=′ C₂.decode
  ; decode∘code = λ a 
      C₁.decode (C₁.code (C₂.code a)) >>=′ C₂.decode  ≡⟨ cong (_>>=′ _) (C₁.decode∘code (C₂.code a)) 
      return (C₂.code a) >>=′ C₂.decode               ≡⟨⟩
      C₂.decode (C₂.code a)                           ≡⟨ by C₂.decode∘code ⟩∎
      return a                                        
  }
  where
  module C₁ = Code c₁
  module C₂ = Code c₂

------------------------------------------------------------------------
-- Some general definitions related to χ

-- Constructor applications can be encoded as expressions (that are
-- also constructor applications).

code-Consts :  λ (cd : Code Consts Exp) 
                 c  Constructor-application (Code.code cd c)
code-Consts = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  } , cd-cs
  where
  mutual

    cd : Consts  Exp
    cd (const c cs) = const c (cd⋆ cs)

    cd⋆ : List Consts  List Exp
    cd⋆ []       = []
    cd⋆ (c  cs) = cd c  cd⋆ cs

  mutual

    cd-cs :  c  Constructor-application (cd c)
    cd-cs (const c cs) = const c (cd⋆-cs cs)

    cd⋆-cs :  cs  Constructor-applications (cd⋆ cs)
    cd⋆-cs []       = []
    cd⋆-cs (c  cs) = cd-cs c  cd⋆-cs cs

  mutual

    dc : Exp  Maybe Consts
    dc (const c es) = const c ⟨$⟩ dc⋆ es
    dc _            = nothing

    dc⋆ : List Exp  Maybe (List Consts)
    dc⋆ []       = return []
    dc⋆ (e  es) = _∷_ ⟨$⟩ dc e  dc⋆ es

  mutual

    dc∘cd :  c  dc (cd c)  just c
    dc∘cd (const c cs) =
      const c ⟨$⟩ dc⋆ (cd⋆ cs)  ≡⟨ by (dc∘cd⋆ cs) 
      const c ⟨$⟩ return cs     ≡⟨ refl ⟩∎
      return (const c cs)       

    dc∘cd⋆ :  cs  dc⋆ (cd⋆ cs)  just cs
    dc∘cd⋆ [] = refl
    dc∘cd⋆ (c  cs) =
      _∷_ ⟨$⟩ dc (cd c)  dc⋆ (cd⋆ cs)  ≡⟨ by (dc∘cd c) 
      _∷_ ⟨$⟩ return c  dc⋆ (cd⋆ cs)   ≡⟨ by (dc∘cd⋆ cs) 
      _∷_ ⟨$⟩ return c  return cs      ≡⟨⟩
      return (c  cs)                   

-- Converts instances of the form Rep A Consts to Rep A Exp.

rep-Consts-Exp :  {a} {A : Set a}  r : Rep A Consts  
                 Rep A Exp
rep-Consts-Exp  r  = rep  proj₁ code-Consts  ∘-rep r

-- Represents something as an expression.

rep-as-Exp :  {a} {A : Set a}  r : Rep A Consts   A  Exp
rep-as-Exp = ⌜_⌝  rep-Consts-Exp 

-- rep-as-Exp returns constructor applications.

rep-const :
   {a} {A : Set a}  r : Rep A Consts 
  (x : A)  Constructor-application (rep-as-Exp x)
rep-const = proj₂ code-Consts  ⌜_⌝

-- rep-as-Exp returns closed expressions.

rep-closed :
   {a} {A : Set a}  r : Rep A Consts 
  (x : A)  Closed (rep-as-Exp x)
rep-closed = const→closed  rep-const

-- Constructor applications can be encoded as closed expressions.

code-Consts-Closed : Code Consts Closed-exp
Code.code code-Consts-Closed c =
  code  r = proj₁ code-Consts  c , const→closed (proj₂ code-Consts c)

Code.decode code-Consts-Closed (e , _) =
  decode  r = proj₁ code-Consts  e

Code.decode∘code code-Consts-Closed c =
  decode  r = proj₁ code-Consts  (code  r = proj₁ code-Consts  c)  ≡⟨ decode∘code  r = proj₁ code-Consts  c ⟩∎
  just c                                                              

-- Converts instances of the form Rep A Consts to Rep A Closed-exp.

rep-Consts-Closed-exp :
   {a} {A : Set a}  r : Rep A Consts   Rep A Closed-exp
rep-Consts-Closed-exp  r  = rep  r = code-Consts-Closed  ∘-rep r

-- rep-as-Exp returns values.

rep-value :
   {a} {A : Set a}  r : Rep A Consts 
  (x : A)  Value (rep-as-Exp x)
rep-value = const→value  rep-const

-- Some derived lemmas.

subst-rep :
   {a} {A : Set a}  r : Rep A Consts  (x : A) {y e} 
  rep-as-Exp x [ y  e ]  rep-as-Exp x
subst-rep x = subst-closed _ _ (rep-closed x)

substs-rep :
   {a} {A : Set a}  r : Rep A Consts  (x : A) ps 
  foldr  ye  _[ proj₁ ye  proj₂ ye ]) (rep-as-Exp x) ps 
  rep-as-Exp x
substs-rep x = substs-closed (rep-as-Exp x) (rep-closed x)

rep⇓rep :
   {a} {A : Set a}  r : Rep A Consts 
  (x : A)  rep-as-Exp x  rep-as-Exp x
rep⇓rep x = values-compute-to-themselves (rep-value x)

rep⇓≡rep :
   {a} {A : Set a}  r : Rep A Consts  {v}
  (x : A)  rep-as-Exp x  v  rep-as-Exp x  v
rep⇓≡rep x = values-only-compute-to-themselves (rep-value x)

------------------------------------------------------------------------
-- Specifications of how a number of types are encoded as χ
-- constructor applications

-- Encoder for booleans.

code-Bool : Code Bool Consts
code-Bool = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  }
  where
  cd : Bool  Consts
  cd true  = const c-true  []
  cd false = const c-false []

  dc : Consts  Maybe Bool
  dc (const c args) with c-true C.≟ c | c-false C.≟ c
  dc (const c [])   | yes _ | _     = return true
  dc (const c [])   | _     | yes _ = return false
  dc (const c _)    | _     | _     = nothing

  dc∘cd :  b  dc (cd b)  just b
  dc∘cd true with c-true C.≟ c-true
  ... | yes _   = refl
  ... | no  t≢t = ⊥-elim (t≢t refl)
  dc∘cd false with c-true C.≟ c-false | c-false C.≟ c-false
  ... | no  _   | no f≢f = ⊥-elim (f≢f refl)
  ... | yes t≡f | _      = ⊥-elim (C.distinct-codes→distinct-names
                                      ()) t≡f)
  ... | no _    | yes _  = refl

-- Encoder for natural numbers.

code-ℕ : Code  Consts
code-ℕ = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  }
  where
  cd :   Consts
  cd zero    = const c-zero []
  cd (suc n) = const c-suc (cd n  [])

  dc : Consts  Maybe 
  dc (const c args)     with c-zero C.≟ c | c-suc C.≟ c
  dc (const c [])       | yes eq | _      = return zero
  dc (const c (n  [])) | _      | yes eq = map suc (dc n)
  dc (const c _)        | _      | _      = nothing

  dc∘cd :  n  dc (cd n)  just n
  dc∘cd zero with c-zero C.≟ c-zero
  ... | yes _   = refl
  ... | no  z≢z = ⊥-elim (z≢z refl)
  dc∘cd (suc n) with c-zero C.≟ c-suc | c-suc C.≟ c-suc
  ... | no  _   | no s≢s = ⊥-elim (s≢s refl)
  ... | yes z≡s | _      = ⊥-elim (C.distinct-codes→distinct-names
                                      ()) z≡s)
  ... | no _    | yes _  =
    map suc (dc (cd n))  ≡⟨ by (dc∘cd n) 
    map suc (return n)   ≡⟨ refl ⟩∎
    return (suc n)       

-- Encoder for variables.

code-Var : Code Var Consts
code-Var = code-ℕ ∘-code ↔→Code V.countably-infinite

-- Encoder for constants.

code-Const : Code Const Consts
code-Const = code-ℕ ∘-code ↔→Code C.countably-infinite

-- Encoders for products.

module _ {a b} {A : Set a} {B : Set b} where

  private

    encode : (A  Consts)  (B  Consts)  A × B  Consts
    encode encA encB (x , y) = const c-pair (encA x  encB y  [])

  rep-× :  r : Rep A Consts   s : Rep B Consts  
          Rep (A × B) Consts
  rep-×  r   s  = record
    { ⌜_⌝           = encode ⌜_⌝ ⌜_⌝
    ; rep-injective = λ { {x₁ , x₂} {y₁ , y₂} 
        const c-pair ( x₁    x₂   []) 
        const c-pair ( y₁    y₂   [])    ↝⟨ lemma 

         x₁    y₁  ×  x₂    y₂       ↝⟨ Σ-map rep-injective rep-injective 

        x₁  y₁ × x₂  y₂                      ↝⟨ uncurry (cong₂ _,_) ⟩□

        (x₁ , x₂)  (y₁ , y₂)                   }
    }
    where
    lemma :
       {c₁ c₂ x₁ x₂ y₁ y₂} 
      Consts.const c₁ (x₁  x₂  [])  const c₂ (y₁  y₂  []) 
      x₁  y₁ × x₂  y₂
    lemma refl = refl , refl

  code-× :  c : Code A Consts   d : Code B Consts  
           Code (A × B) Consts
  code-×  c   d  = record
    { code        = cd
    ; decode      = dc
    ; decode∘code = dc∘cd
    }
    where
    cd : A × B  Consts
    cd = encode code code

    dc : Consts  Maybe (A × B)
    dc (const c args)         with c-pair C.≟ c
    dc (const c (x  y  [])) | yes _ = decode x >>=′ λ x 
                                        decode y >>=′ λ y 
                                        just (x , y)
    dc (const c args)         | _     = nothing

    dc∘cd :  x  dc (cd x)  just x
    dc∘cd (x , y) with c-pair C.≟ c-pair
    ... | no p≢p = ⊥-elim (p≢p refl)
    ... | yes _  =
      (decode  r = c  (code x) >>=′ λ x 
       decode  r = d  (code y) >>=′ λ y 
       just (x , y))                         ≡⟨ by (decode∘code  r = c ⦄) 

      (return x >>=′ λ x 
       decode  r = d  (code y) >>=′ λ y 
       just (x , y))                         ≡⟨⟩

      (decode  r = d  (code y) >>=′ λ y 
       just (x , y))                         ≡⟨ by (decode∘code  r = d ⦄) 

      (return y >>=′ λ y  just (x , y))     ≡⟨ refl ⟩∎

      return (x , y)                         

-- Encoders for lists.

module _ {a} {A : Set a} where

  private

    encode : (A  Consts)  List A  Consts
    encode enc []       = const c-nil []
    encode enc (x  xs) = const c-cons (enc x  encode enc xs  [])

  rep-List :  r : Rep A Consts   Rep (List A) Consts
  rep-List  c  = record
    { ⌜_⌝           = encode ⌜_⌝
    ; rep-injective = injective
    }
    where
    injective :  {xs ys}  encode ⌜_⌝ xs  encode ⌜_⌝ ys  xs  ys
    injective {[]}     {[]}     = λ _  refl
    injective {[]}     {_  _}  = λ ()
    injective {_  _}  {[]}     = λ ()
    injective {x  xs} {y  ys} =
      const c-cons ( x   encode ⌜_⌝ xs  []) 
      const c-cons ( y   encode ⌜_⌝ ys  [])      ↝⟨ lemma 

       x    y  × encode ⌜_⌝ xs  encode ⌜_⌝ ys  ↝⟨ Σ-map rep-injective injective 

      x  y × xs  ys                                ↝⟨ uncurry (cong₂ _∷_) ⟩□

      x  xs  y  ys                                
      where
      lemma :
         {c₁ x₁ y₁ c₂ x₂ y₂} 
        Consts.const c₁ (x₁  y₁  [])  const c₂ (x₂  y₂  []) 
        x₁  x₂ × y₁  y₂
      lemma refl = refl , refl

  code-List :  c : Code A Consts   Code (List A) Consts
  code-List  c  = record
    { code        = cd
    ; decode      = dc
    ; decode∘code = dc∘cd
    }
    where
    cd : List A  Consts
    cd = encode code

    dc : Consts  Maybe (List A)
    dc (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    dc (const c [])             | yes eq | _      = return []
    dc (const c′ (x  xs  [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode x  dc xs
    dc (const c args) | _ | _ = nothing

    dc∘cd :  x  dc (cd x)  just x
    dc∘cd [] with c-nil C.≟ c-nil
    ... | yes _   = refl
    ... | no  n≢n = ⊥-elim (n≢n refl)
    dc∘cd (x  xs) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                        ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ decode  r = c  (code x)  dc (cd xs)  ≡⟨ by (decode∘code  r = c ⦄) 
      _∷_ ⟨$⟩ return x  dc (cd xs)                   ≡⟨ by (dc∘cd xs) 
      _∷_ ⟨$⟩ return x  return xs                    ≡⟨⟩
      return (x  xs)                                 

-- Encoder for lists of variables.

code-Var⋆ : Code (List Var) Consts
code-Var⋆ = code-List  code-Var 

private

  module Var   = Code code-Var
  module Var⋆  = Code code-Var⋆
  module Const = Code code-Const

  -- Encoder for the abstract syntax.

  mutual

    code-E : Exp  Consts
    code-E (apply e₁ e₂) = const c-apply (code-E e₁  code-E e₂  [])
    code-E (lambda x e)  = const c-lambda (code  code-Var  x  code-E e  [])
    code-E (case e bs)   = const c-case (code-E e  code-B⋆ bs  [])
    code-E (rec x e)     = const c-rec (code  code-Var  x  code-E e  [])
    code-E (var x)       = const c-var (code  code-Var  x  [])
    code-E (const c es)  = const c-const (code  code-Const  c  code-⋆ es  [])

    code-B : Br  Consts
    code-B (branch c xs e) =
      const c-branch
        (code  code-Const  c  code  code-Var⋆  xs  code-E e  [])

    -- TODO: One could presumably use sized types to avoid repetitive
    -- code. However, I did not want to use sized types in the
    -- specification of χ.

    code-⋆ : List Exp  Consts
    code-⋆ []       = const c-nil []
    code-⋆ (e  es) = const c-cons (code-E e  code-⋆ es  [])

    code-B⋆ : List Br  Consts
    code-B⋆ []       = const c-nil []
    code-B⋆ (b  bs) = const c-cons (code-B b  code-B⋆ bs  [])

  mutual

    decode-E : Consts  Maybe Exp
    decode-E (const c args) with c-apply  C.≟ c
                               | c-lambda C.≟ c
                               | c-case   C.≟ c
                               | c-rec    C.≟ c
                               | c-var    C.≟ c
                               | c-const  C.≟ c

    decode-E (const c (e₁  e₂  [])) | yes eq | _ | _ | _ | _ | _ =
      apply ⟨$⟩ decode-E e₁  decode-E e₂

    decode-E (const c (x  e  [])) | _ | yes eq | _ | _ | _ | _ =
      lambda ⟨$⟩ decode  code-Var  x  decode-E e

    decode-E (const c (e  bs  [])) | _ | _ | yes eq | _ | _ | _ =
      case ⟨$⟩ decode-E e  decode-B⋆ bs

    decode-E (const c (x  e  [])) | _ | _ | _ | yes eq | _ | _ =
      rec ⟨$⟩ decode  code-Var  x  decode-E e

    decode-E (const c (x  [])) | _ | _ | _ | _ | yes eq | _ =
      var ⟨$⟩ decode  code-Var  x

    decode-E (const c (c′  es  [])) | _ | _ | _ | _ | _ | yes eq =
      const ⟨$⟩ decode  code-Const  c′  decode-⋆ es

    decode-E (const c args) | _ | _ | _ | _ | _ | _ = nothing

    decode-B : Consts  Maybe Br
    decode-B (const c args)               with c-branch C.≟ c
    decode-B (const c (c′  xs  e  [])) | yes eq =
      branch ⟨$⟩ decode  code-Const  c′
                decode  code-Var⋆  xs
                decode-E e
    decode-B (const c args) | _ = nothing

    decode-⋆ : Consts  Maybe (List Exp)
    decode-⋆ (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    decode-⋆ (const c [])             | yes eq | _      = return []
    decode-⋆ (const c′ (e  es  [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode-E e  decode-⋆ es
    decode-⋆ (const c args) | _ | _ = nothing

    decode-B⋆ : Consts  Maybe (List Br)
    decode-B⋆ (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    decode-B⋆ (const c [])             | yes eq | _      = return []
    decode-B⋆ (const c′ (b  bs  [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode-B b  decode-B⋆ bs
    decode-B⋆ (const c args) | _ | _ = nothing

  mutual

    decode∘code-E :  e  decode-E (code-E e)  just e

    decode∘code-E (apply e₁ e₂) with c-apply C.≟ c-apply
    ... | no c≢c = ⊥-elim (c≢c refl)
    ... | yes _  =
      apply ⟨$⟩ decode-E (code-E e₁)  decode-E (code-E e₂)  ≡⟨ by (decode∘code-E e₁) 
      apply ⟨$⟩ return e₁  decode-E (code-E e₂)             ≡⟨ by (decode∘code-E e₂) 
      apply ⟨$⟩ return e₁  return e₂                        ≡⟨⟩
      return (apply e₁ e₂)                                   

    decode∘code-E (lambda x e) with c-apply  C.≟ c-lambda
                                  | c-lambda C.≟ c-lambda
    ... | _       | no l≢l = ⊥-elim (l≢l refl)
    ... | yes a≡l | _      = ⊥-elim (C.distinct-codes→distinct-names
                                        ()) a≡l)
    ... | no _    | yes _  =
      lambda ⟨$⟩ Var.decode (code  code-Var  x)  decode-E (code-E e)  ≡⟨ by Var.decode∘code 
      lambda ⟨$⟩ return x  decode-E (code-E e)                          ≡⟨ by (decode∘code-E e) 
      lambda ⟨$⟩ return x  return e                                     ≡⟨⟩
      return (lambda x e)                                                

    decode∘code-E (case e bs) with c-apply  C.≟ c-case
                                 | c-lambda C.≟ c-case
                                 | c-case   C.≟ c-case
    ... | _       | _       | no c≢c = ⊥-elim (c≢c refl)
    ... | _       | yes l≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                  ()) l≡c)
    ... | yes a≡c | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                  ()) a≡c)
    ... | no _    | no _    | yes _  =
      case ⟨$⟩ decode-E (code-E e)  decode-B⋆ (code-B⋆ bs)  ≡⟨ by (decode∘code-E e) 
      case ⟨$⟩ return e  decode-B⋆ (code-B⋆ bs)             ≡⟨ by (decode∘code-B⋆ bs) 
      case ⟨$⟩ return e  return bs                          ≡⟨⟩
      return (case e bs)                                     

    decode∘code-E (rec x e) with c-apply  C.≟ c-rec
                               | c-lambda C.≟ c-rec
                               | c-case   C.≟ c-rec
                               | c-rec    C.≟ c-rec
    ... | _       | _       | _       | no r≢r = ⊥-elim (r≢r refl)
    ... | _       | _       | yes c≡r | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                            ()) c≡r)
    ... | _       | yes l≡r | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                            ()) l≡r)
    ... | yes a≡r | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                            ()) a≡r)
    ... | no _    | no _    | no _    | yes _  =
      rec ⟨$⟩ Var.decode (code  code-Var  x)  decode-E (code-E e)  ≡⟨ by Var.decode∘code 
      rec ⟨$⟩ return x  decode-E (code-E e)                          ≡⟨ by (decode∘code-E e) 
      rec ⟨$⟩ return x  return e                                     ≡⟨⟩
      return (rec x e)                                                

    decode∘code-E (var x) with c-apply  C.≟ c-var
                             | c-lambda C.≟ c-var
                             | c-case   C.≟ c-var
                             | c-rec    C.≟ c-var
                             | c-var    C.≟ c-var
    ... | _       | _       | _       | _       | no v≢v = ⊥-elim (v≢v refl)
    ... | _       | _       | _       | yes r≡v | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                      ()) r≡v)
    ... | _       | _       | yes c≡v | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                      ()) c≡v)
    ... | _       | yes l≡v | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                      ()) l≡v)
    ... | yes a≡v | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                      ()) a≡v)
    ... | no _    | no _    | no _    | no _    | yes _  =
      var ⟨$⟩ Var.decode (code  code-Var  x)  ≡⟨ by Var.decode∘code 
      var ⟨$⟩ return x                          ≡⟨ refl ⟩∎
      return (var x)                            

    decode∘code-E (const c es) with c-apply  C.≟ c-const
                                  | c-lambda C.≟ c-const
                                  | c-case   C.≟ c-const
                                  | c-rec    C.≟ c-const
                                  | c-var    C.≟ c-const
                                  | c-const  C.≟ c-const
    ... | _       | _       | _       | _       | _       | no c≢c = ⊥-elim (c≢c refl)
    ... | _       | _       | _       | _       | yes v≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                                ()) v≡c)
    ... | _       | _       | _       | yes r≡c | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                                ()) r≡c)
    ... | _       | _       | yes c≡c | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                                ()) c≡c)
    ... | _       | yes l≡c | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                                ()) l≡c)
    ... | yes a≡c | _       | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                                ()) a≡c)
    ... | no _    | no _    | no _    | no _    | no _    | yes _  =
      const ⟨$⟩ Const.decode (code  code-Const  c)  decode-⋆ (code-⋆ es)  ≡⟨ by Const.decode∘code 
      const ⟨$⟩ return c  decode-⋆ (code-⋆ es)                              ≡⟨ by (decode∘code-⋆ es) 
      const ⟨$⟩ return c  return es                                         ≡⟨⟩
      return (const c es)                                                    

    decode∘code-B :  b  decode-B (code-B b)  just b
    decode∘code-B (branch c xs e) with c-branch C.≟ c-branch
    ... | no b≢b = ⊥-elim (b≢b refl)
    ... | yes _  =
      branch ⟨$⟩ Const.decode (code  code-Const  c) 
                 Var⋆.decode (code  code-Var⋆  xs) 
                 decode-E (code-E e)                         ≡⟨ by Const.decode∘code 

      branch ⟨$⟩ return c 
                 Var⋆.decode (code  code-Var⋆  xs) 
                 decode-E (code-E e)                         ≡⟨ by Var⋆.decode∘code 

      branch ⟨$⟩ return c  return xs  decode-E (code-E e)  ≡⟨ by (decode∘code-E e) 

      branch ⟨$⟩ return c  return xs  return e             ≡⟨⟩

      return (branch c xs e)                                 

    decode∘code-⋆ :  es  decode-⋆ (code-⋆ es)  just es
    decode∘code-⋆ [] with c-nil C.≟ c-nil
    ... | no  n≢n = ⊥-elim (n≢n refl)
    ... | yes _   = refl
    decode∘code-⋆ (e  es) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                        ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ decode-E (code-E e)  decode-⋆ (code-⋆ es)  ≡⟨ by (decode∘code-E e) 
      _∷_ ⟨$⟩ return e  decode-⋆ (code-⋆ es)             ≡⟨ by (decode∘code-⋆ es) 
      _∷_ ⟨$⟩ return e  return es                        ≡⟨⟩
      return (e  es)                                     

    decode∘code-B⋆ :  bs  decode-B⋆ (code-B⋆ bs)  just bs
    decode∘code-B⋆ [] with c-nil C.≟ c-nil
    ... | no  n≢n = ⊥-elim (n≢n refl)
    ... | yes _   = refl
    decode∘code-B⋆ (b  bs) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                        ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ decode-B (code-B b)  decode-B⋆ (code-B⋆ bs)  ≡⟨ by (decode∘code-B b) 
      _∷_ ⟨$⟩ return b  decode-B⋆ (code-B⋆ bs)             ≡⟨ by (decode∘code-B⋆ bs) 
      _∷_ ⟨$⟩ return b  return bs                          ≡⟨⟩
      return (b  bs)                                       

code-Exp : Code Exp Consts
Code.code        code-Exp = code-E
Code.decode      code-Exp = decode-E
Code.decode∘code code-Exp = decode∘code-E

code-Br : Code Br Consts
Code.code        code-Br = code-B
Code.decode      code-Br = decode-B
Code.decode∘code code-Br = decode∘code-B

code-Exps : Code (List Exp) Consts
Code.code        code-Exps = code-⋆
Code.decode      code-Exps = decode-⋆
Code.decode∘code code-Exps = decode∘code-⋆

code-Brs : Code (List Br) Consts
Code.code        code-Brs = code-B⋆
Code.decode      code-Brs = decode-B⋆
Code.decode∘code code-Brs = decode∘code-B⋆

-- Encoder for closed expressions.

code-Closed : Code Closed-exp Consts
Code.code   code-Closed = code  code-Exp   proj₁
Code.decode code-Closed c with decode  code-Exp  c
... | nothing = nothing
... | just e  with closed? e
...   | yes cl = just (e , cl)
...   | no _   = nothing
Code.decode∘code code-Closed (c , cl)
  with decode  r = code-Exp  (code  code-Exp  c)
     | decode∘code  r = code-Exp  c
... | .(just c) | refl with closed? c
...   | no  ¬cl = ⊥-elim (¬cl cl)
...   | yes cl′ =
  cong just (closed-equal-if-expressions-equal refl)