{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}

module Main where

import            Language.Prolog.NanoProlog.Lib
import            Text.ParserCombinators.UU
import            System.IO

-- * Running the Interpreter
-- ** The main interpreter
-- | The `main` program prompt for a file with Prolog rules and call the main
-- interpreter loop
main :: IO ()
main = do  hSetBuffering stdin LineBuffering
           putStr "File with rules? "
           fn  <- getLine
           s   <- readFile fn
           let (rules, errors) = startParse (pList pRule)  s
           if null errors  then  do  mapM_ print rules
                                     loop rules
                           else  do  putStrLn "No rules parsed"
                                     mapM_ print errors
                                     main

-- | `loop` ask for a goal, and enuartes all solutions found, each preceded by
-- a trace conatining the rules applied in a tree-like fashion
loop :: [Rule] -> IO ()
loop rules = do  putStr "goal? "
                 s <- getLine
                 unless (s == "quit") $
                   do  let (goal, errors) = startParse pFun s
                       if null errors
                         then  printSolutions (solve rules emptyEnv 0 [goal])
                         else  do  putStrLn "Some goals were expected:"
                                   mapM_ print errors
                       loop rules

-- | `printSolutions` takes the result of a treewalk, which constructs
-- all the proofs, and pairs them with their final
-- substitutions. Alternative approaches in printing are to print the
-- raw proofs, i.e. without applying the final substitution (remove
-- the @subst env@ ). This nicely shows how the intermediate variables
-- come into life. By including the test on the length the facts
-- directly stemming from the data base are not printed. This makes
-- the proofs much shorter, but a bit less complete.
printSolutions ::  Result -> IO ()
printSolutions result = sequence_
  [  do  sequence_ [ putStrLn (prefix ++ " " ++  show (subst env pr))
                   | (prefix, pr@(p :<-: pp)) <- reverse proof
--                 , length pp >0
                   ]
         putStr "substitution: "
         putStrLn (show' env)
         void getLine
  |  (proof, env) <- enumerateDepthFirst [] ["0"] result ]