From 7721955ba54295696064a05a969b2a4fb29f43af Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Wed, 23 Mar 2022 15:02:57 -0500 Subject: [PATCH] Prototyping: add semantic subtyping (#424) Adds subtyping to strict mode. --- prototyping/FFI/Data/Aeson.agda | 4 +- prototyping/FFI/Data/Either.agda | 24 +- prototyping/Luau/RuntimeError.agda | 2 +- prototyping/Luau/StrictMode.agda | 34 +- prototyping/Luau/StrictMode/ToString.agda | 39 +- prototyping/Luau/Subtyping.agda | 62 ++ prototyping/Luau/Type.agda | 7 + prototyping/Luau/TypeCheck.agda | 23 +- prototyping/Properties.agda | 2 + prototyping/Properties/Functions.agda | 6 + prototyping/Properties/StrictMode.agda | 594 +++++++----------- prototyping/Properties/Subtyping.agda | 221 +++++++ prototyping/Properties/TypeCheck.agda | 18 +- .../concat_number_and_string/out.txt | 1 + 14 files changed, 623 insertions(+), 414 deletions(-) create mode 100644 prototyping/Luau/Subtyping.agda create mode 100644 prototyping/Properties/Functions.agda create mode 100644 prototyping/Properties/Subtyping.agda diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index 0cd2723..4301471 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -10,7 +10,7 @@ open import Agda.Builtin.String using (String) open import FFI.Data.ByteString using (ByteString) open import FFI.Data.HaskellString using (HaskellString; pack) open import FFI.Data.Maybe using (Maybe; just; nothing) -open import FFI.Data.Either using (Either; mapLeft) +open import FFI.Data.Either using (Either; mapL) open import FFI.Data.Scientific using (Scientific) open import FFI.Data.Vector using (Vector) @@ -73,5 +73,5 @@ postulate {-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-} eitherDecode : ByteString → Either String Value -eitherDecode bytes = mapLeft pack (eitherHDecode bytes) +eitherDecode bytes = mapL pack (eitherHDecode bytes) diff --git a/prototyping/FFI/Data/Either.agda b/prototyping/FFI/Data/Either.agda index d024c69..8a5d3e6 100644 --- a/prototyping/FFI/Data/Either.agda +++ b/prototyping/FFI/Data/Either.agda @@ -7,10 +7,22 @@ data Either (A B : Set) : Set where Right : B → Either A B {-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-} -mapLeft : ∀ {A B C} → (A → B) → (Either A C) → (Either B C) -mapLeft f (Left x) = Left (f x) -mapLeft f (Right x) = Right x +swapLR : ∀ {A B} → Either A B → Either B A +swapLR (Left x) = Right x +swapLR (Right x) = Left x -mapRight : ∀ {A B C} → (B → C) → (Either A B) → (Either A C) -mapRight f (Left x) = Left x -mapRight f (Right x) = Right (f x) +mapL : ∀ {A B C} → (A → B) → Either A C → Either B C +mapL f (Left x) = Left (f x) +mapL f (Right x) = Right x + +mapR : ∀ {A B C} → (B → C) → Either A B → Either A C +mapR f (Left x) = Left x +mapR f (Right x) = Right (f x) + +mapLR : ∀ {A B C D} → (A → B) → (C → D) → Either A C → Either B D +mapLR f g (Left x) = Left (f x) +mapLR f g (Right x) = Right (g x) + +cond : ∀ {A B C : Set} → (A → C) → (B → C) → (Either A B) → C +cond f g (Left x) = f x +cond f g (Right x) = g x diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index 0c8a594..b9b305c 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -25,7 +25,7 @@ data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w) + FunctionMismatch : ∀ v w → (valueType v ≢ function) → RuntimeErrorᴱ H (val v $ val w) BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w)) BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w)) UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x) diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 08e0f50..0b5fe0d 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -5,28 +5,18 @@ module Luau.StrictMode where open import Agda.Builtin.Equality using (_≡_) open import FFI.Data.Maybe using (just; nothing) open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··) -open import Luau.Type using (Type; strict; nil; number; string; _⇒_; tgt) +open import Luau.Type using (Type; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Luau.Subtyping using (_≮:_) open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function) -open import Properties.Equality using (_≢_) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function; srcBinOp) +open import Properties.Contradiction using (¬) open import Properties.TypeCheck(strict) using (typeCheckᴮ) open import Properties.Product using (_,_) src : Type → Type src = Luau.Type.src strict -data BinOpWarning : BinaryOperator → Type → Set where - + : ∀ {T} → (T ≢ number) → BinOpWarning + T - - : ∀ {T} → (T ≢ number) → BinOpWarning - T - * : ∀ {T} → (T ≢ number) → BinOpWarning * T - / : ∀ {T} → (T ≢ number) → BinOpWarning / T - < : ∀ {T} → (T ≢ number) → BinOpWarning < T - > : ∀ {T} → (T ≢ number) → BinOpWarning > T - <= : ∀ {T} → (T ≢ number) → BinOpWarning <= T - >= : ∀ {T} → (T ≢ number) → BinOpWarning >= T - ·· : ∀ {T} → (T ≢ string) → BinOpWarning ·· T - data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set @@ -46,7 +36,7 @@ data Warningᴱ H {Γ} where FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → - (src T ≢ U) → + (U ≮: src T) → ----------------- Warningᴱ H (app D₁ D₂) @@ -64,13 +54,13 @@ data Warningᴱ H {Γ} where BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → - BinOpWarning op T → + (T ≮: srcBinOp op) → ------------------------------ Warningᴱ H (binexp {op} D₁ D₂) BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → - BinOpWarning op U → + (U ≮: srcBinOp op) → ------------------------------ Warningᴱ H (binexp {op} D₁ D₂) @@ -88,7 +78,7 @@ data Warningᴱ H {Γ} where FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → - (U ≢ V) → + (V ≮: U) → ------------------------- Warningᴱ H (function {f} {U = U} D) @@ -100,7 +90,7 @@ data Warningᴱ H {Γ} where BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} → - (T ≢ U) → + (U ≮: T) → ------------------------------ Warningᴱ H (block {b} {T = T} D) @@ -120,7 +110,7 @@ data Warningᴮ H {Γ} where LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → - (T ≢ U) → + (U ≮: T) → -------------------- Warningᴮ H (local D₁ D₂) @@ -138,7 +128,7 @@ data Warningᴮ H {Γ} where FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → - (U ≢ V) → + (V ≮: U) → ------------------------------------- Warningᴮ H (function D₁ D₂) @@ -158,7 +148,7 @@ data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} → - (U ≢ V) → + (V ≮: U) → --------------------------------- Warningᴼ H (function {f} {U = U} D) diff --git a/prototyping/Luau/StrictMode/ToString.agda b/prototyping/Luau/StrictMode/ToString.agda index ca55888..08ee13b 100644 --- a/prototyping/Luau/StrictMode/ToString.agda +++ b/prototyping/Luau/StrictMode/ToString.agda @@ -2,37 +2,58 @@ 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.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 (strict) +open import Luau.Type using (strict; number; boolean; string; nil) open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_) open import Luau.Addr.ToString using (addrToString) open import Luau.Var.ToString using (varToString) open import Luau.Type.ToString using (typeToString) open import Luau.Syntax.ToString using (binOpToString) +tmp : Nat → String +tmp 0 = "w" +tmp 1 = "x" +tmp 2 = "y" +tmp 3 = "z" +tmp (suc (suc (suc n))) = tmp n ++ "'" + +treeToString : Tree → Nat → String → String +treeToString (scalar number) n v = v ++ " is a number" +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-err t) n v = v ++ "(" ++ w ++ ") can error when\n " ++ treeToString t (suc n) w where w = tmp n + +subtypeWarningToString : ∀ {T U} → (T ≮: U) → String +subtypeWarningToString (witness t p q) = "\n because provided type contains v, where " ++ treeToString t 0 "v" + warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x -warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a -warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U +warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated address " ++ addrToString a +warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U ++ subtypeWarningToString p warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W -warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V +warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n in function expression " ++ varToString f -warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) = "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U +warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) = "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U ++ subtypeWarningToString p warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n in block " ++ varToString b -warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T -warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U +warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T ++ subtypeWarningToString p +warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U ++ subtypeWarningToString p warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W -warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V +warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n in function declaration " ++ varToString f warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W -warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) = "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U +warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) = "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U ++ subtypeWarningToString p warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n in local variable declaration " ++ varToString x warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n in return statement" diff --git a/prototyping/Luau/Subtyping.agda b/prototyping/Luau/Subtyping.agda new file mode 100644 index 0000000..7d67eb4 --- /dev/null +++ b/prototyping/Luau/Subtyping.agda @@ -0,0 +1,62 @@ +{-# OPTIONS --rewriting #-} + +open import Luau.Type using (Type; Scalar; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_) +open import Properties.Equality using (_≢_) + +module Luau.Subtyping where + +-- An implementation of semantic subtyping + +-- We think of types as languages of trees + +data Tree : Set where + + scalar : ∀ {T} → Scalar T → Tree + function : Tree + function-ok : Tree → Tree + function-err : Tree → Tree + +data Language : Type → Tree → Set +data ¬Language : Type → Tree → Set + +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-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t) + scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t) + left : ∀ {T U t} → Language T t → Language (T ∪ U) t + right : ∀ {T U u} → Language U u → Language (T ∪ U) u + _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t + any : ∀ {t} → Language any t + +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) + function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s) + function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u) + function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t) + _,_ : ∀ {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 + none : ∀ {t} → ¬Language none t + +-- Subtyping as language inclusion + +_<:_ : Type → Type → Set +(T <: U) = ∀ t → (Language T t) → (Language U t) + +-- For warnings, we are interested in failures of subtyping, +-- which is whrn there is a tree in T's language that isn't in U's. + +data _≮:_ (T U : Type) : Set where + + witness : ∀ t → + + Language T t → + ¬Language U t → + ----------------- + T ≮: U diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index c5b7614..87815dd 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -17,6 +17,13 @@ data Type : Set where _∪_ : Type → Type → Type _∩_ : Type → Type → Type +data Scalar : Type → Set where + + number : Scalar number + boolean : Scalar boolean + string : Scalar string + nil : Scalar nil + lhs : Type → Type lhs (T ⇒ _) = T lhs (T ∪ _) = T diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index 65ed183..c22618b 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -10,7 +10,7 @@ open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr open import Luau.Var using (Var) open import Luau.Addr using (Addr) open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ) -open import Luau.Type using (Type; Mode; nil; none; number; boolean; string; _⇒_; tgt) +open import Luau.Type using (Type; Mode; nil; any; number; boolean; string; _⇒_; tgt) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import FFI.Data.Vector using (Vector) open import FFI.Data.Maybe using (Maybe; just; nothing) @@ -19,9 +19,22 @@ open import Properties.Product using (_×_; _,_) src : Type → Type src = Luau.Type.src m -orNone : Maybe Type → Type -orNone nothing = none -orNone (just T) = T +orAny : Maybe Type → Type +orAny nothing = any +orAny (just T) = T + +srcBinOp : BinaryOperator → Type +srcBinOp + = number +srcBinOp - = number +srcBinOp * = number +srcBinOp / = number +srcBinOp < = number +srcBinOp > = number +srcBinOp == = any +srcBinOp ~= = any +srcBinOp <= = number +srcBinOp >= = number +srcBinOp ·· = string tgtBinOp : BinaryOperator → Type tgtBinOp + = number @@ -76,7 +89,7 @@ data _⊢ᴱ_∈_ where var : ∀ {x T Γ} → - T ≡ orNone(Γ [ x ]ⱽ) → + T ≡ orAny(Γ [ x ]ⱽ) → ---------------- Γ ⊢ᴱ (var x) ∈ T diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 8b30ce1..5594812 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -5,7 +5,9 @@ module Properties where import Properties.Contradiction import Properties.Dec import Properties.Equality +import Properties.Functions import Properties.Remember import Properties.Step import Properties.StrictMode +import Properties.Subtyping import Properties.TypeCheck diff --git a/prototyping/Properties/Functions.agda b/prototyping/Properties/Functions.agda new file mode 100644 index 0000000..313b0ff --- /dev/null +++ b/prototyping/Properties/Functions.agda @@ -0,0 +1,6 @@ +module Properties.Functions where + +infixr 5 _∘_ + +_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) +(f ∘ g) x = f (g x) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 77852f1..2ff2b15 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -4,13 +4,15 @@ module Properties.StrictMode where import Agda.Builtin.Equality.Rewrite 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.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=; ··) +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; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language) open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=) -open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp) +open import Luau.Type using (Type; strict; nil; number; boolean; string; _⇒_; none; any; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orAny; srcBinOp; tgtBinOp) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) @@ -18,17 +20,19 @@ open import Luau.VarCtxt using (VarCtxt; ∅) open import Properties.Remember using (remember; _,_) 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.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber; mustBeString) +open import Properties.Contradiction using (CONTRADICTION; ¬) +open import Properties.Functions using (_∘_) +open import Properties.Subtyping using (any-≮:; ≡-trans-≮:; ≮:-trans-≡; none-tgt-≮:; tgt-none-≮:; src-any-≮:; any-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-none; any-≮:-scalar; scalar-≮:-none; any-≮:-none) +open import Properties.TypeCheck(strict) 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; +; -; *; /; <; >; <=; >=; ··) -open import Luau.RuntimeType using (valueType) +open import Luau.RuntimeType using (RuntimeType; valueType; number; string; boolean; nil; function) src = Luau.Type.src strict data _⊑_ (H : Heap yes) : Heap yes → Set where refl : (H ⊑ H) - snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′) + snoc : ∀ {H′ a O} → (H′ ≡ᴴ H ⊕ a ↦ O) → (H ⊑ H′) rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′) rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′) @@ -59,90 +63,51 @@ 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 -data OrWarningᴱ {Γ M T} (H : Heap yes) (D : Γ ⊢ᴱ M ∈ T) A : Set where - ok : A → OrWarningᴱ H D A - warning : Warningᴱ H D → OrWarningᴱ H D A +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 = any-≮: p +heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orAny (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 = none-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-none-≮: 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 -data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B ∈ T) A : Set where - ok : A → OrWarningᴮ H D A - warning : Warningᴮ H D → OrWarningᴮ H D A +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 -data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H ▷ M ∈ T) A : Set where - ok : A → OrWarningᴴᴱ H D A - warning : Warningᴴᴱ H D → OrWarningᴴᴱ H D A +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) -data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H ▷ B ∈ T) A : Set where - ok : A → OrWarningᴴᴮ H D A - warning : Warningᴴᴮ H D → OrWarningᴴᴮ H D A +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 none-tgt-≮: (substitutivityᴱ H M v x (tgt-none-≮: 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 orAny (sym (⊕-lookup-miss x y _ _ p))) q) -heap-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M) -heap-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B) - -heap-weakeningᴱ H (var x) h = ok refl -heap-weakeningᴱ H (val nil) h = ok refl -heap-weakeningᴱ H (val (addr a)) refl = ok refl -heap-weakeningᴱ H (val (addr a)) (snoc {a = b} defn) with a ≡ᴬ b -heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl) -heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q))) -heap-weakeningᴱ H (val (number n)) h = ok refl -heap-weakeningᴱ H (val (bool b)) h = ok refl -heap-weakeningᴱ H (val (string x)) h = ok refl -heap-weakeningᴱ H (binexp M op N) h = ok refl -heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h -heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p) -heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W) -heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl -heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl -heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h -heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p -heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W) -heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h -heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p -heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W) -heap-weakeningᴮ H (return M ∙ B) h with heap-weakeningᴱ H M h -heap-weakeningᴮ H (return M ∙ B) h | ok p = ok p -heap-weakeningᴮ H (return M ∙ B) h | warning W = warning (return W) -heap-weakeningᴮ H (done) h = ok refl - -none-not-obj : ∀ O → none ≢ typeOfᴼ O -none-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () - -typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (none ≢ typeOfᴱ H Γ (val v)) -typeOf-val-not-none nil = ok (λ ()) -typeOf-val-not-none (number n) = ok (λ ()) -typeOf-val-not-none (bool b) = ok (λ ()) -typeOf-val-not-none (string x) = ok (λ ()) -typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ) -typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p)))) -typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p) - -substitutivityᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ)) -substitutivityᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p))) -substitutivityᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p))) -substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) -substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p))) -substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p))) - -substitutivityᴱ H (var y) v x p with x ≡ⱽ y -substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p -substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q 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 = cong tgt (substitutivityᴱ H M 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-yes H v x x refl q = cong orNone q -substitutivityᴱ-whenever-no H v x y p q = cong orNone ( sym (⊕-lookup-miss x y _ _ p)) -substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f -substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q) -substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q) -substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y -substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q) -substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x y q p (⊕-swap 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 = refl -substitutivityᴮ-unless-yes H B v x x refl q refl = refl -substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q +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 binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x)) binOpPreservation H (+ m n) = refl @@ -157,306 +122,215 @@ binOpPreservation H (== v w) = refl binOpPreservation H (~= v w) = refl binOpPreservation H (·· v w) = refl -preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′) -preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′) +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)) -preservationᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = ok refl -preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s -preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p) -preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W)) -preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W) -preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s) -preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q) -preservationᴱ H (M $ N) (app₂ p s) | warning W = warning (expr (app₁ W)) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orNone (cong typeOfᴹᴼ p))) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r))) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s → r (trans (trans (sym (cong src (cong orNone (cong typeOfᴹᴼ p)))) s) (cong orNone q))))) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-none v -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (cong orNone q))) -preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W)) -preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl -preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) with T ≡ᵀ typeOfᴱ H ∅ (val v) -preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p -preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (BlockMismatch p)) -preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil -preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p -preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (BlockMismatch p)) -preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s) -preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl -preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl +reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR none-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-none-≮: p)) +reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (none-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-none-≮: 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 orAny (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 -preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s) -preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p -preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W)) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p)) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (cong orNone p))))) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-none v -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orNone p))) -preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W)) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H B (snoc defn) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl)) -preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W)) -preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s -preservationᴮ H (return M ∙ B) (return s) | ok p = ok p -preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W)) -preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W) +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) -reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M) -reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) -reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) -reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B) -reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) -reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +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)) +reflect-substitutionᴮ : ∀ {Γ T} H B v x → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Either (Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T)) +reflect-substitutionᴮ-unless : ∀ {Γ T U} H B v x y (r : Dec(x ≡ y)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r)) → Either (Warningᴮ H (typeCheckᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T)) +reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T)) +reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T)) -reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y -reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W -reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W -reflect-substitutionᴱ H (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r -reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p)))) -reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W) -reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r)))) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r)))) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) -reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) -reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r → q (trans r (substitutivityᴮ H B v x p))) -reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W) -reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₁ q) = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q) -reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q) -reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W) -reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W) +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) | Right W = Right (Right W) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-any-≮: q) +reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ any-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 (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 (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 (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-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r) -reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q) -reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | () +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 p (FunctionDefnMismatch q) with (x ≡ⱽ y) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r)))) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r)))) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W) -reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W) -reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r → q (trans r (substitutivityᴱ H M v x p))) -reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W) -reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y) -reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) -reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) -reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W) +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 (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) -reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W -reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W +reflect-substitutionᴮ-unless H B v x y (yes p) W = reflect-substitutionᴮ-unless-yes H B v x y p (⊕-over p) W +reflect-substitutionᴮ-unless H B v x y (no p) W = reflect-substitutionᴮ-unless-no H B v x y p (⊕-swap p) W +reflect-substitutionᴮ-unless-yes H B v x x refl refl W = Left W +reflect-substitutionᴮ-unless-no H B v x y p refl W = reflect-substitutionᴮ H B v x W -reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) -reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) +reflect-weakeningᴱ : ∀ Γ H M {H′} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) +reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) -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) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h -reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r → p (trans (cong src (sym q₁)) (trans r q₂))) -reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W -reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W -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) with heap-weakeningᴱ H M h -reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p) -reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W -reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h -reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p) -reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | warning W = bin₂ W -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) with heap-weakeningᴮ H B h -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W -reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W) -reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h -reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r → p (trans r q)) -reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | warning W = block₁ W -reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W) +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 (any-src-≮: p (heap-weakeningᴱ Γ H M h (src-any-≮: 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 (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 (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 (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) with heap-weakeningᴱ H M h -reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r → p (trans r q)) -reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | warning W = local₁ W -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ᴮ H B h W) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | warning W = function₁ W -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W) -reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (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 (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 (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) with heap-weakeningᴮ H B h -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W -reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′) +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′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) -reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) +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) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s) -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p (trans (trans (cong src (sym q)) r) q′))) -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W) -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W -reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W = expr (app₂ W) -reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′ -reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W -reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W) -reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′)) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p′ (trans (trans (cong src (sym q)) r) q′))) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | warning W | _ = expr (app₁ W) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (expr W) = expr (app₂ W) -reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (heap W) = heap W -reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′)) -reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′ -reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W -reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ H B v x (sym r)))))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t → s (trans (cong orNone (sym r)) (trans (sym t) (cong src (cong orNone (cong typeOfᴹᴼ p))))))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-none v -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (cong orNone (sym r))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (FunctionCallMismatch (λ s → r (trans (cong orNone (sym q)) (trans (sym s) (cong src (cong orNone (cong typeOfᴹᴼ p))))))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-none v -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (cong orNone (sym q))) -reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W) -reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) with preservationᴮ H B s -reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | ok q = expr (BlockMismatch (λ r → p (trans r q))) -reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W -reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W) -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′ -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W -reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W) -reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′)) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ any-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-any-≮: 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 (any-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-any-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ 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) | 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 orAny (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 orAny (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) (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) with preservationᴱ H M s -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)) -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W) -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s) -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p))) -reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W) -reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M s W′ -reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | heap W = heap W -reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | expr W = expr (bin₁ W) -reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′)) -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s) -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)) -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W) -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)) -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W -reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W) -reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′)) -reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W′ -reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W -reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W) +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) (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) (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) with preservationᴱ H M s -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r → p (trans r q))) -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W) -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with reflectᴱ H M s W′ -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W) -reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′)) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′)) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orNone (sym p)) (sym r)))) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-none v -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orNone (sym p))) -reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W) -reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W′))) -reflectᴮ H (return M ∙ B) (return s) (return W′) with reflectᴱ H M s W′ -reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W -reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return 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) (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′)) +reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ with reflect-substitutionᴮ _ B (addr a) f W′ +reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Left W = Left (function₂ (reflect-weakeningᴮ (f ↦ (T ⇒ U)) H B (snoc defn) W)) +reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Left (UnallocatedAddress ())) +reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Right p) = CONTRADICTION (≮:-refl p) +reflectᴮ H (return M ∙ B) (return s) (return W′) = mapL return (reflectᴱ H M s W′) -reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴᴱ H′ (typeCheckᴴᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) -reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) +reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H)) +reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H)) -reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′ -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q → p (trans q r)) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′)) -reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) -reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′) -reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W -reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W) -reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′) -reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W -reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W) -reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′ -reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′) -reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W -reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W) -reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′ -reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′ -reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W′) = heap W′ -reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′) -reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W -reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W) -reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′) -reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W -reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W) +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 (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) +reflectᴴᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) W = Right W +reflectᴴᴱ H (block var b ∈ T is done end) done W = Right W +reflectᴴᴱ H (binexp M op N) (binOp₀ s) W = Right W +reflectᴴᴱ H (binexp M op N) (binOp₁ s) W = mapL bin₁ (reflectᴴᴱ H M s W) +reflectᴴᴱ H (binexp M op N) (binOp₂ s) W = mapL bin₂ (reflectᴴᴱ H N s W) -reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′ -reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′) -reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W = heap W -reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W) -reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′ -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q → p (trans q r))) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′)) -reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) -reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′) -reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W -reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | expr W = block (return 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 (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) +reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) W = Right W +reflectᴴᴮ H (return M ∙ B) (return s) W = mapL return (reflectᴴᴱ H M s W) -reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) +reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Either (Warningᴮ H′ (typeCheckᴮ H′ ∅ B′)) (Warningᴴ H′ (typeCheckᴴ H′)) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H)) reflect* H B refl W = W -reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W) +reflect* H B (step s t) W = cond (reflectᴮ H B s) (reflectᴴᴮ H B s) (reflect* _ _ t W) -runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → BinOpWarning op (orNone (typeOfⱽ H v)) -runtimeBinOpWarning H v (+ p) = + (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (- p) = - (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (* p) = * (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (/ p) = / (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q)) -runtimeBinOpWarning H v (·· p) = ·· (λ q → p (mustBeString H ∅ v q)) +isntNumber : ∀ H v → (valueType v ≢ number) → (typeOfᴱ H ∅ (val v) ≮: number) +isntNumber H nil p = scalar-≢-impl-≮: nil number (λ ()) +isntNumber H (addr a) p with remember (H [ a ]ᴴ) +isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar number) +isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar number) +isntNumber H (number x) p = CONTRADICTION (p refl) +isntNumber H (bool x) p = scalar-≢-impl-≮: boolean number (λ ()) +isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ()) + +isntString : ∀ H v → (valueType v ≢ string) → (typeOfᴱ H ∅ (val v) ≮: string) +isntString H nil p = scalar-≢-impl-≮: nil string (λ ()) +isntString H (addr a) p with remember (H [ a ]ᴴ) +isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar string) +isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar string) +isntString H (number x) p = scalar-≢-impl-≮: number string (λ ()) +isntString H (bool x) p = scalar-≢-impl-≮: boolean string (λ ()) +isntString H (string x) p = CONTRADICTION (p refl) + +isntFunction : ∀ H v {T U} → (valueType v ≢ function) → (typeOfᴱ H ∅ (val v) ≮: (T ⇒ U)) +isntFunction H nil p = scalar-≮:-function nil +isntFunction H (addr a) p = CONTRADICTION (p refl) +isntFunction H (number x) p = scalar-≮:-function number +isntFunction H (bool x) p = scalar-≮:-function boolean +isntFunction H (string x) p = scalar-≮:-function string + +isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: none) +isntEmpty H nil = scalar-≮:-none nil +isntEmpty H (addr a) with remember (H [ a ]ᴴ) +isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) function-≮:-none +isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) any-≮:-none +isntEmpty H (number x) = scalar-≮:-none number +isntEmpty H (bool x) = scalar-≮:-none boolean +isntEmpty H (string x) = scalar-≮:-none string + +runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → (typeOfᴱ H ∅ (val v) ≮: srcBinOp op) +runtimeBinOpWarning H v (+ p) = isntNumber H v p +runtimeBinOpWarning H v (- p) = isntNumber H v p +runtimeBinOpWarning H v (* p) = isntNumber H v p +runtimeBinOpWarning H v (/ p) = isntNumber H v p +runtimeBinOpWarning H v (< p) = isntNumber H v p +runtimeBinOpWarning H v (> p) = isntNumber H v p +runtimeBinOpWarning H v (<= p) = isntNumber H v p +runtimeBinOpWarning H v (>= p) = isntNumber H v p +runtimeBinOpWarning H v (·· p) = isntString H v p runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M) runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B) runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-none w -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = FunctionCallMismatch (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r)))) -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (any-src-≮: (isntEmpty H w) (isntFunction H v p)) runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err) runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err) runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err) @@ -469,6 +343,6 @@ runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runt runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err) wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B) -wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H′ B′ err)) -wellTypedProgramsDontGoWrong H′ B B′ t err | heap (addr a refl ()) -wellTypedProgramsDontGoWrong H′ B B′ t err | block W = W +wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (Left (runtimeWarningᴮ H′ B′ err)) +wellTypedProgramsDontGoWrong H′ B B′ t err | Right (addr a refl ()) +wellTypedProgramsDontGoWrong H′ B B′ t err | Left W = W diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda new file mode 100644 index 0000000..6a0b420 --- /dev/null +++ b/prototyping/Properties/Subtyping.agda @@ -0,0 +1,221 @@ +{-# OPTIONS --rewriting #-} + +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 Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; any; none; 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; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt) +open import Properties.Contradiction using (CONTRADICTION; ¬) +open import Properties.Equality using (_≢_) +open import Properties.Functions using (_∘_) + +src = Luau.Type.src strict + +-- Language membership is decidable +dec-language : ∀ T t → Either (¬Language T t) (Language T t) +dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ())) +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-err t) = Right (scalar-function-err nil) +dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ())) +dec-language boolean (scalar boolean) = Right (scalar boolean) +dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ())) +dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ())) +dec-language boolean function = Left (scalar-function boolean) +dec-language boolean (function-ok t) = Left (scalar-function-ok boolean) +dec-language boolean (function-err t) = Right (scalar-function-err boolean) +dec-language number (scalar number) = Right (scalar number) +dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ())) +dec-language number (scalar string) = Left (scalar-scalar string number (λ ())) +dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ())) +dec-language number function = Left (scalar-function number) +dec-language number (function-ok t) = Left (scalar-function-ok number) +dec-language number (function-err t) = Right (scalar-function-err number) +dec-language string (scalar number) = Left (scalar-scalar number string (λ ())) +dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ())) +dec-language string (scalar string) = Right (scalar string) +dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ())) +dec-language string function = Left (scalar-function string) +dec-language string (function-ok t) = Left (scalar-function-ok string) +dec-language string (function-err t) = Right (scalar-function-err string) +dec-language (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-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t)) +dec-language none t = Left none +dec-language any t = Right any +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) + +-- ¬Language T is the complement of Language T +language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t) +language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q +language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q +language-comp t (left p) (q₁ , q₂) = language-comp t p q₁ +language-comp t (right p) (q₁ , q₂) = language-comp t p q₂ +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) none (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 + +-- ≮: is the complement of <: +¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U) +¬≮:-impl-<: {T} {U} p t q with dec-language U t +¬≮:-impl-<: {T} {U} p t q | Left r = CONTRADICTION (p (witness t q r)) +¬≮:-impl-<: {T} {U} p t q | Right r = r + +<:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U) +<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q) + +-- reflexivity +≮:-refl : ∀ {T} → ¬(T ≮: T) +≮:-refl (witness t p q) = language-comp t q p + +<:-refl : ∀ {T} → (T <: T) +<:-refl = ¬≮:-impl-<: ≮:-refl + +-- transititivity +≮:-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-≮: 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) + +<:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U) +<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans) + +-- Properties of scalars +skalar = number ∪ (string ∪ (nil ∪ boolean)) + +function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U) +function-≮:-scalar s = witness function function (scalar-function s) + +scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T)) +scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s) + +any-≮:-scalar : ∀ {U} → (Scalar U) → (any ≮: U) +any-≮:-scalar s = witness (function-ok (scalar s)) any (scalar-function-ok s) + +scalar-≮:-none : ∀ {U} → (Scalar U) → (U ≮: none) +scalar-≮:-none s = witness (scalar s) (scalar s) none + +scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U) +scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p) + +-- Properties of tgt +tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t) +tgt-function-ok {T = nil} (scalar ()) +tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p +tgt-function-ok {T = none} (scalar ()) +tgt-function-ok {T = any} p = any +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 any = any + +skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t)) +skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean))) + +skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s)) +skalar-scalar number = left (scalar number) +skalar-scalar boolean = right (right (right (scalar boolean))) +skalar-scalar string = right (left (scalar string)) +skalar-scalar nil = right (right (left (scalar nil))) + +tgt-none-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (none ⇒ U))) +tgt-none-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q) + +none-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (none ⇒ U))) → (tgt T ≮: U) +none-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁)) +none-tgt-≮: (witness function p (q₁ , scalar-function ())) +none-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂ +none-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ()))) + +-- Properties of src +function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t) +function-err-src {T = nil} none = scalar-function-err nil +function-err-src {T = T₁ ⇒ T₂} p = function-err p +function-err-src {T = none} (scalar-scalar number () p) +function-err-src {T = none} (scalar-function-ok ()) +function-err-src {T = any} none = any +function-err-src {T = boolean} p = scalar-function-err boolean +function-err-src {T = number} p = scalar-function-err number +function-err-src {T = string} p = scalar-function-err string +function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p) +function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p) +function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂ + +¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t) +¬function-err-src {T = nil} (scalar ()) +¬function-err-src {T = T₁ ⇒ T₂} p = function-err p +¬function-err-src {T = none} any = none +¬function-err-src {T = any} (scalar ()) +¬function-err-src {T = boolean} (scalar ()) +¬function-err-src {T = number} (scalar ()) +¬function-err-src {T = string} (scalar ()) +¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂) +¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p) +¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p) + +src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t) +src-¬function-err {T = nil} p = none +src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p +src-¬function-err {T = none} (scalar-function-err ()) +src-¬function-err {T = any} p = none +src-¬function-err {T = boolean} p = none +src-¬function-err {T = number} p = none +src-¬function-err {T = string} p = none +src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p) +src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p) +src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂) + +src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t) +src-¬scalar number (scalar number) = none +src-¬scalar boolean (scalar boolean) = none +src-¬scalar string (scalar string) = none +src-¬scalar nil (scalar nil) = none +src-¬scalar s (left p) = left (src-¬scalar s p) +src-¬scalar s (right p) = right (src-¬scalar s p) +src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂) +src-¬scalar s any = none + +src-any-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ any)) +src-any-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p) + +any-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ any)) → (U ≮: src T) +any-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p) +any-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q))) +any-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ()))) +any-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p) + +-- Properties of any and none +any-≮: : ∀ {T U} → (T ≮: U) → (any ≮: U) +any-≮: (witness t p q) = witness t any q + +none-≮: : ∀ {T U} → (T ≮: U) → (T ≮: none) +none-≮: (witness t p q) = witness t p none + +any-≮:-none : (any ≮: none) +any-≮:-none = witness (scalar nil) any none + +function-≮:-none : ∀ {T U} → ((T ⇒ U) ≮: none) +function-≮:-none = witness function function none diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index bec6884..ead0c09 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -8,7 +8,7 @@ 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.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orAny; tgtBinOp) open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=) open import Luau.Type using (Type; nil; any; none; number; boolean; string; _⇒_; tgt) open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType) @@ -42,8 +42,8 @@ typeOfⱽ H (string x) = just string typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type -typeOfᴱ H Γ (var x) = orNone(Γ [ x ]ⱽ) -typeOfᴱ H Γ (val v) = orNone(typeOfⱽ H v) +typeOfᴱ H Γ (var x) = orAny(Γ [ x ]ⱽ) +typeOfᴱ H Γ (val v) = orAny(typeOfⱽ H v) typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M) typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T typeOfᴱ H Γ (block var b ∈ T is B end) = T @@ -64,17 +64,17 @@ 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 orNone (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | () -mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p mustBeNumber H Γ (addr a) p | nothing , q | () mustBeNumber H Γ (number n) p = refl mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string) mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ) -mustBeString H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | () -mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p +mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p mustBeString H Γ (addr a) p | (nothing , q) | () mustBeString H Γ (string x) p = refl @@ -83,7 +83,7 @@ typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) typeCheckᴱ H Γ (var x) = var refl typeCheckᴱ H Γ (val nil) = nil -typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ))) +typeCheckᴱ H Γ (val (addr a)) = addr (orAny (typeOfᴹᴼ (H [ a ]ᴴ))) typeCheckᴱ H Γ (val (number n)) = number typeCheckᴱ H Γ (val (bool b)) = bool typeCheckᴱ H Γ (val (string x)) = string @@ -109,4 +109,4 @@ typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M) typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M) typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M) - \ No newline at end of file + diff --git a/prototyping/Tests/Interpreter/concat_number_and_string/out.txt b/prototyping/Tests/Interpreter/concat_number_and_string/out.txt index a437438..80c9d6e 100644 --- a/prototyping/Tests/Interpreter/concat_number_and_string/out.txt +++ b/prototyping/Tests/Interpreter/concat_number_and_string/out.txt @@ -9,3 +9,4 @@ value 37.0 is not a string TYPE ERROR: Local variable y has type string but expression has type number + because provided type contains v, where v is a number