import Data.List

import Control.Monad

import Test.QuickCheck
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Exception (SomeException, catch)

import Data.Functor
import Data.Maybe

import Text.Parsec hiding (parse)
import Data.Either
import Control.Monad

import Test.QuickCheck hiding(Success,Failure)

 
main = do
        print("Welcome")
        print("Type :h for help.")
        
        loop
        
prog :: Parser Prog
prog = Prog <$> (whitespaces *> many rule <* eof)        
        
loop :: IO()
loop = do 
         line <- getLine
         case line of 
         {":h" -> do 
                  putStrLn  "<goal>      Solves/proves the specified goal."
                  putStrLn  ":h          Shows this help message."
                  putStrLn   ":l <file>   Loads the specified file."
                  putStrLn   ":q          Exits the interactive environment."
                  putStrLn   ":r          Reloads the last loaded file."
                  putStrLn   ":s <strat>  Sets the specified search strategy\nwhere <strat> is one of 'dfs', 'bfs', or 'iddfs'."
           ;":q" -> print()
           ;"append(A, [B|_], [1, 2])" -> print (goalLös "append(A, [B|_], [1, 2])" )
         }
         loop



goalLös :: String -> Goal
goalLös s = x ((parse s)::Either String Goal)



x :: Either a b -> Goal
x (Left a)  = Goal[Var(VarName "T")]
x (Right b) = Goal[Var(VarName "T")]
-- Type class for parsing

class Parse a where
  parse :: String -> Either String a


-- Try to parse a goal
-- Try to parse a goal
instance Parse Goal where
  parse = adjustErrorMessage . simpleParse goal
    where adjustErrorMessage (Left e) = Left ("Parse error (goal" ++ drop 19 e)
          adjustErrorMessage r        = r

-- Try to parse a program
instance Parse Prog where
  parse = simpleParse prog

-- Try to parse a file
parseFile :: Parse a => FilePath -> IO (Either String a)
parseFile fn =
  let f = reverse . dropWhile (== ' ')
  in catch (parse <$> readFile (f (f fn)))
       (\ (_ :: SomeException) -> return (Left "Could not read file."))

-- INTERNAL

-- Parser type
type Parser a = Parsec String () a

-- Apply a parser to a string
simpleParse :: Parser a -> String -> Either String a
simpleParse p =
  either (Left . ("Parse error " ++) . show) Right . runParser p () ""

-- Parse a goal
goal :: Parser Goal
goal = Goal <$> (whitespaces *>
  (try ((: []) <$> var <* symbol ".") <|> commaSep lit <* symbol ".") <* eof)

-- Parse a program
prog :: Parser Prog
prog = Prog <$> (whitespaces *> many rule <* eof)

-- Parse a rule
rule :: Parser Rule
rule = Rule <$> lhs <*> rhs

-- Parse the left hand side of a rule
lhs :: Parser Term
lhs = try (parens lhs) <|> comb

-- Parse the right hand side of a rule
rhs :: Parser [Term]
rhs = symbol "." $> [] <|> symbol ":-" *> commaSep lit <* symbol "."

-- Parse a literal
lit :: Parser Term
lit = try (parens lit) <|> comb

-- Parse a term
term :: Parser Term
term = parens term <|> var <|> list <|> comb

-- Parse a variable term
var :: Parser Term
var = Var <$> varName

-- Parse a variable name
varName :: Parser VarName
varName = VarName <$>
  ((:) <$> upper <*> many (letter <|> digit <|> char '_') <|>
    (:) <$> char '_' <*> many (letter <|> digit <|> char '_')) <* whitespaces

-- Parse a list
list :: Parser Term
list = symbol "[" *> whitespaces *> do
  let nil = Comb "[]" []
      cons x xs = Comb "." [x, xs]
  try (flip (foldr cons) <$> term `sepBy1` symbol "," <* symbol "|" <*>
        term <* symbol "]") <|>
    foldr cons nil <$> commaSep term <* symbol "]"

-- Parse a combination term
comb :: Parser Term
comb = do
  f <- atom
  args <- fromMaybe [] <$> optionMaybe (parens (commaSep term))
  whitespaces
  pure (Comb f args)

-- Parse an atom
atom :: Parser String
atom = (:) <$> lower <*> many (letter <|> digit <|> char '_') <|>
  number <|> (many1 (oneOf "+-*/<=>'\\:.?@#$&^~") <?> "symbol")

-- Parse a number
number :: Parser String
number = try ((:) <$> char '-' <*> (try float <|> int)) <|> try float <|> int
  where float = (++) <$> int <*>
          ((:) <$> char '.' <*> (reverse . trim . reverse <$> many1 digit))
        int   = trim <$> many1 digit
        trim  = show . (read :: String -> Integer)

-- Parse a symbol
symbol :: String -> Parser ()
symbol s = string s *> whitespaces

-- Parse a comment
comment :: Parser ()
comment = () <$ (char '%' *> many (noneOf "\n") *> char '\n') <?> "comment"

-- Parse whitespaces or a comment
whitespaces :: Parser ()
whitespaces =  skipMany (() <$ space <|> comment)

-- Parse a list separated by commas
commaSep :: Parser a -> Parser [a]
commaSep p = p `sepBy` symbol ","

-- Parse something enclosed in parentheses
parens :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")




-- the SLD tree datatype (the Goal is the question, the list of substitutions and trees are the edges)
data SLDTree = Node Goal [(Subst,SLDTree)] | Success | Failure
  deriving Show


sld :: Prog -> Goal -> SLDTree
sld p g  =  sld' p g (allVars p ++ allVars g)    -- we are using a help function that tracks already used variables.

sld' :: Prog -> Goal -> [VarName] -> SLDTree      -- this function does the work and tracks the already used (and forbidden) variables
sld' _ (Goal [])     _  = Success                 -- when there is no Term in the goal left, we was succsessfull
sld' p (Goal (t:ts)) fb = let us = getUnificators fb p t in     -- we first try to get all possible rules with which we can unify our term
                          if  length us == 0 then Failure             -- if there is no option to unify t, then we have a failure
                          else Node (Goal (t:ts))                     -- otherwise we return a new Node with the goal
                                    (map (\(u,r) -> (u,               -- and the edges with each possible unifier
                                                     sld' p           -- the node the edge points to is created through recursion
                                                          (Goal (apply' u ((extractRight r) ++ ts)))  -- The new goal is builded
                                                          (fb ++ (allVars r) ++ (allVars u))))        -- and in the next sld' call there are more forbidden VarNames
                                          us)

   where
     getUnificators :: [VarName] -> Prog -> Term -> [(Subst,Rule)]       -- this function computes all possible rules for a term in a program
     getUnificators fb (Prog [])     _ = []                   -- when there are no terms left in the programm, we hgave tried everything
     getUnificators fb (Prog (r:rs)) t = let r' = rename fb r -- we firstly rename our rule
                                             u  = unify (extractLeft r') t  -- then we try to unify the renamed rule and the term
                                         in  case u of
                                                  Nothing -> getUnificators fb (Prog rs) t          -- when the term and the rule cannot be unified, we try the next rule
                                                  Just u  -> (u, r') : (getUnificators fb (Prog rs) t)  -- otherwise we save the rule and unifier and try the next rule

     toSubst :: Maybe Subst -> Subst
     toSubst Nothing  = empty        -- this case should not be used by a call (only for compiler)
     toSubst (Just s) = s            -- this is the needed case

     apply' :: Subst -> [Term] -> [Term] -- this function applys a substitution to every element of a list of terms
     apply' s ts = map (apply s) ts

     extractLeft :: Rule -> Term     -- This function returns the left side of a rule
     extractLeft (Rule t ts) = t

     extractRight :: Rule -> [Term]       -- this function just extracts the right side of a rule
     extractRight (Rule t ts) = ts



type Strategy = SLDTree -> [Subst]



dfs :: Strategy
dfs t = dfs' empty t

dfs' :: Subst -> SLDTree -> [Subst]
dfs' _ Failure              = []            -- on failure there is no matching substitution!
dfs' s Success              = [s]           -- on success, we canjust return the substitution, that we got from the father node
dfs' s (Node _ [])          = []            -- break condition
dfs' s (Node g ((u, t):us)) = map (\s1 -> compose s1 s) (dfs' u t) ++ dfs' s (Node g us) -- we compose all substitutions from below with the one we got from our father


------------- BFS! ------------------
bfs :: Strategy
bfs t = [empty]



solveWith :: Prog -> Goal -> Strategy -> [Subst]
solveWith p g s = map ((flip restrictTo) (filter (\(VarName x) -> if head x == '_' then False else True)  (allVars g))) (s (sld p g))






rename :: [VarName] -> Rule -> Rule
rename fb r =  let vr = filter (\x -> x /= VarName "_") (allVars r)    -- we need all variables from r (except "_") twice
               in sUS (fb ++ vr) (applyToRule (createSubst (fb ++ vr) vr) r)   -- first create a substitution that rnames variables, then apply it to r and then replace underscores
  where
    createSubst :: [VarName] -> [VarName] -> Subst              -- this method creates a substituion, that renames variables without the forbidden
    createSubst fb []     = empty                               -- when we renamed every variable, we are finished
    createSubst fb (x:xs) = let y = head (filter (\x -> not (x `elem` fb))freshVars)   -- y should be a valid new variablename
                            in  compose (single x (Var y)) (createSubst (fb++ [y]) xs) -- just do the renaming for the first element, then for the rest
    applyToRule :: Subst -> Rule -> Rule     -- this function applys a substitution to every term of a rule
    applyToRule s (Rule t ts) = Rule (apply s t) (map (apply s) ts)

-- this function replaces each underscore ina rule by a unique variable name in the type of "_1"
sUS :: [VarName] -> Rule -> Rule
sUS fb (Rule t ts) = let t' = sUSterm fb t
                     in Rule t' (sUStlist (fb ++ (getUS (allVars t'))) ts)

-- ths function replaces underscores in terms by unique names "_1"
sUSterm :: [VarName] -> Term -> Term
sUSterm fb (Var x)     = if x == VarName "_" then Var (head ( filter (\x -> (not (elem x fb))) underscores  )) else Var x
sUSterm fb (Comb f ts) = Comb f (sUStlist fb ts)

-- this function replaces underscores in lists if terms with names like "_1"
sUStlist :: [VarName] -> [Term] -> [Term]
sUStlist _  []     = []
sUStlist fb (t:ts) = let t' = sUSterm fb t
                     in t':(sUStlist (fb ++ getUS (allVars t')) ts)

-- this function filters a list of Variablenames by variable names such like "_%"  %=anything
getUS :: [VarName] -> [VarName]
getUS []     = []
getUS ((VarName n):ns) = if head n == '_' && (length n) >= 1 then (VarName n):(getUS ns) else getUS ns

-- a list : [VarName "_0", VarName "_1" , ...]
underscores :: [VarName]
underscores = [VarName ("_" ++ (show x)) |  x <- [0..]]

-------- everything for testing

-- checks if the set intersection of two lists is Empty
intersectEmpty :: Eq a => [a] -> [a] ->Bool
intersectEmpty []     _  = True               -- when we checked every element, we are finihed with true
intersectEmpty (a:as) bs = if a `elem` bs then False else intersectEmpty as bs -- if any element of the first list is in the second, the intersection isn't empty




class Vars a where
  allVars :: a -> [VarName]


-- in all this instances we do not track "_", because the underscore isn't relevant in the use cases of this methods.
instance Vars Term where
  allVars (Var vn)       = filter (\x -> not (x == VarName "_")) [vn]
  allVars (Comb _  [])   = []
  allVars (Comb cn (t:ts)) = filter (\x -> not (x == VarName "_")) (nub ((allVars t) ++ (allVars (Comb cn ts))))


instance Vars Rule where
  allVars (Rule t [])      = filter (\x -> not (x == VarName "_")) (nub (allVars t))
  allVars (Rule t (t1:ts)) = filter (\x -> not (x == VarName "_")) (nub ((allVars t) ++ (allVars (Rule t1 ts))))


instance Vars Prog where
  allVars (Prog [])     = []
  allVars (Prog (r:rs)) = filter (\x -> not (x == VarName "_")) (nub ((allVars r) ++ (allVars (Prog rs))))

instance Vars Goal where
  allVars (Goal [])     = []
  allVars (Goal (t:ts)) = filter (\x -> not (x == VarName "_")) (nub ((allVars t) ++ (allVars (Goal ts))))

freshVars :: [VarName]
freshVars = [VarName [x] | x <- ['A' .. 'Z']] ++
            [VarName ([x] ++ show y) | y <- [0..], x <- ['A' .. 'Z']]











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






-- Data type for variable names
data VarName = VarName String
  deriving (Eq, Ord, Show)

-- Generator for variable names
instance Arbitrary VarName where
  arbitrary = VarName <$> elements ["A", "B", "_0", "_"]

-- Alias type for combinators
type CombName = String

-- Data type for terms
data Term = Var VarName | Comb CombName [Term]
  deriving (Eq, Show)

-- Generator for terms
instance Arbitrary Term where
  arbitrary = do
    arity <- choose (0, 2)
    frequency [ (2, Var <$> arbitrary)
              , (3, Comb <$> elements ["f", "g"] <*> replicateM arity arbitrary)
              ]

-- Data type for program rules
data Rule = Rule Term [Term]
  deriving Show

-- Generator for rules
instance Arbitrary Rule where
  arbitrary =
    Rule <$> arbitrary <*> (choose (0, 2) >>= \n -> replicateM n arbitrary)

-- Data type for programs
data Prog = Prog [Rule]
  deriving Show

-- Data type for goals
data Goal = Goal [Term]
  deriving Show