From 4b915fb4884e41754ea8d8a4c080a6a5c609f603 Mon Sep 17 00:00:00 2001
From: "ajeffrey@roblox.com" <ajeffrey@roblox.com>
Date: Tue, 31 May 2022 15:25:19 -0500
Subject: [PATCH] WIP

---
 prototyping/Luau/ResolveOverloads.agda | 85 ++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 prototyping/Luau/ResolveOverloads.agda

diff --git a/prototyping/Luau/ResolveOverloads.agda b/prototyping/Luau/ResolveOverloads.agda
new file mode 100644
index 00000000..0f35e6fe
--- /dev/null
+++ b/prototyping/Luau/ResolveOverloads.agda
@@ -0,0 +1,85 @@
+{-# OPTIONS --rewriting #-}
+
+module Luau.ResolveOverloads where
+
+open import FFI.Data.Either using (Left; Right)
+open import Luau.Subtyping using (_<:_; _≮:_; Language; witness; scalar; unknown; never; function-ok)
+open import Luau.Type using (Type ; _⇒_; _∩_; _∪_; unknown; never)
+open import Luau.TypeSaturation using (saturate)
+open import Luau.TypeNormalization using (normalize)
+open import Properties.Contradiction using (CONTRADICTION)
+open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right)
+open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
+open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)
+
+-- The domain of a normalized type
+srcⁿ : Type → Type
+srcⁿ (S ⇒ T) = S
+srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
+srcⁿ never = unknown
+srcⁿ T = never
+
+-- To get the domain of a type, we normalize it first We need to do
+-- this, since if we try to use it on non-normalized types, we get
+--
+-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
+-- src(never) = unknown
+--
+-- so src doesn't respect type equivalence.
+src : Type → Type
+src (S ⇒ T) = S
+src T = srcⁿ(normalize T)
+
+
+data ResolvedTo F G V : Set where
+
+  yes : ∀ Sʳ Tʳ →
+
+    Overloads F (Sʳ ⇒ Tʳ) →
+    (V <: Sʳ) → 
+    (∀ {S T} → Overloads G (S ⇒ T) → (V <: S) → (Tʳ <: T)) →
+    --------------------------------------------
+    ResolvedTo F G V
+
+  no :
+
+    (∀ {S T} → Overloads G (S ⇒ T) → (V ≮: S)) →
+    --------------------------------------------
+    ResolvedTo F G V
+
+Resolved : Type → Type → Set
+Resolved F V = ResolvedTo F F V
+
+target : ∀ {F V} → Resolved F V → Type
+target (yes _ T _ _ _) = T
+target (no _) = unknown
+
+resolveˢ : ∀ {F G V} → FunType G → Saturated F → Normal V → (G ⊆ᵒ F) → ResolvedTo F G V
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F with dec-subtypingⁿ Vⁿ Sⁿ
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Left V≮:S = no (λ { here → V≮:S })
+resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Right V<:S = yes _ _ (G⊆F here) V<:S (λ { here _ → <:-refl })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F with resolveˢ Gᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ left) | resolveˢ Hᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ right)
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ with sat-∩ o₁ o₂
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ | defn o p₁ p₂ =
+  yes _ _ o (<:-trans (<:-∩-glb V<:S₁ V<:S₂) p₁) (λ { (left o) p → <:-trans p₂ (<:-trans <:-∩-left (tgt₁ o p)) ; (right o) p → <:-trans p₂ (<:-trans <:-∩-right (tgt₂ o p)) })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | no src₂ =
+  yes _ _ o₁ V<:S₁ (λ { (left o) p → tgt₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (src₂ o)) })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ =
+  yes _ _ o₂ V<:S₂ (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (src₁ o)) ; (right o) p → tgt₂ o p })
+resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | no src₂ =
+  no (λ { (left o) → src₁ o ; (right o) → src₂ o })
+
+resolveᶠ : ∀ {F V} → FunType F → Normal V → Type
+resolveᶠ Fᶠ Vⁿ = target (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))
+
+resolveⁿ : ∀ {F V} → Normal F → Normal V → Type
+resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Vⁿ
+resolveⁿ (Fᶠ ∩ Gᶠ) Vⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Vⁿ
+resolveⁿ (Sⁿ ∪ Tˢ) Vⁿ = unknown
+resolveⁿ unknown Vⁿ = unknown
+resolveⁿ never Vⁿ = never
+
+resolve : Type → Type → Type
+resolve F V = resolveⁿ (normal F) (normal V)