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

{- Explicit type annotation: -}
_ : Term
_ =
  `let ($ true of high) ∶ ` Bool of ⋆ at pos 0 `in
  (` 0)


{- Statically accepted: -}
N : Term
N =
  -- dumb    : 𝔹 of high → 𝔹 of low
  `let ƛ⟦ low ⟧ ` Bool of l high ˙ $ false of low of low `in
  -- input   : 𝔹 of high
  `let (user-input · $ tt of low at pos 0) `in
  -- result  : 𝔹 of low
  `let ` 1 {- dumb -} · ` 0 {- input -} at pos 1 `in
    (publish {- publish -} · ` 0 {- result -} at pos 2)

{- `N` is well-typed -}
⊢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))))

{- Compile `N` to CC -}
𝒞N  = compile N ⊢N
⊢𝒞N = compile-preserve N ⊢N

{- `N` evaluates to `tt` -}
_ : ∅ ∣ 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))))

{- Statically rejected because of explicit flow -}
N′ : Term
N′ =
  -- id      : 𝔹 of low → 𝔹 of low
  `let ƛ⟦ low ⟧ ` Bool of l low ˙ ` 0 of low `in
  -- input   : 𝔹 of high
  `let (user-input · $ tt of low at pos 0) `in
  -- result  : 𝔹 of low
  `let ` 1 {- dumb -} · ` 0 {- input -} at pos 1 `in
    (publish {- publish -} · ` 0 {- result -} at pos 2)

-- ⊢N′ : [] ; l low ⊢ᴳ N′ ⦂ ` Unit of l low
-- ⊢N′ =
--   (⊢let (⊢lam (⊢var refl))
--   (⊢let (⊢app ⊢user-input ⊢const ≲-refl ≾-refl ≾-refl)
--   (⊢let (⊢app (⊢var refl) (⊢var refl) (≲-ty (≾-l {!!} {- high ⋠ low -}) ≲-ι) ≾-refl ≾-refl)
--     (⊢app ⊢publish (⊢var refl) ≲-refl ≾-refl ≾-refl))))


{- Statically rejected because of implicit flow -}
M : Term
M =
  -- flip    : 𝔹 of high → 𝔹 of low
  `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
  -- input   : 𝔹 of high
  `let (user-input · $ tt of low at pos 1) `in
  -- result  : 𝔹 of low
  `let ` 1 {- flip -} · ` 0 {- input -} at pos 2 `in
    (publish · ` 0 {- result -} at pos 3)

-- ⊢M : [] ; l low ⊢ᴳ M ⦂ ` Unit of l low
-- ⊢M =
--   (⊢let (⊢ann (⊢lam (⊢if (⊢var refl) ⊢const ⊢const refl)) {!!} {- 𝔹 of high → 𝔹 of high ⋦ 𝔹 of high → 𝔹 of low-})
--   (⊢let (⊢app ⊢user-input ⊢const ≲-refl ≾-refl ≾-refl)
--   (⊢let (⊢app (⊢var refl) (⊢var refl) ≲-refl ≾-refl ≾-refl)
--     (⊢app ⊢publish (⊢var refl) ≲-refl ≾-refl ≾-refl))))


{- We can make the type annotation of `flip` to be more dynamic and defer the checking until runtime: -}
M* : Term
M* =
  -- flip    : 𝔹 of ⋆ → 𝔹 of low
  `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
  -- input   : 𝔹 of high
  `let (user-input · $ tt of low at pos 2) `in
  -- result  : 𝔹 of low
  `let ` 1 {- flip -} · ` 0 {- input -} at pos 3 `in
    (publish · ` 0 {- result -} 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))))

{- Compile `M*` to CC -}
𝒞M*  = compile M* ⊢M*
⊢𝒞M* = compile-preserve M* ⊢M*

{- Alternatively, we can give `result` an extra annotation: -}
M*′ : Term
M*′ =
  -- flip    : 𝔹 of high → 𝔹 of high
  `let ƛ⟦ low ⟧ ` Bool of l high ˙ if (` 0) then $ false of low else $ true of low at (pos 0) of low `in
  -- input   : 𝔹 of high
  `let (user-input · $ tt of low at pos 1) `in
  -- result  : 𝔹 of ⋆
  `let (` 1 {- flip -} · ` 0 {- input -} at pos 2) ∶ ` Bool of ⋆ at pos 3 `in
    (publish · ` 0 {- result -} at pos 4)

{- It's well-typed too -}
⊢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))))

{- Take a look at the compiled CC term. Note the casts inserted: -}
_ :
  𝒞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  {- 1 -}
    —→⟨ ξ {F = let□ _} (fun-cast V-ƛ (V-cast V-const (I-base-inj _)) (I-fun _ I-label I-label)) ⟩  {- ξ fun-cast -}
  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  {- 2 -}
    —→⟨ ξ {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  {- 3 -}
    —→⟨ ξ {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  {- 4 -}
    —→⟨ ξ {F = let□ _} (ξ {F = □⟨ _ ⟩} (prot-ctx (if-cast-true (I-base-inj _)))) ⟩  {- ξ ξ prot-ctx if-cast-true -}
  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  {- 5 -}
    —→⟨ ξ {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  {- 6 -}
    —→⟨ ξ {F = let□ _} (cast (V-cast V-const (I-base-inj _)) (A-base-proj _) (cast-base-proj-blame (λ ()) {- high ⋠ low -})) ⟩
  `let (error (blame (pos 1))) _ ∣ ∅ ∣ low  {- 7 -}
    —→⟨ ξ-err {F = let□ _} ⟩
  error (blame (pos 1)) ∣ ∅ ∣ _  {- 8 -}
    ∎