import Data.Char ()
import Text.Read ( readMaybe )

-- Some aliases
type VarName  = String
type FunName  = String
type PredName = String

-- Data type of first-order terms
data FOTerm = FOVar VarName | FOFun FunName [FOTerm]
    deriving (Read)

-- We make FOTerm an instance of the Read class, which can be used as follows: 
_ = case readMaybe "FOVar \"a\"" :: Maybe FOTerm of Nothing -> "parse error"; Just x -> "fine, we\'ve got " ++ show x
-- Defining a custom instance of Show for nicer input format is welcome

-- Custom "show" for printing it pretty
instance Show FOTerm where
    show :: FOTerm -> String
    show (FOVar x)          = x
    show (FOFun f [])       = f
    show (FOFun f (x : xs)) = f ++ "(" ++ show x ++ foldr ((++) . (", "++) . show) ")" xs

-- Data type of first-order formulas
data FOFormula = FOPred PredName [FOTerm]                           -- add more clauses
    deriving (Read, Show)

data FOJudgement = FOJudgement [VarName] [FOFormula] FOFormula
    deriving (Show)

-- Free variables of a formula
formFreeVars :: FOFormula -> [VarName]
formFreeVars = undefined                                            -- replace with your code 

-- funSubst t x s implements t[s/x] for terms
funSubst :: FOTerm -> VarName -> FOTerm -> FOTerm
funSubst = undefined                                                -- replace with your code

-- formSubst t x s implements t[s/x] for formulas
formSubst :: FOFormula -> VarName -> FOTerm -> FOFormula
formSubst = undefined                                               -- replace with your code 

data ProofState = ProofState                                        -- replace with your code

-- Initialize proof state with the goal
initPS :: FOJudgement -> ProofState
initPS = undefined                                                  -- replace with your code

-- Main code
proofStep :: (String, ProofState) -> (String, ProofState)
proofStep = undefined                                               -- replace with your code

-- Interactive shell wrapper
statefulInteract :: ((String, a) -> (String, a)) -> (String, a) -> IO ()
statefulInteract f (s , x) = (putStr s >> getLine) >>= statefulInteract f . (\s -> f (s , x))

-- Test for statefulInteract
siTest :: (String, Int) -> (String, Int)
siTest (s , n) = ("[" ++ show n ++ "] your input is: " ++ show s ++ "\n[" ++ show (n + 1) ++ "] enter another string: ", n + 1)

goals = [
      undefined :: FOJudgement   -- first test formula 
    , undefined :: FOJudgement   -- second test formula
    , undefined :: FOJudgement   -- third test formula, etc
 ]

prove :: Int -> IO ()
prove n = statefulInteract proofStep ("We are proving " ++ show (goals !! n) ++ ". Which rule to apply?> ", initPS $ goals !! n)