From 8e52542526c0401be46936ab21f2caebf993fcaa Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 16 Feb 2022 23:03:40 -0600 Subject: [PATCH] WIP --- prototyping/FFI/Data/Aeson.agda | 5 + prototyping/FFI/Data/Vector.agda | 5 + prototyping/Luau/AddrCtxt.agda | 2 + prototyping/Luau/Heap.agda | 12 +- prototyping/Luau/OpSem.agda | 2 + prototyping/Luau/RuntimeError.agda | 2 + prototyping/Luau/StrictMode.agda | 97 +++++++----- prototyping/Luau/TypeCheck.agda | 158 +++++++++++++------ prototyping/Luau/VarCtxt.agda | 9 +- prototyping/Properties/Step.agda | 2 + prototyping/Properties/StrictMode.agda | 210 +++++++++++++++++-------- prototyping/Properties/TypeCheck.agda | 62 ++++---- 12 files changed, 374 insertions(+), 192 deletions(-) diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index 69c973a1..77d1b301 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -1,6 +1,9 @@ +{-# OPTIONS --rewriting #-} + module FFI.Data.Aeson where open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Equality.Rewrite using () open import Agda.Builtin.Bool using (Bool) open import Agda.Builtin.String using (String) @@ -42,6 +45,8 @@ postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m postulate lookup-empty : ∀ {A} k → (lookup {A} k empty ≡ nothing) postulate singleton-insert-empty : ∀ {A} k (v : A) → (singleton k v ≡ insert k v empty) +{-# REWRITE lookup-insert lookup-empty singleton-insert-empty #-} + data Value : Set where object : KeyMap Value → Value array : Vector Value → Value diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 2c5d1925..0835698f 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -1,6 +1,9 @@ +{-# OPTIONS --rewriting #-} + module FFI.Data.Vector where open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Equality.Rewrite using () open import Agda.Builtin.Int using (Int; pos; negsuc) open import Agda.Builtin.Nat using (Nat) open import FFI.Data.Bool using (Bool; false; true) @@ -33,6 +36,8 @@ postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0) postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x) postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x) +{-# REWRITE length-empty lookup-snoc lookup-snoc-empty #-} + head : ∀ {A} → (Vector A) → (Maybe A) head vec with null vec head vec | false = just (unsafeHead vec) diff --git a/prototyping/Luau/AddrCtxt.agda b/prototyping/Luau/AddrCtxt.agda index 875ac5ca..592c4645 100644 --- a/prototyping/Luau/AddrCtxt.agda +++ b/prototyping/Luau/AddrCtxt.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.AddrCtxt where open import Luau.Type using (Type) diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index 1d5d9c30..6e30caa8 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.Heap where open import Agda.Builtin.Equality using (_≡_) @@ -37,13 +39,3 @@ next = length allocated : ∀ {a} → Heap a → HeapValue a → Heap a allocated = snoc - --- next-emp : (length empty ≡ 0) -next-emp = FFI.Data.Vector.length-empty - --- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V) -lookup-next = FFI.Data.Vector.lookup-snoc - --- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V) -lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty - diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index c7b33a75..e41102d8 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.OpSem where open import Agda.Builtin.Equality using (_≡_) diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index e514dc9d..91bcfd2c 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.RuntimeError where open import Agda.Builtin.Equality using (_≡_) diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index da0ec058..e4823912 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -1,81 +1,108 @@ +{-# OPTIONS --rewriting #-} + 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; yes; nil; addr; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name) open import Luau.Type using (Type; strict; bot; top; nil; _⇒_; tgt) -open import Luau.Heap using (Heap) renaming (_[_] to _[_]ᴴ) +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; block; return; local; function) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; var; addr; app; block; return; local; function) open import Properties.Equality using (_≢_) -open import Properties.TypeCheck(strict) using (typeOfᴴ) +open import Properties.TypeCheck(strict) using (typeOfᴴ; typeCheckᴮ) src : Type → Type src = Luau.Type.src strict -data Warningᴱ (H : Heap yes) {Γ S} : ∀ {M T Δ} → (Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → Set -data Warningᴮ (H : Heap yes) {Γ S} : ∀ {B T Δ} → (Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → Set +data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set +data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set -data Warningᴱ H {Γ S} where +data Warningᴱ H {Γ} where - bot : ∀ {M T Δ} {D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → + BadlyTypedFunctionAddress : ∀ a f {x S T U B} → - (T ≡ bot) → - ------------ - Warningᴱ H D + (H [ a ]ᴴ ≡ just (function f ⟨ var x ∈ T ⟩∈ U is B end)) → + Warningᴮ H (typeCheckᴮ H (x ↦ T) B) → + -------------------------------------------------------- + Warningᴱ H (addr a S) - addr : ∀ a T → + UnallocatedAddress : ∀ a {T} → - (T ≢ typeOfᴴ(H [ a ]ᴴ)) → - ------------------------- + (H [ a ]ᴴ ≡ nothing) → + -------------------------------------------------------- Warningᴱ H (addr a T) - app₁ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + app₀ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → + + (src T ≢ U) → + ----------------- + Warningᴱ H (app D₁ D₂) + + app₁ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → Warningᴱ H D₁ → ----------------- Warningᴱ H (app D₁ D₂) - app₂ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + app₂ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → Warningᴱ H D₂ → ----------------- - Warningᴱ H(app D₁ D₂) + Warningᴱ H (app D₁ D₂) - block : ∀ b {B T Δ} {D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → + function₀ : ∀ f {x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → + + (U ≢ V) → + ------------------------- + Warningᴱ H (function f {U = U} D) + + function₁ : ∀ f {x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → + + Warningᴮ H D → + ------------------------- + Warningᴱ H (function f {U = U} D) + + block : ∀ b {B T} {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → ----------------- - Warningᴱ H(block b D) + Warningᴱ H (block b D) -data Warningᴮ H {Γ S} where +data Warningᴮ H {Γ} where - disagree : ∀ {B T Δ} {D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → - - (S ≢ T) → - ----------- - Warningᴮ H D - - return : ∀ {M B T U Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁} {D₂ : Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂} → + return : ∀ {M B T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴮ B ∈ U} → Warningᴱ H D₁ → ------------------ Warningᴮ H (return D₁ D₂) - local₁ : ∀ {x M B T U V Δ₁ Δ₂} {D₁ : Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂} → + local₀ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → + + (T ≢ U) → + -------------------- + Warningᴮ H (local D₁ D₂) + + local₁ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → Warningᴱ H D₁ → -------------------- Warningᴮ H (local D₁ D₂) --- data Warningᴴ {H} : ∀ {V T} → (H ▷ V ∈ T) → Set where + local₂ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} → --- nothing : + Warningᴮ H D₂ → + -------------------- + Warningᴮ H (local D₁ D₂) --- ----------------- --- Warningᴴ(nothing) + function₁ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → --- function : ∀ f {x B T U V W} {D : (x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ (x ↦ W)} → + Warningᴮ H D₁ → + -------------------- + Warningᴮ H (function f D₁ D₂) --- Warningᴮ(D) → --- -------------------- --- Warningᴴ(function f D) + function₂ : ∀ f {x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} → + + Warningᴮ H D₂ → + -------------------- + Warningᴮ H (function f D₁ D₂) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index a144a0f9..0a787761 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Luau.Type using (Mode) module Luau.TypeCheck (m : Mode) where @@ -17,70 +19,138 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) src : Type → Type src = Luau.Type.src m -data _⊢ᴮ_∋_∈_⊣_ : VarCtxt → Type → Block yes → Type → VarCtxt → Set -data _⊢ᴱ_∋_∈_⊣_ : VarCtxt → Type → Expr yes → Type → VarCtxt → Set +data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set +data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set -data _⊢ᴮ_∋_∈_⊣_ where +data _⊢ᴮ_∈_ where - done : ∀ {S Γ} → + done : ∀ {Γ} → - ---------------------- - Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ + --------------- + Γ ⊢ᴮ done ∈ nil - return : ∀ {M B S T U Γ Δ₁ Δ₂} → + return : ∀ {M B T U Γ} → - Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → - Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂ → - --------------------------------- - Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ + Γ ⊢ᴱ M ∈ T → + Γ ⊢ᴮ B ∈ U → + --------------------- + Γ ⊢ᴮ return M ∙ B ∈ T - local : ∀ {x M B S T U V Γ Δ₁ Δ₂} → + local : ∀ {x M B T U V Γ} → - Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → - (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → - ---------------------------------------------------------- - Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) + Γ ⊢ᴱ M ∈ U → + (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V → + -------------------------------- + Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V - function : ∀ {f x B C S T U V W Γ Δ₁ Δ₂} → + function : ∀ f {x B C T U V W Γ} → - (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ C ∈ V ⊣ Δ₁ → - (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ W ⊣ Δ₂ → - --------------------------------------------------------------------------------- - Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) + (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V → + (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W → + ------------------------------------------------- + Γ ⊢ᴮ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W -data _⊢ᴱ_∋_∈_⊣_ where +data _⊢ᴱ_∈_ where - nil : ∀ {S Γ} → + nil : ∀ {Γ} → - ---------------------- - Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ + -------------- + Γ ⊢ᴱ nil ∈ nil - var : ∀ x {S T Γ} → + var : ∀ x {T Γ} → T ≡ Γ [ x ]ⱽ → - ---------------------------- - Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) + -------------- + Γ ⊢ᴱ var x ∈ T - addr : ∀ a T {S Γ} → + addr : ∀ a T {Γ} → - ------------------------- - Γ ⊢ᴱ S ∋ (addr a) ∈ T ⊣ ∅ + ----------------- + Γ ⊢ᴱ (addr a) ∈ T - app : ∀ {M N S T U Γ Δ₁ Δ₂} → + app : ∀ {M N T U Γ} → - Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁ → - Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → - -------------------------------------- - Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) + Γ ⊢ᴱ M ∈ T → + Γ ⊢ᴱ N ∈ U → + ---------------------- + Γ ⊢ᴱ (M $ N) ∈ (tgt T) - function : ∀ {f x B S T U V Γ Δ} → + function : ∀ f {x B T U V Γ} → - (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ → - ----------------------------------------------------------------------- - Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) + (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V → + ----------------------------------------------------- + Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) - block : ∀ b {B S T Γ Δ} → + block : ∀ b {B T Γ} → - Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → - ---------------------------------------------------- - Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ + Γ ⊢ᴮ B ∈ T → + --------------------------- + Γ ⊢ᴱ (block b is B end) ∈ T + +-- data _⊢ᴮ_∋_∈_⊣_ : VarCtxt → Type → Block yes → Type → VarCtxt → Set +-- data _⊢ᴱ_∋_∈_⊣_ : VarCtxt → Type → Expr yes → Type → VarCtxt → Set + +-- data _⊢ᴮ_∋_∈_⊣_ where + +-- done : ∀ {S Γ} → + +-- ---------------------- +-- Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ + +-- return : ∀ {M B S T U Γ Δ₁ Δ₂} → + +-- Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → +-- Γ ⊢ᴮ nil ∋ B ∈ U ⊣ Δ₂ → +-- --------------------------------- +-- Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ + +-- local : ∀ {x M B S T U V Γ Δ₁ Δ₂} → + +-- Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁ → +-- (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → +-- ---------------------------------------------------------- +-- Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) + +-- function : ∀ {f x B C S T U V W Γ Δ₁ Δ₂} → + +-- (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ C ∈ V ⊣ Δ₁ → +-- (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ W ⊣ Δ₂ → +-- --------------------------------------------------------------------------------- +-- Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) + +-- data _⊢ᴱ_∋_∈_⊣_ where + +-- nil : ∀ {S Γ} → + +-- ---------------------- +-- Γ ⊢ᴱ S ∋ nil ∈ nil ⊣ ∅ + +-- var : ∀ x {S T Γ} → + +-- T ≡ Γ [ x ]ⱽ → +-- ---------------------------- +-- Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) + +-- addr : ∀ a T {S Γ} → + +-- ------------------------- +-- Γ ⊢ᴱ S ∋ (addr a) ∈ T ⊣ ∅ + +-- app : ∀ {M N S T U Γ Δ₁ Δ₂} → + +-- Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁ → +-- Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂ → +-- -------------------------------------- +-- Γ ⊢ᴱ S ∋ (M $ N) ∈ (tgt T) ⊣ (Δ₁ ⋒ Δ₂) + +-- function : ∀ {f x B S T U V Γ Δ} → + +-- (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ Δ → +-- ----------------------------------------------------------------------- +-- Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) + +-- block : ∀ b {B S T Γ Δ} → + +-- Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → +-- ---------------------------------------------------- +-- Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index 1cbcb48e..9ad2e2f5 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.VarCtxt where open import Agda.Builtin.Equality using (_≡_) @@ -34,10 +36,3 @@ x ↦ T = singleton (fromString x) T _⊕_↦_ : VarCtxt → Var → Type → VarCtxt Γ ⊕ x ↦ T = insert (fromString x) T Γ - --- ⊕-[] : ∀ (Γ : VarCtxt) x T → (((Γ ⊕ x ↦ T) [ x ]) ≡ T) -⊕-[] = λ (Γ : VarCtxt) x T → cong orBot (lookup-insert (fromString x) T Γ) - --- ∅-[] : ∀ x → ∅ [ x ] ≡ bot -∅-[] = λ (x : Var) → cong orBot (lookup-empty (fromString x)) - diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index f4a7aad6..cf7a5ae7 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Properties.Step where open import Agda.Builtin.Equality using (_≡_; refl) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 31a44580..f75b89d7 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -5,102 +5,188 @@ module Properties.StrictMode where import Agda.Builtin.Equality.Rewrite open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Maybe using (Maybe; just; nothing) -open import Luau.Heap using (Heap; HeapValue; function_is_end; defn; alloc; ok; next; lookup-next) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) -open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; disagree; addr; app₁; app₂; block; return; local₁) -open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ) -open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg) +open import Luau.Heap using (Heap; HeapValue; function_is_end; defn; alloc; ok; next) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; BadlyTypedFunctionAddress; UnallocatedAddress; app₀; app₁; app₂; block; return; local₀; local₁; local₂; function₀; function₁; function₂) +open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) +open import Luau.Syntax using (Expr; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg) open import Luau.Type using (Type; strict; nil; _⇒_; bot; tgt) -open import Luau.TypeCheck(strict) using (_⊢ᴮ_∋_∈_⊣_; _⊢ᴱ_∋_∈_⊣_; nil; var; addr; app; function; block; done; return; local) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; nil; var; addr; app; function; block; done; return; local) open import Luau.Value using (val; nil; addr) +open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) open import Luau.AddrCtxt using (AddrCtxt) -open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ∅-[]) renaming (_[_] to _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.VarCtxt using (VarCtxt; ∅) open import Properties.Remember using (remember; _,_) -open import Properties.Equality using (sym; cong; trans; subst₁) +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ᴮ; typeCheckᴱ; typeCheckᴮ) +open import Properties.TypeCheck(strict) using (declaredTypeᴴ; typeOfⱽ; typeOfᴴ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ) open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) -{-# REWRITE lookup-next #-} - src = Luau.Type.src strict +_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) +_≡ᵀ_ = {!!} + data _⊑_ (H : Heap yes) : Heap yes → Set where refl : (H ⊑ H) snoc : ∀ {H′ H″ a V} → (H ⊑ H′) → (H″ ≡ᴴ H′ ⊕ a ↦ V) → (H ⊑ H″) -warning-⊑ : ∀ {H H′ Γ Δ S T M} {D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → (H ⊑ H′) → (Warningᴱ H′ D) → Warningᴱ H D +warning-⊑ : ∀ {H H′ Γ T M} {D : Γ ⊢ᴱ M ∈ T} → (H ⊑ H′) → (Warningᴱ H′ D) → Warningᴱ H D warning-⊑ = {!!} -data TypeOfᴱ-⊑-Result H H′ Γ M : Set where - ok : (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M) → TypeOfᴱ-⊑-Result H H′ Γ M - warning : (∀ {S} → Warningᴱ H (typeCheckᴱ H Γ S M)) → TypeOfᴱ-⊑-Result H H′ Γ M +data LookupResult (H : Heap yes) a V : Set where + just : (H [ a ]ᴴ ≡ just V) → LookupResult H a V + nothing : (H [ a ]ᴴ ≡ nothing) → LookupResult H a V -data TypeOfᴮ-⊑-Result H H′ Γ B : Set where - ok : (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B) → TypeOfᴮ-⊑-Result H H′ Γ B - warning : (∀ {S} → Warningᴮ H (typeCheckᴮ H Γ S B)) → TypeOfᴮ-⊑-Result H H′ Γ B +lookup-⊑-just : ∀ {H H′ V} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ just V) → LookupResult H a V +lookup-⊑-just = {!!} -typeOfᴱ-⊑ : ∀ {H H′ Γ M} → (H ⊑ H′) → (TypeOfᴱ-⊑-Result H H′ Γ M) -typeOfᴱ-⊑ = {!!} +lookup-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ nothing) +lookup-⊑-nothing = {!!} -typeOfᴮ-⊑ : ∀ {H H′ Γ B} → (H ⊑ H′) → (TypeOfᴮ-⊑-Result H H′ Γ B) -typeOfᴮ-⊑ = {!!} +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 -blah : ∀ {H H′ Γ S S′ M} → (H ⊑ H′) → (S ≡ S′) → (Warningᴱ H′ (typeCheckᴱ H′ Γ S′ M)) → (Warningᴱ H (typeCheckᴱ H Γ S M)) -blah = {!!} - -bloz : ∀ {H Γ S S′ M} → (S ≡ S′) → (Warningᴱ H (typeCheckᴱ H Γ S′ M)) → (Warningᴱ H (typeCheckᴱ H Γ S M)) -bloz = {!!} +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 redn-⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′) redn-⊑ = {!!} +⊕-overwrite : ∀ {Γ x y T U} → (x ≡ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ (Γ ⊕ y ↦ U) +⊕-overwrite = {!!} + +⊕-swap : ∀ {Γ x y T U} → (x ≢ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ ((Γ ⊕ y ↦ U) ⊕ x ↦ T) +⊕-swap = {!!} + substitutivityᴱ : ∀ {Γ T H M v x} → (T ≡ typeOfᴱ H Γ (val v)) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ)) substitutivityᴮ : ∀ {Γ T H B v x} → (T ≡ typeOfᴱ H Γ (val v)) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) substitutivityᴱ = {!!} substitutivityᴮ = {!!} -preservationᴱ : ∀ {H H′ M M′ Γ} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M′) -preservationᴮ : ∀ {H H′ B B′ Γ} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B′) +heap-weakeningᴱ : ∀ {H H′ M Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M) +heap-weakeningᴮ : ∀ {H H′ B Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B) -preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = refl -preservationᴱ (app s) = cong tgt (preservationᴱ s) -preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ T} p) = trans (cong tgt (cong typeOfᴴ p)) {!!} -preservationᴱ (block s) = preservationᴮ s -preservationᴱ (return p) = refl -preservationᴱ done = refl +heap-weakeningᴱ = {!!} +heap-weakeningᴮ = {!!} -preservationᴮ (local {x = var x ∈ T} {B = B} s) with typeOfᴮ-⊑ {B = B} (redn-⊑ s) -preservationᴮ (local {x = var x ∈ T} s) | ok p = p -preservationᴮ (local {x = var x ∈ T} s) | warning W = {!!} -preservationᴮ (subst {x = var x ∈ T} {B = B}) = substitutivityᴮ {B = B} {!!} -preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) with typeOfᴮ-⊑ {B = B} (snoc refl defn) -preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | ok r = trans r (substitutivityᴮ {T = S ⇒ T} {B = B} refl) -preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | warning W = {!!} -preservationᴮ (return s) = preservationᴱ s +preservationᴱ : ∀ {H H′ M M′ Γ} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M′) +preservationᴮ : ∀ {H H′ B B′ Γ} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B′) -reflectᴱ : ∀ {H H′ M M′ S} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ S M′) → Warningᴱ H (typeCheckᴱ H ∅ S M) -reflectᴮ : ∀ {H H′ B B′ S} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ S B′) → Warningᴮ H (typeCheckᴮ H ∅ S B) +preservationᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) = ok refl +preservationᴱ (app s) with preservationᴱ s +preservationᴱ (app s) | ok p = ok (cong tgt p) +preservationᴱ (app s) | warning W = warning (app₁ W) +preservationᴱ (beta {F = f ⟨ var x ∈ S ⟩∈ T} p) = {!!} -- ok (trans (cong tgt (cong typeOfᴴ p)) {!!}) +preservationᴱ (block s) with preservationᴮ s +preservationᴱ (block s) | ok p = ok p +preservationᴱ (block {b = b} s) | warning W = warning (block b W) +preservationᴱ (return p) = ok refl +preservationᴱ done = ok refl -reflectᴱ s W with redn-⊑ s -reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (addr a _ r) | p = CONTRADICTION (r refl) -reflectᴱ (app s) (bot x) | p = {!x!} -reflectᴱ (app s) (app₁ W) | p with typeOfᴱ-⊑ p -reflectᴱ (app s) (app₁ W) | p | ok q = app₁ (bloz (cong (λ ∙ → ∙ ⇒ _) q) (reflectᴱ s W)) -reflectᴱ (app s) (app₁ W) | p | warning W′ = app₂ W′ -reflectᴱ (app s) (app₂ W) | p = app₂ (blah p (cong src (preservationᴱ s)) W) -reflectᴱ (beta s) (bot x₁) | p = {!!} -reflectᴱ (beta {F = f ⟨ var x ∈ T ⟩∈ U} q) (block _ (disagree x₁)) | p = {!!} -reflectᴱ (beta {F = f ⟨ var x ∈ T ⟩∈ U} q) (block _ (local₁ W)) | p = app₂ (bloz (cong src (cong typeOfᴴ q)) W) -reflectᴱ (block s) (bot x₁) | p = {!!} -reflectᴱ (block s) (block b W) | p = block b (reflectᴮ s W) -reflectᴱ (return q) W | p = block _ (return W) -reflectᴱ done (bot x) | p = {!!} +preservationᴮ (local {x = var x ∈ T} s) with heap-weakeningᴮ (redn-⊑ s) +preservationᴮ (local {x = var x ∈ T} s) | ok p = ok p +preservationᴮ (local {x = var x ∈ T} s) | warning W = warning (local₂ W) +preservationᴮ (subst {x = var x ∈ T} {B = B}) = ok (substitutivityᴮ {B = B} {!!}) +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) with heap-weakeningᴮ (snoc refl defn) +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | ok r = ok (trans r (substitutivityᴮ {T = S ⇒ T} {B = B} refl)) +preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | warning W = warning (function₂ f W) +preservationᴮ (return s) with preservationᴱ s +preservationᴮ (return s) | ok p = ok p +preservationᴮ (return s) | warning W = warning (return W) -reflectᴮ s = {!!} +reflect-substitutionᴱ : ∀ {H Γ Γ′ T} M v x → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H Γ′ M) +reflect-substitutionᴱ-whenever-yes : ∀ {H Γ Γ′ T} v x y (p : x ≡ y) → (typeOfᴱ H Γ (val v) ≡ T) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H Γ′ (var y)) +reflect-substitutionᴱ-whenever-no : ∀ {H Γ Γ′ T} v x y (p : x ≢ y) → (typeOfᴱ H Γ (val v) ≡ T) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H Γ′ (var y)) +reflect-substitutionᴮ : ∀ {H Γ Γ′ T} B v x → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +reflect-substitutionᴮ-unless-yes : ∀ {H Γ Γ′ T} B v x y (r : x ≡ y) → (T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) + +reflect-substitutionᴱ (var y) v x refl q W with x ≡ⱽ y +reflect-substitutionᴱ (var y) v x refl q W | yes r = reflect-substitutionᴱ-whenever-yes v x y r (typeOfᴱⱽ v) q W +reflect-substitutionᴱ (var y) v x refl q W | no r = reflect-substitutionᴱ-whenever-no v x y r (typeOfᴱⱽ v) q W +reflect-substitutionᴱ (addr a) v x p q (BadlyTypedFunctionAddress a f r W) = BadlyTypedFunctionAddress a f r W +reflect-substitutionᴱ (addr a) v x p q (UnallocatedAddress a r) = UnallocatedAddress a r +reflect-substitutionᴱ (M $ N) v x p q (app₀ r) = {!!} +reflect-substitutionᴱ (M $ N) v x p q (app₁ W) = app₁ (reflect-substitutionᴱ M v x p q W) +reflect-substitutionᴱ (M $ N) v x p q (app₂ W) = app₂ (reflect-substitutionᴱ N v x p q W) +reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p q (function₀ f r) = {!!} +reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p refl (function₁ f W) with (x ≡ⱽ y) +reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p refl (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-overwrite r) W) +reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p refl (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ B v x p (⊕-swap r) W) +reflect-substitutionᴱ (block b is B end) v x p q (block b W) = block b (reflect-substitutionᴮ B v x p q W) + +reflect-substitutionᴱ-whenever-no v x y r refl refl () +reflect-substitutionᴱ-whenever-yes (addr a) x x refl refl refl (BadlyTypedFunctionAddress a f p W) = {!!} +reflect-substitutionᴱ-whenever-yes (addr a) x x refl refl refl (UnallocatedAddress a p) = {!!} + +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₁ f W) = {!!} +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p q (function₂ f W) = {!!} +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₀ r) = {!!} +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₁ W) = local₁ (reflect-substitutionᴱ M v x p q W) +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p q (local₂ W) = {!!} +reflect-substitutionᴮ (return M ∙ B) v x p q (return W) = return (reflect-substitutionᴱ M v x p q W) + +reflect-substitutionᴮ-unless-yes B v x y r p refl W = W + +reflect-weakeningᴱ : ∀ {H H′ Γ M} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) +reflect-weakeningᴮ : ∀ {H H′ Γ B} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) + +reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) with lookup-⊑-just a h p +reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) | just q = BadlyTypedFunctionAddress a f q (reflect-weakeningᴮ h W) +reflect-weakeningᴱ h (BadlyTypedFunctionAddress a f p W) | nothing q = UnallocatedAddress a q +reflect-weakeningᴱ h (UnallocatedAddress a p) = UnallocatedAddress a (lookup-⊑-nothing a h p) +reflect-weakeningᴱ h (app₀ p) with heap-weakeningᴱ h | heap-weakeningᴱ h +reflect-weakeningᴱ h (app₀ p) | ok q₁ | ok q₂ = app₀ (λ r → p (trans (cong src (sym q₁)) (trans r q₂))) +reflect-weakeningᴱ h (app₀ p) | warning W | _ = app₁ W +reflect-weakeningᴱ h (app₀ p) | _ | warning W = app₂ W +reflect-weakeningᴱ h (app₁ W) = app₁ (reflect-weakeningᴱ h W) +reflect-weakeningᴱ h (app₂ W) = app₂ (reflect-weakeningᴱ h W) +reflect-weakeningᴱ h (function₀ f p) with heap-weakeningᴮ h +reflect-weakeningᴱ h (function₀ f p) | ok q = function₀ f (λ r → p (trans r q)) +reflect-weakeningᴱ h (function₀ f p) | warning W = function₁ f W +reflect-weakeningᴱ h (function₁ f W) = function₁ f (reflect-weakeningᴮ h W) +reflect-weakeningᴱ h (block b W) = block b (reflect-weakeningᴮ h W) + +reflect-weakeningᴮ h (return W) = return (reflect-weakeningᴱ h W) +reflect-weakeningᴮ h (local₀ p) with heap-weakeningᴱ h +reflect-weakeningᴮ h (local₀ p) | ok q = local₀ (λ r → p (trans r q)) +reflect-weakeningᴮ h (local₀ p) | warning W = local₁ W +reflect-weakeningᴮ h (local₁ W) = local₁ (reflect-weakeningᴱ h W) +reflect-weakeningᴮ h (local₂ W) = local₂ (reflect-weakeningᴮ h W) +reflect-weakeningᴮ h (function₁ f W) = function₁ f (reflect-weakeningᴮ h W) +reflect-weakeningᴮ h (function₂ f W) = function₂ f (reflect-weakeningᴮ h W) + +reflectᴱ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴱ H (typeCheckᴱ H ∅ M) +reflectᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴮ H (typeCheckᴮ H ∅ B) + +reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (BadlyTypedFunctionAddress a f refl W) = function₁ f (reflect-weakeningᴮ (snoc refl defn) W) +reflectᴱ (app s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (redn-⊑ s) +reflectᴱ (app s) (app₀ p) | ok q | ok q′ = app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′)) +reflectᴱ (app s) (app₀ p) | warning W | _ = app₁ W +reflectᴱ (app s) (app₀ p) | _ | warning W = app₂ W +reflectᴱ (app s) (app₁ W) = app₁ (reflectᴱ s W) +reflectᴱ (app s) (app₂ W) = app₂ (reflect-weakeningᴱ (redn-⊑ s) W) +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₀ p)) = app₀ (λ r → p (trans (sym (cong src (cong declaredTypeᴴ q))) r)) +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₁ W)) = app₂ W +reflectᴱ (beta {a = a} {F = f ⟨ var x ∈ T ⟩∈ U} q) (block f (local₂ {T = T′} W)) = app₁ (BadlyTypedFunctionAddress a f q W) +reflectᴱ (block s) (block b W) = block b (reflectᴮ s W) +reflectᴱ (return q) W = block _ (return W) + +reflectᴮ (local s) (local₀ p) with preservationᴱ s +reflectᴮ (local s) (local₀ p) | ok q = local₀ (λ r → p (trans r q)) +reflectᴮ (local s) (local₀ p) | warning W = local₁ W +reflectᴮ (local s) (local₁ W) = local₁ (reflectᴱ s W) +reflectᴮ (local s) (local₂ W) = local₂ (reflect-weakeningᴮ (redn-⊑ s) W) +reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with T ≡ᵀ (typeOfᴱ H ∅ (val v)) +reflectᴮ (subst {x = var x ∈ T} {v = v}) W | yes refl = local₂ (reflect-substitutionᴮ _ v x (typeOfᴱⱽ v) refl W) +reflectᴮ (subst {x = var x ∈ T} {v = v}) W | no p = local₀ p +reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = function₂ f (reflect-weakeningᴮ (snoc refl defn) (reflect-substitutionᴮ _ _ f refl refl W)) +reflectᴮ (return s) (return W) = return (reflectᴱ s W) -- reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (bot ()) -- reflectᴱ (function defn) (addr a T q) = CONTRADICTION (q refl) @@ -168,12 +254,6 @@ reflectᴮ s = {!!} -- progressᴮ H h (function D₁ D₂) q with alloc H _ -- progressᴮ H h (function D₁ D₂) q | ok a H′ r = step (function r) -import FFI.Data.Aeson -{-# REWRITE FFI.Data.Aeson.singleton-insert-empty #-} - -_≡ᵀ_ : (T U : Type) → Dec (T ≡ U) -_≡ᵀ_ = {!!} - -- data LookupResult {Σ V S} (D : Σ ▷ V ∈ S) : Set where -- function : ∀ f {x B T U W} → diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 98495f25..1ba1c0e7 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Luau.Type using (Mode) module Properties.TypeCheck (m : Mode) where @@ -5,13 +7,14 @@ module Properties.TypeCheck (m : Mode) where open import Agda.Builtin.Equality using (_≡_; refl) 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; app; function; block; done; return; local) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; nil; var; addr; app; function; block; done; return; local) open import Luau.Syntax using (Block; Expr; yes; nil; var; addr; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg) open import Luau.Type using (Type; nil; top; bot; _⇒_; tgt) -open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_; ⊕-[]) renaming (_[_] to _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ) open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) +open import Luau.Value using (Value; nil; addr; val) open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) open import Properties.Dec using (yes; no) open import Properties.Equality using (_≢_; sym; trans; cong) @@ -20,16 +23,20 @@ open import Properties.Remember using (remember; _,_) src : Type → Type src = Luau.Type.src m -typeOfᴴ : Maybe(HeapValue yes) → Type -typeOfᴴ nothing = bot -typeOfᴴ (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) +declaredTypeᴴ : Maybe(HeapValue yes) → Type +declaredTypeᴴ nothing = bot +declaredTypeᴴ (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) + +typeOfⱽ : Heap yes → Value → Type +typeOfⱽ H nil = nil +typeOfⱽ H (addr a) = declaredTypeᴴ (H [ a ]ᴴ) typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type typeOfᴱ H Γ nil = nil typeOfᴱ H Γ (var x) = Γ [ x ]ⱽ -typeOfᴱ H Γ (addr a) = typeOfᴴ (H [ a ]ᴴ) +typeOfᴱ H Γ (addr a) = declaredTypeᴴ (H [ a ]ᴴ) typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M) typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T typeOfᴱ H Γ (block b is B end) = typeOfᴮ H Γ B @@ -39,32 +46,25 @@ typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M typeOfᴮ H Γ done = nil -contextOfᴱ : Heap yes → VarCtxt → Type → (Expr yes) → VarCtxt -contextOfᴮ : Heap yes → VarCtxt → Type → (Block yes) → VarCtxt +typeOfᴴ : Heap yes → Maybe(HeapValue yes) → Type +typeOfᴴ H nothing = bot +typeOfᴴ H (just function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ typeOfᴮ H (x ↦ S) B) -contextOfᴱ H Γ S nil = ∅ -contextOfᴱ H Γ S (var x) = (x ↦ S) -contextOfᴱ H Γ S (addr a) = ∅ -contextOfᴱ H Γ S (M $ N) = (contextOfᴱ H Γ (U ⇒ S) M) ⋒ (contextOfᴱ H Γ (src T) N) where T = typeOfᴱ H Γ M; U = typeOfᴱ H Γ N -contextOfᴱ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = (contextOfᴮ H (Γ ⊕ x ↦ T) U B) ⊝ x -contextOfᴱ H Γ S (block b is B end) = (contextOfᴮ H Γ S B) +typeOfᴱⱽ : ∀ {H Γ} v → (typeOfᴱ H Γ (val v) ≡ typeOfⱽ H v) +typeOfᴱⱽ nil = refl +typeOfᴱⱽ (addr a) = refl -contextOfᴮ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = ((contextOfᴮ H (Γ ⊕ x ↦ T) U C) ⊝ x) ⋒ ((contextOfᴮ H (Γ ⊕ f ↦ (T ⇒ U)) S B) ⊝ f) -contextOfᴮ H Γ S (local var x ∈ T ← M ∙ B) = (contextOfᴱ H Γ T M) ⋒ ((contextOfᴮ H (Γ ⊕ x ↦ T)S B) ⊝ x) -contextOfᴮ H Γ S (return M ∙ B) = (contextOfᴱ H Γ S M) -contextOfᴮ H Γ S done = ∅ +typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M)) +typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) -typeCheckᴱ : ∀ H Γ S M → (Γ ⊢ᴱ S ∋ M ∈ (typeOfᴱ H Γ M) ⊣ (contextOfᴱ H Γ S M)) -typeCheckᴮ : ∀ H Γ S B → (Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ H Γ B) ⊣ (contextOfᴮ H Γ S B)) +typeCheckᴱ H Γ nil = nil +typeCheckᴱ H Γ (var x) = var x refl +typeCheckᴱ H Γ (addr a) = addr a (declaredTypeᴴ (H [ a ]ᴴ)) +typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N) +typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function f (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +typeCheckᴱ H Γ (block b is B end) = block b (typeCheckᴮ H Γ B) -typeCheckᴱ H Γ S nil = nil -typeCheckᴱ H Γ S (var x) = var x refl -typeCheckᴱ H Γ S (addr a) = addr a (typeOfᴴ (H [ a ]ᴴ)) -typeCheckᴱ H Γ S (M $ N) = app (typeCheckᴱ H Γ (typeOfᴱ H Γ N ⇒ S) M) (typeCheckᴱ H Γ (src (typeOfᴱ H Γ M)) N) -typeCheckᴱ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = function(typeCheckᴮ H (Γ ⊕ x ↦ T) U B) -typeCheckᴱ H Γ S (block b is B end) = block b (typeCheckᴮ H Γ S B) - -typeCheckᴮ H Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function(typeCheckᴮ H (Γ ⊕ x ↦ T) U C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) S B) -typeCheckᴮ H Γ S (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ T M) (typeCheckᴮ H (Γ ⊕ x ↦ T) S B) -typeCheckᴮ H Γ S (return M ∙ B) = return (typeCheckᴱ H Γ S M) (typeCheckᴮ H Γ nil B) -typeCheckᴮ H Γ S done = done +typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function f (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B) +typeCheckᴮ H Γ (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +typeCheckᴮ H Γ (return M ∙ B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B) +typeCheckᴮ H Γ done = done