WIP

prototyping/Properties/DecSubtyping.agda

@@ -11,7 +11,7 @@ open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
 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-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
-open import Properties.TypeNormalization using (FunType; Normal; never; unknown; function; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalⁱ; normalᶠ)
+open import Properties.TypeNormalization using (FunType; Inhabited; Normal; never; unknown; function; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalⁱ; normalᶠ; inhabited; inhabitant)
 open import Properties.Equality using (_≢_)
 
 fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
@@ -56,10 +56,18 @@ srcᶠ-function-err : ∀ {F} → (Fᶠ : FunType F) → ∀ s → ¬Language (s
 
 resolveᶠⁿ : ∀ {F V} → FunType F → Normal V → Type
 normal-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → Normal (resolveᶠⁿ Fᶠ Vⁿ)
--- function-ok-resolveᶠⁿ : ∀ {F V} → (Fᶠ : FunType F) → (Vⁿ : Normal V) → (V <: srcᶠ Fᶠ) → ∀ s t → Language V s → Language F (function-ok s t) → Language (resolveᶠⁿ Fᶠ Vⁿ) t
-≮:-resolveᶠⁿ : ∀ {F S T} → (Fᶠ : FunType F) → (Sᶠ : Normal S) → (S <: srcᶠ Fᶠ) → (S ≮: never) → (resolveᶠⁿ Fᶠ Sᶠ ≮: T) → (F ≮: (S ⇒ T))
+-- 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
 
@@ -89,6 +97,83 @@ 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)
@@ -121,7 +206,7 @@ normal-resolveᶠⁿ (F ∩ G) V | Right p | Right q = normal-∩ⁿ (normal-res
 <:-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 s q₁ q₂) (witness t r₁ r₂) = witness (function-ok s t) {!!} (function-ok q₁ {!r₂!})
+≮:-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 | Left p = Left (witness (scalar T) (scalar T) p)
@@ -130,7 +215,7 @@ dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
 dec-subtypingᶠ T function = Right (fun-top T)
 dec-subtypingᶠ T (U ⇒ V) with dec-subtypingⁿ (normalⁱ U) (normal-srcᶠ T) | dec-subtypingⁿ (normal-resolveᶠⁿ T (normalⁱ U)) V
 dec-subtypingᶠ T (U ⇒ V) | Left p | q = Left (≮:-srcᶠ T p)
-dec-subtypingᶠ T (U ⇒ V) | Right p | Left q = Left {!q!} -- Left (<:-trans-≮: {!!} (≮:-function-right {!!} q)) -- (≮:-resolveᶠⁿ T (normalⁱ U) p q)
+dec-subtypingᶠ T (U ⇒ V) | Right p | Left q = Left (≮:-resolveᶠⁿ T U p q)
 dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (<:-trans (<:-resolveᶠⁿ T (normalⁱ U) p) (<:-function <:-refl q))
 dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
 dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)

prototyping/Properties/TypeNormalization.agda

@@ -61,6 +61,12 @@ inhabited (S ∩ T) = inhabitedᶠ (S ∩ T)
 inhabited (S ∪ T) = right (scalar T)
 inhabited unknown = unknown
 
+-- Top function type
+function-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
+function-top function = <:-refl
+function-top (S ⇒ T) = <:-function <:-never <:-unknown
+function-top (F ∩ G) = <:-trans <:-∩-left (function-top F)
+
 -- Normalization produces normal types
 normal : ∀ T → Normal (normalize T)
 normalᶠ : ∀ {F} → FunType F → Normal F