From ef92fd8586c2aa045843284a2c87b71e7daa2ebc Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 22 Feb 2022 17:50:33 -0600 Subject: [PATCH] Finished strict mode subjsect reduction --- prototyping/Examples/OpSem.agda | 2 + prototyping/Examples/Run.agda | 2 - prototyping/FFI/Data/Aeson.agda | 2 + prototyping/FFI/Data/Maybe.agda | 6 ++ prototyping/FFI/Data/Vector.agda | 3 +- prototyping/Luau/Heap.agda | 10 +- prototyping/Luau/Type.agda | 76 ++++++++++++++- prototyping/Luau/VarCtxt.agda | 8 +- prototyping/Properties/StrictMode.agda | 127 ++++++++++++++----------- prototyping/Properties/TypeCheck.agda | 2 +- 10 files changed, 174 insertions(+), 64 deletions(-) diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index ec8bce7b..68ced07f 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Examples.OpSem where open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst) diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 88ca39b6..42215633 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -6,10 +6,8 @@ open import Agda.Builtin.Equality using (_≡_; refl) open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩) open import Luau.Value using (nil) open import Luau.Run using (run; return) -open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp) import Agda.Builtin.Equality.Rewrite -{-# REWRITE lookup-next next-emp lookup-next-emp #-} ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _) ex1 = refl diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index b9ab5954..0cd27232 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -47,6 +47,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 lookup-insert-not : ∀ {A} j k v (m : KeyMap A) → (j ≢ k) → (lookup k m ≡ lookup k (insert j v m)) postulate singleton-insert-empty : ∀ {A} k (v : A) → (singleton k v ≡ insert k v empty) +postulate insert-swap : ∀ {A} j k (v w : A) m → (j ≢ k) → insert j v (insert k w m) ≡ insert k w (insert j v m) +postulate insert-over : ∀ {A} j k (v w : A) m → (j ≡ k) → insert j v (insert k w m) ≡ insert j v m postulate to-from : ∀ k → toString(fromString k) ≡ k postulate from-to : ∀ k → fromString(toString k) ≡ k diff --git a/prototyping/FFI/Data/Maybe.agda b/prototyping/FFI/Data/Maybe.agda index b16fa810..58fd1486 100644 --- a/prototyping/FFI/Data/Maybe.agda +++ b/prototyping/FFI/Data/Maybe.agda @@ -1,8 +1,14 @@ module FFI.Data.Maybe where +open import Agda.Builtin.Equality using (_≡_; refl) + {-# FOREIGN GHC import qualified Data.Maybe #-} data Maybe (A : Set) : Set where nothing : Maybe A just : A → Maybe A {-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-} + +just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y) +just-inv refl = refl + diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 9d3e418f..30a51d69 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -36,10 +36,11 @@ postulate postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0) postulate lookup-empty : ∀ {A} n → (lookup (empty {A}) n ≡ nothing) postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x) +postulate lookup-length : ∀ {A} (v : Vector A) → (lookup v (length v) ≡ nothing) postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x) postulate lookup-snoc-not : ∀ {A n} (x : A) (v : Vector A) → (n ≢ length v) → (lookup v n ≡ lookup (snoc v x) n) -{-# REWRITE length-empty lookup-snoc lookup-snoc-empty lookup-empty #-} +{-# REWRITE length-empty lookup-snoc lookup-length lookup-snoc-empty lookup-empty #-} head : ∀ {A} → (Vector A) → (Maybe A) head vec with null vec diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index 3c31c95b..b0340160 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -2,13 +2,15 @@ module Luau.Heap where -open import Agda.Builtin.Equality using (_≡_) -open import FFI.Data.Maybe using (Maybe; just) +open import Agda.Builtin.Equality using (_≡_; refl) +open import FFI.Data.Maybe using (Maybe; just; nothing) open import FFI.Data.Vector using (Vector; length; snoc; empty; lookup-snoc-not) -open import Luau.Addr using (Addr) +open import Luau.Addr using (Addr; _≡ᴬ_) open import Luau.Var using (Var) open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end) -open import Properties.Equality using (_≢_) +open import Properties.Equality using (_≢_; trans) +open import Properties.Remember using (remember; _,_) +open import Properties.Dec using (yes; no) -- Heap-allocated objects data Object (a : Annotated) : Set where diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 8b12085a..49562ad6 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -1,6 +1,9 @@ module Luau.Type where -open import FFI.Data.Maybe using (Maybe; just; nothing) +open import FFI.Data.Maybe using (Maybe; just; nothing; just-inv) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Equality using (cong) data Type : Set where nil : Type @@ -10,6 +13,77 @@ data Type : Set where _∪_ : Type → Type → Type _∩_ : Type → Type → Type +lhs : Type → Type +lhs (T ⇒ _) = T +lhs (T ∪ _) = T +lhs (T ∩ _) = T +lhs nil = nil +lhs bot = bot +lhs top = top + +rhs : Type → Type +rhs (_ ⇒ T) = T +rhs (_ ∪ T) = T +rhs (_ ∩ T) = T +rhs nil = nil +rhs bot = bot +rhs top = top + +_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) +nil ≡ᵀ nil = yes refl +nil ≡ᵀ (S ⇒ T) = no (λ ()) +nil ≡ᵀ bot = no (λ ()) +nil ≡ᵀ top = no (λ ()) +nil ≡ᵀ (S ∪ T) = no (λ ()) +nil ≡ᵀ (S ∩ T) = no (λ ()) +(S ⇒ T) ≡ᵀ nil = no (λ ()) +(S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V) +(S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl +(S ⇒ T) ≡ᵀ (U ⇒ V) | _ | no p = no (λ q → p (cong rhs q)) +(S ⇒ T) ≡ᵀ (U ⇒ V) | no p | _ = no (λ q → p (cong lhs q)) +(S ⇒ T) ≡ᵀ bot = no (λ ()) +(S ⇒ T) ≡ᵀ top = no (λ ()) +(S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ()) +(S ⇒ T) ≡ᵀ (U ∩ V) = no (λ ()) +bot ≡ᵀ nil = no (λ ()) +bot ≡ᵀ (U ⇒ V) = no (λ ()) +bot ≡ᵀ bot = yes refl +bot ≡ᵀ top = no (λ ()) +bot ≡ᵀ (U ∪ V) = no (λ ()) +bot ≡ᵀ (U ∩ V) = no (λ ()) +top ≡ᵀ nil = no (λ ()) +top ≡ᵀ (U ⇒ V) = no (λ ()) +top ≡ᵀ bot = no (λ ()) +top ≡ᵀ top = yes refl +top ≡ᵀ (U ∪ V) = no (λ ()) +top ≡ᵀ (U ∩ V) = no (λ ()) +(S ∪ T) ≡ᵀ nil = no (λ ()) +(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ()) +(S ∪ T) ≡ᵀ bot = no (λ ()) +(S ∪ T) ≡ᵀ top = no (λ ()) +(S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V) +(S ∪ T) ≡ᵀ (S ∪ T) | yes refl | yes refl = yes refl +(S ∪ T) ≡ᵀ (U ∪ V) | _ | no p = no (λ q → p (cong rhs q)) +(S ∪ T) ≡ᵀ (U ∪ V) | no p | _ = no (λ q → p (cong lhs q)) +(S ∪ T) ≡ᵀ (U ∩ V) = no (λ ()) +(S ∩ T) ≡ᵀ nil = no (λ ()) +(S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ()) +(S ∩ T) ≡ᵀ bot = no (λ ()) +(S ∩ T) ≡ᵀ top = no (λ ()) +(S ∩ T) ≡ᵀ (U ∪ V) = no (λ ()) +(S ∩ T) ≡ᵀ (U ∩ V) with (S ≡ᵀ U) | (T ≡ᵀ V) +(S ∩ T) ≡ᵀ (U ∩ V) | yes refl | yes refl = yes refl +(S ∩ T) ≡ᵀ (U ∩ V) | _ | no p = no (λ q → p (cong rhs q)) +(S ∩ T) ≡ᵀ (U ∩ V) | no p | _ = no (λ q → p (cong lhs q)) + +_≡ᴹᵀ_ : ∀ (T U : Maybe Type) → Dec(T ≡ U) +nothing ≡ᴹᵀ nothing = yes refl +nothing ≡ᴹᵀ just U = no (λ ()) +just T ≡ᴹᵀ nothing = no (λ ()) +just T ≡ᴹᵀ just U with T ≡ᵀ U +(just T ≡ᴹᵀ just T) | yes refl = yes refl +(just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q)) + data Mode : Set where strict : Mode nonstrict : Mode diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index b19beed3..b05cdd7b 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -5,7 +5,7 @@ module Luau.VarCtxt where open import Agda.Builtin.Equality using (_≡_) open import Luau.Type using (Type; bot; _∪_; _∩_) open import Luau.Var using (Var) -open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from) +open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from; insert-swap; insert-over) open import FFI.Data.Maybe using (Maybe; just; nothing) open import Properties.Equality using (_≢_; cong; sym; trans) @@ -33,5 +33,11 @@ x ↦ T = singleton (fromString x) T _⊕_↦_ : VarCtxt → Var → Type → VarCtxt Γ ⊕ x ↦ T = insert (fromString x) T Γ +⊕-over : ∀ {Γ x y T U} → (x ≡ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ (Γ ⊕ y ↦ U) +⊕-over p = insert-over _ _ _ _ _ (cong fromString (sym p)) + +⊕-swap : ∀ {Γ x y T U} → (x ≢ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ ((Γ ⊕ y ↦ U) ⊕ x ↦ T) +⊕-swap p = insert-swap _ _ _ _ _ (λ q → p (trans (sym (to-from _)) (trans (cong toString (sym q) ) (to-from _))) ) + ⊕-lookup-miss : ∀ x y T Γ → (x ≢ y) → (Γ [ y ] ≡ (Γ ⊕ x ↦ T) [ y ]) ⊕-lookup-miss x y T Γ p = lookup-insert-not (fromString x) (fromString y) T Γ λ q → p (trans (sym (to-from x)) (trans (cong toString q) (to-from y))) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 32ea491a..9c56b631 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -9,12 +9,12 @@ open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; nex open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; block; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; addr) 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.Type using (Type; strict; nil; _⇒_; bot; tgt; _≡ᵀ_; _≡ᴹᵀ_) open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orBot) open import Luau.Value using (val; nil; addr) open import Luau.Var using (_≡ⱽ_) open import Luau.Addr using (_≡ᴬ_) -open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss) renaming (_[_] to _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ) open import Luau.VarCtxt using (VarCtxt; ∅) open import Properties.Remember using (remember; _,_) open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) @@ -26,28 +26,35 @@ open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotA src = Luau.Type.src strict -_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U) -_≡ᵀ_ = {!!} - -_≡ᴹᵀ_ : ∀ (T U : Maybe 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″) + snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′) -warning-⊑ : ∀ {H H′ Γ T M} {D : Γ ⊢ᴱ M ∈ T} → (H ⊑ H′) → (Warningᴱ H′ D) → Warningᴱ H D -warning-⊑ = {!!} +rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′) +rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′) + +rednᴱ⊑ (function p) = snoc p +rednᴱ⊑ (app₁ s) = rednᴱ⊑ s +rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s +rednᴱ⊑ (beta p q) = refl +rednᴱ⊑ (block s) = rednᴮ⊑ s +rednᴱ⊑ (return p) = refl +rednᴱ⊑ done = refl + +rednᴮ⊑ (local s) = rednᴱ⊑ s +rednᴮ⊑ subst = refl +rednᴮ⊑ (function p) = snoc p +rednᴮ⊑ (return s) = rednᴱ⊑ s 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 -lookup-⊑-just : ∀ {H H′ V} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ just V) → LookupResult H a V -lookup-⊑-just = {!!} - lookup-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ nothing) -lookup-⊑-nothing = {!!} +lookup-⊑-nothing {H} a refl p = p +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 @@ -65,29 +72,41 @@ 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 -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 = {!!} - -⊕-lookup : ∀ {Γ x y T} → (x ≢ y) → ((Γ ⊕ x ↦ T) [ y ]ⱽ) ≡ (Γ [ y ]ⱽ) -⊕-lookup = {!!} - 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) -heap-weakeningᴱ = {!!} -heap-weakeningᴮ = {!!} +heap-weakeningᴱ {M = nil} h = ok refl +heap-weakeningᴱ {M = var x} h = ok refl +heap-weakeningᴱ {M = addr a} refl = ok refl +heap-weakeningᴱ {M = addr a} (snoc {a = b} defn) with a ≡ᴬ b +heap-weakeningᴱ {M = addr a} (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress a refl) +heap-weakeningᴱ {M = addr a} (snoc {a = b} p) | no q = ok (cong orBot (cong typeOfᴹᴼ (lookup-not-allocated p q))) +heap-weakeningᴱ {M = M $ N} h with heap-weakeningᴱ h +heap-weakeningᴱ {M = M $ N} h | ok p = ok (cong tgt p) +heap-weakeningᴱ {M = M $ N} h | warning W = warning (app₁ W) +heap-weakeningᴱ {M = function f ⟨ var x ∈ T ⟩∈ U is B end} h = ok refl +heap-weakeningᴱ {M = block b is B end} h with heap-weakeningᴮ h +heap-weakeningᴱ {M = block b is B end} h | ok p = ok p +heap-weakeningᴱ {M = block b is B end} h | warning W = warning (block b W) +heap-weakeningᴮ {B = function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B} h with heap-weakeningᴮ h +heap-weakeningᴮ {B = function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B} h | ok p = ok p +heap-weakeningᴮ {B = function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B} h | warning W = warning (function₂ f W) +heap-weakeningᴮ {B = local var x ∈ T ← M ∙ B} h with heap-weakeningᴮ h +heap-weakeningᴮ {B = local var x ∈ T ← M ∙ B} h | ok p = ok p +heap-weakeningᴮ {B = local var x ∈ T ← M ∙ B} h | warning W = warning (local₂ W) +heap-weakeningᴮ {B = return M ∙ B} h with heap-weakeningᴱ h +heap-weakeningᴮ {B = return M ∙ B} h | ok p = ok p +heap-weakeningᴮ {B = return M ∙ B} h | warning W = warning (return W) +heap-weakeningᴮ {B = done} h = ok refl bot-not-obj : ∀ O → bot ≢ typeOfᴼ O bot-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () typeOf-val-not-bot : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (bot ≢ typeOfᴱ H Γ (val v)) -typeOf-val-not-bot = {!!} +typeOf-val-not-bot nil = ok (λ ()) +typeOf-val-not-bot {H = H} (addr a) with remember (H [ a ]ᴴ) +typeOf-val-not-bot {H = H} (addr a) | (just O , p) = ok (λ q → bot-not-obj O (trans q (cong orBot (cong typeOfᴹᴼ p)))) +typeOf-val-not-bot {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress a 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))) @@ -107,10 +126,10 @@ substitutivityᴱ (block b is B end) v x p = substitutivityᴮ B v x p substitutivityᴱ-whenever-yes v x x refl q = trans (cong orBot q) (sym (typeOfᴱⱽ v)) substitutivityᴱ-whenever-no v x y p q = cong orBot ( sym (⊕-lookup-miss x y _ _ p)) substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f -substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x f q p (⊕-overwrite q) +substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x f q p (⊕-over q) substitutivityᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no B v x f q p (⊕-swap q) substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y -substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x y q p (⊕-overwrite q) +substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes B v x y q p (⊕-over q) substitutivityᴮ (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no B v x y q p (⊕-swap q) substitutivityᴮ (return M ∙ B) v x p = substitutivityᴱ M v x p substitutivityᴮ done v x p = refl @@ -125,7 +144,7 @@ preservationᴱ (app₁ s) with preservationᴱ s preservationᴱ (app₁ s) | ok p = ok (cong tgt p) preservationᴱ (app₁ s) | warning (expr W) = warning (expr (app₁ W)) preservationᴱ (app₁ s) | warning (heap W) = warning (heap W) -preservationᴱ (app₂ p s) with heap-weakeningᴱ (redn-⊑ s) +preservationᴱ (app₂ p s) with heap-weakeningᴱ (rednᴱ⊑ s) preservationᴱ (app₂ p s) | ok q = ok (cong tgt q) preservationᴱ (app₂ p s) | warning W = warning (expr (app₁ W)) preservationᴱ {H = H} (beta {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} {V = V} p refl) with remember (typeOfⱽ H V) @@ -143,7 +162,7 @@ preservationᴱ (block {b = b} s) | warning (heap W) = warning (heap W) preservationᴱ (return p) = ok refl preservationᴱ done = ok refl -preservationᴮ (local {x = var x ∈ T} s) with heap-weakeningᴮ (redn-⊑ s) +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 (block (local₂ W)) preservationᴮ {H = H} (subst {v = v}) with remember (typeOfⱽ H v) @@ -153,7 +172,7 @@ preservationᴮ (subst {x = var x ∈ T} {v = v} {B = B}) | (just U , p) | no q preservationᴮ (subst {x = var x ∈ T} {v = v}) | (nothing , p) with typeOf-val-not-bot v preservationᴮ (subst {x = var x ∈ T} {v = v}) | (nothing , p) | ok q = CONTRADICTION (q (sym (trans (typeOfᴱⱽ v) (cong orBot p)))) preservationᴮ (subst {x = var x ∈ T} {v = v}) | (nothing , p) | warning W = warning (block (local₁ W)) -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) with heap-weakeningᴮ (snoc defn) preservationᴮ (function {a = a} {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | ok r = ok (trans r (substitutivityᴮ {T = S ⇒ T} B (addr a) f refl)) preservationᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} {B = B} defn) | warning W = warning (block (function₂ f W)) preservationᴮ (return s) with preservationᴱ s @@ -176,30 +195,30 @@ reflect-substitutionᴱ (M $ N) v x p (app₀ q) = app₀ (λ s → q (trans (co reflect-substitutionᴱ (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ M v x p W) reflect-substitutionᴱ (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ N v x p W) reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) with (x ≡ⱽ y) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes B v x y r p (⊕-overwrite r)))) +reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes B v x y r p (⊕-over r)))) reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₀ f q) | no r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-no B v x y r p (⊕-swap r)))) reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ f W) with (x ≡ⱽ y) -reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (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 (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-over r) W) reflect-substitutionᴱ (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ-unless-no B v x y r p (⊕-swap r) W) reflect-substitutionᴱ (block b is B end) v x p (block b W) = block b (reflect-substitutionᴮ B v x p W) -reflect-substitutionᴱ-whenever-no v x y p q (UnboundVariable y r) = UnboundVariable y (trans (⊕-lookup p) r) +reflect-substitutionᴱ-whenever-no v x y p q (UnboundVariable y r) = UnboundVariable y (trans (sym (⊕-lookup-miss x y _ _ p)) r) reflect-substitutionᴱ-whenever-yes (addr a) x x refl p (UnallocatedAddress a q) with trans p (cong typeOfᴹᴼ q) reflect-substitutionᴱ-whenever-yes (addr a) x x refl p (UnallocatedAddress a q) | () reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) with (x ≡ⱽ y) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes C v x y r p (⊕-overwrite r)))) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) | yes r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-yes C v x y r p (⊕-over r)))) reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₀ f q) | no r = function₀ f (λ s → q (trans s (substitutivityᴮ-unless-no C v x y r p (⊕-swap r)))) reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) with (x ≡ⱽ y) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes C v x y r p (⊕-overwrite r) W) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) | yes r = function₁ f (reflect-substitutionᴮ-unless-yes C v x y r p (⊕-over r) W) reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ f W) | no r = function₁ f (reflect-substitutionᴮ-unless-no C v x y r p (⊕-swap r) W) reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W) with (x ≡ⱽ f) -reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W)| yes r = function₂ f (reflect-substitutionᴮ-unless-yes B v x f r p (⊕-overwrite r) W) +reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W)| yes r = function₂ f (reflect-substitutionᴮ-unless-yes B v x f r p (⊕-over r) W) reflect-substitutionᴮ (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ f W)| no r = function₂ f (reflect-substitutionᴮ-unless-no B v x f r p (⊕-swap r) W) reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₀ q) = local₀ (λ r → q (trans r (substitutivityᴱ M v x p))) reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ M v x p W) reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y) -reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-overwrite r) W) +reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes B v x y r p (⊕-over r) W) reflect-substitutionᴮ (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no B v x y r p (⊕-swap r) W) reflect-substitutionᴮ (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ M v x p W) @@ -244,7 +263,7 @@ reflect-weakeningᴼ h (function₁ f W′) = function₁ f (reflect-weakening 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ᴱ (app₁ s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (redn-⊑ s) +reflectᴱ (app₁ s) (app₀ p) with preservationᴱ s | heap-weakeningᴱ (rednᴱ⊑ s) reflectᴱ (app₁ s) (app₀ p) | ok q | ok q′ = expr (app₀ (λ r → p (trans (trans (cong src (sym q)) r) q′))) reflectᴱ (app₁ s) (app₀ p) | warning (expr W) | _ = expr (app₁ W) reflectᴱ (app₁ s) (app₀ p) | warning (heap W) | _ = heap W @@ -252,13 +271,13 @@ reflectᴱ (app₁ s) (app₀ p) | _ | warning W = expr (app₂ W) reflectᴱ (app₁ s) (app₁ W′) with reflectᴱ s W′ reflectᴱ (app₁ s) (app₁ W′) | heap W = heap W reflectᴱ (app₁ s) (app₁ W′) | expr W = expr (app₁ W) -reflectᴱ (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (redn-⊑ s) W′)) -reflectᴱ (app₂ p s) (app₀ p′) with heap-weakeningᴱ (redn-⊑ s) | preservationᴱ s +reflectᴱ (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ (rednᴱ⊑ s) W′)) +reflectᴱ (app₂ p s) (app₀ p′) with heap-weakeningᴱ (rednᴱ⊑ s) | preservationᴱ s reflectᴱ (app₂ p s) (app₀ p′) | ok q | ok q′ = expr (app₀ (λ r → p′ (trans (trans (cong src (sym q)) r) q′))) reflectᴱ (app₂ p s) (app₀ p′) | warning W | _ = expr (app₁ W) reflectᴱ (app₂ p s) (app₀ p′) | _ | warning (expr W) = expr (app₂ W) reflectᴱ (app₂ p s) (app₀ p′) | _ | warning (heap W) = heap W -reflectᴱ (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ (redn-⊑ s) W′)) +reflectᴱ (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ (rednᴱ⊑ s) W′)) reflectᴱ (app₂ p s) (app₂ W′) with reflectᴱ s W′ reflectᴱ (app₂ p s) (app₂ W′) | heap W = heap W reflectᴱ (app₂ p s) (app₂ W′) | expr W = expr (app₂ W) @@ -282,14 +301,14 @@ reflectᴮ (local s) (local₀ p) | warning (heap W) = heap W reflectᴮ (local s) (local₁ W′) with reflectᴱ s W′ reflectᴮ (local s) (local₁ W′) | heap W = heap W reflectᴮ (local s) (local₁ W′) | expr W = block (local₁ W) -reflectᴮ (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ (redn-⊑ s) W′)) +reflectᴮ (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ (rednᴱ⊑ s) W′)) reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W with just T ≡ᴹᵀ typeOfⱽ H v reflectᴮ (subst {H = H} {x = var x ∈ T} {v = v}) W | yes p = block (local₂ (reflect-substitutionᴮ _ v x p W)) reflectᴮ (subst {H = H} {x = var x ∈ T} {v = nil}) W | no p = block (local₀ λ r → p (cong just r)) reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p with remember(H [ a ]ᴴ) reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p | (nothing , q) = block (local₁ (UnallocatedAddress a q)) reflectᴮ (subst {H = H} {x = var x ∈ T} {v = addr a}) W | no p | (just O , q) = block (local₀ (λ r → p (trans (cong just (trans r (cong orBot (cong typeOfᴹᴼ q)))) (cong typeOfᴹᴼ (sym q))))) -reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = block (function₂ f (reflect-weakeningᴮ (snoc refl defn) (reflect-substitutionᴮ _ _ f refl W))) +reflectᴮ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) W = block (function₂ f (reflect-weakeningᴮ (snoc defn) (reflect-substitutionᴮ _ _ f refl W))) reflectᴮ (return s) (return W′) with reflectᴱ s W′ reflectᴮ (return s) (return W′) | heap W = heap W reflectᴮ (return s) (return W′) | expr W = block (return W) @@ -299,11 +318,11 @@ reflectᴴᴮ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warni reflectᴴᴱ s (expr W′) = reflectᴱ s W′ reflectᴴᴱ (function {a = a} p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc refl defn) +reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc defn) reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = expr (function₀ f λ q → p (trans q r)) reflectᴴᴱ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = expr (function₁ f W) -reflectᴴᴱ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = expr (function₁ f (reflect-weakeningᴮ (snoc refl defn) W′)) -reflectᴴᴱ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc refl p) W′)) +reflectᴴᴱ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = expr (function₁ f (reflect-weakeningᴮ (snoc defn) W′)) +reflectᴴᴱ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc p) W′)) reflectᴴᴱ (app₁ s) (heap W′) with reflectᴴᴱ s (heap W′) reflectᴴᴱ (app₁ s) (heap W′) | heap W = heap W reflectᴴᴱ (app₁ s) (heap W′) | expr W = expr (app₁ W) @@ -323,11 +342,11 @@ reflectᴴᴮ (local {x = var x ∈ T} s) (heap W′) | heap W = heap W reflectᴴᴮ (local {x = var x ∈ T} s) (heap W′) | expr W = block (local₁ W) reflectᴴᴮ (subst) (heap W′) = heap W′ reflectᴴᴮ (function {a = a} p) (heap (addr b refl W′)) with b ≡ᴬ a -reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc refl defn) +reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl with heap-weakeningᴮ (snoc defn) reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | ok r = block (function₀ f (λ q → p (trans q r))) reflectᴴᴮ (function defn) (heap (addr a refl (function₀ f p))) | yes refl | warning W = block (function₁ f W) -reflectᴴᴮ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = block (function₁ f (reflect-weakeningᴮ (snoc refl defn) W′)) -reflectᴴᴮ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc refl p) W′)) +reflectᴴᴮ (function defn) (heap (addr a refl (function₁ f W′))) | yes refl = block (function₁ f (reflect-weakeningᴮ (snoc defn) W′)) +reflectᴴᴮ (function p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ (snoc p) W′)) reflectᴴᴮ (return s) (heap W′) with reflectᴴᴱ s (heap W′) reflectᴴᴮ (return s) (heap W′) | heap W = heap W reflectᴴᴮ (return s) (heap W′) | expr W = block (return W) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 7ffdf3ac..ec1203ae 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -7,7 +7,7 @@ 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; unbound; addr; app; function; block; done; return; local; nothing; orBot) +open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; app; function; block; done; return; local; nothing; orBot) 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 _[_]ⱽ)