diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index ddec8e8b..05d237bd 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -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 diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 9a9df6ad..acb066ce 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -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