From 658fce4631e809d5e58ce0d1fecc0e55de506ffd Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 26 Apr 2022 13:32:42 -0500 Subject: [PATCH] WIP --- prototyping/Properties.agda | 1 + prototyping/Properties/Subtyping.agda | 9 +++++++++ prototyping/Properties/TypeNormalization.agda | 3 ++- 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index cad6ab07..6305ea53 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -6,6 +6,7 @@ import Properties.Contradiction import Properties.Dec import Properties.Equality import Properties.Functions +import Properties.FunctionTypes import Properties.Remember import Properties.Step import Properties.StrictMode diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 5a0f1efd..f9972ee8 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -230,6 +230,15 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp <:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p) -- 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-∩-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) diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda index 08a43cb0..4b069b47 100644 --- a/prototyping/Properties/TypeNormalization.agda +++ b/prototyping/Properties/TypeNormalization.agda @@ -2,7 +2,8 @@ module Properties.TypeNormalization where -open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src) +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)