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

implement == and ~= for strings

Browse source
This commit is contained in:
Lily Brown 2022-02-24 13:59:17 -08:00
parent f597d81965
commit 7840390dfa
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
prototyping/Examples/Run.agda
View file

@ -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; ≅; string)
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,3 +23,6 @@ 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 (string "foo") ≅ (string "bar")) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool true) _)
ex5 = refl

3
prototyping/Luau/OpSem.agda
View file

@ -3,6 +3,7 @@ module Luau.OpSem where
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.String using (primStringEquality)
open import Utility.Bool using (not; _or_; _and_)
open import Agda.Builtin.Nat using (_==_)
open import FFI.Data.Maybe using (just)
@ -30,6 +31,7 @@ evalEqOp (addr x) (addr y) = bool (x == y)
evalEqOp (number x) (number y) = bool (primFloatEquality x y)
evalEqOp (bool true) (bool y) = bool y
evalEqOp (bool false) (bool y) = bool (not y)
evalEqOp (string x) (string y) = bool (primStringEquality x y)
evalEqOp _ _ = bool false
evalNeqOp : Value → Value → Value
@ -38,6 +40,7 @@ evalNeqOp (addr x) (addr y) = bool (not (x == y))
evalNeqOp (number x) (number y) = bool (primFloatInequality x y)
evalNeqOp (bool true) (bool y) = bool (not y)
evalNeqOp (bool false) (bool y) = bool y
evalNeqOp (string x) (string y) = bool (not (primStringEquality x y))
evalNeqOp _ _ = bool true
coerceToBool : Value → Bool