module Hermod.ReCon.LTL.Formula.Yaml(YamlReadError, readPropValues, readFormulas) where

import           Hermod.ReCon.Common.Parser
import           Hermod.ReCon.Common.Types
import           Hermod.ReCon.LTL.Formula (Formula)
import           Hermod.ReCon.LTL.Formula.Parser (Context, Domain (..))
import qualified Hermod.ReCon.LTL.Formula.Parser as Parser

import           Data.Map.Strict (Map)
import qualified Data.Set as Set
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Yaml (prettyPrintParseException)
import           Data.Yaml.Include (decodeFileEither)
import           Text.Megaparsec

type FormulasEncodedType = [Text]

type PropValuesEncodedType = Map Text [Text]

type YamlReadError = Text

readPropValues :: FilePath -> IO (Either YamlReadError (Map Text Domain))
readPropValues :: FilePath -> IO (Either Text (Map Text Domain))
readPropValues FilePath
path = forall a. FromJSON a => FilePath -> IO (Either ParseException a)
decodeFileEither @PropValuesEncodedType FilePath
path IO (Either ParseException PropValuesEncodedType)
-> (Either ParseException PropValuesEncodedType
    -> IO (Either Text (Map Text Domain)))
-> IO (Either Text (Map Text Domain))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left ParseException
err -> Either Text (Map Text Domain) -> IO (Either Text (Map Text Domain))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Either Text (Map Text Domain)
forall a b. a -> Either a b
Left (FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ ParseException -> FilePath
prettyPrintParseException ParseException
err))
  Right PropValuesEncodedType
propValues -> Either Text (Map Text Domain) -> IO (Either Text (Map Text Domain))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Text (Map Text Domain)
 -> IO (Either Text (Map Text Domain)))
-> Either Text (Map Text Domain)
-> IO (Either Text (Map Text Domain))
forall a b. (a -> b) -> a -> b
$ Map Text Domain -> Either Text (Map Text Domain)
forall a b. b -> Either a b
Right (Map Text Domain -> Either Text (Map Text Domain))
-> Map Text Domain -> Either Text (Map Text Domain)
forall a b. (a -> b) -> a -> b
$ ([Text] -> Domain) -> PropValuesEncodedType -> Map Text Domain
forall a b. (a -> b) -> Map Text a -> Map Text b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Text] -> Domain
parseValues PropValuesEncodedType
propValues
  where
    -- | If all values parse as integers, produce an IntDomain; otherwise TextDomain.
    parseValues :: [Text] -> Domain
    parseValues :: [Text] -> Domain
parseValues [Text]
vs =
      case (Text -> Maybe IntValue) -> [Text] -> Maybe [IntValue]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((ParseErrorBundle Text Void -> Maybe IntValue)
-> (IntValue -> Maybe IntValue)
-> Either (ParseErrorBundle Text Void) IntValue
-> Maybe IntValue
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe IntValue -> ParseErrorBundle Text Void -> Maybe IntValue
forall a b. a -> b -> a
const Maybe IntValue
forall a. Maybe a
Nothing) IntValue -> Maybe IntValue
forall a. a -> Maybe a
Just (Either (ParseErrorBundle Text Void) IntValue -> Maybe IntValue)
-> (Text -> Either (ParseErrorBundle Text Void) IntValue)
-> Text
-> Maybe IntValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parsec Void Text IntValue
-> FilePath -> Text -> Either (ParseErrorBundle Text Void) IntValue
forall e s a.
Parsec e s a -> FilePath -> s -> Either (ParseErrorBundle s e) a
parse Parsec Void Text IntValue
parseIntValue FilePath
"input") [Text]
vs of
        Just [IntValue]
ints -> Set IntValue -> Domain
IntDomain ([IntValue] -> Set IntValue
forall a. Ord a => [a] -> Set a
Set.fromList [IntValue]
ints)
        Maybe [IntValue]
Nothing   -> Set Text -> Domain
TextDomain ([Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList [Text]
vs)

readFormulas :: FilePath -> Context -> Parser ty -> IO (Either YamlReadError [Formula event ty])
readFormulas :: forall ty event.
FilePath
-> Context -> Parser ty -> IO (Either Text [Formula event ty])
readFormulas FilePath
path Context
ctx Parser ty
ty = forall a. FromJSON a => FilePath -> IO (Either ParseException a)
decodeFileEither @FormulasEncodedType FilePath
path IO (Either ParseException [Text])
-> (Either ParseException [Text]
    -> IO (Either Text [Formula event ty]))
-> IO (Either Text [Formula event ty])
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Left ParseException
err -> Either Text [Formula event ty]
-> IO (Either Text [Formula event ty])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Either Text [Formula event ty]
forall a b. a -> Either a b
Left (FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ ParseException -> FilePath
prettyPrintParseException ParseException
err))
  Right [Text]
formulas ->
    case (Text -> Either (ParseErrorBundle Text Void) (Formula event ty))
-> [Text] -> Either (ParseErrorBundle Text Void) [Formula event ty]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Parsec Void Text (Formula event ty)
-> FilePath
-> Text
-> Either (ParseErrorBundle Text Void) (Formula event ty)
forall e s a.
Parsec e s a -> FilePath -> s -> Either (ParseErrorBundle s e) a
parse (Context -> Parser ty -> Parsec Void Text (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
Parser.formula Context
ctx Parser ty
ty) FilePath
"input") [Text]
formulas of
      Left ParseErrorBundle Text Void
err   -> Either Text [Formula event ty]
-> IO (Either Text [Formula event ty])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Either Text [Formula event ty]
forall a b. a -> Either a b
Left (FilePath -> Text
Text.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text Void -> FilePath
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> FilePath
errorBundlePretty ParseErrorBundle Text Void
err))
      Right [Formula event ty]
done -> Either Text [Formula event ty]
-> IO (Either Text [Formula event ty])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Formula event ty] -> Either Text [Formula event ty]
forall a b. b -> Either a b
Right [Formula event ty]
done)