liquidhaskell-boot
Safe HaskellNone
LanguageHaskell98

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 refinement 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, where Symbols are replaced with LHName.

BareSpecLHName has an approximate 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. The bijection is approximate because in the roundtrip the representation of LHName's might change.

At the same time, the BareSpecLHName form is kept to serialize and to resolve names of modules that import the specs.

Synopsis

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 a type to a value.

At parse time the arguments of type aliases are all treated as types. This needs fixing before verification because some arguments are meant to be values. Hence, this function to correct the arguments in question. See the documentation of fixExpressionArgsOfTypeAliases for some more context.

fromBareSpecLHName :: BareSpecLHName -> BareSpec Source #

toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName Source #

symbolToLHName :: String -> LogicNameEnv -> HashSet Symbol -> [Symbol] -> Symbol -> Identity LHName Source #

Uses the logic name environment to convert a resolved Symbol to LHName. Symbols not present in the environment correspond to local symbols (e.g. bounded variables) or are explicitly left unhandled.

data LogicNameEnv Source #

For every symbol tells the corresponding LHName and Sort

Symbols are expected to have been created by lhNameToResolvedSymbol.

Constructors

LogicNameEnv 

Fields