liquidhaskell 0.4.0.1 → 0.4.1.0

raw patch · 52 files changed

+465/−283 lines, 52 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• include/Control/Monad.spec +0/−3
• include/Data/Foldable.spec +5/−0
• include/Data/List.spec +1/−11
• include/GHC/Base.spec +2/−1
• include/Prelude.spec +1/−0
• liquidhaskell.cabal +15/−6
• src/Language/Haskell/Liquid/ACSS.hs +54/−55
• src/Language/Haskell/Liquid/ANFTransform.hs +12/−3
• src/Language/Haskell/Liquid/Annotate.hs +1/−0
• src/Language/Haskell/Liquid/Bare/DataType.hs +1/−0
• src/Language/Haskell/Liquid/Bare/Env.hs +2/−0
• src/Language/Haskell/Liquid/Bare/GhcSpec.hs +1/−0
• src/Language/Haskell/Liquid/Bare/Lookup.hs +12/−5
• src/Language/Haskell/Liquid/Bare/Measure.hs +1/−0
• src/Language/Haskell/Liquid/Bare/Misc.hs +1/−0
• src/Language/Haskell/Liquid/Bare/OfType.hs +4/−3
• src/Language/Haskell/Liquid/Bare/RefToLogic.hs +2/−2
• src/Language/Haskell/Liquid/Bare/Resolve.hs +1/−0
• src/Language/Haskell/Liquid/Bare/Spec.hs +1/−0
• src/Language/Haskell/Liquid/Bounds.hs +12/−11
• src/Language/Haskell/Liquid/CmdLine.hs +2/−1
• src/Language/Haskell/Liquid/Constraint/Constraint.hs +5/−5
• src/Language/Haskell/Liquid/Constraint/Generate.hs +41/−8
• src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +2/−2
• src/Language/Haskell/Liquid/Constraint/Types.hs +1/−0
• src/Language/Haskell/Liquid/Desugar/DsExpr.lhs +5/−2
• src/Language/Haskell/Liquid/Dictionaries.hs +3/−4
• src/Language/Haskell/Liquid/DiffCheck.hs +4/−4
• src/Language/Haskell/Liquid/GhcInterface.hs +15/−16
• src/Language/Haskell/Liquid/GhcMisc.hs +81/−10
• src/Language/Haskell/Liquid/GhcPlay.hs +3/−3
• src/Language/Haskell/Liquid/Literals.hs +11/−12
• src/Language/Haskell/Liquid/Misc.hs +9/−2
• src/Language/Haskell/Liquid/Parse.hs +3/−2
• src/Language/Haskell/Liquid/PredType.hs +1/−1
• src/Language/Haskell/Liquid/PrettyPrint.hs +50/−50
• src/Language/Haskell/Liquid/RefSplit.hs +42/−42
• src/Language/Haskell/Liquid/Simplify.hs +0/−1
• src/Language/Haskell/Liquid/Tidy.hs +1/−0
• src/Language/Haskell/Liquid/TransformRec.hs +4/−3
• src/Language/Haskell/Liquid/Types.hs +10/−5
• src/Language/Haskell/Liquid/Variance.hs +1/−1
• src/Language/Haskell/Liquid/Visitors.hs +1/−0
• tests/neg/StateConstraints0.hs +5/−2
• tests/pos/ListLen-LType.hs +1/−0
• tests/pos/ListLen.hs +1/−0
• tests/pos/ListSort.hs +1/−0
• tests/pos/StateConstraints0.hs +7/−5
• tests/pos/ToyMVar.hs +8/−0
• tests/pos/propmeasure1.hs +11/−0
• tests/pos/wrap1.hs +1/−0
• tests/test.hs +6/−2

@@ -1,3 +0,0 @@-module spec Control.Monad where--sequence :: GHC.Base.Monad m => xs:[m a] -> m {v:[a] | (len v) = (len xs)}

@@ -0,0 +1,5 @@+module spec Data.Foldable where++import GHC.Base++assume length :: Data.Foldable.Foldable f => xs:f a -> {v:Nat | v = len xs}

@@ -1,21 +1,11 @@ module spec Data.List where +import GHC.Base import GHC.List import GHC.Types  assume groupBy :: (a -> a -> GHC.Types.Bool) -> [a] -> [{v:[a] | len(v) > 0}]  assume transpose :: [[a]] -> [{v:[a] | (len v) > 0}]--// assume GHC.List.concat :: x:[[a]] -> {v:[a] | (len v) = (sumLens x)}-//-// measure sumLens :: [[a]] -> GHC.Types.Int-//     sumLens ([])   = 0-//     sumLens (c:cs) = (len c) + (sumLens cs)-//-// invariant {v:[[a]] | (sumLens v) >= 0}-// qualif SumLensEq(v:List List a, x:List List a): (sumLens v) = (sumLens x)-// qualif SumLensEq(v:List List a, x:List a): (sumLens v) = (len x)-// qualif SumLensLe(v:List List a, x:List List a): (sumLens v) <= (sumLens x)  

@@ -9,7 +9,8 @@  measure Prop   :: GHC.Types.Bool -> Prop -measure len :: forall a. [a] -> GHC.Types.Int+class measure len :: forall f a. f a -> GHC.Types.Int+instance measure len :: forall a. [a] -> GHC.Types.Int len []     = 0 len (y:ys) = 1 + len ys 

@@ -7,6 +7,7 @@ import GHC.Real import GHC.Word +import Data.Foldable import Data.Maybe import GHC.Exts 

@@ -1,5 +1,5 @@ Name:                liquidhaskell-Version:             0.4.0.1+Version:             0.4.1.0 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego. build-type:          Simple Synopsis:            Liquid Types for Haskell @@ -44,8 +44,13 @@  --Flag devel --  Description: turn on stricter error reporting for development---  Default:     True+--  Default:     False+--  Manual:      True +Flag include+  Description: use in-tree include directory+  Default:     False+ Executable liquid   default-language: Haskell98   Build-Depends: base >= 4 && < 5@@ -83,7 +88,7 @@                , liquidhaskell    Main-is: Liquid.hs-  ghc-options: -W+  ghc-options: -W -fno-warn-unused-imports -fno-warn-dodgy-imports -fno-warn-deprecated-flags -fno-warn-deprecations --  if flag(devel) --    ghc-options: -Werror   Default-Extensions: PatternGuards@@ -159,7 +164,7 @@                 , bytestring                 , fingertree  -   hs-source-dirs:  include, src+   hs-source-dirs:  src, include      Exposed-Modules: Language.Haskell.Liquid.Prelude,                     Language.Haskell.Liquid.Foreign, @@ -221,6 +226,8 @@                     Language.Haskell.Liquid.Bare.SymSort                     Language.Haskell.Liquid.Bare.Spec +   if impl(ghc < 7.10)+     exposed-modules:                     --NOTE: these need to be exposed so GHC generates .dyn_o files for them..                     Language.Haskell.Liquid.Desugar.Desugar,                     Language.Haskell.Liquid.Desugar.DsExpr,@@ -237,10 +244,12 @@                     Language.Haskell.Liquid.Desugar.DsBinds,                     Language.Haskell.Liquid.Desugar.DsGRHSs,                     Language.Haskell.Liquid.Desugar.HscMain-   ghc-options: -W+   ghc-options: -W -fno-warn-unused-imports -fno-warn-dodgy-imports -fno-warn-deprecated-flags -fno-warn-deprecations --   if flag(devel) --     ghc-options: -Werror---   ghc-prof-options: -fprof-auto+   if flag(include)+     hs-source-dirs: devel+   ghc-prof-options: -fprof-auto    Default-Extensions: PatternGuards  test-suite test

@@ -4,7 +4,7 @@   , hsannot   , AnnMap (..)   , breakS-  , srcModuleName +  , srcModuleName   , Status (..)   ) where @@ -14,30 +14,30 @@ import qualified Language.Haskell.HsColour.CSS as CSS  import Data.Either (partitionEithers)-import Data.Maybe  (fromMaybe) +import Data.Maybe  (fromMaybe) import qualified Data.HashMap.Strict as M import Data.List   (find, isPrefixOf, findIndex, elemIndices, intercalate) import Data.Char   (isSpace) import Text.Printf import Language.Haskell.Liquid.GhcMisc -data AnnMap  = Ann { +data AnnMap  = Ann {     types  :: M.HashMap Loc (String, String) -- ^ Loc -> (Var, Type)   , errors :: [(Loc, Loc, String)]           -- ^ List of error intervals-  , status :: !Status          -  } -  -data Status = Safe | Unsafe | Error | Crash +  , status :: !Status+  }++data Status = Safe | Unsafe | Error | Crash               deriving (Eq, Ord, Show) -data Annotation = A { +data Annotation = A {     typ :: Maybe String         -- ^ type  string-  , err :: Maybe String         -- ^ error string -  , lin :: Maybe (Int, Int)     -- ^ line number, total width of lines i.e. max (length (show lineNum)) +  , err :: Maybe String         -- ^ error string+  , lin :: Maybe (Int, Int)     -- ^ line number, total width of lines i.e. max (length (show lineNum))   } deriving (Show)  --- | Formats Haskell source code using HTML and mouse-over annotations +-- | Formats Haskell source code using HTML and mouse-over annotations hscolour :: Bool     -- ^ Whether to include anchors.          -> Bool     -- ^ Whether input document is literate haskell or not          -> String   -- ^ Haskell source code, Annotations as comments at end@@ -47,9 +47,9 @@  type CommentTransform = Maybe (String -> [(TokenType, String)]) --- | Formats Haskell source code using HTML and mouse-over annotations +-- | Formats Haskell source code using HTML and mouse-over annotations hsannot  :: Bool             -- ^ Whether to include anchors.-         -> CommentTransform -- ^ Function to refine comment tokens +         -> CommentTransform -- ^ Function to refine comment tokens          -> Bool             -- ^ Whether input document is literate haskell or not          -> (String, AnnMap) -- ^ Haskell Source, Annotations          -> String           -- ^ Coloured Haskell source code.@@ -63,7 +63,7 @@ litSpans lits = zip lits $ spans lits   where spans = tokenSpans Nothing . map unL -hsannot' baseLoc anchor tx = +hsannot' baseLoc anchor tx =     CSS.pre     . (if anchor then concatMap (renderAnchors renderAnnotToken)                       . insertAnnotAnchors@@ -72,26 +72,26 @@  -- | annotTokenise is absurdly slow: O(#tokens x #errors) -annotTokenise :: Maybe Loc -> CommentTransform -> (String, AnnMap) -> [(TokenType, String, Annotation)] -annotTokenise baseLoc tx (src, annm) = zipWith (\(x,y) z -> (x,y,z)) toks annots -  where -    toks       = tokeniseWithCommentTransform tx src -    spans      = tokenSpans baseLoc $ map snd toks +annotTokenise :: Maybe Loc -> CommentTransform -> (String, AnnMap) -> [(TokenType, String, Annotation)]+annotTokenise baseLoc tx (src, annm) = zipWith (\(x,y) z -> (x,y,z)) toks annots+  where+    toks       = tokeniseWithCommentTransform tx src+    spans      = tokenSpans baseLoc $ map snd toks     annots     = fmap (spanAnnot linWidth annm) spans     linWidth   = length $ show $ length $ lines src -spanAnnot w (Ann ts es _) span = A t e b -  where +spanAnnot w (Ann ts es _) span = A t e b+  where     t = fmap snd (M.lookup span ts)     e = fmap (\_ -> "ERROR") $ find (span `inRange`) [(x,y) | (x,y,_) <- es]     b = spanLine w span -spanLine w (L (l, c)) -  | c == 1    = Just (l, w) +spanLine w (L (l, c))+  | c == 1    = Just (l, w)   | otherwise = Nothing -inRange (L (l0, c0)) (L (l, c), L (l', c')) -  = l <= l0 && c <= c0 && l0 <= l' && c0 < c' +inRange (L (l0, c0)) (L (l, c), L (l', c'))+  = l <= l0 && c <= c0 && l0 <= l' && c0 < c'  tokeniseWithCommentTransform :: Maybe (String -> [(TokenType, String)]) -> String -> [(TokenType, String)] tokeniseWithCommentTransform Nothing  = tokenise@@ -100,10 +100,10 @@         expand _ z            = [z]  tokenSpans :: Maybe Loc -> [String] -> [Loc]-tokenSpans = scanl plusLoc . fromMaybe (L (1, 1)) +tokenSpans = scanl plusLoc . fromMaybe (L (1, 1))  plusLoc :: Loc -> String -> Loc-plusLoc (L (l, c)) s +plusLoc (L (l, c)) s   = case '\n' `elemIndices` s of       [] -> L (l, (c + n))       is -> L ((l + length is), (n - maximum is))@@ -111,19 +111,19 @@  renderAnnotToken :: (TokenType, String, Annotation) -> String renderAnnotToken (x, y, a)  = renderLinAnnot (lin a)-                            $ renderErrAnnot (err a) -                            $ renderTypAnnot (typ a) +                            $ renderErrAnnot (err a)+                            $ renderTypAnnot (typ a)                             $ CSS.renderToken (x, y)    renderTypAnnot (Just ann) s = printf "<a class=annot href=\"#\"><span class=annottext>%s</span>%s</a>" (escape ann) s-renderTypAnnot Nothing    s = s     +renderTypAnnot Nothing    s = s -renderErrAnnot (Just _) s   = printf "<span class=hs-error>%s</span>" s +renderErrAnnot (Just _) s   = printf "<span class=hs-error>%s</span>" s renderErrAnnot Nothing  s   = s -renderLinAnnot (Just d) s   = printf "<span class=hs-linenum>%s: </span>%s" (lineString d) s +renderLinAnnot (Just d) s   = printf "<span class=hs-linenum>%s: </span>%s" (lineString d) s renderLinAnnot Nothing  s   = s  lineString (i, w) = (replicate (w - (length is)) ' ') ++ is@@ -136,25 +136,25 @@   insertAnnotAnchors :: [(TokenType, String, a)] -> [Either String (TokenType, String, a)]-insertAnnotAnchors toks +insertAnnotAnchors toks   = stitch (zip toks' toks) $ insertAnchors toks'-  where toks' = [(x,y) | (x,y,_) <- toks] +  where toks' = [(x,y) | (x,y,_) <- toks]  stitch ::  Eq b => [(b, c)] -> [Either a b] -> [Either a c] stitch xys ((Left a) : rest)   = (Left a) : stitch xys rest-stitch ((x,y):xys) ((Right x'):rest) -  | x == x' +stitch ((x,y):xys) ((Right x'):rest)+  | x == x'   = (Right y) : stitch xys rest   | otherwise   = error "stitch" stitch _ []   = []-stitch _ _ +stitch _ _   = error "stitch: cannot happen" -splitSrcAndAnns ::  String -> (String, AnnMap) -splitSrcAndAnns s = +splitSrcAndAnns ::  String -> (String, AnnMap)+splitSrcAndAnns s =   let ls = lines s in   case findIndex (breakS ==) ls of     Nothing -> (s, Ann M.empty [] Safe)@@ -165,26 +165,26 @@  srcModuleName :: String -> String srcModuleName = fromMaybe "Main" . tokenModule . tokenise-  -tokenModule toks -  = do i <- findIndex ((Keyword, "module") ==) toks ++tokenModule toks+  = do i <- findIndex ((Keyword, "module") ==) toks        let (_, toks')  = splitAt (i+2) toks        j <- findIndex ((Space ==) . fst) toks'        let (toks'', _) = splitAt j toks'        return $ concatMap snd toks'' -breakS = "MOUSEOVER ANNOTATIONS" +breakS = "MOUSEOVER ANNOTATIONS"  annotParse :: String -> String -> AnnMap annotParse mname s = Ann (M.fromList ts) [(x,y,"") | (x,y) <- es] Safe-  where +  where     (ts, es)       = partitionEithers $ parseLines mname 0 $ lines s  -parseLines _ _ [] +parseLines _ _ []   = [] -parseLines mname i ("":ls)      +parseLines mname i ("":ls)   = parseLines mname (i+1) ls  parseLines mname i (_:_:l:c:"0":l':c':rest')@@ -194,10 +194,10 @@           line' = (read l') :: Int           col'  = (read c') :: Int -parseLines mname i (x:f:l:c:n:rest) +parseLines mname i (x:f:l:c:n:rest)   | f /= mname   = parseLines mname (i + 5 + num) rest'-  | otherwise +  | otherwise   = Left (L (line, col), (x, anns)) : parseLines mname (i + 5 + num) rest'     where line  = (read l) :: Int           col   = (read c) :: Int@@ -205,14 +205,14 @@           anns  = intercalate "\n" $ take num rest           rest' = drop num rest -parseLines _ i _              +parseLines _ i _   = error $ "Error Parsing Annot Input on Line: " ++ show i  instance Show AnnMap where   show (Ann ts es _ ) =  "\n\n" ++ (concatMap ppAnnotTyp $ M.toList ts)                                 ++ (concatMap ppAnnotErr [(x,y) | (x,y,_) <- es])-      -ppAnnotTyp (L (l, c), (x, s))     = printf "%s\n%d\n%d\n%d\n%s\n\n\n" x l c (length $ lines s) s ++ppAnnotTyp (L (l, c), (x, s))     = printf "%s\n%d\n%d\n%d\n%s\n\n\n" x l c (length $ lines s) s ppAnnotErr (L (l, c), L (l', c')) = printf " \n%d\n%d\n0\n%d\n%d\n\n\n\n" l c l' c'  @@ -230,8 +230,8 @@ inlines s = lines' s id   where   lines' []             acc = [acc []]-  lines' ('\^M':'\n':s) acc = acc ['\n'] : lines' s id	-- DOS-  lines' ('\n':s)       acc = acc ['\n'] : lines' s id	-- Unix+  lines' ('\^M':'\n':s) acc = acc ['\n'] : lines' s id  -- DOS+  lines' ('\n':s)       acc = acc ['\n'] : lines' s id  -- Unix   lines' (c:s)          acc = lines' s (acc . (c:))  @@ -246,7 +246,7 @@ classify (x:xs)         = Lit x: classify xs  -allProg name  = go +allProg name  = go   where     end       = "\\end{" ++ name ++ "}"     go []     = []  -- Should give an error message,@@ -262,4 +262,3 @@ joinL (Code c:Code c2:xs) = joinL (Code (c++c2):xs) joinL (Lit c :Lit c2 :xs) = joinL (Lit  (c++c2):xs) joinL (any:xs)            = any: joinL xs-

@@ -22,7 +22,7 @@ import           Outputable                       (trace) import           Var                              (varType, setVarType) import           TypeRep-import           Type                             (mkForAllTys, substTy, mkForAllTys, mkTopTvSubst)+import           Type                             (mkForAllTys, substTy, mkForAllTys, mkTopTvSubst, isTyVar) import           TyCon                            (tyConDataCons_maybe) import           DataCon                          (dataConInstArgTys) import           FamInstEnv                       (emptyFamInstEnv)@@ -70,10 +70,10 @@   = do xes' <- runDsM $ execStateT (normalizeBind γ (Rec xes)) (DsST expandFlag [])        return $ map normalizeTyVars (st_binds xes') -normalizeTyVars (NonRec x e) = NonRec (setVarType x t') e+normalizeTyVars (NonRec x e) = NonRec (setVarType x t') $ normalizeForAllTys e   where t'       = subst msg as as' bt         msg      = "WARNING unable to renameVars on " ++ showPpr x-        as'      = fst $ collectTyBinders e+        as'      = fst $ splitForAllTys $ exprType e         (as, bt) = splitForAllTys (varType x) normalizeTyVars (Rec xes)    = Rec xes'   where nrec = normalizeTyVars <$> ((\(x, e) -> NonRec x e) <$> xes)@@ -85,6 +85,15 @@   | otherwise   = trace msg $ mkForAllTys as bt   where su = mkTopTvSubst $ zip as (mkTyVarTys as')++-- | eta-expand CoreBinds with quantified types+normalizeForAllTys :: CoreExpr -> CoreExpr+normalizeForAllTys e = case e of+  Lam b _ | isTyVar b+    -> e+  _ -> mkLams tvs (mkTyApps e (map mkTyVarTy tvs))+  where+  (tvs, _) = splitForAllTys (exprType e)   newtype DsM a = DsM {runDsM :: DsMonad.DsM a}

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE TupleSections              #-} {-# LANGUAGE NoMonomorphismRestriction  #-} {-# LANGUAGE OverloadedStrings          #-}

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE TupleSections #-}  module Language.Haskell.Liquid.Bare.DataType (

@@ -1,3 +1,5 @@+{-# LANGUAGE FlexibleContexts         #-}+ module Language.Haskell.Liquid.Bare.Env (     BareM   , Warn

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE ViewPatterns              #-}

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE OverloadedStrings #-}@@ -18,7 +19,7 @@ import HscMain import Name import PrelInfo                                 (wiredInThings)-import PrelNames                                (fromIntegerName, smallIntegerName)+import PrelNames                                (fromIntegerName, smallIntegerName, integerTyConName) import RdrName (setRdrNameSpace) import SrcLoc (SrcSpan, GenLocated(L)) import TcRnDriver (tcRnLookupRdrName) @@ -91,6 +92,7 @@   where     wiredIns = [ (symbol n, n) | thing <- wiredInThings, let n = getName thing ]     special  = [ ("GHC.Integer.smallInteger", smallIntegerName)+               , ("GHC.Integer.Type.Integer", integerTyConName)                , ("GHC.Num.fromInteger"     , fromIntegerName ) ]  symbolLookupEnv env mod s@@ -141,10 +143,15 @@   where     sx                 = symbol s --lookupGhcDataCon dc  = case isTupleDC $ val dc of-                         Just n  -> return $ tupleCon BoxedTuple n-                         Nothing -> lookupGhcDataCon' dc +lookupGhcDataCon dc+ | Just n <- isTupleDC (val dc)+ = return $ tupleCon BoxedTuple n+ | val dc == "[]"+ = return nilDataCon+ | val dc == ":"+ = return consDataCon+ | otherwise+ = lookupGhcDataCon' dc  isTupleDC zs   | "(," `isPrefixOfSym` zs

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} 

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} module Language.Haskell.Liquid.Bare.Misc (     makeSymbols 

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE TupleSections #-}  module Language.Haskell.Liquid.Bare.OfType (@@ -13,7 +14,7 @@  import BasicTypes import Name-import TyCon+import TyCon hiding (synTyConRhs_maybe) import Type (expandTypeSynonyms) import TysWiredIn @@ -32,7 +33,7 @@ import Language.Fixpoint.Misc (errorstar) import Language.Fixpoint.Types (Expr(..), Reftable, Symbol, meet, mkSubst, subst, symbol) -import Language.Haskell.Liquid.GhcMisc (realTcArity, sourcePosSrcSpan, tyConTyVarsDef)+import Language.Haskell.Liquid.GhcMisc  import Language.Haskell.Liquid.Misc (secondM) import Language.Haskell.Liquid.RefType import Language.Haskell.Liquid.Types@@ -219,7 +220,7 @@  -------------------------------------------------------------------------------- -bareTCApp r (Loc l _ c) rs ts | Just (SynonymTyCon rhs) <- synTyConRhs_maybe c+bareTCApp r (Loc l _ c) rs ts | Just rhs <- synTyConRhs_maybe c   = do when (realTcArity c < length ts) (Ex.throw err)        return $ tyApp (subsTyVars_meet su $ ofType rhs) (drop nts ts) rs r     where

@@ -51,7 +51,7 @@ instance Transformable Reft where   tx s m (Reft (v, Refa p)) = if v == s                               then errorstar "Transformable: this should not happen"-			      else Reft(v, Refa $ tx s m p)+                              else Reft(v, Refa $ tx s m p)  -- OLD instance Transformable Refa where -- OLD   tx s m (RConc p)     = RConc $ tx s m p@@ -100,7 +100,7 @@   tx s m x = x{eqns = tx s m <$> (eqns x)}  instance Transformable (Def t c) where-	tx s m x = x{body = tx s m (body x)} +        tx s m x = x{body = tx s m (body x)}  instance Transformable Body where   tx s m (E e)   = E $ tx s m e

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeSynonymInstances #-}

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts         #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE TupleSections #-}

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-}  module Language.Haskell.Liquid.Bounds (@@ -11,7 +12,7 @@     makeBound,     envToSub -	) where+        ) where  import Text.PrettyPrint.HughesPJ @@ -47,27 +48,27 @@   instance Hashable (Bound t e) where-	hashWithSalt i = hashWithSalt i . bname+        hashWithSalt i = hashWithSalt i . bname  instance Eq (Bound t e) where   b1 == b2 = (bname b1) == (bname b2)  instance (PPrint e, PPrint t) => (Show (Bound t e)) where-	show = showpp+        show = showpp   instance (PPrint e, PPrint t) => (PPrint (Bound t e)) where-	pprint (Bound s vs ps xs e) =   text "bound" <+> pprint s <+>-	                                text "forall" <+> pprint vs <+> text "." <+>-	                                pprint (fst <$> ps) <+> text "=" <+>-	                                pprint_bsyms (fst <$> xs) <+> pprint e+        pprint (Bound s vs ps xs e) =   text "bound" <+> pprint s <+>+                                        text "forall" <+> pprint vs <+> text "." <+>+                                        pprint (fst <$> ps) <+> text "=" <+>+                                        pprint_bsyms (fst <$> xs) <+> pprint e  pprint_bsyms [] = text "" pprint_bsyms xs = text "\\" <+> pprint xs <+> text "->"  instance Bifunctor Bound where-	first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (mapSnd f <$> ps) (mapSnd f <$> xs) e-	second f (Bound s vs ps xs e) = Bound s vs ps xs (f e)+        first  f (Bound s vs ps xs e) = Bound s (f <$> vs) (mapSnd f <$> ps) (mapSnd f <$> xs) e+        second f (Bound s vs ps xs e) = Bound s vs ps xs (f e)   makeBound :: (PPrint r, UReftable r)@@ -101,9 +102,9 @@     go ((x, t):xtss) = (val x, mkt t x):(go xtss)      mkt t x = ofRSort t `strengthen` ofUReft (U (Reft (val x, mempty))-    	                                        (Pr $ M.lookupDefault [] (val x) ps) mempty)+                                                (Pr $ M.lookupDefault [] (val x) ps) mempty)     tp t x  = ofRSort t `strengthen` ofUReft (U (Reft (val x, refa rs))-    	                                        (Pr $ M.lookupDefault [] (val x) ps) mempty)+                                                (Pr $ M.lookupDefault [] (val x) ps) mempty)     tq t x  = ofRSort t `strengthen` makeRef penv x q      (ps, rs) = partitionPs penv qs

@@ -49,6 +49,7 @@ import Language.Fixpoint.Names             (dropModuleNames) import Language.Fixpoint.Types import Language.Haskell.Liquid.Annotate+import Language.Haskell.Liquid.GhcMisc import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.PrettyPrint import Language.Haskell.Liquid.Types       hiding (config, name, typ)@@ -221,7 +222,7 @@        -- idirs' <- if null (idirs cfg) then single <$> getIncludeDir else return (idirs cfg)        id0 <- getIncludeDir        return  $ cfg { files = files' }-                     { idirs = (dropFileName <$> files') ++ [id0] ++ idirs cfg }+                     { idirs = (dropFileName <$> files') ++ [id0 </> gHC_VERSION, id0] ++ idirs cfg }                               -- tests fail if you flip order of idirs'  ---------------------------------------------------------------------------------------

@@ -13,8 +13,8 @@ import Language.Fixpoint.Types  instance Monoid LConstraint where-	mempty  = LC []-	mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)+        mempty  = LC []+        mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)  typeToConstraint t = LC [t] @@ -36,9 +36,9 @@  subConstraintToLogicOne xts (x', (x, t)) = PImp (pAnd rs) r   where-  	(rs , su) = foldl go ([], []) xts-  	([r], _ ) = go ([], su) (x', (x, t))-  	go (acc, su) (x', (x, t)) = let (Reft(v, Refa p)) = toReft (fromMaybe mempty (stripRTypeBase t))+        (rs , su) = foldl go ([], []) xts+        ([r], _ ) = go ([], su) (x', (x, t))+        go (acc, su) (x', (x, t)) = let (Reft(v, Refa p)) = toReft (fromMaybe mempty (stripRTypeBase t))                                         su'               = (x', EVar x):(v, EVar x) : su                                     in                                      (subst (mkSubst su') p : acc, su')

@@ -4,6 +4,7 @@ {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeSynonymInstances      #-}+{-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE TupleSections             #-} {-# LANGUAGE DeriveDataTypeable        #-}@@ -23,10 +24,14 @@   ) where  import CoreUtils     (exprType)-+import MkCore+import Coercion+import DataCon+import Pair import CoreSyn import SrcLoc import Type+import TyCon import PrelNames import TypeRep import Class            (Class, className)@@ -526,7 +531,7 @@   = bsplitC γ t1 t2  splitC (SubC _ t1 t2)-  = errorstar $ "(Another Broken Test!!!) splitc unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2+  = errorstar $ "(Another Broken Test!!!) splitc unexpected:\n" ++ showpp t1 ++ "\n\n" ++ showpp t2  splitC (SubR γ o r)   = do fg     <- pruneRefs <$> get@@ -728,7 +733,7 @@ γ ?= x = fromMaybe err $ lookupREnv x (renv γ)          where err = errorstar $ "EnvLookup: unknown "                                ++ showpp x-                               ++ " in renv "+                               ++ " in renv\n"                                ++ showpp (renv γ)  normalize idx@@ -1317,6 +1322,17 @@ cconsE γ (Tick tt e) t   = cconsE (γ `setLoc` tickSrcSpan tt) e t +-- GHC 7.10 encodes type classes with a single method as newtypes and+-- `cast`s between the method and class type instead of applying the+-- class constructor. Just rewrite the core to what we're used to+-- seeing..+cconsE γ (Cast e co) t+  | Pair _t1 t2 <- coercionKind co+  , isClassPred t2+  , (tc,ts) <- splitTyConApp t2+  , [dc]   <- tyConDataCons tc+  = cconsE γ (mkCoreConApps dc $ map Type ts ++ [e]) t+ cconsE γ e@(Cast e' _) t   = do t' <- castTy γ (exprType e) e'        addC (SubC γ t' t) ("cconsE Cast" ++ showPpr e)@@ -1462,6 +1478,17 @@        return t     where l = tickSrcSpan tt +-- GHC 7.10 encodes type classes with a single method as newtypes and+-- `cast`s between the method and class type instead of applying the+-- class constructor. Just rewrite the core to what we're used to+-- seeing..+consE γ (Cast e co)+  | Pair _t1 t2 <- coercionKind co+  , isClassPred t2+  , (tc,ts) <- splitTyConApp t2+  , [dc]   <- tyConDataCons tc+  = consE γ (mkCoreConApps dc $ map Type ts ++ [e])+ consE γ e@(Cast e' _)   = castTy γ (exprType e) e' @@ -1469,16 +1496,22 @@    = trueTy $ exprType e  consE _ e@(Type t)-  = errorstar $ "consE cannot handle type" ++ showPpr (e, t)+  = errorstar $ "consE cannot handle type " ++ showPpr (e, t)  castTy _ τ (Var x)   = do t <- trueTy τ        return $  t `strengthen` (uTop $ F.uexprReft $ F.expr x) -castTy γ τ e-  = do t <- trueTy (exprType e)-       cconsE γ e t-       trueTy τ+castTy g t (Tick _ e)+  = castTy g t e++castTy _ _ e+  = errorstar $ "castTy cannot handle expr " ++ showPpr e++-- castTy γ τ e+--   = do t <- trueTy (exprType e)+--        cconsE γ e t+--        trueTy τ  singletonReft = uTop . F.symbolReft . F.symbol 

@@ -1,8 +1,8 @@ module Language.Haskell.Liquid.Constraint.ToFixpoint ( -	cgInfoFInfo+        cgInfoFInfo -	) where+        ) where  import qualified Language.Fixpoint.Types        as F import Language.Haskell.Liquid.Constraint.Types

@@ -255,6 +255,7 @@ insertFEnv (FE benv env) ((x, t), i)   = FE (F.insertsIBindEnv [i] benv) (F.insertSEnv x t env) +insertsFEnv :: FEnv -> [((F.Symbol, F.Sort), F.BindId)] -> FEnv insertsFEnv = L.foldl' insertFEnv  initFEnv init = FE F.emptyIBindEnv $ F.fromListSEnv (wiredSortedSyms ++ init)

@@ -8,8 +8,6 @@ \begin{code} module Language.Haskell.Liquid.Desugar.DsExpr ( dsExpr, dsLExpr, dsLocalBinds, dsValBinds, dsLit ) where -import Language.Haskell.Liquid.GhcMisc (srcSpanTick)- import Language.Haskell.Liquid.Desugar.Match import Language.Haskell.Liquid.Desugar.MatchLit import Language.Haskell.Liquid.Desugar.DsBinds@@ -54,6 +52,11 @@ import FastString  import Control.Monad++srcSpanTick :: Module -> SrcSpan -> Tickish a+srcSpanTick m loc+  = ProfNote (AllCafsCC m loc) False True+ \end{code}  

@@ -17,7 +17,7 @@  import Language.Fixpoint.Names      (dropModuleNames) import Language.Fixpoint.Types-import Language.Fixpoint.Misc +import Language.Fixpoint.Misc  import Language.Haskell.Liquid.GhcMisc () import Language.Haskell.Liquid.Types@@ -34,8 +34,8 @@  makeDictionaryName :: Located Symbol -> SpecType -> Symbol makeDictionaryName t (RApp c _ _ _) = symbol ("$f" ++ (symbolString $ val t) ++ c')-  where -  	c' = symbolString (dropModuleNames $ symbol $ rtc_tc c)+  where+        c' = symbolString (dropModuleNames $ symbol $ rtc_tc c)  makeDictionaryName _ _              = errorstar "makeDictionaryName: called with invalid type" @@ -63,4 +63,3 @@ dhasinfo (Just xts) x = M.lookup x' xts   where      x' = (dropModuleNames $ symbol $ show x)-

@@ -3,8 +3,9 @@ --   modified since it was last checked, as determined by a diff against --   a saved version of the file. -{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings         #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE FlexibleInstances         #-}  module Language.Haskell.Liquid.DiffCheck ( @@ -32,7 +33,7 @@ import            Data.Maybe                    (listToMaybe, mapMaybe, fromMaybe) import            Data.Hashable import qualified  Data.IntervalMap.FingerTree as IM-import            CoreSyn+import            CoreSyn                       hiding (sourceName) import            Name import            SrcLoc hiding (Located) import            Var@@ -456,4 +457,3 @@  lineE :: Located a -> Int lineE = sourceLine . locE-

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeSynonymInstances      #-} {-# LANGUAGE FlexibleInstances         #-}@@ -14,17 +15,17 @@ import InstEnv import Bag (bagToList) import ErrUtils-import GHC hiding (Target)+import GHC hiding (Target, desugarModule) import DriverPhases (Phase(..)) import DriverPipeline (compileFile) import Text.PrettyPrint.HughesPJ import HscTypes hiding (Target) import CoreSyn +import Class import Var import CoreMonad    (liftIO) import DataCon-import Language.Haskell.Liquid.Desugar.HscMain (hscDesugarWithLoc) import qualified Control.Exception as Ex  import GHC.Paths (libdir)@@ -97,11 +98,11 @@                             | tc <- mgi_tcs modguts                             , dc <- tyConDataCons tc                             ]-      let impVs           = importVars  coreBinds+      let impVs           = importVars  coreBinds ++ classCons (mgi_cls_inst modguts)       let defVs           = definedVars coreBinds       let useVs           = readVars    coreBinds       let letVs           = letVars     coreBinds-      let derVs           = derivedVars coreBinds $ mgi_is_dfun modguts+      let derVs           = derivedVars coreBinds $ fmap (fmap is_dfun) $ mgi_cls_inst modguts       logicmap           <- liftIO makeLogicMap       (spec, imps, incs) <- moduleSpec cfg coreBinds (impVs ++ defVs) letVs name' modguts tgtSpec logicmap impSpecs'       liftIO              $ whenLoud $ putStrLn $ "Module Imports: " ++ show imps@@ -114,6 +115,10 @@        lspec <- readFile lg        return $ parseSymbolToLogic lg lspec +classCons :: Maybe [ClsInst] -> [Id]+classCons Nothing   = []+classCons (Just cs) = concatMap (dataConImplicitIds . head . tyConDataCons . classTyCon . is_cls) cs+ derivedVars :: CoreProgram -> Maybe [DFunId] -> [Id] derivedVars cbs (Just fds) = concatMap (derivedVs cbs) fds derivedVars _    Nothing    = []@@ -153,6 +158,9 @@                   --     `gopt_set` Opt_Hpc                       `gopt_set` Opt_ImplicitImportQualified                       `gopt_set` Opt_PIC+#if __GLASGOW_HASKELL__ >= 710+                      `gopt_set` Opt_Debug+#endif        (df'',_,_) <- parseDynamicFlags df' (map noLoc $ ghcOptions cfg)        setSessionDynFlags $ df'' -- {profAuto = ProfAutoAll} @@ -187,12 +195,12 @@      Just modSummary -> do        -- mod_guts <- modSummaryModGuts modSummary        mod_p    <- parseModule modSummary-       mod_guts <- coreModule <$> (desugarModuleWithLoc =<< typecheckModule (ignoreInline mod_p))-       let deriv = getDerivedDictionaries mod_guts+       mod_guts <- coreModule <$> (desugarModule =<< typecheckModule (ignoreInline mod_p))+       let deriv = getDerivedDictionaries mod_guts         return   $! (miModGuts (Just deriv) mod_guts)      Nothing     -> exitWithPanic "Ghc Interface: Unable to get GhcModGuts" -getDerivedDictionaries cm = is_dfun <$> (instEnvElts $ mg_inst_env cm)+getDerivedDictionaries cm = instEnvElts $ mg_inst_env cm  cleanFiles :: FilePath -> IO () cleanFiles fn@@ -209,15 +217,6 @@ -- | Desugaring (Taken from GHC, modified to hold onto Loc in Ticks) ----------- -------------------------------------------------------------------------------- -desugarModuleWithLoc :: TypecheckedModule -> Ghc DesugaredModule-desugarModuleWithLoc tcm = do-  let ms = pm_mod_summary $ tm_parsed_module tcm-  -- let ms = modSummary tcm-  let (tcg, _) = tm_internals_ tcm-  hsc_env <- getSession-  let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }-  guts <- liftIO $ hscDesugarWithLoc hsc_env_tmp ms tcg-  return $ DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts }  -------------------------------------------------------------------------------- -- | Extracting Qualifiers -----------------------------------------------------

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP                       #-} {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE GADTs                     #-}@@ -20,7 +21,7 @@  import           Avail                        (availsToNameSet) import           BasicTypes                   (Arity)-import           CoreSyn                      hiding (Expr)+import           CoreSyn                      hiding (Expr, sourceName) import qualified CoreSyn as Core import           CostCentre import           GHC                          hiding (L)@@ -28,6 +29,10 @@ import           Kind                         (superKind) import           NameSet                      (NameSet) import           SrcLoc                       (mkRealSrcLoc, mkRealSrcSpan, srcSpanFileName_maybe)+import           Bag+import           ErrUtils+import           CoreLint+import           CoreMonad  import           Language.Fixpoint.Names      (dropModuleNames) import           Text.Parsec.Pos              (sourceName, sourceLine, sourceColumn, SourcePos, newPos)@@ -41,6 +46,7 @@ import           HscTypes                     (HscEnv(..), FindResult(..)) import           FastString import           TcRnDriver+import           TcRnTypes  import           RdrName import           Type                         (liftedTypeKind)@@ -69,6 +75,14 @@  import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym) ++#if __GLASGOW_HASKELL__ < 710+import Language.Haskell.Liquid.Desugar.HscMain+#else+import qualified HscMain as GHC+#endif++ ----------------------------------------------------------------------- --------------- Datatype For Holding GHC ModGuts ---------------------- -----------------------------------------------------------------------@@ -82,10 +96,10 @@   , mgi_tcs       :: ![TyCon]   , mgi_fam_insts :: ![FamInst]   , mgi_exports   :: !NameSet-  , mgi_is_dfun   :: !(Maybe [DFunId])+  , mgi_cls_inst  :: !(Maybe [ClsInst])   } -miModGuts dids mg = MI {+miModGuts cls mg  = MI {     mgi_binds     = mg_binds mg   , mgi_module    = mg_module mg   , mgi_deps      = mg_deps mg@@ -94,7 +108,7 @@   , mgi_tcs       = mg_tcs mg   , mgi_fam_insts = mg_fam_insts mg   , mgi_exports   = availsToNameSet $ mg_exports mg-  , mgi_is_dfun   = dids+  , mgi_cls_inst  = cls   }  -----------------------------------------------------------------------@@ -107,7 +121,11 @@  tickSrcSpan ::  Outputable a => Tickish a -> SrcSpan tickSrcSpan (ProfNote cc _ _) = cc_loc cc+#if __GLASGOW_HASKELL__ >= 710+tickSrcSpan (SourceNote ss _) = RealSrcSpan ss+#endif tickSrcSpan _                 = noSrcSpan+ ----------------------------------------------------------------------- --------------- Generic Helpers for Accessing GHC Innards ------------- -----------------------------------------------------------------------@@ -238,10 +256,13 @@ pprDoc    = sDocDoc . ppr  -- Overriding Outputable functions because they now require DynFlags!-showPpr      = Out.showPpr unsafeGlobalDynFlags-showSDoc     = Out.showSDoc unsafeGlobalDynFlags-showSDocDump = Out.showSDocDump unsafeGlobalDynFlags+showPpr       = showSDoc . ppr +-- FIXME: somewhere we depend on this printing out all GHC entities with+-- fully-qualified names...+showSDoc sdoc = Out.renderWithStyle unsafeGlobalDynFlags sdoc (Out.mkUserStyle Out.alwaysQualify Out.AllTheWay)+showSDocDump  = Out.showSDocDump unsafeGlobalDynFlags+ typeUniqueString = {- ("sort_" ++) . -} showSDocDump . ppr  instance Fixpoint Var where@@ -425,10 +446,60 @@   symbol = symbol . fastStringText  fastStringText = T.decodeUtf8 . fastStringToByteString-symbolFastString = T.unsafeDupablePerformIO . mkFastStringByteString . T.encodeUtf8 . symbolText - tyConTyVarsDef c | TC.isPrimTyCon c || isFunTyCon c = [] tyConTyVarsDef c | TC.isPromotedTyCon   c = error ("TyVars on " ++ show c) -- tyConTyVarsDef $ TC.ty_con c tyConTyVarsDef c | TC.isPromotedDataCon c = error ("TyVars on " ++ show c) -- DC.dataConUnivTyVars $ TC.datacon c-tyConTyVarsDef c = TC.tyConTyVars c+tyConTyVarsDef c = TC.tyConTyVars c ++++----------------------------------------------------------------------+-- GHC Compatibility Layer+----------------------------------------------------------------------++gHC_VERSION :: String+gHC_VERSION = show __GLASGOW_HASKELL__++desugarModule :: TypecheckedModule -> Ghc DesugaredModule++symbolFastString :: Symbol -> FastString++lintCoreBindings :: [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)++synTyConRhs_maybe :: TyCon -> Maybe Type++#if __GLASGOW_HASKELL__ < 710++desugarModule tcm = do+  let ms = pm_mod_summary $ tm_parsed_module tcm +  -- let ms = modSummary tcm+  let (tcg, _) = tm_internals_ tcm+  hsc_env <- getSession+  let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }+  guts <- liftIO $ hscDesugarWithLoc hsc_env_tmp ms tcg+  return $ DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts }+++symbolFastString = T.unsafeDupablePerformIO . mkFastStringByteString . T.encodeUtf8 . symbolText++lintCoreBindings = CoreLint.lintCoreBindings++synTyConRhs_maybe t+  | Just (TC.SynonymTyCon rhs) <- TC.synTyConRhs_maybe t+  = Just rhs+synTyConRhs_maybe _                     = Nothing++#else++desugarModule = GHC.desugarModule++symbolFastString = mkFastStringByteString . T.encodeUtf8 . symbolText++type Prec = TyPrec++lintCoreBindings = CoreLint.lintCoreBindings CoreDoNothing++synTyConRhs_maybe = TC.synTyConRhs_maybe++#endif

@@ -5,7 +5,7 @@  module Language.Haskell.Liquid.GhcPlay where -import GHC		+import GHC import CoreSyn import Var import TypeRep@@ -38,7 +38,7 @@   subTy s (App e1 e2)  = App (subTy s e1) (subTy s e2)   subTy s (Lam b e)    | isTyVar b = Lam v' (subTy s e)    where v' = case M.lookup b s of-               Just (TyVarTy v) -> v      +               Just (TyVarTy v) -> v                _                -> b    subTy s (Lam b e)      = Lam (subTy s b) (subTy s e)@@ -58,7 +58,7 @@  subTy s (a, b, e) = (a, map (subTy s) b, subTy s e)  instance Subable Var where- sub s v   | M.member v s = subVar $ s M.! v + sub s v   | M.member v s = subVar $ s M.! v            | otherwise    = v  subTy s v = setVarType v (subTy s (varType v)) 

@@ -1,6 +1,6 @@ module Language.Haskell.Liquid.Literals (-	literalFRefType, literalFReft, literalConst-	) where +        literalFRefType, literalFReft, literalConst+        ) where  import TypeRep import Literal @@ -18,24 +18,23 @@ ----------------------- Typing Literals ----------------------- --------------------------------------------------------------- -makeRTypeBase (TyVarTy α)    x       -  = RVar (rTyVar α) x -makeRTypeBase (TyConApp c ts) x +makeRTypeBase (TyVarTy α)    x+  = RVar (rTyVar α) x+makeRTypeBase (TyConApp c ts) x   = rApp c ((`makeRTypeBase` mempty) <$> ts) [] x makeRTypeBase _              _   = error "RefType : makeRTypeBase" -literalFRefType tce l -  = makeRTypeBase (literalType l) (literalFReft tce l) +literalFRefType tce l+  = makeRTypeBase (literalType l) (literalFReft tce l)  literalFReft tce = maybe mempty exprReft . snd . literalConst tce   -- | `literalConst` returns `Nothing` for unhandled lits because---    otherwise string-literals show up as global int-constants ---    which blow up qualifier instantiation. +--    otherwise string-literals show up as global int-constants+--    which blow up qualifier instantiation.  literalConst tce l         = (sort, mkLit l)-  where -    sort                   = typeSort tce $ literalType l -+  where+    sort                   = typeSort tce $ literalType l

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP                       #-} {-# LANGUAGE TupleSections             #-}  module Language.Haskell.Liquid.Misc where@@ -64,9 +65,15 @@ zip4 (x1:xs1) (x2:xs2) (x3:xs3) (x4:xs4) = (x1, x2, x3, x4) : (zip4 xs1 xs2 xs3 xs4)  zip4 _ _ _ _                             = [] -getIncludeDir      = dropFileName <$> (getDataFileName $ "include" </> "Prelude.spec")+#if __GLASGOW_HASKELL__ < 710+ghc = "ghc-7.8"+#else+ghc = "ghc-7.10"+#endif++getIncludeDir      = dropFileName <$> getDataFileName ("include" </> "Prelude.spec") getCssPath         = getDataFileName $ "syntax" </> "liquid.css"-getCoreToLogicPath = getDataFileName $ "include" </> "CoreToLogic.lg"+getCoreToLogicPath = fmap (</> "CoreToLogic.lg") getIncludeDir   maximumWithDefault zero [] = zero

@@ -1,4 +1,5 @@ {-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE UndecidableInstances      #-} {-# LANGUAGE TypeSynonymInstances      #-}@@ -755,7 +756,7 @@   where     idP p  = many1 (satisfy (not . p))     badc c = (c == ':') || (c == ',') || bad c-    bad c  = isSpace c || c `elem` "(,)"+    bad c  = isSpace c || c `elem` ("(,)" :: String)     pwr s  = symbol $ "(" `mappend` s `mappend` ")"  grabs p = try (liftM2 (:) p (grabs p))@@ -821,7 +822,7 @@  <|> pwr <$> parens (idP bad)   where      idP p  = symbol <$> many1 (satisfy (not . p))-     bad c  = isSpace c || c `elem` "(,)"+     bad c  = isSpace c || c `elem` ("(,)" :: String)      pwr s  = "(" <> s <> ")"  dataSizeP

@@ -1,4 +1,4 @@-{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, UndecidableInstances, TupleSections, OverloadedStrings #-}+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, FlexibleContexts, UndecidableInstances, TupleSections, OverloadedStrings #-} module Language.Haskell.Liquid.PredType (     PrType   , TyConP (..), DataConP (..)

@@ -1,4 +1,4 @@-{-# LANGUAGE FlexibleContexts     #-} +{-# LANGUAGE FlexibleContexts     #-} {-# LANGUAGE FlexibleInstances    #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE OverloadedStrings    #-}@@ -7,16 +7,16 @@ -- | Module with all the printing and serialization routines  module Language.Haskell.Liquid.PrettyPrint (-  +   -- * Tidy level   Tidy (..)- +   -- * Printing RType-  , rtypeDoc +  , rtypeDoc   , ppr_rtype    -- * Printing an Orderable List-  , pprManyOrdered +  , pprManyOrdered    -- * Printing a List with many large items   , pprintLongList@@ -36,7 +36,7 @@ import Language.Fixpoint.Misc import Language.Haskell.Liquid.Types hiding (sort) import Language.Fixpoint.Names (dropModuleNames, propConName, hpropConName)-import TypeRep          hiding (maybeParen, pprArrowChain)  +import TypeRep          hiding (maybeParen, pprArrowChain) import Text.Parsec.Error (ParseError, errorMessages, showErrorMessages) import Var              (Var) import TyCon            (TyCon)@@ -56,7 +56,7 @@   pprint = pprDoc  instance PPrint Doc where-  pprint x = x +  pprint x = x  instance PPrint ErrMsg where   pprint = text . show@@ -64,7 +64,7 @@ instance PPrint SourceError where   pprint = text . show -instance PPrint ParseError where +instance PPrint ParseError where   pprint e = vcat $ tail $ map text ls     where       ls = lines $ showErrorMessages "or" "unknown parse error"@@ -75,10 +75,10 @@ --   pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs)  instance PPrint Var where-  pprint = pprDoc +  pprint = pprDoc  instance PPrint Name where-  pprint = pprDoc +  pprint = pprDoc  instance PPrint TyCon where   pprint = pprDoc@@ -109,30 +109,30 @@ -- to figure out all the constraints.  rtypeDoc k    = ppr_rtype (ppE k) TopPrec-  where +  where     ppE Lossy = ppEnvShort ppEnv     ppE Full  = ppEnv -ppTyConB bb +ppTyConB bb   | ppShort bb = text . symbolString . dropModuleNames . symbol . render . ppTycon   | otherwise  = ppTycon -    -ppr_rtype bb p t@(RAllT _ _)       ++ppr_rtype bb p t@(RAllT _ _)   = ppr_forall bb p t-ppr_rtype bb p t@(RAllP _ _)       +ppr_rtype bb p t@(RAllP _ _)   = ppr_forall bb p t-ppr_rtype bb p t@(RAllS _ _)       +ppr_rtype bb p t@(RAllS _ _)   = ppr_forall bb p t-ppr_rtype _ _ (RVar a r)         +ppr_rtype _ _ (RVar a r)   = ppTy r $ pprint a ppr_rtype bb p t@(RFun _ _ _ _)   = maybeParen p FunPrec $ ppr_rty_fun bb empty t ppr_rtype bb p (RApp c [t] rs r)-  | isList c +  | isList c   = ppTy r $ brackets (ppr_rtype bb p t) <> ppReftPs bb rs ppr_rtype bb p (RApp c ts rs r)-  | isTuple c +  | isTuple c   = ppTy r $ parens (intersperse comma (ppr_rtype bb p <$> ts)) <> ppReftPs bb rs ppr_rtype bb p (RApp c ts rs r)   | isEmpty rsDoc && isEmpty tsDoc@@ -143,7 +143,7 @@     rsDoc            = ppReftPs bb rs     tsDoc            = hsep (ppr_rtype bb p <$> ts)     ppT              = ppTyConB bb-    + ppr_rtype bb p t@(REx _ _ _)   = ppExists bb p t ppr_rtype bb p t@(RAllE _ _ _)@@ -154,7 +154,7 @@   = ppTy r $ ppr_rtype bb p t <+> ppr_rtype bb p t' ppr_rtype bb p (RRTy e _ OCons t)            = sep [braces (ppr_rsubtype bb p e) <+> "=>", ppr_rtype bb p t]-ppr_rtype bb p (RRTy e r o t)         +ppr_rtype bb p (RRTy e r o t)   = sep [ppp (pprint o <+> ppe <+> pprint r), ppr_rtype bb p t]   where ppe = (hsep $ punctuate comma (pprint <$> e)) <+> colon <> colon         ppp = \doc -> text "<<" <+> doc <+> text ">>"@@ -189,7 +189,7 @@ maybeParen :: Prec -> Prec -> Doc -> Doc maybeParen ctxt_prec inner_prec pretty   | ctxt_prec < inner_prec = pretty-  | otherwise		       = parens pretty+  | otherwise                  = parens pretty   -- ppExists :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> RType p c tv r -> Doc@@ -197,23 +197,23 @@   = text "exists" <+> brackets (intersperse comma [ppr_dbind bb TopPrec x t | (x, t) <- zs]) <> dot <> ppr_rtype bb p t'     where (zs,  t')               = split [] t           split zs (REx x t t')   = split ((x,t):zs) t'-          split zs t	            = (reverse zs, t)+          split zs t                = (reverse zs, t)  -- ppAllExpr :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> RType p c tv r -> Doc ppAllExpr bb p t   = text "forall" <+> brackets (intersperse comma [ppr_dbind bb TopPrec x t | (x, t) <- zs]) <> dot <> ppr_rtype bb p t'     where (zs,  t')               = split [] t           split zs (RAllE x t t') = split ((x,t):zs) t'-          split zs t	            = (reverse zs, t)+          split zs t                = (reverse zs, t) -ppReftPs _ rs +ppReftPs _ rs   | all isTauto rs   = empty-  | not (ppPs ppEnv) = empty +  | not (ppPs ppEnv) = empty   | otherwise        = angleBrackets $ hsep $ punctuate comma $ pprint <$> rs  -- ppr_dbind :: (RefTypable p c tv (), RefTypable p c tv r) => Bool -> Prec -> Symbol -> RType p c tv r -> Doc-ppr_dbind bb p x t -  | isNonSymbol x || (x == dummySymbol) +ppr_dbind bb p x t+  | isNonSymbol x || (x == dummySymbol)   = ppr_rtype bb p t   | otherwise   = pprint x <> colon <> ppr_rtype bb p t@@ -234,19 +234,19 @@   where     trep                   = toRTypeRep t     (cls, t')              = bkClass $ fromRTypeRep $ trep {ty_vars = [], ty_preds = [], ty_labels = []}-  +     ppr_foralls False _ _  _= empty     ppr_foralls _    [] [] [] = empty     ppr_foralls True αs πs ss = text "forall" <+> dαs αs <+> dπs (ppPs bb) πs <+> dss (ppSs bb) ss <> dot     ppr_clss []            = empty     ppr_clss cs            = (parens $ hsep $ punctuate comma (uncurry (ppr_cls bb p) <$> cs)) <+> text "=>" -    dαs αs                 = sep $ pprint <$> αs -    -    dπs _ []               = empty -    dπs False _            = empty +    dαs αs                 = sep $ pprint <$> αs++    dπs _ []               = empty+    dπs False _            = empty     dπs True πs            = angleBrackets $ intersperse comma $ ppr_pvar_def pprint <$> πs-    dss _ []               = empty +    dss _ []               = empty     dss _ ss               = angleBrackets $ intersperse comma $ pprint <$> ss  @@ -259,16 +259,16 @@  ppr_pvar_def pprv (PV s t _ xts)   = pprint s <+> dcolon <+> intersperse arrow dargs <+> ppr_pvar_kind pprv t-    -  where ++  where     dargs = [pprv t | (t,_,_) <- xts] -ppr_pvar_kind pprv (PVProp t) = pprv t <+> arrow <+> ppr_name propConName  -ppr_pvar_kind _    (PVHProp)  = ppr_name hpropConName -ppr_name                      = text . symbolString -    +ppr_pvar_kind pprv (PVProp t) = pprv t <+> arrow <+> ppr_name propConName+ppr_pvar_kind _    (PVHProp)  = ppr_name hpropConName+ppr_name                      = text . symbolString+ instance PPrint RTyVar where-  pprint (RTV α) +  pprint (RTV α)    | ppTyVar ppEnv = ppr_tyvar α    | otherwise     = ppr_tyvar_short α @@ -304,18 +304,18 @@   pprint (AnnRDf t) = text "AnnRDf" <+> pprint t   pprint (AnnLoc l) = text "AnnLoc" <+> pprDoc l -pprAnnInfoBinds (l, xvs) +pprAnnInfoBinds (l, xvs)   = vcat $ map (pprAnnInfoBind . (l,)) xvs -pprAnnInfoBind (RealSrcSpan k, xv) +pprAnnInfoBind (RealSrcSpan k, xv)   = xd $$ pprDoc l $$ pprDoc c $$ pprint n $$ vd $$ text "\n\n\n"-    where +    where       l        = srcSpanStartLine k       c        = srcSpanStartCol k-      (xd, vd) = pprXOT xv +      (xd, vd) = pprXOT xv       n        = length $ lines $ render vd -pprAnnInfoBind (_, _) +pprAnnInfoBind (_, _)   = empty  pprXOT (x, v) = (xd, pprint v)@@ -323,14 +323,14 @@     xd = maybe (text "unknown") pprint x  instance PPrint a => PPrint (AnnInfo a) where-  pprint (AI m) = vcat $ map pprAnnInfoBinds $ M.toList m +  pprint (AI m) = vcat $ map pprAnnInfoBinds $ M.toList m  instance (Ord k, PPrint k, PPrint v) => PPrint (M.HashMap k v) where   pprint = ppTable-    + ppTable m = vcat $ pprxt <$> xts-  where -    pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t)  +  where+    pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t)     n          = 1 + maximumWithDefault 0 [ i | (x, _) <- xts, let i = keySize x, i <= thresh ]     keySize     = length . render . pprint     xts         = sortBy (compare `on` fst) $ M.toList m

@@ -3,9 +3,9 @@  module Language.Haskell.Liquid.RefSplit ( -	splitXRelatedRefs+        splitXRelatedRefs -	) where+        ) where  import Control.Applicative import Data.List (partition)@@ -14,110 +14,110 @@ import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.PrettyPrint () -import Language.Fixpoint.Types -import Language.Fixpoint.Misc +import Language.Fixpoint.Types+import Language.Fixpoint.Misc  splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType) splitXRelatedRefs x t = splitRType x t-     + splitRType f (RVar a r) = (RVar a r1, RVar a r2)   where-  	(r1, r2) = splitRef f r+        (r1, r2) = splitRef f r -splitRType f (RFun x tx t r) = (RFun x tx1 t1 r1, RFun x tx2 t2 r2) +splitRType f (RFun x tx t r) = (RFun x tx1 t1 r1, RFun x tx2 t2 r2)   where-  	(tx1, tx2) = splitRType f tx-  	(t1,  t2)  = splitRType f t-  	(r1,  r2)  = splitRef   f r+        (tx1, tx2) = splitRType f tx+        (t1,  t2)  = splitRType f t+        (r1,  r2)  = splitRef   f r  splitRType f (RAllT v t) = (RAllT v t1, RAllT v t2)   where-  	(t1, t2) = splitRType f t +        (t1, t2) = splitRType f t  splitRType f (RAllP p t) = (RAllP p t1, RAllP p t2)   where-  	(t1, t2) = splitRType f t+        (t1, t2) = splitRType f t  splitRType f (RAllS s t) = (RAllS s t1, RAllS s t2)   where-  	(t1, t2) = splitRType f t+        (t1, t2) = splitRType f t   splitRType f (RApp c ts rs r) = (RApp c ts1 rs1 r1, RApp c ts2 rs2 r2)   where-  	(ts1, ts2) = unzip (splitRType f <$> ts)-  	(rs1, rs2) = unzip (splitUReft f <$> rs)-  	(r1,  r2)  = splitRef f r +        (ts1, ts2) = unzip (splitRType f <$> ts)+        (rs1, rs2) = unzip (splitUReft f <$> rs)+        (r1,  r2)  = splitRef f r  splitRType f (RAllE x tx t) = (RAllE x tx1 t1, RAllE x tx2 t2)   where-  	(tx1, tx2) = splitRType f tx-  	(t1, t2)   = splitRType f t+        (tx1, tx2) = splitRType f tx+        (t1, t2)   = splitRType f t  splitRType f (REx x tx t) = (REx x tx1 t1, REx x tx2 t2)   where-  	(tx1, tx2) = splitRType f tx-  	(t1, t2)   = splitRType f t+        (tx1, tx2) = splitRType f tx+        (t1, t2)   = splitRType f t  splitRType _ (RExprArg e) = (RExprArg e, RExprArg e)  splitRType f (RAppTy tx t r) = (RAppTy tx1 t1 r1, RAppTy tx2 t2 r2)   where-  	(tx1, tx2) = splitRType f tx-  	(t1,  t2)  = splitRType f t-  	(r1,  r2)  = splitRef   f r+        (tx1, tx2) = splitRType f tx+        (t1,  t2)  = splitRType f t+        (r1,  r2)  = splitRef   f r  splitRType f (RRTy xs r o t) = (RRTy xs1 r1 o t1, RRTy xs2 r2 o t2)   where-  	(xs1, xs2) = unzip (go <$> xs)-  	(r1, r2) = splitRef   f r -  	(t1, t2) = splitRType f t+        (xs1, xs2) = unzip (go <$> xs)+        (r1, r2) = splitRef   f r+        (t1, t2) = splitRType f t -  	go (x, t) = let (t1, t2) = splitRType f t in ((x,t1), (x, t2))+        go (x, t) = let (t1, t2) = splitRType f t in ((x,t1), (x, t2))   splitRType f (RHole r) = (RHole r1, RHole r2)   where-  	(r1, r2) = splitRef f r +        (r1, r2) = splitRef f r  splitUReft :: Symbol -> RTProp c tv (UReft Reft) -> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft)) splitUReft x (RPropP xs r) = (RPropP xs r1, RPropP xs r2)-  where -  	(r1, r2) = splitRef x r+  where+        (r1, r2) = splitRef x r  splitUReft x (RProp xs t) = (RProp xs t1, RProp xs t2)-  where -  	(t1, t2) = splitRType x t+  where+        (t1, t2) = splitRType x t  splitUReft _ (RHProp xs _) = (RHProp xs w1, RHProp xs w2)-  where -  	(w1, w2) = error "TODO: RefSplit.splitUReft"+  where+        (w1, w2) = error "TODO: RefSplit.splitUReft"  splitRef f (U r p s) = (U r1 p1 s, U r2 p2 s)-	where-		(r1, r2) = splitReft f r -		(p1, p2) = splitPred f p+        where+                (r1, r2) = splitReft f r+                (p1, p2) = splitPred f p  splitReft f (Reft (v, Refa xs)) = (Reft (v, Refa $ pAnd xs1), Reft (v, Refa $ pAnd xs2))   where     (xs1, xs2)       = partition (isFree f) (unPAnd xs) -    unPAnd (PAnd ps) = concatMap unPAnd ps +    unPAnd (PAnd ps) = concatMap unPAnd ps     unPAnd p         = [p]  splitPred f (Pr ps) = (Pr ps1, Pr ps2)   where     (ps1, ps2) = partition g ps-    g p = any (isFree f) (thd3 <$> pargs p) 	+    g p = any (isFree f) (thd3 <$> pargs p)   class IsFree a where-	isFree :: Symbol -> a -> Bool+        isFree :: Symbol -> a -> Bool  instance (Subable x) => (IsFree x) where-	isFree x p = x `elem` syms p+        isFree x p = x `elem` syms p  instance Show (UReft Reft) where-	 show = render . pprint+         show = render . pprint

@@ -40,4 +40,3 @@  simplifyLen :: Int simplifyLen = 5-

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts  #-} {-# LANGUAGE OverloadedStrings #-} --------------------------------------------------------------------- -- | This module contains functions for cleaning up types before

@@ -1,4 +1,5 @@ {-# LANGUAGE DeriveDataTypeable        #-}+{-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE ScopedTypeVariables       #-}@@ -13,15 +14,15 @@ import           Coercion import           Control.Arrow       (second) import           Control.Monad.State-import           CoreLint import           CoreSyn+import           CoreUtils import qualified Data.HashMap.Strict as M import           ErrUtils import           Id                  (idOccInfo, setIdInfo) import           IdInfo import           MkCore              (mkCoreLams) import           SrcLoc-import           Type                (mkForAllTys)+import           Type                (mkForAllTys, splitForAllTys) import           TypeRep import           Unique              hiding (deriveUnique) import           Var@@ -136,7 +137,7 @@ isNonPolyRec (Let (Rec xes) _) = any nonPoly (snd <$> xes) isNonPolyRec _                 = False -nonPoly = null . fst . collectTyBinders+nonPoly = null . fst . splitForAllTys . exprType  collectNonRecLets = go []   where go bs (Let b@(NonRec _ _) e') = go (b:bs) e'

@@ -460,8 +460,12 @@ ------ Strictness -------------------------------------------------- -------------------------------------------------------------------- -instance NFData Var-instance NFData SrcSpan+instance NFData Var where+  rnf x = seq x ()++instance NFData SrcSpan where+  rnf x = seq x ()+ -------------------------------------------------------------------- ------------------ Predicates -------------------------------------- --------------------------------------------------------------------@@ -1566,10 +1570,11 @@  data Cinfo    = Ci { ci_loc :: !SrcSpan                    , ci_err :: !(Maybe Error)-                   }-                deriving (Eq, Ord)+                   } +                deriving (Eq, Ord, Generic)  -instance NFData Cinfo+instance NFData Cinfo where+  rnf x = seq x ()   ------------------------------------------------------------------------

@@ -2,7 +2,7 @@  module Language.Haskell.Liquid.Variance (     Variance(..), VarianceInfo-	) where+        ) where  import Data.Typeable import Data.Data

@@ -1,6 +1,7 @@ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeSynonymInstances      #-}  {-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE TupleSections             #-} {-# LANGUAGE DeriveDataTypeable        #-} {-# LANGUAGE ScopedTypeVariables       #-}

@@ -1,5 +1,6 @@ module Compose where +import Prelude hiding (Monad(..))  -- | TODO  -- | @@ -17,7 +18,10 @@ {-@ runState :: forall <p :: s -> Prop, q :: s -> s -> Prop, r :: s -> a -> Prop>. ST <p, q, r> s a -> x:s<p> -> (a<r x>, s<q x>) @-}  -+class Monad m where+  return :: a -> m a+  (>>=)  :: m a -> (a -> m b) -> m b+  (>>)   :: m a -> m b -> m b  instance Monad (ST s) where   {-@ instance Monad ST s where@@ -55,7 +59,6 @@   return x     = ST $ \s -> (x, s)   (ST g) >>= f = ST (\x -> case g x of {(y, s) -> (runState (f y)) s})       (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})    -  fail         = error    

@@ -39,6 +39,7 @@ -- check [] = [liquidAssertB True] -- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss +chk :: List [a] -> Bool chk Nil = liquidAssertB True chk (Cons xs xss) =   case xss of 

@@ -17,6 +17,7 @@ -- check [] = [liquidAssertB True] -- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss +chk :: [[a]] -> Bool chk [] = liquidAssertB True chk (xs:xss) =   case xss of 

@@ -13,6 +13,7 @@ insertSort (x:xs)     = insert x (insertSort xs)   {-@ insertSort' :: (Ord a) => xs:[a] -> OList a @-}+insertSort'           :: (Ord a) => [a] -> [a] insertSort' xs        = foldr insert [] xs  insert y []                   = [y]

@@ -1,5 +1,6 @@ module Compose where +import Prelude hiding (Monad(..))  -- | TODO  -- | @@ -17,6 +18,10 @@ {-@ runState :: forall <p :: s -> Prop, q :: s -> s -> Prop, r :: s -> a -> Prop>. ST <p, q, r> s a -> x:s<p> -> (a<r x>, s<q x>) @-}  +class Monad m where+  return :: a -> m a+  (>>=)  :: m a -> (a -> m b) -> m b+  (>>)   :: m a -> m b -> m b   instance Monad (ST s) where@@ -54,7 +59,6 @@   return x     = ST $ \s -> (x, s)   (ST g) >>= f = ST (\x -> case g x of {(y, s) -> (runState (f y)) s})       (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})    -  fail         = error  {-@ incr :: ST <{\x -> true}, {\x v -> v = x + 1}, {\x v -> v = x}>  Int Int @-} incr :: ST Int Int@@ -62,7 +66,7 @@  {-@ foo :: ST <{\x -> true}, {\x v -> true}, {\x v -> v = 0}>  Bool Int @-} foo :: ST Bool Int-foo = do return 0+foo = return 0  {-@ incr2 :: ST <{\x -> true}, {\x v -> v = x + 2}, {\x v -> v = x + 1}>  Int Int @-} incr2 :: ST Int Int@@ -71,9 +75,7 @@ {-@ incr3 :: ST <{\x -> true}, {\x v -> v = x + 3}, {\x v -> v = x + 2}>  Int Int @-} incr3 :: ST Int Int incr3 -  = do incr-       incr-       incr+  = incr >> incr >> incr  run :: (Int, Int) {-@ run :: ({v:Int |  v = 1}, {v:Int |  v = 2}) @-}

@@ -5,6 +5,7 @@ module ToyMVar where  import Prelude hiding (IO)+import Control.Applicative import Data.Set  data RealWorld data MVar# s a @@ -53,3 +54,10 @@ instance Monad IO where --  GHC-Base.lhs   return = undefined   _ >> _ = undefined++instance Applicative IO where+  pure  = undefined+  (<*>) = undefined++instance Functor IO where+  fmap = undefined

@@ -0,0 +1,11 @@+module PropMeasure where++nil  = []++++++++

@@ -24,6 +24,7 @@ nflibXs n x           = prop2 n (WrapType nxs x)                         where nxs = replicate n x  +prop2 :: Int -> WrapType [a] t -> Bool prop2 n (WrapType xs _) = liquidAssertB (n == length xs)   

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP  #-} {-# LANGUAGE DeriveDataTypeable  #-} {-# LANGUAGE DoAndIfThenElse     #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -19,16 +20,19 @@ import System.Process import Test.Tasty import Test.Tasty.HUnit-import Test.Tasty.Ingredients.Rerun import Test.Tasty.Options import Test.Tasty.Runners import Text.Printf +import Test.Tasty.Ingredients.Rerun++testRunner = rerunningTests [ listingTests, consoleTestReporter ]+ main :: IO () main = run =<< tests   where     run   = defaultMainWithIngredients [-                rerunningTests   [ listingTests, consoleTestReporter ]+                testRunner               , includingOptions [ Option (Proxy :: Proxy NumThreads)                                  , Option (Proxy :: Proxy LiquidOpts)                                  , Option (Proxy :: Proxy SmtSolver) ]