{-# LANGUAGE CPP               #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes       #-}
{-# LANGUAGE Rank2Types        #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeFamilies      #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

{- |
Module      :  Types.hs
Description :  Central data type and Yesod typeclass instances.
Copyright   :  (c) 2011 Cedric Staub
License     :  GPL-3

Maintainer  :  Simon Meier <iridcode@gmail.com>
Stability   :  experimental
Portability :  non-portable
-}


module Web.Types
  ( WebUI(..)
  , Route (..)
  , resourcesWebUI
  , TheoryInfo(..)
  , TheoryPath(..)
  , TheoryOrigin(..)
  , JsonResponse(..)
  , TheoryIdx
  , TheoryMap
  , ThreadMap
  -- , GenericHandler
  , Handler
  -- , URL rendering function
  , RenderUrl
  -- , GenericWidget
  , Widget
  -- Image rendering
  , ImageFormat(..)
  , imageFormatMIME
  )
where


import           Control.Applicative
import           Control.Concurrent
import           Data.Label
import qualified Data.Map            as M
import           Data.Maybe          (listToMaybe)
import           Data.Monoid         (mconcat)
import           Data.Ord            (comparing)
import qualified Data.Text           as T
import           Data.Time.LocalTime

import           Text.Hamlet
import           Yesod.Core
import           Yesod.Static

import           Theory

------------------------------------------------------------------------------
-- Types
------------------------------------------------------------------------------

-- | Type synonym for a generic handler inside our site.
-- type GenericHandler m = Handler WebUI WebUI m
-- type Handler a = Handler WebUI WebUI a

-- | Type synonym for a generic widget inside our site.
-- type GenericWidget m = Widget WebUI (GenericHandler m)
-- type Widget a = Widget WebUI WebUI a

-- | Type synonym representing a numeric index for a theory.
type TheoryIdx = Int

-- | Type synonym representing a map of theories.
type TheoryMap = M.Map TheoryIdx TheoryInfo

-- | Type synonym representing a map of threads.
type ThreadMap = M.Map T.Text ThreadId

-- | The image format used for rendering graphs.
data ImageFormat = PNG | SVG

instance Show ImageFormat where
    show PNG = "png"
    show SVG = "svg"

-- | convert image format to MIME type.
imageFormatMIME :: ImageFormat -> String
imageFormatMIME PNG = "image/png"
imageFormatMIME SVG = "image/svg+xml"

-- | The so-called site argument for our application, which can hold various
-- information that can use to keep info that needs to be available to the
-- handler functions.
data WebUI = WebUI
  { getStatic          :: Static
    -- ^ Settings for static file serving.
  , cacheDir           :: FilePath
    -- ^ The caching directory (for storing rendered graphs).
  , workDir            :: FilePath
    -- ^ The working directory (for storing/loading theories).
  -- , parseThy    :: MonadIO m => String -> GenericHandler m ClosedTheory
  , parseThy           :: String -> IO (Either String ClosedTheory)
    -- ^ Close an open theory according to command-line arguments.
  , theoryVar          :: MVar TheoryMap
    -- ^ MVar that holds the theory map
  , threadVar          :: MVar ThreadMap
    -- ^ MVar that holds the thread map
  , autosaveProofstate :: Bool
    -- ^ Automatically store theory map
  , dotCmd             :: FilePath
    -- ^ The dot command
  , imageFormat        :: ImageFormat
    -- ^ The image-format used for rendering graphs
  , defaultAutoProver  :: AutoProver
    -- ^ The default prover to use for automatic proving.
  , debug              :: Bool
    -- ^ Output debug messages
  }

-- | Simple data type for generating JSON responses.
data JsonResponse
  = JsonHtml T.Text Content   -- ^ Title and HTML content
  | JsonAlert T.Text          -- ^ Alert/dialog box with message
  | JsonRedirect T.Text       -- ^ Redirect to given URL

-- | Data type representing origin of theory.
-- Command line with file path, upload with filename (not path),
-- or created by interactive mode (e.g. through editing).
data TheoryOrigin = Local FilePath | Upload String | Interactive
     deriving (Show, Eq, Ord)

-- | Data type containg both the theory and it's index, making it easier to
-- pass the two around (since they are always tied to each other). We also
-- keep some extra bookkeeping information.
data TheoryInfo = TheoryInfo
  { tiIndex      :: TheoryIdx       -- ^ Index of theory.
  , tiTheory     :: ClosedTheory    -- ^ The closed theory.
  , tiTime       :: ZonedTime       -- ^ Time theory was loaded.
  , tiParent     :: Maybe TheoryIdx -- ^ Prev theory in history
  , tiPrimary    :: Bool            -- ^ This is the orginally loaded theory.
  , tiOrigin     :: TheoryOrigin    -- ^ Origin of theory.
  , tiAutoProver :: AutoProver      -- ^ The automatic prover to use.
  }

-- | We use the ordering in order to display loaded theories to the user.
-- We first compare by name, then by time loaded, and then by source: Theories
-- that were loaded from the command-line are displayed earlier then
-- interactively loaded ones.
compareTI :: TheoryInfo -> TheoryInfo -> Ordering
compareTI (TheoryInfo _ i1 t1 p1 a1 o1 _) (TheoryInfo _ i2 t2 p2 a2 o2 _) =
  mconcat
    [ comparing (get thyName) i1 i2
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]

instance Eq TheoryInfo where
  (==) t1 t2 = compareTI t1 t2 == EQ

instance Ord TheoryInfo where
  compare = compareTI

-- | Simple data type for specifying a path to a specific
-- item within a theory.
data TheoryPath
  = TheoryHelp                          -- ^ The help view (help and info about theory)
  | TheoryLemma String                  -- ^ Theory lemma with given name
  | TheoryCaseDist CaseDistKind Int Int -- ^ Required cases (i'th source, j'th case)
  | TheoryProof String ProofPath        -- ^ Proof path within proof for given lemma
  | TheoryMethod String ProofPath Int   -- ^ Apply the proof method to proof path
  | TheoryRules                         -- ^ Theory rules
  | TheoryMessage                       -- ^ Theory message deduction
  deriving (Eq, Show, Read)

-- | Render a theory path to a list of strings. Note that we prefix an
-- underscore to the empty string and strings starting with an underscore.
-- This avoids empty path segments, which seem to trip up certain versions of
-- Yesod.
renderTheoryPath :: TheoryPath -> [String]
renderTheoryPath =
    map prefixWithUnderscore . go
  where
    go TheoryHelp = ["help"]
    go TheoryRules = ["rules"]
    go TheoryMessage = ["message"]
    go (TheoryLemma name) = ["lemma", name]
    go (TheoryCaseDist k i j) = ["cases", show k, show i, show j]
    go (TheoryProof lemma path) = "proof" : lemma : path
    go (TheoryMethod lemma path idx) = "method" : lemma : show idx : path

-- | Prefix an underscore to the empty string and strings starting with an
-- underscore.
prefixWithUnderscore :: String -> String
prefixWithUnderscore ""         = "_"
prefixWithUnderscore cs@('_':_) = '_' : cs
prefixWithUnderscore cs         = cs

-- | Remove an underscore prefix. It holds that
--
-- > unprefixUnderscore . prefixWithUnderscore = id
--
-- The inverted composition holds for all strings except the empty string and
-- strings starting with an underscore.
unprefixUnderscore :: String -> String
unprefixUnderscore "_"              = ""
unprefixUnderscore ('_':cs@('_':_)) = cs
unprefixUnderscore cs               = cs

-- | Parse a list of strings into a theory path.
parseTheoryPath :: [String] -> Maybe TheoryPath
parseTheoryPath =
    parse . map unprefixUnderscore
  where
    parse []     = Nothing
    parse (x:xs) = case x of
      "help"    -> Just TheoryHelp
      "rules"   -> Just TheoryRules
      "message" -> Just TheoryMessage
      "lemma"   -> parseLemma xs
      "cases"   -> parseCases xs
      "proof"   -> parseProof xs
      "method"  -> parseMethod xs
      _         -> Nothing

    safeRead = listToMaybe . map fst . reads

    parseLemma ys = TheoryLemma <$> listToMaybe ys

    parseProof (y:ys) = Just (TheoryProof y ys)
    parseProof _      = Nothing

    parseMethod (y:z:zs) = safeRead z >>= Just . TheoryMethod y zs
    parseMethod _        = Nothing

    parseCases (kind:y:z:_) = do
      k <- case kind of "typed"   -> return TypedCaseDist
                        "untyped" -> return UntypedCaseDist
                        _         -> Nothing
      m <- safeRead y
      n <- safeRead z
      return (TheoryCaseDist k m n)
    parseCases _       = Nothing


type RenderUrl = Route WebUI -> T.Text

------------------------------------------------------------------------------
-- Routing
------------------------------------------------------------------------------

-- This is a hack we need to work around a bug (?) in the
-- C pre-processor. In order to define multi-pieces we need
-- the asterisk symbol, but the C pre-processor always chokes
-- on them thinking that they are somehow comments. This can
-- be removed once the CPP language ext is disabled, but it's
-- currently needed for GHC < 7 support.
#define MP(x) *x

-- | Static routing for our application.
-- Note that handlers ending in R are general handlers,
-- whereas handlers ending in MR are for the main view
-- and the ones ending in DR are for the debug view.
mkYesodData "WebUI" [parseRoutes|
/                                          RootR                   GET POST
/thy/#Int/overview/MP(TheoryPath)          OverviewR               GET
/thy/#Int/source                           TheorySourceR           GET
/thy/#Int/message                          TheoryMessageDeductionR GET
/thy/#Int/main/MP(TheoryPath)              TheoryPathMR            GET
-- /thy/#Int/debug/MP(TheoryPath)             TheoryPathDR            GET
/thy/#Int/graph/MP(TheoryPath)             TheoryGraphR            GET
/thy/#Int/autoprove/#SolutionExtractor/#Int/MP(TheoryPath) AutoProverR             GET
/thy/#Int/next/#String/MP(TheoryPath)      NextTheoryPathR         GET
/thy/#Int/prev/#String/MP(TheoryPath)      PrevTheoryPathR         GET
-- /thy/#Int/save                             SaveTheoryR             GET
/thy/#Int/download/#String                 DownloadTheoryR         GET
-- /thy/#Int/edit/source                      EditTheoryR             GET POST
-- /thy/#Int/edit/path/MP(TheoryPath)         EditPathR               GET POST
/thy/#Int/del/path/MP(TheoryPath)          DeleteStepR             GET
/thy/#Int/unload                           UnloadTheoryR           GET
/kill                                      KillThreadR             GET
-- /threads                                   ThreadsR                GET
/robots.txt                                RobotsR                 GET
/favicon.ico                               FaviconR                GET
/static                                    StaticR                 Static getStatic
|]

instance PathPiece SolutionExtractor where
  toPathPiece CutNothing = "characterize"
  toPathPiece CutDFS     = "idfs"
  toPathPiece CutBFS     = "bfs"

  fromPathPiece "characterize" = Just CutNothing
  fromPathPiece "idfs"         = Just CutDFS
  fromPathPiece "bfs"          = Just CutBFS
  fromPathPiece _              = Nothing

-- | MultiPiece instance for TheoryPath.
instance PathMultiPiece TheoryPath where
  toPathMultiPiece   = map T.pack . renderTheoryPath
  fromPathMultiPiece = parseTheoryPath . map T.unpack

-- Instance of the Yesod typeclass.
instance Yesod WebUI where
  -- | The approot. We can leave this empty because the
  -- application is always served from the root of the server.
  approot = ApprootStatic T.empty

  -- | The default layout for rendering.
  defaultLayout = defaultLayout'

  -- | The path cleaning function. We make sure empty strings
  -- are not scrubbed from the end of the list. The default
  -- cleanPath function forces canonical URLs.
  cleanPath _ = Right

------------------------------------------------------------------------------
-- Default layout
------------------------------------------------------------------------------

-- | Our application's default layout template.
-- Note: We define the default layout here even tough it doesn't really
-- belong in the "types" module in order to avoid mutually recursive modules.
-- defaultLayout' :: (Yesod master, Route master ~ WebUIRoute)
--                => Widget master ()      -- ^ Widget to embed in layout
--                -> Handler master Html
defaultLayout' :: Widget -> Handler Html
defaultLayout' w = do
  page <- widgetToPageContent w
  message <- getMessage
  giveUrlRenderer [hamlet|
    $newline never
    !!!
    <html>
      <head>
        <title>#{pageTitle page}
        <link rel=stylesheet href=/static/css/tamarin-prover-ui.css>
        <link rel=stylesheet href=/static/css/jquery-contextmenu.css>
        <link rel=stylesheet href=/static/css/smoothness/jquery-ui.css>
        <script src=/static/js/jquery.js></script>
        <script src=/static/js/jquery-ui.js></script>
        <script src=/static/js/jquery-layout.js></script>
        <script src=/static/js/jquery-cookie.js></script>
        <script src=/static/js/jquery-superfish.js></script>
        <script src=/static/js/jquery-contextmenu.js></script>
        <script src=/static/js/tamarin-prover-ui.js></script>
        ^{pageHead page}
      <body>
        $maybe msg <- message
          <p.message>#{msg}
        <p.loading>
          Loading, please wait...
          \  <a id=cancel href='#'>Cancel</a>
        ^{pageBody page}
        <div#dialog>
        <ul#contextMenu>
          <li.autoprove>
            <a href="#autoprove">Autoprove</a>
  |]
          -- <li.delstep>
            -- <a href="#del/path">Remove step</a>