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-25 15:58:14 -05:00
parent 80e54008a7
commit 3b55f94066
9 changed files with 84 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
prototyping/Luau/StrictMode/ToString.agda
View file

@ -4,7 +4,7 @@ module Luau.StrictMode.ToString where
open import Agda.Builtin.Nat using (Nat; suc)
open import FFI.Data.String using (String; _++_)
open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err)
open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err; function-tgt)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
open import Luau.Type using (number; boolean; string; nil)
@ -29,6 +29,7 @@ treeToString (scalar nil) n v = v ++ " is nil"
treeToString function n v = v ++ " is a function"
treeToString (function-ok s t) n v = treeToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n " ++ treeToString s (suc n) w where w = tmp n
treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n " ++ treeToString t (suc n) w where w = tmp n
treeToString (function-tgt t) n v = treeToString t n (v ++ "()")
subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
subtypeWarningToString (witness t p q) = "\n because provided type contains v, where " ++ treeToString t 0 "v"

4
prototyping/Luau/Subtyping.agda
View file

@ -15,6 +15,7 @@ data Tree : Set where
function : Tree
function-ok : Tree → Tree → Tree
function-err : Tree → Tree
function-tgt : Tree → Tree
data Language : Type → Tree → Set
data ¬Language : Type → Tree → Set
@ -26,6 +27,7 @@ data Language where
function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u)
function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t u)
function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
function-tgt : ∀ {T U t} → (Language U t) → Language (T ⇒ U) (function-tgt t)
left : ∀ {T U t} → Language T t → Language (T ∪ U) t
right : ∀ {T U u} → Language U u → Language (T ∪ U) u
_,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
@ -37,9 +39,11 @@ data ¬Language where
scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
scalar-function-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u)
scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
scalar-function-tgt : ∀ {S t} → (Scalar S) → ¬Language S (function-tgt t)
function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
function-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u)
function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
function-tgt : ∀ {T U t} → (¬Language U t) → ¬Language (T ⇒ U) (function-tgt t)
_,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u

27
prototyping/Properties/DecSubtyping.agda
View file

@ -5,13 +5,13 @@ module Properties.DecSubtyping where
open import Agda.Builtin.Equality using (_≡_; refl)
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-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
open import Luau.TypeSaturation using (saturate)
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.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; _∩_; _∪_; _⇒_; 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; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_)
open import Properties.Equality using (_≢_)
@ -25,12 +25,13 @@ 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-err p) = scalar-function-err s
fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
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ˢᶠᵒ : ∀ {F S T} → FunType F → Saturated F → FunType (S ⇒ T) → (S ≮: never) → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
dec-subtypingˢᶠᵒ : ∀ {F S T} → FunType F → Saturated F → FunType (S ⇒ T) → 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)
@ -41,7 +42,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} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (witness s₀ Ss₀ never) = result (top Fᶠ (λ o → o)) where
dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) = result (top Fᶠ (λ o → o)) where
data Top G : Set where
@ -100,7 +101,7 @@ dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (w
})
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₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-tgt t) (ov-language Fᶠ (λ o → function-tgt (tgt₀ o t T₀t))) (function-tgt ¬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 (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
@ -136,11 +137,9 @@ dec-subtypingˢᶠᵒ {F} {S} {T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) (w
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ˢ (S ⇒ T) with dec-subtypingˢᶠᵒ F Fˢ (S ⇒ T)
dec-subtypingˢᶠ F Fˢ (S ⇒ T) | Left F≮:S⇒T = Left F≮:S⇒T
dec-subtypingˢᶠ F Fˢ (S ⇒ T) | 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)
@ -186,7 +185,7 @@ dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (norm
-- <:ᵒ 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
<:-impl-<:ᵒ : ∀ {F S T} → FunType F → Saturated F → (F <: (S ⇒ T)) → (F <:ᵒ (S ⇒ T))
<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ F<:S⇒T with dec-subtypingˢᶠᵒ Fᶠ Fˢ (normal S ⇒ normal T)
<:-impl-<:ᵒ {F} {S} {T} Fᶠ Fˢ 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ˢ F<:S⇒T | Right F<:ᵒS⇒T = F<:ᵒS⇒T >>=ˡ <:-normalize S >>=ʳ normalize-<: T

4
prototyping/Properties/FunctionTypes.agda
View file

@ -4,7 +4,7 @@ module Properties.FunctionTypes where
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.FunctionTypes using (srcⁿ; src; tgt)
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-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
open import Properties.Functions using (_∘_)
@ -65,6 +65,7 @@ fun-¬scalar s (S ∩ T) = left (fun-¬scalar s 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-tgt p) = scalar-function-tgt s
¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂
fun-function : ∀ {T} → FunType T → Language T function
@ -114,3 +115,4 @@ unknown-src-≮: r (witness (function-ok s .function) p (function-ok x (scalar-f
unknown-src-≮: r (witness (function-ok s .(function-ok _ _)) p (function-ok x (scalar-function-ok ())))
unknown-src-≮: r (witness (function-ok s .(function-err _)) p (function-ok x (scalar-function-err ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
unknown-src-≮: r (witness (function-tgt t) p (function-tgt (scalar-function-tgt ())))

32
prototyping/Properties/ResolveOverloads.agda
View file

@ -74,22 +74,22 @@ resolve F R = resolveⁿ (normal F) (normal R)
<:-resolve : ∀ {R S T} → T <: resolve (S ⇒ T) R
<:-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} → (FunType F) → (Saturated F) → (r : Resolved F R) → (F <: (R ⇒ U)) → (target r <: U)
resolveˢ-<:-⇒ Fᶠ Fˢ r F<:R⇒U with <:-impl-<:ᵒ Fᶠ Fˢ F<:R⇒U
resolveˢ-<:-⇒ Fᶠ Fˢ (yes Sʳ Tʳ oʳ R<:Sʳ tgtʳ) F<:R⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂
resolveˢ-<:-⇒ Fᶠ Fˢ (no tgtʳ) 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} → (Fⁿ : Normal F) → (Rⁿ : Normal R) → (F <: (R ⇒ U)) → (resolveⁿ Fⁿ Rⁿ <: U)
resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Rⁿ F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o)) F<:R⇒U
resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Rⁿ F<:R⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Rⁿ (λ o → o)) (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:R⇒U)
resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Rⁿ F<:R⇒U = CONTRADICTION (<:-impl-¬≮: F<:R⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ)))
resolveⁿ-<:-⇒ never Rⁿ F<:R⇒U = <:-never
resolveⁿ-<:-⇒ unknown Rⁿ 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} → (F <: (R ⇒ U)) → (resolve F R <: U)
resolve-<:-⇒ {F} {R} F<:R⇒U = resolveⁿ-<:-⇒ (normal F) (normal R) (<:-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)
resolve-≮:-⇒ : ∀ {F R U} → (resolve F R ≮: U) → (F ≮: (R ⇒ U))
resolve-≮:-⇒ {F} {R} {U} FR≮:U with dec-subtyping F (R ⇒ U)
resolve-≮:-⇒ {F} {R} {U} FR≮:U | Left F≮:R⇒U = F≮:R⇒U
resolve-≮:-⇒ {F} {R} {U} FR≮:U | Right F<:R⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ F<:R⇒U) FR≮:U)

8
prototyping/Properties/StrictMode.agda
View file

@ -86,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
@ -107,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
@ -142,10 +142,10 @@ 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} {S} {U}) p))

54
prototyping/Properties/Subtyping.agda
View file

@ -5,7 +5,7 @@ module Properties.Subtyping where
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import FFI.Data.Maybe using (Maybe; just; nothing)
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-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
open import Properties.Equality using (_≢_)
@ -50,6 +50,11 @@ dec-language never t = Left never
dec-language unknown t = Right unknown
dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
dec-language nil (function-tgt t) = Left (scalar-function-tgt nil)
dec-language (T₁ ⇒ T₂) (function-tgt t) = mapLR function-tgt function-tgt (dec-language T₂ t)
dec-language boolean (function-tgt t) = Left (scalar-function-tgt boolean)
dec-language number (function-tgt t) = Left (scalar-function-tgt number)
dec-language string (function-tgt t) = Left (scalar-function-tgt string)
-- ¬Language T is the complement of Language T
language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
@ -64,7 +69,9 @@ language-comp function (scalar-function ()) function
language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ p)
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₁ q) = language-comp s q p₁
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₂ q) = language-comp t p₂ q
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
language-comp (function-tgt t) (scalar-function-tgt ()) (function-tgt q)
language-comp (function-tgt t) (function-tgt p) (function-tgt q) = language-comp t p q
-- ≮: is the complement of <:
¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
@ -221,6 +228,7 @@ 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₁ (<:-impl-⊇ p s 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-tgt t) (function-tgt r) = function-tgt (q t r)
<:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U))
<:-function-∩-∩ function (function , function) = function
@ -228,6 +236,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-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-∩-∩ (function-tgt s) (function-tgt p , function-tgt q) = function-tgt (p , q)
<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
<:-function-∩-∪ function (function , function) = function
@ -235,6 +244,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-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-err s) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
<:-function-∩-∪ (function-tgt t) (function-tgt p , q) = function-tgt (left p)
<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
<:-function-∩ function (function , function) = function
@ -242,6 +252,7 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-function-∩ (function-ok s t) (function-ok₁ p₁ , p₂) = function-ok₁ p₁
<:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂)
<:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
<:-function-∩ (function-tgt t) (function-tgt p₁ , function-tgt p₂) = function-tgt (p₁ , p₂)
<:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
<:-function-∪ function (left function) = function
@ -254,6 +265,8 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-function-∪ (function-ok s t) (right (function-ok₂ p)) = function-ok₂ (right p)
<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
<:-function-∪ (scalar s) (right (scalar ()))
<:-function-∪ (function-tgt t) (left (function-tgt p)) = function-tgt (left p)
<:-function-∪ (function-tgt t) (right (function-tgt p)) = function-tgt (right p)
<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
<:-function-∪-∩ function function = left function
@ -263,12 +276,8 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-function-∪-∩ (function-ok s t) (function-ok₂ (right p)) = right (function-ok₂ p)
<:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
<:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
<:-function-never : ∀ {T U} → (never ⇒ T) <: (never ⇒ U)
<:-function-never function function = function
<:-function-never (function-ok s t) (function-ok₁ p) = function-ok₁ p
<:-function-never (function-ok s t) (function-ok₂ p) = function-ok₁ never
<:-function-never (function-err s) (function-err p) = function-err p
<:-function-∪-∩ (function-tgt t) (function-tgt (left p)) = left (function-tgt p)
<:-function-∪-∩ (function-tgt t) (function-tgt (right p)) = right (function-tgt p)
<:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S)
<:-function-left {R} {S} p s Rs with dec-language S s
@ -364,6 +373,7 @@ function-≮:-never = witness function function never
<:-everything function p = left function
<:-everything (function-ok s t) p = left (function-ok₁ never)
<:-everything (function-err s) p = left (function-err never)
<:-everything (function-tgt t) p = left (function-tgt unknown)
-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
-- defines a "set-theoretic" model (sec 2.5)
@ -415,23 +425,28 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _)
S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
S₁t | Right r = r
set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
-- We don't quite have that this is a set-theoretic model
-- it's only true when Language S₂ is inhabited
-- in particular it's not true when S₂ is never,
∀ s₂ → Language S₂ s₂ →
-- This is the "only if" part of being a set-theoretic model
(∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) →
(∀ Q → Q ⊆ Comp(Language S₁ ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp(Language S₂ ⊗ Comp(Lift(Language T₂)))) →
(Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))
set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} p = r where
not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ S₂s₂ p = r where
Q : (Tree × Maybe Tree) → Set
Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u)
Q (t , nothing) = ¬Language S₁ t
q : Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁)))
q : Q ⊆ Comp(Language S₁ ⊗ Comp(Lift(Language T₁)))
q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t
r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
r function function = function
r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
@ -445,3 +460,14 @@ set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} p = r where
r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Left ¬S₂s = function-ok₁ ¬S₂s
r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Right S₂s = CONTRADICTION (p Q q (s , just t) (Right T₁t) (S₂s , language-comp t ¬T₂t))
r (function-ok s t) (function-ok₂ T₁t) | Right T₂t = function-ok₂ T₂t
r (function-tgt t) (function-tgt T₁t) with dec-language T₂ t
r (function-tgt t) (function-tgt T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
r (function-tgt t) (function-tgt T₁t) | Right T₂t = function-tgt T₂t
-- A counterexample when the argument type is empty.
set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string)))
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
set-theoretic-counterexample-two = witness (function-tgt (scalar number)) (function-tgt (scalar number)) (function-tgt (scalar-scalar number string (λ ())))

2
prototyping/Properties/TypeNormalization.agda
View file

@ -6,7 +6,7 @@ open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never;
open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
open import Luau.Subtyping using (_<:_; _≮:_; witness; never)
open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect; ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never; <:-function-never)
open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect; ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never)
-- Normal forms for types
data FunType : Type → Set

2
prototyping/Properties/TypeSaturation.agda
View file

@ -8,7 +8,7 @@ open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witn
open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
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; <:-function-∩-∪; <:-function-∩-∩; <:-∩-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-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; function-top; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.Functions using (_∘_)