| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.LHNameResolution
Description
This module provides functions to resolve names in specs.
There are two major namespaces in LH:
1) The names of Haskell entities 2) The names of logic entities
At the moment LH resolves names to Haskell entities, while resolving logic entities remains work in progress.
Haskell entities include all functions that LH might reflect, or types that might be referred in refinment types, type aliases or other annotations.
Logic entities include the names of reflected functions, inlined functions, uninterpreted functions, predefined functions, local bindings, reflected data constructors and parameters of Haskell functions in specs of other local bindings.
The resolution pipeline goes as follows.
- First the module specs are parsed into a
BareSpecParsed. Here all names are unresolved. - Next the names of Haskell entities are resolved by
resolveLHNames. For now, this pass doesn't change the type of the names. - Next the names of logic entities are resolved. This pass produces
a
BareSpecLHName, whereSymbols are replaced withLHName. At the moment most LHNames are just wrappers over the symbols. As name resolution is implemented for logic names, the wrappers will be replaced with the actual result of name resolution.
BareSpecLHName has a bijection to BareSpec via a LogicNameEnv
which allows to convert LHName to an unambiguous form of Symbol
and back. The bijection is implemented with the functions toBareSpecLHName
and fromBareSpecLHName. This allows to use liquid-fixpoint functions
unmodified as they will continue to operate on (now unambiguous) Symbols.
At the same time, the BareSpecLHName form is kept to serialize and to
resolve names of modules that import the specs.
Synopsis
- resolveLHNames :: Config -> Module -> LocalVars -> ImportedMods -> GlobalRdrEnv -> BareSpecParsed -> TargetDependencies -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
- resolveSymbolToTcName :: GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
- exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol
- fromBareSpecLHName :: BareSpecLHName -> BareSpec
- toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName
- data LogicNameEnv = LogicNameEnv {}
Documentation
resolveLHNames :: Config -> Module -> LocalVars -> ImportedMods -> GlobalRdrEnv -> BareSpecParsed -> TargetDependencies -> Either [Error] (BareSpec, LogicNameEnv, LogicMap) Source #
Converts occurrences of LHNUnresolved to LHNResolved using the provided type aliases and GlobalRdrEnv.
resolveSymbolToTcName :: GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName) Source #
Produces an LHName from a symbol by looking it in the rdr environment.
exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol Source #
exprArg converts a tyVar to an exprVar because parser cannot tell
this function allows us to treating (parsed) "types" as "value"
arguments, e.g. type Matrix a Row Col = List (List a Row) Col
Note that during parsing, we don't necessarily know whether a
string is a type or a value expression. E.g. in testsposT1189.hs,
the string `Prop (Ev (plus n n))` where Prop is the alias:
{- type Prop E = {v:_ | prop v = E} -}
the parser will chomp in `Ev (plus n n)` as a BareType and so
exprArg converts that BareType into an Expr.
toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName Source #
data LogicNameEnv Source #
For every symbol tells the corresponding LHName and Sort
Symbols are expected to have been created by lhNameToResolvedSymbol.
Constructors
| LogicNameEnv | |