-- | JSON transport shared by the model observations consumed by live stories.
module Conformance.Lean.Oracle (expectedObservation, modelVerdict) where

import Data.Aeson (Value (..), eitherDecode, encode)
import Data.Aeson.KeyMap qualified as KM
import Data.ByteString.Lazy.Char8 qualified as BSL
import System.Exit (ExitCode (..))
import System.Process (readProcessWithExitCode)

expectedObservation
    :: FilePath -> [String] -> Value -> IO (Either String Value)
expectedObservation :: String -> [String] -> Value -> IO (Either String Value)
expectedObservation String
executable [String]
arguments Value
scenario = do
    (status, output, diagnostics) <-
        String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode
            String
executable
            [String]
arguments
            (ByteString -> String
BSL.unpack (Value -> ByteString
forall a. ToJSON a => a -> ByteString
encode Value
scenario) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n")
    pure $ case status of
        ExitFailure Int
code ->
            String -> Either String Value
forall a b. a -> Either a b
Left
                ( String
"Lean evaluator failed ("
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
code
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"): "
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
diagnostics
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
output
                )
        ExitCode
ExitSuccess -> case ByteString -> Either String Value
forall a. FromJSON a => ByteString -> Either String a
eitherDecode (String -> ByteString
BSL.pack String
output) of
            Left String
reason -> String -> Either String Value
forall a b. a -> Either a b
Left (String
"invalid Lean evaluator response: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
reason)
            Right Value
expected -> Value -> Either String Value
forall a b. b -> Either a b
Right Value
expected

{- | The model's verdict on a submitted transaction, as its outcome and reason:
the law's, from the driver's row, and, when the law accepts and the driver was
asked to judge the transaction's outputs, a refusal for the reason the
judgement names when they do not pay what the exit owes.
-}
modelVerdict :: Value -> Maybe Value -> Either String (Value, Value)
modelVerdict :: Value -> Maybe Value -> Either String (Value, Value)
modelVerdict Value
row Maybe Value
judged = do
    outcome <- Key -> Value -> Either String Value
field Key
"outcome" Value
row
    reason <- field "reason" row
    case (outcome, judged) of
        (String Text
"accepted", Just Value
judgement) -> do
            settled <- Key -> Value -> Either String Value
field Key
"settle" Value
judgement
            case settled of
                Value
Null -> (Value, Value) -> Either String (Value, Value)
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value
outcome, Value
reason)
                String Text
why -> (Value, Value) -> Either String (Value, Value)
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Value
String Text
"refused", Text -> Value
String Text
why)
                Value
_ -> String -> Either String (Value, Value)
forall a b. a -> Either a b
Left String
"the driver's judgement is neither settled nor a reason"
        (Value, Maybe Value)
_ -> (Value, Value) -> Either String (Value, Value)
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value
outcome, Value
reason)
  where
    field :: Key -> Value -> Either String Value
field Key
name (Object Object
fields) =
        Either String Value
-> (Value -> Either String Value)
-> Maybe Value
-> Either String Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
            (String -> Either String Value
forall a b. a -> Either a b
Left (String
"model row has no " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Key -> String
forall a. Show a => a -> String
show Key
name))
            Value -> Either String Value
forall a b. b -> Either a b
Right
            (Key -> Object -> Maybe Value
forall v. Key -> KeyMap v -> Maybe v
KM.lookup Key
name Object
fields)
    field Key
name Value
_ = String -> Either String Value
forall a b. a -> Either a b
Left (String
"model row is not an object reading " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Key -> String
forall a. Show a => a -> String
show Key
name)