97a9a944b5887e91042b019776c41d5dd74557aferikabele{-# LANGUAGE CPP, DoAndIfThenElse #-}
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveDescription : run hets as server
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : (c) Christian Maeder, DFKI GmbH 2010
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveLicense : GPLv2 or higher, see LICENSE.txt
fe64b2ba25510d8c9dba5560a2d537763566cf40ndMaintainer : Christian.Maeder@dfki.de
fe64b2ba25510d8c9dba5560a2d537763566cf40ndStability : provisional
fe64b2ba25510d8c9dba5560a2d537763566cf40ndPortability : non-portable (via imports)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmodule PGIP.Server (hetsServer) where
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified PGIP.Output.Provers as OProvers
3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport PGIP.ReasoningParameters as ReasoningParameters
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7ndimport PGIP.Query as Query
dfb59c684345700bf9186b8d44936f8b1ba082ffgryzorimport qualified PGIP.Server.Examples as Examples
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernaimport Control.Monad.Trans (lift, liftIO)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd#ifdef WARP1
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Data.Conduit.Lazy (lazyConsume)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Data.Text as T
9597f440430d8c876dd64f5f78066804650a18ecnoodlimport qualified Data.ByteString.Lazy.Char8 as BS
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Data.ByteString.Char8 as B8
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrinimport Static.History (changeDGH)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Static.ToJson as ToJson
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Static.ToXml as ToXml
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenerimport qualified Persistence.DevGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Persistence.Reasoning
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Proofs.AbstractState as AbsState
709e3a21ba73b8433462959cd56c773454b34441trawickimport Text.XML.Light.Cursor hiding (lefts, rights)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.DocUtils (pretty, showGlobalDoc, showDoc)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.ExtSign (ExtSign (..))
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.Json (Json (..), ppJson)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Control.Exception (catch, throwTo)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Control.Exception.Base (SomeException)
b00fe3c3354db01001b8eddfd9b88441380f837dwroweimport Control.Concurrent (myThreadId, ThreadId)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Data.Aeson as Aeson
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Data.IntMap as IntMap
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Data.Map as Map
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Data.Set as Set
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Data.CaseInsensitive as CI
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowenimport System.Posix.Process (getProcessID)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowedata UsedAPI = OldWebAPI | RESTfulAPI deriving (Show, Eq, Ord)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorrandomKey :: IO Int
5ae609a8a09239d20f48a4a95c4f21b713995babwrowerandomKey = randomRIO (100000000, 999999999)
5ae609a8a09239d20f48a4a95c4f21b713995babwrowesessGraph :: DGQuery -> Session -> Maybe (LibName, DGraph)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernasessGraph dgQ s =
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener let le = sessLibEnv s
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener ln = sessLibName s
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener in case dgQ of
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener DGQuery _ (Just path) ->
6fad623c3cc52b4a84d4d36538f6eed886f49f98covener find (\ (n, _) -> libToFileName n == path)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna _ -> fmap (\ dg -> (ln, dg)) $ Map.lookup ln le
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernagetVal :: [QueryPair] -> String -> Maybe String
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernagetVal qs = fromMaybe Nothing . (`lookup` qs)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorgetIP4 :: String -> [String]
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernagetIP4 = splitOn '.' . takeWhile (\ c -> isDigit c || c == '.')
031bbbc0d1189b07330e38d0c126820a9ab7795egryzormatchIP4 :: [String] -> [String] -> Bool
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernamatchIP4 ip mask = case mask of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ft : rt -> case ip of
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna [] -> False -- mask too long or IP too short
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna d : s -> (null ft || ft == d) && matchIP4 rt s
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernamatchWhite :: [String] -> [[String]] -> Bool
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernamatchWhite ip l = null l || any (matchIP4 ip) l
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna#ifdef WARP3
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernatype WebResponse = (Response -> IO ResponseReceived) -> IO ResponseReceived
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernacatchException :: SomeException -> Response
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorcatchException e =
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna mkResponse textC
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor internalServerError500
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna ("*** Error:\n" ++ show e)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquernatype WebResponse = (Response -> RsrcIO Response) -> RsrcIO Response
5ae609a8a09239d20f48a4a95c4f21b713995babwrowedeletePidFileAndExit :: HetcatsOpts -> ThreadId -> ExitCode -> IO ()
5ae609a8a09239d20f48a4a95c4f21b713995babwrowedeletePidFileAndExit opts threadId exitCode = do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe deletePidFile opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe throwTo threadId exitCode
5ae609a8a09239d20f48a4a95c4f21b713995babwrowehetsServer :: HetcatsOpts -> IO ()
5ae609a8a09239d20f48a4a95c4f21b713995babwrowehetsServer opts = do
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe tid <- myThreadId
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe writePidFile opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe installHandler sigINT (Catch $ deletePidFileAndExit opts tid ExitSuccess) Nothing
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe installHandler sigTERM (Catch $ deletePidFileAndExit opts tid ExitSuccess) Nothing
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe hetsServer' opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe deletePidFile opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowewritePidFile :: HetcatsOpts -> IO ()
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowenwritePidFile opts =
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe let pidFilePath = pidFile opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe v = verbose opts
5ae609a8a09239d20f48a4a95c4f21b713995babwrowe in (unless (null pidFilePath) $
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor do unless (null pidFilePath)
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna (verbMsgIOLn v 2 ("Writing PIDfile " ++ show pidFilePath))
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna pid <- getProcessID
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowen writeFile pidFilePath (show pid))
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowendeletePidFile :: HetcatsOpts -> IO ()
9f19223e8fb7b99f5f1cc02c8c3c2c6567793262rbowendeletePidFile opts =
7e8f5c6496b3825b6b128e2aacc4b1b09d28553dpquerna let pidFilePath = pidFile opts
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in (unless (null pidFilePath) $ removeFile $ pidFile opts)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhetsServer' :: HetcatsOpts -> IO ()
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhetsServer' opts1 = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd tempDir <- getTemporaryDirectory
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let tempLib = tempDir </> "MyHetsLib"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd logFile = tempDir </>
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ("hets-" ++ show port ++ ".log")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd opts = opts1 { libdirs = tempLib : libdirs opts1 }
fe64b2ba25510d8c9dba5560a2d537763566cf40nd port1 = listen opts1
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen port = if port1 < 0 then 8000 else port1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd wl = whitelist opts1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive bl = blacklist opts1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive prList ll = intercalate ", " $ map (intercalate ".") ll
06ba4a61654b3763ad65f52283832ebf058fdf1cslive createDirectoryIfMissing False tempLib
06ba4a61654b3763ad65f52283832ebf058fdf1cslive writeFile logFile ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unless (null wl) . appendFile logFile
fb77c505254b6e9c925e23e734463e87574f8f40kess $ "white list: " ++ prList wl ++ "\n"
fb77c505254b6e9c925e23e734463e87574f8f40kess unless (null bl) . appendFile logFile
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ "black list: " ++ prList bl ++ "\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive putIfVerbose opts 1 $ "hets server is listening on port " ++ show port
06ba4a61654b3763ad65f52283832ebf058fdf1cslive putIfVerbose opts 2 $ "for more information look into file: " ++ logFile
06ba4a61654b3763ad65f52283832ebf058fdf1cslive#ifdef WARP3
06ba4a61654b3763ad65f52283832ebf058fdf1cslive runSettings (setOnExceptionResponse catchException $
fb77c505254b6e9c925e23e734463e87574f8f40kess setPort port $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive setTimeout 86400 defaultSettings)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ \ re respond -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive run port $ \ re -> do
fb77c505254b6e9c925e23e734463e87574f8f40kess let respond = liftIO . return
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let rhost = shows (remoteHost re) "\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ip = getIP4 rhost
06ba4a61654b3763ad65f52283832ebf058fdf1cslive white = matchWhite ip wl
06ba4a61654b3763ad65f52283832ebf058fdf1cslive black = any (matchIP4 ip) bl
fb77c505254b6e9c925e23e734463e87574f8f40kess splitQuery = map (\ (bs, ms) -> (B8.unpack bs, fmap B8.unpack ms))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ queryString re
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pathBits = map T.unpack $ pathInfo re
06ba4a61654b3763ad65f52283832ebf058fdf1cslive meth = B8.unpack (requestMethod re)
fb77c505254b6e9c925e23e734463e87574f8f40kess query = showPathQuery pathBits splitQuery
fb77c505254b6e9c925e23e734463e87574f8f40kess liftIO $ do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive time <- getCurrentTime
fb77c505254b6e9c925e23e734463e87574f8f40kess createDirectoryIfMissing False tempLib
bc4b55ec8f31569d606d5680d50189a355bcd7a6rbowen (m, _) <- readIORef sessRef
fb77c505254b6e9c925e23e734463e87574f8f40kess appendFile logFile rhost
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unless black $ if white then do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive appendFile logFile $ shows time " sessions: "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ shows (IntMap.size m) "\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive appendFile logFile $ shows (requestHeaders re) "\n"
fb77c505254b6e9c925e23e734463e87574f8f40kess unless (null query) $ appendFile logFile $ query ++ "\n"
fb77c505254b6e9c925e23e734463e87574f8f40kess else appendFile logFile "not white listed\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if not white || black then respond $ mkResponse "" status403 ""
fb77c505254b6e9c925e23e734463e87574f8f40kess -- if path could be a RESTful request, try to parse it
06ba4a61654b3763ad65f52283832ebf058fdf1cslive eith <- liftIO $ getArgFlags splitQuery
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd case eith of
130d299c4b2b15be45532a176604c71fdc7bea5bnd Left err -> queryFail err respond
130d299c4b2b15be45532a176604c71fdc7bea5bnd Right (qr, vs, fs) ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd let eith2 = getSwitches qr
130d299c4b2b15be45532a176604c71fdc7bea5bnd in case eith2 of
130d299c4b2b15be45532a176604c71fdc7bea5bnd Left err -> queryFail err respond
ef8e89e090461194ecadd31e8796a2c51e0531a2kess Right (qr2, fs2) ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd let newOpts = foldl makeOpts opts $ fs ++ map snd fs2
130d299c4b2b15be45532a176604c71fdc7bea5bnd in if isGraphQL meth pathBits then do
130d299c4b2b15be45532a176604c71fdc7bea5bnd responseString <- processGraphQL newOpts sessRef re
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd respond $ mkOkResponse "application/json" responseString
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else if isRESTful pathBits then do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd requestBodyBS <- strictRequestBody re
fe64b2ba25510d8c9dba5560a2d537763566cf40nd requestBodyParams <- parseRequestParams re requestBodyBS
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let unknown = filter (`notElem` allQueryKeys) $ map fst qr2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd if null unknown
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then parseRESTful newOpts sessRef pathBits
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (map fst fs2 ++ map (\ (a, b) -> a ++ "=" ++ b) vs)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd qr2 requestBodyBS requestBodyParams meth respond
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else queryFail ("unknown query key(s): " ++ show unknown) respond
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- only otherwise stick to the old response methods
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else oldWebApi newOpts tempLib sessRef re pathBits qr2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd meth respond
ff797e743eb73c1d45b08158aa6b288c2d0c46eesliveparseRequestParams :: Request -> BS.ByteString -> RsrcIO Json
ff797e743eb73c1d45b08158aa6b288c2d0c46eesliveparseRequestParams request requestBodyBS =
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess noParams :: Json
06ba4a61654b3763ad65f52283832ebf058fdf1cslive noParams = JNull
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd lookupHeader :: String -> Maybe String
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd lookupHeader s =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive liftM B8.unpack $ lookup (CI.mk $ B8.pack s) $ requestHeaders request
06ba4a61654b3763ad65f52283832ebf058fdf1cslive formParams :: RsrcIO (Maybe Json)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive formParams =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let toJsonObject :: [(B8.ByteString, B8.ByteString)] -> String
06ba4a61654b3763ad65f52283832ebf058fdf1cslive toJsonObject assocList = "{"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ intercalate ", " (map (\ (k, v) ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd show k ++ ": " ++ jsonStringOrArray v) assocList)
130d299c4b2b15be45532a176604c71fdc7bea5bnd jsonStringOrArray str =
130d299c4b2b15be45532a176604c71fdc7bea5bnd (formDataB8, _) <- parseRequestBody lbsBackEnd request
130d299c4b2b15be45532a176604c71fdc7bea5bnd return $ parseJson $ toJsonObject formDataB8
fe64b2ba25510d8c9dba5560a2d537763566cf40nd#ifdef WARP1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd lazyRequestBody :: Request -> ResourceT IO BS.ByteString
fe64b2ba25510d8c9dba5560a2d537763566cf40nd lazyRequestBody = fmap BS.fromChunks . lazyConsume . requestBody
fe64b2ba25510d8c9dba5560a2d537763566cf40nd liftM (fromMaybe noParams) $ case lookupHeader "Content-Type" of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just "application/json" -> jsonBody requestBodyBS
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just "multipart/form-data" -> formParams
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> formParams
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd-- | the old API that supports downloading files and interactive stuff
627c978514c54179736d152923478be7c8707f9bndoldWebApi :: HetcatsOpts -> FilePath -> Cache -> Request -> [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> [QueryPair] -> String -> WebResponse
fe64b2ba25510d8c9dba5560a2d537763566cf40ndoldWebApi opts tempLib sessRef re pathBits splitQuery meth respond =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case meth of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "GET" -> if isJust $ lookup "menus" splitQuery
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then mkMenuResponse respond else do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let path = intercalate "/" pathBits
fe64b2ba25510d8c9dba5560a2d537763566cf40nd dirs@(_ : cs) <- liftIO $ getHetsLibContent opts path splitQuery
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd if not (null cs) || null path then htmlResponse path dirs respond
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd -- AUTOMATIC PROOFS (parsing)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd else if isJust $ getVal splitQuery "autoproof" then
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd let qr k = Query (DGQuery k Nothing) $
b95ae799514ad86a15610ad75808d7065e9847c9kess anaAutoProofQuery splitQuery in do
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd Result ds ms <- liftIO $ runResultT
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd $ case readMaybe $ head pathBits of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Nothing -> fail "cannot read session id for automatic proofs"
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just k' -> getHetsResult opts [] sessRef (qr k')
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Nothing OldWebAPI proofFormatterOptions
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd respond $ case ms of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> mkResponse textC status422 $ showRelDiags 1 ds
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just (t, s) -> mkOkResponse t s
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- AUTOMATIC PROOFS E.N.D.
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd else getHetsResponse opts [] sessRef pathBits splitQuery respond
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd "POST" -> do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (params, files) <- parseRequestBody lbsBackEnd re
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let opts' = case lookup (B8.pack "input-type") params of
888b616027180cc8aaa4d2bee5ecc6acec175bc5nd Nothing -> opts
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just inputType -> if null $ B8.unpack inputType
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd else opts { intype = read $ B8.unpack inputType }
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd mTmpFile <- case lookup "content"
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd $ map (\ (a, b) -> (B8.unpack a, b)) params of
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Nothing -> return Nothing
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd Just areatext -> let content = B8.unpack areatext in
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd if all isSpace content then return Nothing else liftIO $ do
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd tmpFile <- getTempFile content "temp.het"
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd return $ Just tmpFile
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd let res tmpFile =
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd getHetsResponse opts' [] sessRef [tmpFile] splitQuery respond
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd mRes = maybe (queryFail "nothing submitted" respond)
5224ff8eae5156a05f676f1dad8add2e2f2efe1dnd res mTmpFile
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case files of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [] -> if isJust $ getVal splitQuery "prove" then
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd getHetsResponse opts' [] sessRef pathBits
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd (splitQuery ++ map (\ (a, b)
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier [(_, f)] | isNothing $ lookup updateS splitQuery -> do
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd let fn = takeFileName $ B8.unpack $ fileName f
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd if any isAlphaNum fn then do
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd let tmpFile = tempLib </> fn
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd liftIO $ BS.writeFile tmpFile $ fileContent f
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier maybe (res tmpFile) res mTmpFile
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd _ -> getHetsResponse
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd opts' (map snd files) sessRef pathBits splitQuery respond
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd _ -> respond $ mkResponse "" status400 ""
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier-- extract what we need to know from an autoproof request
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirieranaAutoProofQuery :: [QueryPair] -> QueryKind
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirieranaAutoProofQuery splitQuery = let
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier lookup2 = getVal splitQuery
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier prover = lookup2 "prover"
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier trans = lookup2 "translation"
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier timeout = lookup2 "timeout" >>= readMaybe
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier include = maybe False (== "on") $ lookup2 "includetheorems"
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier nodeSel = filter (/= "includetheorems")
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier $ map fst $ filter ((== Just "on") . snd) splitQuery
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd axioms = mSplitOnComma $ lookup2 "axioms"
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd prOrCons = case lookup2 "autoproof" of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Just "proof" -> GlProofs
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd Just "cons" -> GlConsistency
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd err -> error $ "illegal autoproof method: " ++ show err
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier in GlAutoProve $
2509f1cd3be884abbe4852e15b8da00bebaad5b1poirier ProveCmd prOrCons include prover trans timeout nodeSel False axioms
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd-- quick approach to whether or not the query can be a RESTful request
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndisRESTful :: [String] -> Bool
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndisRESTful pathBits = case pathBits of
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd [] -> False
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd [h] | elem h ["numeric-version", "version", "robots.txt"] -> True
4335f1cbf345c91bb996eec540c11ba8ce5d4268nd h : _ -> elem h listRESTfulIdentifiers
4335f1cbf345c91bb996eec540c11ba8ce5d4268ndlistRESTfulIdentifiers :: [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndlistRESTfulIdentifiers =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [ "libraries", "sessions", "menus", "filetype", "hets-lib", "dir"]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ nodeEdgeIdes ++ newRESTIdes
627c978514c54179736d152923478be7c8707f9bnd ++ ["available-provers"]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndnodeEdgeIdes :: [String]
6f7c18e70781deff3d1129774221de81b43c828endnodeEdgeIdes = ["nodes", "edges"]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndnewRESTIdes :: [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndnewRESTIdes =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [ "dg", "translations", "provers", "consistency-checkers", "prove"
fb77c505254b6e9c925e23e734463e87574f8f40kess , "consistency-check", "theory" ]
fb77c505254b6e9c925e23e734463e87574f8f40kessqueryFail :: String -> WebResponse
6b64034fa2a644ba291c484c0c01c7df5b8d982ckessqueryFail msg respond = respond $ mkResponse textC status400 msg
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessallQueryKeys :: [String]
10673857794a4b3d9568ca2d983722a87ed352f1rbowenallQueryKeys = [updateS, "library", "consistency-checker"]
fb77c505254b6e9c925e23e734463e87574f8f40kess ++ globalCommands ++ knownQueryKeys
10673857794a4b3d9568ca2d983722a87ed352f1rbowendata RequestBodyParam = Single String | List [String]
bed3c2e56e8f3328e780200466b9d009093db468sf-- query is analysed and processed in accordance with RESTful interface
bed3c2e56e8f3328e780200466b9d009093db468sfparseRESTful :: HetcatsOpts -> Cache -> [String] -> [String] -> [QueryPair]
bed3c2e56e8f3328e780200466b9d009093db468sf -> BS.ByteString -> Json -> String -> WebResponse
bed3c2e56e8f3328e780200466b9d009093db468sfparseRESTful
06ba4a61654b3763ad65f52283832ebf058fdf1cslive opts sessRef pathBits qOpts splitQuery requestBodyBS requestBodyParams meth respond = let
06ba4a61654b3763ad65f52283832ebf058fdf1cslive {- some parameters from the paths query part might be needed more than once
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (when using lookup upon querybits, you need to unpack Maybe twice) -}
fb77c505254b6e9c925e23e734463e87574f8f40kess lookupQueryStringParam :: String -> Maybe String
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lookupQueryStringParam = getVal splitQuery
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lookupBodyParam :: String -> Json -> Maybe RequestBodyParam
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lookupBodyParam key json = case json of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive JObject pairs -> case lookup key pairs of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (JArray a) -> Just $ List $ map (read . ppJson) a
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just v -> Just $ Single $ read $ ppJson v
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> Nothing
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> Nothing
1f53e295ebd19aed1767d12da7abfab9936c148cjerenkrantz lookupSingleParam :: String -> Maybe String
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end lookupSingleParam key = case meth of
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl "GET" -> lookupQueryStringParam key
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl _ -> case lookupBodyParam key requestBodyParams of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (Single s) -> Just s
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> Nothing
06ba4a61654b3763ad65f52283832ebf058fdf1cslive isParamTrue :: Bool -> String -> Bool
604c89126c27104f659d7a51b0113e3bd435faf8fielding isParamTrue def key = case fmap (map toLower) $ lookupSingleParam key of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> def
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just "true" -> True
604c89126c27104f659d7a51b0113e3bd435faf8fielding session = lookupSingleParam "session" >>= readMaybe
604c89126c27104f659d7a51b0113e3bd435faf8fielding library = lookupSingleParam "library"
604c89126c27104f659d7a51b0113e3bd435faf8fielding format_ = lookupSingleParam "format"
604c89126c27104f659d7a51b0113e3bd435faf8fielding nodeM = lookupSingleParam "node"
909ce17e2bd0faef7b1c294f2307f009793fd493nd includeDetails = isParamTrue True "includeDetails"
909ce17e2bd0faef7b1c294f2307f009793fd493nd includeProof = isParamTrue True "includeProof"
909ce17e2bd0faef7b1c294f2307f009793fd493nd transM = lookupSingleParam "translation"
909ce17e2bd0faef7b1c294f2307f009793fd493nd reasoningParametersE = parseReasoningParametersEither requestBodyBS
06ba4a61654b3763ad65f52283832ebf058fdf1cslive queryFailure = queryFail
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ("this query does not comply with RESTful interface: "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ showPathQuery pathBits splitQuery) respond
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- since used more often, generate full query out of nodeIRI and nodeCmd
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nodeQuery s = NodeQuery $ maybe (Right s) Left (readMaybe s :: Maybe Int)
97a9a944b5887e91042b019776c41d5dd74557aferikabele pfOptions = proofFormatterOptions
97a9a944b5887e91042b019776c41d5dd74557aferikabele { pfoIncludeProof = includeProof
97a9a944b5887e91042b019776c41d5dd74557aferikabele , pfoIncludeDetails = includeDetails
06ba4a61654b3763ad65f52283832ebf058fdf1cslive parseNodeQuery :: Monad m => String -> Int -> m NodeCommand -> m Query.Query
06ba4a61654b3763ad65f52283832ebf058fdf1cslive parseNodeQuery p sId ncmd = ncmd >>= let
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in return . Query (DGQuery sId (Just p)) . nodeQuery (getFragment p)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- call getHetsResult with the properly generated query (Final Result)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive getResponseAux myOpts qr = do
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0end let format' = Just $ fromMaybe "xml" format_
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Result ds ms <- liftIO $ runResultT $
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak getHetsResult myOpts [] sessRef qr format' RESTfulAPI pfOptions
06ba4a61654b3763ad65f52283832ebf058fdf1cslive respond $ case ms of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> mkResponse textC status422 $ showRelDiags 1 ds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (t, s) -> mkOkResponse t s
97a9a944b5887e91042b019776c41d5dd74557aferikabele getResponse = getResponseAux opts
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak -- respond depending on request Method
8e31885fc494b603e0650113dde9e29d1b1d2602maczniak in case meth of
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener rm | elem rm ["GET", "POST"] -> case pathBits of
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener ["robots.txt"] -> respond $ mkOkResponse textC
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener $ unlines ["User-agent: *", "Disallow: /"]
2b6565aedca9e9c10691b12fd2f3689bf4c85bc7jim -- show all menu options
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener ["menus"] -> mkMenuResponse respond
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener -- list files from directory
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener "dir" : r -> do
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener let path' = intercalate "/" r
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener dirs <- liftIO $ getHetsLibContent opts path' splitQuery
a011221d1a3bfb6ec07a3596c6dc962c58041ee6covener htmlResponse path' dirs respond
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ["version"] -> respond $ mkOkResponse textC hetsVersion
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ["numeric-version"] ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive respond $ mkOkResponse textC hetsVersionNumeric
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ["available-provers"] ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd liftIO (usableProvers logicGraph)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd >>= respond . mkOkResponse xmlC . ppTopElement
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- get dgraph from file
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "filetype" : libIri : _ -> mkFiletypeResponse opts libIri respond
ed0dae472b518c553c923a86fb4322d4c50d86a6nd "hets-lib" : r -> let file = intercalate "/" r in
ed0dae472b518c553c923a86fb4322d4c50d86a6nd getResponse $ Query (NewDGQuery file []) $ DisplayQuery format_
ed0dae472b518c553c923a86fb4322d4c50d86a6nd -- get library (complies with get/hets-lib for now)
ed0dae472b518c553c923a86fb4322d4c50d86a6nd ["libraries", libIri, "development_graph"] ->
da637bcae7b6e150470e701af29da5604a34a17erbowen getResponse $ Query (NewDGQuery libIri []) $ DisplayQuery format_
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor -- get previously created session
da637bcae7b6e150470e701af29da5604a34a17erbowen "sessions" : sessId : cmd -> case readMaybe sessId of
da637bcae7b6e150470e701af29da5604a34a17erbowen Nothing -> queryFail ("failed to read session number from " ++ sessId)
da637bcae7b6e150470e701af29da5604a34a17erbowen Just sId ->
da637bcae7b6e150470e701af29da5604a34a17erbowen (case nodeM of
da637bcae7b6e150470e701af29da5604a34a17erbowen Just ndIri -> parseNodeQuery ndIri sId $ case cmd of
7802d43d20007fa575e43b6ae77d5177ceffdb71sf ["provers"] -> return $ NcProvers GlProofs transM
7802d43d20007fa575e43b6ae77d5177ceffdb71sf ["translations"] -> return $ NcTranslations Nothing
7802d43d20007fa575e43b6ae77d5177ceffdb71sf _ -> fail $ "unknown node command for a GET-request: "
7802d43d20007fa575e43b6ae77d5177ceffdb71sf ++ intercalate "/" cmd
7802d43d20007fa575e43b6ae77d5177ceffdb71sf Nothing -> fmap (Query (DGQuery sId Nothing)) $ case cmd of
7802d43d20007fa575e43b6ae77d5177ceffdb71sf [] -> return $ DisplayQuery format_
7802d43d20007fa575e43b6ae77d5177ceffdb71sf ["provers"] -> return $ GlProvers GlProofs transM
bed3c2e56e8f3328e780200466b9d009093db468sf ["translations"] -> return GlTranslations
bed3c2e56e8f3328e780200466b9d009093db468sf _ -> fail $ "unknown global command for a GET-request: "
bed3c2e56e8f3328e780200466b9d009093db468sf ++ intercalate "/" cmd) >>= getResponse
bed3c2e56e8f3328e780200466b9d009093db468sf -- get node or edge view
bed3c2e56e8f3328e780200466b9d009093db468sf nodeOrEdge : p : c | elem nodeOrEdge nodeEdgeIdes -> let
bed3c2e56e8f3328e780200466b9d009093db468sf iriPath = takeWhile (/= '#') p
bed3c2e56e8f3328e780200466b9d009093db468sf dgQ = maybe (NewDGQuery (fromMaybe iriPath library) [])
bed3c2e56e8f3328e780200466b9d009093db468sf (`DGQuery` library) session
bed3c2e56e8f3328e780200466b9d009093db468sf f = getFragment p
bed3c2e56e8f3328e780200466b9d009093db468sf in case elemIndex nodeOrEdge nodeEdgeIdes of
bed3c2e56e8f3328e780200466b9d009093db468sf Just 0 -> let
bed3c2e56e8f3328e780200466b9d009093db468sf i = maybe (Right f) Left $ readMaybe f in
bed3c2e56e8f3328e780200466b9d009093db468sf getResponse $ Query dgQ $ NodeQuery i $ case c of
bed3c2e56e8f3328e780200466b9d009093db468sf ["theory"] -> NcCmd Query.Theory
bed3c2e56e8f3328e780200466b9d009093db468sf Just 1 -> case readMaybe f of
bed3c2e56e8f3328e780200466b9d009093db468sf Just i -> getResponse $ Query dgQ $ EdgeQuery i "edge"
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> queryFail ("failed to read edgeId from " ++ f) respond
bed3c2e56e8f3328e780200466b9d009093db468sf _ -> error $ "PGIP.Server.elemIndex " ++ nodeOrEdge
bed3c2e56e8f3328e780200466b9d009093db468sf newIde : libIri : rest ->
bed3c2e56e8f3328e780200466b9d009093db468sf let cmdOptList = filter (/= "") rest
bed3c2e56e8f3328e780200466b9d009093db468sf (optFlags, cmdList) = partition (`elem` map fst optionFlags)
bed3c2e56e8f3328e780200466b9d009093db468sf cmdOptList
bed3c2e56e8f3328e780200466b9d009093db468sf newOpts = foldl makeOpts opts $ mapMaybe (`lookup` optionFlags)
bed3c2e56e8f3328e780200466b9d009093db468sf validReasoningParams = isRight reasoningParametersE <=
bed3c2e56e8f3328e780200466b9d009093db468sf elem newIde ["prove", "consistency-check"]
bed3c2e56e8f3328e780200466b9d009093db468sf in if elem newIde newRESTIdes
bed3c2e56e8f3328e780200466b9d009093db468sf && all (`elem` globalCommands) cmdList
bed3c2e56e8f3328e780200466b9d009093db468sf && validReasoningParams
bed3c2e56e8f3328e780200466b9d009093db468sf qkind = case newIde of
bed3c2e56e8f3328e780200466b9d009093db468sf "translations" -> case nodeM of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> GlTranslations
bed3c2e56e8f3328e780200466b9d009093db468sf Just n -> nodeQuery n $ NcTranslations Nothing
bed3c2e56e8f3328e780200466b9d009093db468sf _ | elem newIde ["provers", "consistency-checkers"] ->
bed3c2e56e8f3328e780200466b9d009093db468sf let pm = if newIde == "provers" then GlProofs else GlConsistency
bed3c2e56e8f3328e780200466b9d009093db468sf in case nodeM of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> GlProvers pm transM
bed3c2e56e8f3328e780200466b9d009093db468sf Just n -> nodeQuery n $ NcProvers pm transM
bed3c2e56e8f3328e780200466b9d009093db468sf _ | elem newIde ["prove", "consistency-check"] ->
bed3c2e56e8f3328e780200466b9d009093db468sf case reasoningParametersE of
bed3c2e56e8f3328e780200466b9d009093db468sf Left message_ -> error ("Invalid parameters: " ++ message_) -- cannot happen
bed3c2e56e8f3328e780200466b9d009093db468sf Right reasoningParameters ->
bed3c2e56e8f3328e780200466b9d009093db468sf let proverMode = if newIde == "prove"
bed3c2e56e8f3328e780200466b9d009093db468sf then GlProofs
bed3c2e56e8f3328e780200466b9d009093db468sf else GlConsistency
bed3c2e56e8f3328e780200466b9d009093db468sf in GlAutoProveREST proverMode reasoningParameters
bed3c2e56e8f3328e780200466b9d009093db468sf "dg" -> case transM of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> DisplayQuery (Just $ fromMaybe "xml" format_)
bed3c2e56e8f3328e780200466b9d009093db468sf "theory" -> case transM of
bed3c2e56e8f3328e780200466b9d009093db468sf Nothing -> case nodeM of
bed3c2e56e8f3328e780200466b9d009093db468sf Just x -> NodeQuery (maybe (Right x) Left $ readMaybe x)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> error "REST: theory"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just tr -> case nodeM of
bed3c2e56e8f3328e780200466b9d009093db468sf Just x -> NodeQuery (maybe (Right x) Left $ readMaybe x)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> error "REST: theory"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error $ "REST: unknown " ++ newIde
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in getResponseAux newOpts . Query (NewDGQuery libIri $ cmdList
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ Set.toList (Set.fromList $ optFlags ++ qOpts)) $ qkind
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else if validReasoningParams
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then queryFailure
fb77c505254b6e9c925e23e734463e87574f8f40kess else case reasoningParametersE of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Left message_ ->
fb77c505254b6e9c925e23e734463e87574f8f40kess queryFail ("Invalid parameters: " ++ message_) respond
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Right _ ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd error "Unexpected error in PGIP.Server.parseRESTful"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> queryFailure
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "PUT" -> case pathBits of
c985aca104389df30d6ec0a637ce0ccaac904362nd {- execute global commands
fe64b2ba25510d8c9dba5560a2d537763566cf40nd TODO load other library ??? -}
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen ["libraries", libIri, "proofs", prId, cmd] ->
fb77c505254b6e9c925e23e734463e87574f8f40kess case readMaybe prId of
fb77c505254b6e9c925e23e734463e87574f8f40kess Nothing -> queryFail ("failed to read sessionId from " ++ prId)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Just sessId -> let
fe64b2ba25510d8c9dba5560a2d537763566cf40nd dgQ = DGQuery sessId $ Just libIri in
fe64b2ba25510d8c9dba5560a2d537763566cf40nd getResponse $ Query dgQ $ GlobCmdQuery cmd
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- execute a proof or calculus request
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ["sessions", sessId, cmd] -> case readMaybe sessId of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> queryFail ("failed to read sessionId from " ++ sessId)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just sId -> case cmd of
fb77c505254b6e9c925e23e734463e87574f8f40kess "prove" -> case reasoningParametersE of
fb77c505254b6e9c925e23e734463e87574f8f40kess Left message_ -> fail ("Invalid parameters: " ++ message_)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Right reasoningParameters ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ Query (DGQuery sId Nothing) $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlAutoProveREST GlProofs reasoningParameters
fe64b2ba25510d8c9dba5560a2d537763566cf40nd >>= getResponse
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- on other cmd look for (optional) specification of node or edge
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> case (nodeM, lookupSingleParam "edge") of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- fail if both are specified
5bb5fba250bf526bc51d13b25378d54acb93c1cbnoodl (Just _, Just _) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive fail "please specify only either node or edge"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- call command upon a single node
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Just ndIri, Nothing) -> parseNodeQuery ndIri sId
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ case lookup cmd $ map (\ a -> (showNodeCmd a, a)) nodeCmds of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just nc -> return $ NcCmd nc
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> fail $ "unknown node command '" ++ cmd ++ "' "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- call (the only) command upon a single edge
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Nothing, Just edIri) -> case readMaybe $ getFragOfCode edIri of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just i -> return $ Query (DGQuery sId Nothing)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ EdgeQuery i "edge"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Nothing ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd fail $ "failed to read edgeId from edgeIRI: " ++ edIri
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- call of global command
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd _ -> return $ Query (DGQuery sId Nothing) $ GlobCmdQuery cmd
06ba4a61654b3763ad65f52283832ebf058fdf1cslive >>= getResponse
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- fail if request doesn't comply
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> queryFailure
06ba4a61654b3763ad65f52283832ebf058fdf1cslive {- create failure response if request method is not known
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (should never happen) -}
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> respond $ mkResponse "" status400 ""
fb77c505254b6e9c925e23e734463e87574f8f40kessparseReasoningParametersEither :: BS.ByteString -> Either String ReasoningParameters
fb77c505254b6e9c925e23e734463e87574f8f40kessparseReasoningParametersEither requestBodyBS = Aeson.eitherDecode requestBodyBS
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmSplitOnComma :: Maybe String -> [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmSplitOnComma mstr = case mstr of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> []
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just str -> splitOn ',' str
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmkMenuResponse :: WebResponse
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmkMenuResponse respond =
604c89126c27104f659d7a51b0113e3bd435faf8fielding respond $ mkOkResponse xmlC $ ppTopElement $ unode "menus" mkMenus
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmkMenus :: [Element]
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmkMenus = menuTriple "" "Get menu triples" "menus"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd : menuTriple "/DGraph" updateS updateS
fe64b2ba25510d8c9dba5560a2d537763566cf40nd : map (\ (c, _) -> menuTriple "/" (menuTextGlobCmd c) $ cmdlGlobCmd c)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd allGlobLibAct
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ map (\ nc -> menuTriple "/DGraph/DGNode" ("Show " ++ nc) nc) nodeCommands
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen ++ [menuTriple "/DGraph/DGLink" "Show edge info" "edge"]
604c89126c27104f659d7a51b0113e3bd435faf8fieldingstatus422 :: Status
604c89126c27104f659d7a51b0113e3bd435faf8fieldingstatus422 = Status 422 $ B8.pack "Unprocessable Entity"
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkFiletypeResponse :: HetcatsOpts -> String -> WebResponse
22265f1724519886e2a2b5e0ebd61477506b7379noodlmkFiletypeResponse opts libIri respond = do
22265f1724519886e2a2b5e0ebd61477506b7379noodl res <- liftIO $ getContentAndFileType opts libIri
22265f1724519886e2a2b5e0ebd61477506b7379noodl respond $ case res of
22265f1724519886e2a2b5e0ebd61477506b7379noodl Left err -> mkResponse textC status422 err
604c89126c27104f659d7a51b0113e3bd435faf8fielding Right (mr, _, fn, _) -> case mr of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> mkResponse textC status422 $ fn ++ ": unknown file type"
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just r -> mkOkResponse textC $ fn ++ ": " ++ r
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmenuTriple :: String -> String -> String -> Element
604c89126c27104f659d7a51b0113e3bd435faf8fieldingmenuTriple q d c = unode "triple"
604c89126c27104f659d7a51b0113e3bd435faf8fielding [ unode "xquery" q
604c89126c27104f659d7a51b0113e3bd435faf8fielding , unode "displayname" d
604c89126c27104f659d7a51b0113e3bd435faf8fielding , unode "command" c ]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhtmlResponse :: FilePath -> [Element] -> WebResponse
9597f440430d8c876dd64f5f78066804650a18ecnoodlhtmlResponse path listElements respond = respond . mkOkResponse htmlC
9597f440430d8c876dd64f5f78066804650a18ecnoodl $ htmlPageWithTopContent path listElements
9597f440430d8c876dd64f5f78066804650a18ecnoodlhtmlPageWithTopContent :: FilePath -> [Element] -> String
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfhtmlPageWithTopContent path listElements =
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf htmlPage (if null path then "Start Page" else path) []
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf (pageHeader ++ pageOptions path listElements)
9597f440430d8c876dd64f5f78066804650a18ecnoodlhtmlPage :: String -> String -> [Element] -> String -> String
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfhtmlPage title javascripts body rawHtmlPageFooter = htmlHead title javascripts
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ intercalate "\n" (map ppElement body)
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ htmlWrapBottomContent rawHtmlPageFooter
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ htmlFoot
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfhtmlHead :: String -> String -> String
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsfhtmlHead title javascript =
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf "<!DOCTYPE html>\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ "<html lang=\"en\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <head>\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <meta charset=\"utf-8\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <meta content=\"width=device-width,initial-scale=1,shrink-to-fit=no\" name=\"viewport\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <meta content=\"#000000\" name=\"theme-color\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <meta name=\"robots\" content=\"noindex,nofollow\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <title>Hets, the DOLiator - " ++ title ++ "</title>\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <!-- Semantic UI stylesheet -->\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <style type=\"text/css\">\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ semanticUiCss ++ "\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " </style>\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <!-- Hets stylesheet -->\n"
141fd59714368d3bbe3a3d8f5b8dc8a516c48f9fsf ++ " <style type=\"text/css\">\n"
9597f440430d8c876dd64f5f78066804650a18ecnoodl ++ hetsCss ++ "\n"
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf ++ " </style>\n"
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf ++ " </head>\n"
cba8c0896ba04d42cf9a9e50df5040fd6bae14a4sf ++ " <body>\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " <!-- jQuery -->\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " <script type=\"text/javascript\">\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ jQueryJs ++ "\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " </script>\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " <!-- Semantic UI Javascript -->\n"
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen ++ " <script type=\"text/javascript\">\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ semanticUiJs ++ "\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " </script>\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " <!-- Static Hets Javascript -->\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " <script type=\"text/javascript\">\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ hetsJs ++ "\n"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ " </script>\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ " <!-- Dynamic Hets Javascript -->\n"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ " <script type=\"text/javascript\">\n"
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen ++ javascript ++ "\n"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor ++ " </script>\n"
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowen ++ " <div class=\"ui left aligned doubling stackable centered relaxed grid container\">\n"
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslivehtmlWrapBottomContent :: String -> String
fb77c505254b6e9c925e23e734463e87574f8f40kesshtmlWrapBottomContent content =
fb77c505254b6e9c925e23e734463e87574f8f40kess if null content then "" else
fb77c505254b6e9c925e23e734463e87574f8f40kess " <div class=\"ui segment pushable left aligned\" style=\"overflow: auto;\">\n"
fb77c505254b6e9c925e23e734463e87574f8f40kess ++ content
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive ++ " </div>\n"
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslivehtmlFoot :: String
130d299c4b2b15be45532a176604c71fdc7bea5bnd " </div>\n"
130d299c4b2b15be45532a176604c71fdc7bea5bnd ++ " </body>\n"
130d299c4b2b15be45532a176604c71fdc7bea5bnd ++ "</html>\n"
130d299c4b2b15be45532a176604c71fdc7bea5bndpageHeader :: [Element]
130d299c4b2b15be45532a176604c71fdc7bea5bndpageHeader =
130d299c4b2b15be45532a176604c71fdc7bea5bnd [ add_attr (mkAttr "class" "row") $ unode "div" $ unode "h1" "Hets, the DOLiator"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , add_attr (mkAttr "class" "row") $ unode "div" $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd add_attr (mkAttr "class" "ui text container raised segment center aligned") $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd unode "div" [ unode "p" "Welcome to DOLiator, the web interface to our implementation of the \"Ontology, Modeling and Specification Language\""
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen , add_attr (mkAttr "class" "ui horizontal list") $ unode "div"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ add_attr (mkAttr "target" "_blank") $ add_attr (mkAttr "class" "item") $ aRef "http://dol-omg.org/" "DOL Homepage"
fb77c505254b6e9c925e23e734463e87574f8f40kess , add_attr (mkAttr "target" "_blank") $ add_attr (mkAttr "class" "item") $ aRef "http://hets.eu/" "Hets Homepage"
fb77c505254b6e9c925e23e734463e87574f8f40kess , add_attr (mkAttr "class" "item") $ aRef "mailto:hets-devel@informatik.uni-bremen.de" "Contact"
d1348237b33bc1755b9f1165eea52317465a7671ndpageOptions :: String -> [Element] -> [Element]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepageOptions path listElements =
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ add_attr (mkAttr "class" "row") $ unode "div" $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd add_attr (mkAttr "class" "ui relaxed grid container segment") $ unode "div"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ add_attr (mkAttr "class" "row centered") $ unode "div" $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd 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\"."
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , add_attr (mkAttr "class" "three column row") $ unode "div"
fb77c505254b6e9c925e23e734463e87574f8f40kess [ pageOptionsFile
fb77c505254b6e9c925e23e734463e87574f8f40kess , pageOptionsExamples (not $ null path) listElements
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepageOptionsFile :: Element
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepageOptionsFile =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive add_attr (mkAttr "class" "ui container ten wide column left aligned") $ unode "div" $
130d299c4b2b15be45532a176604c71fdc7bea5bnd add_attr (mkAttr "class" "ui row") $ unode "div" pageOptionsFileForm
130d299c4b2b15be45532a176604c71fdc7bea5bndpageOptionsExamples :: Bool -> [Element] -> Element
130d299c4b2b15be45532a176604c71fdc7bea5bndpageOptionsExamples moreExamplesAreOpen listElements =
130d299c4b2b15be45532a176604c71fdc7bea5bnd add_attr (mkAttr "class" "ui container six wide column left aligned") $ unode "div"
130d299c4b2b15be45532a176604c71fdc7bea5bnd [ unode "h4" "Minimal Examples"
df70c4445a86c43993e578fd1212c69ac52587a1rbowen , add_attr (mkAttr "class" "ui list") $ unode "div" $
130d299c4b2b15be45532a176604c71fdc7bea5bnd map (\ (elementName, inputType, exampleText) ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd add_attr (mkAttr "class" "item") $ unode "div" $
130d299c4b2b15be45532a176604c71fdc7bea5bnd add_attrs [ mkAttr "class" "insert-example-into-user-input-text"
130d299c4b2b15be45532a176604c71fdc7bea5bnd , mkAttr "data-text" exampleText
130d299c4b2b15be45532a176604c71fdc7bea5bnd , mkAttr "data-input-type" inputType
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ] $ unode "span" elementName
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ) [ ("DOL", "dol", Examples.dol)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("CASL", "casl", Examples.casl)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("OWL", "owl", Examples.owl)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("CLIF", "clif", Examples.clif)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("Propositional", "het", Examples.propositional)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("RDF", "rdf", Examples.rdf)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("TPTP", "tptp", Examples.tptp)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , ("HasCASL", "het", Examples.hascasl)
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , ("Modal", "het", Examples.modal)
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess , pageMoreExamples moreExamplesAreOpen listElements
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepageOptionsFileForm :: Element
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepageOptionsFileForm = add_attr (mkAttr "id" "user-file-form") $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkForm "/" [ pageOptionsFilePickerInput
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , horizontalDivider "OR"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , pageOptionsFileTextArea
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , add_attrs [mkAttr "class" "ui relaxed grid", mkAttr "style" "margin-top: 1em"] $ unode "div"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ add_attr (mkAttr "class" "six wide column") $ unode "div" inputTypeDropDown
130d299c4b2b15be45532a176604c71fdc7bea5bnd , add_attr (mkAttr "class" "ten wide column right aligned") $ unode "div" submitButton
130d299c4b2b15be45532a176604c71fdc7bea5bndinputTypeDropDown :: Element
130d299c4b2b15be45532a176604c71fdc7bea5bndinputTypeDropDown = singleSelectionDropDown
130d299c4b2b15be45532a176604c71fdc7bea5bnd "Input Type of File or Text Field"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive "input-type"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess (Just "user-file-input-type")
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess ( ("", "[Try to determine automatically]", [])
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess : map (\ inType -> (show inType, show inType, [])) plainInTypes
6b64034fa2a644ba291c484c0c01c7df5b8d982ckesssingleSelectionDropDown :: String -> String -> Maybe String -> [(String, String, [Attr])] -> Element
06ba4a61654b3763ad65f52283832ebf058fdf1cslivesingleSelectionDropDown label inputName htmlIdM options = unode "div"
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen [ add_attr (mkAttr "class" "ui sub header") $ unode "div" label
4e10c61d7f924071cad435df940a8f325015b2d3rbowen , add_attrs ( mkAttr "name" inputName
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen : maybe [] (\ htmlId -> [mkAttr "id" htmlId]) htmlIdM
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ) $ unode "select" $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (\ (optionValue, optionLabel, attributes) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive add_attrs (mkAttr "value" optionValue : attributes) $
130d299c4b2b15be45532a176604c71fdc7bea5bnd unode "option" optionLabel
130d299c4b2b15be45532a176604c71fdc7bea5bndcheckboxElement :: String -> [Attr] -> Element
130d299c4b2b15be45532a176604c71fdc7bea5bndcheckboxElement label attributes =
130d299c4b2b15be45532a176604c71fdc7bea5bnd add_attr (mkAttr "class" "four wide column") $ unode "div" $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive add_attr (mkAttr "class" "ui checkbox") $ unode "div"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ add_attrs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ([ mkAttr "type" "checkbox"
fb77c505254b6e9c925e23e734463e87574f8f40kess , mkAttr "tabindex" "0"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , mkAttr "class" "hidden"
fb77c505254b6e9c925e23e734463e87574f8f40kess ] ++ attributes) $ unode "input" ""
fb77c505254b6e9c925e23e734463e87574f8f40kess , unode "label" label
fe64b2ba25510d8c9dba5560a2d537763566cf40ndpageOptionsFileTextArea :: Element
fe64b2ba25510d8c9dba5560a2d537763566cf40ndpageOptionsFileTextArea = add_attrs
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess [ mkAttr "cols" "68"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess , mkAttr "rows" "22"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , mkAttr "name" "content"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "id" "user-input-text"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "style" "font-family: monospace;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ] $ unode "textarea" ""
fe64b2ba25510d8c9dba5560a2d537763566cf40ndpageOptionsFilePickerInput :: Element
fe64b2ba25510d8c9dba5560a2d537763566cf40ndpageOptionsFilePickerInput = filePickerInputElement "file" "file" "Choose File..."
cb43ec0a02f97651bf2f46c9f4b9b48d5cb22df7rbowenpageOptionsFormat :: String -> String -> Element
fe64b2ba25510d8c9dba5560a2d537763566cf40ndpageOptionsFormat delimiter path =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let defaultFormat = "default"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in dropDownElement "Output Format" $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd map (\ f ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd aRef (if f == defaultFormat then "/" </> path else "/" </> path ++ delimiter ++ f) f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ) (defaultFormat : displayTypes)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilePickerInputElement :: String -> String -> String -> Element
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorfilePickerInputElement idArgument nameArgument title =
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor add_attr (mkAttr "class" "field") $ unode "div" $
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor add_attr (mkAttr "class" "ui fluid file input action") $ unode "div"
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener [ add_attrs [mkAttr "type" "text", mkAttr "readonly" "true"] $ unode "input" ""
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , add_attrs [ mkAttr "type" "file"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "id" idArgument
6954edc623ca2c179eb5b33e97e4304d06fd649frbowen , mkAttr "name" nameArgument
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "autocomplete" "off"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ] $ unode "input" ""
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , add_attr (mkAttr "class" "ui button") $ unode "div" title
fa1c7ce09927decc1eecd1e9a35cc5331078a052covenerdropDownElement :: String -> [Element] -> Element
fa1c7ce09927decc1eecd1e9a35cc5331078a052covenerdropDownElement title items =
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener add_attr (mkAttr "class" "ui dropdown button") $ unode "div"
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener [ add_attr (mkAttr "class" "text") $ unode "div" title
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener , add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener , dropDownSubMenu items
fa1c7ce09927decc1eecd1e9a35cc5331078a052covenerlinkButtonElement :: String -> String -> Element
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorlinkButtonElement address label =
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor add_attr (mkAttr "class" "ui button") $ aRef address label
fa1c7ce09927decc1eecd1e9a35cc5331078a052covenerhtmlRow :: Element -> Element
fa1c7ce09927decc1eecd1e9a35cc5331078a052covenerhtmlRow = add_attr (mkAttr "class" "row") . unode "div"
fe64b2ba25510d8c9dba5560a2d537763566cf40nddropDownToLevelsElement :: String -> [(Element, [Element])] -> Element
fe64b2ba25510d8c9dba5560a2d537763566cf40nddropDownToLevelsElement title twoLeveledItems =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive add_attr (mkAttr "class" "ui dropdown button") $ unode "div"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess [ add_attr (mkAttr "class" "text") $ unode "div" title
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess , add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess , add_attr (mkAttr "class" "menu") $ unode "div" $
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess map (\ (label, items) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd add_attr (mkAttr "class" "item") $ unode "div"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ( if null items
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else [add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ [add_attr (mkAttr "class" "text") $ unode "div" label]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ if null items then [] else [dropDownSubMenu items]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ) twoLeveledItems
fe64b2ba25510d8c9dba5560a2d537763566cf40nddropDownSubMenu :: [Element] -> Element
9bcfc3697a91b5215893a7d0206865b13fc72148nddropDownSubMenu items =
fb77c505254b6e9c925e23e734463e87574f8f40kess add_attr (mkAttr "class" "menu") $ unode "div" $
fb77c505254b6e9c925e23e734463e87574f8f40kess map (add_attr (mkAttr "class" "item")) items
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndpageMoreExamples :: Bool -> [Element] -> Element
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndpageMoreExamples isOpen listElements =
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let activeClass = if isOpen then "active " else "" in
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd add_attr (mkAttr "class" "ui ten wide column container left aligned") $ unode "div" $
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd add_attr (mkAttr "class" "ui styled accordion") $ unode "div"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ add_attr (mkAttr "class" (activeClass ++ "title")) $ unode "div"
d565edaec710102f7e7d06252aaf1de67b7ddd25rbowen [ add_attr (mkAttr "class" "dropdown icon") $ unode "i" ""
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , unode "span" "More Examples"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , add_attr (mkAttr "class" (activeClass ++ "content")) $ unode "div" $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive add_attr (mkAttr "class" "transistion hidden") $ unode "div" $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unode "ul" listElements
fe64b2ba25510d8c9dba5560a2d537763566cf40ndhorizontalDivider :: String -> Element
1b01d1ee11c612226cb3141eed4581dc179266c1rbowenhorizontalDivider label =
1b01d1ee11c612226cb3141eed4581dc179266c1rbowen add_attr (mkAttr "class" "ui horizontal divider") $ unode "div" label
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmkResponse :: String -> Status -> String -> Response
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmkResponse ty st = responseLBS st
8559a67073808d84d85bb5dd552d4247caafe709sf (if null ty then [] else
8559a67073808d84d85bb5dd552d4247caafe709sf#ifdef HTTPTYPES
8559a67073808d84d85bb5dd552d4247caafe709sf [headerContentType $ B8.pack ty]
8559a67073808d84d85bb5dd552d4247caafe709sf [(hContentType, B8.pack ty)]
8559a67073808d84d85bb5dd552d4247caafe709sf ) . BS.pack . encodeString
8559a67073808d84d85bb5dd552d4247caafe709sfmkOkResponse :: String -> String -> Response
8559a67073808d84d85bb5dd552d4247caafe709sfmkOkResponse ty = mkResponse ty status200
8559a67073808d84d85bb5dd552d4247caafe709sfaddSess :: Cache -> Session -> IO Int
8559a67073808d84d85bb5dd552d4247caafe709sfaddSess sessRef s = do
8559a67073808d84d85bb5dd552d4247caafe709sf let k = sessKey s
8559a67073808d84d85bb5dd552d4247caafe709sf atomicModifyIORef sessRef $ \ (m, lm) ->
8559a67073808d84d85bb5dd552d4247caafe709sfcleanUpCache :: Cache -> IO ()
8559a67073808d84d85bb5dd552d4247caafe709sfcleanUpCache sessRef = do
8559a67073808d84d85bb5dd552d4247caafe709sf let mSize = 60
8559a67073808d84d85bb5dd552d4247caafe709sf time <- getCurrentTime
8559a67073808d84d85bb5dd552d4247caafe709sf atomicModifyIORef sessRef $ \ (m, lm) ->
8559a67073808d84d85bb5dd552d4247caafe709sf if Map.size lm < mSize then ((m, lm), ()) else
8559a67073808d84d85bb5dd552d4247caafe709sf let ss = cleanUpSessions time mSize m
8559a67073808d84d85bb5dd552d4247caafe709sf in ((IntMap.fromList $ map (\ s -> (sessKey s, s)) ss
8559a67073808d84d85bb5dd552d4247caafe709sf , Map.fromList $ map (\ s -> (sessPath s, s)) ss), ())
8559a67073808d84d85bb5dd552d4247caafe709sf cleanUpSessions :: UTCTime -> Int -> IntMap.IntMap Session -> [Session]
8559a67073808d84d85bb5dd552d4247caafe709sf cleanUpSessions time maxSize =
8559a67073808d84d85bb5dd552d4247caafe709sf unifySessionLists . dropCleanables . sessionCleanableLists
8559a67073808d84d85bb5dd552d4247caafe709sf sessionSort :: [Session] -> [Session]
8559a67073808d84d85bb5dd552d4247caafe709sf sessionSort = sortBy (cmpSess time)
8559a67073808d84d85bb5dd552d4247caafe709sf sessionCleanableLists :: IntMap.IntMap Session -> ([Session], [Session])
8559a67073808d84d85bb5dd552d4247caafe709sf sessionCleanableLists =
8559a67073808d84d85bb5dd552d4247caafe709sf partition sessCleanable . sessionSort . IntMap.elems
8559a67073808d84d85bb5dd552d4247caafe709sf dropCleanables :: ([Session], [Session]) -> ([Session], [Session])
8559a67073808d84d85bb5dd552d4247caafe709sf dropCleanables (cleanables, uncleanables) =
8559a67073808d84d85bb5dd552d4247caafe709sf (drop (maxSize `div` 2) cleanables, uncleanables)
8559a67073808d84d85bb5dd552d4247caafe709sf unifySessionLists :: ([Session], [Session]) -> [Session]
8559a67073808d84d85bb5dd552d4247caafe709sf unifySessionLists = sessionSort . uncurry (++)
8559a67073808d84d85bb5dd552d4247caafe709sfcmpSess :: UTCTime -> Session -> Session -> Ordering
8559a67073808d84d85bb5dd552d4247caafe709sfcmpSess curTime =
8559a67073808d84d85bb5dd552d4247caafe709sf let f s = let
8559a67073808d84d85bb5dd552d4247caafe709sf l = lastAccess s
8559a67073808d84d85bb5dd552d4247caafe709sf b = sessStart s
8559a67073808d84d85bb5dd552d4247caafe709sf d2 = utctDay curTime
8559a67073808d84d85bb5dd552d4247caafe709sf s2 = utctDayTime curTime
8559a67073808d84d85bb5dd552d4247caafe709sf d1 = utctDay l
8559a67073808d84d85bb5dd552d4247caafe709sf s1 = utctDayTime l
8559a67073808d84d85bb5dd552d4247caafe709sf u = usage s
8559a67073808d84d85bb5dd552d4247caafe709sf in if u <= 1 && d1 == d2 && s2 > secondsToDiffTime 3600 + s1
8559a67073808d84d85bb5dd552d4247caafe709sf then (u + 100, diffUTCTime l curTime)
8559a67073808d84d85bb5dd552d4247caafe709sf else (u, diffUTCTime b l)
8559a67073808d84d85bb5dd552d4247caafe709sf in on compare f
8559a67073808d84d85bb5dd552d4247caafe709sfaddNewSess :: Cache -> Session -> IO Int
8559a67073808d84d85bb5dd552d4247caafe709sfaddNewSess sessRef sess = do
8559a67073808d84d85bb5dd552d4247caafe709sf cleanUpCache sessRef
8559a67073808d84d85bb5dd552d4247caafe709sf k <- randomKey
8559a67073808d84d85bb5dd552d4247caafe709sf let s = sess { sessKey = k }
8559a67073808d84d85bb5dd552d4247caafe709sf addSess sessRef s
8559a67073808d84d85bb5dd552d4247caafe709sfnextSess :: LibEnv -> Session -> Cache -> Int -> IO Session
8559a67073808d84d85bb5dd552d4247caafe709sfnextSess newLib =
8559a67073808d84d85bb5dd552d4247caafe709sf modifySessionAndCache "nextSess" (\ s -> s { sessLibEnv = newLib })
8559a67073808d84d85bb5dd552d4247caafe709sfmakeSessCleanable :: Session -> Cache -> Int -> IO Session
8559a67073808d84d85bb5dd552d4247caafe709sfmakeSessCleanable =
8559a67073808d84d85bb5dd552d4247caafe709sf modifySessionAndCache "makeSessCleanable" (\ s -> s { sessCleanable = True })
8559a67073808d84d85bb5dd552d4247caafe709sfmodifySessionAndCache :: String -> (Session -> Session) -> Session -> Cache
8559a67073808d84d85bb5dd552d4247caafe709sf -> Int -> IO Session
8559a67073808d84d85bb5dd552d4247caafe709sfmodifySessionAndCache errorMessage f sess sessRef k =
8559a67073808d84d85bb5dd552d4247caafe709sf if k <= 0 then return sess else
8559a67073808d84d85bb5dd552d4247caafe709sf atomicModifyIORef sessRef
8559a67073808d84d85bb5dd552d4247caafe709sf (\ (m, lm) -> case IntMap.lookup k m of
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> error errorMessage
8559a67073808d84d85bb5dd552d4247caafe709sf Just s -> let newSess = f s
8559a67073808d84d85bb5dd552d4247caafe709sf in ((IntMap.insert k newSess m, lm), newSess))
8559a67073808d84d85bb5dd552d4247caafe709sfppDGraph :: DGraph -> Maybe PrettyType -> ResultT IO (String, String)
8559a67073808d84d85bb5dd552d4247caafe709sfppDGraph dg mt = let ga = globalAnnos dg in case optLibDefn dg of
8559a67073808d84d85bb5dd552d4247caafe709sf Nothing -> fail "parsed LIB-DEFN not avaible"
8559a67073808d84d85bb5dd552d4247caafe709sf Just ld ->
8559a67073808d84d85bb5dd552d4247caafe709sf let d = prettyLG logicGraph ld
8559a67073808d84d85bb5dd552d4247caafe709sf latex = renderLatex Nothing $ toLatex ga d
8559a67073808d84d85bb5dd552d4247caafe709sf in case mt of
8559a67073808d84d85bb5dd552d4247caafe709sf Just pty -> case pty of
8559a67073808d84d85bb5dd552d4247caafe709sf PrettyXml -> return
8559a67073808d84d85bb5dd552d4247caafe709sf (xmlC, ppTopElement $ xmlLibDefn logicGraph ga ld)
8559a67073808d84d85bb5dd552d4247caafe709sf PrettyAscii _ -> return (textC, renderText ga d ++ "\n")
8559a67073808d84d85bb5dd552d4247caafe709sf PrettyHtml -> return (htmlC, renderHtml ga d)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd PrettyLatex _ -> return ("application/latex", latex)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> lift $ do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd tmpDir <- getTemporaryDirectory
fb77c505254b6e9c925e23e734463e87574f8f40kess tmpFile <- writeTempFile (latexHeader ++ latex ++ latexFooter)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd mapM_ (\ s -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let sty = (</> "hetcasl.sty")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ex <- doesFileExist f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd when ex $ copyFile f $ sty tmpDir)
9bcfc3697a91b5215893a7d0206865b13fc72148nd [ "utils", "Hets/utils"
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , "/home/www.informatik.uni-bremen.de/cofi/hets-tmp" ]
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive withinDirectory tmpDir $ do
fb77c505254b6e9c925e23e734463e87574f8f40kess (ex1, out1, err1) <- executeProcess "pdflatex" [tmpFile] ""
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen (ex2, out2, err2) <- executeProcess "pdflatex" [tmpFile] ""
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let pdfFile = replaceExtension tmpFile "pdf"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd pdf <- doesFileExist pdfFile
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd if ex1 == ExitSuccess && ex2 == ExitSuccess && pdf then do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pdfHdl <- openBinaryFile pdfFile ReadMode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd str <- hGetContents pdfHdl
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd when (length str < 0) $ putStrLn "pdf file too large"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hClose pdfHdl
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (pdfC, str)
9bcfc3697a91b5215893a7d0206865b13fc72148nd else return (textC, "could not create pdf:\n"
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poirier ++ unlines [out1, err1, out2, err2])
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poirierincreaseUsage :: Cache -> Session -> ResultT IO (Session, Int)
e4286c93598ad346ac365e59ac9c6f9e6e9fd324poirierincreaseUsage sessRef sess = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive time <- lift getCurrentTime
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let s2 = sess { usage = usage sess + 1, lastAccess = time }
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd k <- lift $ addSess sessRef s2
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return (s2, k)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetDGraph :: HetcatsOpts -> Cache -> DGQuery
fb77c505254b6e9c925e23e734463e87574f8f40kess -> ResultT IO (Session, Int)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndgetDGraph opts sessRef dgQ = do
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh (m, lm) <- lift $ readIORef sessRef
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh case dgQ of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh NewDGQuery file cmdList -> do
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh let cl = mapMaybe (\ s -> find ((== s) . cmdlGlobCmd)
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh $ map fst allGlobLibAct) cmdList
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh mf <- lift $ getContentAndFileType opts file
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess case mf of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Left err -> fail err
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Right (_, mh, f, cont) -> case mh of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Nothing -> fail $ "could determine checksum for: " ++ file
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Just h -> let q = file : h : cmdList in
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case Map.lookup q lm of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just sess -> increaseUsage sessRef sess
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (ln, le1) <- if isDgXmlFile opts f cont
fe64b2ba25510d8c9dba5560a2d537763566cf40nd then readDGXmlR opts f Map.empty
fe64b2ba25510d8c9dba5560a2d537763566cf40nd else anaSourceFile logicGraph opts
fb77c505254b6e9c925e23e734463e87574f8f40kess { outputToStdout = False }
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf Set.empty emptyLibEnv emptyDG file
fe64b2ba25510d8c9dba5560a2d537763566cf40nd le2 <- foldM (\ e c -> liftR
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ fromJust (lookup c allGlobLibAct) ln e) le1 cl
fe64b2ba25510d8c9dba5560a2d537763566cf40nd time <- lift getCurrentTime
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let sess = Session
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf { sessLibEnv = le2
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , sessLibName = ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , sessPath = q
9bcfc3697a91b5215893a7d0206865b13fc72148nd , sessKey = 0 -- to be updated by addNewSess
9bcfc3697a91b5215893a7d0206865b13fc72148nd , sessStart = time
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh , lastAccess = time
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh , usage = 1
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen , sessCleanable = False }
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh k <- lift $ addNewSess sessRef sess
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh return (sess, k)
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick DGQuery k _ -> case IntMap.lookup k m of
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess Nothing -> fail "unknown development graph"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Just sess -> increaseUsage sessRef sess
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshgetSVG :: String -> String -> DGraph -> ResultT IO String
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshgetSVG title url dg = do
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh (exCode, out, err) <- lift $ executeProcess "dot" ["-Tsvg"]
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh $ dotGraph title False url dg
9fb925624300c864fe3969a264e52aa83f3c2dd0slive case exCode of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess ExitSuccess -> liftR $ extractSVG dg out
78f4d313fd5edf76dc5cfb8725e082a08cd29740jwoolley _ -> fail err
f653ca260580e6d64d92ae29963f207b94e87353ndenrichSVG :: DGraph -> Element -> Element
f653ca260580e6d64d92ae29963f207b94e87353ndenrichSVG dg e = processSVG dg $ fromElement e
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessprocessSVG :: DGraph -> Cursor -> Element
9fb925624300c864fe3969a264e52aa83f3c2dd0sliveprocessSVG dg c = case nextDF c of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Nothing -> case toTree (root c) of
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh Elem e -> e
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf _ -> error "processSVG"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf Just c2 -> processSVG dg
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh $ modifyContent (addSVGAttribs dg) c2
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfnodeAttrib :: DGNodeLab -> String
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshnodeAttrib l = let nt = getRealDGNodeType l in
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh (if isRefType nt then "Ref" else "")
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf ++ (if hasSenKind (const True) l then
9fb925624300c864fe3969a264e52aa83f3c2dd0slive (if isProvenNode nt then "P" else "Unp") ++ "roven"
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh ++ if isProvenCons nt then "Cons" else ""
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh else "LocallyEmpty")
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess ++ (if isInternalSpec nt then "Internal" else "")
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess ++ if labelHasHiding l then "HasIngoingHidingLink" else ""
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessedgeAttrib :: DGLinkLab -> String
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshedgeAttrib l = show (pretty $ dgl_type l) ++
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejesh if dglPending l then "IncompleteProofChain" else ""
832853bb93c1831daf24e4727c5ca0e1b1786e83larsaddSVGAttribs :: DGraph -> Content -> Content
78f97ce162b66a0dbfd7af4dcd9984f162569b04minfrinaddSVGAttribs dg c = case c of
832853bb93c1831daf24e4727c5ca0e1b1786e83lars Elem e -> case getAttrVal "id" e of
832853bb93c1831daf24e4727c5ca0e1b1786e83lars Just istr | isNat istr -> let i = read istr in
832853bb93c1831daf24e4727c5ca0e1b1786e83lars case getAttrVal "class" e of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just "node" -> case lab (dgBody dg) i of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Nothing -> c
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Just l -> Elem $ add_attr (mkAttr "type" $ nodeAttrib l) e
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Just "edge" -> case getDGLinksById (EdgeId i) dg of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick [(_, _, l)] ->
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Elem $ add_attr (mkAttr "type" $ edgeAttrib l) e
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickextractSVG :: DGraph -> String -> Result String
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickextractSVG dg str = case parseXMLDoc str of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Nothing -> fail "did not recognize svg element"
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Just e -> return $ showTopElement $ enrichSVG dg e
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickcmpFilePath :: FilePath -> FilePath -> Ordering
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickcmpFilePath f1 f2 = case comparing hasTrailingPathSeparator f2 f1 of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick EQ -> compare f1 f2
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickgetHetsResponse :: HetcatsOpts -> [W.FileInfo BS.ByteString]
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick -> Cache -> [String] -> [QueryPair] -> WebResponse
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickgetHetsResponse opts updates sessRef pathBits query respond = do
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Result ds ms <- liftIO $ runResultT $ case anaUri pathBits query
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick $ updateS : globalCommands of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Left err -> fail err
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Right q -> getHetsResult opts updates sessRef q Nothing OldWebAPI
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick proofFormatterOptions
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick respond $ case ms of
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick Just (t, s) | not $ hasErrors ds -> mkOkResponse t s
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick _ -> mkResponse textC status422 $ showRelDiags 1 ds
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickgetHetsResult :: HetcatsOpts -> [W.FileInfo BS.ByteString]
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick -> Cache -> Query.Query -> Maybe String -> UsedAPI -> ProofFormatterOptions
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawick -> ResultT IO (String, String)
dce2bc31f4940687c7ffabb80570bc37ea7296d8trawickgetHetsResult opts updates sessRef (Query dgQ qk) format_ api pfOptions = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let getCom n = let ncoms = filter (\(Comorphism cid) -> language_name cid == n) comorphismList
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in case ncoms of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [] -> error $ "comorphism not found:" ++ n
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> error $ "more than one comorphism found for:" ++ n
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sk@(sess', k) <- getDGraph opts sessRef dgQ
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sess <- lift $ makeSessCleanable sess' sessRef k
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let libEnv = sessLibEnv sess
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (ln, dg) <- maybe (fail "unknown development graph") return
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ sessGraph dgQ sess
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let title = libToFileName ln
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let svg = getSVG title ('/' : show k) dg
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DisplayQuery ms -> case format_ `mplus` ms of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "db" -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive result <- liftIO $ Control.Exception.catch
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (jsonC, "{\"savedToDatabase\": true}")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (\ exception ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (jsonC, "{\"savedToDatabase\": false, \"error\": " ++ show (exception :: SomeException) ++ "}")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd liftR $ return result
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "svg" -> fmap (\ s -> (svgC, s)) svg
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "xml" -> liftR $ return (xmlC, ppTopElement
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ ToXml.dGraph opts libEnv ln dg)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "json" -> liftR $ return (jsonC, ppJson
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ ToJson.dGraph opts libEnv ln dg)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "dot" -> liftR $ return
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen (dotC, dotGraph title False title dg)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just "symbols" -> liftR $ return (xmlC, ppTopElement
59cd19c3d75e35ae820e23f6b0161910784fce4eslive Just "session" -> liftR $ return (htmlC, ppElement
59cd19c3d75e35ae820e23f6b0161910784fce4eslive $ aRef (mkPath sess ln k) $ show k)
59cd19c3d75e35ae820e23f6b0161910784fce4eslive Just str | elem str ppList
59cd19c3d75e35ae820e23f6b0161910784fce4eslive -> ppDGraph dg $ lookup str $ zip ppList prettyList
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> sessAns ln svg sk
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- compose the comorphisms passed in translation
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let coms = map getCom $ splitOn ',' path
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd com <- foldM compComorphism (head coms) $ tail coms
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd dg' <- liftR $ dg_translation libEnv ln dg com
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd liftR $ return (xmlC, ppTopElement
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ ToXml.dGraph opts libEnv ln dg')
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GlProvers mp mt -> do
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen availableProvers <- liftIO $ getFullProverList mp mt dg
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd return $ case api of
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen OldWebAPI -> (xmlC, formatProvers mp $
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd proversToStringAux availableProvers)
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd RESTfulAPI -> OProvers.formatProvers format_ mp availableProvers
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GlTranslations -> do
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd availableComorphisms <- liftIO $ getFullComorphList dg
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd return $ case api of
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd OldWebAPI ->
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd (xmlC, formatComorphs availableComorphisms)
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd RESTfulAPI ->
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd formatTranslations format_ availableComorphisms
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GlShowProverWindow prOrCons -> showAutoProofWindow dg k prOrCons
7a497a1b89d0b52f5284854eb12662b4bd80ba5cnd GlAutoProveREST proverMode reasoningParameters -> case api of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive RESTfulAPI -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (newLib, nodesAndProofResults) <-
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen reasonREST opts libEnv ln dg proverMode (queryLib dgQ) reasoningParameters
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if all (null . snd) nodesAndProofResults
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then return (textC, "nothing to prove")
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lift $ nextSess newLib sess sessRef k
06ba4a61654b3763ad65f52283832ebf058fdf1cslive processProofResult format_ pfOptions nodesAndProofResults
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> fail ("The GlAutoProveREST path is only "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ "available in the REST interface.")
06ba4a61654b3763ad65f52283832ebf058fdf1cslive GlAutoProve (ProveCmd prOrCons incl mp mt tl nds xForm axioms) -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (newLib, nodesAndProofResults) <-
06ba4a61654b3763ad65f52283832ebf058fdf1cslive proveMultiNodes prOrCons libEnv ln dg incl mp mt tl nds axioms
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess if all (null . snd) nodesAndProofResults
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then return (textC, "nothing to prove")
fb77c505254b6e9c925e23e734463e87574f8f40kess lift $ nextSess newLib sess sessRef k
fb77c505254b6e9c925e23e734463e87574f8f40kess case api of
fb77c505254b6e9c925e23e734463e87574f8f40kess OldWebAPI -> let
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive sens = foldr (\ (dgNodeName, proofResults) res ->
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive formatResultsAux xForm prOrCons dgNodeName proofResults
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick ) [] nodesAndProofResults
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive in return (htmlC, formatResultsMultiple xForm k sens prOrCons)
59cd19c3d75e35ae820e23f6b0161910784fce4eslive RESTfulAPI ->
59cd19c3d75e35ae820e23f6b0161910784fce4eslive processProofResult format_ pfOptions nodesAndProofResults
59cd19c3d75e35ae820e23f6b0161910784fce4eslive GlobCmdQuery s ->
59cd19c3d75e35ae820e23f6b0161910784fce4eslive case find ((s ==) . cmdlGlobCmd . fst) allGlobLibAct of
59cd19c3d75e35ae820e23f6b0161910784fce4eslive Nothing -> if s == updateS then
59cd19c3d75e35ae820e23f6b0161910784fce4eslive case filter ((== ".xupdate") . takeExtension . B8.unpack
59cd19c3d75e35ae820e23f6b0161910784fce4eslive . fileName) updates of
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor ch : _ -> do
b5d3d68a9f683722eac7a3ca507c3e571908dfc0rbowen let str = BS.unpack $ fileContent ch
b5d3d68a9f683722eac7a3ca507c3e571908dfc0rbowen (newLn, newLib) <- dgXUpdate opts str libEnv ln dg
b5d3d68a9f683722eac7a3ca507c3e571908dfc0rbowen newSess <- lift $ nextSess newLib sess sessRef k
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen sessAns newLn svg (newSess, k)
59cd19c3d75e35ae820e23f6b0161910784fce4eslive [] -> sessAns ln svg sk
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just (_, act) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd newLib <- liftR $ act ln libEnv
fe64b2ba25510d8c9dba5560a2d537763566cf40nd newSess <- lift $ nextSess newLib sess sessRef k
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- calculate updated SVG-view from modified development graph
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let newSvg = getSVG title ('/' : show k)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ lookupDGraph ln newLib
fe64b2ba25510d8c9dba5560a2d537763566cf40nd sessAns ln newSvg (newSess, k)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd NodeQuery ein nc -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nl@(i, dgnode) <- case ein of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Right n -> case lookupNodeByName n dg of
c1fcddc76fd5db5ac4ccd7c6ae839d53d128f354minfrin p : _ -> return p
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [] -> fail $ "no node name: " ++ n
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Left i -> case lab (dgBody dg) i of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> fail $ "no node id: " ++ show i
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just dgnode -> return (i, dgnode)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let fstLine = (if isDGRef dgnode then ("reference " ++) else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if isInternalNode dgnode then ("internal " ++) else id)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor "Node " ++ getDGNodeName dgnode ++ " (#" ++ show i ++ ")\n"
c68acc9d712af079afa2bd1a5a4aeef9a3ea573ckess ins = getImportNames dg i
fb109b84906e3ee61680aa289953c2f9e859354erbowen showN d = showGlobalDoc (globalAnnos dg) d "\n"
fb109b84906e3ee61680aa289953c2f9e859354erbowen NcCmd cmd | elem cmd [Query.Node, Info, Symbols]
fb109b84906e3ee61680aa289953c2f9e859354erbowen -> case cmd of
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Symbols -> return (xmlC, ppTopElement
fb109b84906e3ee61680aa289953c2f9e859354erbowen $ showSymbols opts ins (globalAnnos dg) dgnode)
db2474c3448fc75c325aa43ba0144fced1a38c53rjung _ -> return (textC, fstLine ++ showN dgnode)
db2474c3448fc75c325aa43ba0144fced1a38c53rjung _ -> case maybeResult $ getGlobalTheory dgnode of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> fail $
fb109b84906e3ee61680aa289953c2f9e859354erbowen "cannot compute global theory of:\n" ++ fstLine
fb109b84906e3ee61680aa289953c2f9e859354erbowen Just gTh -> let subL = sublogicOfTh gTh in case nc of
fb109b84906e3ee61680aa289953c2f9e859354erbowen ProveNode (ProveCmd pm incl mp mt tl thms xForm axioms) ->
db2474c3448fc75c325aa43ba0144fced1a38c53rjung GlProofs -> do
db2474c3448fc75c325aa43ba0144fced1a38c53rjung (newLib, proofResults) <- proveNode libEnv ln dg nl
db2474c3448fc75c325aa43ba0144fced1a38c53rjung gTh subL incl mp mt tl thms axioms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if null proofResults
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then return (textC, "nothing to prove")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd lift $ nextSess newLib sess sessRef k
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd case api of
5155e92c6100b47513159eee1b2b9914ab204a5acovener OldWebAPI -> return (htmlC,
5155e92c6100b47513159eee1b2b9914ab204a5acovener formatResults xForm k i .
5155e92c6100b47513159eee1b2b9914ab204a5acovener add_attr (mkAttr "class" "results") $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unode "div" $ formatGoals True proofResults)
fb109b84906e3ee61680aa289953c2f9e859354erbowen RESTfulAPI -> processProofResult format_ pfOptions
fb109b84906e3ee61680aa289953c2f9e859354erbowen [(getDGNodeName dgnode, proofResults)]
fb109b84906e3ee61680aa289953c2f9e859354erbowen GlConsistency -> do
fb109b84906e3ee61680aa289953c2f9e859354erbowen (newLib, [(_, res, txt, _, _, _, _)]) <-
06ba4a61654b3763ad65f52283832ebf058fdf1cslive consNode libEnv ln dg nl subL incl mp mt tl
06ba4a61654b3763ad65f52283832ebf058fdf1cslive lift $ nextSess newLib sess sessRef k
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawick return (xmlC, ppTopElement $ formatConsNode res txt)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> case nc of
c023f60e35022146373e40249f0c8c8d623b6fcfnd NcCmd Query.Theory -> case api of
c023f60e35022146373e40249f0c8c8d623b6fcfnd OldWebAPI -> lift $ fmap (\ t -> (htmlC, t))
d972e4a0688f66b1402473dd9dacfecefa2132a8rbowen $ showGlobalTh dg i gTh k fstLine
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor RESTfulAPI -> lift $ fmap (\ t -> (xmlC, t))
c023f60e35022146373e40249f0c8c8d623b6fcfnd $ showNodeXml opts (globalAnnos dg) libEnv dg i
c023f60e35022146373e40249f0c8c8d623b6fcfnd NcCmd (Query.Translate x) -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- compose the comorphisms passed in translation
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let coms = map getCom $ splitOn ',' x
fe64b2ba25510d8c9dba5560a2d537763566cf40nd com <- foldM compComorphism (head coms) $ tail coms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- translate the theory of i along com
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen gTh1 <- liftR $ mapG_theory com gTh
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- insert the translation of i in dg
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin let n1 = getNewNodeDG dg
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin labN1 = newInfoNodeLab
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf emptyNodeName
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (newNodeInfo DGBasic) -- to be corrected
2851546ce44280e54301016a7e92b00a87745509sf dg1 = insLNodeDG (n1, labN1) dg
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf gmor <- liftR $ gEmbedComorphism com $ signOf $ dgn_theory dgnode
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- add a link from i to n1 labeled with (com, id)
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf let (_, dg2) = insLEdgeDG
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (i, n1, globDefLink gmor SeeSource) -- origin to be corrected
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- show the theory of n1 in xml format
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf lift $ fmap (\ t -> (xmlC, t)) $ showNodeXml opts (globalAnnos dg2) libEnv dg2 n1
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf NcProvers mp mt -> do
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf availableProvers <- liftIO $ getProverList mp mt subL
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf return $ case api of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf OldWebAPI -> (xmlC, formatProvers mp $
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf proversToStringAux availableProvers)
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf RESTfulAPI ->
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf OProvers.formatProvers format_ mp availableProvers
4cb65c31bc681540ea623e1cb2bdd09749fb8d7esf NcTranslations mp -> do
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf availableComorphisms <- liftIO $ getComorphs mp subL
2bb4320391b88748dc6e851deca941b058231664rbowen return $ case api of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf OldWebAPI ->
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (xmlC, formatComorphs availableComorphisms)
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf RESTfulAPI ->
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf formatTranslations format_ availableComorphisms
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf EdgeQuery i _ ->
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf case getDGLinksById (EdgeId i) dg of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [e@(_, _, l)] ->
2bb4320391b88748dc6e851deca941b058231664rbowen return (textC, showLEdge e ++ "\n" ++ showDoc l "")
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [] -> fail $ "no edge found with id: " ++ show i
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf _ -> fail $ "multiple edges found with id: " ++ show i
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfprocessProofResult :: Maybe String
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -> ProofFormatterOptions
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -> [(String, [ProofResult])]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -> ResultT IO (String, String)
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfprocessProofResult format_ options nodesAndProofResults =
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf if format_ == Just "db"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf then return (jsonC, "{\"savedToDatabase\": true}")
2bb4320391b88748dc6e851deca941b058231664rbowen else return $ formatProofs format_ options nodesAndProofResults
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatGoals :: Bool -> [ProofResult] -> [Element]
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowenformatGoals includeDetails =
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowen map (\ (n, e, d, _, _, mps, _) -> add_attr (mkAttr "class" "results-goal") $ unode "div"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf ([ unode "h3" ("Results for " ++ n ++ " (" ++ e ++ ")") ]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf ++ [add_attr (mkAttr "class" "results-details") $ unode "div" d | includeDetails]
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowen ++ case mps of
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowen Nothing -> []
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowen Just ps -> formatProofStatus ps))
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowenformatProofStatus :: ProofStatus G_proof_tree -> [Element]
221a06bb836af6024708190895834af79c90d1c8rbowenformatProofStatus ps =
221a06bb836af6024708190895834af79c90d1c8rbowen [ unode "h5" "Used Prover"
221a06bb836af6024708190895834af79c90d1c8rbowen , add_attr (mkAttr "class" "usedProver") $ unode "p" $ usedProver ps
221a06bb836af6024708190895834af79c90d1c8rbowen -- `read` makes this type-unsafe
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "h5" "Tactic Script"
2bb4320391b88748dc6e851deca941b058231664rbowen , add_attr (mkAttr "class" "tacticScript") $ unode "p" $ formatTacticScript $ read $
2bb4320391b88748dc6e851deca941b058231664rbowen (\ (TacticScript ts) -> ts) $ tacticScript ps
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "h5" "Proof Tree"
2bb4320391b88748dc6e851deca941b058231664rbowen , add_attr (mkAttr "class" "proofTree") $ unode "div" $ show $ proofTree ps
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "h5" "Used Time"
2bb4320391b88748dc6e851deca941b058231664rbowen , add_attr (mkAttr "class" "usedTime") $ unode "div" $ formatUsedTime $ usedTime ps
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "h5" "Used Axioms"
2bb4320391b88748dc6e851deca941b058231664rbowen , add_attr (mkAttr "class" "usedAxioms") $ unode "div" $ formatUsedAxioms $ usedAxioms ps
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "h5" "Prover Output"
2bb4320391b88748dc6e851deca941b058231664rbowen , add_attr (mkAttr "class" "proverOutput") $ unode "div" $ formatProverOutput $ proofLines ps
2bb4320391b88748dc6e851deca941b058231664rbowenformatProverOutput :: [String] -> Element
2bb4320391b88748dc6e851deca941b058231664rbowenformatProverOutput = unode "pre" . unlines
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatTacticScript :: ATPTacticScript -> [Element]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatTacticScript ts =
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [ unode "timeLimit" $ show $ tsTimeLimit ts
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , unode "extraOpts" $ map (unode "option") $ tsExtraOpts ts
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatUsedTime :: TimeOfDay -> [Element]
2bb4320391b88748dc6e851deca941b058231664rbowenformatUsedTime tod =
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [ unode "seconds" $ init $ show $ timeOfDayToTime tod
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "components"
0b5f11662dee7135ff8dd04311a4ee6df7fe2b1crbowen [ unode "hours" $ show $ todHour tod
2bb4320391b88748dc6e851deca941b058231664rbowen , unode "minutes" $ show $ todMin tod
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , unode "seconds" $ show $ todSec tod
0b5f11662dee7135ff8dd04311a4ee6df7fe2b1crbowenformatUsedAxioms :: [String] -> [Element]
2bb4320391b88748dc6e851deca941b058231664rbowenformatUsedAxioms = map (unode "axiom")
2bb4320391b88748dc6e851deca941b058231664rbowenformatConsNode :: String -> String -> Element
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatConsNode res txt = add_attr (mkAttr "state" res) $ unode "result" txt
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfformatResultsMultiple :: Bool -> Int -> [Element] -> ProverMode -> String
2bb4320391b88748dc6e851deca941b058231664rbowenformatResultsMultiple xForm sessId rs prOrCons =
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf if xForm then ppTopElement $ unode "Results" rs else let
2bb4320391b88748dc6e851deca941b058231664rbowen goBack1 = case prOrCons of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf GlConsistency -> aRef ('/' : show sessId ++ "?consistency") "return"
2bb4320391b88748dc6e851deca941b058231664rbowen GlProofs -> aRef ('/' : show sessId ++ "?autoproof") "return"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf goBack2 = aRef ('/' : show sessId) "return to DGraph"
dd2f29c187db35e7635ce67a83dddceb75be87a4minfrin in htmlPage "Results" []
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [ htmlRow $ unode "h1" "Results"
2bb4320391b88748dc6e851deca941b058231664rbowen , htmlRow $ unode "div" [goBack1, goBack2]
0b5f11662dee7135ff8dd04311a4ee6df7fe2b1crbowen , htmlRow $ unode "div" $
2bb4320391b88748dc6e851deca941b058231664rbowen foldr (\ el r -> unode "h4" (qName $ elName el) : el : r) [] rs
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf-- | display results of proving session (single node)
2bb4320391b88748dc6e851deca941b058231664rbowenformatResults :: Bool -> Int -> Int -> Element -> String
ffb01336be79c64046b636e59fa8ddca8ec029edsfformatResults xForm sessId i rs =
ffb01336be79c64046b636e59fa8ddca8ec029edsf if xForm || sessId <= 0 then ppTopElement rs else let
2bb4320391b88748dc6e851deca941b058231664rbowen goBack1 = linkButtonElement ('/' : show sessId ++ "?theory=" ++ show i) "return to Theory"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf goBack2 = linkButtonElement ('/' : show sessId) "return to DGraph"
2bb4320391b88748dc6e851deca941b058231664rbowen in htmlPage "Results" []
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [ htmlRow $ unode "h1" "Results"
2bb4320391b88748dc6e851deca941b058231664rbowen , htmlRow $ unode "div" [goBack1, goBack2]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , htmlRow $ add_attr (mkAttr "class" "ui relaxed grid raised segment container left aligned") $ unode "div" rs
e80f65dadea03d04ee5b9e2d3de8c5fcef9e6714minfrinshowBool :: Bool -> String
e80f65dadea03d04ee5b9e2d3de8c5fcef9e6714minfrinshowBool = map toLower . show
e80f65dadea03d04ee5b9e2d3de8c5fcef9e6714minfrinshowNodeXml :: HetcatsOpts -> GlobalAnnos -> LibEnv -> DGraph -> Int -> IO String
e80f65dadea03d04ee5b9e2d3de8c5fcef9e6714minfrinshowNodeXml opts ga lenv dg n = let
e80f65dadea03d04ee5b9e2d3de8c5fcef9e6714minfrin lNodeN = lab (dgBody dg) n
ffb01336be79c64046b636e59fa8ddca8ec029edsf in case lNodeN of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf Just lNode -> return $ ppTopElement $ ToXml.lnode opts ga lenv (n,lNode)
ffb01336be79c64046b636e59fa8ddca8ec029edsf Nothing -> error $ "no node for " ++ show n
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf{- | displays the global theory for a node with the option to prove theorems
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfand select proving options -}
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfshowGlobalTh :: DGraph -> Int -> G_theory -> Int -> String -> IO String
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfshowGlobalTh dg i gTh sessId fstLine = case simplifyTh gTh of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf sGTh@(G_theory lid _ (ExtSign sig _) _ thsens _) -> let
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf ga = globalAnnos dg
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- links to translations and provers xml view
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic transBt = linkButtonElement ('/' : show sessId ++ "?translations=" ++ show i)
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic "translations"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf prvsBt = linkButtonElement ('/' : show sessId ++ "?provers=" ++ show i) "provers"
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen headr = htmlRow $ unode "h3" fstLine
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen thShow = renderHtml ga $ vcat $ map (print_named lid) $ toNamedList thsens
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf sbShow = renderHtml ga $ pretty sig
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf in case getThGoals sGTh of
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- show simple view if no goals are found
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen [] -> return $ htmlPage fstLine ""
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen , htmlRow $ unode "h4" "Theory"
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen ] $ "<pre>\n" ++ sbShow ++ "\n<br />" ++ thShow ++ "\n</pre>\n"
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen -- else create proving functionality
abdaaa23d72ef7e7ff91eab9c5581d40130680c1rbowen -- create list of theorems, selectable for proving
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf let thmSl =
a547340d7d0f0e79c9ba921c7dec7b18d0c800ffrbowen map (\ (nm, bp) ->
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf let gSt = maybe GOpen basicProofToGStatus bp
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf in checkboxElement (nm ++ " (" ++ showSimple gSt ++ ")")
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf [ mkAttr "name" $ escStr nm
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , mkAttr "unproven" $ showBool $ elem gSt [GOpen, GTimeout]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- select unproven, all or none theorems by button
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (btUnpr, btAll, btNone, jvScr1) = showSelectionButtons True
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- create prove button and prover/comorphism selection
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (prSl, cmrSl, jvScr2) <- showProverSelection GlProofs [sublogicOfTh gTh]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf let (prBt, timeout) = showProveButton True
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- hidden param field
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf hidStr = add_attrs [ mkAttr "name" "prove"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , mkAttr "type" "hidden", mkAttr "style" "display:none;"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf , mkAttr "value" $ show i ] inputNode
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -- combine elements within a form
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf add_attrs [ mkAttr "name" "thmSel", mkAttr "method" "get"]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf . add_attr (mkAttr "class" "ui form") $ unode "form"
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf $ add_attr (mkAttr "class" "ui relaxed grid container left aligned") $ unode "div"
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin $ [ add_attr (mkAttr "class" "row") $ unode "div" [hidStr, prSl, cmrSl]
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin , add_attr (mkAttr "class" "row") $ unode "div" [btUnpr, btAll, btNone, timeout]
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , add_attr (mkAttr "class" "row") $ unode "div" thmSl
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin , add_attr (mkAttr "class" "row") $ unode "div" prBt
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin -- save dg and return to svg-view
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin goBack = linkButtonElement ('/' : show sessId) "Return to DGraph"
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin return $ htmlPage fstLine (jvScr1 ++ jvScr2)
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , htmlRow $ unode "h4" "Theorems"
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin , htmlRow $ unode "h4" "Theory"
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin ] $ "<pre>\n" ++ sbShow ++ "\n<br />" ++ thShow ++ "\n</pre>\n"
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin-- | show window of the autoproof function
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrinshowAutoProofWindow :: DGraph -> Int -> ProverMode
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin -> ResultT IO (String, String)
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrinshowAutoProofWindow dg sessId prOrCons = let
e797af4d7b0cada1278d72d6c8ac77210ef78632minfrin dgnodes = labNodesDG dg
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin -- some parameters need to be different for consistency and autoproof mode
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor (prMethod, isProver, title, nodeSel) = case prOrCons of
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin GlProofs -> ("proof", True, "automatic proofs"
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin , map (\ fn -> add_attrs [ mkAttr "type" "checkbox"
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin , mkAttr "unproven" $ showBool $ not $ allProved fn
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin , mkAttr "name" $ escStr $ name fn ]
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin $ unode "input" $ showHtml fn) $ initFNodes dgnodes)
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin -- TODO sort out nodes with no sentences!
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin GlConsistency -> ("cons", False, "consistency checker"
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin , map (\ (_, dgn) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let cstat = getConsistencyOf dgn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nm = getDGNodeName dgn in add_attrs [ mkAttr "type" "checkbox"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "unproven" $ showBool $ sType cstat == CSUnchecked
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "name" nm]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ unode "input" (cStatusToPrefix cstat ++ nm)) dgnodes)
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener -- generate param field for the query string, invisible to the user
fe64b2ba25510d8c9dba5560a2d537763566cf40nd hidStr = add_attrs [ mkAttr "name" "autoproof"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "type" "hidden", mkAttr "style" "display:none;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "value" prMethod ] inputNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- select unproven, all or no nodes by button
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (btUnpr, btAll, btNone, jvScr1) = showSelectionButtons isProver
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (prBt, timeout) = showProveButton isProver
fe64b2ba25510d8c9dba5560a2d537763566cf40nd include = add_attrs [ mkAttr "type" "checkbox", mkAttr "checked" "true"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , mkAttr "name" "includetheorems"] $ unode "input" "include Theorems"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive goBack = aRef ('/' : show sessId) "return to DGraph"
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener (jvScr2, nodeMenu) <- case dgnodes of
fb77c505254b6e9c925e23e734463e87574f8f40kess -- return simple feedback if no nodes are present
c976a7c7d20f2be319b128dd7d0b1568da224c0arbowen [] -> return ("", plain "nothing to prove (graph has no nodes)")
fb77c505254b6e9c925e23e734463e87574f8f40kess -- otherwise
fb77c505254b6e9c925e23e734463e87574f8f40kess (_, nd) : _ -> case maybeResult $ getGlobalTheory nd of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> fail $ "cannot compute global theory of:\n" ++ show nd
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just gTh -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let br = unode "br " ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (prSel, cmSel, jvSc) <- lift $ showProverSelection prOrCons
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [sublogicOfTh gTh]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (jvSc, add_attrs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ mkAttr "name" "nodeSel", mkAttr "method" "get" ]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . unode "form" $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ hidStr, prSel, cmSel, br, btAll, btNone, btUnpr, timeout
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , include ] ++ intersperse br (prBt : nodeSel))
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return (htmlC, htmlPage title (jvScr1 ++ jvScr2)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ goBack, plain " ", nodeMenu ] "")
fb77c505254b6e9c925e23e734463e87574f8f40kessshowProveButton :: Bool -> (Element, Element)
fb77c505254b6e9c925e23e734463e87574f8f40kessshowProveButton isProver = (prBt, timeout) where
06ba4a61654b3763ad65f52283832ebf058fdf1cslive prBt = add_attrs
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ mkAttr "type" "submit"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "class" "ui button"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "value" $ if isProver then "Prove" else "Check"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ] inputNode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- create timeout field
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd timeout = add_attr (mkAttr "class" "three wide field") $ unode "div"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ unode "label" "Timeout (Sec/Goal)"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , add_attrs
db99fa79ac42b9cc42b63386eb289aecb0f3cb9cnd [ mkAttr "type" "text"
db99fa79ac42b9cc42b63386eb289aecb0f3cb9cnd , mkAttr "name" "timeout"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , mkAttr "placeholder" "Timeout (Sec/Goal)"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , mkAttr "value" "1"
db99fa79ac42b9cc42b63386eb289aecb0f3cb9cnd ] $ unode "input" ""
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluem-- | select unproven, all or none theorems by button
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluemshowSelectionButtons :: Bool -> (Element, Element, Element, String)
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluemshowSelectionButtons isProver = (selUnPr, selAll, selNone, jvScr)
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluem where prChoice = if isProver then "SPASS" else "darwin"
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluem selUnPr = add_attrs
8010b66c363b5b847dc83d9d23f12c68e5bf3a56rpluem [ mkAttr "type" "button"
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener , mkAttr "class" "ui button"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , mkAttr "value" $ if isProver then "Unproven" else "Unchecked"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , mkAttr "onClick" "chkUnproven()"
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener ] inputNode
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener selAll = add_attrs
a5f060e0c74a44cb8896ae794c08f94f7c9a46a7covener [ mkAttr "type" "button", mkAttr "value" "All"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "class" "ui button"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "onClick" "chkAll(true)"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ] inputNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd selNone = add_attrs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [ mkAttr "type" "button", mkAttr "value" "None"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "class" "ui button"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , mkAttr "onClick" "chkAll(false)"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ] inputNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- javascript features
fe64b2ba25510d8c9dba5560a2d537763566cf40nd jvScr = unlines
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- select unproven goals by button
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [ "\nfunction chkUnproven() {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var e = document.forms[0].elements;"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " for (i = 0; i < e.length; i++) {"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , " if( e[i].type == 'checkbox'"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , " && e[i].name != 'includetheorems' )"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , " e[i].checked = e[i].getAttribute('unproven') == 'true';"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess -- select or deselect all theorems by button
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , "}\nfunction chkAll(b) {"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " var e = document.forms[0].elements;"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " for (i = 0; i < e.length; i++) {"
97a9a944b5887e91042b019776c41d5dd74557aferikabele , " if( e[i].type == 'checkbox'"
97a9a944b5887e91042b019776c41d5dd74557aferikabele , " && e[i].name != 'includetheorems' ) e[i].checked = b;"
97a9a944b5887e91042b019776c41d5dd74557aferikabele -- autoselect SPASS if possible
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , "}\nwindow.onload = function() {"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " prSel = document.forms[0].elements.namedItem('prover');"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , " prs = prSel.getElementsByTagName('option');"
fb77c505254b6e9c925e23e734463e87574f8f40kess , " for ( i=0; i<prs.length; i++ ) {"
d1348237b33bc1755b9f1165eea52317465a7671nd , " if( prs[i].value == '" ++ prChoice ++ "' ) {"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , " prs[i].selected = 'selected';"
d1348237b33bc1755b9f1165eea52317465a7671nd , " updCmSel('" ++ prChoice ++ "');"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " return;"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- if SPASS unable, select first one in list
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , " prs[0].selected = 'selected';"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , " updCmSel( prs[0].value );"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | create prover and comorphism menu and combine them using javascript
97a9a944b5887e91042b019776c41d5dd74557aferikabeleshowProverSelection :: ProverMode -> [G_sublogics]
fb77c505254b6e9c925e23e734463e87574f8f40kess -> IO (Element, Element, String)
fb77c505254b6e9c925e23e734463e87574f8f40kessshowProverSelection prOrCons subLs = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let jvScr = unlines
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- the chosen prover is passed as param
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [ "\nfunction updCmSel(pr) {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var cmrSl = document.forms[0].elements.namedItem('translation');"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess -- then, all selectable comorphisms are gathered and iterated
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess , " var opts = cmrSl.getElementsByTagName('option');"
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess -- try to keep current comorph-selection
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var selAccept = false;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " for( var i = opts.length-1; i >= 0; i-- ) {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var cmr = opts.item( i );"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- the list of supported provers is extracted
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var prs = cmr.getAttribute('4prover').split(';');"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " var pFit = false;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " for( var j = 0; ! pFit && j < prs.length; j++ ) {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " pFit = prs[j] == pr;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- if prover is supported, remove disabled attribute
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " if( pFit ) {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " cmr.removeAttribute('disabled');"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " selAccept = selAccept || cmr.selected;"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- else create and append a disabled attribute
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , " } else {"
6b64034fa2a644ba291c484c0c01c7df5b8d982ckess , " var ds = document.createAttribute('disabled');"
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor , " ds.value = 'disabled';"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -- check if selected comorphism fits, and select fst. in list otherwise
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , " if( ! selAccept ) {"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " for( i = 0; i < opts.length; i++ ) {"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , " if( ! opts.item(i).disabled ) {"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " opts.item(i).selected = 'selected';"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , " return;"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd pcs <- mapM (liftM proversToStringAux . (case prOrCons of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlProofs -> getProversAux
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlConsistency -> getConsCheckersAux) Nothing) subLs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let allPrCm = nub $ concat pcs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- create prover selection (drop-down)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd prs = add_attr (mkAttr "class" "eight wide column") $ unode "div" $
604c89126c27104f659d7a51b0113e3bd435faf8fielding singleSelectionDropDown "Prover" "prover" Nothing $
604c89126c27104f659d7a51b0113e3bd435faf8fielding map (\ p ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (p, p, [mkAttr "onClick" $ "updCmSel('" ++ p ++ "')"])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ) $ showProversOnly allPrCm
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- create comorphism selection (drop-down)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd cmrs = add_attr (mkAttr "class" "eight wide column") $ unode "div" $
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen singleSelectionDropDown "Translation" "translation" Nothing $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd map (\ (cm, ps) -> let c = showComorph cm in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (c, c, [mkAttr "4prover" $ intercalate ";" ps])
fb77c505254b6e9c925e23e734463e87574f8f40kess return (prs, cmrs, jvScr)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowHtml :: FNode -> String
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowHtml fn = name fn ++ " " ++ goalsToPrefix (toGtkGoals fn)
fb77c505254b6e9c925e23e734463e87574f8f40kessgetAllAutomaticProvers :: G_sublogics -> IO [(G_prover, AnyComorphism)]
fb77c505254b6e9c925e23e734463e87574f8f40kessgetAllAutomaticProvers subL =
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd getUsableProvers ProveCMDLautomatic subL logicGraph
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndfilterByProver :: Maybe String -> [(G_prover, AnyComorphism)]
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -> [(G_prover, AnyComorphism)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilterByProver mp = case mp of
604c89126c27104f659d7a51b0113e3bd435faf8fielding Nothing -> id
604c89126c27104f659d7a51b0113e3bd435faf8fielding Just p -> filter ((== p) . mkNiceProverName . getProverName . fst)
7654193c1faf603feec999850322ad79e6c551bcndfilterByComorph :: Maybe String -> [(a, AnyComorphism)]
604c89126c27104f659d7a51b0113e3bd435faf8fielding -> [(a, AnyComorphism)]
604c89126c27104f659d7a51b0113e3bd435faf8fieldingfilterByComorph mt = case mt of
c97e8972ab1f4dd167e3dc4db87daf91114009fbnd Nothing -> id
7654193c1faf603feec999850322ad79e6c551bcnd Just c -> filter ((== c) . showComorph . snd)
7654193c1faf603feec999850322ad79e6c551bcndgetProverAndComorph :: Maybe String -> Maybe String -> G_sublogics
7654193c1faf603feec999850322ad79e6c551bcnd -> IO [(G_prover, AnyComorphism)]
7654193c1faf603feec999850322ad79e6c551bcndgetProverAndComorph mp mc subL = do
7654193c1faf603feec999850322ad79e6c551bcnd ps <- getFilteredProvers mc subL
7654193c1faf603feec999850322ad79e6c551bcnd let spps = case filterByProver (Just "SPASS") ps of
7654193c1faf603feec999850322ad79e6c551bcnd fps -> fps
7654193c1faf603feec999850322ad79e6c551bcnd return $ case mp of
7654193c1faf603feec999850322ad79e6c551bcnd Nothing -> spps
7654193c1faf603feec999850322ad79e6c551bcnd _ -> filterByProver mp ps
7654193c1faf603feec999850322ad79e6c551bcndgetProverList :: ProverMode -> Maybe String -> G_sublogics
7654193c1faf603feec999850322ad79e6c551bcnd -> IO [(AnyComorphism, [ProverOrConsChecker])]
7654193c1faf603feec999850322ad79e6c551bcndgetProverList mp mt subL = case mp of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlProofs -> getProversAux mt subL
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf GlConsistency -> getConsCheckersAux mt subL
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorgetFullProverList :: ProverMode -> Maybe String -> DGraph
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf -> IO [(AnyComorphism, [ProverOrConsChecker])]
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csfgetFullProverList mp mt = foldM
29b517f9fe7f32a2c3fbdc53e359b6db6f8e8c2csf (\ ls (_, nd) -> maybe (return ls) (fmap (++ ls) . case mp of
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener GlProofs -> getProversAux mt
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener GlConsistency -> getConsCheckersAux mt
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener . sublogicOfTh)
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener $ maybeResult $ getGlobalTheory nd) [] . labNodesDG
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenergroupOnSnd :: Eq b => (a -> c) -> [(a, b)] -> [(b, [c])]
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenergroupOnSnd f =
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener map (\ l@((_, b) : _) -> (b, map (f . fst) l)) . groupBy (on (==) snd)
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenerproversToStringAux :: [(AnyComorphism, [ProverOrConsChecker])]
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener -> [(AnyComorphism, [String])]
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenerproversToStringAux = map (\ (x, ps) ->
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener (x, map (mkNiceProverName . internalProverName) ps))
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener{- | gather provers and comorphisms and resort them to
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covener(comorhism, supported provers) while not changing orig comorphism order -}
031bbbc0d1189b07330e38d0c126820a9ab7795egryzorgetProversAux :: Maybe String -> G_sublogics
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalic -> IO [(AnyComorphism, [ProverOrConsChecker])]
c3e2e664a67b1adb9b6a6b91ff161f4f562cecf6covenergetProversAux mt x =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd fmap (groupOnSnd AbsState.Prover) $ getFilteredProvers mt x
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetFilteredProvers :: Maybe String -> G_sublogics
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> IO [(G_prover, AnyComorphism)]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetFilteredProvers mt = fmap (filterByComorph mt) . getAllAutomaticProvers
fb77c505254b6e9c925e23e734463e87574f8f40kessformatProvers :: ProverMode -> [(AnyComorphism, [String])] -> String
fe64b2ba25510d8c9dba5560a2d537763566cf40ndformatProvers pm = let
fe64b2ba25510d8c9dba5560a2d537763566cf40nd tag = case pm of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlProofs -> "prover"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlConsistency -> "consistency-checker"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in ppTopElement . unode (tag ++ "s") . map (unode tag)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . showProversOnly
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess-- | retrieve a list of consistency checkers
9b5e2c5e769dc678a1aca06df75c32022b2f1492trawickgetConsCheckersAux :: Maybe String -> G_sublogics
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> IO [(AnyComorphism, [ProverOrConsChecker])]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetConsCheckersAux mt =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive fmap (groupOnSnd AbsState.ConsChecker) . getFilteredConsCheckers mt
cb3a1082aec4b3b4f4ed238c93c3cc54933a7f0endgetFilteredConsCheckers :: Maybe String -> G_sublogics
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> IO [(G_cons_checker, AnyComorphism)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetFilteredConsCheckers mt = fmap
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (filterByComorph mt . filter (getCcBatch . fst))
fb77c505254b6e9c925e23e734463e87574f8f40kess . getConsCheckers . findComorphismPaths logicGraph
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetComorphs :: Maybe String -> G_sublogics -> IO [(G_prover, AnyComorphism)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetComorphs mp = fmap (filterByProver mp)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . getAllAutomaticProvers
fb77c505254b6e9c925e23e734463e87574f8f40kessgetFullComorphList :: DGraph -> IO [(G_prover, AnyComorphism)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetFullComorphList = foldM
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (\ ls (_, nd) -> maybe (return ls)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (fmap (++ ls) . getAllAutomaticProvers . sublogicOfTh)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ maybeResult $ getGlobalTheory nd) [] . labNodesDG
9bcfc3697a91b5215893a7d0206865b13fc72148ndformatComorphs :: [(G_prover, AnyComorphism)] -> String
9bcfc3697a91b5215893a7d0206865b13fc72148ndformatComorphs = ppTopElement . unode "translations"
9bcfc3697a91b5215893a7d0206865b13fc72148nd . map (unode "comorphism") . nubOrd . map (showComorph . snd)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndconsNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab)
db8dceaf53a26fba6048c2ad4d86c5507344187drbowen -> G_sublogics -> Bool -> Maybe String -> Maybe String -> Maybe Int
db8dceaf53a26fba6048c2ad4d86c5507344187drbowen -> ResultT IO (LibEnv, [ProofResult])
db8dceaf53a26fba6048c2ad4d86c5507344187drbowenconsNode le ln dg nl@(i, lb) subL useTh mp mt tl = do
db8dceaf53a26fba6048c2ad4d86c5507344187drbowen (cc, c) <- liftIO $ findConsChecker mt subL mp
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl cstat <- consistencyCheck useTh cc c ln le dg nl $ fromMaybe 1 tl
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl -- Consistency Results are stored in LibEnv via DGChange object
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl let cSt = sType cstat
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl le'' = if cSt == CSUnchecked then le else
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl Map.insert ln (changeDGH dg $ SetNodeLab lb
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl (i, case cSt of
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl CSInconsistent -> markNodeInconsistent "" lb
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl CSConsistent -> markNodeConsistent "" lb
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl _ -> lb)) le
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl return (le'', [(" ", drop 2 $ show cSt, show cstat,
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl AbsState.ConsChecker cc, c, Nothing, Just $ sMessage cstat)])
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodlfindConsChecker :: Maybe String -> G_sublogics -> Maybe String
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl -> IO (G_cons_checker, AnyComorphism)
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodlfindConsChecker translationM gSublogic consCheckerNameM = do
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl consList <- getFilteredConsCheckers translationM gSublogic
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl let findCC x = filter ((== x ) . getCcName . fst) consList
8559a67073808d84d85bb5dd552d4247caafe709sf consCheckersL = maybe (findCC "darwin") findCC consCheckerNameM
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl case consCheckersL of
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl [] -> fail "no cons checker found"
8559a67073808d84d85bb5dd552d4247caafe709sf (gConsChecker, comorphism) : _ -> return (gConsChecker, comorphism)
8559a67073808d84d85bb5dd552d4247caafe709sfreasonREST :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> ProverMode
8559a67073808d84d85bb5dd552d4247caafe709sf -> String -> ReasoningParameters
8559a67073808d84d85bb5dd552d4247caafe709sf -> ResultT IO (LibEnv, [(String, [ProofResult])])
8559a67073808d84d85bb5dd552d4247caafe709sfreasonREST opts libEnv libName dGraph_ proverMode location reasoningParameters = do
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic reasoningCacheE <- liftIO buildReasoningCache
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic failOnLefts reasoningCacheE
011e567af90fe9d72bbabf8cc5e373b4436b9d08rbowen let reasoningCache1 = rights reasoningCacheE
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic reasoningCache2 <- liftIO $ PGIP.Server.setupReasoning opts reasoningCache1
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic (libEnv', cacheGoalsAndProofResults) <-
8559a67073808d84d85bb5dd552d4247caafe709sf PGIP.Server.performReasoning opts libEnv libName
8559a67073808d84d85bb5dd552d4247caafe709sf dGraph_ location reasoningCache2
8559a67073808d84d85bb5dd552d4247caafe709sf let nodesAndProofResults = map
8559a67073808d84d85bb5dd552d4247caafe709sf (\ (nodeLabel, proofResults) ->
8559a67073808d84d85bb5dd552d4247caafe709sf (show (getName $ dgn_name nodeLabel), proofResults)
1a0ca5f6b566a5eb77d63f466fcf78fb388a4182igalic cacheGoalsAndProofResults
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl return (libEnv', nodesAndProofResults)
c8c717fafa0a09ed13469a603a178921b851dd22igalic useDatabase :: Bool
c8c717fafa0a09ed13469a603a178921b851dd22igalic useDatabase = format reasoningParameters == Just "db"
8559a67073808d84d85bb5dd552d4247caafe709sf failOnLefts :: ReasoningCacheE -> ResultT IO ()
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl failOnLefts reasoningCache =
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl let lefts_ = lefts reasoningCache
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl in unless (null lefts_) $ fail $ unlines lefts_
8559a67073808d84d85bb5dd552d4247caafe709sf buildReasoningCache :: IO ReasoningCacheE
8559a67073808d84d85bb5dd552d4247caafe709sf buildReasoningCache =
3cc4ff86e6cc4cfd7d4ccfc58dedff599091444bnoodl let reasoningParametersGroupedByNodeName =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd groupBy (\ a b ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ) $ ReasoningParameters.goals reasoningParameters
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in foldM buildReasoningCacheForNode [] reasoningParametersGroupedByNodeName
fe64b2ba25510d8c9dba5560a2d537763566cf40nd buildReasoningCacheForNode :: ReasoningCacheE
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> IO ReasoningCacheE
fe64b2ba25510d8c9dba5560a2d537763566cf40nd buildReasoningCacheForNode reasoningCacheE goalConfigsOfSameNode =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let nodeName = ReasoningParameters.node $ head goalConfigsOfSameNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nodeM = find (\ (_, nodeLabel) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd showName (dgn_name nodeLabel) == nodeName
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ) $ labNodesDG dGraph_
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd in case nodeM of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Nothing ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return (Left ("Node \"" ++ nodeName ++ "\" not found")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd : reasoningCacheE)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just node_@(_, nodeLabel) -> do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let gTheoryM = maybeResult $ getGlobalTheory nodeLabel
06ba4a61654b3763ad65f52283832ebf058fdf1cslive gTheory <- case gTheoryM of
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Nothing ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive fail ("Cannot compute global theory of: "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ showName (dgn_name nodeLabel) ++ "\n")
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Just gTheory -> return gTheory
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let gSublogic = sublogicOfTh gTheory
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd foldM (buildReasoningCacheForGoal nodeName node_ gTheory gSublogic)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive reasoningCacheE goalConfigsOfSameNode
06ba4a61654b3763ad65f52283832ebf058fdf1cslive buildReasoningCacheForGoal :: String
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> (Int, DGNodeLab)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -> G_theory
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> G_sublogics
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd -> ReasoningCacheE
9597f440430d8c876dd64f5f78066804650a18ecnoodl -> IO ReasoningCacheE
9597f440430d8c876dd64f5f78066804650a18ecnoodl buildReasoningCacheForGoal nodeName node_ gTheory gSublogic reasoningCacheE goalConfig =
9597f440430d8c876dd64f5f78066804650a18ecnoodl let reasonerM = reasoner $ reasonerConfiguration goalConfig
06ba4a61654b3763ad65f52283832ebf058fdf1cslive translationM = translation goalConfig
06ba4a61654b3763ad65f52283832ebf058fdf1cslive reasonerConfiguration goalConfig
06ba4a61654b3763ad65f52283832ebf058fdf1cslive caseReasoningCacheEntry = ReasoningCacheGoal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive { rceProverMode = proverMode
130d299c4b2b15be45532a176604c71fdc7bea5bnd , rceNode = node_
46f74e65e6051e6e9391c8e17c5116317210facetakashi , rceGoalNameM = Nothing
130d299c4b2b15be45532a176604c71fdc7bea5bnd , rceGoalConfig = goalConfig
130d299c4b2b15be45532a176604c71fdc7bea5bnd , rceGTheory = gTheory
130d299c4b2b15be45532a176604c71fdc7bea5bnd , rceGSublogic = gSublogic
130d299c4b2b15be45532a176604c71fdc7bea5bnd , rceReasoner = undefined -- will be overwritten a few lines below
46f74e65e6051e6e9391c8e17c5116317210facetakashi , rceComorphism = undefined -- will be overwritten a few lines below
46f74e65e6051e6e9391c8e17c5116317210facetakashi , rceTimeLimit = timeLimit_
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi , rceUseDatabase = useDatabase
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi , rceReasonerConfigurationKeyM = Nothing
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi , rceReasoningAttemptKeyM = Nothing
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi in case proverMode of
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi GlConsistency -> do
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi (gConsChecker, comorphism) <-
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi findConsChecker translationM gSublogic reasonerM
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi return ((Right $ caseReasoningCacheEntry
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi { rceReasoner = AbsState.ConsChecker gConsChecker
78f97ce162b66a0dbfd7af4dcd9984f162569b04minfrin , rceComorphism = comorphism
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi ) : reasoningCacheE)
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi GlProofs -> do
6f93a0120b20c42e90d5ab61766c0e36fc024636takashi proversAndComorphisms <-
130d299c4b2b15be45532a176604c71fdc7bea5bnd getProverAndComorph reasonerM translationM gSublogic
130d299c4b2b15be45532a176604c71fdc7bea5bnd (gProver, comorphism) <- case proversAndComorphisms of
130d299c4b2b15be45532a176604c71fdc7bea5bnd [] -> fail ("No matching translation or prover found for "
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ++ nodeName ++ "\n")
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (gProver, comorphism) : _ ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return (gProver, comorphism)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let possibleGoalNames = map fst $ getThGoals gTheory :: [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let goalNames = (case conjecture goalConfig of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> possibleGoalNames
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just goalName_ ->
a850a44a7d6af013c766944483e00c2a1c8b183dnd filter (== goalName_) possibleGoalNames) :: [String]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (map (\ goalName_ -> Right $ caseReasoningCacheEntry
fe64b2ba25510d8c9dba5560a2d537763566cf40nd { rceGoalNameM = Just goalName_
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , rceReasoner = AbsState.Prover gProver
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , rceComorphism = comorphism
a850a44a7d6af013c766944483e00c2a1c8b183dnd ) goalNames ++ reasoningCacheE)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndsetupReasoning :: HetcatsOpts -> ReasoningCache -> IO ReasoningCache
fb77c505254b6e9c925e23e734463e87574f8f40kesssetupReasoning opts reasoningCache =
fb77c505254b6e9c925e23e734463e87574f8f40kess mapM (\ reasoningCacheGoal -> do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd reasoningConfigurationKey <-
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Persistence.Reasoning.setupReasoning opts reasoningCacheGoal
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return reasoningCacheGoal
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd { rceReasonerConfigurationKeyM = reasoningConfigurationKey }
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ) reasoningCache
06ba4a61654b3763ad65f52283832ebf058fdf1csliveperformReasoning :: HetcatsOpts -> LibEnv -> LibName -> DGraph
a850a44a7d6af013c766944483e00c2a1c8b183dnd -> String -> ReasoningCache
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> ResultT IO (LibEnv, [(DGNodeLab, [ProofResult])])
06ba4a61654b3763ad65f52283832ebf058fdf1csliveperformReasoning opts libEnv libName dGraph_ location reasoningCache = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (libEnv', nodesAndProofResults') <- liftIO $ foldM
a850a44a7d6af013c766944483e00c2a1c8b183dnd (\ (libEnvAcc1, nodesAndProofResults1) reasoningCacheGoalsByNode -> do
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen let nodeLabel = snd $ rceNode $ head reasoningCacheGoalsByNode
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (libEnvAcc2, proofResults2) <-
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (\ (libEnvAcc3, proofResults3) reasoningCacheGoal -> do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- update state
a850a44a7d6af013c766944483e00c2a1c8b183dnd let gTheoryM = maybeResult $ getGlobalTheory nodeLabel
a850a44a7d6af013c766944483e00c2a1c8b183dnd gTheory_ <- case gTheoryM of
a850a44a7d6af013c766944483e00c2a1c8b183dnd Nothing ->
a850a44a7d6af013c766944483e00c2a1c8b183dnd fail ("Cannot compute global theory of: "
a850a44a7d6af013c766944483e00c2a1c8b183dnd ++ showName (dgn_name nodeLabel) ++ "\n")
bea526116133aa3d7dabd1924bfc580b37fbf22aslive Just gTheory_ -> return gTheory_
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let reasoningCacheGoal' = reasoningCacheGoal { rceGTheory = gTheory_ }
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- preprocess (with database)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (premisesM, reasoningCacheGoal3) <-
bea526116133aa3d7dabd1924bfc580b37fbf22aslive Persistence.Reasoning.preprocessReasoning opts location
bea526116133aa3d7dabd1924bfc580b37fbf22aslive reasoningCacheGoal'
fb77c505254b6e9c925e23e734463e87574f8f40kess -- run the reasoner
bea526116133aa3d7dabd1924bfc580b37fbf22aslive Result _ (Just (libEnvAcc4, proofResult : _)) <- runResultT $
bea526116133aa3d7dabd1924bfc580b37fbf22aslive runReasoning libEnvAcc3 libName dGraph_ reasoningCacheGoal3 premisesM
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- postprocess (with database)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Persistence.Reasoning.postprocessReasoning opts reasoningCacheGoal3
fe64b2ba25510d8c9dba5560a2d537763566cf40nd premisesM proofResult
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- update state
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let proofResults4 = proofResult : proofResults3
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen return (libEnvAcc4, proofResults4)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (libEnvAcc1, [])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd reasoningCacheGoalsByNode
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin return (libEnvAcc2, (nodeLabel, proofResults2) : nodesAndProofResults1)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (libEnv, []) $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive groupBy sameNode reasoningCache
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (libEnv', nodesAndProofResults')
5b258a8d58679c6587757189339bb3c2d0488f93poirier sameNode :: ReasoningCacheGoal -> ReasoningCacheGoal -> Bool
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin sameNode a b = fst (rceNode a) == fst (rceNode b)
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrinrunReasoning :: LibEnv -> LibName -> DGraph
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen -> ReasoningCacheGoal -> Maybe [String]
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin -> ResultT IO (LibEnv, [ProofResult])
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrinrunReasoning libEnv libName dGraph_ reasoningCacheGoal premisesM =
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin let node_ = rceNode reasoningCacheGoal
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin gTheory_ = rceGTheory reasoningCacheGoal
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin gSublogic = rceGSublogic reasoningCacheGoal
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin useTheorems_ = fromMaybe True $ useTheorems $ rceGoalConfig reasoningCacheGoal
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen reasonerM = reasoner $ reasonerConfiguration $ rceGoalConfig reasoningCacheGoal
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen translationM = translation $ rceGoalConfig reasoningCacheGoal
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen timeLimitM = Just $ ReasoningParameters.timeLimit $ reasonerConfiguration $
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen rceGoalConfig reasoningCacheGoal
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen goalName_ = fromJust $ rceGoalNameM reasoningCacheGoal
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen premises = fromMaybe [] premisesM
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen in case rceProverMode reasoningCacheGoal of
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen GlConsistency -> consNode libEnv libName dGraph_ node_ gSublogic
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen useTheorems_ reasonerM translationM timeLimitM
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen GlProofs -> proveNode libEnv libName dGraph_ node_ gTheory_ gSublogic
2bb4320391b88748dc6e851deca941b058231664rbowen useTheorems_ reasonerM translationM timeLimitM [goalName_] premises
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowenproveNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab)
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> G_theory -> G_sublogics -> Bool
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> Maybe String -> Maybe String -> Maybe Int
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> [String] -> [String]
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> ResultT IO (LibEnv, [ProofResult])
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowenproveNode le ln dg nl gTh subL useTh mp mt tl thms axioms = do
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin ps <- lift $ getProverAndComorph mp mt subL
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen [] -> fail "no matching translation or prover found"
cd75115baac4df586f9a346dc1c2c9d9bd3d58aaminfrin cp : _ -> do
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor let ks = map fst $ getThGoals gTh
06ba4a61654b3763ad65f52283832ebf058fdf1cslive unless (Set.null diffs) . fail $ "unknown theorems: " ++ show diffs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive when (null thms && null ks) $ fail "no theorems to prove"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let selectedGoals_ = if null thms then ks else thms
7b5535ed88e0f561b3bfb3330137bd804846afd4slive let timeLimit_ = maybe 1 (max 1) tl
7b5535ed88e0f561b3bfb3330137bd804846afd4slive (nTh, sens, proofStatuses) <- do
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let premises = axioms
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ((nTh, sens), (_, proofStatuses)) <-
7b5535ed88e0f561b3bfb3330137bd804846afd4slive autoProofAtNode useTh timeLimit_ selectedGoals_ premises gTh cp
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return (nTh, sens, proofStatuses)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return ( if null sens
7b5535ed88e0f561b3bfb3330137bd804846afd4slive else Map.insert ln ( updateLabelTheory le ln dg nl nTh) le
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , combineToProofResult sens cp proofStatuses
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowencombineToProofResult :: [(String, String, String)] -> (G_prover, AnyComorphism)
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> [ProofStatus G_proof_tree] -> [ProofResult]
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowencombineToProofResult sens (prover, comorphism) proofStatuses = let
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor findProofStatusByName :: String -> Maybe (ProofStatus G_proof_tree)
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin findProofStatusByName n =
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen case filter ((n ==) . goalName) proofStatuses of
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin [] -> Nothing
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin (ps : _) -> Just ps
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin combineSens :: (String, String, String) -> ProofResult
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen combineSens (n, e, d) = (n, e, d, AbsState.Prover prover, comorphism,
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen findProofStatusByName n, Nothing)
09b49da7bdbc59b56fb52d19a092e30d7d4a1bbaminfrin in map combineSens sens
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen-- run over multiple dgnodes and prove available goals for each
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowenproveMultiNodes :: ProverMode -> LibEnv -> LibName -> DGraph
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor -> Bool -> Maybe String -> Maybe String -> Maybe Int -> [String] -> [String]
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> ResultT IO (LibEnv, [(String, [ProofResult])])
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowenproveMultiNodes pm le ln dg useTh mp mt tl nodeSel axioms = let
cd75115baac4df586f9a346dc1c2c9d9bd3d58aaminfrin runProof :: LibEnv -> G_theory -> (Int, DGNodeLab)
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen -> ResultT IO (LibEnv, [ProofResult])
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen runProof le' gTh nl = let
d68b7e44d489058bcb5b18992a0f247a80f52f9frbowen subL = sublogicOfTh gTh
cd75115baac4df586f9a346dc1c2c9d9bd3d58aaminfrin dg' = lookupDGraph ln le' in case pm of
cd75115baac4df586f9a346dc1c2c9d9bd3d58aaminfrin GlConsistency -> consNode le' ln dg' nl subL useTh mp mt tl
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlProofs ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd proveNode le' ln dg' nl gTh subL useTh mp mt tl
9bcfc3697a91b5215893a7d0206865b13fc72148nd (map fst $ getThGoals gTh) axioms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd nodes2check = filter (case nodeSel of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd [] -> case pm of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlConsistency -> const True
fe64b2ba25510d8c9dba5560a2d537763566cf40nd GlProofs -> hasOpenGoals . snd
fe64b2ba25510d8c9dba5560a2d537763566cf40nd _ -> (`elem` nodeSel) . getDGNodeName . snd) $ labNodesDG dg
fb77c505254b6e9c925e23e734463e87574f8f40kess (\ (le', res) nl@(_, dgn) ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case maybeResult $ getGlobalTheory dgn of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> fail $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd "cannot compute global theory of:\n" ++ show dgn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just gTh -> do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (le'', proofResults) <- runProof le' gTh nl
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (le'', (getDGNodeName dgn, proofResults) : res)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nodes2check
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessformatResultsAux :: Bool -> ProverMode -> String -> [ProofResult] -> Element
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessformatResultsAux xF pm nm sens = unode nm $ case (sens, pm) of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ([(_, e, d, _, _, _, _)], GlConsistency) | xF -> formatConsNode e d
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> add_attr (mkAttr "class" "results") $ unode "div" $ formatGoals xF sens
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkPath :: Session -> LibName -> Int -> String
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkPath sess l k =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive '/' : concat [ libToFileName l ++ "?session="
06ba4a61654b3763ad65f52283832ebf058fdf1cslive | l /= sessLibName sess ]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveextPath :: Session -> LibName -> Int -> String
06ba4a61654b3763ad65f52283832ebf058fdf1csliveextPath sess l k = mkPath sess l k ++
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if l /= sessLibName sess then "&" else "?"
7a9fd3b88382052ae000d95ff0d35a1f318d6b23pquernaglobalCommands :: [String]
4a31db3c3a0202003c1b9f87affa7cc143e120e5sfglobalCommands = map (cmdlGlobCmd . fst) allGlobLibAct
7a9fd3b88382052ae000d95ff0d35a1f318d6b23pquernasessAns :: LibName -> ResultT IO String -> (Session, Int)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> ResultT IO (String, String)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndsessAns libName svgComp (sess, k) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd svgComp >>= \ svg -> return $ sessAnsAux libName svg (sess, k)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndsessAnsAux :: LibName -> String -> (Session, Int) -> (String, String)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndsessAnsAux libName svg (sess, k) =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let libEnv = sessLibEnv sess
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ln = libToFileName libName
fe64b2ba25510d8c9dba5560a2d537763566cf40nd libref l =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ( aRef (mkPath sess l k) (libToFileName l)
50cb7e2b30597f481fee57bac945190f06ebcc58jorton , aRef (mkPath sess l k) "default"
ee1af2aeb57527f33baa4737aa431e4aef997855rbowen : map (\ d -> aRef (extPath sess l k ++ d) d) displayTypes
fe64b2ba25510d8c9dba5560a2d537763566cf40nd libPath = extPath sess libName k
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ref d = aRef (libPath ++ d) d
031bbbc0d1189b07330e38d0c126820a9ab7795egryzor autoProofBt = aRef ('/' : show k ++ "?autoproof") "automatic proofs"
88d86cfadffe2275a3dfb67a4d7bdc018630b661rbowen consBt = aRef ('/' : show k ++ "?consistency") "consistency checker"
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- the html quicklinks to nodes and edges have been removed with R.16827
50cb7e2b30597f481fee57bac945190f06ebcc58jorton ("Hets, the DOLiator - (" ++ shows k ")" ++ ln)
97a9a944b5887e91042b019776c41d5dd74557aferikabele [ add_attr (mkAttr "class" "row") (unode "div" $ unode "h1" ("Library " ++ ln))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , add_attr (mkAttr "class" "row") $ unode "div"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [ pageOptionsFormat "" libPath
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , dropDownElement "Tools" [autoProofBt, consBt]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , dropDownElement "Commands" (map ref globalCommands)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , dropDownToLevelsElement "Imported Libraries" $ map libref $ Map.keys libEnv
e23d878014f00a27b043a25e59f809c7af497e5ctakashi , add_attr (mkAttr "class" "row") $ unode "div" $ unode "h3" "Development Graph"
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetHetsLibContent :: HetcatsOpts -> String -> [QueryPair] -> IO [Element]
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetHetsLibContent opts dir query = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let hlibs = libdirs opts
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ds <- if null dir || isAbsolute dir then return hlibs else
fe64b2ba25510d8c9dba5560a2d537763566cf40nd filterM doesDirectoryExist $ map (</> dir) hlibs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd fs <- fmap (sortBy cmpFilePath . filter (not . isPrefixOf ".") . concat)
5f00eedb74adc88b8282475faf6275dad390c9a3rpluem $ mapM getDirContents ds
5f00eedb74adc88b8282475faf6275dad390c9a3rpluem return $ map (mkHtmlRef query) $ getParent dir : fs
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetParent :: String -> String
fe64b2ba25510d8c9dba5560a2d537763566cf40ndgetParent = addTrailingPathSeparator . ("/" </>) . takeDirectory
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . dropTrailingPathSeparator
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | a variant that adds a trailing slash
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetDirContents :: FilePath -> IO [FilePath]
130d299c4b2b15be45532a176604c71fdc7bea5bndgetDirContents d = do
06ba4a61654b3763ad65f52283832ebf058fdf1cslive fs <- getDirectoryContents d
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mapM (\ f -> doesDirectoryExist (d </> f) >>= \ b -> return
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ if b then addTrailingPathSeparator f else f) fs
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessaRef :: String -> String -> Element
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessaRef lnk txt = add_attr (mkAttr "href" lnk) $ unode "a" txt
313bb560bc5c323cfd40c9cad7335b4b8e060aedkessmkHtmlRef :: [QueryPair] -> String -> Element
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkHtmlRef query entry = unode "dir" $ aRef
130d299c4b2b15be45532a176604c71fdc7bea5bnd (entry ++ if null query then "" else '?' : intercalate "&"
130d299c4b2b15be45532a176604c71fdc7bea5bnd (map (\ (x, ms) -> x ++ maybe "" ('=' :) ms) query)) entry
130d299c4b2b15be45532a176604c71fdc7bea5bndplain :: String -> Element
130d299c4b2b15be45532a176604c71fdc7bea5bndplain = unode "p"
130d299c4b2b15be45532a176604c71fdc7bea5bndinputNode :: Element
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndinputNode = unode "input" ()
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cndsubmitButton :: Element
6c5c651b0b97607b8c8b4965c1385c67699f217fndsubmitButton = add_attrs
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd [ mkAttr "type" "submit"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "value" "submit"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , mkAttr "class" "ui button"
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd ] inputNode
5f00eedb74adc88b8282475faf6275dad390c9a3rpluemmkForm :: String -> [Element] -> Element
4bb78e7cdd53f50240cff4ad7a97c7ed36483797slive add_attrs [ mkAttr "action" a
5f00eedb74adc88b8282475faf6275dad390c9a3rpluem , mkAttr "enctype" "multipart/form-data"
5f00eedb74adc88b8282475faf6275dad390c9a3rpluem , mkAttr "method" "post"
4bb78e7cdd53f50240cff4ad7a97c7ed36483797slive , mkAttr "class" "ui basic form"
4bb78e7cdd53f50240cff4ad7a97c7ed36483797slive ] . unode "form"