From 121bc52cc39cdadaee0e0029270e0da6d42b4b6f Mon Sep 17 00:00:00 2001
From: "ajeffrey@roblox.com" <ajeffrey@roblox.com>
Date: Mon, 7 Feb 2022 16:34:03 -0600
Subject: [PATCH] Exit code 1 on errors

---
 prototyping/FFI/IO.agda          |  4 ++++
 prototyping/FFI/System/Exit.agda | 29 +++++++++++++++++++++++++++++
 prototyping/Main.agda            |  8 +++++---
 3 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 prototyping/FFI/System/Exit.agda

diff --git a/prototyping/FFI/IO.agda b/prototyping/FFI/IO.agda
index 2b230055..825a788f 100644
--- a/prototyping/FFI/IO.agda
+++ b/prototyping/FFI/IO.agda
@@ -7,6 +7,7 @@ open import Agda.Builtin.String using (String)
 open import FFI.Data.HaskellString using (HaskellString; pack ; unpack)
 
 infixl 1 _>>=_
+infixl 1 _>>_
 
 postulate
   return : ∀ {a} {A : Set a} → A → IO A
@@ -28,3 +29,6 @@ getContents = fmap pack getHContents
 
 putStrLn : String → IO ⊤
 putStrLn txt = putHStrLn (unpack txt)
+
+_>>_ : ∀ {a} {A : Set a} → IO ⊤ → IO A → IO A
+a >> b = a >>= (λ _ → b )
diff --git a/prototyping/FFI/System/Exit.agda b/prototyping/FFI/System/Exit.agda
new file mode 100644
index 00000000..fcf01395
--- /dev/null
+++ b/prototyping/FFI/System/Exit.agda
@@ -0,0 +1,29 @@
+module FFI.System.Exit where
+
+open import Agda.Builtin.Int using (Int)
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Unit using (⊤)
+
+data ExitCode : Set where
+  ExitSuccess : ExitCode
+  ExitFailure : Int → ExitCode
+
+{-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
+{-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}
+
+{-# FOREIGN GHC import qualified System.Exit #-}
+
+{-# FOREIGN GHC
+toExitCode :: AgdaExitCode -> System.Exit.ExitCode
+toExitCode AgdaExitSuccess = System.Exit.ExitSuccess
+toExitCode (AgdaExitFailure n) = System.Exit.ExitFailure (fromIntegral n)
+
+fromExitCode :: System.Exit.ExitCode -> AgdaExitCode
+fromExitCode System.Exit.ExitSuccess = AgdaExitSuccess
+fromExitCode (System.Exit.ExitFailure n) = AgdaExitFailure (fromIntegral n)
+#-}
+
+postulate
+  exitWith : ExitCode → IO ⊤
+
+{-# COMPILE GHC exitWith = System.Exit.exitWith . toExitCode #-}
diff --git a/prototyping/Main.agda b/prototyping/Main.agda
index ebf261bb..c0917163 100644
--- a/prototyping/Main.agda
+++ b/prototyping/Main.agda
@@ -1,13 +1,15 @@
 module Main where
 
 open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Int using (pos)
 open import Agda.Builtin.Unit using (⊤)
 
-open import FFI.IO using (getContents; putStrLn; _>>=_)
+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.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.Syntax.FromJSON using (blockFromJSON)
@@ -18,12 +20,12 @@ runBlock block = putStrLn (blockToString block)
 
 runJSON : Value → IO ⊤
 runJSON value with blockFromJSON(value)
-runJSON value | (Left err) = putStrLn ("Luau error: " ++ err)
+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)
+runString txt | (Left err) = putStrLn ("JSON error: " ++ err) >> exitWith (ExitFailure (pos 1))
 runString txt | (Right value) = runJSON value
 
 main : IO ⊤