Merge branch 'master' into merge
This commit is contained in:
Arseny Kapoulkine
commit
2a549cfbad
|
|
@ -34,6 +34,11 @@ jobs:
|
|||
with:
|
||||
path: ~/.cabal/store
|
||||
key: prototyping-${{ runner.os }}-${{ matrix.agda }}
|
||||
- uses: actions/cache@v2
|
||||
id: luau-ast-cache
|
||||
with:
|
||||
path: ./build
|
||||
key: prototyping-${{ runner.os }}-${{ hashFiles('Ast/**', 'Analysis/**', 'CLI/Ast.cpp', 'CLI/FileUtils.*')}}
|
||||
- name: install cabal
|
||||
run: sudo apt-get install -y cabal-install
|
||||
- name: cabal update
|
||||
|
|
@ -43,26 +48,35 @@ jobs:
|
|||
working-directory: prototyping
|
||||
run: |
|
||||
cabal install Agda-${{ matrix.agda }}
|
||||
cabal install --lib scientific --package-env .
|
||||
cabal install --lib vector --package-env .
|
||||
cabal install --lib aeson --package-env .
|
||||
- name: check examples
|
||||
cabal install --lib scientific vector aeson --package-env .
|
||||
- name: check targets
|
||||
working-directory: prototyping
|
||||
run: ~/.cabal/bin/agda Examples.agda
|
||||
run: |
|
||||
~/.cabal/bin/agda Examples.agda
|
||||
~/.cabal/bin/agda Properties.agda
|
||||
- name: build executables
|
||||
working-directory: prototyping
|
||||
run: |
|
||||
~/.cabal/bin/agda --compile PrettyPrinter.agda
|
||||
~/.cabal/bin/agda --compile Interpreter.agda
|
||||
- name: cmake configure
|
||||
run: cmake .
|
||||
if: steps.luau-ast-cache.outputs.cache-hit != 'true'
|
||||
run: |
|
||||
mkdir -p build
|
||||
cd build
|
||||
cmake build ../
|
||||
- name: cmake build luau-ast
|
||||
run: cmake --build . --target Luau.Ast.CLI
|
||||
- name: run smoketest
|
||||
if: steps.luau-ast-cache.outputs.cache-hit != 'true'
|
||||
run: |
|
||||
cmake --build ./build --target Luau.Ast.CLI
|
||||
- name: run tests
|
||||
working-directory: prototyping
|
||||
run: |
|
||||
../luau-ast Examples/SmokeTest.lua | ./PrettyPrinter > Examples/SmokeTestOutput.lua
|
||||
../luau-ast Examples/SmokeTest.lua | ./Interpreter
|
||||
- name: diff smoketest
|
||||
working-directory: prototyping
|
||||
run: diff Examples/SmokeTest.lua Examples/SmokeTestOutput.lua
|
||||
mkdir test-failures
|
||||
python tests.py -l ../build/luau-ast --write-diff-failures --diff-failure-location test-failures/
|
||||
- uses: actions/upload-artifact@v2
|
||||
if: failure()
|
||||
with:
|
||||
name: test failures
|
||||
path: prototyping/test-failures
|
||||
retention-days: 5
|
||||
|
|
|
|||
|
|
@ -178,11 +178,11 @@ LUA_API int lua_pushthread(lua_State* L);
|
|||
/*
|
||||
** get functions (Lua -> stack)
|
||||
*/
|
||||
LUA_API void lua_gettable(lua_State* L, int idx);
|
||||
LUA_API void lua_getfield(lua_State* L, int idx, const char* k);
|
||||
LUA_API void lua_rawgetfield(lua_State* L, int idx, const char* k);
|
||||
LUA_API void lua_rawget(lua_State* L, int idx);
|
||||
LUA_API void lua_rawgeti(lua_State* L, int idx, int n);
|
||||
LUA_API int lua_gettable(lua_State* L, int idx);
|
||||
LUA_API int lua_getfield(lua_State* L, int idx, const char* k);
|
||||
LUA_API int lua_rawgetfield(lua_State* L, int idx, const char* k);
|
||||
LUA_API int lua_rawget(lua_State* L, int idx);
|
||||
LUA_API int lua_rawgeti(lua_State* L, int idx, int n);
|
||||
LUA_API void lua_createtable(lua_State* L, int narr, int nrec);
|
||||
|
||||
LUA_API void lua_setreadonly(lua_State* L, int idx, int enabled);
|
||||
|
|
|
|||
|
|
@ -659,16 +659,16 @@ int lua_pushthread(lua_State* L)
|
|||
** get functions (Lua -> stack)
|
||||
*/
|
||||
|
||||
void lua_gettable(lua_State* L, int idx)
|
||||
int lua_gettable(lua_State* L, int idx)
|
||||
{
|
||||
luaC_checkthreadsleep(L);
|
||||
StkId t = index2addr(L, idx);
|
||||
api_checkvalidindex(L, t);
|
||||
luaV_gettable(L, t, L->top - 1, L->top - 1);
|
||||
return;
|
||||
return ttype(L->top - 1);
|
||||
}
|
||||
|
||||
void lua_getfield(lua_State* L, int idx, const char* k)
|
||||
int lua_getfield(lua_State* L, int idx, const char* k)
|
||||
{
|
||||
luaC_checkthreadsleep(L);
|
||||
StkId t = index2addr(L, idx);
|
||||
|
|
@ -677,10 +677,10 @@ void lua_getfield(lua_State* L, int idx, const char* k)
|
|||
setsvalue(L, &key, luaS_new(L, k));
|
||||
luaV_gettable(L, t, &key, L->top);
|
||||
api_incr_top(L);
|
||||
return;
|
||||
return ttype(L->top - 1);
|
||||
}
|
||||
|
||||
void lua_rawgetfield(lua_State* L, int idx, const char* k)
|
||||
int lua_rawgetfield(lua_State* L, int idx, const char* k)
|
||||
{
|
||||
luaC_checkthreadsleep(L);
|
||||
StkId t = index2addr(L, idx);
|
||||
|
|
@ -689,26 +689,26 @@ void lua_rawgetfield(lua_State* L, int idx, const char* k)
|
|||
setsvalue(L, &key, luaS_new(L, k));
|
||||
setobj2s(L, L->top, luaH_getstr(hvalue(t), tsvalue(&key)));
|
||||
api_incr_top(L);
|
||||
return;
|
||||
return ttype(L->top - 1);
|
||||
}
|
||||
|
||||
void lua_rawget(lua_State* L, int idx)
|
||||
int lua_rawget(lua_State* L, int idx)
|
||||
{
|
||||
luaC_checkthreadsleep(L);
|
||||
StkId t = index2addr(L, idx);
|
||||
api_check(L, ttistable(t));
|
||||
setobj2s(L, L->top - 1, luaH_get(hvalue(t), L->top - 1));
|
||||
return;
|
||||
return ttype(L->top - 1);
|
||||
}
|
||||
|
||||
void lua_rawgeti(lua_State* L, int idx, int n)
|
||||
int lua_rawgeti(lua_State* L, int idx, int n)
|
||||
{
|
||||
luaC_checkthreadsleep(L);
|
||||
StkId t = index2addr(L, idx);
|
||||
api_check(L, ttistable(t));
|
||||
setobj2s(L, L->top, luaH_getnum(hvalue(t), n));
|
||||
api_incr_top(L);
|
||||
return;
|
||||
return ttype(L->top - 1);
|
||||
}
|
||||
|
||||
void lua_createtable(lua_State* L, int narray, int nrec)
|
||||
|
|
|
|||
|
|
@ -68,8 +68,8 @@ SingletonType = STRING | 'true' | 'false'
|
|||
|
||||
Type =
|
||||
SimpleType ['?'] |
|
||||
SimpleType ['|' Type] |
|
||||
SimpleType ['&' Type]
|
||||
Type ['|' Type] |
|
||||
Type ['&' Type]
|
||||
|
||||
GenericTypePackParameter = NAME '...' ['=' (TypePack | VariadicTypePack | GenericTypePack)]
|
||||
GenericTypeParameterList = NAME ['=' Type] [',' GenericTypeParameterList] | GenericTypePackParameter {',' GenericTypePackParameter}
|
||||
|
|
|
|||
|
|
@ -317,3 +317,13 @@ The code above can be rewritten as follows to avoid the warning and the associat
|
|||
```lua
|
||||
local x = if flag then false else true
|
||||
```
|
||||
|
||||
## CommentDirective (26)
|
||||
|
||||
Luau uses comments that start from `!` to control certain aspects of analysis, for example setting type checking mode via `--!strict` or disabling individual lints with `--!nolint`. Unknown directives are ignored, for example `--!nostrict` doesn't have any effect on the type checking process as the correct spelling is `--!nonstrict`. This warning flags comment directives that are ignored during processing:
|
||||
|
||||
```lua
|
||||
--!nostrict
|
||||
-- Unknown comment directive 'nostrict'; did you mean 'nonstrict'?"
|
||||
```
|
||||
```
|
||||
|
|
|
|||
|
|
@ -2,5 +2,11 @@
|
|||
*.agdai
|
||||
Main
|
||||
MAlonzo
|
||||
Examples
|
||||
PrettyPrinter
|
||||
Interpreter
|
||||
Properties
|
||||
!Tests/Interpreter
|
||||
!Tests/PrettyPrinter
|
||||
.ghc.*
|
||||
test-failures/
|
||||
|
|
|
|||
|
|
@ -6,4 +6,3 @@ open import Luau.Heap using (∅)
|
|||
|
||||
ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
|
||||
ex1 = subst
|
||||
|
||||
|
|
|
|||
|
|
@ -3,8 +3,9 @@
|
|||
module Examples.Run where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
|
||||
open import Luau.Value using (nil)
|
||||
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.Value using (nil; number; bool)
|
||||
open import Luau.Run using (run; return)
|
||||
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
|
||||
|
||||
|
|
@ -13,3 +14,12 @@ import Agda.Builtin.Equality.Rewrite
|
|||
|
||||
ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
|
||||
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
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -1,8 +0,0 @@
|
|||
module FFI.Data.Bool where
|
||||
|
||||
{-# FOREIGN GHC import qualified Data.Bool #-}
|
||||
|
||||
data Bool : Set where
|
||||
false : Bool
|
||||
true : Bool
|
||||
{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}
|
||||
|
|
@ -1,6 +1,21 @@
|
|||
module FFI.Data.Scientific where
|
||||
|
||||
open import Agda.Builtin.Float using (Float)
|
||||
open import FFI.Data.String using (String)
|
||||
open import FFI.Data.HaskellString using (HaskellString; pack; unpack)
|
||||
|
||||
{-# FOREIGN GHC import qualified Data.Scientific #-}
|
||||
{-# FOREIGN GHC import qualified Text.Show #-}
|
||||
|
||||
postulate Scientific : Set
|
||||
{-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}
|
||||
|
||||
postulate
|
||||
showHaskell : Scientific → HaskellString
|
||||
toFloat : Scientific → Float
|
||||
|
||||
{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
|
||||
{-# COMPILE GHC toFloat = \x -> Data.Scientific.toRealFloat x #-}
|
||||
|
||||
show : Scientific → String
|
||||
show x = pack (showHaskell x)
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ module FFI.Data.Vector where
|
|||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Int using (Int; pos; negsuc)
|
||||
open import Agda.Builtin.Nat using (Nat)
|
||||
open import FFI.Data.Bool using (Bool; false; true)
|
||||
open import Agda.Builtin.Bool using (Bool; false; true)
|
||||
open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
|
||||
|
|
|
|||
|
|
@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value
|
|||
|
||||
main : IO ⊤
|
||||
main = getContents >>= runString
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,50 @@
|
|||
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 Utility.Bool using (not; _or_; _and_)
|
||||
open import Agda.Builtin.Nat using (_==_)
|
||||
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; Value; bool)
|
||||
open import Luau.RuntimeType using (RuntimeType; valueType)
|
||||
|
||||
evalNumOp : Float → BinaryOperator → Float → Value
|
||||
evalNumOp x + y = number (primFloatPlus x y)
|
||||
evalNumOp x - y = number (primFloatMinus x y)
|
||||
evalNumOp x * y = number (primFloatTimes x y)
|
||||
evalNumOp x / y = number (primFloatDiv x y)
|
||||
evalNumOp x < y = bool (primFloatLess x y)
|
||||
evalNumOp x > y = bool (primFloatLess y x)
|
||||
evalNumOp x ≡ y = bool (primFloatEquality x y)
|
||||
evalNumOp x ≅ y = bool (primFloatInequality x y)
|
||||
evalNumOp x ≤ y = bool ((primFloatLess x y) or (primFloatEquality x y))
|
||||
evalNumOp x ≥ y = bool ((primFloatLess y x) or (primFloatEquality x y))
|
||||
|
||||
evalEqOp : Value → Value → Value
|
||||
evalEqOp Value.nil Value.nil = bool true
|
||||
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 _ _ = bool false
|
||||
|
||||
evalNeqOp : Value → Value → Value
|
||||
evalNeqOp Value.nil Value.nil = bool false
|
||||
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 _ _ = bool true
|
||||
|
||||
coerceToBool : Value → Bool
|
||||
coerceToBool Value.nil = false
|
||||
coerceToBool (addr x) = true
|
||||
coerceToBool (number x) = true
|
||||
coerceToBool (bool x) = x
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
|
||||
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
|
||||
|
|
@ -23,17 +62,23 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
-------------------------------------------
|
||||
H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
|
||||
|
||||
app : ∀ {H H′ M M′ N} →
|
||||
app₁ : ∀ {H H′ M M′ N} →
|
||||
|
||||
H ⊢ M ⟶ᴱ M′ ⊣ H′ →
|
||||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
|
||||
|
||||
beta : ∀ {H M a F B} →
|
||||
app₂ : ∀ {H H′ V N N′} →
|
||||
|
||||
H ⊢ N ⟶ᴱ N′ ⊣ H′ →
|
||||
-----------------------------
|
||||
H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′
|
||||
|
||||
beta : ∀ {H a F B V} →
|
||||
|
||||
H [ a ] ≡ just(function F is B end) →
|
||||
-----------------------------------------------------
|
||||
H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
|
||||
-----------------------------------------------------------------------------
|
||||
H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H
|
||||
|
||||
block : ∀ {H H′ B B′ b} →
|
||||
|
||||
|
|
@ -51,6 +96,34 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
---------------------------------
|
||||
H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
|
||||
|
||||
binOpEquality :
|
||||
∀ {H x y} →
|
||||
---------------------------------------------------------------------------
|
||||
H ⊢ (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H
|
||||
|
||||
binOpInequality :
|
||||
∀ {H x y} →
|
||||
----------------------------------------------------------------------------
|
||||
H ⊢ (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H
|
||||
|
||||
binOpNumbers :
|
||||
∀ {H x op y} →
|
||||
-----------------------------------------------------------------------
|
||||
H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp 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} →
|
||||
|
|
@ -88,5 +161,3 @@ data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set wher
|
|||
H′ ⊢ B′ ⟶* B″ ⊣ H″ →
|
||||
------------------
|
||||
H ⊢ B ⟶* B″ ⊣ H″
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -3,19 +3,25 @@ module Luau.RuntimeError where
|
|||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Luau.Heap using (Heap; _[_])
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
|
||||
open import FFI.Data.String using (String)
|
||||
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 : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
|
||||
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 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)
|
||||
return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,19 +1,27 @@
|
|||
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; UnboundVariable; SEGV; 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.Syntax using (name)
|
||||
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ᴱ (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ᴱ (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"
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,15 @@
|
|||
module Luau.RuntimeType where
|
||||
|
||||
open import Luau.Value using (Value; nil; addr; number; bool)
|
||||
|
||||
data RuntimeType : Set where
|
||||
function : RuntimeType
|
||||
number : RuntimeType
|
||||
nil : RuntimeType
|
||||
boolean : RuntimeType
|
||||
|
||||
valueType : Value → RuntimeType
|
||||
valueType nil = nil
|
||||
valueType (addr x) = function
|
||||
valueType (number x) = number
|
||||
valueType (bool _) = boolean
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
module Luau.RuntimeType.ToString where
|
||||
|
||||
open import FFI.Data.String using (String)
|
||||
open import Luau.RuntimeType using (RuntimeType; function; number; nil; boolean)
|
||||
|
||||
runtimeTypeToString : RuntimeType → String
|
||||
runtimeTypeToString function = "function"
|
||||
runtimeTypeToString number = "number"
|
||||
runtimeTypeToString nil = "nil"
|
||||
runtimeTypeToString boolean = "boolean"
|
||||
|
|
@ -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)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; 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)
|
||||
|
|
@ -11,11 +11,15 @@ var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr
|
|||
_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
|
||||
|
||||
nil [ v / x ]ᴱ = nil
|
||||
true [ v / x ]ᴱ = true
|
||||
false [ v / x ]ᴱ = false
|
||||
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
|
||||
addr a [ v / x ]ᴱ = addr a
|
||||
(number y) [ v / x ]ᴱ = number y
|
||||
(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))
|
||||
|
|
@ -27,4 +31,3 @@ var y [ v / x ]ᴱwhenever no p = var y
|
|||
|
||||
B [ v / x ]ᴮunless yes p = B
|
||||
B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
module Luau.Syntax where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Float using (Float)
|
||||
open import Properties.Dec using (⊥)
|
||||
open import Luau.Var using (Var)
|
||||
open import Luau.Addr using (Addr)
|
||||
|
|
@ -32,6 +33,18 @@ arg : ∀ {a} → FunDec a → VarDec a
|
|||
arg (f ⟨ x ⟩∈ T) = x
|
||||
arg (f ⟨ x ⟩) = x
|
||||
|
||||
data BinaryOperator : Set where
|
||||
+ : BinaryOperator
|
||||
- : BinaryOperator
|
||||
* : BinaryOperator
|
||||
/ : BinaryOperator
|
||||
< : BinaryOperator
|
||||
> : BinaryOperator
|
||||
≡ : BinaryOperator
|
||||
≅ : BinaryOperator
|
||||
≤ : BinaryOperator
|
||||
≥ : BinaryOperator
|
||||
|
||||
data Block (a : Annotated) : Set
|
||||
data Stat (a : Annotated) : Set
|
||||
data Expr (a : Annotated) : Set
|
||||
|
|
@ -47,9 +60,12 @@ data Stat a where
|
|||
|
||||
data Expr a where
|
||||
nil : Expr a
|
||||
true : Expr a
|
||||
false : Expr a
|
||||
var : Var → Expr a
|
||||
addr : Addr → Expr a
|
||||
_$_ : Expr a → Expr a → Expr a
|
||||
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
|
||||
|
|
|
|||
|
|
@ -1,14 +1,15 @@
|
|||
module Luau.Syntax.FromJSON where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec)
|
||||
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; _∷_; [])
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
|
||||
open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
|
||||
open import FFI.Data.Bool using (true; false)
|
||||
open import FFI.Data.Either using (Either; Left; Right)
|
||||
open import FFI.Data.Maybe using (Maybe; nothing; just)
|
||||
open import FFI.Data.Scientific using (toFloat)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import FFI.Data.Vector using (head; tail; null; empty)
|
||||
|
||||
|
|
@ -19,8 +20,12 @@ lokal = fromString "local"
|
|||
list = fromString "list"
|
||||
name = fromString "name"
|
||||
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
|
||||
|
|
@ -32,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)
|
||||
|
|
@ -41,6 +48,21 @@ 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 "CompareEq" = Right ≡
|
||||
binOpFromString "CompareNe" = Right ≅
|
||||
binOpFromString "CompareLt" = Right <
|
||||
binOpFromString "CompareLe" = Right ≤
|
||||
binOpFromString "CompareGt" = Right >
|
||||
binOpFromString "CompareGe" = Right ≥
|
||||
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
|
||||
|
||||
varDecFromJSON (object arg) = varDecFromObject arg
|
||||
varDecFromJSON val = Left "VarDec not an object"
|
||||
|
||||
|
|
@ -83,6 +105,24 @@ exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
|
|||
exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
|
||||
exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
|
||||
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
|
||||
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 "AstExprConstantBool") with lookup value obj
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
|
||||
exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool 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"
|
||||
|
|
@ -140,3 +180,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)
|
||||
|
||||
|
|
@ -1,6 +1,7 @@
|
|||
module Luau.Syntax.ToString where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
|
||||
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; true; false)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Type.ToString using (typeToString)
|
||||
|
|
@ -16,6 +17,18 @@ 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 / = "/"
|
||||
binOpToString < = "<"
|
||||
binOpToString > = ">"
|
||||
binOpToString ≡ = "=="
|
||||
binOpToString ≅ = "~="
|
||||
binOpToString ≤ = "<="
|
||||
binOpToString ≥ = ">="
|
||||
|
||||
exprToString′ : ∀ {a} → String → Expr a → String
|
||||
statToString′ : ∀ {a} → String → Stat a → String
|
||||
blockToString′ : ∀ {a} → String → Block a → String
|
||||
|
|
@ -36,6 +49,10 @@ exprToString′ lb (block b is B end) =
|
|||
"(" ++ b ++ "()" ++ lb ++
|
||||
" " ++ (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
|
||||
exprToString′ lb true = "true"
|
||||
exprToString′ lb false = "false"
|
||||
|
||||
statToString′ lb (function F is B end) =
|
||||
"local " ++ funDecToString F ++ lb ++
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ data Type : Set where
|
|||
_⇒_ : Type → Type → Type
|
||||
none : Type
|
||||
any : Type
|
||||
number : Type
|
||||
_∪_ : Type → Type → Type
|
||||
_∩_ : Type → Type → Type
|
||||
|
||||
|
|
@ -15,6 +16,7 @@ src nil = none
|
|||
src (S ⇒ T) = S
|
||||
src none = none
|
||||
src any = any
|
||||
src number = none
|
||||
src (S ∪ T) = (src S) ∪ (src T)
|
||||
src (S ∩ T) = (src S) ∩ (src T)
|
||||
|
||||
|
|
@ -23,6 +25,7 @@ tgt nil = none
|
|||
tgt (S ⇒ T) = T
|
||||
tgt none = none
|
||||
tgt any = any
|
||||
tgt number = none
|
||||
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
|
||||
tgt (S ∩ T) = (tgt S) ∩ (tgt T)
|
||||
|
||||
|
|
@ -40,4 +43,3 @@ normalizeOptional (S ∪ T) | S′ | nil = optional S′
|
|||
normalizeOptional (S ∪ T) | nil | T′ = optional T′
|
||||
normalizeOptional (S ∪ T) | S′ | T′ = S′ ∪ T′
|
||||
normalizeOptional T = T
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
module Luau.Type.FromJSON where
|
||||
|
||||
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any)
|
||||
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
|
||||
|
||||
open import Agda.Builtin.List using (List; _∷_; [])
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
|
||||
open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
|
||||
open import FFI.Data.Bool using (true; false)
|
||||
open import FFI.Data.Either using (Either; Left; Right)
|
||||
open import FFI.Data.Maybe using (Maybe; nothing; just)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
|
|
@ -41,6 +41,7 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
|
|||
typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
|
||||
|
||||
typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
module Luau.Type.ToString where
|
||||
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
|
||||
open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)
|
||||
|
||||
{-# TERMINATING #-}
|
||||
typeToString : Type → String
|
||||
|
|
@ -12,6 +12,7 @@ typeToString nil = "nil"
|
|||
typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
|
||||
typeToString none = "none"
|
||||
typeToString any = "any"
|
||||
typeToString number = "number"
|
||||
typeToString (S ∪ T) with normalizeOptional(S ∪ T)
|
||||
typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
|
||||
typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
|
||||
|
|
|
|||
|
|
@ -1,15 +1,20 @@
|
|||
module Luau.Value where
|
||||
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import Agda.Builtin.Float using (Float)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Syntax using (Block; Expr; nil; addr)
|
||||
open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false)
|
||||
open import Luau.Var using (Var)
|
||||
|
||||
data Value : Set where
|
||||
nil : Value
|
||||
addr : Addr → Value
|
||||
number : Float → Value
|
||||
bool : Bool → Value
|
||||
|
||||
val : ∀ {a} → Value → Expr a
|
||||
val nil = nil
|
||||
val (addr a) = addr a
|
||||
|
||||
|
||||
val (number x) = number x
|
||||
val (bool false) = false
|
||||
val (bool true) = true
|
||||
|
|
|
|||
|
|
@ -1,10 +1,14 @@
|
|||
module Luau.Value.ToString where
|
||||
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Luau.Value using (Value; nil; addr)
|
||||
open import Agda.Builtin.Float using (primShowFloat)
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import Luau.Value using (Value; nil; addr; number; bool)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
|
||||
valueToString : Value → String
|
||||
valueToString nil = "nil"
|
||||
valueToString (addr a) = addrToString a
|
||||
|
||||
valueToString (number x) = primShowFloat x
|
||||
valueToString (bool false) = "false"
|
||||
valueToString (bool true) = "true"
|
||||
|
|
|
|||
|
|
@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value
|
|||
|
||||
main : IO ⊤
|
||||
main = getContents >>= runString
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
module Properties where
|
||||
|
||||
import Properties.Contradiction
|
||||
import Properties.Dec
|
||||
import Properties.Equality
|
||||
import Properties.Step
|
||||
import Properties.Remember
|
||||
|
|
|
|||
|
|
@ -0,0 +1,9 @@
|
|||
module Properties.Contradiction where
|
||||
|
||||
data ⊥ : Set where
|
||||
|
||||
¬ : Set → Set
|
||||
¬ A = A → ⊥
|
||||
|
||||
CONTRADICTION : ∀ {A : Set} → ⊥ → A
|
||||
CONTRADICTION ()
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
module Properties.Equality where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Properties.Contradiction using (¬)
|
||||
|
||||
sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a)
|
||||
sym refl = refl
|
||||
|
||||
trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
|
||||
trans refl refl = refl
|
||||
|
||||
cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b)
|
||||
cong f refl = refl
|
||||
|
||||
subst₁ : ∀ {A : Set} {a b : A} (F : A → Set) → (a ≡ b) → (F a) → (F b)
|
||||
subst₁ F refl x = x
|
||||
|
||||
subst₂ : ∀ {A B : Set} {a b : A} {c d : B} (F : A → B → Set) → (a ≡ b) → (c ≡ d) → (F a c) → (F b d)
|
||||
subst₂ F refl refl x = x
|
||||
|
||||
_≢_ : ∀ {A : Set} → A → A → Set
|
||||
(a ≢ b) = ¬(a ≡ b)
|
||||
|
||||
|
|
@ -1,13 +1,16 @@
|
|||
module Properties.Step where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
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)
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; true; false; 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; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality)
|
||||
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)
|
||||
open import Luau.Value using (nil; addr; val; number; bool)
|
||||
open import Properties.Remember using (remember; _,_)
|
||||
|
||||
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
|
||||
|
|
@ -30,13 +33,21 @@ stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
|
|||
stepᴱ H nil = value nil refl
|
||||
stepᴱ H (var x) = error (UnboundVariable x)
|
||||
stepᴱ H (addr a) = value (addr a) refl
|
||||
stepᴱ H (number x) = value (number x) refl
|
||||
stepᴱ H (true) = value (bool true) refl
|
||||
stepᴱ H (false) = value (bool false) refl
|
||||
stepᴱ H (M $ N) with stepᴱ H M
|
||||
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
|
||||
stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
|
||||
stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
|
||||
stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
|
||||
stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
|
||||
stepᴱ H (M $ N) | error E = error (app E)
|
||||
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 (app₁ (TypeMismatch function nil λ()))
|
||||
stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
|
||||
stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ()))
|
||||
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)
|
||||
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
|
||||
stepᴱ H (M $ N) | error E = error (app₁ E)
|
||||
stepᴱ H (block b is B end) with stepᴮ H B
|
||||
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
|
||||
stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
|
||||
|
|
@ -44,6 +55,22 @@ 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
|
||||
-- Have to use explicit form for ≡ here because it's a heavily overloaded symbol
|
||||
stepᴱ H (binexp x Luau.Syntax.≡ y) | value x′ refl | value y′ refl = step H (val (evalEqOp x′ y′)) binOpEquality
|
||||
stepᴱ H (binexp x ≅ y) | value x′ refl | value y′ refl = step H (val (evalNeqOp x′ y′)) binOpInequality
|
||||
stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (val (evalNumOp x′ op y′)) binOpNumbers
|
||||
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) | value (bool x′) refl | _ = error (bin₁ (TypeMismatch number (bool x′) λ()))
|
||||
stepᴱ H (binexp x op y) | _ | value (bool y′) refl = error (bin₂ (TypeMismatch number (bool y′) λ()))
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -25,3 +25,21 @@ and run!
|
|||
```
|
||||
luau-ast Examples/SmokeTest.lua | ./PrettyPrinter
|
||||
```
|
||||
|
||||
## Testing
|
||||
|
||||
We have a series of snapshot tests in the `Tests/` directory. You interact with the tests using the `tests` Python script in the `prototyping` directory. To simply run the tests, run:
|
||||
|
||||
```sh
|
||||
tests --luau-cli ../build/luau-ast --build
|
||||
```
|
||||
|
||||
This will build the test targets and run them. Run `tests --help` for information about all the command-line options.
|
||||
|
||||
### Adding a new test
|
||||
|
||||
To add a new test, add it to `Tests/{SUITE_NAME}/{CASE_NAME}`. You'll need an `in.lua` file and an `out.txt` file. The `in.lua` file is the input Luau source code, while the `out.txt` file is the expected output after running `luau-ast in.lua | test_executable`.
|
||||
|
||||
### Updating a test
|
||||
|
||||
If you make a change to the prototype that results in an expected change in behavior, you might want to update the test cases automatically. To do this, run `tests` with the `--accept-new-output` (`-a` for short) flag. Rather than diffing the output, this will overwrite the `out.txt` files for each test case with the actual result. Commit the resulting changes with your PR.
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
return true == false
|
||||
|
|
@ -0,0 +1 @@
|
|||
false
|
||||
|
|
@ -0,0 +1 @@
|
|||
return 1 == 1
|
||||
|
|
@ -0,0 +1 @@
|
|||
true
|
||||
|
|
@ -0,0 +1 @@
|
|||
return 1 + 2 - 2 * 2 / 2
|
||||
|
|
@ -0,0 +1 @@
|
|||
1.0
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
local function foo(x)
|
||||
return nil
|
||||
end
|
||||
|
||||
return foo(nil)
|
||||
|
|
@ -0,0 +1 @@
|
|||
nil
|
||||
|
|
@ -1,12 +1,12 @@
|
|||
local function id(x)
|
||||
return x
|
||||
return x
|
||||
end
|
||||
local function comp(f)
|
||||
return function(g)
|
||||
return function(x)
|
||||
return f(g(x))
|
||||
end
|
||||
end
|
||||
return function(g)
|
||||
return function(x)
|
||||
return f(g(x))
|
||||
end
|
||||
end
|
||||
end
|
||||
local id2 = comp(id)(id)
|
||||
local nil2 = id2(nil)
|
||||
|
|
@ -15,4 +15,5 @@ local b : nil = nil
|
|||
local c : (nil) -> nil = nil
|
||||
local d : (any & nil) = nil
|
||||
local e : any? = nil
|
||||
local f : number = 123
|
||||
return id2(nil2)
|
||||
|
|
@ -15,4 +15,5 @@ local b : nil = nil
|
|||
local c : (nil) -> nil = nil
|
||||
local d : (any & nil) = nil
|
||||
local e : any? = nil
|
||||
local f : number = 123.0
|
||||
return id2(nil2)
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
module Utility.Bool where
|
||||
|
||||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
|
||||
not : Bool → Bool
|
||||
not false = true
|
||||
not true = false
|
||||
|
||||
_or_ : Bool → Bool → Bool
|
||||
true or _ = true
|
||||
_ or true = true
|
||||
_ or _ = false
|
||||
|
||||
_and_ : Bool → Bool → Bool
|
||||
true and true = true
|
||||
_ and _ = false
|
||||
|
|
@ -0,0 +1,197 @@
|
|||
#!/usr/bin/python
|
||||
|
||||
import argparse
|
||||
import difflib
|
||||
import enum
|
||||
import os
|
||||
import os.path
|
||||
import subprocess
|
||||
import sys
|
||||
|
||||
SUITES = ["interpreter", "prettyprinter"]
|
||||
IN_FILE_NAME = "in.lua"
|
||||
OUT_FILE_NAME = "out.txt"
|
||||
SUITE_EXE_NAMES = {
|
||||
"interpreter": "Interpreter",
|
||||
"prettyprinter": "PrettyPrinter",
|
||||
}
|
||||
|
||||
SUITE_ENTRY_POINTS = {
|
||||
"interpreter": "Interpreter.agda",
|
||||
"prettyprinter": "PrettyPrinter.agda",
|
||||
}
|
||||
|
||||
SUITE_ROOTS = {
|
||||
"interpreter": "Tests/Interpreter",
|
||||
"prettyprinter": "Tests/PrettyPrinter",
|
||||
}
|
||||
|
||||
class TestResultStatus(enum.Enum):
|
||||
CLI_ERROR = 0
|
||||
EXE_ERROR = 1
|
||||
DIFF_ERROR = 2
|
||||
SUCCESS = 3
|
||||
WROTE_NEW = 4
|
||||
|
||||
class DiffFailure:
|
||||
def __init__(self, expected, actual):
|
||||
self.expected = expected
|
||||
self.actual = actual
|
||||
|
||||
def diff_text(self):
|
||||
diff_generator = difflib.context_diff(self.expected.splitlines(), self.actual.splitlines(), fromfile="expected", tofile="actual", n=3)
|
||||
return "".join(diff_generator)
|
||||
|
||||
def diff_html(self):
|
||||
differ = difflib.HtmlDiff(tabsize=4)
|
||||
return differ.make_file(self.expected.splitlines(), self.actual.splitlines(), fromdesc="Expected", todesc="Actual", context=True, numlines=5)
|
||||
|
||||
class TestCaseResult:
|
||||
def __init__(self, suite, case, status, details):
|
||||
self.suite = suite
|
||||
self.case = case
|
||||
self.status = status
|
||||
self.details = details
|
||||
|
||||
def did_pass(self):
|
||||
return self.status == TestResultStatus.SUCCESS or self.status == TestResultStatus.WROTE_NEW
|
||||
|
||||
def to_string(self):
|
||||
prefix = f"[{self.suite}/{self.case}]: "
|
||||
if self.status == TestResultStatus.CLI_ERROR:
|
||||
return f"{prefix}CLI ERROR: {self.details}"
|
||||
elif self.status == TestResultStatus.EXE_ERROR:
|
||||
return f"{prefix}EXE ERROR: {self.details}"
|
||||
elif self.status == TestResultStatus.DIFF_ERROR:
|
||||
text_diff = self.details.diff_text()
|
||||
return f"{prefix}FAILED:\n{text_diff}"
|
||||
elif self.status == TestResultStatus.SUCCESS:
|
||||
return f"{prefix}SUCCEEDED"
|
||||
elif self.status == TestResultStatus.WROTE_NEW:
|
||||
return f"{prefix}WROTE NEW RESULT"
|
||||
|
||||
def write_artifact(self, artifact_root):
|
||||
if self.status != TestResultStatus.DIFF_ERROR:
|
||||
return
|
||||
|
||||
filename = f"{self.suite}-{self.case}.out.html"
|
||||
path = os.path.join(artifact_root, filename)
|
||||
html = self.details.diff_html()
|
||||
with open(path, "w") as file:
|
||||
file.write(html)
|
||||
|
||||
parser = argparse.ArgumentParser(description="Runs prototype test cases")
|
||||
parser.add_argument("--luau-cli", "-l", dest="cli_location", required=True, help="The location of luau-cli")
|
||||
parser.add_argument("--root", "-r", dest="prototype_root", required=False, default=os.getcwd(), help="The root of the prototype")
|
||||
parser.add_argument("--build", "-b", dest="build", action="store_true", default=True, help="Whether to automatically build required test binaries")
|
||||
parser.add_argument("--suite", "-s", dest="suites", action="append", default=[], choices=SUITES, help="Which test suites to run")
|
||||
parser.add_argument("--case", "-c", dest="cases", action="append", default=[], help="Which test cases to run")
|
||||
parser.add_argument("--accept-new-output", "-a", dest="snapshot", action="store_true", default=False, help="Whether to write the new output to files, instead of diffing against it")
|
||||
parser.add_argument("--write-diff-failures", dest="write_diffs", action="store_true", default=False, help="Whether to write test failure diffs to files")
|
||||
parser.add_argument("--diff-failure-location", dest="diff_location", default=None, help="Where to write diff failure files to")
|
||||
|
||||
def build_suite(root, suite):
|
||||
entry_point = SUITE_ENTRY_POINTS.get(suite)
|
||||
if entry_point is None:
|
||||
return (False, "Invalid suite")
|
||||
|
||||
result = subprocess.run(["~/.cabal/bin/agda", "--compile", entry_point], shell=True, cwd=root, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
|
||||
if result.returncode == 0:
|
||||
return (True, None)
|
||||
else:
|
||||
return (False, result.stdout)
|
||||
|
||||
def run_test(in_path, out_path, cli_path, exe_path, snapshot):
|
||||
cli_result = subprocess.run([cli_path, in_path], capture_output=True)
|
||||
if cli_result.returncode != 0:
|
||||
return (TestResultStatus.CLI_ERROR, f"CLI error: {cli_result.stderr}")
|
||||
|
||||
exe_result = subprocess.run(exe_path, input=cli_result.stdout, capture_output=True)
|
||||
if exe_result.returncode != 0:
|
||||
return (TestResultStatus.EXE_ERROR, f"Executable error; stdout:{exe_result.stdout}\n\nstderr: {exe_result.stderr}")
|
||||
actual_result = exe_result.stdout.decode("utf-8")
|
||||
|
||||
if snapshot:
|
||||
with open(out_path, "w") as out_file:
|
||||
out_file.write(actual_result)
|
||||
return (TestResultStatus.WROTE_NEW, None)
|
||||
else:
|
||||
with open(out_path, "r") as out_file:
|
||||
expected_result = out_file.read()
|
||||
|
||||
if expected_result != actual_result:
|
||||
return (TestResultStatus.DIFF_ERROR, DiffFailure(expected_result, actual_result))
|
||||
|
||||
return (TestResultStatus.SUCCESS, None)
|
||||
|
||||
def should_run_case(case_name, filters):
|
||||
if len(filters) == 0:
|
||||
return True
|
||||
|
||||
return any([f in case_name for f in filters])
|
||||
|
||||
def run_test_suite(args, suite, suite_root, suite_exe):
|
||||
results = []
|
||||
|
||||
for entry in os.listdir(suite_root):
|
||||
if not should_run_case(entry, args.cases):
|
||||
continue
|
||||
|
||||
case_path = os.path.join(suite_root, entry)
|
||||
if os.path.isdir(case_path):
|
||||
in_path = os.path.join(case_path, IN_FILE_NAME)
|
||||
out_path = os.path.join(case_path, OUT_FILE_NAME)
|
||||
|
||||
if not os.path.exists(in_path) or not os.path.exists(out_path):
|
||||
continue
|
||||
|
||||
status, details = run_test(in_path, out_path, args.cli_location, suite_exe, args.snapshot)
|
||||
result = TestCaseResult(suite, entry, status, details)
|
||||
results.append(result)
|
||||
|
||||
return results
|
||||
|
||||
def main():
|
||||
args = parser.parse_args()
|
||||
|
||||
suites = args.suites if len(args.suites) > 0 else SUITES
|
||||
root = os.path.abspath(args.prototype_root)
|
||||
|
||||
if args.build:
|
||||
for suite in suites:
|
||||
success, reason = build_suite(root, suite)
|
||||
|
||||
if not success:
|
||||
print(f"Error building executable for test suite {suite}:\n{reason}")
|
||||
sys.exit(1)
|
||||
else:
|
||||
print(f"Built executable for test suite {suite} successfully.")
|
||||
|
||||
failed = False
|
||||
for suite in suites:
|
||||
suite_root = os.path.join(root, SUITE_ROOTS.get(suite))
|
||||
suite_exe = os.path.join(root, SUITE_EXE_NAMES.get(suite))
|
||||
print(f"Running test suite {suite}...")
|
||||
results = run_test_suite(args, suite, suite_root, suite_exe)
|
||||
|
||||
passed = 0
|
||||
total = len(results)
|
||||
|
||||
for result in results:
|
||||
if result.did_pass():
|
||||
passed += 1
|
||||
else:
|
||||
failed = True
|
||||
|
||||
print(f"Suite {suite} [{passed} / {total} passed]:")
|
||||
for result in results:
|
||||
print(result.to_string())
|
||||
|
||||
if args.write_diffs:
|
||||
result.write_artifact(args.diff_location)
|
||||
|
||||
if failed:
|
||||
sys.exit(1)
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
|
@ -23,12 +23,6 @@ This document tracks unimplemented RFCs.
|
|||
|
||||
**Status**: Implemented but depends on new transaction log implementation that is not fully live yet.
|
||||
|
||||
## Default type parameters
|
||||
|
||||
[RFC: Default type alias type parameters](https://github.com/Roblox/luau/blob/master/rfcs/syntax-default-type-alias-type-parameters.md)
|
||||
|
||||
**Status**: Implemented but not fully rolled out yet.
|
||||
|
||||
## Singleton types
|
||||
|
||||
[RFC: Singleton types](https://github.com/Roblox/luau/blob/master/rfcs/syntax-singleton-types.md)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
# Default type alias type parameters
|
||||
|
||||
**Status**: Implemented
|
||||
|
||||
## Summary
|
||||
|
||||
Introduce syntax to provide default type values inside the type alias type parameter list.
|
||||
|
|
|
|||
|
|
@ -712,6 +712,47 @@ TEST_CASE("Reference")
|
|||
CHECK(dtorhits == 2);
|
||||
}
|
||||
|
||||
TEST_CASE("ApiTables")
|
||||
{
|
||||
StateRef globalState(luaL_newstate(), lua_close);
|
||||
lua_State* L = globalState.get();
|
||||
|
||||
lua_newtable(L);
|
||||
lua_pushnumber(L, 123.0);
|
||||
lua_setfield(L, -2, "key");
|
||||
lua_pushstring(L, "test");
|
||||
lua_rawseti(L, -2, 5);
|
||||
|
||||
// lua_gettable
|
||||
lua_pushstring(L, "key");
|
||||
CHECK(lua_gettable(L, -2) == LUA_TNUMBER);
|
||||
CHECK(lua_tonumber(L, -1) == 123.0);
|
||||
lua_pop(L, 1);
|
||||
|
||||
// lua_getfield
|
||||
CHECK(lua_getfield(L, -1, "key") == LUA_TNUMBER);
|
||||
CHECK(lua_tonumber(L, -1) == 123.0);
|
||||
lua_pop(L, 1);
|
||||
|
||||
// lua_rawgetfield
|
||||
CHECK(lua_rawgetfield(L, -1, "key") == LUA_TNUMBER);
|
||||
CHECK(lua_tonumber(L, -1) == 123.0);
|
||||
lua_pop(L, 1);
|
||||
|
||||
// lua_rawget
|
||||
lua_pushstring(L, "key");
|
||||
CHECK(lua_rawget(L, -2) == LUA_TNUMBER);
|
||||
CHECK(lua_tonumber(L, -1) == 123.0);
|
||||
lua_pop(L, 1);
|
||||
|
||||
// lua_rawgeti
|
||||
CHECK(lua_rawgeti(L, -1, 5) == LUA_TSTRING);
|
||||
CHECK(strcmp(lua_tostring(L, -1), "test") == 0);
|
||||
lua_pop(L, 1);
|
||||
|
||||
lua_pop(L, 1);
|
||||
}
|
||||
|
||||
TEST_CASE("ApiFunctionCalls")
|
||||
{
|
||||
StateRef globalState = runConformance("apicalls.lua");
|
||||
|
|
|
|||
Loading…
Reference in New Issue