checkpoint

prototyping/Luau/OpSem.agda

@@ -1,11 +1,20 @@
 module Luau.OpSem where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
 open import FFI.Data.Maybe using (just)
 open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg)
-open import Luau.Value using (addr; val)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; %; ^; number)
+open import Luau.Value using (addr; val; number)
+
+evalBinOp : Float → BinaryOperator → Float → Float
+evalBinOp x + y = primFloatPlus x y
+evalBinOp x - y = primFloatMinus x y
+evalBinOp x * y = primFloatTimes x y
+evalBinOp x / y = primFloatDiv x y
+evalBinOp x % y = x -- TODO: Actually implement this
+evalBinOp x ^ y = x -- TODO: Actually implement this
 
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
@@ -51,6 +60,12 @@ data _⊢_⟶ᴱ_⊣_  where
     ---------------------------------
     H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
   
+  binOp :
+    ∀ {H x op y} →
+    --------------------------------------------------------------------------
+    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H
+
+  
 data _⊢_⟶ᴮ_⊣_  where
 
   local : ∀ {H H′ x M M′ B} →
@@ -88,5 +103,3 @@ data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set wher
     H′ ⊢ B′ ⟶* B″ ⊣ H″ →
     ------------------
     H ⊢ B ⟶* B″ ⊣ H″
-
-

prototyping/Luau/RuntimeError.agda

@@ -5,13 +5,13 @@ open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
 open import FFI.Data.String using (String)
 open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number)
+open import Luau.RuntimeType using (RuntimeType; valueType)
 
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
-  NumberIsNotAFunction : ∀ n {M} → RuntimeErrorᴱ H ((number n) $ M)
+  TypeMismatch : ∀ {t} → RuntimeErrorᴱ H (number n)
   UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
   SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
   app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)

prototyping/Luau/RuntimeError/ToString.agda

@@ -2,7 +2,7 @@ module Luau.RuntimeError.ToString where
 
 open import Agda.Builtin.Float using (primShowFloat)
 open import FFI.Data.String using (String; _++_)
-open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; ValueIsNotANumber)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
@@ -17,6 +17,7 @@ errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unboun
 errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app E) = errToStringᴱ E
 errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
+errToStringᴱ (ValueIsNotANumber v) = exprToString v ++ " is not a number"
 
 errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"

prototyping/Luau/RuntimeType.agda

@@ -0,0 +1,13 @@
+module Luau.RuntimeType where
+
+open import Luau.Value using (Value; nil; addr; number)
+
+data RuntimeType : Set where
+  function : RuntimeType
+  number : RuntimeType
+  nil : RuntimeType
+
+valueType : Value → RuntimeType
+valueType nil = nil
+valueType (addr x) = function
+valueType (number x) = number

prototyping/Luau/Substitution.agda

@@ -1,6 +1,6 @@
 module Luau.Substitution where
 
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -17,6 +17,7 @@ addr a [ v / x ]ᴱ = addr a
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
 function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
 block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
+(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)
 
 (function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
 (local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))

prototyping/Luau/Syntax.agda

@@ -33,6 +33,14 @@ arg : ∀ {a} → FunDec a → VarDec a
 arg (f ⟨ x ⟩∈ T) = x
 arg (f ⟨ x ⟩) = x
 
+data BinaryOperator : Set where
+  + : BinaryOperator
+  - : BinaryOperator
+  * : BinaryOperator
+  / : BinaryOperator
+  % : BinaryOperator
+  ^ : BinaryOperator
+
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set
 data Expr (a : Annotated) : Set
@@ -54,3 +62,4 @@ data Expr a where
   function_is_end : FunDec a → Block a → Expr a
   block_is_end : Var → Block a → Expr a
   number : Float → Expr a
+  binexp : Expr a → BinaryOperator → Expr a → Expr a

prototyping/Luau/Syntax/ToString.agda

@@ -1,7 +1,7 @@
 module Luau.Syntax.ToString where
 
 open import Agda.Builtin.Float using (primShowFloat)
-open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; binexp)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -17,6 +17,14 @@ funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
 funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
 funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
 
+binOpToString : BinaryOperator → String
+binOpToString BinaryOperator.+ = "+"
+binOpToString BinaryOperator.- = "-"
+binOpToString BinaryOperator.* = "*"
+binOpToString BinaryOperator./ = "/"
+binOpToString BinaryOperator.% = "%"
+binOpToString BinaryOperator.^ = "^"
+
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String
 blockToString′ : ∀ {a} → String → Block a → String
@@ -38,6 +46,7 @@ exprToString′ lb (block b is B end) =
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
 exprToString′ lb (number x) = primShowFloat x
+exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++

prototyping/Properties/Step.agda

@@ -1,10 +1,11 @@
 module Properties.Step where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number)
-open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +)
+open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst; binOp; evalBinOp)
 open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val; number)
@@ -46,6 +47,8 @@ stepᴱ H (block b is done end) | done refl = step H nil done
 stepᴱ H (block b is B end) | error E = error (block b E)
 stepᴱ H (function F is C end) with alloc H (function F is C end)
 stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
+stepᴱ H (binexp x op y) with stepᴱ H x | stepᴱ H y
+stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOp
 
 stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
 stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
@@ -58,3 +61,4 @@ stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (r
 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
+ 

prototyping/Tests/Interpreter/binary_exps/in.lua

@@ -0,0 +1 @@
+return 1 + 2 - 3

prototyping/Tests/Interpreter/binary_exps/out.txt

@@ -0,0 +1 @@
+-1.0