{- |
Module      :  ./PGIP/Query.hs
Description :  hets server queries
Copyright   :  (c) Christian Maeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via imports)

query strings
-}

module PGIP.Query where

{-

As a path we expect an existing directory, a file or library name or a
number (Int) referecing a current LibEnv (or Session). The session also stores
the top-level library name.

In order to address other (i.e. imported) libraries of a session given by a
number this number should be part of a query containing "dg=<id>" with the
library name as path.

As queries we basically allow actions to be taken, like displaying:
 - the whole LibEnv
 - the development graph (for a library name)
    - as xml or svg
 - a specific node or edge from a development graph (given by id=<id>)
    in various format (like local or global theory)
other actions are commands like performing global decomposition (or "auto")
on a graph or individual proofs on a node or edge.

But rather than requiring a full query like "?dg=5&command=display&format=xml"
it should be sufficient to write "/5?xml" or "/5?auto". The notation "dg=5" is
only necessary to address an imported library of the session. Also some
default display should be generated for a missing query like just "/5".

State changing commands like "auto" (or other proofs) will generate a new
numbers for the new graphs (i.e. "dg=6").

The default display for a LibEnv should be:

 - the current top-level library name
 - links to every imported library
 - links to display the current top-level development graphs in various formats.
 - links to perform the possible global commands
 - (several) links for every node
 - (several) links for every edge

-}

import Common.Utils

import PGIP.ReasoningParameters
import PGIP.Shared
import Control.Exception

import Data.Char
import Data.List
import Data.Maybe
import qualified Data.Map as Map

import Common.Percent

import Driver.Options

ppList :: [String]
ppList :: [String]
ppList = (PrettyType -> String) -> [PrettyType] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (OutType -> String
forall a. Show a => a -> String
show (OutType -> String)
-> (PrettyType -> OutType) -> PrettyType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyType -> OutType
PrettyOut) [PrettyType]
prettyList [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["pdf"]

displayTypes :: [String]
displayTypes :: [String]
displayTypes =
  ["svg", "xml", "json", "dot", "symbols", "session"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ppList

comorphs :: [String]
comorphs :: [String]
comorphs = ["provers", "translations"]

data NodeCmd = Node | Info | Theory | Symbols | Translate String
  deriving (Int -> NodeCmd -> ShowS
[NodeCmd] -> ShowS
NodeCmd -> String
(Int -> NodeCmd -> ShowS)
-> (NodeCmd -> String) -> ([NodeCmd] -> ShowS) -> Show NodeCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeCmd] -> ShowS
$cshowList :: [NodeCmd] -> ShowS
show :: NodeCmd -> String
$cshow :: NodeCmd -> String
showsPrec :: Int -> NodeCmd -> ShowS
$cshowsPrec :: Int -> NodeCmd -> ShowS
Show, NodeCmd -> NodeCmd -> Bool
(NodeCmd -> NodeCmd -> Bool)
-> (NodeCmd -> NodeCmd -> Bool) -> Eq NodeCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeCmd -> NodeCmd -> Bool
$c/= :: NodeCmd -> NodeCmd -> Bool
== :: NodeCmd -> NodeCmd -> Bool
$c== :: NodeCmd -> NodeCmd -> Bool
Eq)

nodeCmds :: [NodeCmd]
nodeCmds :: [NodeCmd]
nodeCmds = [NodeCmd
Node, NodeCmd
Info, NodeCmd
Theory, NodeCmd
Symbols]

showNodeCmd :: NodeCmd -> String
showNodeCmd :: NodeCmd -> String
showNodeCmd = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> (NodeCmd -> String) -> NodeCmd -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeCmd -> String
forall a. Show a => a -> String
show

nodeCommands :: [String]
nodeCommands :: [String]
nodeCommands = (NodeCmd -> String) -> [NodeCmd] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NodeCmd -> String
showNodeCmd [NodeCmd]
nodeCmds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
comorphs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["prove"]

proveParams :: [String]
proveParams :: [String]
proveParams = ["timeout", "include", "prover", "translation", "theorems",
  "axioms", "includeDetails", "includeProof"]

edgeCommands :: [String]
edgeCommands :: [String]
edgeCommands = ["edge"]

knownQueryKeys :: [String]
knownQueryKeys :: [String]
knownQueryKeys = [String]
displayTypes [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nodeCommands [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
proveParams [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
edgeCommands
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["format", "autoproof", "consistency", "dg", "name", "id"]

-- Lib- and node name can be IRIs now (the query id is the session number)
data DGQuery = DGQuery
  { DGQuery -> Int
queryId :: Int
  , DGQuery -> Maybe String
optQueryLibPath :: Maybe String
  }
  | NewDGQuery
  { DGQuery -> String
queryLib :: FilePath
  , DGQuery -> [String]
commands :: [String]
  } deriving Int -> DGQuery -> ShowS
[DGQuery] -> ShowS
DGQuery -> String
(Int -> DGQuery -> ShowS)
-> (DGQuery -> String) -> ([DGQuery] -> ShowS) -> Show DGQuery
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGQuery] -> ShowS
$cshowList :: [DGQuery] -> ShowS
show :: DGQuery -> String
$cshow :: DGQuery -> String
showsPrec :: Int -> DGQuery -> ShowS
$cshowsPrec :: Int -> DGQuery -> ShowS
Show

data Query = Query
  { Query -> DGQuery
dgQuery :: DGQuery
  , Query -> QueryKind
queryKind :: QueryKind
  } deriving Int -> Query -> ShowS
[Query] -> ShowS
Query -> String
(Int -> Query -> ShowS)
-> (Query -> String) -> ([Query] -> ShowS) -> Show Query
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Query] -> ShowS
$cshowList :: [Query] -> ShowS
show :: Query -> String
$cshow :: Query -> String
showsPrec :: Int -> Query -> ShowS
$cshowsPrec :: Int -> Query -> ShowS
Show

type NodeIdOrName = Either Int String

type QueryPair = (String, Maybe String)

showQuery :: [QueryPair] -> String
showQuery :: [QueryPair] -> String
showQuery = ('?' Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ([QueryPair] -> String) -> [QueryPair] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "&" ([String] -> String)
-> ([QueryPair] -> [String]) -> [QueryPair] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QueryPair -> String) -> [QueryPair] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, ms :: Maybe String
ms) ->
  ShowS
encode String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (('=' Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
encode) Maybe String
ms)

showPath :: [String] -> String
showPath :: [String] -> String
showPath = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "/" ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
encode

showPathQuery :: [String] -> [QueryPair] -> String
showPathQuery :: [String] -> [QueryPair] -> String
showPathQuery p :: [String]
p q :: [QueryPair]
q = [String] -> String
showPath [String]
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ if [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
q then "" else [QueryPair] -> String
showQuery [QueryPair]
q

data QueryKind =
    DisplayQuery (Maybe String)
  | DGTranslation String
  | GlobCmdQuery String
  | GlProvers ProverMode (Maybe String)
  | GlTranslations
  | GlShowProverWindow ProverMode
  | GlAutoProveREST ProverMode ReasoningParameters
  | GlAutoProve ProveCmd
  | NodeQuery NodeIdOrName NodeCommand
  | EdgeQuery Int String deriving (Int -> QueryKind -> ShowS
[QueryKind] -> ShowS
QueryKind -> String
(Int -> QueryKind -> ShowS)
-> (QueryKind -> String)
-> ([QueryKind] -> ShowS)
-> Show QueryKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QueryKind] -> ShowS
$cshowList :: [QueryKind] -> ShowS
show :: QueryKind -> String
$cshow :: QueryKind -> String
showsPrec :: Int -> QueryKind -> ShowS
$cshowsPrec :: Int -> QueryKind -> ShowS
Show, QueryKind -> QueryKind -> Bool
(QueryKind -> QueryKind -> Bool)
-> (QueryKind -> QueryKind -> Bool) -> Eq QueryKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QueryKind -> QueryKind -> Bool
$c/= :: QueryKind -> QueryKind -> Bool
== :: QueryKind -> QueryKind -> Bool
$c== :: QueryKind -> QueryKind -> Bool
Eq)

data ProveCmd = ProveCmd
  { ProveCmd -> ProverMode
pcProverMode :: ProverMode
  , ProveCmd -> Bool
pcInclTheorems :: Bool
  , ProveCmd -> Maybe String
pcProver :: Maybe String
  , ProveCmd -> Maybe String
pcTranslation :: Maybe String
  , ProveCmd -> Maybe Int
pcTimeout :: Maybe Int
  , ProveCmd -> [String]
pcTheoremsOrNodes :: [String]
  , ProveCmd -> Bool
pcXmlResult :: Bool
  , ProveCmd -> [String]
pcAxioms :: [String] } deriving (Int -> ProveCmd -> ShowS
[ProveCmd] -> ShowS
ProveCmd -> String
(Int -> ProveCmd -> ShowS)
-> (ProveCmd -> String) -> ([ProveCmd] -> ShowS) -> Show ProveCmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProveCmd] -> ShowS
$cshowList :: [ProveCmd] -> ShowS
show :: ProveCmd -> String
$cshow :: ProveCmd -> String
showsPrec :: Int -> ProveCmd -> ShowS
$cshowsPrec :: Int -> ProveCmd -> ShowS
Show, ProveCmd -> ProveCmd -> Bool
(ProveCmd -> ProveCmd -> Bool)
-> (ProveCmd -> ProveCmd -> Bool) -> Eq ProveCmd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProveCmd -> ProveCmd -> Bool
$c/= :: ProveCmd -> ProveCmd -> Bool
== :: ProveCmd -> ProveCmd -> Bool
$c== :: ProveCmd -> ProveCmd -> Bool
Eq)

data NodeCommand =
    NcCmd NodeCmd
  | NcProvers ProverMode (Maybe String) -- optional comorphism
  | NcTranslations (Maybe String) -- optional prover name
  | ProveNode ProveCmd deriving (Int -> NodeCommand -> ShowS
[NodeCommand] -> ShowS
NodeCommand -> String
(Int -> NodeCommand -> ShowS)
-> (NodeCommand -> String)
-> ([NodeCommand] -> ShowS)
-> Show NodeCommand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeCommand] -> ShowS
$cshowList :: [NodeCommand] -> ShowS
show :: NodeCommand -> String
$cshow :: NodeCommand -> String
showsPrec :: Int -> NodeCommand -> ShowS
$cshowsPrec :: Int -> NodeCommand -> ShowS
Show, NodeCommand -> NodeCommand -> Bool
(NodeCommand -> NodeCommand -> Bool)
-> (NodeCommand -> NodeCommand -> Bool) -> Eq NodeCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeCommand -> NodeCommand -> Bool
$c/= :: NodeCommand -> NodeCommand -> Bool
== :: NodeCommand -> NodeCommand -> Bool
$c== :: NodeCommand -> NodeCommand -> Bool
Eq)

-- | the path is not empty and leading slashes are removed
anaUri :: [String] -> [QueryPair] -> [String] -> Either String Query
anaUri :: [String] -> [QueryPair] -> [String] -> Either String Query
anaUri pathBits :: [String]
pathBits query :: [QueryPair]
query globals :: [String]
globals = case [QueryPair] -> [String] -> Either String (Maybe Int, QueryKind)
anaQuery [QueryPair]
query [String]
globals of
    Left err :: String
err -> String -> Either String Query
forall a b. a -> Either a b
Left String
err
    Right (mi :: Maybe Int
mi, qk :: QueryKind
qk) -> let path :: String
path = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "/" [String]
pathBits in
     case (Maybe Int
mi, String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
path) of
      (Just i :: Int
i, Just j :: Int
j) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j -> String -> Either String Query
forall a b. a -> Either a b
Left "different dg ids"
      (_, mj :: Maybe Int
mj) -> Query -> Either String Query
forall a b. b -> Either a b
Right (Query -> Either String Query) -> Query -> Either String Query
forall a b. (a -> b) -> a -> b
$ DGQuery -> QueryKind -> Query
Query
        (case [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int
mi, Maybe Int
mj] of
          [] -> String -> [String] -> DGQuery
NewDGQuery String
path []
          i :: Int
i : _ -> Int -> Maybe String -> DGQuery
DGQuery Int
i (Maybe String -> DGQuery) -> Maybe String -> DGQuery
forall a b. (a -> b) -> a -> b
$ if Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
mj then Maybe String
forall a. Maybe a
Nothing else String -> Maybe String
forall a. a -> Maybe a
Just String
path)
        QueryKind
qk

isNat :: String -> Bool
isNat :: String -> Bool
isNat s :: String
s = (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
s Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s) Bool -> Bool -> Bool
&& String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 11

getSwitches :: [QueryPair] -> Either String ([QueryPair], [(String, Flag)])
getSwitches :: [QueryPair] -> Either String ([QueryPair], [(String, Flag)])
getSwitches qs :: [QueryPair]
qs = case [QueryPair]
qs of
  [] -> ([QueryPair], [(String, Flag)])
-> Either String ([QueryPair], [(String, Flag)])
forall a b. b -> Either a b
Right ([], [])
  q :: QueryPair
q@(s :: String
s, mv :: Maybe String
mv) : r :: [QueryPair]
r ->
    let eith :: Either String ([QueryPair], [(String, Flag)])
eith = [QueryPair] -> Either String ([QueryPair], [(String, Flag)])
getSwitches [QueryPair]
r
    in case String -> [(String, Flag)] -> Maybe Flag
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, Flag)]
optionFlags of
      Just f :: Flag
f -> case Maybe String
mv of
        Just v :: String
v | String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
v) ["on", "t", "true", "1"] ->
          String -> Either String ([QueryPair], [(String, Flag)])
forall a b. a -> Either a b
Left (String -> Either String ([QueryPair], [(String, Flag)]))
-> String -> Either String ([QueryPair], [(String, Flag)])
forall a b. (a -> b) -> a -> b
$ "query flag can only be switched on: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v
        _ -> case Either String ([QueryPair], [(String, Flag)])
eith of
          Right (qr :: [QueryPair]
qr, ps :: [(String, Flag)]
ps) -> ([QueryPair], [(String, Flag)])
-> Either String ([QueryPair], [(String, Flag)])
forall a b. b -> Either a b
Right ([QueryPair]
qr, (String
s, Flag
f) (String, Flag) -> [(String, Flag)] -> [(String, Flag)]
forall a. a -> [a] -> [a]
: [(String, Flag)]
ps)
          err :: Either String ([QueryPair], [(String, Flag)])
err -> Either String ([QueryPair], [(String, Flag)])
err
      Nothing -> case Either String ([QueryPair], [(String, Flag)])
eith of
        Right (qr :: [QueryPair]
qr, ps :: [(String, Flag)]
ps) -> ([QueryPair], [(String, Flag)])
-> Either String ([QueryPair], [(String, Flag)])
forall a b. b -> Either a b
Right (QueryPair
q QueryPair -> [QueryPair] -> [QueryPair]
forall a. a -> [a] -> [a]
: [QueryPair]
qr, [(String, Flag)]
ps)
        err :: Either String ([QueryPair], [(String, Flag)])
err -> Either String ([QueryPair], [(String, Flag)])
err

-- due to the error calls in the option parsers this needs to be in the IO monad
getArgFlags :: [QueryPair]
  -> IO (Either String ([QueryPair], [(String, String)], [Flag]))
getArgFlags :: [QueryPair]
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
getArgFlags qs :: [QueryPair]
qs = case [QueryPair]
qs of
  [] -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String ([QueryPair], [(String, String)], [Flag])
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall a b. (a -> b) -> a -> b
$ ([QueryPair], [(String, String)], [Flag])
-> Either String ([QueryPair], [(String, String)], [Flag])
forall a b. b -> Either a b
Right ([], [], [])
  q :: QueryPair
q@(s :: String
s, mv :: Maybe String
mv) : r :: [QueryPair]
r -> do
    Either String ([QueryPair], [(String, String)], [Flag])
eith <- [QueryPair]
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
getArgFlags [QueryPair]
r
    case String -> [(String, String -> Flag)] -> Maybe (String -> Flag)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, String -> Flag)]
optionArgs of
     Just p :: String -> Flag
p -> case Maybe String
mv of
       Nothing -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String ([QueryPair], [(String, String)], [Flag])
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> (String
    -> Either String ([QueryPair], [(String, String)], [Flag]))
-> String
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String ([QueryPair], [(String, String)], [Flag])
forall a b. a -> Either a b
Left (String
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> String
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall a b. (a -> b) -> a -> b
$ "missing value for query argument: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
       Just v :: String
v -> do
         Either ErrorCall Flag
eith2 <- IO Flag -> IO (Either ErrorCall Flag)
forall e a. Exception e => IO a -> IO (Either e a)
try (IO Flag -> IO (Either ErrorCall Flag))
-> IO Flag -> IO (Either ErrorCall Flag)
forall a b. (a -> b) -> a -> b
$ Flag -> IO Flag
forall a. a -> IO a
evaluate (Flag -> IO Flag) -> Flag -> IO Flag
forall a b. (a -> b) -> a -> b
$ String -> Flag
p String
v
         case Either ErrorCall Flag
eith2 :: Either ErrorCall Flag of
           Right f :: Flag
f -> case Either String ([QueryPair], [(String, String)], [Flag])
eith of
               Right (qr :: [QueryPair]
qr, vs :: [(String, String)]
vs, fs :: [Flag]
fs) -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String ([QueryPair], [(String, String)], [Flag])
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall a b. (a -> b) -> a -> b
$ ([QueryPair], [(String, String)], [Flag])
-> Either String ([QueryPair], [(String, String)], [Flag])
forall a b. b -> Either a b
Right ([QueryPair]
qr, (String
s, String
v) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
vs, Flag
f Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
fs)
               err :: Either String ([QueryPair], [(String, String)], [Flag])
err -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return Either String ([QueryPair], [(String, String)], [Flag])
err
           Left _ ->
             Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String ([QueryPair], [(String, String)], [Flag])
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> (String
    -> Either String ([QueryPair], [(String, String)], [Flag]))
-> String
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String ([QueryPair], [(String, String)], [Flag])
forall a b. a -> Either a b
Left (String
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> String
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall a b. (a -> b) -> a -> b
$ "illegal value for option: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v
     Nothing -> case Either String ([QueryPair], [(String, String)], [Flag])
eith of
       Right (qr :: [QueryPair]
qr, vs :: [(String, String)]
vs, fs :: [Flag]
fs) -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String ([QueryPair], [(String, String)], [Flag])
 -> IO (Either String ([QueryPair], [(String, String)], [Flag])))
-> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall a b. (a -> b) -> a -> b
$ ([QueryPair], [(String, String)], [Flag])
-> Either String ([QueryPair], [(String, String)], [Flag])
forall a b. b -> Either a b
Right (QueryPair
q QueryPair -> [QueryPair] -> [QueryPair]
forall a. a -> [a] -> [a]
: [QueryPair]
qr, [(String, String)]
vs, [Flag]
fs)
       err :: Either String ([QueryPair], [(String, String)], [Flag])
err -> Either String ([QueryPair], [(String, String)], [Flag])
-> IO (Either String ([QueryPair], [(String, String)], [Flag]))
forall (m :: * -> *) a. Monad m => a -> m a
return Either String ([QueryPair], [(String, String)], [Flag])
err

-- | a leading question mark is removed, possibly a session id is returned
anaQuery :: [QueryPair] -> [String] -> Either String (Maybe Int, QueryKind)
anaQuery :: [QueryPair] -> [String] -> Either String (Maybe Int, QueryKind)
anaQuery q' :: [QueryPair]
q' globals :: [String]
globals =
       let (atP :: [QueryPair]
atP, q'' :: [QueryPair]
q'') = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "autoproof") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
q'
           (atC :: [QueryPair]
atC, q :: [QueryPair]
q) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "consistency") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
q''
           (q1 :: [QueryPair]
q1, qm :: [QueryPair]
qm) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ l :: QueryPair
l -> case QueryPair
l of
                        (x :: String
x, Nothing) -> String -> Bool
isNat String
x Bool -> Bool -> Bool
|| String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
x
                               ([String]
displayTypes [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
globals
                                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["include", "autoproof"]
                                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nodeCommands [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
edgeCommands)
                        _ -> Bool
False) [QueryPair]
q
           (q2 :: [QueryPair]
q2, qr :: [QueryPair]
qr) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ l :: QueryPair
l -> case QueryPair
l of
                        (x :: String
x, Just y :: String
y) ->
                            String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
x (["dg", "id", "session"]
                                    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
edgeCommands)
                            Bool -> Bool -> Bool
&& String -> Bool
isNat String
y
                               Bool -> Bool -> Bool
|| String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "command" Bool -> Bool -> Bool
&&
                                  String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
y [String]
globals
                               Bool -> Bool -> Bool
|| String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "format" Bool -> Bool -> Bool
&& String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
y [String]
displayTypes
                               Bool -> Bool -> Bool
|| String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
x ("name" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
forall a. [a] -> [a]
tail [String]
proveParams
                                          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nodeCommands)
                                  -- note: allows illegal timeout values
                               Bool -> Bool -> Bool
|| String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "timeout"
                                  -- without timeout, see above
                        _ -> Bool
False) [QueryPair]
qm
           (fs :: [String]
fs, r1 :: [String]
r1) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
displayTypes) ([String] -> ([String], [String]))
-> [String] -> ([String], [String])
forall a b. (a -> b) -> a -> b
$ (QueryPair -> String) -> [QueryPair] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QueryPair -> String
forall a b. (a, b) -> a
fst [QueryPair]
q1
           (gs :: [String]
gs, r2 :: [String]
r2) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
globals) [String]
r1
           (ns :: [String]
ns, r3 :: [String]
r3) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
nodeCommands) [String]
r2
           (es :: [String]
es, r4 :: [String]
r4) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
edgeCommands) [String]
r3
           (incls :: [String]
incls, is :: [String]
is) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "include") [String]
r4
           (fs2 :: [QueryPair]
fs2, p1 :: [QueryPair]
p1) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "format") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
q2
           (cs2 :: [QueryPair]
cs2, p2 :: [QueryPair]
p2) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "command") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p1
           (is2 :: [QueryPair]
is2, p3 :: [QueryPair]
p3) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["dg", "session"]) (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p2
           (ns2 :: [QueryPair]
ns2, p4 :: [QueryPair]
p4) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
nodeCommands) (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p3
           (es2 :: [QueryPair]
es2, p5 :: [QueryPair]
p5) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
edgeCommands) (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p4
           (nns :: [QueryPair]
nns, p6 :: [QueryPair]
p6) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "name") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p5
           (ids :: [QueryPair]
ids, pps :: [QueryPair]
pps) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "id") (String -> Bool) -> (QueryPair -> String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> String
forall a b. (a, b) -> a
fst) [QueryPair]
p6
           snds :: [(a, Maybe b)] -> [b]
snds = ((a, Maybe b) -> Maybe b) -> [(a, Maybe b)] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (a, Maybe b) -> Maybe b
forall a b. (a, b) -> b
snd
           afs :: [String]
afs = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
fs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> [String]
forall a b. [(a, Maybe b)] -> [b]
snds [QueryPair]
fs2
           ags :: [String]
ags = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
gs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> [String]
forall a b. [(a, Maybe b)] -> [b]
snds [QueryPair]
cs2
           ans :: [String]
ans = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
ns [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (QueryPair -> String) -> [QueryPair] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QueryPair -> String
forall a b. (a, b) -> a
fst [QueryPair]
ns2
           aes :: [String]
aes = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
es [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (QueryPair -> String) -> [QueryPair] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QueryPair -> String
forall a b. (a, b) -> a
fst [QueryPair]
es2
           ais :: [String]
ais = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
is [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> [String]
forall a b. [(a, Maybe b)] -> [b]
snds [QueryPair]
is2
           aids :: [String]
aids = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String])
-> ([QueryPair] -> [String]) -> [QueryPair] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QueryPair] -> [String]
forall a b. [(a, Maybe b)] -> [b]
snds ([QueryPair] -> [String]) -> [QueryPair] -> [String]
forall a b. (a -> b) -> a -> b
$ [QueryPair]
ns2 [QueryPair] -> [QueryPair] -> [QueryPair]
forall a. [a] -> [a] -> [a]
++ [QueryPair]
es2 [QueryPair] -> [QueryPair] -> [QueryPair]
forall a. [a] -> [a] -> [a]
++ [QueryPair]
ids [QueryPair] -> [QueryPair] -> [QueryPair]
forall a. [a] -> [a] -> [a]
++ [QueryPair]
nns
           mi :: Maybe Int
mi = (String -> Int) -> Maybe String -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Int
forall a. Read a => String -> a
read (Maybe String -> Maybe Int) -> Maybe String -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String]
ais
           (theorems :: [QueryPair]
theorems, qqr :: [QueryPair]
qqr) = (QueryPair -> Bool) -> [QueryPair] -> ([QueryPair], [QueryPair])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just "on") (Maybe String -> Bool)
-> (QueryPair -> Maybe String) -> QueryPair -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryPair -> Maybe String
forall a b. (a, b) -> b
snd) [QueryPair]
qr
           noPP :: Bool
noPP = [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
pps Bool -> Bool -> Bool
&& [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
incls Bool -> Bool -> Bool
&& [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
theorems
       -- TODO i kind of abused this functions structure for autoproofs here
       in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
atP then (Maybe Int, QueryKind) -> Either String (Maybe Int, QueryKind)
forall a b. b -> Either a b
Right (Maybe Int
mi, ProverMode -> QueryKind
GlShowProverWindow ProverMode
GlProofs) else
          if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
atC then (Maybe Int, QueryKind) -> Either String (Maybe Int, QueryKind)
forall a b. b -> Either a b
Right (Maybe Int
mi, ProverMode -> QueryKind
GlShowProverWindow ProverMode
GlConsistency)
          else
          if [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
qqr Bool -> Bool -> Bool
&& [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
ais Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then case ([String]
afs, [String]
ags, [String]
ans, [String]
aes, [String]
aids) of
         (_, [], [], [], []) | Bool
noPP -> if [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
afs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1
           then String -> Either String (Maybe Int, QueryKind)
forall a b. a -> Either a b
Left (String -> Either String (Maybe Int, QueryKind))
-> String -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$ "non-unique format " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
afs
           else (Maybe Int, QueryKind) -> Either String (Maybe Int, QueryKind)
forall a b. b -> Either a b
Right (Maybe Int
mi, Maybe String -> QueryKind
DisplayQuery (Maybe String -> QueryKind) -> Maybe String -> QueryKind
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String]
afs)
         (_, c :: String
c : r :: [String]
r, [], [], []) | Bool
noPP -> if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
r
           then (Maybe Int, QueryKind) -> Either String (Maybe Int, QueryKind)
forall a b. b -> Either a b
Right (Maybe Int
mi, String -> QueryKind
GlobCmdQuery String
c)
           else String -> Either String (Maybe Int, QueryKind)
forall a b. a -> Either a b
Left (String -> Either String (Maybe Int, QueryKind))
-> String -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$ "non-unique command " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
r
         (_, [], _, [], [_]) -> (QueryKind -> (Maybe Int, QueryKind))
-> Either String QueryKind -> Either String (Maybe Int, QueryKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ qk :: QueryKind
qk -> (Maybe Int
mi, QueryKind
qk)) (Either String QueryKind -> Either String (Maybe Int, QueryKind))
-> Either String QueryKind -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$
           [String]
-> NodeIdOrName
-> [String]
-> [String]
-> [QueryPair]
-> Either String QueryKind
anaNodeQuery [String]
ans ([QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName
getIdOrName [QueryPair]
ids [QueryPair]
nns [QueryPair]
ns2) ((QueryPair -> String) -> [QueryPair] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QueryPair -> String
forall a b. (a, b) -> a
fst [QueryPair]
theorems)
             [String]
incls [QueryPair]
pps
         (_, [], [], e :: String
e : r :: [String]
r, i :: String
i : s :: [String]
s) | Bool
noPP ->
           if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
r Bool -> Bool -> Bool
&& [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
s Bool -> Bool -> Bool
&& [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
nns Bool -> Bool -> Bool
&& [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
ns2
           then (Maybe Int, QueryKind) -> Either String (Maybe Int, QueryKind)
forall a b. b -> Either a b
Right (Maybe Int
mi, Int -> String -> QueryKind
EdgeQuery (String -> Int
forall a. Read a => String -> a
read String
i) String
e)
           else String -> Either String (Maybe Int, QueryKind)
forall a b. a -> Either a b
Left (String -> Either String (Maybe Int, QueryKind))
-> String -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$ "non-unique edge " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show ([String]
aes [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
aids)
         _ -> String -> Either String (Maybe Int, QueryKind)
forall a b. a -> Either a b
Left (String -> Either String (Maybe Int, QueryKind))
-> String -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$ "non-unique query " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> String
forall a. Show a => a -> String
show [QueryPair]
q
       else String -> Either String (Maybe Int, QueryKind)
forall a b. a -> Either a b
Left (String -> Either String (Maybe Int, QueryKind))
-> String -> Either String (Maybe Int, QueryKind)
forall a b. (a -> b) -> a -> b
$ if [QueryPair] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QueryPair]
qqr then "non-unique dg " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> String
forall a. Show a => a -> String
show [QueryPair]
q else
                       "ill-formed query " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> String
forall a. Show a => a -> String
show [QueryPair]
qqr

getIdOrName :: [QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName
getIdOrName :: [QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName
getIdOrName ids :: [QueryPair]
ids nns :: [QueryPair]
nns ns2 :: [QueryPair]
ns2 = case [QueryPair]
ids of
  (_, Just v :: String
v) : _ -> Int -> NodeIdOrName
forall a b. a -> Either a b
Left (Int -> NodeIdOrName) -> Int -> NodeIdOrName
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
v
  _ -> case [QueryPair]
nns of
    (_, Just v :: String
v) : _ -> String -> NodeIdOrName
forall a b. b -> Either a b
Right String
v
    _ -> case [QueryPair]
ns2 of
      (_, Just v :: String
v) : _ -> if String -> Bool
isNat String
v then Int -> NodeIdOrName
forall a b. a -> Either a b
Left (Int -> NodeIdOrName) -> Int -> NodeIdOrName
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
v else String -> NodeIdOrName
forall a b. b -> Either a b
Right String
v
      _ -> String -> NodeIdOrName
forall a. HasCallStack => String -> a
error "getIdOrName"

escMap :: [(Char, Char)]
escMap :: [(Char, Char)]
escMap = (String -> (Char, Char)) -> [String] -> [(Char, Char)]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: String
l -> let [f :: Char
f, s :: Char
s] = String
l in (Char
f, Char
s))
  [ "+P"
  , "&A"
  , "=E"
  , ";S"
  , " B"
  , "XX" ]

escStr :: String -> String
escStr :: ShowS
escStr = (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: Char
c -> case Char -> Map Char Char -> Maybe Char
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Char
c (Map Char Char -> Maybe Char) -> Map Char Char -> Maybe Char
forall a b. (a -> b) -> a -> b
$ [(Char, Char)] -> Map Char Char
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Char, Char)]
escMap of
    Nothing -> [Char
c]
    Just e :: Char
e -> ['X', Char
e])

unEsc :: String -> String
unEsc :: ShowS
unEsc s :: String
s = let m :: Map Char Char
m = [(Char, Char)] -> Map Char Char
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Char, Char)] -> Map Char Char)
-> [(Char, Char)] -> Map Char Char
forall a b. (a -> b) -> a -> b
$ ((Char, Char) -> (Char, Char)) -> [(Char, Char)] -> [(Char, Char)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: Char
a, b :: Char
b) -> (Char
b, Char
a)) [(Char, Char)]
escMap
  in case String
s of
  "" -> ""
  'X' : c :: Char
c : r :: String
r -> Char -> Char -> Map Char Char -> Char
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Char
c Char
c Map Char Char
m Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
unEsc String
r
  c :: Char
c : r :: String
r -> Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
unEsc String
r

decodePlus :: Char -> Char
decodePlus :: Char -> Char
decodePlus c :: Char
c = if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '+' then ' ' else Char
c

decodeQuery :: String -> String
decodeQuery :: ShowS
decodeQuery = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
decodePlus ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
decode

getFragOfCode :: String -> String
getFragOfCode :: ShowS
getFragOfCode = ShowS
getFragment ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
decodeQuery

getFragment :: String -> String
getFragment :: ShowS
getFragment s :: String
s = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '#') String
s of
  _ : t :: String
t -> String
t
  "" -> String
s

anaNodeQuery :: [String] -> NodeIdOrName -> [String] -> [String]
  -> [QueryPair] -> Either String QueryKind
anaNodeQuery :: [String]
-> NodeIdOrName
-> [String]
-> [String]
-> [QueryPair]
-> Either String QueryKind
anaNodeQuery ans :: [String]
ans i :: NodeIdOrName
i moreTheorems :: [String]
moreTheorems incls :: [String]
incls pss :: [QueryPair]
pss =
  let pps :: [(String, String)]
pps = (QueryPair -> [(String, String)] -> [(String, String)])
-> [(String, String)] -> [QueryPair] -> [(String, String)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ l :: QueryPair
l -> case QueryPair
l of
                (x :: String
x, Just y :: String
y) -> ((String
x, String
y) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
:)
                _ -> [(String, String)] -> [(String, String)]
forall a. a -> a
id) [] [QueryPair]
pss
      incl :: Maybe String
incl = String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "include" [(String, String)]
pps
      trans :: Maybe String
trans = ShowS -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ShowS
decodeQuery (Maybe String -> Maybe String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "translation" [(String, String)]
pps
      prover :: Maybe String
prover = String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "prover" [(String, String)]
pps
      theorems :: [String]
theorems = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
unEsc [String]
moreTheorems
          [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ case String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "theorems" [(String, String)]
pps of
        Nothing -> []
        Just str :: String
str -> ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
unEsc ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ' ' (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ ShowS
decodeQuery String
str
      timeLimit_ :: Maybe Int
timeLimit_ = Maybe Int -> (String -> Maybe Int) -> Maybe String -> Maybe Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe Int
forall a. Maybe a
Nothing String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (Maybe String -> Maybe Int) -> Maybe String -> Maybe Int
forall a b. (a -> b) -> a -> b
$ String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "timeout" [(String, String)]
pps
      pp :: NodeCommand
pp = ProveCmd -> NodeCommand
ProveNode (ProveCmd -> NodeCommand) -> ProveCmd -> NodeCommand
forall a b. (a -> b) -> a -> b
$ ProverMode
-> Bool
-> Maybe String
-> Maybe String
-> Maybe Int
-> [String]
-> Bool
-> [String]
-> ProveCmd
ProveCmd ProverMode
GlProofs (Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
incls) Bool -> Bool -> Bool
|| case Maybe String
incl of
        Nothing -> Bool
True
        Just str :: String
str -> (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
str String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ["f", "false"])
        Maybe String
prover Maybe String
trans Maybe Int
timeLimit_ [String]
theorems Bool
False []
      noPP :: Bool
noPP = [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
incls Bool -> Bool -> Bool
&& [(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
pps
      noIncl :: Bool
noIncl = [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
incls Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
incl Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
timeLimit_
      cmds :: [(String, NodeCmd)]
cmds = (NodeCmd -> (String, NodeCmd)) -> [NodeCmd] -> [(String, NodeCmd)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: NodeCmd
a -> (NodeCmd -> String
showNodeCmd NodeCmd
a, NodeCmd
a)) [NodeCmd]
nodeCmds
  in case [String]
ans of
       [] -> QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i
         (NodeCommand -> QueryKind) -> NodeCommand -> QueryKind
forall a b. (a -> b) -> a -> b
$ if Bool
noPP then NodeCmd -> NodeCommand
NcCmd NodeCmd
Node else NodeCommand
pp
       [cmd :: String
cmd] -> case String
cmd of
         "prove" -> QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i NodeCommand
pp
         "provers" | Bool
noIncl Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
prover ->
            QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i (NodeCommand -> QueryKind) -> NodeCommand -> QueryKind
forall a b. (a -> b) -> a -> b
$ ProverMode -> Maybe String -> NodeCommand
NcProvers ProverMode
GlProofs Maybe String
trans
         "translations" | Bool
noIncl Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
trans ->
            QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i (NodeCommand -> QueryKind) -> NodeCommand -> QueryKind
forall a b. (a -> b) -> a -> b
$ Maybe String -> NodeCommand
NcTranslations Maybe String
prover
         _ -> case (String -> [(String, NodeCmd)] -> Maybe NodeCmd
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
cmd [(String, NodeCmd)]
cmds,Maybe String
trans) of
           (Just nc :: NodeCmd
nc,_) | Bool
noPP -> QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i (NodeCommand -> QueryKind) -> NodeCommand -> QueryKind
forall a b. (a -> b) -> a -> b
$ NodeCmd -> NodeCommand
NcCmd NodeCmd
nc
           (Just Theory, Just tr :: String
tr) -> QueryKind -> Either String QueryKind
forall a b. b -> Either a b
Right (QueryKind -> Either String QueryKind)
-> QueryKind -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ NodeIdOrName -> NodeCommand -> QueryKind
NodeQuery NodeIdOrName
i (NodeCommand -> QueryKind) -> NodeCommand -> QueryKind
forall a b. (a -> b) -> a -> b
$ NodeCmd -> NodeCommand
NcCmd (NodeCmd -> NodeCommand) -> NodeCmd -> NodeCommand
forall a b. (a -> b) -> a -> b
$ String -> NodeCmd
Translate String
tr
           _ -> String -> Either String QueryKind
forall a b. a -> Either a b
Left (String -> Either String QueryKind)
-> String -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ "unknown node command '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd String -> ShowS
forall a. [a] -> [a] -> [a]
++ "' "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> ShowS
forall a. Show a => a -> ShowS
shows [String]
incls " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [QueryPair] -> String
forall a. Show a => a -> String
show [QueryPair]
pss
       _ -> String -> Either String QueryKind
forall a b. a -> Either a b
Left (String -> Either String QueryKind)
-> String -> Either String QueryKind
forall a b. (a -> b) -> a -> b
$ "non-unique node command " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
ans