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

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-25 15:00:41 -06:00
parent cad61447f2
commit e717262099
2 changed files with 174 additions and 3669 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3833
Makefile
View file

File diff suppressed because it is too large Load diff

10
prototyping/Luau/OpSem.agda
View file

@ -22,6 +22,14 @@ evalEqOp (bool true) (bool y) = y
evalEqOp (bool false) (bool y) = not y evalEqOp (bool false) (bool y) = not y
evalEqOp _ _ = false evalEqOp _ _ = false
evalNeqOp : Value → Value → Bool
evalNeqOp Value.nil Value.nil = false
evalNeqOp (addr x) (addr y) = not (x ==ᴬ y)
evalNeqOp (number x) (number y) = primFloatInequality x y
evalNeqOp (bool true) (bool y) = not y
evalNeqOp (bool false) (bool y) = y
evalNeqOp _ _ = true
data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
+ : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n) + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)
- : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n) - : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n)
@ -32,7 +40,7 @@ data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
<= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n)) <= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n))
>= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n)) >= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
== : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w) == : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (not (evalEqOp v w)) ~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
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