module Main where

import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq (getForWebInterface)
import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight(highlight)

import Network.CGI
import Data.ByteString.Lazy.UTF8 (fromString)
import Text.XHtml
import Control.Monad
import Data.Maybe
import Text.PrettyPrint.HughesPJ (render)
import qualified Data.Map as M
import Data.Generics
import Language.Haskell.FreeTheorems.Variations.PolySeq.TimeOut

askDiv v e =  maindiv << (
	p << ("To get a quick impression about the influence of strictness, toggle the let expressions between strict " +++ tt << "let!" +++ " and non-strict " +++ tt << "let" +++ ".") +++
	p << ( "You can also enter your own term, " +++
	       "e.g. " +++ primHtmlChar "ldquo" +++ tt << "/\\a.\\x::a.\\f::forall b.b->Int.seq f_{Int} (f_{a} x)" +++ primHtmlChar "rdquo" +++ "." +++ 
	p << (textarea ! [name "term", cols "80", rows "11"] << v +++
 	      submit "submit" "Generate" )) +++
	e
			 )


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

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

--generateResult :: (MonadIO t) => [Char] -> t Html
generateResult termStr = 
    do run_algorithm <- run_algorithmM
       return(askDiv termStr noHtml +++
        maindiv << (case run_algorithm of 
		Left (err,msg) -> p << case err of
                                       "TimeOut"    -> msg +++ ""
                                       "ParseError" -> "A parse error occured:" +++ pre << msg
                                       "NotTypable" -> "The term" +++ pre << tt << msg +++ "is not typable."
		Right result   ->
	                let (term,constraint,typ,normalFT,minTypeFTList) = result 
		            l = length minTypeFTList
                        in
			p << "The term" +++
	        	     pre << tt << term +++
--                        p << "can be typed to " +++ tt << typ +++ 
--			p << "if the constraint " +++
--                             pre << tt << constraint +++ "is satisfied, which leads to the optimal type(s)" +++
		        p << (if l > 1
		                then "can be typed to the optimal types" +++
	                          (if l == 2 
	                             then printTypeAndFT (head minTypeFTList) +++ "and"
                                     else (foldr (\x y -> y +++ (printTypeAndFT x) +++ ",") (""+++"") (init $ minTypeFTList)) +++ " and")
	                          +++ printTypeAndFT (last minTypeFTList)
                                else "can be typed to the optimal type" +++
                                  printTypeAndFT (head minTypeFTList))
                             +++
                        p << "The normal free theorem for the type without marks would be:" +++
                             pre << tt << (highlight normalFT)))
 where run_algorithmM = do res <- liftIO (watchdog2 3000 (getForWebInterface termStr))
			   return (case res of
			                Nothing -> Left ("TimeOut","Unfortunately the generator the type generator timed out. Time was restricted to 3 seconds.")
			                Just x  -> x)
       printTypeAndFT (tau,ft) = p << pre << tt << tau +++
                                 p << "with the free theorem" +++
				      pre << tt << (highlight ft)

main = runCGI (handleErrors cgiMain)

--cgiMain :: CGI CGIResult
cgiMain = do
	setHeader "Content-type" "text/html; charset=UTF-8"
	
	mTypeStr <- getInput "term"

	
	let content = case mTypeStr of 
		Nothing      -> return askTypeForm
                Just typeStr -> generateResult typeStr
	con  <- content
	outputFPS $ fromString $ showHtml $
	       header (
		thetitle << "Taming Selective Strictness" +++
		style ! [ thetype "text/css" ] << cdata cssStyle
	       ) +++
	       body ( form ! [method "POST", action "#"] << (
		thediv ! [theclass "top"] << (
			thespan ! [theclass "title"] << "Haskell" +++
			thespan ! [theclass "subtitle"] << "Taming Selective Strictness"
		) +++
	        maindiv ( p << ("This tool allows you to experiment with the method described in the paper "
                                +++ primHtmlChar "ldquo" 
                                +++ hotlink "http://www.iai.uni-bonn.de/~jv/atps09.pdf" 
                                    << "Taming Selective Strictness"
                                +++ primHtmlChar "rdquo"
                                +++ " (ATPS'09) by Daniel Seidel and " 
                                +++ hotlink "http://www.iai.uni-bonn.de/~jv"
                                    << (toHtml "Janis Voigtländer")
                                +++ ".")) +++
		con +++
		maindiv ( p << ("The source code is available for " +++ 
--				hotlink "http://www-ps.iai.uni-bonn.de/downloads/polyseq.tar.gz" << "download" +++
				hotlink "http://hackage.haskell.org/package/polyseq" << "download" +++
				".") +++
			   p << ("© 2009 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ ">")
			)       
		))

maindiv = thediv ! [theclass "main"]

cdata s = primHtml $
    -- ("<![CDATA[\n"++ 
    s
    -- ++ "\n]]>")

cssStyle = unlines 
        [ "body { padding:0px; margin: 0px; }"
        , "div.top { margin:0px; padding:10px; margin-bottom:20px;"
        , "              background-color:#efefef;"
        , "              border-bottom:1px solid black; }"
        , "span.title { font-size:xx-large; font-weight:bold; }"
        , "span.subtitle { padding-left:30px; font-size:large; }"
        , "div.main { border:1px dotted black;"
        , "                   padding:10px; margin:10px; }"
        , "div.submain { padding:10px; margin:11px; }"
        , "p.subtitle { font-size:large; font-weight:bold; }"
        , "input.type { font-family:monospace; }"
        , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"
        , "span.mono { font-family:monospace; }"
        , "pre { margin:10px; margin-left:20px; padding:10px;"
        , "          border:1px solid black; }"
        , "textarea { margin:10px; margin-left:20px; padding:10px;  }"
        , "p { text-align:justify; }"
        ]