From 3f2ca3d4ad3796da02754605b05f90a9fe54afdf Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Mon, 14 Feb 2022 18:43:46 -0600 Subject: [PATCH] Working on strict mode --- prototyping/Luau/OpSem.agda | 14 +++----- prototyping/Luau/StrictMode.agda | 6 ++++ prototyping/Properties/Step.agda | 2 +- prototyping/Properties/StrictMode.agda | 10 +++--- prototyping/Properties/TypeCheck.agda | 50 +++++++++++++------------- 5 files changed, 42 insertions(+), 40 deletions(-) diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index 878b8bd0..2bc9be13 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -12,11 +12,6 @@ data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set data _⊢_⟶ᴱ_⊣_ where - nil : ∀ {H} → - - ------------------- - H ⊢ nil ⟶ᴱ nil ⊣ H - function : ∀ {H H′ a F B} → H′ ≡ H ⊕ a ↦ (function F is B end) → @@ -41,10 +36,11 @@ data _⊢_⟶ᴱ_⊣_ where ---------------------------------------------------- H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′ - return : ∀ {H V B b} → - - -------------------------------------------------------- - H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H + return : ∀ {H M V B b} → + + M ≡ val V → + -------------------------------------------- + H ⊢ (block b is return M ∙ B end) ⟶ᴱ M ⊣ H done : ∀ {H b} → diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 5b1ef4cf..bfd0c998 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -27,6 +27,12 @@ data Warningᴱ {Σ Γ S} where ----------------- Warningᴱ(app D₁ D₂) + app₂ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + + Warningᴱ D₂ → + ----------------- + Warningᴱ(app D₁ D₂) + block : ∀ b {B T Δ} {D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → Warningᴮ D → diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index eeda4ef2..f4a7aad6 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -39,7 +39,7 @@ stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = stepᴱ H (M $ N) | error E = error (app E) stepᴱ H (block b is B end) with stepᴮ H B stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D) -stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return +stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) (return refl) stepᴱ H (block b is done end) | done refl = step H nil done stepᴱ H (block b is B end) | error E = error (block b E) stepᴱ H (function F is C end) with alloc H (function F is C end) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index fd115f56..f84b739f 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -5,15 +5,17 @@ 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; alloc; ok) renaming (_[_] to _[_]ᴴ) -open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; app₁; block; return; local₁) -open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; block_is_end; done; return; local_←_; _∙_; fun; arg) +open import Luau.Heap using (Heap; HeapValue; function_is_end; defn; alloc; ok; next; lookup-next) renaming (_[_] to _[_]ᴴ) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; app₁; app₂; block; return; local₁) +open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; nil; 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; nothing) open import Luau.Value using (val; nil; addr) +open import Luau.AddrCtxt using (AddrCtxt) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ∅-[]) renaming (_[_] to _[_]ⱽ) open import Properties.Remember using (remember; _,_) open import Properties.Equality using (cong) +open import Properties.TypeCheck(strict) using (typeOfᴱ; typeCheckᴱ) open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) {-# REWRITE ∅-[] #-} @@ -58,7 +60,7 @@ progressᴱ H h (function D) _ with alloc H _ progressᴱ H h (function D) _ | ok a H′ r = step (function r) progressᴱ H h (block b D) q with progressᴮ H h D q progressᴱ H h (block b D) q | done refl = step done -progressᴱ H h (block b D) q | return V refl = step return +progressᴱ H h (block b D) q | return V refl = step (return refl) progressᴱ H h (block b D) q | warning W = warning (block b W) progressᴱ H h (block b D) q | step S = step (block S) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 4df8fa57..8e6b9bb0 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -34,34 +34,32 @@ typeOfᴮ Σ Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ Σ (Γ ⊕ x ↦ T) typeOfᴮ Σ Γ (return M ∙ B) = typeOfᴱ Σ Γ M typeOfᴮ Σ Γ done = nil -data TypeCheckResultᴱ (Σ : AddrCtxt) (Γ : VarCtxt) (S : Type) (M : Expr yes) : Set -data TypeCheckResultᴮ (Σ : AddrCtxt) (Γ : VarCtxt) (S : Type) (B : Block yes) : Set +contextOfᴱ : AddrCtxt → VarCtxt → Type → (Expr yes) → VarCtxt +contextOfᴮ : AddrCtxt → VarCtxt → Type → (Block yes) → VarCtxt -data TypeCheckResultᴱ Σ Γ S M where +contextOfᴱ Σ Γ S nil = ∅ +contextOfᴱ Σ Γ S (var x) = (x ↦ S) +contextOfᴱ Σ Γ S (addr a) = ∅ +contextOfᴱ Σ Γ S (M $ N) = (contextOfᴱ Σ Γ (U ⇒ S) M) ⋒ (contextOfᴱ Σ Γ (src T) N) where T = typeOfᴱ Σ Γ M; U = typeOfᴱ Σ Γ N +contextOfᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = (contextOfᴮ Σ (Γ ⊕ x ↦ T) U B) ⊝ x +contextOfᴱ Σ Γ S (block b is B end) = (contextOfᴮ Σ Γ S B) - ok : ∀ Δ → (Σ ▷ Γ ⊢ᴱ S ∋ M ∈ (typeOfᴱ Σ Γ M) ⊣ Δ) → TypeCheckResultᴱ Σ Γ S M - -data TypeCheckResultᴮ Σ Γ S B where +contextOfᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = ((contextOfᴮ Σ (Γ ⊕ x ↦ T) U C) ⊝ x) ⋒ ((contextOfᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B) ⊝ f) +contextOfᴮ Σ Γ S (local var x ∈ T ← M ∙ B) = (contextOfᴱ Σ Γ T M) ⋒ ((contextOfᴮ Σ (Γ ⊕ x ↦ T)S B) ⊝ x) +contextOfᴮ Σ Γ S (return M ∙ B) = (contextOfᴱ Σ Γ S M) +contextOfᴮ Σ Γ S done = ∅ - ok : ∀ Δ → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ Σ Γ B) ⊣ Δ) → TypeCheckResultᴮ Σ Γ S B - -typeCheckᴱ : ∀ Σ Γ S M → (TypeCheckResultᴱ Σ Γ S M) -typeCheckᴮ : ∀ Σ Γ S B → (TypeCheckResultᴮ Σ Γ S B) +typeCheckᴱ : ∀ Σ Γ S M → (Σ ▷ Γ ⊢ᴱ S ∋ M ∈ (typeOfᴱ Σ Γ M) ⊣ (contextOfᴱ Σ Γ S M)) +typeCheckᴮ : ∀ Σ Γ S B → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ Σ Γ B) ⊣ (contextOfᴮ Σ Γ S B)) -typeCheckᴱ Σ Γ S nil = ok ∅ nil -typeCheckᴱ Σ Γ S (var x) = ok (x ↦ S) (var x refl) -typeCheckᴱ Σ Γ S (addr a) = ok ∅ (addr a refl) -typeCheckᴱ Σ Γ S (M $ N) with typeCheckᴱ Σ Γ (typeOfᴱ Σ Γ N ⇒ S) M | typeCheckᴱ Σ Γ (src (typeOfᴱ Σ Γ M)) N -typeCheckᴱ Σ Γ S (M $ N) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok (Δ₁ ⋒ Δ₂) (app D₁ D₂) -typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) with typeCheckᴮ Σ (Γ ⊕ x ↦ T) U B -typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) | ok Δ D = ok (Δ ⊝ x) (function D) -typeCheckᴱ Σ Γ S (block b is B end) with typeCheckᴮ Σ Γ S B -typeCheckᴱ Σ Γ S block b is B end | ok Δ D = ok Δ (block b D) +typeCheckᴱ Σ Γ S nil = nil +typeCheckᴱ Σ Γ S (var x) = var x refl +typeCheckᴱ Σ Γ S (addr a) = addr a refl +typeCheckᴱ Σ Γ S (M $ N) = app (typeCheckᴱ Σ Γ (typeOfᴱ Σ Γ N ⇒ S) M) (typeCheckᴱ Σ Γ (src (typeOfᴱ Σ Γ M)) N) +typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) = function(typeCheckᴮ Σ (Γ ⊕ x ↦ T) U B) +typeCheckᴱ Σ Γ S (block b is B end) = block b (typeCheckᴮ Σ Γ S B) -typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with typeCheckᴮ Σ (Γ ⊕ x ↦ T) U C | typeCheckᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B -typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) (function D₁ D₂) -typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) with typeCheckᴱ Σ Γ T M | typeCheckᴮ Σ (Γ ⊕ x ↦ T) S B -typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok (Δ₁ ⋒ (Δ₂ ⊝ x)) (local D₁ D₂) -typeCheckᴮ Σ Γ S (return M ∙ B) with typeCheckᴱ Σ Γ S M | typeCheckᴮ Σ Γ top B -typeCheckᴮ Σ Γ S (return M ∙ B) | ok Δ₁ D₁ | ok Σ₂ D₂ = ok Δ₁ (return D₁ D₂) -typeCheckᴮ Σ Γ S done = ok ∅ done +typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function(typeCheckᴮ Σ (Γ ⊕ x ↦ T) U C) (typeCheckᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B) +typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ Σ Γ T M) (typeCheckᴮ Σ (Γ ⊕ x ↦ T) S B) +typeCheckᴮ Σ Γ S (return M ∙ B) = return (typeCheckᴱ Σ Γ S M) (typeCheckᴮ Σ Γ top B) +typeCheckᴮ Σ Γ S done = done