-- * The module ExFind contains the calling functions for the algorithm.

module Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getTerm, getComplete, getForWebInterface,
     getWithDebug, testTerm, getIt, getContradiction, getItContradiction, getRawContradiction,
     getItRawContradiction, getExample, getItExample, testSimple, webInterface) where

import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M hiding (M)
import qualified Prelude as E (Either(..))
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync
import Prelude hiding (Either(..))
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
import qualified Data.Map as Map

-- ** calling functions for ExFind

-- | takes the input in Typ format and returns the monad's debuging information and the result term
getTerm :: Typ -> IO()
getTerm tau = do printTyp tau
		 putStr "\n"
	         case runM $ alg emptyCont tau emptyTermCont of
	           Nothing             -> putStr "No Term."
		   Just ((term,termCont,trackCont),debug,funcNames) -> do putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug))
					                                  printResult (term)

-- | takes the input in Typ format and returns the monad's tracking information, the result term t, the disrelater applied to 't' as variable and as term
getComplete :: Typ -> IO()
getComplete tau = do {printTyp tau;
		      putStr "\n";
		      case runM $ alg emptyCont tau emptyTermCont of
		      Nothing             -> putStr "No Term."
		      Just ((term,termCont,trackCont),debug,funcs) -> 
		          do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));
			      printResult (term);
			      putStr ("Like webinterface:\n\n" ++ showTrackContApplication trackCont (Var (TermVar 0)) ++ "\n\n");
			      putStr ("With the disrelater:\n\n" ++ showTrackContApplication trackCont term ++"\n\n");
			      putStr ("And the variables are:\n\n" ++ showFuncNamesInt funcs ++ "\n\n");
			      putStr ("And completely solved: " ++ showTrackContApplicationSolved trackCont funcs term ++ "\n\n");
			     }
		     }

-- | Output for the webinterface defined in polyfix-cgi.hs (second version)
getForWebInterface :: Typ -> E.Either String (Term,TrackCont,[(Int,Term)])
getForWebInterface tau =
    case runM $ alg emptyCont tau emptyTermCont of
      Nothing             -> E.Left "No Term."
      Just ((term,termCont,trackCont),debug,funcs) -> E.Right (term,trackCont,funcs)


-- | takes the input in Typ format and returns the monad's tracking information, the result term t and all term variable environment entries
getWithDebug :: Typ -> IO()
getWithDebug tau = do {printTyp tau;
		      putStr "\n";
		      case runM $ alg emptyCont tau emptyTermCont of
		      Nothing             -> putStr "No Term."
		      Just ((term,termCont,trackCont),debug,funcs) -> 
		          do {putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug));
			      printResult (term);
			      printTermCont (termCont);
			      putStr (showTrackCont trackCont);
			     }
		     }

-- | takes the input in Typ format and returns the result term
testTerm :: Typ -> Maybe Term
testTerm tau = case runM $ alg emptyCont tau emptyTermCont of
		 Nothing    -> Nothing
                 Just ((term,termCont,trackCont),_,_) -> Just (term)

-- | getComplete with prepended type parsing
getIt :: String -> IO()
getIt typstring = getComplete $ parseType typstring

-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All in pretty printing.
getContradiction :: Typ -> IO()
getContradiction tau = 
    case runM $ alg emptyCont tau emptyTermCont of
    Nothing    -> putStr "No Term.\n"
    Just ((term,termCont,trackCont),debug,funcs) ->
	let (t1',t2') = applyTrackCont term trackCont 
	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2') in
            putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug) ++
		    "TrackCont:\n\n" ++ (showTrackCont trackCont) ++
		    "TermCont:\n\n" ++ (showTermCont termCont) ++
		    "Term: " ++ (showTerm term) ++ "\n\n" ++
		    (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")

-- | getContradiction with prepended type parsing
getItContradiction :: String -> IO()
getItContradiction typstring = getContradiction $ parseType typstring
		
-- | takes the input in Typ format and returns the monad's tracking information, the disrelater entries, the term environment entries, the result term t and the result of the application of the disrelater to the term t. All _not_ in pretty printing
getRawContradiction :: Typ -> IO()
getRawContradiction tau = 
    case runM $ alg emptyCont tau emptyTermCont of
    Nothing    -> putStr "No Term.\n"
    Just ((term,termCont,trackCont),debug,funcs) ->
	let (t1',t2') = applyTrackCont term trackCont 
	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2') in
            putStr ("    " ++ (foldr (\x -> \y -> x ++ "\n    " ++ y) "\n" debug) ++
		    "TrackCont:\n\n" ++ (showRawTrackCont trackCont) ++
		    "TermCont:\n\n" ++ (show termCont) ++
		    "Term: " ++ (show term) ++ "\n\n" ++
		    (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")

-- | getRawContradiction with prepended type parsing
getItRawContradiction :: String -> IO()
getItRawContradiction typstring = getRawContradiction $ parseType typstring

-- | takes the input in Typ format and returns the result term, the disrelater and the application of the disrelater to the result term.
getExample:: Typ -> IO()
getExample tau =
    case runM $ alg emptyCont tau emptyTermCont of
    Nothing    -> putStr "No Term.\n"
    Just ((term,termCont,trackCont),debug,funcs) ->
	let (t1',t2') = applyTrackCont term trackCont 
	    (t1,t2)   = (simplifyTerm t1', simplifyTerm t2')
	    t         = Var (TermVar 0)
            (td1,td2) = applyTrackCont t trackCont 
            [term',td1',td2'] = renumberVariables [term,simplifyAppOnly td1,simplifyAppOnly td2] in
        putStr ("Term: " ++ (showTerm term') ++ "\n\n" ++
--		"Disrelater:\n\n" ++ (showTrackCont trackCont) ++
		"The disrelater applied to the term leads to: \n\n" ++ (showTerm td1') ++ " == " ++ (showTerm td2') ++ "\n\n" ++
		"which is resolved: " ++ (showTerm t1) ++ " == " ++ (showTerm t2) ++ "\n")

-- | getExample with prepended type parsing
getItExample :: String -> IO()
getItExample typstring = getExample $ parseType typstring

-- | test function for QuickCheck. It returns false, if the disrelater is not working properly, i.e. its application to the result term is not in (p+,_|_) or (_|_,_|_). It does not check for Pointedness, thus it would also accept the wrong result (_|_,_|_) on a pointed type.
testSimple :: Typ -> Bool
testSimple tau =
    case runM $ alg emptyCont tau emptyTermCont of
    Nothing    -> True
    Just ((term,termCont,trackCont),debug,funcs) ->
	let (t1,t2) = getTrackContApplicationSolved trackCont funcs term in
            case t2 of
            Bottom _ -> case t1 of
			Zero     -> True
                        Brace    -> True
		        Bottom _ -> True
                        Fls      -> True
		        Cons _ _ -> True
			Pair _ _ -> True
			Left _   -> True
                        MJust _  -> True
                        _        -> error (showTerm t1) False
            _        -> error (showTerm t1) False

-- | simulation of the web interface output of the counterexample
webInterface typString =
    let typ = parseType typString in
  putStr("The counterexample:\n\n" ++
	( case getForWebInterface typ of 
		E.Left err -> "No term could be derived: " ++ err
		E.Right result ->
	                let (term,trackCont,funcs) = result
                            names = zip (fst.unzip$funcs) drelNames in
	                ("By disregarding the strictness conditions for the chosen "++
                         "relations, setting all selectable types to () and\n\n" ++
                         assignTypeRelFuncs typ funcNames ++
                         "\n\nthe following term is a counter example:\n\n" ++
                         (termName++" = " ++ (showTerm.head.renumberVariables $ [term]))) ++
			 ("\n\nWhereas we confute the theorem by regarding:\n\n" ++
                         (prependRelFunc funcNames (fst trackCont) (showTrackContApplicationWithNames trackCont names (Var (TermVar 0)))) ++ "\n\n"++ showFuncNames (zip drelNames (snd.unzip$funcs)))
	)
        )