From a3866d544f3776bb85e40c317ba0510155612891 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 24 May 2022 19:26:00 -0500 Subject: [PATCH] WIP --- prototyping/Properties/DecSubtyping.agda | 42 ++++++++---- prototyping/Properties/ResolveOverloads.agda | 71 ++++++++++++-------- prototyping/Properties/StrictMode.agda | 15 ++--- prototyping/Properties/Subtyping.agda | 3 + prototyping/Properties/TypeSaturation.agda | 3 + 5 files changed, 85 insertions(+), 49 deletions(-) diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda index 31b12615..bf194930 100644 --- a/prototyping/Properties/DecSubtyping.agda +++ b/prototyping/Properties/DecSubtyping.agda @@ -13,7 +13,7 @@ open import Properties.Contradiction using (CONTRADICTION; ¬) open import Properties.Functions using (_∘_) open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub; ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-function-never; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp) open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; function-top) -open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate) +open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_) open import Properties.Equality using (_≢_) fun-function : ∀ {F} → FunType F → Language F function @@ -30,9 +30,10 @@ fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂ -- Honest this terminates, since saturation maintains the depth of nested arrows {-# TERMINATING #-} dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U) -dec-subtypingˢᶠ : ∀ {T U} → FunType T → Saturated T → FunType U → Either (T ≮: U) (T <: U) -dec-subtypingᶠ : ∀ {T U} → FunType T → FunType U → Either (T ≮: U) (T <: U) -dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U) +dec-subtypingˢᶠᵒ : ∀ {F S T} → FunType F → Saturated F → FunType (S ⇒ T) → (S ≮: never) → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T)) +dec-subtypingˢᶠ : ∀ {F G} → FunType F → Saturated F → FunType G → Either (F ≮: G) (F <: G) +dec-subtypingᶠ : ∀ {F G} → FunType F → FunType G → Either (F ≮: G) (F <: G) +dec-subtypingᶠⁿ : ∀ {F U} → FunType F → Normal U → Either (F ≮: U) (F <: U) dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U) dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U) @@ -40,13 +41,7 @@ dec-subtypingˢⁿ T U with dec-language _ (scalar T) dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p) dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p) -dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H -dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G) -dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H) -dec-subtypingˢᶠ F Fˢ (G ∩ H) | Right F<:G | Right F<:H = Right (<:-∩-glb F<:G F<:H) -dec-subtypingˢᶠ F (defn sat-∩ sat-∪) (S ⇒ T) with dec-subtypingⁿ S never -dec-subtypingˢᶠ F (defn sat-∩ sat-∪) (S ⇒ T) | Right S<:never = Right (<:-trans (function-top F) (<:-trans <:-function-never (<:-function S<:never <:-refl))) -dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) | Left (witness s₀ Ss₀ never) = result (top Fᶠ (λ o → o)) where +dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (witness s₀ Ss₀ never) = result (top Fᶠ (λ o → o)) where data Top G : Set where @@ -64,7 +59,7 @@ dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) | L top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ | defn n r r₁ = defn _ _ n (λ { (left o) → <:-trans (<:-trans (p₁ o) <:-∪-left) r ; (right o) → <:-trans (<:-trans (q₁ o) <:-∪-right) r }) - result : Top F → Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T)) + result : Top F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T)) result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ oᵗ) result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness s Ss ¬Sᵗs) = Left (witness (function-err s) (ov-language Fᶠ (λ o → function-err (<:-impl-⊇ (srcᵗ o) s ¬Sᵗs))) (function-err Ss)) result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where @@ -104,10 +99,10 @@ dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) | L ; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src) }) - result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T)) + result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T)) result₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-ok s₀ t) (ov-language Fᶠ (λ o → function-ok₂ (tgt₀ o t T₀t))) (function-ok Ss₀ ¬Tt)) result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ o₀) - result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right (ov-<: Fᶠ o₀ (<:-function S<:S₀ T₀<:T)) + result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right (defn o₀ S<:S₀ T₀<:T) result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where data SmallestTgt (G : Type) : Set where @@ -141,6 +136,16 @@ dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) | L lemma {S′} o | Left ¬S′s = function-ok₁ ¬S′s lemma {S′} o | Right S′s = function-ok₂ (tgt₁ o S′s t T₁t) +dec-subtypingˢᶠ F Fˢ (S ⇒ T) with dec-subtypingⁿ S never +dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Right S<:never = Right (<:-trans (function-top F) (<:-trans <:-function-never (<:-function S<:never <:-refl))) +dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never with dec-subtypingˢᶠᵒ F Fˢ (S ⇒ T) S≮:never +dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never | Left F≮:S⇒T = Left F≮:S⇒T +dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left S≮:never | Right F<:ᵒS⇒T = Right (<:ᵒ-impl-<: F F<:ᵒS⇒T) +dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H +dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G) +dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H) +dec-subtypingˢᶠ F Fˢ (G ∩ H) | Right F<:G | Right F<:H = Right (<:-∩-glb F<:G F<:H) + dec-subtypingᶠ F G with dec-subtypingˢᶠ (normal-saturate F) (saturated F) G dec-subtypingᶠ F G | Left H≮:G = Left (<:-trans-≮: (saturate-<: F) H≮:G) dec-subtypingᶠ F G | Right H<:G = Right (<:-trans (<:-saturate F) H<:G) @@ -176,3 +181,12 @@ dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q) dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U) dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U))) dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U))) + +-- As a corollary, for saturated functions +-- <:ᵒ coincides with <:, that is F is a subtype of (S ⇒ T) precisely +-- when one of its overloads is. + +<:-impl-<:ᵒ : ∀ {F S T} → FunType F → Saturated F → (S ≮: never) → (F <: (S ⇒ T)) → (F <:ᵒ (S ⇒ T)) +<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T with dec-subtypingˢᶠᵒ Fᶠ Fˢ (normal S ⇒ normal T) (<:-trans-≮: (<:-normalize S) S≮:never) +<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T | Left F≮:S⇒T = CONTRADICTION (<:-impl-¬≮: (<:-trans F<:S⇒T (<:-normalize (S ⇒ T))) F≮:S⇒T) +<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ S≮:never F<:S⇒T | Right F<:ᵒS⇒T = F<:ᵒS⇒T >>=ˡ <:-normalize S >>=ʳ normalize-<: T diff --git a/prototyping/Properties/ResolveOverloads.agda b/prototyping/Properties/ResolveOverloads.agda index 8c9bf204..82a9971f 100644 --- a/prototyping/Properties/ResolveOverloads.agda +++ b/prototyping/Properties/ResolveOverloads.agda @@ -3,15 +3,15 @@ module Properties.ResolveOverloads where open import FFI.Data.Either using (Left; Right) -open import Luau.Subtyping using (_<:_; _≮:_) +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 Properties.Contradiction using (CONTRADICTION) -open import Properties.DecSubtyping using (dec-subtypingⁿ) +open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ) open import Properties.Functions using (_∘_) -open import Properties.Subtyping using (<:-refl; <:-trans; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; function-≮:-never) -open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize) -open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; normal-saturate; saturated; defn; here; left; right) +open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∪-right; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function) +open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:) +open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right) data ResolvedTo F G R : Set where @@ -29,15 +29,13 @@ data ResolvedTo F G R : Set where -------------------------------------------- ResolvedTo F G R - never : - - (F <: never) → - -------------------------------------------- - ResolvedTo F G R - Resolved : Type → Type → Set Resolved F R = ResolvedTo F F R +target : ∀ {F R} → Resolved F R → Type +target (yes _ T _ _ _) = T +target (no _) = unknown + resolveˢ : ∀ {F G R} → FunType G → Saturated F → Normal R → (G ⊆ᵒ F) → ResolvedTo F G R resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Rⁿ G⊆F with dec-subtypingⁿ Rⁿ Sⁿ resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Rⁿ G⊆F | Left R≮:S = no (λ { here → R≮:S }) @@ -52,27 +50,46 @@ resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | no src₁ | yes S yes _ _ o₂ R<:S₂ (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (src₁ o)) ; (right o) p → tgt₂ o p }) resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | no src₁ | no src₂ = no (λ { (left o) → src₁ o ; (right o) → src₂ o }) -resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | _ | never q = never q -resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | never p | _ = never p resolveᶠ : ∀ {F R} → FunType F → Normal R → Resolved (saturate F) R resolveᶠ Fᶠ Rⁿ = resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Rⁿ (λ o → o) -resolveⁿ : ∀ {F R} → Normal F → Normal R → Resolved (saturate F) R -resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Rⁿ -resolveⁿ (Fᶠ ∩ Gᶠ) Rⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Rⁿ -resolveⁿ (Sⁿ ∪ Tˢ) Rⁿ = no (λ ()) -resolveⁿ never Rⁿ = never <:-refl -resolveⁿ unknown Rⁿ = no (λ ()) +resolveⁿ : ∀ {F R} → Normal F → Normal R → Type +resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = target (resolveᶠ (Sⁿ ⇒ Tⁿ) Rⁿ) +resolveⁿ (Fᶠ ∩ Gᶠ) Rⁿ = target (resolveᶠ (Fᶠ ∩ Gᶠ) Rⁿ) +resolveⁿ (Sⁿ ∪ Tˢ) Rⁿ = unknown +resolveⁿ unknown Rⁿ = unknown +resolveⁿ never Rⁿ = never resolve : Type → Type → Type -resolve F R with resolveⁿ (normal F) (normal R) -resolve F R | yes S T o R<:S p = T -resolve F R | no p = unknown -resolve F R | never p = never +resolve F R = resolveⁿ (normal F) (normal R) + +<:-target-⇒ : ∀ {R S T} → (r : Resolved (S ⇒ T) R) → (T <: target r) +<:-target-⇒ (yes Sʳ Tʳ here x₁ x₂) = <:-refl +<:-target-⇒ (no x) = <:-unknown + +<:-resolveⁿ : ∀ {R S T} → (Fⁿ : Normal (S ⇒ T)) → (Rⁿ : Normal R) → T <: resolveⁿ Fⁿ Rⁿ +<:-resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = <:-target-⇒ (resolveˢ (Sⁿ ⇒ Tⁿ) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o)) <:-resolve : ∀ {R S T} → T <: resolve (S ⇒ T) R -<:-resolve {R} {S} {T} with resolveⁿ (normal (S ⇒ T)) (normal R) -<:-resolve {R} {S} {T} | yes Sⁿ Tⁿ here Rⁿ<:Sʳ p = <:-normalize T -<:-resolve {R} {S} {T} | no p = <:-unknown -<:-resolve {R} {S} {T} | never p = CONTRADICTION (<:-impl-¬≮: p function-≮:-never) +<:-resolve {R} {S} {T} = <:-trans (<:-normalize T) (<:-resolveⁿ (normal (S ⇒ T)) (normal R)) + +resolveˢ-<:-⇒ : ∀ {F R U} → (FunType F) → (Saturated F) → (r : Resolved F R) → (R ≮: never) → (F <: (R ⇒ U)) → (target r <: U) +resolveˢ-<:-⇒ Fᶠ Fˢ r R≮:never F<:R⇒U with <:-impl-<:ᵒ Fᶠ Fˢ R≮:never F<:R⇒U +resolveˢ-<:-⇒ Fᶠ Fˢ (yes Sʳ Tʳ oʳ R<:Sʳ tgtʳ) R≮:never F<:R⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂ +resolveˢ-<:-⇒ Fᶠ Fˢ (no tgtʳ) R≮:never F<:R⇒U | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: o₁ (tgtʳ o)) + +resolveⁿ-<:-⇒ : ∀ {F R U} → (Fⁿ : Normal F) → (Rⁿ : Normal R) → (R ≮: never) → (F <: (R ⇒ U)) → (resolveⁿ Fⁿ Rⁿ <: U) +resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Rⁿ R≮:never F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o)) R≮:never F<:R⇒U +resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Rⁿ R≮:never F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Rⁿ (λ o → o)) R≮:never (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:R⇒U) +resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Rⁿ R≮:never F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ))) +resolveⁿ-<:-⇒ never Rⁿ R≮:never F<:R⇒U = <:-never +resolveⁿ-<:-⇒ unknown Rⁿ R≮:never F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U unknown-≮:-function) + +resolve-<:-⇒ : ∀ {F R U} → (R ≮: never) → (F <: (R ⇒ U)) → (resolve F R <: U) +resolve-<:-⇒ {F} {R} R≮:never F<:R⇒U = resolveⁿ-<:-⇒ (normal F) (normal R) (<:-trans-≮: (<:-normalize R) R≮:never) (<:-trans (normalize-<: F) (<:-trans F<:R⇒U (<:-function (normalize-<: R) <:-refl))) + +resolve-≮:-⇒ : ∀ {F R U} → (R ≮: never) → (resolve F R ≮: U) → (F ≮: (R ⇒ U)) +resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U with dec-subtyping F (R ⇒ U) +resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U | Left F≮:R⇒U = F≮:R⇒U +resolve-≮:-⇒ {F} {R} {U} R≮:never FR≮:U | Right F<:R⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ R≮:never F<:R⇒U) FR≮:U) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 53cbbaa7..fef7eaf6 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -9,7 +9,7 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ) open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr) open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) -open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) +open import Luau.Subtyping using (_<:_; _≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=) open import Luau.FunctionTypes using (src; tgt) open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; _≡ᵀ_; _≡ᴹᵀ_) @@ -26,7 +26,7 @@ open import Properties.Functions using (_∘_) open import Properties.DecSubtyping using (dec-subtyping) open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) open import Properties.FunctionTypes using (src-unknown-≮:; unknown-src-≮:) -open import Properties.ResolveOverloads using (resolve; <:-resolve) +open import Properties.ResolveOverloads using (resolve; <:-resolve; resolve-≮:-⇒) open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; <:-trans-≮:; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ) open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··) @@ -37,7 +37,6 @@ open import Luau.RuntimeType using (RuntimeType; valueType; number; string; bool postulate resolve⁻¹ : Type → Type → Type - resolve-≮:-⇒ : ∀ {F V U} → (resolve F V ≮: U) → (F ≮: (V ⇒ U)) ⇒-≮:-resolve : ∀ {F V U} → (F ≮: (V ⇒ U)) → (resolve F V ≮: U) ⇒-≮:-resolve⁻¹ : ∀ {F V U} → (F ≮: (V ⇒ U)) → (V ≮: resolve⁻¹ F U) resolve⁻¹-≮:-⇒ : ∀ {F V U} → (V ≮: resolve⁻¹ F U) → (F ≮: (V ⇒ U)) @@ -87,7 +86,7 @@ heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: heap-weakeningᴱ Γ H (val (number x)) h p = p heap-weakeningᴱ Γ H (val (bool x)) h p = p heap-weakeningᴱ Γ H (val (string x)) h p = p -heap-weakeningᴱ Γ H (M $ N) h p = ⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ Γ H N h (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ Γ H M h (resolve-≮:-⇒ p))))) +heap-weakeningᴱ Γ H (M $ N) h p = ⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ Γ H N h (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ Γ H M h (resolve-≮:-⇒ ? p))))) heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p heap-weakeningᴱ Γ H (binexp M op N) h p = p @@ -108,7 +107,7 @@ substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p substitutivityᴱ H (val w) v x p = Left p substitutivityᴱ H (binexp M op N) v x p = Left p -substitutivityᴱ H (M $ N) v x p with substitutivityᴱ H M v x (resolve-≮:-⇒ p) +substitutivityᴱ H (M $ N) v x p with substitutivityᴱ H M v x (resolve-≮:-⇒ ? p) substitutivityᴱ H (M $ N) v x p | Left q with substitutivityᴱ H N v x (⇒-≮:-resolve⁻¹ q) substitutivityᴱ H (M $ N) v x p | Left q | Left r = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ r)) substitutivityᴱ H (M $ N) v x p | Left q | Right r = Right r @@ -143,13 +142,13 @@ binOpPreservation H (·· v w) = refl reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M)) reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B)) -reflect-subtypingᴱ H (M $ N) (app₁ s) p with reflect-subtypingᴱ H M s (resolve-≮:-⇒ p) +reflect-subtypingᴱ H (M $ N) (app₁ s) p with reflect-subtypingᴱ H M s (resolve-≮:-⇒ ? p) reflect-subtypingᴱ H (M $ N) (app₁ s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) (⇒-≮:-resolve⁻¹ q)))) reflect-subtypingᴱ H (M $ N) (app₁ s) p | Right W = Right (app₁ W) -reflect-subtypingᴱ H (M $ N) (app₂ v s) p with reflect-subtypingᴱ H N s (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (resolve-≮:-⇒ p))) +reflect-subtypingᴱ H (M $ N) (app₂ v s) p with reflect-subtypingᴱ H N s (⇒-≮:-resolve⁻¹ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (resolve-≮:-⇒ ? p))) reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Left q = Left (⇒-≮:-resolve (resolve⁻¹-≮:-⇒ q)) reflect-subtypingᴱ H (M $ N) (app₂ v s) p | Right W = Right (app₂ W) -reflect-subtypingᴱ H (M $ N) {T = T} (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong (λ F → resolve F (typeOfᴱ H ∅ N)) (cong orUnknown (cong typeOfᴹᴼ q))) (<:-trans-≮: (<:-resolve {typeOfᴱ H ∅ N}) p)) +reflect-subtypingᴱ H (M $ N) {T = T} (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong (λ F → resolve F (typeOfᴱ H ∅ N)) (cong orUnknown (cong typeOfᴹᴼ q))) (<:-trans-≮: (<:-resolve {typeOfᴱ H ∅ N} {S} {U}) p)) reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p)) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index a5c07e19..c9400d2e 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -337,6 +337,9 @@ never-≮: (witness t p q) = witness t p never unknown-≮:-never : (unknown ≮: never) unknown-≮:-never = witness (scalar nil) unknown never +unknown-≮:-function : ∀ {S T} → (unknown ≮: (S ⇒ T)) +unknown-≮:-function = witness (scalar nil) unknown (function-scalar nil) + function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never) function-≮:-never = witness function function never diff --git a/prototyping/Properties/TypeSaturation.agda b/prototyping/Properties/TypeSaturation.agda index a482cad3..b2e35473 100644 --- a/prototyping/Properties/TypeSaturation.agda +++ b/prototyping/Properties/TypeSaturation.agda @@ -233,6 +233,9 @@ ov-<: F here p = p ov-<: (F ∩ G) (left o) p = <:-trans <:-∩-left (ov-<: F o p) ov-<: (F ∩ G) (right o) p = <:-trans <:-∩-right (ov-<: G o p) +<:ᵒ-impl-<: : ∀ {F S T} → FunType F → F <:ᵒ (S ⇒ T) → F <: (S ⇒ T) +<:ᵒ-impl-<: F (defn o o₁ o₂) = ov-<: F o (<:-function o₁ o₂) + ⊂:-overloads-left : ∀ {F G} → Overloads F ⊂: Overloads (F ∩ G) ⊂:-overloads-left p = just (left p)