From 8573eeda4942f3266f1b240168111dec7928f1e1 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 9 Feb 2022 14:23:25 -0600 Subject: [PATCH] First draft interpreter --- prototyping/Examples.agda | 2 + prototyping/Examples/OpSem.agda | 4 +- prototyping/Examples/Run.agda | 18 +++++++++ prototyping/Examples/SmokeTest.lua | 3 +- prototyping/FFI/Data/Vector.agda | 21 +++++----- prototyping/Interpreter.agda | 39 ++++++++++++++++++ prototyping/Luau/Addr.agda | 4 -- prototyping/Luau/Addr/ToString.agda | 8 ++++ prototyping/Luau/Heap.agda | 23 +++++++++-- prototyping/Luau/OpSem.agda | 44 ++++++++++++++------- prototyping/Luau/Run.agda | 28 +++++++++++++ prototyping/Luau/RuntimeError.agda | 21 ++++++++++ prototyping/Luau/RuntimeError/ToString.agda | 18 +++++++++ prototyping/Luau/Substitution.agda | 4 +- prototyping/Luau/Syntax.agda | 2 +- prototyping/Luau/Syntax/ToString.agda | 10 ++--- prototyping/Luau/Value/ToString.agda | 10 +++++ prototyping/Luau/Var.agda | 3 -- prototyping/Luau/Var/ToString.agda | 8 ++++ prototyping/Properties/Step.agda | 37 ++++++----------- 20 files changed, 234 insertions(+), 73 deletions(-) create mode 100644 prototyping/Examples/Run.agda create mode 100644 prototyping/Interpreter.agda create mode 100644 prototyping/Luau/Addr/ToString.agda create mode 100644 prototyping/Luau/Run.agda create mode 100644 prototyping/Luau/RuntimeError.agda create mode 100644 prototyping/Luau/RuntimeError/ToString.agda create mode 100644 prototyping/Luau/Value/ToString.agda create mode 100644 prototyping/Luau/Var/ToString.agda diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda index 291d39b4..fe396eff 100644 --- a/prototyping/Examples.agda +++ b/prototyping/Examples.agda @@ -1,5 +1,7 @@ +{-# OPTIONS --rewriting #-} module Examples where import Examples.Syntax import Examples.OpSem +import Examples.Run diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index e5a1f0cf..a8d11080 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -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 diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda new file mode 100644 index 00000000..573c1d06 --- /dev/null +++ b/prototyping/Examples/Run.agda @@ -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 diff --git a/prototyping/Examples/SmokeTest.lua b/prototyping/Examples/SmokeTest.lua index b1b91e19..5ea8e592 100644 --- a/prototyping/Examples/SmokeTest.lua +++ b/prototyping/Examples/SmokeTest.lua @@ -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) \ No newline at end of file diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 0b49c786..2c5d1925 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -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)) diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda new file mode 100644 index 00000000..9184235e --- /dev/null +++ b/prototyping/Interpreter.agda @@ -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 + diff --git a/prototyping/Luau/Addr.agda b/prototyping/Luau/Addr.agda index f1497f23..c1978047 100644 --- a/prototyping/Luau/Addr.agda +++ b/prototyping/Luau/Addr.agda @@ -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) → ⊥ diff --git a/prototyping/Luau/Addr/ToString.agda b/prototyping/Luau/Addr/ToString.agda new file mode 100644 index 00000000..2fc38335 --- /dev/null +++ b/prototyping/Luau/Addr/ToString.agda @@ -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)) diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index 2c90c18e..1a0416e4 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -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 + diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 3b6ee22e..dcd474bf 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -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″ + + diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda new file mode 100644 index 00000000..29709ceb --- /dev/null +++ b/prototyping/Luau/Run.agda @@ -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 diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda new file mode 100644 index 00000000..86e7cf21 --- /dev/null +++ b/prototyping/Luau/RuntimeError.agda @@ -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) + diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda new file mode 100644 index 00000000..f11756f7 --- /dev/null +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -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" diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index a30b7f70..1a361174 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -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)) diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index eed15b65..3fe05bc8 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -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 diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 59a15c64..afec0935 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -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)()" diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda new file mode 100644 index 00000000..3cac3ee7 --- /dev/null +++ b/prototyping/Luau/Value/ToString.agda @@ -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 + diff --git a/prototyping/Luau/Var.agda b/prototyping/Luau/Var.agda index 03d37496..091ce125 100644 --- a/prototyping/Luau/Var.agda +++ b/prototyping/Luau/Var.agda @@ -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) → ⊥ diff --git a/prototyping/Luau/Var/ToString.agda b/prototyping/Luau/Var/ToString.agda new file mode 100644 index 00000000..10cd915b --- /dev/null +++ b/prototyping/Luau/Var/ToString.agda @@ -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 + diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 9de4ea48..0eddd9fe 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -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