{- |

Module : ./CMDL/Shell.hs

Description : shell related functions

Copyright : uni-bremen and DFKI

License : GPLv2 or higher, see LICENSE.txt

Maintainer : r.pascanu@jacobs-university.de

Stability : provisional

Portability : portable

CMDL.Shell contains almost all functions related

the CMDL shell or haskeline

-}

module CMDL.Shell

( cComment

, cOpenComment

, cCloseComment

, nodeNames

, cmdlCompletionFn

, checkCom

) where

import CMDL.DataTypes

import CMDL.Utils

import CMDL.DataTypesUtils

import Common.Utils (trimLeft, trimRight, nubOrd, splitOn)

import Common.Result (Result (Result))

import Comorphisms.LogicGraph (comorphismList, logicGraph,

lookupComorphism_in_LG)

import Interfaces.Command (Command (CommentCmd))

import Interfaces.DataTypes

import Interfaces.Utils

import Interfaces.GenericATPState

import Logic.Comorphism

import Logic.Grothendieck (logics, findComorphismPaths,

G_sublogics (..))

import Logic.Prover

import Logic.Logic

import Logic.Coerce (coerceSublogic)

import Proofs.AbstractState

import Static.DevGraph

import Static.GTheory

import Data.Char (isSpace)

import Data.List

import qualified Data.Map

import Data.Maybe (mapMaybe, isNothing)

import System.Directory (doesDirectoryExist, getDirectoryContents)

register2history :: CmdlCmdDescription -> CmdlState -> IO CmdlState

register2history dscr state = do

let oldHistory = i_hist $ intState state

case undoList oldHistory of

[] -> return state

h : r -> case command h of

CommentCmd _ -> do

let nwh = h {

command = cmdDescription dscr }

return $ state {

intState = (intState state) {

i_hist = oldHistory {

undoList = nwh : r,

redoList = []

} } }

_ -> return state

-- process a comment line

processComment :: CmdlState -> String -> CmdlState

processComment st inp =

if isInfixOf "}%" inp then st { openComment = False } else st

-- adds a line to the script

addToScript :: CmdlState -> IntIState -> String -> CmdlState

addToScript st ist str

= let olds = script ist

oldextOpts = tsExtraOpts olds

in st {

intState = (intState st) {

i_state = Just ist {

script = olds { tsExtraOpts = str : oldextOpts } }

} }

checkCom :: CmdlCmdDescription -> CmdlState -> IO CmdlState

checkCom descr state =

-- check the priority of the current command

case cmdPriority descr of

CmdNoPriority ->

-- check if there is open comment

if openComment state

then return $ processComment state $ cmdInput descr

else

case i_state $ intState state of

Nothing -> register2history descr state

Just ist ->

-- check if there is inside a script

if loadScript ist

then return $ addToScript state ist

$ cmdName descr ++ " " ++ cmdInput descr

else register2history descr state

CmdGreaterThanComments ->

case i_state $ intState state of

Nothing -> register2history descr state

Just ist ->

if loadScript ist

then return $ addToScript state ist

$ cmdName descr ++ " " ++ cmdInput descr

else register2history descr state

CmdGreaterThanScriptAndComments -> return state

-- | Function handle a comment line

cComment :: String -> CmdlState -> IO CmdlState

cComment _ = return

-- For normal keyboard input

cOpenComment :: String -> CmdlState -> IO CmdlState

cOpenComment _ state = return state { openComment = True }

cCloseComment :: CmdlState -> IO CmdlState

cCloseComment state = return state { openComment = False }

{- | given an input it assumes that it starts with a

command name and tries to remove this command name -}

subtractCommandName :: [CmdlCmdDescription] -> String -> String

subtractCommandName allcmds input =

let inp = trimLeft input

in case mapMaybe ((`stripPrefix` inp) . cmdName) allcmds of

[] -> inp

hd : _ -> hd

{- This function tries to extract the name of command. In most cases this

would be the first word of the string but we have a few exceptions :

dg * commands

dg-all * commands

del * commands

del-all * commands

add * commands

set * commands

set-all * commands -}

getCmdName :: String -> String

getCmdName inp = case words inp of

[] -> []

hw : tws -> case tws of

[] -> hw

hwd : _ -> let

cs = ["dg", "del", "set"]

csa = "add" : cs ++ map (++ "-all") cs

in if elem hw csa then hw ++ ' ' : hwd else hw

{- | The function determines the requirements of the command

name found at the begining of the string -}

getTypeOf :: [CmdlCmdDescription] -> String -> CmdlCmdRequirements

getTypeOf allcmds input

= let nwInput = getCmdName input

tmp = concatMap (\ x -> case find (== nwInput) [cmdName x] of

Nothing -> []

Just _ -> [cmdReq x]) allcmds

in case tmp of

result : [] -> result

_ -> ReqUnknown

nodeNames :: [(a, DGNodeLab)] -> [String]

nodeNames = map (getDGNodeName . snd)

{- | The function provides a list of possible completion

to a given input if any -}

cmdlCompletionFn :: [CmdlCmdDescription] -> CmdlState -> String -> IO [String]

cmdlCompletionFn allcmds allState input =

let s0_9 = map show [0 .. (9 :: Int)]

app h = (h ++) . (' ' :)

in case getTypeOf allcmds input of

ReqNodesOrEdges mn mf ->

case i_state $ intState allState of

Nothing -> return []

Just state -> do

{- a pair, where the first element is what needs

to be completed while the second is what is

before the word that needs to be completed

-}

let -- get all nodes

ns = getAllNodes state

fns = nodeNames $ maybe id (\ f -> filter (\ (_, nd) ->

case f of

OpenCons -> hasOpenNodeConsStatus False nd

OpenGoals -> hasOpenGoals nd))

mf ns

es = map fst

$ maybe id (\ f -> filter $ case f of

OpenCons -> isOpenConsEdge

OpenGoals -> edgeContainsGoals

. snd) mf

$ createEdgeNames ns (getAllEdges state)

allNames = case mn of

Nothing -> es ++ fns

Just b -> if b then fns else es

(fins, tC) = finishedNames allNames

$ subtractCommandName allcmds input

-- what is before tC

bC = reverse $ trimLeft $ drop (length tC) $ reverse input

{- filter out words that do not start with the word

that needs to be completed and add the word that

was before the word that needs to be completed -}

return $ map (app bC) $ filter (isPrefixOf tC) $ allNames \\ fins

ReqConsCheck -> do

let tC = if isSpace $ lastChar input

then []

else lastString $ words input

bC = if isSpace $ lastChar input

then trimRight input

else unwords $ init $ words input

getCCName (G_cons_checker _ p) = ccName p

createConsCheckersList = map (getCCName . fst) . getAllConsCheckers

case i_state $ intState allState of

Nothing ->

{- not in proving mode !? you can not choose a consistency

checker here -}

return []

Just proofState ->

case cComorphism proofState of

-- some comorphism was used

Just c -> return $ map (app bC) $ filter (isPrefixOf tC)

$ createConsCheckersList [c]

Nothing ->

case elements proofState of

-- no elements selected

[] -> return []

c : _ -> case c of

Element z _ -> return $ map (app bC)

$ filter (isPrefixOf tC)

$ createConsCheckersList

$ findComorphismPaths logicGraph

(sublogicOfTheory z)

ReqProvers -> do

let bC : tl = words input

tC = unwords tl

{- find the last comorphism used if none use the

the comorphism of the first selected node -}

case i_state $ intState allState of

Nothing ->

{- not in proving mode !? you can not choose

provers here -}

return []

Just proofState ->

case elements proofState of

-- no elements selected

[] -> return []

-- use the first element to get a comorphism

c : _ -> case c of

Element z _ -> do

ps <- getUsableProvers ProveCMDLautomatic

(sublogicOfTheory z) logicGraph

let lst = nub $ map (getProverName . fst) ps

return $ map (app bC) $ filter (isPrefixOf tC) lst

ReqComorphism ->

let input'' = case words input of

cmd : s' -> unwords (cmd : concatMap (splitOn ':')

(concatMap (splitOn ';') s'))

_ -> input

input' = if elem (lastChar input) ";: " then

input'' ++ " " else input''

in case i_state $ intState allState of

Nothing -> return []

Just pS ->

case elements pS of

[] -> return []

Element st _ : _ ->

let tC = if isSpace $ lastChar input'

then []

else lastString $ words input'

appendC' =

map (\ coname -> case lookupComorphism_in_LG coname of

Result _ cmor -> cmor) $

tail $ words input'

appendC = sequence $ (if not (null appendC') &&

isNothing (last appendC')

then init else id) appendC'

comor = case appendC of

Nothing -> cComorphism pS

Just cs ->

foldl (\ c1 c2 -> maybe Nothing

(`compComorphism` c2) c1)

(cComorphism pS) cs

bC = if isSpace $ lastChar input'

then trimRight input'

else unwords $ init $ words input'

sl = case comor of

Just (Comorphism cid) ->

case sublogicOfTheory st of

G_sublogics lid sl2 ->

case coerceSublogic lid (sourceLogic cid) "" sl2 of

Just sl2' -> case mapSublogic cid sl2' of

Just sl1 -> G_sublogics (targetLogic cid) sl1

Nothing -> G_sublogics (targetLogic cid)

(top_sublogic $ targetLogic cid)

Nothing -> G_sublogics (targetLogic cid)

(top_sublogic $ targetLogic cid)

Nothing -> sublogicOfTheory st

cL = concatMap (\ (Comorphism cid) ->

[ language_name cid

| isSubElemG sl (G_sublogics

(sourceLogic cid)

(sourceSublogic cid)) ]

) comorphismList

in return $ map (app bC)

$ filter (isPrefixOf tC) cL

ReqLogic ->

let l' = lastString $ words input

i = unwords (init $ words input) ++ " "

in if elem '.' l'

then let (l, _ : sl) = Data.List.break (== '.') l'

in case Data.Map.lookup l $ logics logicGraph of

Just (Logic lid) -> return $ map ((i ++ l ++ ".") ++) $

filter (Data.List.isPrefixOf sl)

(map sublogicName $ all_sublogics lid)

Nothing -> return []

else return $ concatMap

(\ (n, Logic lid) ->

case map sublogicName $ all_sublogics lid of

[_] -> [i ++ n]

sls -> (i ++ n) : map

(\ sl -> i ++ n ++ "." ++ sl) sls) $

filter (Data.List.isPrefixOf l' . fst) $

Data.Map.toList $ logics logicGraph

ReqFile -> do

-- the incomplete path introduced until now

let initwd = if isSpace $ lastChar input

then []

else lastString $ words input

{- the folder in which to look for (it might be

empty) -}

tmpPath = reverse $ dropWhile (/= '/') $ reverse initwd

{- in case no folder was introduced yet look into

current folder -}

lastPath = case tmpPath of

[] -> "./"

_ -> tmpPath

{- the name of file/directory that needs to be

completed from the already introduced path -}

tC = reverse $ takeWhile (/= '/') $ reverse initwd

bC = if isSpace $ lastChar input

then input

else unwords (init $ words input) ++ " " ++ tmpPath

-- leave just folders and files with extenstion .casl

b' <- doesDirectoryExist lastPath

ls <- if b' then getDirectoryContents lastPath else return []

names <- fileFilter lastPath ls []

{- case list contains only one name

then if it is a folder extend it -}

let names' = filter (isPrefixOf tC) names

names'' <- case safeTail names' of

{- check CMDL.Utils to see how it

works, function should be done with

something like map but that can handle

functions with IO

(mapIO !? couldn't make it work though) -}

[] -> fileExtend lastPath names' []

_ -> return names'

return $ map (bC ++) names''

ReqAxm b ->

case i_state $ intState allState of

Nothing -> return []

Just pS ->

do

let tC = if isSpace $ lastChar input

then []

else lastString $ words input

bC = if isSpace $ lastChar input

then trimRight input

else unwords $ init $ words input

return $ map (app bC) $ filter (isPrefixOf tC) $ nubOrd

$ concatMap (\ (Element st nb) ->

if b then map fst $ getAxioms st else

case getTh Do_translate nb allState of

Nothing -> []

Just th -> map fst $ filter

(maybe False (not . isProvedBasically) . snd)

$ getThGoals th)

$ elements pS

ReqNumber -> case words input of

[hd] -> return $ map (app hd) s0_9

_ : _ : [] -> return $ if isSpace $ lastChar input

then []

else map (input ++) s0_9

_ -> return []

ReqNothing -> return []

ReqUnknown -> return []