module HyLo.InputFile ( InputFile, parse, myparse, write, parseOldFormat, OldInputFile,
                        --unit_tests
                        )

where

import Control.Monad.State
-- import HyLo.Signature ( Signature,
--                         emptySignature )

-- import Test.QuickCheck ( Property, (==>) )
-- import HyLo.Test       ( UnitTest, runTest )

import HyLo.Formula          ( Formula,
--                               mapSig, boundVars
                               )
import HyLo.Signature.String ( NomSymbol(..), PropSymbol, RelSymbol )
import qualified HyLo.Signature.Simple as Simple

import qualified HyLo.InputFile.Lexer  as L
import qualified HyLo.InputFile.Parser as P

import qualified HyLo.InputFile.OldLexer  as Old.L
import qualified HyLo.InputFile.OldParser as Old.P

type InputFile = [Formula NomSymbol PropSymbol RelSymbol]

runParser :: State P.ParseState a -> a
runParser r = evalState r P.initParseState

parse :: String -> InputFile
parse = P.theory . runParser . P.parse . L.alexScanTokens

myparse :: String -> P.ParseOutput
myparse = runParser . P.parse . L.alexScanTokens

write :: (Show n, Show p, Show r) => [Formula n p r] -> String
write input = unlines $ "{":addSemicolon (map show input) ++ ["}"]
    where addSemicolon (x:xs@(_:_)) = (x ++ ";") : addSemicolon xs
          addSemicolon xs           = xs

type OldInputFile = [Formula Simple.NomSymbol Simple.PropSymbol Simple.RelSymbol]

parseOldFormat :: String -> OldInputFile
parseOldFormat = Old.P.parse . Old.L.alexScanTokens


-- -------------------
-- QuickCheck stuff
-- -------------------

--prop_parseWrite :: InputFile -> Property
--prop_parseWrite in_f = (not . null $ in_f') ==>
--                         show in_f' == (show . parse . write $ in_f')
--     where in_f' = map only_vars_bound in_f
--           only_vars_bound f = mapSig mn id id f
--             where mn n@(Simple.N i) | n `elem` bound_vars = Simple.X i
--                   mn n = n
--                   bound_vars = boundVars f
--
-- unit_tests :: UnitTest
-- unit_tests = [("parse . write == id", runTest prop_parseWrite)]