| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Bare.Expand
Description
This module has the code for applying refinement (and) type aliases
and the pipeline for "cooking" a BareType into a SpecType.
TODO: _only_ export makeRTEnv, cookSpecType and maybe qualifyExpand...
Synopsis
- makeRTEnv :: Env -> ModName -> BareSpec -> ModSpecs -> LogicMap -> BareRTEnv
- qualifyExpand :: (Expand a, Qualify a) => Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
- cookSpecType :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType
- cookSpecTypeE :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> Either UserError LocSpecType
- specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
- plugHoles :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
Create alias expansion environment
Expand and Qualify
qualifyExpand :: (Expand a, Qualify a) => Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a Source #
qualifyExpand first qualifies names so that we can successfully resolve
them during expansion.
Converting BareType to SpecType
cookSpecType :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType Source #
cookSpecType is the central place where a BareType gets processed,
in multiple steps, into a SpecType. See [NOTE:Cooking-SpecType] for
details of each of the individual steps.
cookSpecTypeE :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> Either UserError LocSpecType Source #
specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType Source #
Re-exported for data-constructors
plugHoles :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType Source #