mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
244 lines
7.9 KiB
Agda
244 lines
7.9 KiB
Agda
{-# 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; 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; boolean; none; any; _⇒_; _∪_; _∩_; tgt)
|
||
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; srcBinOp)
|
||
open import Properties.Contradiction using (¬)
|
||
open import Properties.Equality using (_≢_)
|
||
open import Properties.TypeCheck(strict) using (typeCheckᴮ)
|
||
open import Properties.Product using (_,_)
|
||
|
||
src : Type → Type
|
||
src = Luau.Type.src strict
|
||
|
||
data Scalar : Type → Set where
|
||
|
||
number : Scalar number
|
||
boolean : Scalar boolean
|
||
string : Scalar string
|
||
nil : Scalar nil
|
||
|
||
data Tree : Set where
|
||
|
||
scalar : ∀ {T} → Scalar T → 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-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)
|
||
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-ok : ∀ {S u} → (Scalar S) → ¬Language S (function-ok u)
|
||
scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
|
||
function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
|
||
function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u)
|
||
function-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
|
||
|
||
data _≮:_ (T U : Type) : Set where
|
||
|
||
witness : ∀ t →
|
||
|
||
Language T t →
|
||
¬Language U t →
|
||
-----------------
|
||
T ≮: U
|
||
|
||
data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
|
||
data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set
|
||
|
||
data Warningᴱ H {Γ} where
|
||
|
||
UnallocatedAddress : ∀ {a T} →
|
||
|
||
(H [ a ]ᴴ ≡ nothing) →
|
||
---------------------
|
||
Warningᴱ H (addr {a} T)
|
||
|
||
UnboundVariable : ∀ {x T p} →
|
||
|
||
(Γ [ x ]ⱽ ≡ nothing) →
|
||
------------------------
|
||
Warningᴱ H (var {x} {T} p)
|
||
|
||
FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
(U ≮: src T) →
|
||
-----------------
|
||
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₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
Warningᴱ H D₂ →
|
||
-----------------
|
||
Warningᴱ H (app D₁ D₂)
|
||
|
||
BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
(T ≮: srcBinOp op) →
|
||
------------------------------
|
||
Warningᴱ H (binexp {op} D₁ D₂)
|
||
|
||
BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
(U ≮: srcBinOp op) →
|
||
------------------------------
|
||
Warningᴱ H (binexp {op} D₁ D₂)
|
||
|
||
bin₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
Warningᴱ H D₁ →
|
||
------------------------------
|
||
Warningᴱ H (binexp {op} D₁ D₂)
|
||
|
||
bin₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
|
||
|
||
Warningᴱ H D₂ →
|
||
------------------------------
|
||
Warningᴱ H (binexp {op} D₁ D₂)
|
||
|
||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||
|
||
(V ≮: U) →
|
||
-------------------------
|
||
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)
|
||
|
||
BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||
|
||
(U ≮: T) →
|
||
------------------------------
|
||
Warningᴱ H (block {b} {T = T} D)
|
||
|
||
block₁ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
|
||
|
||
Warningᴮ H D →
|
||
------------------------------
|
||
Warningᴱ H (block {b} {T = T} D)
|
||
|
||
data Warningᴮ H {Γ} where
|
||
|
||
return : ∀ {M B T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴮ B ∈ U} →
|
||
|
||
Warningᴱ H D₁ →
|
||
------------------
|
||
Warningᴮ H (return D₁ D₂)
|
||
|
||
LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||
|
||
(U ≮: T) →
|
||
--------------------
|
||
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₂)
|
||
|
||
local₂ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
|
||
|
||
Warningᴮ H D₂ →
|
||
--------------------
|
||
Warningᴮ H (local D₁ D₂)
|
||
|
||
FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
|
||
|
||
(V ≮: U) →
|
||
-------------------------------------
|
||
Warningᴮ H (function D₁ 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 D₁ 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 D₁ D₂)
|
||
|
||
data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where
|
||
|
||
FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
|
||
|
||
(V ≮: U) →
|
||
---------------------------------
|
||
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)
|
||
|
||
data Warningᴴ H (D : ⊢ᴴ H) : Set where
|
||
|
||
addr : ∀ a {O} →
|
||
|
||
(p : H [ a ]ᴴ ≡ O) →
|
||
Warningᴼ H (D a p) →
|
||
---------------
|
||
Warningᴴ H D
|
||
|
||
data Warningᴴᴱ H {Γ M T} : (Γ ⊢ᴴᴱ H ▷ M ∈ T) → Set where
|
||
|
||
heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →
|
||
|
||
Warningᴴ H D₁ →
|
||
-----------------
|
||
Warningᴴᴱ H (D₁ , D₂)
|
||
|
||
expr : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →
|
||
|
||
Warningᴱ H D₂ →
|
||
---------------------
|
||
Warningᴴᴱ H (D₁ , D₂)
|
||
|
||
data Warningᴴᴮ H {Γ B T} : (Γ ⊢ᴴᴮ H ▷ B ∈ T) → Set where
|
||
|
||
heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →
|
||
|
||
Warningᴴ H D₁ →
|
||
-----------------
|
||
Warningᴴᴮ H (D₁ , D₂)
|
||
|
||
block : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →
|
||
|
||
Warningᴮ H D₂ →
|
||
---------------------
|
||
Warningᴴᴮ H (D₁ , D₂)
|