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
• famEnv :: !(HashMap Symbol DataCon)

  see NOTE:Family-Instance-Environment

• 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

NOTE:Family-Instance-Environment

For some reason, the usual lookup machinery (lookupGhcThing) refuses to properly lookup _imported_ names of family-instance data-constructors. e.g. see testsposExactGADT8.hs and testsposExactGADT9.hs; inside the latter, the lookupGhcThing fails to resolve the name of BlobXVal (but it works just fine when BlobXVal is a plain DataCon as in testsposExactGADT8a.hs To get around this hassle, we also save a map from _family instance_ DataCon-names to the corresponding family instance Tycon in the famEnv field of BareEnv. This map is *created* inside the function FIXME, and *used* inside the function FIXME.

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