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

Copilot.Compile.SBV.Copilot2SBV

Documentation

c2sExpr :: [Input] -> Expr a -> SBV aSource

data Input Source

Constructors

ExtIn Name ExtInput 
ArrIn Id ArrInput 

data ExtInput Source

Constructors

forall a . ExtInput 

Fields

extInput :: SBV a
 
extType :: Type a
 

data ArrInput Source

Constructors

forall a . ArrInput 

Fields

arrInput :: QueueIn a
 

data QueueIn a Source

Constructors

QueueIn 

Fields

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