exp package:liquidhaskell-boot

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.

Exported logic symbols originated by reflecting functions

expect failure from Liquid with any message

expect failure from Liquid with at least one of the following messages

Expand out all type synonyms. Actually, it'd suffice to expand out just the ones that discard type variables (e.g. type Funny a = Int) But we don't know which those are currently, so we just expand all. expandTypeSynonyms only expands out type synonyms mentioned in the type, not in the kinds of any TyCon or TyVar mentioned in the type. Keep this synchronized with synonymTyConsOfType

Find all locally-defined free Ids or type variables in an expression returning a non-deterministic set.

Find all locally-defined free Ids or type variables in an expression returning a deterministically ordered list.

Finds free variables in an expression selected by a predicate returning a deterministically ordered list.

Recover the type of a well-typed Core expression. Fails when applied to the actual Type expression as it cannot really be said to have a type

Finds the free external names of several expressions: see exprOrphNames for details

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...

Using the BareRTEnv to do alias-expansion

This is the data type that represents GHCs core intermediate language. Currently GHC uses System FC https://www.microsoft.com/en-us/research/publication/system-f-with-type-equality-coercions/ for this purpose, which is closely related to the simpler and better known System F http://en.wikipedia.org/wiki/System_F. We get from Haskell source to this Core language in a number of stages:

1. The source code is parsed into an abstract syntax tree, which is represented by the data type HsExpr with the names being RdrNames
2. This syntax tree is renamed, which attaches a Unique to every RdrName (yielding a Name) to disambiguate identifiers which are lexically identical. For example, this program:

f x = let f x = x + 1
in f (x - 2)

Would be renamed by having Uniques attached so it looked something like this:

f_1 x_2 = let f_3 x_4 = x_4 + 1
in f_3 (x_2 - 2)

But see Note [Shadowing in Core] below.

1. The resulting syntax tree undergoes type checking (which also deals with instantiating type class arguments) to yield a HsExpr type that has Id as it's names.
2. Finally the syntax tree is desugared from the expressive HsExpr type into this Expr type, which has far fewer constructors and hence is easier to perform optimization, analysis and code generation on.

The type parameter b is for the type of binders in the expression tree. The language consists of the following elements:

• Variables See Note [Variable occurrences in Core]
• Primitive literals
• Applications: note that the argument may be a Type. See Note [Representation polymorphism invariants]
• Lambda abstraction See Note [Representation polymorphism invariants]
• Recursive and non recursive lets. Operationally this corresponds to allocating a thunk for the things bound and then executing the sub-expression.

See Note [Core letrec invariant] See Note [Core let-can-float invariant] See Note [Representation polymorphism invariants] See Note [Core type and coercion invariant]

• Case expression. Operationally this corresponds to evaluating the scrutinee (expression examined) to weak head normal form and then examining at most one level of resulting constructor (i.e. you cannot do nested pattern matching directly with this).

The binder gets bound to the value of the scrutinee, and the Type must be that of all the case alternatives IMPORTANT: see Note [Case expression invariants]

• Cast an expression to a particular type. This is used to implement newtypes (a newtype constructor or destructor just becomes a Cast in Core) and GADTs.
• Ticks. These are used to represent all the source annotation we support: profiling SCCs, HPC ticks, and GHCi breakpoints.
• A type: this should only show up at the top level of an Arg
• A coercion

Expression with an explicit type signature. e :: type

• AnnKeywordId : AnnDcolon

Embed fixpoint expressions into parsed haskell expressions. It allows us to bypass the GHC parser and use arbitrary symbols for identifiers (compared to using the string API)