db6af887f634d80de59ae1a53658ee77921a5594cmaeder{-# LANGUAGE CPP, DoAndIfThenElse #-}
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : run hets as server
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2010
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : Christian.Maeder@dfki.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable (via imports)
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maedermodule PGIP.Server (hetsServer) where
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksaimport qualified PGIP.Output.Provers as OProvers
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksaimport PGIP.ReasoningParameters as ReasoningParameters
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksaimport qualified PGIP.Server.Examples as Examples
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maederimport Control.Monad.Trans (lift, liftIO)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder#ifdef WARP1
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksaimport Data.Conduit.Lazy (lazyConsume)
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maederimport qualified Data.Text as T
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport qualified Data.ByteString.Lazy.Char8 as BS
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport qualified Data.ByteString.Char8 as B8
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbrichtimport Static.History (changeDGH)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport qualified Static.ToJson as ToJson
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederimport Proofs.AbstractState as AbsState
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksaimport Text.XML.Light.Cursor hiding (lefts, rights)
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maederimport Common.DocUtils (pretty, showGlobalDoc, showDoc)
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbrichtimport Common.ExtSign (ExtSign (..))
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Common.Json (Json (..), ppJson)
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Control.Exception (catch, throwTo)
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport Control.Exception.Base (SomeException)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksaimport Control.Concurrent (myThreadId, ThreadId)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksaimport qualified Data.Aeson as Aeson
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maederimport qualified Data.IntMap as IntMap
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon Ulbrichtimport qualified Data.Map as Map
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport qualified Data.Set as Set
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksaimport qualified Data.CaseInsensitive as CI
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksaimport System.Posix.Process (getProcessID)
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksadata UsedAPI = OldWebAPI | RESTfulAPI deriving (Show, Eq, Ord)
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederrandomKey :: IO Int
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederrandomKey = randomRIO (100000000, 999999999)
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian MaedersessGraph :: DGQuery -> Session -> Maybe (LibName, DGraph)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedersessGraph dgQ s =
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let le = sessLibEnv s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder ln = sessLibName s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in case dgQ of
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder DGQuery _ (Just path) ->
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder find (\ (n, _) -> libToFileName n == path)
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder _ -> fmap (\ dg -> (ln, dg)) $ Map.lookup ln le
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaedergetVal :: [QueryPair] -> String -> Maybe String
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaedergetVal qs = fromMaybe Nothing . (`lookup` qs)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedergetIP4 :: String -> [String]
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedergetIP4 = splitOn '.' . takeWhile (\ c -> isDigit c || c == '.')
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedermatchIP4 :: [String] -> [String] -> Bool
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedermatchIP4 ip mask = case mask of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ft : rt -> case ip of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder [] -> False -- mask too long or IP too short
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder d : s -> (null ft || ft == d) && matchIP4 rt s
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedermatchWhite :: [String] -> [[String]] -> Bool
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedermatchWhite ip l = null l || any (matchIP4 ip) l
8723ec450f2e7a024230467c0c28a3f154905483cmaeder#ifdef WARP3
8723ec450f2e7a024230467c0c28a3f154905483cmaedertype WebResponse = (Response -> IO ResponseReceived) -> IO ResponseReceived
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill MossakowskicatchException :: SomeException -> Response
e99cb5db53054d96bb97c9b8b130bd249802450eTill MossakowskicatchException e =
83ce5f14d356cd62e98f4f674da7f11ea1869eb0Till Mossakowski mkResponse textC
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski internalServerError500
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski ("*** Error:\n" ++ show e)
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksatype WebResponse = (Response -> RsrcIO Response) -> RsrcIO Response
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksadeletePidFileAndExit :: HetcatsOpts -> ThreadId -> ExitCode -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksadeletePidFileAndExit opts threadId exitCode = do
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa deletePidFile opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa throwTo threadId exitCode
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederhetsServer :: HetcatsOpts -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksahetsServer opts = do
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa tid <- myThreadId
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa writePidFile opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa installHandler sigINT (Catch $ deletePidFileAndExit opts tid ExitSuccess) Nothing
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa installHandler sigTERM (Catch $ deletePidFileAndExit opts tid ExitSuccess) Nothing
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa hetsServer' opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa deletePidFile opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksawritePidFile :: HetcatsOpts -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksawritePidFile opts =
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa let pidFilePath = pidFile opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa v = verbose opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa in (unless (null pidFilePath) $
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa do unless (null pidFilePath)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (verbMsgIOLn v 2 ("Writing PIDfile " ++ show pidFilePath))
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pid <- getProcessID
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa writeFile pidFilePath (show pid))
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksadeletePidFile :: HetcatsOpts -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksadeletePidFile opts =
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa let pidFilePath = pidFile opts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa in (unless (null pidFilePath) $ removeFile $ pidFile opts)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksahetsServer' :: HetcatsOpts -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksahetsServer' opts1 = do
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder tempDir <- getTemporaryDirectory
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder let tempLib = tempDir </> "MyHetsLib"
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder logFile = tempDir </>
5d3978bb76c33d08d6297f69f10bbc04721ee3a5cmaeder ("hets-" ++ show port ++ ".log")
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder opts = opts1 { libdirs = tempLib : libdirs opts1 }
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder port1 = listen opts1
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder port = if port1 < 0 then 8000 else port1
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder wl = whitelist opts1
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder bl = blacklist opts1
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder prList ll = intercalate ", " $ map (intercalate ".") ll
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder createDirectoryIfMissing False tempLib
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder writeFile logFile ""
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder unless (null wl) . appendFile logFile
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder $ "white list: " ++ prList wl ++ "\n"
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder unless (null bl) . appendFile logFile
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder $ "black list: " ++ prList bl ++ "\n"
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder sessRef <- newIORef (IntMap.empty, Map.empty)
293abe6af19382a456dbe612aef45054ef76832fcmaeder putIfVerbose opts 1 $ "hets server is listening on port " ++ show port
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder putIfVerbose opts 2 $ "for more information look into file: " ++ logFile
8723ec450f2e7a024230467c0c28a3f154905483cmaeder#ifdef WARP3
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski runSettings (setOnExceptionResponse catchException $
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski setPort port $
8e3e7896a1818bb0521674cf4f10403e9f9911b3Till Mossakowski setTimeout 86400 defaultSettings)
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder $ \ re respond -> do
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder run port $ \ re -> do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder let respond = liftIO . return
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder let rhost = shows (remoteHost re) "\n"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ip = getIP4 rhost
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder white = matchWhite ip wl
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder black = any (matchIP4 ip) bl
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder splitQuery = map (\ (bs, ms) -> (B8.unpack bs, fmap B8.unpack ms))
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder $ queryString re
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder pathBits = map T.unpack $ pathInfo re
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder meth = B8.unpack (requestMethod re)
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder query = showPathQuery pathBits splitQuery
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder time <- getCurrentTime
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder createDirectoryIfMissing False tempLib
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder (m, _) <- readIORef sessRef
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder appendFile logFile rhost
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder unless black $ if white then do
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder appendFile logFile $ shows time " sessions: "
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder ++ shows (IntMap.size m) "\n"
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder appendFile logFile $ shows (requestHeaders re) "\n"
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder unless (null query) $ appendFile logFile $ query ++ "\n"
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder else appendFile logFile "not white listed\n"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder if not white || black then respond $ mkResponse "" status403 ""
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa -- if path could be a RESTful request, try to parse it
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder eith <- liftIO $ getArgFlags splitQuery
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder case eith of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Left err -> queryFail err respond
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Right (qr, vs, fs) ->
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder let eith2 = getSwitches qr
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder in case eith2 of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Left err -> queryFail err respond
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Right (qr2, fs2) ->
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder let newOpts = foldl makeOpts opts $ fs ++ map snd fs2
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa in if isGraphQL meth pathBits then do
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa responseString <- processGraphQL newOpts sessRef re
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa respond $ mkOkResponse "application/json" responseString
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa else if isRESTful pathBits then do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa requestBodyBS <- strictRequestBody re
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa requestBodyParams <- parseRequestParams re requestBodyBS
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder let unknown = filter (`notElem` allQueryKeys) $ map fst qr2
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa if null unknown
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa then parseRESTful newOpts sessRef pathBits
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa (map fst fs2 ++ map (\ (a, b) -> a ++ "=" ++ b) vs)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa qr2 requestBodyBS requestBodyParams meth respond
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder else queryFail ("unknown query key(s): " ++ show unknown) respond
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -- only otherwise stick to the old response methods
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder else oldWebApi newOpts tempLib sessRef re pathBits qr2
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder meth respond
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaparseRequestParams :: Request -> BS.ByteString -> RsrcIO Json
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaparseRequestParams request requestBodyBS =
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa noParams :: Json
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa noParams = JNull
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa lookupHeader :: String -> Maybe String
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa lookupHeader s =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa liftM B8.unpack $ lookup (CI.mk $ B8.pack s) $ requestHeaders request
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa formParams :: RsrcIO (Maybe Json)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa formParams =
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa let toJsonObject :: [(B8.ByteString, B8.ByteString)] -> String
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa toJsonObject assocList = "{"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ++ intercalate ", " (map (\ (k, v) ->
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa show k ++ ": " ++ jsonStringOrArray v) assocList)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa jsonStringOrArray str =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa if B8.head str == '[' then B8.unpack str else show str
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (formDataB8, _) <- parseRequestBody lbsBackEnd request
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa return $ parseJson $ toJsonObject formDataB8
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa lazyRequestBody :: Request -> ResourceT IO BS.ByteString
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa lazyRequestBody = fmap BS.fromChunks . lazyConsume . requestBody
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa liftM (fromMaybe noParams) $ case lookupHeader "Content-Type" of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Just "application/json" -> jsonBody requestBodyBS
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa Just "multipart/form-data" -> formParams
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa _ -> formParams
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder-- | the old API that supports downloading files and interactive stuff
6f9d360a425bdae3bd15289388e64c14a85eca43cmaederoldWebApi :: HetcatsOpts -> FilePath -> Cache -> Request -> [String]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -> [QueryPair] -> String -> WebResponse
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen KuksaoldWebApi opts tempLib sessRef re pathBits splitQuery meth respond =
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa case meth of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder "GET" -> if isJust $ lookup "menus" splitQuery
8723ec450f2e7a024230467c0c28a3f154905483cmaeder then mkMenuResponse respond else do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder let path = intercalate "/" pathBits
8723ec450f2e7a024230467c0c28a3f154905483cmaeder dirs@(_ : cs) <- liftIO $ getHetsLibContent opts path splitQuery
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa if not (null cs) || null path then htmlResponse path dirs respond
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht -- AUTOMATIC PROOFS (parsing)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder else if isJust $ getVal splitQuery "autoproof" then
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht let qr k = Query (DGQuery k Nothing) $
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht anaAutoProofQuery splitQuery in do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Result ds ms <- liftIO $ runResultT
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ case readMaybe $ head pathBits of
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Nothing -> fail "cannot read session id for automatic proofs"
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Just k' -> getHetsResult opts [] sessRef (qr k')
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Nothing OldWebAPI proofFormatterOptions
8723ec450f2e7a024230467c0c28a3f154905483cmaeder respond $ case ms of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> mkResponse textC status422 $ showRelDiags 1 ds
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just (t, s) -> mkOkResponse t s
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht -- AUTOMATIC PROOFS E.N.D.
8723ec450f2e7a024230467c0c28a3f154905483cmaeder else getHetsResponse opts [] sessRef pathBits splitQuery respond
233754e153e665aa748bf8b45bd8b1938b6c21a7Christian Maeder (params, files) <- parseRequestBody lbsBackEnd re
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa let opts' = case lookup (B8.pack "input-type") params of
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa Nothing -> opts
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa Just inputType -> if null $ B8.unpack inputType
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa else opts { intype = read $ B8.unpack inputType }
8723ec450f2e7a024230467c0c28a3f154905483cmaeder mTmpFile <- case lookup "content"
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht $ map (\ (a, b) -> (B8.unpack a, b)) params of
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Nothing -> return Nothing
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Just areatext -> let content = B8.unpack areatext in
8723ec450f2e7a024230467c0c28a3f154905483cmaeder if all isSpace content then return Nothing else liftIO $ do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht tmpFile <- getTempFile content "temp.het"
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return $ Just tmpFile
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let res tmpFile =
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa getHetsResponse opts' [] sessRef [tmpFile] splitQuery respond
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder mRes = maybe (queryFail "nothing submitted" respond)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder case files of
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder [] -> if isJust $ getVal splitQuery "prove" then
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa getHetsResponse opts' [] sessRef pathBits
8723ec450f2e7a024230467c0c28a3f154905483cmaeder (splitQuery ++ map (\ (a, b)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -> (B8.unpack a, Just $ B8.unpack b)) params) respond
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder [(_, f)] | isNothing $ lookup updateS splitQuery -> do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let fn = takeFileName $ B8.unpack $ fileName f
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht if any isAlphaNum fn then do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder let tmpFile = tempLib </> fn
8723ec450f2e7a024230467c0c28a3f154905483cmaeder liftIO $ BS.writeFile tmpFile $ fileContent f
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht maybe (res tmpFile) res mTmpFile
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht _ -> getHetsResponse
5586064a8b4b5328f37f9a7cf2aaf893ed099e67Eugen Kuksa opts' (map snd files) sessRef pathBits splitQuery respond
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaeder _ -> respond $ mkResponse "" status400 ""
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht-- extract what we need to know from an autoproof request
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaederanaAutoProofQuery :: [QueryPair] -> QueryKind
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon UlbrichtanaAutoProofQuery splitQuery = let
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder lookup2 = getVal splitQuery
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht prover = lookup2 "prover"
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht trans = lookup2 "translation"
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht timeout = lookup2 "timeout" >>= readMaybe
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht include = maybe False (== "on") $ lookup2 "includetheorems"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht nodeSel = filter (/= "includetheorems")
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht $ map fst $ filter ((== Just "on") . snd) splitQuery
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa axioms = mSplitOnComma $ lookup2 "axioms"
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht prOrCons = case lookup2 "autoproof" of
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Just "proof" -> GlProofs
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht Just "cons" -> GlConsistency
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht err -> error $ "illegal autoproof method: " ++ show err
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa in GlAutoProve $
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ProveCmd prOrCons include prover trans timeout nodeSel False axioms
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa-- quick approach to whether or not the query can be a RESTful request
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksaisRESTful :: [String] -> Bool
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksaisRESTful pathBits = case pathBits of
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa [h] | elem h ["numeric-version", "version", "robots.txt"] -> True
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa h : _ -> elem h listRESTfulIdentifiers
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksalistRESTfulIdentifiers :: [String]
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksalistRESTfulIdentifiers =
1698621aea64f7a2b04a4084984eed1437e22771Christian Maeder [ "libraries", "sessions", "menus", "filetype", "hets-lib", "dir"]
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder ++ nodeEdgeIdes ++ newRESTIdes
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder ++ ["available-provers"]
6fb590a3747600c145abfd7c3483039fb03af032Christian MaedernodeEdgeIdes :: [String]
6fb590a3747600c145abfd7c3483039fb03af032Christian MaedernodeEdgeIdes = ["nodes", "edges"]
6fb590a3747600c145abfd7c3483039fb03af032Christian MaedernewRESTIdes :: [String]
cbd64ad1d663565751cb9442f78a40ff96c6bed6Eugen Kuksa [ "dg", "translations", "provers", "consistency-checkers", "prove"
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu , "consistency-check", "theory" ]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederqueryFail :: String -> WebResponse
986888e7f4d8ed681272a79c63f329ce8037063dcmaederqueryFail msg respond = respond $ mkResponse textC status400 msg
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaederallQueryKeys :: [String]
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaederallQueryKeys = [updateS, "library", "consistency-checker"]
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder ++ globalCommands ++ knownQueryKeys
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksadata RequestBodyParam = Single String | List [String]
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa-- query is analysed and processed in accordance with RESTful interface
4937a0e373f619dc520799923acec42db5da5eb3Eugen KuksaparseRESTful :: HetcatsOpts -> Cache -> [String] -> [String] -> [QueryPair]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> BS.ByteString -> Json -> String -> WebResponse
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa opts sessRef pathBits qOpts splitQuery requestBodyBS requestBodyParams meth respond = let
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht {- some parameters from the paths query part might be needed more than once
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (when using lookup upon querybits, you need to unpack Maybe twice) -}
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupQueryStringParam :: String -> Maybe String
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupQueryStringParam = getVal splitQuery
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupBodyParam :: String -> Json -> Maybe RequestBodyParam
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupBodyParam key json = case json of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa JObject pairs -> case lookup key pairs of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Just (JArray a) -> Just $ List $ map (read . ppJson) a
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Just v -> Just $ Single $ read $ ppJson v
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> Nothing
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> Nothing
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupSingleParam :: String -> Maybe String
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa lookupSingleParam key = case meth of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa "GET" -> lookupQueryStringParam key
f345dca8aecfdbc7137a28dda45f9a5574d1fd14Eugen Kuksa _ -> case lookupBodyParam key requestBodyParams of
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa Just (Single s) -> Just s
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> Nothing
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa isParamTrue :: Bool -> String -> Bool
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa isParamTrue def key = case fmap (map toLower) $ lookupSingleParam key of
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa Nothing -> def
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa Just "true" -> True
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa session = lookupSingleParam "session" >>= readMaybe
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa library = lookupSingleParam "library"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa format_ = lookupSingleParam "format"
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa nodeM = lookupSingleParam "node"
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa includeDetails = isParamTrue True "includeDetails"
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa includeProof = isParamTrue True "includeProof"
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa transM = lookupSingleParam "translation"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningParametersE = parseReasoningParametersEither requestBodyBS
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder queryFailure = queryFail
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa ("this query does not comply with RESTful interface: "
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder ++ showPathQuery pathBits splitQuery) respond
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht -- since used more often, generate full query out of nodeIRI and nodeCmd
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder nodeQuery s = NodeQuery $ maybe (Right s) Left (readMaybe s :: Maybe Int)
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa pfOptions = proofFormatterOptions
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa { pfoIncludeProof = includeProof
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa , pfoIncludeDetails = includeDetails
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder parseNodeQuery :: Monad m => String -> Int -> m NodeCommand -> m Query.Query
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder parseNodeQuery p sId ncmd = ncmd >>= let
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder in return . Query (DGQuery sId (Just p)) . nodeQuery (getFragment p)
562e30787355109feb0133ffea2ad86b6c143c26Simon Ulbricht -- call getHetsResult with the properly generated query (Final Result)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder getResponseAux myOpts qr = do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let format' = Just $ fromMaybe "xml" format_
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Result ds ms <- liftIO $ runResultT $
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu getHetsResult myOpts [] sessRef qr format' RESTfulAPI pfOptions
8723ec450f2e7a024230467c0c28a3f154905483cmaeder respond $ case ms of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> mkResponse textC status422 $ showRelDiags 1 ds
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just (t, s) -> mkOkResponse t s
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder getResponse = getResponseAux opts
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht -- respond depending on request Method
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder in case meth of
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder rm | elem rm ["GET", "POST"] -> case pathBits of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ["robots.txt"] -> respond $ mkOkResponse textC
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder $ unlines ["User-agent: *", "Disallow: /"]
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- show all menu options
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder ["menus"] -> mkMenuResponse respond
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -- list files from directory
8723ec450f2e7a024230467c0c28a3f154905483cmaeder "dir" : r -> do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder let path' = intercalate "/" r
8723ec450f2e7a024230467c0c28a3f154905483cmaeder dirs <- liftIO $ getHetsLibContent opts path' splitQuery
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa htmlResponse path' dirs respond
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa ["version"] -> respond $ mkOkResponse textC hetsVersion
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa ["numeric-version"] ->
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa respond $ mkOkResponse textC hetsVersionNumeric
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder ["available-provers"] ->
90d3a604eeb43972cef8bfd283a0118a4ad6e9e7cmaeder liftIO (usableProvers logicGraph)
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder >>= respond . mkOkResponse xmlC . ppTopElement
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -- get dgraph from file
8723ec450f2e7a024230467c0c28a3f154905483cmaeder "filetype" : libIri : _ -> mkFiletypeResponse opts libIri respond
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht "hets-lib" : r -> let file = intercalate "/" r in
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa getResponse $ Query (NewDGQuery file []) $ DisplayQuery format_
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -- get library (complies with get/hets-lib for now)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ["libraries", libIri, "development_graph"] ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa getResponse $ Query (NewDGQuery libIri []) $ DisplayQuery format_
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -- get previously created session
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht "sessions" : sessId : cmd -> case readMaybe sessId of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> queryFail ("failed to read session number from " ++ sessId)
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder (case nodeM of
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Just ndIri -> parseNodeQuery ndIri sId $ case cmd of
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder ["provers"] -> return $ NcProvers GlProofs transM
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht ["translations"] -> return $ NcTranslations Nothing
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht _ -> fail $ "unknown node command for a GET-request: "
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht ++ intercalate "/" cmd
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht Nothing -> fmap (Query (DGQuery sId Nothing)) $ case cmd of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa [] -> return $ DisplayQuery format_
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder ["provers"] -> return $ GlProvers GlProofs transM
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder ["translations"] -> return GlTranslations
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht _ -> fail $ "unknown global command for a GET-request: "
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht ++ intercalate "/" cmd) >>= getResponse
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -- get node or edge view
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder nodeOrEdge : p : c | elem nodeOrEdge nodeEdgeIdes -> let
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder iriPath = takeWhile (/= '#') p
7f150d7930b47c297e184638ecd811b3656b0dadChristian Maeder dgQ = maybe (NewDGQuery (fromMaybe iriPath library) [])
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (`DGQuery` library) session
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder f = getFragment p
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder in case elemIndex nodeOrEdge nodeEdgeIdes of
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Just 0 -> let
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder i = maybe (Right f) Left $ readMaybe f in
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder getResponse $ Query dgQ $ NodeQuery i $ case c of
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht ["theory"] -> NcCmd Query.Theory
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Just 1 -> case readMaybe f of
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder Just i -> getResponse $ Query dgQ $ EdgeQuery i "edge"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> queryFail ("failed to read edgeId from " ++ f) respond
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder _ -> error $ "PGIP.Server.elemIndex " ++ nodeOrEdge
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder newIde : libIri : rest ->
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder let cmdOptList = filter (/= "") rest
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder (optFlags, cmdList) = partition (`elem` map fst optionFlags)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder newOpts = foldl makeOpts opts $ mapMaybe (`lookup` optionFlags)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa validReasoningParams = isRight reasoningParametersE <=
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa elem newIde ["prove", "consistency-check"]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in if elem newIde newRESTIdes
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa && all (`elem` globalCommands) cmdList
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa && validReasoningParams
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu qkind = case newIde of
cbd64ad1d663565751cb9442f78a40ff96c6bed6Eugen Kuksa "translations" -> case nodeM of
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder Nothing -> GlTranslations
f382d86a384743a770cd5490a641e38ed1069c5cChristian Maeder Just n -> nodeQuery n $ NcTranslations Nothing
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder _ | elem newIde ["provers", "consistency-checkers"] ->
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder let pm = if newIde == "provers" then GlProofs else GlConsistency
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder in case nodeM of
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder Nothing -> GlProvers pm transM
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder Just n -> nodeQuery n $ NcProvers pm transM
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder _ | elem newIde ["prove", "consistency-check"] ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa case reasoningParametersE of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Left message_ -> error ("Invalid parameters: " ++ message_) -- cannot happen
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Right reasoningParameters ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let proverMode = if newIde == "prove"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa then GlProofs
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa else GlConsistency
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in GlAutoProveREST proverMode reasoningParameters
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu "dg" -> case transM of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Nothing -> DisplayQuery (Just $ fromMaybe "xml" format_)
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu "theory" -> case transM of
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Nothing -> case nodeM of
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu Just x -> NodeQuery (maybe (Right x) Left $ readMaybe x)
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Nothing -> error "REST: theory"
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Just tr -> case nodeM of
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu Just x -> NodeQuery (maybe (Right x) Left $ readMaybe x)
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Nothing -> error "REST: theory"
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu _ -> error $ "REST: unknown " ++ newIde
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu in getResponseAux newOpts . Query (NewDGQuery libIri $ cmdList
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu ++ Set.toList (Set.fromList $ optFlags ++ qOpts)) $ qkind
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa else if validReasoningParams
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa then queryFailure
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa else case reasoningParametersE of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Left message_ ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa queryFail ("Invalid parameters: " ++ message_) respond
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa error "Unexpected error in PGIP.Server.parseRESTful"
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht _ -> queryFailure
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht "PUT" -> case pathBits of
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht {- execute global commands
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht TODO load other library ??? -}
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ["libraries", libIri, "proofs", prId, cmd] ->
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht case readMaybe prId of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> queryFail ("failed to read sessionId from " ++ prId)
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht Just sessId -> let
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder dgQ = DGQuery sessId $ Just libIri in
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht getResponse $ Query dgQ $ GlobCmdQuery cmd
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht -- execute a proof or calculus request
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ["sessions", sessId, cmd] -> case readMaybe sessId of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Nothing -> queryFail ("failed to read sessionId from " ++ sessId)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht Just sId -> case cmd of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa "prove" -> case reasoningParametersE of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Left message_ -> fail ("Invalid parameters: " ++ message_)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Right reasoningParameters ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return $ Query (DGQuery sId Nothing) $
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlAutoProveREST GlProofs reasoningParameters
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder >>= getResponse
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- on other cmd look for (optional) specification of node or edge
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa _ -> case (nodeM, lookupSingleParam "edge") of
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- fail if both are specified
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder (Just _, Just _) ->
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder fail "please specify only either node or edge"
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- call command upon a single node
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder (Just ndIri, Nothing) -> parseNodeQuery ndIri sId
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder $ case lookup cmd $ map (\ a -> (showNodeCmd a, a)) nodeCmds of
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Just nc -> return $ NcCmd nc
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht _ -> fail $ "unknown node command '" ++ cmd ++ "' "
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- call (the only) command upon a single edge
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder (Nothing, Just edIri) -> case readMaybe $ getFragOfCode edIri of
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder Just i -> return $ Query (DGQuery sId Nothing)
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder $ EdgeQuery i "edge"
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder fail $ "failed to read edgeId from edgeIRI: " ++ edIri
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder -- call of global command
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder _ -> return $ Query (DGQuery sId Nothing) $ GlobCmdQuery cmd
30ccae9374798a92124e1b294404f7b55ffbb412Christian Maeder >>= getResponse
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht -- fail if request doesn't comply
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht _ -> queryFailure
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht {- create failure response if request method is not known
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (should never happen) -}
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaeder _ -> respond $ mkResponse "" status400 ""
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaparseReasoningParametersEither :: BS.ByteString -> Either String ReasoningParameters
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaparseReasoningParametersEither requestBodyBS = Aeson.eitherDecode requestBodyBS
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen KuksamSplitOnComma :: Maybe String -> [String]
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen KuksamSplitOnComma mstr = case mstr of
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa Nothing -> []
f07364021546acc2fa5da55501bd6207b040f7bfEugen Kuksa Just str -> splitOn ',' str
8723ec450f2e7a024230467c0c28a3f154905483cmaedermkMenuResponse :: WebResponse
8723ec450f2e7a024230467c0c28a3f154905483cmaedermkMenuResponse respond =
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder respond $ mkOkResponse xmlC $ ppTopElement $ unode "menus" mkMenus
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaedermkMenus :: [Element]
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaedermkMenus = menuTriple "" "Get menu triples" "menus"
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder : menuTriple "/DGraph" updateS updateS
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder : map (\ (c, _) -> menuTriple "/" (menuTextGlobCmd c) $ cmdlGlobCmd c)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder allGlobLibAct
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder ++ map (\ nc -> menuTriple "/DGraph/DGNode" ("Show " ++ nc) nc) nodeCommands
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder ++ [menuTriple "/DGraph/DGLink" "Show edge info" "edge"]
986888e7f4d8ed681272a79c63f329ce8037063dcmaederstatus422 :: Status
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaederstatus422 = Status 422 $ B8.pack "Unprocessable Entity"
8723ec450f2e7a024230467c0c28a3f154905483cmaedermkFiletypeResponse :: HetcatsOpts -> String -> WebResponse
8723ec450f2e7a024230467c0c28a3f154905483cmaedermkFiletypeResponse opts libIri respond = do
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder res <- liftIO $ getContentAndFileType opts libIri
8723ec450f2e7a024230467c0c28a3f154905483cmaeder respond $ case res of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Left err -> mkResponse textC status422 err
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Right (mr, _, fn, _) -> case mr of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Nothing -> mkResponse textC status422 $ fn ++ ": unknown file type"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just r -> mkOkResponse textC $ fn ++ ": " ++ r
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaedermenuTriple :: String -> String -> String -> Element
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian MaedermenuTriple q d c = unode "triple"
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder [ unode "xquery" q
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder , unode "displayname" d
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder , unode "command" c ]
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlResponse :: FilePath -> [Element] -> WebResponse
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlResponse path listElements respond = respond . mkOkResponse htmlC
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa $ htmlPageWithTopContent path listElements
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlPageWithTopContent :: FilePath -> [Element] -> String
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksahtmlPageWithTopContent path listElements =
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa htmlPage (if null path then "Start Page" else path) []
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa (pageHeader ++ pageOptions path listElements)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlPage :: String -> String -> [Element] -> String -> String
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlPage title javascripts body rawHtmlPageFooter = htmlHead title javascripts
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ intercalate "\n" (map ppElement body)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ++ htmlWrapBottomContent rawHtmlPageFooter
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlHead :: String -> String -> String
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlHead title javascript =
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa "<!DOCTYPE html>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ "<html lang=\"en\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <head>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <meta charset=\"utf-8\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <meta content=\"width=device-width,initial-scale=1,shrink-to-fit=no\" name=\"viewport\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <meta content=\"#000000\" name=\"theme-color\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <meta name=\"robots\" content=\"noindex,nofollow\">\n"
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa ++ " <title>Hets, the DOLiator - " ++ title ++ "</title>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <!-- Semantic UI stylesheet -->\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <style type=\"text/css\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ semanticUiCss ++ "\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </style>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <!-- Hets stylesheet -->\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <style type=\"text/css\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ hetsCss ++ "\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </style>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </head>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <body>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <!-- jQuery -->\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <script type=\"text/javascript\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ jQueryJs ++ "\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </script>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <!-- Semantic UI Javascript -->\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <script type=\"text/javascript\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ semanticUiJs ++ "\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </script>\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " <!-- Static Hets Javascript -->\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " <script type=\"text/javascript\">\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ hetsJs ++ "\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " </script>\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " <!-- Dynamic Hets Javascript -->\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " <script type=\"text/javascript\">\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ javascript ++ "\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ " </script>\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " <div class=\"ui left aligned doubling stackable centered relaxed grid container\">\n"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlWrapBottomContent :: String -> String
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlWrapBottomContent content =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa if null content then "" else
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa " <div class=\"ui segment pushable left aligned\" style=\"overflow: auto;\">\n"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ++ " </div>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen KuksahtmlFoot :: String
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa ++ " </body>\n"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa ++ "</html>\n"
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageHeader :: [Element]
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa [ add_attr (mkAttr "class" "row") $ unode "div" $ unode "h1" "Hets, the DOLiator"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui text container raised segment center aligned") $
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa unode "div" [ unode "p" "Welcome to DOLiator, the web interface to our implementation of the \"Ontology, Modeling and Specification Language\""
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa , add_attr (mkAttr "class" "ui horizontal list") $ unode "div"
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa [ add_attr (mkAttr "target" "_blank") $ add_attr (mkAttr "class" "item") $ aRef "http://dol-omg.org/" "DOL Homepage"
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa , add_attr (mkAttr "target" "_blank") $ add_attr (mkAttr "class" "item") $ aRef "http://hets.eu/" "Hets Homepage"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa , add_attr (mkAttr "class" "item") $ aRef "mailto:hets-devel@informatik.uni-bremen.de" "Contact"
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageOptions :: String -> [Element] -> [Element]
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageOptions path listElements =
a0f7f1d3aef3e4229f57eb6065a62e48d15b66fbEugen Kuksa [ add_attr (mkAttr "class" "row") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui relaxed grid container segment") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ add_attr (mkAttr "class" "row centered") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa unode "p" "Select a local DOL file as library or enter a DOL specification in the text area or choose one of the minimal examples from the right hand side and press \"Submit\"."
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "three column row") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ pageOptionsFile
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa , pageOptionsExamples (not $ null path) listElements
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageOptionsFile :: Element
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageOptionsFile =
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa add_attr (mkAttr "class" "ui container ten wide column left aligned") $ unode "div" $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "ui row") $ unode "div" pageOptionsFileForm
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageOptionsExamples :: Bool -> [Element] -> Element
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageOptionsExamples moreExamplesAreOpen listElements =
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa add_attr (mkAttr "class" "ui container six wide column left aligned") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ unode "h4" "Minimal Examples"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "ui list") $ unode "div" $
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa map (\ (elementName, inputType, exampleText) ->
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "item") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attrs [ mkAttr "class" "insert-example-into-user-input-text"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "data-text" exampleText
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , mkAttr "data-input-type" inputType
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ] $ unode "span" elementName
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa ) [ ("DOL", "dol", Examples.dol)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("CASL", "casl", Examples.casl)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("OWL", "owl", Examples.owl)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("CLIF", "clif", Examples.clif)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("Propositional", "het", Examples.propositional)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("RDF", "rdf", Examples.rdf)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("TPTP", "tptp", Examples.tptp)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("HasCASL", "het", Examples.hascasl)
7e92d8017cdef293b8ab8d9eb925867bbd77ae10Eugen Kuksa , ("Modal", "het", Examples.modal)
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa , pageMoreExamples moreExamplesAreOpen listElements
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageOptionsFileForm :: Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksapageOptionsFileForm = add_attr (mkAttr "id" "user-file-form") $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa mkForm "/" [ pageOptionsFilePickerInput
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa , horizontalDivider "OR"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa , pageOptionsFileTextArea
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attrs [mkAttr "class" "ui relaxed grid", mkAttr "style" "margin-top: 1em"] $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ add_attr (mkAttr "class" "six wide column") $ unode "div" inputTypeDropDown
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "ten wide column right aligned") $ unode "div" submitButton
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksainputTypeDropDown :: Element
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen KuksainputTypeDropDown = singleSelectionDropDown
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa "Input Type of File or Text Field"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa "input-type"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa (Just "user-file-input-type")
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ( ("", "[Try to determine automatically]", [])
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa : map (\ inType -> (show inType, show inType, [])) plainInTypes
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen KuksasingleSelectionDropDown :: String -> String -> Maybe String -> [(String, String, [Attr])] -> Element
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen KuksasingleSelectionDropDown label inputName htmlIdM options = unode "div"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ add_attr (mkAttr "class" "ui sub header") $ unode "div" label
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , add_attrs ( mkAttr "name" inputName
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa : maybe [] (\ htmlId -> [mkAttr "id" htmlId]) htmlIdM
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ) $ unode "select" $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa map (\ (optionValue, optionLabel, attributes) ->
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa add_attrs (mkAttr "value" optionValue : attributes) $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa unode "option" optionLabel
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen KuksacheckboxElement :: String -> [Attr] -> Element
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen KuksacheckboxElement label attributes =
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa add_attr (mkAttr "class" "four wide column") $ unode "div" $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa add_attr (mkAttr "class" "ui checkbox") $ unode "div"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ([ mkAttr "type" "checkbox"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "tabindex" "0"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "class" "hidden"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ] ++ attributes) $ unode "input" ""
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , unode "label" label
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageOptionsFileTextArea :: Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksapageOptionsFileTextArea = add_attrs
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ mkAttr "cols" "68"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "rows" "22"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "name" "content"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "id" "user-input-text"
943f025155b53035a7212cf8f5979e3ec11d5978Eugen Kuksa , mkAttr "style" "font-family: monospace;"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ] $ unode "textarea" ""
5282dcff047a0541e424d77b46dc837093e99586Eugen KuksapageOptionsFilePickerInput :: Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksapageOptionsFilePickerInput = filePickerInputElement "file" "file" "Choose File..."
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksapageOptionsFormat :: String -> String -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksapageOptionsFormat delimiter path =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa let defaultFormat = "default"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa in dropDownElement "Output Format" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa aRef (if f == defaultFormat then "/" </> path else "/" </> path ++ delimiter ++ f) f
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ) (defaultFormat : displayTypes)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksafilePickerInputElement :: String -> String -> String -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksafilePickerInputElement idArgument nameArgument title =
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "field") $ unode "div" $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "ui fluid file input action") $ unode "div"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa [ add_attrs [mkAttr "type" "text", mkAttr "readonly" "true"] $ unode "input" ""
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attrs [ mkAttr "type" "file"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "id" idArgument
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "name" nameArgument
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "autocomplete" "off"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ] $ unode "input" ""
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "ui button") $ unode "div" title
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownElement :: String -> [Element] -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownElement title items =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui dropdown button") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ add_attr (mkAttr "class" "text") $ unode "div" title
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , dropDownSubMenu items
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksalinkButtonElement :: String -> String -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksalinkButtonElement address label =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui button") $ aRef address label
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlRow :: Element -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahtmlRow = add_attr (mkAttr "class" "row") . unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownToLevelsElement :: String -> [(Element, [Element])] -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownToLevelsElement title twoLeveledItems =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui dropdown button") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ add_attr (mkAttr "class" "text") $ unode "div" title
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "menu") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa map (\ (label, items) ->
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "item") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ( if null items
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa else [add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""]
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ++ [add_attr (mkAttr "class" "text") $ unode "div" label]
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ++ if null items then [] else [dropDownSubMenu items]
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ) twoLeveledItems
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownSubMenu :: [Element] -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksadropDownSubMenu items =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "menu") $ unode "div" $
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa map (add_attr (mkAttr "class" "item")) items
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageMoreExamples :: Bool -> [Element] -> Element
876c7f5a5366669437a05d63694bdece02bdd58eEugen KuksapageMoreExamples isOpen listElements =
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa let activeClass = if isOpen then "active " else "" in
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "ui ten wide column container left aligned") $ unode "div" $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "ui styled accordion") $ unode "div"
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa [ add_attr (mkAttr "class" (activeClass ++ "title")) $ unode "div"
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa [ add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa , unode "span" "More Examples"
876c7f5a5366669437a05d63694bdece02bdd58eEugen Kuksa , add_attr (mkAttr "class" (activeClass ++ "content")) $ unode "div" $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa add_attr (mkAttr "class" "transistion hidden") $ unode "div" $
5282dcff047a0541e424d77b46dc837093e99586Eugen Kuksa unode "ul" listElements
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahorizontalDivider :: String -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksahorizontalDivider label =
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attr (mkAttr "class" "ui horizontal divider") $ unode "div" label
986888e7f4d8ed681272a79c63f329ce8037063dcmaedermkResponse :: String -> Status -> String -> Response
986888e7f4d8ed681272a79c63f329ce8037063dcmaedermkResponse ty st = responseLBS st
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder (if null ty then [] else
853f27e556cb4e8c53f535df8e7b0ad665cf9bbcnotanartist#ifdef HTTPTYPES
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder [headerContentType $ B8.pack ty]
00d671cc654fe8d1571fa594bbebc9a2906ea880cmaeder [(hContentType, B8.pack ty)]
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder ) . BS.pack . encodeString
986888e7f4d8ed681272a79c63f329ce8037063dcmaedermkOkResponse :: String -> String -> Response
986888e7f4d8ed681272a79c63f329ce8037063dcmaedermkOkResponse ty = mkResponse ty status200
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederaddSess :: Cache -> Session -> IO Int
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederaddSess sessRef s = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let k = sessKey s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder atomicModifyIORef sessRef $ \ (m, lm) ->
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder ((IntMap.insert k s m, Map.insert (sessPath s) s lm), k)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedercleanUpCache :: Cache -> IO ()
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedercleanUpCache sessRef = do
cde581220edad4942fc8a012e3ba41607c280fc0Eugen Kuksa let mSize = 60
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder time <- getCurrentTime
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder atomicModifyIORef sessRef $ \ (m, lm) ->
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder if Map.size lm < mSize then ((m, lm), ()) else
bb20498381d61cb76b362f1164aa3d6cbde165aaEugen Kuksa let ss = cleanUpSessions time mSize m
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in ((IntMap.fromList $ map (\ s -> (sessKey s, s)) ss
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , Map.fromList $ map (\ s -> (sessPath s, s)) ss), ())
bb20498381d61cb76b362f1164aa3d6cbde165aaEugen Kuksa cleanUpSessions :: UTCTime -> Int -> IntMap.IntMap Session -> [Session]
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa cleanUpSessions time maxSize =
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa unifySessionLists . dropCleanables . sessionCleanableLists
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa sessionSort :: [Session] -> [Session]
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa sessionSort = sortBy (cmpSess time)
bb20498381d61cb76b362f1164aa3d6cbde165aaEugen Kuksa sessionCleanableLists :: IntMap.IntMap Session -> ([Session], [Session])
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa sessionCleanableLists =
bb20498381d61cb76b362f1164aa3d6cbde165aaEugen Kuksa partition sessCleanable . sessionSort . IntMap.elems
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa dropCleanables :: ([Session], [Session]) -> ([Session], [Session])
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa dropCleanables (cleanables, uncleanables) =
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa (drop (maxSize `div` 2) cleanables, uncleanables)
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa unifySessionLists :: ([Session], [Session]) -> [Session]
a8df18d7f9cbcecd3d6e54a61a2adec16dcb7914Eugen Kuksa unifySessionLists = sessionSort . uncurry (++)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedercmpSess :: UTCTime -> Session -> Session -> Ordering
eca54dc24f2c59cc51645115347a89ba2b40de36cmaedercmpSess curTime =
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let f s = let
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder l = lastAccess s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder b = sessStart s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder d2 = utctDay curTime
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder s2 = utctDayTime curTime
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder d1 = utctDay l
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder s1 = utctDayTime l
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder u = usage s
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in if u <= 1 && d1 == d2 && s2 > secondsToDiffTime 3600 + s1
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder then (u + 100, diffUTCTime l curTime)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder else (u, diffUTCTime b l)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder in on compare f
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederaddNewSess :: Cache -> Session -> IO Int
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederaddNewSess sessRef sess = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder cleanUpCache sessRef
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder k <- randomKey
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maeder let s = sess { sessKey = k }
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder addSess sessRef s
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen KuksanextSess :: LibEnv -> Session -> Cache -> Int -> IO Session
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen KuksanextSess newLib =
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa modifySessionAndCache "nextSess" (\ s -> s { sessLibEnv = newLib })
9dc3201888f22f8f78e83090cbf46b10b6109625Eugen KuksamakeSessCleanable :: Session -> Cache -> Int -> IO Session
9dc3201888f22f8f78e83090cbf46b10b6109625Eugen KuksamakeSessCleanable =
9dc3201888f22f8f78e83090cbf46b10b6109625Eugen Kuksa modifySessionAndCache "makeSessCleanable" (\ s -> s { sessCleanable = True })
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen KuksamodifySessionAndCache :: String -> (Session -> Session) -> Session -> Cache
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa -> Int -> IO Session
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen KuksamodifySessionAndCache errorMessage f sess sessRef k =
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa if k <= 0 then return sess else
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder atomicModifyIORef sessRef
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder (\ (m, lm) -> case IntMap.lookup k m of
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa Nothing -> error errorMessage
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa Just s -> let newSess = f s
3f5ac250048068c0a1c4ead95e50a1212588ecafEugen Kuksa in ((IntMap.insert k newSess m, lm), newSess))
986888e7f4d8ed681272a79c63f329ce8037063dcmaederppDGraph :: DGraph -> Maybe PrettyType -> ResultT IO (String, String)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian MaederppDGraph dg mt = let ga = globalAnnos dg in case optLibDefn dg of
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder Nothing -> fail "parsed LIB-DEFN not avaible"
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder let d = prettyLG logicGraph ld
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder latex = renderLatex Nothing $ toLatex ga d
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder in case mt of
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder Just pty -> case pty of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder PrettyXml -> return
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder (xmlC, ppTopElement $ xmlLibDefn logicGraph ga ld)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder PrettyAscii _ -> return (textC, renderText ga d ++ "\n")
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa PrettyHtml -> return (htmlC, renderHtml ga d)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder PrettyLatex _ -> return ("application/latex", latex)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder Nothing -> lift $ do
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder tmpDir <- getTemporaryDirectory
5a448e9be8c4482a978b174b744237757335140fChristian Maeder tmpFile <- writeTempFile (latexHeader ++ latex ++ latexFooter)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder mapM_ (\ s -> do
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder let sty = (</> "hetcasl.sty")
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ex <- doesFileExist f
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder when ex $ copyFile f $ sty tmpDir)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder , "/home/www.informatik.uni-bremen.de/cofi/hets-tmp" ]
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder withinDirectory tmpDir $ do
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (ex1, out1, err1) <- executeProcess "pdflatex" [tmpFile] ""
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (ex2, out2, err2) <- executeProcess "pdflatex" [tmpFile] ""
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder let pdfFile = replaceExtension tmpFile "pdf"
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder pdf <- doesFileExist pdfFile
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder if ex1 == ExitSuccess && ex2 == ExitSuccess && pdf then do
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder pdfHdl <- openBinaryFile pdfFile ReadMode
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder str <- hGetContents pdfHdl
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder when (length str < 0) $ putStrLn "pdf file too large"
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder hClose pdfHdl
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return (pdfC, str)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder else return (textC, "could not create pdf:\n"
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder ++ unlines [out1, err1, out2, err2])
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederincreaseUsage :: Cache -> Session -> ResultT IO (Session, Int)
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederincreaseUsage sessRef sess = do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder time <- lift getCurrentTime
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let s2 = sess { usage = usage sess + 1, lastAccess = time }
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder k <- lift $ addSess sessRef s2
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder return (s2, k)
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian MaedergetDGraph :: HetcatsOpts -> Cache -> DGQuery
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder -> ResultT IO (Session, Int)
016b8f06b709deef8c24b3d6c59f085857a166d4Christian MaedergetDGraph opts sessRef dgQ = do
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder (m, lm) <- lift $ readIORef sessRef
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder case dgQ of
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder NewDGQuery file cmdList -> do
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder let cl = mapMaybe (\ s -> find ((== s) . cmdlGlobCmd)
016b8f06b709deef8c24b3d6c59f085857a166d4Christian Maeder $ map fst allGlobLibAct) cmdList
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder mf <- lift $ getContentAndFileType opts file
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Left err -> fail err
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Right (_, mh, f, cont) -> case mh of
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Nothing -> fail $ "could determine checksum for: " ++ file
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just h -> let q = file : h : cmdList in
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just sess -> increaseUsage sessRef sess
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Nothing -> do
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder (ln, le1) <- if isDgXmlFile opts f cont
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder then readDGXmlR opts f Map.empty
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder else anaSourceFile logicGraph opts
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder { outputToStdout = False }
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Set.empty emptyLibEnv emptyDG file
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder le2 <- foldM (\ e c -> liftR
016b8f06b709deef8c24b3d6c59f085857a166d4Christian Maeder $ fromJust (lookup c allGlobLibAct) ln e) le1 cl
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder time <- lift getCurrentTime
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder let sess = Session
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder { sessLibEnv = le2
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , sessLibName = ln
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , sessPath = q
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , sessKey = 0 -- to be updated by addNewSess
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , sessStart = time
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder , lastAccess = time
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa , sessCleanable = False }
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder k <- lift $ addNewSess sessRef sess
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder return (sess, k)
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder DGQuery k _ -> case IntMap.lookup k m of
bf51e183eda8e66f16795b35ce9a62468974b8e3Christian Maeder Nothing -> fail "unknown development graph"
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Just sess -> increaseUsage sessRef sess
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaedergetSVG :: String -> String -> DGraph -> ResultT IO String
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaedergetSVG title url dg = do
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (exCode, out, err) <- lift $ executeProcess "dot" ["-Tsvg"]
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder $ dotGraph title False url dg
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht case exCode of
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht ExitSuccess -> liftR $ extractSVG dg out
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht _ -> fail err
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederenrichSVG :: DGraph -> Element -> Element
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederenrichSVG dg e = processSVG dg $ fromElement e
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederprocessSVG :: DGraph -> Cursor -> Element
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederprocessSVG dg c = case nextDF c of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Nothing -> case toTree (root c) of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder _ -> error "processSVG"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just c2 -> processSVG dg
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder $ modifyContent (addSVGAttribs dg) c2
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedernodeAttrib :: DGNodeLab -> String
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedernodeAttrib l = let nt = getRealDGNodeType l in
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (if isRefType nt then "Ref" else "")
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder ++ (if hasSenKind (const True) l then
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder (if isProvenNode nt then "P" else "Unp") ++ "roven"
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder ++ if isProvenCons nt then "Cons" else ""
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder else "LocallyEmpty")
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ (if isInternalSpec nt then "Internal" else "")
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ++ if labelHasHiding l then "HasIngoingHidingLink" else ""
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederedgeAttrib :: DGLinkLab -> String
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederedgeAttrib l = show (pretty $ dgl_type l) ++
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder if dglPending l then "IncompleteProofChain" else ""
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederaddSVGAttribs :: DGraph -> Content -> Content
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederaddSVGAttribs dg c = case c of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Elem e -> case getAttrVal "id" e of
be9d4ffdd00c0665f9c25a4a905b0a0bf0c90bbfChristian Maeder Just istr | isNat istr -> let i = read istr in
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder case getAttrVal "class" e of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just "node" -> case lab (dgBody dg) i of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just l -> Elem $ add_attr (mkAttr "type" $ nodeAttrib l) e
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just "edge" -> case getDGLinksById (EdgeId i) dg of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder [(_, _, l)] ->
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Elem $ add_attr (mkAttr "type" $ edgeAttrib l) e
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederextractSVG :: DGraph -> String -> Result String
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederextractSVG dg str = case parseXMLDoc str of
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Nothing -> fail "did not recognize svg element"
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just e -> return $ showTopElement $ enrichSVG dg e
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaedercmpFilePath :: FilePath -> FilePath -> Ordering
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaedercmpFilePath f1 f2 = case comparing hasTrailingPathSeparator f2 f1 of
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder EQ -> compare f1 f2
18b36f727b1d0be6ce1ec918de15f5c17da7b53fcmaedergetHetsResponse :: HetcatsOpts -> [W.FileInfo BS.ByteString]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -> Cache -> [String] -> [QueryPair] -> WebResponse
8723ec450f2e7a024230467c0c28a3f154905483cmaedergetHetsResponse opts updates sessRef pathBits query respond = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder Result ds ms <- liftIO $ runResultT $ case anaUri pathBits query
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder $ updateS : globalCommands of
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht Left err -> fail err
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Right q -> getHetsResult opts updates sessRef q Nothing OldWebAPI
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa proofFormatterOptions
8723ec450f2e7a024230467c0c28a3f154905483cmaeder respond $ case ms of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just (t, s) | not $ hasErrors ds -> mkOkResponse t s
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder _ -> mkResponse textC status422 $ showRelDiags 1 ds
18b36f727b1d0be6ce1ec918de15f5c17da7b53fcmaedergetHetsResult :: HetcatsOpts -> [W.FileInfo BS.ByteString]
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa -> Cache -> Query.Query -> Maybe String -> UsedAPI -> ProofFormatterOptions
4ded733c298c9fd95db25858b897da482f4ab3e7Eugen Kuksa -> ResultT IO (String, String)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksagetHetsResult opts updates sessRef (Query dgQ qk) format_ api pfOptions = do
5606c84ebef3de545602e215bbd87931334d48f0mcodescu let getCom n = let ncoms = filter (\(Comorphism cid) -> language_name cid == n) comorphismList
5606c84ebef3de545602e215bbd87931334d48f0mcodescu in case ncoms of
5606c84ebef3de545602e215bbd87931334d48f0mcodescu [] -> error $ "comorphism not found:" ++ n
5606c84ebef3de545602e215bbd87931334d48f0mcodescu _ -> error $ "more than one comorphism found for:" ++ n
ace3ac8a6ba9031ea228823af98d12f95c56785fEugen Kuksa sk@(sess', k) <- getDGraph opts sessRef dgQ
ace3ac8a6ba9031ea228823af98d12f95c56785fEugen Kuksa sess <- lift $ makeSessCleanable sess' sessRef k
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian Maeder let libEnv = sessLibEnv sess
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (ln, dg) <- maybe (fail "unknown development graph") return
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht $ sessGraph dgQ sess
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let title = libToFileName ln
1defc008da0fae281b776ffe464e2fef549804b5cmaeder let svg = getSVG title ('/' : show k) dg
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa DisplayQuery ms -> case format_ `mplus` ms of
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa Just "db" -> do
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa result <- liftIO $ Control.Exception.catch
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa return (jsonC, "{\"savedToDatabase\": true}")
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa (\ exception ->
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa return (jsonC, "{\"savedToDatabase\": false, \"error\": " ++ show (exception :: SomeException) ++ "}")
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa liftR $ return result
103848575cd92efdb3d4dc9809c16254d7415c2ecmaeder Just "svg" -> fmap (\ s -> (svgC, s)) svg
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just "xml" -> liftR $ return (xmlC, ppTopElement
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder $ ToXml.dGraph opts libEnv ln dg)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just "json" -> liftR $ return (jsonC, ppJson
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder $ ToJson.dGraph opts libEnv ln dg)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just "dot" -> liftR $ return
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder (dotC, dotGraph title False title dg)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just "symbols" -> liftR $ return (xmlC, ppTopElement
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Just "session" -> liftR $ return (htmlC, ppElement
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder $ aRef (mkPath sess ln k) $ show k)
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder Just str | elem str ppList
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder -> ppDGraph dg $ lookup str $ zip ppList prettyList
1defc008da0fae281b776ffe464e2fef549804b5cmaeder _ -> sessAns ln svg sk
5606c84ebef3de545602e215bbd87931334d48f0mcodescu -- compose the comorphisms passed in translation
5606c84ebef3de545602e215bbd87931334d48f0mcodescu let coms = map getCom $ splitOn ',' path
5606c84ebef3de545602e215bbd87931334d48f0mcodescu com <- foldM compComorphism (head coms) $ tail coms
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu dg' <- liftR $ dg_translation libEnv ln dg com
5606c84ebef3de545602e215bbd87931334d48f0mcodescu liftR $ return (xmlC, ppTopElement
5606c84ebef3de545602e215bbd87931334d48f0mcodescu $ ToXml.dGraph opts libEnv ln dg')
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa GlProvers mp mt -> do
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa availableProvers <- liftIO $ getFullProverList mp mt dg
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen Kuksa return $ case api of
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa OldWebAPI -> (xmlC, formatProvers mp $
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa proversToStringAux availableProvers)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa RESTfulAPI -> OProvers.formatProvers format_ mp availableProvers
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa GlTranslations -> do
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa availableComorphisms <- liftIO $ getFullComorphList dg
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa return $ case api of
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa OldWebAPI ->
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa (xmlC, formatComorphs availableComorphisms)
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa RESTfulAPI ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa formatTranslations format_ availableComorphisms
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht GlShowProverWindow prOrCons -> showAutoProofWindow dg k prOrCons
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlAutoProveREST proverMode reasoningParameters -> case api of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa RESTfulAPI -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (newLib, nodesAndProofResults) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasonREST opts libEnv ln dg proverMode (queryLib dgQ) reasoningParameters
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa if all (null . snd) nodesAndProofResults
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa then return (textC, "nothing to prove")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa lift $ nextSess newLib sess sessRef k
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa processProofResult format_ pfOptions nodesAndProofResults
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa _ -> fail ("The GlAutoProveREST path is only "
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ++ "available in the REST interface.")
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa GlAutoProve (ProveCmd prOrCons incl mp mt tl nds xForm axioms) -> do
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (newLib, nodesAndProofResults) <-
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa proveMultiNodes prOrCons libEnv ln dg incl mp mt tl nds axioms
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa if all (null . snd) nodesAndProofResults
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa then return (textC, "nothing to prove")
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen Kuksa lift $ nextSess newLib sess sessRef k
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa OldWebAPI -> let
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa sens = foldr (\ (dgNodeName, proofResults) res ->
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa formatResultsAux xForm prOrCons dgNodeName proofResults
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa ) [] nodesAndProofResults
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in return (htmlC, formatResultsMultiple xForm k sens prOrCons)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa RESTfulAPI ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa processProofResult format_ pfOptions nodesAndProofResults
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder GlobCmdQuery s ->
b0bf54186358372d2be6a95e36ed3ef5fd64b7a3Christian Maeder case find ((s ==) . cmdlGlobCmd . fst) allGlobLibAct of
e4a035578fa9d1911eee097e2ed9a998c90c7805Christian Maeder Nothing -> if s == updateS then
7c661ba558707feaa5d8a299365c2191e1afabb2Christian Maeder case filter ((== ".xupdate") . takeExtension . B8.unpack
7c661ba558707feaa5d8a299365c2191e1afabb2Christian Maeder . fileName) updates of
3abf8a8f697c113233027f0c865ed57deb274542Christian Maeder let str = BS.unpack $ fileContent ch
8ca6b0820806f62042d84a1fff11599db55591c4Christian Maeder (newLn, newLib) <- dgXUpdate opts str libEnv ln dg
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen Kuksa newSess <- lift $ nextSess newLib sess sessRef k
1defc008da0fae281b776ffe464e2fef549804b5cmaeder sessAns newLn svg (newSess, k)
1defc008da0fae281b776ffe464e2fef549804b5cmaeder [] -> sessAns ln svg sk
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Just (_, act) -> do
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian Maeder newLib <- liftR $ act ln libEnv
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen Kuksa newSess <- lift $ nextSess newLib sess sessRef k
23ee432f8fe96e07f2523ca7c4bda9bcce1ea6f0Simon Ulbricht -- calculate updated SVG-view from modified development graph
1defc008da0fae281b776ffe464e2fef549804b5cmaeder let newSvg = getSVG title ('/' : show k)
1defc008da0fae281b776ffe464e2fef549804b5cmaeder $ lookupDGraph ln newLib
1defc008da0fae281b776ffe464e2fef549804b5cmaeder sessAns ln newSvg (newSess, k)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder NodeQuery ein nc -> do
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder nl@(i, dgnode) <- case ein of
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Right n -> case lookupNodeByName n dg of
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder p : _ -> return p
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder [] -> fail $ "no node name: " ++ n
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Left i -> case lab (dgBody dg) i of
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Nothing -> fail $ "no node id: " ++ show i
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Just dgnode -> return (i, dgnode)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder let fstLine = (if isDGRef dgnode then ("reference " ++) else
43d8d7472d3a0a78d9a2c85122815a81deb8689aChristian Maeder if isInternalNode dgnode then ("internal " ++) else id)
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa "Node " ++ getDGNodeName dgnode ++ " (#" ++ show i ++ ")\n"
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder ins = getImportNames dg i
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder showN d = showGlobalDoc (globalAnnos dg) d "\n"
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder NcCmd cmd | elem cmd [Query.Node, Info, Symbols]
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder -> case cmd of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder Symbols -> return (xmlC, ppTopElement
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ showSymbols opts ins (globalAnnos dg) dgnode)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder _ -> return (textC, fstLine ++ showN dgnode)
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder _ -> case maybeResult $ getGlobalTheory dgnode of
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Nothing -> fail $
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder "cannot compute global theory of:\n" ++ fstLine
5727dbcb926ede2e7b05f43685476ce656ce01e4Christian Maeder Just gTh -> let subL = sublogicOfTh gTh in case nc of
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa ProveNode (ProveCmd pm incl mp mt tl thms xForm axioms) ->
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder GlProofs -> do
e2374b99721dab596695fda64b96aecc5ecf23c9Eugen Kuksa (newLib, proofResults) <- proveNode libEnv ln dg nl
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa gTh subL incl mp mt tl thms axioms
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa if null proofResults
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa then return (textC, "nothing to prove")
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen Kuksa lift $ nextSess newLib sess sessRef k
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa OldWebAPI -> return (htmlC,
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa formatResults xForm k i .
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa add_attr (mkAttr "class" "results") $
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa unode "div" $ formatGoals True proofResults)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa RESTfulAPI -> processProofResult format_ pfOptions
2ed0ce5565323b3a233d9258b0ff63dfa4a8e8e1Eugen Kuksa [(getDGNodeName dgnode, proofResults)]
5a89ec196dfd3e342f6d4ef3a318bc9992190bbaChristian Maeder GlConsistency -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (newLib, [(_, res, txt, _, _, _, _)]) <-
d4d3caef3878e583180d50f670957f1406d1effbcmaeder consNode libEnv ln dg nl subL incl mp mt tl
8846af9dfc3d74f8b1d2566e81c9e5aa25647b99Eugen Kuksa lift $ nextSess newLib sess sessRef k
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return (xmlC, ppTopElement $ formatConsNode res txt)
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder _ -> case nc of
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu NcCmd Query.Theory -> case api of
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu OldWebAPI -> lift $ fmap (\ t -> (htmlC, t))
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu $ showGlobalTh dg i gTh k fstLine
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu RESTfulAPI -> lift $ fmap (\ t -> (xmlC, t))
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu $ showNodeXml opts (globalAnnos dg) libEnv dg i
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu NcCmd (Query.Translate x) -> do
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu -- compose the comorphisms passed in translation
5606c84ebef3de545602e215bbd87931334d48f0mcodescu let coms = map getCom $ splitOn ',' x
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu com <- foldM compComorphism (head coms) $ tail coms
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu -- translate the theory of i along com
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu gTh1 <- liftR $ mapG_theory com gTh
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu -- insert the translation of i in dg
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu let n1 = getNewNodeDG dg
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu labN1 = newInfoNodeLab
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu emptyNodeName
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu (newNodeInfo DGBasic) -- to be corrected
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu dg1 = insLNodeDG (n1, labN1) dg
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu gmor <- liftR $ gEmbedComorphism com $ signOf $ dgn_theory dgnode
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu -- add a link from i to n1 labeled with (com, id)
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu let (_, dg2) = insLEdgeDG
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu (i, n1, globDefLink gmor SeeSource) -- origin to be corrected
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu -- show the theory of n1 in xml format
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu lift $ fmap (\ t -> (xmlC, t)) $ showNodeXml opts (globalAnnos dg2) libEnv dg2 n1
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa NcProvers mp mt -> do
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa availableProvers <- liftIO $ getProverList mp mt subL
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa return $ case api of
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa OldWebAPI -> (xmlC, formatProvers mp $
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa proversToStringAux availableProvers)
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa RESTfulAPI ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa OProvers.formatProvers format_ mp availableProvers
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa NcTranslations mp -> do
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen Kuksa availableComorphisms <- liftIO $ getComorphs mp subL
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa return $ case api of
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa OldWebAPI ->
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa (xmlC, formatComorphs availableComorphisms)
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa RESTfulAPI ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa formatTranslations format_ availableComorphisms
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder EdgeQuery i _ ->
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder case getDGLinksById (EdgeId i) dg of
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder [e@(_, _, l)] ->
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder return (textC, showLEdge e ++ "\n" ++ showDoc l "")
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder [] -> fail $ "no edge found with id: " ++ show i
b532acc045cf5e26beb0691acc136d11188cce87Christian Maeder _ -> fail $ "multiple edges found with id: " ++ show i
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaprocessProofResult :: Maybe String
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ProofFormatterOptions
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> [(String, [ProofResult])]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ResultT IO (String, String)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaprocessProofResult format_ options nodesAndProofResults =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa if format_ == Just "db"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa then return (jsonC, "{\"savedToDatabase\": true}")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa else return $ formatProofs format_ options nodesAndProofResults
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaformatGoals :: Bool -> [ProofResult] -> [Element]
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaformatGoals includeDetails =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa map (\ (n, e, d, _, _, mps, _) -> add_attr (mkAttr "class" "results-goal") $ unode "div"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa ([ unode "h3" ("Results for " ++ n ++ " (" ++ e ++ ")") ]
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa ++ [add_attr (mkAttr "class" "results-details") $ unode "div" d | includeDetails]
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa ++ case mps of
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa Nothing -> []
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa Just ps -> formatProofStatus ps))
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatProofStatus :: ProofStatus G_proof_tree -> [Element]
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatProofStatus ps =
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa [ unode "h5" "Used Prover"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "usedProver") $ unode "p" $ usedProver ps
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa -- `read` makes this type-unsafe
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , unode "h5" "Tactic Script"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "tacticScript") $ unode "p" $ formatTacticScript $ read $
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (\ (TacticScript ts) -> ts) $ tacticScript ps
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , unode "h5" "Proof Tree"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "proofTree") $ unode "div" $ show $ proofTree ps
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , unode "h5" "Used Time"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "usedTime") $ unode "div" $ formatUsedTime $ usedTime ps
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , unode "h5" "Used Axioms"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "usedAxioms") $ unode "div" $ formatUsedAxioms $ usedAxioms ps
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , unode "h5" "Prover Output"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , add_attr (mkAttr "class" "proverOutput") $ unode "div" $ formatProverOutput $ proofLines ps
682260563efe78f762d2d9db032a161ee0088851Eugen KuksaformatProverOutput :: [String] -> Element
682260563efe78f762d2d9db032a161ee0088851Eugen KuksaformatProverOutput = unode "pre" . unlines
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatTacticScript :: ATPTacticScript -> [Element]
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatTacticScript ts =
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa [ unode "timeLimit" $ show $ tsTimeLimit ts
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa , unode "extraOpts" $ map (unode "option") $ tsExtraOpts ts
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatUsedTime :: TimeOfDay -> [Element]
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatUsedTime tod =
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa [ unode "seconds" $ init $ show $ timeOfDayToTime tod
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa , unode "components"
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa [ unode "hours" $ show $ todHour tod
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa , unode "minutes" $ show $ todMin tod
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa , unode "seconds" $ show $ todSec tod
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaformatUsedAxioms :: [String] -> [Element]
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen KuksaformatUsedAxioms = map (unode "axiom")
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederformatConsNode :: String -> String -> Element
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederformatConsNode res txt = add_attr (mkAttr "state" res) $ unode "result" txt
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederformatResultsMultiple :: Bool -> Int -> [Element] -> ProverMode -> String
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederformatResultsMultiple xForm sessId rs prOrCons =
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder if xForm then ppTopElement $ unode "Results" rs else let
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht goBack1 = case prOrCons of
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht GlConsistency -> aRef ('/' : show sessId ++ "?consistency") "return"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht GlProofs -> aRef ('/' : show sessId ++ "?autoproof") "return"
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht goBack2 = aRef ('/' : show sessId) "return to DGraph"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa in htmlPage "Results" []
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa [ htmlRow $ unode "h1" "Results"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , htmlRow $ unode "div" [goBack1, goBack2]
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , htmlRow $ unode "div" $
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa foldr (\ el r -> unode "h4" (qName $ elName el) : el : r) [] rs
319f8219a74a41859b9d1991817644549ab43d61Simon Ulbricht-- | display results of proving session (single node)
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian MaederformatResults :: Bool -> Int -> Int -> Element -> String
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian MaederformatResults xForm sessId i rs =
1cc76b3190979d475bc8f2c1ffe627d9abf2410bChristian Maeder if xForm || sessId <= 0 then ppTopElement rs else let
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa goBack1 = linkButtonElement ('/' : show sessId ++ "?theory=" ++ show i) "return to Theory"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa goBack2 = linkButtonElement ('/' : show sessId) "return to DGraph"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa in htmlPage "Results" []
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa [ htmlRow $ unode "h1" "Results"
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , htmlRow $ unode "div" [goBack1, goBack2]
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa , htmlRow $ add_attr (mkAttr "class" "ui relaxed grid raised segment container left aligned") $ unode "div" rs
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian MaedershowBool :: Bool -> String
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian MaedershowBool = map toLower . show
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescushowNodeXml :: HetcatsOpts -> GlobalAnnos -> LibEnv -> DGraph -> Int -> IO String
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescushowNodeXml opts ga lenv dg n = let
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu lNodeN = lab (dgBody dg) n
dab141168df1b5ae84852d862b3aefc8782cfc7emcodescu in case lNodeN of
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Just lNode -> return $ ppTopElement $ ToXml.lnode opts ga lenv (n,lNode)
c24f7998fe7dfca4277f83076a119aabfe6186a0mcodescu Nothing -> error $ "no node for " ++ show n
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht{- | displays the global theory for a node with the option to prove theorems
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbrichtand select proving options -}
cddd87cd39be9d031348ef95051c4d14067e1646cmaedershowGlobalTh :: DGraph -> Int -> G_theory -> Int -> String -> IO String
92b34c379207fb8752258be174cb8ef4162dc865Simon UlbrichtshowGlobalTh dg i gTh sessId fstLine = case simplifyTh gTh of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder sGTh@(G_theory lid _ (ExtSign sig _) _ thsens _) -> let
993e01fc242fa58d3dcf1b3272cd411726817eeeSimon Ulbricht ga = globalAnnos dg
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht -- links to translations and provers xml view
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa transBt = linkButtonElement ('/' : show sessId ++ "?translations=" ++ show i)
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht "translations"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa prvsBt = linkButtonElement ('/' : show sessId ++ "?provers=" ++ show i) "provers"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa headr = htmlRow $ unode "h3" fstLine
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht thShow = renderHtml ga $ vcat $ map (print_named lid) $ toNamedList thsens
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht sbShow = renderHtml ga $ pretty sig
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht in case getThGoals sGTh of
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- show simple view if no goals are found
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [] -> return $ htmlPage fstLine ""
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , htmlRow $ unode "h4" "Theory"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ] $ "<pre>\n" ++ sbShow ++ "\n<br />" ++ thShow ++ "\n</pre>\n"
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- else create proving functionality
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- create list of theorems, selectable for proving
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa map (\ (nm, bp) ->
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa let gSt = maybe GOpen basicProofToGStatus bp
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa in checkboxElement (nm ++ " (" ++ showSimple gSt ++ ")")
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "name" $ escStr nm
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "unproven" $ showBool $ elem gSt [GOpen, GTimeout]
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht -- select unproven, all or none theorems by button
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (btUnpr, btAll, btNone, jvScr1) = showSelectionButtons True
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- create prove button and prover/comorphism selection
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (prSl, cmrSl, jvScr2) <- showProverSelection GlProofs [sublogicOfTh gTh]
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let (prBt, timeout) = showProveButton True
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht -- hidden param field
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder hidStr = add_attrs [ mkAttr "name" "prove"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder , mkAttr "type" "hidden", mkAttr "style" "display:none;"
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder , mkAttr "value" $ show i ] inputNode
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht -- combine elements within a form
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa add_attrs [ mkAttr "name" "thmSel", mkAttr "method" "get"]
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa . add_attr (mkAttr "class" "ui form") $ unode "form"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa $ add_attr (mkAttr "class" "ui relaxed grid container left aligned") $ unode "div"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa $ [ add_attr (mkAttr "class" "row") $ unode "div" [hidStr, prSl, cmrSl]
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div" [btUnpr, btAll, btNone, timeout]
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div" thmSl
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div" prBt
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht -- save dg and return to svg-view
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa goBack = linkButtonElement ('/' : show sessId) "Return to DGraph"
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa return $ htmlPage fstLine (jvScr1 ++ jvScr2)
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , htmlRow $ unode "h4" "Theorems"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , htmlRow $ unode "h4" "Theory"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ] $ "<pre>\n" ++ sbShow ++ "\n<br />" ++ thShow ++ "\n</pre>\n"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht-- | show window of the autoproof function
986888e7f4d8ed681272a79c63f329ce8037063dcmaedershowAutoProofWindow :: DGraph -> Int -> ProverMode
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder -> ResultT IO (String, String)
465c6b72e8e480969b5f08658e394992bcc08bfcSimon UlbrichtshowAutoProofWindow dg sessId prOrCons = let
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht dgnodes = labNodesDG dg
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht -- some parameters need to be different for consistency and autoproof mode
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder (prMethod, isProver, title, nodeSel) = case prOrCons of
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder GlProofs -> ("proof", True, "automatic proofs"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , map (\ fn -> add_attrs [ mkAttr "type" "checkbox"
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder , mkAttr "unproven" $ showBool $ not $ allProved fn
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , mkAttr "name" $ escStr $ name fn ]
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht $ unode "input" $ showHtml fn) $ initFNodes dgnodes)
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht -- TODO sort out nodes with no sentences!
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder GlConsistency -> ("cons", False, "consistency checker"
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder , map (\ (_, dgn) ->
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht let cstat = getConsistencyOf dgn
a2af8492313011f78cbedbfd302dc12150b9f7efChristian Maeder nm = getDGNodeName dgn in add_attrs [ mkAttr "type" "checkbox"
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder , mkAttr "unproven" $ showBool $ sType cstat == CSUnchecked
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , mkAttr "name" nm]
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht $ unode "input" (cStatusToPrefix cstat ++ nm)) dgnodes)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht -- generate param field for the query string, invisible to the user
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht hidStr = add_attrs [ mkAttr "name" "autoproof"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , mkAttr "type" "hidden", mkAttr "style" "display:none;"
3420e25193b07f6213b0c11c31c9baf799c9c9e2Simon Ulbricht , mkAttr "value" prMethod ] inputNode
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht -- select unproven, all or no nodes by button
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder (btUnpr, btAll, btNone, jvScr1) = showSelectionButtons isProver
66e5f6ab072171b6fd02ccc20846386773354391Christian Maeder (prBt, timeout) = showProveButton isProver
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht include = add_attrs [ mkAttr "type" "checkbox", mkAttr "checked" "true"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , mkAttr "name" "includetheorems"] $ unode "input" "include Theorems"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht goBack = aRef ('/' : show sessId) "return to DGraph"
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht (jvScr2, nodeMenu) <- case dgnodes of
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht -- return simple feedback if no nodes are present
439fdeeb1323b17084fad1b7fe619e49c270999fSimon Ulbricht [] -> return ("", plain "nothing to prove (graph has no nodes)")
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht (_, nd) : _ -> case maybeResult $ getGlobalTheory nd of
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht Nothing -> fail $ "cannot compute global theory of:\n" ++ show nd
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder Just gTh -> do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let br = unode "br " ()
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (prSel, cmSel, jvSc) <- lift $ showProverSelection prOrCons
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht [sublogicOfTh gTh]
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder return (jvSc, add_attrs
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder [ mkAttr "name" "nodeSel", mkAttr "method" "get" ]
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder . unode "form" $
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder [ hidStr, prSel, cmSel, br, btAll, btNone, btUnpr, timeout
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder , include ] ++ intersperse br (prBt : nodeSel))
8d11785bab797efec9c78e11c9c07e7a32b35e21Eugen Kuksa return (htmlC, htmlPage title (jvScr1 ++ jvScr2)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ goBack, plain " ", nodeMenu ] "")
66e5f6ab072171b6fd02ccc20846386773354391Christian MaedershowProveButton :: Bool -> (Element, Element)
66e5f6ab072171b6fd02ccc20846386773354391Christian MaedershowProveButton isProver = (prBt, timeout) where
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa prBt = add_attrs
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "type" "submit"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "class" "ui button"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "value" $ if isProver then "Prove" else "Check"
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- create timeout field
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa timeout = add_attr (mkAttr "class" "three wide field") $ unode "div"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ unode "label" "Timeout (Sec/Goal)"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "type" "text"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "name" "timeout"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "placeholder" "Timeout (Sec/Goal)"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "value" "1"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ] $ unode "input" ""
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht-- | select unproven, all or none theorems by button
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian MaedershowSelectionButtons :: Bool -> (Element, Element, Element, String)
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian MaedershowSelectionButtons isProver = (selUnPr, selAll, selNone, jvScr)
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder where prChoice = if isProver then "SPASS" else "darwin"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa selUnPr = add_attrs
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "type" "button"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "class" "ui button"
f59ad2f2dc308e549d70f0de4c0054df3b2bbfcaChristian Maeder , mkAttr "value" $ if isProver then "Unproven" else "Unchecked"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "onClick" "chkUnproven()"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa selAll = add_attrs
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "type" "button", mkAttr "value" "All"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "class" "ui button"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "onClick" "chkAll(true)"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa selNone = add_attrs
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa [ mkAttr "type" "button", mkAttr "value" "None"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "class" "ui button"
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa , mkAttr "onClick" "chkAll(false)"
2b1abe6d680bc23b703f7ffbf6d214be15aa9f1fSimon Ulbricht -- javascript features
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht jvScr = unlines
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht -- select unproven goals by button
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht [ "\nfunction chkUnproven() {"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " var e = document.forms[0].elements;"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " for (i = 0; i < e.length; i++) {"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , " if( e[i].type == 'checkbox'"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , " && e[i].name != 'includetheorems' )"
f8b5384f117f1eb77f87b9bc982513109b3c2d56Christian Maeder , " e[i].checked = e[i].getAttribute('unproven') == 'true';"
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht -- select or deselect all theorems by button
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht , "}\nfunction chkAll(b) {"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " var e = document.forms[0].elements;"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " for (i = 0; i < e.length; i++) {"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , " if( e[i].type == 'checkbox'"
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht , " && e[i].name != 'includetheorems' ) e[i].checked = b;"
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht -- autoselect SPASS if possible
d5a6311a0badccb57c915d3f7d0657615338e12cSimon Ulbricht , "}\nwindow.onload = function() {"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " prSel = document.forms[0].elements.namedItem('prover');"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " prs = prSel.getElementsByTagName('option');"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " for ( i=0; i<prs.length; i++ ) {"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , " if( prs[i].value == '" ++ prChoice ++ "' ) {"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " prs[i].selected = 'selected';"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , " updCmSel('" ++ prChoice ++ "');"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht -- if SPASS unable, select first one in list
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " prs[0].selected = 'selected';"
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , " updCmSel( prs[0].value );"
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht-- | create prover and comorphism menu and combine them using javascript
c4afbc0e8d0896b0e7efec66a9f15e3ca16f2233Simon UlbrichtshowProverSelection :: ProverMode -> [G_sublogics]
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> IO (Element, Element, String)
cddd87cd39be9d031348ef95051c4d14067e1646cmaedershowProverSelection prOrCons subLs = do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let jvScr = unlines
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht -- the chosen prover is passed as param
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht [ "\nfunction updCmSel(pr) {"
9d46cd96eb5f63953a7608635e9cc2d22506e5d7Simon Ulbricht , " var cmrSl = document.forms[0].elements.namedItem('translation');"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht -- then, all selectable comorphisms are gathered and iterated
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " var opts = cmrSl.getElementsByTagName('option');"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht -- try to keep current comorph-selection
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " var selAccept = false;"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " for( var i = opts.length-1; i >= 0; i-- ) {"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " var cmr = opts.item( i );"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht -- the list of supported provers is extracted
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " var prs = cmr.getAttribute('4prover').split(';');"
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht , " var pFit = false;"
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht , " for( var j = 0; ! pFit && j < prs.length; j++ ) {"
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht , " pFit = prs[j] == pr;"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht -- if prover is supported, remove disabled attribute
679aeef257123e594df0769b43ac12fe98854a54Simon Ulbricht , " if( pFit ) {"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " cmr.removeAttribute('disabled');"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " selAccept = selAccept || cmr.selected;"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht -- else create and append a disabled attribute
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " } else {"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " var ds = document.createAttribute('disabled');"
98fb0b2bb596c5af3ef20eb9dc063871cc03ee03Simon Ulbricht , " ds.value = 'disabled';"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht -- check if selected comorphism fits, and select fst. in list otherwise
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " if( ! selAccept ) {"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " for( i = 0; i < opts.length; i++ ) {"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " if( ! opts.item(i).disabled ) {"
98530a5430d24712d3d75213f8e21b6b0421770eSimon Ulbricht , " opts.item(i).selected = 'selected';"
d4d3caef3878e583180d50f670957f1406d1effbcmaeder pcs <- mapM (liftM proversToStringAux . (case prOrCons of
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder GlProofs -> getProversAux
d4d3caef3878e583180d50f670957f1406d1effbcmaeder GlConsistency -> getConsCheckersAux) Nothing) subLs
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let allPrCm = nub $ concat pcs
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht -- create prover selection (drop-down)
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa prs = add_attr (mkAttr "class" "eight wide column") $ unode "div" $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa singleSelectionDropDown "Prover" "prover" Nothing $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa (p, p, [mkAttr "onClick" $ "updCmSel('" ++ p ++ "')"])
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa ) $ showProversOnly allPrCm
0f3c9fa687758f7282fd74539600c580ac165594Simon Ulbricht -- create comorphism selection (drop-down)
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa cmrs = add_attr (mkAttr "class" "eight wide column") $ unode "div" $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa singleSelectionDropDown "Translation" "translation" Nothing $
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa map (\ (cm, ps) -> let c = showComorph cm in
7448a23dbbf0306a484e1caf5a05f7dff0210856Eugen Kuksa (c, c, [mkAttr "4prover" $ intercalate ";" ps])
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder return (prs, cmrs, jvScr)
734a5ebd38032798f0ab908e2d52862c71b2c127Simon UlbrichtshowHtml :: FNode -> String
41a3368af0eaad78c660477e7ded53b2ba85a275Christian MaedershowHtml fn = name fn ++ " " ++ goalsToPrefix (toGtkGoals fn)
cddd87cd39be9d031348ef95051c4d14067e1646cmaedergetAllAutomaticProvers :: G_sublogics -> IO [(G_prover, AnyComorphism)]
cddd87cd39be9d031348ef95051c4d14067e1646cmaedergetAllAutomaticProvers subL =
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder getUsableProvers ProveCMDLautomatic subL logicGraph
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian MaederfilterByProver :: Maybe String -> [(G_prover, AnyComorphism)]
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder -> [(G_prover, AnyComorphism)]
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian MaederfilterByProver mp = case mp of
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder Nothing -> id
26f0691ae6929941ee21ca3d33732a0ce45a8079cmaeder Just p -> filter ((== p) . mkNiceProverName . getProverName . fst)
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian MaederfilterByComorph :: Maybe String -> [(a, AnyComorphism)]
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder -> [(a, AnyComorphism)]
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian MaederfilterByComorph mt = case mt of
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder Nothing -> id
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder Just c -> filter ((== c) . showComorph . snd)
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian MaedergetProverAndComorph :: Maybe String -> Maybe String -> G_sublogics
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> IO [(G_prover, AnyComorphism)]
cddd87cd39be9d031348ef95051c4d14067e1646cmaedergetProverAndComorph mp mc subL = do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ps <- getFilteredProvers mc subL
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let spps = case filterByProver (Just "SPASS") ps of
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder return $ case mp of
d2111c9d2eb254b2a5ab71b27a6a07f1e353aec7Christian Maeder Nothing -> spps
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder _ -> filterByProver mp ps
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen KuksagetProverList :: ProverMode -> Maybe String -> G_sublogics
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa -> IO [(AnyComorphism, [ProverOrConsChecker])]
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen KuksagetProverList mp mt subL = case mp of
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen Kuksa GlProofs -> getProversAux mt subL
96074fcf7dc0751450e132610b9bb31207ce0cd2Eugen Kuksa GlConsistency -> getConsCheckersAux mt subL
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen KuksagetFullProverList :: ProverMode -> Maybe String -> DGraph
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa -> IO [(AnyComorphism, [ProverOrConsChecker])]
5c89bca8b187e75ff87be1afe964c1aeba8a7725Eugen KuksagetFullProverList mp mt = foldM
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (\ ls (_, nd) -> maybe (return ls) (fmap (++ ls) . case mp of
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder GlProofs -> getProversAux mt
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder GlConsistency -> getConsCheckersAux mt
eb24ac2f4701c8e012acf1bb8f686baa5422bb5aChristian Maeder . sublogicOfTh)
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder $ maybeResult $ getGlobalTheory nd) [] . labNodesDG
f56cdf11927c31495bae642a9eb383212c90ba61Christian MaedergroupOnSnd :: Eq b => (a -> c) -> [(a, b)] -> [(b, [c])]
f56cdf11927c31495bae642a9eb383212c90ba61Christian MaedergroupOnSnd f =
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder map (\ l@((_, b) : _) -> (b, map (f . fst) l)) . groupBy (on (==) snd)
d102a920578426a89411cc8dabe47d7a881eab8fEugen KuksaproversToStringAux :: [(AnyComorphism, [ProverOrConsChecker])]
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa -> [(AnyComorphism, [String])]
ceb5bd32f163b29b1cbea577334bc869c07add04Eugen KuksaproversToStringAux = map (\ (x, ps) ->
ceb5bd32f163b29b1cbea577334bc869c07add04Eugen Kuksa (x, map (mkNiceProverName . internalProverName) ps))
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder{- | gather provers and comorphisms and resort them to
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder(comorhism, supported provers) while not changing orig comorphism order -}
d102a920578426a89411cc8dabe47d7a881eab8fEugen KuksagetProversAux :: Maybe String -> G_sublogics
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa -> IO [(AnyComorphism, [ProverOrConsChecker])]
d102a920578426a89411cc8dabe47d7a881eab8fEugen KuksagetProversAux mt x =
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder fmap (groupOnSnd AbsState.Prover) $ getFilteredProvers mt x
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian MaedergetFilteredProvers :: Maybe String -> G_sublogics
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> IO [(G_prover, AnyComorphism)]
cddd87cd39be9d031348ef95051c4d14067e1646cmaedergetFilteredProvers mt = fmap (filterByComorph mt) . getAllAutomaticProvers
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian MaederformatProvers :: ProverMode -> [(AnyComorphism, [String])] -> String
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian MaederformatProvers pm = let
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder tag = case pm of
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder GlProofs -> "prover"
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder GlConsistency -> "consistency-checker"
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian Maeder in ppTopElement . unode (tag ++ "s") . map (unode tag)
10eaa95e20c860acbfbecd6cf07e3ae0bf7b55cbSimon Ulbricht . showProversOnly
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder-- | retrieve a list of consistency checkers
22bb4a9063684a0f37dd7d0e6b21086adcc1e789Christian MaedergetConsCheckersAux :: Maybe String -> G_sublogics
d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa -> IO [(AnyComorphism, [ProverOrConsChecker])]
d102a920578426a89411cc8dabe47d7a881eab8fEugen KuksagetConsCheckersAux mt =
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder fmap (groupOnSnd AbsState.ConsChecker) . getFilteredConsCheckers mt
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian MaedergetFilteredConsCheckers :: Maybe String -> G_sublogics
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder -> IO [(G_cons_checker, AnyComorphism)]
cddd87cd39be9d031348ef95051c4d14067e1646cmaedergetFilteredConsCheckers mt = fmap
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (filterByComorph mt . filter (getCcBatch . fst))
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian Maeder . getConsCheckers . findComorphismPaths logicGraph
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksagetComorphs :: Maybe String -> G_sublogics -> IO [(G_prover, AnyComorphism)]
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksagetComorphs mp = fmap (filterByProver mp)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder . getAllAutomaticProvers
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksagetFullComorphList :: DGraph -> IO [(G_prover, AnyComorphism)]
0552b690f40f3d73d4d4b2241fcb24d2ecc0c21eEugen KuksagetFullComorphList = foldM
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (\ ls (_, nd) -> maybe (return ls)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (fmap (++ ls) . getAllAutomaticProvers . sublogicOfTh)
41a3368af0eaad78c660477e7ded53b2ba85a275Christian Maeder $ maybeResult $ getGlobalTheory nd) [] . labNodesDG
10eaa95e20c860acbfbecd6cf07e3ae0bf7b55cbSimon UlbrichtformatComorphs :: [(G_prover, AnyComorphism)] -> String
10eaa95e20c860acbfbecd6cf07e3ae0bf7b55cbSimon UlbrichtformatComorphs = ppTopElement . unode "translations"
10eaa95e20c860acbfbecd6cf07e3ae0bf7b55cbSimon Ulbricht . map (unode "comorphism") . nubOrd . map (showComorph . snd)
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian MaederconsNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab)
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian Maeder -> G_sublogics -> Bool -> Maybe String -> Maybe String -> Maybe Int
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa -> ResultT IO (LibEnv, [ProofResult])
cddd87cd39be9d031348ef95051c4d14067e1646cmaederconsNode le ln dg nl@(i, lb) subL useTh mp mt tl = do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (cc, c) <- liftIO $ findConsChecker mt subL mp
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa cstat <- consistencyCheck useTh cc c ln le dg nl $ fromMaybe 1 tl
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- Consistency Results are stored in LibEnv via DGChange object
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let cSt = sType cstat
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa le'' = if cSt == CSUnchecked then le else
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Map.insert ln (changeDGH dg $ SetNodeLab lb
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (i, case cSt of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa CSInconsistent -> markNodeInconsistent "" lb
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa CSConsistent -> markNodeConsistent "" lb
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa _ -> lb)) le
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (le'', [(" ", drop 2 $ show cSt, show cstat,
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa AbsState.ConsChecker cc, c, Nothing, Just $ sMessage cstat)])
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksafindConsChecker :: Maybe String -> G_sublogics -> Maybe String
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> IO (G_cons_checker, AnyComorphism)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksafindConsChecker translationM gSublogic consCheckerNameM = do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa consList <- getFilteredConsCheckers translationM gSublogic
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder let findCC x = filter ((== x ) . getCcName . fst) consList
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa consCheckersL = maybe (findCC "darwin") findCC consCheckerNameM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa case consCheckersL of
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian Maeder [] -> fail "no cons checker found"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (gConsChecker, comorphism) : _ -> return (gConsChecker, comorphism)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksareasonREST :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> ProverMode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> String -> ReasoningParameters
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ResultT IO (LibEnv, [(String, [ProofResult])])
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksareasonREST opts libEnv libName dGraph_ proverMode location reasoningParameters = do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningCacheE <- liftIO buildReasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa failOnLefts reasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let reasoningCache1 = rights reasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningCache2 <- liftIO $ PGIP.Server.setupReasoning opts reasoningCache1
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (libEnv', cacheGoalsAndProofResults) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa PGIP.Server.performReasoning opts libEnv libName
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa dGraph_ location reasoningCache2
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let nodesAndProofResults = map
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (\ (nodeLabel, proofResults) ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (show (getName $ dgn_name nodeLabel), proofResults)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa cacheGoalsAndProofResults
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (libEnv', nodesAndProofResults)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa useDatabase :: Bool
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa useDatabase = format reasoningParameters == Just "db"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa failOnLefts :: ReasoningCacheE -> ResultT IO ()
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa failOnLefts reasoningCache =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let lefts_ = lefts reasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in unless (null lefts_) $ fail $ unlines lefts_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCache :: IO ReasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCache =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let reasoningParametersGroupedByNodeName =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa groupBy (\ a b ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ReasoningParameters.node a == ReasoningParameters.node b
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ) $ ReasoningParameters.goals reasoningParameters
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in foldM buildReasoningCacheForNode [] reasoningParametersGroupedByNodeName
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCacheForNode :: ReasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> IO ReasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCacheForNode reasoningCacheE goalConfigsOfSameNode =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let nodeName = ReasoningParameters.node $ head goalConfigsOfSameNode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa nodeM = find (\ (_, nodeLabel) ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa showName (dgn_name nodeLabel) == nodeName
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ) $ labNodesDG dGraph_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in case nodeM of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (Left ("Node \"" ++ nodeName ++ "\" not found")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa : reasoningCacheE)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Just node_@(_, nodeLabel) -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let gTheoryM = maybeResult $ getGlobalTheory nodeLabel
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa gTheory <- case gTheoryM of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa fail ("Cannot compute global theory of: "
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ++ showName (dgn_name nodeLabel) ++ "\n")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Just gTheory -> return gTheory
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let gSublogic = sublogicOfTh gTheory
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa foldM (buildReasoningCacheForGoal nodeName node_ gTheory gSublogic)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningCacheE goalConfigsOfSameNode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCacheForGoal :: String
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> (Int, DGNodeLab)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> G_sublogics
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ReasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> IO ReasoningCacheE
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa buildReasoningCacheForGoal nodeName node_ gTheory gSublogic reasoningCacheE goalConfig =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let reasonerM = reasoner $ reasonerConfiguration goalConfig
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa translationM = translation goalConfig
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasonerConfiguration goalConfig
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa caseReasoningCacheEntry = ReasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa { rceProverMode = proverMode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceNode = node_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceGoalNameM = Nothing
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceGoalConfig = goalConfig
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceGTheory = gTheory
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceGSublogic = gSublogic
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceReasoner = undefined -- will be overwritten a few lines below
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceComorphism = undefined -- will be overwritten a few lines below
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceTimeLimit = timeLimit_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceUseDatabase = useDatabase
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceReasonerConfigurationKeyM = Nothing
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceReasoningAttemptKeyM = Nothing
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in case proverMode of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlConsistency -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (gConsChecker, comorphism) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa findConsChecker translationM gSublogic reasonerM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return ((Right $ caseReasoningCacheEntry
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa { rceReasoner = AbsState.ConsChecker gConsChecker
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceComorphism = comorphism
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ) : reasoningCacheE)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlProofs -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa proversAndComorphisms <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa getProverAndComorph reasonerM translationM gSublogic
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (gProver, comorphism) <- case proversAndComorphisms of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa [] -> fail ("No matching translation or prover found for "
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ++ nodeName ++ "\n")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (gProver, comorphism) : _ ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (gProver, comorphism)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let possibleGoalNames = map fst $ getThGoals gTheory :: [String]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let goalNames = (case conjecture goalConfig of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Nothing -> possibleGoalNames
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Just goalName_ ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa filter (== goalName_) possibleGoalNames) :: [String]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (map (\ goalName_ -> Right $ caseReasoningCacheEntry
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa { rceGoalNameM = Just goalName_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceReasoner = AbsState.Prover gProver
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , rceComorphism = comorphism
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ) goalNames ++ reasoningCacheE)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksasetupReasoning :: HetcatsOpts -> ReasoningCache -> IO ReasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksasetupReasoning opts reasoningCache =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa mapM (\ reasoningCacheGoal -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningConfigurationKey <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Persistence.Reasoning.setupReasoning opts reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa { rceReasonerConfigurationKeyM = reasoningConfigurationKey }
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ) reasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaperformReasoning :: HetcatsOpts -> LibEnv -> LibName -> DGraph
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> String -> ReasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ResultT IO (LibEnv, [(DGNodeLab, [ProofResult])])
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaperformReasoning opts libEnv libName dGraph_ location reasoningCache = do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (libEnv', nodesAndProofResults') <- liftIO $ foldM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (\ (libEnvAcc1, nodesAndProofResults1) reasoningCacheGoalsByNode -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let nodeLabel = snd $ rceNode $ head reasoningCacheGoalsByNode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (libEnvAcc2, proofResults2) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (\ (libEnvAcc3, proofResults3) reasoningCacheGoal -> do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- update state
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let gTheoryM = maybeResult $ getGlobalTheory nodeLabel
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa gTheory_ <- case gTheoryM of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa fail ("Cannot compute global theory of: "
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ++ showName (dgn_name nodeLabel) ++ "\n")
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Just gTheory_ -> return gTheory_
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let reasoningCacheGoal' = reasoningCacheGoal { rceGTheory = gTheory_ }
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- preprocess (with database)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (premisesM, reasoningCacheGoal3) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Persistence.Reasoning.preprocessReasoning opts location
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningCacheGoal'
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- run the reasoner
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Result _ (Just (libEnvAcc4, proofResult : _)) <- runResultT $
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa runReasoning libEnvAcc3 libName dGraph_ reasoningCacheGoal3 premisesM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- postprocess (with database)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa Persistence.Reasoning.postprocessReasoning opts reasoningCacheGoal3
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa premisesM proofResult
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -- update state
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let proofResults4 = proofResult : proofResults3
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (libEnvAcc4, proofResults4)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (libEnvAcc1, [])
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasoningCacheGoalsByNode
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (libEnvAcc2, (nodeLabel, proofResults2) : nodesAndProofResults1)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (libEnv, []) $
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa groupBy sameNode reasoningCache
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (libEnv', nodesAndProofResults')
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa sameNode :: ReasoningCacheGoal -> ReasoningCacheGoal -> Bool
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa sameNode a b = fst (rceNode a) == fst (rceNode b)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksarunReasoning :: LibEnv -> LibName -> DGraph
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ReasoningCacheGoal -> Maybe [String]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ResultT IO (LibEnv, [ProofResult])
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksarunReasoning libEnv libName dGraph_ reasoningCacheGoal premisesM =
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let node_ = rceNode reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa gTheory_ = rceGTheory reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa gSublogic = rceGSublogic reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa useTheorems_ = fromMaybe True $ useTheorems $ rceGoalConfig reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa reasonerM = reasoner $ reasonerConfiguration $ rceGoalConfig reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa translationM = translation $ rceGoalConfig reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa timeLimitM = Just $ ReasoningParameters.timeLimit $ reasonerConfiguration $
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa rceGoalConfig reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa goalName_ = fromJust $ rceGoalNameM reasoningCacheGoal
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa premises = fromMaybe [] premisesM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa in case rceProverMode reasoningCacheGoal of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlConsistency -> consNode libEnv libName dGraph_ node_ gSublogic
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa useTheorems_ reasonerM translationM timeLimitM
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa GlProofs -> proveNode libEnv libName dGraph_ node_ gTheory_ gSublogic
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa useTheorems_ reasonerM translationM timeLimitM [goalName_] premises
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaproveNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> G_theory -> G_sublogics -> Bool
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> Maybe String -> Maybe String -> Maybe Int
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> [String] -> [String]
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> ResultT IO (LibEnv, [ProofResult])
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen KuksaproveNode le ln dg nl gTh subL useTh mp mt tl thms axioms = do
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ps <- lift $ getProverAndComorph mp mt subL
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder [] -> fail "no matching translation or prover found"
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht let ks = map fst $ getThGoals gTh
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder unless (Set.null diffs) . fail $ "unknown theorems: " ++ show diffs
dbce18afddbe9b055be0e37f51e00d00d519b1cdChristian Maeder when (null thms && null ks) $ fail "no theorems to prove"
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let selectedGoals_ = if null thms then ks else thms
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let timeLimit_ = maybe 1 (max 1) tl
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (nTh, sens, proofStatuses) <- do
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa let premises = axioms
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ((nTh, sens), (_, proofStatuses)) <-
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa autoProofAtNode useTh timeLimit_ selectedGoals_ premises gTh cp
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (nTh, sens, proofStatuses)
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return ( if null sens
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa else Map.insert ln ( updateLabelTheory le ln dg nl nTh) le
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa , combineToProofResult sens cp proofStatuses
8fa44603c0dfe55e122bb003c4afb558ef1e33adEugen KuksacombineToProofResult :: [(String, String, String)] -> (G_prover, AnyComorphism)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa -> [ProofStatus G_proof_tree] -> [ProofResult]
18d589be75aa0cbaacae9ab2884c0b07943de024Eugen KuksacombineToProofResult sens (prover, comorphism) proofStatuses = let
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa findProofStatusByName :: String -> Maybe (ProofStatus G_proof_tree)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa findProofStatusByName n =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case filter ((n ==) . goalName) proofStatuses of
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa [] -> Nothing
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (ps : _) -> Just ps
48ae34aa39aba121ea4f8dea362aadb0472a59feEugen Kuksa combineSens :: (String, String, String) -> ProofResult
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder combineSens (n, e, d) = (n, e, d, AbsState.Prover prover, comorphism,
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa findProofStatusByName n, Nothing)
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa in map combineSens sens
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht-- run over multiple dgnodes and prove available goals for each
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen KuksaproveMultiNodes :: ProverMode -> LibEnv -> LibName -> DGraph
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa -> Bool -> Maybe String -> Maybe String -> Maybe Int -> [String] -> [String]
68e05447f5ab8b56cd39012a58ab5ae280cfb25dEugen Kuksa -> ResultT IO (LibEnv, [(String, [ProofResult])])
68e05447f5ab8b56cd39012a58ab5ae280cfb25dEugen KuksaproveMultiNodes pm le ln dg useTh mp mt tl nodeSel axioms = let
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa runProof :: LibEnv -> G_theory -> (Int, DGNodeLab)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa -> ResultT IO (LibEnv, [ProofResult])
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian Maeder runProof le' gTh nl = let
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht subL = sublogicOfTh gTh
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder dg' = lookupDGraph ln le' in case pm of
ea4d82b1b67b5c79725c196883cab4bb78f412e5Christian Maeder GlConsistency -> consNode le' ln dg' nl subL useTh mp mt tl
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa proveNode le' ln dg' nl gTh subL useTh mp mt tl
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (map fst $ getThGoals gTh) axioms
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht nodes2check = filter (case nodeSel of
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian Maeder [] -> case pm of
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht GlConsistency -> const True
af2bfaed5d36cafe1092fe2bc1dbf5a763dfafcdSimon Ulbricht GlProofs -> hasOpenGoals . snd
a2af8492313011f78cbedbfd302dc12150b9f7efChristian Maeder _ -> (`elem` nodeSel) . getDGNodeName . snd) $ labNodesDG dg
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa (\ (le', res) nl@(_, dgn) ->
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa case maybeResult $ getGlobalTheory dgn of
e6c31a14c3fe6eb0eb93f376f2224f4023315e55Simon Ulbricht Nothing -> fail $
e6c31a14c3fe6eb0eb93f376f2224f4023315e55Simon Ulbricht "cannot compute global theory of:\n" ++ show dgn
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht Just gTh -> do
68e05447f5ab8b56cd39012a58ab5ae280cfb25dEugen Kuksa (le'', proofResults) <- runProof le' gTh nl
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa return (le'', (getDGNodeName dgn, proofResults) : res)
48ae34aa39aba121ea4f8dea362aadb0472a59feEugen KuksaformatResultsAux :: Bool -> ProverMode -> String -> [ProofResult] -> Element
29d783ee57c3d959b74fea330bb21ff7e5b8e185Christian MaederformatResultsAux xF pm nm sens = unode nm $ case (sens, pm) of
abdc8c3bcf5b761e9bebf51e6ba2bce659d29512Eugen Kuksa ([(_, e, d, _, _, _, _)], GlConsistency) | xF -> formatConsNode e d
682260563efe78f762d2d9db032a161ee0088851Eugen Kuksa _ -> add_attr (mkAttr "class" "results") $ unode "div" $ formatGoals xF sens
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian MaedermkPath :: Session -> LibName -> Int -> String
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian MaedermkPath sess l k =
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder '/' : concat [ libToFileName l ++ "?session="
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian Maeder | l /= sessLibName sess ]
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian MaederextPath :: Session -> LibName -> Int -> String
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian MaederextPath sess l k = mkPath sess l k ++
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian Maeder if l /= sessLibName sess then "&" else "?"
9cdf614df292d5984d9ffa69755e7e039f328116Christian MaederglobalCommands :: [String]
9cdf614df292d5984d9ffa69755e7e039f328116Christian MaederglobalCommands = map (cmdlGlobCmd . fst) allGlobLibAct
103848575cd92efdb3d4dc9809c16254d7415c2ecmaedersessAns :: LibName -> ResultT IO String -> (Session, Int)
103848575cd92efdb3d4dc9809c16254d7415c2ecmaeder -> ResultT IO (String, String)
1defc008da0fae281b776ffe464e2fef549804b5cmaedersessAns libName svgComp (sess, k) =
1defc008da0fae281b776ffe464e2fef549804b5cmaeder svgComp >>= \ svg -> return $ sessAnsAux libName svg (sess, k)
103848575cd92efdb3d4dc9809c16254d7415c2ecmaedersessAnsAux :: LibName -> String -> (Session, Int) -> (String, String)
1defc008da0fae281b776ffe464e2fef549804b5cmaedersessAnsAux libName svg (sess, k) =
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder let libEnv = sessLibEnv sess
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder ln = libToFileName libName
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ( aRef (mkPath sess l k) (libToFileName l)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , aRef (mkPath sess l k) "default"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa : map (\ d -> aRef (extPath sess l k ++ d) d) displayTypes
a07a6a1143844a6f061a49aefc550e3bdd28f331Christian Maeder libPath = extPath sess libName k
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder ref d = aRef (libPath ++ d) d
04c445e50a1d8b95e667595594e6b551c8b2ff59Simon Ulbricht autoProofBt = aRef ('/' : show k ++ "?autoproof") "automatic proofs"
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht consBt = aRef ('/' : show k ++ "?consistency") "consistency checker"
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht-- the html quicklinks to nodes and edges have been removed with R.16827
c4f9e16aa6d0b26e8ef6f896aac0daea9072f994Eugen Kuksa ("Hets, the DOLiator - (" ++ shows k ")" ++ ln)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ add_attr (mkAttr "class" "row") (unode "div" $ unode "h1" ("Library " ++ ln))
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa [ pageOptionsFormat "" libPath
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , dropDownElement "Tools" [autoProofBt, consBt]
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , dropDownElement "Commands" (map ref globalCommands)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , dropDownToLevelsElement "Imported Libraries" $ map libref $ Map.keys libEnv
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , add_attr (mkAttr "class" "row") $ unode "div" $ unode "h3" "Development Graph"
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaedergetHetsLibContent :: HetcatsOpts -> String -> [QueryPair] -> IO [Element]
f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian MaedergetHetsLibContent opts dir query = do
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let hlibs = libdirs opts
0caaa1bfea2f6665771ded5c54ef42b212da1217cmaeder ds <- if null dir || isAbsolute dir then return hlibs else
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder filterM doesDirectoryExist $ map (</> dir) hlibs
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder fs <- fmap (sortBy cmpFilePath . filter (not . isPrefixOf ".") . concat)
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder $ mapM getDirContents ds
b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder return $ map (mkHtmlRef query) $ getParent dir : fs
b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian MaedergetParent :: String -> String
187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian MaedergetParent = addTrailingPathSeparator . ("/" </>) . takeDirectory
187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian Maeder . dropTrailingPathSeparator
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder-- | a variant that adds a trailing slash
7710f7c3425e45af11af124ff37bec27229d24f7Christian MaedergetDirContents :: FilePath -> IO [FilePath]
7710f7c3425e45af11af124ff37bec27229d24f7Christian MaedergetDirContents d = do
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder fs <- getDirectoryContents d
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder mapM (\ f -> doesDirectoryExist (d </> f) >>= \ b -> return
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder $ if b then addTrailingPathSeparator f else f) fs
b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian MaederaRef :: String -> String -> Element
b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian MaederaRef lnk txt = add_attr (mkAttr "href" lnk) $ unode "a" txt
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian MaedermkHtmlRef :: [QueryPair] -> String -> Element
5d93620c37abd9c665d3fe532d4852d62dff4233Christian MaedermkHtmlRef query entry = unode "dir" $ aRef
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (entry ++ if null query then "" else '?' : intercalate "&"
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (map (\ (x, ms) -> x ++ maybe "" ('=' :) ms) query)) entry
3036e860d4b58913e4ac7a5b90583fa4390d1584Simon Ulbrichtplain :: String -> Element
3036e860d4b58913e4ac7a5b90583fa4390d1584Simon Ulbrichtplain = unode "p"
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederinputNode :: Element
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederinputNode = unode "input" ()
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksasubmitButton :: Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen KuksasubmitButton = add_attrs
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder [ mkAttr "type" "submit"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "value" "submit"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "class" "ui button"
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian MaedermkForm :: String -> [Element] -> Element
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa add_attrs [ mkAttr "action" a
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "enctype" "multipart/form-data"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "method" "post"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , mkAttr "class" "ui basic form"
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa ] . unode "form"