mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
First draft interpreter
This commit is contained in:
ajeffrey@roblox.com
parent
496a093abb
commit
8573eeda49
20 changed files with 234 additions and 73 deletions
|
|
@ -1,5 +1,7 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
module Examples where
|
||||
|
||||
import Examples.Syntax
|
||||
import Examples.OpSem
|
||||
import Examples.Run
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
module Examples.OpSem where
|
||||
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; local)
|
||||
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
|
||||
open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_end)
|
||||
open import Luau.Heap using (emp)
|
||||
|
||||
x = var "x"
|
||||
|
||||
ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
|
||||
ex1 = local
|
||||
ex1 = subst
|
||||
|
||||
|
|
|
|||
18
prototyping/Examples/Run.agda
Normal file
18
prototyping/Examples/Run.agda
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
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.Value using (nil)
|
||||
open import Luau.Run using (run; return)
|
||||
open import Luau.Heap using (emp; lookup-next; next-emp; lookup-next-emp)
|
||||
|
||||
import Agda.Builtin.Equality.Rewrite
|
||||
{-# REWRITE lookup-next next-emp lookup-next-emp #-}
|
||||
|
||||
x = var "x"
|
||||
id = var "id"
|
||||
|
||||
ex1 : (run emp (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
|
||||
ex1 = refl
|
||||
|
|
@ -8,5 +8,6 @@ local function comp(f)
|
|||
end
|
||||
end
|
||||
end
|
||||
local id2 = id(id)
|
||||
local id2 = comp (id)(id)
|
||||
local nil2 = id2(nil)
|
||||
return nil2(nil2)
|
||||
|
|
@ -1,5 +1,6 @@
|
|||
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)
|
||||
|
|
@ -17,17 +18,21 @@ postulate
|
|||
null : ∀ {A} → (Vector A) → Bool
|
||||
unsafeHead : ∀ {A} → (Vector A) → A
|
||||
unsafeTail : ∀ {A} → (Vector A) → (Vector A)
|
||||
hLength : ∀ {A} → (Vector A) → HaskellInt
|
||||
hLookup : ∀ {A} → (Vector A) → HaskellInt → (Maybe A)
|
||||
length : ∀ {A} → (Vector A) → Nat
|
||||
lookup : ∀ {A} → (Vector A) → Nat → (Maybe A)
|
||||
snoc : ∀ {A} → (Vector A) → A → (Vector A)
|
||||
{-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
|
||||
{-# COMPILE GHC null = \_ -> Data.Vector.null #-}
|
||||
{-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
|
||||
{-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
|
||||
{-# COMPILE GHC hLength = \_ -> Data.Vector.length #-}
|
||||
{-# COMPILE GHC hLookup = \_ -> (Data.Vector.!?) #-}
|
||||
{-# COMPILE GHC length = \_ -> (fromIntegral . Data.Vector.length) #-}
|
||||
{-# COMPILE GHC lookup = \_ v -> ((v Data.Vector.!?) . fromIntegral) #-}
|
||||
{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}
|
||||
|
||||
postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0)
|
||||
postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x)
|
||||
postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x)
|
||||
|
||||
head : ∀ {A} → (Vector A) → (Maybe A)
|
||||
head vec with null vec
|
||||
head vec | false = just (unsafeHead vec)
|
||||
|
|
@ -37,11 +42,3 @@ tail : ∀ {A} → (Vector A) → Vector A
|
|||
tail vec with null vec
|
||||
tail vec | false = unsafeTail vec
|
||||
tail vec | true = empty
|
||||
|
||||
length : ∀ {A} → (Vector A) → Nat
|
||||
length vec with haskellIntToInt(hLength vec)
|
||||
length vec | pos n = n
|
||||
length vec | negsuc n = 0
|
||||
|
||||
lookup : ∀ {A} → (Vector A) → Nat → Maybe A
|
||||
lookup vec n = hLookup vec (intToHaskellInt (pos n))
|
||||
|
|
|
|||
39
prototyping/Interpreter.agda
Normal file
39
prototyping/Interpreter.agda
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
module Interpreter where
|
||||
|
||||
open import Agda.Builtin.IO using (IO)
|
||||
open import Agda.Builtin.Int using (pos)
|
||||
open import Agda.Builtin.Unit using (⊤)
|
||||
|
||||
open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
|
||||
open import FFI.Data.Aeson using (Value; eitherDecode)
|
||||
open import FFI.Data.Either using (Left; Right)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import FFI.Data.Text.Encoding using (encodeUtf8)
|
||||
open import FFI.System.Exit using (exitWith; ExitFailure)
|
||||
|
||||
open import Luau.Syntax using (Block)
|
||||
open import Luau.Syntax.FromJSON using (blockFromJSON)
|
||||
open import Luau.Syntax.ToString using (blockToString)
|
||||
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 block with run block
|
||||
runBlock block | return V D = putStrLn (valueToString V)
|
||||
runBlock block | done D = putStrLn "nil"
|
||||
runBlock block | error E D = putStrLn (errToStringᴮ E)
|
||||
|
||||
runJSON : Value → IO ⊤
|
||||
runJSON value with blockFromJSON(value)
|
||||
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runJSON value | (Right block) = runBlock block
|
||||
|
||||
runString : String → IO ⊤
|
||||
runString txt with eitherDecode (encodeUtf8 txt)
|
||||
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
|
||||
runString txt | (Right value) = runJSON value
|
||||
|
||||
main : IO ⊤
|
||||
main = getContents >>= runString
|
||||
|
||||
|
|
@ -2,7 +2,6 @@ module Luau.Addr where
|
|||
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Agda.Builtin.Int using (Int; primShowInteger; pos)
|
||||
open import Agda.Builtin.Nat using (Nat; _==_)
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Agda.Builtin.TrustMe using (primTrustMe)
|
||||
|
|
@ -11,9 +10,6 @@ open import Properties.Dec using (Dec; yes; no; ⊥)
|
|||
Addr : Set
|
||||
Addr = Nat
|
||||
|
||||
addrToString : Addr → String
|
||||
addrToString a = primShowInteger (pos a)
|
||||
|
||||
_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b)
|
||||
a ≡ᴬ b with a == b
|
||||
a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥
|
||||
|
|
|
|||
8
prototyping/Luau/Addr/ToString.agda
Normal file
8
prototyping/Luau/Addr/ToString.agda
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
module Luau.Addr.ToString where
|
||||
|
||||
open import Agda.Builtin.String using (String; primStringAppend)
|
||||
open import Luau.Addr using (Addr)
|
||||
open import Agda.Builtin.Int using (Int; primShowInteger; pos)
|
||||
|
||||
addrToString : Addr → String
|
||||
addrToString a = primStringAppend "a" (primShowInteger (pos a))
|
||||
|
|
@ -1,13 +1,14 @@
|
|||
module Luau.Heap where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (Maybe; just)
|
||||
open import FFI.Data.Vector using (Vector; length; snoc)
|
||||
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; nil; addr; function⟨_⟩_end)
|
||||
|
||||
data HeapValue : Set where
|
||||
function⟨_⟩_end : Var → Block → HeapValue
|
||||
function_⟨_⟩_end : Var → Var → Block → HeapValue
|
||||
|
||||
Heap = Vector HeapValue
|
||||
|
||||
|
|
@ -22,10 +23,26 @@ lookup : Heap → Addr → Maybe HeapValue
|
|||
lookup = FFI.Data.Vector.lookup
|
||||
|
||||
emp : Heap
|
||||
emp = FFI.Data.Vector.empty
|
||||
emp = empty
|
||||
|
||||
data AllocResult (H : Heap) (V : HeapValue) : Set where
|
||||
ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
|
||||
|
||||
alloc : ∀ H V → AllocResult H V
|
||||
alloc H V = ok (length H) (snoc H V) defn
|
||||
|
||||
next : Heap → Addr
|
||||
next = length
|
||||
|
||||
allocated : Heap → HeapValue → Heap
|
||||
allocated = snoc
|
||||
|
||||
-- next-emp : (length empty ≡ 0)
|
||||
next-emp = FFI.Data.Vector.length-empty
|
||||
|
||||
-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
|
||||
lookup-next = FFI.Data.Vector.lookup-snoc
|
||||
|
||||
-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
|
||||
lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty
|
||||
|
||||
|
|
|
|||
|
|
@ -2,9 +2,9 @@ module Luau.OpSem where
|
|||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Maybe using (just)
|
||||
open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function⟨_⟩_end)
|
||||
open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function_⟨_⟩_end)
|
||||
open import Luau.Substitution using (_[_/_]ᴮ)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
|
||||
open import Luau.Value using (addr; val)
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
|
||||
|
|
@ -19,7 +19,7 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
|
||||
function : ∀ {H H′ a x B} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ B end) →
|
||||
H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
|
||||
-------------------------------------------
|
||||
H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
|
||||
|
||||
|
|
@ -29,27 +29,27 @@ data _⊢_⟶ᴱ_⊣_ where
|
|||
-----------------------------
|
||||
H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
|
||||
|
||||
beta : ∀ {H M a x B} →
|
||||
beta : ∀ {H M a f x B} →
|
||||
|
||||
(lookup H a) ≡ just(function⟨ x ⟩ B end) →
|
||||
(lookup H a) ≡ just(function f ⟨ x ⟩ B end) →
|
||||
-----------------------------------------------------
|
||||
H ⊢ (addr a $ M) ⟶ᴱ (block local x ← M ∙ B end) ⊣ H
|
||||
H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H
|
||||
|
||||
block : ∀ {H H′ B B′} →
|
||||
block : ∀ {H H′ B B′ b} →
|
||||
|
||||
H ⊢ B ⟶ᴮ B′ ⊣ H′ →
|
||||
------------------------------------------
|
||||
H ⊢ (block B end) ⟶ᴱ (block B′ end) ⊣ H′
|
||||
----------------------------------------------------
|
||||
H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′
|
||||
|
||||
return : ∀ {H V B} →
|
||||
return : ∀ {H V B b} →
|
||||
|
||||
---------------------------------------------------
|
||||
H ⊢ (block return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H
|
||||
--------------------------------------------------------
|
||||
H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H
|
||||
|
||||
done : ∀ {H} →
|
||||
done : ∀ {H b} →
|
||||
|
||||
---------------------------------
|
||||
H ⊢ (block done end) ⟶ᴱ nil ⊣ H
|
||||
H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
|
||||
|
||||
data _⊢_⟶ᴮ_⊣_ where
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ data _⊢_⟶ᴮ_⊣_ where
|
|||
|
||||
function : ∀ {H H′ a f x B C} →
|
||||
|
||||
H′ ≡ H ⊕ a ↦ (function⟨ x ⟩ C end) →
|
||||
H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
|
||||
--------------------------------------------------------------
|
||||
H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
|
||||
|
||||
|
|
@ -76,3 +76,17 @@ data _⊢_⟶ᴮ_⊣_ where
|
|||
--------------------------------------------
|
||||
H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
|
||||
|
||||
data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → Set where
|
||||
|
||||
refl : ∀ {H B} →
|
||||
|
||||
----------------
|
||||
H ⊢ B ⟶* B ⊣ H
|
||||
|
||||
step : ∀ {H H′ H″ B B′ B″} →
|
||||
H ⊢ B ⟶ᴮ B′ ⊣ H′ →
|
||||
H′ ⊢ B′ ⟶* B″ ⊣ H″ →
|
||||
------------------
|
||||
H ⊢ B ⟶* B″ ⊣ H″
|
||||
|
||||
|
||||
|
|
|
|||
28
prototyping/Luau/Run.agda
Normal file
28
prototyping/Luau/Run.agda
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
module Luau.Run where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import Luau.Heap using (Heap; emp)
|
||||
open import Luau.Syntax using (Block; return; _∙_; done)
|
||||
open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
|
||||
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
|
||||
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′ 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′)
|
||||
run′ H B | step H′ B′ D | done D′ = done (step D D′)
|
||||
run′ H B | step H′ B′ D | error E D′ = error E (step D D′)
|
||||
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 emp B
|
||||
run = run′ emp
|
||||
21
prototyping/Luau/RuntimeError.agda
Normal file
21
prototyping/Luau/RuntimeError.agda
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
module Luau.RuntimeError where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import Luau.Heap using (Heap; lookup)
|
||||
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; _∙_)
|
||||
|
||||
data RuntimeErrorᴮ (H : Heap) : Block → Set
|
||||
data RuntimeErrorᴱ (H : Heap) : Expr → Set
|
||||
|
||||
data RuntimeErrorᴱ H where
|
||||
NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
|
||||
UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
|
||||
SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
|
||||
app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
|
||||
block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
|
||||
|
||||
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)
|
||||
|
||||
18
prototyping/Luau/RuntimeError/ToString.agda
Normal file
18
prototyping/Luau/RuntimeError/ToString.agda
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
module Luau.RuntimeError.ToString where
|
||||
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Var.ToString using (varToString)
|
||||
|
||||
errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
|
||||
errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ 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ᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b
|
||||
|
||||
errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString x
|
||||
errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement"
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
module Luau.Substitution where
|
||||
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
|
||||
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
|
||||
open import Luau.Value using (Value; val)
|
||||
open import Luau.Var using (Var; _≡ⱽ_)
|
||||
open import Properties.Dec using (Dec; yes; no)
|
||||
|
|
@ -15,7 +15,7 @@ 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 ≡ⱽ y) end
|
||||
block C end [ v / x ]ᴱ = block C [ v / x ]ᴮ 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 ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
|
||||
(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y))
|
||||
|
|
|
|||
|
|
@ -24,4 +24,4 @@ data Expr where
|
|||
addr : Addr → Expr
|
||||
_$_ : Expr → Expr → Expr
|
||||
function⟨_⟩_end : Var → Block → Expr
|
||||
block_end : Block → Expr
|
||||
block_is_end : Var → Block → Expr
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
module Luau.Syntax.ToString where
|
||||
|
||||
open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_end)
|
||||
open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
|
||||
open import FFI.Data.String using (String; _++_)
|
||||
open import Luau.Addr using (addrToString)
|
||||
open import Luau.Var using (varToString)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
open import Luau.Var.ToString using (varToString)
|
||||
|
||||
exprToString′ : String → Expr → String
|
||||
statToString′ : String → Stat → String
|
||||
|
|
@ -21,8 +21,8 @@ exprToString′ lb (function⟨ x ⟩ B end) =
|
|||
"function(" ++ x ++ ")" ++ lb ++
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end"
|
||||
exprToString′ lb (block B end) =
|
||||
"(function()" ++ lb ++
|
||||
exprToString′ lb (block b is B end) =
|
||||
"(function " ++ b ++ "()" ++ lb ++
|
||||
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
|
||||
"end)()"
|
||||
|
||||
|
|
|
|||
10
prototyping/Luau/Value/ToString.agda
Normal file
10
prototyping/Luau/Value/ToString.agda
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
module Luau.Value.ToString where
|
||||
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Luau.Value using (Value; nil; addr)
|
||||
open import Luau.Addr.ToString using (addrToString)
|
||||
|
||||
valueToString : Value → String
|
||||
valueToString nil = "nil"
|
||||
valueToString (addr a) = addrToString a
|
||||
|
||||
|
|
@ -9,9 +9,6 @@ open import Properties.Dec using (Dec; yes; no; ⊥)
|
|||
Var : Set
|
||||
Var = String
|
||||
|
||||
varToString : Var → String
|
||||
varToString x = x
|
||||
|
||||
_≡ⱽ_ : (a b : Var) → Dec (a ≡ b)
|
||||
a ≡ⱽ b with primStringEquality a b
|
||||
a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥
|
||||
|
|
|
|||
8
prototyping/Luau/Var/ToString.agda
Normal file
8
prototyping/Luau/Var/ToString.agda
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
module Luau.Var.ToString where
|
||||
|
||||
open import Agda.Builtin.String using (String)
|
||||
open import Luau.Var using (Var)
|
||||
|
||||
varToString : Var → String
|
||||
varToString x = x
|
||||
|
||||
|
|
@ -2,27 +2,14 @@ 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; lookup; alloc; ok; function⟨_⟩_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
|
||||
open import Luau.Heap using (Heap; lookup; alloc; ok; function_⟨_⟩_end)
|
||||
open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
|
||||
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 RuntimeErrorᴮ (H : Heap) : Block → Set
|
||||
data RuntimeErrorᴱ (H : Heap) : Expr → Set
|
||||
|
||||
data RuntimeErrorᴱ H where
|
||||
NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
|
||||
UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
|
||||
SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
|
||||
app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
|
||||
block : ∀ {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block B end)
|
||||
|
||||
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)
|
||||
|
||||
data StepResultᴮ (H : Heap) (B : Block) : Set
|
||||
data StepResultᴱ (H : Heap) (M : Expr) : Set
|
||||
|
||||
|
|
@ -48,22 +35,22 @@ 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 (lookup 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⟨ x ⟩ B end) , p) = step H (block local x ← N ∙ B end) (beta 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 (M $ N) | error E = error (app E)
|
||||
stepᴱ H (function⟨ x ⟩ B end) with alloc H (function⟨ x ⟩ B end)
|
||||
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 end) with stepᴮ H B
|
||||
stepᴱ H (block B end) | step H′ B′ D = step H′ (block B′ end) (block D)
|
||||
stepᴱ H (block (return _ ∙ B′) end) | return V refl = step H (val V) return
|
||||
stepᴱ H (block done end) | done refl = step H nil done
|
||||
stepᴱ H (block B end) | error E = error (block 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
|
||||
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 ⟨ x ⟩ C end ∙ B) with alloc H (function⟨ x ⟩ C end)
|
||||
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 (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 / x ]ᴮ) subst
|
||||
stepᴮ H (local x ← M ∙ B) | error E = error (local E)
|
||||
stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
|
||||
stepᴮ H (return M ∙ B) with stepᴱ H M
|
||||
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
|
||||
stepᴮ H (return _ ∙ B) | value V refl = return V refl
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue