From 6193fc8fc429efb77d89b05c72f253c43b58a52b Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 11 Feb 2022 10:43:33 -0600 Subject: [PATCH] Removed AnonFunDec --- prototyping/Examples/OpSem.agda | 2 +- prototyping/Examples/Syntax.agda | 4 ++-- prototyping/Luau/OpSem.agda | 4 ++-- prototyping/Luau/Substitution.agda | 4 ++-- prototyping/Luau/Syntax.agda | 10 +--------- prototyping/Luau/Syntax/FromJSON.agda | 6 +++--- prototyping/Luau/Syntax/ToString.agda | 8 ++------ prototyping/Properties/Step.agda | 4 ++-- 8 files changed, 15 insertions(+), 27 deletions(-) diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index 143bc45c..ec8bce7b 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 (Block; no; var; nil; local_←_; _∙_; done; return; block_is_end) +open import Luau.Syntax using (Block; 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/Syntax.agda b/prototyping/Examples/Syntax.agda index ea065884..73160ca0 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -2,10 +2,10 @@ 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_is_end; local_←_; done; _∙_; _⟨_⟩; anon⟨_⟩) +open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩) open import Luau.Syntax.ToString using (exprToString; blockToString) -ex1 : exprToString(function anon⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡ +ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡ "function (x)\n" ++ " return f(x)\n" ++ "end" diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index d325f03b..878b8bd0 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -4,7 +4,7 @@ open import Agda.Builtin.Equality using (_≡_) open import FFI.Data.Maybe using (just) open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end) open import Luau.Substitution using (_[_/_]ᴮ) -open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; namify) +open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg) open import Luau.Value using (addr; val) data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set @@ -19,7 +19,7 @@ data _⊢_⟶ᴱ_⊣_ where function : ∀ {H H′ a F B} → - H′ ≡ H ⊕ a ↦ (function (namify F) is B end) → + H′ ≡ H ⊕ a ↦ (function F is B end) → ------------------------------------------- H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′ diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index f22adb41..b956aeae 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_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; namify) +open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg) open import Luau.Value using (Value; val) open import Luau.Var using (Var; _≡ⱽ_) open import Properties.Dec using (Dec; yes; no) @@ -14,7 +14,7 @@ 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 F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg(namify F))) end +function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end (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)) diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index cdd7f648..3707e948 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -24,10 +24,6 @@ data FunDec : Annotated → Set where _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a _⟨_⟩ : Var → VarDec maybe → FunDec maybe -data AnonFunDec : Annotated → Set where - anon⟨_⟩∈_ : ∀ {a} → VarDec a → Type → AnonFunDec a - anon⟨_⟩ : VarDec maybe → AnonFunDec maybe - fun : ∀ {a} → FunDec a → Var fun (f ⟨ x ⟩∈ T) = f fun (f ⟨ x ⟩) = f @@ -36,10 +32,6 @@ 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 @@ -58,6 +50,6 @@ data Expr a where var : Var → Expr a addr : Addr → Expr a _$_ : Expr a → Expr a → Expr a - function_is_end : AnonFunDec a → Block a → Expr a + function_is_end : FunDec 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 f10a922d..b081d156 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_is_end; anon⟨_⟩; _⟨_⟩; local_←_; return; done; _∙_; maybe) +open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe) open import Agda.Builtin.List using (List; _∷_; []) @@ -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 anon⟨ var x ⟩ is B end) +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function "" ⟨ 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 anon⟨ x ⟩ is B end) = Right (function f ⟨ x ⟩ is B end) +statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function "" ⟨ 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 df43c166..8ab5eece 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -1,6 +1,6 @@ module Luau.Syntax.ToString where -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 Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_) open import FFI.Data.String using (String; _++_) open import Luau.Addr.ToString using (addrToString) open import Luau.Type.ToString using (typeToString) @@ -14,10 +14,6 @@ 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 @@ -31,7 +27,7 @@ exprToString′ lb (var x) = exprToString′ lb (M $ N) = (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")" exprToString′ lb (function F is B end) = - "function " ++ anonFunDecToString F ++ lb ++ + "function " ++ funDecToString F ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end" exprToString′ lb (block b is B end) = diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 86c6e55d..eeda4ef2 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -3,7 +3,7 @@ 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_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.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg) open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst) open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) open import Luau.Substitution using (_[_/_]ᴮ) @@ -42,7 +42,7 @@ stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end 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) with alloc H (function F is C end) stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p) stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)