hets_cgi.hs

{- |
Module       : ./GUI/hets_cgi.hs
Copyright    : (c) Uni Magdeburg 2004-2017
License      : GPLv2 or higher, see LICENSE.txt

Maintainer   : till@iks.cs.ovgu.de
Stability    : provisional
Portability  : non-portable(imports Logic.Logic)

Interface for web page with WASH/CGI
-}

module Main where

import WASH.CGI.CGI as CGI

import Driver.Options
import Driver.WriteLibDefn
import Driver.ReadLibDefn
import Driver.Version

import qualified Data.Set as Set

import qualified Common.Result as CRes
import Common.Doc (renderText)
import Common.GlobalAnnotations
import Common.LibName
import Common.ResultT
import Common.PrintLaTeX

import Comorphisms.LogicGraph

import Static.AnalysisLibrary
import Static.DevGraph

import Syntax.AS_Library
import Syntax.Print_AS_Structured
import Syntax.ToXml

import Text.XML.Light

import System.Random
import System.IO
import System.Time
import System.Process
import System.Posix.IO
import System.Posix.Types
import System.Posix.Files
import System.Posix.Process

import Control.Monad

-- ---- Configuration section -------------------------

-- - site specific configuration

-- a valid email address for the contact field / link
contactUrl :: String
contactUrl = "mailto:" ++ contactText

-- the text displayed with the previous link
contactText :: String
contactText = "hets-devel@informatik.uni-bremen.de"

{- a directory which must be accessable and exposed by the web server,
where all the generated files are stored. This string must end with
a slash! -}
baseDirGenerated :: String
baseDirGenerated = "/home/www.informatik.uni-bremen.de/cofi/hets-tmp/"

-- path to the log file
logFile :: String
logFile = baseDirGenerated ++ "hets.log"

-- the url pointing to the above specified directory
baseUrlGenerated :: String
baseUrlGenerated = "http://www.informatik.uni-bremen.de/cofi/hets-tmp/"

{- the directory where the Hets-lib repository is checked out. Must be
accessable by the cgi script -}
caslLibDir :: String
caslLibDir = "/home/cofi/Hets-lib"

-- where is the pdflatex command for the generation of PDF-files
pdflatexCmd :: String
pdflatexCmd = "/opt/csw/bin/pdflatex"

-- - site independant configuration

cofiUrl :: String
cofiUrl =
  "http://www.cofi.info/"

-- link to the homepage of hetcasl
hetcaslUrl :: String
hetcaslUrl = "http://dol-omg.org/"

hetsUrl :: String
hetsUrl = "http://hets.eu/"

-- link to the manual of Hets
hetsManualUrl :: String
hetsManualUrl = hetsUrl ++ "UserGuide.pdf"

-- link to the hetcasl.sty file
hetcaslStyUrl :: String
hetcaslStyUrl = hetsUrl ++ "hetcasl.sty"

-- ---- End of Configuration section ------------------

webOpts :: HetcatsOpts
webOpts = defaultHetcatsOpts
  { outputToStdout = False
  , libdirs = [caslLibDir]
  , verbose = 0 }

data SelectedBoxes = SB
  { outputTree :: Bool
  , outputTxt :: Bool
  , outputTex :: Bool
  , archive :: Bool
  } deriving Show

data Output = OP
  { asciiTxt :: String
  , parseTree :: String }

defaultOutput :: Output
defaultOutput = OP "" ""

newtype RESL = RESL (CRes.Result Output)

instance Read RESL where
    readsPrec _ _ = error "Read for \"RESL\" not implemented!!"

instance Show RESL where
    showsPrec _ _ _ = error "Show for \"RESL\" not implemented!!"

main :: IO ()
main = run mainCGI

mainCGI :: CGI ()
mainCGI = ask $ html $ do
      CGI.head $ title $ text "Hets Web Interface"
      CGI.body $ makeForm $ page1 hetsVersion

page1 :: String -> WithHTML x CGI ()
page1 title1 = do
      h1 $ text title1
      p $ do
        text "You may also want to try out our experimental "
        hlink (URL "http://rest.hets.eu/")
          $ text "Hets Server"
      p $ do
        text "Enter a "
        hlink (URL hetcaslUrl) $ text "CASL or DOL"
        text
          " specification or library in the input zone, then press SUBMIT:"
      -- Input field
      input <- p $ makeTextarea "" (attr "rows" "22" ## attr "cols" "68")
      -- check box
      selectTxt <- checkboxInputField (attr "valus" "yes")
      text "output pretty print ASCII"
      selectTex <- checkboxInputField (attr "valus" "yes")
      text "output pretty print LaTeX"
      selectTree <- checkboxInputField (attr "valus" "yes")
      text "output xml tree"
      selectAchiv <- p $ b $ checkboxInputField (attr "checked" "checked") ##
        text "If this checkbox is selected, your input will be logged!"
      -- submit/reset botton
      p $ do
        submit (F5 input selectTree selectTxt selectTex selectAchiv)
                 handle (fieldVALUE "Submit")
        submit0 mainCGI (fieldVALUE "reset")
      hr_S CGI.empty
      p $ do
        text "Contact address: "
        hlink (URL contactUrl) $ text contactText

-- handle of the submit botton
handle :: HasValue i => F5 (i String) (i Bool) (i Bool) (i Bool) (i Bool) VALID
       -> CGI ()
handle (F5 input box1 box2 box3 box4) = do
    random1 <- io $ getStdRandom $ randomR (100000, 999999)
    processID <- io getProcessID
    let outputfile = baseDirGenerated ++ "result" ++ show processID
                     ++ show (random1 :: Int)
        str = CGI.value input
        selectedBoxes = SB
          { outputTree = CGI.value box1
          , outputTxt = CGI.value box2
          , outputTex = CGI.value box3
          , archive = CGI.value box4 }
    RESL res <- io $ fmap RESL $ anaInput str selectedBoxes outputfile
    ask $ html $ do
          CGI.head $ title $ text "HETS results"
          CGI.body $ printR str res selectedBoxes outputfile

-- Analyze the input
anaInput :: String -> SelectedBoxes -> FilePath
         -> IO (CRes.Result Output)
anaInput contents selectedBoxes outputfiles = do
  CRes.Result _ (Just (ast : _)) <- runResultT
    $ readLibDefn logicGraph webOpts Nothing "<stdin>" "<stdin>" contents
  CRes.Result ds mres <- runResultT
      $ anaLibDefn logicGraph webOpts Set.empty emptyLibEnv emptyDG ast ""
  let ds1 = filter diagFilter ds
  if CRes.hasErrors ds1 then return $ CRes.Result ds1 Nothing else
    maybe (return $ CRes.Result ds1 Nothing)
           (\ res -> do
              saveLog (archive selectedBoxes)
              process_result ds1 res outputfiles selectedBoxes)
           mres
 where
      diagFilter d = case CRes.diagKind d of
                     CRes.Hint -> False
                     CRes.Debug -> False
                     _ -> True

      process_result :: [CRes.Diagnosis]
                      -> (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
                      -> FilePath
                      -> SelectedBoxes
                      -> IO (CRes.Result Output)
      process_result ds (_, libDefn, gannos, _) outputfile conf = do
             let fMode = foldl unionFileModes nullFileMode
                                [ownerReadMode, ownerWriteMode,
                                 groupReadMode, groupWriteMode,
                                 otherReadMode]
             when (outputTex conf) $ do
                    let pptexFile = outputfile ++ ".pp.tex"
                        latexFile = outputfile ++ ".tex"
                        pdfFile = outputfile ++ ".pdf"
                        tmpFile = outputfile ++ ".tmp"
                    writeLibDefnLatex logicGraph False gannos pptexFile libDefn
                    writeFile latexFile (latexHeader ++
                                         "\\input{" ++ pptexFile ++
                                         "}\n \\end{document}\n")
                    setFileMode pptexFile fMode
                    setFileMode latexFile fMode

                    system ("(cd " ++ baseDirGenerated ++ " ; ls -lh " ++
                            pdflatexCmd ++ " ; " ++ pdflatexCmd ++ " " ++
                           latexFile ++ ") > " ++ tmpFile)
                    setFileMode pdfFile fMode
             when (outputTxt conf) $ do
                    let txtFile = outputfile ++ ".txt"
                    writeFile txtFile $ show (renderText gannos $
                      prettyLG logicGraph libDefn) ++ "\n"
                    setFileMode txtFile fMode
             when (outputTree conf) $ do
                    let txtFile = outputfile ++ ".pp.xml"
                    writeFile txtFile . ppTopElement
                      $ xmlLibDefn logicGraph gannos libDefn
                    setFileMode txtFile fMode
             return (CRes.Result ds $ Just $ selectOut conf libDefn gannos)
      selectOut :: SelectedBoxes -> LIB_DEFN -> GlobalAnnos -> Output
      selectOut conf ld ga = defaultOutput
        { asciiTxt = if outputTxt conf
            then show $ renderText ga $ prettyLG logicGraph ld else ""
        , parseTree = if outputTree conf
            then ppElement $ xmlLibDefn logicGraph ga ld else "" }
      -- log file
      saveLog :: Bool -> IO ()
      saveLog willSave = when willSave $ do
            fd <- openFd logFile ReadWrite Nothing
                               defaultFileFlags {append = True}
            fSize <- sizeof fd
            let filelock = (WriteLock, AbsoluteSeek, 0, fSize)
                fileunlock = (Unlock, AbsoluteSeek, 0, fSize)
            aktTime <- timeStamp
            setLock fd filelock
            fdWrite fd (aktTime ++ "\n" ++ contents ++ "\n\n")
            setLock fd fileunlock
            closeFd fd
      timeStamp :: IO String
      timeStamp = do
            t <- getClockTime
            ct <- toCalendarTime t
            return $ calendarTimeToString ct
      sizeof :: Fd -> IO FileOffset
      sizeof fd = do
            fstatus <- getFdStatus fd
            return $ fileSize fstatus

-- Print the result
printR :: String -> CRes.Result Output -> SelectedBoxes
       -> FilePath
       -> WithHTML x CGI ()
printR str (CRes.Result ds mres) conf outputFile =
  do h3 $ text "You have submitted the CASL or DOL library:"
     mapM_ (\ l -> text l >> br CGI.empty) $ lines str
     h3 $ text "Diagnostic messages of parsing and static analysis:"
     mapM_ (\ l -> text (show l) >> br CGI.empty) ds
     maybe CGI.empty printRes mres
     hr_S CGI.empty
     p $ do
       text "Not the result you expected? Please check the "
       hlink (read hetsManualUrl) $ text "Hets Manual"
       text "."
     hr_S CGI.empty
     p $ do
       text "Contact address: "
       hlink (read contactUrl) $ text contactText
    where
       adjustOutfile ext = baseUrlGenerated ++
         drop (length baseDirGenerated) (outputFile ++ ext)
       printRes res = do
            when (outputTxt conf) $ do
               heading3 "Pretty printed text:"
               formatTxt (asciiTxt res)
               p $ i $ do
                 text "You can download the "
                 hlink (read $ adjustOutfile ".txt") $ text "text file"
                 text " here. The file will be deleted after 30 minutes.\n"
            when (outputTex conf) $ do
               heading3 "LaTeX code:"
               p $ i $ do
                 text "You can download the "
                 hlink (read $ adjustOutfile ".pp.tex") $ text "LaTeX file"
                 text " here. For compiling the LaTeX output, you need "
                 hlink (read hetcaslStyUrl) $ text "hetcasl.sty"
                 text "."
               p $ i $ do
                 text "You can also download the "
                 hlink (read $ adjustOutfile ".pdf") $ text "PDF file"
                 text ". All files will be deleted after 30 minutes.\n"
            when (outputTree conf) $ do
               heading3 "XML parse tree:"
               formatTxt (parseTree res)
               p $ i $ do
                 text "You can download the "
                 hlink (read $ adjustOutfile ".pp.xml") $ text "XML file"
                 text " here. The file will be deleted after 30 minutes.\n"
       formatTxt = p . mapM_ (\ l -> text l >> br CGI.empty) . lines
       heading3 = h3 . text