Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Bare.DataType

Contents

Names for accessing Data Constuctors
Constructors

Synopsis

dataConMap :: [DataDecl] -> DataConMap
makeDataConChecker :: DataCon -> Symbol
makeDataConSelector :: Maybe DataConMap -> DataCon -> Int -> Symbol
addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
makeDataDecls :: Config -> TCEmb TyCon -> ModName -> [(ModName, TyCon, DataPropDecl)] -> [Located DataConP] -> [DataDecl]
makeConTypes :: Env -> (ModName, BareSpec) -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeRecordSelectorSigs :: Env -> ModName -> [Located DataConP] -> [(Var, LocSpecType)]
meetDataConSpec :: TCEmb TyCon -> [(Var, SpecType)] -> [DataConP] -> [(Var, SpecType)]

Documentation

dataConMap :: [DataDecl] -> DataConMap 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.

Names for accessing Data Constuctors

makeDataConChecker :: DataCon -> Symbol Source #

'makeDataConChecker d' creates the measure for `is$d` which tests whether a given value was created by d. e.g. is$Nil or is$Cons.

makeDataConSelector :: Maybe DataConMap -> DataCon -> Int -> Symbol Source #

'makeDataConSelector d' creates the selector `select$d$i` which projects the i-th field of a constructed value. e.g. `select$Cons$1` and `select$Cons$2` are respectively equivalent to head and tail.

addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon Source #

makeClassEmbeds: sort-embeddings for numeric, and family-instance tycons

Constructors

makeDataDecls :: Config -> TCEmb TyCon -> ModName -> [(ModName, TyCon, DataPropDecl)] -> [Located DataConP] -> [DataDecl] Source #

makeConTypes :: Env -> (ModName, BareSpec) -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]) Source #

Bare Predicate: DataCon Definitions ---------------------------------------

makeRecordSelectorSigs :: Env -> ModName -> [Located DataConP] -> [(Var, LocSpecType)] Source #

meetDataConSpec :: TCEmb TyCon -> [(Var, SpecType)] -> [DataConP] -> [(Var, SpecType)] Source #