Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Bare.Expand

Contents

Create alias expansion environment
Expand
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 -> [(ModName, BareSpec)] -> LogicMap -> BareRTEnv
class Expand a where
- expand :: BareRTEnv -> SourcePos -> 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

makeRTEnv :: Env -> ModName -> BareSpec -> [(ModName, BareSpec)] -> LogicMap -> BareRTEnv Source #

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

Expand

class Expand a where Source #

Using the BareRTEnv to do alias-expansion

Methods

expand :: BareRTEnv -> SourcePos -> a -> a Source #

Instances

Instances details

Expand Expr Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> Expr -> Expr Source #
Expand Reft Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> Reft -> Reft Source #
Expand DataCtor Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor Source #
Expand DataDecl Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl Source #
Expand BareType Source #	`expand` on a BareType actually applies the type- and expression- aliases.
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareType -> BareType Source #
Expand RReft Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> RReft -> RReft Source #
Expand SpecType Source #	`expand` on a SpecType simply expands the refinements, i.e. does not apply the type aliases, but just the 1. predicate aliases, 2. inlines, 3. stuff from `LogicMap`
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> SpecType -> SpecType Source #
Expand BareDef Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #
Expand BareMeasure Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #
Expand BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec Source #
Expand BareRTAlias Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BareRTAlias -> BareRTAlias Source #
Expand Body Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> Body -> Body Source #
Expand () Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> () -> () Source #
Expand a => Expand (Located a) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> Located a -> Located a Source #
Expand (BRType ()) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> BRType () -> BRType () Source #
Expand a => Expand (Maybe a) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> Maybe a -> Maybe a Source #
Expand a => Expand [a] Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> [a] -> [a] Source #
Expand (RTAlias Symbol Expr) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> RTAlias Symbol Expr -> RTAlias Symbol Expr Source #
Expand a => Expand (HashMap k a) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> HashMap k a -> HashMap k a Source #
Expand a => Expand (LocSymbol, a) Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Expand Methods expand :: BareRTEnv -> SourcePos -> (LocSymbol, a) -> (LocSymbol, a) Source #

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 #