mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
Sigh, forgot to add some files
This commit is contained in:
ajeffrey@roblox.com
parent
4033100f50
commit
ec32877f06
2 changed files with 170 additions and 0 deletions
38
prototyping/Luau/FunctionTypes.agda
Normal file
38
prototyping/Luau/FunctionTypes.agda
Normal 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)
|
||||
|
||||
132
prototyping/Properties/FunctionTypes.agda
Normal file
132
prototyping/Properties/FunctionTypes.agda
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
{-# 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)
|
||||
|
||||
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 ())))
|
||||
Loading…
Add table
Reference in a new issue