module Main ( main )

where

import HyLo.InputFile

import HyLo.Formula
import HyLo.Formula.Rewrite
import HyLo.Signature.Simple

import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Traversable as T
import Data.Generics.UniplateStr

import Control.Monad.State

import System.Exit
import System.Environment

main :: IO ()
main = do args <- getArgs
          case args of
            [inf,outf] -> readFile inf >>=
                          writeFile outf . write . rename . pnf . parseOldFormat
            _          -> do prg_name <- getProgName
                             putStrLn $ concat ["Usage: ", prg_name, ": ",
                                                             "<input> <output>"]
                             exitFailure

rename :: [Formula NomSymbol (Rewr PropSymbol) RelSymbol] -> OldInputFile
rename fs = map (mapSig id map_prop id) fs
    where map_prop p = fromMaybe (error "rename?!") (Map.lookup p ren_props)
          ren_props  = evalState (T.mapM renProp all_props) new_props
          new_props  = [PropSymbol (max_orig + 1)..]
          max_orig   = maximum [n | f <- fs,
                                    Prop (Orig (PropSymbol n)) <- universe f]
          all_props  = Map.fromList [(p,p) | f <- fs, Prop p <- universe f]
          renProp rp  = case rp of
                           (Orig p) -> return p
                           (Rewr _) -> do (p:ps) <- get
                                          put ps
                                          return p