Add a formalization of the nested-loop language

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Language/Flat.agda

@@ -1,5 +1,15 @@
 {-# OPTIONS --guardedness #-}
-module Lang where
+module Language.Flat where
+
+open import Language.Values using
+    ( Value; int; bool
+    ; ValueType; tint; tbool
+    ; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
+    ; s; s'; s''
+    ; st; st'; st''
+    ; b; b₁; b₂
+    ; z; z₁; z₂
+    )
 
 open import Data.Integer using (ℤ; _+_; +_)
 open import Data.Nat using (ℕ; suc; _<_)
@@ -10,10 +20,6 @@ open import Data.Unit using (⊤; tt)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Product using (Σ; _×_; _,_)
 
-data Value : Set where
-    int : ℤ → Value
-    bool : Bool → Value
-
 data Instruction : Set where
     pushint : ℤ → Instruction
     pushbool : Bool → Instruction
@@ -33,10 +39,7 @@ variable
     i : Instruction
     is is' is'' : Program
     S S' S'' : Env
-    s s' s'' : List Value
     n : ℕ
-    b : Bool
-    z z₁ z₂ : ℤ
 
 data _⇒ₓ_ : Program → Program → Set where
     pushint-skip : is ⇒ₓ is' → (pushint z ∷ is) ⇒ₓ is'
@@ -97,9 +100,6 @@ basic₂ = loop-evalⁿ thenᵉ pushbool-eval thenᵉ break-evalᵗ (pushint-ski
 basic₃ : ( [] , (loop 1 ∷ pushbool false ∷ break ∷ pushint (+ 1) ∷ end ∷ []) , [] ) ⇒* ( (int (+ 1) ∷ []) , [] , [] )
 basic₃ = loop-evalⁿ thenᵉ pushbool-eval thenᵉ break-evalᶠ thenᵉ pushint-eval thenᵉ end-eval thenᵉ (loop-eval⁰ (pushbool-skip (break-skip (pushint-skip end-skip)))) thenᵉ doneᵉ
 
-data ValueType : Set where
-    tint tbool : ValueType
-
 -- A stack type describes the current stack and the continuation types
 infix 35 _⟨_⟩
 record StackType : Set where
@@ -109,7 +109,6 @@ record StackType : Set where
         frames : List (List ValueType)
 
 variable
-    st st' st'' : List ValueType
     F F' F'' : List (List ValueType)
     σ σ' σ'' : StackType
 
@@ -146,6 +145,9 @@ _⊢_↦|_ σ is st = σ ⊢ is ↦* st ⟨ [] ⟩
 basict₁ : [] ⟨ [] ⟩ ⊢ (pushint (+ 1) ∷ pushint (+ 2) ∷ pushint (+ 3) ∷ add ∷ add ∷ []) ↦* (tint ∷ []) ⟨ [] ⟩
 basict₁ = pushint-t thenᵗ pushint-t thenᵗ pushint-t thenᵗ add-t thenᵗ add-t thenᵗ doneᵗ
 
+basict₄ : [] ⟨ [] ⟩ ⊢ (pushint (+ 1) ∷ loop 3 ∷ pushint (+ 2) ∷ add ∷ end ∷ []) ↦* (tint ∷ []) ⟨ [] ⟩
+basict₄ = pushint-t thenᵗ loop-t thenᵗ pushint-t thenᵗ add-t thenᵗ end-t thenᵗ doneᵗ
+
 -- doesn't typecheck: violates type discipline because on break, stack has different type than on end.
 --
 -- basict₂ : ([] ⟨ []  ⟩) ⊢ (loop 1 ∷ pushbool true ∷ break ∷ pushint (+ 1) ∷ end ∷ []) ↦* ([] ⟨ [] ⟩)
@@ -185,12 +187,6 @@ lemma₂ (loop-t thenᵗ ist⊢is↦|st'') =
     (_ , loop-skip is''⇒ₓis' is'₁⇒ₓis'₂  , is'₂↦|st'')
 lemma₂ (end-t thenᵗ rest) = (_ , end-skip , rest)
 
--- what it means for list of value types to describe a list of values
-data ⟦_⟧ˢ : List ValueType → List Value → Set where
-    ⟦⟧ˢ-empty : ⟦ [] ⟧ˢ []
-    ⟦⟧ˢ-int : ⟦ st ⟧ˢ s → ⟦ tint ∷ st ⟧ˢ (int z ∷ s)
-    ⟦⟧ˢ-bool : ⟦ st ⟧ˢ s → ⟦ tbool ∷ st ⟧ˢ (bool b ∷ s)
-
 -- Parameterize by final stack type. The reason to do this is that we want
 -- all continuations to end in the same type, so that control flow doesn't change
 -- what final type the program is evaluated to. This is an unfortunate consequence
@@ -277,4 +273,4 @@ stackToString (bool b ∷ s) = showBool b ++ " :: " ++ stackToString s
 open import IO
 open import Level using (0ℓ)
 
-main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic _ (⟦⟧ˢ-empty , ⟦⟧ᶠ-empty , basict₁)))))
+main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic _ (⟦⟧ˢ-empty , ⟦⟧ᶠ-empty , basict₄)))))

Language/Nested.agda

@@ -0,0 +1,189 @@
+{-# OPTIONS --guardedness #-}
+module Language.Nested where
+
+open import Language.Values using
+    ( Value; int; bool
+    ; ValueType; tint; tbool
+    ; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
+    ; s; s'; s''
+    ; st; st'; st''
+    ; b; b₁; b₂
+    ; z; z₁; z₂
+    )
+
+open import Data.Integer using (ℤ; _+_; +_)
+open import Data.Nat using (ℕ; suc)
+open import Data.Bool using (Bool; true; false)
+open import Data.List using (List; _∷_; []; length)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Product using (Σ; _×_; _,_)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+data Instruction : Set where
+    pushint : ℤ → Instruction
+    pushbool : Bool → Instruction
+    add : Instruction
+
+    loop : ℕ → List Instruction → Instruction
+    break : Instruction
+
+Program : Set
+Program = List Instruction
+
+Env : Set
+Env = List (List Instruction)
+
+variable
+    i : Instruction
+    is is' is'' : Program
+    S S' S'' : Env
+    n : ℕ
+
+Triple : Set
+Triple = List Value × Program × Env
+
+data _⇒_ : Triple → Triple → Set where
+    pushint-eval : ( s , (pushint z ∷ is) , S ) ⇒ ( ((int z) ∷ s) , is , S )
+    pushbool-eval : ( s , (pushbool b ∷ is) , S ) ⇒ ( ((bool b) ∷ s) , is , S )
+    add-eval : ( (int z₁ ∷ int z₂ ∷ s) , (add ∷ is), S ) ⇒ ( ((int (z₁ + z₂)) ∷ s) , is , S )
+
+    loop-eval⁰ : (s , loop 0 is' ∷ is , S) ⇒ (s , is , S)
+    loop-evalⁿ : (s , loop (suc n) is' ∷ is , S) ⇒ (s , is' , (loop n is' ∷ is) ∷ S)
+    break-evalᶠ : (bool false ∷ s , break ∷ is , is' ∷ S) ⇒ (s , is , is' ∷ S)
+    break-evalᵗ : (bool true ∷ s , break ∷ is , (loop n is'' ∷ is') ∷ S) ⇒ (s , is' , S)
+
+    empty-eval : (s , [] , is' ∷ S) ⇒ (s , is' , S)
+
+infixr 30 _thenᵉ_
+data _⇒*_ : Triple → Triple → Set where
+    doneᵉ : ( s , [] , []  ) ⇒* ( s , [] , [] )
+    _thenᵉ_ : ( s , is , S ) ⇒ ( s' , is' , S' ) →
+             ( s' , is' , S' ) ⇒* ( s'' , is'' , S'' ) →
+             ( s , is , S ) ⇒* ( s'' , is'' , S'' )
+
+StackType : Set
+StackType = List ValueType
+
+variable
+    F F' F'' : List (List ValueType)
+    σ σ' σ'' : StackType
+    mst : Maybe StackType
+
+interleaved mutual
+    data _⊢⟨_⟩_↦_ : StackType → Maybe StackType → Instruction → StackType → Set
+    data _⊢⟨_⟩_↦*_ : StackType → Maybe StackType → Program → StackType → Set
+
+    data _⊢⟨_⟩_↦_ where
+        pushint-t : st ⊢⟨ mst ⟩ (pushint z) ↦ (tint ∷ st)
+        pushbool-t : st ⊢⟨ mst ⟩ (pushbool b) ↦ (tbool ∷ st)
+        add-t : (tint ∷ tint ∷ st) ⊢⟨ mst ⟩ add ↦ (tint ∷ st)
+
+        loop-t : st ⊢⟨ just st ⟩ is ↦* st →
+                 st ⊢⟨ mst ⟩ loop n is ↦ st
+        break-t : (tbool ∷ st) ⊢⟨ just st ⟩ break ↦ st
+
+    infixr 30 _thenᵗ_
+    data _⊢⟨_⟩_↦*_ where
+        doneᵗ-just : st ⊢⟨ just st ⟩ [] ↦* st
+        doneᵗ-nothing : st ⊢⟨ nothing ⟩ [] ↦* st
+        _thenᵗ_ : st ⊢⟨ mst ⟩ i ↦ st' →
+                  st' ⊢⟨ mst ⟩ is ↦* st'' →
+                  st ⊢⟨ mst ⟩ (i ∷ is) ↦* st''
+
+_⊢_↦|_ : StackType → Program → StackType → Set
+_⊢_↦|_ st is st' = st ⊢⟨ nothing ⟩ is ↦* st'
+
+basict₄ : [] ⊢ (pushint (+ 1) ∷ loop 3 (pushint (+ 2) ∷ add ∷ []) ∷ pushint (+ 1) ∷ add ∷ []) ↦| (tint ∷ [])
+basict₄ = pushint-t thenᵗ loop-t (pushint-t thenᵗ add-t thenᵗ doneᵗ-just) thenᵗ pushint-t thenᵗ add-t thenᵗ doneᵗ-nothing
+
+data _⊢_↦*_ : StackType → (Program × Env) → StackType → Set where
+    program-typed-flat : st ⊢⟨ nothing ⟩ is ↦* st' →
+                         st ⊢ (is , []) ↦* st'
+    program-typed-rec : ∀ {stˡ} →
+                        st ⊢⟨ just st' ⟩ is ↦* st' →
+                        st' ⊢ (loop n is'' ∷ is' , S) ↦* stˡ →
+                        st ⊢ (is , (loop n is'' ∷ is') ∷ S) ↦* stˡ
+
+skip-loop-continuation : st ⊢ (loop n is ∷ is' , S) ↦* st' →
+                         st ⊢ (is' , S) ↦* st'
+skip-loop-continuation (program-typed-flat (loop-t _ thenᵗ rest)) = (program-typed-flat rest)
+skip-loop-continuation (program-typed-rec (loop-t _ thenᵗ rest) frames) = (program-typed-rec rest frames)
+
+preservation : ∀ {stˡ} →
+               (s , is , S) ⇒ (s' , is' , S') →
+               ⟦ st ⟧ˢ s →
+               st ⊢ (is , S) ↦* stˡ →
+               Σ StackType (λ st' → ⟦ st' ⟧ˢ s' × st' ⊢ (is' , S') ↦* stˡ)
+preservation pushint-eval ⟦st⟧ (program-typed-flat (pushint-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
+preservation pushint-eval ⟦st⟧ (program-typed-rec (pushint-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
+preservation pushbool-eval ⟦st⟧ (program-typed-flat (pushbool-t thenᵗ rest)) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-flat rest))
+preservation pushbool-eval ⟦st⟧ (program-typed-rec (pushbool-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-rec rest frames))
+preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-flat (add-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
+preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-rec (add-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
+preservation loop-eval⁰ ⟦st⟧ (program-typed-flat ((loop-t _) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-flat rest))
+preservation loop-eval⁰ ⟦st⟧ (program-typed-rec ((loop-t _) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest) frames)
+preservation loop-evalⁿ ⟦st⟧ (program-typed-flat ((loop-t loopt) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-flat (loop-t loopt thenᵗ rest))))
+preservation loop-evalⁿ ⟦st⟧ (program-typed-rec ((loop-t loopt) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-rec (loop-t loopt thenᵗ rest) frames)))
+preservation break-evalᵗ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , skip-loop-continuation frames)
+preservation break-evalᶠ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest frames))
+preservation empty-eval ⟦st⟧ (program-typed-rec (doneᵗ-just) frames) = (_ , ⟦st⟧ , frames)
+
+progress : ∀ {stˡ} →
+           st ⊢ (is , S) ↦* stˡ →
+           ⟦ st ⟧ˢ s →
+           (Σ Triple ((s , is , S) ⇒_)) ⊎ (is ≡ [] × S ≡ [] × ⟦ stˡ ⟧ˢ s)
+progress (program-typed-flat (pushint-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushint-eval)
+progress (program-typed-rec (pushint-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushint-eval)
+progress (program-typed-flat (pushbool-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushbool-eval)
+progress (program-typed-rec (pushbool-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushbool-eval)
+progress (program-typed-flat (add-t thenᵗ rest)) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
+progress (program-typed-rec (add-t thenᵗ rest) frames) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
+progress {is = loop 0 is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
+progress {is = loop 0 is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
+progress {is = loop (suc n) is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
+progress {is = loop (suc n) is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
+progress {s = bool true ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᵗ)
+progress {s = bool false ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᶠ)
+progress {is = []} (program-typed-rec (doneᵗ-just) frames) ⟦st⟧ = inj₁ (_ , empty-eval)
+progress {is = []} (program-typed-flat (doneᵗ-nothing)) ⟦st⟧ = inj₂ (refl , refl , ⟦st⟧)
+
+{-# TERMINATING #-} -- evaluation always terminates, but proving it is tedious
+static-dynamic-help : ∀ {stˡ} →
+                      st ⊢ (is , S) ↦* stˡ →
+                      ⟦ st ⟧ˢ s →
+                      Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , S) ⇒* (sˡ , [] , []))
+static-dynamic-help {s = s} frames ⟦st⟧
+    with progress frames ⟦st⟧
+...   | inj₁ ((s' , is' , S') , is⇒is') =
+        let (st' , (⟦st'⟧ , frames')) = preservation is⇒is' ⟦st⟧ frames in
+        let (sˡ , (⟦stˡ⟧ , is'⇒*[])) = static-dynamic-help frames' ⟦st'⟧ in
+        (sˡ , (⟦stˡ⟧ , is⇒is' thenᵉ is'⇒*[]))
+...   | inj₂ (refl , refl , ⟦stˡ⟧) = (s , (⟦stˡ⟧ , doneᵉ))
+
+
+static-dynamic : ∀ {stˡ} →
+                 st ⊢ is ↦| stˡ →
+                 ⟦ st ⟧ˢ s →
+                 Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , []) ⇒* (sˡ , [] , []))
+static-dynamic st⊢is↦|stˡ = static-dynamic-help (program-typed-flat st⊢is↦|stˡ)
+
+-- Copied from Flat.agda
+
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Integer.Show using () renaming (show to showℤ)
+open import Data.Bool.Show using () renaming (show to showBool)
+open import Data.String using (String; _++_)
+open import Data.Product using (proj₁)
+
+stackToString : List Value → String
+stackToString [] = "[]"
+stackToString (int i ∷ s) = showℤ i ++ " :: " ++ stackToString s
+stackToString (bool b ∷ s) = showBool b ++ " :: " ++ stackToString s
+
+open import IO
+open import Level using (0ℓ)
+
+main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic basict₄ ⟦⟧ˢ-empty))))

Language/Values.agda

@@ -0,0 +1,24 @@
+module Language.Values where
+
+open import Data.Integer using (ℤ)
+open import Data.Bool using (Bool)
+open import Data.List using (List; []; _∷_)
+
+data Value : Set where
+    int : ℤ → Value
+    bool : Bool → Value
+
+data ValueType : Set where
+    tint tbool : ValueType
+
+variable
+    s s' s'' : List Value
+    st st' st'' : List ValueType
+    b b₁ b₂ : Bool
+    z z₁ z₂ : ℤ
+
+-- what it means for list of value types to describe a list of values
+data ⟦_⟧ˢ : List ValueType → List Value → Set where
+    ⟦⟧ˢ-empty : ⟦ [] ⟧ˢ []
+    ⟦⟧ˢ-int : ⟦ st ⟧ˢ s → ⟦ tint ∷ st ⟧ˢ (int z ∷ s)
+    ⟦⟧ˢ-bool : ⟦ st ⟧ˢ s → ⟦ tbool ∷ st ⟧ˢ (bool b ∷ s)