{- |
Module      : ./CMDL/DataTypes.hs
Description : Internal data types of the CMDL interface
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.DataTypes describes the internal states(or datatypes) of the CMDL
interface.
-}


module CMDL.DataTypes
  ( CmdlState (..)
  , emptyCmdlState
  , CmdlCmdDescription (..)
  , cmdInput
  , cmdName
  , CmdlCmdPriority (..)
  , CmdlCmdFnClasses (..)
  , NodeOrEdgeFilter (..)
  , CmdlCmdRequirements (..)
  , formatRequirement
  , CmdlChannel (..)
  , CmdlChannelType (..)
  , CmdlChannelProperties (..)
  , CmdlSocket (..)
  , CmdlUseTranslation (..)
  , CmdlProverConsChecker (..)
  , CmdlPrompterState (..)
  , CmdlMessage (..)
  , emptyCmdlMessage
  , CmdlListAction (..)
  , CmdlGoalAxiom (..)
  , ProveCmdType (..)
  ) where

import Interfaces.DataTypes
import Interfaces.Command

import Driver.Options

import Network.Socket

import Proofs.AbstractState (G_cons_checker)

import System.IO (Handle)

data CmdlGoalAxiom =
    ChangeGoals
  | ChangeAxioms

data CmdlProverConsChecker =
    Use_prover
  | Use_consChecker

data CmdlUseTranslation =
    Do_translate
  | Dont_translate

-- * CMDL datatypes

{- | CMDLState contains all information the CMDL interface
   might use at any time. -}
data CmdlState = CmdlState
  { CmdlState -> IntState
intState :: IntState -- ^ common interface state
  , CmdlState -> CmdlPrompterState
prompter :: CmdlPrompterState -- ^ promter of the interface
  , CmdlState -> Bool
openComment :: Bool -- ^ open comment
  , CmdlState -> [CmdlChannel]
connections :: [CmdlChannel] -- ^ opened connections
  , CmdlState -> CmdlMessage
output :: CmdlMessage -- ^ output of interface
  , CmdlState -> HetcatsOpts
hetsOpts :: HetcatsOpts  -- ^ hets command options
  , CmdlState -> Int
errorCode :: Int
  , CmdlState -> [G_cons_checker]
consCheckers :: [G_cons_checker]
  }

data ProveCmdType = Prove | Disprove | ConsCheck

-- | Creates an empty CmdlState
emptyCmdlState :: HetcatsOpts -> CmdlState
emptyCmdlState :: HetcatsOpts -> CmdlState
emptyCmdlState opts :: HetcatsOpts
opts = CmdlState :: IntState
-> CmdlPrompterState
-> Bool
-> [CmdlChannel]
-> CmdlMessage
-> HetcatsOpts
-> Int
-> [G_cons_checker]
-> CmdlState
CmdlState
  { intState :: IntState
intState = IntState :: IntHistory -> Maybe IntIState -> String -> IntState
IntState
      { i_state :: Maybe IntIState
i_state = Maybe IntIState
forall a. Maybe a
Nothing
      , i_hist :: IntHistory
i_hist = IntHistory :: [CmdHistory] -> [CmdHistory] -> IntHistory
IntHistory
          { undoList :: [CmdHistory]
undoList = []
          , redoList :: [CmdHistory]
redoList = [] }
      , filename :: String
filename = [] }
  , prompter :: CmdlPrompterState
prompter = CmdlPrompterState :: String -> String -> CmdlPrompterState
CmdlPrompterState
      { fileLoaded :: String
fileLoaded = ""
      , prompterHead :: String
prompterHead = "> " }
  , output :: CmdlMessage
output = CmdlMessage
emptyCmdlMessage
  , openComment :: Bool
openComment = Bool
False
  , connections :: [CmdlChannel]
connections = []
  , hetsOpts :: HetcatsOpts
hetsOpts = HetcatsOpts
opts
  , errorCode :: Int
errorCode = 0
  , consCheckers :: [G_cons_checker]
consCheckers = []
}

data CmdlPrompterState = CmdlPrompterState
  { CmdlPrompterState -> String
fileLoaded :: String
  , CmdlPrompterState -> String
prompterHead :: String }

{- | Description of a command in order to have a uniform access to any of
   the commands -}
data CmdlCmdDescription = CmdlCmdDescription
  { CmdlCmdDescription -> Command
cmdDescription :: Command
  , CmdlCmdDescription -> CmdlCmdPriority
cmdPriority :: CmdlCmdPriority
  , CmdlCmdDescription -> CmdlCmdFnClasses
cmdFn :: CmdlCmdFnClasses
  , CmdlCmdDescription -> CmdlCmdRequirements
cmdReq :: CmdlCmdRequirements }

instance Show CmdlCmdDescription where
  show :: CmdlCmdDescription -> String
show cmd :: CmdlCmdDescription
cmd = Command -> String
forall a. Show a => a -> String
show (Command -> String) -> Command -> String
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> Command
cmdDescription CmdlCmdDescription
cmd

cmdInput :: CmdlCmdDescription -> String
cmdInput :: CmdlCmdDescription -> String
cmdInput = Command -> String
cmdInputStr (Command -> String)
-> (CmdlCmdDescription -> Command) -> CmdlCmdDescription -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> Command
cmdDescription

cmdName :: CmdlCmdDescription -> String
cmdName :: CmdlCmdDescription -> String
cmdName = Command -> String
cmdNameStr (Command -> String)
-> (CmdlCmdDescription -> Command) -> CmdlCmdDescription -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> Command
cmdDescription

{- | Some commands have different status, for example 'end-script'
   needs to be processed even though the interface is in reading script
   state. The same happens with '}%' even though the interface is in
   multi line comment state. In order not to treat this few commands
   separately from the other it is easy just to give to all commands
   different priorities -}
data CmdlCmdPriority =
    CmdNoPriority
  | CmdGreaterThanComments
  | CmdGreaterThanScriptAndComments

{- | Any command belongs to one of the following classes of functions,
   a) f :: s -> IO s
   b) f :: String -> s -> IO s -}
data CmdlCmdFnClasses =
    CmdNoInput (CmdlState -> IO CmdlState)
  | CmdWithInput (String -> CmdlState -> IO CmdlState)

data NodeOrEdgeFilter = OpenCons | OpenGoals

{- | Datatype describing the types of commands according
   to what they expect as input -}
data CmdlCmdRequirements =
    ReqNodesOrEdges (Maybe Bool) (Maybe NodeOrEdgeFilter)
        -- ^ Nothing: Both, True: Nodes, False: Edges
  | ReqProvers
  | ReqConsCheck
  | ReqComorphism
  | ReqLogic
  | ReqFile
  | ReqAxm Bool   -- ^ True: Axioms, False: Goals
  | ReqNumber
  | ReqNothing
  | ReqUnknown

formatRequirement :: CmdlCmdRequirements -> String
formatRequirement :: CmdlCmdRequirements -> String
formatRequirement r :: CmdlCmdRequirements
r = let s :: String
s = CmdlCmdRequirements -> String
showRequirement CmdlCmdRequirements
r in
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then "" else '<' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ">"

showRequirement :: CmdlCmdRequirements -> String
showRequirement :: CmdlCmdRequirements -> String
showRequirement cr :: CmdlCmdRequirements
cr = case CmdlCmdRequirements
cr of
    ReqConsCheck -> "ConsChecker"
    ReqProvers -> "Prover"
    ReqComorphism -> "Comorphism"
    ReqLogic -> "Logic"
    ReqNodesOrEdges n :: Maybe Bool
n m :: Maybe NodeOrEdgeFilter
m -> String
-> (NodeOrEdgeFilter -> String) -> Maybe NodeOrEdgeFilter -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\ f :: NodeOrEdgeFilter
f -> case NodeOrEdgeFilter
f of
        OpenCons -> "OpenCons"
        OpenGoals -> "Goal") Maybe NodeOrEdgeFilter
m
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (Bool -> String) -> Maybe Bool -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "NodesOrEdges"
         (\ b :: Bool
b -> if Bool
b then "Nodes" else "Edges") Maybe Bool
n
    ReqFile -> "File"
    ReqAxm b :: Bool
b -> if Bool
b then "Axioms" else "Goals"
    ReqNumber -> "Number"
    ReqNothing -> ""
    ReqUnknown -> ""

-- Communication channel datatypes -----------------------------------------

{- | CMDLSocket takes care of opened sockets for comunication with other
   application like the Broker in the case of PGIP -}
data CmdlChannel = CmdlChannel
  { CmdlChannel -> String
chName :: String
  , CmdlChannel -> CmdlChannelType
chType :: CmdlChannelType
  , CmdlChannel -> Handle
chHandler :: Handle
  , CmdlChannel -> Maybe CmdlSocket
chSocket :: Maybe CmdlSocket
  , CmdlChannel -> CmdlChannelProperties
chProperties :: CmdlChannelProperties }

-- | Channel type describes different type of channel
data CmdlChannelType =
    ChSocket
  | ChFile
  | ChStdin
  | ChStdout

-- | Channel properties describes what a channel can do
data CmdlChannelProperties =
    ChRead
  | ChWrite
  | ChReadWrite

-- | Describes a socket
data CmdlSocket = CmdlSocket
  { CmdlSocket -> Socket
socketHandler :: Socket
  , CmdlSocket -> String
socketHostName :: HostName
  , CmdlSocket -> PortNumber
socketPortNumber :: PortNumber }

{- | Datatype describing the list of possible action on a list
   of selected items -}
data CmdlListAction =
    ActionSet
  | ActionSetAll
  | ActionDel
  | ActionDelAll
  | ActionAdd

-- | output message given by the interface
data CmdlMessage = CmdlMessage
  { CmdlMessage -> String
outputMsg :: String
  , CmdlMessage -> String
warningMsg :: String
  , CmdlMessage -> String
errorMsg :: String }

emptyCmdlMessage :: CmdlMessage
emptyCmdlMessage :: CmdlMessage
emptyCmdlMessage = CmdlMessage :: String -> String -> String -> CmdlMessage
CmdlMessage
  { errorMsg :: String
errorMsg = []
  , outputMsg :: String
outputMsg = []
  , warningMsg :: String
warningMsg = [] }