Safe Haskell | None |
---|---|
Language | Haskell98 |
- type BareM = WriterT [Warn] (ExceptT Error (StateT BareEnv IO))
- type Warn = String
- type TCEnv = HashMap TyCon RTyCon
- data BareEnv = BE {}
- type InlnEnv = HashMap Symbol LMap
- inModule :: ModName -> BareM b -> BareM b
- withVArgs :: (Foldable t, PPrint a) => SourcePos -> SourcePos -> t a -> BareM b -> BareM b
- setRTAlias :: Symbol -> RTAlias RTyVar SpecType -> BareM ()
- setREAlias :: Symbol -> RTAlias Symbol Expr -> BareM ()
- setDataDecls :: [DataDecl] -> BareM ()
- execBare :: BareM a -> BareEnv -> IO (Either Error a)
- insertLogicEnv :: String -> LocSymbol -> [Symbol] -> Expr -> BareM ()
- insertAxiom :: Var -> Maybe Symbol -> BareM ()
- addDefs :: HashSet (Var, Symbol) -> BareM ()
- type DataConMap = HashMap (Symbol, Int) Symbol
- dataConMap :: [DataDecl] -> DataConMap
Documentation
type BareM = WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) Source #
Error-Reader-IO For Bare Transformation -----------------------------------
setREAlias :: Symbol -> RTAlias Symbol Expr -> BareM () Source #
setDataDecls :: [DataDecl] -> BareM () Source #
Exact DataConstructor Functions
type DataConMap = HashMap (Symbol, Int) Symbol Source #
DataConMap
stores the names of those ctor-fields that have been declared
as SMT ADTs so we don't make up new names for them.
dataConMap :: [DataDecl] -> DataConMap Source #