copilot-sbv-2.2.1: A compiler for CoPilot targeting SBV.

Safe Haskell	None
Language	Haskell2010

Copilot.Compile.SBV.Copilot2SBV

Documentation

c2sExpr :: Inputs -> Expr a -> SBV a Source #

data Inputs Source #

Constructors

Inputs
Fields extVars :: [Ext] extArrs :: [Ext] extFuns :: [Ext] extQues :: [ExtQue]

type Ext = (Name, ExtInput) Source #

type ExtQue = (Id, QueInput) Source #

data ExtInput Source #

Constructors

ExtInput
Fields extInput :: SBV a extType :: Type a

data QueInput Source #

Constructors

QueInput
Fields arrInput :: QueueIn a

data QueueIn a Source #

Constructors

QueueIn
Fields queue :: [SBV a] quePtr :: SBV QueueSize arrType :: Type a