ogma-core-1.15.0: Ogma: Helper tool to interoperate between Copilot and other languages.

Safe Haskell	None
Language	Haskell2010

Command.Overview

Description

Produce an overview of the input files.

Synopsis

command :: CommandOptions -> IO (Maybe CommandSummary, Result ErrorCode)
data CommandOptions = CommandOptions {
- commandInputFiles :: [OverviewFile]
}
data OverviewFile = OverviewFile {
- overviewFilePath :: FilePath
- overviewFileFormat :: String
- overviewFilePropFormat :: String
- overviewFilePropVia :: Maybe String
}
data CommandSummary = CommandSummary {
- commandSummaryRequirements :: [CommandSummaryRequirements]
- commandSummaryDiagrams :: [CommandSummaryDiagram]
}
data CommandSummaryRequirements = CommandSummaryRequirements {
}
data CommandSummaryDiagram = CommandSummaryDiagram {
}
type ErrorCode = Int

Documentation

command Source #

Arguments

:: CommandOptions	Customization options
-> IO (Maybe CommandSummary, Result ErrorCode)

Generate overview of a spec given in an input file.

PRE: The file given is readable, contains a valid file with recognizable format, the formulas in the file do not use any identifiers that exist in Copilot, or any of prop, clock, ftp, notPreviousNot. All identifiers used are valid C99 identifiers. The template, if provided, exists and uses the variables needed by the overview application generator. The target directory is writable and there's enough disk space to copy the files over.

data CommandOptions Source #

Options used to customize the interpretation of input specifications.

Constructors

CommandOptions
Fields commandInputFiles :: [OverviewFile]

data OverviewFile Source #

Information about one file in the command options.

Constructors

OverviewFile
Fields overviewFilePath :: FilePath overviewFileFormat :: String overviewFilePropFormat :: String overviewFilePropVia :: Maybe String

data CommandSummary Source #

Constructors

CommandSummary
Fields commandSummaryRequirements :: [CommandSummaryRequirements] commandSummaryDiagrams :: [CommandSummaryDiagram]

Instances

Instances details

ToJSON CommandSummary Source #

Instance details

Defined in Command.Overview

Methods

toJSON :: CommandSummary -> Value Source #

toEncoding :: CommandSummary -> Encoding Source #

toJSONList :: [CommandSummary] -> Value Source #

toEncodingList :: [CommandSummary] -> Encoding Source #

omitField :: CommandSummary -> Bool Source #

Monoid CommandSummary Source #

Instance details

Defined in Command.Overview

Methods

mempty :: CommandSummary Source #

mappend :: CommandSummary -> CommandSummary -> CommandSummary Source #

mconcat :: [CommandSummary] -> CommandSummary Source #

Semigroup CommandSummary Source #

Instance details

Defined in Command.Overview

Methods

(<>) :: CommandSummary -> CommandSummary -> CommandSummary Source #

sconcat :: NonEmpty CommandSummary -> CommandSummary Source #

stimes :: Integral b => b -> CommandSummary -> CommandSummary Source #

Generic CommandSummary Source #

Instance details

Defined in Command.Overview

Associated Types

type Rep CommandSummary

Instance details

Defined in Command.Overview

type Rep CommandSummary = D1 ('MetaData "CommandSummary" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummary" 'PrefixI 'True) (S1 ('MetaSel ('Just "commandSummaryRequirements") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CommandSummaryRequirements]) :*: S1 ('MetaSel ('Just "commandSummaryDiagrams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CommandSummaryDiagram])))

Methods

from :: CommandSummary -> Rep CommandSummary x Source #

to :: Rep CommandSummary x -> CommandSummary Source #

Show CommandSummary Source #

Instance details

Defined in Command.Overview

Methods

showsPrec :: Int -> CommandSummary -> ShowS Source #

show :: CommandSummary -> String Source #

showList :: [CommandSummary] -> ShowS Source #

type Rep CommandSummary Source #

Instance details

Defined in Command.Overview

type Rep CommandSummary = D1 ('MetaData "CommandSummary" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummary" 'PrefixI 'True) (S1 ('MetaSel ('Just "commandSummaryRequirements") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CommandSummaryRequirements]) :*: S1 ('MetaSel ('Just "commandSummaryDiagrams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CommandSummaryDiagram])))

data CommandSummaryRequirements Source #

Requirement data for inclusion in the summary.

Constructors

CommandSummaryRequirements
Fields commandRequirementsFile :: FilePath commandExternalVariables :: Int commandInternalVariables :: Int commandRequirements :: Int commandRequirementsTrue :: Int commandRequirementsFalse :: Int commandRequirementsConsistent :: Bool

Instances

Instances details

ToJSON CommandSummaryRequirements Source #

Instance details

Defined in Command.Overview

Methods

toJSON :: CommandSummaryRequirements -> Value Source #

toEncoding :: CommandSummaryRequirements -> Encoding Source #

toJSONList :: [CommandSummaryRequirements] -> Value Source #

toEncodingList :: [CommandSummaryRequirements] -> Encoding Source #

omitField :: CommandSummaryRequirements -> Bool Source #

Generic CommandSummaryRequirements Source #

Instance details

Defined in Command.Overview

Associated Types

type Rep CommandSummaryRequirements

Instance details

Defined in Command.Overview

type Rep CommandSummaryRequirements = D1 ('MetaData "CommandSummaryRequirements" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummaryRequirements" 'PrefixI 'True) ((S1 ('MetaSel ('Just "commandRequirementsFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "commandExternalVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandInternalVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :*: ((S1 ('MetaSel ('Just "commandRequirements") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandRequirementsTrue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "commandRequirementsFalse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandRequirementsConsistent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

Methods

from :: CommandSummaryRequirements -> Rep CommandSummaryRequirements x Source #

to :: Rep CommandSummaryRequirements x -> CommandSummaryRequirements Source #

Show CommandSummaryRequirements Source #

Instance details

Defined in Command.Overview

Methods

showsPrec :: Int -> CommandSummaryRequirements -> ShowS Source #

show :: CommandSummaryRequirements -> String Source #

showList :: [CommandSummaryRequirements] -> ShowS Source #

type Rep CommandSummaryRequirements Source #

Instance details

Defined in Command.Overview

type Rep CommandSummaryRequirements = D1 ('MetaData "CommandSummaryRequirements" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummaryRequirements" 'PrefixI 'True) ((S1 ('MetaSel ('Just "commandRequirementsFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "commandExternalVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandInternalVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :*: ((S1 ('MetaSel ('Just "commandRequirements") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandRequirementsTrue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "commandRequirementsFalse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandRequirementsConsistent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data CommandSummaryDiagram Source #

Diagram Data for inclusion in the summary.

Constructors

CommandSummaryDiagram
Fields commandDiagramFile :: FilePath commandDiagramNumStates :: Int commandDiagramDeterministic :: Bool

Instances

Instances details

ToJSON CommandSummaryDiagram Source #

Instance details

Defined in Command.Overview

Methods

toJSON :: CommandSummaryDiagram -> Value Source #

toEncoding :: CommandSummaryDiagram -> Encoding Source #

toJSONList :: [CommandSummaryDiagram] -> Value Source #

toEncodingList :: [CommandSummaryDiagram] -> Encoding Source #

omitField :: CommandSummaryDiagram -> Bool Source #

Generic CommandSummaryDiagram Source #

Instance details

Defined in Command.Overview

Associated Types

type Rep CommandSummaryDiagram

Instance details

Defined in Command.Overview

type Rep CommandSummaryDiagram = D1 ('MetaData "CommandSummaryDiagram" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummaryDiagram" 'PrefixI 'True) (S1 ('MetaSel ('Just "commandDiagramFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "commandDiagramNumStates") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandDiagramDeterministic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

Methods

from :: CommandSummaryDiagram -> Rep CommandSummaryDiagram x Source #

to :: Rep CommandSummaryDiagram x -> CommandSummaryDiagram Source #

Show CommandSummaryDiagram Source #

Instance details

Defined in Command.Overview

Methods

showsPrec :: Int -> CommandSummaryDiagram -> ShowS Source #

show :: CommandSummaryDiagram -> String Source #

showList :: [CommandSummaryDiagram] -> ShowS Source #

type Rep CommandSummaryDiagram Source #

Instance details

Defined in Command.Overview

type Rep CommandSummaryDiagram = D1 ('MetaData "CommandSummaryDiagram" "Command.Overview" "ogma-core-1.15.0-3hUeuqKaNPy9Y9bmZmPCXy" 'False) (C1 ('MetaCons "CommandSummaryDiagram" 'PrefixI 'True) (S1 ('MetaSel ('Just "commandDiagramFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "commandDiagramNumStates") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "commandDiagramDeterministic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

type ErrorCode = Int Source #

Encoding of reasons why the command can fail.