| Safe Haskell | Safe-Inferred |
|---|---|
| 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 :: (PPrint a, 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 -> Lookup LocSpecType
- specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
- plugHoles :: Bool -> SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
Create alias expansion environment
Expand and Qualify
qualifyExpand :: (PPrint a, 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.
When expanding, it's important we pass around a BareRTEnv where the type aliases have been qualified as well.
This is subtle, see for example T1761. In that test, we had a type alias "OneTyAlias a = {v:a | oneFunPred v}" where
"oneFunPred" was marked inline. However, inlining couldn't happen because the BareRTEnv had an
entry for "T1761.oneFunPred", so the relevant expansion of "oneFunPred" couldn't happen. This was
because the type alias entry inside BareRTEnv mentioned the tuple ("OneTyAlias", "{v:a | oneFunPred v}") but
the snd element needed to be qualified as well, before trying to expand anything.
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 -> Lookup LocSpecType Source #
specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType Source #
Re-exported for data-constructors
plugHoles :: Bool -> SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType Source #