Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Transforms.QuestionMark

Description

Eliminate applications of the ? operator from Core after ANF.

After ANF, e ? s becomes:

let a1 = e
let a2 = s
... (?) @A @B a1 a2

This pass replaces (?) @A @B a1 a2 with just a1, so that no KVars are introduced in the signature of ?. The binding a2 = s remains in scope, so the lemma's postcondition still enters the environment during constraint generation.

Synopsis

eliminateQuestionMark :: GlobalRdrEnv -> [CoreBind] -> [CoreBind]

Documentation

eliminateQuestionMark :: GlobalRdrEnv -> [CoreBind] -> [CoreBind] Source #

Look up the ? operator in the GlobalRdrEnv. If found, eliminate all its applications from the Core program. If not found (module doesn't import ProofCombinators), return the bindings unchanged.