module Main where

import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType')
import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getForWebInterface)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon(showTerm, showTrackContApplicationWithNames, showTrackContApplicationSolved, Term(Var), TermVar(..), assignTypeRelFuncs, prependRelFunc, renumberVariables, showFuncNames, showVarList, getTypeRelFuncNamesNonStrict, mapDisRelFuncsToNames)
import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
	( runChecks
	, check
	, filterSignatures
	, prettyTheorem
	, asTheorem
	, interpret
	, unfoldLifts
	, prettyUnfoldedLift
	, LanguageSubset(SubsetWithFix)
        , TheoremType(EquationalTheorem)
	, PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets)
        , specialise
        , relationVariables
	)

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.CounterExamples.Internal.TimeOut
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync


askDiv v e =  maindiv << (
	p << ( "Please enter a type. " +++
	       "You can prepend it with a list of type variables " +++
	       "that should not be considered for counterexample generation, e.g. " +++ primHtmlChar "ldquo"  +++ tt << "a b. ((a,c) -> b) -> b" +++ primHtmlChar "rdquo" +++ "." +++
	       p << ( input ! [name "type", value v] +++ " " +++
 	       submit "submit" "Generate" )) +++
	e
	)


askTypeForm = askDiv "[a] -> [a]" noHtml

typeError typeStr err = askDiv typeStr (
	p << ("There was a problem parsing your type: " +++
  	      pre << err )
	)

generateResult typeStr typ = 
    do counter_example <- counter_exampleM
       return (askDiv typeStr noHtml +++
	maindiv << (
	h3 << "The Free Theorem" +++
	(case ft_full of
		Left err -> p << "The full Free Theorem deriver failed:" +++
                            pre << err
                Right s  -> p << "The theorem generated for functions of the type" +++
	                    pre << (termName ++ " :: " ++ dropedPreFix) +++
	                    "is:" +++
         	            pre << s
	)) +++
	maindiv << (
	h3 << "The Counterexample" +++
	( case counter_example of 
		Left err -> p << if err == "_timeOut" 
	                         then "Unfortunately the generator for the counterexample timed out. Time was restricted to 3 seconds." +++ ""
	                         else (let nonstrict = getTypeRelFuncNamesNonStrict typ funcNames in
                                       case nonstrict of
				         []  -> "No type variables were made available for consideration for counterexample generation." +++ ""
                                         [x] -> "Even without strictness condition on " +++ tt << x +++ " the algorithm found no counterexample."
				         xs  -> "Even without strictness conditions on " +++ tt <<showVarList xs +++ " the algorithm found no counterexample.")
		Right result ->
	                let (term,trackCont,funcs) = result
                            names = mapDisRelFuncsToNames funcs drelNames varNames 
                            nonstricts = getTypeRelFuncNamesNonStrict typ funcNames in
			p << ((if length nonstricts == 1 
			      then ("By disregarding the strictness condition on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")
			      else ("By disregarding the strictness conditions on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")) +++
                             " The term" +++
	        	     pre << tt << (termName ++ " = " ++ (showTerm.head.renumberVariables $ [term])) +++
                             "is a counterexample.") +++
                        p << ("By setting " +++ tt << "t1 = t2 = ... = ()" +++ " and" +++
                             pre << assignTypeRelFuncs typ funcNames) +++
			p << ("the following would be a consequence of the thus " +++ primHtmlChar "ldquo" +++ "naivified" +++ primHtmlChar "rdquo" +++ " free theorem:" +++
                              pre << prependRelFunc funcNames (fst trackCont) ((showTrackContApplicationWithNames trackCont names (Var (TermVar 0))) ++ "\n\nwhere\n\n" ++  showFuncNames (zip (snd.unzip$names) (snd.unzip$funcs)))) +++
			p << ("But this is wrong since with the above " +++ tt << termName +++ " it reduces to:" +++
			      pre << prependRelFunc funcNames (fst trackCont) (showTrackContApplicationSolved trackCont funcs term))
	)))
  where ft_full = let properType = termName ++ " :: " ++ case span (/='.') typeStr of
                                       (t,"")  -> t
                                       (_,_:t) -> t
		      either  = "data Either a b = Left a | Right b"
                      bool    = "data Bool = False | True"
		      maybe   = "data Maybe a = Nothing | Just a"
		      parse_input = unlines [either, bool, maybe, properType]
		      (ds,es) = runChecks (parse parse_input >>= check)
                      [s]     = filterSignatures ds
		  in if null es
                     then case interpret ds (SubsetWithFix  EquationalTheorem) s of
			Nothing -> Left "interpret returned nothing"
			Just i  -> let i' = foldl specialise i (relationVariables i) in
                                   Right $ render (prettyTheorem [OmitTypeInstantiations,OmitLanguageSubsets] (asTheorem i')) ++
			      case unfoldLifts ds i' of
				[] -> ""
				ls -> (if length ls == 1 
				       then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
				       else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
				      unlines (map (render . prettyUnfoldedLift []) ls)
                     else Left (unlines (map render es))
		    
        counter_exampleM = do res <- liftIO (watchdog2 3000 (getForWebInterface typ))
			      return (case res of
			                Nothing -> Left "_timeOut"
			                Just x  -> x)
	dropedPreFix = let (prefix,typ) = break (=='.') typeStr in
                       if typ == [] then prefix else tail typ 
	
main = runCGI (handleErrors cgiMain)

cgiMain = do
	setHeader "Content-type" "text/xml; charset=UTF-8"
	
	mTypeStr <- getInput "type"

	
	let content = case mTypeStr of 
		Nothing      -> return askTypeForm
                Just typeStr -> case parseType' typeStr of
			Left err  -> return (typeError typeStr err)
			Right typ -> generateResult typeStr typ
	con  <- content
	outputFPS $ fromString $ showHtml $
	       header (
		thetitle << "Automatically Generating Counterexamples to Naive Free Theorems" +++
		style ! [ thetype "text/css" ] << cdata cssStyle
	       ) +++
	       body ( form ! [method "POST", action "#"] << (
		thediv ! [theclass "top"] << (
			thespan ! [theclass "title"] << "Haskell" +++
			thespan ! [theclass "subtitle"] << "Automatically Generating Counterexamples to Naive Free Theorems"
		) +++
               maindiv ( p << ("This tool allows you to run the algorithm described in the paper "
	       +++ primHtmlChar "ldquo"
               +++ hotlink "http://www.iai.uni-bonn.de/~jv/paper.pdf" 
               << "Automatically Generating Counterexamples to Naive Free Theorems"
	       +++ primHtmlChar "rdquo" 
       	       +++ " (FLOPS'10) by Daniel Seidel and " 
               +++ hotlink "http://www.iai.uni-bonn.de/~jv"
               << (toHtml "Janis Voigtländer")
                +++ ".") 
               +++ p << ("You may also want to try the following related tools:" 
                         +++ ulist << [ li << (primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/ft" << "Automatic Generation of Free Theorems" +++ primHtmlChar "rdquo") 
                                      , li << (primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi" << "Taming Selective Strictness" +++ primHtmlChar "rdquo") 
                                      ])) +++
		con +++
		maindiv ( p << ("The source code is available for " +++ 
				hotlink "http://hackage.haskell.org/package/free-theorems-counterexamples" << "download" +++
				".") +++
			   p << ("© 2010 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ "> and Joachim Breitner <" +++
				hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.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; }"
        ]