{- |
Module      :  Web.Handler
Description :  Application-specific handler functions.
Copyright   :  (c) 2011 Cedric Staub
License     :  GPL-3

Maintainer  :  Cedric Staub <cstaub@ethz.ch>
Stability   :  experimental
Portability :  non-portable
-}

{-# LANGUAGE
    OverloadedStrings, QuasiQuotes, TypeFamilies, 
    RankNTypes, TemplateHaskell, CPP #-}

module Web.Handler
  ( getOverviewR
  , getRootR
  , postRootR
  , getTheorySourceR
  , getTheoryMessageDeductionR
  , getTheoryVariantsR
  , getTheoryPathMR
  , getTheoryPathDR
  , getTheoryGraphR
  , getAutoProverR
  , getDeleteStepR
  , getKillThreadR
  , getNextTheoryPathR
  , getPrevTheoryPathR
  , getSaveTheoryR
  , getDownloadTheoryR
  , getEditTheoryR
  , postEditTheoryR
  , getEditPathR
  , postEditPathR
  , getUnloadTheoryR
  , getThreadsR
  )
where

import Theory (
    ClosedTheory,
    lName, thyName, 
    lookupLemma, addLemma, removeLemma,
    openTheory, 
    mapProverProof, sorryProver, autoProver, cutOnAttackDFS,
    prettyProof, prettyLemma, prettyClosedTheory, prettyOpenTheory 
  )
import Theory.Parser
import Theory.Proof.Sequent.Dot
import Web.Types
import Web.Hamlet
import Web.Theory
import Web.Instances ()
import Web.Settings
import Text.PrettyPrint.Html

import Yesod.Core
import Yesod.Json()
import Yesod.Form
import Text.Hamlet

import Data.Maybe
import Data.Aeson
import Data.Aeson.Encode (fromValue)
import Data.Label
import Data.Traversable (traverse)

import qualified Data.Map as M
import qualified Data.Text as T
import qualified Data.Traversable as Tr
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.Text.Encoding
import qualified Blaze.ByteString.Builder   as B
import Network.HTTP.Types ( urlDecode )

import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.IO.Control
import Control.Applicative
import Control.Concurrent
import Control.DeepSeq
import qualified Control.Exception.Control as E
import Control.Exception.Base
import qualified Control.Concurrent.Thread as Thread ( forkIO )
import Data.Time.LocalTime
import qualified Data.Binary as Bin
import System.Directory

import Debug.Trace (trace)

-- Quasi-quotation syntax changed from GHC 6 to 7,
-- so we need this switch in order to support both
#if __GLASGOW_HASKELL__ >= 700
#define HAMLET hamlet
#else
#define HAMLET $hamlet
#endif


------------------------------------------------------------------------------
-- Manipulate the state
------------------------------------------------------------------------------

-- | Store theory map in file if option enabled.
storeTheory :: WebUI
               -> TheoryInfo
               -> TheoryIdx
               -> IO ()
storeTheory yesod thy idx =
    when (autosaveProofstate yesod) $ do
      let f = workDir yesod++"/"++autosaveSubdir++"/"++show idx++".img"
      Bin.encodeFile (f++".tmp") thy
      renameFile (f++".tmp") f

-- | Load a theory given an index.
getTheory :: MonadIO m
           => TheoryIdx
           -> GenericHandler m (Maybe TheoryInfo)
getTheory idx = do
    yesod <- getYesod
    liftIO $ withMVar (theoryVar yesod) $ return . M.lookup idx

-- | Store a theory, return index.
putTheory :: MonadIO m
           => Maybe TheoryInfo     -- ^ Index of parent theory
           -> Maybe TheoryOrigin   -- ^ Origin of this theory
           -> ClosedTheory         -- ^ The new closed theory
           -> GenericHandler m TheoryIdx
putTheory parent origin thy = do
    yesod <- getYesod
    liftIO $ modifyMVar (theoryVar yesod) $ \theories -> do
      time <- getZonedTime
      let idx = if M.null theories then 1 else fst (M.findMax theories) + 1
          parentIdx = tiIndex <$> parent
          parentOrigin = tiOrigin <$> parent
          newOrigin = parentOrigin <|> origin <|> (Just Interactive)
          newThy = TheoryInfo idx thy time parentIdx False (fromJust newOrigin)
      storeTheory yesod newThy idx
      return (M.insert idx newThy theories, idx)

-- | Delete theory.
delTheory :: MonadIO m => TheoryIdx -> GenericHandler m ()
delTheory idx = do
    yesod <- getYesod
    liftIO $ modifyMVar_ (theoryVar yesod) $ \theories -> do
      let theories' = M.delete idx theories
      -- FIXME: delete from autosave directory?
      return theories'

-- | Get a map of all stored theories.
getTheories :: MonadIO m => GenericHandler m TheoryMap
getTheories = do
    yesod <- getYesod
    liftIO $ withMVar (theoryVar yesod) return


-- | Modify a theory in the map of theories.
adjTheory :: MonadIO m
          => TheoryIdx
          -> (TheoryInfo -> TheoryInfo)
          -> GenericHandler m ()
adjTheory idx f = do
    yesod <- getYesod
    liftIO $ modifyMVar_ (theoryVar yesod) $ \theories ->
      case M.lookup idx theories of
        Just thy -> do
          let newThy =  f thy
          storeTheory yesod newThy idx
          return $ M.insert idx newThy theories
        Nothing -> error "adjTheory: invalid theory index"

-- | Debug tracing.
dtrace :: WebUI -> String -> a -> a
dtrace yesod msg | debug yesod = trace msg
                 | otherwise   = id

-- | Register a thread for killing.
putThread :: MonadControlIO m
          => T.Text                      -- ^ Request path
          -> ThreadId                    -- ^ Thread ID
          -> GenericHandler m ()
putThread str tid = do
    yesod <- getYesod
    liftIO $ dtrace yesod msg $
      modifyMVar_ (threadVar yesod) $ return . (M.insert str tid)
  where
    msg = "Registering thread: " ++ T.unpack str

-- | Unregister a thread for killing.
delThread :: MonadControlIO m
          => T.Text       -- ^ Request path
          -> GenericHandler m ()
delThread str = do
    yesod <- getYesod
    liftIO $ dtrace yesod msg $
      modifyMVar_ (threadVar yesod) $ return . (M.delete str)
  where
    msg = "Deleting thread: " ++ T.unpack str

-- | Get a thread for the given request URL.
getThread :: MonadIO m
          => T.Text       -- ^ Request path
          -> GenericHandler m (Maybe ThreadId)
getThread str = do
    yesod <- getYesod
    liftIO $ dtrace yesod msg $
      withMVar (threadVar yesod) $ return . M.lookup str
  where
    msg = "Retrieving thread id of: " ++ T.unpack str

-- | Get the map of all threads.
getThreads :: MonadIO m
           => GenericHandler m [T.Text]
getThreads = do
    yesod <- getYesod
    liftIO $ withMVar (threadVar yesod) (return . M.keys)


------------------------------------------------------------------------------
-- Helper functions
------------------------------------------------------------------------------

-- | Print exceptions, if they happen.
traceExceptions :: MonadControlIO m => String -> m a -> m a
traceExceptions info = 
    E.handle handler
  where
    handler :: MonadControlIO m => E.SomeException -> m a
    handler e =
      trace (info ++ ": exception `" ++ show e ++ "'") $ 
          liftIO $ E.throw e

-- | Helper functions for generating JSON reponses.
jsonResp :: Monad m => JsonResponse -> GenericHandler m RepJson
jsonResp = return . RepJson . toContent . fromValue . responseToJson

responseToJson :: JsonResponse -> Value
responseToJson = go
  where
    jsonObj key val = object [ key .= val ]

    go (JsonAlert msg)          = jsonObj "alert" $ toJSON msg
    go (JsonRedirect url)       = jsonObj "redirect" $ toJSON url
    go (JsonHtml title content) = object
      [ "html"  .= contentToJson content
      , "title" .= title ]
    
    contentToJson (ContentBuilder b _) = toJSON $ B.toLazyByteString b 
    contentToJson _ = error "Unsupported content format in json response!"

-- | Fully evaluate a value in a thread that can be canceled.
evalInThread :: (NFData a, MonadControlIO m)
             => IO a
             -> GenericHandler m (Either SomeException a)
evalInThread io = do
    renderF <- getUrlRender
    maybeRoute <- getCurrentRoute
    case maybeRoute of
      Just route -> do
        let key = renderF route
        (tid, wait) <- liftIO $ Thread.forkIO $ do x <- io
                                                   evaluate (rnf x)
                                                   return x
        putThread key tid
        res <- liftIO $ wait
        delThread key
        return res
      Nothing -> Right `liftM` liftIO io

-- | Evaluate a handler with a given theory specified by the index,
-- return notFound if theory does not exist.
withTheory :: MonadIO m
           => TheoryIdx
           -> (TheoryInfo -> GenericHandler m a)
           -> GenericHandler m a
withTheory idx handler = do
  maybeThy <- getTheory idx
  case maybeThy of
    Just ti -> handler ti
    Nothing -> notFound

-- | Run a form and provide a JSON response.
formHandler :: (HamletValue h, HamletUrl h ~ WebUIRoute, h ~ Widget ())
            => T.Text                              -- ^ The form title
            -> Form WebUI WebUI a                  -- ^ The formlet to run
            -> (Widget () -> Enctype -> Html -> h) -- ^ Template to render form with
            -> (a -> GenericHandler IO RepJson)    -- ^ Function to call on success
            -> Handler RepJson
formHandler title formlet template success = do
    (result, widget, enctype, nonce) <- runFormPost formlet
    case result of
      FormMissing -> do
        RepHtml content <- ajaxLayout (template widget enctype nonce)
        jsonResp $ JsonHtml title content
      FormFailure _ -> jsonResp $ JsonAlert
        "Missing fields in form. Please fill out all required fields."
      FormSuccess ret -> liftIOHandler (success ret)


-- | Modify a theory, redirect if successful.
modifyTheory :: (MonadControlIO m, Functor m)
             => TheoryInfo                                -- ^ Theory to modify
             -> (ClosedTheory -> IO (Maybe ClosedTheory)) -- ^ Function to apply
             -> JsonResponse                              -- ^ Response on failure
             -> GenericHandler m Value
modifyTheory ti f errResponse = do
    -- res <- evalInThread (liftIO $ f (tiTheory ti))
    res <- evalInThread (liftIO $ f (tiTheory ti))
    case res of
      Left e           -> return (excResponse e)
      Right Nothing    -> return (responseToJson errResponse)
      Right (Just thy) -> do
        newThyIdx <- putTheory (Just ti) Nothing thy
        newUrl <- getUrlRender <*> pure (OverviewR newThyIdx) 
        return . responseToJson $ JsonRedirect newUrl
  where
   excResponse e = responseToJson
                     (JsonAlert $ "Last request failed with exception: " `T.append` (T.pack (show e)))

------------------------------------------------------------------------------
-- Handler functions
------------------------------------------------------------------------------

-- | The root handler lists all theories by default,
-- or load a new theory if the corresponding form was submitted.
getRootR :: Handler RepHtml
getRootR = postRootR

postRootR :: Handler RepHtml
postRootR = do
    (result, widget, enctype, nonce) <- runFormPost submitForm
    case result of
      FormMissing -> return ()
      FormFailure errs -> do
        mapM_ (liftIO . print) errs
        setMessage "Loading failed."
      FormSuccess fileinfo -> do
        yesod <- getYesod
        closedThy <- parseThy yesod (BS.unpack $ fileContent fileinfo)
        void $ putTheory Nothing
          (Just $ Upload $ T.unpack $ fileName fileinfo) closedThy
        setMessage "Loaded new theory!"
    theories <- getTheories
    defaultLayout $ do
      setTitle "Welcome to the tamarin prover"
      addWidget (rootTpl theories widget enctype nonce)
  where
    submitForm = fieldsToDivs $ fileField $ FormFieldSettings
      "Select file:" "Select file" Nothing Nothing


-- | Show overview over theory (framed layout).
getOverviewR :: TheoryIdx -> Handler RepHtml
getOverviewR idx = withTheory idx $ \ti -> defaultLayout $ do
  overview <- liftIO $ overviewTpl ti TheoryMain
  setTitle (toHtml $ "Theory: " ++ get thyName (tiTheory ti))
  addWidget overview

-- | Show source (pretty-printed open theory).
getTheorySourceR :: TheoryIdx -> Handler RepPlain
getTheorySourceR idx = withTheory idx $ \ti ->
  return $ RepPlain $ toContent $ prettyRender ti
  where 
    -- prettyRender = render . prettyOpenTheory . openTheory . tiTheory
    prettyRender = render . prettyClosedTheory . tiTheory

-- | Show variants (pretty-printed closed theory).
getTheoryVariantsR :: TheoryIdx -> Handler RepPlain
getTheoryVariantsR idx = withTheory idx $ \ti ->
  return $ RepPlain $ toContent $ prettyRender ti
  where prettyRender = render . prettyClosedTheory . tiTheory

-- | Show variants (pretty-printed closed theory).
getTheoryMessageDeductionR :: TheoryIdx -> Handler RepPlain
getTheoryMessageDeductionR idx = withTheory idx $ \ti ->
  return $ RepPlain $ toContent $ prettyRender ti
  where prettyRender = render . prettyClosedTheory . tiTheory


-- | Show a given path within a theory (main view).
getTheoryPathMR :: TheoryIdx
                -> TheoryPath
                -> Handler RepJson
getTheoryPathMR idx path = liftIOHandler $ do
    jsonValue <- withTheory idx (go path)
    return $ RepJson $ toContent $ fromValue jsonValue
  where
    --
    -- Handle method paths by trying to solve the given goal/method
    --
    go (TheoryMethod lemma proofPath i) ti = modifyTheory ti
      (\thy -> return $ applyMethodAtPath thy lemma proofPath i)
      (JsonAlert "Sorry, but the prover failed on the selected method!")

    --
    -- Handle generic paths by trying to render them
    --
    go _ ti = do
      let title = T.pack $ titleThyPath (tiTheory ti) path
      let html = T.pack $ renderHtmlDoc $ htmlThyPath (tiTheory ti) path
      return $ responseToJson (JsonHtml title (toContent html))


-- | Show a given path within a theory (debug view).
getTheoryPathDR :: TheoryIdx -> TheoryPath -> Handler RepHtml
getTheoryPathDR idx path = withTheory idx $ \ti -> ajaxLayout $ do
  let maybeDebug = htmlThyDbgPath (tiTheory ti) path
  let maybeWidget = wrapHtmlDoc <$> maybeDebug
  addWidget [HAMLET|
    <h2>Theory information</h2>
    <ul>
      <li>Index = #{show (tiIndex ti)}
      <li>Path = #{show path}
      <li>Time = #{show (tiTime ti)}
      <li>Origin = #{show (tiOrigin ti)}
      <li>NextPath = #{show (nextThyPath (tiTheory ti) path)}
      <li>PrevPath = #{show (prevThyPath (tiTheory ti) path)}
      <li>NextSmartPath = #{show (nextSmartThyPath (tiTheory ti) path)}
      <li>PrevSmartPath = #{show (prevSmartThyPath (tiTheory ti) path)}
    $if isJust maybeWidget
      <h2>Current sequent</h2><br>
      \^{fromJust maybeWidget}
  |]

-- | Get rendered graph for theory and given path.
getTheoryGraphR :: TheoryIdx -> TheoryPath -> Handler ()
getTheoryGraphR idx path = withTheory idx $ \ti -> do
      yesod <- getYesod
      compact <- isNothing <$> lookupGetParam "uncompact"
      compress <- isNothing <$> lookupGetParam "uncompress"
      png <- liftIO $ traceExceptions "getTheoryGraphR" $
        pngThyPath
          (workDir yesod)
          (graphStyle compact compress)
          (tiTheory ti) path
      sendFile "image/png" png
  where
    graphStyle d c = dotStyle d . compression c
    dotStyle True = dotSequentCompact
    dotStyle False = dotSequentLoose
    compression True = compressSequent
    compression False = id

-- | Kill a thread (aka 'cancel request').
getKillThreadR :: Handler RepPlain
getKillThreadR = liftIOHandler $ do
    maybeKey <- lookupGetParam "path"
    case maybeKey of
      Just key0 -> do
        let key = decodeUtf8 . urlDecode True . encodeUtf8 $ key0
        tryKillThread key
        return $ RepPlain $ toContent ("Canceled request!" :: T.Text)
      Nothing -> invalidArgs ["No path to kill specified!"]
  where
    -- thread waiting for the result is responsible for
    -- updating the ThreadMap.
    tryKillThread k = do
      maybeTid <- getThread k
      case maybeTid of
        Nothing  -> trace ("Killing failed: "++ T.unpack k) $ return ()
        Just tid -> trace ("Killing: " ++ T.unpack k)
                          (liftIO $ killThread tid)

-- | Get the 'next' theory path for a given path.
-- This function is used for implementing keyboard shortcuts.
getNextTheoryPathR :: TheoryIdx         -- ^ Theory index
                   -> String            -- ^ Jumping mode (smart?)
                   -> TheoryPath        -- ^ Current path
                   -> Handler RepPlain
getNextTheoryPathR idx md path = withTheory idx $ \ti -> return $
    RepPlain $ toContent $ joinPath' $ renderPath $ next md (tiTheory ti) path
  where
    next "normal" = nextThyPath
    next "smart"  = nextSmartThyPath
    next _        = const id

-- | Get the 'prev' theory path for a given path.
-- This function is used for implementing keyboard shortcuts.
getPrevTheoryPathR :: TheoryIdx -> String -> TheoryPath -> Handler RepPlain
getPrevTheoryPathR idx md path = withTheory idx $ \ti -> return $
    RepPlain $ toContent $ joinPath' $ renderPath $ prev md (tiTheory ti) path
  where
    prev "normal" = prevThyPath
    prev "smart" = prevSmartThyPath
    prev _ = const id

-- | Get the edit theory page.
getEditTheoryR :: TheoryIdx -> Handler RepJson
getEditTheoryR = postEditTheoryR

-- | Post edit theory page form data.
postEditTheoryR :: TheoryIdx -> Handler RepJson
postEditTheoryR idx = withTheory idx $ \ti -> formHandler
    "Edit theory"
    (theoryFormlet ti)
    theoryFormTpl $ \(Textarea input) ->
      E.handle exHandler $ do
        yesod <- getYesod
        closedThy <- checkProofs <$> parseThy yesod (T.unpack input)
        newIdx <- putTheory (Just ti) Nothing closedThy
        jsonResp . JsonRedirect =<<
          getUrlRender <*> pure (OverviewR newIdx)
  where
    theoryFormlet ti = fieldsToDivs $ textareaField
      (FormFieldSettings
        ("Edit theory source: " `T.append` name ti)
        (toHtml $ name ti) Nothing Nothing)
      (Just $ Textarea $ T.pack $ render $ prettyClosedTheory $ tiTheory ti)

    exHandler :: MonadControlIO m => E.SomeException -> GenericHandler m RepJson
    exHandler err = jsonResp $ JsonAlert $ T.unlines
      [ "Unable to load theory due to parse error!"
      , "Parser returned the message:"
      , T.pack $ show err ]

    name = T.pack . get thyName . tiTheory
    theoryFormTpl = formTpl (EditTheoryR idx) "Load as new theory" 

-- | Get the add lemma page.
getEditPathR :: TheoryIdx -> TheoryPath -> Handler RepJson
getEditPathR = postEditPathR

-- | Post edit theory page form data.
postEditPathR :: TheoryIdx -> TheoryPath -> Handler RepJson
postEditPathR idx (TheoryLemma lemmaName) = withTheory idx $ \ti -> do
    yesod <- getYesod
    let lemma = lookupLemma lemmaName (tiTheory ti)
    formHandler
      (T.pack $ action lemma)
      (formlet lemma)
      (lemmaFormTpl lemma) $ \(Textarea input) ->
        case parseLemma (T.unpack input) of
          Left err -> jsonResp $ JsonAlert $ T.unlines
            [ "Unable to add lemma to theory due to parse error!"
            , "Parser returned the message:"
            , T.pack $ show err ]
          Right newLemma -> (RepJson . toContent . fromValue) <$> modifyTheory ti
            -- Add or replace lemma
            (\thy -> do
              let openThy  = openTheory thy
                  openThy' = case lemma of
                    Nothing -> addLemma newLemma openThy
                    Just _  -> removeLemma lemmaName openThy 
                                  >>= addLemma newLemma
              traverse (closeThy yesod) openThy')
            -- Error response
            (JsonAlert $ T.unwords
               [ "Unable to add lemma to theory."
               , "Does a lemma with the same name already exist?" ])
  where
    path (Just l) = TheoryLemma (get lName l)
    path Nothing = TheoryLemma ""

    action (Just l) = "Edit lemma " ++ get lName l
    action Nothing = "Add new lemma"

    formlet lemma = fieldsToDivs $ textareaField
      (FormFieldSettings
        (T.pack $ action lemma)
        (toHtml $ action lemma)
        Nothing Nothing)
      (Textarea . T.pack . render . prettyLemma prettyProof <$> lemma)

    lemmaFormTpl lemma = formTpl (EditPathR idx (path lemma)) "Submit"

postEditPathR _ _ =
  jsonResp $ JsonAlert $ "Editing for this path is not implemented!"


-- | Run the autoprover on a given proof path.
getAutoProverR :: TheoryIdx -> TheoryPath -> Handler RepJson
getAutoProverR idx path = liftIOHandler $ do
    jsonValue <- withTheory idx (go path)
    return $ RepJson $ toContent $ fromValue jsonValue
  where
    go (TheoryProof lemma proofPath) ti = modifyTheory ti
      (\thy -> 
          return $ applyProverAtPath thy lemma proofPath (mapProverProof cutOnAttackDFS autoProver))
      (JsonAlert "Sorry, but the autoprover failed on given proof step!")

    go _ _ = return . responseToJson $ JsonAlert
      "Can't run autoprover on the given theory path!"

-- | Delete a given proof step.
getDeleteStepR :: TheoryIdx -> TheoryPath -> Handler RepJson
getDeleteStepR idx path = liftIOHandler $ do
    jsonValue <- withTheory idx (go path)
    return $ RepJson $ toContent $ fromValue jsonValue
  where
    go (TheoryLemma lemma) ti = modifyTheory ti
      (return . removeLemma lemma)
      (JsonAlert "Sorry, but removing the selected lemma failed!")

    go (TheoryProof lemma proofPath) ti = modifyTheory ti
      (\thy -> return $ 
          applyProverAtPath thy lemma proofPath (sorryProver "removed"))
      (JsonAlert "Sorry, but removing the selected proof step failed!")

    go _ _ = return . responseToJson $ JsonAlert
      "Can't delete the given theory path!"

-- | Save a theory to the working directory.
getSaveTheoryR :: TheoryIdx -> Handler RepJson
getSaveTheoryR idx = withTheory idx $ \ti -> do
    let origin = tiOrigin ti
    case origin of
      -- Saving interactive/uploaded files not supported yet.
      Interactive -> notFound
      Upload _ -> notFound
      -- Saving of local files implemented.
      Local file -> do
        -- Save theory to disk
        liftIO $ writeFile file (prettyRender ti)
        -- Find original theorie(s) with same origin
        -- Set original -> modified
        thys <- M.filter (same origin) <$> getTheories
        _ <- Tr.mapM (\t -> adjTheory (tiIndex t) (setPrimary False)) thys
        -- Find current theory
        -- Set modified -> original
        adjTheory (tiIndex ti) (setPrimary True)
        -- Return message
        jsonResp (JsonAlert $ T.pack $ "Saved theory to file: " ++ file)
  where
    prettyRender = render . prettyOpenTheory . openTheory . tiTheory
    same origin ti = tiPrimary ti && (tiOrigin ti == origin)
    setPrimary bool ti = ti { tiPrimary = bool }


-- | Prompt downloading of theory.
getDownloadTheoryR :: TheoryIdx -> String -> Handler (ContentType, Content)
getDownloadTheoryR idx _ = do
    RepPlain source <- getTheorySourceR idx
    return (typeOctet, source)

-- | Unload a theory from the interactive server.
getUnloadTheoryR :: TheoryIdx -> Handler RepPlain
getUnloadTheoryR idx = do
    delTheory idx 
    redirect RedirectPermanent RootR

-- | Show a list of all currently running threads.
getThreadsR :: Handler RepHtml
getThreadsR = do
    threads <- getThreads
    defaultLayout $ do
      setTitle "Registered threads"
      addWidget (threadsTpl threads)