From 29b7623b840d71ba408a69589e244def0ed37f0b Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 25 Feb 2022 15:36:53 -0600 Subject: [PATCH] WIP --- prototyping/Interpreter.agda | 8 +- prototyping/Luau/StrictMode.agda | 2 +- prototyping/Luau/Type.agda | 92 +++++++++---------- prototyping/Luau/Type/FromJSON.agda | 4 +- prototyping/Luau/Type/ToString.agda | 6 +- prototyping/Luau/TypeCheck.agda | 10 +- prototyping/Luau/VarCtxt.agda | 2 +- prototyping/Properties/Step.agda | 4 +- prototyping/Properties/StrictMode.agda | 64 ++++++------- prototyping/Properties/TypeCheck.agda | 16 ++-- .../Interpreter/binary_equality_bools/out.txt | 5 +- .../binary_equality_numbers/out.txt | 5 +- .../Tests/Interpreter/binary_exps/out.txt | 5 +- .../Tests/Interpreter/return_nil/out.txt | 8 +- 14 files changed, 123 insertions(+), 108 deletions(-) diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index cb62c707..d8036740 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -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 ⊤ diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda index 44991043..d7b2129f 100644 --- a/prototyping/Luau/StrictMode.agda +++ b/prototyping/Luau/StrictMode.agda @@ -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) diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 59c4db66..10f39c44 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -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) diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda index 805460c1..9057fef4 100644 --- a/prototyping/Luau/Type/FromJSON.agda +++ b/prototyping/Luau/Type/FromJSON.agda @@ -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" diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index 958840a7..dec7c14c 100644 --- a/prototyping/Luau/Type/ToString.agda +++ b/prototyping/Luau/Type/ToString.agda @@ -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) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index d4725f13..f240e17e 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -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 diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index b05cdd7b..a9280ec4 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -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) diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 608912b8..0b5fd062 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -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₂ (<= (λ ())) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index adea8ea1..08411188 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -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) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index 746ce3ec..c144bc12 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -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) diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/out.txt b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt index c508d536..ee6f2a25 100644 --- a/prototyping/Tests/Interpreter/binary_equality_bools/out.txt +++ b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt @@ -1 +1,4 @@ -false +ANNOTATED PROGRAM: +return true == false + +RAN WITH RESULT: false diff --git a/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt index 27ba77dd..86a499a8 100644 --- a/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt +++ b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt @@ -1 +1,4 @@ -true +ANNOTATED PROGRAM: +return 1.0 == 1.0 + +RAN WITH RESULT: true diff --git a/prototyping/Tests/Interpreter/binary_exps/out.txt b/prototyping/Tests/Interpreter/binary_exps/out.txt index d3827e75..5b4d2644 100644 --- a/prototyping/Tests/Interpreter/binary_exps/out.txt +++ b/prototyping/Tests/Interpreter/binary_exps/out.txt @@ -1 +1,4 @@ -1.0 +ANNOTATED PROGRAM: +return 1.0 + 2.0 - 2.0 * 2.0 / 2.0 + +RAN WITH RESULT: 1.0 diff --git a/prototyping/Tests/Interpreter/return_nil/out.txt b/prototyping/Tests/Interpreter/return_nil/out.txt index 607602cf..1d5f45b6 100644 --- a/prototyping/Tests/Interpreter/return_nil/out.txt +++ b/prototyping/Tests/Interpreter/return_nil/out.txt @@ -1 +1,7 @@ -nil +UNANNOTATED PROGRAM: +local function foo(x) + return nil +end +return foo(nil) + +RAN WITH RESULT: nil