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

Safe HaskellSafe-Infered

Copilot.Compile.SBV.Copilot2SBV

Documentation

c2sExpr :: Inputs -> Expr a -> SBV aSource

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

forall a . ExtInput 

Fields

extInput :: SBV a
 
extType :: Type a
 

data QueInput Source

Constructors

forall a . QueInput 

Fields

arrInput :: QueueIn a
 

data QueueIn a Source

Constructors

QueueIn 

Fields

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