Prototype bools and relational operators (#387)

Prototypes booleans and relational operators.

As part of this I removed `FFI/Data/Bool.agda`, because it was getting in the way - we already use `Agda.Builtin.Bool` instead for other cases.

prototyping/Examples/Run.agda

@@ -3,8 +3,9 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +)
-open import Luau.Value using (nil; number)
+open import Agda.Builtin.Bool using (true; false)
+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)
 
@@ -19,3 +20,6 @@ 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
+
+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

prototyping/FFI/Data/Bool.agda

@@ -1,8 +0,0 @@
-module FFI.Data.Bool where
-
-{-# FOREIGN GHC import qualified Data.Bool #-}
-
-data Bool : Set where
-  false : Bool
-  true : Bool
-{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}

prototyping/FFI/Data/Vector.agda

@@ -3,7 +3,7 @@ module FFI.Data.Vector where
 open import Agda.Builtin.Equality using (_≡_)
 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 Agda.Builtin.Bool using (Bool; false; true)
 open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 

prototyping/Luau/OpSem.agda

@@ -1,18 +1,50 @@
 module Luau.OpSem where
 
 open import Agda.Builtin.Equality using (_≡_)
-open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
+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_; _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.Value using (addr; val; 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)
 
-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
+evalNumOp : Float → BinaryOperator → Float → Value
+evalNumOp x + y = number (primFloatPlus x y)
+evalNumOp x - y = number (primFloatMinus x y)
+evalNumOp x * y = number (primFloatTimes x y)
+evalNumOp x / y = number (primFloatDiv x y)
+evalNumOp x < y = bool (primFloatLess x y)
+evalNumOp x > y = bool (primFloatLess y x)
+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))
+
+evalEqOp : Value → Value → Value
+evalEqOp Value.nil Value.nil = bool true
+evalEqOp (addr x) (addr y) = bool (x == y)
+evalEqOp (number x) (number y) = bool (primFloatEquality x y)
+evalEqOp (bool true) (bool y) = bool y
+evalEqOp (bool false) (bool y) = bool (not y)
+evalEqOp _ _ = bool false
+
+evalNeqOp : Value → Value → Value
+evalNeqOp Value.nil Value.nil = bool false
+evalNeqOp (addr x) (addr y) = bool (not (x == y))
+evalNeqOp (number x) (number y) = bool (primFloatInequality x y)
+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
 
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
@@ -64,10 +96,20 @@ data _⊢_⟶ᴱ_⊣_  where
     ---------------------------------
     H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
   
-  binOpEval :
+  binOpEquality :
+    ∀ {H x y} →
+    ---------------------------------------------------------------------------
+    H ⊢ (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H
+  
+  binOpInequality :
+    ∀ {H x y} →
+    ----------------------------------------------------------------------------
+    H ⊢ (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H
+  
+  binOpNumbers :
     ∀ {H x op y} →
-    --------------------------------------------------------------------------
-    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H
+    -----------------------------------------------------------------------
+    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H
   
   binOp₁ :
     ∀ {H H′ x x′ op y} →

prototyping/Luau/RuntimeType.agda

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

prototyping/Luau/RuntimeType/ToString.agda

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

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; binexp)
+open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; 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)
@@ -11,6 +11,8 @@ var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr
 _[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
 
 nil [ v / x ]ᴱ = nil
+true [ v / x ]ᴱ = true
+false [ v / x ]ᴱ = false
 var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
 addr a [ v / x ]ᴱ = addr a
 (number y) [ v / x ]ᴱ = number y

prototyping/Luau/Syntax.agda

@@ -38,6 +38,12 @@ data BinaryOperator : Set where
   - : BinaryOperator
   * : BinaryOperator
   / : BinaryOperator
+  < : BinaryOperator
+  > : BinaryOperator
+  ≡ : BinaryOperator
+  ≅ : BinaryOperator
+  ≤ : BinaryOperator
+  ≥ : BinaryOperator
 
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set
@@ -54,6 +60,8 @@ data Stat a where
 
 data Expr a where
   nil : Expr a
+  true : Expr a
+  false : Expr a
   var : Var → Expr a
   addr : Addr → Expr a
   _$_ : Expr a → Expr a → Expr a

prototyping/Luau/Syntax/FromJSON.agda

@@ -1,12 +1,12 @@
 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; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
 
 open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
-open import FFI.Data.Bool using (true; false)
 open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; nothing; just)
 open import FFI.Data.Scientific using (toFloat)
@@ -55,6 +55,12 @@ binOpFromString "Add" = Right +
 binOpFromString "Sub" = Right -
 binOpFromString "Mul" = Right *
 binOpFromString "Div" = Right /
+binOpFromString "CompareEq" = Right ≡
+binOpFromString "CompareNe" = Right ≅
+binOpFromString "CompareLt" = Right <
+binOpFromString "CompareLe" = Right ≤
+binOpFromString "CompareGt" = Right >
+binOpFromString "CompareGe" = Right ≥
 binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
 
 varDecFromJSON (object arg) = varDecFromObject arg
@@ -103,6 +109,11 @@ 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 "AstExprConstantBool") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true
+exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false
+exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
+exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool 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′)

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)
+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)
@@ -22,6 +22,12 @@ binOpToString + = "+"
 binOpToString - = "-"
 binOpToString * = "*"
 binOpToString / = "/"
+binOpToString < = "<"
+binOpToString > = ">"
+binOpToString ≡ = "=="
+binOpToString ≅ = "~="
+binOpToString ≤ = "<="
+binOpToString ≥ = ">="
 
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String
@@ -45,6 +51,8 @@ exprToString′ lb (block b is B end) =
   "end)()"
 exprToString′ lb (number x) = primShowFloat x
 exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
+exprToString′ lb true = "true"
+exprToString′ lb false = "false"
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++

prototyping/Luau/Type/FromJSON.agda

@@ -3,9 +3,9 @@ module Luau.Type.FromJSON where
 open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
 
 open import Agda.Builtin.List using (List; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
 
 open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
-open import FFI.Data.Bool using (true; false)
 open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; nothing; just)
 open import FFI.Data.String using (String; _++_)

prototyping/Luau/Value.agda

@@ -1,16 +1,20 @@
 module Luau.Value where
 
+open import Agda.Builtin.Bool using (Bool; true; false)
 open import Agda.Builtin.Float using (Float)
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr; number)
+open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
   number : Float → Value
+  bool : Bool → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
 val (number x) = number x
+val (bool false) = false
+val (bool true) = true

prototyping/Luau/Value/ToString.agda

@@ -2,10 +2,13 @@ module Luau.Value.ToString where
 
 open import Agda.Builtin.String using (String)
 open import Agda.Builtin.Float using (primShowFloat)
-open import Luau.Value using (Value; nil; addr; number)
+open import Agda.Builtin.Bool using (true; false)
+open import Luau.Value using (Value; nil; addr; number; bool)
 open import Luau.Addr.ToString using (addrToString)
 
 valueToString : Value → String
 valueToString nil = "nil"
 valueToString (addr a) = addrToString a
 valueToString (number x) = primShowFloat x
+valueToString (bool false) = "false"
+valueToString (bool true) = "true"

prototyping/Properties/Step.agda

@@ -2,14 +2,15 @@ module Properties.Step where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
+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; 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.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.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 Luau.Value using (nil; addr; val; number; bool)
 open import Properties.Remember using (remember; _,_)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@@ -33,12 +34,15 @@ stepᴱ H nil = value nil refl
 stepᴱ H (var x) = error (UnboundVariable x)
 stepᴱ H (addr a) = value (addr a) refl
 stepᴱ H (number x) = value (number x) refl
+stepᴱ H (true) = value (bool true) refl
+stepᴱ H (false) = value (bool false) 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 (_ $ 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 (app₁ (TypeMismatch function nil λ()))
 stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
+stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ()))
 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)
@@ -53,13 +57,18 @@ 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
+-- 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 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)
 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) | value (bool x′) refl | _ = error (bin₁ (TypeMismatch number (bool x′) λ()))
+stepᴱ H (binexp x op y) | _ | value (bool y′) refl = error (bin₂ (TypeMismatch number (bool y′) λ()))
 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)
 

prototyping/Tests/Interpreter/binary_equality_bools/in.lua

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

prototyping/Tests/Interpreter/binary_equality_bools/out.txt

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

prototyping/Tests/Interpreter/binary_equality_numbers/in.lua

@@ -0,0 +1 @@
+return 1 == 1

prototyping/Tests/Interpreter/binary_equality_numbers/out.txt

@@ -0,0 +1 @@
+true

prototyping/Utility/Bool.agda

@@ -0,0 +1,16 @@
+module Utility.Bool where
+
+open import Agda.Builtin.Bool using (Bool; true; false)
+
+not : Bool → Bool
+not false = true
+not true = false
+
+_or_ : Bool → Bool → Bool
+true or _ = true
+_ or true = true
+_ or _ = false
+
+_and_ : Bool → Bool → Bool
+true and true = true
+_ and _ = false