mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
Track untyped v typed syntax
This commit is contained in:
ajeffrey@roblox.com
parent
53b5251c0a
commit
1d66d8a3d3
19 changed files with 164 additions and 125 deletions
|
|
@ -1,7 +1,7 @@
|
|||
module Examples.OpSem where
|
||||
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
|
||||
open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_is_end)
|
||||
open import Luau.Syntax using (Block; no; var; nil; local_←_; _∙_; done; return; block_is_end)
|
||||
open import Luau.Heap using (∅)
|
||||
|
||||
ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
module Examples.Run where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Luau.Syntax using (nil; var; _$_; function_⟨_⟩_end; return; _∙_; done)
|
||||
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
|
||||
open import Luau.Value using (nil)
|
||||
open import Luau.Run using (run; return)
|
||||
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
|
||||
|
|
@ -11,5 +11,5 @@ open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
|
|||
import Agda.Builtin.Equality.Rewrite
|
||||
{-# REWRITE lookup-next next-emp lookup-next-emp #-}
|
||||
|
||||
ex1 : (run (function "id" ⟨ var "x" ⟩ return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
|
||||
ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
|
||||
ex1 = refl
|
||||
|
|
|
|||
|
|
@ -2,18 +2,21 @@ module Examples.Syntax where
|
|||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.String using (_++_)
|
||||
open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
|
||||
open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩; anon⟨_⟩)
|
||||
open import Luau.Syntax.ToString using (exprToString; blockToString)
|
||||
|
||||
ex1 : exprToString(var "f" $ var "x") ≡
|
||||
"f(x)"
|
||||
ex1 : exprToString(function anon⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
|
||||
"function (x)\n" ++
|
||||
" return f(x)\n" ++
|
||||
"end"
|
||||
ex1 = refl
|
||||
|
||||
ex2 : blockToString(return nil ∙ done) ≡
|
||||
"return nil"
|
||||
ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡
|
||||
"local x = nil\n" ++
|
||||
"return x"
|
||||
ex2 = refl
|
||||
|
||||
ex3 : blockToString(function "f" ⟨ var "x" ⟩ return (var "x") ∙ done end ∙ return (var "f") ∙ done) ≡
|
||||
ex3 : blockToString(function "f" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "f") ∙ done) ≡
|
||||
"local function f(x)\n" ++
|
||||
" return x\n" ++
|
||||
"end\n" ++
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ open import Luau.Run using (run; return; done; error)
|
|||
open import Luau.RuntimeError.ToString using (errToStringᴮ)
|
||||
open import Luau.Value.ToString using (valueToString)
|
||||
|
||||
runBlock : Block → IO ⊤
|
||||
runBlock : ∀ {a} → Block a → IO ⊤
|
||||
runBlock block with run block
|
||||
runBlock block | return V D = putStrLn (valueToString V)
|
||||
runBlock block | done D = putStrLn "nil"
|
||||
|
|
|
|||
|
|
@ -5,36 +5,37 @@ open import FFI.Data.Maybe using (Maybe; just)
|
|||
open import FFI.Data.Vector using (Vector; length; snoc; empty)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Var using (Var)
|
||||
open import Luau.Syntax using (Block; Expr; VarDec; nil; addr; function⟨_⟩_end)
|
||||
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)
|
||||
|
||||
data HeapValue : Set where
|
||||
function_⟨_⟩_end : Var → VarDec → Block → HeapValue
|
||||
data HeapValue (a : Annotated) : Set where
|
||||
function_is_end : FunDec a → Block a → HeapValue a
|
||||
|
||||
Heap = Vector HeapValue
|
||||
Heap : Annotated → Set
|
||||
Heap a = Vector (HeapValue a)
|
||||
|
||||
data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where
|
||||
data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where
|
||||
|
||||
defn : ∀ {H val} →
|
||||
|
||||
-----------------------------------
|
||||
(snoc H val) ≡ H ⊕ (length H) ↦ val
|
||||
|
||||
_[_] : Heap → Addr → Maybe HeapValue
|
||||
_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a)
|
||||
_[_] = FFI.Data.Vector.lookup
|
||||
|
||||
∅ : Heap
|
||||
∅ : ∀ {a} → Heap a
|
||||
∅ = empty
|
||||
|
||||
data AllocResult (H : Heap) (V : HeapValue) : Set where
|
||||
ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
|
||||
data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
|
||||
ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V
|
||||
|
||||
alloc : ∀ H V → AllocResult H V
|
||||
alloc : ∀ {a} H V → AllocResult a H V
|
||||
alloc H V = ok (length H) (snoc H V) defn
|
||||
|
||||
next : Heap → Addr
|
||||
next : ∀ {a} → Heap a → Addr
|
||||
next = length
|
||||
|
||||
allocated : Heap → HeapValue → Heap
|
||||
allocated : ∀ {a} → Heap a → HeapValue a → Heap a
|
||||
allocated = snoc
|
||||
|
||||
-- next-emp : (length empty ≡ 0)
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@ module Luau.OpSem where
|
|||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (just)
|
||||
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_⟨_⟩_end)
|
||||
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⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return; name)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; namify)
|
||||
open import Luau.Value using (addr; val)
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
|
||||
data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
|
||||
data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
|
||||
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
|
||||
|
||||
data _⊢_⟶ᴱ_⊣_ where
|
||||
|
||||
|
|
@ -17,11 +17,11 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
-------------------
|
||||
H ⊢ nil ⟶ᴱ nil ⊣ H
|
||||
|
||||
function : ∀ {H H′ a x B} →
|
||||
function : ∀ {H H′ a F B} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
|
||||
H′ ≡ H ⊕ a ↦ (function (namify F) is B end) →
|
||||
-------------------------------------------
|
||||
H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
|
||||
H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
|
||||
|
||||
app : ∀ {H H′ M M′ N} →
|
||||
|
||||
|
|
@ -29,11 +29,11 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
|
||||
|
||||
beta : ∀ {H M a f x B} →
|
||||
beta : ∀ {H M a F B} →
|
||||
|
||||
H [ a ] ≡ just(function f ⟨ x ⟩ B end) →
|
||||
H [ a ] ≡ just(function F is B end) →
|
||||
-----------------------------------------------------
|
||||
H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H
|
||||
H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
|
||||
|
||||
block : ∀ {H H′ B B′ b} →
|
||||
|
||||
|
|
@ -64,11 +64,11 @@ data _⊢_⟶ᴮ_⊣_ where
|
|||
------------------------------------------------------
|
||||
H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H
|
||||
|
||||
function : ∀ {H H′ a f x B C} →
|
||||
function : ∀ {H H′ a F B C} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
|
||||
H′ ≡ H ⊕ a ↦ (function F is C end) →
|
||||
--------------------------------------------------------------
|
||||
H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
|
||||
H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′
|
||||
|
||||
return : ∀ {H H′ M M′ B} →
|
||||
|
||||
|
|
@ -76,7 +76,7 @@ data _⊢_⟶ᴮ_⊣_ where
|
|||
--------------------------------------------
|
||||
H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
|
||||
|
||||
data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → Set where
|
||||
data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where
|
||||
|
||||
refl : ∀ {H B} →
|
||||
|
||||
|
|
|
|||
|
|
@ -8,13 +8,13 @@ open import Luau.Value using (val)
|
|||
open import Properties.Step using (stepᴮ; step; return; done; error)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ)
|
||||
|
||||
data RunResult (H : Heap) (B : Block) : Set where
|
||||
data RunResult {a} (H : Heap a) (B : Block a) : Set where
|
||||
return : ∀ V {B′ H′} → (H ⊢ B ⟶* (return (val V) ∙ B′) ⊣ H′) → RunResult H B
|
||||
done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B
|
||||
error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B
|
||||
|
||||
{-# TERMINATING #-}
|
||||
run′ : ∀ H B → RunResult H B
|
||||
run′ : ∀ {a} H B → RunResult {a} H B
|
||||
run′ H B with stepᴮ H B
|
||||
run′ H B | step H′ B′ D with run′ H′ B′
|
||||
run′ H B | step H′ B′ D | return V D′ = return V (step D D′)
|
||||
|
|
@ -24,5 +24,5 @@ run′ H _ | return V refl = return V refl
|
|||
run′ H _ | done refl = done refl
|
||||
run′ H B | error E = error E refl
|
||||
|
||||
run : ∀ B → RunResult ∅ B
|
||||
run : ∀ {a} B → RunResult {a} ∅ B
|
||||
run = run′ ∅
|
||||
|
|
|
|||
|
|
@ -3,10 +3,10 @@ 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; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
|
||||
|
||||
data RuntimeErrorᴮ (H : Heap) : Block → Set
|
||||
data RuntimeErrorᴱ (H : Heap) : Expr → Set
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -6,8 +6,8 @@ open import Luau.Addr.ToString using (addrToString)
|
|||
open import Luau.Var.ToString using (varToString)
|
||||
open import Luau.Syntax using (name)
|
||||
|
||||
errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
|
||||
errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String
|
||||
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"
|
||||
|
|
|
|||
|
|
@ -1,23 +1,23 @@
|
|||
module Luau.Substitution where
|
||||
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return; name)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; namify)
|
||||
open import Luau.Value using (Value; val)
|
||||
open import Luau.Var using (Var; _≡ⱽ_)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
|
||||
_[_/_]ᴱ : Expr → Value → Var → Expr
|
||||
_[_/_]ᴮ : Block → Value → Var → Block
|
||||
var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr
|
||||
_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block
|
||||
_[_/_]ᴱ : ∀ {a} → Expr a → Value → Var → Expr a
|
||||
_[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
|
||||
var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a
|
||||
_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
|
||||
|
||||
nil [ v / x ]ᴱ = nil
|
||||
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
|
||||
addr a [ v / x ]ᴱ = addr a
|
||||
(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
|
||||
function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ name y) end
|
||||
function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg(namify F))) end
|
||||
block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
|
||||
|
||||
(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ name y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
|
||||
(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))
|
||||
(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
|
||||
done [ v / x ]ᴮ = done
|
||||
|
|
|
|||
|
|
@ -1,37 +1,63 @@
|
|||
module Luau.Syntax where
|
||||
|
||||
open import Luau.Var using (Var)
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Properties.Dec using (⊥)
|
||||
open import Luau.Var using (Var; anon)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Type using (Type)
|
||||
|
||||
infixr 5 _∙_
|
||||
|
||||
data VarDec : Set where
|
||||
var : Var → VarDec
|
||||
var_∈_ : Var → Type → VarDec
|
||||
data Annotated : Set where
|
||||
maybe : Annotated
|
||||
yes : Annotated
|
||||
|
||||
name : VarDec → Var
|
||||
data VarDec : Annotated → Set where
|
||||
var : Var → VarDec maybe
|
||||
var_∈_ : ∀ {a} → Var → Type → VarDec a
|
||||
|
||||
name : ∀ {a} → VarDec a → Var
|
||||
name (var x) = x
|
||||
name (var x ∈ T) = x
|
||||
|
||||
data Block : Set
|
||||
data Stat : Set
|
||||
data Expr : Set
|
||||
data FunDec : Annotated → Set where
|
||||
_⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
|
||||
_⟨_⟩ : Var → VarDec maybe → FunDec maybe
|
||||
|
||||
data Block where
|
||||
_∙_ : Stat → Block → Block
|
||||
done : Block
|
||||
data AnonFunDec : Annotated → Set where
|
||||
anon⟨_⟩∈_ : ∀ {a} → VarDec a → Type → AnonFunDec a
|
||||
anon⟨_⟩ : VarDec maybe → AnonFunDec maybe
|
||||
|
||||
data Stat where
|
||||
function_⟨_⟩_end : Var → VarDec → Block → Stat
|
||||
local_←_ : VarDec → Expr → Stat
|
||||
return : Expr → Stat
|
||||
fun : ∀ {a} → FunDec a → Var
|
||||
fun (f ⟨ x ⟩∈ T) = f
|
||||
fun (f ⟨ x ⟩) = f
|
||||
|
||||
data Expr where
|
||||
nil : Expr
|
||||
var : Var → Expr
|
||||
addr : Addr → Expr
|
||||
_$_ : Expr → Expr → Expr
|
||||
function⟨_⟩_end : VarDec → Block → Expr
|
||||
block_is_end : Var → Block → Expr
|
||||
arg : ∀ {a} → FunDec a → VarDec a
|
||||
arg (f ⟨ x ⟩∈ T) = x
|
||||
arg (f ⟨ x ⟩) = x
|
||||
|
||||
namify : ∀ {a} → AnonFunDec a → FunDec a
|
||||
namify (anon⟨ x ⟩∈ T) = anon ⟨ x ⟩∈ T
|
||||
namify anon⟨ x ⟩ = anon ⟨ x ⟩
|
||||
|
||||
data Block (a : Annotated) : Set
|
||||
data Stat (a : Annotated) : Set
|
||||
data Expr (a : Annotated) : Set
|
||||
|
||||
data Block a where
|
||||
_∙_ : Stat a → Block a → Block a
|
||||
done : Block a
|
||||
|
||||
data Stat a where
|
||||
function_is_end : FunDec a → Block a → Stat a
|
||||
local_←_ : VarDec a → Expr a → Stat a
|
||||
return : Expr a → Stat a
|
||||
|
||||
data Expr a where
|
||||
nil : Expr a
|
||||
var : Var → Expr a
|
||||
addr : Addr → Expr a
|
||||
_$_ : Expr a → Expr a → Expr a
|
||||
function_is_end : AnonFunDec a → Block a → Expr a
|
||||
block_is_end : Var → Block a → Expr a
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
module Luau.Syntax.FromJSON where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
|
||||
open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function_is_end; anon⟨_⟩; _⟨_⟩; local_←_; return; done; _∙_; maybe)
|
||||
|
||||
open import Agda.Builtin.List using (List; _∷_; [])
|
||||
|
||||
|
|
@ -31,12 +31,12 @@ 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)
|
||||
|
||||
exprFromJSON : Value → Either String Expr
|
||||
exprFromObject : Object → Either String Expr
|
||||
statFromJSON : Value → Either String Stat
|
||||
statFromObject : Object → Either String Stat
|
||||
blockFromJSON : Value → Either String Block
|
||||
blockFromArray : Array → Either String Block
|
||||
exprFromJSON : Value → Either String (Expr maybe)
|
||||
exprFromObject : Object → Either String (Expr maybe)
|
||||
statFromJSON : Value → Either String (Stat maybe)
|
||||
statFromObject : Object → Either String (Stat maybe)
|
||||
blockFromJSON : Value → Either String (Block maybe)
|
||||
blockFromArray : Array → Either String (Block maybe)
|
||||
|
||||
exprFromJSON (object obj) = exprFromObject obj
|
||||
exprFromJSON val = Left "AstExpr not an object"
|
||||
|
|
@ -55,7 +55,7 @@ exprFromObject obj | just (string "AstExprCall") | _ | nothing = Left ("AstExpr
|
|||
exprFromObject obj | just (string "AstExprConstantNil") = Right nil
|
||||
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value with head arr | blockFromJSON value
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function⟨ var x ⟩ B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function anon⟨ var x ⟩ is B end)
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just _ | Right B = Left "AstExprFunction args not a string array"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | nothing | Right B = Left "Unsupported AstExprFunction empty args"
|
||||
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | _ | Left err = Left err
|
||||
|
|
@ -89,7 +89,7 @@ statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "Ast
|
|||
statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
|
||||
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value with exprFromJSON value
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function⟨ x ⟩ B end) = Right (function f ⟨ x ⟩ B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function anon⟨ x ⟩ is B end) = Right (function f ⟨ x ⟩ is B end)
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Left err = Left err
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
|
||||
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ = Left "AstStatLocalFunction name is not a string"
|
||||
|
|
|
|||
|
|
@ -1,18 +1,26 @@
|
|||
module Luau.Syntax.ToString where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat; Expr; VarDec; nil; var; var_∈_; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
|
||||
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; AnonFunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; anon⟨_⟩; anon⟨_⟩∈_)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Type.ToString using (typeToString)
|
||||
open import Luau.Var.ToString using (varToString)
|
||||
|
||||
varDecToString : VarDec → String
|
||||
varDecToString : ∀ {a} → VarDec a → String
|
||||
varDecToString (var x) = varToString x
|
||||
varDecToString (var x ∈ T) = varToString x ++ " : " ++ typeToString T
|
||||
|
||||
exprToString′ : String → Expr → String
|
||||
statToString′ : String → Stat → String
|
||||
blockToString′ : String → Block → String
|
||||
funDecToString : ∀ {a} → FunDec a → String
|
||||
funDecToString (f ⟨ x ⟩∈ T) = varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
|
||||
funDecToString (f ⟨ x ⟩) = varToString f ++ "(" ++ varDecToString x ++ ")"
|
||||
|
||||
anonFunDecToString : ∀ {a} → AnonFunDec a → String
|
||||
anonFunDecToString (anon⟨ x ⟩∈ T) = "(" ++ varDecToString x ++ "): " ++ typeToString T
|
||||
anonFunDecToString anon⟨ x ⟩ = "(" ++ varDecToString x ++ ")"
|
||||
|
||||
exprToString′ : ∀ {a} → String → Expr a → String
|
||||
statToString′ : ∀ {a} → String → Stat a → String
|
||||
blockToString′ : ∀ {a} → String → Block a → String
|
||||
|
||||
exprToString′ lb nil =
|
||||
"nil"
|
||||
|
|
@ -22,8 +30,8 @@ exprToString′ lb (var x) =
|
|||
varToString(x)
|
||||
exprToString′ lb (M $ N) =
|
||||
(exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
|
||||
exprToString′ lb (function⟨ x ⟩ B end) =
|
||||
"function(" ++ varDecToString x ++ ")" ++ lb ++
|
||||
exprToString′ lb (function F is B end) =
|
||||
"function " ++ anonFunDecToString F ++ lb ++
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end"
|
||||
exprToString′ lb (block b is B end) =
|
||||
|
|
@ -31,8 +39,8 @@ exprToString′ lb (block b is B end) =
|
|||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end)()"
|
||||
|
||||
statToString′ lb (function f ⟨ x ⟩ B end) =
|
||||
"local function " ++ f ++ "(" ++ varDecToString x ++ ")" ++ lb ++
|
||||
statToString′ lb (function F is B end) =
|
||||
"local function " ++ funDecToString F ++ lb ++
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end"
|
||||
statToString′ lb (local x ← M) =
|
||||
|
|
@ -44,11 +52,11 @@ blockToString′ lb (S ∙ done) = statToString′ lb S
|
|||
blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
|
||||
blockToString′ lb (done) = ""
|
||||
|
||||
exprToString : Expr → String
|
||||
exprToString : ∀ {a} → Expr a → String
|
||||
exprToString = exprToString′ "\n"
|
||||
|
||||
statToString : Stat → String
|
||||
statToString : ∀ {a} → Stat a → String
|
||||
statToString = statToString′ "\n"
|
||||
|
||||
blockToString : Block → String
|
||||
blockToString : ∀ {a} → Block a → String
|
||||
blockToString = blockToString′ "\n"
|
||||
|
|
|
|||
|
|
@ -2,10 +2,10 @@ module Luau.TypeCheck where
|
|||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (Maybe; just)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; var_∈_; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return; name)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; var_∈_; _⟨_⟩∈_; anon⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name)
|
||||
open import Luau.Var using (Var)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Heap using (Heap; HeapValue; function_⟨_⟩_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Luau.Value using (addr; val)
|
||||
open import Luau.Type using (Type; nil; any; _⇒_; src; tgt)
|
||||
open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ)
|
||||
|
|
@ -13,8 +13,8 @@ open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) re
|
|||
open import FFI.Data.Vector using (Vector)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
|
||||
data _▷_⊢ᴮ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Block → Type → VarCtxt → Set
|
||||
data _▷_⊢ᴱ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Expr → Type → VarCtxt → Set
|
||||
data _▷_⊢ᴮ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Block yes → Type → VarCtxt → Set
|
||||
data _▷_⊢ᴱ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Expr yes → Type → VarCtxt → Set
|
||||
|
||||
data _▷_⊢ᴮ_∋_∈_⊣_ where
|
||||
|
||||
|
|
@ -41,7 +41,7 @@ data _▷_⊢ᴮ_∋_∈_⊣_ where
|
|||
Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ any ∋ C ∈ U ⊣ Δ₁ →
|
||||
Σ ▷ (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ →
|
||||
---------------------------------------------------------------------------
|
||||
Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩ C end ∙ B ∈ V ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f))
|
||||
Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ V ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f))
|
||||
|
||||
data _▷_⊢ᴱ_∋_∈_⊣_ where
|
||||
|
||||
|
|
@ -69,11 +69,11 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where
|
|||
--------------------------------------
|
||||
Σ ▷ Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂)
|
||||
|
||||
function : ∀ {Σ x B S T U Γ Δ} →
|
||||
function : ∀ {Σ x B S T U V Γ Δ} →
|
||||
|
||||
Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ any ∋ B ∈ U ⊣ Δ →
|
||||
--------------------------------------------------------------
|
||||
Σ ▷ Γ ⊢ᴱ S ∋ (function⟨ var x ∈ T ⟩ B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x)
|
||||
Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ →
|
||||
----------------------------------------------------------------------
|
||||
Σ ▷ Γ ⊢ᴱ S ∋ (function anon⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x)
|
||||
|
||||
block : ∀ {Σ b B S T Γ Δ} →
|
||||
|
||||
|
|
@ -81,19 +81,19 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where
|
|||
----------------------------------------------------
|
||||
Σ ▷ Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ
|
||||
|
||||
data _▷_∈_ (Σ : AddrCtxt) : (Maybe HeapValue) → (Maybe Type) → Set where
|
||||
data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → (Maybe Type) → Set where
|
||||
|
||||
nothing :
|
||||
|
||||
---------------------
|
||||
Σ ▷ nothing ∈ nothing
|
||||
|
||||
function : ∀ {f x B T} →
|
||||
function : ∀ {f x B T U V W} →
|
||||
|
||||
Σ ▷ ∅ ⊢ᴱ any ∋ (function⟨ x ⟩ B end) ∈ T ⊣ ∅ →
|
||||
------------------------------------------------
|
||||
Σ ▷ just (function f ⟨ x ⟩ B end) ∈ just T
|
||||
Σ ▷ (x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ (x ↦ W) →
|
||||
--------------------------------------------------------------
|
||||
Σ ▷ just (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ just (T ⇒ U)
|
||||
|
||||
data _▷_✓ (Σ : AddrCtxt) (H : Heap) : Set where
|
||||
data _▷_✓ (Σ : AddrCtxt) (H : Heap yes) : Set where
|
||||
|
||||
defn : (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) → (Σ ▷ H ✓)
|
||||
defn : (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) → (Σ ▷ H ✓)
|
||||
|
|
|
|||
|
|
@ -1,14 +1,14 @@
|
|||
module Luau.Value where
|
||||
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; addr)
|
||||
open import Luau.Var using (Var)
|
||||
|
||||
data Value : Set where
|
||||
nil : Value
|
||||
addr : Addr → Value
|
||||
|
||||
val : Value → Expr
|
||||
val : ∀ {a} → Value → Expr a
|
||||
val nil = nil
|
||||
val (addr a) = addr a
|
||||
|
||||
|
|
|
|||
|
|
@ -14,3 +14,5 @@ a ≡ⱽ b with primStringEquality a b
|
|||
a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥
|
||||
a ≡ⱽ b | true = yes primTrustMe
|
||||
|
||||
anon : Var
|
||||
anon = "(anonymous)"
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ open import Luau.Syntax using (Block)
|
|||
open import Luau.Syntax.FromJSON using (blockFromJSON)
|
||||
open import Luau.Syntax.ToString using (blockToString)
|
||||
|
||||
runBlock : Block → IO ⊤
|
||||
runBlock : ∀ {a} → Block a → IO ⊤
|
||||
runBlock block = putStrLn (blockToString block)
|
||||
|
||||
runJSON : Value → IO ⊤
|
||||
|
|
|
|||
|
|
@ -3,4 +3,3 @@ module Properties where
|
|||
import Properties.Dec
|
||||
import Properties.Remember
|
||||
import Properties.Step
|
||||
import Properties.TypeCheck
|
||||
|
|
|
|||
|
|
@ -2,16 +2,16 @@ module Properties.Step where
|
|||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.Maybe using (just; nothing)
|
||||
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_⟨_⟩_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_; name)
|
||||
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; namify)
|
||||
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.Substitution using (_[_/_]ᴮ)
|
||||
open import Luau.Value using (nil; addr; val)
|
||||
open import Properties.Remember using (remember; _,_)
|
||||
|
||||
data StepResultᴮ (H : Heap) (B : Block) : Set
|
||||
data StepResultᴱ (H : Heap) (M : Expr) : Set
|
||||
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
|
||||
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
|
||||
|
||||
data StepResultᴮ H B where
|
||||
step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
|
||||
|
|
@ -24,8 +24,8 @@ data StepResultᴱ H M where
|
|||
value : ∀ V → (M ≡ val V) → StepResultᴱ H M
|
||||
error : (RuntimeErrorᴱ H M) → StepResultᴱ H M
|
||||
|
||||
stepᴱ : ∀ H M → StepResultᴱ H M
|
||||
stepᴮ : ∀ H B → StepResultᴮ H B
|
||||
stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
|
||||
stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
|
||||
|
||||
stepᴱ H nil = value nil refl
|
||||
stepᴱ H (var x) = error (UnboundVariable x)
|
||||
|
|
@ -35,18 +35,18 @@ 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 ⟨ x ⟩ B end) , p) = step H (block f is local x ← N ∙ B end) (beta 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 (function⟨ x ⟩ B end) with alloc H (function "anon" ⟨ x ⟩ B end)
|
||||
stepᴱ H (function⟨ x ⟩ B end) | ok a H′ p = step H′ (addr a) (function p)
|
||||
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
|
||||
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 (namify F) is C end)
|
||||
stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
|
||||
|
||||
stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function f ⟨ x ⟩ C end)
|
||||
stepᴮ H (function f ⟨ x ⟩ C end ∙ B) | ok a H′ p = step H′ (B [ addr a / f ]ᴮ) (function p)
|
||||
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)
|
||||
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
|
||||
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
|
||||
stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue