hets_cgi.hs revision 43b4c41fbb07705c9df321221ab9cb9832460407
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-|
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederCopyright : (c) Heng Jiang, Uni Bremen 2004
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : hets@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Interface for web page with WASH/CGI
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder todo:
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder - default for checkbox regarding logging of input must be "selected"
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder .. done
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder - temporary files should be created with these permissions:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder -rw-rw-r-- (than every member of grp agcofi can remove
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder temporary files)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder .. done
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder - LaTeX code should only be available as download .. done
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder - ASCII code should also be available as download .. done
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich - additionally to (show random) the temporary file names
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder should contain a fraction of the seconds since epoch and/or
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder the ProcessID
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder .. done
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder - english sentences in the output need corrections
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder .. done
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich - when the HTML-PrettyPrinting is available: generated HTML-Code
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder instead of poorly rendered ASCII has to be inserted as response
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder .. ???
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder - a handler for warning message
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder-}
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maedermodule Main where
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederimport CGI
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport Driver.Options
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Driver.WriteFn
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederimport Driver.ReadFn
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Common.Lib.Map as Map
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Common.Result
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maederimport Common.AS_Annotation
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport Static.AnalysisLibrary
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport Comorphisms.LogicGraph
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport Static.DevGraph
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport Syntax.AS_Library
05a62e84edac8c64de04f8349dee418598d216b9Christian Maederimport Syntax.Parse_AS_Structured
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederimport Maybe
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport Random
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport IO
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Time
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport System.Cmd
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport System.Posix.IO
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport System.Posix.Types
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport System.Posix.Files
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederimport System.Posix.Process
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederimport System.Posix.Env
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maederimport Driver.Version
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maedertype DiagStr = String
8cacad2a09782249243b80985f28e9387019fe40Christian Maedertype HtmlTitle = String
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maedertype ResAna = String
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maedertype SelectedBox = (Bool, Bool, Bool, Bool)
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maedermain :: IO()
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichmain =
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder run mainCGI
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder
feca1d35123d8c31aee238c9ce79947b0bf65494Christian MaedermainCGI :: CGI()
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedermainCGI =
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder do
c8012b9719c73f08418af7a0b4ba28fa1d200631Christian Maeder ask $ html (do CGI.head (title $ text "Hets Web Interface")
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder CGI.body $ makeForm $ page1 ("Hets " ++ hetcats_version))
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederpage1 :: String -> WithHTML x CGI ()
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederpage1 title1 =
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder h1 $ text title1
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder p (do text "Enter a "
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder hlink (read "http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/index_e.htm") $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (text "HetCASL")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder text " specification or library in the input zone, then press SUBMIT:")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Input field
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder input <- p (makeTextarea "" (attr "rows" "22" ## attr "cols" "68"))
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -- check box
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder selectEnv <- checkboxInputField (attr "valus" "yes")
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder text "output pretty print ASCII"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder selectTex <- checkboxInputField (attr "valus" "yes")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder text "output pretty print LaTeX"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder selectTree <- checkboxInputField (attr "valus" "yes")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder text "output parse tree"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder selectAchiv <- p $ b ( checkboxInputField(attr "checked" "checked") ##
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder text "If this checkbox is selected, your input will be logged!")
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder -- submit/reset botton
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder p (submit (F5 input selectTree selectEnv selectTex selectAchiv)
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder handle (fieldVALUE "Submit") >>
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder submit0 reset (fieldVALUE "reset"))
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder hr_S $ CGI.empty
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder p $ (do text "Contact address: "
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder hlink (read "mailto:cofi@informatik.uni-bremen.de") $
b363eb04791e7f735633b9b4088502c2bc50ebfcChristian Maeder text "cofi@informatik.uni-bremen.de")
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederreset :: CGI()
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maederreset = mainCGI
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- handle of the submit botton
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maederhandle (F5 input box1 box2 box3 box4) =
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder let str = value input
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder tree = value box1
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder env = value box2
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder tex = value box3
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder achiv= value box4
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder in do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder random1 <- io $ getRandom
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder processID <- io $ getProcessID
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let outputfile = "/home/www/cofi/hets-tmp/result" ++ (show processID) ++
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (show random1)
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder res <- io $ anaInput str (tree, env, tex, achiv) outputfile
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder ask $ html ( do CGI.head (title $ text "HETS results")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder CGI.body $ printR str res (tree, env, tex, achiv) outputfile)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder getRandom :: IO Int
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder getRandom = getStdRandom (randomR (100000,999999))
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- Analyze the input
4017ebc0f692820736d796af3110c3b3018c108aChristian MaederanaInput :: String -> SelectedBox -> FilePath -> IO([DiagStr],[(HtmlTitle, ResAna)])
b568982efd0997d877286faa592d81b03c8c67b8Christian MaederanaInput contents showS@(_,_,_,willAchiv) outputfiles =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder do
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich setEnv "HETS_LIB" "/home/cofi/CASL-lib" True
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (parseErrors, ast) <- read_LIB_DEFN_M_WI defaultLogic "<stdin>" contents
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if parseErrors == "" then
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Common.Result.Result ds res <- ioresToIO
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder (ana_LIB_DEFN logicGraph defaultLogic
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder defaultHetcatsOpts{outputToStdout = False} emptyLibEnv ast)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder let diagStrs1 = Prelude.map show ds
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder diagStrs2 = reverse $ filterDiagStr [] diagStrs1
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder -- putStrLn $ show $ length $ lines $ Prelude.head diagStrs1
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder case res of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (_, libdefn1, _, _) ->
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let Lib_defn _ alibItems _ _ = libdefn1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder items = reverse $ Prelude.map item alibItems
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- diagStrs' <- addSpnToDiags items diagStrs
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder if hasErrors ds then
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return (diagStrs2, [])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder saveLog willAchiv contents
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder anaInput_aux diagStrs2 res outputfiles showS
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return(diagStrs2,[])
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder else return (parseErrors:[], [])
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder where
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder filterDiagStr :: [String] -> [DiagStr] -> [DiagStr]
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder filterDiagStr str [] = str
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder filterDiagStr str d@(hdiags:rdiags)
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder | (length $ lines hdiags) < 2 =
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder if "*** Hint" == take 8 hdiags then filterDiagStr str rdiags
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder else if "*** FatalError" == take 14 hdiags then hdiags:str
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder else if "*** MessageW ," == take 14 hdiags then
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder filterDiagStr ((drop 14 hdiags):str) rdiags
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder else filterDiagStr (hdiags:str) rdiags
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder | otherwise = filterDiagStr (filterDiagStr' str $ lines hdiags) rdiags
8d178ae08a52d61379e6b8074f61646499bc88bbChristian Maeder
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder filterDiagStr' :: [String] -> [DiagStr] -> [DiagStr]
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder filterDiagStr' str' [] = str'
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder filterDiagStr' str' (hd:rd)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder | "*** Hint" == take 8 hd = filterDiagStr' str' rd
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder | "*** MessageW ," == take 14 hd = filterDiagStr' ((drop 14 hd):str') rd
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder | otherwise = filterDiagStr' (hd:str') rd
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder
59138b404f12352d103eeffbeaeb3957b90e75fdChristian Maeder anaInput_aux :: [DiagStr]
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -> Maybe(LIB_NAME, LIB_DEFN, DGraph, LibEnv)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -> FilePath
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -> SelectedBox
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> IO([DiagStr],[(HtmlTitle, ResAna)])
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder anaInput_aux diags1 res outputfiles1 (showTree, showEnv, showTex, _) =
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder case res of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just (libName, libDefn, _, libEnv) ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder let (globalAnnos, _, _) = fromJust $ Map.lookup libName libEnv
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder fileMode = foldl unionFileModes nullFileMode
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [ownerReadMode, ownerWriteMode, groupReadMode, groupWriteMode, otherReadMode]
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder resAsc <- write_casl_asc_stdout defaultHetcatsOpts globalAnnos libDefn
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder resTex <- write_casl_latex_stdout defaultHetcatsOpts globalAnnos libDefn
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder if showTex then
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder do
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder let pptexFile = outputfiles1 ++ ".pp.tex"
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder latexFile = outputfiles1 ++ ".tex"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder pdfFile = outputfiles1 ++ ".pdf"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder tmpFile = outputfiles1 ++ ".tmp"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder write_casl_latex defaultHetcatsOpts globalAnnos (pptexFile) libDefn
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder rawSystem "cp" ["/home/www/cofi/hets-tmp/mould.m", latexFile]
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder setFileMode pptexFile fileMode
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder setFileMode latexFile fileMode
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder appendFile latexFile ("\\input{"++ pptexFile ++"}\n" ++ "\\end{document}\n")
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang system ("cd /home/www/cofi/hets-tmp; /usr/local/share/teTeX/2.0/bin/ix86-linux2/pdflatex " ++
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett latexFile ++ " > " ++ tmpFile)
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder -- system "mv result* /home/www/cofi/hets-tmp/"
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder setFileMode pdfFile fileMode
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder return()
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers else return()
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder if showEnv then
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let txtFile = outputfiles1 ++ ".txt"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder write_casl_asc defaultHetcatsOpts globalAnnos txtFile libDefn
d6697ad2479099b816203fd2c36f593c72c73c76Christian Maeder setFileMode txtFile fileMode
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder else return()
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder return $ (diags1, selectOut [showEnv, showTex, showTree] libDefn resAsc resTex)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder Nothing -> return ([],[])
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder selectOut :: [Bool] -> LIB_DEFN -> String -> String -> [(HtmlTitle, ResAna)]
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder selectOut [] _ _ _ = []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder selectOut (hb:rb) libDefn ra rt
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | length rb == 2 && hb =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ("ASCII code:", ra):(selectOut rb libDefn ra rt)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder | length rb == 1 && hb =
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder ("LaTeX code:", ""):(selectOut rb libDefn ra rt)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- ("LaTeX code:", rt):(selectOut rb libDefn ra rt)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder | length rb == 0 && hb =
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder ("Parse tree:", show libDefn):(selectOut rb libDefn ra rt)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder | otherwise = selectOut rb libDefn ra rt
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -- log file
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder saveLog :: Bool -> String -> IO()
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder saveLog willSave contents
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder | willSave =
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder do
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder let logFile = "/home/www/cofi/hets-tmp/hets.log"
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder fd <- openFd logFile ReadWrite Nothing defaultFileFlags{append = True}
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder fileSize <- sizeof fd
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder let filelock = (WriteLock, AbsoluteSeek, 0, fileSize)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder fileunlock = (Unlock, AbsoluteSeek, 0, fileSize)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder aktTime <- timeStamp
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder setLock fd filelock
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder fdWrite fd (aktTime ++ "\n" ++ contents ++ "\n\n")
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder setLock fd fileunlock
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder closeFd fd
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder | otherwise = return ()
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder where
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder timeStamp :: IO String
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder timeStamp = do t <- getClockTime
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder ct <- toCalendarTime t
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder return $ calendarTimeToString ct
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder sizeof :: Fd -> IO FileOffset
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder sizeof fd = do fstatus <- getFdStatus fd
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return $ fileSize fstatus
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- Print the result
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederprintR :: String -> ([DiagStr], [(HtmlTitle, ResAna)]) -> SelectedBox -> FilePath
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder -> WithHTML x CGI ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederprintR str (diags2, result) selectedBoxes outputFiles =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder h1 $ text "You have submitted the HetCASL library:"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder mapM_ (\l -> text l >> br CGI.empty) $ lines str
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder h1 $ text "Result of parsing and static checking:"
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder mapM_ (\l -> h3 $ text l >> br CGI.empty) $ diags2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder printRes selectedBoxes outputFiles result
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder hr_S $ CGI.empty
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder p (do text "Not the result you expected ? Please check the "
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder hlink (read "http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf") $ text "Hets Manual"
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder text "."
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder )
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder hr_S $ CGI.empty
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder p $ (do text "Contact address: "
df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder hlink (read "mailto:cofi@informatik.uni-bremen.de") $
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder text "cofi@informatik.uni-bremen.de"
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder )
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder where
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder printRes :: SelectedBox -> FilePath ->
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder [(DiagStr, ResAna)] -> WithHTML x CGI ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder printRes _ _ [] = CGI.empty
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly printRes (isTree, isEnv, isTex, willAchiv) outputfiles
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ((title_ana, text_ana):rR) =
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke do h3 $ text title_ana
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder p $ mapM_ (\l -> text l >> br CGI.empty) $ lines text_ana
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder if isEnv then
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder do
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu p $ i(do text "You can download the "
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroeder hlink (read ("http://www.informatik.uni-bremen.de/cofi/hets-tmp/" ++
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu (drop 24 (outputfiles++".txt")))) $ text "ACSII file"
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder text " here. The file will be deleted after 30 minutes.\n"
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder )
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder printRes (isTree, False, isTex, willAchiv) outputfiles rR
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder else if isTex then
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke do
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke p $ i(do text "You can download the "
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder hlink (read ("http://www.informatik.uni-bremen.de/cofi/hets-tmp/" ++
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder (drop 24 (outputfiles++".pp.tex")))) $ text "LaTeX file"
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder text " here. For compiling the LaTeX output, you need "
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder hlink (read "http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/hetcasl.sty") $ text "hetcasl.sty"
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski text "."
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder )
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder p $ i(do text "You can also download the "
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder hlink (read ("http://www.informatik.uni-bremen.de/cofi/hets-tmp/" ++
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder (drop 24 (outputfiles++".pdf")))) $ text "PDF file"
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder text ". All files will be deleted after 30 minutes.\n"
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder )
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder printRes (isTree, isEnv, False, willAchiv) outputfiles rR
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke else if isTree then
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich printRes (False, isEnv, isTex, willAchiv) outputfiles rR
247cc88aa55d0a7b6831767cd593ea885c6747a0Christian Maeder else printRes (isTree, isEnv, isTex, willAchiv) outputfiles rR
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder