mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
Added decidability of subtyping
This commit is contained in:
ajeffrey@roblox.com
parent
ec32877f06
commit
81d90b032f
4 changed files with 104 additions and 0 deletions
|
|
@ -4,6 +4,7 @@ module Properties where
|
|||
|
||||
import Properties.Contradiction
|
||||
import Properties.Dec
|
||||
import Properties.DecSubtyping
|
||||
import Properties.Equality
|
||||
import Properties.Functions
|
||||
import Properties.FunctionTypes
|
||||
|
|
|
|||
70
prototyping/Properties/DecSubtyping.agda
Normal file
70
prototyping/Properties/DecSubtyping.agda
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
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.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-err; left; right; _,_)
|
||||
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
|
||||
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)
|
||||
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
|
||||
open import Properties.FunctionTypes using (fun-¬scalar; ¬fun-scalar; fun-function; src-unknown-≮:; tgt-never-≮:; src-tgtᶠ-<:)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
-- Honest this terminates, since src and tgt reduce 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 → FunType 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 → Either (T ≮: U) (T <: U)
|
||||
|
||||
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ᶠ {T = T} _ (U ⇒ V) with dec-subtypingⁿ U (normal (src T)) | dec-subtypingⁿ (normal (tgt T)) V
|
||||
dec-subtypingᶠ {T = T} _ (U ⇒ V) | Left p | q = Left (≮:-trans-<: (src-unknown-≮: (≮:-trans-<: p (<:-normalize (src T)))) (<:-function <:-refl <:-unknown))
|
||||
dec-subtypingᶠ {T = T} _ (U ⇒ V) | Right p | Left q = Left (≮:-trans-<: (tgt-never-≮: (<:-trans-≮: (normalize-<: (tgt T)) q)) (<:-trans (<:-function <:-never <:-refl) <:-∪-right))
|
||||
dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (src-tgtᶠ-<: T (<:-trans p (normalize-<: _)) (<:-trans (<:-normalize _) 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)
|
||||
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)
|
||||
|
||||
dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
|
||||
dec-subtypingᶠⁿ T unknown = Right <:-unknown
|
||||
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) | Left (witness t p q) = Left (witness t p (q , ¬fun-scalar V T p))
|
||||
dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
|
||||
|
||||
dec-subtypingⁿ never U = Right <:-never
|
||||
dec-subtypingⁿ unknown unknown = Right <:-refl
|
||||
dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
|
||||
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₁ | Left p = Left (<:-trans-≮: <:-unknown p)
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
|
||||
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
|
||||
dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
|
||||
dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
|
||||
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 | Right p | Left q = Left (≮:-∪-right q)
|
||||
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)))
|
||||
|
||||
|
|
@ -60,6 +60,16 @@ fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s
|
|||
fun-¬scalar s (S ⇒ T) = function-scalar s
|
||||
fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)
|
||||
|
||||
¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t
|
||||
¬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-err p) = scalar-function-err s
|
||||
¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂
|
||||
|
||||
fun-function : ∀ {T} → FunType T → Language T function
|
||||
fun-function (S ⇒ T) = function
|
||||
fun-function (S ∩ T) = (fun-function S , fun-function T)
|
||||
|
||||
srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t)
|
||||
srcⁿ-¬scalar s never (scalar ())
|
||||
srcⁿ-¬scalar s unknown p = never
|
||||
|
|
@ -130,3 +140,11 @@ never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (
|
|||
never-tgt-≮: (witness function p (q₁ , scalar-function ()))
|
||||
never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
|
||||
never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))
|
||||
|
||||
src-tgtᶠ-<: : ∀ {T U V} → (FunType T) → (U <: src T) → (tgt T <: V) → (T <: (U ⇒ V))
|
||||
src-tgtᶠ-<: T p q (scalar s) r = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s T) r)
|
||||
src-tgtᶠ-<: T p q function r = function
|
||||
src-tgtᶠ-<: T p q (function-ok s) r = function-ok (q s (function-ok-tgt r))
|
||||
src-tgtᶠ-<: T p q (function-err s) r = function-err (<:-impl-⊇ p s (src-¬function-err r))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -102,6 +102,9 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
<:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U)
|
||||
<:-trans-≮: p (witness t q r) = witness t (p t q) r
|
||||
|
||||
≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T)
|
||||
≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q)
|
||||
|
||||
-- Properties of union
|
||||
|
||||
<:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U))
|
||||
|
|
@ -229,10 +232,22 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
<:-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-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
|
||||
≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)
|
||||
|
||||
≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
|
||||
≮:-function-right (witness t p q) = witness (function-ok t) (function-ok p) (function-ok q)
|
||||
|
||||
-- Properties of scalars
|
||||
skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
|
||||
skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
|
||||
|
||||
scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T)
|
||||
scalar-<: number p (scalar number) (scalar number) = p
|
||||
scalar-<: boolean p (scalar boolean) (scalar boolean) = p
|
||||
scalar-<: string p (scalar string) (scalar string) = p
|
||||
scalar-<: nil p (scalar nil) (scalar nil) = p
|
||||
|
||||
scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never
|
||||
scalar-∩-function-<:-never number .(scalar number) (() , scalar number)
|
||||
scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue