luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-05-24 11:43:57 -05:00
parent 01e09862fd
commit cf97b4aa3d
3 changed files with 164 additions and 299 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

306
prototyping/Properties/DecSubtyping.agda
View file

@ -8,223 +8,145 @@ open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_) open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_) open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_) open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
open import Luau.TypeSaturation using (saturate)
open import Properties.Contradiction using (CONTRADICTION; ¬) open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Functions using (_∘_) 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-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp) 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; Inhabited; Normal; never; unknown; function; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalⁱ; normalᶠ; inhabited; inhabitant) 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.Equality using (_≢_) open import Properties.Equality using (_≢_)
fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
fun-top function = <:-refl
fun-top (S ⇒ T) = <:-function <:-never <:-unknown
fun-top (F ∩ G) = <:-trans <:-∩-left (fun-top F)
fun-function : ∀ {F} → FunType F → Language F function fun-function : ∀ {F} → FunType F → Language F function
fun-function function = function
fun-function (S ⇒ T) = function fun-function (S ⇒ T) = function
fun-function (F ∩ G) = (fun-function F , fun-function G) fun-function (F ∩ G) = (fun-function F , fun-function G)
¬fun-scalar : ∀ {F S} → (s : Scalar S) → FunType F → ¬Language F (scalar s)
¬fun-scalar = {!!}
fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F t → ¬Language S t fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F t → ¬Language S t
fun-¬scalar s function function = scalar-function s
fun-¬scalar s function (function-ok₁ p) = scalar-function-ok s
fun-¬scalar s function (function-ok₂ p) = scalar-function-ok s
fun-¬scalar s function (function-err p) = scalar-function-err s
fun-¬scalar s (S ⇒ T) function = scalar-function s fun-¬scalar s (S ⇒ T) function = scalar-function s
fun-¬scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s fun-¬scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
fun-¬scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s fun-¬scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂ fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
function-err-ok : ∀ {F s t} → FunType F → Language F (function-err s) → Language F (function-ok s t) -- Honest this terminates, since saturation maintains the depth of nested arrows
function-err-ok = {!!}
-- Honest this terminates, since src and tgt reduce the depth of nested arrows
{-# TERMINATING #-} {-# TERMINATING #-}
dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U) 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 → FunType U → Either (T ≮: U) (T <: U)
dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U) dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U)
dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U) dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U) dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
srcᶠ : ∀ {F} → FunType F → Type
normal-srcᶠ : ∀ {F} → (Fᶠ : FunType F) → Normal (srcᶠ Fᶠ)
srcᶠ-function-err : ∀ {F} → (Fᶠ : FunType F) → ∀ s → ¬Language (srcᶠ Fᶠ) s → Language F (function-err s)
≮:-srcᶠ : ∀ {F S T} → (Fᶠ : FunType F) → (S ≮: srcᶠ Fᶠ) → (F ≮: (S ⇒ T))
resolveᶠⁿ : ∀ {F V} → FunType F → Normal V → Type
normal-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → Normal (resolveᶠⁿ Fᶠ Vⁿ)
-- foo : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → (V ≮: never) → Tree → Tree
-- bar : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → ∀ p t → Language V (foo Fᶠ Vⁿ p t)
-- baz : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → ∀ p t → Language (resolveᶠⁿ Fᶠ Vⁿ) t → Language F (function-ok (foo Fᶠ Vⁿ p t) t)
-- function-ok-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → ∀ s t → Language (srcᶠ Fᶠ) s → Language (resolveᶠⁿ Fᶠ Vⁿ) t → Language F (function-ok s t)
-- foo : ∀ {F S} → (Fᶠ : FunType F) → (Sⁿ : Normal S) → (S <: srcᶠ Fᶠ) → ∀ s t → Language S s → ¬Language (resolveᶠⁿ Fᶠ Sⁿ) t → ¬Language F (function-ok s t)
-- bar : ∀ {F S} → (Fᶠ : FunType F) → (Sⁿ : Normal S) → (S <: srcᶠ Fᶠ) → ∀ s t → Language S s → Language (resolveᶠⁿ Fᶠ Sⁿ) t → Language F (function-ok s t)
≮:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sⁱ : Inhabited S) → (S <: srcᶠ Fᶠ) → (resolveᶠⁿ Fᶠ (normalⁱ Sⁱ) ≮: T) → (F ≮: (S ⇒ T))
<:-resolveᶠⁿ : ∀ {F S} → (Fᶠ : FunType F) → (Sⁿ : Normal S) → (S <: srcᶠ Fᶠ) → (F <: (S ⇒ resolveᶠⁿ Fᶠ Sⁿ))
resolveᶠⁿ-<: : ∀ {F S T} → (Fᶠ : FunType F) → (Sⁿ : Normal S) → (S <: srcᶠ Fᶠ) → (F <: (S ⇒ T)) → (resolveᶠⁿ Fᶠ Sⁿ <: T)
srcᶠ {S ⇒ T} F = S
srcᶠ (F ∩ G) = srcᶠ F ∪ⁿ srcᶠ G
normal-srcᶠ function = never
normal-srcᶠ (S ⇒ T) = normalⁱ S
normal-srcᶠ (F ∩ G) = normal-∪ⁿ (normal-srcᶠ F) (normal-srcᶠ G)
srcᶠ-function-err function s p = function-err p
srcᶠ-function-err (S ⇒ T) s p = function-err p
srcᶠ-function-err (F ∩ G) s p with <:-impl-⊇ (∪-<:-∪ⁿ (normal-srcᶠ F) (normal-srcᶠ G)) s p
srcᶠ-function-err (F ∩ G) s p | (p₁ , p₂) = (srcᶠ-function-err F s p₁ , srcᶠ-function-err G s p₂)
≮:-srcᶠ F (witness s p q) = witness (function-err s) (srcᶠ-function-err F s q) (function-err p)
resolveᶠⁿ {S ⇒ T} F V = T
resolveᶠⁿ (F ∩ G) V with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
resolveᶠⁿ (F ∩ G) V | Left p | Left q = resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V) ∪ⁿ resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V)
resolveᶠⁿ (F ∩ G) V | Left p | Right q = resolveᶠⁿ G V
resolveᶠⁿ (F ∩ G) V | Right p | Left q = resolveᶠⁿ F V
resolveᶠⁿ (F ∩ G) V | Right p | Right q = resolveᶠⁿ F V ∩ⁿ resolveᶠⁿ G V
normal-resolveᶠⁿ function V = unknown
normal-resolveᶠⁿ (S ⇒ T) V = T
normal-resolveᶠⁿ (F ∩ G) V with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
normal-resolveᶠⁿ (F ∩ G) V | Left p | Left q = normal-∪ⁿ (normal-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V)) (normal-resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V))
normal-resolveᶠⁿ (F ∩ G) V | Left p | Right q = normal-resolveᶠⁿ G V
normal-resolveᶠⁿ (F ∩ G) V | Right p | Left q = normal-resolveᶠⁿ F V
normal-resolveᶠⁿ (F ∩ G) V | Right p | Right q = normal-∩ⁿ (normal-resolveᶠⁿ F V) (normal-resolveᶠⁿ G V)
resolveᶠⁿ-<: function V p₁ p₂ t q = {!!}
resolveᶠⁿ-<: (S ⇒ T) V p₁ p₂ t q = {!!}
resolveᶠⁿ-<: {F ∩ G} {V} {T} (Fᶠ ∩ Gᶠ) Vⁿ p q with dec-subtypingⁿ Vⁿ (normal-srcᶠ Fᶠ) | dec-subtypingⁿ Vⁿ (normal-srcᶠ Gᶠ)
resolveᶠⁿ-<: {F ∩ G} {V} {T} (Fᶠ ∩ Gᶠ) Vⁿ p q | Left r₁ | Left r₂ = result where
V₁ = (srcᶠ Fᶠ) ∩ⁿ V
V₂ = (srcᶠ Gᶠ) ∩ⁿ V
V₁ⁿ = normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ
V₂ⁿ = normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ
Tⁿ = normal-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
Uⁿ = normal-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
p₁ : V₁ <: srcᶠ Fᶠ
p₁ = <:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Fᶠ) Vⁿ) <:-∩-left
q₁ : F <: (V₁ ⇒ T)
q₁ = {!!}
result : ((resolveᶠⁿ Fᶠ V₁ⁿ) ∪ⁿ (resolveᶠⁿ Gᶠ V₂ⁿ)) <: T
result = <:-trans (∪ⁿ-<:-∪ (normal-resolveᶠⁿ Fᶠ V₁ⁿ) (normal-resolveᶠⁿ Gᶠ V₂ⁿ)) (<:-∪-lub (resolveᶠⁿ-<: Fᶠ V₁ⁿ p₁ q₁) {!!})
-- foo function V p t q = inhabitant V
-- foo (S ⇒ T) V p t q = inhabitant V
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p t q with dec-subtypingⁿ (normalⁱ Vⁿ) (normal-srcᶠ Fᶠ) | dec-subtypingⁿ Vⁿ (normal-srcᶠ Gᶠ)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p t q | Left r₁ | Left r₂ = ?
-- bar function V p t q = inhabited V
-- bar (S ⇒ T) V p t q = inhabited V
-- bar (F ∩ G) V p t q = {!!}
-- baz function V p t q = function-ok₁ never
-- baz (S ⇒ T) V p t q = function-ok₂ q
-- baz (F ∩ G) V p t q = {!!}
-- function-ok-resolveᶠⁿ function V s t p₁ p₂ = function-ok₂ p₂
-- function-ok-resolveᶠⁿ (S ⇒ T) V s t p₁ p₂ = function-ok₂ p₂
-- function-ok-resolveᶠⁿ (F ∩ G) V s t p₁ p₂ with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
-- function-ok-resolveᶠⁿ (F ∩ G) V s t p₁ p₂ | Left q₁ | Left q₂ = (function-ok-resolveᶠⁿ F (normal-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V)) s t {!!} {!p₂!} , {!!})
-- foo function V o s t p q = CONTRADICTION (language-comp s never (o s p))
-- foo (S ⇒ T) V o s t p q = function-ok (o s p) q
-- foo (F ∩ G) V o s t p q with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Left r₁ | Left r₂ = result where
-- Tⁿ = normal-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
-- Uⁿ = normal-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
-- result : ¬Language (F ∩ G) (function-ok s t)
-- result with <:-impl-⊇ (∪-<:-∪ⁿ Tⁿ Uⁿ) t q | dec-language (srcᶠ Fᶠ) s | dec-language (srcᶠ Gᶠ) s
-- result | (q₁ , q₂) | Left r₃ | Left r₄ = CONTRADICTION (language-comp s (r₃ , r₄) (∪ⁿ-<:-∪ (normal-srcᶠ Fᶠ) (normal-srcᶠ Gᶠ) s (o s p)))
-- result | (q₁ , q₂) | Right r | _ = left (foo Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Fᶠ) Vⁿ) <:-∩-left) s t (∩-<:-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ s (r , p)) q₁)
-- result | (q₁ , q₂) | _ | Right r = right (foo Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Gᶠ) Vⁿ) <:-∩-left) s t (∩-<:-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ s (r , p)) q₂)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Left r₁ | Right r₂ = right (foo Gᶠ Vⁿ r₂ s t p q)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Right r₁ | Left r₂ = left (foo Fᶠ Vⁿ r₁ s t p q)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Right r₁ | Right r₂ with <:-impl-⊇ (∩-<:-∩ⁿ (normal-resolveᶠⁿ Fᶠ Vⁿ) (normal-resolveᶠⁿ Gᶠ Vⁿ)) t q
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Right r₁ | Right r₂ | left q₁ = left (foo Fᶠ Vⁿ r₁ s t p q₁)
-- foo {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ o s t p q | Right r₁ | Right r₂ | right q₂ = right (foo Gᶠ Vⁿ r₂ s t p q₂)
-- bar function V p s t q₁ q₂ = {!!}
-- bar (S ⇒ T) V p s t q₁ q₂ = {!!}
-- bar {(F ∩ G)} {V} (Fᶠ ∩ Gᶠ) Vⁿ p s t q₁ q₂ with dec-subtypingⁿ Vⁿ (normal-srcᶠ Fᶠ) | dec-subtypingⁿ Vⁿ (normal-srcᶠ Gᶠ)
-- bar {(F ∩ G)} {V} (Fᶠ ∩ Gᶠ) Vⁿ p s t q₁ q₂ | Left r₁ | Left r₂ = result where
-- T = srcᶠ Fᶠ ∩ⁿ V
-- Tⁿ = normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ
-- lemma₁ : Language F (function-ok s t)
-- lemma₁ with dec-language (srcᶠ Fᶠ) s
-- lemma₁ | Left r₃ = function-err-ok Fᶠ (srcᶠ-function-err Fᶠ s r₃)
-- lemma₁ | Right r₃ = bar Fᶠ Tⁿ {!!} s t {!!} {!q₂!}
-- result : Language (F ∩ G) (function-ok s t)
-- result = {!!}
-- function-ok-resolveᶠⁿ function V p s t q₁ q₂ = {!!}
-- function-ok-resolveᶠⁿ (S ⇒ T) V p s t q₁ q₂ = {!!}
-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) | Left r₁ | Left r₂ with ∪ⁿ-<:-∪ (normal-srcᶠ F) (normal-srcᶠ G) s (p s q₁)
-- function-ok-resolveᶠⁿ (F ∩ G) V p s t q₁ (q₂ , q₃) | Left r₁ | Left r₂ | left r₃ = ∪-<:-∪ⁿ (normal-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V))
-- (normal-resolveᶠⁿ G (normal-∩ⁿ (normal-srcᶠ G) V)) t (left {!function-ok-resolveᶠⁿ F (normal-∩ⁿ (normal-srcᶠ F) V) ? s t ? !}) -- ∪-<:-∪ⁿ (normal-resolveᶠⁿ F V) {!normal-resolveᶠⁿ G V!} t (left (function-ok-resolveᶠⁿ F V {!!} s t q₁ q₂))
<:-resolveᶠⁿ function V p = <:-function p <:-refl
<:-resolveᶠⁿ (S ⇒ T) V p = <:-function p <:-refl
<:-resolveᶠⁿ (F ∩ G) V p with dec-subtypingⁿ V (normal-srcᶠ F) | dec-subtypingⁿ V (normal-srcᶠ G)
<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Left q | Left r = result where
T = resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
U = resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
Tⁿ = normal-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ)
Uⁿ = normal-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ)
lemma₁ : F <: ((srcᶠ Fᶠ ∩ V) ⇒ T)
lemma₁ = <:-trans (<:-resolveᶠⁿ Fᶠ (normal-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Fᶠ) Vⁿ) <:-∩-left)) (<:-function (∩-<:-∩ⁿ (normal-srcᶠ Fᶠ) Vⁿ) <:-refl)
lemma₂ : G <: ((srcᶠ Gᶠ ∩ V) ⇒ U)
lemma₂ = <:-trans (<:-resolveᶠⁿ Gᶠ (normal-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ) (<:-trans (∩ⁿ-<:-∩ (normal-srcᶠ Gᶠ) Vⁿ) <:-∩-left)) (<:-function (∩-<:-∩ⁿ (normal-srcᶠ Gᶠ) Vⁿ) <:-refl)
result : (F ∩ G) <: (V ⇒ (T ∪ⁿ U))
result = <:-trans (<:-trans (<:-intersect lemma₁ lemma₂) <:-function-∩-∪) (<:-function (<:-trans (<:-∩-glb (<:-trans p (∪ⁿ-<:-∪ (normal-srcᶠ Fᶠ) (normal-srcᶠ Gᶠ))) <:-refl) <:-∩-distr-∪) (∪-<:-∪ⁿ Tⁿ Uⁿ))
<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Left q | Right r = <:-trans <:-∩-right (<:-resolveᶠⁿ Gᶠ Vⁿ r)
<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Right q | Left r = <:-trans <:-∩-left (<:-resolveᶠⁿ Fᶠ Vⁿ q)
<:-resolveᶠⁿ {F ∩ G} {V} (Fᶠ ∩ Gᶠ) Vⁿ p | Right q | Right r = <:-trans (<:-intersect (<:-resolveᶠⁿ Fᶠ Vⁿ q) (<:-resolveᶠⁿ Gᶠ Vⁿ r)) (<:-trans <:-function-∩ (<:-function <:-refl (∩-<:-∩ⁿ (normal-resolveᶠⁿ Fᶠ Vⁿ) (normal-resolveᶠⁿ Gᶠ Vⁿ))))
≮:-resolveᶠⁿ F V p (witness t r₁ r₂) = {!!} -- witness (function-ok (foo F V p t r₁) t) (baz F V p t r₁) (function-ok (bar F V p t r₁) r₂)
dec-subtypingˢⁿ T U with dec-language _ (scalar T) 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 | Left p = Left (witness (scalar T) (scalar T) p)
dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p) dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
dec-subtypingᶠ T function = Right (fun-top T) dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H
dec-subtypingᶠ T (U ⇒ V) with dec-subtypingⁿ (normalⁱ U) (normal-srcᶠ T) | dec-subtypingⁿ (normal-resolveᶠⁿ T (normalⁱ U)) V dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G)
dec-subtypingᶠ T (U ⇒ V) | Left p | q = Left (≮:-srcᶠ T p) dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H)
dec-subtypingᶠ T (U ⇒ V) | Right p | Left q = Left (≮:-resolveᶠⁿ T U p q) dec-subtypingˢᶠ F Fˢ (G ∩ H) | Right F<:G | Right F<:H = Right (<:-∩-glb F<:G F<:H)
dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (<:-trans (<:-resolveᶠⁿ T (normalⁱ U) p) (<:-function <:-refl q)) dec-subtypingˢᶠ F (defn sat-∩ sat-∪) (S ⇒ T) with dec-subtypingⁿ S never
dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V 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ᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p) dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) | Left (witness s₀ Ss₀ never) = result (top Fᶠ (λ o → o)) where
dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q) data Top G : Set where
defn : ∀ Sᵗ Tᵗ →
Overloads F (Sᵗ ⇒ Tᵗ) →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
-------------
Top G
top : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Top G
top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
top (Gᶠ ∩ Hᶠ) G⊆F with top Gᶠ (G⊆F ∘ left) | top Hᶠ (G⊆F ∘ right)
top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ with sat-∪ p q
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 (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
data LargestSrc (G : Type) : Set where
yes : ∀ S₀ T₀ →
Overloads F (S₀ ⇒ T₀) →
T₀ <: T →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
-----------------------
LargestSrc G
no : ∀ S₀ T₀ →
Overloads F (S₀ ⇒ T₀) →
T₀ ≮: T →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T₀ <: T′) →
-----------------------
LargestSrc G
largest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → LargestSrc G
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F with dec-subtypingⁿ T′ⁿ Tⁿ
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Left T′≮:T = no S′ T′ (G⊆F here) T′≮:T λ { here → <:-refl }
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Right T′<:T = yes S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl })
largest (Gᶠ ∩ Hᶠ) GH⊆F with largest Gᶠ (GH⊆F ∘ left) | largest Hᶠ (GH⊆F ∘ right)
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ with sat-∩ o₁ o₂
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt with dec-subtypingⁿ (normal-overload-tgt Fᶠ o) Tⁿ
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Left T₀≮:T = no _ _ o T₀≮:T (λ { (left o) → <:-trans tgt (<:-trans <:-∩-left (tgt₁ o)) ; (right o) → <:-trans tgt (<:-trans <:-∩-right (tgt₂ o)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Right T₀<:T = yes _ _ o T₀<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | yes S₂ T₂ o₂ T₂<:T src₂ = yes S₂ T₂ o₂ T₂<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → src₂ o p })
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ = yes S₁ T₁ o₁ T₁<:T (λ { (left o) p → src₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ with sat-∪ o₁ o₂
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ | defn o src tgt = yes _ _ o (<:-trans tgt (<:-∪-lub T₁<:T T₂<:T))
(λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src)
; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src)
})
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₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where
data SmallestTgt (G : Type) : Set where
defn : ∀ S₁ T₁ →
Overloads F (S₁ ⇒ T₁) →
Language S₁ s →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
-----------------------
SmallestTgt G
smallest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → SmallestTgt G
smallest {S′ ⇒ T′} _ G⊆F with dec-language S′ s
smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) }
smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl })
smallest (Gᶠ ∩ Hᶠ) GH⊆F with smallest Gᶠ (GH⊆F ∘ left) | smallest Hᶠ (GH⊆F ∘ right)
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ with sat-∩ o₁ o₂
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ | defn o src tgt = defn _ _ o (src s (R₁s , R₂s))
(λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s)
; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)
})
result₁ : SmallestTgt F → (F ≮: (S ⇒ T))
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) with dec-subtypingⁿ (normal-overload-tgt Fᶠ o₁) Tⁿ
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp s ¬S₀s (src₀ o₁ T₁<:T s S₁s))
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness t T₁t ¬Tt) = witness (function-ok s t) (ov-language Fᶠ lemma) (function-ok Ss ¬Tt) where
lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
lemma {S′} o with dec-language S′ s
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 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)
dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never) dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
dec-subtypingᶠⁿ T unknown = Right <:-unknown dec-subtypingᶠⁿ T unknown = Right <:-unknown
dec-subtypingᶠⁿ T function = Right (fun-top T)
dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V) dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V) dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
@ -233,7 +155,7 @@ dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
dec-subtypingⁿ never U = Right <:-never dec-subtypingⁿ never U = Right <:-never
dec-subtypingⁿ unknown unknown = Right <:-refl dec-subtypingⁿ unknown unknown = Right <:-refl
dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ function U dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p) dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p) dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
@ -250,12 +172,6 @@ dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p) dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q) dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q) dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)
dec-subtypingⁿ function function = Right <:-refl
dec-subtypingⁿ function (T ⇒ U) = dec-subtypingᶠ function (T ⇒ U)
dec-subtypingⁿ function (T ∩ U) = dec-subtypingᶠ function (T ∩ U)
dec-subtypingⁿ function (T ∪ U) = dec-subtypingᶠⁿ function (T ∪ U)
dec-subtypingⁿ function never = Left (witness function function never)
dec-subtypingⁿ function unknown = Right <:-unknown
dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U) 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 | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))

9
prototyping/Properties/Subtyping.agda
View file

@ -222,12 +222,19 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-function p q (function-ok s t) (function-ok₂ r) = function-ok₂ (q t r) <:-function p q (function-ok s t) (function-ok₂ r) = function-ok₂ (q t r)
<:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r) <:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r)
<:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U))
<:-function-∩-∩ function (function , function) = function
<:-function-∩-∩ (function-ok s t) (function-ok₁ p , q) = function-ok₁ (left p)
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₁ q) = function-ok₁ (right q)
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₂ q) = function-ok₂ (p , q)
<:-function-∩-∩ (function-err s) (function-err p , q) = function-err (left p)
<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U)) <:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
<:-function-∩-∪ function (function , function) = function <:-function-∩-∪ function (function , function) = function
<:-function-∩-∪ (function-ok s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂) <:-function-∩-∪ (function-ok s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂)
<:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂) <:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
<:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁) <:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
<:-function-∩-∪ (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂) <:-function-∩-∪ (function-err s) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U)) <:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
<:-function-∩ function (function , function) = function <:-function-∩ function (function , function) = function

148
prototyping/Properties/TypeSaturation.agda
View file

@ -8,8 +8,8 @@ open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witn
open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown) open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_) open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate) open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate)
open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-never; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:) open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-never; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
open import Properties.TypeNormalization using (FunType; _⇒_; _∩_; _∪_; never; unknown; function-top; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ) open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; function-top; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
open import Properties.Contradiction using (CONTRADICTION) open import Properties.Contradiction using (CONTRADICTION)
open import Properties.Functions using (_∘_) open import Properties.Functions using (_∘_)
@ -35,6 +35,39 @@ normal-∪-saturate (F ∩ G) = (normal-∪-saturate F ∩ normal-∪-saturate G
normal-saturate : ∀ {F} → FunType F → FunType (saturate F) normal-saturate : ∀ {F} → FunType F → FunType (saturate F)
normal-saturate F = normal-∪-saturate (normal-∩-saturate F) normal-saturate F = normal-∪-saturate (normal-∩-saturate F)
-- Saturation resects subtyping
∪-saturate-<: : ∀ {F} → FunType F → ∪-saturate F <: F
∪-saturate-<: (S ⇒ T) = <:-refl
∪-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∪-saturate-<: F) (∪-saturate-<: G))
∩-saturate-<: : ∀ {F} → FunType F → ∩-saturate F <: F
∩-saturate-<: (S ⇒ T) = <:-refl
∩-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∩-saturate-<: F) (∩-saturate-<: G))
saturate-<: : ∀ {F} → FunType F → saturate F <: F
saturate-<: F = <:-trans (∪-saturate-<: (normal-∩-saturate F)) (∩-saturate-<: F)
∩-<:-⋓ : ∀ {F G} → FunType F → FunType G → (F ∩ G) <: (F ⋓ G)
∩-<:-⋓ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∩-∪ (<:-function (∪ⁿ-<:-∪ R T) (∪-<:-∪ⁿ S U))
∩-<:-⋓ (R ⇒ S) (G ∩ H) = <:-trans (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋓ (R ⇒ S) G) (∩-<:-⋓ (R ⇒ S) H))
∩-<:-⋓ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋓ E G) (∩-<:-⋓ F G))
∩-<:-⋒ : ∀ {F G} → FunType F → FunType G → (F ∩ G) <: (F ⋒ G)
∩-<:-⋒ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∩-∩ (<:-function (∩ⁿ-<:-∩ R T) (∩-<:-∩ⁿ S U))
∩-<:-⋒ (R ⇒ S) (G ∩ H) = <:-trans (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋒ (R ⇒ S) G) (∩-<:-⋒ (R ⇒ S) H))
∩-<:-⋒ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋒ E G) (∩-<:-⋒ F G))
<:-∪-saturate : ∀ {F} → FunType F → F <: ∪-saturate F
<:-∪-saturate (S ⇒ T) = <:-refl
<:-∪-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (<:-trans (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (∩-<:-⋓ (normal-∪-saturate F) (normal-∪-saturate G)))
<:-∩-saturate : ∀ {F} → FunType F → F <: ∩-saturate F
<:-∩-saturate (S ⇒ T) = <:-refl
<:-∩-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (<:-trans (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (∩-<:-⋒ (normal-∩-saturate F) (normal-∩-saturate G)))
<:-saturate : ∀ {F} → FunType F → F <: saturate F
<:-saturate F = <:-trans (<:-∩-saturate F) (<:-∪-saturate (normal-∩-saturate F))
-- Overloads F is the set of overloads of F -- Overloads F is the set of overloads of F
data Overloads : Type → Type → Set where data Overloads : Type → Type → Set where
@ -42,6 +75,16 @@ data Overloads : Type → Type → Set where
left : ∀ {S T F G} → Overloads F (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T) left : ∀ {S T F G} → Overloads F (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
right : ∀ {S T F G} → Overloads G (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T) right : ∀ {S T F G} → Overloads G (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
normal-overload-src : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal S
normal-overload-src (S ⇒ T) here = S
normal-overload-src (F ∩ G) (left o) = normal-overload-src F o
normal-overload-src (F ∩ G) (right o) = normal-overload-src G o
normal-overload-tgt : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal T
normal-overload-tgt (S ⇒ T) here = T
normal-overload-tgt (F ∩ G) (left o) = normal-overload-tgt F o
normal-overload-tgt (F ∩ G) (right o) = normal-overload-tgt G o
-- An inductive presentation of the overloads of F ⋓ G -- An inductive presentation of the overloads of F ⋓ G
data ∪-Lift (P Q : Type → Set) : Type → Set where data ∪-Lift (P Q : Type → Set) : Type → Set where
@ -383,104 +426,3 @@ saturated : ∀ {F} → FunType F → Saturated (saturate F)
saturated F = defn saturated F = defn
(λ n o → (saturate-overloads F n [∩] saturate-overloads F o) >>= ∪-saturate-resp-∩-saturation ⊂:-∩-lift-saturate >>= overloads-saturate F) (λ n o → (saturate-overloads F n [∩] saturate-overloads F o) >>= ∪-saturate-resp-∩-saturation ⊂:-∩-lift-saturate >>= overloads-saturate F)
(λ n o → ∪-saturated (normal-∩-saturate F) (union n o)) (λ n o → ∪-saturated (normal-∩-saturate F) (union n o))
-- Subtyping is decidable on saturated normalized types
dec-<:-overloads : ∀ {F S T} → FunType F → FunType (S ⇒ T) → Saturated F → (S ≮: never) →
(∀ {S′ T′} → (Overloads F (S′ ⇒ T′)) → Either (S ≮: S′) (S <: S′)) →
(∀ {S′ T′} → (Overloads F (S′ ⇒ T′)) → Either (T′ ≮: T) (T′ <: T)) →
Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T))
dec-<:-overloads {F} {S} {T} Fᶠ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) (witness s₀ Ss₀ never) dec-src dec-tgt = result (top Fᶠ (λ o → o)) where
data Top G : Set where
defn : ∀ Sᵗ Tᵗ →
Overloads F (Sᵗ ⇒ Tᵗ) →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
-------------
Top G
top : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Top G
top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
top (Gᶠ ∩ Hᶠ) G⊆F with top Gᶠ (G⊆F ∘ left) | top Hᶠ (G⊆F ∘ right)
top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ with sat-∪ p q
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 (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-src 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
data LargestSrc (G : Type) : Set where
yes : ∀ S₀ T₀ →
Overloads F (S₀ ⇒ T₀) →
T₀ <: T →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
-----------------------
LargestSrc G
no : ∀ S₀ T₀ →
Overloads F (S₀ ⇒ T₀) →
T₀ ≮: T →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T₀ <: T′) →
-----------------------
LargestSrc G
largest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → LargestSrc G
largest {S′ ⇒ T′} _ G⊆F with dec-tgt (G⊆F here)
largest {S′ ⇒ T′} _ G⊆F | Left T′≮:T = no S′ T′ (G⊆F here) T′≮:T λ { here → <:-refl }
largest {S′ ⇒ T′} _ G⊆F | Right T′<:T = yes S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl })
largest (Gᶠ ∩ Hᶠ) GH⊆F with largest Gᶠ (GH⊆F ∘ left) | largest Hᶠ (GH⊆F ∘ right)
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ with sat-∩ o₁ o₂
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt with dec-tgt o
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Left T₀≮:T = no _ _ o T₀≮:T (λ { (left o) → <:-trans tgt (<:-trans <:-∩-left (tgt₁ o)) ; (right o) → <:-trans tgt (<:-trans <:-∩-right (tgt₂ o)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Right T₀<:T = yes _ _ o T₀<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | yes S₂ T₂ o₂ T₂<:T src₂ = yes S₂ T₂ o₂ T₂<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → src₂ o p })
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ = yes S₁ T₁ o₁ T₁<:T (λ { (left o) p → src₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ with sat-∪ o₁ o₂
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ | defn o src tgt = yes _ _ o (<:-trans tgt (<:-∪-lub T₁<:T T₂<:T))
(λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src)
; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src)
})
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-src 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₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where
data SmallestTgt (G : Type) : Set where
defn : ∀ S₁ T₁ →
Overloads F (S₁ ⇒ T₁) →
Language S₁ s →
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
-----------------------
SmallestTgt G
smallest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → SmallestTgt G
smallest {S′ ⇒ T′} _ G⊆F with dec-language S′ s
smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) }
smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl })
smallest (Gᶠ ∩ Hᶠ) GH⊆F with smallest Gᶠ (GH⊆F ∘ left) | smallest Hᶠ (GH⊆F ∘ right)
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ with sat-∩ o₁ o₂
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ | defn o src tgt = defn _ _ o (src s (R₁s , R₂s))
(λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s)
; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)
})
result₁ : SmallestTgt F → (F ≮: (S ⇒ T))
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) with dec-tgt o₁
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp s ¬S₀s (src₀ o₁ T₁<:T s S₁s))
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness t T₁t ¬Tt) = witness (function-ok s t) (ov-language Fᶠ lemma) (function-ok Ss ¬Tt) where
lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
lemma {S′} o with dec-language S′ s
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)