content: {-# OPTIONS_GHC -Wall #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TypeFamilies #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  toyfmf
  -- Copyright   :  (c) Masahiro Sakai 2012
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  experimental
  -- Portability :  non-portable
  --
  -- A toy-level model finder
  --
  -----------------------------------------------------------------------------
  module Main where
  
  import Control.Monad
  import Data.Interned (intern, unintern)
  import Data.IORef
  import qualified Data.Map as Map
  import Data.Ratio
  import Data.String
  import qualified Data.Text as Text
  import Options.Applicative
  import qualified Codec.TPTP as TPTP
  import ToySolver.Data.Boolean
  import qualified ToySolver.EUF.FiniteModelFinder as MF
  import ToySolver.Internal.Util (setEncodingChar8)
  
  data Options
    = Options
    { optInput :: FilePath
    , optSize :: Int
    }
  
  optionsParser :: Parser Options
  optionsParser = Options
    <$> fileInput
    <*> sizeInput
    where
      fileInput :: Parser FilePath
      fileInput = argument str $ metavar "FILE.tptp"
  
      sizeInput :: Parser Int
      sizeInput = argument auto $ metavar "SIZE"
  
  parserInfo :: ParserInfo Options
  parserInfo = info (helper <*> optionsParser)
    $  fullDesc
    <> header "toyfmf - a finite model finder"
  
  main :: IO ()
  main = do
  #ifdef FORCE_CHAR8
    setEncodingChar8
  #endif
    opt <- execParser parserInfo
    solve (optInput opt) (optSize opt)
  
  solve :: FilePath -> Int -> IO ()
  solve _ size | size <= 0 = error "<size> should be >=1"
  solve fpath size = do
    inputs <- TPTP.parseFile fpath
    let fs = translateProblem inputs
  
    ref <- newIORef (0::Int)
    let skolem name _ = do
          n <- readIORef ref
          let fsym = intern $ unintern name <> "#" <> fromString (show n)
          writeIORef ref (n+1)
          return fsym
    cs <- liftM concat $ mapM (MF.toSkolemNF skolem) fs
  
    ret <- MF.findModel size cs
    case ret of
      Nothing -> do
        putStrLn "s NO MODEL FOUND"
      Just m -> do
        putStrLn "s SATISFIABLE"
        let isSkolem k = Text.any ('#'==) (unintern k)
        let m' = m{ MF.mFunctions = Map.filterWithKey (\k _ -> not (isSkolem k)) (MF.mFunctions m) }
        forM_ (MF.showModel m') $ \s ->
          putStrLn $ "v " ++ s
  
    return ()
  
  -- ---------------------------------------------------------------------------
  
  translateProblem :: [TPTP.TPTP_Input] -> [MF.Formula]
  translateProblem inputs = do
    i <- inputs
    case i of
      TPTP.Comment _ -> []
      TPTP.Include _ _ -> error "\"include\" is not supported yet "
      TPTP.AFormula{ TPTP.name = _, TPTP.role = _, TPTP.formula = formula, TPTP.annotations = _ } ->
        return $ translateFormula formula
  
  translateFormula :: TPTP.Formula -> MF.Formula
  translateFormula = TPTP.foldF neg quant binop eq rel
    where
      neg phi = notB $ translateFormula phi
      quant q vs phi = foldr q' (translateFormula phi) [fromString v | TPTP.V v <- vs]
        where
          q' =
            case q of
              TPTP.All    -> MF.Forall
              TPTP.Exists -> MF.Exists
      binop phi op psi = op' phi' psi'
        where
          phi' = translateFormula phi
          psi' = translateFormula psi
          op' =
            case op of
              (TPTP.:<=>:)  -> (.<=>.)
              (TPTP.:=>:)   -> (.=>.)
              (TPTP.:<=:)   -> flip (.=>.)
              (TPTP.:&:)    -> (.&&.)
              (TPTP.:|:)    -> (.||.)
              (TPTP.:~&:)   -> \a b -> notB (a .&&. b)
              (TPTP.:~|:)   -> \a b -> notB (a .||. b)
              (TPTP.:<~>:)  -> \a b -> notB (a .<=>. b)
      eq lhs op rhs =
        case op of
          (TPTP.:=:)  -> MF.Atom $ MF.PApp "=" [lhs', rhs']
          (TPTP.:!=:) -> MF.Not $ MF.Atom $ MF.PApp "=" [lhs', rhs']
        where
          lhs' = translateTerm lhs
          rhs' = translateTerm rhs
      rel (TPTP.AtomicWord p) ts = MF.Atom $ MF.PApp (fromString p) ts'
        where
          ts' = map translateTerm ts
  
  translateTerm :: TPTP.Term -> MF.Term
  translateTerm = TPTP.foldT str num var app
    where
      str s = MF.TmApp (fromString (show s)) []
      num r = MF.TmApp (fromString (showRational r)) []
      var (TPTP.V v) = MF.TmVar (fromString v)
      app (TPTP.AtomicWord f) ts = MF.TmApp (fromString f) ts'
        where
          ts' = map translateTerm ts
  
      showRational r =
        if denominator r == 1
        then show (numerator r)
        else show (numerator r) ++ "/" ++ show (denominator r)
  
  -- ---------------------------------------------------------------------------
  