open import Atom
module Coding (atoms : χ-atoms) where
open import Equality.Propositional
open import Prelude hiding (const)
open import Tactic.By.Propositional
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J as Eq using (_≃_)
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
record Rep {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
field
⌜_⌝ : A → B
rep-injective : Injective ⌜_⌝
open Rep ⦃ … ⦄ public
id-rep : ∀ {a} {A : Type a} → Rep A A
id-rep = record
{ ⌜_⌝ = id
; rep-injective = id
}
infixr 9 _∘-rep_
_∘-rep_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type 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₂
record Code {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
field
code : A → B
decode : B → Maybe A
decode∘code : ∀ x → decode (code x) ≡ just x
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 ∎)
rep : Rep A B
rep = record
{ ⌜_⌝ = code
; rep-injective = code-injective
}
open Code ⦃ … ⦄ public
≃→Code : ∀ {a b} {A : Type a} {B : Type 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
id-code : ∀ {a} {A : Type a} → Code A A
id-code = ≃→Code Eq.id
infixr 9 _∘-code_
_∘-code_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type 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₂
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) ∎
rep-Consts-Exp : ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ →
Rep A Exp
rep-Consts-Exp ⦃ r ⦄ = rep ⦃ proj₁ code-Consts ⦄ ∘-rep r
rep-as-Exp : ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ → A → Exp
rep-as-Exp = ⌜_⌝ ⦃ rep-Consts-Exp ⦄
rep-const :
∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
(x : A) → Constructor-application (rep-as-Exp x)
rep-const = proj₂ code-Consts ∘ ⌜_⌝
rep-closed :
∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
(x : A) → Closed (rep-as-Exp x)
rep-closed = const→closed ∘ rep-const
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 ∎
rep-Consts-Closed-exp :
∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ → Rep A Closed-exp
rep-Consts-Closed-exp ⦃ r ⦄ = rep ⦃ r = code-Consts-Closed ⦄ ∘-rep r
rep-value :
∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
(x : A) → Value (rep-as-Exp x)
rep-value = const→value ∘ rep-const
subst-rep :
∀ {a} {A : Type 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 : Type 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 : Type 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 : Type 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)
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
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) ∎
code-Var : Code Var Consts
code-Var = code-ℕ ∘-code ≃→Code V.countably-infinite
code-Const : Code Const Consts
code-Const = code-ℕ ∘-code ≃→Code C.countably-infinite
module _ {a b} {A : Type a} {B : Type 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-× = 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 (code x) ⟩ >>=′ λ x →
decode (code y) >>=′ λ y →
just (x , y)) ≡⟨ ⟨by⟩ decode∘code ⟩
(return x >>=′ λ x →
decode (code y) >>=′ λ y →
just (x , y)) ≡⟨⟩
(⟨ decode (code y) ⟩ >>=′ λ y →
just (x , y)) ≡⟨ ⟨by⟩ decode∘code ⟩
(return y >>=′ λ y → just (x , y)) ≡⟨ refl ⟩∎
return (x , y) ∎
module _ {a} {A : Type 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 = 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 = 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 (code x) ⟩ ⊛ dc (cd xs) ≡⟨ ⟨by⟩ decode∘code ⟩
_∷_ ⟨$⟩ return x ⊛ ⟨ dc (cd xs) ⟩ ≡⟨ ⟨by⟩ (dc∘cd xs) ⟩
_∷_ ⟨$⟩ return x ⊛ return xs ≡⟨⟩
return (x ∷ xs) ∎
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
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 ∷ [])
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⋆
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)