Exit code 1 on errors

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 )

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 #-}

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 ⊤