{- |

Module : $Header$

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

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

{ intState :: IntState -- ^ common interface state

, prompter :: CmdlPrompterState -- ^ promter of the interface

, openComment :: Bool -- ^ open comment

, connections :: [CmdlChannel] -- ^ opened connections

, output :: CmdlMessage -- ^ output of interface

, hetsOpts :: HetcatsOpts -- ^ hets command options

, errorCode :: Int

}

data ProveCmdType = Prove | Disprove | ConsCheck

-- | Creates an empty CmdlState

emptyCmdlState :: HetcatsOpts -> CmdlState

emptyCmdlState opts = CmdlState

{ intState = IntState

{ i_state = Nothing

, i_hist = IntHistory

{ undoList = []

, redoList = [] }

, filename = [] }

, prompter = CmdlPrompterState

{ fileLoaded = ""

, prompterHead = "> " }

, output = emptyCmdlMessage

, openComment = False

, connections = []

, hetsOpts = opts

, errorCode = 0

}

data CmdlPrompterState = CmdlPrompterState

{ fileLoaded :: String

, prompterHead :: String }

{- | Description of a command in order to have a uniform access to any of

the commands -}

data CmdlCmdDescription = CmdlCmdDescription

{ cmdDescription :: Command

, cmdPriority :: CmdlCmdPriority

, cmdFn :: CmdlCmdFnClasses

, cmdReq :: CmdlCmdRequirements }

instance Show CmdlCmdDescription where

show cmd = show $ cmdDescription cmd

cmdInput :: CmdlCmdDescription -> String

cmdInput = cmdInputStr . cmdDescription

cmdName :: CmdlCmdDescription -> String

cmdName = cmdNameStr . 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 r = let s = showRequirement r in

if null s then "" else '<' : s ++ ">"

showRequirement :: CmdlCmdRequirements -> String

showRequirement cr = case cr of

ReqConsCheck -> "ConsChecker"

ReqProvers -> "Prover"

ReqComorphism -> "Comorphism"

ReqLogic -> "Logic"

ReqNodesOrEdges n m -> maybe "" (\ f -> case f of

OpenCons -> "OpenCons"

OpenGoals -> "Goal") m

++ maybe "NodesOrEdges"

(\ b -> if b then "Nodes" else "Edges") n

ReqFile -> "File"

ReqAxm b -> if 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

{ chName :: String

, chType :: CmdlChannelType

, chHandler :: Handle

, chSocket :: Maybe CmdlSocket

, 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

{ socketHandler :: Socket

, socketHostName :: HostName

, 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

{ outputMsg :: String

, warningMsg :: String

, errorMsg :: String }

emptyCmdlMessage :: CmdlMessage

emptyCmdlMessage = CmdlMessage

{ errorMsg = []

, outputMsg = []

, warningMsg = [] }