Merge branch 'master' into merge

This commit is contained in:
Arseny Kapoulkine 2022-04-28 18:05:04 -07:00
commit 9ce46fd381
13 changed files with 940 additions and 138 deletions

View File

@ -0,0 +1,38 @@
{-# OPTIONS --rewriting #-}
open import FFI.Data.Either using (Either; Left; Right)
open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; __; _∩_)
open import Luau.TypeNormalization using (normalize)
module Luau.FunctionTypes where
-- The domain of a normalized type
srcⁿ : Type Type
srcⁿ (S T) = S
srcⁿ (S T) = srcⁿ S srcⁿ T
srcⁿ never = unknown
srcⁿ T = never
-- To get the domain of a type, we normalize it first We need to do
-- this, since if we try to use it on non-normalized types, we get
--
-- src(number ∩ string) = src(number) src(string) = never never
-- src(never) = unknown
--
-- so src doesn't respect type equivalence.
src : Type Type
src (S T) = S
src T = srcⁿ(normalize T)
-- The codomain of a type
tgt : Type Type
tgt nil = never
tgt (S T) = T
tgt never = never
tgt unknown = unknown
tgt number = never
tgt boolean = never
tgt string = never
tgt (S T) = (tgt S) (tgt T)
tgt (S T) = (tgt S) (tgt T)

View File

@ -5,7 +5,8 @@ module Luau.StrictMode where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; __; _∩_; src; tgt)
open import Luau.FunctionTypes using (src; tgt)
open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; __; _∩_)
open import Luau.Subtyping using (_≮:_)
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)

View File

@ -25,7 +25,6 @@ data Language where
function : {T U} Language (T U) function
function-ok : {T U u} (Language U u) Language (T U) (function-ok u)
function-err : {T U t} (¬Language T t) Language (T U) (function-err t)
scalar-function-err : {S t} (Scalar S) Language S (function-err 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
@ -36,6 +35,7 @@ data ¬Language where
scalar-scalar : {S T} (s : Scalar S) (Scalar T) (S T) ¬Language T (scalar s)
scalar-function : {S} (Scalar S) ¬Language S function
scalar-function-ok : {S u} (Scalar S) ¬Language S (function-ok u)
scalar-function-err : {S t} (Scalar S) ¬Language S (function-err t)
function-scalar : {S T U} (s : Scalar S) ¬Language (T U) (scalar s)
function-ok : {T U u} (¬Language U u) ¬Language (T U) (function-ok u)
function-err : {T U t} (Language T t) ¬Language (T U) (function-err t)

View File

@ -24,6 +24,8 @@ data Scalar : Type → Set where
string : Scalar string
nil : Scalar nil
skalar = number (string (nil boolean))
lhs : Type Type
lhs (T _) = T
lhs (T _) = T
@ -146,28 +148,6 @@ just T ≡ᴹᵀ just U with T ≡ᵀ U
(just T ≡ᴹᵀ just T) | yes refl = yes refl
(just T ≡ᴹᵀ just U) | no p = no (λ q p (just-inv q))
src : Type Type
src nil = never
src number = never
src boolean = never
src string = never
src (S T) = S
src (S T) = (src S) (src T)
src (S T) = (src S) (src T)
src never = unknown
src unknown = never
tgt : Type Type
tgt nil = never
tgt (S T) = T
tgt never = never
tgt unknown = unknown
tgt number = never
tgt boolean = never
tgt string = never
tgt (S T) = (tgt S) (tgt T)
tgt (S T) = (tgt S) (tgt T)
optional : Type Type
optional nil = nil
optional (T nil) = (T nil)

View File

@ -7,8 +7,9 @@ open import FFI.Data.Maybe using (Maybe; just)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.FunctionTypes using (src; tgt)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_; src; tgt)
open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import FFI.Data.Vector using (Vector)
open import FFI.Data.Maybe using (Maybe; just; nothing)

View File

@ -0,0 +1,69 @@
module Luau.TypeNormalization where
open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; __; _∩_)
-- The top non-function type
¬function : Type
¬function = number (string (nil boolean))
-- Unions and intersections of normalized types
_ᶠ_ : Type Type Type
_ⁿˢ_ : Type Type Type
_∩ⁿˢ_ : Type Type Type
_ⁿ_ : Type Type Type
_∩ⁿ_ : Type Type Type
-- Union of function types
(F₁ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) (F₂ ∪ᶠ G)
F ∪ᶠ (G₁ G₂) = (F ∪ᶠ G₁) (F ∪ᶠ G₂)
(R S) ∪ᶠ (T U) = (R ∩ⁿ T) (S ∪ⁿ U)
F ∪ᶠ G = F G
-- Union of normalized types
S ∪ⁿ (T₁ T₂) = (S ∪ⁿ T₁) T₂
S ∪ⁿ unknown = unknown
S ∪ⁿ never = S
unknown ∪ⁿ T = unknown
never ∪ⁿ T = T
(S₁ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) S₂
F ∪ⁿ G = F ∪ᶠ G
-- Intersection of normalized types
S ∩ⁿ (T₁ T₂) = (S ∩ⁿ T₁) ∪ⁿˢ (S ∩ⁿˢ T₂)
S ∩ⁿ unknown = S
S ∩ⁿ never = never
(S₁ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
unknown ∩ⁿ G = G
never ∩ⁿ G = never
F ∩ⁿ G = F G
-- Intersection of normalized types with a scalar
(S₁ nil) ∩ⁿˢ nil = nil
(S₁ boolean) ∩ⁿˢ boolean = boolean
(S₁ number) ∩ⁿˢ number = number
(S₁ string) ∩ⁿˢ string = string
(S₁ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
unknown ∩ⁿˢ T = T
F ∩ⁿˢ T = never
-- Union of normalized types with an optional scalar
S ∪ⁿˢ never = S
unknown ∪ⁿˢ T = unknown
(S₁ nil) ∪ⁿˢ nil = S₁ nil
(S₁ boolean) ∪ⁿˢ boolean = S₁ boolean
(S₁ number) ∪ⁿˢ number = S₁ number
(S₁ string) ∪ⁿˢ string = S₁ string
(S₁ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) S₂
F ∪ⁿˢ T = F T
-- Normalize!
normalize : Type Type
normalize nil = never nil
normalize (S T) = (normalize S normalize T)
normalize never = never
normalize unknown = unknown
normalize boolean = never boolean
normalize number = never number
normalize string = never string
normalize (S T) = normalize S ∪ⁿ normalize T
normalize (S T) = normalize S ∩ⁿ normalize T

View File

@ -4,10 +4,13 @@ module Properties where
import Properties.Contradiction
import Properties.Dec
import Properties.DecSubtyping
import Properties.Equality
import Properties.Functions
import Properties.FunctionTypes
import Properties.Remember
import Properties.Step
import Properties.StrictMode
import Properties.Subtyping
import Properties.TypeCheck
import Properties.TypeNormalization

View 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)))

View File

@ -0,0 +1,150 @@
{-# OPTIONS --rewriting #-}
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-err; 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 (_∘_)
open import Properties.Subtyping using (<:-refl; ≮:-refl; <:-trans-≮:; skalar-scalar; <:-impl-⊇; skalar-function-ok; language-comp)
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; __; _⇒_; normal; <:-normalize; normalize-<:)
-- Properties of src
function-err-srcⁿ : {T t} (FunType T) (¬Language (srcⁿ T) t) Language T (function-err t)
function-err-srcⁿ (S T) p = function-err p
function-err-srcⁿ (S T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂)
¬function-err-srcᶠ : {T t} (FunType T) (Language (srcⁿ T) t) ¬Language T (function-err t)
¬function-err-srcᶠ (S T) p = function-err p
¬function-err-srcᶠ (S T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcᶠ (S T) (right p) = right (¬function-err-srcᶠ T p)
¬function-err-srcⁿ : {T t} (Normal T) (Language (srcⁿ T) t) ¬Language T (function-err t)
¬function-err-srcⁿ never p = never
¬function-err-srcⁿ unknown (scalar ())
¬function-err-srcⁿ (S T) p = function-err p
¬function-err-srcⁿ (S T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcⁿ (S T) (right p) = right (¬function-err-srcᶠ T p)
¬function-err-srcⁿ (S T) (scalar ())
¬function-err-src : {T t} (Language (src T) t) ¬Language T (function-err t)
¬function-err-src {T = S T} p = function-err p
¬function-err-src {T = nil} p = scalar-function-err nil
¬function-err-src {T = never} p = never
¬function-err-src {T = unknown} (scalar ())
¬function-err-src {T = boolean} p = scalar-function-err boolean
¬function-err-src {T = number} p = scalar-function-err number
¬function-err-src {T = string} p = scalar-function-err string
¬function-err-src {T = S T} p = <:-impl-⊇ (<:-normalize (S T)) _ (¬function-err-srcⁿ (normal (S T)) p)
¬function-err-src {T = S T} p = <:-impl-⊇ (<:-normalize (S T)) _ (¬function-err-srcⁿ (normal (S T)) p)
src-¬function-errᶠ : {T t} (FunType T) Language T (function-err t) (¬Language (srcⁿ T) t)
src-¬function-errᶠ (S T) (function-err p) = p
src-¬function-errᶠ (S T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
src-¬function-errⁿ : {T t} (Normal T) Language T (function-err t) (¬Language (srcⁿ T) t)
src-¬function-errⁿ unknown p = never
src-¬function-errⁿ (S T) (function-err p) = p
src-¬function-errⁿ (S T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
src-¬function-errⁿ (S T) p = never
src-¬function-err : {T t} Language T (function-err t) (¬Language (src T) t)
src-¬function-err {T = S T} (function-err p) = p
src-¬function-err {T = unknown} p = never
src-¬function-err {T = S T} p = src-¬function-errⁿ (normal (S T)) (<:-normalize (S T) _ p)
src-¬function-err {T = S T} p = src-¬function-errⁿ (normal (S T)) (<:-normalize (S T) _ p)
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
srcⁿ-¬scalar s (S T) (scalar ())
srcⁿ-¬scalar s (S T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁)
srcⁿ-¬scalar s (S T) p = never
src-¬scalar : {S T t} (s : Scalar S) Language T (scalar s) (¬Language (src T) t)
src-¬scalar {T = nil} s p = never
src-¬scalar {T = T U} s (scalar ())
src-¬scalar {T = never} s (scalar ())
src-¬scalar {T = unknown} s p = never
src-¬scalar {T = boolean} s p = never
src-¬scalar {T = number} s p = never
src-¬scalar {T = string} s p = never
src-¬scalar {T = T U} s p = srcⁿ-¬scalar s (normal (T U)) (<:-normalize (T U) (scalar s) p)
src-¬scalar {T = T U} s p = srcⁿ-¬scalar s (normal (T U)) (<:-normalize (T U) (scalar s) p)
srcⁿ-unknown-≮: : {T U} (Normal U) (T ≮: srcⁿ U) (U ≮: (T unknown))
srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown)
srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p)
srcⁿ-unknown-≮: (U V) (witness t p q) = witness (function-err t) (function-err q) (function-err p)
srcⁿ-unknown-≮: (U V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U V) q) (function-err p)
srcⁿ-unknown-≮: (U V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V)
src-unknown-≮: : {T U} (T ≮: src U) (U ≮: (T unknown))
src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil)
src-unknown-≮: {U = T U} (witness t p q) = witness (function-err t) (function-err q) (function-err p)
src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown)
src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p)
src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean)
src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number)
src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string)
src-unknown-≮: {U = T U} p = <:-trans-≮: (normalize-<: (T U)) (srcⁿ-unknown-≮: (normal (T U)) p)
src-unknown-≮: {U = T U} p = <:-trans-≮: (normalize-<: (T U)) (srcⁿ-unknown-≮: (normal (T U)) p)
unknown-src-≮: : {S T U} (U ≮: S) (T ≮: (U unknown)) (U ≮: src T)
unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
-- Properties of tgt
tgt-function-ok : {T t} (Language (tgt T) t) Language T (function-ok t)
tgt-function-ok {T = nil} (scalar ())
tgt-function-ok {T = T₁ T₂} p = function-ok p
tgt-function-ok {T = never} (scalar ())
tgt-function-ok {T = unknown} p = unknown
tgt-function-ok {T = boolean} (scalar ())
tgt-function-ok {T = number} (scalar ())
tgt-function-ok {T = string} (scalar ())
tgt-function-ok {T = T₁ T₂} (left p) = left (tgt-function-ok p)
tgt-function-ok {T = T₁ T₂} (right p) = right (tgt-function-ok p)
tgt-function-ok {T = T₁ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)
function-ok-tgt : {T t} Language T (function-ok t) (Language (tgt T) t)
function-ok-tgt (function-ok p) = p
function-ok-tgt (left p) = left (function-ok-tgt p)
function-ok-tgt (right p) = right (function-ok-tgt p)
function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
function-ok-tgt unknown = unknown
tgt-never-≮: : {T U} (tgt T ≮: U) (T ≮: (skalar (never U)))
tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)
never-tgt-≮: : {T U} (T ≮: (skalar (never U))) (tgt T ≮: U)
never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
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))

View File

@ -11,7 +11,8 @@ open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warning
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.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.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; __; src; tgt; _≡ᵀ_; _≡ᴹᵀ_)
open import Luau.FunctionTypes using (src; tgt)
open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; __; _≡ᵀ_; _≡ᴹᵀ_)
open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp)
open import Luau.Var using (_≡ⱽ_)
open import Luau.Addr using (_≡ᴬ_)
@ -22,7 +23,8 @@ open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
open import Properties.FunctionTypes using (never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:)
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.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; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)

View File

@ -4,9 +4,10 @@ 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-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; __; _∩_; src; tgt)
open import Properties.Contradiction using (CONTRADICTION; ¬)
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 (_≢_)
open import Properties.Functions using (_∘_)
open import Properties.Product using (_×_; _,_)
@ -19,28 +20,28 @@ dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
dec-language nil (scalar nil) = Right (scalar nil)
dec-language nil function = Left (scalar-function nil)
dec-language nil (function-ok t) = Left (scalar-function-ok nil)
dec-language nil (function-err t) = Right (scalar-function-err nil)
dec-language nil (function-err t) = Left (scalar-function-err nil)
dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
dec-language boolean (scalar boolean) = Right (scalar boolean)
dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
dec-language boolean function = Left (scalar-function boolean)
dec-language boolean (function-ok t) = Left (scalar-function-ok boolean)
dec-language boolean (function-err t) = Right (scalar-function-err boolean)
dec-language boolean (function-err t) = Left (scalar-function-err boolean)
dec-language number (scalar number) = Right (scalar number)
dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
dec-language number function = Left (scalar-function number)
dec-language number (function-ok t) = Left (scalar-function-ok number)
dec-language number (function-err t) = Right (scalar-function-err number)
dec-language number (function-err t) = Left (scalar-function-err number)
dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
dec-language string (scalar string) = Right (scalar string)
dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
dec-language string function = Left (scalar-function string)
dec-language string (function-ok t) = Left (scalar-function-ok string)
dec-language string (function-err t) = Right (scalar-function-err string)
dec-language string (function-err t) = Left (scalar-function-err string)
dec-language (T₁ T₂) (scalar s) = Left (function-scalar s)
dec-language (T₁ T₂) function = Right function
dec-language (T₁ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t)
@ -73,6 +74,11 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-impl-¬≮: : {T U} (T <: U) ¬(T ≮: U)
<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)
<:-impl-⊇ : {T U} (T <: U) t ¬Language U t ¬Language T t
<:-impl-⊇ {T} p t q with dec-language T t
<:-impl-⊇ {_} p t q | Left r = r
<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r))
-- reflexivity
≮:-refl : {T} ¬(T ≮: T)
:-refl (witness t p q) = language-comp t q p
@ -91,10 +97,162 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z witness t z q) (dec-language T t)
<:-trans : {S T U} (S <: T) (T <: U) (S <: U)
<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ≮:-trans)
<:-trans p q t r = q t (p t r)
<:-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))
<:-union p q t (left r) = left (p t r)
<:-union p q t (right r) = right (q t r)
<:--left : {S T} S <: (S T)
<:--left t p = left p
<:--right : {S T} T <: (S T)
<:--right t p = right p
<:--lub : {S T U} (S <: U) (T <: U) ((S T) <: U)
<:--lub p q t (left r) = p t r
<:--lub p q t (right r) = q t r
<:--symm : {T U} (T U) <: (U T)
<:--symm t (left p) = right p
<:--symm t (right p) = left p
<:--assocl : {S T U} (S (T U)) <: ((S T) U)
<:--assocl t (left p) = left (left p)
<:--assocl t (right (left p)) = left (right p)
<:--assocl t (right (right p)) = right p
<:--assocr : {S T U} ((S T) U) <: (S (T U))
<:--assocr t (left (left p)) = left p
<:--assocr t (left (right p)) = right (left p)
<:--assocr t (right p) = right (right p)
≮:--left : {S T U} (S ≮: U) ((S T) ≮: U)
:--left (witness t p q) = witness t (left p) q
≮:--right : {S T U} (T ≮: U) ((S T) ≮: U)
:--right (witness t p q) = witness t (right p) q
-- Properties of intersection
<:-intersect : {R S T U} (R <: T) (S <: U) ((R S) <: (T U))
<:-intersect p q t (r₁ , r₂) = (p t r₁ , q t r₂)
<:-∩-left : {S T} (S T) <: S
<:-∩-left t (p , _) = p
<:-∩-right : {S T} (S T) <: T
<:-∩-right t (_ , p) = p
<:-∩-glb : {S T U} (S <: T) (S <: U) (S <: (T U))
<:-∩-glb p q t r = (p t r , q t r)
<:-∩-symm : {T U} (T U) <: (U T)
<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
≮:-∩-left : {S T U} (S ≮: T) (S ≮: (T U))
:-∩-left (witness t p q) = witness t p (left q)
≮:-∩-right : {S T U} (S ≮: U) (S ≮: (T U))
:-∩-right (witness t p q) = witness t p (right q)
-- Distribution properties
<:-∩-distl- : {S T U} (S (T U)) <: ((S T) (S U))
<:-∩-distl- t (p₁ , left p₂) = left (p₁ , p₂)
<:-∩-distl- t (p₁ , right p₂) = right (p₁ , p₂)
∩-distl--<: : {S T U} ((S T) (S U)) <: (S (T U))
∩-distl--<: t (left (p₁ , p₂)) = (p₁ , left p₂)
∩-distl--<: t (right (p₁ , p₂)) = (p₁ , right p₂)
<:-∩-distr- : {S T U} ((S T) U) <: ((S U) (T U))
<:-∩-distr- t (left p₁ , p₂) = left (p₁ , p₂)
<:-∩-distr- t (right p₁ , p₂) = right (p₁ , p₂)
∩-distr--<: : {S T U} ((S U) (T U)) <: ((S T) U)
∩-distr--<: t (left (p₁ , p₂)) = (left p₁ , p₂)
∩-distr--<: t (right (p₁ , p₂)) = (right p₁ , p₂)
<:--distl-∩ : {S T U} (S (T U)) <: ((S T) (S U))
<:--distl-∩ t (left p) = (left p , left p)
<:--distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)
-distl-∩-<: : {S T U} ((S T) (S U)) <: (S (T U))
-distl-∩-<: t (left p₁ , p₂) = left p₁
-distl-∩-<: t (right p₁ , left p₂) = left p₂
-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)
<:--distr-∩ : {S T U} ((S T) U) <: ((S U) (T U))
<:--distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂
<:--distr-∩ t (right p) = (right p , right p)
-distr-∩-<: : {S T U} ((S U) (T U)) <: ((S T) U)
-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂)
-distr-∩-<: t (left p₁ , right p₂) = right p₂
-distr-∩-<: t (right p₁ , p₂) = right p₁
-- Properties of functions
<:-function : {R S T U} (R <: S) (T <: U) (S T) <: (R U)
<:-function p q function function = function
<:-function p q (function-ok 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-∩- : {R S T U} ((R T) (S U)) <: ((R S) (T U))
<:-function-∩- function (function , function) = function
<:-function-∩- (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (right p₂)
<:-function-∩- (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
<:-function-∩ : {S T U} ((S T) (S U)) <: (S (T U))
<:-function-∩ function (function , function) = function
<:-function-∩ (function-ok 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- : {R S T U} ((R S) (T U)) <: ((R T) (S U))
<:-function- function (left function) = function
<:-function- (function-ok t) (left (function-ok p)) = function-ok (left p)
<:-function- (function-err s) (left (function-err p)) = function-err (left p)
<:-function- (scalar s) (left (scalar ()))
<:-function- function (right function) = function
<:-function- (function-ok 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--∩ : {R S T U} ((R S) (T U)) <: ((R T) (S U))
<:-function--∩ function function = left function
<:-function--∩ (function-ok t) (function-ok (left p)) = left (function-ok p)
<:-function--∩ (function-ok 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-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 = number (string (nil boolean))
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)
scalar-∩-function-<:-never string .(scalar string) (() , scalar string)
scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil)
function-≮:-scalar : {S T U} (Scalar U) ((S T) ≮: U)
function-≮:-scalar s = witness function function (scalar-function s)
@ -111,28 +269,8 @@ scalar-≮:-never s = witness (scalar s) (scalar s) never
scalar-≢-impl-≮: : {T U} (Scalar T) (Scalar U) (T U) (T ≮: U)
scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)
-- Properties of tgt
tgt-function-ok : {T t} (Language (tgt T) t) Language T (function-ok t)
tgt-function-ok {T = nil} (scalar ())
tgt-function-ok {T = T₁ T₂} p = function-ok p
tgt-function-ok {T = never} (scalar ())
tgt-function-ok {T = unknown} p = unknown
tgt-function-ok {T = boolean} (scalar ())
tgt-function-ok {T = number} (scalar ())
tgt-function-ok {T = string} (scalar ())
tgt-function-ok {T = T₁ T₂} (left p) = left (tgt-function-ok p)
tgt-function-ok {T = T₁ T₂} (right p) = right (tgt-function-ok p)
tgt-function-ok {T = T₁ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)
function-ok-tgt : {T t} Language T (function-ok t) (Language (tgt T) t)
function-ok-tgt (function-ok p) = p
function-ok-tgt (left p) = left (function-ok-tgt p)
function-ok-tgt (right p) = right (function-ok-tgt p)
function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
function-ok-tgt unknown = unknown
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-≢-∩-<:-never : {T U V} (Scalar T) (Scalar U) (T U) (T U) <: V
scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl)
skalar-scalar : {T} (s : Scalar T) (Language skalar (scalar s))
skalar-scalar number = left (scalar number)
@ -140,72 +278,6 @@ skalar-scalar boolean = right (right (right (scalar boolean)))
skalar-scalar string = right (left (scalar string))
skalar-scalar nil = right (right (left (scalar nil)))
tgt-never-≮: : {T U} (tgt T ≮: U) (T ≮: (skalar (never U)))
tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)
never-tgt-≮: : {T U} (T ≮: (skalar (never U))) (tgt T ≮: U)
never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
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 ())))
-- Properties of src
function-err-src : {T t} (¬Language (src T) t) Language T (function-err t)
function-err-src {T = nil} never = scalar-function-err nil
function-err-src {T = T₁ T₂} p = function-err p
function-err-src {T = never} (scalar-scalar number () p)
function-err-src {T = never} (scalar-function-ok ())
function-err-src {T = unknown} never = unknown
function-err-src {T = boolean} p = scalar-function-err boolean
function-err-src {T = number} p = scalar-function-err number
function-err-src {T = string} p = scalar-function-err string
function-err-src {T = T₁ T₂} (left p) = left (function-err-src p)
function-err-src {T = T₁ T₂} (right p) = right (function-err-src p)
function-err-src {T = T₁ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂
¬function-err-src : {T t} (Language (src T) t) ¬Language T (function-err t)
¬function-err-src {T = nil} (scalar ())
¬function-err-src {T = T₁ T₂} p = function-err p
¬function-err-src {T = never} unknown = never
¬function-err-src {T = unknown} (scalar ())
¬function-err-src {T = boolean} (scalar ())
¬function-err-src {T = number} (scalar ())
¬function-err-src {T = string} (scalar ())
¬function-err-src {T = T₁ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂)
¬function-err-src {T = T₁ T₂} (left p) = left (¬function-err-src p)
¬function-err-src {T = T₁ T₂} (right p) = right (¬function-err-src p)
src-¬function-err : {T t} Language T (function-err t) (¬Language (src T) t)
src-¬function-err {T = nil} p = never
src-¬function-err {T = T₁ T₂} (function-err p) = p
src-¬function-err {T = never} (scalar-function-err ())
src-¬function-err {T = unknown} p = never
src-¬function-err {T = boolean} p = never
src-¬function-err {T = number} p = never
src-¬function-err {T = string} p = never
src-¬function-err {T = T₁ T₂} (left p) = left (src-¬function-err p)
src-¬function-err {T = T₁ T₂} (right p) = right (src-¬function-err p)
src-¬function-err {T = T₁ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂)
src-¬scalar : {S T t} (s : Scalar S) Language T (scalar s) (¬Language (src T) t)
src-¬scalar number (scalar number) = never
src-¬scalar boolean (scalar boolean) = never
src-¬scalar string (scalar string) = never
src-¬scalar nil (scalar nil) = never
src-¬scalar s (left p) = left (src-¬scalar s p)
src-¬scalar s (right p) = right (src-¬scalar s p)
src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂)
src-¬scalar s unknown = never
src-unknown-≮: : {T U} (T ≮: src U) (U ≮: (T unknown))
src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)
unknown-src-≮: : {S T U} (U ≮: S) (T ≮: (U unknown)) (U ≮: src T)
unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
-- Properties of unknown and never
unknown-≮: : {T U} (T ≮: U) (unknown ≮: U)
unknown-≮: (witness t p q) = witness t unknown q
@ -219,6 +291,28 @@ unknown-≮:-never = witness (scalar nil) unknown never
function-≮:-never : {T U} ((T U) ≮: never)
function-≮:-never = witness function function never
<:-never : {T} (never <: T)
<:-never t (scalar ())
≮:-never-left : {S T U} (S <: (T U)) (S ≮: T) (S U) ≮: never
:-never-left p (witness t q₁ q₂) with p t q₁
:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r)
:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never
≮:-never-right : {S T U} (S <: (T U)) (S ≮: U) (S T) ≮: never
:-never-right p (witness t q₁ q₂) with p t q₁
:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never
:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r)
<:-unknown : {T} (T <: unknown)
<:-unknown t p = unknown
<:-everything : unknown <: ((never unknown) skalar)
<:-everything (scalar s) p = right (skalar-scalar s)
<:-everything function p = left function
<:-everything (function-ok t) p = left (function-ok unknown)
<:-everything (function-err s) p = left (function-err never)
-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
-- defines a "set-theoretic" model (sec 2.5)
-- Unfortunately we don't quite have this property, due to uninhabited types,
@ -234,13 +328,21 @@ _⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set)
Comp : {A : Set} (A Set) (A Set)
Comp P a = ¬(P a)
Lift : {A : Set} (A Set) (Maybe A Set)
Lift P nothing =
Lift P (just a) = P a
set-theoretic-if : {S₁ T₁ S₂ T₂}
-- This is the "if" part of being a set-theoretic model
-- though it uses the definition from Frisch's thesis
-- rather than from the Gentle Introduction. The difference
-- being the presence of Lift, (written D_Ω in Defn 4.2 of
-- https://www.cduce.org/papers/frisch_phd.pdf).
(Language (S₁ T₁) Language (S₂ T₂))
( Q Q Comp((Language S₁) Comp(Language T₁)) Q Comp((Language S₂) Comp(Language T₂)))
( Q Q Comp((Language S₁) Comp(Lift(Language T₁))) Q Comp((Language S₂) Comp(Lift(Language T₂))))
set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) = q (t , u) Qtu (S₁t , ¬T₁u) where
set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T₂u) = q (t , just u) Qtu (S₁t , ¬T₁u) where
S₁t : Language S₁ t
S₁t with dec-language S₁ t
@ -252,6 +354,14 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u)
¬T₁u T₁u with p (function-ok u) (function-ok T₁u)
¬T₁u T₁u | function-ok T₂u = ¬T₂u T₂u
set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where
S₁t : Language S₁ t
S₁t with dec-language S₁ t
S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
S₁t | Right r = r
not-quite-set-theoretic-only-if : {S₁ T₁ S₂ T₂}
-- We don't quite have that this is a set-theoretic model
@ -260,32 +370,33 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
s₂ t₂ Language S₂ s₂ ¬Language T₂ t₂
-- This is the "only if" part of being a set-theoretic model
( Q Q Comp((Language S₁) Comp(Language T₁)) Q Comp((Language S₂) Comp(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₂))
not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where
Q : (Tree × Tree) Set
Q (t , u) = Either (¬Language S₁ t) (Language T₁ u)
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(Language T₁))
q (t , u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
q (t , u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
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 t) (function-err ¬S₁t) with dec-language S₂ t
r (function-err t) (function-err ¬S₁t) | Left ¬S₂t = function-err ¬S₂t
r (function-err t) (function-err ¬S₁t) | Right S₂t = CONTRADICTION (p Q q (t , t₂) (Left ¬S₁t) (S₂t , language-comp t₂ ¬T₂t₂))
r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
r (function-err s) (function-err ¬S₁s) | Left ¬S₂s = function-err ¬S₂s
r (function-err s) (function-err ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
r (function-ok t) (function-ok T₁t) with dec-language T₂ t
r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
r (function-ok t) (function-ok T₁t) | Right T₂t = function-ok 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 Comp((Language never) Comp(Lift(Language number))) Q Comp((Language never) Comp(Lift(Language string))))
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p)
set-theoretic-counterexample-two : (never number) ≮: (never string)
set-theoretic-counterexample-two = witness

View File

@ -8,7 +8,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Either using (Either)
open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp)
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; src; tgt)
open import Luau.FunctionTypes using (src; tgt)
open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.Addr using (Addr)

View File

@ -0,0 +1,376 @@
{-# OPTIONS --rewriting #-}
module Properties.TypeNormalization where
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; __; _∩_)
open import Luau.Subtyping using (scalar-function-err)
open import Luau.TypeNormalization using (_ⁿ_; _∩ⁿ_; _ᶠ_; _ⁿˢ_; _∩ⁿˢ_; normalize)
open import Luau.Subtyping using (_<:_)
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)
-- Notmal forms for types
data FunType : Type Set
data Normal : Type Set
data FunType where
_⇒_ : {S T} Normal S Normal T FunType (S T)
_∩_ : {F G} FunType F FunType G FunType (F G)
data Normal where
never : Normal never
unknown : Normal unknown
_⇒_ : {S T} Normal S Normal T Normal (S T)
_∩_ : {F G} FunType F FunType G Normal (F G)
__ : {S T} Normal S Scalar T Normal (S T)
data OptScalar : Type Set where
never : OptScalar never
number : OptScalar number
boolean : OptScalar boolean
string : OptScalar string
nil : OptScalar nil
-- Normalization produces normal types
normal : T Normal (normalize T)
normalᶠ : {F} FunType F Normal F
normal-∪ⁿ : {S T} Normal S Normal T Normal (S ∪ⁿ T)
normal-∩ⁿ : {S T} Normal S Normal T Normal (S ∩ⁿ T)
normal-∪ⁿˢ : {S T} Normal S OptScalar T Normal (S ∪ⁿˢ T)
normal-∩ⁿˢ : {S T} Normal S Scalar T OptScalar (S ∩ⁿˢ T)
normal-∪ᶠ : {F G} FunType F FunType G FunType (F ∪ᶠ G)
normal nil = never nil
normal (S T) = normalᶠ ((normal S) (normal T))
normal never = never
normal unknown = unknown
normal boolean = never boolean
normal number = never number
normal string = never string
normal (S T) = normal-∪ⁿ (normal S) (normal T)
normal (S T) = normal-∩ⁿ (normal S) (normal T)
normalᶠ (S T) = S T
normalᶠ (F G) = F G
normal-∪ⁿ S (T₁ T₂) = (normal-∪ⁿ S T₁) T₂
normal-∪ⁿ S never = S
normal-∪ⁿ S unknown = unknown
normal-∪ⁿ never (T U) = T U
normal-∪ⁿ never (G₁ G₂) = G₁ G₂
normal-∪ⁿ unknown (T U) = unknown
normal-∪ⁿ unknown (G₁ G₂) = unknown
normal-∪ⁿ (R S) (T U) = normalᶠ (normal-∪ᶠ (R S) (T U))
normal-∪ⁿ (R S) (G₁ G₂) = normalᶠ (normal-∪ᶠ (R S) (G₁ G₂))
normal-∪ⁿ (F₁ F₂) (T U) = normalᶠ (normal-∪ᶠ (F₁ F₂) (T U))
normal-∪ⁿ (F₁ F₂) (G₁ G₂) = normalᶠ (normal-∪ᶠ (F₁ F₂) (G₁ G₂))
normal-∪ⁿ (S₁ S₂) (T₁ T₂) = normal-∪ⁿ S₁ (T₁ T₂) S₂
normal-∪ⁿ (S₁ S₂) (G₁ G₂) = normal-∪ⁿ S₁ (G₁ G₂) S₂
normal-∩ⁿ S never = never
normal-∩ⁿ S unknown = S
normal-∩ⁿ S (T U) = normal-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U )
normal-∩ⁿ never (T U) = never
normal-∩ⁿ unknown (T U) = T U
normal-∩ⁿ (R S) (T U) = (R S) (T U)
normal-∩ⁿ (R S) (T U) = (R S) (T U)
normal-∩ⁿ (R S) (T U) = normal-∩ⁿ R (T U)
normal-∩ⁿ never (T U) = never
normal-∩ⁿ unknown (T U) = T U
normal-∩ⁿ (R S) (T U) = (R S) (T U)
normal-∩ⁿ (R S) (T U) = (R S) (T U)
normal-∩ⁿ (R S) (T U) = normal-∩ⁿ R (T U)
normal-∪ⁿˢ S never = S
normal-∪ⁿˢ never number = never number
normal-∪ⁿˢ unknown number = unknown
normal-∪ⁿˢ (R S) number = (R S) number
normal-∪ⁿˢ (R S) number = (R S) number
normal-∪ⁿˢ (R number) number = R number
normal-∪ⁿˢ (R boolean) number = normal-∪ⁿˢ R number boolean
normal-∪ⁿˢ (R string) number = normal-∪ⁿˢ R number string
normal-∪ⁿˢ (R nil) number = normal-∪ⁿˢ R number nil
normal-∪ⁿˢ never boolean = never boolean
normal-∪ⁿˢ unknown boolean = unknown
normal-∪ⁿˢ (R S) boolean = (R S) boolean
normal-∪ⁿˢ (R S) boolean = (R S) boolean
normal-∪ⁿˢ (R number) boolean = normal-∪ⁿˢ R boolean number
normal-∪ⁿˢ (R boolean) boolean = R boolean
normal-∪ⁿˢ (R string) boolean = normal-∪ⁿˢ R boolean string
normal-∪ⁿˢ (R nil) boolean = normal-∪ⁿˢ R boolean nil
normal-∪ⁿˢ never string = never string
normal-∪ⁿˢ unknown string = unknown
normal-∪ⁿˢ (R S) string = (R S) string
normal-∪ⁿˢ (R S) string = (R S) string
normal-∪ⁿˢ (R number) string = normal-∪ⁿˢ R string number
normal-∪ⁿˢ (R boolean) string = normal-∪ⁿˢ R string boolean
normal-∪ⁿˢ (R string) string = R string
normal-∪ⁿˢ (R nil) string = normal-∪ⁿˢ R string nil
normal-∪ⁿˢ never nil = never nil
normal-∪ⁿˢ unknown nil = unknown
normal-∪ⁿˢ (R S) nil = (R S) nil
normal-∪ⁿˢ (R S) nil = (R S) nil
normal-∪ⁿˢ (R number) nil = normal-∪ⁿˢ R nil number
normal-∪ⁿˢ (R boolean) nil = normal-∪ⁿˢ R nil boolean
normal-∪ⁿˢ (R string) nil = normal-∪ⁿˢ R nil string
normal-∪ⁿˢ (R nil) nil = R nil
normal-∩ⁿˢ never number = never
normal-∩ⁿˢ never boolean = never
normal-∩ⁿˢ never string = never
normal-∩ⁿˢ never nil = never
normal-∩ⁿˢ unknown number = number
normal-∩ⁿˢ unknown boolean = boolean
normal-∩ⁿˢ unknown string = string
normal-∩ⁿˢ unknown nil = nil
normal-∩ⁿˢ (R S) number = never
normal-∩ⁿˢ (R S) boolean = never
normal-∩ⁿˢ (R S) string = never
normal-∩ⁿˢ (R S) nil = never
normal-∩ⁿˢ (R S) number = never
normal-∩ⁿˢ (R S) boolean = never
normal-∩ⁿˢ (R S) string = never
normal-∩ⁿˢ (R S) nil = never
normal-∩ⁿˢ (R number) number = number
normal-∩ⁿˢ (R boolean) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R string) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R nil) number = normal-∩ⁿˢ R number
normal-∩ⁿˢ (R number) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R boolean) boolean = boolean
normal-∩ⁿˢ (R string) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R nil) boolean = normal-∩ⁿˢ R boolean
normal-∩ⁿˢ (R number) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R boolean) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R string) string = string
normal-∩ⁿˢ (R nil) string = normal-∩ⁿˢ R string
normal-∩ⁿˢ (R number) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R boolean) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R string) nil = normal-∩ⁿˢ R nil
normal-∩ⁿˢ (R nil) nil = nil
normal-∪ᶠ (R S) (T U) = (normal-∩ⁿ R T) (normal-∪ⁿ S U)
normal-∪ᶠ (R S) (G H) = normal-∪ᶠ (R S) G normal-∪ᶠ (R S) H
normal-∪ᶠ (E F) G = normal-∪ᶠ E G normal-∪ᶠ F G
scalar-∩-fun-<:-never : {F S} FunType F Scalar S (F S) <: never
scalar-∩-fun-<:-never (T U) S = scalar-∩-function-<:-never S
scalar-∩-fun-<:-never (F G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)
flipper : {S T U} ((S T) U) <: ((S U) T)
flipper = <:-trans <:--assocr (<:-trans (<:-union <:-refl <:--symm) <:--assocl)
∩-<:-∩ⁿ : {S T} Normal S Normal T (S T) <: (S ∩ⁿ T)
∩ⁿ-<:-∩ : {S T} Normal S Normal T (S ∩ⁿ T) <: (S T)
∩-<:-∩ⁿˢ : {S T} Normal S Scalar T (S T) <: (S ∩ⁿˢ T)
∩ⁿˢ-<:-∩ : {S T} Normal S Scalar T (S ∩ⁿˢ T) <: (S T)
∪ᶠ-<:- : {F G} FunType F FunType G (F ∪ᶠ G) <: (F G)
∪ⁿ-<:- : {S T} Normal S Normal T (S ∪ⁿ T) <: (S T)
-<:-∪ⁿ : {S T} Normal S Normal T (S T) <: (S ∪ⁿ T)
∪ⁿˢ-<:- : {S T} Normal S OptScalar T (S ∪ⁿˢ T) <: (S T)
-<:-∪ⁿˢ : {S T} Normal S OptScalar T (S T) <: (S ∪ⁿˢ T)
∩-<:-∩ⁿ S never = <:-∩-right
∩-<:-∩ⁿ S unknown = <:-∩-left
∩-<:-∩ⁿ S (T U) = <:-trans <:-∩-distl- (<:-trans (<:-union (∩-<:-∩ⁿ S T) (∩-<:-∩ⁿˢ S U)) (-<:-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) )
∩-<:-∩ⁿ never (T U) = <:-∩-left
∩-<:-∩ⁿ unknown (T U) = <:-∩-right
∩-<:-∩ⁿ (R S) (T U) = <:-refl
∩-<:-∩ⁿ (R S) (T U) = <:-refl
∩-<:-∩ⁿ (R S) (T U) = <:-trans <:-∩-distr- (<:-trans (<:-union (∩-<:-∩ⁿ R (T U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T U) S))) (<:--lub <:-refl <:-never))
∩-<:-∩ⁿ never (T U) = <:-∩-left
∩-<:-∩ⁿ unknown (T U) = <:-∩-right
∩-<:-∩ⁿ (R S) (T U) = <:-refl
∩-<:-∩ⁿ (R S) (T U) = <:-refl
∩-<:-∩ⁿ (R S) (T U) = <:-trans <:-∩-distr- (<:-trans (<:-union (∩-<:-∩ⁿ R (T U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T U) S))) (<:--lub <:-refl <:-never))
∩ⁿ-<:-∩ S never = <:-never
∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown
∩ⁿ-<:-∩ S (T U) = <:-trans (∪ⁿˢ-<:- (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) (<:-trans (<:-union (∩ⁿ-<:-∩ S T) (∩ⁿˢ-<:-∩ S U)) ∩-distl--<:)
∩ⁿ-<:-∩ never (T U) = <:-never
∩ⁿ-<:-∩ unknown (T U) = <:-∩-glb <:-unknown <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-trans (∩ⁿ-<:-∩ R (T U)) (<:-∩-glb (<:-trans <:-∩-left <:--left) <:-∩-right)
∩ⁿ-<:-∩ never (T U) = <:-never
∩ⁿ-<:-∩ unknown (T U) = <:-∩-glb <:-unknown <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-refl
∩ⁿ-<:-∩ (R S) (T U) = <:-trans (∩ⁿ-<:-∩ R (T U)) (<:-∩-glb (<:-trans <:-∩-left <:--left) <:-∩-right)
∩-<:-∩ⁿˢ never number = <:-∩-left
∩-<:-∩ⁿˢ never boolean = <:-∩-left
∩-<:-∩ⁿˢ never string = <:-∩-left
∩-<:-∩ⁿˢ never nil = <:-∩-left
∩-<:-∩ⁿˢ unknown T = <:-∩-right
∩-<:-∩ⁿˢ (R S) T = scalar-∩-fun-<:-never (R S) T
∩-<:-∩ⁿˢ (F G) T = scalar-∩-fun-<:-never (F G) T
∩-<:-∩ⁿˢ (R number) number = <:-∩-right
∩-<:-∩ⁿˢ (R boolean) number = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never boolean number (λ ())))
∩-<:-∩ⁿˢ (R string) number = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never string number (λ ())))
∩-<:-∩ⁿˢ (R nil) number = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never nil number (λ ())))
∩-<:-∩ⁿˢ (R number) boolean = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never number boolean (λ ())))
∩-<:-∩ⁿˢ (R boolean) boolean = <:-∩-right
∩-<:-∩ⁿˢ (R string) boolean = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never string boolean (λ ())))
∩-<:-∩ⁿˢ (R nil) boolean = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never nil boolean (λ ())))
∩-<:-∩ⁿˢ (R number) string = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never number string (λ ())))
∩-<:-∩ⁿˢ (R boolean) string = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never boolean string (λ ())))
∩-<:-∩ⁿˢ (R string) string = <:-∩-right
∩-<:-∩ⁿˢ (R nil) string = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never nil string (λ ())))
∩-<:-∩ⁿˢ (R number) nil = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never number nil (λ ())))
∩-<:-∩ⁿˢ (R boolean) nil = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never boolean nil (λ ())))
∩-<:-∩ⁿˢ (R string) nil = <:-trans <:-∩-distr- (<:--lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never string nil (λ ())))
∩-<:-∩ⁿˢ (R nil) nil = <:-∩-right
∩ⁿˢ-<:-∩ never T = <:-never
∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl
∩ⁿˢ-<:-∩ (R S) T = <:-never
∩ⁿˢ-<:-∩ (F G) T = <:-never
∩ⁿˢ-<:-∩ (R number) number = <:-∩-glb <:--right <:-refl
∩ⁿˢ-<:-∩ (R boolean) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R string) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R nil) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R number) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R boolean) boolean = <:-∩-glb <:--right <:-refl
∩ⁿˢ-<:-∩ (R string) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R nil) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R number) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R boolean) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R string) string = <:-∩-glb <:--right <:-refl
∩ⁿˢ-<:-∩ (R nil) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R number) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:--left <:-refl)
∩ⁿˢ-<:-∩ (R nil) nil = <:-∩-glb <:--right <:-refl
∪ᶠ-<:- (R S) (T U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:- S U)) <:-function--∩
∪ᶠ-<:- (R S) (G H) = <:-trans (<:-intersect (∪ᶠ-<:- (R S) G) (∪ᶠ-<:- (R S) H)) -distl-∩-<:
∪ᶠ-<:- (E F) G = <:-trans (<:-intersect (∪ᶠ-<:- E G) (∪ᶠ-<:- F G)) -distr-∩-<:
-<:-∪ᶠ : {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 <:--distl-∩ (<:-intersect (-<:-∪ᶠ (R S) G) (-<:-∪ᶠ (R S) H))
-<:-∪ᶠ (E F) G = <:-trans <:--distr-∩ (<:-intersect (-<:-∪ᶠ E G) (-<:-∪ᶠ F G))
∪ⁿˢ-<:- S never = <:--left
∪ⁿˢ-<:- never number = <:-refl
∪ⁿˢ-<:- never boolean = <:-refl
∪ⁿˢ-<:- never string = <:-refl
∪ⁿˢ-<:- never nil = <:-refl
∪ⁿˢ-<:- unknown number = <:--left
∪ⁿˢ-<:- unknown boolean = <:--left
∪ⁿˢ-<:- unknown string = <:--left
∪ⁿˢ-<:- unknown nil = <:--left
∪ⁿˢ-<:- (R S) number = <:-refl
∪ⁿˢ-<:- (R S) boolean = <:-refl
∪ⁿˢ-<:- (R S) string = <:-refl
∪ⁿˢ-<:- (R S) nil = <:-refl
∪ⁿˢ-<:- (R S) number = <:-refl
∪ⁿˢ-<:- (R S) boolean = <:-refl
∪ⁿˢ-<:- (R S) string = <:-refl
∪ⁿˢ-<:- (R S) nil = <:-refl
∪ⁿˢ-<:- (R number) number = <:-union <:--left <:-refl
∪ⁿˢ-<:- (R boolean) number = <:-trans (<:-union (∪ⁿˢ-<:- R number) <:-refl) flipper
∪ⁿˢ-<:- (R string) number = <:-trans (<:-union (∪ⁿˢ-<:- R number) <:-refl) flipper
∪ⁿˢ-<:- (R nil) number = <:-trans (<:-union (∪ⁿˢ-<:- R number) <:-refl) flipper
∪ⁿˢ-<:- (R number) boolean = <:-trans (<:-union (∪ⁿˢ-<:- R boolean) <:-refl) flipper
∪ⁿˢ-<:- (R boolean) boolean = <:-union <:--left <:-refl
∪ⁿˢ-<:- (R string) boolean = <:-trans (<:-union (∪ⁿˢ-<:- R boolean) <:-refl) flipper
∪ⁿˢ-<:- (R nil) boolean = <:-trans (<:-union (∪ⁿˢ-<:- R boolean) <:-refl) flipper
∪ⁿˢ-<:- (R number) string = <:-trans (<:-union (∪ⁿˢ-<:- R string) <:-refl) flipper
∪ⁿˢ-<:- (R boolean) string = <:-trans (<:-union (∪ⁿˢ-<:- R string) <:-refl) flipper
∪ⁿˢ-<:- (R string) string = <:-union <:--left <:-refl
∪ⁿˢ-<:- (R nil) string = <:-trans (<:-union (∪ⁿˢ-<:- R string) <:-refl) flipper
∪ⁿˢ-<:- (R number) nil = <:-trans (<:-union (∪ⁿˢ-<:- R nil) <:-refl) flipper
∪ⁿˢ-<:- (R boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:- R nil) <:-refl) flipper
∪ⁿˢ-<:- (R string) nil = <:-trans (<:-union (∪ⁿˢ-<:- R nil) <:-refl) flipper
∪ⁿˢ-<:- (R nil) nil = <:-union <:--left <:-refl
-<:-∪ⁿˢ T never = <:--lub <:-refl <:-never
-<:-∪ⁿˢ never number = <:-refl
-<:-∪ⁿˢ never boolean = <:-refl
-<:-∪ⁿˢ never string = <:-refl
-<:-∪ⁿˢ never nil = <:-refl
-<:-∪ⁿˢ unknown number = <:-unknown
-<:-∪ⁿˢ unknown boolean = <:-unknown
-<:-∪ⁿˢ unknown string = <:-unknown
-<:-∪ⁿˢ unknown nil = <:-unknown
-<:-∪ⁿˢ (R S) number = <:-refl
-<:-∪ⁿˢ (R S) boolean = <:-refl
-<:-∪ⁿˢ (R S) string = <:-refl
-<:-∪ⁿˢ (R S) nil = <:-refl
-<:-∪ⁿˢ (R S) number = <:-refl
-<:-∪ⁿˢ (R S) boolean = <:-refl
-<:-∪ⁿˢ (R S) string = <:-refl
-<:-∪ⁿˢ (R S) nil = <:-refl
-<:-∪ⁿˢ (R number) number = <:--lub <:-refl <:--right
-<:-∪ⁿˢ (R boolean) number = <:-trans flipper (<:-union (-<:-∪ⁿˢ R number) <:-refl)
-<:-∪ⁿˢ (R string) number = <:-trans flipper (<:-union (-<:-∪ⁿˢ R number) <:-refl)
-<:-∪ⁿˢ (R nil) number = <:-trans flipper (<:-union (-<:-∪ⁿˢ R number) <:-refl)
-<:-∪ⁿˢ (R number) boolean = <:-trans flipper (<:-union (-<:-∪ⁿˢ R boolean) <:-refl)
-<:-∪ⁿˢ (R boolean) boolean = <:--lub <:-refl <:--right
-<:-∪ⁿˢ (R string) boolean = <:-trans flipper (<:-union (-<:-∪ⁿˢ R boolean) <:-refl)
-<:-∪ⁿˢ (R nil) boolean = <:-trans flipper (<:-union (-<:-∪ⁿˢ R boolean) <:-refl)
-<:-∪ⁿˢ (R number) string = <:-trans flipper (<:-union (-<:-∪ⁿˢ R string) <:-refl)
-<:-∪ⁿˢ (R boolean) string = <:-trans flipper (<:-union (-<:-∪ⁿˢ R string) <:-refl)
-<:-∪ⁿˢ (R string) string = <:--lub <:-refl <:--right
-<:-∪ⁿˢ (R nil) string = <:-trans flipper (<:-union (-<:-∪ⁿˢ R string) <:-refl)
-<:-∪ⁿˢ (R number) nil = <:-trans flipper (<:-union (-<:-∪ⁿˢ R nil) <:-refl)
-<:-∪ⁿˢ (R boolean) nil = <:-trans flipper (<:-union (-<:-∪ⁿˢ R nil) <:-refl)
-<:-∪ⁿˢ (R string) nil = <:-trans flipper (<:-union (-<:-∪ⁿˢ R nil) <:-refl)
-<:-∪ⁿˢ (R nil) nil = <:--lub <:-refl <:--right
∪ⁿ-<:- S never = <:--left
∪ⁿ-<:- S unknown = <:--right
∪ⁿ-<:- never (T U) = <:--right
∪ⁿ-<:- unknown (T U) = <:--left
∪ⁿ-<:- (R S) (T U) = ∪ᶠ-<:- (R S) (T U)
∪ⁿ-<:- (R S) (T U) = ∪ᶠ-<:- (R S) (T U)
∪ⁿ-<:- (R S) (T U) = <:-trans (<:-union (∪ⁿ-<:- R (T U)) <:-refl) (<:--lub (<:--lub (<:-trans <:--left <:--left) <:--right) (<:-trans <:--right <:--left))
∪ⁿ-<:- never (T U) = <:--right
∪ⁿ-<:- unknown (T U) = <:--left
∪ⁿ-<:- (R S) (T U) = ∪ᶠ-<:- (R S) (T U)
∪ⁿ-<:- (R S) (T U) = ∪ᶠ-<:- (R S) (T U)
∪ⁿ-<:- (R S) (T U) = <:-trans (<:-union (∪ⁿ-<:- R (T U)) <:-refl) (<:--lub (<:--lub (<:-trans <:--left <:--left) <:--right) (<:-trans <:--right <:--left))
∪ⁿ-<:- S (T U) = <:--lub (<:-trans (∪ⁿ-<:- S T) (<:-union <:-refl <:--left)) (<:-trans <:--right <:--right)
-<:-∪ⁿ S never = <:--lub <:-refl <:-never
-<:-∪ⁿ S unknown = <:-unknown
-<:-∪ⁿ never (T U) = <:--lub <:-never <:-refl
-<:-∪ⁿ unknown (T U) = <:-unknown
-<:-∪ⁿ (R S) (T U) = -<:-∪ᶠ (R S) (T U)
-<:-∪ⁿ (R S) (T U) = -<:-∪ᶠ (R S) (T U)
-<:-∪ⁿ (R S) (T U) = <:-trans <:--assocr (<:-trans (<:-union <:-refl <:--symm) (<:-trans <:--assocl (<:-union (-<:-∪ⁿ R (T U)) <:-refl)))
-<:-∪ⁿ never (T U) = <:--lub <:-never <:-refl
-<:-∪ⁿ unknown (T U) = <:-unknown
-<:-∪ⁿ (R S) (T U) = -<:-∪ᶠ (R S) (T U)
-<:-∪ⁿ (R S) (T U) = -<:-∪ᶠ (R S) (T U)
-<:-∪ⁿ (R S) (T U) = <:-trans <:--assocr (<:-trans (<:-union <:-refl <:--symm) (<:-trans <:--assocl (<:-union (-<:-∪ⁿ R (T U)) <:-refl)))
-<:-∪ⁿ never (T U) = <:-trans <:--assocl (<:-union (-<:-∪ⁿ never T) <:-refl)
-<:-∪ⁿ unknown (T U) = <:-trans <:--assocl (<:-union (-<:-∪ⁿ unknown T) <:-refl)
-<:-∪ⁿ (R S) (T U) = <:-trans <:--assocl (<:-union (-<:-∪ⁿ (R S) T) <:-refl)
-<:-∪ⁿ (R S) (T U) = <:-trans <:--assocl (<:-union (-<:-∪ⁿ (R S) T) <:-refl)
-<:-∪ⁿ (R S) (T U) = <:-trans <:--assocl (<:-union (-<:-∪ⁿ (R S) T) <:-refl)
normalize-<: : T normalize T <: T
<:-normalize : T T <: normalize T
<:-normalize nil = <:--right
<:-normalize (S T) = <:-function (normalize-<: S) (<:-normalize T)
<:-normalize never = <:-refl
<:-normalize unknown = <:-refl
<:-normalize boolean = <:--right
<:-normalize number = <:--right
<:-normalize string = <:--right
<:-normalize (S T) = <:-trans (<:-union (<:-normalize S) (<:-normalize T)) (-<:-∪ⁿ (normal S) (normal T))
<:-normalize (S T) = <:-trans (<:-intersect (<:-normalize S) (<:-normalize T)) (∩-<:-∩ⁿ (normal S) (normal T))
normalize-<: nil = <:--lub <:-never <:-refl
normalize-<: (S T) = <:-function (<:-normalize S) (normalize-<: T)
normalize-<: never = <:-refl
normalize-<: unknown = <:-refl
normalize-<: boolean = <:--lub <:-never <:-refl
normalize-<: number = <:--lub <:-never <:-refl
normalize-<: string = <:--lub <:-never <:-refl
normalize-<: (S T) = <:-trans (∪ⁿ-<:- (normal S) (normal T)) (<:-union (normalize-<: S) (normalize-<: T))
normalize-<: (S T) = <:-trans (∩ⁿ-<:-∩ (normal S) (normal T)) (<:-intersect (normalize-<: S) (normalize-<: T))