and/or operators

prototyping/Examples/Run.agda

@@ -3,8 +3,8 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Agda.Builtin.Bool using (true)
+open import Agda.Builtin.Bool using (true; false)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; ∧; ∨; true; false)
 open import Luau.Value using (nil; number; bool)
 open import Luau.Run using (run; return)
 open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
@@ -23,3 +23,15 @@ ex3 = refl
 
 ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) < (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool true) _)
 ex4 = refl
+
+ex5 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) ∧ (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 2.0) _)
+ex5 = refl
+
+ex6 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp nil ∨ (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 2.0) _)
+ex6 = refl
+
+ex7 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp nil ∧ (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return nil _)
+ex7 = refl
+
+ex8 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp true ∧ false) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool false) _)
+ex8 = refl

prototyping/Luau/OpSem.agda

@@ -3,12 +3,12 @@ module Luau.OpSem where
 open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
 open import Agda.Builtin.Bool using (Bool; true; false)
-open import Utility.Bool using (not; _or_)
+open import Utility.Bool using (not; _or_; _and_)
 open import Agda.Builtin.Nat using (_==_)
 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; binexp; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; number)
+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; Value; bool)
 open import Luau.RuntimeType using (RuntimeType; valueType)
 
@@ -23,6 +23,8 @@ evalNumOp x ≡ y = bool (primFloatEquality x y)
 evalNumOp x ≅ y = bool (primFloatInequality x y)
 evalNumOp x ≤ y = bool ((primFloatLess x y) or (primFloatEquality x y))
 evalNumOp x ≥ y = bool ((primFloatLess y x) or (primFloatEquality x y))
+evalNumOp x ∧ y = number x
+evalNumOp x ∨ y = number x
 
 evalEqOp : Value → Value → Value
 evalEqOp Value.nil Value.nil = bool true
@@ -40,6 +42,22 @@ evalNeqOp (bool true) (bool y) = bool (not y)
 evalNeqOp (bool false) (bool y) = bool y
 evalNeqOp _ _ = bool true
 
+coerceToBool : Value → Bool
+coerceToBool Value.nil = false
+coerceToBool (addr x) = true
+coerceToBool (number x) = true
+coerceToBool (bool x) = x
+
+eval∨ : Value → Value → Value
+eval∨ x y with coerceToBool x
+eval∨ x y | false = y
+eval∨ x y | true = x
+
+eval∧ : Value → Value → Value
+eval∧ x y with coerceToBool x
+eval∧ x y | true = y
+eval∧ x y | false = x
+
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
 
@@ -105,6 +123,16 @@ data _⊢_⟶ᴱ_⊣_  where
     -----------------------------------------------------------------------
     H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H
   
+  binOpOr :
+    ∀ {H x y} →
+    ---------------------------------------------------------------------------
+    H ⊢ (binexp (val x) ∨ (val y)) ⟶ᴱ (val (eval∨ x y)) ⊣ H
+  
+  binOpAnd :
+    ∀ {H x y} →
+    ----------------------------------------------------------------------------
+    H ⊢ (binexp (val x) ∧ (val y)) ⟶ᴱ (val (eval∧ x y)) ⊣ H
+  
   binOp₁ :
     ∀ {H H′ x x′ op y} →
     H ⊢ x ⟶ᴱ x′ ⊣ H′ →

prototyping/Luau/Syntax.agda

@@ -44,6 +44,8 @@ data BinaryOperator : Set where
   ≅ : BinaryOperator
   ≤ : BinaryOperator
   ≥ : BinaryOperator
+  ∧ : BinaryOperator
+  ∨ : BinaryOperator
 
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set

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; binexp; BinaryOperator; +; -; *; /; ≡; ≅; <; >; ≤; ≥)
+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; _∷_; [])
@@ -61,6 +61,8 @@ binOpFromString "CompareLt" = Right <
 binOpFromString "CompareLe" = Right ≤
 binOpFromString "CompareGt" = Right >
 binOpFromString "CompareGe" = Right ≥
+binOpFromString "And" = Right ∧
+binOpFromString "Or" = Right ∨
 binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
 
 varDecFromJSON (object arg) = varDecFromObject arg

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; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; binexp; true; false)
+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; true; false)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -28,6 +28,8 @@ binOpToString ≡ = "=="
 binOpToString ≅ = "~="
 binOpToString ≤ = "<="
 binOpToString ≥ = ">="
+binOpToString ∧ = "and"
+binOpToString ∨ = "or"
 
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String

prototyping/Properties/Step.agda

@@ -5,8 +5,8 @@ open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTi
 open import Agda.Builtin.Bool using (true; false)
 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; true; false; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; ≅)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; true; false; 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; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality)
+open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality; eval∧; eval∨; binOpAnd; binOpOr)
 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 (_[_/_]ᴮ)
@@ -60,6 +60,8 @@ stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y
 -- Have to use explicit form for ≡ here because it's a heavily overloaded symbol
 stepᴱ H (binexp x Luau.Syntax.≡ y) | value x′ refl | value y′ refl = step H (val (evalEqOp x′ y′)) binOpEquality
 stepᴱ H (binexp x ≅ y) | value x′ refl | value y′ refl = step H (val (evalNeqOp x′ y′)) binOpInequality
+stepᴱ H (binexp x ∧ y) | value x′ refl | value y′ refl = step H (val (eval∧ x′ y′)) binOpAnd
+stepᴱ H (binexp x ∨ y) | value x′ refl | value y′ refl = step H (val (eval∨ x′ y′)) binOpOr
 stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (val (evalNumOp x′ op y′)) binOpNumbers
 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)

prototyping/Tests/Interpreter/binary_and_bools/in.lua

@@ -0,0 +1 @@
+return true and false

prototyping/Tests/Interpreter/binary_and_bools/out.txt

@@ -0,0 +1 @@
+false

prototyping/Utility/Bool.agda

@@ -10,3 +10,7 @@ _or_ : Bool → Bool → Bool
 true or _ = true
 _ or true = true
 _ or _ = false
+
+_and_ : Bool → Bool → Bool
+true and true = true
+_ and _ = false