module Main ( main )

where

import System.Environment ( getArgs )

import Control.Applicative ( (<$>) )
import qualified Data.Set as Set

import HyLo.Model ( Model, (|=), worlds )

import HyLo.Signature.String ( NomSymbol, PropSymbol, RelSymbol )

import HyLo.InputFile ( InputFile, parse )

import Data.List ( delete )

main :: IO ()
main =
    do args <- getArgs
       case args of
         [mf, ff] -> do m  <- read  <$> readFile mf :: IO M
                        fs <- parseAnyFormat <$> readFile ff
                        --
                        let ws = Set.toList (worlds m)
                        --
                        print $ any (\w -> and [(m,w) |= f | f <- fs]) ws
         --
         _        -> putStrLn "Usage: mcheck <model> <formulas>"


parseAnyFormat :: String -> InputFile
parseAnyFormat s | head (words s) == "begin"
 =  parse $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"
          where removeBeginEnd = unwords . delete "begin" . delete "end" . words
parseAnyFormat s = parse s


type M = Model NomSymbol NomSymbol PropSymbol RelSymbol