From 1d66d8a3d338f450f78bd6cdf76d8213fbbbcde3 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 10 Feb 2022 20:11:59 -0600 Subject: [PATCH] Track untyped v typed syntax --- prototyping/Examples/OpSem.agda | 2 +- prototyping/Examples/Run.agda | 4 +- prototyping/Examples/Syntax.agda | 15 +++-- prototyping/Interpreter.agda | 2 +- prototyping/Luau/Heap.agda | 25 ++++---- prototyping/Luau/OpSem.agda | 28 ++++----- prototyping/Luau/Run.agda | 6 +- prototyping/Luau/RuntimeError.agda | 6 +- prototyping/Luau/RuntimeError/ToString.agda | 4 +- prototyping/Luau/Substitution.agda | 14 ++--- prototyping/Luau/Syntax.agda | 70 ++++++++++++++------- prototyping/Luau/Syntax/FromJSON.agda | 18 +++--- prototyping/Luau/Syntax/ToString.agda | 32 ++++++---- prototyping/Luau/TypeCheck.agda | 32 +++++----- prototyping/Luau/Value.agda | 4 +- prototyping/Luau/Var.agda | 2 + prototyping/PrettyPrinter.agda | 2 +- prototyping/Properties.agda | 1 - prototyping/Properties/Step.agda | 22 +++---- 19 files changed, 164 insertions(+), 125 deletions(-) diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index a69da4c4..143bc45c 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -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) ⊣ ∅ diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index fe0f7f23..88ca39b6 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -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 diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda index e1e3a403..ea065884 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -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" ++ diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index 9184235e..3ec5b8d1 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -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" diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index f10e6a24..a6333e3f 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -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) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 0339c0d1..d325f03b 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -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} → diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda index 166f5e64..d84f75de 100644 --- a/prototyping/Luau/Run.agda +++ b/prototyping/Luau/Run.agda @@ -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′ ∅ diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index a3bf4c40..e514dc9d 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -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) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index 6eeb0161..e8287157 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -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" diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index ff41a7a9..f22adb41 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -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 diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index af9eefa2..cdd7f648 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -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 diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index f09ea887..f10a922d 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -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" diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 8d533d31..df43c166 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -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" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index a7314950..8420bda8 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -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 ✓) diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda index 855e663e..4768f859 100644 --- a/prototyping/Luau/Value.agda +++ b/prototyping/Luau/Value.agda @@ -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 diff --git a/prototyping/Luau/Var.agda b/prototyping/Luau/Var.agda index 091ce125..a2096975 100644 --- a/prototyping/Luau/Var.agda +++ b/prototyping/Luau/Var.agda @@ -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)" diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda index dfb2c053..4a6c7dd6 100644 --- a/prototyping/PrettyPrinter.agda +++ b/prototyping/PrettyPrinter.agda @@ -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 ⊤ diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 6f7d4659..a8b59f30 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -3,4 +3,3 @@ module Properties where import Properties.Dec import Properties.Remember import Properties.Step -import Properties.TypeCheck diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 818ef014..86c6e55d 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -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