{- |

Module : $Header$

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.LibName

import Common.Utils

import Interfaces.Command

import Interfaces.CmdAction

import Static.DgUtils

import Driver.Options

import Data.Char

import Data.List

import Data.Maybe

import qualified Data.Map as Map

import Numeric

ppList :: [String]

ppList = map (show . PrettyOut) prettyList ++ ["pdf"]

displayTypes :: [String]

displayTypes =

["svg", "xml", "dot", "session"] ++ ppList

comorphs :: [String]

comorphs = ["provers", "translations"]

data NodeCmd = Node | Info | Theory | Symbols

deriving (Show, Eq, Bounded, Enum)

nodeCmds :: [NodeCmd]

nodeCmds = [minBound .. maxBound]

showNodeCmd :: NodeCmd -> String

showNodeCmd = map toLower . show

nodeCommands :: [String]

nodeCommands = map showNodeCmd nodeCmds ++ comorphs ++ ["prove"]

proveParams :: [String]

proveParams = ["timeout", "include", "prover", "translation", "theorems"]

edgeCommands :: [String]

edgeCommands = ["edge"]

getGlobCmds :: [(GlobCmd, a)] -> [String]

getGlobCmds = map (cmdlGlobCmd . fst)

globalCommands :: [String]

globalCommands = concat

[ getGlobCmds globLibAct

, getGlobCmds globLibResultAct

, getGlobCmds globResultAct ]

data DGQuery = DGQuery

{ queryId :: Int

, optQueryLibPath :: Maybe PATH

}

| NewDGQuery { queryLib :: FilePath }

data Query = Query

{ dgQuery :: DGQuery

, queryKind :: QueryKind

}

type NodeIdOrName = Either Int String

type QueryPair = (String, Maybe String)

data QueryKind =

DisplayQuery (Maybe String)

| GlobCmdQuery String

| NodeQuery NodeIdOrName NodeCommand

| EdgeQuery EdgeId String

data NodeCommand =

NcCmd NodeCmd

| NcProvers (Maybe String)

| NcTranslations (Maybe String)

| ProveNode

{ ncInclTheorems :: Bool

, ncProver :: Maybe String

, ncTranslation :: Maybe String

, ncTimeout :: Maybe Int

, ncTheorems :: [String] }

deriving Show

-- | the path is not empty and leading slashes are removed

anaUri :: FilePath -> [QueryPair] -> Either String Query

anaUri path query = case anaQuery query of

Right (mi, qk) -> case (mi, readMaybe path) of

(Just i, Just j) | i /= j -> Left "different dg ids"

(_, mj) -> Right $ Query

(case catMaybes [mi, mj] of

[] -> NewDGQuery path

i : _ -> DGQuery i $ if isJust mj then Nothing else Just path)

qk

Left err -> Left err

isNat :: String -> Bool

isNat s = all isDigit s && not (null s) && length s < 11

-- | a leading question mark is removed

anaQuery :: [QueryPair] -> Either String (Maybe Int, QueryKind)

anaQuery q =

let globals = "update" : globalCommands

(q1, qm) = partition (\ l -> case l of

(x, Nothing) -> isNat x || elem x

(displayTypes ++ globals ++ ["include"]

++ nodeCommands ++ edgeCommands)

_ -> False) q

(q2, qr) = partition (\ l -> case l of

(x, Just y) ->

elem x (["dg", "id", "session", "timeout"]

++ edgeCommands)

&& isNat y

|| x == "command" &&

elem y globals

|| x == "format" && elem y displayTypes

|| elem x ("name" : tail proveParams

++ nodeCommands)

-- without timeout, see above

_ -> False) qm

(fs, r1) = partition (`elem` displayTypes) $ map fst q1

(gs, r2) = partition (`elem` globals) r1

(ns, r3) = partition (`elem` nodeCommands) r2

(es, r4) = partition (`elem` edgeCommands) r3

(incls, is) = partition (== "include") r4

(fs2, p1) = partition ((== "format") . fst) q2

(cs2, p2) = partition ((== "command") . fst) p1

(is2, p3) = partition ((`elem` ["dg", "session"]) . fst) p2

(ns2, p4) = partition ((`elem` nodeCommands) . fst) p3

(es2, p5) = partition ((`elem` edgeCommands) . fst) p4

(nns, p6) = partition ((== "name") . fst) p5

(ids, pps) = partition ((== "id") . fst) p6

snds = mapMaybe snd

afs = nubOrd $ fs ++ snds fs2

ags = nubOrd $ gs ++ snds cs2

ans = nubOrd $ ns ++ map fst ns2

aes = nubOrd $ es ++ map fst es2

ais = nubOrd $ is ++ snds is2

aids = nubOrd . snds $ ns2 ++ es2 ++ ids ++ nns

mi = fmap read $ listToMaybe ais

noPP = null pps && null incls

in if null qr && length ais < 2 then case (afs, ags, ans, aes, aids) of

(_, [], [], [], []) | noPP -> if length afs > 1

then Left $ "non-unique format " ++ show afs

else Right (mi, DisplayQuery $ listToMaybe afs)

(_, c : r, [], [], []) | noPP -> if null r

then Right (mi, GlobCmdQuery c)

else Left $ "non-unique command " ++ show r

(_, [], _, [], [_]) | null es2 ->

anaNodeQuery mi ans (getIdOrName ids nns ns2) incls pps

(_, [], [], e : r, i : s) | noPP ->

if null r && null s && null nns && null ns2

then Right (mi, EdgeQuery (EdgeId $ read i) e)

else Left $ "non-unique edge " ++ show (aes ++ aids)

_ -> Left $ "non-unique query " ++ show q

else Left $ if null qr then "non-unique dg " ++ show q else

"ill-formed query " ++ show qr

getIdOrName :: [QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName

getIdOrName ids nns ns2 = case ids of

(_, Just v) : _ -> Left $ read v

_ -> case nns of

(_, Just v) : _ -> Right v

_ -> case ns2 of

(_, Just v) : _ -> if isNat v then Left $ read v else Right v

_ -> error "getIdOrName"

escMap :: [(Char, Char)]

escMap = map (\ l -> let [f, s] = l in (f, s))

[ "+P"

, "&A"

, "=E"

, ";S"

, " B"

, "XX" ]

escStr :: String -> String

escStr = concatMap (\ c -> case Map.lookup c $ Map.fromList escMap of

Nothing -> [c]

Just e -> ['X', e])

unEsc :: String -> String

unEsc s = let m = Map.fromList $ map (\ (a, b) -> (b, a)) escMap

in case s of

"" -> ""

'X' : c : r -> Map.findWithDefault c c m : unEsc r

c : r -> c : unEsc r

encodeForQuery :: String -> String

encodeForQuery = concatMap (\ c -> let n = ord c in case c of

_ | isAscii c && isAlphaNum c || elem c "_.-" -> [c]

' ' -> "+"

_ | n <= 255 -> '%' : (if n < 16 then "0" else "") ++ showHex n ""

_ -> "") -- ignore real unicode stuff

decodePlus :: Char -> Char

decodePlus c = if c == '+' then ' ' else c

decodeQueryCode :: String -> String

decodeQueryCode s = case s of

"" -> ""

'%' : h1 : h2 : r -> case readHex [h1, h2] of

(i, "") : _ -> decodePlus (chr i) : decodeQueryCode r

_ -> error $ "decodeQueryCode hex: " ++ take 3 s

c : r

-> decodePlus c : decodeQueryCode r

anaNodeQuery :: Maybe Int -> [String] -> NodeIdOrName -> [String]

-> [QueryPair] -> Either String (Maybe Int, QueryKind)

anaNodeQuery mi ans i incls pss =

let pps = foldr (\ l -> case l of

(x, Just y) -> ((x, y) :)

_ -> id) [] pss

incl = lookup "include" pps

trans = lookup "translation" pps

prover = lookup "prover" pps

theorems = case lookup "theorems" pps of

Nothing -> []

Just str -> map unEsc $ splitOn ' ' $ decodeQueryCode str

timeLimit = fmap read $ lookup "timeout" pps

pp = ProveNode (not (null incls) || case lookup "include" pps of

Nothing -> True

Just str -> map toLower str `notElem` ["f", "false"])

prover trans timeLimit theorems

noPP = null incls && null pps

noIncl = null incls && isNothing incl && isNothing timeLimit

cmds = map (\ a -> (showNodeCmd a, a)) nodeCmds

in case ans of

[] -> Right (mi, NodeQuery i

$ if noPP then NcCmd minBound else pp)

[cmd] -> case cmd of

"prove" -> Right (mi, NodeQuery i pp)

"provers" | noIncl && isNothing prover ->

Right (mi, NodeQuery i $ NcProvers trans)

"translations" | noIncl && isNothing trans ->

Right (mi, NodeQuery i $ NcTranslations prover)

_ -> case lookup cmd cmds of

Just nc | noPP -> Right (mi, NodeQuery i $ NcCmd nc)

_ -> Left $ "unknown node command '" ++ cmd ++ "' "

++ shows incls " " ++ show pss

_ -> Left $ "non-unique node command " ++ show ans