Started on typechecking

prototyping/Examples/OpSem.agda

@@ -1,11 +1,11 @@
 module Examples.OpSem where
 
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
-open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_end)
+open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_is_end; untyped)
 open import Luau.Heap using (emp)
 
 x = var "x"
 
-ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
+ex1 : emp ⊢ (local (untyped "x") ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
 ex1 = subst
 

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_⟨_⟩_end; return; _∙_; done; untyped)
 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)
@@ -14,5 +14,5 @@ import Agda.Builtin.Equality.Rewrite
 x = var "x"
 id = var "id"
 
-ex1 : (run emp (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
+ex1 : (run (function "id" ⟨ untyped "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
 ex1 = refl

prototyping/Examples/Syntax.agda

@@ -2,7 +2,7 @@ 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_⟨_⟩_end; done; _∙_; untyped)
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
 f = var "f"
@@ -16,7 +16,7 @@ ex2 : blockToString(return nil ∙ done) ≡
   "return nil"
 ex2 = refl
 
-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
+ex3 : blockToString(function "f" ⟨ untyped "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
   "local function f(x)\n" ++
   "  return x\n" ++
   "end\n" ++

prototyping/Luau/Heap.agda

@@ -5,10 +5,10 @@ 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; nil; addr; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; VarDec; nil; addr; function⟨_⟩_end)
 
 data HeapValue : Set where
-  function_⟨_⟩_end : Var → Var → Block → HeapValue
+  function_⟨_⟩_end : Var → VarDec → Block → HeapValue
 
 Heap = Vector HeapValue
 

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; _≡_⊕_↦_; lookup; function_⟨_⟩_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)
+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.Value using (addr; val)
 
 data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
@@ -61,8 +61,8 @@ data _⊢_⟶ᴮ_⊣_  where
 
   subst : ∀ {H x v B} →
   
-    -------------------------------------------------
-    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
+    ------------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H
 
   function : ∀ {H H′ a f x B C} →
   

prototyping/Luau/RuntimeError/ToString.agda

@@ -4,6 +4,7 @@ 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)
+open import Luau.Syntax using (name)
 
 errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
 errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String
@@ -14,5 +15,5 @@ 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ᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"

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_is_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; name)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -14,11 +14,11 @@ 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 ≡ⱽ y) end
+function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ name y) 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))
+(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))
+(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
 

prototyping/Luau/Syntax.agda

@@ -2,9 +2,18 @@ module Luau.Syntax where
 
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
+open import Luau.Type using (Type)
 
 infixr 5 _∙_
 
+data VarDec : Set where
+  untyped : Var → VarDec
+  typed_∈_ : Var → Type → VarDec
+
+name : VarDec → Var
+name (untyped x) = x
+name (typed x ∈ T) = x
+
 data Block : Set
 data Stat : Set
 data Expr : Set
@@ -14,8 +23,8 @@ data Block where
   done : Block
 
 data Stat where
-  function_⟨_⟩_end : Var → Var → Block → Stat
-  local_←_ : Var → Expr → Stat
+  function_⟨_⟩_end : Var → VarDec → Block → Stat
+  local_←_ : VarDec → Expr → Stat
   return : Expr → Stat
 
 data Expr where
@@ -23,5 +32,6 @@ data Expr where
   var : Var → Expr
   addr : Addr → Expr
   _$_ : Expr → Expr → Expr
-  function⟨_⟩_end : Var → Block → Expr
+  function⟨_⟩_end : VarDec → Block → Expr
   block_is_end : Var → Block → Expr
+

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⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_; untyped)
 
 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⟨ x ⟩ B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function⟨ untyped x ⟩ 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
@@ -78,7 +78,7 @@ statFromObject obj with lookup type obj
 statFromObject obj | just(string "AstStatLocal") with lookup vars obj | lookup values obj
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) with head(arr1) | head(arr2)
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) with exprFromJSON(value)
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local x ← M)
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local untyped x ← M)
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Left err = Left err
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | nothing = Left "AstStatLocal empty values"
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(_) | _ = Left "AstStatLocal vars not a string array"

prototyping/Luau/Syntax/ToString.agda

@@ -1,10 +1,15 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end; typed_∈_; untyped)
 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 (untyped x) = varToString x
+varDecToString (typed x ∈ T) =  varToString x ++ " : " ++ typeToString T
+
 exprToString′ : String → Expr → String
 statToString′ : String → Stat → String
 blockToString′ : String → Block → String
@@ -18,7 +23,7 @@ exprToString′ lb (var x) =
 exprToString′ lb (M $ N) =
   (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
 exprToString′ lb (function⟨ x ⟩ B end) =
-  "function(" ++ x ++ ")" ++ lb ++
+  "function(" ++ varDecToString x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 exprToString′ lb (block b is B end) =
@@ -27,11 +32,11 @@ exprToString′ lb (block b is B end) =
   "end)()"
 
 statToString′ lb (function f ⟨ x ⟩ B end) =
-  "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
+  "local function " ++ f ++ "(" ++ varDecToString x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 statToString′ lb (local x ← M) =
-  "local " ++ x ++ " = " ++ (exprToString′ lb M)
+  "local " ++ varDecToString x ++ " = " ++ (exprToString′ lb M)
 statToString′ lb (return M) =
   "return " ++ (exprToString′ lb M)
 

prototyping/Luau/Type.agda

@@ -8,3 +8,18 @@ data Type : Set where
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
+src : Type → Type
+src nil = none
+src (S ⇒ T) = S
+src none = none
+src any = any
+src (S ∪ T) = (src S) ∪ (src T)
+src (S ∩ T) = (src S) ∩ (src T)
+
+tgt : Type → Type
+tgt nil = none
+tgt (S ⇒ T) = T
+tgt none = none
+tgt any = any
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)

prototyping/Luau/Type/ToString.agda

@@ -0,0 +1,13 @@
+module Luau.Type.ToString where
+
+open import FFI.Data.String using (String; _++_)
+open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_)
+
+typeToString : Type → String
+typeToString nil = "nil"
+typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
+typeToString none = "none"
+typeToString any = "any"
+typeToString (S ∪ T) = (typeToString S) ++ " | " ++ (typeToString T)
+typeToString (S ∩ T) = (typeToString S) ++ " & " ++ (typeToString T)
+

prototyping/Luau/TypeCheck.agda

@@ -0,0 +1,50 @@
+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; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return; name)
+open import Luau.Var using (Var)
+open import Luau.Value using (addr; val)
+open import Luau.Type using (Type; nil; _⇒_; src; tgt)
+open import FFI.Data.Aeson using (KeyMap; Key)
+
+Context : Set
+Context = KeyMap Type
+
+∅ : Context
+∅ = {!!}
+
+_⋒_ : Context → Context → Context
+_⋒_ = {!!}
+
+lookup : Context → Var → Maybe Type
+lookup = {!!}
+
+_↦_ : Var → Type → Context
+_↦_ = {!!}
+
+data _⊢ᴮ_∋_∈_⊣_ : Context → Type → Block → Type → Context → Set
+data _⊢ᴱ_∋_∈_⊣_ : Context → Type → Expr → Type → Context → Set
+
+data _⊢ᴮ_∋_∈_⊣_ where
+
+data _⊢ᴱ_∋_∈_⊣_  where
+
+  nil : ∀ {S Γ} →
+
+    ----------------------
+    Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅
+
+  var : ∀ x {S T Γ} →
+
+    just T ≡ lookup Γ x →
+    ----------------------------
+    Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ T)
+
+  app : ∀ {M N S T U Γ Δ₁ Δ₂} →
+
+    Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ U ⊣ Δ₂ →
+    Γ ⊢ᴱ (src S) ∋ N ∈ U ⊣ Δ₂ →
+    --------------------------------------
+    Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂)
+

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; 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.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_; name)
 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 (_[_/_]ᴮ)
@@ -49,7 +49,7 @@ stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function f ⟨ x ⟩
 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 ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
 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)