mirror of
https://github.com/luau-lang/luau.git
synced 2024-12-12 13:00:38 +00:00
Prototyping function overload resolution (#508)
This commit is contained in:
Alan Jeffrey
GitHub
parent
da01056022
commit
948f678f93
17 changed files with 1207 additions and 380 deletions
|
|
@ -1,38 +0,0 @@
|
|||
{-# 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)
|
||||
|
||||
98
prototyping/Luau/ResolveOverloads.agda
Normal file
98
prototyping/Luau/ResolveOverloads.agda
Normal file
|
|
@ -0,0 +1,98 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Luau.ResolveOverloads where
|
||||
|
||||
open import FFI.Data.Either using (Left; Right)
|
||||
open import Luau.Subtyping using (_<:_; _≮:_; Language; witness; scalar; unknown; never; function-ok)
|
||||
open import Luau.Type using (Type ; _⇒_; _∩_; _∪_; unknown; never)
|
||||
open import Luau.TypeSaturation using (saturate)
|
||||
open import Luau.TypeNormalization using (normalize)
|
||||
open import Properties.Contradiction using (CONTRADICTION)
|
||||
open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
|
||||
open import Properties.Functions using (_∘_)
|
||||
open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right)
|
||||
open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
|
||||
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)
|
||||
|
||||
-- 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)
|
||||
|
||||
-- Calculate the result of applying a function type `F` to an argument type `V`.
|
||||
-- We do this by finding an overload of `F` that has the most precise type,
|
||||
-- that is an overload `(Sʳ ⇒ Tʳ)` where `V <: Sʳ` and moreover
|
||||
-- for any other such overload `(S ⇒ T)` we have that `Tʳ <: T`.
|
||||
|
||||
-- For example if `F` is `(number -> number) & (nil -> nil) & (number? -> number?)`
|
||||
-- then to resolve `F` with argument type `number`, we pick the `number -> number`
|
||||
-- overload, but if the argument is `number?`, we pick `number? -> number?`./
|
||||
|
||||
-- Not all types have such a most precise overload, but saturated ones do.
|
||||
|
||||
data ResolvedTo F G V : Set where
|
||||
|
||||
yes : ∀ Sʳ Tʳ →
|
||||
|
||||
Overloads F (Sʳ ⇒ Tʳ) →
|
||||
(V <: Sʳ) →
|
||||
(∀ {S T} → Overloads G (S ⇒ T) → (V <: S) → (Tʳ <: T)) →
|
||||
--------------------------------------------
|
||||
ResolvedTo F G V
|
||||
|
||||
no :
|
||||
|
||||
(∀ {S T} → Overloads G (S ⇒ T) → (V ≮: S)) →
|
||||
--------------------------------------------
|
||||
ResolvedTo F G V
|
||||
|
||||
Resolved : Type → Type → Set
|
||||
Resolved F V = ResolvedTo F F V
|
||||
|
||||
target : ∀ {F V} → Resolved F V → Type
|
||||
target (yes _ T _ _ _) = T
|
||||
target (no _) = unknown
|
||||
|
||||
-- We can resolve any saturated function type
|
||||
resolveˢ : ∀ {F G V} → FunType G → Saturated F → Normal V → (G ⊆ᵒ F) → ResolvedTo F G V
|
||||
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F with dec-subtypingⁿ Vⁿ Sⁿ
|
||||
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Left V≮:S = no (λ { here → V≮:S })
|
||||
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Right V<:S = yes _ _ (G⊆F here) V<:S (λ { here _ → <:-refl })
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F with resolveˢ Gᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ left) | resolveˢ Hᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ right)
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ with sat-∩ o₁ o₂
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ | defn o p₁ p₂ =
|
||||
yes _ _ o (<:-trans (<:-∩-glb V<:S₁ V<:S₂) p₁) (λ { (left o) p → <:-trans p₂ (<:-trans <:-∩-left (tgt₁ o p)) ; (right o) p → <:-trans p₂ (<:-trans <:-∩-right (tgt₂ o p)) })
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | no src₂ =
|
||||
yes _ _ o₁ V<:S₁ (λ { (left o) p → tgt₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (src₂ o)) })
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ =
|
||||
yes _ _ o₂ V<:S₂ (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (src₁ o)) ; (right o) p → tgt₂ o p })
|
||||
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | no src₂ =
|
||||
no (λ { (left o) → src₁ o ; (right o) → src₂ o })
|
||||
|
||||
-- Which means we can resolve any normalized type, by saturating it first
|
||||
resolveᶠ : ∀ {F V} → FunType F → Normal V → Type
|
||||
resolveᶠ Fᶠ Vⁿ = target (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))
|
||||
|
||||
resolveⁿ : ∀ {F V} → Normal F → Normal V → Type
|
||||
resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Vⁿ
|
||||
resolveⁿ (Fᶠ ∩ Gᶠ) Vⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Vⁿ
|
||||
resolveⁿ (Sⁿ ∪ Tˢ) Vⁿ = unknown
|
||||
resolveⁿ unknown Vⁿ = unknown
|
||||
resolveⁿ never Vⁿ = never
|
||||
|
||||
-- Which means we can resolve any type, by normalizing it first
|
||||
resolve : Type → Type → Type
|
||||
resolve F V = resolveⁿ (normal F) (normal V)
|
||||
|
|
@ -5,8 +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.FunctionTypes using (src; tgt)
|
||||
open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_)
|
||||
open import Luau.ResolveOverloads using (src; resolve)
|
||||
open import Luau.Subtyping using (_≮:_)
|
||||
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
|
|
|
|||
|
|
@ -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 (_≮:_; Tree; witness; scalar; function; function-ok; function-err)
|
||||
open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err; function-tgt)
|
||||
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)
|
||||
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
|
||||
open import Luau.Type using (number; boolean; string; nil)
|
||||
|
|
@ -27,8 +27,9 @@ treeToString (scalar boolean) n v = v ++ " is a boolean"
|
|||
treeToString (scalar string) n v = v ++ " is a string"
|
||||
treeToString (scalar nil) n v = v ++ " is nil"
|
||||
treeToString function n v = v ++ " is a function"
|
||||
treeToString (function-ok t) n v = treeToString t n (v ++ "()")
|
||||
treeToString (function-ok s t) n v = treeToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n " ++ treeToString s (suc n) w where w = tmp n
|
||||
treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n " ++ treeToString t (suc n) w where w = tmp n
|
||||
treeToString (function-tgt t) n v = treeToString t n (v ++ "()")
|
||||
|
||||
subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
|
||||
subtypeWarningToString (witness t p q) = "\n because provided type contains v, where " ++ treeToString t 0 "v"
|
||||
|
|
|
|||
|
|
@ -13,8 +13,9 @@ data Tree : Set where
|
|||
|
||||
scalar : ∀ {T} → Scalar T → Tree
|
||||
function : Tree
|
||||
function-ok : Tree → Tree
|
||||
function-ok : Tree → Tree → Tree
|
||||
function-err : Tree → Tree
|
||||
function-tgt : Tree → Tree
|
||||
|
||||
data Language : Type → Tree → Set
|
||||
data ¬Language : Type → Tree → Set
|
||||
|
|
@ -23,8 +24,10 @@ data Language where
|
|||
|
||||
scalar : ∀ {T} → (s : Scalar T) → Language T (scalar s)
|
||||
function : ∀ {T U} → Language (T ⇒ U) function
|
||||
function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u)
|
||||
function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u)
|
||||
function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t u)
|
||||
function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
|
||||
function-tgt : ∀ {T U t} → (Language U t) → Language (T ⇒ U) (function-tgt 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
|
||||
|
|
@ -34,11 +37,13 @@ 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-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u)
|
||||
scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
|
||||
scalar-function-tgt : ∀ {S t} → (Scalar S) → ¬Language S (function-tgt 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-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u)
|
||||
function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
|
||||
function-tgt : ∀ {T U t} → (¬Language U t) → ¬Language (T ⇒ U) (function-tgt t)
|
||||
_,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
|
||||
left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
|
||||
right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
|
||||
|
|
|
|||
|
|
@ -3,16 +3,18 @@
|
|||
module Luau.TypeCheck where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_)
|
||||
open import FFI.Data.Either using (Either; Left; Right)
|
||||
open import FFI.Data.Maybe using (Maybe; just)
|
||||
open import Luau.ResolveOverloads using (resolve)
|
||||
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; _⇒_)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import FFI.Data.Vector using (Vector)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Properties.DecSubtyping using (dec-subtyping)
|
||||
open import Properties.Product using (_×_; _,_)
|
||||
|
||||
orUnknown : Maybe Type → Type
|
||||
|
|
@ -113,8 +115,8 @@ data _⊢ᴱ_∈_ where
|
|||
|
||||
Γ ⊢ᴱ M ∈ T →
|
||||
Γ ⊢ᴱ N ∈ U →
|
||||
----------------------
|
||||
Γ ⊢ᴱ (M $ N) ∈ (tgt T)
|
||||
----------------------------
|
||||
Γ ⊢ᴱ (M $ N) ∈ (resolve T U)
|
||||
|
||||
function : ∀ {f x B T U V Γ} →
|
||||
|
||||
|
|
|
|||
|
|
@ -2,11 +2,7 @@ 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
|
||||
-- Operations on normalized types
|
||||
_∪ᶠ_ : Type → Type → Type
|
||||
_∪ⁿˢ_ : Type → Type → Type
|
||||
_∩ⁿˢ_ : Type → Type → Type
|
||||
|
|
@ -23,8 +19,8 @@ F ∪ᶠ G = F ∪ G
|
|||
S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
|
||||
S ∪ⁿ unknown = unknown
|
||||
S ∪ⁿ never = S
|
||||
unknown ∪ⁿ T = unknown
|
||||
never ∪ⁿ T = T
|
||||
unknown ∪ⁿ T = unknown
|
||||
(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
|
||||
F ∪ⁿ G = F ∪ᶠ G
|
||||
|
||||
|
|
|
|||
66
prototyping/Luau/TypeSaturation.agda
Normal file
66
prototyping/Luau/TypeSaturation.agda
Normal file
|
|
@ -0,0 +1,66 @@
|
|||
module Luau.TypeSaturation where
|
||||
|
||||
open import Luau.Type using (Type; _⇒_; _∩_; _∪_)
|
||||
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
|
||||
|
||||
-- So, there's a problem with overloaded functions
|
||||
-- (of the form (S_1 ⇒ T_1) ∩⋯∩ (S_n ⇒ T_n))
|
||||
-- which is that it's not good enough to compare them
|
||||
-- for subtyping by comparing all of their overloads.
|
||||
|
||||
-- For example (nil → nil) is a subtype of (number? → number?) ∩ (string? → string?)
|
||||
-- but not a subtype of any of its overloads.
|
||||
|
||||
-- To fix this, we adapt the semantic subtyping algorithm for
|
||||
-- function types, given in
|
||||
-- https://www.irif.fr/~gc/papers/covcon-again.pdf and
|
||||
-- https://pnwamk.github.io/sst-tutorial/
|
||||
|
||||
-- A function type is *intersection-saturated* if for any overloads
|
||||
-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
|
||||
-- of ((S₁ ∩ S₂) ⇒ (T₁ ∩ T₂)).
|
||||
|
||||
-- A function type is *union-saturated* if for any overloads
|
||||
-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
|
||||
-- of ((S₁ ∪ S₂) ⇒ (T₁ ∪ T₂)).
|
||||
|
||||
-- A function type is *saturated* if it is both intersection- and
|
||||
-- union-saturated.
|
||||
|
||||
-- For example (number? → number?) ∩ (string? → string?)
|
||||
-- is not saturated, but (number? → number?) ∩ (string? → string?) ∩ (nil → nil) ∩ ((number ∪ string)? → (number ∪ string)?)
|
||||
-- is.
|
||||
|
||||
-- Saturated function types have the nice property that they can ber
|
||||
-- compared by just comparing their overloads: F <: G whenever for any
|
||||
-- overload of G, there is an overload os F which is a subtype of it.
|
||||
|
||||
-- Forunately every function type can be saturated!
|
||||
_⋓_ : Type → Type → Type
|
||||
(S₁ ⇒ T₁) ⋓ (S₂ ⇒ T₂) = (S₁ ∪ⁿ S₂) ⇒ (T₁ ∪ⁿ T₂)
|
||||
(F₁ ∩ G₁) ⋓ F₂ = (F₁ ⋓ F₂) ∩ (G₁ ⋓ F₂)
|
||||
F₁ ⋓ (F₂ ∩ G₂) = (F₁ ⋓ F₂) ∩ (F₁ ⋓ G₂)
|
||||
F ⋓ G = F ∩ G
|
||||
|
||||
_⋒_ : Type → Type → Type
|
||||
(S₁ ⇒ T₁) ⋒ (S₂ ⇒ T₂) = (S₁ ∩ⁿ S₂) ⇒ (T₁ ∩ⁿ T₂)
|
||||
(F₁ ∩ G₁) ⋒ F₂ = (F₁ ⋒ F₂) ∩ (G₁ ⋒ F₂)
|
||||
F₁ ⋒ (F₂ ∩ G₂) = (F₁ ⋒ F₂) ∩ (F₁ ⋒ G₂)
|
||||
F ⋒ G = F ∩ G
|
||||
|
||||
_∩ᵘ_ : Type → Type → Type
|
||||
F ∩ᵘ G = (F ∩ G) ∩ (F ⋓ G)
|
||||
|
||||
_∩ⁱ_ : Type → Type → Type
|
||||
F ∩ⁱ G = (F ∩ G) ∩ (F ⋒ G)
|
||||
|
||||
∪-saturate : Type → Type
|
||||
∪-saturate (F ∩ G) = (∪-saturate F ∩ᵘ ∪-saturate G)
|
||||
∪-saturate F = F
|
||||
|
||||
∩-saturate : Type → Type
|
||||
∩-saturate (F ∩ G) = (∩-saturate F ∩ⁱ ∩-saturate G)
|
||||
∩-saturate F = F
|
||||
|
||||
saturate : Type → Type
|
||||
saturate F = ∪-saturate (∩-saturate F)
|
||||
|
|
@ -7,7 +7,6 @@ import Properties.Dec
|
|||
import Properties.DecSubtyping
|
||||
import Properties.Equality
|
||||
import Properties.Functions
|
||||
import Properties.FunctionTypes
|
||||
import Properties.Remember
|
||||
import Properties.Step
|
||||
import Properties.StrictMode
|
||||
|
|
|
|||
|
|
@ -4,21 +4,23 @@ 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.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
|
||||
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
|
||||
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
|
||||
open import Luau.TypeSaturation using (saturate)
|
||||
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.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; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
|
||||
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; fun-top; fun-function; fun-¬scalar)
|
||||
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_)
|
||||
open import Properties.Equality using (_≢_)
|
||||
|
||||
-- Honest this terminates, since src and tgt reduce the depth of nested arrows
|
||||
-- Honest this terminates, since saturation maintains 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ˢᶠ : ∀ {F G} → FunType F → Saturated F → FunType G → Either (F ≮: G) (F <:ᵒ G)
|
||||
dec-subtypingᶠ : ∀ {F G} → FunType F → FunType G → Either (F ≮: G) (F <: G)
|
||||
dec-subtypingᶠⁿ : ∀ {F U} → FunType F → Normal U → Either (F ≮: U) (F <: U)
|
||||
dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
|
||||
dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
|
||||
|
||||
|
|
@ -26,22 +28,116 @@ 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ˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) = result (top Fᶠ (λ o → o)) where
|
||||
|
||||
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)
|
||||
data Top G : Set where
|
||||
|
||||
defn : ∀ Sᵗ Tᵗ →
|
||||
|
||||
Overloads F (Sᵗ ⇒ Tᵗ) →
|
||||
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
|
||||
-------------
|
||||
Top G
|
||||
|
||||
top : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Top G
|
||||
top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
|
||||
top (Gᶠ ∩ Hᶠ) G⊆F with top Gᶠ (G⊆F ∘ left) | top Hᶠ (G⊆F ∘ right)
|
||||
top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ with sat-∪ p q
|
||||
top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ | defn n r r₁ = defn _ _ n
|
||||
(λ { (left o) → <:-trans (<:-trans (p₁ o) <:-∪-left) r ; (right o) → <:-trans (<:-trans (q₁ o) <:-∪-right) r })
|
||||
|
||||
result : Top F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
|
||||
result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ oᵗ)
|
||||
result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness s Ss ¬Sᵗs) = Left (witness (function-err s) (ov-language Fᶠ (λ o → function-err (<:-impl-⊇ (srcᵗ o) s ¬Sᵗs))) (function-err Ss))
|
||||
result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where
|
||||
|
||||
data LargestSrc (G : Type) : Set where
|
||||
|
||||
yes : ∀ S₀ T₀ →
|
||||
|
||||
Overloads F (S₀ ⇒ T₀) →
|
||||
T₀ <: T →
|
||||
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
|
||||
-----------------------
|
||||
LargestSrc G
|
||||
|
||||
no : ∀ S₀ T₀ →
|
||||
|
||||
Overloads F (S₀ ⇒ T₀) →
|
||||
T₀ ≮: T →
|
||||
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T₀ <: T′) →
|
||||
-----------------------
|
||||
LargestSrc G
|
||||
|
||||
largest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → LargestSrc G
|
||||
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F with dec-subtypingⁿ T′ⁿ Tⁿ
|
||||
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Left T′≮:T = no S′ T′ (G⊆F here) T′≮:T λ { here → <:-refl }
|
||||
largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Right T′<:T = yes S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl })
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F with largest Gᶠ (GH⊆F ∘ left) | largest Hᶠ (GH⊆F ∘ right)
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ with sat-∩ o₁ o₂
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt with dec-subtypingⁿ (normal-overload-tgt Fᶠ o) Tⁿ
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Left T₀≮:T = no _ _ o T₀≮:T (λ { (left o) → <:-trans tgt (<:-trans <:-∩-left (tgt₁ o)) ; (right o) → <:-trans tgt (<:-trans <:-∩-right (tgt₂ o)) })
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Right T₀<:T = yes _ _ o T₀<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | yes S₂ T₂ o₂ T₂<:T src₂ = yes S₂ T₂ o₂ T₂<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → src₂ o p })
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ = yes S₁ T₁ o₁ T₁<:T (λ { (left o) p → src₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ with sat-∪ o₁ o₂
|
||||
largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ | defn o src tgt = yes _ _ o (<:-trans tgt (<:-∪-lub T₁<:T T₂<:T))
|
||||
(λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src)
|
||||
; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src)
|
||||
})
|
||||
|
||||
result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
|
||||
result₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-tgt t) (ov-language Fᶠ (λ o → function-tgt (tgt₀ o t T₀t))) (function-tgt ¬Tt))
|
||||
result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ o₀)
|
||||
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₁ (smallest Fᶠ (λ o → o))) where
|
||||
|
||||
data SmallestTgt (G : Type) : Set where
|
||||
|
||||
defn : ∀ S₁ T₁ →
|
||||
|
||||
Overloads F (S₁ ⇒ T₁) →
|
||||
Language S₁ s →
|
||||
(∀ {S′ T′} → Overloads G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
|
||||
-----------------------
|
||||
SmallestTgt G
|
||||
|
||||
smallest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → SmallestTgt G
|
||||
smallest {S′ ⇒ T′} _ G⊆F with dec-language S′ s
|
||||
smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) }
|
||||
smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl })
|
||||
smallest (Gᶠ ∩ Hᶠ) GH⊆F with smallest Gᶠ (GH⊆F ∘ left) | smallest Hᶠ (GH⊆F ∘ right)
|
||||
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ with sat-∩ o₁ o₂
|
||||
smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ | defn o src tgt = defn _ _ o (src s (R₁s , R₂s))
|
||||
(λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s)
|
||||
; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)
|
||||
})
|
||||
|
||||
result₁ : SmallestTgt F → (F ≮: (S ⇒ T))
|
||||
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) with dec-subtypingⁿ (normal-overload-tgt Fᶠ o₁) Tⁿ
|
||||
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp s ¬S₀s (src₀ o₁ T₁<:T s S₁s))
|
||||
result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness t T₁t ¬Tt) = witness (function-ok s t) (ov-language Fᶠ lemma) (function-ok Ss ¬Tt) where
|
||||
|
||||
lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
|
||||
lemma {S′} o with dec-language S′ s
|
||||
lemma {S′} o | Left ¬S′s = function-ok₁ ¬S′s
|
||||
lemma {S′} o | Right S′s = function-ok₂ (tgt₁ o S′s t T₁t)
|
||||
|
||||
dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H
|
||||
dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G)
|
||||
dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H)
|
||||
dec-subtypingˢᶠ F Fˢ (G ∩ H) | Right F<:G | Right F<:H = Right (λ { (left o) → F<:G o ; (right o) → F<:H o })
|
||||
|
||||
dec-subtypingᶠ F G with dec-subtypingˢᶠ (normal-saturate F) (saturated F) G
|
||||
dec-subtypingᶠ F G | Left H≮:G = Left (<:-trans-≮: (saturate-<: F) H≮:G)
|
||||
dec-subtypingᶠ F G | Right H<:G = Right (<:-trans (<:-saturate F) (<:ᵒ-impl-<: (normal-saturate F) G H<:G))
|
||||
|
||||
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) | 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
|
||||
|
|
@ -68,3 +164,11 @@ 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)))
|
||||
|
||||
-- As a corollary, for saturated functions
|
||||
-- <:ᵒ coincides with <:, that is F is a subtype of (S ⇒ T) precisely
|
||||
-- when one of its overloads is.
|
||||
|
||||
<:-impl-<:ᵒ : ∀ {F G} → FunType F → Saturated F → FunType G → (F <: G) → (F <:ᵒ G)
|
||||
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G with dec-subtypingˢᶠ Fᶠ Fˢ Gᶠ
|
||||
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G | Left F≮:G = CONTRADICTION (<:-impl-¬≮: F<:G F≮:G)
|
||||
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G | Right F<:ᵒG = F<:ᵒG
|
||||
|
|
|
|||
|
|
@ -1,150 +0,0 @@
|
|||
{-# 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))
|
||||
|
||||
|
||||
189
prototyping/Properties/ResolveOverloads.agda
Normal file
189
prototyping/Properties/ResolveOverloads.agda
Normal file
|
|
@ -0,0 +1,189 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Properties.ResolveOverloads where
|
||||
|
||||
open import FFI.Data.Either using (Left; Right)
|
||||
open import Luau.ResolveOverloads using (Resolved; src; srcⁿ; resolve; resolveⁿ; resolveᶠ; resolveˢ; target; yes; no)
|
||||
open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; witness; scalar; unknown; never; function; function-ok; function-err; function-tgt; function-scalar; function-ok₁; function-ok₂; scalar-scalar; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; _,_; left; right)
|
||||
open import Luau.Type using (Type ; Scalar; _⇒_; _∩_; _∪_; nil; boolean; number; string; unknown; never)
|
||||
open import Luau.TypeSaturation using (saturate)
|
||||
open import Luau.TypeNormalization using (normalize)
|
||||
open import Properties.Contradiction using (CONTRADICTION)
|
||||
open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
|
||||
open import Properties.Functions using (_∘_)
|
||||
open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right; <:-impl-⊇; language-comp)
|
||||
open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
|
||||
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)
|
||||
|
||||
-- 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-ok₂ p) = scalar-function-ok s
|
||||
¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
|
||||
¬fun-scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt 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 s .(scalar s₁)) p (function-ok x (scalar-scalar s₁ () x₂)))
|
||||
unknown-src-≮: r (witness (function-ok s .function) p (function-ok x (scalar-function ())))
|
||||
unknown-src-≮: r (witness (function-ok s .(function-ok _ _)) p (function-ok x (scalar-function-ok ())))
|
||||
unknown-src-≮: r (witness (function-ok s .(function-err _)) p (function-ok x (scalar-function-err ())))
|
||||
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
|
||||
unknown-src-≮: r (witness (function-tgt t) p (function-tgt (scalar-function-tgt ())))
|
||||
|
||||
-- Properties of resolve
|
||||
resolveˢ-<:-⇒ : ∀ {F V U} → (FunType F) → (Saturated F) → (FunType (V ⇒ U)) → (r : Resolved F V) → (F <: (V ⇒ U)) → (target r <: U)
|
||||
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ r F<:V⇒U with <:-impl-<:ᵒ Fᶠ Fˢ V⇒Uᶠ F<:V⇒U here
|
||||
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) F<:V⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂
|
||||
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ (no tgtʳ) F<:V⇒U | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: o₁ (tgtʳ o))
|
||||
|
||||
resolveⁿ-<:-⇒ : ∀ {F V U} → (Fⁿ : Normal F) → (Vⁿ : Normal V) → (Uⁿ : Normal U) → (F <: (V ⇒ U)) → (resolveⁿ Fⁿ Vⁿ <: U)
|
||||
resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Vⁿ Uⁿ F<:V⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (Vⁿ ⇒ Uⁿ) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Vⁿ (λ o → o)) F<:V⇒U
|
||||
resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Vⁿ Uⁿ F<:V⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (Vⁿ ⇒ Uⁿ) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Vⁿ (λ o → o)) (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:V⇒U)
|
||||
resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Vⁿ Uⁿ F<:V⇒U = CONTRADICTION (<:-impl-¬≮: F<:V⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ)))
|
||||
resolveⁿ-<:-⇒ never Vⁿ Uⁿ F<:V⇒U = <:-never
|
||||
resolveⁿ-<:-⇒ unknown Vⁿ Uⁿ F<:V⇒U = CONTRADICTION (<:-impl-¬≮: F<:V⇒U unknown-≮:-function)
|
||||
|
||||
resolve-<:-⇒ : ∀ {F V U} → (F <: (V ⇒ U)) → (resolve F V <: U)
|
||||
resolve-<:-⇒ {F} {V} {U} F<:V⇒U = <:-trans (resolveⁿ-<:-⇒ (normal F) (normal V) (normal U) (<:-trans (normalize-<: F) (<:-trans F<:V⇒U (<:-normalize (V ⇒ U))))) (normalize-<: U)
|
||||
|
||||
resolve-≮:-⇒ : ∀ {F V U} → (resolve F V ≮: U) → (F ≮: (V ⇒ U))
|
||||
resolve-≮:-⇒ {F} {V} {U} FV≮:U with dec-subtyping F (V ⇒ U)
|
||||
resolve-≮:-⇒ {F} {V} {U} FV≮:U | Left F≮:V⇒U = F≮:V⇒U
|
||||
resolve-≮:-⇒ {F} {V} {U} FV≮:U | Right F<:V⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ F<:V⇒U) FV≮:U)
|
||||
|
||||
<:-resolveˢ-⇒ : ∀ {S T V} → (r : Resolved (S ⇒ T) V) → (V <: S) → T <: target r
|
||||
<:-resolveˢ-⇒ (yes S T here _ _) V<:S = <:-refl
|
||||
<:-resolveˢ-⇒ (no _) V<:S = <:-unknown
|
||||
|
||||
<:-resolveⁿ-⇒ : ∀ {S T V} → (Sⁿ : Normal S) → (Tⁿ : Normal T) → (Vⁿ : Normal V) → (V <: S) → T <: resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ
|
||||
<:-resolveⁿ-⇒ Sⁿ Tⁿ Vⁿ V<:S = <:-resolveˢ-⇒ (resolveˢ (Sⁿ ⇒ Tⁿ) (saturated (Sⁿ ⇒ Tⁿ)) Vⁿ (λ o → o)) V<:S
|
||||
|
||||
<:-resolve-⇒ : ∀ {S T V} → (V <: S) → T <: resolve (S ⇒ T) V
|
||||
<:-resolve-⇒ {S} {T} {V} V<:S = <:-trans (<:-normalize T) (<:-resolveⁿ-⇒ (normal S) (normal T) (normal V) (<:-trans (normalize-<: V) (<:-trans V<:S (<:-normalize S))))
|
||||
|
||||
<:-resolveˢ : ∀ {F G V W} → (r : Resolved F V) → (s : Resolved G W) → (F <:ᵒ G) → (V <: W) → target r <: target s
|
||||
<:-resolveˢ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) (yes Sˢ Tˢ oˢ W<:Sˢ tgtˢ) F<:G V<:W with F<:G oˢ
|
||||
<:-resolveˢ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) (yes Sˢ Tˢ oˢ W<:Sˢ tgtˢ) F<:G V<:W | defn o o₁ o₂ = <:-trans (tgtʳ o (<:-trans (<:-trans V<:W W<:Sˢ) o₁)) o₂
|
||||
<:-resolveˢ (no r) (yes Sˢ Tˢ oˢ W<:Sˢ tgtˢ) F<:G V<:W with F<:G oˢ
|
||||
<:-resolveˢ (no r) (yes Sˢ Tˢ oˢ W<:Sˢ tgtˢ) F<:G V<:W | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: (<:-trans V<:W (<:-trans W<:Sˢ o₁)) (r o))
|
||||
<:-resolveˢ r (no s) F<:G V<:W = <:-unknown
|
||||
|
||||
<:-resolveᶠ : ∀ {F G V W} → (Fᶠ : FunType F) → (Gᶠ : FunType G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveᶠ Fᶠ Vⁿ <: resolveᶠ Gᶠ Wⁿ
|
||||
<:-resolveᶠ Fᶠ Gᶠ Vⁿ Wⁿ F<:G V<:W = <:-resolveˢ
|
||||
(resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))
|
||||
(resolveˢ (normal-saturate Gᶠ) (saturated Gᶠ) Wⁿ (λ o → o))
|
||||
(<:-impl-<:ᵒ (normal-saturate Fᶠ) (saturated Fᶠ) (normal-saturate Gᶠ) (<:-trans (saturate-<: Fᶠ) (<:-trans F<:G (<:-saturate Gᶠ))))
|
||||
V<:W
|
||||
|
||||
<:-resolveⁿ : ∀ {F G V W} → (Fⁿ : Normal F) → (Gⁿ : Normal G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveⁿ Fⁿ Vⁿ <: resolveⁿ Gⁿ Wⁿ
|
||||
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
|
||||
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
|
||||
<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
|
||||
<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
|
||||
<:-resolveⁿ (Fⁿ ∪ Sˢ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-function Sˢ)))
|
||||
<:-resolveⁿ unknown (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G unknown-≮:-function)
|
||||
<:-resolveⁿ (Fⁿ ∪ Sˢ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-fun (Gⁿ ∩ Hⁿ) Sˢ)))
|
||||
<:-resolveⁿ unknown (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (unknown-≮:-fun (Gⁿ ∩ Hⁿ)))
|
||||
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Rⁿ ⇒ Sⁿ)))
|
||||
<:-resolveⁿ (Eⁿ ∩ Fⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Eⁿ ∩ Fⁿ)))
|
||||
<:-resolveⁿ (Fⁿ ∪ Sˢ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-never Sˢ)))
|
||||
<:-resolveⁿ unknown never Vⁿ Wⁿ F<:G V<:W = F<:G
|
||||
<:-resolveⁿ never Gⁿ Vⁿ Wⁿ F<:G V<:W = <:-never
|
||||
<:-resolveⁿ Fⁿ (Gⁿ ∪ Uˢ) Vⁿ Wⁿ F<:G V<:W = <:-unknown
|
||||
<:-resolveⁿ Fⁿ unknown Vⁿ Wⁿ F<:G V<:W = <:-unknown
|
||||
|
||||
<:-resolve : ∀ {F G V W} → (F <: G) → (V <: W) → resolve F V <: resolve G W
|
||||
<:-resolve {F} {G} {V} {W} F<:G V<:W = <:-resolveⁿ (normal F) (normal G) (normal V) (normal W)
|
||||
(<:-trans (normalize-<: F) (<:-trans F<:G (<:-normalize G)))
|
||||
(<:-trans (normalize-<: V) (<:-trans V<:W (<:-normalize W)))
|
||||
|
|
@ -7,11 +7,11 @@ open import Agda.Builtin.Equality using (_≡_; refl)
|
|||
open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
|
||||
open import Luau.ResolveOverloads using (src; resolve)
|
||||
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr)
|
||||
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.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.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 (_≡ⱽ_)
|
||||
|
|
@ -23,8 +23,10 @@ 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.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.DecSubtyping using (dec-subtyping)
|
||||
open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never; <:-refl; <:-unknown; <:-impl-¬≮:)
|
||||
open import Properties.ResolveOverloads using (src-unknown-≮:; unknown-src-≮:; <:-resolve; resolve-<:-⇒; <:-resolve-⇒)
|
||||
open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; <:-trans-≮:; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never; ≡-impl-<:; ≡-trans-<:; <:-trans-≡; ≮:-trans-<:; <:-trans)
|
||||
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; +; -; *; /; <; >; <=; >=; ··)
|
||||
|
|
@ -63,51 +65,32 @@ lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
|
|||
lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
|
||||
lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p
|
||||
|
||||
heap-weakeningᴱ : ∀ Γ H M {H′ U} → (H ⊑ H′) → (typeOfᴱ H′ Γ M ≮: U) → (typeOfᴱ H Γ M ≮: U)
|
||||
heap-weakeningᴱ Γ H (var x) h p = p
|
||||
heap-weakeningᴱ Γ H (val nil) h p = p
|
||||
heap-weakeningᴱ Γ H (val (addr a)) refl p = p
|
||||
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p with a ≡ᴬ b
|
||||
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = unknown-≮: p
|
||||
heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orUnknown (cong typeOfᴹᴼ (lookup-not-allocated q r))) p
|
||||
heap-weakeningᴱ Γ H (val (number x)) h p = p
|
||||
heap-weakeningᴱ Γ H (val (bool x)) h p = p
|
||||
heap-weakeningᴱ Γ H (val (string x)) h p = p
|
||||
heap-weakeningᴱ Γ H (M $ N) h p = never-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-never-≮: p))
|
||||
heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p
|
||||
heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p
|
||||
heap-weakeningᴱ Γ H (binexp M op N) h p = p
|
||||
<:-heap-weakeningᴱ : ∀ Γ H M {H′} → (H ⊑ H′) → (typeOfᴱ H′ Γ M <: typeOfᴱ H Γ M)
|
||||
<:-heap-weakeningᴱ Γ H (var x) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (val nil) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (val (addr a)) refl = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) with a ≡ᴬ b
|
||||
<:-heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) | yes refl = <:-unknown
|
||||
<:-heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) | no r = ≡-impl-<: (sym (cong orUnknown (cong typeOfᴹᴼ (lookup-not-allocated q r))))
|
||||
<:-heap-weakeningᴱ Γ H (val (number n)) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (val (bool b)) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (val (string s)) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (M $ N) h = <:-resolve (<:-heap-weakeningᴱ Γ H M h) (<:-heap-weakeningᴱ Γ H N h)
|
||||
<:-heap-weakeningᴱ Γ H (function f ⟨ var x ∈ S ⟩∈ T is B end) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (block var b ∈ T is N end) h = <:-refl
|
||||
<:-heap-weakeningᴱ Γ H (binexp M op N) h = <:-refl
|
||||
|
||||
heap-weakeningᴮ : ∀ Γ H B {H′ U} → (H ⊑ H′) → (typeOfᴮ H′ Γ B ≮: U) → (typeOfᴮ H Γ B ≮: U)
|
||||
heap-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h p = heap-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h p
|
||||
heap-weakeningᴮ Γ H (local var x ∈ T ← M ∙ B) h p = heap-weakeningᴮ (Γ ⊕ x ↦ T) H B h p
|
||||
heap-weakeningᴮ Γ H (return M ∙ B) h p = heap-weakeningᴱ Γ H M h p
|
||||
heap-weakeningᴮ Γ H done h p = p
|
||||
<:-heap-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → (typeOfᴮ H′ Γ B <: typeOfᴮ H Γ B)
|
||||
<:-heap-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h = <:-heap-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h
|
||||
<:-heap-weakeningᴮ Γ H (local var x ∈ T ← M ∙ B) h = <:-heap-weakeningᴮ (Γ ⊕ x ↦ T) H B h
|
||||
<:-heap-weakeningᴮ Γ H (return M ∙ B) h = <:-heap-weakeningᴱ Γ H M h
|
||||
<:-heap-weakeningᴮ Γ H done h = <:-refl
|
||||
|
||||
substitutivityᴱ : ∀ {Γ T U} H M v x → (typeOfᴱ H Γ (M [ v / x ]ᴱ) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) M ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
substitutivityᴱ-whenever : ∀ {Γ T U} H v x y (r : Dec(x ≡ y)) → (typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever r) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
substitutivityᴮ : ∀ {Γ T U} H B v x → (typeOfᴮ H Γ (B [ v / x ]ᴮ) ≮: U) → Either (typeOfᴮ H (Γ ⊕ x ↦ T) B ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
substitutivityᴮ-unless : ∀ {Γ T U V} H B v x y (r : Dec(x ≡ y)) → (typeOfᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r) ≮: V) → Either (typeOfᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T V} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless yes r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless no r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
≮:-heap-weakeningᴱ : ∀ Γ H M {H′ U} → (H ⊑ H′) → (typeOfᴱ H′ Γ M ≮: U) → (typeOfᴱ H Γ M ≮: U)
|
||||
≮:-heap-weakeningᴱ Γ H M h p = <:-trans-≮: (<:-heap-weakeningᴱ Γ H M h) p
|
||||
|
||||
substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
|
||||
substitutivityᴱ H (val w) v x p = Left p
|
||||
substitutivityᴱ H (binexp M op N) v x p = Left p
|
||||
substitutivityᴱ H (M $ N) v x p = mapL never-tgt-≮: (substitutivityᴱ H M v x (tgt-never-≮: p))
|
||||
substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p
|
||||
substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p
|
||||
substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q)
|
||||
substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orUnknown (sym (⊕-lookup-miss x y _ _ p))) q)
|
||||
|
||||
substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p
|
||||
substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p
|
||||
substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p
|
||||
substitutivityᴮ H done v x p = Left p
|
||||
substitutivityᴮ-unless H B v x y (yes p) q = substitutivityᴮ-unless-yes H B v x y p (⊕-over p) q
|
||||
substitutivityᴮ-unless H B v x y (no p) q = substitutivityᴮ-unless-no H B v x y p (⊕-swap p) q
|
||||
substitutivityᴮ-unless-yes H B v x y refl refl p = Left p
|
||||
substitutivityᴮ-unless-no H B v x y p refl q = substitutivityᴮ H B v x q
|
||||
≮:-heap-weakeningᴮ : ∀ Γ H B {H′ U} → (H ⊑ H′) → (typeOfᴮ H′ Γ B ≮: U) → (typeOfᴮ H Γ B ≮: U)
|
||||
≮:-heap-weakeningᴮ Γ H B h p = <:-trans-≮: (<:-heap-weakeningᴮ Γ H B h) p
|
||||
|
||||
binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x))
|
||||
binOpPreservation H (+ m n) = refl
|
||||
|
|
@ -122,24 +105,78 @@ binOpPreservation H (== v w) = refl
|
|||
binOpPreservation H (~= v w) = refl
|
||||
binOpPreservation H (·· v w) = refl
|
||||
|
||||
reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
|
||||
reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))
|
||||
<:-substitutivityᴱ : ∀ {Γ T} H M v x → (typeOfᴱ H ∅ (val v) <: T) → (typeOfᴱ H Γ (M [ v / x ]ᴱ) <: typeOfᴱ H (Γ ⊕ x ↦ T) M)
|
||||
<:-substitutivityᴱ-whenever : ∀ {Γ T} H v x y (r : Dec(x ≡ y)) → (typeOfᴱ H ∅ (val v) <: T) → (typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever r) <: typeOfᴱ H (Γ ⊕ x ↦ T) (var y))
|
||||
<:-substitutivityᴮ : ∀ {Γ T} H B v x → (typeOfᴱ H ∅ (val v) <: T) → (typeOfᴮ H Γ (B [ v / x ]ᴮ) <: typeOfᴮ H (Γ ⊕ x ↦ T) B)
|
||||
<:-substitutivityᴮ-unless : ∀ {Γ T U} H B v x y (r : Dec(x ≡ y)) → (typeOfᴱ H ∅ (val v) <: T) → (typeOfᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r) <: typeOfᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B)
|
||||
<:-substitutivityᴮ-unless-yes : ∀ {Γ Γ′} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless yes r) <: typeOfᴮ H Γ′ B)
|
||||
<:-substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴱ H ∅ (val v) <: T) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless no r) <: typeOfᴮ H Γ′ B)
|
||||
|
||||
reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR never-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-never-≮: p))
|
||||
reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (never-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-never-≮: p)))
|
||||
reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orUnknown (cong typeOfᴹᴼ q))) p)
|
||||
reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p
|
||||
reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p
|
||||
reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p))
|
||||
reflect-subtypingᴱ H (block var b ∈ T is done end) done p = mapR BlockMismatch (swapLR (≮:-trans p))
|
||||
reflect-subtypingᴱ H (binexp M op N) (binOp₀ s) p = Left (≡-trans-≮: (binOpPreservation H s) p)
|
||||
reflect-subtypingᴱ H (binexp M op N) (binOp₁ s) p = Left p
|
||||
reflect-subtypingᴱ H (binexp M op N) (binOp₂ s) p = Left p
|
||||
<:-substitutivityᴱ H (var y) v x p = <:-substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
|
||||
<:-substitutivityᴱ H (val w) v x p = <:-refl
|
||||
<:-substitutivityᴱ H (binexp M op N) v x p = <:-refl
|
||||
<:-substitutivityᴱ H (M $ N) v x p = <:-resolve (<:-substitutivityᴱ H M v x p) (<:-substitutivityᴱ H N v x p)
|
||||
<:-substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = <:-refl
|
||||
<:-substitutivityᴱ H (block var b ∈ T is B end) v x p = <:-refl
|
||||
<:-substitutivityᴱ-whenever H v x x (yes refl) p = p
|
||||
<:-substitutivityᴱ-whenever H v x y (no o) p = (≡-impl-<: (cong orUnknown (⊕-lookup-miss x y _ _ o)))
|
||||
|
||||
reflect-subtypingᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) p = mapLR (heap-weakeningᴮ _ _ B (snoc defn)) (CONTRADICTION ∘ ≮:-refl) (substitutivityᴮ _ B (addr a) f p)
|
||||
reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (local s) p = Left (heap-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) p)
|
||||
reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (subst v) p = mapR LocalVarMismatch (substitutivityᴮ H B v x p)
|
||||
reflect-subtypingᴮ H (return M ∙ B) (return s) p = mapR return (reflect-subtypingᴱ H M s p)
|
||||
<:-substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = <:-substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p
|
||||
<:-substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = <:-substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p
|
||||
<:-substitutivityᴮ H (return M ∙ B) v x p = <:-substitutivityᴱ H M v x p
|
||||
<:-substitutivityᴮ H done v x p = <:-refl
|
||||
<:-substitutivityᴮ-unless H B v x y (yes r) p = <:-substitutivityᴮ-unless-yes H B v x y r (⊕-over r)
|
||||
<:-substitutivityᴮ-unless H B v x y (no r) p = <:-substitutivityᴮ-unless-no H B v x y r (⊕-swap r) p
|
||||
<:-substitutivityᴮ-unless-yes H B v x y refl refl = <:-refl
|
||||
<:-substitutivityᴮ-unless-no H B v x y r refl p = <:-substitutivityᴮ H B v x p
|
||||
|
||||
≮:-substitutivityᴱ : ∀ {Γ T U} H M v x → (typeOfᴱ H Γ (M [ v / x ]ᴱ) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) M ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
≮:-substitutivityᴱ {T = T} H M v x p with dec-subtyping (typeOfᴱ H ∅ (val v)) T
|
||||
≮:-substitutivityᴱ H M v x p | Left q = Right q
|
||||
≮:-substitutivityᴱ H M v x p | Right q = Left (<:-trans-≮: (<:-substitutivityᴱ H M v x q) p)
|
||||
|
||||
≮:-substitutivityᴮ : ∀ {Γ T U} H B v x → (typeOfᴮ H Γ (B [ v / x ]ᴮ) ≮: U) → Either (typeOfᴮ H (Γ ⊕ x ↦ T) B ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
≮:-substitutivityᴮ {T = T} H M v x p with dec-subtyping (typeOfᴱ H ∅ (val v)) T
|
||||
≮:-substitutivityᴮ H M v x p | Left q = Right q
|
||||
≮:-substitutivityᴮ H M v x p | Right q = Left (<:-trans-≮: (<:-substitutivityᴮ H M v x q) p)
|
||||
|
||||
≮:-substitutivityᴮ-unless : ∀ {Γ T U V} H B v x y (r : Dec(x ≡ y)) → (typeOfᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r) ≮: V) → Either (typeOfᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
|
||||
≮:-substitutivityᴮ-unless {T = T} H B v x y r p with dec-subtyping (typeOfᴱ H ∅ (val v)) T
|
||||
≮:-substitutivityᴮ-unless H B v x y r p | Left q = Right q
|
||||
≮:-substitutivityᴮ-unless H B v x y r p | Right q = Left (<:-trans-≮: (<:-substitutivityᴮ-unless H B v x y r q) p)
|
||||
|
||||
<:-reductionᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Either (typeOfᴱ H′ ∅ M′ <: typeOfᴱ H ∅ M) (Warningᴱ H (typeCheckᴱ H ∅ M))
|
||||
<:-reductionᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Either (typeOfᴮ H′ ∅ B′ <: typeOfᴮ H ∅ B) (Warningᴮ H (typeCheckᴮ H ∅ B))
|
||||
|
||||
<:-reductionᴱ H (M $ N) (app₁ s) = mapLR (λ p → <:-resolve p (<:-heap-weakeningᴱ ∅ H N (rednᴱ⊑ s))) app₁ (<:-reductionᴱ H M s)
|
||||
<:-reductionᴱ H (M $ N) (app₂ q s) = mapLR (λ p → <:-resolve (<:-heap-weakeningᴱ ∅ H M (rednᴱ⊑ s)) p) app₂ (<:-reductionᴱ H N s)
|
||||
<:-reductionᴱ H (M $ N) (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) with dec-subtyping (typeOfᴱ H ∅ (val v)) S
|
||||
<:-reductionᴱ H (M $ N) (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) | Left r = Right (FunctionCallMismatch (≮:-trans-≡ r (cong src (cong orUnknown (cong typeOfᴹᴼ (sym q))))))
|
||||
<:-reductionᴱ H (M $ N) (beta (function f ⟨ var y ∈ S ⟩∈ U is B end) v refl q) | Right r = Left (<:-trans-≡ (<:-resolve-⇒ r) (cong (λ F → resolve F (typeOfᴱ H ∅ N)) (cong orUnknown (cong typeOfᴹᴼ (sym q)))))
|
||||
<:-reductionᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = Left <:-refl
|
||||
<:-reductionᴱ H (block var b ∈ T is B end) (block s) = Left <:-refl
|
||||
<:-reductionᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) with dec-subtyping (typeOfᴱ H ∅ (val v)) T
|
||||
<:-reductionᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) | Left p = Right (BlockMismatch p)
|
||||
<:-reductionᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) | Right p = Left p
|
||||
<:-reductionᴱ H (block var b ∈ T is done end) done with dec-subtyping nil T
|
||||
<:-reductionᴱ H (block var b ∈ T is done end) done | Left p = Right (BlockMismatch p)
|
||||
<:-reductionᴱ H (block var b ∈ T is done end) done | Right p = Left p
|
||||
<:-reductionᴱ H (binexp M op N) (binOp₀ s) = Left (≡-impl-<: (sym (binOpPreservation H s)))
|
||||
<:-reductionᴱ H (binexp M op N) (binOp₁ s) = Left <:-refl
|
||||
<:-reductionᴱ H (binexp M op N) (binOp₂ s) = Left <:-refl
|
||||
|
||||
<:-reductionᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) = Left (<:-trans (<:-substitutivityᴮ _ B (addr a) f <:-refl) (<:-heap-weakeningᴮ (f ↦ (T ⇒ U)) H B (snoc defn)))
|
||||
<:-reductionᴮ H (local var x ∈ T ← M ∙ B) (local s) = Left (<:-heap-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s))
|
||||
<:-reductionᴮ H (local var x ∈ T ← M ∙ B) (subst v) with dec-subtyping (typeOfᴱ H ∅ (val v)) T
|
||||
<:-reductionᴮ H (local var x ∈ T ← M ∙ B) (subst v) | Left p = Right (LocalVarMismatch p)
|
||||
<:-reductionᴮ H (local var x ∈ T ← M ∙ B) (subst v) | Right p = Left (<:-substitutivityᴮ H B v x p)
|
||||
<:-reductionᴮ H (return M ∙ B) (return s) = mapR return (<:-reductionᴱ H M s)
|
||||
|
||||
≮:-reductionᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
|
||||
≮:-reductionᴱ H M s p = mapL (λ q → <:-trans-≮: q p) (<:-reductionᴱ H M s)
|
||||
|
||||
≮:-reductionᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))
|
||||
≮:-reductionᴮ H B s p = mapL (λ q → <:-trans-≮: q p) (<:-reductionᴮ H B s)
|
||||
|
||||
reflect-substitutionᴱ : ∀ {Γ T} H M v x → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
|
||||
reflect-substitutionᴱ-whenever : ∀ {Γ T} H v x y (p : Dec(x ≡ y)) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever p)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
|
||||
|
|
@ -150,29 +187,29 @@ reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) →
|
|||
|
||||
reflect-substitutionᴱ H (var y) v x W = reflect-substitutionᴱ-whenever H v x y (x ≡ⱽ y) W
|
||||
reflect-substitutionᴱ H (val (addr a)) v x (UnallocatedAddress r) = Left (UnallocatedAddress r)
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with substitutivityᴱ H N v x p
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with ≮:-substitutivityᴱ H N v x p
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Right W = Right (Right W)
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-unknown-≮: q)
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with ≮:-substitutivityᴱ H M v x (src-unknown-≮: q)
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ unknown-src-≮: q) r)
|
||||
reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Right W = Right (Right W)
|
||||
reflect-substitutionᴱ H (M $ N) v x (app₁ W) = mapL app₁ (reflect-substitutionᴱ H M v x W)
|
||||
reflect-substitutionᴱ H (M $ N) v x (app₂ W) = mapL app₂ (reflect-substitutionᴱ H N v x W)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H B v x y (x ≡ⱽ y) q)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (≮:-substitutivityᴮ-unless H B v x y (x ≡ⱽ y) q)
|
||||
reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (function₁ W) = mapL function₁ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x (BlockMismatch q) = mapLR BlockMismatch Right (substitutivityᴮ H B v x q)
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x (BlockMismatch q) = mapLR BlockMismatch Right (≮:-substitutivityᴮ H B v x q)
|
||||
reflect-substitutionᴱ H (block var b ∈ T is B end) v x (block₁ W′) = mapL block₁ (reflect-substitutionᴮ H B v x W′)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₁ q) = mapLR BinOpMismatch₁ Right (substitutivityᴱ H M v x q)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₂ q) = mapLR BinOpMismatch₂ Right (substitutivityᴱ H N v x q)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₁ q) = mapLR BinOpMismatch₁ Right (≮:-substitutivityᴱ H M v x q)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₂ q) = mapLR BinOpMismatch₂ Right (≮:-substitutivityᴱ H N v x q)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (bin₁ W) = mapL bin₁ (reflect-substitutionᴱ H M v x W)
|
||||
reflect-substitutionᴱ H (binexp M op N) v x (bin₂ W) = mapL bin₂ (reflect-substitutionᴱ H N v x W)
|
||||
|
||||
reflect-substitutionᴱ-whenever H a x x (yes refl) (UnallocatedAddress p) = Right (Left (UnallocatedAddress p))
|
||||
reflect-substitutionᴱ-whenever H v x y (no p) (UnboundVariable q) = Left (UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) q))
|
||||
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H C v x y (x ≡ⱽ y) q)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (≮:-substitutivityᴮ-unless H C v x y (x ≡ⱽ y) q)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₁ W) = mapL function₁ (reflect-substitutionᴮ-unless H C v x y (x ≡ⱽ y) W)
|
||||
reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₂ W) = mapL function₂ (reflect-substitutionᴮ-unless H B v x f (x ≡ⱽ f) W)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (LocalVarMismatch q) = mapLR LocalVarMismatch Right (substitutivityᴱ H M v x q)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (LocalVarMismatch q) = mapLR LocalVarMismatch Right (≮:-substitutivityᴱ H M v x q)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₁ W) = mapL local₁ (reflect-substitutionᴱ H M v x W)
|
||||
reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₂ W) = mapL local₂ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
|
||||
reflect-substitutionᴮ H (return M ∙ B) v x (return W) = mapL return (reflect-substitutionᴱ H M v x W)
|
||||
|
|
@ -187,61 +224,61 @@ reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (t
|
|||
|
||||
reflect-weakeningᴱ Γ H (var x) h (UnboundVariable p) = (UnboundVariable p)
|
||||
reflect-weakeningᴱ Γ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
|
||||
reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (unknown-src-≮: p (heap-weakeningᴱ Γ H M h (src-unknown-≮: p))))
|
||||
reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (≮:-heap-weakeningᴱ Γ H N h (unknown-src-≮: p (≮:-heap-weakeningᴱ Γ H M h (src-unknown-≮: p))))
|
||||
reflect-weakeningᴱ Γ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ Γ H M h W)
|
||||
reflect-weakeningᴱ Γ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ Γ H N h W)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₁ p) = BinOpMismatch₁ (heap-weakeningᴱ Γ H M h p)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₂ p) = BinOpMismatch₂ (heap-weakeningᴱ Γ H N h p)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₁ p) = BinOpMismatch₁ (≮:-heap-weakeningᴱ Γ H M h p)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₂ p) = BinOpMismatch₂ (≮:-heap-weakeningᴱ Γ H N h p)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ Γ H M h W′)
|
||||
reflect-weakeningᴱ Γ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ Γ H N h W′)
|
||||
reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ y ↦ T) H B h p)
|
||||
reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (≮:-heap-weakeningᴮ (Γ ⊕ y ↦ T) H B h p)
|
||||
reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
|
||||
reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (BlockMismatch p) = BlockMismatch (heap-weakeningᴮ Γ H B h p)
|
||||
reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (BlockMismatch p) = BlockMismatch (≮:-heap-weakeningᴮ Γ H B h p)
|
||||
reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ Γ H B h W)
|
||||
|
||||
reflect-weakeningᴮ Γ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ Γ H M h W)
|
||||
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) = LocalVarMismatch (heap-weakeningᴱ Γ H M h p)
|
||||
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) = LocalVarMismatch (≮:-heap-weakeningᴱ Γ H M h p)
|
||||
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ Γ H M h W)
|
||||
reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
|
||||
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ x ↦ T) H C h p)
|
||||
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) = FunctionDefnMismatch (≮:-heap-weakeningᴮ (Γ ⊕ x ↦ T) H C h p)
|
||||
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ x ↦ T) H C h W)
|
||||
reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h W)
|
||||
|
||||
reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
|
||||
reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B h p)
|
||||
reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (≮:-heap-weakeningᴮ (x ↦ T) H B h p)
|
||||
reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (x ↦ T) H B h W)
|
||||
|
||||
reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H))
|
||||
reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))
|
||||
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ unknown-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-unknown-≮: p))
|
||||
reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ ≮:-heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ unknown-src-≮: p) (Left ∘ app₁) (≮:-reductionᴱ H M s (src-unknown-≮: p))
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₁ W′) = mapL app₁ (reflectᴱ H M s W′)
|
||||
reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = Left (app₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (unknown-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-unknown-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (unknown-src-≮: r (≮:-heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-unknown-≮: r))))) (Left ∘ app₂) (≮:-reductionᴱ H N s q)
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = Left (app₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) = mapL app₂ (reflectᴱ H N s W′)
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with substitutivityᴮ H B v x q
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with ≮:-substitutivityᴮ H B v x q
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Left r = Right (addr a p (FunctionDefnMismatch r))
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orUnknown (cong typeOfᴹᴼ (sym p)))))))
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with reflect-substitutionᴮ _ B v x W′
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Left W = Right (addr a p (function₁ W))
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Left W) = Left (app₂ W)
|
||||
reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orUnknown (cong typeOfᴹᴼ (sym p))))))
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (reflect-subtypingᴮ H B s p))
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (≮:-reductionᴮ H B s p))
|
||||
reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) = mapL block₁ (reflectᴮ H B s W′)
|
||||
reflectᴱ H (block var b ∈ T is B end) (return v) W′ = Left (block₁ (return W′))
|
||||
reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
|
||||
reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) = Left (cond BinOpMismatch₁ bin₁ (reflect-subtypingᴱ H M s p))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) = Left (BinOpMismatch₂ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) = Left (cond BinOpMismatch₁ bin₁ (≮:-reductionᴱ H M s p))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) = Left (BinOpMismatch₂ (≮:-heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) = mapL bin₁ (reflectᴱ H M s W′)
|
||||
reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = Left (bin₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) = Left (BinOpMismatch₁ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) = Left (cond BinOpMismatch₂ bin₂ (reflect-subtypingᴱ H N s p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) = Left (BinOpMismatch₁ (≮:-heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) = Left (cond BinOpMismatch₂ bin₂ (≮:-reductionᴱ H N s p))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = Left (bin₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
|
||||
reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) = mapL bin₂ (reflectᴱ H N s W′)
|
||||
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) = Left (cond LocalVarMismatch local₁ (reflect-subtypingᴱ H M s p))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) = Left (cond LocalVarMismatch local₁ (≮:-reductionᴱ H M s p))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) = mapL local₁ (reflectᴱ H M s W′)
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = Left (local₂ (reflect-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) W′))
|
||||
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ = Left (cond local₂ (cond local₁ LocalVarMismatch) (reflect-substitutionᴮ H B v x W′))
|
||||
|
|
@ -258,7 +295,7 @@ reflectᴴᴱ H (M $ N) (app₁ s) W = mapL app₁ (reflectᴴᴱ H M s W)
|
|||
reflectᴴᴱ H (M $ N) (app₂ v s) W = mapL app₂ (reflectᴴᴱ H N s W)
|
||||
reflectᴴᴱ H (M $ N) (beta O v refl p) W = Right W
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) with b ≡ᴬ a
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B (snoc defn) p))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (≮:-heap-weakeningᴮ (x ↦ T) H B (snoc defn) p))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H B (snoc defn) W))
|
||||
reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
|
||||
reflectᴴᴱ H (block var b ∈ T is B end) (block s) W = mapL block₁ (reflectᴴᴮ H B s W)
|
||||
|
|
@ -269,7 +306,7 @@ reflectᴴᴱ H (binexp M op N) (binOp₁ s) W = mapL bin₁ (reflectᴴᴱ H M
|
|||
reflectᴴᴱ H (binexp M op N) (binOp₂ s) W = mapL bin₂ (reflectᴴᴱ H N s W)
|
||||
|
||||
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) with b ≡ᴬ a
|
||||
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H C (snoc defn) p))
|
||||
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (≮:-heap-weakeningᴮ (x ↦ T) H C (snoc defn) p))
|
||||
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H C (snoc defn) W))
|
||||
reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
|
||||
reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) W = mapL local₁ (reflectᴴᴱ H M s W)
|
||||
|
|
|
|||
|
|
@ -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 (_<:_; _≮:_; 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.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; 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.Equality using (_≢_)
|
||||
|
|
@ -19,37 +19,42 @@ dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
|
|||
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-ok s t) = Left (scalar-function-ok 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-ok s t) = Left (scalar-function-ok 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-ok s t) = Left (scalar-function-ok 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-ok s t) = Left (scalar-function-ok 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)
|
||||
dec-language (T₁ ⇒ T₂) (function-ok s t) = cond (Right ∘ function-ok₁) (λ p → mapLR (function-ok p) function-ok₂ (dec-language T₂ t)) (dec-language T₁ s)
|
||||
dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
|
||||
dec-language never t = Left never
|
||||
dec-language unknown t = Right unknown
|
||||
dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
|
||||
dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
|
||||
dec-language nil (function-tgt t) = Left (scalar-function-tgt nil)
|
||||
dec-language (T₁ ⇒ T₂) (function-tgt t) = mapLR function-tgt function-tgt (dec-language T₂ t)
|
||||
dec-language boolean (function-tgt t) = Left (scalar-function-tgt boolean)
|
||||
dec-language number (function-tgt t) = Left (scalar-function-tgt number)
|
||||
dec-language string (function-tgt t) = Left (scalar-function-tgt string)
|
||||
|
||||
-- ¬Language T is the complement of Language T
|
||||
language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
|
||||
|
|
@ -61,9 +66,12 @@ language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
|
|||
language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
|
||||
language-comp (scalar s) never (scalar ())
|
||||
language-comp function (scalar-function ()) function
|
||||
language-comp (function-ok t) (scalar-function-ok ()) (function-ok q)
|
||||
language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q
|
||||
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
|
||||
language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ p)
|
||||
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₁ q) = language-comp s q p₁
|
||||
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₂ q) = language-comp t p₂ q
|
||||
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
|
||||
language-comp (function-tgt t) (scalar-function-tgt ()) (function-tgt q)
|
||||
language-comp (function-tgt t) (function-tgt p) (function-tgt q) = language-comp t p q
|
||||
|
||||
-- ≮: is the complement of <:
|
||||
¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
|
||||
|
|
@ -90,9 +98,18 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
≮:-trans-≡ : ∀ {S T U} → (S ≮: T) → (T ≡ U) → (S ≮: U)
|
||||
≮:-trans-≡ p refl = p
|
||||
|
||||
<:-trans-≡ : ∀ {S T U} → (S <: T) → (T ≡ U) → (S <: U)
|
||||
<:-trans-≡ p refl = p
|
||||
|
||||
≡-impl-<: : ∀ {T U} → (T ≡ U) → (T <: U)
|
||||
≡-impl-<: refl = <:-refl
|
||||
|
||||
≡-trans-≮: : ∀ {S T U} → (S ≡ T) → (T ≮: U) → (S ≮: U)
|
||||
≡-trans-≮: refl p = p
|
||||
|
||||
≡-trans-<: : ∀ {S T U} → (S ≡ T) → (T <: U) → (S <: U)
|
||||
≡-trans-<: refl p = p
|
||||
|
||||
≮:-trans : ∀ {S T U} → (S ≮: U) → Either (S ≮: T) (T ≮: U)
|
||||
≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)
|
||||
|
||||
|
|
@ -141,6 +158,12 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
≮:-∪-right : ∀ {S T U} → (T ≮: U) → ((S ∪ T) ≮: U)
|
||||
≮:-∪-right (witness t p q) = witness t (right p) q
|
||||
|
||||
≮:-left-∪ : ∀ {S T U} → (S ≮: (T ∪ U)) → (S ≮: T)
|
||||
≮:-left-∪ (witness t p (q₁ , q₂)) = witness t p q₁
|
||||
|
||||
≮:-right-∪ : ∀ {S T U} → (S ≮: (T ∪ U)) → (S ≮: U)
|
||||
≮:-right-∪ (witness t p (q₁ , q₂)) = witness t p q₂
|
||||
|
||||
-- Properties of intersection
|
||||
|
||||
<:-intersect : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∩ S) <: (T ∩ U))
|
||||
|
|
@ -158,6 +181,12 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
|
||||
<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
|
||||
|
||||
<:-∩-assocl : ∀ {S T U} → (S ∩ (T ∩ U)) <: ((S ∩ T) ∩ U)
|
||||
<:-∩-assocl t (p , (p₁ , p₂)) = (p , p₁) , p₂
|
||||
|
||||
<:-∩-assocr : ∀ {S T U} → ((S ∩ T) ∩ U) <: (S ∩ (T ∩ U))
|
||||
<:-∩-assocr t ((p , p₁) , p₂) = p , (p₁ , p₂)
|
||||
|
||||
≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
|
||||
≮:-∩-left (witness t p q) = witness t p (left q)
|
||||
|
||||
|
|
@ -199,47 +228,84 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
|
|||
∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
|
||||
∪-distr-∩-<: t (right p₁ , p₂) = right p₁
|
||||
|
||||
∩-<:-∪ : ∀ {S T} → (S ∩ T) <: (S ∪ T)
|
||||
∩-<:-∪ t (p , _) = left 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-ok s t) (function-ok₁ r) = function-ok₁ (<:-impl-⊇ p s r)
|
||||
<:-function p q (function-ok s 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 p q (function-tgt t) (function-tgt r) = function-tgt (q t r)
|
||||
|
||||
<:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U))
|
||||
<:-function-∩-∩ function (function , function) = function
|
||||
<:-function-∩-∩ (function-ok s t) (function-ok₁ p , q) = function-ok₁ (left p)
|
||||
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₁ q) = function-ok₁ (right q)
|
||||
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₂ q) = function-ok₂ (p , q)
|
||||
<:-function-∩-∩ (function-err s) (function-err p , q) = function-err (left p)
|
||||
<:-function-∩-∩ (function-tgt s) (function-tgt p , function-tgt q) = function-tgt (p , q)
|
||||
|
||||
<:-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-∩-∪ (function-ok s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂)
|
||||
<:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
|
||||
<:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
|
||||
<:-function-∩-∪ (function-err s) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
|
||||
<:-function-∩-∪ (function-tgt t) (function-tgt p , q) = function-tgt (left p)
|
||||
|
||||
<:-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-ok s t) (p₁ , function-ok₁ p₂) = function-ok₁ p₂
|
||||
<:-function-∩ (function-ok s t) (function-ok₁ p₁ , p₂) = function-ok₁ p₁
|
||||
<:-function-∩ (function-ok s 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-∩ (function-tgt t) (function-tgt p₁ , function-tgt p₂) = function-tgt (p₁ , 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-ok s t) (left (function-ok₁ p)) = function-ok₁ (left p)
|
||||
<:-function-∪ (function-ok s 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-ok s t) (right (function-ok₁ p)) = function-ok₁ (right p)
|
||||
<:-function-∪ (function-ok s 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-∪ (function-tgt t) (left (function-tgt p)) = function-tgt (left p)
|
||||
<:-function-∪ (function-tgt t) (right (function-tgt p)) = function-tgt (right p)
|
||||
|
||||
<:-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-ok s t) (function-ok₁ (left p)) = left (function-ok₁ p)
|
||||
<:-function-∪-∩ (function-ok s t) (function-ok₂ (left p)) = left (function-ok₂ p)
|
||||
<:-function-∪-∩ (function-ok s t) (function-ok₁ (right p)) = right (function-ok₁ p)
|
||||
<:-function-∪-∩ (function-ok s 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-∪-∩ (function-tgt t) (function-tgt (left p)) = left (function-tgt p)
|
||||
<:-function-∪-∩ (function-tgt t) (function-tgt (right p)) = right (function-tgt p)
|
||||
|
||||
<:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S)
|
||||
<:-function-left {R} {S} p s Rs with dec-language S s
|
||||
<:-function-left p s Rs | Right Ss = Ss
|
||||
<:-function-left p s Rs | Left ¬Ss with p (function-err s) (function-err ¬Ss)
|
||||
<:-function-left p s Rs | Left ¬Ss | function-err ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)
|
||||
|
||||
<:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (T <: U)
|
||||
<:-function-right p t Tt with p (function-tgt t) (function-tgt Tt)
|
||||
<:-function-right p t Tt | function-tgt St = St
|
||||
|
||||
≮:-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)
|
||||
≮:-function-right (witness t p q) = witness (function-tgt t) (function-tgt p) (function-tgt q)
|
||||
|
||||
-- Properties of scalars
|
||||
skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
|
||||
skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s 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)
|
||||
|
|
@ -261,7 +327,7 @@ scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
|
|||
scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)
|
||||
|
||||
unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U)
|
||||
unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s)
|
||||
unknown-≮:-scalar s = witness function unknown (scalar-function s)
|
||||
|
||||
scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never)
|
||||
scalar-≮:-never s = witness (scalar s) (scalar s) never
|
||||
|
|
@ -288,6 +354,9 @@ never-≮: (witness t p q) = witness t p never
|
|||
unknown-≮:-never : (unknown ≮: never)
|
||||
unknown-≮:-never = witness (scalar nil) unknown never
|
||||
|
||||
unknown-≮:-function : ∀ {S T} → (unknown ≮: (S ⇒ T))
|
||||
unknown-≮:-function = witness (scalar nil) unknown (function-scalar nil)
|
||||
|
||||
function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never)
|
||||
function-≮:-never = witness function function never
|
||||
|
||||
|
|
@ -310,8 +379,9 @@ function-≮:-never = witness function function never
|
|||
<:-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-ok s t) p = left (function-ok₁ never)
|
||||
<:-everything (function-err s) p = left (function-err never)
|
||||
<:-everything (function-tgt t) p = left (function-tgt unknown)
|
||||
|
||||
-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
|
||||
-- defines a "set-theoretic" model (sec 2.5)
|
||||
|
|
@ -351,8 +421,9 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T
|
|||
S₁t | Right r = r
|
||||
|
||||
¬T₁u : ¬(Language 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
|
||||
¬T₁u T₁u with p (function-ok t u) (function-ok₂ T₁u)
|
||||
¬T₁u T₁u | function-ok₁ ¬S₂t = language-comp t ¬S₂t S₂t
|
||||
¬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
|
||||
|
||||
|
|
@ -365,33 +436,41 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _)
|
|||
not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
|
||||
|
||||
-- We don't quite have that this is a set-theoretic model
|
||||
-- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited
|
||||
-- in particular it's not true when T₁ is never, or T₂ is unknown.
|
||||
∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ →
|
||||
-- it's only true when Language S₂ is inhabited
|
||||
-- in particular it's not true when S₂ is never,
|
||||
∀ s₂ → Language S₂ s₂ →
|
||||
|
||||
-- This is the "only if" part of being a set-theoretic model
|
||||
(∀ 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
|
||||
not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ S₂s₂ p = r where
|
||||
|
||||
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(Lift(Language T₁)))
|
||||
|
||||
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 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₂ , 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
|
||||
r (function-ok s t) (function-ok₁ ¬S₁s) with dec-language S₂ s
|
||||
r (function-ok s t) (function-ok₁ ¬S₁s) | Left ¬S₂s = function-ok₁ ¬S₂s
|
||||
r (function-ok s t) (function-ok₁ ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
|
||||
r (function-ok s t) (function-ok₂ T₁t) with dec-language T₂ t
|
||||
r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t with dec-language S₂ s
|
||||
r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Left ¬S₂s = function-ok₁ ¬S₂s
|
||||
r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Right S₂s = CONTRADICTION (p Q q (s , just t) (Right T₁t) (S₂s , language-comp t ¬T₂t))
|
||||
r (function-ok s t) (function-ok₂ T₁t) | Right T₂t = function-ok₂ T₂t
|
||||
r (function-tgt t) (function-tgt T₁t) with dec-language T₂ t
|
||||
r (function-tgt t) (function-tgt T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
|
||||
r (function-tgt t) (function-tgt T₁t) | Right T₂t = function-tgt T₂t
|
||||
|
||||
-- A counterexample when the argument type is empty.
|
||||
|
||||
|
|
@ -399,22 +478,4 @@ set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Co
|
|||
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
|
||||
|
||||
set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
|
||||
set-theoretic-counterexample-two = witness
|
||||
(function-ok (scalar number)) (function-ok (scalar number))
|
||||
(function-ok (scalar-scalar number string (λ ())))
|
||||
|
||||
-- At some point we may deal with overloaded function resolution, which should fix this problem...
|
||||
-- The reason why this is connected to overloaded functions is that currently we have that the type of
|
||||
-- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U),
|
||||
-- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V)
|
||||
-- and tgt(never => T) should be unknown. For example
|
||||
--
|
||||
-- tgt((number => string) & (string => bool))(number)
|
||||
-- is tgt(number => string)(number) & tgt(string => bool)(number)
|
||||
-- is tgt(number => string)(number) & tgt(string => bool)(number&unknown)
|
||||
-- is tgt(number => string)(number) & tgt(string&number => bool)(unknown)
|
||||
-- is tgt(number => string)(number) & tgt(never => bool)(unknown)
|
||||
-- is string & unknown
|
||||
-- is string
|
||||
--
|
||||
-- there's some discussion of this in the Gentle Introduction paper.
|
||||
set-theoretic-counterexample-two = witness (function-tgt (scalar number)) (function-tgt (scalar number)) (function-tgt (scalar-scalar number string (λ ())))
|
||||
|
|
|
|||
|
|
@ -6,9 +6,9 @@ open import Agda.Builtin.Equality using (_≡_; refl)
|
|||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import FFI.Data.Either using (Either)
|
||||
open import Luau.ResolveOverloads using (resolve)
|
||||
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.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 _[_]ⱽ)
|
||||
|
|
@ -40,7 +40,7 @@ typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
|
|||
|
||||
typeOfᴱ H Γ (var x) = orUnknown(Γ [ x ]ⱽ)
|
||||
typeOfᴱ H Γ (val v) = orUnknown(typeOfⱽ H v)
|
||||
typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M)
|
||||
typeOfᴱ H Γ (M $ N) = resolve (typeOfᴱ H Γ M) (typeOfᴱ H Γ N)
|
||||
typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T
|
||||
typeOfᴱ H Γ (block var b ∈ T is B end) = T
|
||||
typeOfᴱ H Γ (binexp M op N) = tgtBinOp op
|
||||
|
|
@ -50,14 +50,6 @@ typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B
|
|||
typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M
|
||||
typeOfᴮ H Γ done = nil
|
||||
|
||||
mustBeFunction : ∀ H Γ v → (never ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v))
|
||||
mustBeFunction H Γ nil p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (addr a) p = refl
|
||||
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (string x) p = CONTRADICTION (p refl)
|
||||
|
||||
mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
|
||||
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
|
||||
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p
|
||||
|
|
|
|||
|
|
@ -3,12 +3,12 @@
|
|||
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.Subtyping using (Tree; Language; ¬Language; function; scalar; unknown; left; right; function-ok₁; function-ok₂; function-err; function-tgt; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; function-scalar; _,_)
|
||||
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
|
||||
open import Luau.Subtyping using (_<:_)
|
||||
open import Luau.Subtyping using (_<:_; _≮:_; witness; never)
|
||||
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
|
||||
-- Normal forms for types
|
||||
data FunType : Type → Set
|
||||
data Normal : Type → Set
|
||||
|
||||
|
|
@ -17,11 +17,11 @@ data FunType where
|
|||
_∩_ : ∀ {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)
|
||||
never : Normal never
|
||||
unknown : Normal unknown
|
||||
|
||||
data OptScalar : Type → Set where
|
||||
never : OptScalar never
|
||||
|
|
@ -30,6 +30,38 @@ data OptScalar : Type → Set where
|
|||
string : OptScalar string
|
||||
nil : OptScalar nil
|
||||
|
||||
-- Top function type
|
||||
fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
|
||||
fun-top (S ⇒ T) = <:-function <:-never <:-unknown
|
||||
fun-top (F ∩ G) = <:-trans <:-∩-left (fun-top F)
|
||||
|
||||
-- function types are inhabited
|
||||
fun-function : ∀ {F} → FunType F → Language F function
|
||||
fun-function (S ⇒ T) = function
|
||||
fun-function (F ∩ G) = (fun-function F , fun-function G)
|
||||
|
||||
fun-≮:-never : ∀ {F} → FunType F → (F ≮: never)
|
||||
fun-≮:-never F = witness function (fun-function F) never
|
||||
|
||||
-- function types aren't scalars
|
||||
fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F 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-ok₂ p) = scalar-function-ok s
|
||||
fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
|
||||
fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
|
||||
fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
|
||||
|
||||
¬scalar-fun : ∀ {F S} → FunType F → (s : Scalar S) → ¬Language F (scalar s)
|
||||
¬scalar-fun (S ⇒ T) s = function-scalar s
|
||||
¬scalar-fun (F ∩ G) s = left (¬scalar-fun F s)
|
||||
|
||||
scalar-≮:-fun : ∀ {F S} → FunType F → Scalar S → S ≮: F
|
||||
scalar-≮:-fun F s = witness (scalar s) (scalar s) (¬scalar-fun F s)
|
||||
|
||||
unknown-≮:-fun : ∀ {F} → FunType F → unknown ≮: F
|
||||
unknown-≮:-fun F = witness (scalar nil) unknown (¬scalar-fun F nil)
|
||||
|
||||
-- Normalization produces normal types
|
||||
normal : ∀ T → Normal (normalize T)
|
||||
normalᶠ : ∀ {F} → FunType F → Normal F
|
||||
|
|
@ -40,7 +72,7 @@ normal-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → OptScalar (S ∩ⁿˢ
|
|||
normal-∪ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∪ᶠ G)
|
||||
|
||||
normal nil = never ∪ nil
|
||||
normal (S ⇒ T) = normalᶠ ((normal S) ⇒ (normal T))
|
||||
normal (S ⇒ T) = (normal S) ⇒ (normal T)
|
||||
normal never = never
|
||||
normal unknown = unknown
|
||||
normal boolean = never ∪ boolean
|
||||
|
|
@ -338,7 +370,7 @@ flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪
|
|||
∪-<:-∪ⁿ 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)))
|
||||
∪-<:-∪ⁿ (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)
|
||||
|
|
|
|||
433
prototyping/Properties/TypeSaturation.agda
Normal file
433
prototyping/Properties/TypeSaturation.agda
Normal file
|
|
@ -0,0 +1,433 @@
|
|||
{-# OPTIONS --rewriting #-}
|
||||
|
||||
module Properties.TypeSaturation where
|
||||
|
||||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||||
open import FFI.Data.Either using (Either; Left; Right)
|
||||
open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witness; scalar; function; function-err; function-ok; function-ok₁; function-ok₂; scalar-function; _,_; never)
|
||||
open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
|
||||
open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
|
||||
open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate)
|
||||
open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
|
||||
open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
|
||||
open import Properties.Contradiction using (CONTRADICTION)
|
||||
open import Properties.Functions using (_∘_)
|
||||
|
||||
-- Saturation preserves normalization
|
||||
normal-⋒ : ∀ {F G} → FunType F → FunType G → FunType (F ⋒ G)
|
||||
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
|
||||
|
||||
normal-⋓ : ∀ {F G} → FunType F → FunType G → FunType (F ⋓ G)
|
||||
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
|
||||
|
||||
normal-∩-saturate : ∀ {F} → FunType F → FunType (∩-saturate F)
|
||||
normal-∩-saturate (S ⇒ T) = S ⇒ T
|
||||
normal-∩-saturate (F ∩ G) = (normal-∩-saturate F ∩ normal-∩-saturate G) ∩ normal-⋒ (normal-∩-saturate F) (normal-∩-saturate G)
|
||||
|
||||
normal-∪-saturate : ∀ {F} → FunType F → FunType (∪-saturate F)
|
||||
normal-∪-saturate (S ⇒ T) = S ⇒ T
|
||||
normal-∪-saturate (F ∩ G) = (normal-∪-saturate F ∩ normal-∪-saturate G) ∩ normal-⋓ (normal-∪-saturate F) (normal-∪-saturate G)
|
||||
|
||||
normal-saturate : ∀ {F} → FunType F → FunType (saturate F)
|
||||
normal-saturate F = normal-∪-saturate (normal-∩-saturate F)
|
||||
|
||||
-- Saturation resects subtyping
|
||||
∪-saturate-<: : ∀ {F} → FunType F → ∪-saturate F <: F
|
||||
∪-saturate-<: (S ⇒ T) = <:-refl
|
||||
∪-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∪-saturate-<: F) (∪-saturate-<: G))
|
||||
|
||||
∩-saturate-<: : ∀ {F} → FunType F → ∩-saturate F <: F
|
||||
∩-saturate-<: (S ⇒ T) = <:-refl
|
||||
∩-saturate-<: (F ∩ G) = <:-trans <:-∩-left (<:-intersect (∩-saturate-<: F) (∩-saturate-<: G))
|
||||
|
||||
saturate-<: : ∀ {F} → FunType F → saturate F <: F
|
||||
saturate-<: F = <:-trans (∪-saturate-<: (normal-∩-saturate F)) (∩-saturate-<: F)
|
||||
|
||||
∩-<:-⋓ : ∀ {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 (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋓ (R ⇒ S) G) (∩-<:-⋓ (R ⇒ S) H))
|
||||
∩-<:-⋓ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋓ E G) (∩-<:-⋓ F G))
|
||||
|
||||
∩-<:-⋒ : ∀ {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 (<:-∩-glb (<:-intersect <:-refl <:-∩-left) (<:-intersect <:-refl <:-∩-right)) (<:-intersect (∩-<:-⋒ (R ⇒ S) G) (∩-<:-⋒ (R ⇒ S) H))
|
||||
∩-<:-⋒ (E ∩ F) G = <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-intersect <:-∩-right <:-refl)) (<:-intersect (∩-<:-⋒ E G) (∩-<:-⋒ F G))
|
||||
|
||||
<:-∪-saturate : ∀ {F} → FunType F → F <: ∪-saturate F
|
||||
<:-∪-saturate (S ⇒ T) = <:-refl
|
||||
<:-∪-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (<:-trans (<:-intersect (<:-∪-saturate F) (<:-∪-saturate G)) (∩-<:-⋓ (normal-∪-saturate F) (normal-∪-saturate G)))
|
||||
|
||||
<:-∩-saturate : ∀ {F} → FunType F → F <: ∩-saturate F
|
||||
<:-∩-saturate (S ⇒ T) = <:-refl
|
||||
<:-∩-saturate (F ∩ G) = <:-∩-glb (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (<:-trans (<:-intersect (<:-∩-saturate F) (<:-∩-saturate G)) (∩-<:-⋒ (normal-∩-saturate F) (normal-∩-saturate G)))
|
||||
|
||||
<:-saturate : ∀ {F} → FunType F → F <: saturate F
|
||||
<:-saturate F = <:-trans (<:-∩-saturate F) (<:-∪-saturate (normal-∩-saturate F))
|
||||
|
||||
-- Overloads F is the set of overloads of F
|
||||
data Overloads : Type → Type → Set where
|
||||
|
||||
here : ∀ {S T} → Overloads (S ⇒ T) (S ⇒ T)
|
||||
left : ∀ {S T F G} → Overloads F (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
|
||||
right : ∀ {S T F G} → Overloads G (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
|
||||
|
||||
normal-overload-src : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal S
|
||||
normal-overload-src (S ⇒ T) here = S
|
||||
normal-overload-src (F ∩ G) (left o) = normal-overload-src F o
|
||||
normal-overload-src (F ∩ G) (right o) = normal-overload-src G o
|
||||
|
||||
normal-overload-tgt : ∀ {F S T} → FunType F → Overloads F (S ⇒ T) → Normal T
|
||||
normal-overload-tgt (S ⇒ T) here = T
|
||||
normal-overload-tgt (F ∩ G) (left o) = normal-overload-tgt F o
|
||||
normal-overload-tgt (F ∩ G) (right o) = normal-overload-tgt G o
|
||||
|
||||
-- An inductive presentation of the overloads of F ⋓ G
|
||||
data ∪-Lift (P Q : Type → Set) : Type → Set where
|
||||
|
||||
union : ∀ {R S T U} →
|
||||
|
||||
P (R ⇒ S) →
|
||||
Q (T ⇒ U) →
|
||||
--------------------
|
||||
∪-Lift P Q ((R ∪ T) ⇒ (S ∪ U))
|
||||
|
||||
-- An inductive presentation of the overloads of F ⋒ G
|
||||
data ∩-Lift (P Q : Type → Set) : Type → Set where
|
||||
|
||||
intersect : ∀ {R S T U} →
|
||||
|
||||
P (R ⇒ S) →
|
||||
Q (T ⇒ U) →
|
||||
--------------------
|
||||
∩-Lift P Q ((R ∩ T) ⇒ (S ∩ U))
|
||||
|
||||
-- An inductive presentation of the overloads of ∪-saturate F
|
||||
data ∪-Saturate (P : Type → Set) : Type → Set where
|
||||
|
||||
base : ∀ {S T} →
|
||||
|
||||
P (S ⇒ T) →
|
||||
--------------------
|
||||
∪-Saturate P (S ⇒ T)
|
||||
|
||||
union : ∀ {R S T U} →
|
||||
|
||||
∪-Saturate P (R ⇒ S) →
|
||||
∪-Saturate P (T ⇒ U) →
|
||||
--------------------
|
||||
∪-Saturate P ((R ∪ T) ⇒ (S ∪ U))
|
||||
|
||||
-- An inductive presentation of the overloads of ∩-saturate F
|
||||
data ∩-Saturate (P : Type → Set) : Type → Set where
|
||||
|
||||
base : ∀ {S T} →
|
||||
|
||||
P (S ⇒ T) →
|
||||
--------------------
|
||||
∩-Saturate P (S ⇒ T)
|
||||
|
||||
intersect : ∀ {R S T U} →
|
||||
|
||||
∩-Saturate P (R ⇒ S) →
|
||||
∩-Saturate P (T ⇒ U) →
|
||||
--------------------
|
||||
∩-Saturate P ((R ∩ T) ⇒ (S ∩ U))
|
||||
|
||||
-- The <:-up-closure of a set of function types
|
||||
data <:-Close (P : Type → Set) : Type → Set where
|
||||
|
||||
defn : ∀ {R S T U} →
|
||||
|
||||
P (S ⇒ T) →
|
||||
R <: S →
|
||||
T <: U →
|
||||
------------------
|
||||
<:-Close P (R ⇒ U)
|
||||
|
||||
-- F ⊆ᵒ G whenever every overload of F is an overload of G
|
||||
_⊆ᵒ_ : Type → Type → Set
|
||||
F ⊆ᵒ G = ∀ {S T} → Overloads F (S ⇒ T) → Overloads G (S ⇒ T)
|
||||
|
||||
-- F <:ᵒ G when every overload of G is a supertype of an overload of F
|
||||
_<:ᵒ_ : Type → Type → Set
|
||||
_<:ᵒ_ F G = ∀ {S T} → Overloads G (S ⇒ T) → <:-Close (Overloads F) (S ⇒ T)
|
||||
|
||||
-- P ⊂: Q when any type in P is a subtype of some type in Q
|
||||
_⊂:_ : (Type → Set) → (Type → Set) → Set
|
||||
P ⊂: Q = ∀ {S T} → P (S ⇒ T) → <:-Close Q (S ⇒ T)
|
||||
|
||||
-- <:-Close is a monad
|
||||
just : ∀ {P S T} → P (S ⇒ T) → <:-Close P (S ⇒ T)
|
||||
just p = defn p <:-refl <:-refl
|
||||
|
||||
infixl 5 _>>=_ _>>=ˡ_ _>>=ʳ_
|
||||
_>>=_ : ∀ {P Q S T} → <:-Close P (S ⇒ T) → (P ⊂: Q) → <:-Close Q (S ⇒ T)
|
||||
(defn p p₁ p₂) >>= P⊂Q with P⊂Q p
|
||||
(defn p p₁ p₂) >>= P⊂Q | defn q q₁ q₂ = defn q (<:-trans p₁ q₁) (<:-trans q₂ p₂)
|
||||
|
||||
_>>=ˡ_ : ∀ {P R S T} → <:-Close P (S ⇒ T) → (R <: S) → <:-Close P (R ⇒ T)
|
||||
(defn p p₁ p₂) >>=ˡ q = defn p (<:-trans q p₁) p₂
|
||||
|
||||
_>>=ʳ_ : ∀ {P S T U} → <:-Close P (S ⇒ T) → (T <: U) → <:-Close P (S ⇒ U)
|
||||
(defn p p₁ p₂) >>=ʳ q = defn p p₁ (<:-trans p₂ q)
|
||||
|
||||
-- Properties of ⊂:
|
||||
⊂:-refl : ∀ {P} → P ⊂: P
|
||||
⊂:-refl p = just p
|
||||
|
||||
_[∪]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∪-Lift P Q) ((R ∪ T) ⇒ (S ∪ U))
|
||||
(defn p p₁ p₂) [∪] (defn q q₁ q₂) = defn (union p q) (<:-union p₁ q₁) (<:-union p₂ q₂)
|
||||
|
||||
_[∩]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∩-Lift P Q) ((R ∩ T) ⇒ (S ∩ U))
|
||||
(defn p p₁ p₂) [∩] (defn q q₁ q₂) = defn (intersect p q) (<:-intersect p₁ q₁) (<:-intersect p₂ q₂)
|
||||
|
||||
⊂:-∩-saturate-inj : ∀ {P} → P ⊂: ∩-Saturate P
|
||||
⊂:-∩-saturate-inj p = defn (base p) <:-refl <:-refl
|
||||
|
||||
⊂:-∪-saturate-inj : ∀ {P} → P ⊂: ∪-Saturate P
|
||||
⊂:-∪-saturate-inj p = just (base p)
|
||||
|
||||
⊂:-∩-lift-saturate : ∀ {P} → ∩-Lift (∩-Saturate P) (∩-Saturate P) ⊂: ∩-Saturate P
|
||||
⊂:-∩-lift-saturate (intersect p q) = just (intersect p q)
|
||||
|
||||
⊂:-∪-lift-saturate : ∀ {P} → ∪-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P
|
||||
⊂:-∪-lift-saturate (union p q) = just (union p q)
|
||||
|
||||
⊂:-∩-lift : ∀ {P Q R S} → (P ⊂: Q) → (R ⊂: S) → (∩-Lift P R ⊂: ∩-Lift Q S)
|
||||
⊂:-∩-lift P⊂Q R⊂S (intersect n o) = P⊂Q n [∩] R⊂S o
|
||||
|
||||
⊂:-∪-lift : ∀ {P Q R S} → (P ⊂: Q) → (R ⊂: S) → (∪-Lift P R ⊂: ∪-Lift Q S)
|
||||
⊂:-∪-lift P⊂Q R⊂S (union n o) = P⊂Q n [∪] R⊂S o
|
||||
|
||||
⊂:-∩-saturate : ∀ {P Q} → (P ⊂: Q) → (∩-Saturate P ⊂: ∩-Saturate Q)
|
||||
⊂:-∩-saturate P⊂Q (base p) = P⊂Q p >>= ⊂:-∩-saturate-inj
|
||||
⊂:-∩-saturate P⊂Q (intersect p q) = (⊂:-∩-saturate P⊂Q p [∩] ⊂:-∩-saturate P⊂Q q) >>= ⊂:-∩-lift-saturate
|
||||
|
||||
⊂:-∪-saturate : ∀ {P Q} → (P ⊂: Q) → (∪-Saturate P ⊂: ∪-Saturate Q)
|
||||
⊂:-∪-saturate P⊂Q (base p) = P⊂Q p >>= ⊂:-∪-saturate-inj
|
||||
⊂:-∪-saturate P⊂Q (union p q) = (⊂:-∪-saturate P⊂Q p [∪] ⊂:-∪-saturate P⊂Q q) >>= ⊂:-∪-lift-saturate
|
||||
|
||||
⊂:-∩-saturate-indn : ∀ {P Q} → (P ⊂: Q) → (∩-Lift Q Q ⊂: Q) → (∩-Saturate P ⊂: Q)
|
||||
⊂:-∩-saturate-indn P⊂Q QQ⊂Q (base p) = P⊂Q p
|
||||
⊂:-∩-saturate-indn P⊂Q QQ⊂Q (intersect p q) = (⊂:-∩-saturate-indn P⊂Q QQ⊂Q p [∩] ⊂:-∩-saturate-indn P⊂Q QQ⊂Q q) >>= QQ⊂Q
|
||||
|
||||
⊂:-∪-saturate-indn : ∀ {P Q} → (P ⊂: Q) → (∪-Lift Q Q ⊂: Q) → (∪-Saturate P ⊂: Q)
|
||||
⊂:-∪-saturate-indn P⊂Q QQ⊂Q (base p) = P⊂Q p
|
||||
⊂:-∪-saturate-indn P⊂Q QQ⊂Q (union p q) = (⊂:-∪-saturate-indn P⊂Q QQ⊂Q p [∪] ⊂:-∪-saturate-indn P⊂Q QQ⊂Q q) >>= QQ⊂Q
|
||||
|
||||
∪-saturate-resp-∩-saturation : ∀ {P} → (∩-Lift P P ⊂: P) → (∩-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P)
|
||||
∪-saturate-resp-∩-saturation ∩P⊂P (intersect (base p) (base q)) = ∩P⊂P (intersect p q) >>= ⊂:-∪-saturate-inj
|
||||
∪-saturate-resp-∩-saturation ∩P⊂P (intersect p (union q q₁)) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q₁)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distl-∪ >>=ʳ ∩-distl-∪-<:
|
||||
∪-saturate-resp-∩-saturation ∩P⊂P (intersect (union p p₁) q) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p₁ q)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distr-∪ >>=ʳ ∩-distr-∪-<:
|
||||
|
||||
ov-language : ∀ {F t} → FunType F → (∀ {S T} → Overloads F (S ⇒ T) → Language (S ⇒ T) t) → Language F t
|
||||
ov-language (S ⇒ T) p = p here
|
||||
ov-language (F ∩ G) p = (ov-language F (p ∘ left) , ov-language G (p ∘ right))
|
||||
|
||||
ov-<: : ∀ {F R S T U} → FunType F → Overloads F (R ⇒ S) → ((R ⇒ S) <: (T ⇒ U)) → F <: (T ⇒ U)
|
||||
ov-<: F here p = p
|
||||
ov-<: (F ∩ G) (left o) p = <:-trans <:-∩-left (ov-<: F o p)
|
||||
ov-<: (F ∩ G) (right o) p = <:-trans <:-∩-right (ov-<: G o p)
|
||||
|
||||
<:ᵒ-impl-<: : ∀ {F G} → FunType F → FunType G → (F <:ᵒ G) → (F <: G)
|
||||
<:ᵒ-impl-<: F (T ⇒ U) F<G with F<G here
|
||||
<:ᵒ-impl-<: F (T ⇒ U) F<G | defn o o₁ o₂ = ov-<: F o (<:-function o₁ o₂)
|
||||
<:ᵒ-impl-<: F (G ∩ H) F<G = <:-∩-glb (<:ᵒ-impl-<: F G (F<G ∘ left)) (<:ᵒ-impl-<: F H (F<G ∘ right))
|
||||
|
||||
⊂:-overloads-left : ∀ {F G} → Overloads F ⊂: Overloads (F ∩ G)
|
||||
⊂:-overloads-left p = just (left p)
|
||||
|
||||
⊂:-overloads-right : ∀ {F G} → Overloads G ⊂: Overloads (F ∩ G)
|
||||
⊂:-overloads-right p = just (right p)
|
||||
|
||||
⊂:-overloads-⋒ : ∀ {F G} → FunType F → FunType G → ∩-Lift (Overloads F) (Overloads G) ⊂: Overloads (F ⋒ G)
|
||||
⊂:-overloads-⋒ (R ⇒ S) (T ⇒ U) (intersect here here) = defn here (∩-<:-∩ⁿ R T) (∩ⁿ-<:-∩ S U)
|
||||
⊂:-overloads-⋒ (R ⇒ S) (G ∩ H) (intersect here (left o)) = ⊂:-overloads-⋒ (R ⇒ S) G (intersect here o) >>= ⊂:-overloads-left
|
||||
⊂:-overloads-⋒ (R ⇒ S) (G ∩ H) (intersect here (right o)) = ⊂:-overloads-⋒ (R ⇒ S) H (intersect here o) >>= ⊂:-overloads-right
|
||||
⊂:-overloads-⋒ (E ∩ F) G (intersect (left n) o) = ⊂:-overloads-⋒ E G (intersect n o) >>= ⊂:-overloads-left
|
||||
⊂:-overloads-⋒ (E ∩ F) G (intersect (right n) o) = ⊂:-overloads-⋒ F G (intersect n o) >>= ⊂:-overloads-right
|
||||
|
||||
⊂:-⋒-overloads : ∀ {F G} → FunType F → FunType G → Overloads (F ⋒ G) ⊂: ∩-Lift (Overloads F) (Overloads G)
|
||||
⊂:-⋒-overloads (R ⇒ S) (T ⇒ U) here = defn (intersect here here) (∩ⁿ-<:-∩ R T) (∩-<:-∩ⁿ S U)
|
||||
⊂:-⋒-overloads (R ⇒ S) (G ∩ H) (left o) = ⊂:-⋒-overloads (R ⇒ S) G o >>= ⊂:-∩-lift ⊂:-refl ⊂:-overloads-left
|
||||
⊂:-⋒-overloads (R ⇒ S) (G ∩ H) (right o) = ⊂:-⋒-overloads (R ⇒ S) H o >>= ⊂:-∩-lift ⊂:-refl ⊂:-overloads-right
|
||||
⊂:-⋒-overloads (E ∩ F) G (left o) = ⊂:-⋒-overloads E G o >>= ⊂:-∩-lift ⊂:-overloads-left ⊂:-refl
|
||||
⊂:-⋒-overloads (E ∩ F) G (right o) = ⊂:-⋒-overloads F G o >>= ⊂:-∩-lift ⊂:-overloads-right ⊂:-refl
|
||||
|
||||
⊂:-overloads-⋓ : ∀ {F G} → FunType F → FunType G → ∪-Lift (Overloads F) (Overloads G) ⊂: Overloads (F ⋓ G)
|
||||
⊂:-overloads-⋓ (R ⇒ S) (T ⇒ U) (union here here) = defn here (∪-<:-∪ⁿ R T) (∪ⁿ-<:-∪ S U)
|
||||
⊂:-overloads-⋓ (R ⇒ S) (G ∩ H) (union here (left o)) = ⊂:-overloads-⋓ (R ⇒ S) G (union here o) >>= ⊂:-overloads-left
|
||||
⊂:-overloads-⋓ (R ⇒ S) (G ∩ H) (union here (right o)) = ⊂:-overloads-⋓ (R ⇒ S) H (union here o) >>= ⊂:-overloads-right
|
||||
⊂:-overloads-⋓ (E ∩ F) G (union (left n) o) = ⊂:-overloads-⋓ E G (union n o) >>= ⊂:-overloads-left
|
||||
⊂:-overloads-⋓ (E ∩ F) G (union (right n) o) = ⊂:-overloads-⋓ F G (union n o) >>= ⊂:-overloads-right
|
||||
|
||||
⊂:-⋓-overloads : ∀ {F G} → FunType F → FunType G → Overloads (F ⋓ G) ⊂: ∪-Lift (Overloads F) (Overloads G)
|
||||
⊂:-⋓-overloads (R ⇒ S) (T ⇒ U) here = defn (union here here) (∪ⁿ-<:-∪ R T) (∪-<:-∪ⁿ S U)
|
||||
⊂:-⋓-overloads (R ⇒ S) (G ∩ H) (left o) = ⊂:-⋓-overloads (R ⇒ S) G o >>= ⊂:-∪-lift ⊂:-refl ⊂:-overloads-left
|
||||
⊂:-⋓-overloads (R ⇒ S) (G ∩ H) (right o) = ⊂:-⋓-overloads (R ⇒ S) H o >>= ⊂:-∪-lift ⊂:-refl ⊂:-overloads-right
|
||||
⊂:-⋓-overloads (E ∩ F) G (left o) = ⊂:-⋓-overloads E G o >>= ⊂:-∪-lift ⊂:-overloads-left ⊂:-refl
|
||||
⊂:-⋓-overloads (E ∩ F) G (right o) = ⊂:-⋓-overloads F G o >>= ⊂:-∪-lift ⊂:-overloads-right ⊂:-refl
|
||||
|
||||
∪-saturate-overloads : ∀ {F} → FunType F → Overloads (∪-saturate F) ⊂: ∪-Saturate (Overloads F)
|
||||
∪-saturate-overloads (S ⇒ T) here = just (base here)
|
||||
∪-saturate-overloads (F ∩ G) (left (left o)) = ∪-saturate-overloads F o >>= ⊂:-∪-saturate ⊂:-overloads-left
|
||||
∪-saturate-overloads (F ∩ G) (left (right o)) = ∪-saturate-overloads G o >>= ⊂:-∪-saturate ⊂:-overloads-right
|
||||
∪-saturate-overloads (F ∩ G) (right o) =
|
||||
⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) o >>=
|
||||
⊂:-∪-lift (∪-saturate-overloads F) (∪-saturate-overloads G) >>=
|
||||
⊂:-∪-lift (⊂:-∪-saturate ⊂:-overloads-left) (⊂:-∪-saturate ⊂:-overloads-right) >>=
|
||||
⊂:-∪-lift-saturate
|
||||
|
||||
overloads-∪-saturate : ∀ {F} → FunType F → ∪-Saturate (Overloads F) ⊂: Overloads (∪-saturate F)
|
||||
overloads-∪-saturate F = ⊂:-∪-saturate-indn (inj F) (step F) where
|
||||
|
||||
inj : ∀ {F} → FunType F → Overloads F ⊂: Overloads (∪-saturate F)
|
||||
inj (S ⇒ T) here = just here
|
||||
inj (F ∩ G) (left p) = inj F p >>= ⊂:-overloads-left >>= ⊂:-overloads-left
|
||||
inj (F ∩ G) (right p) = inj G p >>= ⊂:-overloads-right >>= ⊂:-overloads-left
|
||||
|
||||
step : ∀ {F} → FunType F → ∪-Lift (Overloads (∪-saturate F)) (Overloads (∪-saturate F)) ⊂: Overloads (∪-saturate F)
|
||||
step (S ⇒ T) (union here here) = defn here (<:-∪-lub <:-refl <:-refl) <:-∪-left
|
||||
step (F ∩ G) (union (left (left p)) (left (left q))) = step F (union p q) >>= ⊂:-overloads-left >>= ⊂:-overloads-left
|
||||
step (F ∩ G) (union (left (left p)) (left (right q))) = ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) (union p q) >>= ⊂:-overloads-right
|
||||
step (F ∩ G) (union (left (right p)) (left (left q))) = ⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) (union q p) >>= ⊂:-overloads-right >>=ˡ <:-∪-symm >>=ʳ <:-∪-symm
|
||||
step (F ∩ G) (union (left (right p)) (left (right q))) = step G (union p q) >>= ⊂:-overloads-right >>= ⊂:-overloads-left
|
||||
step (F ∩ G) (union p (right q)) with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) q
|
||||
step (F ∩ G) (union (left (left p)) (right q)) | defn (union q₁ q₂) q₃ q₄ =
|
||||
(step F (union p q₁) [∪] just q₂) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union <:-refl q₃) <:-∪-assocl >>=ʳ
|
||||
<:-trans <:-∪-assocr (<:-union <:-refl q₄)
|
||||
step (F ∩ G) (union (left (right p)) (right q)) | defn (union q₁ q₂) q₃ q₄ =
|
||||
(just q₁ [∪] step G (union p q₂)) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union <:-refl q₃) (<:-∪-lub (<:-trans <:-∪-left <:-∪-right) (<:-∪-lub <:-∪-left (<:-trans <:-∪-right <:-∪-right))) >>=ʳ
|
||||
<:-trans (<:-∪-lub (<:-trans <:-∪-left <:-∪-right) (<:-∪-lub <:-∪-left (<:-trans <:-∪-right <:-∪-right))) (<:-union <:-refl q₄)
|
||||
step (F ∩ G) (union (right p) (right q)) | defn (union q₁ q₂) q₃ q₄ with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) p
|
||||
step (F ∩ G) (union (right p) (right q)) | defn (union q₁ q₂) q₃ q₄ | defn (union p₁ p₂) p₃ p₄ =
|
||||
(step F (union p₁ q₁) [∪] step G (union p₂ q₂)) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union p₃ q₃) (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) >>=ʳ
|
||||
<:-trans (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) (<:-union p₄ q₄)
|
||||
step (F ∩ G) (union (right p) q) with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) p
|
||||
step (F ∩ G) (union (right p) (left (left q))) | defn (union p₁ p₂) p₃ p₄ =
|
||||
(step F (union p₁ q) [∪] just p₂) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union p₃ <:-refl) (<:-∪-lub (<:-union <:-∪-left <:-refl) (<:-trans <:-∪-right <:-∪-left)) >>=ʳ
|
||||
<:-trans (<:-∪-lub (<:-union <:-∪-left <:-refl) (<:-trans <:-∪-right <:-∪-left)) (<:-union p₄ <:-refl)
|
||||
step (F ∩ G) (union (right p) (left (right q))) | defn (union p₁ p₂) p₃ p₄ =
|
||||
(just p₁ [∪] step G (union p₂ q)) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union p₃ <:-refl) <:-∪-assocr >>=ʳ
|
||||
<:-trans <:-∪-assocl (<:-union p₄ <:-refl)
|
||||
step (F ∩ G) (union (right p) (right q)) | defn (union p₁ p₂) p₃ p₄ with ⊂:-⋓-overloads (normal-∪-saturate F) (normal-∪-saturate G) q
|
||||
step (F ∩ G) (union (right p) (right q)) | defn (union p₁ p₂) p₃ p₄ | defn (union q₁ q₂) q₃ q₄ =
|
||||
(step F (union p₁ q₁) [∪] step G (union p₂ q₂)) >>=
|
||||
⊂:-overloads-⋓ (normal-∪-saturate F) (normal-∪-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-union p₃ q₃) (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) >>=ʳ
|
||||
<:-trans (<:-∪-lub (<:-union <:-∪-left <:-∪-left) (<:-union <:-∪-right <:-∪-right)) (<:-union p₄ q₄)
|
||||
|
||||
∪-saturated : ∀ {F} → FunType F → ∪-Lift (Overloads (∪-saturate F)) (Overloads (∪-saturate F)) ⊂: Overloads (∪-saturate F)
|
||||
∪-saturated F o =
|
||||
⊂:-∪-lift (∪-saturate-overloads F) (∪-saturate-overloads F) o >>=
|
||||
⊂:-∪-lift-saturate >>=
|
||||
overloads-∪-saturate F
|
||||
|
||||
∩-saturate-overloads : ∀ {F} → FunType F → Overloads (∩-saturate F) ⊂: ∩-Saturate (Overloads F)
|
||||
∩-saturate-overloads (S ⇒ T) here = just (base here)
|
||||
∩-saturate-overloads (F ∩ G) (left (left o)) = ∩-saturate-overloads F o >>= ⊂:-∩-saturate ⊂:-overloads-left
|
||||
∩-saturate-overloads (F ∩ G) (left (right o)) = ∩-saturate-overloads G o >>= ⊂:-∩-saturate ⊂:-overloads-right
|
||||
∩-saturate-overloads (F ∩ G) (right o) =
|
||||
⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) o >>=
|
||||
⊂:-∩-lift (∩-saturate-overloads F) (∩-saturate-overloads G) >>=
|
||||
⊂:-∩-lift (⊂:-∩-saturate ⊂:-overloads-left) (⊂:-∩-saturate ⊂:-overloads-right) >>=
|
||||
⊂:-∩-lift-saturate
|
||||
|
||||
overloads-∩-saturate : ∀ {F} → FunType F → ∩-Saturate (Overloads F) ⊂: Overloads (∩-saturate F)
|
||||
overloads-∩-saturate F = ⊂:-∩-saturate-indn (inj F) (step F) where
|
||||
|
||||
inj : ∀ {F} → FunType F → Overloads F ⊂: Overloads (∩-saturate F)
|
||||
inj (S ⇒ T) here = just here
|
||||
inj (F ∩ G) (left p) = inj F p >>= ⊂:-overloads-left >>= ⊂:-overloads-left
|
||||
inj (F ∩ G) (right p) = inj G p >>= ⊂:-overloads-right >>= ⊂:-overloads-left
|
||||
|
||||
step : ∀ {F} → FunType F → ∩-Lift (Overloads (∩-saturate F)) (Overloads (∩-saturate F)) ⊂: Overloads (∩-saturate F)
|
||||
step (S ⇒ T) (intersect here here) = defn here <:-∩-left (<:-∩-glb <:-refl <:-refl)
|
||||
step (F ∩ G) (intersect (left (left p)) (left (left q))) = step F (intersect p q) >>= ⊂:-overloads-left >>= ⊂:-overloads-left
|
||||
step (F ∩ G) (intersect (left (left p)) (left (right q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect p q) >>= ⊂:-overloads-right
|
||||
step (F ∩ G) (intersect (left (right p)) (left (left q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect q p) >>= ⊂:-overloads-right >>=ˡ <:-∩-symm >>=ʳ <:-∩-symm
|
||||
step (F ∩ G) (intersect (left (right p)) (left (right q))) = step G (intersect p q) >>= ⊂:-overloads-right >>= ⊂:-overloads-left
|
||||
step (F ∩ G) (intersect (right p) q) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
|
||||
step (F ∩ G) (intersect (right p) (left (left q))) | defn (intersect p₁ p₂) p₃ p₄ =
|
||||
(step F (intersect p₁ q) [∩] just p₂) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect p₃ <:-refl) (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) >>=ʳ
|
||||
<:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) (<:-intersect p₄ <:-refl)
|
||||
step (F ∩ G) (intersect (right p) (left (right q))) | defn (intersect p₁ p₂) p₃ p₄ =
|
||||
(just p₁ [∩] step G (intersect p₂ q)) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect p₃ <:-refl) <:-∩-assocr >>=ʳ
|
||||
<:-trans <:-∩-assocl (<:-intersect p₄ <:-refl)
|
||||
step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
|
||||
step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ | defn (intersect q₁ q₂) q₃ q₄ =
|
||||
(step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
|
||||
<:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)
|
||||
step (F ∩ G) (intersect p (right q)) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
|
||||
step (F ∩ G) (intersect (left (left p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
|
||||
(step F (intersect p q₁) [∩] just q₂) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect <:-refl q₃) <:-∩-assocl >>=ʳ
|
||||
<:-trans <:-∩-assocr (<:-intersect <:-refl q₄)
|
||||
step (F ∩ G) (intersect (left (right p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
|
||||
(just q₁ [∩] step G (intersect p q₂) ) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect <:-refl q₃) (<:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right))) >>=ʳ
|
||||
<:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-trans (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right)) q₄)
|
||||
step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
|
||||
step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ | defn (intersect p₁ p₂) p₃ p₄ =
|
||||
(step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
|
||||
⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
|
||||
⊂:-overloads-right >>=ˡ
|
||||
<:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
|
||||
<:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)
|
||||
|
||||
saturate-overloads : ∀ {F} → FunType F → Overloads (saturate F) ⊂: ∪-Saturate (∩-Saturate (Overloads F))
|
||||
saturate-overloads F o = ∪-saturate-overloads (normal-∩-saturate F) o >>= (⊂:-∪-saturate (∩-saturate-overloads F))
|
||||
|
||||
overloads-saturate : ∀ {F} → FunType F → ∪-Saturate (∩-Saturate (Overloads F)) ⊂: Overloads (saturate F)
|
||||
overloads-saturate F o = ⊂:-∪-saturate (overloads-∩-saturate F) o >>= overloads-∪-saturate (normal-∩-saturate F)
|
||||
|
||||
-- Saturated F whenever
|
||||
-- * if F has overloads (R ⇒ S) and (T ⇒ U) then F has an overload which is a subtype of ((R ∩ T) ⇒ (S ∩ U))
|
||||
-- * ditto union
|
||||
data Saturated (F : Type) : Set where
|
||||
|
||||
defn :
|
||||
|
||||
(∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → <:-Close (Overloads F) ((R ∩ T) ⇒ (S ∩ U))) →
|
||||
(∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → <:-Close (Overloads F) ((R ∪ T) ⇒ (S ∪ U))) →
|
||||
-----------
|
||||
Saturated F
|
||||
|
||||
-- saturated F is saturated!
|
||||
saturated : ∀ {F} → FunType F → Saturated (saturate F)
|
||||
saturated F = defn
|
||||
(λ n o → (saturate-overloads F n [∩] saturate-overloads F o) >>= ∪-saturate-resp-∩-saturation ⊂:-∩-lift-saturate >>= overloads-saturate F)
|
||||
(λ n o → ∪-saturated (normal-∩-saturate F) (union n o))
|
||||
Loading…
Reference in a new issue