Prototyping: binary operations (#377)

Adds support for binary operations on numbers.

prototyping/Examples/Run.agda

@@ -3,7 +3,7 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +)
 open import Luau.Value using (nil; number)
 open import Luau.Run using (run; return)
 open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
@@ -16,3 +16,6 @@ ex1 = refl
 
 ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
 ex2 = refl
+
+ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _)
+ex3 = refl

prototyping/Luau/OpSem.agda

@@ -1,11 +1,18 @@
 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
 
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
@@ -57,6 +64,24 @@ data _⊢_⟶ᴱ_⊣_  where
     ---------------------------------
     H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
   
+  binOpEval :
+    ∀ {H x op y} →
+    --------------------------------------------------------------------------
+    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H
+  
+  binOp₁ :
+    ∀ {H H′ x x′ op y} →
+    H ⊢ x ⟶ᴱ x′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′
+  
+  binOp₂ :
+    ∀ {H H′ x op y y′} →
+    H ⊢ y ⟶ᴱ y′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′
+
+  
 data _⊢_⟶ᴮ_⊣_  where
 
   local : ∀ {H H′ x M M′ B} →
@@ -94,5 +119,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

@@ -4,20 +4,23 @@ open import Agda.Builtin.Equality using (_≡_)
 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.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp)
+open import Luau.RuntimeType using (RuntimeType; valueType)
 open import Luau.Value using (val)
+open import Properties.Equality using (_≢_)
 
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  NilIsNotAFunction : ∀ {V} → RuntimeErrorᴱ H (nil $ val V)
-  NumberIsNotAFunction : ∀ n {V} → RuntimeErrorᴱ H (number n $ val V)
+  TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v)
   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)
   app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
   block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
+  bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
+  bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)
 
 data RuntimeErrorᴮ H where
   local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)

prototyping/Luau/RuntimeError/ToString.agda

@@ -2,22 +2,25 @@ 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₁; app₂; block)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
+open import Luau.RuntimeType.ToString using (runtimeTypeToString)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
+open import Luau.Value.ToString using (valueToString)
 open import Luau.Syntax using (name; _$_)
 
 errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
 errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
 
-errToStringᴱ NilIsNotAFunction = "nil is not a function"
-errToStringᴱ (NumberIsNotAFunction n) = "number " ++ primShowFloat n ++ " is not a function"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
 errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app₁ E) = errToStringᴱ E
 errToStringᴱ (app₂ E) = errToStringᴱ E
+errToStringᴱ (bin₁ E) = errToStringᴱ E
+errToStringᴱ (bin₂ E) = errToStringᴱ E
 errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
+errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t
 
 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/RuntimeType/ToString.agda

@@ -0,0 +1,9 @@
+module Luau.RuntimeType.ToString where
+
+open import FFI.Data.String using (String)
+open import Luau.RuntimeType using (RuntimeType; function; number; nil)
+
+runtimeTypeToString : RuntimeType → String
+runtimeTypeToString function = "function"
+runtimeTypeToString number = "number"
+runtimeTypeToString nil = "nil"

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,12 @@ arg : ∀ {a} → FunDec a → VarDec a
 arg (f ⟨ x ⟩∈ T) = x
 arg (f ⟨ x ⟩) = x
 
+data BinaryOperator : Set where
+  + : BinaryOperator
+  - : BinaryOperator
+  * : BinaryOperator
+  / : BinaryOperator
+
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set
 data Expr (a : Annotated) : Set
@@ -54,3 +60,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/FromJSON.agda

@@ -1,6 +1,6 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
@@ -23,6 +23,9 @@ type = fromString "type"
 value = fromString "value"
 values = fromString "values"
 vars = fromString "vars"
+op = fromString "op"
+left = fromString "left"
+right = fromString "right"
 
 data Lookup : Set where
   _,_ : String → Value → Lookup
@@ -34,6 +37,8 @@ lookupIn (key ∷ keys) obj with lookup (fromString key) obj
 lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
 lookupIn (key ∷ keys) obj | just value = (key , value)
 
+binOpFromJSON : Value → Either String BinaryOperator
+binOpFromString : String → Either String BinaryOperator
 varDecFromJSON : Value → Either String (VarDec maybe)
 varDecFromObject : Object → Either String (VarDec maybe)
 exprFromJSON : Value → Either String (Expr maybe)
@@ -43,6 +48,15 @@ statFromObject : Object → Either String (Stat maybe)
 blockFromJSON : Value → Either String (Block maybe)
 blockFromArray : Array → Either String (Block maybe)
 
+binOpFromJSON (string s) = binOpFromString s
+binOpFromJSON val = Left "Binary operator not a string"
+
+binOpFromString "Add" = Right +
+binOpFromString "Sub" = Right -
+binOpFromString "Mul" = Right *
+binOpFromString "Div" = Right /
+binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
+
 varDecFromJSON (object arg) = varDecFromObject arg
 varDecFromJSON val = Left "VarDec not an object"
 
@@ -89,6 +103,15 @@ exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
 exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
 exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
 exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
+exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o′ | Right l′ | Right r′ = Right (binexp l′ o′ r′)
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary"
 exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
 exprFromObject obj | nothing = Left "AstExpr missing type"
@@ -146,3 +169,4 @@ blockFromArray arr | just value | Left err = Left err
 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,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,12 @@ 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 + = "+"
+binOpToString - = "-"
+binOpToString * = "*"
+binOpToString / = "/"
+
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String
 blockToString′ : ∀ {a} → String → Block a → String
@@ -38,6 +44,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,11 +1,13 @@
 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₁ ; app₂ ; beta; function; block; return; done; local; subst)
-open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block; local; return)
+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₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpEval; evalBinOp; binOp₁; binOp₂)
+open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
+open import Luau.RuntimeType using (function; number)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val; number)
 open import Properties.Remember using (remember; _,_)
@@ -35,8 +37,8 @@ stepᴱ H (M $ N) with stepᴱ H M
 stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
 stepᴱ H (_ $ N) | value V refl with stepᴱ H N
 stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s)
-stepᴱ H (_ $ _) | value nil refl | value W refl = error NilIsNotAFunction
-stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (NumberIsNotAFunction n)
+stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
+stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (nothing , p) = error (app₁ (SEGV a p))
 stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
@@ -49,6 +51,17 @@ 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 (binexp x op y) | value x′ refl with stepᴱ H y
+stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOpEval
+stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s)
+stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E)
+stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ()))
+stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
+stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
+stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
+stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s)
+stepᴱ H (binexp x op y) | error E = error (bin₁ E)
 
 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)

prototyping/Tests/Interpreter/binary_exps/in.lua

@@ -0,0 +1 @@
+return 1 + 2 - 2 * 2 / 2

prototyping/Tests/Interpreter/binary_exps/out.txt

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