From 0bd21762aef0b0523f8cfcffb0d4784d039e1c76 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Thu, 24 Feb 2022 11:17:46 -0800 Subject: [PATCH] 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 | 8 ++- prototyping/FFI/Data/Bool.agda | 8 --- prototyping/FFI/Data/Vector.agda | 2 +- prototyping/Luau/OpSem.agda | 64 +++++++++++++++---- prototyping/Luau/RuntimeType.agda | 4 +- prototyping/Luau/RuntimeType/ToString.agda | 3 +- prototyping/Luau/Substitution.agda | 4 +- prototyping/Luau/Syntax.agda | 8 +++ prototyping/Luau/Syntax/FromJSON.agda | 15 ++++- prototyping/Luau/Syntax/ToString.agda | 10 ++- prototyping/Luau/Type/FromJSON.agda | 2 +- prototyping/Luau/Value.agda | 6 +- prototyping/Luau/Value/ToString.agda | 5 +- prototyping/Properties/Step.agda | 17 +++-- .../Interpreter/binary_equality_bools/in.lua | 1 + .../Interpreter/binary_equality_bools/out.txt | 1 + .../binary_equality_numbers/in.lua | 1 + .../binary_equality_numbers/out.txt | 1 + prototyping/Utility/Bool.agda | 16 +++++ 19 files changed, 141 insertions(+), 35 deletions(-) delete mode 100644 prototyping/FFI/Data/Bool.agda create mode 100644 prototyping/Tests/Interpreter/binary_equality_bools/in.lua create mode 100644 prototyping/Tests/Interpreter/binary_equality_bools/out.txt create mode 100644 prototyping/Tests/Interpreter/binary_equality_numbers/in.lua create mode 100644 prototyping/Tests/Interpreter/binary_equality_numbers/out.txt create mode 100644 prototyping/Utility/Bool.agda diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 534bb122..ddec8e8b 100644 --- a/prototyping/Examples/Run.agda +++ b/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 diff --git a/prototyping/FFI/Data/Bool.agda b/prototyping/FFI/Data/Bool.agda deleted file mode 100644 index 4b04b033..00000000 --- a/prototyping/FFI/Data/Bool.agda +++ /dev/null @@ -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) #-} diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 2c5d1925..7d2f5012 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/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) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index bfc63a4a..bd75d9d6 100644 --- a/prototyping/Luau/OpSem.agda +++ b/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} → diff --git a/prototyping/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda index 25c0283a..375fc540 100644 --- a/prototyping/Luau/RuntimeType.agda +++ b/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 diff --git a/prototyping/Luau/RuntimeType/ToString.agda b/prototyping/Luau/RuntimeType/ToString.agda index be67ee0c..dfb7c955 100644 --- a/prototyping/Luau/RuntimeType/ToString.agda +++ b/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" diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index 61287d36..d909c350 100644 --- a/prototyping/Luau/Substitution.agda +++ b/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 diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index c1c31e42..57e59a7e 100644 --- a/prototyping/Luau/Syntax.agda +++ b/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 diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index a2c9a42f..330739b9 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/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′) diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 4a3061ba..58a784bf 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ 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; 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 ++ diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda index c585c3f3..49f74626 100644 --- a/prototyping/Luau/Type/FromJSON.agda +++ b/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; _++_) diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda index 1086d39c..ed51abd7 100644 --- a/prototyping/Luau/Value.agda +++ b/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 diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda index 51c3fa78..3421d4cd 100644 --- a/prototyping/Luau/Value/ToString.agda +++ b/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" diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 2a0978ff..69dbac84 100644 --- a/prototyping/Properties/Step.agda +++ b/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) diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/in.lua b/prototyping/Tests/Interpreter/binary_equality_bools/in.lua new file mode 100644 index 00000000..c9c72dc6 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_equality_bools/in.lua @@ -0,0 +1 @@ +return true == false diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/out.txt b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt new file mode 100644 index 00000000..c508d536 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt @@ -0,0 +1 @@ +false diff --git a/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua b/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua new file mode 100644 index 00000000..4efc68a7 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua @@ -0,0 +1 @@ +return 1 == 1 diff --git a/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt @@ -0,0 +1 @@ +true diff --git a/prototyping/Utility/Bool.agda b/prototyping/Utility/Bool.agda new file mode 100644 index 00000000..1afffb0d --- /dev/null +++ b/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