module ExamplePrograms.Demo.Example1 where
open import Data.Unit
open import Data.List
open import Data.Bool renaming (Bool to 𝔹)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Common.Utils
open import Common.Types
open import Common.BlameLabels
open import Surface.SurfaceLang
open import CC.CCStatics renaming (Term to CCTerm;
`_ to var; $_of_ to const_of_; ƛ⟦_⟧_˙_of_ to lam⟦_⟧_˙_of_; !_ to deref)
open import CC.Compile
open import CC.Reduction
open import CC.MultiStep
open import CC.BigStep
open import Memory.Heap CCTerm Value
open import ExamplePrograms.Demo.Common
A₁ : Type
A₁ = ⟦ ⋆ ⟧ (` Bool of ⋆) ⇒ (` Bool of l high) of l low
A₂ : Type
A₂ = Ref (` Unit of ⋆) of l high
_ : Term
_ = (ƛ⟦ low ⟧ ` Bool of ⋆ ˙ ` 0 of high) · (` 0) at pos 0
_ : Term
_ =
`let ($ true of high) ∶ ` Bool of ⋆ at pos 0 `in
(` 0)
N : Term
N =
`let ƛ⟦ low ⟧ ` Bool of l high ˙ $ false of low of low `in
`let (user-input · $ tt of low at pos 0) `in
`let ` 1 · ` 0 at pos 1 `in
(publish · ` 0 at pos 2)
⊢N : [] ; l low ⊢ᴳ N ⦂ ` Unit of l low
⊢N =
(⊢let (⊢lam ⊢const)
(⊢let (⊢app ⊢user-input ⊢const ≲-refl ≾-refl ≾-refl)
(⊢let (⊢app (⊢var refl) (⊢var refl) ≲-refl ≾-refl ≾-refl)
(⊢app ⊢publish (⊢var refl) ≲-refl ≾-refl ≾-refl))))
𝒞N = compile N ⊢N
⊢𝒞N = compile-preserve N ⊢N
_ : ∅ ∣ low ⊢ 𝒞N ⇓ const tt of low ∣ ∅
_ = ⇓-let (⇓-val V-ƛ)
(⇓-let (⇓-app (⇓-val V-ƛ) (⇓-val V-const) (⇓-val V-const))
(⇓-let (⇓-app (⇓-val V-ƛ) (⇓-val V-const) (⇓-val V-const))
(⇓-app (⇓-val V-ƛ) (⇓-val V-const) (⇓-val V-const))))
N′ : Term
N′ =
`let ƛ⟦ low ⟧ ` Bool of l low ˙ ` 0 of low `in
`let (user-input · $ tt of low at pos 0) `in
`let ` 1 · ` 0 at pos 1 `in
(publish · ` 0 at pos 2)
M : Term
M =
`let (ƛ⟦ low ⟧ ` Bool of l high ˙ if (` 0) then $ false of low else $ true of low at (pos 0) of low) ∶
⟦ l low ⟧ (` Bool of l high) ⇒ (` Bool of l low) of l low at pos 1 `in
`let (user-input · $ tt of low at pos 1) `in
`let ` 1 · ` 0 at pos 2 `in
(publish · ` 0 at pos 3)
M* : Term
M* =
`let (ƛ⟦ low ⟧ ` Bool of ⋆ ˙ if (` 0) then $ false of low else $ true of low at (pos 0) of low) ∶
⟦ l low ⟧ (` Bool of ⋆) ⇒ (` Bool of l low) of l low at pos 1 `in
`let (user-input · $ tt of low at pos 2) `in
`let ` 1 · ` 0 at pos 3 `in
(publish · ` 0 at pos 4)
⊢M* : [] ; l low ⊢ᴳ M* ⦂ ` Unit of l low
⊢M* =
(⊢let (⊢ann (⊢lam (⊢if (⊢var refl) ⊢const ⊢const refl)) (≲-ty ≾-refl (≲-fun ≾-refl (≲-ty ≾-⋆r ≲ᵣ-refl) (≲-ty ≾-⋆l ≲ᵣ-refl))))
(⊢let (⊢app ⊢user-input ⊢const ≲-refl ≾-refl ≾-refl)
(⊢let (⊢app (⊢var refl) (⊢var refl) (≲-ty ≾-⋆r ≲-ι) ≾-refl ≾-refl)
(⊢app ⊢publish (⊢var refl) (≲-ty ≾-refl ≲ᵣ-refl) ≾-refl ≾-refl))))
𝒞M* = compile M* ⊢M*
⊢𝒞M* = compile-preserve M* ⊢M*
M*′ : Term
M*′ =
`let ƛ⟦ low ⟧ ` Bool of l high ˙ if (` 0) then $ false of low else $ true of low at (pos 0) of low `in
`let (user-input · $ tt of low at pos 1) `in
`let (` 1 · ` 0 at pos 2) ∶ ` Bool of ⋆ at pos 3 `in
(publish · ` 0 at pos 4)
⊢M*′ : [] ; l low ⊢ᴳ M*′ ⦂ ` Unit of l low
⊢M*′ =
(⊢let (⊢lam (⊢if (⊢var refl) ⊢const ⊢const refl))
(⊢let (⊢app ⊢user-input ⊢const ≲-refl ≾-refl ≾-refl)
(⊢let (⊢ann (⊢app (⊢var refl) (⊢var refl) ≲-refl ≾-refl ≾-refl) (≲-ty ≾-⋆r ≲ᵣ-refl))
(⊢app ⊢publish (⊢var refl) (≲-ty ≾-⋆l ≲ᵣ-refl) ≾-refl ≾-refl))))
_ :
𝒞M* ≡
let c~ = ~-ty ~ₗ-refl (~-fun ~ₗ-refl (~-ty ⋆~ ~-ι) (~-ty ⋆~ ~-ι)) in
let c₁ = cast (⟦ l low ⟧ (` Bool of ⋆) ⇒ (` Bool of ⋆) of l low)
(⟦ l low ⟧ (` Bool of ⋆) ⇒ (` Bool of l low) of l low)
(pos 1) c~ in
let c₂ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) (~-ty ~⋆ ~-ι) in
(`let (lam⟦ low ⟧ ` Bool of ⋆ ˙ if (var 0) (` Bool of l low) (const false of low) (const true of low) of low ⟨ c₁ ⟩)
(`let (compile {[]} user-input ⊢user-input · const tt of low)
(`let (var 1 · var 0 ⟨ c₂ ⟩)
(compile {[]} publish ⊢publish · var 0))))
_ = refl
_ : 𝒞M* ∣ ∅ ∣ low —↠ error (blame (pos 1)) ∣ ∅
_ =
𝒞M* ∣ ∅ ∣ low
—→⟨ β-let (V-cast V-ƛ (I-fun _ I-label I-label)) ⟩
_ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (β V-const) ⟩
_ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (prot-val V-const) ⟩
_ ∣ ∅ ∣ low
—→⟨ β-let V-const ⟩
let c₁ = cast (⟦ _ ⟧ (` Bool of ⋆) ⇒ (` Bool of ⋆) of _) (⟦ _ ⟧ (` Bool of ⋆) ⇒ (` Bool of l low) of _ ) (pos 1) _ in
let c₂ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
`let (lam⟦ low ⟧ _ ˙ if (var 0) _ _ _ of low ⟨ c₁ ⟩ · const true of high ⟨ c₂ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (fun-cast V-ƛ (V-cast V-const (I-base-inj _)) (I-fun _ I-label I-label)) ⟩
let c₁ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
let c₂ = cast (` Bool of ⋆) (` Bool of ⋆) (pos 1) _ in
let c₃ = cast (` Bool of ⋆) (` Bool of l low) (pos 1) _ in
`let ((lam⟦ low ⟧ _ ˙ if (var 0) _ _ _ of low · const true of high ⟨ c₁ ⟩ ⟨ c₂ ⟩) ⟨ c₃ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (ξ {F = (_ ·□) V-ƛ} (cast (V-cast V-const (I-base-inj _)) (A-base-id _) cast-base-id))) ⟩
let c₁ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
let c₂ = cast (` Bool of ⋆) (` Bool of l low) (pos 1) _ in
`let ((lam⟦ low ⟧ _ ˙ _ of low · const true of high ⟨ c₁ ⟩) ⟨ c₂ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (β (V-cast V-const (I-base-inj _)))) ⟩
let c₁ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
let c₂ = cast (` Bool of ⋆) (` Bool of l low) (pos 1) _ in
`let (prot low (if (const true of high ⟨ c₁ ⟩) _ (const false of low) _) ⟨ c₂ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (prot-ctx (if-cast-true (I-base-inj _)))) ⟩
let c₁ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
let c₂ = cast (` Bool of ⋆) (` Bool of l low) (pos 1) _ in
`let (prot low (prot high (cast-pc ⋆ (const false of low)) ⟨ c₁ ⟩) ⟨ c₂ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (prot-ctx (ξ {F = □⟨ _ ⟩} (prot-ctx (β-cast-pc V-const))))) ⟩
_ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (prot-ctx (ξ {F = □⟨ _ ⟩} (prot-val V-const)))) ⟩
_ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (prot-val (V-cast V-const (I-base-inj _)))) ⟩
let c₁ = cast (` Bool of l high) (` Bool of ⋆) (pos 3) _ in
let c₂ = cast (` Bool of ⋆) (` Bool of l low) (pos 1) _ in
`let (const false of high ⟨ c₁ ⟩ ⟨ c₂ ⟩) _ ∣ ∅ ∣ low
—→⟨ ξ {F = let□ _} (cast (V-cast V-const (I-base-inj _)) (A-base-proj _) (cast-base-proj-blame (λ ()) )) ⟩
`let (error (blame (pos 1))) _ ∣ ∅ ∣ low
—→⟨ ξ-err {F = let□ _} ⟩
error (blame (pos 1)) ∣ ∅ ∣ _
∎