Prototyping strict mode (#399)

* First cut of strict mode

Co-authored-by: Lily Brown <lily@lily.fyi>

prototyping/.gitignore

@@ -2,10 +2,8 @@
 *.agdai
 Main
 MAlonzo
-Examples
 PrettyPrinter
 Interpreter
-Properties
 !Tests/Interpreter
 !Tests/PrettyPrinter
 .ghc.*

prototyping/Everything.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --rewriting #-}
+
+module Everything where
+
+import Examples
+import Properties
+import PrettyPrinter
+import Interpreter

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

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

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

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
+

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

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
+

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

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 ⊤

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
 

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