From 53b5251c0a6eb54c032fc9221cde925868b02c7e Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 10 Feb 2022 16:53:59 -0600 Subject: [PATCH] Complete (I hope) defn of typechecking derivation trees --- prototyping/Examples/OpSem.agda | 4 +- prototyping/Examples/Run.agda | 2 +- prototyping/FFI/Data/Aeson.agda | 10 +++ prototyping/Luau/AddrCtxt.agda | 15 ++++ prototyping/Luau/Heap.agda | 8 +- prototyping/Luau/OpSem.agda | 4 +- prototyping/Luau/Run.agda | 6 +- prototyping/Luau/RuntimeError.agda | 4 +- prototyping/Luau/TypeCheck.agda | 113 +++++++++++++++++++++-------- prototyping/Luau/VarCtxt.agda | 31 ++++++++ prototyping/Properties.agda | 1 + prototyping/Properties/Step.agda | 4 +- 12 files changed, 154 insertions(+), 48 deletions(-) create mode 100644 prototyping/Luau/AddrCtxt.agda create mode 100644 prototyping/Luau/VarCtxt.agda diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index 4b8c2d6d..a69da4c4 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -2,8 +2,8 @@ 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.Heap using (emp) +open import Luau.Heap using (∅) -ex1 : emp ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp +ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅ ex1 = subst diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 90a56a09..fe0f7f23 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -6,7 +6,7 @@ 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) +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 #-} diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index a9082d31..684f2177 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -19,12 +19,22 @@ postulate Key : Set fromString : String → Key toString : Key → String + empty : ∀ {A} → KeyMap A + singleton : ∀ {A} → Key → A → (KeyMap A) + insert : ∀ {A} → Key → A → (KeyMap A) → (KeyMap A) + delete : ∀ {A} → Key → (KeyMap A) → (KeyMap A) + unionWith : ∀ {A} → (A → A → A) → (KeyMap A) → (KeyMap A) → (KeyMap A) lookup : ∀ {A} → Key -> KeyMap A -> Maybe A {-# POLARITY KeyMap ++ #-} {-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-} {-# COMPILE GHC Key = type Data.Aeson.Key.Key #-} {-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-} {-# COMPILE GHC toString = Data.Aeson.Key.toText #-} +{-# COMPILE GHC empty = \_ -> Data.Aeson.KeyMap.empty #-} +{-# COMPILE GHC singleton = \_ -> Data.Aeson.KeyMap.singleton #-} +{-# COMPILE GHC insert = \_ -> Data.Aeson.KeyMap.insert #-} +{-# COMPILE GHC delete = \_ -> Data.Aeson.KeyMap.delete #-} +{-# COMPILE GHC unionWith = \_ -> Data.Aeson.KeyMap.unionWith #-} {-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-} data Value : Set where diff --git a/prototyping/Luau/AddrCtxt.agda b/prototyping/Luau/AddrCtxt.agda new file mode 100644 index 00000000..b19e784e --- /dev/null +++ b/prototyping/Luau/AddrCtxt.agda @@ -0,0 +1,15 @@ +module Luau.AddrCtxt where + +open import Luau.Type using (Type) +open import Luau.Addr using (Addr) +open import FFI.Data.Vector using (Vector; empty; lookup) +open import FFI.Data.Maybe using (Maybe; just; nothing) + +AddrCtxt : Set +AddrCtxt = Vector Type + +∅ : AddrCtxt +∅ = empty + +_[_] : AddrCtxt → Addr → Maybe Type +_[_] = lookup diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index eeb90c97..f10e6a24 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -19,11 +19,11 @@ data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where ----------------------------------- (snoc H val) ≡ H ⊕ (length H) ↦ val -lookup : Heap → Addr → Maybe HeapValue -lookup = FFI.Data.Vector.lookup +_[_] : Heap → Addr → Maybe HeapValue +_[_] = FFI.Data.Vector.lookup -emp : Heap -emp = empty +∅ : Heap +∅ = empty data AllocResult (H : Heap) (V : HeapValue) : Set where ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 5b2b5729..0339c0d1 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -2,7 +2,7 @@ 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; _≡_⊕_↦_; _[_]; 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; name) open import Luau.Value using (addr; val) @@ -31,7 +31,7 @@ data _⊢_⟶ᴱ_⊣_ where beta : ∀ {H M a f x B} → - (lookup H a) ≡ just(function f ⟨ x ⟩ B end) → + H [ a ] ≡ just(function f ⟨ x ⟩ B end) → ----------------------------------------------------- H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda index 29709ceb..166f5e64 100644 --- a/prototyping/Luau/Run.agda +++ b/prototyping/Luau/Run.agda @@ -1,7 +1,7 @@ module Luau.Run where open import Agda.Builtin.Equality using (_≡_; refl) -open import Luau.Heap using (Heap; emp) +open import Luau.Heap using (Heap; ∅) open import Luau.Syntax using (Block; return; _∙_; done) open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step) open import Luau.Value using (val) @@ -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 emp B -run = run′ emp +run : ∀ B → RunResult ∅ B +run = run′ ∅ diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 86e7cf21..a3bf4c40 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -1,7 +1,7 @@ module Luau.RuntimeError where open import Agda.Builtin.Equality using (_≡_) -open import Luau.Heap using (Heap; lookup) +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; _∙_) @@ -11,7 +11,7 @@ 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) + SEGV : ∀ a → (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) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index e7d8d7cd..a7314950 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -2,49 +2,98 @@ 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.Syntax using (Expr; Stat; Block; nil; addr; var; var_∈_; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; 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.Value using (addr; val) -open import Luau.Type using (Type; nil; _⇒_; src; tgt) -open import FFI.Data.Aeson using (KeyMap; Key) +open import Luau.Type using (Type; nil; any; _⇒_; src; tgt) +open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) +open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) +open import FFI.Data.Vector using (Vector) +open import FFI.Data.Maybe using (Maybe; just; nothing) -Context : Set -Context = KeyMap Type +data _▷_⊢ᴮ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Block → Type → VarCtxt → Set +data _▷_⊢ᴱ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Expr → Type → VarCtxt → Set -∅ : Context -∅ = {!!} +data _▷_⊢ᴮ_∋_∈_⊣_ where -_⋒_ : 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 Γ} → + done : ∀ {Σ S Γ} → ---------------------- - Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ + Σ ▷ Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ - var : ∀ x {S T Γ} → + return : ∀ {Σ M B S T Γ Δ} → - just T ≡ lookup Γ x → + Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ → + --------------------------------- + Σ ▷ Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ + + local : ∀ {Σ x M B S T U V Γ Δ₁ Δ₂} → + + Σ ▷ Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → + Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → + ---------------------------------------------------------- + Σ ▷ Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) + + function : ∀ {Σ f x B C S T U V Γ Δ₁ Δ₂} → + + Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ any ∋ C ∈ U ⊣ Δ₁ → + Σ ▷ (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → + --------------------------------------------------------------------------- + Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩ C end ∙ B ∈ V ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) + +data _▷_⊢ᴱ_∋_∈_⊣_ where + + nil : ∀ {Σ S Γ} → + + ---------------------- + Σ ▷ Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ + + var : ∀ x {Σ S T Γ} → + + just T ≡ Γ [ x ]ⱽ → ---------------------------- - Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ T) + Σ ▷ Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) - app : ∀ {M N S T U Γ Δ₁ Δ₂} → + addr : ∀ a {Σ S T Γ} → - Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ U ⊣ Δ₂ → - Γ ⊢ᴱ (src S) ∋ N ∈ U ⊣ Δ₂ → + just T ≡ Σ [ a ]ᴬ → + ---------------------------- + Σ ▷ Γ ⊢ᴱ S ∋ addr a ∈ T ⊣ ∅ + + app : ∀ {Σ M N S T U Γ Δ₁ Δ₂} → + + Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₂ → + Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → -------------------------------------- - Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) + Σ ▷ Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) + function : ∀ {Σ x B S T U Γ Δ} → + + Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ any ∋ B ∈ U ⊣ Δ → + -------------------------------------------------------------- + Σ ▷ Γ ⊢ᴱ S ∋ (function⟨ var x ∈ T ⟩ B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) + + block : ∀ {Σ b B S T Γ Δ} → + + Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → + ---------------------------------------------------- + Σ ▷ Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ + +data _▷_∈_ (Σ : AddrCtxt) : (Maybe HeapValue) → (Maybe Type) → Set where + + nothing : + + --------------------- + Σ ▷ nothing ∈ nothing + + function : ∀ {f x B T} → + + Σ ▷ ∅ ⊢ᴱ any ∋ (function⟨ x ⟩ B end) ∈ T ⊣ ∅ → + ------------------------------------------------ + Σ ▷ just (function f ⟨ x ⟩ B end) ∈ just T + +data _▷_✓ (Σ : AddrCtxt) (H : Heap) : Set where + + defn : (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) → (Σ ▷ H ✓) diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda new file mode 100644 index 00000000..ab170d3a --- /dev/null +++ b/prototyping/Luau/VarCtxt.agda @@ -0,0 +1,31 @@ +module Luau.VarCtxt where + +open import Luau.Type using (Type; _∪_; _∩_) +open import Luau.Var using (Var) +open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; fromString) +open import FFI.Data.Maybe using (Maybe; just; nothing) + +VarCtxt : Set +VarCtxt = KeyMap Type + +∅ : VarCtxt +∅ = empty + +_⋒_ : VarCtxt → VarCtxt → VarCtxt +_⋒_ = unionWith _∩_ + +_⋓_ : VarCtxt → VarCtxt → VarCtxt +_⋓_ = unionWith _∪_ + +_[_] : VarCtxt → Var → Maybe Type +_[_] Γ x = lookup (fromString x) Γ + +_⊝_ : VarCtxt → Var → VarCtxt +Γ ⊝ x = delete (fromString x) Γ + +_↦_ : Var → Type → VarCtxt +x ↦ T = singleton (fromString x) T + +_⊕_↦_ : VarCtxt → Var → Type → VarCtxt +Γ ⊕ x ↦ T = insert (fromString x) T Γ + diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index a8b59f30..6f7d4659 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -3,3 +3,4 @@ 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 b35727bb..818ef014 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -2,7 +2,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.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.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst) open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) @@ -33,7 +33,7 @@ stepᴱ H (addr a) = value (addr a) refl stepᴱ H (M $ N) with stepᴱ H M 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 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 (M $ N) | error E = error (app E)