Copilot.Theorem.Kind2

Documentation

module Copilot.Theorem.Kind2.Prover

prettyPrint :: File -> String

toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File

data Style

Constructors

Inlined

Modular

data File

Constructors

File

Fields

• filePreds :: [PredDef]
• fileProps :: [Prop]

data Prop

Constructors

Prop

Fields

• propName :: String
• propTerm :: Term

data PredDef

Constructors

PredDef

Fields

• predId :: String
• predStateVars :: [StateVarDef]
• predInit :: Term
• predTrans :: Term

data StateVarDef

Constructors

StateVarDef

Fields

• varId :: String
• varType :: Type
• varFlags :: [StateVarFlag]

data Type

Constructors

Int

Real

Bool

data StateVarFlag

Constructors

FConst

data PredType

Constructors

Init

Trans

data Term

Constructors

ValueLiteral String

PrimedStateVar String

StateVar String

FunApp String [Term]

PredApp String PredType [Term]