module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq where

import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg
import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon(removeTrue,getEquals,instantiateWithEpsilon)
import Language.Haskell.FreeTheorems.Variations.PolySeq.M
import Language.Haskell.FreeTheorems.Variations.PolySeq.TheoremGen
import Language.Haskell.FreeTheorems.Variations.PolySeq.ConstraintSolver
import Text.PrettyPrint(renderStyle,Style(..),Mode(..),(<+>),text)
import Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint
import Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag)
import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight
import Text.XHtml hiding(text)

--polySeq :: Term -> Maybe (Constraint,Typ)
polySeq =  runM.algPolySeq

shellStyle = Style PageMode 80 0.2
webStyle = Style PageMode 80 0.2

--getItT :: Term -> IO()
getItT t = 
    case polySeq t of
      Just ((t',c,tau),_) -> do{ putStr "The term: ";
				 putStr (renderStyle shellStyle (prettyMarkedTerm t'));
				 putStr "\n\nThe Constraint: ";
				 putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
				 putStr "\n\nWith the equations: ";
				 putStr (show (getEquals c));
				 putStr "\n\nThe Type:";
				 putStr (renderStyle shellStyle (prettyMarkedTyp tau));
				 putStr "\n\nUsed Label Variables: ";
				 putStr "\n\n newSimplify:\n\n";
				 let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
				 do{putStr "The term: ";
				    putStr (renderStyle shellStyle (prettyMarkedTerm ts));
				    putStr "\n\nThe Constraint: ";
				    putStr (renderStyle shellStyle (prettyConstraint cs));
				    putStr "\n\nThe Type:";
				    putStr (renderStyle shellStyle (prettyMarkedTyp taus));
				    putStr "\n\nWhich optimal would be:";
				    putStr (show (getOpt True taus));
				    putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
				    putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n"++y) ""
					    (makeTypes taus ((filterTyp taus).solveConstraint$cs)));
				    putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
				    putStr (foldr (\x y->(renderStyle shellStyle (prettyMarkedTyp x))++"\n\n"++y) ""
					    (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
				   };
				 putStr "\n\n";
			    }
      Nothing            -> putStr "Term is not typable at all.\n"

--getItTRaw :: Term -> IO()
getItTRaw t = 
    case polySeq t of
      Just ((t',c,tau),_) -> do{ putStr "The term: ";
				 putStr (renderStyle shellStyle (prettyMarkedTerm t'));
				 putStr "\n\nThe Constraint: ";
				 putStr (renderStyle shellStyle (prettyConstraint (removeTrue c)));
				 putStr "\n\nWith the equations: ";
				 putStr (show (getEquals c));
				 putStr "\n\nThe Type:";
				 putStr (renderStyle shellStyle (prettyMarkedTyp tau));
				 putStr "\n\nUsed Label Variables: ";
				 putStr "\n\n newSimplify:\n\n";
				 let (ts,taus,cs) = simplifyConstraint (t',tau,c) in
				 do{putStr "The term: ";
				    putStr (renderStyle shellStyle (prettyMarkedTerm ts));
				    putStr "\n\nThe Constraint: ";
				    putStr (renderStyle shellStyle (prettyConstraint cs));
				    putStr "\n\nThe Type:";
				    putStr (renderStyle shellStyle (prettyMarkedTyp taus));
				    putStr "\n\nWhich optimal would be:";
				    putStr (show (getOpt True taus));
				    putStr "\n\nThat means, it is typable to the following concrete Types\n\n";
				    putStr (foldr (\x y->(show x)++"\n\n"++y) ""
					    (makeTypes taus ((filterTyp taus).solveConstraint$cs)));
				    putStr "\n\nAnd consequently, it is typable to the following minimal concrete Types\n\n";
				    putStr (foldr (\x y->(show x)++"\n\n"++y) ""
					    (makeMinimalTypes taus ((filterTyp taus).solveConstraint$cs)));
				   };
				 putStr "\n\n";
			    }
      Nothing            -> putStr "Term is not typable at all.\n"

getIt str = 
    case parseTerm str of
      Left err -> putStr (show err)
      Right t  -> getItT t

getItRaw str =
    case parseTerm str of
      Left err -> putStr (show err)
      Right t  -> getItTRaw t


--                    termstring         (ErrType,ErrMsg) (Term  ,Constraint,Typ   ,NormalFT, [(MinTyp,FT)])
getForWebInterface :: String  ->  Either (String, String) (String,String,      String,String,  [(String,String)])
getForWebInterface termstr =
    case parseTermWithFlag termstr of
      Left err       -> Left ("ParseError",(show err))
      Right (t,flag) -> case polySeq t of
                           Just ((t'',c',tau'),_) -> 
			     let (t',tau,c)   = simplifyConstraint (t'',tau',c')
                                 minTypes     = makeMinimalTypes tau ((filterTyp tau).solveConstraint$c)
                                 optFT        = map (fromRight.(makeFTFullFuncWithFlag flag)) minTypes
                                 minTypFTList = zip (map ((renderStyle webStyle).prettyMarkedTyp) minTypes) optFT
                                 normalFT     = fromRight.(makeFTFullFuncWithFlag flag).instantiateWithEpsilon$ tau'
                                 termStr      = renderStyle webStyle (text "t =" <+> prettyUnMarkedTerm (adjustTypAbstraction flag t'))
                                 constStr     = renderStyle webStyle (prettyConstraint c)
                                 tauStr       = renderStyle webStyle (prettyMarkedTyp tau)
                             in
			     Right (termStr, constStr, tauStr,normalFT,minTypFTList)
                           Nothing             -> Left ("NotTypable",renderStyle webStyle (prettyUnMarkedTerm t))
    where fromRight (Right x) = x



testTerm = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs }))"

test = case getForWebInterface testTerm of
	 Left _ -> putStr "shit happened."
         Right (t,c,tau,nft,l) -> do{ putStr "\n\nThe normal Theorem:\n\n";
				      putStr nft;
				      putStr "\n\nThe highlighted version:\n\n";
				      putStr (show.highlight$nft);
				    }

foldl'' = "/\\a./\\b.\\c :: a -> b -> a.let! c' = c in fix ( \\h :: a -> [b] -> a.\\n :: a.\\ys :: [b].let c'' = c n in case ys of {[]   -> n; x:xs -> let! xs' = xs in let! x' = x in let n' = c'' x' in h n' xs' })"