Removed AnonFunDec

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) ⊣ ∅

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"

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′
 

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))

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
 

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"

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) =

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)