Language.Haskell.Liquid.Bare.Env

Documentation

type BareM = WriterT [Warn] (ExceptT Error (StateT BareEnv IO))

Error-Reader-IO For Bare Transformation -----------------------------------

type Warn = String

type TCEnv = HashMap TyCon RTyCon

data BareEnv

Constructors

BE

Fields

• modName :: !ModName
• tcEnv :: !TCEnv
• rtEnv :: !RTEnv
• varEnv :: !(HashMap Symbol Var)
• hscEnv :: !HscEnv
• logicEnv :: !LogicMap
• dcEnv :: !DataConMap
• bounds :: !RBEnv
• embeds :: !(TCEmb TyCon)
• axSyms :: !(HashMap Symbol LocSymbol)
• propSyms :: !(HashMap Symbol LocSymbol)
• beConfig :: !Config
• beIndex :: !Integer

Instances

HasConfig BareEnv

Methods

getConfig :: BareEnv -> Config

patternFlag :: BareEnv -> Bool

higherOrderFlag :: BareEnv -> Bool

pruneFlag :: BareEnv -> Bool

expandFlag :: BareEnv -> Bool

hasOpt :: BareEnv -> (Config -> Bool) -> Bool

totalityCheck :: BareEnv -> Bool

terminationCheck :: BareEnv -> Bool

Freshable BareM Integer

Methods

fresh :: BareM Integer

true :: Integer -> BareM Integer

refresh :: Integer -> BareM Integer

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 ()

Exact DataConstructor Functions

type DataConMap = HashMap (Symbol, Int) Symbol

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