Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Bare.Expand

Contents

Create alias expansion environment
Expand and Qualify
Converting BareType to SpecType
Re-exported for data-constructors

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

makeRTEnv :: Env -> ModName -> BareSpec -> ModSpecs -> LogicMap -> BareRTEnv #

makeRTEnv initializes the env needed to expand refinements and types, that is, the below needs to be called *before* we use expand

Expand and Qualify

qualifyExpand :: (Expand a, Qualify a) => Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a #

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 #

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 #

specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType #

Re-exported for data-constructors

plugHoles :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType #