Server.hs revision 1fac5c1cbbeac0c3b506437e7be4183809943af2
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule : $Header$
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerDescription : run hets as server
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerCopyright : (c) Christian Maeder, DFKI GmbH 2010
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : GPLv2 or higher, see LICENSE.txt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerMaintainer : Christian.Maeder@dfki.de
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerStability : provisional
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederPortability : non-portable (via imports)
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowskimodule PGIP.Server (hetsServer, sourceToBs) where
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.ByteString.Lazy.Char8 as BS
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.ByteString.Char8 as B8
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Map as Map
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyerimport qualified Data.IntMap as IntMap
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyerimport qualified Data.Set as Set
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederdata Session = Session
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder { sessLibEnv :: LibEnv
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder , sessLibName :: LibName
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , _previousKeys :: [Int]
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer , _sessStart :: UTCTime }
f456529a89bfb620d39e5fd5b0a53b24643db96dDominik LueckerandomKey :: IO Int
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerrandomKey = randomRIO (100000000, 999999999)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyersessGraph :: DGQuery -> Session -> Maybe (LibName, DGraph)
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian MaedersessGraph dgQ (Session le ln _ _) = case dgQ of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer DGQuery _ (Just path) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer find (\ (n, _) -> show (getLibId n) == path)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer _ -> fmap (\ dg -> (ln, dg)) $ Map.lookup ln le
415b2b968b52f687ba19f57aa85c9c5ee36f91e0Thiemo WiedemeyerhetsServer :: HetcatsOpts -> IO ()
1ac36418f204bbe56f4cd951a979180721758999Christian MaederhetsServer opts1 = do
2028dc2c091bb60343e15985948a59b955276cbfChristian Maeder tempDir <- getTemporaryDirectory
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let tempHetsLib = tempDir </> "MyHetsLib"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer permFile = tempDir </> "empty.txt"
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder opts = opts1 { libdirs = tempHetsLib : libdirs opts1 }
40b73e7d13a858afeac95321fcdb9ac216bfbf01Thiemo Wiedemeyer createDirectoryIfMissing False tempHetsLib
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer writeFile permFile ""
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sessRef <- newIORef IntMap.empty
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu run 8000 $ \ re -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let query = B8.unpack $ queryString re
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu path = dropWhile (== '/') $ B8.unpack (pathInfo re)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer rhost = shows (remoteHost re) "\n"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer time <- getCurrentTime
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer m <- readIORef sessRef
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer appendFile permFile $ shows time " sessions: " ++ shows (IntMap.size m) "\n"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer appendFile permFile rhost
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer appendFile permFile $ shows (requestHeaders re) "\n"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer -- better try to read hosts to exclude from a file
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer if isInfixOf "crawl" rhost then return $ mkResponse status403 "" else
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer case B8.unpack (requestMethod re) of
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer "GET" -> if query == "?menus" then mkMenuResponse else do
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder dirs@(_ : cs) <- getHetsLibContent opts path query
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer if null cs then getHetsResponse opts [] sessRef path query
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer else mkHtmlPage path dirs
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder (params, files) <- parseRequestBody tempFileSink re
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer mTmpFile <- case lookup "content"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder $ map (\ (a, b) -> (B8.unpack a, b)) params of
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer Nothing -> return Nothing
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just areatext -> let content = B8.unpack areatext in
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer if all isSpace content then return Nothing else do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder tmpFile <- getTempFile content "temp.het"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu copyPermissions permFile tmpFile
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu return $ Just tmpFile
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder let res tmpFile = getHetsResponse opts [] sessRef tmpFile query
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu mRes = maybe (return $ mkResponse status400 "nothing submitted")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [(_, f)] | query /= "?update" -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let fn = takeFileName $ B8.unpack $ fileName f
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo Wiedemeyer if any isAlphaNum fn then do
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer let tmpFile = tempHetsLib </> fn
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer snkFile = fileContent f
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu copyPermissions permFile snkFile
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder copyFile snkFile tmpFile
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder maybe (res tmpFile) res mTmpFile
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu _ -> getHetsResponse opts (map snd files) sessRef path query
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu _ -> return $ mkResponse status405 ""
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder-- for debugging purposes copied from Network.Wai.Parse
1ac36418f204bbe56f4cd951a979180721758999Christian MaedersourceToBs :: Source -> IO B8.ByteString
1ac36418f204bbe56f4cd951a979180721758999Christian MaedersourceToBs = fmap B8.concat . go id
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu go front (Source s) = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> return $ front []
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just (bs, src') -> go (front . (:) bs) src'
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkMenuResponse :: IO Response
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkMenuResponse = return $ mkOkResponse $ ppTopElement $ unode "menus" mkMenus
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo WiedemeyermkMenus :: [Element]
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo WiedemeyermkMenus = menuTriple "" "Get menu triples" "menus"
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder : menuTriple "/DGraph" "update" "update"
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer : map (\ (c, _) -> menuTriple "/" (menuTextGlobCmd c) $ cmdlGlobCmd c)
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder allGlobLibAct
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer ++ map (\ nc -> menuTriple "/DGraph/DGNode" ("Show " ++ nc) nc) nodeCommands
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ [menuTriple "/DGraph/DGLink" "Show edge info" "edge"]
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo WiedemeyermenuTriple :: String -> String -> String -> Element
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermenuTriple q d c = unode "triple"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [ unode "xquery" q
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , unode "displayname" d
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu , unode "command" c ]
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian MaedermkHtmlString :: FilePath -> [Element] -> String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkHtmlString path dirs = htmlHead ++ mkHtmlElem
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ("Listing of" ++ if null path then " repository" else ": " ++ path)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (headElems path ++ [unode "ul" dirs])
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkHtmlElem :: String -> [Element] -> String
79d103748927615310322af6f7806c7cef11a802Christian MaedermkHtmlElem title body = ppElement $ unode "html"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [ unode "head" $ unode "title" title
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu , unode "body" body ]
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo WiedemeyermkHtmlPage :: FilePath -> [Element] -> IO Response
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo WiedemeyermkHtmlPage path = return . mkOkResponse . mkHtmlString path
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkResponse :: Status -> String -> Response
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkResponse st = Response st [] . ResponseLBS . BS.pack
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkOkResponse :: String -> Response
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkOkResponse = mkResponse status200
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo WiedemeyeraddNewSess :: IORef (IntMap.IntMap Session) -> Session -> IO Int
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo WiedemeyeraddNewSess sessRef sess = do
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo Wiedemeyer k <- randomKey
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer atomicModifyIORef sessRef
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer (\ m -> (IntMap.insert k sess m, k))
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian MaedernextSess :: IORef (IntMap.IntMap Session) -> LibEnv -> Int -> IO Session
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanunextSess sessRef newLib k =
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder atomicModifyIORef sessRef
86b2d79be961f0247a2eed10ed4f86d8d6a7639dChristian Maeder (\ m -> case IntMap.lookup k m of
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer Nothing -> error "nextSess"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just s -> let newSess = s { sessLibEnv = newLib }
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in (IntMap.insert k newSess m, newSess))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerppDGraph :: DGraph -> Maybe PrettyType -> ResultT IO String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuppDGraph dg mt = let ga = globalAnnos dg in case optLibDefn dg of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> fail "parsed LIB-DEFN not avaible"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let latex = renderLatex Nothing (toLatex ga $ pretty ld) in case mt of
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu Just pty -> case pty of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu PrettyXml -> return $ ppTopElement $ xmlLibDefn ga ld
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu PrettyAscii -> return $ showGlobalDoc ga ld "\n"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer PrettyHtml -> return $ htmlHead ++ renderHtml ga (pretty ld)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer PrettyLatex -> return latex
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> lift $ do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder tmpDir <- getTemporaryDirectory
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (tmpFile, hdl) <- openTempFile tmpDir "temp.tex"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer copyPermissions (tmpDir </> "empty.txt") tmpFile
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder hSetEncoding hdl latin1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer hPutStr hdl $ latexHeader ++ latex ++ latexFooter
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer mapM_ (\ s -> do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let sty = (</> "hetcasl.sty")
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder ex <- doesFileExist f
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu when ex $ copyFile f $ sty tmpDir)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu , "/home/www.informatik.uni-bremen.de/cofi/hets-tmp" ]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu withinDirectory tmpDir $ do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (ex1, out1, err1) <- readProcessWithExitCode "pdflatex" [tmpFile] ""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (ex2, out2, err2) <- readProcessWithExitCode "pdflatex" [tmpFile] ""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let pdfFile = replaceExtension tmpFile "pdf"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu pdf <- doesFileExist pdfFile
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu if ex1 == ExitSuccess && ex2 == ExitSuccess && pdf then do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu pdfHdl <- openBinaryFile pdfFile ReadMode
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu str <- hGetContents pdfHdl
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer when (length str < 0) $ putStrLn "pdf file too large"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu hClose pdfHdl
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer else return $ "could not create pdf:\n"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ unlines [out1, err1, out2, err2]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetDGraph :: HetcatsOpts -> IORef (IntMap.IntMap Session) -> DGQuery
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> ResultT IO (Session, Int)
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo WiedemeyergetDGraph opts sessRef dgQ = case dgQ of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu NewDGQuery file -> do
1be357403a65d1954fd6b5f38e5cf8a630d8112fThiemo Wiedemeyer (ln, le) <- case guess file GuessIn of
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder mf <- lift $ findFileOfLibName opts file
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just f -> readDGXmlR opts f Map.empty
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> liftR $ fail "xml file not found"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu _ -> anaSourceFile logicGraph opts
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu { outputToStdout = False, useLibPos = True }
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Set.empty emptyLibEnv emptyDG file
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu time <- lift getCurrentTime
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let sess = Session le ln [] time
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu k <- lift $ addNewSess sessRef sess
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (sess, k)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer DGQuery k _ -> do
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer m <- lift $ readIORef sessRef
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer Nothing -> liftR $ fail "unknown development graph"
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Just sess -> return (sess, k)
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyergetSVG :: String -> String -> DGraph -> ResultT IO String
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyergetSVG title url dg = do
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (exCode, out, err) <- lift $ readProcessWithExitCode "dot" ["-Tsvg"]
86b2d79be961f0247a2eed10ed4f86d8d6a7639dChristian Maeder $ dotGraph title False url dg
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case exCode of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer ExitSuccess -> liftR $ extractSVG dg out
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerenrichSVG :: DGraph -> Element -> Element
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerenrichSVG dg e = processSVG dg $ fromElement e
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerprocessSVG :: DGraph -> Cursor -> Element
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerprocessSVG dg c = case nextDF c of
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer Nothing -> case toTree (root c) of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer _ -> error "processSVG"
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Just c2 -> processSVG dg
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ modifyContent (addSVGAttribs dg) c2
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanunodeAttrib :: DGNodeLab -> String
545d0cd78159cade346b579d06052638b19b0f72Thiemo WiedemeyernodeAttrib l = let nt = getRealDGNodeType l in
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (if isRefType nt then "Ref" else "")
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ (if hasSenKind (const True) l then
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (if isProvenNode nt then "P" else "Unp") ++ "roven"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ if isProvenCons nt then "Cons" else ""
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder else "LocallyEmpty")
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ++ (if isInternalSpec nt then "Internal" else "")
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ if labelHasHiding l then "HasIngoingHidingLink" else ""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuedgeAttrib :: DGLinkLab -> String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuedgeAttrib l = show (pretty $ dgl_type l) ++
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu if dglPending l then "IncompleteProofChain" else ""
5b00a9d748d5bea461601ed7ed5198dfd30cf2d2Thiemo WiedemeyeraddSVGAttribs :: DGraph -> Content -> Content
5b00a9d748d5bea461601ed7ed5198dfd30cf2d2Thiemo WiedemeyeraddSVGAttribs dg c = case c of
5b00a9d748d5bea461601ed7ed5198dfd30cf2d2Thiemo Wiedemeyer Elem e -> case getAttrVal "id" e of
5b00a9d748d5bea461601ed7ed5198dfd30cf2d2Thiemo Wiedemeyer Just istr | isNat istr -> let i = read istr in
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu case getAttrVal "class" e of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just "node" -> case lab (dgBody dg) i of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just l -> Elem $ add_attr (mkAttr "type" $ nodeAttrib l) e
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just "edge" -> case getDGLinksById (EdgeId i) dg of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [(_, _, l)] ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Elem $ add_attr (mkAttr "type" $ edgeAttrib l) e
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyerextractSVG :: DGraph -> String -> Result String
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyerextractSVG dg str = case parseXMLDoc str of
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Nothing -> fail "did not recognize svg element"
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just e -> return $ showTopElement $ enrichSVG dg e
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyercmpFilePath :: FilePath -> FilePath -> Ordering
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyercmpFilePath f1 f2 = case comparing hasTrailingPathSeparator f2 f1 of
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder EQ -> compare f1 f2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyergetHetsResponse :: HetcatsOpts -> [FileInfo FilePath]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> IORef (IntMap.IntMap Session) -> FilePath
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> String -> IO Response
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyergetHetsResponse opts updates sessRef path query = do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder Result ds ms <- getHetsResult opts updates sessRef path query
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return $ case ms of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> mkResponse status400 $ showRelDiags 1 ds
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just s -> mkOkResponse s
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo WiedemeyergetHetsResult :: HetcatsOpts -> [FileInfo FilePath]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> IORef (IntMap.IntMap Session) -> FilePath
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> String -> IO (Result String)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyergetHetsResult opts updates sessRef file query =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer runResultT $ case anaUri file $ dropWhile (== '?')
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer $ filter (not . isSpace) query of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Left err -> fail err
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Right (Query dgQ qk) -> do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer sk@(sess, k) <- getDGraph opts sessRef dgQ
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let libEnv = sessLibEnv sess
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder case sessGraph dgQ sess of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> fail $ "unknown library given by: " ++ file
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just (ln, dg) -> let title = show $ getLibId ln in
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer DisplayQuery ms -> case ms of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just "svg" -> getSVG title ('/' : file) dg
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just "xml" -> liftR $ return $ ppTopElement
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Just "dot" -> liftR $ return $ dotGraph title False title dg
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just "session" -> liftR $ return $ ppElement
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer $ aRef (mkPath sess ln k) (show k)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Just str | elem str ppList
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> ppDGraph dg $ lookup str $ zip ppList prettyList
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder _ -> liftR $ return $ sessAns ln sk
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer GlobCmdQuery s ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case find ((s ==) . cmdlGlobCmd . fst) allGlobLibAct of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Nothing -> if s == "update" then
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case filter ((== ".xupdate") . takeExtension . B8.unpack
545d0cd78159cade346b579d06052638b19b0f72Thiemo Wiedemeyer . fileName) updates of
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer str <- lift $ readFile $ fileContent ch
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu newDg <- liftR $ dgXUpdate str libEnv dg
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let newLib = Map.insert ln newDg libEnv
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder newSess <- lift $ nextSess sessRef newLib k
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu liftR $ return $ sessAns ln (newSess, k)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [] -> liftR $ return $ sessAns ln sk
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just (_, act) -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu newLib <- liftR $ act ln libEnv
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer newSess <- lift $ nextSess sessRef newLib k
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu liftR $ return $ sessAns ln (newSess, k)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu NodeQuery ein nc -> do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nl@(i, dgnode) <- case ein of
8681833aefdae18bfd52607b841373f024bbd99cChristian Maeder Right n -> case lookupNodeByName n dg of
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer p : _ -> return p
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer [] -> fail $ "no node name: " ++ n
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Left i -> case lab (dgBody dg) i of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> fail $ "no node id: " ++ show i
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Just dgnode -> return (i, dgnode)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let fstLine = (if isDGRef dgnode then ("reference " ++) else
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder if isInternalNode dgnode then ("internal " ++) else id)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu "node " ++ getDGNodeName dgnode ++ " " ++ show i ++ "\n"
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder showN d = showGlobalDoc (globalAnnos dg) d "\n"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu NcInfo -> return $ fstLine ++ showN dgnode
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu _ -> case maybeResult $ getGlobalTheory dgnode of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Nothing -> fail $
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer "cannot compute global theory of:\n" ++ fstLine
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Just gTh -> let subL = sublogicOfTh gTh in case nc of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer ProveNode incl mp mt tl thms -> do
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (newLib, sens) <- proveNode libEnv ln dg nl
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer gTh subL incl mp mt tl thms
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian if null sens then return "nothing to prove" else do
da955132262baab309a50fdffe228c9efe68251dCui Jian lift $ nextSess sessRef newLib k
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian return $ ppTopElement $ unode "results" $
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian map (\ (n, e) -> unode "goal"
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian [unode "name" n, unode "result" e]) sens
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian _ -> return $ case nc of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer NcTheory -> fstLine ++ showN gTh
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer NcProvers mt -> getProvers mt subL
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer NcTranslations mp -> getComorphs mp subL
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer EdgeQuery i _ ->
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder case getDGLinksById i dg of
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich [e@(_, _, l)] -> return $ showLEdge e ++ "\n" ++ showDoc l ""
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [] -> fail $ "no edge found with id: " ++ showEdgeId i
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer _ -> fail $ "multiple edges found with id: " ++ showEdgeId i
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyergetAllAutomaticProvers :: G_sublogics -> [(G_prover, AnyComorphism)]
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus LuettichgetAllAutomaticProvers subL = getAllProvers ProveCMDLautomatic subL logicGraph
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerfilterByProver :: Maybe String -> [(G_prover, AnyComorphism)]
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> [(G_prover, AnyComorphism)]
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerfilterByProver mp = case mp of
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder Nothing -> id
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just p -> filter ((== p) . getWebProverName . fst)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerfilterByComorph :: Maybe String -> [(G_prover, AnyComorphism)]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> [(G_prover, AnyComorphism)]
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian MaederfilterByComorph mt = case mt of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> id
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder Just c -> filter ((== c) . showComorph . snd)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetProverAndComorph :: Maybe String -> Maybe String -> G_sublogics
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [(G_prover, AnyComorphism)]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetProverAndComorph mp mc subL =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let ps = filterByComorph mc $ getAllAutomaticProvers subL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer spps = case filterByProver (Just "SPASS") ps of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu in case mp of
4d3b50fc78a0c99ff2914fb23f3c7fba6e38d790Thiemo Wiedemeyer Nothing -> spps
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu _ -> case filterByProver mp ps of
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanushowComorph :: AnyComorphism -> String
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyershowComorph (Comorphism cid) = removeFunnyChars . drop 1 . dropWhile (/= ':')
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer . map (\ c -> if c == ';' then ':' else c)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer $ language_name cid
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerremoveFunnyChars :: String -> String
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerremoveFunnyChars = filter (\ c -> isAlphaNum c || elem c "_.-")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetWebProverName :: G_prover -> String
d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyergetWebProverName = removeFunnyChars . getProverName
d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyergetProvers :: Maybe String -> G_sublogics -> String
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetProvers mt subL = ppTopElement . unode "provers" . map (unode "prover")
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer . nubOrd . map (getWebProverName . fst)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer . filterByComorph mt
5107ba7da675778f2fded68493512b60eff8a455Christian Maeder $ getAllAutomaticProvers subL
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetComorphs :: Maybe String -> G_sublogics -> String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetComorphs mp subL = ppTopElement . unode "translations"
5107ba7da675778f2fded68493512b60eff8a455Christian Maeder . map (unode "comorphism")
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu . nubOrd . map (showComorph . snd)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu . filterByProver mp
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu $ getAllAutomaticProvers subL
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian MaederproveNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab) -> G_theory
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder -> G_sublogics -> Bool -> Maybe String -> Maybe String -> Maybe Int
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer -> [String] -> ResultT IO (LibEnv, [(String, String)])
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo WiedemeyerproveNode le ln dg nl gTh subL useTh mp mt tl thms = case
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer getProverAndComorph mp mt subL of
5044e8de9e6fde7a139a5e34324c92a4d08a6e73Thiemo Wiedemeyer [] -> fail "no prover found"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let ks = map fst $ getThGoals gTh
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu unless (Set.null diffs) $ fail $ "unknown theorems: " ++ show diffs
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (res, prfs) <- lift $ autoProofAtNode useTh (fromMaybe 5 tl) thms gTh cp
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Nothing -> fail "proving failed"
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer Just sens -> if null sens then return (le, sens) else
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu Nothing -> error "proveNode"
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Just nTh -> return
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (Map.insert ln (updateLabelTheory le dg nl nTh) le, sens)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkPath :: Session -> LibName -> Int -> String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumkPath sess l k =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu '/' : concat [ show (getLibId l) ++ "?session="
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu | l /= sessLibName sess ]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerextPath :: Session -> LibName -> Int -> String
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerextPath sess l k = mkPath sess l k ++
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer if l /= sessLibName sess then "&" else "?"
1ac36418f204bbe56f4cd951a979180721758999Christian MaedersessAns :: LibName -> (Session, Int) -> String
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyersessAns libName (sess, k) =
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer let libEnv = sessLibEnv sess
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ln = show $ getLibId libName
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer aRef (mkPath sess l k) (show $ getLibId l) : map (\ d ->
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer aRef (extPath sess l k ++ d) d) displayTypes
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer libPath = extPath sess libName k
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer ref d = aRef (libPath ++ d) d
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer noderef (n, lbl) =
79d103748927615310322af6f7806c7cef11a802Christian Maeder let s = show n
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer lTh = dgn_theory lbl
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer gTh = globOrLocTh lbl
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder gs = getThGoals gTh
b6a59f004903ac7bc96323ee3ef09c01fd221157Christian Maeder noProvers = null $ getAllAutomaticProvers $ sublogicOfTh gTh
b6a59f004903ac7bc96323ee3ef09c01fd221157Christian Maeder lgs = map fst (getThGoals lTh) \\ map fst gs
b6a59f004903ac7bc96323ee3ef09c01fd221157Christian Maeder (ps, os) = partition (maybe False isProvedBasically . snd) gs
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder subsumed = if null lgs then "" else
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu " (" ++ shows (length lgs) " subsumed)"
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu goalInfo = '[' : shows (length ps) "/" ++ shows (length gs) "]"
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder unode "i" (s ++ " " ++ getDGNodeName lbl) : map (\ c ->
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder let isProve = c == "prove" in
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu if isProve && (null gs || noProvers) then
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer (if null gs then "no goals" ++ subsumed else
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer "no provers available " ++ goalInfo)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer else aRef (libPath ++ c ++ "=" ++ s
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ if isProve then "&theorems="
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer ++ intercalate "+"
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (map encodeForQuery
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- theorems containing spaces do not work with "+"
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer $ filter (all $ not . isSpace) $ map fst
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer $ if null os then gs else os)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder $ if isProve then c ++ goalInfo else c)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (if noProvers then nodeCommands \\ comorphs else nodeCommands)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer edgeref e@(_, _, lbl) =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer aRef (libPath ++ "edge=" ++ showEdgeId (dgl_id lbl))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer dg = lookupDGraph libName libEnv
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer nlabs = labNodesDG dg
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder elabs = labEdgesDG dg
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder in htmlHead ++ mkHtmlElem
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder ('(' : shows k ")" ++ ln)
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder (unode "b" ("library " ++ ln)
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder : map ref displayTypes
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder ++ menuElement : loadXUpdate (libPath ++ "update")
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder : [unode "p" "commands:"]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ [unode "ul" $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer map (unode "li" . ref) globalCommands]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ [unode "p" "imported libraries:"]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ [unode "ul" $
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu map (unode "li" . libref) $ Map.keys libEnv]
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu ++ [unode "p" (show (length nlabs)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ++ " nodes with local and global theories:")]
79d103748927615310322af6f7806c7cef11a802Christian Maeder ++ [unode "ul" $
038fc609b1d0dfe9698c4cab26fc7db2225820efMihai Codescu map (unode "li" . noderef) nlabs]
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu ++ [unode "p" (show (length elabs) ++ " edges:")]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ++ [unode "ul" $
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder map (unode "li" . edgeref)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder $ sortBy (comparing (\ (_, _, l) -> dgl_id l)) elabs]
d1066b8fb69179973dcab47154858d77e72760a7Thiemo WiedemeyergetHetsLibContent :: HetcatsOpts -> String -> String -> IO [Element]
66b035879accdc5f8337726173f800286a87fd78Christian MaedergetHetsLibContent opts dir query = do
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder let hlibs = libdirs opts
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ds <- if null dir then return hlibs else
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder filterM doesDirectoryExist $ map (</> dir) hlibs
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer fs <- fmap (sortBy cmpFilePath . filter (not . isPrefixOf ".") . concat)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer $ mapM getDirContents ds
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return $ map (mkHtmlRef query) $ getParent dir : fs
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai CodescugetParent :: String -> String
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetParent = addTrailingPathSeparator . ("/" </>) . takeDirectory
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder . dropTrailingPathSeparator
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- | a variant that adds a trailing slash
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetDirContents :: FilePath -> IO [FilePath]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanugetDirContents d = do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu fs <- getDirectoryContents d
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu mapM (\ f -> doesDirectoryExist (d </> f) >>= \ b -> return
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu $ if b then addTrailingPathSeparator f else f) fs
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuaRef :: String -> String -> Element
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai CodescuaRef lnk txt = add_attr (mkAttr "href" lnk) $ unode "a" txt
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyermkHtmlRef :: String -> String -> Element
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyermkHtmlRef query entry = unode "dir" $ aRef (entry ++ query) entry
8b23feb0879618f786f08152c6df6b6e2cb8898bMihai CodescuheadElems :: String -> [Element]
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian MaederheadElems path = let d = "default" in unode "strong" "Choose query type:" :
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu map (\ q -> aRef (if q == d then "/" </> path else '?' : q) q)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (d : displayTypes) ++ [menuElement, uploadHtml]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermenuElement :: Element
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermenuElement = aRef "?menus" "menus"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerhtmlHead :: String
66b035879accdc5f8337726173f800286a87fd78Christian Maeder let dtd = "PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu url = "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\""
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu in concat ["<!DOCTYPE html ", dtd, " ", url, ">\n"]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuinputNode :: Element
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuinputNode = unode "input" ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuloadNode :: String -> Element
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuloadNode name = add_attrs
66b035879accdc5f8337726173f800286a87fd78Christian Maeder [ mkAttr "type" "file"
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , mkAttr "name" name
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , mkAttr "size" "40"]
66b035879accdc5f8337726173f800286a87fd78Christian MaedersubmitNode :: Element
66b035879accdc5f8337726173f800286a87fd78Christian MaedersubmitNode = add_attrs
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer [ mkAttr "type" "submit"
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , mkAttr "value" "submit"]
66b035879accdc5f8337726173f800286a87fd78Christian MaedermkForm :: String -> [Element] -> Element
66b035879accdc5f8337726173f800286a87fd78Christian MaedermkForm a = add_attrs
66b035879accdc5f8337726173f800286a87fd78Christian Maeder [ mkAttr "action" a
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , mkAttr "enctype" "multipart/form-data"
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , mkAttr "method" "post" ]
66b035879accdc5f8337726173f800286a87fd78Christian Maeder . unode "form"
66b035879accdc5f8337726173f800286a87fd78Christian MaederuploadHtml :: Element
66b035879accdc5f8337726173f800286a87fd78Christian MaederuploadHtml = mkForm "/"
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer [ loadNode "file"
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder , unode "p" $ add_attrs
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [ mkAttr "cols" "68"
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder , mkAttr "rows" "22"
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder , mkAttr "name" "content" ] $ unode "textarea" ""
66b035879accdc5f8337726173f800286a87fd78Christian Maeder , submitNode ]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerloadXUpdate :: String -> Element
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyerloadXUpdate a = mkForm a
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [ unode "i" "xupdate"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , loadNode "xupdate"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , unode "i" "impacts"
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer , loadNode "impacts"
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer , submitNode ]