https://github.com/YouyouCong/fscd21-artifact
Tip revision: c88b251d074865dd2d22d7cd755a2ffa40c42891 authored by Youyou Cong on 02 May 2021, 10:36:52 UTC
Revert "rename variables"
Revert "rename variables"
Tip revision: c88b251
lambdac-red.agda
-- Reduction of λC
module LambdaC-Red where
open import LambdaF hiding (〚_〛τ; 〚_〛μ)
open import CPS
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Bool using (true; false; if_then_else_) renaming (Bool to 𝔹)
open import Data.String using (String)
open import Relation.Binary.PropositionalEquality
-- Substitution
data SubstVal {var : CTy → Set} : {τ₁ τ₂ : CTy} →
(var τ₁ → CVal[ var ] τ₂) →
CVal[ var ] τ₁ →
CVal[ var ] τ₂ → Set₁
data Subst {var : CTy → Set} : {τ₁ τ₂ : CTy} →
(var τ₁ → CExp[ var ] τ₂) → CVal[ var ] τ₁ →
CExp[ var ] τ₂ → Set₁
data SubstVal {var} where
sVar= : {τ : CTy} {v : CVal[ var ] τ} →
SubstVal (λ x → Var x) v v
sVar≠ : {τ₁ τ₂ : CTy}
{v : CVal[ var ] τ₂} {x : var τ₁} →
SubstVal (λ y → Var x) v (Var x)
sNum : {τ : CTy} {n : ℕ}
{v : CVal[ var ] τ} →
SubstVal (λ x → Num n) v (Num n)
sBol : {τ : CTy} {b : 𝔹}
{v : CVal[ var ] τ} →
SubstVal (λ x → Bol b) v (Bol b)
sStr : {τ : CTy} {s : String}
{v : CVal[ var ] τ} →
SubstVal (λ x → Str s) v (Str s)
sAbs : {τ τ₁ τ₂ : CTy}
{e : var τ₁ → var τ → CExp[ var ] τ₂} →
{v : CVal[ var ] τ₁} →
{e' : var τ → CExp[ var ] τ₂} →
((x : var τ) → Subst (λ y → (e y) x) v (e' x)) →
SubstVal (λ y → Abs (e y)) v (Abs e')
sEmp : {τ : CTy} {v : CVal[ var ] τ} →
SubstVal (λ x → Emp) v Emp
data Subst {var} where
sVal : {τ τ₁ : CTy}
{v₁ : var τ → CVal[ var ] τ₁}
{v : CVal[ var ] τ}
{v₁' : CVal[ var ] τ₁} →
SubstVal v₁ v v₁' →
Subst (λ y → Val (v₁ y)) v (Val v₁')
sApp : {τ τ₁ τ₂ : CTy}
{e₁ : var τ → CExp[ var ] (τ₁ ⇒ τ₂)}
{e₂ : var τ → CExp[ var ] τ₁}
{v : CVal[ var ] τ}
{e₁' : CExp[ var ] (τ₁ ⇒ τ₂)}
{e₂' : CExp[ var ] τ₁} →
Subst e₁ v e₁' → Subst e₂ v e₂' →
Subst (λ y → App (e₁ y) (e₂ y)) v (App e₁' e₂')
sPlu : {τ : CTy}
{e₁ : var τ → CExp[ var ] Nat}
{e₂ : var τ → CExp[ var ] Nat}
{v : CVal[ var ] τ}
{e₁' : CExp[ var ] Nat}
{e₂' : CExp[ var ] Nat} →
Subst e₁ v e₁' → Subst e₂ v e₂' →
Subst (λ y → Plus (e₁ y) (e₂ y)) v (Plus e₁' e₂')
sIs0 : {τ : CTy}
{e : var τ → CExp[ var ] Nat}
{v : CVal[ var ] τ}
{e' : CExp[ var ] Nat} →
Subst e v e' →
Subst (λ y → Is0 (e y)) v (Is0 e')
sB2S : {τ : CTy}
{e : var τ → CExp[ var ] Bool}
{v : CVal[ var ] τ}
{e' : CExp[ var ] Bool} →
Subst e v e' →
Subst (λ y → B2S (e y)) v (B2S e')
sCase : {μ : Tr} {τ τ₂ : CTy}
{t : var τ → CExp[ var ] 〚 μ 〛μ}
{e₁ : var τ → μ ≡ ● → CExp[ var ] τ₂}
{e₂ : var τ → {τ₁ τ₁' : Ty} {μ₁' : Tr} →
μ ≡ τ₁ ⇒⟨ μ₁' ⟩ τ₁' → CExp[ var ] τ₂}
{v : CVal[ var ] τ}
{t' : CExp[ var ] 〚 μ 〛μ}
{e₁' : μ ≡ ● → CExp[ var ] τ₂}
{e₂' : {τ₁ τ₁' : Ty} {μ₁' : Tr} →
μ ≡ τ₁ ⇒⟨ μ₁' ⟩ τ₁' → CExp[ var ] τ₂} →
Subst t v t' →
((q : μ ≡ ●) → Subst (λ y → (e₁ y) q) v (e₁' q)) →
({τ₁ τ₁' : Ty} {μ₁' : Tr} →
(q : μ ≡ τ₁ ⇒⟨ μ₁' ⟩ τ₁') → Subst (λ y → (e₂ y) q) v (e₂' q)) →
Subst (λ y → Case (t y) (e₁ y) (e₂ y)) v
(Case t' e₁' e₂')
-- Frames
data CFr[_] (var : CTy → Set) : CTy → CTy → Set₁ where
App₁ : {τ₁ τ₂ : CTy} →
(e₂ : CExp[ var ] τ₁) → CFr[ var ] (τ₁ ⇒ τ₂) τ₂
App₂ : {τ₁ τ₂ : CTy} →
(v₁ : CVal[ var ] (τ₁ ⇒ τ₂)) → CFr[ var ] τ₁ τ₂
Is0 : CFr[ var ] Nat Bool
B2S : CFr[ var ] Bool Str
Case : {μ : Tr} {τ : CTy} →
(μ ≡ ● → CExp[ var ] τ) →
({τ₁ τ₁' : Ty} {μ₁ : Tr} →
μ ≡ τ₁ ⇒⟨ μ₁ ⟩ τ₁' → CExp[ var ] τ) →
CFr[ var ] 〚 μ 〛μ τ
Fr-plug : {var : CTy → Set} {τ₁ τ₂ : CTy} →
CFr[ var ] τ₁ τ₂ → CExp[ var ] τ₁ → CExp[ var ] τ₂
Fr-plug (App₁ e₂) e = App e e₂
Fr-plug (App₂ v₁) e = App (Val v₁) e
Fr-plug Is0 e = Is0 e
Fr-plug B2S e = B2S e
Fr-plug (Case e₁ e₂) e = Case e e₁ e₂
-- Evaluation contexts
data CCxt[_] (var : CTy → Set) : CTy → CTy → Set₁ where
Hole : {τ : CTy} → CCxt[ var ] τ τ
Fr : {τ₁ τ₂ τ₃ : CTy} →
CFr[ var ] τ₂ τ₃ → CCxt[ var ] τ₁ τ₂ →
CCxt[ var ] τ₁ τ₃
Cxt-plug : {var : CTy → Set} {τ₁ τ₂ : CTy} →
CCxt[ var ] τ₁ τ₂ → CExp[ var ] τ₁ → CExp[ var ] τ₂
Cxt-plug Hole e = e
Cxt-plug (Fr f c) e = Fr-plug f (Cxt-plug c e)
-- One-step reduction
data Reduce {var : CTy → Set} :
{τ : CTy} →
CExp[ var ] τ → CExp[ var ] τ → Set₁ where
RBeta : {τ τ₁ : CTy} →
{e : var τ → CExp[ var ] τ₁} →
{v : CVal[ var ] τ} →
{e' : CExp[ var ] τ₁} →
Subst e v e' →
Reduce (App (Val (Abs e)) (Val v)) e'
RPlus : {n₁ n₂ : ℕ} →
Reduce (Plus (Val (Num n₁)) (Val (Num n₂))) (Val (Num (n₁ + n₂)))
RIs0 : {n : ℕ} →
Reduce (Is0 (Val (Num n))) (Val (Bol (is0 n)))
RB2S : {b : 𝔹} →
Reduce (B2S (Val (Bol b))) (Val (Str (b2s b)))
RCaseEmp : {τ : CTy} →
(e₁ : ● ≡ ● → CExp[ var ] τ) →
(e₂ : {τ₁ τ₁' : Ty} {μ₁ : Tr} →
● ≡ τ₁ ⇒⟨ μ₁ ⟩ τ₁' → CExp[ var ] τ) →
Reduce (Case (Val Emp) e₁ e₂) (e₁ refl)
RCaseCxt : {τ τ' : Ty} {μ : Tr} {τ₂ : CTy}
{k : CVal[ var ] (〚 τ 〛τ ⇒ 〚 μ 〛μ ⇒ 〚 τ' 〛τ)} →
(e₁ : τ ⇒⟨ μ ⟩ τ' ≡ ● → CExp[ var ] τ₂) →
(e₂ : {τ₁ τ₁' : Ty} {μ₁ : Tr} →
τ ⇒⟨ μ ⟩ τ' ≡ τ₁ ⇒⟨ μ₁ ⟩ τ₁' → CExp[ var ] τ₂) →
Reduce (Case (Val k) e₁ e₂) (e₂ refl)
RFr : {τ₁ τ₂ : CTy} (e e' : CExp[ var ] τ₁)
(f : CFr[ var ] τ₁ τ₂) →
Reduce e e' →
Reduce (Fr-plug f e) (Fr-plug f e')
-- Multi-step reduction
R*Id : {τ : CTy} {e : CExp[ var ] τ} →
Reduce e e
R*Trans : {τ : CTy} →
(e₁ e₂ e₃ : CExp[ var ] τ) →
Reduce e₁ e₂ → Reduce e₂ e₃ →
Reduce e₁ e₃