Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
-- Urara Yamada, Kenichi Asai -- Certifying CPS transformation of Let-polymorphic Calculus Using PHOAS -- APLAS 2018 -- the correctness of a one-pass CPS transformation -- for the lambda calculus extended with let-polymorphism -- tested on Agda 2.5.2, standard library 0.13 (Aug 2018) module aplas18 where open import Data.Nat hiding (equal) open import Relation.Binary.PropositionalEquality hiding (subst) open import Data.Product infixr 5 _⇒_ -- type data typ[_] (tvar : Set) : Set where TVar : tvar → typ[ tvar ] Nat : typ[ tvar ] _⇒_ : typ[ tvar ] → typ[ tvar ] → typ[ tvar ] Type : Set₁ Type = (tvar : Set) → typ[ tvar ] -- type scheme data ts[_] (tvar : Set) : Set where Typ : typ[ tvar ] → ts[ tvar ] Forall : (tvar → ts[ tvar ]) → ts[ tvar ] Ts : Set₁ Ts = (tvar : Set) → ts[ tvar ] -- substitution relation on types data substTyp {tvar : Set} : (tvar → typ[ tvar ]) → typ[ tvar ] → typ[ tvar ] → Set where sTVar= : {τ : typ[ tvar ]} → substTyp (λ α → TVar α) τ τ sTVar≠ : {τ : typ[ tvar ]} → {α : tvar} → substTyp (λ β → TVar α) τ (TVar α) sNat : {τ : typ[ tvar ]} → substTyp (λ _ → Nat) τ Nat sArrow : {τ₁ τ₂ : tvar → typ[ tvar ]} → {τ τ₁′ τ₂′ : typ[ tvar ]} → substTyp τ₁ τ τ₁′ → substTyp τ₂ τ τ₂′ → substTyp (λ β → τ₁ β ⇒ τ₂ β) τ (τ₁′ ⇒ τ₂′) -- substitution relation on type schemes data substTs {tvar : Set} : (tvar → ts[ tvar ]) → typ[ tvar ] → ts[ tvar ] → Set where sTyp : {τ₁ : tvar → typ[ tvar ]} → {τ : typ[ tvar ]} → {τ₁′ : typ[ tvar ]} → substTyp τ₁ τ τ₁′ → substTs (λ β → Typ (τ₁ β)) τ (Typ τ₁′) sForall : {σ₁ : tvar → tvar → ts[ tvar ]} → {τ : typ[ tvar ]} → {σ₁′ : tvar → ts[ tvar ]} → ((α : tvar) → substTs (λ β → (σ₁ β) α) τ (σ₁′ α)) → substTs (λ β → Forall (σ₁ β)) τ (Forall σ₁′) -- instantiation relation data inst {tvar : Set} : ts[ tvar ] → typ[ tvar ] → Set where instTyp : {τ : typ[ tvar ]} → inst (Typ τ) τ instForall : {σ : tvar → ts[ tvar ]} → {σ′ : ts[ tvar ]} → {τ τ′ : typ[ tvar ]} → substTs σ τ′ σ′ → inst σ′ τ → inst (Forall σ) τ -- DS term mutual data value[_]_ {tvar : Set} (var : ts[ tvar ] → Set) : typ[ tvar ] → Set where Var : {σ₁ : ts[ tvar ]} → (x : var σ₁) {τ₁ : typ[ tvar ]} → (p : inst σ₁ τ₁) → value[ var ] τ₁ Num : ℕ → value[ var ] Nat Fun : {τ₁ τ₂ : typ[ tvar ]} → (var (Typ τ₂) → term[ var ] τ₁) → value[ var ] (τ₂ ⇒ τ₁) data term[_]_ {tvar : Set} (var : ts[ tvar ] → Set) : typ[ tvar ] → Set where Val : {τ₁ : typ[ tvar ]} → value[ var ] τ₁ → term[ var ] τ₁ App : {τ₁ τ₂ : typ[ tvar ]} → (e₁ : term[ var ] (τ₂ ⇒ τ₁)) → (e₂ : term[ var ] τ₂) → term[ var ] τ₁ Let : (σ₁ : ts[ tvar ]) → {τ₂ : typ[ tvar ]} → (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) → (e₂ : var σ₁ → term[ var ] τ₂) → term[ var ] τ₂ Term : Type → Set₁ Term T = (tvar : Set) → (var : ts[ tvar ] → Set) → term[ var ] (T tvar) Value : Type → Set₁ Value T = (tvar : Set) → (var : ts[ tvar ] → Set) → value[ var ] (T tvar) -- substitution relation on DS terms mutual data substV {tvar : Set} {var : ts[ tvar ] → Set} : {σ₁ : ts[ tvar ]} {τ₂ : typ[ tvar ]} → (var σ₁ → value[ var ] τ₂) → ({τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) → value[ var ] τ₂ → Set where sVar= : {τ : typ[ tvar ]} {σ₁ : ts[ tvar ]} {p : inst σ₁ τ} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → substV (λ x → Var x p) v (v p) sVar≠ : {τ : typ[ tvar ]} {σ₁ σ₂ : ts[ tvar ]} {p : inst σ₂ τ} {x : var σ₂} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → substV (λ y → Var x p) v (Var x p) sNum : {σ₁ : ts[ tvar ]} {n : ℕ} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → substV (λ _ → Num n) v (Num n) sFun : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {e₁ : var σ₁ → var (Typ τ₂) → term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {e₁′ : var (Typ τ₂) → term[ var ] τ₁} → ((x : var (Typ τ₂)) → subst (λ y → (e₁ y) x) v (e₁′ x)) → substV (λ y → Fun (e₁ y)) v (Fun e₁′) data subst {tvar : Set} {var : ts[ tvar ] → Set} : {σ₁ : ts[ tvar ]} {τ₂ : typ[ tvar ]} → (var σ₁ → term[ var ] τ₂) → ({τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) → term[ var ] τ₂ → Set where sVal : {τ₁ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {v₁ : var σ₁ → value[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {v₁′ : value[ var ] τ₁} → substV v₁ v v₁′ → subst (λ y → Val (v₁ y)) v (Val v₁′) sApp : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {e₁ : var σ₁ → term[ var ] (τ₂ ⇒ τ₁)} → {e₂ : var σ₁ → term[ var ] τ₂} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {e₁′ : term[ var ] (τ₂ ⇒ τ₁)} → {e₂′ : term[ var ] τ₂} → subst e₁ v e₁′ → subst e₂ v e₂′ → subst (λ y → App (e₁ y) (e₂ y)) v (App e₁′ e₂′) sLet : {τ₂ : typ[ tvar ]} {σ₁ σ₂ : ts[ tvar ]} → {v₁ : var σ₁ → {τ₁ : typ[ tvar ]} → inst σ₂ τ₁ → value[ var ] τ₁} → {e₂ : var σ₁ → var σ₂ → term[ var ] τ₂} {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {v₁′ : {τ₁ : typ[ tvar ]} → inst σ₂ τ₁ → value[ var ] τ₁} → {e₂′ : var σ₂ → term[ var ] τ₂} → ({x : typ[ tvar ]} → (y : inst σ₂ x) → substV (λ z → (v₁ z) y) v (v₁′ y)) → ((x : var σ₂) → subst (λ y → (e₂ y) x) v (e₂′ x)) → subst (λ y → Let σ₂ (v₁ y) (e₂ y)) v (Let σ₂ v₁′ e₂′) mutual substV≠ : {tvar : Set} {var : ts[ tvar ] → Set} → {σ₁ : ts[ tvar ]} {τ₂ : typ[ tvar ]} → {t : value[ var ] τ₂} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → substV (λ y → t) v t substV≠ {t = Var x p} = sVar≠ substV≠ {t = Num x} = sNum substV≠ {t = Fun e₁} = sFun (λ x → subst≠) subst≠ : {tvar : Set} {var : ts[ tvar ] → Set} → {σ₁ : ts[ tvar ]} {τ₂ : typ[ tvar ]} → {t : term[ var ] τ₂} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → subst (λ y → t) v t subst≠ {t = Val x} = sVal substV≠ subst≠ {t = App t t₁} = sApp subst≠ subst≠ subst≠ {t = Let σ₂ v₁ e₂} = sLet (λ x → substV≠) (λ x → subst≠) -- reduction relation (= preservation) on DS terms data reduce {tvar : Set} {var : ts[ tvar ] → Set} : {τ₁ : typ[ tvar ]} → term[ var ] τ₁ → term[ var ] τ₁ → Set where rBeta : {τ₁ τ₂ : typ[ tvar ]} → {e₁ : var (Typ τ₂) → term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst (Typ τ₂) τ → value[ var ] τ} → {e₂ : term[ var ] τ₁} → subst e₁ v e₂ → reduce (App (Val (Fun e₁)) (Val (v instTyp))) e₂ rLet : {σ₁ : ts[ tvar ]} {τ₂ : typ[ tvar ]} → {v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → {e₂ : var σ₁ → term[ var ] τ₂} → {e₂′ : term[ var ] τ₂} → subst e₂ v₁ e₂′ → reduce (Let σ₁ v₁ e₂) e₂′ rApp₁ : {τ₁ τ₂ : typ[ tvar ]} → {e₁ e₁′ : term[ var ] (τ₂ ⇒ τ₁)} → (e₂ : term[ var ] τ₂) → reduce e₁ e₁′ → reduce (App e₁ e₂) (App e₁′ e₂) rApp₂ : {τ₁ τ₂ : typ[ tvar ]} → (v₁ : value[ var ] (τ₂ ⇒ τ₁)) → {e₂ e₂′ : term[ var ] τ₂} → reduce e₂ e₂′ → reduce (App (Val v₁) e₂) (App (Val v₁) e₂′) -- data reduce* {tvar : Set} {var : ts[ tvar ] → Set} : -- {τ₁ : typ[ tvar ]} → term[ var ] τ₁ → term[ var ] τ₁ → Set where -- rId : {τ₁ : typ[ tvar ]} → -- {e : term[ var ] τ₁} → -- reduce* e e -- rTrans : {τ₁ : typ[ tvar ]} → -- (e₁ e₂ e₃ : term[ var ] τ₁) → -- reduce e₁ e₂ → -- reduce* e₂ e₃ → -- reduce* e₁ e₃ data Reduce : {T : Type} → Term T → Term T → Set₁ where RRed : {T : Type} → (e₁ e₂ : Term T) → ((tvar : Set) → (var : ts[ tvar ] → Set) → reduce (e₁ tvar var) (e₂ tvar var)) → Reduce e₁ e₂ -- data Reduce* : {T : Type} → Term T → Term T → Set₁ where -- R*Red : {T : Type} → (e₁ e₂ : Term T) → -- ((tvar : Set) → (var : ts[ tvar ] → Set) → -- reduce* (e₁ tvar var) (e₂ tvar var)) → -- Reduce* e₁ e₂ -- CPS term mutual data cpscont[_]_⇒Nat {tvar : Set} (var : ts[ tvar ] → Set) : typ[ tvar ] → Set where Var : {τ₁ : typ[ tvar ]} → (k : var (Typ (τ₁ ⇒ Nat))) → cpscont[ var ] τ₁ ⇒Nat Fun : {τ₁ : typ[ tvar ]} → (e₁ : var (Typ τ₁) → cpsterm[ var ]Nat) → cpscont[ var ] τ₁ ⇒Nat data cpsvalue[_]_ {tvar : Set} (var : ts[ tvar ] → Set) : typ[ tvar ] → Set where Var : {σ₁ : ts[ tvar ]} → (x : var σ₁) → {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁ Num : ℕ → cpsvalue[ var ] Nat Fun : {τ₁ τ₂ : typ[ tvar ]} → (var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat) → cpsvalue[ var ] (τ₂ ⇒ τ₁) data cpsterm[_]Nat {tvar : Set} (var : ts[ tvar ] → Set) : Set where Val : cpsvalue[ var ] Nat → cpsterm[ var ]Nat App : {τ₁ τ₂ : typ[ tvar ]} → (v₁ : cpsvalue[ var ] (τ₂ ⇒ τ₁)) → (v₂ : cpsvalue[ var ] τ₂) → (c : cpscont[ var ] τ₁ ⇒Nat) → cpsterm[ var ]Nat Ret : {τ₁ : typ[ tvar ]} → (c : cpscont[ var ] τ₁ ⇒Nat) → (v : cpsvalue[ var ] τ₁) → cpsterm[ var ]Nat Let : (σ₁ : ts[ tvar ]) → (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁) → (e₂ : var σ₁ → cpsterm[ var ]Nat) → cpsterm[ var ]Nat CpsCont : Type → Set₁ CpsCont T = (tvar : Set) → (var : ts[ tvar ] → Set) → cpscont[ var ] (T tvar) ⇒Nat CpsValue : Type → Set₁ CpsValue T = (tvar : Set) → (var : ts[ tvar ] → Set) → cpsvalue[ var ] (T tvar) CpsTerm : Set₁ CpsTerm = (tvar : Set) → (var : ts[ tvar ] → Set) → cpsterm[ var ]Nat -- substitution relation on CPS terms (for function application) mutual data cpssubstC {tvar : Set} {var : ts[ tvar ] → Set} : {σ₁ : ts[ tvar ]} {τ₁ τ₂ : typ[ tvar ]} → (c₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpscont[ var ] τ₂ ⇒Nat) → (v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ) → (c : cpscont[ var ] τ₁ ⇒Nat) → (c₁′ : cpscont[ var ] τ₂ ⇒Nat) → Set where sVar= : {τ₁ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → cpssubstC (λ _ k → Var k) v c c sVar≠ : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {k′ : var (Typ (τ₂ ⇒ Nat))} → cpssubstC (λ _ k → Var k′) v c (Var k′) sFun : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {e₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → var (Typ τ₂) → cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {e₁′ : var (Typ τ₂) → cpsterm[ var ]Nat} → ((x : var (Typ τ₂)) → cpssubst (λ x′ k′ → (e₁ x′ k′) x) v c (e₁′ x)) → cpssubstC (λ x k → Fun (e₁ x k)) v c (Fun e₁′) data cpssubstV {tvar : Set} {var : ts[ tvar ] → Set} : {σ₁ : ts[ tvar ]} {τ₁ τ₂ : typ[ tvar ]} → (v₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsvalue[ var ] τ₂) → (v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ) → (c : cpscont[ var ] τ₁ ⇒Nat) → (v₁′ : cpsvalue[ var ] τ₂) → Set where sVar= : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} {p : inst σ₁ τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₂ ⇒Nat} → cpssubstV (λ x _ → Var x p) v c (v p) sVar≠ : {τ₁ τ₂ : typ[ tvar ]} {σ₁ σ₂ : ts[ tvar ]} {p : inst σ₂ τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₂ ⇒Nat} → {y : var σ₂} → cpssubstV (λ x _ → Var y p) v c (Var y p) sNum : {σ₁ : ts[ tvar ]} {τ₁ : typ[ tvar ]} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {n : ℕ} → cpssubstV (λ _ _ → Num n) v c (Num n) sFun : {τ₁ τ₂ τ₃ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {e₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → var (Typ τ₃) → var (Typ (τ₂ ⇒ Nat)) → cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {e₁′ : var (Typ τ₃) → var (Typ (τ₂ ⇒ Nat)) → cpsterm[ var ]Nat} → ((x : var (Typ τ₃)) → (k : var (Typ (τ₂ ⇒ Nat))) → cpssubst (λ x′ k′ → (e₁ x′ k′) x k) v c (e₁′ x k)) → cpssubstV (λ x k → Fun (e₁ x k)) v c (Fun e₁′) data cpssubst {tvar : Set} {var : ts[ tvar ] → Set} : {σ₁ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → (e : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat) → (v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ) → (c : cpscont[ var ] τ₁ ⇒Nat) → (e′ : cpsterm[ var ]Nat) → Set where sVal : {τ₁ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {v₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsvalue[ var ] Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {v₁′ : cpsvalue[ var ] Nat} → cpssubstV v₁ v c v₁′ → cpssubst (λ x y → (Val (v₁ x y))) v c (Val v₁′) sApp : {τ₁ τ₂ τ₃ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {v₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsvalue[ var ] (τ₃ ⇒ τ₂)} → {v₂ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsvalue[ var ] τ₃} → {c₃ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpscont[ var ] τ₂ ⇒Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {v₁′ : cpsvalue[ var ] (τ₃ ⇒ τ₂)} → {v₂′ : cpsvalue[ var ] τ₃} → {c₃′ : cpscont[ var ] τ₂ ⇒Nat} → cpssubstV v₁ v c v₁′ → cpssubstV v₂ v c v₂′ → cpssubstC c₃ v c c₃′ → cpssubst (λ x k → App (v₁ x k) (v₂ x k) (c₃ x k)) v c (App v₁′ v₂′ c₃′) sRet : {τ₁ τ₂ : typ[ tvar ]} {σ₁ : ts[ tvar ]} → {c₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpscont[ var ] τ₂ ⇒Nat} → {v₂ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → cpsvalue[ var ] τ₂} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {c₁′ : cpscont[ var ] τ₂ ⇒Nat} → {v₂′ : cpsvalue[ var ] τ₂} → cpssubstC c₁ v c c₁′ → cpssubstV v₂ v c v₂′ → cpssubst (λ x k → Ret (c₁ x k) (v₂ x k)) v c (Ret c₁′ v₂′) sLet : {τ₁ : typ[ tvar ]} {σ₁ σ₂ : ts[ tvar ]} → {v₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → {τ : typ[ tvar ]} → inst σ₂ τ → cpsvalue[ var ] τ} → {e₁ : var σ₁ → var (Typ (τ₁ ⇒ Nat)) → var σ₂ → cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {v₁′ : {τ : typ[ tvar ]} → inst σ₂ τ → cpsvalue[ var ] τ} → {e₁′ : var σ₂ → cpsterm[ var ]Nat} → ({τ : typ[ tvar ]} → (p : inst σ₂ τ) → cpssubstV (λ x k → (v₁ x k) p) v c (v₁′ p)) → ((x : var σ₂) → cpssubst (λ x′ k′ → (e₁ x′ k′) x) v c (e₁′ x)) → cpssubst (λ x k → Let σ₂ (v₁ x k) (e₁ x k)) v c (Let σ₂ v₁′ e₁′) -- mutual -- cpssubstC≠ : {tvar : Set} {var : ts[ tvar ] → Set} -- {σ₁ : ts[ tvar ]} {τ₁ τ₂ : typ[ tvar ]} → -- {t : cpscont[ var ] τ₂ ⇒Nat} → -- {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → -- {c : cpscont[ var ] τ₁ ⇒Nat} → -- cpssubstC (λ x y → t) v c t -- cpssubstC≠ {t = Var k} = sVar≠ -- cpssubstC≠ {t = Fun e₁} = sFun (λ x → cpssubst≠) -- cpssubstV≠ : {tvar : Set} {var : ts[ tvar ] → Set} -- {σ₁ : ts[ tvar ]} {τ₁ τ₂ : typ[ tvar ]} → -- {t : cpsvalue[ var ] τ₂} → -- {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → -- {c : cpscont[ var ] τ₁ ⇒Nat} → -- cpssubstV (λ x y → t) v c t -- cpssubstV≠ {t = Var x p} = sVar≠ -- cpssubstV≠ {t = Num x} = sNum -- cpssubstV≠ {t = Fun e} = sFun (λ x k → cpssubst≠) -- cpssubst≠ : {tvar : Set} {var : ts[ tvar ] → Set} -- {σ₁ : ts[ tvar ]} {τ₁ : typ[ tvar ]} → -- {t : cpsterm[ var ]Nat} → -- {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → -- {c : cpscont[ var ] τ₁ ⇒Nat} → -- cpssubst (λ x y → t) v c t -- cpssubst≠ {t = Val x} = sVal cpssubstV≠ -- cpssubst≠ {t = App v₁ v₂ c} = sApp cpssubstV≠ cpssubstV≠ cpssubstC≠ -- cpssubst≠ {t = Ret c v} = sRet cpssubstC≠ cpssubstV≠ -- cpssubst≠ {t = Let σ₂ v₁ e₂} = sLet (λ _ → cpssubstV≠) (λ _ → cpssubst≠) -- substitution relation on CPS terms (for continuation application) mutual data cpssubstCK {tvar : Set} {var : ts[ tvar ] → Set} : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → (c₁ : var σ → cpscont[ var ] τ₁ ⇒Nat) → (v : {τ : typ[ tvar ]} → inst σ τ → cpsvalue[ var ] τ) → (c₁′ : cpscont[ var ] τ₁ ⇒Nat) → Set where sVar≠ : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {k′ : var (Typ (τ ⇒ Nat))} → cpssubstCK (λ _ → Var k′) v (Var k′) sFun : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → {e₁ : var σ → var (Typ τ₁) → cpsterm[ var ]Nat} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {e₁′ : var (Typ τ₁) → cpsterm[ var ]Nat} → ((x : var (Typ τ₁)) → cpssubstK (λ x′ → (e₁ x′) x) v (e₁′ x)) → cpssubstCK (λ x → Fun (e₁ x)) v (Fun e₁′) data cpssubstVK {tvar : Set} {var : ts[ tvar ] → Set} : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → (v₁ : var σ → cpsvalue[ var ] τ₁) → (v : {τ : typ[ tvar ]} → inst σ τ → cpsvalue[ var ] τ) → (v₁′ : cpsvalue[ var ] τ₁) → Set where sVar= : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} → {p : inst σ τ} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → cpssubstVK (λ x → Var x p) v (v p) sVar≠ : {σ σ₁ : ts[ tvar ]} → {τ : typ[ tvar ]} → {p : inst σ₁ τ} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {y : var σ₁} → cpssubstVK (λ _ → Var y p) v (Var y p) sNum : {σ : ts[ tvar ]} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {n : ℕ} → cpssubstVK (λ x → Num n) v (Num n) sFun : {σ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} → {e₁ : var σ → var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {e₁′ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat} → ((x : var (Typ τ₂)) → (k : var (Typ (τ₁ ⇒ Nat))) → cpssubstK (λ x′ → (e₁ x′) x k) v (e₁′ x k)) → cpssubstVK (λ x → Fun (e₁ x)) v (Fun e₁′) data cpssubstK {tvar : Set} {var : ts[ tvar ] → Set} : {σ : ts[ tvar ]} → (e : var σ → cpsterm[ var ]Nat) → (v : {τ : typ[ tvar ]} → inst σ τ → cpsvalue[ var ] τ) → (e′ : cpsterm[ var ]Nat) → Set where sVal : {σ : ts[ tvar ]} {v₁ : var σ → cpsvalue[ var ] Nat} → {v : {τ₂ : typ[ tvar ]} → inst σ τ₂ → cpsvalue[ var ] τ₂} → {v₁′ : cpsvalue[ var ] Nat} → cpssubstVK v₁ v v₁′ → cpssubstK (λ x → (Val (v₁ x))) v (Val v₁′) sApp : {σ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} → {v₁ : var σ → cpsvalue[ var ] (τ₂ ⇒ τ₁)} → {v₂ : var σ → cpsvalue[ var ] τ₂} → {c₃ : var σ → cpscont[ var ] τ₁ ⇒Nat} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {v₁′ : cpsvalue[ var ] (τ₂ ⇒ τ₁)} → {v₂′ : cpsvalue[ var ] τ₂} → {c₃′ : cpscont[ var ] τ₁ ⇒Nat} → cpssubstVK v₁ v v₁′ → cpssubstVK v₂ v v₂′ → cpssubstCK c₃ v c₃′ → cpssubstK (λ x → App (v₁ x) (v₂ x) (c₃ x)) v (App v₁′ v₂′ c₃′) sRet : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → {c₁ : var σ → cpscont[ var ] τ₁ ⇒Nat} → {v₂ : var σ → cpsvalue[ var ] τ₁} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {c₁′ : cpscont[ var ] τ₁ ⇒Nat} → {v₂′ : cpsvalue[ var ] τ₁} → cpssubstCK c₁ v c₁′ → cpssubstVK v₂ v v₂′ → cpssubstK (λ x → Ret (c₁ x) (v₂ x)) v (Ret c₁′ v₂′) sLet : {σ σ₁ : ts[ tvar ]} {v₁ : var σ → {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} → {e₁ : var σ → var σ₁ → cpsterm[ var ]Nat} → {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} → {v₁′ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} → {e₁′ : var σ₁ → cpsterm[ var ]Nat} → ({τ₁ : typ[ tvar ]} → (p : inst σ₁ τ₁) → cpssubstVK (λ x → (v₁ x) p) v (v₁′ p)) → ((x : var σ₁) → cpssubstK (λ x′ → (e₁ x′) x) v (e₁′ x)) → cpssubstK (λ x → Let σ₁ (v₁ x) (e₁ x)) v (Let σ₁ v₁′ e₁′) mutual cpssubstCK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} {τ₁ : typ[ tvar ]} → {t : cpscont[ var ] τ₁ ⇒Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → cpssubstCK (λ x → t) v t cpssubstCK≠ {t = Var k} = sVar≠ cpssubstCK≠ {t = Fun e₁} = sFun (λ x → cpssubstK≠) cpssubstVK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} {τ₁ : typ[ tvar ]} → {t : cpsvalue[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → cpssubstVK (λ x → t) v t cpssubstVK≠ {t = Var x p} = sVar≠ cpssubstVK≠ {t = Num x} = sNum cpssubstVK≠ {t = Fun e₁} = sFun (λ x k → cpssubstK≠) cpssubstK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {t : cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} → cpssubstK (λ x → t) v t cpssubstK≠ {t = Val x} = sVal cpssubstVK≠ cpssubstK≠ {t = App v₁ v₂ c} = sApp cpssubstVK≠ cpssubstVK≠ cpssubstCK≠ cpssubstK≠ {t = Ret c v} = sRet cpssubstCK≠ cpssubstVK≠ cpssubstK≠ {t = Let σ₂ v₁ e₂} = sLet (λ _ → cpssubstVK≠) (λ _ → cpssubstK≠) -- CPS transformation (that produces no eta-redex) mutual cpsEtaV : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} → value[ var ] τ₁ → cpsvalue[ var ] τ₁ cpsEtaV (Var x p) = Var x p cpsEtaV (Num n) = Num n cpsEtaV (Fun e₁) = Fun (λ x k → cpsEta′ (e₁ x) (Var k)) cpsEta : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} → term[ var ] τ₁ → (cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → cpsterm[ var ]Nat cpsEta (Val v) κ = κ (cpsEtaV v) cpsEta (App e₁ e₂) κ = cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp))))) cpsEta (Let σ₁ v₁ e₂) κ = Let σ₁ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEta (e₂ x) κ) cpsEta′ : {tvar : Set} {var : ts[ tvar ] → Set } → {τ₁ : typ[ tvar ]} → term[ var ] τ₁ → cpscont[ var ] τ₁ ⇒Nat → cpsterm[ var ]Nat cpsEta′ (Val v) k = Ret k (cpsEtaV v) cpsEta′ (App e₁ e₂) k = cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ → App v₁ v₂ k)) cpsEta′ (Let σ₁ v₁ e₂) k = Let σ₁ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEta′ (e₂ x) k) CpsEta : {T : Type} → Term T → ((tvar : Set) → (var : ts[ tvar ] → Set) → cpsvalue[ var ] (T tvar) → cpsterm[ var ]Nat) → CpsTerm CpsEta e κ = λ tvar var → cpsEta (e tvar var) (κ tvar var) -- equality relation for CPS terms mutual data equalC {tvar : Set} {var : ts[ tvar ] → Set} : {τ₁ : typ[ tvar ]} → cpscont[ var ] τ₁ ⇒Nat → cpscont[ var ] τ₁ ⇒Nat → Set where eqFun : {τ₁ : typ[ tvar ]} → {e₁ : var (Typ τ₁) → cpsterm[ var ]Nat} → {e₂ : var (Typ τ₁) → cpsterm[ var ]Nat} → ((x : var (Typ τ₁)) → equal (e₁ x) (e₂ x)) → equalC (Fun (λ x → e₁ x)) (Fun (λ x → e₂ x)) data equalV {tvar : Set} {var : ts[ tvar ] → Set} : {τ₁ : typ[ tvar ]} → cpsvalue[ var ] τ₁ → cpsvalue[ var ] τ₁ → Set where eqFun : {τ₁ τ₂ : typ[ tvar ]} → {e₁ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat} → {e₂ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat} → ((x : var (Typ τ₂)) → (c : var (Typ (τ₁ ⇒ Nat))) → equal (e₁ x c) (e₂ x c)) → equalV (Fun (λ x c → e₁ x c)) (Fun (λ x c → e₂ x c)) data equal {tvar : Set} {var : ts[ tvar ] → Set} : cpsterm[ var ]Nat → cpsterm[ var ]Nat → Set where eqBeta : {τ₁ τ₂ : typ[ tvar ]} → {e₁ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) → cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst (Typ τ₂) τ → value[ var ] τ} → {c : cpscont[ var ] τ₁ ⇒Nat} → {e₂ : cpsterm[ var ]Nat} → cpssubst e₁ (λ p → cpsEtaV (v p)) c e₂ → equal (App (Fun e₁) (cpsEtaV (v instTyp)) c) e₂ eqCont : {τ₁ : typ[ tvar ]} → {e₁ : var (Typ τ₁) → cpsterm[ var ]Nat} → {v : {τ : typ[ tvar ]} → inst (Typ τ₁) τ → value[ var ] τ} → {e₂ : cpsterm[ var ]Nat} → cpssubstK e₁ (λ p → cpsEtaV (v p)) e₂ → equal (Ret (Fun e₁) (cpsEtaV (v instTyp))) e₂ eqLet : {σ₁ : ts[ tvar ]} → {v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → {e₂ : var σ₁ → cpsterm[ var ]Nat} → {e₂′ : cpsterm[ var ]Nat} → cpssubstK e₂ (λ p → cpsEtaV (v₁ p)) e₂′ → equal (Let σ₁ (λ p → cpsEtaV (v₁ p)) e₂) e₂′ eqApp₁ : {τ₁ τ₂ : typ[ tvar ]} → {v₁ v₁′ : cpsvalue[ var ] (τ₂ ⇒ τ₁)} → (v₂ : cpsvalue[ var ] τ₂) → (c : cpscont[ var ] τ₁ ⇒Nat) → equalV v₁ v₁′ → equal (App v₁ v₂ c) (App v₁′ v₂ c) eqApp₂ : {τ₁ τ₂ : typ[ tvar ]} → (v₁ : cpsvalue[ var ] (τ₂ ⇒ τ₁)) → {v₂ v₂′ : cpsvalue[ var ] τ₂} → (c : cpscont[ var ] τ₁ ⇒Nat) → equalV v₂ v₂′ → equal (App v₁ v₂ c) (App v₁ v₂′ c) eqApp₃ : {τ₁ τ₂ : typ[ tvar ]} → (v₁ : cpsvalue[ var ] (τ₂ ⇒ τ₁)) → (v₂ : cpsvalue[ var ] τ₂) → {c c′ : cpscont[ var ] τ₁ ⇒Nat} → equalC c c′ → equal (App v₁ v₂ c) (App v₁ v₂ c′) eqRet₁ : {τ₁ : typ[ tvar ]} → {c c′ : cpscont[ var ] τ₁ ⇒Nat} → (v : cpsvalue[ var ] τ₁) → equalC c c′ → equal (Ret c v) (Ret c′ v) eqRet₂ : {τ₁ : typ[ tvar ]} → (c : cpscont[ var ] τ₁ ⇒Nat) → {v v′ : cpsvalue[ var ] τ₁} → equalV v v′ → equal (Ret c v) (Ret c v′) eqLet₁ : {σ₁ : ts[ tvar ]} → {v₁ v₁′ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} → (e₂ : var σ₁ → cpsterm[ var ]Nat) → ({τ₁ : typ[ tvar ]} → (p : inst σ₁ τ₁) → equalV (v₁ p) (v₁′ p)) → equal (Let σ₁ v₁ e₂) (Let σ₁ v₁′ e₂) eqLet₂ : {σ₁ : ts[ tvar ]} → (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁) → {e₂ e₂′ : var σ₁ → cpsterm[ var ]Nat} → ((x : var σ₁) → equal (e₂ x) (e₂′ x)) → equal (Let σ₁ v₁ e₂) (Let σ₁ v₁ e₂′) eqId : {e : cpsterm[ var ]Nat} → equal e e eqTrans : (e₁ e₂ e₃ : cpsterm[ var ]Nat) → equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃ eqTrans′ : (e₁ e₂ e₃ : cpsterm[ var ]Nat) → equal e₂ e₁ → equal e₂ e₃ → equal e₁ e₃ data Equal : CpsTerm → CpsTerm → Set₁ where EqRed : (e₁ e₂ : CpsTerm) → ((tvar : Set) → (var : ts[ tvar ] → Set) → equal (e₁ tvar var) (e₂ tvar var)) → Equal e₁ e₂ -- equational reasoning module eq-Reasoning {tvar : Set} {var : ts[ tvar ] → Set} where infix 3 _∎ infixr 2 _⟷⟨_⟩_ _⟶⟨_⟩_ _⟵⟨_⟩_ _≡⟨_⟩_ infix 1 begin_ begin_ : {e₁ e₂ : cpsterm[ var ]Nat} → equal e₁ e₂ → equal e₁ e₂ begin_ eq = eq _⟷⟨_⟩_ : (e₁ {e₂ e₃} : cpsterm[ var ]Nat) → equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃ _⟷⟨_⟩_ e₁ {e₂} {e₃} e₁-eq-e₂ e₂-eq*-e₃ = eqTrans e₁ e₂ e₃ e₁-eq-e₂ e₂-eq*-e₃ -- the same as _⟷⟨_⟩_ _⟶⟨_⟩_ : (e₁ {e₂ e₃} : cpsterm[ var ]Nat) → equal e₁ e₂ → equal e₂ e₃ → equal e₁ e₃ _⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-eq-e₂ e₂-eq*-e₃ = eqTrans e₁ e₂ e₃ e₁-eq-e₂ e₂-eq*-e₃ _⟵⟨_⟩_ : (e₁ {e₂ e₃} : cpsterm[ var ]Nat) → equal e₂ e₁ → equal e₂ e₃ → equal e₁ e₃ _⟵⟨_⟩_ e₁ {e₂} {e₃} e₂-eq-e₁ e₂-eq*-e₃ = eqTrans′ e₁ e₂ e₃ e₂-eq-e₁ e₂-eq*-e₃ _≡⟨_⟩_ : (e₁ {e₂ e₃} : cpsterm[ var ]Nat) → e₁ ≡ e₂ → equal e₂ e₃ → equal e₁ e₃ _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-eq-e₃ = e₂-eq-e₃ _∎ : (e : cpsterm[ var ]Nat) → equal e e _∎ e = eqId open eq-Reasoning -- Definition 1 schematic : {tvar : Set} {var : ts[ tvar ] → Set} {τ : typ[ tvar ]} → (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) → Set schematic {tvar} {var} {τ} κ = {σ₁ : ts[ tvar ]} → {v₁ : var σ₁ → cpsvalue[ var ] τ} → {v₁′ : cpsvalue[ var ] τ} → {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} → cpssubstVK v₁ (λ p → cpsEtaV (v p)) v₁′ → cpssubstK (λ x → κ (v₁ x)) (λ p → cpsEtaV (v p)) (κ v₁′) -- Definition 2 cont-equal : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ τ₃ : typ[ tvar ]} → (κ₁ : var σ₁ → var (Typ (τ₃ ⇒ Nat)) → cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → (v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ) → (c : cpscont[ var ] τ₃ ⇒Nat) → (κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → Set cont-equal {tvar} {var} {σ₁} {τ₁} {τ₃} κ₁ v c κ₂ = {v₁ : var σ₁ → var (Typ (τ₃ ⇒ Nat)) → cpsvalue[ var ] τ₁} → {v₁′ : cpsvalue[ var ] τ₁} → cpssubstV v₁ (λ p → cpsEtaV (v p)) c v₁′ → cpssubst (λ x k → κ₁ x k (v₁ x k)) (λ p → cpsEtaV (v p)) c (κ₂ v₁′) -- Definition 3 cont-equalK : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → (κ₁ : var σ₁ → cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → (v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ) → (κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → Set cont-equalK {tvar} {var} {σ₁} {τ₁} κ₁ v κ₂ = {v₁ : var σ₁ → cpsvalue[ var ] τ₁} → {v₁′ : cpsvalue[ var ] τ₁} → cpssubstVK v₁ (λ p → cpsEtaV (v p)) v₁′ → cpssubstK (λ x → κ₁ x (v₁ x)) (λ p → cpsEtaV (v p)) (κ₂ v₁′) -- Lemma 1 mutual ekSubstEtaV : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} → {v₁ : var σ₁ → value[ var ] τ₁} → {v₁′ : value[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {c : cpscont[ var ] τ₂ ⇒Nat} → substV v₁ v v₁′ → cpssubstV (λ x _ → cpsEtaV (v₁ x)) (λ p → cpsEtaV (v p)) c (cpsEtaV v₁′) ekSubstEtaV sVar= = sVar= ekSubstEtaV sVar≠ = sVar≠ ekSubstEtaV sNum = sNum ekSubstEtaV {c = c} (sFun x) = sFun (λ x₁ k → ekSubstEta′ (x x₁) (Var k) sVar≠) ekSubstEta : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} → {e : var σ₁ → term[ var ] τ₁} → {e′ : term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → {c : cpscont[ var ] τ₂ ⇒Nat} → subst e v e′ → (κ₁ : var σ₁ → var (Typ (τ₂ ⇒ Nat)) → cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → {κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat} → cont-equal κ₁ v c κ₂ → cpssubst (λ x k → cpsEta (e x) (κ₁ x k)) (λ p → cpsEtaV (v p)) c (cpsEta e′ κ₂) ekSubstEta (sVal x) κ₁ eq = eq (ekSubstEtaV x) ekSubstEta (sApp {e₁ = e₁} {e₂} sub sub₁) κ₁ eq = ekSubstEta sub (λ x k v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Fun (λ v → κ₁ x k (Var v instTyp))))) (λ {v₁} s₁ → ekSubstEta sub₁ (λ x k v₂ → App (v₁ x k) v₂ (Fun (λ v → κ₁ x k (Var v instTyp)))) (λ s₂ → sApp s₁ s₂ (sFun (λ _ → eq sVar≠)))) ekSubstEta (sLet x x₁) κ₁ eq = sLet (λ p → ekSubstEtaV (x p)) (λ v₁ → ekSubstEta (x₁ v₁) κ₁ eq) ekSubstEta′ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} → {e : var σ₁ → term[ var ] τ₁} → {e′ : term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → subst e v e′ → {c : cpscont[ var ] τ₂ ⇒Nat} → {k : var σ₁ → var (Typ (τ₂ ⇒ Nat)) → cpscont[ var ] τ₁ ⇒Nat} → (k′ : cpscont[ var ] τ₁ ⇒Nat) → cpssubstC k (λ p → cpsEtaV (v p)) c k′ → cpssubst (λ x k₁ → cpsEta′ (e x) (k x k₁)) (λ p → cpsEtaV (v p)) c (cpsEta′ e′ k′) ekSubstEta′ (sVal x) k′ sub′ = sRet sub′ (ekSubstEtaV x) ekSubstEta′ (sApp {e₂ = e₂} sub sub₁) k′ sVar= = ekSubstEta sub (λ x k₁ v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Var k₁))) (λ {v₁} s₁ → ekSubstEta sub₁ (λ x k₁ v₂ → App (v₁ x k₁) v₂ (Var k₁)) (λ s₂ → sApp s₁ s₂ sVar=)) ekSubstEta′ (sApp {e₂ = e₂} sub sub₁) (Var k′) sVar≠ = ekSubstEta sub (λ x k₁ v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Var k′))) (λ {v₁} s₁ → ekSubstEta sub₁ (λ x k₁ v₂ → App (v₁ x k₁) v₂ (Var k′)) (λ s₂ → sApp s₁ s₂ sVar≠)) ekSubstEta′ (sApp {e₂ = e₃} sub sub₁) (Fun k′) (sFun {e₁ = e₁} x) = ekSubstEta sub (λ x₁ k₁ v₁ → cpsEta (e₃ x₁) (λ v₂ → App v₁ v₂ (Fun (e₁ x₁ k₁)))) (λ {v₁} s₁ → ekSubstEta sub₁ (λ x₁ k₁ v₂ → App (v₁ x₁ k₁) v₂ (Fun (e₁ x₁ k₁))) (λ s₂ → sApp s₁ s₂ (sFun x))) ekSubstEta′ (sLet x x₁) k′ sub′ = sLet (λ p → ekSubstEtaV (x p)) (λ v₁ → ekSubstEta′ (x₁ v₁) k′ sub′) -- Lemma 2 mutual ekSubstEtaKV : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → {v₁ : var σ₁ → value[ var ] τ₁} → {v₁′ : value[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → substV v₁ v v₁′ → cpssubstVK (λ x → cpsEtaV (v₁ x)) (λ p → cpsEtaV (v p)) (cpsEtaV v₁′) ekSubstEtaKV sVar= = sVar= ekSubstEtaKV sVar≠ = sVar≠ ekSubstEtaKV sNum = sNum ekSubstEtaKV (sFun x) = sFun (λ x₁ k → ekSubstEtaK′ (x x₁) (Var k)) ekSubstEtaK′ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → {e : var σ₁ → term[ var ] τ₁} → {e′ : term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → subst e v e′ → (k : cpscont[ var ] τ₁ ⇒Nat) → cpssubstK (λ x → cpsEta′ (e x) k) (λ p → cpsEtaV (v p)) (cpsEta′ e′ k) ekSubstEtaK′ (sVal x) k = sRet cpssubstCK≠ (ekSubstEtaKV x) ekSubstEtaK′ (sApp {e₁ = e₁} {e₂} sub sub₁) k = ekSubstEtaK (λ x v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ k)) sub (λ {v₁} subk₁ → ekSubstEtaK (λ x v₂ → App (v₁ x) v₂ k) sub₁ (λ subk₂ → sApp subk₁ subk₂ cpssubstCK≠)) ekSubstEtaK′ (sLet x x₁) k = sLet (λ p → ekSubstEtaKV (x p)) (λ x₂ → ekSubstEtaK′ (x₁ x₂) k) ekSubstEtaK : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} → {e₁ : var σ₁ → term[ var ] τ₁} → {e₁′ : term[ var ] τ₁} → {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} → (κ₁ : var σ₁ → cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → {κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat} → subst e₁ v e₁′ → cont-equalK κ₁ v κ₂ → cpssubstK (λ x₁ → cpsEta (e₁ x₁) (κ₁ x₁)) (λ p → cpsEtaV (v p)) (cpsEta e₁′ κ₂) ekSubstEtaK κ₁ (sVal x) eq = eq (ekSubstEtaKV x) ekSubstEtaK κ₁ (sApp {e₁ = e₁} {e₂} sub sub₁) eq = ekSubstEtaK (λ x v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Fun (λ v → κ₁ x (Var v instTyp))))) sub (λ {v₁} s₁ → ekSubstEtaK (λ x v₂ → App (v₁ x) v₂ (Fun (λ x₁ → κ₁ x (Var x₁ instTyp)))) sub₁ (λ {v₁} s₂ → sApp s₁ s₂ (sFun (λ x → eq sVar≠)))) ekSubstEtaK κ₁ (sLet x x₁) eq = sLet (λ p → ekSubstEtaKV (x p)) (λ v₂ → ekSubstEtaK κ₁ (x₁ v₂) (λ sub → eq sub)) cpsEtaEta′ : {tvar : Set} {var : ts[ tvar ] → Set} {τ : typ[ tvar ]} → (e : term[ var ] τ) → (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) → schematic κ → equal (cpsEta′ e (Fun (λ x → κ (Var x instTyp)))) (cpsEta e κ) cpsEtaEta′ (Val v) κ sche = begin cpsEta′ (Val v) (Fun (λ x → κ (Var x instTyp))) ≡⟨ refl ⟩ Ret (Fun (λ x → κ (Var x instTyp))) (cpsEtaV v) ⟶⟨ eqCont (sche {v₁ = λ x → Var x instTyp} {v₁′ = cpsEtaV v} {v = λ { instTyp → v }} sVar= ) ⟩ cpsEta (Val v) κ ∎ cpsEtaEta′ (App e₁ e₂) κ sche = begin cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp))))) ∎ cpsEtaEta′ (Let σ₁ v₁ e₂) κ sche = begin cpsEta′ (Let σ₁ v₁ e₂) (Fun (λ x → κ (Var x instTyp))) ⟷⟨ eqLet₂ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEtaEta′ (e₂ x) κ sche) ⟩ cpsEta (Let σ₁ v₁ e₂) κ ∎ -- Theorem 1 correctEta : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ : typ[ tvar ]} → {e e′ : term[ var ] τ} → (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) → reduce e e′ → schematic κ → equal (cpsEta e κ) (cpsEta e′ κ) correctEta {e′ = e′} κ (rBeta {e₁ = e₁} {v} sub) sche = begin cpsEta (App (Val (Fun e₁)) (Val (v instTyp))) κ ≡⟨ refl ⟩ App (Fun (λ x k → cpsEta′ (e₁ x) (Var k))) (cpsEtaV (v instTyp)) (Fun (λ v₁ → κ (Var v₁ instTyp))) ⟶⟨ eqBeta (ekSubstEta′ sub (Fun (λ x → κ (Var x instTyp))) sVar=) ⟩ cpsEta′ e′ (Fun (λ x → κ (Var x instTyp))) ⟷⟨ cpsEtaEta′ e′ κ sche ⟩ cpsEta e′ κ ∎ correctEta {e′ = e′} κ (rLet {σ₁} {v₁ = v₁} {e₂} sub) sche = begin cpsEta (Let σ₁ v₁ e₂) κ ≡⟨ refl ⟩ Let σ₁ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEta (e₂ x) κ) ⟷⟨ eqLet (ekSubstEtaK (λ _ v₂ → κ v₂) sub sche) ⟩ cpsEta e′ κ ∎ correctEta κ (rApp₁ {e₁ = e₁} {e₁′} e₂ red) sche = begin cpsEta (App e₁ e₂) κ ⟷⟨ correctEta (λ v₁ → cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp))))) red (λ {σ₁} {v₁} {_} {v} sub → ekSubstEtaK {e₁ = λ _ → e₂} {e₁′ = e₂} {v = v} (λ z z₁ → App (v₁ z) z₁ (Fun (λ z₂ → κ (Var z₂ instTyp)))) subst≠ (λ x → sApp sub x cpssubstCK≠)) ⟩ cpsEta (App e₁′ e₂) κ ∎ correctEta κ (rApp₂ v₁ {e₂} {e₂′} red) sche = begin cpsEta (App (Val v₁) e₂) κ ⟷⟨ correctEta (λ v₂ → App (cpsEtaV v₁) v₂ (Fun (λ v → κ (Var v instTyp)))) red (λ sub → sApp cpssubstVK≠ sub cpssubstCK≠) ⟩ cpsEta (App (Val v₁) e₂′) κ ∎ -- Corollary 1 Correct : {T : Type} → {e e′ : Term T} → (κ : (tvar : Set) → (var : ts[ tvar ] → Set) → cpsvalue[ var ] (T tvar) → cpsterm[ var ]Nat) → ((tvar : Set) → (var : ts[ tvar ] → Set) → schematic (κ tvar var)) → Reduce e e′ → Equal (CpsEta e κ) (CpsEta e′ κ) Correct κ sche (RRed e₁ e₂ red) = EqRed (CpsEta e₁ κ) (CpsEta e₂ κ) (λ tvar var → correctEta (κ tvar var) (red tvar var) (sche tvar var)) -- when k is an identity function -- Corollary 2 CpsEtaId : Term (λ _ → Nat) → CpsTerm CpsEtaId e = λ tvar var → cpsEta (e tvar var) (λ v → Val v) CorrectEtaId : {e e′ : Term (λ _ → Nat)} → Reduce e e′ → Equal (CpsEtaId e) (CpsEtaId e′) CorrectEtaId red = Correct (λ tvar var v → Val v) (λ tvar var sub → sVal sub) red