remove and/or

prototyping/Examples/Run.agda

@@ -4,7 +4,7 @@ module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 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.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,15 +23,3 @@ 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

@@ -8,7 +8,7 @@ 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,8 +23,6 @@ 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
@@ -48,16 +46,6 @@ 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
 
@@ -123,16 +111,6 @@ 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,8 +44,6 @@ 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,8 +61,6 @@ 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,8 +28,6 @@ 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; eval∧; eval∨; binOpAnd; binOpOr)
+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 (_[_/_]ᴮ)
@@ -60,8 +60,6 @@ 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)