From f625d798d10638b58abd2cead4ae86bd6231089f Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Mon, 6 Nov 2023 17:41:32 -0600 Subject: [PATCH 1/8] Tidying up presentation of subtyping --- Luau/Subtyping.agda | 20 +++++--- Properties/Subtyping.agda | 98 +++++++++++++++++++++++---------------- 2 files changed, 72 insertions(+), 46 deletions(-) diff --git a/Luau/Subtyping.agda b/Luau/Subtyping.agda index 6fcdf09..6f06613 100644 --- a/Luau/Subtyping.agda +++ b/Luau/Subtyping.agda @@ -17,7 +17,6 @@ data Value : Set data TypedValue where scalar : Scalar → TypedValue - warning : Value → TypedValue _↦_ : Arguments → Result → TypedValue data Arguments where @@ -29,9 +28,10 @@ data Arguments where data Result where - -- The effects we're tracking are causing a runtime error, a typecheck warning, + -- The effects we're tracking are causing a runtime error, an argument check failing, -- or diverging error : Result + check : Result diverge : Result ⟨_⟩ : TypedValue → Result @@ -46,13 +46,14 @@ data RLanguage : Type → Result → Set data ¬RLanguage : Type → Result → Set data ALanguage : Type → Arguments → Set data ¬ALanguage : Type → Arguments → Set +data ¬NoneCheck : Arguments → Result → Set data Language where scalar : ∀ T → Language (scalar T) ⟨ scalar T ⟩ function-nok : ∀ {T U t u} → (¬ALanguage T t) → Language (T ⇒ U) ⟨ t ↦ u ⟩ function-ok : ∀ {T U t u} → (RLanguage U u) → Language (T ⇒ U) ⟨ t ↦ u ⟩ - function-warning : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) ⟨ warning t ⟩ + function-none-check : ∀ {T U} → Language (T ⇒ U) ⟨ ⟨⟩ ↦ check ⟩ 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 @@ -63,11 +64,9 @@ data ¬Language where scalar-scalar : ∀ S T → (S ≢ T) → ¬Language (scalar T) ⟨ scalar S ⟩ scalar-function : ∀ S {t u} → ¬Language (scalar S) ⟨ t ↦ u ⟩ - scalar-warning : ∀ {T t} → ¬Language (scalar T) ⟨ warning t ⟩ scalar-error : ∀ S → ¬Language (scalar S) error function-scalar : ∀ S {T U} → ¬Language (T ⇒ U) ⟨ scalar S ⟩ - function-function : ∀ {T U t u} → (ALanguage T t) → (¬RLanguage U u) → ¬Language (T ⇒ U) ⟨ t ↦ u ⟩ - function-warning : ∀ {T U t} → Language T t → ¬Language (T ⇒ U) ⟨ warning t ⟩ + function-function : ∀ {T U t u} → (ALanguage T t) → (¬RLanguage U u) → (¬NoneCheck t u) → ¬Language (T ⇒ U) ⟨ t ↦ u ⟩ function-error : ∀ {T U} → ¬Language (T ⇒ U) error _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t @@ -84,6 +83,7 @@ data RLanguage where data ¬RLanguage where error : ∀ {T} → ¬Language T error → ¬RLanguage T error + check : ∀ {T} → ¬RLanguage T check one : ∀ {T t} → ¬Language T ⟨ t ⟩ → ¬RLanguage T ⟨ t ⟩ data ALanguage where @@ -97,6 +97,14 @@ data ¬ALanguage where untyped : ∀ {T} → ¬Language T error → ¬ALanguage T ⟨untyped⟩ one : ∀ {T t} → ¬Language T ⟨ t ⟩ → ¬ALanguage T ⟨ t ⟩ +data ¬NoneCheck where + + one₁ : ∀ {t u} → ¬NoneCheck ⟨ t ⟩ u + one₂ : ∀ {t u} → ¬NoneCheck t ⟨ u ⟩ + error : ∀ {t} → ¬NoneCheck t error + diverge : ∀ {t} → ¬NoneCheck t diverge + untyped : ∀ {u} → ¬NoneCheck ⟨untyped⟩ u + -- Subtyping as language inclusion _<:_ : Type → Type → Set diff --git a/Properties/Subtyping.agda b/Properties/Subtyping.agda index 77964bd..cfe1524 100644 --- a/Properties/Subtyping.agda +++ b/Properties/Subtyping.agda @@ -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 (_<:_; _≮:_; Value; Language; ¬Language; ALanguage; ¬ALanguage; RLanguage; ¬RLanguage; witness; any; never; scalar; scalar-function; scalar-scalar; scalar-error; scalar-warning; function-scalar; function-ok; function-nok; function-error; function-function; function-warning; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; error; warning; diverge; ⟨untyped⟩; one; none; untyped) +open import Luau.Subtyping using (_<:_; _≮:_; Value; Language; ¬Language; ALanguage; ¬ALanguage; RLanguage; ¬RLanguage; witness; any; never; scalar; scalar-function; scalar-scalar; scalar-error; function-scalar; function-ok; function-nok; function-error; function-function; function-none-check; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; error; check; diverge; ⟨untyped⟩; one; one₁; one₂; none; untyped) open import Luau.Type using (Type; Scalar; scalar; error; never; unknown; funktion;_⇒_; _∪_; _∩_; any; number; string; NIL; NUMBER; STRING; BOOLEAN; _≡ˢ_) open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥) open import Properties.Dec using (Dec; yes; no) @@ -15,8 +15,8 @@ open import Properties.Product using (_×_; _,_) -- Language membership is decidable dec-language : ∀ T t → Either (¬Language T t) (Language T t) -dec-alanguage : ∀ T t → Either (¬ALanguage T t) (ALanguage T t) -dec-rlanguage : ∀ T t → Either (¬RLanguage T t) (RLanguage T t) +-- dec-alanguage : ∀ T t → Either (¬ALanguage T t) (ALanguage T t) +-- dec-rlanguage : ∀ T t → Either (¬RLanguage T t) (RLanguage T t) dec-language (scalar S) error = Left (scalar-error S) dec-language (scalar S) ⟨ scalar T ⟩ with T ≡ˢ S @@ -24,24 +24,41 @@ dec-language (scalar S) ⟨ scalar T ⟩ | yes refl = Right (scalar S) dec-language (scalar S) ⟨ scalar T ⟩ | no p = Left (scalar-scalar T S p) dec-language (scalar S) ⟨ s ↦ t ⟩ = Left (scalar-function S) dec-language (S ⇒ T) ⟨ scalar s ⟩ = Left (function-scalar s) -dec-language (S ⇒ T) ⟨ s ↦ t ⟩ = cond (Right ∘ function-nok) (λ p → mapLR (function-function p) function-ok (dec-rlanguage T t)) (dec-alanguage S s) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ t ⟩ with dec-language S error +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ t ⟩ | Left p = Right (function-nok (untyped p)) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ error ⟩ | Right p with dec-language T error +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ error ⟩ | Right p | Left q = Left (function-function (untyped p) (error q) error) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ error ⟩ | Right p | Right q = Right (function-ok (error q)) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ check ⟩ | Right p = Left (function-function (untyped p) check untyped) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ diverge ⟩ | Right p = Right (function-ok diverge) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ ⟨ t ⟩ ⟩ | Right p with dec-language T ⟨ t ⟩ +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ ⟨ t ⟩ ⟩ | Right p | Left q = Left (function-function (untyped p) (one q) one₂) +dec-language (S ⇒ T) ⟨ ⟨untyped⟩ ↦ ⟨ t ⟩ ⟩ | Right p | Right q = Right (function-ok (one q)) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ t ⟩ with dec-language S ⟨ s ⟩ +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ t ⟩ | Left p = Right (function-nok (one p)) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ error ⟩ | Right p with dec-language T error +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ error ⟩ | Right p | Left q = Left (function-function (one p) (error q) one₁) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ error ⟩ | Right p | Right q = Right (function-ok (error q)) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ check ⟩ | Right p = Left (function-function (one p) check one₁) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ diverge ⟩ | Right p = Right (function-ok diverge) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ ⟨ t ⟩ ⟩ | Right p with dec-language T ⟨ t ⟩ +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ ⟨ t ⟩ ⟩ | Right p | Left q = Left (function-function (one p) (one q) one₁) +dec-language (S ⇒ T) ⟨ ⟨ s ⟩ ↦ ⟨ t ⟩ ⟩ | Right p | Right q = Right (function-ok (one q)) +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ error ⟩ with dec-language T error +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ error ⟩ | Left q = Left (function-function none (error q) error) +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ error ⟩ | Right q = Right (function-ok (error q)) +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ check ⟩ = Right function-none-check +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ diverge ⟩ = Right (function-ok diverge) +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩ with dec-language T ⟨ t ⟩ +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩ | Left q = Left (function-function none (one q) one₂) +dec-language (S ⇒ T) ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩ | Right q = Right (function-ok (one q)) +dec-language (S ⇒ T) error = Left function-error dec-language never t = Left never dec-language any t = Right any dec-language (S ∪ T) t = cond (λ p → mapLR (_,_ p) right (dec-language T t)) (Right ∘ left) (dec-language S t) dec-language (S ∩ T) t = cond (Left ∘ left) (λ p → mapLR right (_,_ p) (dec-language T t)) (dec-language S t) -dec-language (T ⇒ T₁) error = Left function-error dec-language error error = Right error dec-language error ⟨ t ⟩ = Left error -dec-language (scalar S) ⟨ warning t ⟩ = Left scalar-warning -dec-language (S ⇒ T) ⟨ warning t ⟩ = cond (Right ∘ function-warning) (Left ∘ function-warning) (dec-language S t) - -dec-alanguage T ⟨⟩ = Right none -dec-alanguage T ⟨untyped⟩ = mapLR untyped untyped (dec-language T error) -dec-alanguage T ⟨ t ⟩ = mapLR one one (dec-language T ⟨ t ⟩) - -dec-rlanguage T error = mapLR error error (dec-language T error) -dec-rlanguage T diverge = Right diverge -dec-rlanguage T ⟨ t ⟩ = mapLR one one (dec-language T ⟨ t ⟩) -- ¬Language T is the complement of Language T language-comp : ∀ {T t} → ¬Language T t → ¬(Language T t) @@ -50,11 +67,10 @@ language-comp (p₁ , p₂) (right q) = language-comp p₂ q language-comp (left p) (q₁ , q₂) = language-comp p q₁ language-comp (right p) (q₁ , q₂) = language-comp p q₂ language-comp (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl -language-comp (function-function (untyped p₁) p₂) (function-nok (untyped q)) = language-comp q p₁ -language-comp (function-function (one p₁) p₂) (function-nok (one q)) = language-comp q p₁ -language-comp (function-function p₁ (error p₂)) (function-ok (error q)) = language-comp p₂ q -language-comp (function-function p₁ (one p₂)) (function-ok (one q)) = language-comp p₂ q -language-comp (function-warning p) (function-warning q) = language-comp q p +language-comp (function-function (untyped p₁) p₂ p₃) (function-nok (untyped q)) = language-comp q p₁ +language-comp (function-function (one p₁) p₂ p₃) (function-nok (one q)) = language-comp q p₁ +language-comp (function-function p₁ (error p₂) p₃) (function-ok (error q)) = language-comp p₂ q +language-comp (function-function p₁ (one p₂) p₃) (function-ok (one q)) = language-comp p₂ q -- ≮: is the complement of <: ¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U) @@ -221,7 +237,7 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function p q (function-ok (one r)) = function-ok (one (q r)) <:-function p q (function-nok (untyped r)) = function-nok (untyped (<:-impl-⊇ p r)) <:-function p q (function-nok (one r)) = function-nok (one (<:-impl-⊇ p r)) -<:-function p q (function-warning r) = function-warning (<:-impl-⊇ p r) +<:-function p q function-none-check = function-none-check <:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U)) <:-function-∩-∩ (p , function-ok diverge) = function-ok diverge @@ -231,18 +247,18 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function-∩-∩ (p , function-nok (one q)) = function-nok (one (right q)) <:-function-∩-∩ (function-ok (error p) , function-ok (error q)) = function-ok (error (p , q)) <:-function-∩-∩ (function-ok (one p) , function-ok (one q)) = function-ok (one (p , q)) -<:-function-∩-∩ (function-warning p , q) = function-warning (left p) +<:-function-∩-∩ (function-none-check , function-none-check) = function-none-check <:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U)) <:-function-∩-∪ (p , function-ok (error q)) = function-ok (error (right q)) <:-function-∩-∪ (p , function-ok diverge) = function-ok diverge <:-function-∩-∪ (p , function-ok (one q)) = function-ok (one (right q)) +<:-function-∩-∪ (p , function-none-check) = function-none-check <:-function-∩-∪ (function-nok (untyped p) , function-nok (untyped q)) = function-nok (untyped (p , q)) <:-function-∩-∪ (function-nok (one p) , function-nok (one q)) = function-nok (one (p , q)) <:-function-∩-∪ (function-ok (error p) , q) = function-ok (error (left p)) <:-function-∩-∪ (function-ok diverge , q) = function-ok diverge <:-function-∩-∪ (function-ok (one p) , q) = function-ok (one (left p)) -<:-function-∩-∪ (function-warning p , function-warning q) = function-warning (p , q) <:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U)) <:-function-∩ (function-nok p , q) = function-nok p @@ -250,7 +266,7 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function-∩ (function-ok (error p) , function-ok (error q)) = function-ok (error (p , q)) <:-function-∩ (function-ok diverge , q) = function-ok diverge <:-function-∩ (function-ok (one p) , function-ok (one q)) = function-ok (one (p , q)) -<:-function-∩ (function-warning p , q) = function-warning p +<:-function-∩ (function-none-check , q) = function-none-check <:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U)) <:-function-∪ (left (function-nok (untyped p))) = function-nok (untyped (left p)) @@ -258,13 +274,13 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function-∪ (left (function-ok (error p))) = function-ok (error (left p)) <:-function-∪ (left (function-ok diverge)) = function-ok diverge <:-function-∪ (left (function-ok (one p))) = function-ok (one (left p)) -<:-function-∪ (left (function-warning p)) = function-warning (left p) +<:-function-∪ (left function-none-check) = function-none-check <:-function-∪ (right (function-nok (untyped p))) = function-nok (untyped (right p)) <:-function-∪ (right (function-nok (one p))) = function-nok (one (right p)) <:-function-∪ (right (function-ok (error p))) = function-ok (error (right p)) <:-function-∪ (right (function-ok diverge)) = function-ok diverge <:-function-∪ (right (function-ok (one p))) = function-ok (one (right p)) -<:-function-∪ (right (function-warning p)) = function-warning (right p) +<:-function-∪ (right function-none-check) = function-none-check <:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U)) <:-function-∪-∩ (function-nok (untyped (left p))) = left (function-nok (untyped p)) @@ -276,18 +292,17 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function-∪-∩ (function-ok diverge) = left (function-ok diverge) <:-function-∪-∩ (function-ok (one (left p))) = left (function-ok (one p)) <:-function-∪-∩ (function-ok (one (right p))) = right (function-ok (one p)) -<:-function-∪-∩ (function-warning (left p)) = left (function-warning p) -<:-function-∪-∩ (function-warning (right p)) = right (function-warning p) +<:-function-∪-∩ function-none-check = left function-none-check <:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S) <:-function-left {R} {S} p {error} Rs with dec-language S error <:-function-left {R} {S} p {error} Re | Right Se = Se -<:-function-left {R} {S} p {error} Re | Left ¬Se with p (function-warning ¬Se) -<:-function-left {R} {S} p {error} Re | Left ¬Se | function-warning ¬Re = CONTRADICTION (language-comp ¬Re Re) +<:-function-left {R} {S} p {error} Re | Left ¬Se with p (function-nok {u = check} (untyped ¬Se)) +<:-function-left {R} {S} p {error} Re | Left ¬Se | function-nok (untyped ¬Re) = CONTRADICTION (language-comp ¬Re Re) <:-function-left {R} {S} p {⟨ s ⟩} Rs with dec-language S ⟨ s ⟩ <:-function-left {R} {S} p {⟨ s ⟩} Rs | Right Ss = Ss -<:-function-left {R} {S} p {⟨ s ⟩} Rs | Left ¬Ss with p (function-warning ¬Ss) -<:-function-left {R} {S} p {⟨ s ⟩} Rs | Left ¬Ss | function-warning ¬Rs = CONTRADICTION (language-comp ¬Rs Rs) +<:-function-left {R} {S} p {⟨ s ⟩} Rs | Left ¬Ss with p (function-nok {u = check} (one ¬Ss)) +<:-function-left {R} {S} p {⟨ s ⟩} Rs | Left ¬Ss | function-nok (one ¬Rs) = CONTRADICTION (language-comp ¬Rs Rs) <:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (T <: U) <:-function-right p {error} Te with p (function-ok {t = ⟨⟩} (error Te)) @@ -296,11 +311,12 @@ language-comp (function-warning p) (function-warning q) = language-comp q p <:-function-right p {⟨ t ⟩} Tt | function-ok (one Ut) = Ut ≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U) -≮:-function-left (witness p q) = witness (function-warning q) (function-warning p) +≮:-function-left (witness {error} p q) = witness (function-nok (untyped q)) (function-function (untyped p) check untyped) +≮:-function-left (witness {⟨ s ⟩} p q) = witness (function-nok (one q)) (function-function (one p) check one₁) ≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U) -≮:-function-right (witness {error} p q) = witness (function-ok (error p)) (function-function none (error q)) -≮:-function-right (witness {⟨ s ⟩} p q) = witness (function-ok (one p)) (function-function none (one q)) +≮:-function-right (witness {error} p q) = witness (function-ok (error p)) (function-function none (error q) error) +≮:-function-right (witness {⟨ s ⟩} p q) = witness (function-ok (one p)) (function-function none (one q) one₂) function-<:-funktion : ∀ {S T} → (S ⇒ T) <: funktion function-<:-funktion = <:-function (λ ()) (λ p → any) @@ -399,12 +415,12 @@ function-≮:-never = witness (function-ok {t = ⟨⟩} diverge) never <:-everything {⟨ scalar BOOLEAN ⟩} p = left (right (scalar BOOLEAN)) <:-everything {⟨ scalar STRING ⟩} p = left (left (left (right (scalar STRING)))) <:-everything {⟨ scalar NIL ⟩} p = left (left (right (scalar NIL))) -<:-everything {⟨ warning t ⟩} p = left (left (left (left (left (function-warning never))))) <:-everything {⟨ ⟨⟩ ↦ error ⟩} p = left (left (left (left (left (function-ok (error any)))))) <:-everything {⟨ ⟨⟩ ↦ diverge ⟩} p = left (left (left (left (left (function-ok diverge))))) <:-everything {⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩} p = left (left (left (left (left (function-ok (one any)))))) <:-everything {⟨ ⟨untyped⟩ ↦ t ⟩} p = left (left (left (left (left (function-nok (untyped never)))))) <:-everything {⟨ ⟨ s ⟩ ↦ t ⟩} p = left (left (left (left (left (function-nok (one never)))))) +<:-everything {⟨ ⟨⟩ ↦ check ⟩} p = left (left (left (left (left function-none-check)))) -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf) -- defines a "set-theoretic" model (sec 2.5) @@ -439,8 +455,10 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) S₂⊆S₁ : Language S₂ ⊆ Language S₁ S₂⊆S₁ t S₂t with dec-language S₁ t - S₂⊆S₁ t S₂t | Left ¬S₁t with p ⟨ warning t ⟩ (function-warning ¬S₁t) - S₂⊆S₁ t S₂t | Left ¬S₁t | function-warning ¬S₂t = CONTRADICTION (language-comp ¬S₂t S₂t) + S₂⊆S₁ error S₂e | Left ¬S₁e with p ⟨ ⟨untyped⟩ ↦ check ⟩ (function-nok (untyped ¬S₁e)) + S₂⊆S₁ error S₂e | Left ¬S₁e | function-nok (untyped ¬S₂e) = CONTRADICTION (language-comp ¬S₂e S₂e) + S₂⊆S₁ ⟨ t ⟩ S₂t | Left ¬S₁t with p ⟨ ⟨ t ⟩ ↦ check ⟩ (function-nok (one ¬S₁t)) + S₂⊆S₁ ⟨ t ⟩ S₂t | Left ¬S₁t | function-nok (one ¬S₂t) = CONTRADICTION (language-comp ¬S₂t S₂t) S₂⊆S₁ t S₂t | Right S₁t = S₁t ¬T₂⊆¬T₁ : Comp(Lift(Language T₂)) ⊆ Comp(Lift(Language T₁)) @@ -482,12 +500,12 @@ not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ S₂s₂ p = r T₁⊆T₂ t T₁t | Right T₂t = T₂t r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂) - r ⟨ warning s ⟩ (function-warning ¬S₁s) = function-warning (¬S₁⊆¬S₂ s ¬S₁s) r ⟨ ⟨ s ⟩ ↦ t ⟩ (function-nok (one ¬S₁s)) = function-nok (one (¬S₁⊆¬S₂ ⟨ s ⟩ ¬S₁s)) r ⟨ s ↦ ⟨ t ⟩ ⟩ (function-ok (one T₁t)) = function-ok (one (T₁⊆T₂ ⟨ t ⟩ T₁t)) r ⟨ ⟨untyped⟩ ↦ t ⟩ (function-nok (untyped ¬S₁e)) = function-nok (untyped (¬S₁⊆¬S₂ error ¬S₁e)) r ⟨ s ↦ error ⟩ (function-ok (error T₁e)) = function-ok (error (T₁⊆T₂ error T₁e)) r ⟨ s ↦ diverge ⟩ p = function-ok diverge + r ⟨ ⟨⟩ ↦ check ⟩ p = function-none-check -- A counterexample when the argument type is empty. @@ -496,4 +514,4 @@ set-theoretic-counterexample-one Q q (⟨ scalar s ⟩ , u) Qtu (() , p) set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string) set-theoretic-counterexample-two = witness (function-ok (one (scalar NUMBER))) - (function-function none (one (scalar-scalar NUMBER STRING (λ ())))) + (function-function none (one (scalar-scalar NUMBER STRING (λ ()))) one₂) From de84e989434da1181b1c276b42e58c2869fb0802 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Tue, 7 Nov 2023 19:03:20 -0600 Subject: [PATCH 2/8] Properties of tidy subtypig --- Luau/ErrorSuppression.agda | 4 +-- Luau/StrictMode/ToString.agda | 7 +++-- Properties/DecSubtyping.agda | 17 +++++----- Properties/ResolveOverloads.agda | 52 +++++++++++++++++++++---------- Properties/TypeNormalization.agda | 6 ++-- 5 files changed, 53 insertions(+), 33 deletions(-) diff --git a/Luau/ErrorSuppression.agda b/Luau/ErrorSuppression.agda index 707a656..52f0971 100644 --- a/Luau/ErrorSuppression.agda +++ b/Luau/ErrorSuppression.agda @@ -5,7 +5,7 @@ module Luau.ErrorSuppression where open import Agda.Builtin.Unit using (⊤) open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond) open import Luau.Type using (Type; unknown; never; any; error; funktion; scalar; _⇒_; _∪_; _∩_) -open import Luau.Subtyping using (Value; TypedValue; Arguments; Result; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; warning; witness; ⟨untyped⟩; error; diverge; scalar; ⟨⟩) +open import Luau.Subtyping using (Value; TypedValue; Arguments; Result; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; check; witness; ⟨untyped⟩; error; diverge; scalar; ⟨⟩) open import Properties.Contradiction using (¬; ⊥) open import Properties.Product using (_×_) @@ -21,7 +21,6 @@ SuppressedValue T ⟨ t ⟩ = SuppressedTypedValue T t SuppressedTypedValue (scalar S) t = ⊥ SuppressedTypedValue (S ⇒ T) (scalar s) = ⊥ -SuppressedTypedValue (S ⇒ T) (warning s) = SuppressedValue S s SuppressedTypedValue (S ⇒ T) (s ↦ t) = Either (SuppressedArguments S s) (SuppressedResult T t) SuppressedTypedValue never t = ⊥ SuppressedTypedValue any t = ⊤ @@ -35,6 +34,7 @@ SuppressedArguments T ⟨ t ⟩ = SuppressedTypedValue T t SuppressedResult T error = Language T error SuppressedResult T diverge = ⊥ +SuppressedResult T check = ⊥ SuppressedResult T ⟨ t ⟩ = SuppressedTypedValue T t -- A subtyping failure which should not be suppressed diff --git a/Luau/StrictMode/ToString.agda b/Luau/StrictMode/ToString.agda index dabe2bd..a8a639a 100644 --- a/Luau/StrictMode/ToString.agda +++ b/Luau/StrictMode/ToString.agda @@ -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 (_≮:_; TypedValue; error; witness; scalar; warning; diverge; ⟨untyped⟩; function-ok; function-warning; _↦_; ⟨⟩; ⟨_⟩) +open import Luau.Subtyping using (_≮:_; TypedValue; error; witness; scalar; check; diverge; ⟨untyped⟩; function-ok; _↦_; ⟨⟩; ⟨_⟩) 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; NotFunctionCall; UnsafeFunction; UnsafeBlock; UnsafeLocal) open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; num; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name) open import Luau.Type using (NUMBER; BOOLEAN; STRING; NIL; _⇒_) @@ -29,13 +29,14 @@ valueToString (scalar STRING) n v = v ++ " is a string" valueToString (scalar NIL) n v = v ++ " is nil" valueToString (⟨ s ⟩ ↦ ⟨ t ⟩) n v = valueToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n " ++ valueToString s (suc n) w where w = tmp n valueToString (⟨⟩ ↦ ⟨ t ⟩) n v = valueToString t n (v ++ "()") -valueToString (warning ⟨ t ⟩) n v = v ++ "(" ++ w ++ ") can error when\n " ++ valueToString t (suc n) w where w = tmp n -valueToString (warning error) n v = v ++ "(" ++ w ++ ") can error when\n " ++ w ++ " is untyped" where w = tmp n +valueToString (⟨⟩ ↦ check) n v = v ++ "() can check that an argument is provided" valueToString (⟨⟩ ↦ error) n v = v ++ "() can error" valueToString (⟨⟩ ↦ diverge) n v = v ++ "() can diverge" +valueToString (⟨untyped⟩ ↦ check) n v = v ++ "(" ++ w ++ ") can fail a check when\n " ++ w ++ " is untyped" where w = tmp n valueToString (⟨untyped⟩ ↦ error) n v = v ++ "(" ++ w ++ ") can error when\n " ++ w ++ " is untyped" where w = tmp n valueToString (⟨untyped⟩ ↦ diverge) n v = v ++ "(" ++ w ++ ") can diverge when\n " ++ w ++ " is untyped" where w = tmp n valueToString (⟨untyped⟩ ↦ ⟨ t ⟩) n v = valueToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n " ++ w ++ " is untyped" where w = tmp n +valueToString (⟨ s ⟩ ↦ check) n v = v ++ "(" ++ w ++ ")" ++ "can fail a check when\n " ++ valueToString s (suc n) w where w = tmp n valueToString (⟨ s ⟩ ↦ error) n v = v ++ "(" ++ w ++ ")" ++ "can error when\n " ++ valueToString s (suc n) w where w = tmp n valueToString (⟨ s ⟩ ↦ diverge) n v = v ++ "(" ++ w ++ ")" ++ "can diverge when\n " ++ valueToString s (suc n) w where w = tmp n diff --git a/Properties/DecSubtyping.agda b/Properties/DecSubtyping.agda index e6cd056..a80515b 100644 --- a/Properties/DecSubtyping.agda +++ b/Properties/DecSubtyping.agda @@ -4,7 +4,7 @@ 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 (_<:_; _≮:_; Language; ¬Language; witness; any; never; scalar; error; warning; scalar-function; scalar-scalar; function-scalar; function-ok; function-nok; function-error; function-warning; function-function; none; one; untyped; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; ⟨untyped⟩) +open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; witness; any; never; scalar; error; scalar-function; scalar-scalar; function-scalar; function-ok; function-nok; function-error; function-function; none; one; one₁; one₂; check; untyped; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; ⟨untyped⟩) open import Luau.Type using (Type; Scalar; scalar; never; any; _⇒_; _∪_; _∩_) open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_) open import Luau.TypeSaturation using (saturate) @@ -51,7 +51,8 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ result : Top F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T)) result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-subtyping S Sᵗ - result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness Ss ¬Sᵗs) = Left (witness (ov-language Fᶠ (λ o → function-warning (<:-impl-⊇ (srcᵗ o) ¬Sᵗs))) (function-warning Ss)) + result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness {error} Se ¬Sᵗe) = Left (witness (ov-language Fᶠ (λ o → function-nok (untyped (<:-impl-⊇ (srcᵗ o) ¬Sᵗe)))) (function-function (untyped Se) check untyped)) + result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness {⟨ s ⟩} Ss ¬Sᵗs) = Left (witness (ov-language Fᶠ (λ o → function-nok (one (<:-impl-⊇ (srcᵗ o) ¬Sᵗs)))) (function-function (one Ss) check one₁)) result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where data LargestSrc (G : Type) : Set where @@ -90,8 +91,8 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ }) result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T)) - result₀ (no S₀ T₀ o₀ (witness {error} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ error ⟩} (ov-language Fᶠ (λ o → function-ok (error (tgt₀ o T₀t)))) (function-function none (error ¬Tt))) - result₀ (no S₀ T₀ o₀ (witness {⟨ t ⟩} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩} (ov-language Fᶠ (λ o → function-ok (one (tgt₀ o T₀t)))) (function-function none (one ¬Tt))) + result₀ (no S₀ T₀ o₀ (witness {error} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ error ⟩} (ov-language Fᶠ (λ o → function-ok (error (tgt₀ o T₀t)))) (function-function none (error ¬Tt) error)) + result₀ (no S₀ T₀ o₀ (witness {⟨ t ⟩} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩} (ov-language Fᶠ (λ o → function-ok (one (tgt₀ o T₀t)))) (function-function none (one ¬Tt) one₂)) result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtyping S S₀ result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right λ { here → defn o₀ S<:S₀ T₀<:T } result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Left (witness {s} Ss ¬S₀s) = Left (result₁ s Ss ¬S₀s (smallest Fᶠ (λ o → o))) where @@ -120,28 +121,28 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ result₁ : ∀ s → Language S s → ¬Language S₀ s → SmallestTgt F s → (F ≮: (S ⇒ T)) result₁ s Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) with dec-subtyping T₁ T result₁ s Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp ¬S₀s (src₀ o₁ T₁<:T S₁s)) - result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (error ¬Tt)) where + result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (error ¬Tt) error) where lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨untyped⟩ ↦ error ⟩ lemma {S′} {T′} o with dec-language S′ error lemma {S′} {T′} o | Left ¬S′e = function-nok (untyped ¬S′e) lemma {S′} {T′} o | Right S′e = function-ok (error (tgt₁ o S′e T₁t)) - result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (one ¬Tt)) where + result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (one ¬Tt) one₂) where lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨untyped⟩ ↦ ⟨ t ⟩ ⟩ lemma {S′} {T′} o with dec-language S′ error lemma {S′} {T′} o | Left ¬S′e = function-nok (untyped ¬S′e) lemma {S′} {T′} o | Right S′e = function-ok (one (tgt₁ o S′e T₁t)) - result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (error ¬Tt)) where + result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (error ¬Tt) one₁) where lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨ s ⟩ ↦ error ⟩ lemma {S′} {T′} o with dec-language S′ ⟨ s ⟩ lemma {S′} {T′} o | Left ¬S′s = function-nok (one ¬S′s) lemma {S′} {T′} o | Right S′s = function-ok (error (tgt₁ o S′s T₁t)) - result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (one ¬Tt)) where + result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (one ¬Tt) one₁) where lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨ s ⟩ ↦ ⟨ t ⟩ ⟩ lemma {S′} {T′} o with dec-language S′ ⟨ s ⟩ diff --git a/Properties/ResolveOverloads.agda b/Properties/ResolveOverloads.agda index a7c01bf..0823142 100644 --- a/Properties/ResolveOverloads.agda +++ b/Properties/ResolveOverloads.agda @@ -4,7 +4,7 @@ module Properties.ResolveOverloads where open import FFI.Data.Either using (Left; Right) open import Luau.ResolveOverloads using (Resolved; src; srcⁿ; resolve; resolveⁿ; resolveᶠ; resolveToˢ; target; yes; no) -open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; witness; scalar; any; never; function-ok; function-nok; function-scalar; function-warning; function-error; function-function; scalar-scalar; scalar-function; scalar-warning; scalar-error; _,_; left; right; _↦_; ⟨⟩; ⟨_⟩; warning; diverge; error; untyped; none; one) +open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; Value; TypedValue; witness; scalar; any; never; function-ok; function-nok; function-scalar; function-none-check; function-error; function-function; scalar-scalar; scalar-function; scalar-warning; scalar-error; _,_; left; right; _↦_; ⟨⟩; ⟨_⟩; warning; diverge; error; check; untyped; none; one; one₁; one₂; ⟨untyped⟩) open import Luau.Type using (Type ; Scalar; _⇒_; _∩_; _∪_; scalar; any; never; error; unknown; NUMBER; BOOLEAN; NIL; STRING) open import Luau.TypeSaturation using (saturate) open import Luau.TypeNormalization using (normalize) @@ -15,43 +15,57 @@ open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-t open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; scalar; error; <:-normalize; normalize-<:; fun-≮:-never; scalar-≮:-fun; error-≮:-fun) open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right) +warning : Value → TypedValue +warning error = ⟨untyped⟩ ↦ check +warning ⟨ t ⟩ = ⟨ t ⟩ ↦ check + -- Properties of src function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T ⟨ warning t ⟩ -function-err-srcⁿ (S ⇒ T) p = function-warning p +function-err-srcⁿ {t = error} (S ⇒ T) p = function-nok (untyped p) +function-err-srcⁿ {t = ⟨ t ⟩} (S ⇒ T) p = function-nok (one 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 ⟨ warning t ⟩ -¬function-err-srcᶠ (S ⇒ T) p = function-warning p +¬function-err-srcᶠ {t = error} (S ⇒ T) p = function-function (untyped p) check untyped +¬function-err-srcᶠ {t = ⟨ t ⟩} (S ⇒ T) p = function-function (one p) check one₁ ¬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 ⟨ warning t ⟩ ¬function-err-srcⁿ never p = never -¬function-err-srcⁿ (S ⇒ T) p = function-warning p +¬function-err-srcⁿ {t = error} (S ⇒ T) p = function-function (untyped p) check untyped +¬function-err-srcⁿ {t = ⟨ t ⟩} (S ⇒ T) p = function-function (one p) check one₁ ¬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} → (Language (src T) t) → ¬Language T ⟨ warning t ⟩ -¬function-err-src {T = S ⇒ T} p = function-warning p -¬function-err-src {T = scalar s} p = scalar-warning +¬function-err-src {T = S ⇒ T} {t = error} p = function-function (untyped p) check untyped +¬function-err-src {T = S ⇒ T} {t = ⟨ t ⟩} p = function-function (one p) check one₁ +¬function-err-src {T = scalar s} {t = error} p = scalar-function s +¬function-err-src {T = scalar s} {t = ⟨ t ⟩} p = scalar-function s ¬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) ¬function-err-src {T = never} p = never src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T ⟨ warning t ⟩ → (¬Language (srcⁿ T) t) src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂) -src-¬function-errᶠ (S ⇒ T) (function-warning p) = p +src-¬function-errᶠ {t = error} (S ⇒ T) (function-nok (untyped p)) = p +src-¬function-errᶠ {t = ⟨ t ⟩} (S ⇒ T) (function-nok (one p)) = p src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T ⟨ warning t ⟩ → (¬Language (srcⁿ T) t) -src-¬function-errⁿ (S ⇒ T) (function-warning p) = p +src-¬function-errⁿ {t = error} (S ⇒ T) (function-nok (untyped p)) = p +src-¬function-errⁿ {t = ⟨ t ⟩} (S ⇒ T) (function-nok (one 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 ⟨ warning t ⟩ → (¬Language (src T) t) -src-¬function-err {T = S ⇒ T} (function-warning p) = p +src-¬function-err {T = S ⇒ T} {t = error} (function-nok (untyped p)) = p +src-¬function-err {T = S ⇒ T} {t = ⟨ t ⟩} (function-nok (one p)) = p src-¬function-err {T = any} 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) +src-¬function-err {T = scalar s} {t = error} () +src-¬function-err {T = scalar s} {t = ⟨ t ⟩} () src-function-errᶠ : ∀ {F t} → (FunType F) → ¬Language F ⟨ warning t ⟩ → (Language (srcⁿ F) t) src-function-errᶠ {F} {t} Fᶠ p with dec-language (srcⁿ F) t @@ -68,7 +82,7 @@ fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S) ¬fun-scalar s (S ⇒ T) (function-ok (error x)) = scalar-function s ¬fun-scalar s (S ⇒ T) (function-ok diverge) = scalar-function s ¬fun-scalar s (S ⇒ T) (function-ok (one p)) = scalar-function s -¬fun-scalar s (S ⇒ T) (function-warning p) = scalar-warning +¬fun-scalar s (S ⇒ T) function-none-check = scalar-function s ¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂ fun-function : ∀ {T} → FunType T → Language T ⟨ ⟨⟩ ↦ diverge ⟩ @@ -87,22 +101,26 @@ src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normal srcⁿ-any-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ any)) srcⁿ-any-≮: never (witness p q) = CONTRADICTION (language-comp q any) -srcⁿ-any-≮: (U ⇒ V) (witness p q) = witness (function-warning q) (function-warning p) -srcⁿ-any-≮: (U ∩ V) (witness p q) = witness (function-err-srcⁿ (U ∩ V) q) (function-warning p) +srcⁿ-any-≮: (U ⇒ V) (witness {t = error} p q) = witness (function-nok (untyped q))(function-function (untyped p) check untyped) +srcⁿ-any-≮: (U ⇒ V) (witness {t = ⟨ t ⟩} p q) = witness (function-nok (one q)) (function-function (one p) check one₁) +srcⁿ-any-≮: (U ∩ V) (witness {t = error} p q) = witness (function-err-srcⁿ (U ∩ V) q) (function-function (untyped p) check untyped) +srcⁿ-any-≮: (U ∩ V) (witness {t = ⟨ t ⟩} p q) = witness (function-err-srcⁿ (U ∩ V) q) (function-function (one p) check one₁) srcⁿ-any-≮: (U ∪ scalar s) (witness p q) = witness (right (scalar s)) (function-scalar s) srcⁿ-any-≮: (U ∪ error) (witness p q) = witness (right error) function-error src-any-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ any)) -src-any-≮: {U = T ⇒ U} (witness p q) = witness (function-warning q) (function-warning p) +src-any-≮: {U = T ⇒ U} (witness {t = error} p q) = witness (function-nok (untyped q)) (function-function (untyped p) check untyped) +src-any-≮: {U = T ⇒ U} (witness {t = ⟨ t ⟩} p q) = witness (function-nok (one q)) (function-function (one p) check one₁) src-any-≮: {U = never} (witness p q) = CONTRADICTION (language-comp q any) -src-any-≮: {U = any} (witness p q) = witness any (function-warning p) +src-any-≮: {U = any} (witness p q) = witness any function-error src-any-≮: {U = scalar s} (witness p q) = witness (scalar s) (function-scalar s) src-any-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-any-≮: (normal (T ∪ U)) p) src-any-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-any-≮: (normal (T ∩ U)) p) src-any-≮: {U = error} (witness p q) = witness error function-error srcᶠ-warning : ∀ {T t} → FunType T → Language T ⟨ warning t ⟩ → ¬Language (srcⁿ T) t -srcᶠ-warning (S ⇒ T) (function-warning p) = p +srcᶠ-warning {t = error} (S ⇒ T) (function-nok (untyped p)) = p +srcᶠ-warning {t = ⟨ t ⟩} (S ⇒ T) (function-nok (one p)) = p srcᶠ-warning (F ∩ G) (p , q) = (srcᶠ-warning F p , srcᶠ-warning G q) srcⁿ-warning : ∀ {T t} → Normal T → Language T ⟨ warning t ⟩ → ¬Language (srcⁿ T) t @@ -116,8 +134,8 @@ src-warning {T} p = srcⁿ-warning (normal T) (<:-normalize T p) any-src-≮: : ∀ {S T U} → (U ≮: S) → (T <: unknown) → (T ≮: (U ⇒ any)) → (U ≮: src T) any-src-≮: (witness p _) _ (witness q (function-scalar s)) = witness p (src-¬scalar s q) -any-src-≮: _ _ (witness _ (function-function _ (one ()))) -any-src-≮: _ _ (witness p (function-warning q)) = witness q (src-warning p) +-- any-src-≮: _ _ (witness _ (function-function _ (one ()))) +-- any-src-≮: _ _ (witness p (function-warning q)) = witness q (src-warning p) any-src-≮: _ p (witness q function-error) = CONTRADICTION (language-comp ((((function-error , scalar-error NUMBER) , scalar-error STRING) , scalar-error NIL) diff --git a/Properties/TypeNormalization.agda b/Properties/TypeNormalization.agda index 5dfa6bb..5c86b71 100644 --- a/Properties/TypeNormalization.agda +++ b/Properties/TypeNormalization.agda @@ -4,7 +4,7 @@ module Properties.TypeNormalization where open import Agda.Builtin.Equality using (refl) open import Luau.Type using (Type; Scalar; nill; number; string; boolean; error; never; any; unknown; scalar; _⇒_; _∪_; _∩_; NIL; NUMBER; STRING; BOOLEAN; _≡ˢ_; _≡ᵀ_) -open import Luau.Subtyping using (Language; ¬Language; scalar; any; left; right; function-ok; function-error; function-nok; function-warning; scalar-warning; scalar-function; function-scalar; _,_; _↦_; ⟨⟩; ⟨_⟩; error; diverge) +open import Luau.Subtyping using (Language; ¬Language; scalar; any; left; right; function-ok; function-error; function-nok; function-none-check; scalar-function; function-scalar; _,_; _↦_; ⟨⟩; ⟨_⟩; error; diverge) open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize) open import Luau.Subtyping using (_<:_; _≮:_; witness; never) open import Properties.Dec using (Dec; yes; no) @@ -50,7 +50,7 @@ fun-≮:-never F = witness (fun-function F) never fun-¬scalar : ∀ S {F t} → FunType F → Language F t → ¬Language (scalar S) t fun-¬scalar s (S ⇒ T) (function-nok p) = scalar-function s fun-¬scalar s (S ⇒ T) (function-ok p) = scalar-function s -fun-¬scalar s (S ⇒ T) (function-warning p) = scalar-warning +fun-¬scalar s (S ⇒ T) function-none-check = scalar-function s fun-¬scalar s (F ∩ G) (p , q) = fun-¬scalar s G q ¬scalar-fun : ∀ {F} → FunType F → ∀ S → ¬Language F ⟨ scalar S ⟩ @@ -64,7 +64,7 @@ scalar-≮:-fun F s = witness (scalar s) (¬scalar-fun F s) fun-¬error : ∀ {F t} → FunType F → Language F t → ¬Language error t fun-¬error (S ⇒ T) (function-nok p) = error fun-¬error (S ⇒ T) (function-ok p) = error -fun-¬error (S ⇒ T) (function-warning p) = error +fun-¬error (S ⇒ T) function-none-check = error fun-¬error (F ∩ G) (p , q) = fun-¬error G q ¬error-fun : ∀ {F} → FunType F → ¬Language F error From 9f5c395b1e55c361a53c64e6b2edef5511f6b8b3 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Thu, 9 Nov 2023 12:47:42 -0600 Subject: [PATCH 3/8] Finished up tidy subtyping --- Properties/ErrorSuppression.agda | 5 ++--- Properties/ResolveOverloads.agda | 6 +++--- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Properties/ErrorSuppression.agda b/Properties/ErrorSuppression.agda index 4585723..eed4654 100644 --- a/Properties/ErrorSuppression.agda +++ b/Properties/ErrorSuppression.agda @@ -4,7 +4,7 @@ module Properties.ErrorSuppression where open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond) open import Luau.Type using (Type; unknown; never; any; error; funktion; scalar; _⇒_; _∪_; _∩_) -open import Luau.Subtyping using (Value; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; ⟨⟩; ⟨untyped⟩; warning; witness; scalar; function-nok; function-ok; function-warning; left; right; _,_; any; error; untyped; one; diverge; scalar-scalar; scalar-function; scalar-warning; scalar-error; function-scalar; function-function; function-error; never; none) +open import Luau.Subtyping using (Value; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; ⟨⟩; ⟨untyped⟩; check; witness; scalar; function-nok; function-ok; left; right; _,_; any; error; untyped; one; diverge; scalar-scalar; scalar-function; scalar-error; function-scalar; function-function; function-error; never; none) open import Luau.ErrorSuppression using (SuppressedValue; SuppressedTypedValue; SuppressedArguments; SuppressedResult; _≮:ᵘ_; _,_) open import Luau.SafeTypes using (Unsafe; any; error; param; result; ∪-left; ∪-right; ∩-left; ∩-right) open import Properties.Contradiction using (¬; ⊥) @@ -28,8 +28,6 @@ dec-SuppressedValue T ⟨ t ⟩ = dec-SuppressedTypedValue T t dec-SuppressedTypedValue (scalar s) t = Right (λ ()) dec-SuppressedTypedValue (S ⇒ T) (scalar s) = Right (λ ()) -dec-SuppressedTypedValue (S ⇒ T) (warning error) = mapL param (dec-SuppressedValue S error) -dec-SuppressedTypedValue (S ⇒ T) (warning ⟨ s ⟩) = mapL param (dec-SuppressedTypedValue S s) dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) with dec-SuppressedArguments S s dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) | Left p = Left (param p) dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) | Right p = mapLR result (cond p) (dec-SuppressedResult T t) @@ -50,6 +48,7 @@ dec-SuppressedArguments T ⟨ t ⟩ = dec-SuppressedTypedValue T t dec-SuppressedResult T error = dec-SuppressedValue T error dec-SuppressedResult T diverge = Right (λ ()) dec-SuppressedResult T ⟨ t ⟩ = dec-SuppressedTypedValue T t +dec-SuppressedResult T check = Right (λ ()) dec-Unsafe-≮:ᵘ : ∀ {T U} → (T ≮: U) → Either (Unsafe T) (T ≮:ᵘ U) dec-Unsafe-≮:ᵘ {T} (witness {t} p q) = mapR (λ r → (witness p q , r)) (dec-SuppressedValue T t) diff --git a/Properties/ResolveOverloads.agda b/Properties/ResolveOverloads.agda index 0823142..b01e07e 100644 --- a/Properties/ResolveOverloads.agda +++ b/Properties/ResolveOverloads.agda @@ -4,7 +4,7 @@ module Properties.ResolveOverloads where open import FFI.Data.Either using (Left; Right) open import Luau.ResolveOverloads using (Resolved; src; srcⁿ; resolve; resolveⁿ; resolveᶠ; resolveToˢ; target; yes; no) -open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; Value; TypedValue; witness; scalar; any; never; function-ok; function-nok; function-scalar; function-none-check; function-error; function-function; scalar-scalar; scalar-function; scalar-warning; scalar-error; _,_; left; right; _↦_; ⟨⟩; ⟨_⟩; warning; diverge; error; check; untyped; none; one; one₁; one₂; ⟨untyped⟩) +open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; Value; TypedValue; witness; scalar; any; never; function-ok; function-nok; function-scalar; function-none-check; function-error; function-function; scalar-scalar; scalar-function; scalar-error; _,_; left; right; _↦_; ⟨⟩; ⟨_⟩; diverge; error; check; untyped; none; one; one₁; one₂; ⟨untyped⟩) open import Luau.Type using (Type ; Scalar; _⇒_; _∩_; _∪_; scalar; any; never; error; unknown; NUMBER; BOOLEAN; NIL; STRING) open import Luau.TypeSaturation using (saturate) open import Luau.TypeNormalization using (normalize) @@ -134,8 +134,8 @@ src-warning {T} p = srcⁿ-warning (normal T) (<:-normalize T p) any-src-≮: : ∀ {S T U} → (U ≮: S) → (T <: unknown) → (T ≮: (U ⇒ any)) → (U ≮: src T) any-src-≮: (witness p _) _ (witness q (function-scalar s)) = witness p (src-¬scalar s q) --- any-src-≮: _ _ (witness _ (function-function _ (one ()))) --- any-src-≮: _ _ (witness p (function-warning q)) = witness q (src-warning p) +any-src-≮: _ _ (witness p (function-function (one q) check one₁)) = witness q (src-warning p) +any-src-≮: _ _ (witness p (function-function (untyped q) check untyped)) = witness q (src-warning p) any-src-≮: _ p (witness q function-error) = CONTRADICTION (language-comp ((((function-error , scalar-error NUMBER) , scalar-error STRING) , scalar-error NIL) From ea886ba848ee2a00c6651190c2287be95db22543 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Fri, 1 Dec 2023 16:23:45 -0600 Subject: [PATCH 4/8] Bumped Agda version --- .github/workflows/test.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index fea1e75..244a8a2 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -10,9 +10,9 @@ jobs: linux: strategy: matrix: - agda: [2.6.2.2] - hackageDate: ["2022-12-08"] - hackageTime: ["00:41:16"] + agda: [2.6.4] + hackageDate: ["2023-12-01"] + hackageTime: ["20:29:20"] runs-on: ubuntu-latest steps: - uses: actions/checkout@v1 From 391522e67dae731c207724d0a89770d53a1b25d8 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Fri, 1 Dec 2023 16:40:11 -0600 Subject: [PATCH 5/8] Agda install dir --- .github/workflows/test.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 244a8a2..098d9f4 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -30,11 +30,11 @@ jobs: cabal install --allow-newer Agda-${{ matrix.agda }} - name: check targets run: | - ~/.cabal/bin/agda Everything.agda + ~/.local/bin/agda Everything.agda - name: build executables run: | - ~/.cabal/bin/agda --compile PrettyPrinter.agda - ~/.cabal/bin/agda --compile Interpreter.agda + ~/.local/bin/agda --compile PrettyPrinter.agda + ~/.local/bin/agda --compile Interpreter.agda - name: clone Luau uses: actions/checkout@v2 with: From 81c5e1cd08eedc9b418dbb860ff74bb267629732 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Fri, 1 Dec 2023 17:43:47 -0600 Subject: [PATCH 6/8] Link to the text lib --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 098d9f4..83a713e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -26,7 +26,7 @@ jobs: run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z" - name: cabal install run: | - cabal install --lib scientific vector aeson --package-env . + cabal install --lib text scientific vector aeson --package-env . cabal install --allow-newer Agda-${{ matrix.agda }} - name: check targets run: | From 20514746bd79abf7a06767df096524944cf013b1 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Fri, 1 Dec 2023 18:02:05 -0600 Subject: [PATCH 7/8] Link to the bytestring lib --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 83a713e..7cd06c9 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -26,7 +26,7 @@ jobs: run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z" - name: cabal install run: | - cabal install --lib text scientific vector aeson --package-env . + cabal install --lib text bytestring scientific vector aeson --package-env . cabal install --allow-newer Agda-${{ matrix.agda }} - name: check targets run: | From e505e617ab050abdfcf11faa2c4d0a3b2e0eef5a Mon Sep 17 00:00:00 2001 From: Alan Jeffrey Date: Fri, 1 Dec 2023 18:21:16 -0600 Subject: [PATCH 8/8] Agda install dir in tests.py --- tests.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests.py b/tests.py index 20070ae..1feecb0 100755 --- a/tests.py +++ b/tests.py @@ -95,7 +95,7 @@ def build_suite(root, suite): if entry_point is None: return (False, "Invalid suite") - result = subprocess.run(["~/.cabal/bin/agda", "--compile", entry_point], shell=True, cwd=root, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + result = subprocess.run(["~/.local/bin/agda", "--compile", entry_point], shell=True, cwd=root, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) if result.returncode == 0: return (True, None) else: