First cut operational semantics

prototyping/Examples.agda

@@ -1,4 +1,5 @@
 module Examples where
 
 import Examples.Syntax
+import Examples.OpSem
 

prototyping/Examples/OpSem.agda

@@ -0,0 +1,11 @@
+module Examples.OpSem where
+
+open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; local)
+open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_end)
+open import Luau.Heap using (emp)
+
+x = var "x"
+
+ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
+ex1 = local
+

prototyping/Examples/SmokeTestOutput.lua

@@ -0,0 +1,12 @@
+local function id(x)
+  return x
+end
+local function comp(f)
+  return function(g)
+    return function(x)
+      return f(g(x))
+    end
+  end
+end
+local id2 = id(id)
+local nil2 = id2(nil)

prototyping/Examples/Syntax.agda

@@ -2,7 +2,7 @@ module Examples.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.String using (_++_)
-open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; _∙; _∙_)
+open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
 f = var "f"
@@ -12,11 +12,11 @@ ex1 : exprToString(f $ x) ≡
   "f(x)"
 ex1 = refl
 
-ex2 : blockToString(return nil ∙) ≡
+ex2 : blockToString(return nil ∙ done) ≡
   "return nil"
 ex2 = refl
 
-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
   "local function f(x)\n" ++
   "  return x\n" ++
   "end\n" ++

prototyping/FFI/Data/HaskellInt.agda

@@ -0,0 +1,14 @@
+module FFI.Data.HaskellInt where
+
+open import Agda.Builtin.Int using (Int)
+
+{-# FOREIGN GHC import qualified Data.Int #-}
+
+postulate HaskellInt : Set
+{-# COMPILE GHC HaskellInt = type Data.Int.Int #-}
+
+postulate
+  intToHaskellInt : Int → HaskellInt
+  haskellIntToInt : HaskellInt → Int
+{-# COMPILE GHC intToHaskellInt = fromIntegral #-}
+{-# COMPILE GHC haskellIntToInt = fromIntegral #-}

prototyping/FFI/Data/Vector.agda

@@ -1,6 +1,9 @@
 module FFI.Data.Vector where
 
+open import Agda.Builtin.Int using (Int; pos; negsuc)
+open import Agda.Builtin.Nat using (Nat)
 open import FFI.Data.Bool using (Bool; false; true)
+open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 
 {-# FOREIGN GHC import qualified Data.Vector #-}
@@ -14,10 +17,16 @@ postulate
   null : ∀ {A} → (Vector A) → Bool
   unsafeHead : ∀ {A} → (Vector A) → A
   unsafeTail : ∀ {A} → (Vector A) → (Vector A)
+  hLength : ∀ {A} → (Vector A) → HaskellInt
+  hLookup : ∀ {A} → (Vector A) → HaskellInt → (Maybe A)
+  snoc : ∀ {A} → (Vector A) → A → (Vector A)
 {-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
 {-# COMPILE GHC null = \_ -> Data.Vector.null #-}
 {-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
 {-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
+{-# COMPILE GHC hLength = \_ -> Data.Vector.length #-}
+{-# COMPILE GHC hLookup = \_ -> (Data.Vector.!?) #-}
+{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}
 
 head : ∀ {A} → (Vector A) → (Maybe A)
 head vec with null vec
@@ -29,3 +38,10 @@ tail vec with null vec
 tail vec | false = unsafeTail vec
 tail vec | true = empty
 
+length : ∀ {A} → (Vector A) → Nat
+length vec with haskellIntToInt(hLength vec)
+length vec | pos n = n
+length vec | negsuc n = 0
+
+lookup : ∀ {A} → (Vector A) → Nat → Maybe A
+lookup vec n = hLookup vec (intToHaskellInt (pos n))

prototyping/Luau/Addr.agda

@@ -0,0 +1,21 @@
+module Luau.Addr where
+
+open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Int using (Int; primShowInteger; pos)
+open import Agda.Builtin.Nat using (Nat; _==_)
+open import Agda.Builtin.String using (String)
+open import Agda.Builtin.TrustMe using (primTrustMe)
+open import Properties.Dec using (Dec; yes; no; ⊥)
+
+Addr : Set
+Addr = Nat
+
+addrToString : Addr → String
+addrToString a = primShowInteger (pos a)
+
+_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b)
+a ≡ᴬ b with a == b
+a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥
+a ≡ᴬ b | true = yes primTrustMe
+

prototyping/Luau/Heap.agda

@@ -0,0 +1,21 @@
+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)
+
+Heap = Vector Value
+
+data _≡_⊕_↦_ : Heap → Heap → Addr → Value → Set where
+
+  defn : ∀ {H val} →
+
+    -----------------------------------
+    (snoc H val) ≡ H ⊕ (length H) ↦ val
+
+lookup : Heap → Addr → Maybe Value
+lookup = FFI.Data.Vector.lookup
+
+emp : Heap
+emp = FFI.Data.Vector.empty

prototyping/Luau/OpSem.agda

@@ -0,0 +1,65 @@
+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.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)
+
+data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
+data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
+
+data _⊢_⟶ᴱ_⊣_  where
+
+  nil : ∀ {H} →
+
+    -------------------
+    H ⊢ nil ⟶ᴱ nil ⊣ H
+
+  function : ∀ {H H′ a x B} →
+
+    H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ B end) →
+    -------------------------------------------
+    H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
+
+  app : ∀ {H H′ M M′ N} →
+  
+    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
+    -----------------------------
+    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
+
+  beta : ∀ {H M a x B} →
+  
+    (lookup H a) ≡ just(function⟨ x ⟩ B end) →
+    -----------------------------------------------------
+    H ⊢ (addr a $ M) ⟶ᴱ (block local x ← M ∙ B end) ⊣ H
+
+  block : ∀ {H H′ B B′} →
+ 
+    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
+    ------------------------------------------
+    H ⊢ (block B end) ⟶ᴱ (block B′ end) ⊣ H′
+
+  return : ∀ {H M B} →
+ 
+    ----------------------------
+    H ⊢ (block return M ∙ B end) ⟶ᴱ M ⊣ H
+
+  done : ∀ {H} →
+ 
+    ---------------------------------
+    H ⊢ (block done end) ⟶ᴱ nil ⊣ H
+  
+data _⊢_⟶ᴮ_⊣_  where
+
+  local : ∀ {H x v B} →
+  
+    -------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
+
+  function : ∀ {H H′ a f x B C} →
+  
+    H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ C end) →
+    --------------------------------------------------------------
+    H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′

prototyping/Luau/Substitution.agda

@@ -0,0 +1,30 @@
+module Luau.Substitution where
+
+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 (Value; val)
+open import Luau.Var using (Var; _≡ⱽ_)
+open import Properties.Dec using (Dec; yes; no)
+
+_[_/_]ᴱ : Expr → Value → Var → Expr
+_[_/_]ᴮ : Block → Value → Var → Block
+var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr
+_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block
+
+nil [ v / x ]ᴱ = nil
+var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
+addr a [ v / x ]ᴱ = addr a
+(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
+function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ y) end
+block C end [ v / x ]ᴱ = block C [ v / x ]ᴮ end
+
+(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
+(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y))
+(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
+done [ v / x ]ᴮ = done
+
+var y [ v / x ]ᴱwhenever yes p = val v
+var y [ v / x ]ᴱwhenever no p = var y
+
+B [ v / x ]ᴮunless yes p = B
+B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ
+

prototyping/Luau/Syntax.agda

@@ -1,27 +1,17 @@
 module Luau.Syntax where
 
-open import Agda.Builtin.String using (String)
+open import Luau.Var using (Var)
+open import Luau.Addr using (Addr)
 
 infixr 5 _∙_
 
-data Type : Set where
-  nil : Type
-  _⇒_ : Type → Type → Type
-  none : Type
-  any : Type
-  _∪_ : Type → Type → Type
-  _∩_ : Type → Type → Type
-
-Var : Set
-Var = String
-
 data Block : Set
 data Stat : Set
 data Expr : Set
 
 data Block where
   _∙_ : Stat → Block → Block
-  _∙ : Stat → Block
+  done : Block
 
 data Stat where
   function_⟨_⟩_end : Var → Var → Block → Stat
@@ -31,5 +21,7 @@ data Stat where
 data Expr where
   nil : Expr
   var : Var → Expr
+  addr : Addr → Expr
   _$_ : Expr → Expr → Expr
   function⟨_⟩_end : Var → Block → Expr
+  block_end : Block → Expr

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Type; Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; _∙; _∙_)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
@@ -117,11 +117,9 @@ blockFromJSON (object obj) | nothing | _ = Left "AstStatBlock missing type"
 blockFromJSON _ = Left "AstBlock not an array or AstStatBlock object"
 
 blockFromArray arr with head arr
-blockFromArray arr | nothing = Left "Block should be a non-empty array"
+blockFromArray arr | nothing = Right done
 blockFromArray arr | just value with statFromJSON value
 blockFromArray arr | just value | Left err = Left err
-blockFromArray arr | just value | Right S with null (tail arr)
-blockFromArray arr | just value | Right S | true = Right (S ∙)
-blockFromArray arr | just value | Right S | false with blockFromArray(tail arr)
-blockFromArray arr | just value | Right S | false | Left err = Left (err)
-blockFromArray arr | just value | Right S | false | Right B  = Right (S ∙ B)
+blockFromArray arr | just value | Right S with blockFromArray(tail arr)
+blockFromArray arr | just value | Right S | Left err = Left (err)
+blockFromArray arr | just value | Right S | Right B  = Right (S ∙ B)

prototyping/Luau/Syntax/ToString.agda

@@ -1,8 +1,9 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Type; Block; Stat; Expr; nil; var; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; _∙)
-
+open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_end)
 open import FFI.Data.String using (String; _++_)
+open import Luau.Addr using (addrToString)
+open import Luau.Var using (varToString)
 
 exprToString′ : String → Expr → String
 statToString′ : String → Stat → String
@@ -10,14 +11,20 @@ blockToString′ : String → Block → String
 
 exprToString′ lb nil =
   "nil"
+exprToString′ lb (addr a) =
+  addrToString(a)
 exprToString′ lb (var x) =
-  x
+  varToString(x)
 exprToString′ lb (M $ N) =
   (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
 exprToString′ lb (function⟨ x ⟩ B end) =
   "function(" ++ x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
+exprToString′ lb (block B end) =
+  "(function()" ++ lb ++
+  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end)()"
 
 statToString′ lb (function f ⟨ x ⟩ B end) =
   "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
@@ -28,8 +35,9 @@ statToString′ lb (local x ← M) =
 statToString′ lb (return M) =
   "return " ++ (exprToString′ lb M)
 
+blockToString′ lb (S ∙ done) = statToString′ lb S
 blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
-blockToString′ lb (S ∙) = statToString′ lb S
+blockToString′ lb (done) = ""
 
 exprToString : Expr → String
 exprToString = exprToString′ "\n"

prototyping/Luau/Type.agda

@@ -0,0 +1,10 @@
+module Luau.Type where
+
+data Type : Set where
+  nil : Type
+  _⇒_ : Type → Type → Type
+  none : Type
+  any : Type
+  _∪_ : Type → Type → Type
+  _∩_ : Type → Type → Type
+

prototyping/Luau/Value.agda

@@ -0,0 +1,16 @@
+module Luau.Value where
+
+open import Luau.Addr using (Addr)
+open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+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/Luau/Var.agda

@@ -0,0 +1,19 @@
+module Luau.Var where
+
+open import Agda.Builtin.Bool using (true; false)
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.String using (String; primStringEquality)
+open import Agda.Builtin.TrustMe using (primTrustMe)
+open import Properties.Dec using (Dec; yes; no; ⊥)
+
+Var : Set
+Var = String
+
+varToString : Var → String
+varToString x = x
+
+_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
+a ≡ⱽ b with primStringEquality a b
+a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥
+a ≡ⱽ b | true = yes primTrustMe
+

prototyping/Properties.agda

@@ -0,0 +1,3 @@
+module Properties where
+
+import Properties.Dec

prototyping/Properties/Dec.agda

@@ -0,0 +1,8 @@
+module Properties.Dec where
+
+data ⊥ : Set where
+
+data Dec(A : Set) : Set where
+  yes : A → Dec A
+  no : (A → ⊥) → Dec A
+