liquidhaskell-boot-0.9.2.5.0: Liquid Types for Haskell
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Haskell.Liquid.Transforms.CoreToLogic

Synopsis

Documentation

inlineSpecType :: Bool -> Var -> SpecType Source #

NOTE:inlineSpecType type
the refinement depends on whether the result type is a Bool or not: CASE1: measure flogic :: X -> Bool = fhaskell :: x:X -> {v:Bool | v = (flogic x)} CASE2: measure flogic :: X -> Y = fhaskell :: x:X -> {v:Y | v = (flogic x)}

measureSpecType :: Bool -> Var -> SpecType Source #

Refine types of measures: keep going until you find the last data con! this code is a hack! we refine the last data constructor, it got complicated to support both 1. multi parameter measures (see testsposHasElem.hs) 2. measures returning functions (fromReader :: Reader r a -> (r -> a) ) TODO: SIMPLIFY by dropping support for multi parameter measures

weakenResult :: Bool -> Var -> SpecType -> SpecType Source #

'weakenResult foo t' drops the singleton constraint `v = foo x y` that is added, e.g. for measures in /strengthenResult'. This should only be used _when_ checking the body of foo where the output, is, by definition, equal to the singleton.

normalize :: Simplify a => Bool -> a -> a Source #

Orphan instances

Show CoreExpr Source # 
Instance details