luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

remove % and ^

Browse source
This commit is contained in:
Lily Brown 2022-02-18 16:04:22 -08:00
parent 64ce6c2367
commit 186424b8a8
3 changed files with 6 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
prototyping/Luau/OpSem.agda
View file

@ -5,7 +5,7 @@ open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; prim
open import FFI.Data.Maybe using (just) open import FFI.Data.Maybe using (just)
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end) open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
open import Luau.Substitution using (_[_/_]ᴮ) 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) open import Luau.Value using (addr; val; number)
evalBinOp : Float → BinaryOperator → Float → Float evalBinOp : Float → BinaryOperator → Float → Float
@ -13,8 +13,6 @@ evalBinOp x + y = primFloatPlus x y
evalBinOp x - y = primFloatMinus x y evalBinOp x - y = primFloatMinus x y
evalBinOp x * y = primFloatTimes x y evalBinOp x * y = primFloatTimes x y
evalBinOp x / y = primFloatDiv 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 → Block a → Block a → Heap a → Set
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set

2
prototyping/Luau/Syntax.agda
View file

@ -38,8 +38,6 @@ data BinaryOperator : Set where
- : BinaryOperator - : BinaryOperator
* : BinaryOperator * : BinaryOperator
/ : BinaryOperator / : BinaryOperator
% : BinaryOperator
^ : BinaryOperator
data Block (a : Annotated) : Set data Block (a : Annotated) : Set
data Stat (a : Annotated) : Set data Stat (a : Annotated) : Set

12
prototyping/Luau/Syntax/ToString.agda
View file

@ -1,7 +1,7 @@
module Luau.Syntax.ToString where module Luau.Syntax.ToString where
open import Agda.Builtin.Float using (primShowFloat) 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)
open import FFI.Data.String using (String; _++_) open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString) open import Luau.Addr.ToString using (addrToString)
open import Luau.Type.ToString using (typeToString) open import Luau.Type.ToString using (typeToString)
@ -18,12 +18,10 @@ funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDe
funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")" funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
binOpToString : BinaryOperator → String binOpToString : BinaryOperator → String
binOpToString BinaryOperator.+ = "+" binOpToString + = "+"
binOpToString BinaryOperator.- = "-" binOpToString - = "-"
binOpToString BinaryOperator.* = "*" binOpToString * = "*"
binOpToString BinaryOperator./ = "/" binOpToString / = "/"
binOpToString BinaryOperator.% = "%"
binOpToString BinaryOperator.^ = "^"
exprToString′ : ∀ {a} → String → Expr a → String exprToString′ : ∀ {a} → String → Expr a → String
statToString′ : ∀ {a} → String → Stat a → String statToString′ : ∀ {a} → String → Stat a → String