{-# LANGUAGE FlexibleInstances, Rank2Types #-}
module Main where

import Network.CGI
import Text.XHtml
import Data.List (intercalate, (\\))
import Data.Maybe (fromMaybe)
import Control.Monad (MonadPlus, mzero)

import Language.Haskell.FreeTheorems
import Language.Haskell.FreeTheorems.Theorems (Theorem)

import KnownDeclarations (knownDeclarations, arbitraryButFixedTypes)
import Pages (input_page, help_page)
import FTTools
import GeneratePDF (generatePDF, generateTeX)
import TypesetAsImage (typesetAsHtmlImg)
import LogRequests (logRequest)




main = runCGI (handleErrors cgiMain)

cgiMain :: CGI CGIResult
cgiMain = do
   mb_help <- getInput "help"
   case mb_help of
      Nothing -> cgiInputPage
      Just _  -> cgiHelpPage

cgiInputPage :: CGI CGIResult
cgiInputPage = do
   inputs <- getInputs
   logRequest inputs
   let generate = case lookup "format" inputs of
                     Nothing          -> generateHTML Graphical inputs
                     Just "html+png"  -> generateHTML Graphical inputs
                     Just "html+text" -> generateHTML PlainText inputs
                     Just "tex"       -> generateTeX
                     Just "pdf"       -> generatePDF
       model   = modelFromOptions inputs
       xtraSrc = fromMaybe "" $ lookup "xtraSrc" inputs
       showTheorem = showTheoremFromOptions inputs
       outputHtml = output . renderHtml . input_page inputs
       reportError title text = outputHtml $ errorBox title text
   case lookup "type" inputs of
      Nothing -> outputHtml noHtml
      Just type_ ->
         if null type_
            then reportError "Error: Missing type" "Please enter a type in the input field."
            else case parseDeclarations knownDeclarations xtraSrc of
               Left err -> reportError "Error while parsing extra declarations" err
               Right xtraDecls ->
                  let decls = knownDeclarations ++ xtraDecls
                  in case parseTypeString decls type_ of
                     Left err -> reportError "Error while parsing type string" err
                     Right sig ->
                        case interpret decls model sig of
                           Nothing -> reportError "Error while interpreting signature" "not possible"
                           Just im -> generate model showTheorem decls sig im

modelFromOptions opts =
   case lookup "model" opts of
      Nothing      -> BasicSubset
      Just "basic" -> BasicSubset
      Just "fix"   -> SubsetWithFix style
      Just "seq"   -> SubsetWithSeq style
   where
      style = maybe EquationalTheorem styleFromOption $ lookup "style" opts
      styleFromOption "eq"   = EquationalTheorem
      styleFromOption "ineq" = InequationalTheorem

showTheoremFromOptions opts =
   case lookup "hideTypeInstantiations" opts of
      Just "yes" -> show . prettyTheorem [OmitTypeInstantiations]
      Nothing    -> show . prettyTheorem []


data FormulaeFormat = Graphical -- Formulae are rendered as graphics
                    | PlainText -- Formulae are rendered as plain text

generateHTML formulaeFormat inputs model showTheorem decls sig im = do

  -- Select the appropriate rendering action
  let (renderTheorem, renderLifts, renderClasses) =
         case formulaeFormat of
            Graphical ->
               -- Convert to string and pass to the TeX renderer.
               ( liftIO . typesetAsHtmlImg      . showTheorem . asTheorem
               , liftIO . mapM typesetAsHtmlImg . map show
               , liftIO . mapM typesetAsHtmlImg . map show
               )
            PlainText ->
               -- Just convert everything to string.
               ( return . stringToHtml . showTheorem . asTheorem
               , return . map (stringToHtml . show)
               , return . map (stringToHtml . show)
               )

  -- Render all formulae to Html/[Html] with the selected method
  theorem            <- renderTheorem im
  special_theorem    <- renderTheorem special_im
  specialInv_theorem <- renderTheorem specialInv_im
  lifts              <- renderLifts   (unfoldLifts decls im)
  special_lifts      <- renderLifts   (unfoldLifts decls special_im)
  specialInv_lifts   <- renderLifts   (unfoldLifts decls specialInv_im)
  classes            <- renderClasses (unfoldClasses decls im)
  special_classes    <- renderClasses (unfoldClasses decls special_im)
  specialInv_classes <- renderClasses (unfoldClasses decls specialInv_im)

  -- Display the result page
  output $ renderHtml $ input_page inputs $
      thediv <<
         [ h3 << ("The Free Theorem for \"" ++ show sig ++ "\"")
         , pre << theorem
         , pre `aroundEach` lifts
         , pre `aroundEach` classes
         , h3 << "Reducing all permissable relation variables to functions"
         , pre << special_theorem
         , pre `aroundEach` special_lifts
         , pre `aroundEach` special_classes
         , concatHtml $ onlyIf (isInequational model)
            [ h3 << "Reducing all permissable relation variables to the inverse of functions"
            , pre << specialInv_theorem
            , pre `aroundEach` specialInv_lifts
            , pre `aroundEach` specialInv_classes
            ]
         ]
      where
         special_im    = specialiseAll im
         specialInv_im = specialiseAllInverse im



onlyIf :: MonadPlus m => Bool -> m a -> m a
onlyIf True  x = x
onlyIf False _ = mzero

aroundEach :: (HTML a) => (Html -> Html) -> [a] -> Html
aroundEach elem (x:xs) = elem (toHtml x) +++ aroundEach elem xs
aroundEach _    []     = noHtml

errorBox :: String -> String -> Html
errorBox title text =
   thediv ! [theclass "error"] <<
      [ h3 << title
      , p << text
      ]


cgiHelpPage :: CGI CGIResult
cgiHelpPage =
   output $ renderHtml $ help_page << html
      where html = map generateDeclarationBox
               [ ("Types of predefined functions", map show . filterSignatures)
               , ("Supported algebraic data types (excluding T0 to T9)", map rawDeclarationName . filterDataDeclarations)
               , ("Supported type synonyms", map rawDeclarationName . filterTypeDeclarations)
               , ("Supported type classes", map rawDeclarationName . filterClassDeclarations)
               ]
            generateDeclarationBox (text, f) =
               thediv <<
                  [ h3 << text
                  -- Not all known declarations are shown here, just the standard Haskell ones.
                  -- This excludes the arbitrary but fixed types T0 to T9
                  , pre << (unlines $ f $ knownDeclarations \\ arbitraryButFixedTypes)
                  ]