From c5477d522dcb31368a8ee864fb9c7b9c34d7730c Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Wed, 2 Mar 2022 16:02:51 -0600 Subject: [PATCH] Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown --- prototyping/.gitignore | 2 - prototyping/Everything.agda | 8 + prototyping/Examples/OpSem.agda | 8 +- prototyping/Examples/Run.agda | 15 +- prototyping/Examples/Syntax.agda | 4 +- prototyping/Examples/Type.agda | 1 + prototyping/FFI/Data/Aeson.agda | 29 +- prototyping/FFI/Data/Maybe.agda | 6 + prototyping/FFI/Data/Vector.agda | 9 + prototyping/Interpreter.agda | 32 +- prototyping/Luau/Addr.agda | 5 +- prototyping/Luau/Heap.agda | 42 +- prototyping/Luau/OpSem.agda | 138 +++-- prototyping/Luau/Run.agda | 7 +- prototyping/Luau/RuntimeError.agda | 29 +- prototyping/Luau/RuntimeError/ToString.agda | 36 +- prototyping/Luau/RuntimeType.agda | 8 +- prototyping/Luau/StrictMode.agda | 205 ++++++++ prototyping/Luau/StrictMode/ToString.agda | 39 ++ prototyping/Luau/Substitution.agda | 11 +- prototyping/Luau/Syntax.agda | 64 ++- prototyping/Luau/Syntax/FromJSON.agda | 59 ++- prototyping/Luau/Syntax/ToString.agda | 29 +- prototyping/Luau/Type.agda | 135 ++++- prototyping/Luau/Type/FromJSON.agda | 2 + prototyping/Luau/Type/ToString.agda | 3 +- prototyping/Luau/TypeCheck.agda | 143 ++++++ prototyping/Luau/Value.agda | 20 - prototyping/Luau/Value/ToString.agda | 14 - prototyping/Luau/Var.agda | 6 +- prototyping/Luau/VarCtxt.agda | 43 ++ prototyping/PrettyPrinter.agda | 2 + prototyping/Properties.agda | 6 +- prototyping/Properties/Dec.agda | 5 +- prototyping/Properties/Product.agda | 14 + prototyping/Properties/Step.agda | 145 ++++-- prototyping/Properties/StrictMode.agda | 470 ++++++++++++++++++ prototyping/Properties/TypeCheck.agda | 103 ++++ .../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 +- 42 files changed, 1601 insertions(+), 319 deletions(-) create mode 100644 prototyping/Everything.agda create mode 100644 prototyping/Luau/StrictMode.agda create mode 100644 prototyping/Luau/StrictMode/ToString.agda create mode 100644 prototyping/Luau/TypeCheck.agda delete mode 100644 prototyping/Luau/Value.agda delete mode 100644 prototyping/Luau/Value/ToString.agda create mode 100644 prototyping/Luau/VarCtxt.agda create mode 100644 prototyping/Properties/Product.agda create mode 100644 prototyping/Properties/StrictMode.agda create mode 100644 prototyping/Properties/TypeCheck.agda diff --git a/prototyping/.gitignore b/prototyping/.gitignore index 10edac520..31e8c073f 100644 --- a/prototyping/.gitignore +++ b/prototyping/.gitignore @@ -2,10 +2,8 @@ *.agdai Main MAlonzo -Examples PrettyPrinter Interpreter -Properties !Tests/Interpreter !Tests/PrettyPrinter .ghc.* diff --git a/prototyping/Everything.agda b/prototyping/Everything.agda new file mode 100644 index 000000000..d8a1fd5ae --- /dev/null +++ b/prototyping/Everything.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --rewriting #-} + +module Everything where + +import Examples +import Properties +import PrettyPrinter +import Interpreter diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index c4cfc5e5c..c3f74ec1d 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -1,8 +1,10 @@ +{-# OPTIONS --rewriting #-} + module Examples.OpSem where open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst) -open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end) +open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end) open import Luau.Heap using (∅) -ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅ -ex1 = subst +ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅ +ex1 = subst nil diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index ddec8e8b0..545ecf51d 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -4,22 +4,17 @@ module Examples.Run where open import Agda.Builtin.Equality using (_≡_; refl) open import Agda.Builtin.Bool using (true; false) -open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; true; false) -open import Luau.Value using (nil; number; bool) +open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool) 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 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ val nil) ∙ done) ≡ return nil _) ex1 = refl -ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _) +ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (val (number 123.0)) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 123.0) _) ex2 = refl -ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _) +ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) + (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 3.0) _) ex3 = refl -ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) < (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool true) _) +ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) < (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _) ex4 = refl diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda index 4ffcf4c50..e2793023e 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -2,7 +2,7 @@ module Examples.Syntax where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.String using (_++_) -open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩) +open import Luau.Syntax using (var; _$_; return; val; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩) open import Luau.Syntax.ToString using (exprToString; blockToString) ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡ @@ -11,7 +11,7 @@ ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ "end" ex1 = refl -ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡ +ex2 : blockToString(local var "x" ← (val nil) ∙ return (var "x") ∙ done) ≡ "local x = nil\n" ++ "return x" ex2 = refl diff --git a/prototyping/Examples/Type.agda b/prototyping/Examples/Type.agda index 859227ee3..3fdd37d56 100644 --- a/prototyping/Examples/Type.agda +++ b/prototyping/Examples/Type.agda @@ -25,3 +25,4 @@ ex6 = refl ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?" ex7 = refl + diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index a9082d31a..0cd272320 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -1,15 +1,21 @@ +{-# OPTIONS --rewriting #-} + module FFI.Data.Aeson where +open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Equality.Rewrite using () open import Agda.Builtin.Bool using (Bool) open import Agda.Builtin.String using (String) open import FFI.Data.ByteString using (ByteString) open import FFI.Data.HaskellString using (HaskellString; pack) -open import FFI.Data.Maybe using (Maybe) +open import FFI.Data.Maybe using (Maybe; just; nothing) open import FFI.Data.Either using (Either; mapLeft) open import FFI.Data.Scientific using (Scientific) open import FFI.Data.Vector using (Vector) +open import Properties.Equality using (_≢_) + {-# FOREIGN GHC import qualified Data.Aeson #-} {-# FOREIGN GHC import qualified Data.Aeson.Key #-} {-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-} @@ -19,14 +25,35 @@ postulate Key : Set fromString : String → Key toString : Key → String + empty : ∀ {A} → KeyMap A + singleton : ∀ {A} → Key → A → (KeyMap A) + insert : ∀ {A} → Key → A → (KeyMap A) → (KeyMap A) + delete : ∀ {A} → Key → (KeyMap A) → (KeyMap A) + unionWith : ∀ {A} → (A → A → A) → (KeyMap A) → (KeyMap A) → (KeyMap A) lookup : ∀ {A} → Key -> KeyMap A -> Maybe A {-# POLARITY KeyMap ++ #-} {-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-} {-# COMPILE GHC Key = type Data.Aeson.Key.Key #-} {-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-} {-# COMPILE GHC toString = Data.Aeson.Key.toText #-} +{-# COMPILE GHC empty = \_ -> Data.Aeson.KeyMap.empty #-} +{-# COMPILE GHC singleton = \_ -> Data.Aeson.KeyMap.singleton #-} +{-# COMPILE GHC insert = \_ -> Data.Aeson.KeyMap.insert #-} +{-# COMPILE GHC delete = \_ -> Data.Aeson.KeyMap.delete #-} +{-# COMPILE GHC unionWith = \_ -> Data.Aeson.KeyMap.unionWith #-} {-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-} +postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m) ≡ just v) +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 + +{-# REWRITE lookup-insert lookup-empty singleton-insert-empty #-} + data Value : Set where object : KeyMap Value → Value array : Vector Value → Value diff --git a/prototyping/FFI/Data/Maybe.agda b/prototyping/FFI/Data/Maybe.agda index b16fa810f..58fd14861 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 7d2f5012b..08761edf8 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -1,11 +1,15 @@ +{-# OPTIONS --rewriting #-} + module FFI.Data.Vector where open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Equality.Rewrite using () open import Agda.Builtin.Int using (Int; pos; negsuc) open import Agda.Builtin.Nat using (Nat) open import Agda.Builtin.Bool using (Bool; false; true) open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt) open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Properties.Equality using (_≢_) {-# FOREIGN GHC import qualified Data.Vector #-} @@ -30,8 +34,13 @@ postulate {-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-} 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-length lookup-snoc-empty lookup-empty #-} head : ∀ {A} → (Vector A) → (Maybe A) head vec with null vec diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index fe311e578..d8036740c 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Interpreter where open import Agda.Builtin.IO using (IO) @@ -7,31 +9,41 @@ open import Agda.Builtin.Unit using (⊤) open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_) open import FFI.Data.Aeson using (Value; eitherDecode) open import FFI.Data.Either using (Left; Right) +open import FFI.Data.Maybe using (just; nothing) open import FFI.Data.String using (String; _++_) open import FFI.Data.Text.Encoding using (encodeUtf8) open import FFI.System.Exit using (exitWith; ExitFailure) -open import Luau.Syntax using (Block) +open import Luau.StrictMode.ToString using (warningToStringᴮ) +open import Luau.Syntax using (Block; yes; maybe; isAnnotatedᴮ) open import Luau.Syntax.FromJSON using (blockFromJSON) -open import Luau.Syntax.ToString using (blockToString) +open import Luau.Syntax.ToString using (blockToString; valueToString) open import Luau.Run using (run; return; done; error) open import Luau.RuntimeError.ToString using (errToStringᴮ) -open import Luau.Value.ToString using (valueToString) -runBlock : ∀ {a} → Block a → IO ⊤ -runBlock block with run block -runBlock block | return V D = putStrLn (valueToString V) -runBlock block | done D = putStrLn "nil" -runBlock block | error E D = putStrLn (errToStringᴮ E) +open import Properties.StrictMode using (wellTypedProgramsDontGoWrong) + +runBlock′ : ∀ a → Block a → IO ⊤ +runBlock′ a block with run block +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) + +runBlock : Block maybe → IO ⊤ +runBlock B with isAnnotatedᴮ B +runBlock B | nothing = putStrLn ("UNANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ maybe B +runBlock B | just B′ = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ yes 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/Addr.agda b/prototyping/Luau/Addr.agda index c19780476..b6f989f57 100644 --- a/prototyping/Luau/Addr.agda +++ b/prototyping/Luau/Addr.agda @@ -5,13 +5,14 @@ open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.Nat using (Nat; _==_) open import Agda.Builtin.String using (String) open import Agda.Builtin.TrustMe using (primTrustMe) -open import Properties.Dec using (Dec; yes; no; ⊥) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Equality using (_≢_) Addr : Set Addr = Nat _≡ᴬ_ : (a b : Addr) → Dec (a ≡ b) a ≡ᴬ b with a == b -a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ᴬ b | false = no p where postulate p : (a ≢ b) a ≡ᴬ b | true = yes primTrustMe diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda index 12f8dab07..713b0a1ae 100644 --- a/prototyping/Luau/Heap.agda +++ b/prototyping/Luau/Heap.agda @@ -1,32 +1,39 @@ +{-# OPTIONS --rewriting #-} + module Luau.Heap where -open import Agda.Builtin.Equality using (_≡_) -open import FFI.Data.Maybe using (Maybe; just) -open import FFI.Data.Vector using (Vector; length; snoc; empty) -open import Luau.Addr using (Addr) +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.Var using (Var) -open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end) +open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end) +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 -data HeapValue (a : Annotated) : Set where - function_is_end : FunDec a → Block a → HeapValue a + function_is_end : FunDec a → Block a → Object a Heap : Annotated → Set -Heap a = Vector (HeapValue a) +Heap a = Vector (Object a) -data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where +data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → Object a → Set where defn : ∀ {H val} → ----------------------------------- (snoc H val) ≡ H ⊕ (length H) ↦ val -_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a) +_[_] : ∀ {a} → Heap a → Addr → Maybe (Object a) _[_] = FFI.Data.Vector.lookup ∅ : ∀ {a} → Heap a ∅ = empty -data AllocResult a (H : Heap a) (V : HeapValue a) : Set where +data AllocResult a (H : Heap a) (V : Object a) : Set where ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V alloc : ∀ {a} H V → AllocResult a H V @@ -35,15 +42,8 @@ alloc H V = ok (length H) (snoc H V) defn next : ∀ {a} → Heap a → Addr next = length -allocated : ∀ {a} → Heap a → HeapValue a → Heap a +allocated : ∀ {a} → Heap a → Object a → Heap a allocated = snoc --- next-emp : (length ∅ ≡ 0) -next-emp = FFI.Data.Vector.length-empty - --- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V) -lookup-next = FFI.Data.Vector.lookup-snoc - --- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V) -lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty - +lookup-not-allocated : ∀ {a} {H H′ : Heap a} {b c O} → (H′ ≡ H ⊕ b ↦ O) → (c ≢ b) → (H [ c ] ≡ H′ [ c ]) +lookup-not-allocated {H = H} {O = O} defn p = lookup-snoc-not O H p diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda index bd75d9d6f..cbb559787 100644 --- a/prototyping/Luau/OpSem.agda +++ b/prototyping/Luau/OpSem.agda @@ -1,66 +1,53 @@ +{-# OPTIONS --rewriting #-} + module Luau.OpSem where open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality) open import Agda.Builtin.Bool using (Bool; true; false) open import Utility.Bool using (not; _or_; _and_) -open import Agda.Builtin.Nat using (_==_) -open import FFI.Data.Maybe using (just) +open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_) +open import FFI.Data.Maybe using (Maybe; just; nothing) open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end) open import Luau.Substitution using (_[_/_]ᴮ) -open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; number) -open import Luau.Value using (addr; val; number; Value; bool) +open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; number; bool) open import Luau.RuntimeType using (RuntimeType; valueType) - -evalNumOp : Float → BinaryOperator → Float → Value -evalNumOp x + y = number (primFloatPlus x y) -evalNumOp x - y = number (primFloatMinus x y) -evalNumOp x * y = number (primFloatTimes x y) -evalNumOp x / y = number (primFloatDiv x y) -evalNumOp x < y = bool (primFloatLess x y) -evalNumOp x > y = bool (primFloatLess y x) -evalNumOp x ≡ y = bool (primFloatEquality x y) -evalNumOp x ≅ y = bool (primFloatInequality x y) -evalNumOp x ≤ y = bool ((primFloatLess x y) or (primFloatEquality x y)) -evalNumOp x ≥ y = bool ((primFloatLess y x) or (primFloatEquality x y)) - -evalEqOp : Value → Value → Value -evalEqOp Value.nil Value.nil = bool true -evalEqOp (addr x) (addr y) = bool (x == y) -evalEqOp (number x) (number y) = bool (primFloatEquality x y) -evalEqOp (bool true) (bool y) = bool y -evalEqOp (bool false) (bool y) = bool (not y) -evalEqOp _ _ = bool false - -evalNeqOp : Value → Value → Value -evalNeqOp Value.nil Value.nil = bool false -evalNeqOp (addr x) (addr y) = bool (not (x == y)) -evalNeqOp (number x) (number y) = bool (primFloatInequality x y) -evalNeqOp (bool true) (bool y) = bool (not y) -evalNeqOp (bool false) (bool y) = bool y -evalNeqOp _ _ = bool true - -coerceToBool : Value → Bool -coerceToBool Value.nil = false -coerceToBool (addr x) = true -coerceToBool (number x) = true -coerceToBool (bool x) = x - +open import Properties.Product using (_×_; _,_) + +evalEqOp : Value → Value → Bool +evalEqOp Value.nil Value.nil = true +evalEqOp (addr x) (addr y) = (x ==ᴬ y) +evalEqOp (number x) (number y) = primFloatEquality x y +evalEqOp (bool true) (bool y) = y +evalEqOp (bool false) (bool y) = not y +evalEqOp _ _ = false + +evalNeqOp : Value → Value → Bool +evalNeqOp (number x) (number y) = primFloatInequality x y +evalNeqOp x y = not (evalEqOp x y) + +data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where + + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n) + - : ∀ m n → (number m) ⟦ - ⟧ (number n) ⟶ number (primFloatMinus m n) + / : ∀ m n → (number m) ⟦ / ⟧ (number n) ⟶ number (primFloatTimes m n) + * : ∀ m n → (number m) ⟦ * ⟧ (number n) ⟶ number (primFloatDiv m n) + < : ∀ m n → (number m) ⟦ < ⟧ (number n) ⟶ bool (primFloatLess m n) + > : ∀ m n → (number m) ⟦ > ⟧ (number n) ⟶ bool (primFloatLess n m) + <= : ∀ m n → (number m) ⟦ <= ⟧ (number n) ⟶ bool ((primFloatLess m n) or (primFloatEquality m n)) + >= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n)) + == : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w) + ~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w) + data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set 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} → + function : ∀ a {H H′ F B} → H′ ≡ H ⊕ a ↦ (function F is B end) → ------------------------------------------- - H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′ + H ⊢ (function F is B end) ⟶ᴱ val(addr a) ⊣ H′ app₁ : ∀ {H H′ M M′ N} → @@ -68,17 +55,18 @@ data _⊢_⟶ᴱ_⊣_ where ----------------------------- H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′ - app₂ : ∀ {H H′ V N N′} → + app₂ : ∀ v {H H′ N N′} → H ⊢ N ⟶ᴱ N′ ⊣ H′ → ----------------------------- - H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′ + H ⊢ (val v $ N) ⟶ᴱ (val v $ N′) ⊣ H′ - beta : ∀ {H a F B V} → - - H [ a ] ≡ just(function F is B end) → + beta : ∀ O v {H a F B} → + + (O ≡ function F is B end) → + H [ a ] ≡ just(O) → ----------------------------------------------------------------------------- - H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H + H ⊢ (val (addr a) $ val v) ⟶ᴱ (block (fun F) is (B [ v / name(arg F) ]ᴮ) end) ⊣ H block : ∀ {H H′ B B′ b} → @@ -86,44 +74,34 @@ data _⊢_⟶ᴱ_⊣_ where ---------------------------------------------------- H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′ - return : ∀ {H V B b} → - + return : ∀ v {H B b} → + -------------------------------------------------------- - H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H + H ⊢ (block b is return (val v) ∙ B end) ⟶ᴱ val v ⊣ H done : ∀ {H b} → - --------------------------------- - H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H - - binOpEquality : - ∀ {H x y} → - --------------------------------------------------------------------------- - H ⊢ (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H - - binOpInequality : - ∀ {H x y} → - ---------------------------------------------------------------------------- - H ⊢ (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H - - binOpNumbers : - ∀ {H x op y} → - ----------------------------------------------------------------------- - H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H + -------------------------------------------- + H ⊢ (block b is done end) ⟶ᴱ (val nil) ⊣ H - binOp₁ : - ∀ {H H′ x x′ op y} → + binOp₀ : ∀ {H op v₁ v₂ w} → + + v₁ ⟦ op ⟧ v₂ ⟶ w → + -------------------------------------------------- + H ⊢ (binexp (val v₁) op (val v₂)) ⟶ᴱ (val w) ⊣ H + + binOp₁ : ∀ {H H′ x x′ op y} → + H ⊢ x ⟶ᴱ x′ ⊣ H′ → --------------------------------------------- H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′ - binOp₂ : - ∀ {H H′ x op y y′} → + binOp₂ : ∀ {H H′ x op y y′} → + H ⊢ y ⟶ᴱ y′ ⊣ H′ → --------------------------------------------- H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′ - data _⊢_⟶ᴮ_⊣_ where local : ∀ {H H′ x M M′ B} → @@ -132,16 +110,16 @@ data _⊢_⟶ᴮ_⊣_ where ------------------------------------------------- H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′ - subst : ∀ {H x v B} → + subst : ∀ v {H x B} → ------------------------------------------------------ H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H - function : ∀ {H H′ a F B C} → + function : ∀ a {H H′ F B C} → H′ ≡ H ⊕ a ↦ (function F is C end) → -------------------------------------------------------------- - H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′ + H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / name(fun F) ]ᴮ) ⊣ H′ return : ∀ {H H′ M M′ B} → diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda index d84f75de4..bcd755782 100644 --- a/prototyping/Luau/Run.agda +++ b/prototyping/Luau/Run.agda @@ -1,15 +1,16 @@ +{-# OPTIONS --rewriting #-} + module Luau.Run where open import Agda.Builtin.Equality using (_≡_; refl) open import Luau.Heap using (Heap; ∅) -open import Luau.Syntax using (Block; return; _∙_; done) +open import Luau.Syntax using (Block; val; return; _∙_; done) open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step) -open import Luau.Value using (val) open import Properties.Step using (stepᴮ; step; return; done; error) open import Luau.RuntimeError using (RuntimeErrorᴮ) data RunResult {a} (H : Heap a) (B : Block a) : Set where - return : ∀ V {B′ H′} → (H ⊢ B ⟶* (return (val V) ∙ B′) ⊣ H′) → RunResult H B + return : ∀ v {B′ H′} → (H ⊢ B ⟶* (return (val v) ∙ B′) ⊣ H′) → RunResult H B done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda index b479a72a4..4440d2b7f 100644 --- a/prototyping/Luau/RuntimeError.agda +++ b/prototyping/Luau/RuntimeError.agda @@ -1,27 +1,40 @@ +{-# OPTIONS --rewriting #-} + module Luau.RuntimeError where open import Agda.Builtin.Equality using (_≡_) open import Luau.Heap using (Heap; _[_]) open import FFI.Data.Maybe using (just; nothing) open import FFI.Data.String using (String) -open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp) -open import Luau.RuntimeType using (RuntimeType; valueType) -open import Luau.Value using (val) +open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp; +; -; *; /; <; >; <=; >=) +open import Luau.RuntimeType using (RuntimeType; valueType; function; number) open import Properties.Equality using (_≢_) +data BinOpError : BinaryOperator → RuntimeType → Set where + + : ∀ {t} → (t ≢ number) → BinOpError + t + - : ∀ {t} → (t ≢ number) → BinOpError - t + * : ∀ {t} → (t ≢ number) → BinOpError * t + / : ∀ {t} → (t ≢ number) → BinOpError / t + < : ∀ {t} → (t ≢ number) → BinOpError < t + > : ∀ {t} → (t ≢ number) → BinOpError > t + <= : ∀ {t} → (t ≢ number) → BinOpError <= t + >= : ∀ {t} → (t ≢ number) → BinOpError >= t + data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set data RuntimeErrorᴱ H where - TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v) - UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x) - SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a) + FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w) + BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w)) + BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w)) + UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x) + SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (val (addr a)) app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N) app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N) - block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end) + block : ∀ {b B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end) bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N) bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N) data RuntimeErrorᴮ H where - local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B) + local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B) return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B) diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda index d5528c8b1..6a6ed3e28 100644 --- a/prototyping/Luau/RuntimeError/ToString.agda +++ b/prototyping/Luau/RuntimeError/ToString.agda @@ -1,27 +1,29 @@ +{-# OPTIONS --rewriting #-} + module Luau.RuntimeError.ToString where open import Agda.Builtin.Float using (primShowFloat) open import FFI.Data.String using (String; _++_) -open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂) +open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂) open import Luau.RuntimeType.ToString using (runtimeTypeToString) open import Luau.Addr.ToString using (addrToString) -open import Luau.Syntax.ToString using (exprToString) +open import Luau.Syntax.ToString using (valueToString; exprToString) open import Luau.Var.ToString using (varToString) -open import Luau.Value.ToString using (valueToString) -open import Luau.Syntax using (name; _$_) +open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_) -errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String -errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String +errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String +errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String -errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound" -errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated" -errToStringᴱ (app₁ E) = errToStringᴱ E -errToStringᴱ (app₂ E) = errToStringᴱ E -errToStringᴱ (bin₁ E) = errToStringᴱ E -errToStringᴱ (bin₂ E) = errToStringᴱ E -errToStringᴱ (block b E) = errToStringᴮ E ++ "\n in call of function " ++ varToString b -errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t +errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound" +errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is unallocated" +errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function" +errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E +errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E +errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number" +errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number" +errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E +errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E +errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n in call of function " ++ varToString (name b) -errToStringᴮ (local x E) = errToStringᴱ E ++ "\n in definition of " ++ varToString (name x) -errToStringᴮ (return E) = errToStringᴱ E ++ "\n in return statement" - +errToStringᴮ (local x ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n in definition of " ++ varToString (name x) +errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n in return statement" diff --git a/prototyping/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda index 375fc5402..f6b8b4a44 100644 --- a/prototyping/Luau/RuntimeType.agda +++ b/prototyping/Luau/RuntimeType.agda @@ -1,6 +1,6 @@ module Luau.RuntimeType where -open import Luau.Value using (Value; nil; addr; number; bool) +open import Luau.Syntax using (Value; nil; addr; number; bool) data RuntimeType : Set where function : RuntimeType @@ -10,6 +10,6 @@ data RuntimeType : Set where valueType : Value → RuntimeType valueType nil = nil -valueType (addr x) = function -valueType (number x) = number -valueType (bool _) = boolean +valueType (addr a) = function +valueType (number n) = number +valueType (bool b) = boolean diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda new file mode 100644 index 000000000..d7b2129fc --- /dev/null +++ b/prototyping/Luau/StrictMode.agda @@ -0,0 +1,205 @@ +{-# 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; _⇒_; 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) +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 BinOpWarning : BinaryOperator → Type → Set where + + : ∀ {T} → (T ≢ number) → BinOpWarning + T + - : ∀ {T} → (T ≢ number) → BinOpWarning - T + * : ∀ {T} → (T ≢ number) → BinOpWarning * T + / : ∀ {T} → (T ≢ number) → BinOpWarning / T + < : ∀ {T} → (T ≢ number) → BinOpWarning < T + > : ∀ {T} → (T ≢ number) → BinOpWarning > T + <= : ∀ {T} → (T ≢ number) → BinOpWarning <= T + >= : ∀ {T} → (T ≢ number) → BinOpWarning >= T + +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} → + + (src T ≢ U) → + ----------------- + 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} → + + BinOpWarning op T → + ------------------------------ + Warningᴱ H (binexp {op} D₁ D₂) + + BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} → + + BinOpWarning op U → + ------------------------------ + 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} → + + (U ≢ V) → + ------------------------- + 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} → + + (T ≢ U) → + ------------------------------ + 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} → + + (T ≢ U) → + -------------------- + 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} → + + (U ≢ V) → + ------------------------------------- + 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} → + + (U ≢ V) → + --------------------------------- + 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₂) diff --git a/prototyping/Luau/StrictMode/ToString.agda b/prototyping/Luau/StrictMode/ToString.agda new file mode 100644 index 000000000..ca55888c6 --- /dev/null +++ b/prototyping/Luau/StrictMode/ToString.agda @@ -0,0 +1,39 @@ +{-# OPTIONS --rewriting #-} + +module Luau.StrictMode.ToString where + +open import FFI.Data.String using (String; _++_) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr) +open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name) +open import Luau.Type using (strict) +open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_) +open import Luau.Addr.ToString using (addrToString) +open import Luau.Var.ToString using (varToString) +open import Luau.Type.ToString using (typeToString) +open import Luau.Syntax.ToString using (binOpToString) + +warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String +warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String + +warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x +warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a +warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U +warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W +warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W +warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V +warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n in function expression " ++ varToString f +warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) = "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U +warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n in block " ++ varToString b +warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T +warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U +warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W +warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W + +warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V +warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n in function declaration " ++ varToString f +warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W +warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) = "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U +warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n in local variable declaration " ++ varToString x +warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W +warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n in return statement" + diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda index d909c3509..883cc6380 100644 --- a/prototyping/Luau/Substitution.agda +++ b/prototyping/Luau/Substitution.agda @@ -1,7 +1,6 @@ module Luau.Substitution where -open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp) -open import Luau.Value using (Value; val) +open import Luau.Syntax using (Value; Expr; Stat; Block; val; nil; bool; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp) open import Luau.Var using (Var; _≡ⱽ_) open import Properties.Dec using (Dec; yes; no) @@ -10,18 +9,14 @@ _[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a _[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a -nil [ v / x ]ᴱ = nil -true [ v / x ]ᴱ = true -false [ v / x ]ᴱ = false +val w [ v / x ]ᴱ = val w var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y) -addr a [ v / x ]ᴱ = addr a -(number y) [ v / x ]ᴱ = number y (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ) function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end (binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ) -(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F)) +(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name(fun F))) (local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y)) (return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ) done [ v / x ]ᴮ = done diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 57e59a7e4..8be0830fa 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -1,11 +1,12 @@ module Luau.Syntax where open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.Bool using (Bool; true; false) open import Agda.Builtin.Float using (Float) -open import Properties.Dec using (⊥) open import Luau.Var using (Var) open import Luau.Addr using (Addr) open import Luau.Type using (Type) +open import FFI.Data.Maybe using (Maybe; just; nothing) infixr 5 _∙_ @@ -25,9 +26,9 @@ data FunDec : Annotated → Set where _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a _⟨_⟩ : Var → VarDec maybe → FunDec maybe -fun : ∀ {a} → FunDec a → Var -fun (f ⟨ x ⟩∈ T) = f -fun (f ⟨ x ⟩) = f +fun : ∀ {a} → FunDec a → VarDec a +fun (f ⟨ x ⟩∈ T) = (var f ∈ T) +fun (f ⟨ x ⟩) = (var f) arg : ∀ {a} → FunDec a → VarDec a arg (f ⟨ x ⟩∈ T) = x @@ -40,10 +41,16 @@ data BinaryOperator : Set where / : BinaryOperator < : BinaryOperator > : BinaryOperator - ≡ : BinaryOperator - ≅ : BinaryOperator - ≤ : BinaryOperator - ≥ : BinaryOperator + == : BinaryOperator + ~= : BinaryOperator + <= : BinaryOperator + >= : BinaryOperator + +data Value : Set where + nil : Value + addr : Addr → Value + number : Float → Value + bool : Bool → Value data Block (a : Annotated) : Set data Stat (a : Annotated) : Set @@ -59,13 +66,42 @@ data Stat a where return : Expr a → Stat a data Expr a where - nil : Expr a - true : Expr a - false : Expr a var : Var → Expr a - addr : Addr → Expr a + val : Value → Expr a _$_ : Expr a → Expr a → Expr a function_is_end : FunDec a → Block a → Expr a - block_is_end : Var → Block a → Expr a - number : Float → Expr a + block_is_end : VarDec a → Block a → Expr a binexp : Expr a → BinaryOperator → Expr a → Expr a + +isAnnotatedᴱ : ∀ {a} → Expr a → Maybe (Expr yes) +isAnnotatedᴮ : ∀ {a} → Block a → Maybe (Block yes) + +isAnnotatedᴱ (var x) = just (var x) +isAnnotatedᴱ (val v) = just (val v) +isAnnotatedᴱ (M $ N) with isAnnotatedᴱ M | isAnnotatedᴱ N +isAnnotatedᴱ (M $ N) | just M′ | just N′ = just (M′ $ N′) +isAnnotatedᴱ (M $ N) | _ | _ = nothing +isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) with isAnnotatedᴮ B +isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | just B′ = just (function f ⟨ var x ∈ T ⟩∈ U is B′ end) +isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | _ = nothing +isAnnotatedᴱ (function _ is B end) = nothing +isAnnotatedᴱ (block var b ∈ T is B end) with isAnnotatedᴮ B +isAnnotatedᴱ (block var b ∈ T is B end) | just B′ = just (block var b ∈ T is B′ end) +isAnnotatedᴱ (block var b ∈ T is B end) | _ = nothing +isAnnotatedᴱ (block _ is B end) = nothing +isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N +isAnnotatedᴱ (binexp M op N) | just M′ | just N′ = just (binexp M′ op N′) +isAnnotatedᴱ (binexp M op N) | _ | _ = nothing + +isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with isAnnotatedᴮ B | isAnnotatedᴮ C +isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | just B′ | just C′ = just (function f ⟨ var x ∈ T ⟩∈ U is C′ end ∙ B′) +isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | _ | _ = nothing +isAnnotatedᴮ (function _ is C end ∙ B) = nothing +isAnnotatedᴮ (local var x ∈ T ← M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B +isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | just M′ | just B′ = just (local var x ∈ T ← M′ ∙ B′) +isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | _ | _ = nothing +isAnnotatedᴮ (local _ ← M ∙ B) = nothing +isAnnotatedᴮ (return M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B +isAnnotatedᴮ (return M ∙ B) | just M′ | just B′ = just (return M′ ∙ B′) +isAnnotatedᴮ (return M ∙ B) | _ | _ = nothing +isAnnotatedᴮ done = just done diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda index 330739b9c..a727a5b07 100644 --- a/prototyping/Luau/Syntax/FromJSON.agda +++ b/prototyping/Luau/Syntax/FromJSON.agda @@ -1,6 +1,8 @@ +{-# OPTIONS --rewriting #-} + module Luau.Syntax.FromJSON where -open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /; ≡; ≅; <; >; ≤; ≥) +open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=) open import Luau.Type.FromJSON using (typeFromJSON) open import Agda.Builtin.List using (List; _∷_; []) @@ -26,6 +28,8 @@ vars = fromString "vars" op = fromString "op" left = fromString "left" right = fromString "right" +returnAnnotation = fromString "returnAnnotation" +types = fromString "types" data Lookup : Set where _,_ : String → Value → Lookup @@ -49,22 +53,22 @@ blockFromJSON : Value → Either String (Block maybe) blockFromArray : Array → Either String (Block maybe) binOpFromJSON (string s) = binOpFromString s -binOpFromJSON val = Left "Binary operator not a string" +binOpFromJSON _ = Left "Binary operator not a string" binOpFromString "Add" = Right + binOpFromString "Sub" = Right - binOpFromString "Mul" = Right * binOpFromString "Div" = Right / -binOpFromString "CompareEq" = Right ≡ -binOpFromString "CompareNe" = Right ≅ +binOpFromString "CompareEq" = Right == +binOpFromString "CompareNe" = Right ~= binOpFromString "CompareLt" = Right < -binOpFromString "CompareLe" = Right ≤ +binOpFromString "CompareLe" = Right <= binOpFromString "CompareGt" = Right > -binOpFromString "CompareGe" = Right ≥ +binOpFromString "CompareGe" = Right >= binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator") varDecFromJSON (object arg) = varDecFromObject arg -varDecFromJSON val = Left "VarDec not an object" +varDecFromJSON _ = Left "VarDec not an object" varDecFromObject obj with lookup name obj | lookup type obj varDecFromObject obj | just (string name) | nothing = Right (var name) @@ -76,7 +80,7 @@ varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string" varDecFromObject obj | nothing | _ = Left "AstLocal missing name" exprFromJSON (object obj) = exprFromObject obj -exprFromJSON val = Left "AstExpr not an object" +exprFromJSON _ = Left "AstExpr not an object" exprFromObject obj with lookup type obj exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj @@ -89,29 +93,37 @@ exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array") exprFromObject obj | just (string "AstExprCall") | nothing | _ = Left ("AstExprCall missing func") exprFromObject obj | just (string "AstExprCall") | _ | nothing = Left ("AstExprCall missing args") -exprFromObject obj | just (string "AstExprConstantNil") = Right nil -exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue with head arr | blockFromJSON blockValue -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end) -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args" -exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | Left err = Left err -exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array" -exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args" -exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body" +exprFromObject obj | just (string "AstExprConstantNil") = Right (val nil) +exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj | lookup returnAnnotation obj +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn with head arr | blockFromJSON blockValue +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B with varDecFromJSON argValue +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg with lookup types rtnObj +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) with head rtnTypes +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType with typeFromJSON rtnType +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Left err = Left err +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | just rtnType | Right T = Right (function "" ⟨ arg ⟩∈ T is B end) +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just (array rtnTypes) | nothing = Right (function "" ⟨ arg ⟩ is B end) +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | just _ = Left "returnAnnotation types not an array" +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just (object rtnObj) | just argValue | Right B | Right arg | nothing = Left "returnAnnotation missing types" +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just _ | just argValue | Right B | Right arg = Left "returnAnnotation not an object" +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end) +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | just argValue | Right B | Left err = Left err +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | nothing | Right B = Left "Unsupported AstExprFunction empty args" +exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | rtn | _ | Left err = Left err +exprFromObject obj | just (string "AstExprFunction") | just _ | just _ | rtn = Left "AstExprFunction args not an array" +exprFromObject obj | just (string "AstExprFunction") | nothing | _ | rtn = Left "AstExprFunction missing args" +exprFromObject obj | just (string "AstExprFunction") | _ | nothing | rtn = Left "AstExprFunction missing body" exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′)) exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local" exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj -exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x)) +exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (val (number (toFloat x))) exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number" exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value" exprFromObject obj | just (string "AstExprConstantBool") with lookup value obj -exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true -exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false +exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool b) = Right (val (bool b)) exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool" exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool missing value" exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj @@ -147,6 +159,7 @@ statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLo statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩ is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩ is B end) +statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩∈ T is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩∈ T is B end) statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction" @@ -180,4 +193,4 @@ blockFromArray arr | just value | Left err = Left err blockFromArray arr | just value | Right S with blockFromArray(tail arr) blockFromArray arr | just value | Right S | Left err = Left (err) blockFromArray arr | just value | Right S | Right B = Right (S ∙ B) - \ No newline at end of file + diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda index 58a784bf1..60ec471d0 100644 --- a/prototyping/Luau/Syntax/ToString.agda +++ b/prototyping/Luau/Syntax/ToString.agda @@ -1,7 +1,8 @@ module Luau.Syntax.ToString where +open import Agda.Builtin.Bool using (true; false) open import Agda.Builtin.Float using (primShowFloat) -open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; binexp; true; false) +open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; binexp) open import FFI.Data.String using (String; _++_) open import Luau.Addr.ToString using (addrToString) open import Luau.Type.ToString using (typeToString) @@ -24,19 +25,24 @@ binOpToString * = "*" binOpToString / = "/" binOpToString < = "<" binOpToString > = ">" -binOpToString ≡ = "==" -binOpToString ≅ = "~=" -binOpToString ≤ = "<=" -binOpToString ≥ = ">=" +binOpToString == = "==" +binOpToString ~= = "~=" +binOpToString <= = "<=" +binOpToString >= = ">=" + +valueToString : Value → String +valueToString nil = "nil" +valueToString (addr a) = addrToString a +valueToString (number x) = primShowFloat x +valueToString (bool false) = "false" +valueToString (bool true) = "true" exprToString′ : ∀ {a} → String → Expr a → String statToString′ : ∀ {a} → String → Stat a → String blockToString′ : ∀ {a} → String → Block a → String -exprToString′ lb nil = - "nil" -exprToString′ lb (addr a) = - addrToString(a) +exprToString′ lb (val v) = + valueToString(v) exprToString′ lb (var x) = varToString(x) exprToString′ lb (M $ N) = @@ -46,13 +52,10 @@ exprToString′ lb (function F is B end) = " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end" exprToString′ lb (block b is B end) = - "(" ++ b ++ "()" ++ lb ++ + "(" ++ varDecToString b ++ "()" ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ "end)()" -exprToString′ lb (number x) = primShowFloat x exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y -exprToString′ lb true = "true" -exprToString′ lb false = "false" statToString′ lb (function F is B end) = "local " ++ funDecToString F ++ lb ++ diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index af5f857cb..10f39c449 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -1,5 +1,9 @@ module Luau.Type where +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) open import FFI.Data.Maybe using (Maybe; just; nothing) data Type : Set where @@ -7,18 +11,132 @@ data Type : Set where _⇒_ : Type → Type → Type none : Type any : Type + boolean : Type number : Type _∪_ : Type → Type → Type _∩_ : Type → Type → Type -src : Type → Type -src nil = none -src (S ⇒ T) = S -src none = none -src any = any -src number = none -src (S ∪ T) = (src S) ∪ (src T) -src (S ∩ T) = (src S) ∩ (src T) +lhs : Type → Type +lhs (T ⇒ _) = T +lhs (T ∪ _) = T +lhs (T ∩ _) = T +lhs nil = nil +lhs none = none +lhs any = any +lhs number = number +lhs boolean = boolean + +rhs : Type → Type +rhs (_ ⇒ T) = T +rhs (_ ∪ T) = T +rhs (_ ∩ T) = T +rhs nil = nil +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 ≡ᵀ none = no (λ ()) +nil ≡ᵀ any = no (λ ()) +nil ≡ᵀ number = no (λ ()) +nil ≡ᵀ boolean = 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) ≡ᵀ none = no (λ ()) +(S ⇒ T) ≡ᵀ any = no (λ ()) +(S ⇒ T) ≡ᵀ number = no (λ ()) +(S ⇒ T) ≡ᵀ boolean = no (λ ()) +(S ⇒ T) ≡ᵀ (U ∪ V) = no (λ ()) +(S ⇒ T) ≡ᵀ (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 ≡ᵀ 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 ≡ᵀ 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) ≡ᵀ none = no (λ ()) +(S ∪ T) ≡ᵀ any = no (λ ()) +(S ∪ T) ≡ᵀ number = no (λ ()) +(S ∪ T) ≡ᵀ boolean = 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) ≡ᵀ none = no (λ ()) +(S ∩ T) ≡ᵀ any = no (λ ()) +(S ∩ T) ≡ᵀ number = no (λ ()) +(S ∩ T) ≡ᵀ boolean = 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 + +src : Mode → Type → Type +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 none = any +src nonstrict none = none +src strict any = none +src nonstrict any = any tgt : Type → Type tgt nil = none @@ -26,6 +144,7 @@ tgt (S ⇒ T) = T 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 49f746264..9057fef4e 100644 --- a/prototyping/Luau/Type/FromJSON.agda +++ b/prototyping/Luau/Type/FromJSON.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Luau.Type.FromJSON where open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number) diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index e7a7c1c07..dec7c14cd 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; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional) +open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; _∪_; _∩_; normalizeOptional) {-# TERMINATING #-} typeToString : Type → String @@ -13,6 +13,7 @@ typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T) typeToString none = "none" typeToString any = "any" typeToString number = "number" +typeToString boolean = "boolean" typeToString (S ∪ T) with normalizeOptional(S ∪ T) typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?" typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda new file mode 100644 index 000000000..f240e17e7 --- /dev/null +++ b/prototyping/Luau/TypeCheck.agda @@ -0,0 +1,143 @@ +{-# OPTIONS --rewriting #-} + +open import Luau.Type using (Mode) + +module Luau.TypeCheck (m : Mode) where + +open import Agda.Builtin.Equality using (_≡_) +open import FFI.Data.Maybe using (Maybe; just) +open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=) +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; 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) +open import Properties.Product using (_×_; _,_) + +src : Type → Type +src = Luau.Type.src m + +orNone : Maybe Type → Type +orNone nothing = none +orNone (just T) = T + +tgtBinOp : BinaryOperator → Type +tgtBinOp + = number +tgtBinOp - = number +tgtBinOp * = number +tgtBinOp / = number +tgtBinOp < = boolean +tgtBinOp > = boolean +tgtBinOp == = boolean +tgtBinOp ~= = boolean +tgtBinOp <= = boolean +tgtBinOp >= = boolean + +data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set +data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set + +data _⊢ᴮ_∈_ where + + done : ∀ {Γ} → + + --------------- + Γ ⊢ᴮ done ∈ nil + + return : ∀ {M B T U Γ} → + + Γ ⊢ᴱ M ∈ T → + Γ ⊢ᴮ B ∈ U → + --------------------- + Γ ⊢ᴮ return M ∙ B ∈ T + + local : ∀ {x M B T U V Γ} → + + Γ ⊢ᴱ M ∈ U → + (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V → + -------------------------------- + Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V + + function : ∀ {f x B C T U V W Γ} → + + (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V → + (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W → + ------------------------------------------------- + Γ ⊢ᴮ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W + +data _⊢ᴱ_∈_ where + + nil : ∀ {Γ} → + + -------------------- + Γ ⊢ᴱ (val nil) ∈ nil + + var : ∀ {x T Γ} → + + T ≡ orNone(Γ [ x ]ⱽ) → + ---------------- + Γ ⊢ᴱ (var x) ∈ T + + addr : ∀ {a Γ} T → + + ----------------- + Γ ⊢ᴱ val(addr a) ∈ T + + number : ∀ {n Γ} → + + --------------------------- + Γ ⊢ᴱ val(number n) ∈ number + + bool : ∀ {b Γ} → + + -------------------------- + Γ ⊢ᴱ val(bool b) ∈ boolean + + app : ∀ {M N T U Γ} → + + Γ ⊢ᴱ M ∈ T → + Γ ⊢ᴱ N ∈ U → + ---------------------- + Γ ⊢ᴱ (M $ N) ∈ (tgt T) + + function : ∀ {f x B T U V Γ} → + + (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V → + ----------------------------------------------------- + Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) + + block : ∀ {b B T U Γ} → + + Γ ⊢ᴮ B ∈ U → + ------------------------------------ + Γ ⊢ᴱ (block var b ∈ T is B end) ∈ T + + binexp : ∀ {op Γ M N T U} → + + Γ ⊢ᴱ M ∈ T → + Γ ⊢ᴱ N ∈ U → + ---------------------------------- + Γ ⊢ᴱ (binexp M op N) ∈ tgtBinOp op + +data ⊢ᴼ_ : Maybe(Object yes) → Set where + + nothing : + + --------- + ⊢ᴼ nothing + + function : ∀ {f x T U V B} → + + (x ↦ T) ⊢ᴮ B ∈ V → + ---------------------------------------------- + ⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end) + +⊢ᴴ_ : Heap yes → Set +⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O) + +_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set +(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T) + +_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set +(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T) diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda deleted file mode 100644 index ed51abd74..000000000 --- a/prototyping/Luau/Value.agda +++ /dev/null @@ -1,20 +0,0 @@ -module Luau.Value where - -open import Agda.Builtin.Bool using (Bool; true; false) -open import Agda.Builtin.Float using (Float) -open import Luau.Addr using (Addr) -open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false) -open import Luau.Var using (Var) - -data Value : Set where - nil : Value - addr : Addr → Value - number : Float → Value - bool : Bool → Value - -val : ∀ {a} → Value → Expr a -val nil = nil -val (addr a) = addr a -val (number x) = number x -val (bool false) = false -val (bool true) = true diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda deleted file mode 100644 index 3421d4cd7..000000000 --- a/prototyping/Luau/Value/ToString.agda +++ /dev/null @@ -1,14 +0,0 @@ -module Luau.Value.ToString where - -open import Agda.Builtin.String using (String) -open import Agda.Builtin.Float using (primShowFloat) -open import Agda.Builtin.Bool using (true; false) -open import Luau.Value using (Value; nil; addr; number; bool) -open import Luau.Addr.ToString using (addrToString) - -valueToString : Value → String -valueToString nil = "nil" -valueToString (addr a) = addrToString a -valueToString (number x) = primShowFloat x -valueToString (bool false) = "false" -valueToString (bool true) = "true" diff --git a/prototyping/Luau/Var.agda b/prototyping/Luau/Var.agda index 091ce125d..23d8b56e3 100644 --- a/prototyping/Luau/Var.agda +++ b/prototyping/Luau/Var.agda @@ -4,13 +4,13 @@ open import Agda.Builtin.Bool using (true; false) open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.String using (String; primStringEquality) open import Agda.Builtin.TrustMe using (primTrustMe) -open import Properties.Dec using (Dec; yes; no; ⊥) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Equality using (_≢_) Var : Set Var = String _≡ⱽ_ : (a b : Var) → Dec (a ≡ b) a ≡ⱽ b with primStringEquality a b -a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ⱽ b | false = no p where postulate p : (a ≢ b) a ≡ⱽ b | true = yes primTrustMe - diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda new file mode 100644 index 000000000..76f64dfe3 --- /dev/null +++ b/prototyping/Luau/VarCtxt.agda @@ -0,0 +1,43 @@ +{-# OPTIONS --rewriting #-} + +module Luau.VarCtxt where + +open import Agda.Builtin.Equality using (_≡_) +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) +open import Properties.Equality using (_≢_; cong; sym; trans) + +VarCtxt : Set +VarCtxt = KeyMap Type + +∅ : VarCtxt +∅ = empty + +_⋒_ : VarCtxt → VarCtxt → VarCtxt +_⋒_ = unionWith _∩_ + +_⋓_ : VarCtxt → VarCtxt → VarCtxt +_⋓_ = unionWith _∪_ + +_[_] : VarCtxt → Var → Maybe Type +Γ [ x ] = lookup (fromString x) Γ + +_⊝_ : VarCtxt → Var → VarCtxt +Γ ⊝ x = delete (fromString x) Γ + +_↦_ : Var → Type → VarCtxt +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/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda index fdad32d6a..3ce0905b5 100644 --- a/prototyping/PrettyPrinter.agda +++ b/prototyping/PrettyPrinter.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module PrettyPrinter where open import Agda.Builtin.IO using (IO) diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 1a6f92fab..8b30ce121 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -1,7 +1,11 @@ +{-# OPTIONS --rewriting #-} + module Properties where import Properties.Contradiction import Properties.Dec import Properties.Equality -import Properties.Step import Properties.Remember +import Properties.Step +import Properties.StrictMode +import Properties.TypeCheck diff --git a/prototyping/Properties/Dec.agda b/prototyping/Properties/Dec.agda index d89fd754e..c61f23659 100644 --- a/prototyping/Properties/Dec.agda +++ b/prototyping/Properties/Dec.agda @@ -1,8 +1,7 @@ module Properties.Dec where -data ⊥ : Set where +open import Properties.Contradiction using (¬) data Dec(A : Set) : Set where yes : A → Dec A - no : (A → ⊥) → Dec A - + no : ¬ A → Dec A diff --git a/prototyping/Properties/Product.agda b/prototyping/Properties/Product.agda new file mode 100644 index 000000000..0d41c817c --- /dev/null +++ b/prototyping/Properties/Product.agda @@ -0,0 +1,14 @@ +module Properties.Product where + +infixr 5 _×_ _,_ + +record Σ {A : Set} (B : A → Set) : Set where + + constructor _,_ + field fst : A + field snd : B fst + +open Σ public + +_×_ : Set → Set → Set +A × B = Σ (λ (a : A) → B) diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 69dbac846..0b5fd062a 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -1,24 +1,91 @@ +{-# OPTIONS --rewriting #-} + module Properties.Step where open import Agda.Builtin.Equality using (_≡_; refl) -open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv) +open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess) 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; addr; true; false; 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; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality) -open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂) -open import Luau.RuntimeType using (function; number) +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; 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 (_[_/_]ᴮ) -open import Luau.Value using (nil; addr; val; number; bool) open import Properties.Remember using (remember; _,_) +open import Utility.Bool using (not; _or_) + +data BinOpStepResult v op w : Set where + step : ∀ x → (v ⟦ op ⟧ w ⟶ x) → BinOpStepResult v op w + error₁ : BinOpError op (valueType(v)) → BinOpStepResult v op w + error₂ : BinOpError op (valueType(w)) → BinOpStepResult v op w + +binOpStep : ∀ v op w → BinOpStepResult v op w +binOpStep nil + w = error₁ (+ (λ ())) +binOpStep (addr a) + w = error₁ (+ (λ ())) +binOpStep (number m) + nil = error₂ (+ (λ ())) +binOpStep (number m) + (addr a) = error₂ (+ (λ ())) +binOpStep (number m) + (number n) = step (number (primFloatPlus m n)) (+ m n) +binOpStep (number m) + (bool b) = error₂ (+ (λ ())) +binOpStep (bool b) + w = error₁ (+ (λ ())) +binOpStep nil - w = error₁ (- (λ ())) +binOpStep (addr a) - w = error₁ (- (λ ())) +binOpStep (number x) - nil = error₂ (- (λ ())) +binOpStep (number x) - (addr a) = error₂ (- (λ ())) +binOpStep (number x) - (number n) = step (number (primFloatMinus x n)) (- x n) +binOpStep (number x) - (bool b) = error₂ (- (λ ())) +binOpStep (bool b) - w = error₁ (- (λ ())) +binOpStep nil * w = error₁ (* (λ ())) +binOpStep (addr a) * w = error₁ (* (λ ())) +binOpStep (number m) * nil = error₂ (* (λ ())) +binOpStep (number m) * (addr a) = error₂ (* (λ ())) +binOpStep (number m) * (number n) = step (number (primFloatDiv m n)) (* m n) +binOpStep (number m) * (bool b) = error₂ (* (λ ())) +binOpStep (bool b) * w = error₁ (* (λ ())) +binOpStep nil / w = error₁ (/ (λ ())) +binOpStep (addr a) / w = error₁ (/ (λ ())) +binOpStep (number m) / nil = error₂ (/ (λ ())) +binOpStep (number m) / (addr a) = error₂ (/ (λ ())) +binOpStep (number m) / (number n) = step (number (primFloatTimes m n)) (/ m n) +binOpStep (number m) / (bool b) = error₂ (/ (λ ())) +binOpStep (bool b) / w = error₁ (/ (λ ())) +binOpStep nil < w = error₁ (< (λ ())) +binOpStep (addr a) < w = error₁ (< (λ ())) +binOpStep (number m) < nil = error₂ (< (λ ())) +binOpStep (number m) < (addr a) = error₂ (< (λ ())) +binOpStep (number m) < (number n) = step (bool (primFloatLess m n)) (< m n) +binOpStep (number m) < (bool b) = error₂ (< (λ ())) +binOpStep (bool b) < w = error₁ (< (λ ())) +binOpStep nil > w = error₁ (> (λ ())) +binOpStep (addr a) > w = error₁ (> (λ ())) +binOpStep (number m) > nil = error₂ (> (λ ())) +binOpStep (number m) > (addr a) = error₂ (> (λ ())) +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 (evalNeqOp v w)) (~= v w) +binOpStep nil <= w = error₁ (<= (λ ())) +binOpStep (addr a) <= w = error₁ (<= (λ ())) +binOpStep (number m) <= nil = error₂ (<= (λ ())) +binOpStep (number m) <= (addr a) = error₂ (<= (λ ())) +binOpStep (number m) <= (number n) = step (bool (primFloatLess m n or primFloatEquality m n)) (<= m n) +binOpStep (number m) <= (bool b) = error₂ (<= (λ ())) +binOpStep (bool b) <= w = error₁ (<= (λ ())) +binOpStep nil >= w = error₁ (>= (λ ())) +binOpStep (addr a) >= w = error₁ (>= (λ ())) +binOpStep (number m) >= nil = error₂ (>= (λ ())) +binOpStep (number m) >= (addr a) = error₂ (>= (λ ())) +binOpStep (number m) >= (number n) = step (bool (primFloatLess n m or primFloatEquality m n)) (>= m n) +binOpStep (number m) >= (bool b) = error₂ (>= (λ ())) +binOpStep (bool b) >= w = error₁ (>= (λ ())) data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set data StepResultᴮ H B where step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B - return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B + return : ∀ v {B′} → (B ≡ (return (val v) ∙ B′)) → StepResultᴮ H B done : (B ≡ done) → StepResultᴮ H B error : (RuntimeErrorᴮ H B) → StepResultᴮ H B @@ -30,54 +97,44 @@ data StepResultᴱ H M where stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B -stepᴱ H nil = value nil refl -stepᴱ H (var x) = error (UnboundVariable x) -stepᴱ H (addr a) = value (addr a) refl -stepᴱ H (number x) = value (number x) refl -stepᴱ H (true) = value (bool true) refl -stepᴱ H (false) = value (bool false) refl +stepᴱ H (val v) = value v refl +stepᴱ H (var x) = error UnboundVariable stepᴱ H (M $ N) with stepᴱ H M stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D) -stepᴱ H (_ $ N) | value V refl with stepᴱ H N -stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s) -stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ())) -stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ())) -stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ())) -stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ]) -stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (nothing , p) = error (app₁ (SEGV a p)) -stepᴱ H (_ $ _) | value (addr a) refl | value W refl | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p) +stepᴱ H (_ $ N) | value v refl with stepᴱ H N +stepᴱ H (_ $ N) | value v refl | step H′ N′ s = step H′ (val v $ N′) (app₂ v s) +stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ]) +stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV p)) +stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p) +stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ())) +stepᴱ H (_ $ _) | value (number m) refl | value w refl = error (FunctionMismatch (number m) w (λ ())) +stepᴱ H (_ $ _) | value (bool b) refl | value w refl = error (FunctionMismatch (bool b) w (λ ())) stepᴱ H (M $ N) | value V p | error E = error (app₂ E) 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 done end) | done refl = step H nil done -stepᴱ H (block b is B end) | error E = error (block b E) +stepᴱ H (block b is (return _ ∙ B′) end) | return v refl = step H (val v) (return v) +stepᴱ H (block b is done end) | done refl = step H (val nil) done +stepᴱ H (block b is B end) | error E = error (block E) stepᴱ H (function F is C end) with alloc H (function F is C end) -stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p) -stepᴱ H (binexp x op y) with stepᴱ H x -stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y --- Have to use explicit form for ≡ here because it's a heavily overloaded symbol -stepᴱ H (binexp x Luau.Syntax.≡ y) | value x′ refl | value y′ refl = step H (val (evalEqOp x′ y′)) binOpEquality -stepᴱ H (binexp x ≅ y) | value x′ refl | value y′ refl = step H (val (evalNeqOp x′ y′)) binOpInequality -stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (val (evalNumOp x′ op y′)) binOpNumbers -stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s) -stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E) -stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ())) -stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ())) -stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ())) -stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ())) -stepᴱ H (binexp x op y) | value (bool x′) refl | _ = error (bin₁ (TypeMismatch number (bool x′) λ())) -stepᴱ H (binexp x op y) | _ | value (bool y′) refl = error (bin₂ (TypeMismatch number (bool y′) λ())) -stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s) -stepᴱ H (binexp x op y) | error E = error (bin₁ E) +stepᴱ H function F is C end | ok a H′ p = step H′ (val (addr a)) (function a p) +stepᴱ H (binexp M op N) with stepᴱ H M +stepᴱ H (binexp M op N) | step H′ M′ s = step H′ (binexp M′ op N) (binOp₁ s) +stepᴱ H (binexp M op N) | error E = error (bin₁ E) +stepᴱ H (binexp M op N) | value v refl with stepᴱ H N +stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s) +stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E) +stepᴱ H (binexp M op N) | value v refl | value w refl with binOpStep v op w +stepᴱ H (binexp M op N) | value v refl | value w refl | step x p = step H (val x) (binOp₀ p) +stepᴱ H (binexp M op N) | value v refl | value w refl | error₁ E = error (BinOpMismatch₁ v w E) +stepᴱ H (binexp M op N) | value v refl | value w refl | error₂ E = error (BinOpMismatch₂ v w E) stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end) -stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p) +stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / name (fun F) ]ᴮ) (function a p) stepᴮ H (local x ← M ∙ B) with stepᴱ H M stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D) -stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst -stepᴮ H (local x ← M ∙ B) | error E = error (local x E) +stepᴮ H (local x ← _ ∙ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v) +stepᴮ H (local x ← M ∙ B) | error E = error (local E) stepᴮ H (return M ∙ B) with stepᴱ H M stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D) stepᴮ H (return _ ∙ B) | value V refl = return V refl diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda new file mode 100644 index 000000000..084111886 --- /dev/null +++ b/prototyping/Properties/StrictMode.agda @@ -0,0 +1,470 @@ +{-# OPTIONS --rewriting #-} + +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; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ) +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; _⇒_; 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 _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅) +open import Properties.Remember using (remember; _,_) +open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Contradiction using (CONTRADICTION) +open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber) +open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=) +open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=) +open import Luau.RuntimeType using (valueType) + +src = Luau.Type.src strict + +data _⊑_ (H : Heap yes) : Heap yes → Set where + refl : (H ⊑ H) + snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′) + +rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′) +rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′) + +rednᴱ⊑ (function a p) = snoc p +rednᴱ⊑ (app₁ s) = rednᴱ⊑ s +rednᴱ⊑ (app₂ p s) = rednᴱ⊑ s +rednᴱ⊑ (beta O v p q) = refl +rednᴱ⊑ (block s) = rednᴮ⊑ s +rednᴱ⊑ (return v) = refl +rednᴱ⊑ done = refl +rednᴱ⊑ (binOp₀ p) = refl +rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s +rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s + +rednᴮ⊑ (local s) = rednᴱ⊑ s +rednᴮ⊑ (subst v) = refl +rednᴮ⊑ (function a 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-⊑-nothing : ∀ {H H′} a → (H ⊑ H′) → (H′ [ a ]ᴴ ≡ nothing) → (H [ a ]ᴴ ≡ 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 + warning : Warningᴱ H D → OrWarningᴱ H D A + +data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B ∈ T) A : Set where + ok : A → OrWarningᴮ H D A + warning : Warningᴮ H D → OrWarningᴮ H D A + +data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H ▷ M ∈ T) A : Set where + ok : A → OrWarningᴴᴱ H D A + warning : Warningᴴᴱ H D → OrWarningᴴᴱ H D A + +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 + +heap-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M) +heap-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B) + +heap-weakeningᴱ H (var x) h = ok refl +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 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 +heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h +heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p) +heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W) +heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl +heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl +heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h +heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p +heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W) +heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h +heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p +heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W) +heap-weakeningᴮ H (return M ∙ B) h with heap-weakeningᴱ H M h +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 + +none-not-obj : ∀ O → none ≢ typeOfᴼ O +none-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () + +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))) +substitutivityᴱ-whenever-no : ∀ {Γ 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 (no p))) +substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ)) +substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p))) +substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p))) + +substitutivityᴱ H (var y) v x p with x ≡ⱽ y +substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p +substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p +substitutivityᴱ H (val w) v x p = refl +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 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) +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q) +substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x y q p (⊕-swap q) +substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p +substitutivityᴮ H done v x p = refl +substitutivityᴮ-unless-yes H B v x x refl q refl = refl +substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q + +binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x)) +binOpPreservation H (+ m n) = refl +binOpPreservation H (- m n) = refl +binOpPreservation H (/ m n) = refl +binOpPreservation H (* m n) = refl +binOpPreservation H (< m n) = refl +binOpPreservation H (> m n) = refl +binOpPreservation H (<= m n) = refl +binOpPreservation H (>= m n) = refl +binOpPreservation H (== v w) = refl +binOpPreservation H (~= v w) = refl + +preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′) +preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′) + +preservationᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = ok refl +preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s +preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p) +preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W)) +preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W) +preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s) +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 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 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) +preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p +preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (BlockMismatch p)) +preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil +preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p +preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (BlockMismatch p)) +preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s) +preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl +preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl + +preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s) +preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p +preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W)) +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 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)) +preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W)) +preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s +preservationᴮ H (return M ∙ B) (return s) | ok p = ok p +preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W)) +preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W) + +reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M) +reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) +reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y)) +reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) +reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B) + +reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y +reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W +reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W +reflect-substitutionᴱ H (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r +reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p)))) +reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W) +reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r)))) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r)))) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) +reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) +reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r → q (trans r (substitutivityᴮ H B v x p))) +reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W) +reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₁ q) = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q) +reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q) +reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W) +reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W) + +reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r) +reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q) +reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | () + +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r)))) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r)))) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W) +reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r → q (trans r (substitutivityᴱ H M v x p))) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W) +reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W) +reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W) + +reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W +reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W + +reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M) +reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B) + +reflect-weakeningᴱ H (var x) h (UnboundVariable p) = (UnboundVariable p) +reflect-weakeningᴱ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p) +reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h +reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r → p (trans (cong src (sym q₁)) (trans r q₂))) +reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W +reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W +reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W) +reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W) +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) with heap-weakeningᴱ H M h +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p) +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p) +reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | warning W = bin₂ W +reflect-weakeningᴱ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ H M h W′) +reflect-weakeningᴱ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ H N h W′) +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W +reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W) +reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h +reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r → p (trans r q)) +reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | warning W = block₁ W +reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W) + +reflect-weakeningᴮ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ H M h W) +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) with heap-weakeningᴱ H M h +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r → p (trans r q)) +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | warning W = local₁ W +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W) +reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | warning W = function₁ W +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W) +reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W) + +reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O) +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q)) +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W +reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′) + +reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) +reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) + +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p (trans (trans (cong src (sym q)) r) q′))) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W) +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W +reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W = expr (app₂ W) +reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′ +reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W +reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W) +reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′)) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p′ (trans (trans (cong src (sym q)) r) q′))) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | warning W | _ = expr (app₁ W) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (expr W) = expr (app₂ W) +reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (heap W) = heap W +reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′)) +reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′ +reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W +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 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 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))) +reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W +reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W) +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′ +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W +reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W) +reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′)) +reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ()) +reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p) +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) with preservationᴱ H M s +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)) +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W) +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s) +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p))) +reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W) +reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M s W′ +reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | heap W = heap W +reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | expr W = expr (bin₁ W) +reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′)) +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s) +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)) +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W) +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)) +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W +reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W) +reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′)) +reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W′ +reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W +reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W) + +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) with preservationᴱ H M s +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r → p (trans r q))) +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W) +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with reflectᴱ H M s W′ +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W) +reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′)) +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 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′ +reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W +reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return W) + +reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴᴱ H′ (typeCheckᴴᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M) +reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) + +reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′ +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q → p (trans q r)) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′)) +reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) +reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′) +reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W +reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W) +reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′) +reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W +reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W) +reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′ +reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′) +reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W +reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W) +reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′ +reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′ +reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W′) = heap W′ +reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′) +reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W +reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W) +reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′) +reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W +reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W) + +reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′ +reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′) +reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W = heap W +reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W) +reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′ +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q → p (trans q r))) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′)) +reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′)) +reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′) +reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W +reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | expr W = block (return W) + +reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) +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 (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)) +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)) +runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q)) +runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q)) + +runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M) +runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B) + +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-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) +runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err) +runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err) +runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₁ v w p) = BinOpMismatch₁ (runtimeBinOpWarning H v p) +runtimeWarningᴱ H (binexp M op N) (BinOpMismatch₂ v w p) = BinOpMismatch₂ (runtimeBinOpWarning H w p) +runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err) +runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err) + +runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err) +runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err) + +wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B) +wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H′ B′ err)) +wellTypedProgramsDontGoWrong H′ B B′ t err | heap (addr a refl ()) +wellTypedProgramsDontGoWrong H′ B B′ t err | block W = W diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda new file mode 100644 index 000000000..c144bc12b --- /dev/null +++ b/prototyping/Properties/TypeCheck.agda @@ -0,0 +1,103 @@ +{-# OPTIONS --rewriting #-} + +open import Luau.Type using (Mode) + +module Properties.TypeCheck (m : Mode) where + +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; 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; 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) +open import Luau.Var using (Var; _≡ⱽ_) +open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ) +open import Properties.Contradiction using (CONTRADICTION) +open import Properties.Dec using (yes; no) +open import Properties.Equality using (_≢_; sym; trans; cong) +open import Properties.Product using (_×_; _,_) +open import Properties.Remember using (Remember; remember; _,_) + +src : Type → Type +src = Luau.Type.src m + +typeOfᴼ : Object yes → Type +typeOfᴼ (function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T) + +typeOfᴹᴼ : Maybe(Object yes) → Maybe Type +typeOfᴹᴼ nothing = nothing +typeOfᴹᴼ (just O) = just (typeOfᴼ O) + +typeOfⱽ : Heap yes → Value → Maybe Type +typeOfⱽ H nil = just nil +typeOfⱽ H (bool b) = just boolean +typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ) +typeOfⱽ H (number n) = just number + +typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type +typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type + +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 +typeOfᴱ H Γ (binexp M op N) = tgtBinOp op + +typeOfᴮ H Γ (function f ⟨ var x ∈ S ⟩∈ T is C end ∙ B) = typeOfᴮ H (Γ ⊕ f ↦ (S ⇒ T)) B +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 → (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) +mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl) +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 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 orNone (cong typeOfᴹᴼ (sym q))) p +mustBeNumber H Γ (addr a) p | nothing , q | () +mustBeNumber H Γ (number n) p = refl +mustBeNumber H Γ (bool true) () +mustBeNumber H Γ (bool false) () + +typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M)) +typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B)) + +typeCheckᴱ H Γ (var x) = var refl +typeCheckᴱ H Γ (val nil) = nil +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) +typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B) +typeCheckᴱ H Γ (binexp M op N) = binexp (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N) + +typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B) +typeCheckᴮ H Γ (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ ⊕ x ↦ T) B) +typeCheckᴮ H Γ (return M ∙ B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B) +typeCheckᴮ H Γ done = done + +typeCheckᴼ : ∀ H O → (⊢ᴼ O) +typeCheckᴼ H nothing = nothing +typeCheckᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (x ↦ T) B) + +typeCheckᴴ : ∀ H → (⊢ᴴ H) +typeCheckᴴ H a {O} p = typeCheckᴼ H (O) + +typeCheckᴴᴱ : ∀ H Γ M → (Γ ⊢ᴴᴱ H ▷ M ∈ typeOfᴱ H Γ M) +typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M) + +typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M) +typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M) diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/out.txt b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt index c508d5366..ee6f2a25b 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 27ba77dda..86a499a8c 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 d3827e75a..5b4d26440 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 607602cfc..1d5f45b6e 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