liquidhaskell-0.8.10.1: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Bare.DataType

Synopsis

Documentation

dataConMap :: [DataDecl] -> DataConMap #

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 #

'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 #

'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 #

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

Constructors

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

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

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

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