Added step function

prototyping/Luau/Heap.agda

@@ -3,19 +3,29 @@ module Luau.Heap where
 open import FFI.Data.Maybe using (Maybe; just)
 open import FFI.Data.Vector using (Vector; length; snoc)
 open import Luau.Addr using (Addr)
-open import Luau.Value using (Value)
+open import Luau.Var using (Var)
+open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
 
-Heap = Vector Value
+data HeapValue : Set where
+  function⟨_⟩_end : Var → Block → HeapValue
 
-data _≡_⊕_↦_ : Heap → Heap → Addr → Value → Set where
+Heap = Vector HeapValue
+
+data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where
 
   defn : ∀ {H val} →
 
     -----------------------------------
     (snoc H val) ≡ H ⊕ (length H) ↦ val
 
-lookup : Heap → Addr → Maybe Value
+lookup : Heap → Addr → Maybe HeapValue
 lookup = FFI.Data.Vector.lookup
 
 emp : Heap
 emp = FFI.Data.Vector.empty
+
+data AllocResult (H : Heap) (V : HeapValue) : Set where
+  ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
+
+alloc : ∀ H V → AllocResult H V
+alloc H V = ok (length H) (snoc H V) defn

prototyping/Luau/OpSem.agda

@@ -2,10 +2,10 @@ module Luau.OpSem where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just)
-open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup)
+open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function⟨_⟩_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
-open import Luau.Value using (function⟨_⟩_end; addr; val)
+open import Luau.Value using (addr; val)
 
 data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
 data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
@@ -41,10 +41,10 @@ data _⊢_⟶ᴱ_⊣_  where
     ------------------------------------------
     H ⊢ (block B end) ⟶ᴱ (block B′ end) ⊣ H′
 
-  return : ∀ {H M B} →
+  return : ∀ {H V B} →
  
-    ----------------------------
+    ---------------------------------------------------
-    H ⊢ (block return M ∙ B end) ⟶ᴱ M ⊣ H
+    H ⊢ (block return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H
 
   done : ∀ {H} →
  
@@ -53,7 +53,13 @@ data _⊢_⟶ᴱ_⊣_  where
   
 data _⊢_⟶ᴮ_⊣_  where
 
-  local : ∀ {H x v B} →
+  local : ∀ {H H′ x M M′ B} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    -------------------------------------------------
+    H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′
+
+  subst : ∀ {H x v B} →
   
     -------------------------------------------------
     H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
@@ -63,3 +69,10 @@ data _⊢_⟶ᴮ_⊣_  where
     H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ C end) →
     --------------------------------------------------------------
     H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
+
+  return : ∀ {H H′ M M′ B} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    --------------------------------------------
+    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
+

prototyping/Luau/Value.agda

@@ -7,10 +7,9 @@ open import Luau.Var using (Var)
 data Value : Set where
   nil : Value
   addr : Addr → Value
-  function⟨_⟩_end : Var → Block → Value
 
 val : Value → Expr
 val nil = nil
 val (addr a) = addr a
-val (function⟨ x ⟩ B end) = function⟨ x ⟩ B end
+
 

prototyping/Properties/Remember.agda

@@ -0,0 +1,9 @@
+module Properties.Remember where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+
+data Remember {A : Set} (a : A) : Set where
+  _,_ : ∀ b → (a ≡ b) → Remember(a)
+  
+remember : ∀ {A} (a : A) → Remember(a)
+remember a = (a , refl)

prototyping/Properties/Step.agda

@@ -0,0 +1,71 @@
+module Properties.Step where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Maybe using (just; nothing)
+open import Luau.Heap using (Heap; lookup; alloc; ok; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
+open import Luau.Substitution using (_[_/_]ᴮ)
+open import Luau.Value using (nil; addr; val)
+open import Properties.Remember using (remember; _,_)
+
+data RuntimeErrorᴮ (H : Heap) : Block → Set
+data RuntimeErrorᴱ (H : Heap) : Expr → Set
+
+data RuntimeErrorᴱ H where
+  NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
+  UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
+  SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
+  app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
+  block : ∀ {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block B end)
+
+data RuntimeErrorᴮ H where
+  local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
+  return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
+
+data StepResultᴮ (H : Heap) (B : Block) : Set
+data StepResultᴱ (H : Heap) (M : Expr) : Set
+
+data StepResultᴮ H B where
+  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
+  return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B
+  done : (B ≡ done) → StepResultᴮ H B
+  error : (RuntimeErrorᴮ H B) → StepResultᴮ H B
+
+data StepResultᴱ H M where
+  step : ∀ H′ M′ → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → StepResultᴱ H M
+  value : ∀ V → (M ≡ val V) → StepResultᴱ H M
+  error : (RuntimeErrorᴱ H M) → StepResultᴱ H M
+
+stepᴱ : ∀ H M → StepResultᴱ H M
+stepᴮ : ∀ H B → StepResultᴮ H B
+
+stepᴱ H nil = value nil refl
+stepᴱ H (var x) = error (UnboundVariable x)
+stepᴱ H (addr a) = value (addr a) refl
+stepᴱ H (M $ N) with stepᴱ H M
+stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
+stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
+stepᴱ H (addr a $ N) | value (addr a) refl with remember (lookup H a)
+stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
+stepᴱ H (addr a $ N) | value (addr a) refl | (just(function⟨ x ⟩ B end) , p) = step H (block local x ← N ∙ B end) (beta p)
+stepᴱ H (M $ N) | error E = error (app E)
+stepᴱ H (function⟨ x ⟩ B end) with alloc H (function⟨ x ⟩ B end)
+stepᴱ H (function⟨ x ⟩ B end) | ok a H′ p = step H′ (addr a) (function p)
+stepᴱ H (block B end) with stepᴮ H B
+stepᴱ H (block B end) | step H′ B′ D = step H′ (block B′ end) (block D)
+stepᴱ H (block (return _ ∙ B′) end) | return V refl = step H (val V) return
+stepᴱ H (block done end) | done refl = step H nil done
+stepᴱ H (block B end) | error E = error (block E)
+
+stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function⟨ x ⟩ C end)
+stepᴮ H (function f ⟨ x ⟩ C end ∙ B) | ok a H′ p = step H′ (B [ addr a / f ]ᴮ) (function p)
+stepᴮ H (local x ← M ∙ B) with stepᴱ H M
+stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
+stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / x ]ᴮ) subst
+stepᴮ H (local x ← M ∙ B) | error E = error (local E)
+stepᴮ H (return M ∙ B) with stepᴱ H M
+stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
+stepᴮ H (return _ ∙ B) | value V refl = return V refl
+stepᴮ H (return M ∙ B) | error E = error (return E)
+stepᴮ H done = done refl