diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 9e851347..ddec8e8b 100644 --- a/prototyping/Examples/Run.agda +++ b/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 diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index eff0305e..bd75d9d6 100644 --- a/prototyping/Luau/OpSem.agda +++ b/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′ → diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 5f9ac3be..57e59a7e 100644 --- a/prototyping/Luau/Syntax.agda +++ b/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 diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 24dd7228..330739b9 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/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 diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index bd7a6c04..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; 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 diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index cae42080..69dbac84 100644 --- a/prototyping/Properties/Step.agda +++ b/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.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.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 (_[_/_]ᴮ) @@ -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)