-----------------------------------------------------------------------------
-- |
-- Module      :  toyfmf
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-- A toy-level model finder
--
-----------------------------------------------------------------------------
module Main where

import Control.Monad
import Data.IORef
import qualified Data.Map as Map
import Data.Ratio
import System.Environment
import System.IO
import qualified Codec.TPTP as TPTP
import ToySolver.Data.Boolean
import qualified ToySolver.FOLModelFinder as MF

main :: IO ()
main = do
  args <- getArgs
  case args of
    [fpath, size] -> solve fpath (read size)
    _ -> hPutStrLn stderr "Usage: toyfmf <file.tptp> <size>"

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
  let skolem name _ = do
        n <- readIORef ref
        let fsym = name ++ "#" ++ 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 = '#' `elem` 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 = 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) [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 p ts'
      where
        ts' = map translateTerm ts

translateTerm :: TPTP.Term -> MF.Term
translateTerm = TPTP.foldT str num var app
  where
    str s = MF.TmApp (show s) []
    num r = MF.TmApp (showRational r) []
    var (TPTP.V v) = MF.TmVar v
    app (TPTP.AtomicWord f) ts = MF.TmApp f ts'
      where
        ts' = map translateTerm ts

    showRational r =
      if denominator r == 1
      then show (numerator r)
      else show (numerator r) ++ "/" ++ show (denominator r)

-- ---------------------------------------------------------------------------