luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-25 15:36:53 -06:00
parent e717262099
commit 29b7623b84
14 changed files with 123 additions and 108 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
prototyping/Interpreter.agda
View file

@ -25,8 +25,8 @@ open import Properties.StrictMode using (wellTypedProgramsDontGoWrong)
runBlock′ : ∀ a → Block a → IO ⊤
runBlock′ a block with run block
runBlock′ a block | return V D = putStrLn (valueToString V)
runBlock′ a block | done D = putStrLn "nil"
runBlock′ a block | return V D = putStrLn ("\nRAN WITH RESULT: " ++ valueToString V)
runBlock′ a block | done D = putStrLn ("\nRAN")
runBlock′ maybe block | error E D = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E)
runBlock′ yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
runBlock′ yes block | error E D | W = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E ++ "\n\nTYPE ERROR:\n" ++ warningToStringᴮ _ W)
@ -38,12 +38,12 @@ runBlock B | just B′ = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >>
runJSON : Value → IO ⊤
runJSON value with blockFromJSON(value)
runJSON value | (Left err) = putStrLn ("Luau error: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Left err) = putStrLn ("LUAU ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Right block) = runBlock block
runString : String → IO ⊤
runString txt with eitherDecode (encodeUtf8 txt)
runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Left err) = putStrLn ("JSON ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Right value) = runJSON value
main : IO ⊤

2
prototyping/Luau/StrictMode.agda
View file

@ -5,7 +5,7 @@ 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; bot; top; nil; number; _⇒_; tgt)
open import Luau.Type using (Type; strict; nil; number; _⇒_; 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)

92
prototyping/Luau/Type.agda
View file

@ -9,8 +9,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing)
data Type : Set where
nil : Type
_⇒_ : Type → Type → Type
bot : Type
top : Type
none : Type
any : Type
boolean : Type
number : Type
_∪_ : Type → Type → Type
@ -21,8 +21,8 @@ lhs (T ⇒ _) = T
lhs (T ∪ _) = T
lhs (T ∩ _) = T
lhs nil = nil
lhs bot = bot
lhs top = top
lhs none = none
lhs any = any
lhs number = number
lhs boolean = boolean
@ -31,16 +31,16 @@ rhs (_ ⇒ T) = T
rhs (_ ∪ T) = T
rhs (_ ∩ T) = T
rhs nil = nil
rhs bot = bot
rhs top = top
rhs none = none
rhs any = any
rhs number = number
rhs boolean = boolean
_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
nil ≡ᵀ nil = yes refl
nil ≡ᵀ (S ⇒ T) = no (λ ())
nil ≡ᵀ bot = no (λ ())
nil ≡ᵀ top = no (λ ())
nil ≡ᵀ none = no (λ ())
nil ≡ᵀ any = no (λ ())
nil ≡ᵀ number = no (λ ())
nil ≡ᵀ boolean = no (λ ())
nil ≡ᵀ (S ∪ T) = no (λ ())
@ -50,48 +50,48 @@ nil ≡ᵀ (S ∩ T) = no (λ ())
(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) ≡ᵀ none = no (λ ())
(S ⇒ T) ≡ᵀ any = no (λ ())
(S ⇒ T) ≡ᵀ number = no (λ ())
(S ⇒ T) ≡ᵀ boolean = 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 ≡ᵀ number = no (λ ())
bot ≡ᵀ boolean = no (λ ())
bot ≡ᵀ (U ∪ V) = no (λ ())
bot ≡ᵀ (U ∩ V) = no (λ ())
top ≡ᵀ nil = no (λ ())
top ≡ᵀ (U ⇒ V) = no (λ ())
top ≡ᵀ bot = no (λ ())
top ≡ᵀ top = yes refl
top ≡ᵀ number = no (λ ())
top ≡ᵀ boolean = no (λ ())
top ≡ᵀ (U ∪ V) = no (λ ())
top ≡ᵀ (U ∩ V) = no (λ ())
none ≡ᵀ nil = no (λ ())
none ≡ᵀ (U ⇒ V) = no (λ ())
none ≡ᵀ none = yes refl
none ≡ᵀ any = no (λ ())
none ≡ᵀ number = no (λ ())
none ≡ᵀ boolean = no (λ ())
none ≡ᵀ (U ∪ V) = no (λ ())
none ≡ᵀ (U ∩ V) = no (λ ())
any ≡ᵀ nil = no (λ ())
any ≡ᵀ (U ⇒ V) = no (λ ())
any ≡ᵀ none = no (λ ())
any ≡ᵀ any = yes refl
any ≡ᵀ number = no (λ ())
any ≡ᵀ boolean = no (λ ())
any ≡ᵀ (U ∪ V) = no (λ ())
any ≡ᵀ (U ∩ V) = no (λ ())
number ≡ᵀ nil = no (λ ())
number ≡ᵀ (T ⇒ U) = no (λ ())
number ≡ᵀ bot = no (λ ())
number ≡ᵀ top = no (λ ())
number ≡ᵀ none = no (λ ())
number ≡ᵀ any = no (λ ())
number ≡ᵀ number = yes refl
number ≡ᵀ boolean = no (λ ())
number ≡ᵀ (T ∪ U) = no (λ ())
number ≡ᵀ (T ∩ U) = no (λ ())
boolean ≡ᵀ nil = no (λ ())
boolean ≡ᵀ (T ⇒ U) = no (λ ())
boolean ≡ᵀ bot = no (λ ())
boolean ≡ᵀ top = no (λ ())
boolean ≡ᵀ none = no (λ ())
boolean ≡ᵀ any = no (λ ())
boolean ≡ᵀ boolean = yes refl
boolean ≡ᵀ number = no (λ ())
boolean ≡ᵀ (T ∪ U) = no (λ ())
boolean ≡ᵀ (T ∩ U) = no (λ ())
(S ∪ T) ≡ᵀ nil = no (λ ())
(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
(S ∪ T) ≡ᵀ bot = no (λ ())
(S ∪ T) ≡ᵀ top = no (λ ())
(S ∪ T) ≡ᵀ none = no (λ ())
(S ∪ T) ≡ᵀ any = no (λ ())
(S ∪ T) ≡ᵀ number = no (λ ())
(S ∪ T) ≡ᵀ boolean = no (λ ())
(S ∪ T) ≡ᵀ (U ∪ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
@ -101,8 +101,8 @@ boolean ≡ᵀ (T ∩ U) = no (λ ())
(S ∪ T) ≡ᵀ (U ∩ V) = no (λ ())
(S ∩ T) ≡ᵀ nil = no (λ ())
(S ∩ T) ≡ᵀ (U ⇒ V) = no (λ ())
(S ∩ T) ≡ᵀ bot = no (λ ())
(S ∩ T) ≡ᵀ top = no (λ ())
(S ∩ T) ≡ᵀ none = no (λ ())
(S ∩ T) ≡ᵀ any = no (λ ())
(S ∩ T) ≡ᵀ number = no (λ ())
(S ∩ T) ≡ᵀ boolean = no (λ ())
(S ∩ T) ≡ᵀ (U ∪ V) = no (λ ())
@ -124,27 +124,27 @@ data Mode : Set where
nonstrict : Mode
src : Mode → Type → Type
src m nil = bot
src m number = bot
src m boolean = bot
src m nil = none
src m number = none
src m boolean = none
src m (S ⇒ T) = S
-- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant
src strict (S ∪ T) = (src strict S) ∩ (src strict T)
src nonstrict (S ∪ T) = (src nonstrict S) ∪ (src nonstrict T)
src strict (S ∩ T) = (src strict S) ∪ (src strict T)
src nonstrict (S ∩ T) = (src nonstrict S) ∩ (src nonstrict T)
src strict bot = top
src nonstrict bot = bot
src strict top = bot
src nonstrict top = top
src strict none = any
src nonstrict none = none
src strict any = none
src nonstrict any = any
tgt : Type → Type
tgt nil = bot
tgt nil = none
tgt (S ⇒ T) = T
tgt bot = bot
tgt top = top
tgt number = bot
tgt boolean = bot
tgt none = none
tgt any = any
tgt number = none
tgt boolean = none
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
tgt (S ∩ T) = (tgt S) ∩ (tgt T)

4
prototyping/Luau/Type/FromJSON.agda
View file

@ -2,7 +2,7 @@
module Luau.Type.FromJSON where
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; top; number)
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
open import Agda.Builtin.List using (List; _∷_; [])
open import Agda.Builtin.Bool using (true; false)
@ -42,7 +42,7 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right top
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"

6
prototyping/Luau/Type/ToString.agda
View file

@ -1,7 +1,7 @@
module Luau.Type.ToString where
open import FFI.Data.String using (String; _++_)
open import Luau.Type using (Type; nil; _⇒_; bot; top; number; boolean; _∪_; _∩_; normalizeOptional)
open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; _∪_; _∩_; normalizeOptional)
{-# TERMINATING #-}
typeToString : Type → String
@ -10,8 +10,8 @@ typeToStringᴵ : Type → String
typeToString nil = "nil"
typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
typeToString bot = "bot"
typeToString top = "top"
typeToString none = "none"
typeToString any = "any"
typeToString number = "number"
typeToString boolean = "boolean"
typeToString (S ∪ T) with normalizeOptional(S ∪ T)

10
prototyping/Luau/TypeCheck.agda
View file

@ -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; bot; top; number; boolean; _⇒_; tgt)
open import Luau.Type using (Type; Mode; nil; none; number; boolean; _⇒_; 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,9 @@ open import Properties.Product using (_×_; _,_)
src : Type → Type
src = Luau.Type.src m
orBot : Maybe Type → Type
orBot nothing = bot
orBot (just T) = T
orNone : Maybe Type → Type
orNone nothing = none
orNone (just T) = T
tgtBinOp : BinaryOperator → Type
tgtBinOp + = number
@ -75,7 +75,7 @@ data _⊢ᴱ_∈_ where
var : ∀ {x T Γ} →
T ≡ orBot(Γ [ x ]ⱽ) →
T ≡ orNone(Γ [ x ]ⱽ) →
----------------
Γ ⊢ᴱ (var x) ∈ T

2
prototyping/Luau/VarCtxt.agda
View file

@ -3,7 +3,7 @@
module Luau.VarCtxt where
open import Agda.Builtin.Equality using (_≡_)
open import Luau.Type using (Type; bot; _∪_; _∩_)
open import Luau.Type using (Type; _∪_; _∩_)
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; insert-swap; insert-over)
open import FFI.Data.Maybe using (Maybe; just; nothing)

4
prototyping/Properties/Step.agda
View file

@ -8,7 +8,7 @@ open import Agda.Builtin.Bool using (true; false)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp; evalNeqOp)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=)
open import Luau.RuntimeType using (valueType; function; number)
open import Luau.Substitution using (_[_/_]ᴮ)
@ -64,7 +64,7 @@ binOpStep (number m) > (number n) = step (bool (primFloatLess n m)) (> m n)
binOpStep (number m) > (bool b) = error₂ (> (λ ()))
binOpStep (bool b) > w = error₁ (> (λ ()))
binOpStep v == w = step (bool (evalEqOp v w)) (== v w)
binOpStep v ~= w = step (bool (not (evalEqOp v w))) (~= v w)
binOpStep v ~= w = step (bool (evalNeqOp v w)) (~= v w)
binOpStep nil <= w = error₁ (<= (λ ()))
binOpStep (addr a) <= w = error₁ (<= (λ ()))
binOpStep (number m) <= nil = error₂ (<= (λ ()))

64
prototyping/Properties/StrictMode.agda
View file

@ -9,8 +9,8 @@ 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; FunctionCallMismatch; app₁; app₂; BinOpWarning; 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.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
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; tgtBinOp)
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.Var using (_≡ⱽ_)
open import Luau.Addr using (_≡ᴬ_)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
@ -83,7 +83,7 @@ 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 orBot (cong typeOfᴹᴼ (lookup-not-allocated p q)))
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 (binexp M op N) h = ok refl
@ -103,16 +103,16 @@ 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
bot-not-obj : ∀ O → bot ≢ typeOfᴼ O
bot-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) ()
none-not-obj : ∀ O → none ≢ typeOfᴼ O
none-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 nil = ok (λ ())
typeOf-val-not-bot (number n) = ok (λ ())
typeOf-val-not-bot (bool b) = 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 p)
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 {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)))
@ -129,8 +129,8 @@ 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 orBot q
substitutivityᴱ-whenever-no H v x y p q = cong orBot ( sym (⊕-lookup-miss x y _ _ p))
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)
@ -167,11 +167,11 @@ 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 orBot (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 | 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 orBot (cong typeOfᴹᴼ p)))) s) (cong orBot 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-bot 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 orBot q)))
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)
@ -190,9 +190,9 @@ preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warnin
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 orBot p)))))
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-bot v
preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orBot 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))
@ -322,16 +322,16 @@ 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 orBot (sym r)) (trans (sym t) (cong src (cong orBot (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-bot 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 orBot (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 orBot (sym q)) (trans (sym s) (cong src (cong orBot (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-bot 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 orBot (sym q)))
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)))
@ -377,9 +377,9 @@ reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (
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 orBot (sym p)) (sym r))))
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-bot v
reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orBot (sym p)))
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′
@ -435,7 +435,7 @@ reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴ
reflect* H B refl W = W
reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → BinOpWarning op (orBot (typeOfⱽ H v))
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))
@ -450,7 +450,7 @@ runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheck
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-bot w
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) (app₁ err) = app₁ (runtimeWarningᴱ H M err)

16
prototyping/Properties/TypeCheck.agda
View file

@ -8,9 +8,9 @@ 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; app; function; block; binexp; done; return; local; nothing; orBot; tgtBinOp)
open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Type using (Type; nil; top; bot; number; boolean; _⇒_; tgt)
open import Luau.Type using (Type; nil; any; none; number; boolean; _⇒_; tgt)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType)
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.Addr using (Addr)
@ -41,8 +41,8 @@ typeOfⱽ H (number n) = just number
typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
typeOfᴱ H Γ (var x) = orBot(Γ [ x ]ⱽ)
typeOfᴱ H Γ (val v) = orBot(typeOfⱽ H v)
typeOfᴱ H Γ (var x) = orNone(Γ [ x ]ⱽ)
typeOfᴱ H Γ (val v) = orNone(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
@ -53,7 +53,7 @@ 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
mustBeFunction : ∀ H Γ v → (bot ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v))
mustBeFunction : ∀ H Γ v → (none ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v))
mustBeFunction H Γ nil p = CONTRADICTION (p refl)
mustBeFunction H Γ (addr a) p = refl
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
@ -63,9 +63,9 @@ mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
mustBeNumber H Γ nil ()
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orBot (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (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 orBot (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | nothing , q | ()
mustBeNumber H Γ (number n) p = refl
mustBeNumber H Γ (bool true) ()
@ -76,7 +76,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 (orBot (typeOfᴹᴼ (H [ a ]ᴴ)))
typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
typeCheckᴱ H Γ (val (number n)) = number
typeCheckᴱ H Γ (val (bool b)) = bool
typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)

5
prototyping/Tests/Interpreter/binary_equality_bools/out.txt
View file

@ -1 +1,4 @@
false
ANNOTATED PROGRAM:
return true == false
RAN WITH RESULT: false

5
prototyping/Tests/Interpreter/binary_equality_numbers/out.txt
View file

@ -1 +1,4 @@
true
ANNOTATED PROGRAM:
return 1.0 == 1.0
RAN WITH RESULT: true

5
prototyping/Tests/Interpreter/binary_exps/out.txt
View file

@ -1 +1,4 @@
1.0
ANNOTATED PROGRAM:
return 1.0 + 2.0 - 2.0 * 2.0 / 2.0
RAN WITH RESULT: 1.0

8
prototyping/Tests/Interpreter/return_nil/out.txt
View file

@ -1 +1,7 @@
nil
UNANNOTATED PROGRAM:
local function foo(x)
return nil
end
return foo(nil)
RAN WITH RESULT: nil