{- |
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 :: CmdlCmdDescription -> CmdlState -> IO CmdlState
register2history dscr :: CmdlCmdDescription
dscr state :: CmdlState
state = do
    let oldHistory :: IntHistory
oldHistory = IntState -> IntHistory
i_hist (IntState -> IntHistory) -> IntState -> IntHistory
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state
    case IntHistory -> [CmdHistory]
undoList IntHistory
oldHistory of
       [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
       h :: CmdHistory
h : r :: [CmdHistory]
r -> case CmdHistory -> Command
command CmdHistory
h of
               CommentCmd _ -> do
                     let nwh :: CmdHistory
nwh = CmdHistory
h {
                                command :: Command
command = CmdlCmdDescription -> Command
cmdDescription CmdlCmdDescription
dscr }
                     CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state {
                         intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                            i_hist :: IntHistory
i_hist = IntHistory
oldHistory {
                               undoList :: [CmdHistory]
undoList = CmdHistory
nwh CmdHistory -> [CmdHistory] -> [CmdHistory]
forall a. a -> [a] -> [a]
: [CmdHistory]
r,
                               redoList :: [CmdHistory]
redoList = []
                             } } }
               _ -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state

-- process a comment line
processComment :: CmdlState -> String -> CmdlState
processComment :: CmdlState -> String -> CmdlState
processComment st :: CmdlState
st inp :: String
inp =
  if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "}%" String
inp then CmdlState
st { openComment :: Bool
openComment = Bool
False } else CmdlState
st

-- adds a line to the script
addToScript :: CmdlState -> IntIState -> String -> CmdlState
addToScript :: CmdlState -> IntIState -> String -> CmdlState
addToScript st :: CmdlState
st ist :: IntIState
ist str :: String
str
 = let olds :: ATPTacticScript
olds = IntIState -> ATPTacticScript
script IntIState
ist
       oldextOpts :: [String]
oldextOpts = ATPTacticScript -> [String]
tsExtraOpts ATPTacticScript
olds
   in CmdlState
st {
        intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
st) {
                     i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
ist {
                       script :: ATPTacticScript
script = ATPTacticScript
olds { tsExtraOpts :: [String]
tsExtraOpts = String
str String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
oldextOpts } }
          } }

checkCom :: CmdlCmdDescription -> CmdlState -> IO CmdlState
checkCom :: CmdlCmdDescription -> CmdlState -> IO CmdlState
checkCom descr :: CmdlCmdDescription
descr state :: CmdlState
state =
    -- check the priority of the current command
    case CmdlCmdDescription -> CmdlCmdPriority
cmdPriority CmdlCmdDescription
descr of
     CmdNoPriority ->
      -- check if there is open comment
      if CmdlState -> Bool
openComment CmdlState
state
       then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState -> String -> CmdlState
processComment CmdlState
state (String -> CmdlState) -> String -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> String
cmdInput CmdlCmdDescription
descr
       else
        case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
         Nothing -> CmdlCmdDescription -> CmdlState -> IO CmdlState
register2history CmdlCmdDescription
descr CmdlState
state
         Just ist :: IntIState
ist ->
          -- check if there is inside a script
          if IntIState -> Bool
loadScript IntIState
ist
            then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntIState -> String -> CmdlState
addToScript CmdlState
state IntIState
ist
                        (String -> CmdlState) -> String -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> String
cmdName CmdlCmdDescription
descr String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CmdlCmdDescription -> String
cmdInput CmdlCmdDescription
descr
            else CmdlCmdDescription -> CmdlState -> IO CmdlState
register2history CmdlCmdDescription
descr CmdlState
state
     CmdGreaterThanComments ->
      case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
       Nothing -> CmdlCmdDescription -> CmdlState -> IO CmdlState
register2history CmdlCmdDescription
descr CmdlState
state
       Just ist :: IntIState
ist ->
        if IntIState -> Bool
loadScript IntIState
ist
          then CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntIState -> String -> CmdlState
addToScript CmdlState
state IntIState
ist
                      (String -> CmdlState) -> String -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> String
cmdName CmdlCmdDescription
descr String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CmdlCmdDescription -> String
cmdInput CmdlCmdDescription
descr
          else CmdlCmdDescription -> CmdlState -> IO CmdlState
register2history CmdlCmdDescription
descr CmdlState
state
     CmdGreaterThanScriptAndComments -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state

-- | Function handle a comment line
cComment :: String -> CmdlState -> IO CmdlState
cComment :: String -> CmdlState -> IO CmdlState
cComment _ = CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return

-- For normal keyboard input

cOpenComment :: String -> CmdlState -> IO CmdlState
cOpenComment :: String -> CmdlState -> IO CmdlState
cOpenComment _ state :: CmdlState
state = CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state { openComment :: Bool
openComment = Bool
True }

cCloseComment :: CmdlState -> IO CmdlState
cCloseComment :: CmdlState -> IO CmdlState
cCloseComment state :: CmdlState
state = CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state { openComment :: Bool
openComment = Bool
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 :: [CmdlCmdDescription] -> String -> String
subtractCommandName allcmds :: [CmdlCmdDescription]
allcmds input :: String
input =
  let inp :: String
inp = String -> String
trimLeft String
input
  in case (CmdlCmdDescription -> Maybe String)
-> [CmdlCmdDescription] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
`stripPrefix` String
inp) (String -> Maybe String)
-> (CmdlCmdDescription -> String)
-> CmdlCmdDescription
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> String
cmdName) [CmdlCmdDescription]
allcmds of
       [] -> String
inp
       hd :: String
hd : _ -> String
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 :: String -> String
getCmdName inp :: String
inp = case String -> [String]
words String
inp of
    [] -> []
    hw :: String
hw : tws :: [String]
tws -> case [String]
tws of
      [] -> String
hw
      hwd :: String
hwd : _ -> let
        cs :: [String]
cs = ["dg", "del", "set"]
        csa :: [String]
csa = "add" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
cs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-all") [String]
cs
        in if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
hw [String]
csa then String
hw String -> String -> String
forall a. [a] -> [a] -> [a]
++ ' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
hwd else String
hw

{- | The function determines the requirements of the command
   name found at the begining of the string -}
getTypeOf :: [CmdlCmdDescription] -> String -> CmdlCmdRequirements
getTypeOf :: [CmdlCmdDescription] -> String -> CmdlCmdRequirements
getTypeOf allcmds :: [CmdlCmdDescription]
allcmds input :: String
input
 = let nwInput :: String
nwInput = String -> String
getCmdName String
input
       tmp :: [CmdlCmdRequirements]
tmp = (CmdlCmdDescription -> [CmdlCmdRequirements])
-> [CmdlCmdDescription] -> [CmdlCmdRequirements]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ x :: CmdlCmdDescription
x -> case (String -> Bool) -> [String] -> Maybe String
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nwInput) [CmdlCmdDescription -> String
cmdName CmdlCmdDescription
x] of
                                Nothing -> []
                                Just _ -> [CmdlCmdDescription -> CmdlCmdRequirements
cmdReq CmdlCmdDescription
x]) [CmdlCmdDescription]
allcmds
   in case [CmdlCmdRequirements]
tmp of
       result :: CmdlCmdRequirements
result : [] -> CmdlCmdRequirements
result
       _ -> CmdlCmdRequirements
ReqUnknown

nodeNames :: [(a, DGNodeLab)] -> [String]
nodeNames :: [(a, DGNodeLab)] -> [String]
nodeNames = ((a, DGNodeLab) -> String) -> [(a, DGNodeLab)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (DGNodeLab -> String
getDGNodeName (DGNodeLab -> String)
-> ((a, DGNodeLab) -> DGNodeLab) -> (a, DGNodeLab) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, DGNodeLab) -> DGNodeLab
forall a b. (a, b) -> b
snd)

{- | The function provides a list of possible completion
   to a given input if any -}
cmdlCompletionFn :: [CmdlCmdDescription] -> CmdlState -> String -> IO [String]
cmdlCompletionFn :: [CmdlCmdDescription] -> CmdlState -> String -> IO [String]
cmdlCompletionFn allcmds :: [CmdlCmdDescription]
allcmds allState :: CmdlState
allState input :: String
input =
   let s0_9 :: [String]
s0_9 = (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [0 .. (9 :: Int)]
       app :: String -> String -> String
app h :: String
h = (String
h String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (' ' Char -> String -> String
forall a. a -> [a] -> [a]
:)
   in case [CmdlCmdDescription] -> String -> CmdlCmdRequirements
getTypeOf [CmdlCmdDescription]
allcmds String
input of
   ReqNodesOrEdges mn :: Maybe Bool
mn mf :: Maybe NodeOrEdgeFilter
mf ->
    case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
allState of
     Nothing -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     Just state :: IntIState
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 :: [LNode DGNodeLab]
ns = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
state
           fns :: [String]
fns = [LNode DGNodeLab] -> [String]
forall a. [(a, DGNodeLab)] -> [String]
nodeNames ([LNode DGNodeLab] -> [String]) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> a -> b
$ ([LNode DGNodeLab] -> [LNode DGNodeLab])
-> (NodeOrEdgeFilter -> [LNode DGNodeLab] -> [LNode DGNodeLab])
-> Maybe NodeOrEdgeFilter
-> [LNode DGNodeLab]
-> [LNode DGNodeLab]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. a -> a
id (\ f :: NodeOrEdgeFilter
f -> (LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, nd :: DGNodeLab
nd) ->
                     case NodeOrEdgeFilter
f of
                       OpenCons -> Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus Bool
False DGNodeLab
nd
                       OpenGoals -> DGNodeLab -> Bool
hasOpenGoals DGNodeLab
nd))
                     Maybe NodeOrEdgeFilter
mf [LNode DGNodeLab]
ns
           es :: [String]
es = ((String, LEdge DGLinkLab) -> String)
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, LEdge DGLinkLab) -> String
forall a b. (a, b) -> a
fst
                ([(String, LEdge DGLinkLab)] -> [String])
-> [(String, LEdge DGLinkLab)] -> [String]
forall a b. (a -> b) -> a -> b
$ ([(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)])
-> (NodeOrEdgeFilter
    -> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)])
-> Maybe NodeOrEdgeFilter
-> [(String, LEdge DGLinkLab)]
-> [(String, LEdge DGLinkLab)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)]
forall a. a -> a
id (\ f :: NodeOrEdgeFilter
f -> ((String, LEdge DGLinkLab) -> Bool)
-> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (((String, LEdge DGLinkLab) -> Bool)
 -> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)])
-> ((String, LEdge DGLinkLab) -> Bool)
-> [(String, LEdge DGLinkLab)]
-> [(String, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ case NodeOrEdgeFilter
f of
                    OpenCons -> LEdge DGLinkLab -> Bool
isOpenConsEdge
                    OpenGoals -> LEdge DGLinkLab -> Bool
edgeContainsGoals
                  (LEdge DGLinkLab -> Bool)
-> ((String, LEdge DGLinkLab) -> LEdge DGLinkLab)
-> (String, LEdge DGLinkLab)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, LEdge DGLinkLab) -> LEdge DGLinkLab
forall a b. (a, b) -> b
snd) Maybe NodeOrEdgeFilter
mf
                ([(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)])
-> [(String, LEdge DGLinkLab)] -> [(String, LEdge DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab]
-> [LEdge DGLinkLab] -> [(String, LEdge DGLinkLab)]
createEdgeNames [LNode DGNodeLab]
ns (IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
state)
           allNames :: [String]
allNames = case Maybe Bool
mn of
             Nothing -> [String]
es [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
fns
             Just b :: Bool
b -> if Bool
b then [String]
fns else [String]
es
           (fins :: [String]
fins, tC :: String
tC) = [String] -> String -> ([String], String)
finishedNames [String]
allNames
              (String -> ([String], String)) -> String -> ([String], String)
forall a b. (a -> b) -> a -> b
$ [CmdlCmdDescription] -> String -> String
subtractCommandName [CmdlCmdDescription]
allcmds String
input
           -- what is before tC
           bC :: String
bC = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
trimLeft (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
tC) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
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 -}
       [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
allNames [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
fins
   ReqConsCheck -> do
       let tC :: String
tC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                 then []
                 else [String] -> String
lastString ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
           bC :: String
bC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                 then String -> String
trimRight String
input
                 else [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
           getCCName :: G_cons_checker -> String
getCCName (G_cons_checker _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p) = ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
p
           createConsCheckersList :: [AnyComorphism] -> [String]
createConsCheckersList = ((G_cons_checker, AnyComorphism) -> String)
-> [(G_cons_checker, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (G_cons_checker -> String
getCCName (G_cons_checker -> String)
-> ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> (G_cons_checker, AnyComorphism)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst) ([(G_cons_checker, AnyComorphism)] -> [String])
-> ([AnyComorphism] -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers
       case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
allState of
        Nothing ->
         {- not in proving mode !? you can not choose a consistency
            checker here -}
               [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just proofState :: IntIState
proofState ->
         case IntIState -> Maybe AnyComorphism
cComorphism IntIState
proofState of
          -- some comorphism was used
          Just c :: AnyComorphism
c -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC)
                   ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism] -> [String]
createConsCheckersList [AnyComorphism
c]
          Nothing ->
           case IntIState -> [Int_NodeInfo]
elements IntIState
proofState of
            -- no elements selected
            [] -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
            c :: Int_NodeInfo
c : _ -> case Int_NodeInfo
c of
               Element z :: ProofState
z _ -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC)
                               ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC)
                               ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism] -> [String]
createConsCheckersList
                               ([AnyComorphism] -> [String]) -> [AnyComorphism] -> [String]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph
                                   (ProofState -> G_sublogics
sublogicOfTheory ProofState
z)
   ReqProvers -> do
       let bC :: String
bC : tl :: [String]
tl = String -> [String]
words String
input
           tC :: String
tC = [String] -> String
unwords [String]
tl
      {- find the last comorphism used if none use the
         the comorphism of the first selected node -}
       case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
allState of
        Nothing ->
       {- not in proving mode !? you can not choose
          provers here -}
                [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just proofState :: IntIState
proofState ->
           case IntIState -> [Int_NodeInfo]
elements IntIState
proofState of
             -- no elements selected
             [] -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
             -- use the first element to get a comorphism
             c :: Int_NodeInfo
c : _ -> case Int_NodeInfo
c of
                Element z :: ProofState
z _ -> do
                  [(G_prover, AnyComorphism)]
ps <- ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers ProverKind
ProveCMDLautomatic
                          (ProofState -> G_sublogics
sublogicOfTheory ProofState
z) LogicGraph
logicGraph
                  let lst :: [String]
lst = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ((G_prover, AnyComorphism) -> String)
-> [(G_prover, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (G_prover -> String
getProverName (G_prover -> String)
-> ((G_prover, AnyComorphism) -> G_prover)
-> (G_prover, AnyComorphism)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_prover, AnyComorphism) -> G_prover
forall a b. (a, b) -> a
fst) [(G_prover, AnyComorphism)]
ps
                  [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC) [String]
lst
   ReqComorphism ->
    let input'' :: String
input'' = case String -> [String]
words String
input of
                   cmd :: String
cmd : s' :: [String]
s' -> [String] -> String
unwords (String
cmd String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ':')
                                               ((String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ';') [String]
s'))
                   _ -> String
input
        input' :: String
input' = if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (String -> Char
lastChar String
input) ";: " then
                   String
input'' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " else String
input''
    in case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
allState of
         Nothing -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         Just pS :: IntIState
pS ->
          case IntIState -> [Int_NodeInfo]
elements IntIState
pS of
           [] -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           Element st :: ProofState
st _ : _ ->
              let tC :: String
tC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input'
                        then []
                        else [String] -> String
lastString ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input'
                  appendC' :: [Maybe AnyComorphism]
appendC' =
                   (String -> Maybe AnyComorphism)
-> [String] -> [Maybe AnyComorphism]
forall a b. (a -> b) -> [a] -> [b]
map (\ coname :: String
coname -> case String -> Result AnyComorphism
lookupComorphism_in_LG String
coname of
                                    Result _ cmor :: Maybe AnyComorphism
cmor -> Maybe AnyComorphism
cmor) ([String] -> [Maybe AnyComorphism])
-> [String] -> [Maybe AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                    [String] -> [String]
forall a. [a] -> [a]
tail ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input'
                  appendC :: Maybe [AnyComorphism]
appendC = [Maybe AnyComorphism] -> Maybe [AnyComorphism]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Maybe AnyComorphism] -> Maybe [AnyComorphism])
-> [Maybe AnyComorphism] -> Maybe [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ (if Bool -> Bool
not ([Maybe AnyComorphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Maybe AnyComorphism]
appendC') Bool -> Bool -> Bool
&&
                                            Maybe AnyComorphism -> Bool
forall a. Maybe a -> Bool
isNothing ([Maybe AnyComorphism] -> Maybe AnyComorphism
forall a. [a] -> a
last [Maybe AnyComorphism]
appendC')
                                         then [Maybe AnyComorphism] -> [Maybe AnyComorphism]
forall a. [a] -> [a]
init else [Maybe AnyComorphism] -> [Maybe AnyComorphism]
forall a. a -> a
id) [Maybe AnyComorphism]
appendC'
                  comor :: Maybe AnyComorphism
comor = case Maybe [AnyComorphism]
appendC of
                           Nothing -> IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS
                           Just cs :: [AnyComorphism]
cs ->
                            (Maybe AnyComorphism -> AnyComorphism -> Maybe AnyComorphism)
-> Maybe AnyComorphism -> [AnyComorphism] -> Maybe AnyComorphism
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ c1 :: Maybe AnyComorphism
c1 c2 :: AnyComorphism
c2 -> Maybe AnyComorphism
-> (AnyComorphism -> Maybe AnyComorphism)
-> Maybe AnyComorphism
-> Maybe AnyComorphism
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe AnyComorphism
forall a. Maybe a
Nothing
                             (AnyComorphism -> AnyComorphism -> Maybe AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
`compComorphism` AnyComorphism
c2) Maybe AnyComorphism
c1)
                             (IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS) [AnyComorphism]
cs
                  bC :: String
bC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input'
                        then String -> String
trimRight String
input'
                        else [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input'
                  sl :: G_sublogics
sl = case Maybe AnyComorphism
comor of
                        Just (Comorphism cid :: cid
cid) ->
                         case ProofState -> G_sublogics
sublogicOfTheory ProofState
st of
                          G_sublogics lid :: lid
lid sl2 :: sublogics
sl2 ->
                           case lid -> lid1 -> String -> sublogics -> Maybe sublogics1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> String -> sublogics1 -> m sublogics2
coerceSublogic lid
lid (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid) "" sublogics
sl2 of
                            Just sl2' :: sublogics1
sl2' -> case cid -> sublogics1 -> Maybe sublogics2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1 -> Maybe sublogics2
mapSublogic cid
cid sublogics1
sl2' of
                             Just sl1 :: sublogics2
sl1 -> lid2 -> sublogics2 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) sublogics2
sl1
                             Nothing -> lid2 -> sublogics2 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid)
                                          (lid2 -> sublogics2
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics
top_sublogic (lid2 -> sublogics2) -> lid2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid)
                            Nothing -> lid2 -> sublogics2 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid)
                                        (lid2 -> sublogics2
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics
top_sublogic (lid2 -> sublogics2) -> lid2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid)
                        Nothing -> ProofState -> G_sublogics
sublogicOfTheory ProofState
st
                  cL :: [String]
cL = (AnyComorphism -> [String]) -> [AnyComorphism] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Comorphism cid :: cid
cid) ->
                                  [ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
                                    | G_sublogics -> G_sublogics -> Bool
isSubElemG G_sublogics
sl (lid1 -> sublogics1 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics
                                         (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid)
                                         (cid -> sublogics1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic cid
cid)) ]
                                 ) [AnyComorphism]
comorphismList
              in [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC)
                        ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC) [String]
cL
   ReqLogic ->
    let l' :: String
l' = [String] -> String
lastString ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
        i :: String
i = [String] -> String
unwords ([String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " "
    in if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem '.' String
l'
       then let (l :: String
l, _ : sl :: String
sl) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
Data.List.break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') String
l'
            in case String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup String
l (Map String AnyLogic -> Maybe AnyLogic)
-> Map String AnyLogic -> Maybe AnyLogic
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph of
                Just (Logic lid :: lid
lid) -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".") String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
                                     (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
Data.List.isPrefixOf String
sl)
                                     ((sublogics -> String) -> [sublogics] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map sublogics -> String
forall l. SublogicName l => l -> String
sublogicName ([sublogics] -> [String]) -> [sublogics] -> [String]
forall a b. (a -> b) -> a -> b
$ lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
lid)
                Nothing -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
       else [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ ((String, AnyLogic) -> [String])
-> [(String, AnyLogic)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                     (\ (n :: String
n, Logic lid :: lid
lid) ->
                        case (sublogics -> String) -> [sublogics] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map sublogics -> String
forall l. SublogicName l => l -> String
sublogicName ([sublogics] -> [String]) -> [sublogics] -> [String]
forall a b. (a -> b) -> a -> b
$ lid -> [sublogics]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [sublogics]
all_sublogics lid
lid of
                         [_] -> [String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n]
                         sls :: [String]
sls -> (String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
                          (\ sl :: String
sl -> String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sl) [String]
sls) ([(String, AnyLogic)] -> [String])
-> [(String, AnyLogic)] -> [String]
forall a b. (a -> b) -> a -> b
$
                     ((String, AnyLogic) -> Bool)
-> [(String, AnyLogic)] -> [(String, AnyLogic)]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
Data.List.isPrefixOf String
l' (String -> Bool)
-> ((String, AnyLogic) -> String) -> (String, AnyLogic) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, AnyLogic) -> String
forall a b. (a, b) -> a
fst) ([(String, AnyLogic)] -> [(String, AnyLogic)])
-> [(String, AnyLogic)] -> [(String, AnyLogic)]
forall a b. (a -> b) -> a -> b
$
                     Map String AnyLogic -> [(String, AnyLogic)]
forall k a. Map k a -> [(k, a)]
Data.Map.toList (Map String AnyLogic -> [(String, AnyLogic)])
-> Map String AnyLogic -> [(String, AnyLogic)]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph
   ReqFile -> do
        -- the incomplete path introduced until now
        let initwd :: String
initwd = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                      then []
                      else [String] -> String
lastString ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
        {- the folder in which to look for (it might be
           empty) -}
            tmpPath :: String
tmpPath = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '/') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
initwd
        {- in case no folder was introduced yet look into
           current folder -}
            lastPath :: String
lastPath = case String
tmpPath of
                       [] -> "./"
                       _ -> String
tmpPath
        {- the name of file/directory that needs to be
           completed from the already introduced path -}
            tC :: String
tC = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '/') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
initwd
            bC :: String
bC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                  then String
input
                  else [String] -> String
unwords ([String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tmpPath
        -- leave just folders and files with extenstion .casl
        Bool
b' <- String -> IO Bool
doesDirectoryExist String
lastPath
        [String]
ls <- if Bool
b' then String -> IO [String]
getDirectoryContents String
lastPath else [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        [String]
names <- String -> [String] -> [String] -> IO [String]
fileFilter String
lastPath [String]
ls []
        {- case list contains only one name
           then if it is a folder extend it -}
        let names' :: [String]
names' = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC) [String]
names
        [String]
names'' <- case [String] -> [String]
forall a. [a] -> [a]
safeTail [String]
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) -}
                   [] -> String -> [String] -> [String] -> IO [String]
fileExtend String
lastPath [String]
names' []
                   _ -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
names'
        [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
bC String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
names''
   ReqAxm b :: Bool
b ->
      case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
allState of
       Nothing -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
       Just pS :: IntIState
pS ->
        do
         let tC :: String
tC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                    then []
                    else [String] -> String
lastString ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
             bC :: String
bC = if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                    then String -> String
trimRight String
input
                    else [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
input
         [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
bC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tC) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd
           ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Int_NodeInfo -> [String]) -> [Int_NodeInfo] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Element st :: ProofState
st nb :: Int
nb) ->
               if Bool
b then ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst ([(String, Bool)] -> [String]) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> a -> b
$ ProofState -> [(String, Bool)]
getAxioms ProofState
st else
                        case CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory
getTh CmdlUseTranslation
Do_translate Int
nb CmdlState
allState of
                        Nothing -> []
                        Just th :: G_theory
th -> ((String, Maybe BasicProof) -> String)
-> [(String, Maybe BasicProof)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Maybe BasicProof) -> String
forall a b. (a, b) -> a
fst ([(String, Maybe BasicProof)] -> [String])
-> [(String, Maybe BasicProof)] -> [String]
forall a b. (a -> b) -> a -> b
$ ((String, Maybe BasicProof) -> Bool)
-> [(String, Maybe BasicProof)] -> [(String, Maybe BasicProof)]
forall a. (a -> Bool) -> [a] -> [a]
filter
                            (Bool -> (BasicProof -> Bool) -> Maybe BasicProof -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not (Bool -> Bool) -> (BasicProof -> Bool) -> BasicProof -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BasicProof -> Bool
isProvedBasically) (Maybe BasicProof -> Bool)
-> ((String, Maybe BasicProof) -> Maybe BasicProof)
-> (String, Maybe BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Maybe BasicProof) -> Maybe BasicProof
forall a b. (a, b) -> b
snd)
                            ([(String, Maybe BasicProof)] -> [(String, Maybe BasicProof)])
-> [(String, Maybe BasicProof)] -> [(String, Maybe BasicProof)]
forall a b. (a -> b) -> a -> b
$ G_theory -> [(String, Maybe BasicProof)]
getThGoals G_theory
th)
                ([Int_NodeInfo] -> [String]) -> [Int_NodeInfo] -> [String]
forall a b. (a -> b) -> a -> b
$ IntIState -> [Int_NodeInfo]
elements IntIState
pS
   ReqNumber -> case String -> [String]
words String
input of
                   [hd :: String
hd] -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
app String
hd) [String]
s0_9
                   _ : _ : [] -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ if Char -> Bool
isSpace (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Char
lastChar String
input
                          then []
                          else (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
input String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
s0_9
                   _ -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
   ReqNothing -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
   ReqUnknown -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []