From cd18adc20ecb805b8eeb770a9e5ef8e0cd123734 Mon Sep 17 00:00:00 2001 From: Lily Brown Date: Tue, 22 Feb 2022 15:52:56 -0800 Subject: [PATCH] Prototyping: binary operations (#377) Adds support for binary operations on numbers. --- prototyping/Examples/Run.agda | 5 ++- prototyping/Luau/OpSem.agda | 31 ++++++++++++++++--- prototyping/Luau/RuntimeError.agda | 9 ++++-- prototyping/Luau/RuntimeError/ToString.agda | 9 ++++-- prototyping/Luau/RuntimeType.agda | 13 ++++++++ prototyping/Luau/RuntimeType/ToString.agda | 9 ++++++ prototyping/Luau/Substitution.agda | 3 +- prototyping/Luau/Syntax.agda | 7 +++++ prototyping/Luau/Syntax/FromJSON.agda | 26 +++++++++++++++- prototyping/Luau/Syntax/ToString.agda | 9 +++++- prototyping/Properties/Step.agda | 23 +++++++++++--- .../Tests/Interpreter/binary_exps/in.lua | 1 + .../Tests/Interpreter/binary_exps/out.txt | 1 + 13 files changed, 127 insertions(+), 19 deletions(-) create mode 100644 prototyping/Luau/RuntimeType.agda create mode 100644 prototyping/Luau/RuntimeType/ToString.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/Examples/Run.agda b/prototyping/Examples/Run.agda index 3cac564d..534bb122 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -3,7 +3,7 @@ module Examples.Run where open import Agda.Builtin.Equality using (_≡_; refl) -open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number) +open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +) open import Luau.Value using (nil; number) open import Luau.Run using (run; return) open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp) @@ -16,3 +16,6 @@ ex1 = refl ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _) 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 diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 89564769..bfc63a4a 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -1,11 +1,18 @@ 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 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set @@ -57,6 +64,24 @@ data _⊢_⟶ᴱ_⊣_ where --------------------------------- H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H + binOpEval : + ∀ {H x op y} → + -------------------------------------------------------------------------- + H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H + + binOp₁ : + ∀ {H H′ x x′ op y} → + H ⊢ x ⟶ᴱ x′ ⊣ H′ → + --------------------------------------------- + H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′ + + binOp₂ : + ∀ {H H′ x op y y′} → + H ⊢ y ⟶ᴱ y′ ⊣ H′ → + --------------------------------------------- + H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′ + + data _⊢_⟶ᴮ_⊣_ where local : ∀ {H H′ x M M′ B} → @@ -94,5 +119,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 a54d48fe..b479a72a 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -4,20 +4,23 @@ open import Agda.Builtin.Equality using (_≡_) 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.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp) +open import Luau.RuntimeType using (RuntimeType; valueType) open import Luau.Value using (val) +open import Properties.Equality using (_≢_) data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - NilIsNotAFunction : ∀ {V} → RuntimeErrorᴱ H (nil $ val V) - NumberIsNotAFunction : ∀ n {V} → RuntimeErrorᴱ H (number n $ val V) + TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v) 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) app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N) block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end) + bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N) + bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N) data RuntimeErrorᴮ H where local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index 10c0fe08..d5528c8b 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -2,22 +2,25 @@ 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₁; app₂; block) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂) +open import Luau.RuntimeType.ToString using (runtimeTypeToString) open import Luau.Addr.ToString using (addrToString) open import Luau.Syntax.ToString using (exprToString) open import Luau.Var.ToString using (varToString) +open import Luau.Value.ToString using (valueToString) open import Luau.Syntax using (name; _$_) errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String -errToStringᴱ NilIsNotAFunction = "nil is not a function" -errToStringᴱ (NumberIsNotAFunction n) = "number " ++ primShowFloat n ++ " is not a function" errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound" errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated" errToStringᴱ (app₁ E) = errToStringᴱ E errToStringᴱ (app₂ E) = errToStringᴱ E +errToStringᴱ (bin₁ E) = errToStringᴱ E +errToStringᴱ (bin₂ E) = errToStringᴱ E errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b +errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t 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/RuntimeType/ToString.agda b/prototyping/Luau/RuntimeType/ToString.agda new file mode 100644 index 00000000..be67ee0c --- /dev/null +++ b/prototyping/Luau/RuntimeType/ToString.agda @@ -0,0 +1,9 @@ +module Luau.RuntimeType.ToString where + +open import FFI.Data.String using (String) +open import Luau.RuntimeType using (RuntimeType; function; number; nil) + +runtimeTypeToString : RuntimeType → String +runtimeTypeToString function = "function" +runtimeTypeToString number = "number" +runtimeTypeToString nil = "nil" 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..c1c31e42 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -33,6 +33,12 @@ arg : ∀ {a} → FunDec a → VarDec a arg (f ⟨ x ⟩∈ T) = x arg (f ⟨ x ⟩) = x +data BinaryOperator : Set where + + : BinaryOperator + - : BinaryOperator + * : BinaryOperator + / : BinaryOperator + data Block (a : Annotated) : Set data Stat (a : Annotated) : Set data Expr (a : Annotated) : Set @@ -54,3 +60,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/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 8191e9e7..a2c9a42f 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) +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; _∷_; []) @@ -23,6 +23,9 @@ type = fromString "type" value = fromString "value" values = fromString "values" vars = fromString "vars" +op = fromString "op" +left = fromString "left" +right = fromString "right" data Lookup : Set where _,_ : String → Value → Lookup @@ -34,6 +37,8 @@ lookupIn (key ∷ keys) obj with lookup (fromString key) obj lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj lookupIn (key ∷ keys) obj | just value = (key , value) +binOpFromJSON : Value → Either String BinaryOperator +binOpFromString : String → Either String BinaryOperator varDecFromJSON : Value → Either String (VarDec maybe) varDecFromObject : Object → Either String (VarDec maybe) exprFromJSON : Value → Either String (Expr maybe) @@ -43,6 +48,15 @@ statFromObject : Object → Either String (Stat maybe) blockFromJSON : Value → Either String (Block maybe) blockFromArray : Array → Either String (Block maybe) +binOpFromJSON (string s) = binOpFromString s +binOpFromJSON val = Left "Binary operator not a string" + +binOpFromString "Add" = Right + +binOpFromString "Sub" = Right - +binOpFromString "Mul" = Right * +binOpFromString "Div" = Right / +binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator") + varDecFromJSON (object arg) = varDecFromObject arg varDecFromJSON val = Left "VarDec not an object" @@ -89,6 +103,15 @@ 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 "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′) +exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err +exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err +exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err +exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary" +exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary" +exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary" exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty) exprFromObject obj | just _ = Left "AstExpr type not a string" exprFromObject obj | nothing = Left "AstExpr missing type" @@ -146,3 +169,4 @@ blockFromArray arr | just value | Left err = Left err blockFromArray arr | just value | Right S with blockFromArray(tail arr) blockFromArray arr | just value | Right S | Left err = Left (err) blockFromArray arr | just value | Right S | Right B = Right (S ∙ B) + \ No newline at end of file diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index a20b360b..4a3061ba 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,12 @@ 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 + = "+" +binOpToString - = "-" +binOpToString * = "*" +binOpToString / = "/" + exprToString′ : ∀ {a} → String → Expr a → String statToString′ : ∀ {a} → String → Stat a → String blockToString′ : ∀ {a} → String → Block a → String @@ -38,6 +44,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 914c3468..2a0978ff 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -1,11 +1,13 @@ 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₁ ; app₂ ; beta; function; block; return; done; local; subst) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; NumberIsNotAFunction; UnboundVariable; SEGV; app₁; app₂; block; local; return) +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.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 Properties.Remember using (remember; _,_) @@ -35,8 +37,8 @@ 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 NilIsNotAFunction -stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (NumberIsNotAFunction n) +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 (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) @@ -49,6 +51,17 @@ 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 (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 +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) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s) +stepᴱ H (binexp x op y) | error E = error (bin₁ E) 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) diff --git a/prototyping/Tests/Interpreter/binary_exps/in.lua b/prototyping/Tests/Interpreter/binary_exps/in.lua new file mode 100644 index 00000000..0750f9e6 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_exps/in.lua @@ -0,0 +1 @@ +return 1 + 2 - 2 * 2 / 2 diff --git a/prototyping/Tests/Interpreter/binary_exps/out.txt b/prototyping/Tests/Interpreter/binary_exps/out.txt new file mode 100644 index 00000000..d3827e75 --- /dev/null +++ b/prototyping/Tests/Interpreter/binary_exps/out.txt @@ -0,0 +1 @@ +1.0