From b1b1d408c9816e7d974201489826023455e5599e Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Fri, 18 Feb 2022 14:41:13 -0800 Subject: [PATCH] checkpoint --- prototyping/Luau/OpSem.agda | 21 +++++++++++++++---- prototyping/Luau/RuntimeError.agda | 4 ++-- prototyping/Luau/RuntimeError/ToString.agda | 3 ++- prototyping/Luau/RuntimeType.agda | 13 ++++++++++++ prototyping/Luau/Substitution.agda | 3 ++- prototyping/Luau/Syntax.agda | 9 ++++++++ prototyping/Luau/Syntax/ToString.agda | 11 +++++++++- prototyping/Properties/Step.agda | 8 +++++-- .../Tests/Interpreter/binary_exps/in.lua | 1 + .../Tests/Interpreter/binary_exps/out.txt | 1 + 10 files changed, 63 insertions(+), 11 deletions(-) create mode 100644 prototyping/Luau/RuntimeType.agda create mode 100644 prototyping/Tests/Interpreter/binary_exps/in.lua create mode 100644 prototyping/Tests/Interpreter/binary_exps/out.txt diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 878b8bd0..9290b722 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -1,11 +1,20 @@ module Luau.OpSem where open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv) 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) -open import Luau.Value using (addr; val) +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) + +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 +evalBinOp x % y = x -- TODO: Actually implement this +evalBinOp x ^ y = x -- TODO: Actually implement this data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set @@ -51,6 +60,12 @@ data _⊢_⟶ᴱ_⊣_ where --------------------------------- H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H + binOp : + ∀ {H x op y} → + -------------------------------------------------------------------------- + H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H + + data _⊢_⟶ᴮ_⊣_ where local : ∀ {H H′ x M M′ B} → @@ -88,5 +103,3 @@ data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set wher H′ ⊢ B′ ⟶* B″ ⊣ H″ → ------------------ H ⊢ B ⟶* B″ ⊣ H″ - - diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index f9e684b3..5e0d4684 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -5,13 +5,13 @@ open import Luau.Heap using (Heap; _[_]) open import FFI.Data.Maybe using (just; nothing) open import FFI.Data.String using (String) open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number) +open import Luau.RuntimeType using (RuntimeType; valueType) data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M) - NumberIsNotAFunction : ∀ n {M} → RuntimeErrorᴱ H ((number n) $ M) + TypeMismatch : ∀ {t} → RuntimeErrorᴱ H (number n) UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x) SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a) app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index ac760fab..a8b7d4ac 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -2,7 +2,7 @@ module Luau.RuntimeError.ToString where open import Agda.Builtin.Float using (primShowFloat) open import FFI.Data.String using (String; _++_) -open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; ValueIsNotANumber) open import Luau.Addr.ToString using (addrToString) open import Luau.Syntax.ToString using (exprToString) open import Luau.Var.ToString using (varToString) @@ -17,6 +17,7 @@ errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unboun errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated" errToStringᴱ (app E) = errToStringᴱ E errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b +errToStringᴱ (ValueIsNotANumber v) = exprToString v ++ " is not a number" errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x) errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement" diff --git a/prototyping/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda new file mode 100644 index 00000000..25c0283a --- /dev/null +++ b/prototyping/Luau/RuntimeType.agda @@ -0,0 +1,13 @@ +module Luau.RuntimeType where + +open import Luau.Value using (Value; nil; addr; number) + +data RuntimeType : Set where + function : RuntimeType + number : RuntimeType + nil : RuntimeType + +valueType : Value → RuntimeType +valueType nil = nil +valueType (addr x) = function +valueType (number x) = number diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index e364a000..61287d36 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) +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.Value using (Value; val) open import Luau.Var using (Var; _≡ⱽ_) open import Properties.Dec using (Dec; yes; no) @@ -17,6 +17,7 @@ addr a [ v / x ]ᴱ = addr a (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ) function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end +(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ) (function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F)) (local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y)) diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 1313456b..abd7e13e 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -33,6 +33,14 @@ arg : ∀ {a} → FunDec a → VarDec a arg (f ⟨ x ⟩∈ T) = x arg (f ⟨ x ⟩) = x +data BinaryOperator : Set where + + : BinaryOperator + - : BinaryOperator + * : BinaryOperator + / : BinaryOperator + % : BinaryOperator + ^ : BinaryOperator + data Block (a : Annotated) : Set data Stat (a : Annotated) : Set data Expr (a : Annotated) : Set @@ -54,3 +62,4 @@ data Expr a where function_is_end : FunDec a → Block a → Expr a block_is_end : Var → Block a → Expr a number : Float → Expr a + binexp : Expr a → BinaryOperator → Expr a → Expr a diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index a20b360b..1ebc9720 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) +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 FFI.Data.String using (String; _++_) open import Luau.Addr.ToString using (addrToString) open import Luau.Type.ToString using (typeToString) @@ -17,6 +17,14 @@ funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")" funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")" +binOpToString : BinaryOperator → String +binOpToString BinaryOperator.+ = "+" +binOpToString BinaryOperator.- = "-" +binOpToString BinaryOperator.* = "*" +binOpToString BinaryOperator./ = "/" +binOpToString BinaryOperator.% = "%" +binOpToString BinaryOperator.^ = "^" + exprToString′ : ∀ {a} → String → Expr a → String statToString′ : ∀ {a} → String → Stat a → String blockToString′ : ∀ {a} → String → Block a → String @@ -38,6 +46,7 @@ exprToString′ lb (block b is B end) = " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end)()" exprToString′ lb (number x) = primShowFloat x +exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y statToString′ lb (function F is B end) = "local " ++ funDecToString F ++ lb ++ diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 620dc618..bb851202 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -1,10 +1,11 @@ module Properties.Step where open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv) 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) -open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst) +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 ; beta; function; block; return; done; local; subst; binOp; evalBinOp) open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) open import Luau.Substitution using (_[_/_]ᴮ) open import Luau.Value using (nil; addr; val; number) @@ -46,6 +47,8 @@ stepᴱ H (block b is done end) | done refl = step H nil done stepᴱ H (block b is B end) | error E = error (block b E) 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 y +stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOp stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end) stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p) @@ -58,3 +61,4 @@ stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (r stepᴮ H (return _ ∙ B) | value V refl = return V refl stepᴮ H (return M ∙ B) | error E = error (return E) stepᴮ H done = done refl + \ No newline at end of file diff --git a/prototyping/Tests/Interpreter/binary_exps/in.lua b/prototyping/Tests/Interpreter/binary_exps/in.lua new file mode 100644 index 00000000..5e0cae51 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_exps/in.lua @@ -0,0 +1 @@ +return 1 + 2 - 3 diff --git a/prototyping/Tests/Interpreter/binary_exps/out.txt b/prototyping/Tests/Interpreter/binary_exps/out.txt new file mode 100644 index 00000000..18e16e38 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_exps/out.txt @@ -0,0 +1 @@ +-1.0