Language.Haskell.Liquid.Bare.DataType

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

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

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