liquidhaskell 0.3.0.0 → 0.3.1.0

raw patch · 36 files changed

+525/−1076 lines, 36 filesdep ~liquid-fixpointPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: liquid-fixpoint

API changes (from Hackage documentation)

Files

• Liquid.hs +2/−1
• include/GHC/Base.spec +4/−4
• include/GHC/CString.spec +7/−0
• include/GHC/Num.spec +3/−3
• include/GHC/Types.spec +3/−3
• include/Prelude.hquals +4/−0
• liquidhaskell.cabal +12/−4
• src/Language/Haskell/Liquid/Bare/Check.hs +60/−4
• src/Language/Haskell/Liquid/Bare/Existential.hs +8/−1
• src/Language/Haskell/Liquid/Bare/Expand.hs +2/−0
• src/Language/Haskell/Liquid/Bare/GhcSpec.hs +13/−5
• src/Language/Haskell/Liquid/Bare/Measure.hs +5/−3
• src/Language/Haskell/Liquid/Bare/Plugged.hs +6/−5
• src/Language/Haskell/Liquid/Bare/RTEnv.hs +2/−0
• src/Language/Haskell/Liquid/Bare/RefToLogic.hs +2/−1
• src/Language/Haskell/Liquid/Bare/Resolve.hs +1/−0
• src/Language/Haskell/Liquid/CTags.hs +1/−1
• src/Language/Haskell/Liquid/CmdLine.hs +47/−21
• src/Language/Haskell/Liquid/Constraint/Constraint.hs +1/−2
• src/Language/Haskell/Liquid/Constraint/Generate.hs +49/−22
• src/Language/Haskell/Liquid/CoreToLogic.hs +23/−8
• src/Language/Haskell/Liquid/DiffCheck.hs +2/−1
• src/Language/Haskell/Liquid/Errors.hs +10/−4
• src/Language/Haskell/Liquid/Fresh.hs +16/−4
• src/Language/Haskell/Liquid/GhcInterface.hs +8/−124
• src/Language/Haskell/Liquid/Parse.hs +26/−9
• src/Language/Haskell/Liquid/PredType.hs +3/−2
• src/Language/Haskell/Liquid/Qualifier.hs +1/−2
• src/Language/Haskell/Liquid/Simplify.hs +32/−0
• src/Language/Haskell/Liquid/Types.hs +26/−56
• src/Language/Haskell/Liquid/Visitors.hs +142/−0
• syntax/flycheck-liquid.el +0/−86
• syntax/haskell.vim +0/−379
• syntax/liquid-tip.el +0/−270
• syntax/liquid.vim +0/−47
• tests/test.hs +4/−4

@@ -1,5 +1,6 @@ {-# LANGUAGE TupleSections  #-} +import           Data.Maybe import           Data.Monoid      (mconcat, mempty) import           System.Exit  import           Control.Applicative ((<$>))@@ -87,7 +88,7 @@        let out0  = mkOutput cfg res sol annm        return    $ out0 { o_vars = names } { o_errors  = warns} { o_result = res }     where -       fx        = def { FC.solver = smtsolver cfg, FC.real = real cfg }+       fx        = def { FC.solver = fromJust (smtsolver cfg), FC.real = real cfg }        ferr s r  = fmap (tidyError s) $ result $ sinfo <$> r  

@@ -10,11 +10,11 @@ measure Prop   :: GHC.Types.Bool -> Prop  measure len :: forall a. [a] -> GHC.Types.Int-len ([])     = 0-len (y:ys)   = 1 + (len ys)+len []     = 0+len (y:ys) = 1 + len ys  measure null :: forall a. [a] -> Prop-null ([])   = true+null []     = true null (x:xs) = false  measure fst :: (a,b) -> a@@ -31,7 +31,7 @@ map       :: (a -> b) -> xs:[a] -> {v: [b] | len(v) = len(xs)} (++)      :: xs:[a] -> ys:[a] -> {v:[a] | (len v) = (len xs) + (len ys)} -$         :: (a -> b) -> a -> b+($)       :: (a -> b) -> a -> b id        :: x:a -> {v:a | v = x}  

@@ -0,0 +1,7 @@+module spec GHC.CString where++import GHC.Prim ++-- The equality is untyped, but there is an implicit logic cast+GHC.CString.unpackCString# :: x:GHC.Prim.Addr# -> {v:String | v = x}+

@@ -4,6 +4,6 @@                     => x:GHC.Integer.Type.Integer                     -> {v:a | v = x } --- GHC.Num.negate :: (GHC.Num.Num a)---                => x:a---                -> {v:a | v = (0-x)}+GHC.Num.negate :: (GHC.Num.Num a)+               => x:a+               -> {v:a | v = -x}

@@ -6,9 +6,9 @@ GHC.Types.GT :: {v:GHC.Types.Ordering | v = (cmp v) }  measure cmp :: GHC.Types.Ordering -> GHC.Types.Ordering-cmp (GHC.Types.EQ) = { v | v = GHC.Types.EQ }-cmp (GHC.Types.LT) = { v | v = GHC.Types.LT }-cmp (GHC.Types.GT) = { v | v = GHC.Types.GT }+cmp GHC.Types.EQ = { v | v = GHC.Types.EQ }+cmp GHC.Types.LT = { v | v = GHC.Types.LT }+cmp GHC.Types.GT = { v | v = GHC.Types.GT }   GHC.Types.True  :: {v:GHC.Types.Bool | (Prop(v))}

@@ -24,4 +24,8 @@ qualif Papp3(v:a,~X:b, ~Y:c, ~P:Pred a b c) : papp3(~P, v, ~X, ~Y) constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool]) +// qualif Papp4(v:a,~X:b, ~Y:c, ~Z:d, ~P:Pred a b c d) : papp4(~P, v, ~X, ~Y, ~Z)+constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])++ constant Prop : func(0, [GHC.Types.Bool; bool])

@@ -1,5 +1,5 @@ Name:                liquidhaskell-Version:             0.3.0.0+Version:             0.3.1.0 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego. build-type:          Simple Synopsis:            Liquid Types for Haskell @@ -33,13 +33,15 @@           , include/Language/Haskell/Liquid/*.pred           , include/System/*.spec           , syntax/liquid.css-          , syntax/*.el-          , syntax/*.vim  Source-Repository head   Type:        git   Location:    https://github.com/ucsd-progsys/liquidhaskell/ +--Flag devel+--  Description: turn on stricter error reporting for development+--  Default:     False+ Executable liquid   default-language: Haskell98   Build-Depends: base >= 4 && < 5@@ -78,6 +80,8 @@    Main-is: Liquid.hs   ghc-options: -W+  -- if flag(devel)+  --   ghc-options: -Werror   Default-Extensions: PatternGuards  -- Executable liquid-count-binders@@ -146,7 +150,7 @@                 , vector                 , hashable                 , unordered-containers-                , liquid-fixpoint >= 0.2.2.0+                , liquid-fixpoint >= 0.2.3.0                 , aeson                 , bytestring                 , fingertree@@ -185,9 +189,11 @@                     Language.Haskell.Liquid.TransformRec,                      Language.Haskell.Liquid.Tidy,                      Language.Haskell.Liquid.Types,+                    Language.Haskell.Liquid.Simplify,                     Language.Haskell.Liquid.Literals,                     Language.Haskell.Liquid.Strata,                     Language.Haskell.Liquid.Fresh,+                    Language.Haskell.Liquid.Visitors,                     Language.Haskell.Liquid.WiredIn,                     Paths_liquidhaskell, @@ -226,6 +232,8 @@                     Language.Haskell.Liquid.Desugar.DsGRHSs,                     Language.Haskell.Liquid.Desugar.HscMain    ghc-options: -W+   -- if flag(devel)+   --   ghc-options: -Werror    ghc-prof-options: -fprof-auto    Default-Extensions: PatternGuards 

@@ -28,7 +28,7 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S -import Language.Fixpoint.Misc (applyNonNull, group, mapSnd, snd3)+import Language.Fixpoint.Misc (applyNonNull, group, mapSnd, snd3, errorstar, safeHead) import Language.Fixpoint.Names (isPrefixOfSym, stripParensSym) import Language.Fixpoint.Sort (checkSorted, checkSortedReftFull, checkSortFull) import Language.Fixpoint.Types hiding (R)@@ -203,10 +203,10 @@ ------------------------------------------------------------------------------------------------ -- | @checkRType@ determines if a type is malformed in a given environment --------------------- -------------------------------------------------------------------------------------------------checkRType :: (PPrint r, Reftable r) => TCEmb TyCon -> SEnv SortedReft -> RRType r -> Maybe Doc +checkRType :: (PPrint r, Reftable r) => TCEmb TyCon -> SEnv SortedReft -> RRType (UReft r) -> Maybe Doc  ------------------------------------------------------------------------------------------------ -checkRType emb env t         = efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t +checkRType emb env t         = checkAbstractRefs t <|> efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t    where      cb c ts                  = classBinds (rRCls c ts)     f env me r err           = err <|> checkReft env emb me r@@ -214,8 +214,64 @@     pbinds p                 = (pname p, pvarRType p :: RSort)                                : [(x, t) | (t, x, _) <- pargs p] +checkAbstractRefs t = go t+  where+    penv = mkPEnv t -checkReft                    :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType r) -> r -> Maybe Doc +    go (RAllT _ t)        = go t+    go (RAllP _ t)        = go t+    go (RAllS _ t)        = go t+    go t@(RApp c ts rs r) = check (toRSort t :: RSort) r <|>  efold go ts <|> go' c rs+    go t@(RFun _ t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2+    go t@(RVar _ r)       = check (toRSort t :: RSort) r+    go (RAllE _ t1 t2)    = go t1 <|> go t2+    go (REx _ t1 t2)      = go t1 <|> go t2+    go t@(RAppTy t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2+    go (RRTy xts _ _ t)   = efold go (snd <$> xts) <|> go t+    go (RExprArg _)       = Nothing+    go (RHole _)          = Nothing++    go' c rs = foldl (\acc (x, y) -> acc <|> checkOne' x y) Nothing (zip rs (rTyConPVs c))++    checkOne' (RProp xs t) p +      | pvType p /= toRSort t +      = Just $ text "Unexpected Sort in" <+> pprint p+      | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)]  +      = Just $ text "Wrong Arguments in" <+> pprint p+      | length xs /= length (pargs p) +      = Just $ text "Wrong Number of Arguments in" <+> pprint p+      | otherwise  +      = go t+    checkOne' (RPropP xs _) p +      | or [s1 /= s2 | ((_, s1), (s2, _, _)) <- zip xs (pargs p)]  +      = Just $ text "Wrong Arguments in" <+> pprint p+      | length xs /= length (pargs p) +      = Just $ text "Wrong Number of Arguments in" <+> pprint p+      | otherwise  +      = Nothing +    checkOne' _ _ = errorstar "This cannot happen"  ++    efold f = foldl (\acc x -> acc <|> f x) Nothing ++    check s (U _ (Pr ps) _) = foldl (\acc pp -> acc <|> checkOne s pp) Nothing ps++    checkOne s p | pvType' p /= s                          +                 = Just $ text "Incorrect Sort"        <+> pprint p+                 | or [x == y | (_, x, EVar y) <- pargs p] +                 = Just $ text "Missing arguments on " <+> pprint p+                 | otherwise                               +                 = Nothing ++    mkPEnv (RAllT _ t) = mkPEnv t+    mkPEnv (RAllP p t) = p:mkPEnv t +    mkPEnv _           = []++    pvType' p = safeHead (showpp p ++ " not in env of " ++ showpp t) [pvType q | q <- penv, pname p == pname q]+++++checkReft                    :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType (UReft r)) -> (UReft r) -> Maybe Doc  checkReft _   _   Nothing _  = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.   checkReft env emb (Just t) _ = (dr $+$) <$> checkSortedReftFull env' r    where 

@@ -52,7 +52,14 @@   = do t1' <- expToBindT t1        t2' <- expToBindT t2        expToBindRef r >>= addExists . RAppTy t1' t2'-expToBindT t +expToBindT (RRTy xts r o t)+  = do xts' <- zip xs <$> mapM expToBindT ts+       r'   <- expToBindRef r+       t'   <- expToBindT t+       return $ RRTy xts' r' o t'+  where+     (xs, ts) = unzip xts +expToBindT t   = return t  expToBindReft              :: SpecProp -> State ExSt SpecProp

@@ -104,6 +104,8 @@          Nothing ->            EApp f <$> mapM expandExpr es +expandExpr (ENeg e)+  = ENeg <$> expandExpr e expandExpr (EBin op e1 e2)   = EBin op <$> expandExpr e1 <*> expandExpr e2 expandExpr (EIte p e1 e2)

@@ -13,6 +13,7 @@ import NameSet import TyCon import Var+import TysWiredIn   import Control.Applicative ((<$>)) import Control.Monad.Reader@@ -26,9 +27,9 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S -import Language.Fixpoint.Misc (mapSnd, thd3)+import Language.Fixpoint.Misc import Language.Fixpoint.Names (takeWhileSym)-import Language.Fixpoint.Types (Expr, SEnv, SortedReft, Symbol, TCEmb, fromListSEnv, insertSEnv, mkSubst, subst, substa, symbol)+import Language.Fixpoint.Types (Expr(..), SEnv, SortedReft, Symbol, TCEmb, fromListSEnv, insertSEnv, mkSubst, subst, substa, symbol)  import Language.Haskell.Liquid.Dictionaries import Language.Haskell.Liquid.GhcMisc (getSourcePos, sourcePosSrcSpan)@@ -36,6 +37,8 @@ import Language.Haskell.Liquid.RefType import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.WiredIn+import Language.Haskell.Liquid.Visitors+import Language.Haskell.Liquid.CoreToLogic  import qualified Language.Haskell.Liquid.Measure as Ms @@ -61,8 +64,8 @@ makeGhcSpec cfg name cbs vars defVars exports env lmap specs      = do sp <- throwLeft =<< execBare act initEnv-       let env = ghcSpecEnv sp-       throwLeft $ checkGhcSpec specs env $ postProcess cbs env sp+       let renv = ghcSpecEnv sp cbs +       throwLeft $ checkGhcSpec specs renv $ postProcess cbs renv sp   where     act       = makeGhcSpec' cfg cbs vars defVars exports specs     throwLeft = either Ex.throw return@@ -78,16 +81,21 @@     asmSigs' = mapSnd (addTyConInfo tcEmbeds tyconEnv <$>) <$> asmSigs     dicts'   = dmapty (addTyConInfo tcEmbeds tyconEnv) dicts -ghcSpecEnv sp        = fromListSEnv binds+ghcSpecEnv sp cbs    = fromListSEnv binds   where      emb              = tcEmbeds sp     binds            =  [(x,        rSort t) | (x, Loc _ t) <- meas sp]                      ++ [(symbol v, rSort t) | (v, Loc _ t) <- ctors sp]                      ++ [(x,        vSort v) | (x, v) <- freeSyms sp, isConLikeId v]+                     ++ [(val x   , rSort stringrSort) | Just (ELit x s) <- mkLit <$> lconsts, isString s]     rSort            = rTypeSortedReft emb      vSort            = rSort . varRSort      varRSort         :: Var -> RSort     varRSort         = ofType . varType+    lconsts          = literals cbs+    stringrSort      :: RSort +    stringrSort      = ofType stringTy+    isString s       = rTypeSort emb stringrSort == s  ------------------------------------------------------------------------------------------------ makeGhcSpec' :: Config -> [CoreBind] -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec

@@ -20,7 +20,7 @@ import DataCon import Id import Name-import Type+import Type hiding (isFunTy) import Var  import Control.Applicative ((<$>), (<*>))@@ -126,9 +126,11 @@ strengthenHaskellMeasures hmeas = (\v -> (val v, fmap strengthenResult v)) <$> (S.toList hmeas)  makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon]-makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = go <$> zip (reverse xts) [1..]+makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = catMaybes (go <$> zip (reverse xts) [1..])   where-    go ((x,t), i) = makeMeasureSelector (Loc loc x) (dty t) dc n i+    go ((x,t), i)+      | isFunTy t = Nothing+      | True      = Just $ makeMeasureSelector (Loc loc x) (dty t) dc n i              dty t         = foldr RAllT  (RFun dummySymbol r (fmap mempty t) mempty) vs     n             = length xts

@@ -21,8 +21,6 @@ import Data.Generics.Aliases (mkT) import Data.Generics.Schemes (everywhere) import Data.Monoid-import Text.PrettyPrint.HughesPJ-import Text.Printf  import qualified Data.HashMap.Strict as M @@ -88,14 +86,17 @@     go (RFun _ i o _)   (RFun x i' o' r)   = RFun x <$> go i i' <*> go o o' <*> return r     go (RAllT _ t)      (RAllT a t')       = RAllT a <$> go t t'     go (RAllT a t)      t'                 = RAllT a <$> go t t'+    go t                (RAllP p t')       = RAllP p <$> go t t'+    go t                (RAllS s t')       = RAllS s <$> go t t'     go t                (RAllE b a t')     = RAllE b a <$> go t t'     go t                (REx b x t')       = REx b x <$> go t t'     go t                (RRTy e r o t')    = RRTy e r o <$> go t t'     go (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy <$> go t1 t1' <*> go t2 t2' <*> return r     go (RApp _ t _ _)   (RApp c t' p r)    = RApp c <$> (zipWithM go t t') <*> return p <*> return r-    go t                st                 = throwError err-     where-       err = errOther $ text $ printf "plugHoles: unhandled case!\nt  = %s\nst = %s\n" (showpp t) (showpp st)+    -- If we reach the default case, there's probably an error, but we defer+    -- throwing it as checkGhcSpec does a much better job of reporting the+    -- problem to the user.+    go _                st                 = return st      pushCls cs (RRTy e r o t) = RRTy e r o (pushCls cs t)     pushCls cs t              = foldr (uncurry rFun) t cs 

@@ -222,6 +222,8 @@         go (EApp (Loc _ f) es)           = go_alias f ++ concatMap go es +        go (ENeg e)+          = go e         go (EBin _ e1 e2)           = go e1 ++ go e2         go (EIte _ e1 e2)

@@ -87,6 +87,7 @@ 	tx _ _ (ESym c)       = ESym c 	tx _ _ (ECon c)       = ECon c 	tx _ _ (ELit l s')    = ELit l s'+	tx s m (ENeg e)       = ENeg (tx s m e) 	tx s m (EBin o e1 e2) = EBin o (tx s m e1) (tx s m e2) 	tx s m (EIte p e1 e2) = EIte (tx s m p) (tx s m e1) (tx s m e2) 	tx s m (ECst e s')    = ECst (tx s m e) s'@@ -136,4 +137,4 @@ txPApp (s, m) f es = PBexp $ txEApp (s, m) f es  cmpSymbol s1 {- symbol in Core -} s2 {- logical Symbol-}-  = (dropModuleNames s1) == s2  +  = (dropModuleNames s1) == s2

@@ -47,6 +47,7 @@ instance Resolvable Expr where   resolve l (EVar s)       = EVar   <$> resolve l s   resolve l (EApp s es)    = EApp   <$> resolve l s  <*> resolve l es+  resolve l (ENeg e)       = ENeg   <$> resolve l e   resolve l (EBin o e1 e2) = EBin o <$> resolve l e1 <*> resolve l e2   resolve l (EIte p e1 e2) = EIte   <$> resolve l p  <*> resolve l e1 <*> resolve l e2   resolve l (ECst x s)     = ECst   <$> resolve l x  <*> resolve l s

@@ -28,7 +28,7 @@  import Language.Fixpoint.Misc         (mapSnd) import Language.Fixpoint.Types     (Tag)-import Language.Haskell.Liquid.GhcInterface (freeVars)+import Language.Haskell.Liquid.Visitors (freeVars)  -- | The @TagKey@ is the top-level binder, and @Tag@ is a singleton Int list 

@@ -26,30 +26,35 @@    , diffcheck ) where -import           Control.Applicative                 ((<$>))-import           Control.Monad+import Control.Applicative                 ((<$>))+import Control.Monad+import Data.Maybe+import System.Directory+import System.Exit+import System.Environment -import           Data.List                           (nub)-import           Data.Monoid+import System.Console.CmdArgs.Explicit+import System.Console.CmdArgs.Implicit     hiding (Loud)+import System.Console.CmdArgs.Text -import           System.Console.CmdArgs              hiding (Loud)-import           System.Directory                    (doesDirectoryExist, canonicalizePath, getCurrentDirectory)-import           System.Environment                  (lookupEnv, withArgs)+import Data.List                           (nub)+import Data.Monoid+ import           System.FilePath                     (dropFileName, isAbsolute,                                                       takeDirectory, (</>)) -import           Language.Fixpoint.Config            hiding (Config, real)-import           Language.Fixpoint.Files-import           Language.Fixpoint.Misc-import           Language.Fixpoint.Names             (dropModuleNames)-import           Language.Fixpoint.Types             -import           Language.Haskell.Liquid.Annotate-import           Language.Haskell.Liquid.Misc-import           Language.Haskell.Liquid.PrettyPrint-import           Language.Haskell.Liquid.Types       hiding (config, name, typ)+import Language.Fixpoint.Config            hiding (Config, real)+import Language.Fixpoint.Files+import Language.Fixpoint.Misc+import Language.Fixpoint.Names             (dropModuleNames)+import Language.Fixpoint.Types+import Language.Haskell.Liquid.Annotate+import Language.Haskell.Liquid.Misc+import Language.Haskell.Liquid.PrettyPrint+import Language.Haskell.Liquid.Types       hiding (config, name, typ) -import           Text.Parsec.Pos                     (newPos)-import           Text.PrettyPrint.HughesPJ+import Text.Parsec.Pos                     (newPos)+import Text.PrettyPrint.HughesPJ           hiding (Mode)   ---------------------------------------------------------------------------------@@ -155,12 +160,33 @@  getOpts :: IO Config getOpts = do cfg0    <- envCfg-             cfg1    <- mkOpts =<< cmdArgsRun config+             cfg1    <- mkOpts =<< cmdArgsRun' config              pwd     <- getCurrentDirectory              cfg     <- canonicalizePaths (fixCfg $ mconcat [cfg0, cfg1]) pwd              whenNormal $ putStrLn copyright-             return cfg+             case smtsolver cfg of+               Just _  -> return cfg+               Nothing -> do smts <- mapM find [Z3, Cvc4, Mathsat]+                             case catMaybes smts of+                               (s:_) -> return (cfg {smtsolver = Just s})+                               _     -> do putStrLn "ERROR: LiquidHaskell requires z3, cvc4, or mathsat to be installed."+                                           exitWith $ ExitFailure 2 +cmdArgsRun' :: Mode (CmdArgs a) -> IO a+cmdArgsRun' mode+  = do parseResult <- process mode <$> getArgs+       case parseResult of+         Left err ->+           putStrLn (help err) >> exitFailure+         Right args ->+           cmdArgsApply args+  where+    help err+      = showText defaultWrap $ helpText [err] HelpFormatDefault mode++find :: SMTSolver -> IO (Maybe SMTSolver)+find smt = maybe Nothing (const $ Just smt) <$> findExecutable (show smt)+ -- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have --   to worry about relative paths. canonicalizePaths :: Config -> FilePath -> IO Config@@ -284,7 +310,7 @@     writeBlock _  _ ss     = forM_ ("\n" : ss) putStrLn  resDocs _ Safe             = [text "SAFE"]-resDocs k (Crash xs s)     = text ("CRASH: " ++ s) : pprManyOrdered k "" xs+resDocs k (Crash xs s)     = text ("ERROR: " ++ s) : pprManyOrdered k "" xs resDocs k (Unsafe xs)      = text "UNSAFE" : pprManyOrdered k "" (nub xs) resDocs _ (UnknownError d) = [text $ "PANIC: Unexpected Error: " ++ d, reportUrl] 

@@ -10,8 +10,7 @@ import Language.Haskell.Liquid.Types import Language.Haskell.Liquid.Constraint.Types -import Language.Fixpoint.Types           -+import Language.Fixpoint.Types  instance Monoid LConstraint where 	mempty  = LC []

@@ -1,3 +1,5 @@+{-# LANGUAGE DeriveFoldable            #-}+{-# LANGUAGE DeriveTraversable         #-} {-# LANGUAGE StandaloneDeriving        #-} {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE NoMonomorphismRestriction #-}@@ -46,6 +48,8 @@ import qualified Data.Text           as T import Data.Bifunctor import Data.List (foldl')+import qualified Data.Foldable    as F+import qualified Data.Traversable as T  import Text.Printf @@ -60,8 +64,8 @@ import Language.Haskell.Liquid.Variance import Language.Haskell.Liquid.Types            hiding (binds, Loc, loc, freeTyVars, Def) import Language.Haskell.Liquid.Strata-import Language.Haskell.Liquid.GhcInterface import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.Visitors import Language.Haskell.Liquid.PredType         hiding (freeTyVars)           import Language.Haskell.Liquid.GhcMisc          ( isInternal, collectArguments, tickSrcSpan                                                 , hasBaseTypeVar, showPpr)@@ -554,7 +558,7 @@        pflag <- pruneRefs <$> get        γ' <- γ ++= ("bsplitC", v, t1)         let r = (mempty :: UReft F.Reft){ur_reft = F.Reft (F.dummySymbol,  [F.RConc $ constraintToLogic γ' (lcs γ')])}-       let t1' = t1 `strengthen` r+       let t1' = addRTyConInv (invs γ')  t1 `strengthen` r        return $ bsplitC' γ' t1' t2 pflag   where     F.Reft(v, _) = ur_reft (fromMaybe mempty (stripRTypeBase t1))@@ -656,6 +660,11 @@  {- see tests/pos/polyfun for why you need everything in fixenv -}  addCGEnv :: (SpecType -> SpecType) -> CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv+addCGEnv tx γ (msg, x, RAllE y tyy tyx)+  = do y' <- fresh +       γ' <- addCGEnv tx γ (msg, y', tyy)+       addCGEnv tx γ' (msg, x, tyx `F.subst1` (y, F.EVar y'))+ addCGEnv tx γ (_, x, t')    = do idx   <- fresh        let t  = tx $ normalize {-x-} idx t'  @@ -893,13 +902,25 @@ ----------------------- TERMINATION TYPE -------------------------------------- ------------------------------------------------------------------------------- -makeDecrIndex :: (Var, SpecType)-> CG [Int]-makeDecrIndex (x, t) +makeDecrIndex :: (Var, Template SpecType)-> CG [Int]+makeDecrIndex (x, Assumed t)+  = do dindex <- makeDecrIndexTy x t+       case dindex of+         Left _  -> return []+         Right i -> return i+makeDecrIndex (x, Asserted t)+  = do dindex <- makeDecrIndexTy x t+       case dindex of+         Left msg -> addWarning msg >> return []+         Right i  -> return i+makeDecrIndex _ = return []++makeDecrIndexTy x t   = do spDecr <- specDecr <$> get        hint   <- checkHint' (L.lookup x $ spDecr)        case dindex of-         Nothing -> addWarning msg >> return []-         Just i  -> return $ fromMaybe [i] hint+         Nothing -> return $ Left msg -- addWarning msg >> return []+         Just i  -> return $ Right $ fromMaybe [i] hint     where        ts         = ty_args $ toRTypeRep t        checkHint' = checkHint x ts isDecreasing@@ -921,7 +942,7 @@        mapM  (safeLogIndex msg  ts) index     where        loc   = getSrcSpan x-       ts    = ty_args $ toRTypeRep t+       ts    = ty_args $ toRTypeRep $ unTemplate t        msg'  = ErrTermin [x] loc (text $ "No decreasing argument on " ++ (showPpr x) ++ " with " ++ (showPpr vs))        msg   = ErrTermin [x] loc (text "No decreasing parameter") @@ -1002,22 +1023,22 @@        let cmakeFinType = if sflag then makeFinType else id        let cmakeFinTy   = if sflag then makeFinTy   else snd        let xets = mapThd3 (fmap cmakeFinType) <$> xets''-       ts'      <- mapM refreshArgs $ (fromAsserted . thd3 <$> xets)+       ts'      <- mapM (T.mapM refreshArgs) $ (thd3 <$> xets)        let vs    = zipWith collectArgs ts' es        is       <- mapM makeDecrIndex (zip xs ts') >>= checkSameLens        let ts = cmakeFinTy  <$> zip is ts'-       let xeets = (\vis -> [(vis, x) | x <- zip3 xs is ts]) <$> (zip vs is)+       let xeets = (\vis -> [(vis, x) | x <- zip3 xs is $ map unTemplate ts]) <$> (zip vs is)        (L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes        let rts   = (recType <$>) <$> xeets-       let xts   = zip xs (Asserted <$> ts)+       let xts   = zip xs ts        γ'       <- foldM extender γ xts        let γs    = [γ' `withTRec` (zip xs rts') | rts' <- rts]-       let xets' = zip3 xs es (Asserted <$> ts)+       let xets' = zip3 xs es ts        mapM_ (uncurry $ consBind True) (zip γs xets')        return γ'   where        (xs, es) = unzip xes-       collectArgs    = collectArguments . length . ty_binds . toRTypeRep+       collectArgs    = collectArguments . length . ty_binds . toRTypeRep . unTemplate        checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]        checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)        checkSameLens  = checkAll err2 length@@ -1050,8 +1071,11 @@                    | otherwise              = Nothing         err      = "Constant: consCBWithExprs" -makeFinTy (ns, t) = fromRTypeRep $ trep {ty_args = args'}-  where trep = toRTypeRep t+makeFinTy (ns, t) = fmap go t+  where+    go t = fromRTypeRep $ trep {ty_args = args'}+      where+        trep = toRTypeRep t         args' = mapNs ns makeFinType $ ty_args trep  @@ -1181,18 +1205,18 @@  addBinders γ0 x' cbs   = foldM (++=) (γ0 -= x') [("addBinders", x, t) | (x, t) <- cbs] -data Template a = Asserted a | Assumed a | Unknown deriving (Functor)+data Template a = Asserted a | Assumed a | Unknown deriving (Functor, F.Foldable, T.Traversable)  deriving instance (Show a) => (Show (Template a)) +unTemplate (Asserted t) = t+unTemplate (Assumed t) = t+unTemplate _ = errorstar "Constraint.Generate.unTemplate called on `Unknown`"  addPostTemplate γ (Asserted t) = Asserted <$> addPost γ t addPostTemplate γ (Assumed  t) = Assumed  <$> addPost γ t addPostTemplate _ Unknown      = return Unknown  -fromAsserted (Asserted t) = t-fromAsserted _            = errorstar "Constraint.Generate.fromAsserted called on invalid inputs"- safeFromAsserted _ (Asserted t) = t safeFromAsserted msg _ = errorstar $ "safeFromAsserted:" ++ msg  @@ -1407,8 +1431,8 @@ consE _ e@(Coercion _)    = trueTy $ exprType e -consE _ e	    -  = errorstar $ "consE cannot handle " ++ showPpr e +consE _ e@(Type t)     +  = errorstar $ "consE cannot handle type" ++ showPpr (e, t)   castTy _ τ (Var x)   = do t <- trueTy τ @@ -1446,8 +1470,11 @@        return t  checkUnbound γ e x t -  | x `notElem` (F.syms t) = t-  | otherwise              = errorstar $ "consE: cannot handle App " ++ showPpr e ++ " at " ++ showPpr (loc γ)+  | x `notElem` (F.syms t) +  = t+  | otherwise              +  = errorstar $ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t+                 ++ "\nIn\t"  ++ showPpr e ++ " at " ++ showPpr (loc γ)  dropExists γ (REx x tx t) = liftM (, t) $ (γ, "dropExists") += (x, tx) dropExists γ t            = return (γ, t)

@@ -22,13 +22,13 @@ import Literal import IdInfo --import TysWiredIn+import qualified Data.ByteString as B+import TysWiredIn   import Control.Applicative   import Language.Fixpoint.Misc-import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym)+import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym, propConName) import Language.Fixpoint.Types hiding (Def, R, simplify) import qualified Language.Fixpoint.Types as F import Language.Haskell.Liquid.GhcMisc@@ -79,11 +79,12 @@   where rep = toRTypeRep t         res = ty_res rep         xs  = intSymbol (symbol ("x" :: String)) <$> [1..]-        r'  = U (exprReft (EApp f (EVar <$> vxs)))         mempty mempty-        r   = U (propReft (PBexp $ EApp f (EVar <$> vxs))) mempty mempty-        vxs = fst $  unzip $ dropWhile isClassBind $ zip xs (ty_args rep)+        r'  = U (exprReft (EApp f (mkA <$> vxs)))         mempty mempty+        r   = U (propReft (PBexp $ EApp f (mkA <$> vxs))) mempty mempty+        vxs = dropWhile isClassBind $ zip xs (ty_args rep)         f   = dummyLoc $ dropModuleNames $ simplesymbol v         t   = (ofType $ varType v) :: SpecType+        mkA = \(x, t) -> if isBool t then EApp (dummyLoc propConName) [(EVar x)] else EVar x   simplesymbol = symbol . getName@@ -151,9 +152,9 @@     go acc (C.Lam x e)  = go (symbol x : acc) e     go acc (C.Tick _ e) = go acc e     go acc e            | eqType rty boolTy -                        = (reverse acc,) . Left  . traceShow "coreToPred"  <$> coreToPred e  +                        = (reverse acc,) . Left  <$> coreToPred e                           | otherwise       -                        = (reverse acc,) . Right . traceShow "coreToLogic" <$> coreToLogic e+                        = (reverse acc,) . Right <$> coreToLogic e      inline_preds = inline (eqType boolTy . varType) @@ -242,6 +243,9 @@         (\x -> makeApp def lmap x args) <$> tosymbol' f  makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr+makeApp _ _ f [e] | val f == symbol ("GHC.Num.negate" :: String)+  = ENeg e+ makeApp _ _ f [e1, e2] | Just op <- M.lookup (val f) bops   = EBin op e1 e2 @@ -299,9 +303,20 @@ mkLit (MachFloat  n)   = mkR n mkLit (MachDouble n)   = mkR n mkLit (LitInteger n _) = mkI n+mkLit (MachStr s)      = mkS s  mkLit _                = Nothing -- ELit sym sort+ mkI                    = Just . ECon . I   mkR                    = Just . ECon . F.R . fromRational+mkS s                  = Just (ELit  (dummyLoc $ symbol s) stringSort)+++stringSort = rTypeSort M.empty (ofType stringTy :: RSort)+-- stringSort = rTypeSort M.empty (ofType stringTy :: RSort)+++instance Symbolic B.ByteString where+  symbol x = symbol $ init $ tail $ show x  ignoreVar i = simpleSymbolVar i `elem` ["I#"] 

@@ -42,8 +42,9 @@ import            Language.Fixpoint.Types         (FixResult (..)) import            Language.Fixpoint.Files import            Language.Haskell.Liquid.Types   (AnnInfo (..), Error, TError (..), Output (..))-import            Language.Haskell.Liquid.GhcInterface import            Language.Haskell.Liquid.GhcMisc+import            Language.Haskell.Liquid.Visitors+import            Language.Haskell.Liquid.Errors   () import            Text.Parsec.Pos                  (sourceName, sourceLine, sourceColumn, SourcePos, newPos) import            Text.PrettyPrint.HughesPJ        (text, render, Doc) 

@@ -9,11 +9,13 @@   import           Control.Applicative                 ((<$>), (<*>))+import           Control.Arrow                       (second) import           Control.Exception                   (Exception (..)) import           Data.Aeson-import           Data.Hashable+import           Data.Generics                       (everywhere, mkT) import qualified Data.HashMap.Strict                 as M import qualified Data.HashSet                        as S+import           Data.Hashable import           Data.List                           (intersperse) import           Data.Maybe                          (fromMaybe, maybeToList) import           Data.Monoid                         hiding ((<>))@@ -21,12 +23,13 @@ import           Language.Fixpoint.Types             hiding (shiftVV) import           Language.Haskell.Liquid.PrettyPrint import           Language.Haskell.Liquid.RefType+import           Language.Haskell.Liquid.Simplify import           Language.Haskell.Liquid.Tidy import           Language.Haskell.Liquid.Types import           SrcLoc                              (SrcSpan) import           Text.PrettyPrint.HughesPJ-import           Control.Arrow                       (second) + type Ctx = M.HashMap Symbol SpecType  ------------------------------------------------------------------------@@ -64,10 +67,11 @@     (t', ro)  = stripRType t                  stripRType    :: SpecType -> (SpecType, Maybe RReft)-stripRType t  = (t', ro)+stripRType st = (t', ro)   where     t'        = fmap (const (uTop mempty)) t     ro        = stripRTypeBase  t +    t         = simplifyBounds st   tidyREnv      :: [Symbol] -> M.HashMap Symbol SpecType -> [(Symbol, SpecType)] tidyREnv xs m = [(x, t) | x <- xs', t <- maybeToList (M.lookup x m), ok t]@@ -119,8 +123,10 @@   | otherwise   = dt <+> dr      where       dt        = rtypeDoc Lossy t'-      dr        = maybe empty ((text "|" <+>) . pprint) ro +      dr        = maybe empty ((text "|" <+>) . pprint . everywhere (mkT noCasts)) ro        (t', ro)  = stripRType t+      noCasts (ECst x _) = x+      noCasts e          = e  -- full = isNontrivialVV $ rTypeValueVar t =  

@@ -50,13 +50,13 @@   refresh [] = fresh   refresh s  = return s -instance (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) where+instance (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r) where   fresh   = errorstar "fresh RefType"   refresh = refreshRefType   true    = trueRefType  ------------------------------------------------------------------------------------------------trueRefType :: (Freshable m Integer, Freshable m r, Reftable r) => RRType r -> m (RRType r)+trueRefType :: (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => RRType r -> m (RRType r) ----------------------------------------------------------------------------------------------- trueRefType (RAllT α t)   = RAllT α <$> true t@@ -79,7 +79,13 @@ trueRefType (RVar a r)   = RVar a <$> true r -trueRefType t+trueRefType (RAllE y ty tx)+  = do y'  <- fresh +       ty' <- true ty+       tx' <- true tx+       return $ RAllE y' ty' (tx' `subst1` (y, EVar y')) ++trueRefType t    = return t  trueRef (RProp s t) = RProp s <$> trueRefType t@@ -87,7 +93,7 @@   ------------------------------------------------------------------------------------------------refreshRefType :: (Freshable m Integer, Freshable m r, Reftable r) => RRType r -> m (RRType r)+refreshRefType :: (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => RRType r -> m (RRType r) ----------------------------------------------------------------------------------------------- refreshRefType (RAllT α t)   = RAllT α <$> refresh t@@ -110,6 +116,12 @@  refreshRefType (RAppTy t t' r)   = RAppTy <$> refresh t <*> refresh t' <*> refresh r++refreshRefType (RAllE y ty tx)+  = do y'  <- fresh +       ty' <- refresh ty+       tx' <- refresh tx+       return $ RAllE y' ty' (tx' `subst1` (y, EVar y'))   refreshRefType t   = return t

@@ -10,8 +10,6 @@   -- * extract all information needed for verification     getGhcInfo -  -- * visitors -  , CBVisitable (..)    ) where import IdInfo import InstEnv@@ -22,7 +20,6 @@ import DriverPipeline (compileFile) import Text.PrettyPrint.HughesPJ import HscTypes hiding (Target)-import Literal import CoreSyn  import Var@@ -36,10 +33,9 @@  import DynFlags import Control.Monad (filterM, foldM, when, forM, forM_, liftM)-import Control.DeepSeq import Control.Applicative  hiding (empty) import Data.Monoid hiding ((<>))-import Data.List (foldl', find, (\\), delete, nub)+import Data.List (find, nub) import Data.Maybe (catMaybes, maybeToList) import qualified Data.HashSet        as S   @@ -55,6 +51,8 @@ import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.PrettyPrint +import Language.Haskell.Liquid.Visitors+ import Language.Haskell.Liquid.CmdLine (withPragmas) import Language.Haskell.Liquid.Parse @@ -96,6 +94,10 @@       modguts            <- getGhcModGuts1 target       hscEnv             <- getSession       coreBinds          <- liftIO $ anormalize (not $ nocaseexpand cfg) hscEnv modguts+      let datacons        = [ dataConWorkId dc+                            | tc <- mgi_tcs modguts+                            , dc <- tyConDataCons tc+                            ]       let impVs           = importVars  coreBinds        let defVs           = definedVars coreBinds        let useVs           = readVars    coreBinds@@ -105,7 +107,7 @@       (spec, imps, incs) <- moduleSpec cfg coreBinds (impVs ++ defVs) letVs name' modguts tgtSpec logicmap impSpecs'       liftIO              $ whenLoud $ putStrLn $ "Module Imports: " ++ show imps       hqualFiles         <- moduleHquals modguts paths target imps incs-      return              $ GI hscEnv coreBinds derVs impVs letVs useVs hqualFiles imps incs spec +      return              $ GI hscEnv coreBinds derVs impVs (letVs ++ datacons) useVs hqualFiles imps incs spec    makeLogicMap @@ -335,126 +337,8 @@   = Nothing  ---------------------------------------------------------------------------------------------------------------- A CoreBind Visitor --------------------------------------------------------------------------------------------------------- --- TODO: syb-shrinkage -class CBVisitable a where-  freeVars :: S.HashSet Var -> a -> [Var]-  readVars :: a -> [Var] -  letVars  :: a -> [Var] -  literals :: a -> [Literal]--instance CBVisitable [CoreBind] where-  freeVars env cbs = (sortNub xs) \\ ys -    where xs = concatMap (freeVars env) cbs -          ys = concatMap bindings cbs-  -  readVars = concatMap readVars-  letVars  = concatMap letVars -  literals = concatMap literals--instance CBVisitable CoreBind where-  freeVars env (NonRec x e) = freeVars (extendEnv env [x]) e -  freeVars env (Rec xes)    = concatMap (freeVars env') es -                              where (xs,es) = unzip xes -                                    env'    = extendEnv env xs --  readVars (NonRec _ e)     = readVars e-  readVars (Rec xes)        = concat [x `delete` nubReadVars e |(x, e) <- xes]-    where nubReadVars = sortNub . readVars--  letVars (NonRec x e)      = x : letVars e-  letVars (Rec xes)         = xs ++ concatMap letVars es-    where -      (xs, es)              = unzip xes--  literals (NonRec _ e)      = literals e-  literals (Rec xes)         = concatMap literals $ map snd xes--instance CBVisitable (Expr Var) where-  freeVars = exprFreeVars-  readVars = exprReadVars-  letVars  = exprLetVars-  literals = exprLiterals--exprFreeVars = go -  where -    go env (Var x)         = if x `S.member` env then [] else [x]  -    go env (App e a)       = (go env e) ++ (go env a)-    go env (Lam x e)       = go (extendEnv env [x]) e-    go env (Let b e)       = (freeVars env b) ++ (go (extendEnv env (bindings b)) e)-    go env (Tick _ e)      = go env e-    go env (Cast e _)      = go env e-    go env (Case e x _ cs) = (go env e) ++ (concatMap (freeVars (extendEnv env [x])) cs) -    go _   _               = []--exprReadVars = go-  where-    go (Var x)             = [x]-    go (App e a)           = concatMap go [e, a] -    go (Lam _ e)           = go e-    go (Let b e)           = readVars b ++ go e -    go (Tick _ e)          = go e-    go (Cast e _)          = go e-    go (Case e _ _ cs)     = (go e) ++ (concatMap readVars cs) -    go _                   = []--exprLetVars = go-  where-    go (Var _)             = []-    go (App e a)           = concatMap go [e, a] -    go (Lam x e)           = x : go e-    go (Let b e)           = letVars b ++ go e -    go (Tick _ e)          = go e-    go (Cast e _)          = go e-    go (Case e x _ cs)     = x : go e ++ concatMap letVars cs-    go _                   = []--exprLiterals = go-  where-    go (Lit l)             = [l]-    go (App e a)           = concatMap go [e, a] -    go (Let b e)           = literals b ++ go e -    go (Lam _ e)           = go e-    go (Tick _ e)          = go e-    go (Cast e _)          = go e-    go (Case e _ _ cs)     = (go e) ++ (concatMap literals cs) -    go _                   = []---instance CBVisitable (Alt Var) where-  freeVars env (a, xs, e) = freeVars env a ++ freeVars (extendEnv env xs) e-  readVars (_,_, e)       = readVars e-  letVars  (_,xs,e)       = xs ++ letVars e-  literals (c,_, e)       = literals c ++ literals e---instance CBVisitable AltCon where-  freeVars _ (DataAlt dc) = dataConImplicitIds dc-  freeVars _ _            = []-  readVars _              = []-  letVars  _              = []-  literals (LitAlt l)     = [l]-  literals _              = []----extendEnv = foldl' (flip S.insert)--bindings (NonRec x _) -  = [x]-bindings (Rec  xes  ) -  = map fst xes----------------------------------------------------------------------------- Strictness -------------------------------------------------------------------------------------------------------------------------instance NFData Var-instance NFData SrcSpan  instance PPrint GhcSpec where   pprint spec =  (text "******* Target Variables ********************")

@@ -184,6 +184,13 @@ holeRefP    = reserved "_" >> spaces >> return (RHole . uTop) refasHoleP  = refasP <|> (reserved "_" >> return [hole]) +-- FIXME: the use of `blanks = oneOf " \t"` here is a terrible and fragile hack+-- to avoid parsing:+--+--   foo :: a -> b+--   bar :: a+--+-- as `foo :: a -> b bar`.. bbaseP :: Parser (Reft -> BareType) bbaseP    =  holeRefP@@ -645,7 +652,7 @@   = do pos  <- getPosition        name <- upperIdP        spaces-       args <- sepBy aliasIdP spaces+       args <- sepBy aliasIdP blanks        whiteSpace >> reservedOp "=" >> whiteSpace        body <- bodyP         let (tArgs, vArgs) = partition (isLower . headSym) args@@ -740,16 +747,16 @@  measurePatP :: Parser (LocSymbol, [LocSymbol]) measurePatP -  =  try tupPatP - <|> try (parens conPatP)- <|> try (parens consPatP)- <|>     (parens nilPatP)+  =  parens (try conPatP <|> try consPatP <|> nilPatP <|> tupPatP)+ <|> nullaryConPatP -tupPatP  = mkTupPat  <$> (parens       $  sepBy locLowerIdP comma)+tupPatP  = mkTupPat  <$> sepBy1 locLowerIdP comma conPatP  = (,)       <$> locParserP dataConNameP <*> sepBy locLowerIdP whiteSpace consPatP = mkConsPat <$> locLowerIdP  <*> colon <*> locLowerIdP-nilPatP  = mkNilPat  <$> brackets whiteSpace +nilPatP  = mkNilPat  <$> brackets whiteSpace +nullaryConPatP = nilPatP <|> ((,[]) <$> locParserP dataConNameP)+ mkTupPat zs     = (tupDataCon (length zs), zs) mkNilPat _      = (dummyLoc "[]", []    ) mkConsPat x _ y = (dummyLoc ":" , [x, y])@@ -762,8 +769,18 @@  dataConFieldsP    =   (braces $ sepBy predTypeDDP comma)-  <|> (sepBy (parens predTypeDDP) spaces)+  <|> (sepBy dataConFieldP spaces) +dataConFieldP+  = parens ( try predTypeDDP+             <|> do v <- dummyBindP+                    t <- bareTypeP+                    return (v,t)+           )+    <|> do v <- dummyBindP+           t <- bareTypeP+           return (v,t)+ predTypeDDP    = liftM2 (,) bbindP bareTypeP @@ -827,7 +844,7 @@          Nothing -> return []  -- specWrap  = between     (string "{-@" >> spaces) (spaces >> string "@-}")-specWraps = betweenMany (string "{-@" >> spaces) (spaces >> string "@-}")+specWraps = betweenMany (string "{-@" >> whiteSpace) (whiteSpace >> string "@-}")  --------------------------------------------------------------- -- | Bundling Parsers into a Typeclass ------------------------

@@ -281,9 +281,10 @@   = r2 `meet` r1   | all (\(_, x, EVar y) -> x /= y) (pargs π)   = r2 `meet` (subst su r1)-  | otherwise+  | otherwise    = errorstar $ "PredType.meetListWithPSub partial application to " ++ showpp π-  where su  = mkSubst [(x, y) | (x, (_, _, y)) <- zip (fst <$> ss) (pargs π)]+  where +    su  = mkSubst [(x, y) | (x, (_, _, y)) <- zip (fst <$> ss) (pargs π)]  meetListWithPSubRef ss (RProp s1 r1) (RProp s2 r2) π   | all (\(_, x, EVar y) -> x == y) (pargs π)

@@ -22,14 +22,13 @@ specificationQualifiers :: Int -> GhcInfo -> [Qualifier] ----------------------------------------------------------------------------------- specificationQualifiers k info-  = [ q | (x, t) <- (tySigs $ spec info) ++ (asmSigs $ spec info)+  = [ q | (x, t) <- (tySigs $ spec info) ++ (asmSigs $ spec info) ++ (ctors $ spec info)         -- FIXME: this mines extra, useful qualifiers but causes a significant increase in running time         -- , ((isClassOp x || isDataCon x) && x `S.member` (S.fromList $ impVars info ++ defVars info)) || x `S.member` (S.fromList $ defVars info)         , x `S.member` (S.fromList $ defVars info)         , q <- refTypeQuals (getSourcePos x) (tcEmbeds $ spec info) (val t)         , length (q_params q) <= k + 1     ]-  -- GRAVEYARD: scraping quals from imports kills the system with too much crap -- specificationQualifiers info = {- filter okQual -} qs 

@@ -0,0 +1,32 @@+module Language.Haskell.Liquid.Simplify (simplifyBounds) where++import Language.Haskell.Liquid.Types++import Language.Fixpoint.Types++import Control.Applicative                 ((<$>))++simplifyLen = 5++simplifyBounds :: SpecType -> SpecType+simplifyBounds = fmap go +  where+  	go x = x{ur_reft = go' $ ur_reft x}++  	go' (Reft (v, rs)) = Reft(v, filter (not . isBoundLike) rs)++  	isBoundLike (RConc pred) = isBoundLikePred pred+  	isBoundLike (RKvar _ _)  = False++  	isBoundLikePred (PAnd ps)+  	  = moreThan simplifyLen (isImp <$> ps)+  	isBoundLikePred _ = False++  	isImp (PImp _ _) = True+  	isImp _          = False++  	moreThan 0 _          = True+  	moreThan _ []         = False+  	moreThan i (True:xs)  = moreThan (i-1) xs+  	moreThan i (False:xs) = moreThan i xs+

@@ -231,6 +231,7 @@ import Language.Fixpoint.Misc import Language.Fixpoint.Types      hiding (Predicate, Def, R) import Language.Fixpoint.Names      (funConName, listConName, tupConName)+import qualified Language.Fixpoint.PrettyPrint as F import CoreSyn (CoreBind)  import Language.Haskell.Liquid.Variance@@ -238,7 +239,6 @@   import Data.Default- ----------------------------------------------------------------------------- -- | Command Line Config Options -------------------------------------------- -----------------------------------------------------------------------------@@ -261,7 +261,7 @@   , totality       :: Bool       -- ^ check totality in definitions   , noPrune        :: Bool       -- ^ disable prunning unsorted Refinements   , maxParams      :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers-  , smtsolver      :: SMTSolver  -- ^ name of smtsolver to use [default: z3-API]+  , smtsolver      :: Maybe SMTSolver  -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order]   , shortNames     :: Bool       -- ^ drop module qualifers from pretty-printed names.   , shortErrors    :: Bool       -- ^ don't show subtyping errors and contexts.    , ghcOptions     :: [String]   -- ^ command-line options to pass to GHC@@ -302,7 +302,7 @@  ppEnv           = ppEnvPrintPreds _ppEnvCurrent    = PP False False False False-ppEnvPrintPreds = PP True False False False+ppEnvPrintPreds = PP False False False False ppEnvShort pp   = pp { ppShort = True }  @@ -449,7 +449,14 @@   hashWithSalt i (PV n _ _ _) = hashWithSalt i n  + --------------------------------------------------------------------+------ Strictness --------------------------------------------------+--------------------------------------------------------------------++instance NFData Var+instance NFData SrcSpan+-------------------------------------------------------------------- ------------------ Predicates -------------------------------------- -------------------------------------------------------------------- @@ -991,20 +998,17 @@ instance (PPrint r, Reftable r) => Reftable (UReft r) where   isTauto            = isTauto_ureft    ppTy               = ppTy_ureft-  toReft (U r ps _)  = toReft r `meet` toReft ps+  toReft (U r ps _)  = toReft r `meet` toReft ps    params (U r _ _)   = params r   bot (U r _ s)      = U (bot r) (Pr []) (bot s)   top (U r p s)      = U (top r) (top p) (top s)    ofReft = error "TODO: UReft.ofReft" -isTauto_ureft u      = isTauto (ur_reft u) && isTauto (ur_pred u) && (isTauto $ ur_strata u)--isTauto_ureft' u     = isTauto (ur_reft u) && isTauto (ur_pred u)+isTauto_ureft u      = isTauto (ur_reft u) && isTauto (ur_pred u) -- && (isTauto $ ur_strata u)  ppTy_ureft u@(U r p s) d    | isTauto_ureft  u  = d-  | isTauto_ureft' u  = d <> ppr_str s   | otherwise         = ppr_reft r (ppTy p d) s  ppr_reft r d s       = braces (toFix v <+> colon <+> d <> ppr_str s <+> text "|" <+> pprint r')@@ -1050,6 +1054,7 @@   isTauto (Pr ps)      = null ps    bot (Pr _)           = errorstar "No BOT instance for Predicate"+  -- NV: This does not print abstract refinements....   -- HACK: Hiding to not render types in WEB DEMO. NEED TO FIX.   ppTy r d | isTauto r        = d             | not (ppPs ppEnv) = d@@ -1117,6 +1122,7 @@ isBase (RFun _ t1 t2 _) = isBase t1 && isBase t2 isBase (RAppTy t1 t2 _) = isBase t1 && isBase t2 isBase (RRTy _ _ _ t)   = isBase t+isBase (RAllE _ _ t)    = isBase t isBase _                = False  isFunTy (RAllE _ _ t)    = isFunTy t@@ -1308,66 +1314,34 @@   pprint = pprint . val   instance PPrint Int where-  pprint = toFix+  pprint = F.pprint  instance PPrint Integer where-  pprint = toFix+  pprint = F.pprint  instance PPrint Constant where-  pprint = toFix+  pprint = F.pprint  instance PPrint Brel where-  pprint Eq = text "=="-  pprint Ne = text "/="-  pprint r  = toFix r+  pprint = F.pprint  instance PPrint Bop where-  pprint  = toFix +  pprint = F.pprint  instance PPrint Sort where-  pprint = toFix  +  pprint = F.pprint  instance PPrint Symbol where   pprint = pprint . symbolText  instance PPrint Expr where-  pprint (EApp f es)     = {- parens $ -} intersperse empty $ (pprint f) : (pprint <$> es) -  pprint (ECon c)        = pprint c -  pprint (EVar s)        = pprint s-  pprint (ELit s _)      = pprint s-  pprint (EBin o e1 e2)  = {- parens $ -} pprint e1 <+> pprint o <+> pprint e2-  pprint (EIte p e1 e2)  = {- parens $ -} text "if" <+> parens (pprint p) <+> text "then" <+> pprint e1 <+> text "else" <+> pprint e2 -  pprint (ECst e so)     = parens $ pprint e <+> text " : " <+> pprint so -  pprint (EBot)          = text "_|_"-  pprint (ESym s)        = pprint s+  pprint = F.pprint  instance PPrint SymConst where-  pprint (SL s)          = text $ T.unpack s+  pprint = F.pprint  instance PPrint Pred where-  pprint PTop            = text "???"-  pprint PTrue           = trueD -  pprint PFalse          = falseD-  pprint (PBexp e)       = {- parens $ -} pprint e-  pprint (PNot p)        = {- parens $ -} text "not" <+> parens (pprint p)-  pprint (PImp p1 p2)    = {- parens $ -} pprint p1 <+> text "=>"  <+> pprint p2-  pprint (PIff p1 p2)    = {- parens $ -} (pprint p1) <+> text "<=>" <+> (pprint p2)-  pprint (PAnd ps)       = {- parens $ -} pprintBin trueD  andD ps-  pprint (POr  ps)       = {- parens $ -} pprintBin falseD orD  ps -  pprint (PAtom r e1 e2) = {- parens $ -} pprint e1 <+> pprint r <+> pprint e2-  pprint (PAll xts p)    = text "forall" <+> toFix xts <+> text "." <+> pprint p--trueD  = text "true"-falseD = text "false"-andD   = text " &&"-orD    = text " ||"--pprintBin b _ []     = b-pprintBin _ o xs     = intersperse o $ pprint <$> xs ---- pprintBin b o []     = b--- pprintBin b o [x]    = pprint x--- pprintBin b o (x:xs) = pprint x <+> o <+> pprintBin b o xs +  pprint = F.pprint  instance PPrint a => PPrint (PVar a) where   pprint (PV s _ _ xts)   = pprint s <+> hsep (pprint <$> dargs xts)@@ -1382,15 +1356,11 @@   pprint (RConc p)     = pprint p   pprint k             = toFix k  -instance PPrint Reft where -  pprint r@(Reft (_,ras)) -    | isTauto r        = text "true"-    | otherwise        = {- intersperse comma -} pprintBin trueD andD $ flattenRefas ras+instance PPrint Reft where+  pprint = F.pprint  instance PPrint SortedReft where-  pprint (RR so (Reft (v, ras))) -    = braces -    $ (pprint v) <+> (text ":") <+> (toFix so) <+> (text "|") <+> pprint ras+  pprint = F.pprint  ------------------------------------------------------------------------ -- | Error Data Type ---------------------------------------------------

@@ -0,0 +1,142 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE TypeSynonymInstances      #-} +{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE TupleSections             #-}+{-# LANGUAGE DeriveDataTypeable        #-}+{-# LANGUAGE ScopedTypeVariables       #-}+++module Language.Haskell.Liquid.Visitors (+  +  -- * visitors +  CBVisitable (..) ++  ) where+++import DataCon+import Literal+import CoreSyn++import Var++import Data.List (foldl', (\\), delete)++import qualified Data.HashSet        as S+import Language.Fixpoint.Misc+import Language.Haskell.Liquid.GhcMisc ()+++------------------------------------------------------------------------------+-------------------------------- A CoreBind Visitor --------------------------+------------------------------------------------------------------------------++-- TODO: syb-shrinkage++class CBVisitable a where+  freeVars :: S.HashSet Var -> a -> [Var]+  readVars :: a -> [Var] +  letVars  :: a -> [Var] +  literals :: a -> [Literal]++instance CBVisitable [CoreBind] where+  freeVars env cbs = (sortNub xs) \\ ys +    where xs = concatMap (freeVars env) cbs +          ys = concatMap bindings cbs+  +  readVars = concatMap readVars+  letVars  = concatMap letVars +  literals = concatMap literals++instance CBVisitable CoreBind where+  freeVars env (NonRec x e) = freeVars (extendEnv env [x]) e +  freeVars env (Rec xes)    = concatMap (freeVars env') es +                              where (xs,es) = unzip xes +                                    env'    = extendEnv env xs ++  readVars (NonRec _ e)     = readVars e+  readVars (Rec xes)        = concat [x `delete` nubReadVars e |(x, e) <- xes]+    where nubReadVars = sortNub . readVars++  letVars (NonRec x e)      = x : letVars e+  letVars (Rec xes)         = xs ++ concatMap letVars es+    where +      (xs, es)              = unzip xes++  literals (NonRec _ e)      = literals e+  literals (Rec xes)         = concatMap literals $ map snd xes++instance CBVisitable (Expr Var) where+  freeVars = exprFreeVars+  readVars = exprReadVars+  letVars  = exprLetVars+  literals = exprLiterals++exprFreeVars = go +  where +    go env (Var x)         = if x `S.member` env then [] else [x]  +    go env (App e a)       = (go env e) ++ (go env a)+    go env (Lam x e)       = go (extendEnv env [x]) e+    go env (Let b e)       = (freeVars env b) ++ (go (extendEnv env (bindings b)) e)+    go env (Tick _ e)      = go env e+    go env (Cast e _)      = go env e+    go env (Case e x _ cs) = (go env e) ++ (concatMap (freeVars (extendEnv env [x])) cs) +    go _   _               = []++exprReadVars = go+  where+    go (Var x)             = [x]+    go (App e a)           = concatMap go [e, a] +    go (Lam _ e)           = go e+    go (Let b e)           = readVars b ++ go e +    go (Tick _ e)          = go e+    go (Cast e _)          = go e+    go (Case e _ _ cs)     = (go e) ++ (concatMap readVars cs) +    go _                   = []++exprLetVars = go+  where+    go (Var _)             = []+    go (App e a)           = concatMap go [e, a] +    go (Lam x e)           = x : go e+    go (Let b e)           = letVars b ++ go e +    go (Tick _ e)          = go e+    go (Cast e _)          = go e+    go (Case e x _ cs)     = x : go e ++ concatMap letVars cs+    go _                   = []++exprLiterals = go+  where+    go (Lit l)             = [l]+    go (App e a)           = concatMap go [e, a] +    go (Let b e)           = literals b ++ go e +    go (Lam _ e)           = go e+    go (Tick _ e)          = go e+    go (Cast e _)          = go e+    go (Case e _ _ cs)     = (go e) ++ (concatMap literals cs) +    go _                   = []+++instance CBVisitable (Alt Var) where+  freeVars env (a, xs, e) = freeVars env a ++ freeVars (extendEnv env xs) e+  readVars (_,_, e)       = readVars e+  letVars  (_,xs,e)       = xs ++ letVars e+  literals (c,_, e)       = literals c ++ literals e+++instance CBVisitable AltCon where+  freeVars _ (DataAlt dc) = dataConImplicitIds dc+  freeVars _ _            = []+  readVars _              = []+  letVars  _              = []+  literals (LitAlt l)     = [l]+  literals _              = []++++extendEnv = foldl' (flip S.insert)++bindings (NonRec x _) +  = [x]+bindings (Rec  xes  ) +  = map fst xes

@@ -1,86 +0,0 @@-;;; flycheck-liquid.el --- A flycheck checker for Haskell using liquid (i.e. liquidhaskell)--;; Modified from flycheck-hdevtools.el by Steve Purcell--;; Author: Ranjit Jhala <jhala@cs.ucsd.edu>-;; URL: https://github.com/ucsd-progsys/liquidhaskell/flycheck-liquid.el-;; Keywords: convenience languages tools-;; Package-Requires: ((flycheck "0.15"))-;; Version: 20140801.00-;; X-Original-Version: DEV--;; This file is not part of GNU Emacs.--;; This program is free software; you can redistribute it and/or modify-;; it under the terms of the GNU General Public License as published by-;; the Free Software Foundation, either version 3 of the License, or-;; (at your option) any later version.--;; This program is distributed in the hope that it will be useful,-;; but WITHOUT ANY WARRANTY; without even the implied warranty of-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the-;; GNU General Public License for more details.--;; You should have received a copy of the GNU General Public License-;; along with this program.  If not, see <http://www.gnu.org/licenses/>.--;;; Commentary:--;; Adds a Flycheck syntax checker for Haskell based on liquid-haskell.--;;;; Setup--;; (eval-after-load 'flycheck '(require 'flycheck-liquid))--;;; Code:--(require 'flycheck)--(defvar flycheck-liquid-diffcheck nil-  "Whether to run liquid in incremental-checking mode.")--(flycheck-define-checker haskell-liquid-  "A Haskell refinement type checker using liquidhaskell.--See URL `https://github.com/ucsd-progsys/liquidhaskell'."-  :command-  ("liquid" (option-flag "--diffcheck" flycheck-liquid-diffcheck) source-inplace)-  ;; ("~/bin/Checker.hs" source-inplace)-  :error-patterns-  (-   (error line-start " " (file-name) ":" line ":" column ":"-          (message-	   (one-or-more " ") (one-or-more not-newline)-	   (zero-or-more "\n"-			 (one-or-more " ")-			 (zero-or-more not-newline)))-          line-end)--   (error line-start " " (file-name) ":" line ":" column "-" (one-or-more digit) ":"-	  (message-	   (one-or-more " ") (one-or-more not-newline)-	   (zero-or-more "\n"-			 (one-or-more " ")-			 (zero-or-more not-newline)))-          line-end)--   (error line-start " " (file-name) ":(" line "," column ")-(" (one-or-more digit) "," (one-or-more digit) "):"-	  (message-	   (one-or-more " ") (one-or-more not-newline)-	   (zero-or-more "\n"-			 (one-or-more " ")-			 (zero-or-more not-newline)))-          line-end)-   )-  :error-filter-  (lambda (errors)-    (-> errors-      flycheck-dedent-error-messages-      flycheck-sanitize-errors))-  :modes (haskell-mode literate-haskell-mode)-  :next-checkers ((warnings-only . haskell-hlint)))--(add-to-list 'flycheck-checkers 'haskell-liquid)--(provide 'flycheck-liquid)-;;; flycheck-liquid.el ends here

@@ -1,379 +0,0 @@-" Vim syntax file-"-" Modification of vims Haskell syntax file:-"   - match types using regular expression-"   - highlight toplevel functions-"   - use "syntax keyword" instead of "syntax match" where appropriate-"   - functions and types in import and module declarations are matched-"   - removed hs_highlight_more_types (just not needed anymore)-"   - enable spell checking in comments and strings only-"   - FFI highlighting-"   - QuasiQuotation-"   - top level Template Haskell slices-"   - PackageImport-"-" TODO: find out which vim versions are still supported-"-" From Original file:-" ===================-"-" Language:		    Haskell-" Maintainer:		Haskell Cafe mailinglist <haskell-cafe@haskell.org>-" Last Change:		2010 Feb 21-" Original Author:	John Williams <jrw@pobox.com>-"-" Thanks to Ryan Crumley for suggestions and John Meacham for-" pointing out bugs. Also thanks to Ian Lynagh and Donald Bruce Stewart-" for providing the inspiration for the inclusion of the handling-" of C preprocessor directives, and for pointing out a bug in the-" end-of-line comment handling.-"-" Options-assign a value to these variables to turn the option on:-"-" hs_highlight_delimiters - Highlight delimiter characters--users-"			    with a light-colored background will-"			    probably want to turn this on.-" hs_highlight_boolean - Treat True and False as keywords.-" hs_highlight_types - Treat names of primitive types as keywords.-" hs_highlight_debug - Highlight names of debugging functions.-" hs_allow_hash_operator - Don't highlight seemingly incorrect C-"			   preprocessor directives but assume them to be-"			   operators-" -" --if version < 600-  syn clear-elseif exists("b:current_syntax")-  finish-endif--"syntax sync fromstart "mmhhhh.... is this really ok to do so?-syntax sync linebreaks=15 minlines=50 maxlines=500--syn match  hsSpecialChar	contained "\\\([0-9]\+\|o[0-7]\+\|x[0-9a-fA-F]\+\|[\"\\'&\\abfnrtv]\|^[A-Z^_\[\\\]]\)"-syn match  hsSpecialChar	contained "\\\(NUL\|SOH\|STX\|ETX\|EOT\|ENQ\|ACK\|BEL\|BS\|HT\|LF\|VT\|FF\|CR\|SO\|SI\|DLE\|DC1\|DC2\|DC3\|DC4\|NAK\|SYN\|ETB\|CAN\|EM\|SUB\|ESC\|FS\|GS\|RS\|US\|SP\|DEL\)"-syn match  hsSpecialCharError	contained "\\&\|'''\+"-sy region  hsString		start=+"+  skip=+\\\\\|\\"+  end=+"+  contains=hsSpecialChar,@Spell-sy match   hsCharacter		"[^a-zA-Z0-9_']'\([^\\]\|\\[^']\+\|\\'\)'"lc=1 contains=hsSpecialChar,hsSpecialCharError-sy match   hsCharacter		"^'\([^\\]\|\\[^']\+\|\\'\)'" contains=hsSpecialChar,hsSpecialCharError--" (Qualified) identifiers (no default highlighting)-syn match ConId "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=\<[A-Z][a-zA-Z0-9_']*\>"-syn match VarId "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=\<[a-z][a-zA-Z0-9_']*\>"--" Infix operators--most punctuation characters and any (qualified) identifier-" enclosed in `backquotes`. An operator starting with : is a constructor,-" others are variables (e.g. functions).-syn match hsVarSym "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[-!#$%&\*\+/<=>\?@\\^|~.][-!#$%&\*\+/<=>\?@\\^|~:.]*"-syn match hsConSym "\(\<[A-Z][a-zA-Z0-9_']*\.\)\=:[-!#$%&\*\+./<=>\?@\\^|~:]*"-syn match hsVarSym "`\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[a-z][a-zA-Z0-9_']*`"-syn match hsConSym "`\(\<[A-Z][a-zA-Z0-9_']*\.\)\=[A-Z][a-zA-Z0-9_']*`"--" Toplevel Template Haskell support-"sy match hsTHTopLevel "^[a-z]\(\(.\&[^=]\)\|\(\n[^a-zA-Z0-9]\)\)*"-sy match hsTHIDTopLevel "^[a-z]\S*" -sy match hsTHTopLevel "^\$(\?" nextgroup=hsTHTopLevelName -sy match hsTHTopLevelName "[a-z]\S*" contained--" Reserved symbols--cannot be overloaded.-syn match hsDelimiter  "(\|)\|\[\|\]\|,\|;\|_\|{\|}"--sy region hsInnerParen start="(" end=")" contained contains=hsInnerParen,hsConSym,hsType,hsVarSym-sy region hs_InfixOpFunctionName start="^(" end=")\s*[^:`]\(\W\&\S\&[^'\"`()[\]{}@]\)\+"re=s-    \ contained keepend contains=hsInnerParen,hs_HlInfixOp--sy match hs_hlFunctionName "[a-z_]\(\S\&[^,\(\)\[\]]\)*" contained -sy match hs_FunctionName "^[a-z_]\(\S\&[^,\(\)\[\]]\)*" contained contains=hs_hlFunctionName-sy match hs_HighliteInfixFunctionName "`[a-z_][^`]*`" contained-sy match hs_InfixFunctionName "^\S[^=]*`[a-z_][^`]*`"me=e-1 contained contains=hs_HighliteInfixFunctionName,hsType,hsConSym,hsVarSym,hsString,hsCharacter-sy match hs_HlInfixOp "\(\W\&\S\&[^`(){}'[\]]\)\+" contained contains=hsString-sy match hs_InfixOpFunctionName "^\(\(\w\|[[\]{}]\)\+\|\(\".*\"\)\|\('.*'\)\)\s*[^:]=*\(\W\&\S\&[^='\"`()[\]{}@]\)\+"-    \ contained contains=hs_HlInfixOp,hsCharacter--sy match hs_OpFunctionName        "(\(\W\&[^(),\"]\)\+)" contained-"sy region hs_Function start="^["'a-z_([{]" end="=\(\s\|\n\|\w\|[([]\)" keepend extend-sy region hs_Function start="^["'a-zA-Z_([{]\(\(.\&[^=]\)\|\(\n\s\)\)*=" end="\(\s\|\n\|\w\|[([]\)" -        \ contains=hs_OpFunctionName,hs_InfixOpFunctionName,hs_InfixFunctionName,hs_FunctionName,hsType,hsConSym,hsVarSym,hsString,hsCharacter--sy match hs_TypeOp "::"-sy match hs_DeclareFunction "^[a-z_(]\S*\(\s\|\n\)*::" contains=hs_FunctionName,hs_OpFunctionName,hs_TypeOp--" hi hs_TypeOp guibg=red--" hi hs_InfixOpFunctionName guibg=yellow-" hi hs_Function guibg=green-" hi hs_InfixFunctionName guibg=red-" hi hs_DeclareFunction guibg=red--sy keyword hsStructure data family class where instance default deriving-sy keyword hsTypedef type newtype--sy keyword hsInfix infix infixl infixr-sy keyword hsStatement  do case of let in-sy keyword hsConditional if then else--"if exists("hs_highlight_types")-  " Primitive types from the standard prelude and libraries.-  sy match hsType "\<[A-Z]\(\S\&[^,.]\)*\>"-  sy match hsType "()"-"endif--" Not real keywords, but close.-if exists("hs_highlight_boolean")-  " Boolean constants from the standard prelude.-  syn keyword hsBoolean True False-endif--syn region	hsPackageString	start=+L\="+ skip=+\\\\\|\\"\|\\$+ excludenl end=+"+ end='$' contains=cSpecial contained-sy match   hsModuleName  excludenl "\([A-Z]\w*\.\?\)*" contained --sy match hsImport "\<import\>\s\+\(qualified\s\+\)\?\(\<\(\w\|\.\)*\>\)" -    \ contains=hsModuleName,hsImportLabel-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite-sy keyword hsImportLabel import qualified contained--sy match hsImportIllegal "\w\+" contained--sy keyword hsAsLabel as contained-sy keyword hsHidingLabel hiding contained--sy match hsImportParams "as\s\+\(\w\+\)" contained-    \ contains=hsModuleName,hsAsLabel-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite-sy match hsImportParams "hiding" contained-    \ contains=hsHidingLabel-    \ nextgroup=hsImportParams,hsImportIllegal skipwhite -sy region hsImportParams start="(" end=")" contained-    \ contains=hsBlockComment,hsLineComment, hsType,hsDelimTypeExport,hs_hlFunctionName,hs_OpFunctionName-    \ nextgroup=hsImportIllegal skipwhite--" hi hsImport guibg=red-"hi hsImportParams guibg=bg-"hi hsImportIllegal guibg=bg-"hi hsModuleName guibg=bg--"sy match hsImport		"\<import\>\(.\|[^(]\)*\((.*)\)\?" -"         \ contains=hsPackageString,hsImportLabel,hsImportMod,hsModuleName,hsImportList-"sy keyword hsImportLabel import contained-"sy keyword hsImportMod		as qualified hiding contained-"sy region hsImportListInner start="(" end=")" contained keepend extend contains=hs_OpFunctionName-"sy region  hsImportList matchgroup=hsImportListParens start="("rs=s+1 end=")"re=e-1-"        \ contained -"        \ keepend extend-"        \ contains=hsType,hsLineComment,hsBlockComment,hs_hlFunctionName,hsImportListInner----" new module highlighting-syn region hsDelimTypeExport start="\<[A-Z]\(\S\&[^,.]\)*\>(" end=")" contained-   \ contains=hsType--sy keyword hsExportModuleLabel module contained-sy match hsExportModule "\<module\>\(\s\|\t\|\n\)*\([A-Z]\w*\.\?\)*" contained contains=hsExportModuleLabel,hsModuleName--sy keyword hsModuleStartLabel module contained-sy keyword hsModuleWhereLabel where contained--syn match hsModuleStart "^module\(\s\|\n\)*\(\<\(\w\|\.\)*\>\)\(\s\|\n\)*" -  \ contains=hsModuleStartLabel,hsModuleName-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel--syn region hsModuleCommentA start="{-" end="-}"-  \ contains=hsModuleCommentA,hsCommentTodo,@Spell contained-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel skipwhite skipnl--syn match hsModuleCommentA "--.*\n"-  \ contains=hsCommentTodo,@Spell contained-  \ nextgroup=hsModuleCommentA,hsModuleExports,hsModuleWhereLabel skipwhite skipnl--syn region hsModuleExports start="(" end=")" contained-   \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl-   \ contains=hsBlockComment,hsLineComment,hsType,hsDelimTypeExport,hs_hlFunctionName,hs_OpFunctionName,hsExportModule--syn match hsModuleCommentB "--.*\n"-  \ contains=hsCommentTodo,@Spell contained-  \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl--syn region hsModuleCommentB start="{-" end="-}"-   \ contains=hsModuleCommentB,hsCommentTodo,@Spell contained-   \ nextgroup=hsModuleCommentB,hsModuleWhereLabel skipwhite skipnl-" end module highlighting--" FFI support-sy keyword hsFFIForeign foreign contained-"sy keyword hsFFIImportExport import export contained-sy keyword hsFFIImportExport export contained-sy keyword hsFFICallConvention ccall stdcall contained-sy keyword hsFFISafety safe unsafe contained-sy region  hsFFIString		start=+"+  skip=+\\\\\|\\"+  end=+"+  contained contains=hsSpecialChar-sy match hsFFI excludenl "\<foreign\>\(.\&[^\"]\)*\"\(.\)*\"\(\s\|\n\)*\(.\)*::"-  \ keepend-  \ contains=hsFFIForeign,hsFFIImportExport,hsFFICallConvention,hsFFISafety,hsFFIString,hs_OpFunctionName,hs_hlFunctionName---sy match   hsNumber		"\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"-sy match   hsFloat		"\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"--" Comments-sy keyword hsCommentTodo    TODO FIXME XXX TBD contained-sy match   hsLineComment      "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=hsCommentTodo,@Spell-sy region  hsBlockComment     start="{-"  end="-}" contains=hsBlockComment,hsCommentTodo,@Spell-sy region  hsPragma	       start="{-#" end="#-}"--" Liquid Types-sy region  hsLiquidAnnot   start="{-@\s*" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy region  hsLiquidAnnot   start="{-@\s*\<invariant\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy region  hsLiquidAnnot   start="{-@\s*\<predicate\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy region  hsLiquidAnnot   start="{-@\s*\<assert\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy region  hsLiquidAnnot   start="{-@\s*\<type\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy region  hsLiquidAnnot   start="{-@\s*\<data\>" end="@-}" contains=hsLiquidKeyword,hsLiquidReftA,hsLiquidReftB,hsLiquidReftC-sy keyword hsLiquidKeyword  assume assert invariant predicate type data contained-sy region  hsLiquidReftA   start="{\(\s\|\w\)" end=":" contained-sy region  hsLiquidReftB   start="|" end="}" contained-sy match   hsLiquidReftC   "\w*:" contained--" QuasiQuotation-sy region hsQQ start="\[\$" end="|\]"me=e-2 keepend contains=hsQQVarID,hsQQContent nextgroup=hsQQEnd-sy region hsQQNew start="\[\(.\&[^|]\&\S\)*|" end="|\]"me=e-2 keepend contains=hsQQVarIDNew,hsQQContent nextgroup=hsQQEnd-sy match hsQQContent ".*" contained-sy match hsQQEnd "|\]" contained-sy match hsQQVarID "\[\$\(.\&[^|]\)*|" contained-sy match hsQQVarIDNew "\[\(.\&[^|]\)*|" contained--if exists("hs_highlight_debug")-  " Debugging functions from the standard prelude.-  syn keyword hsDebug undefined error trace-endif---" C Preprocessor directives. Shamelessly ripped from c.vim and trimmed-" First, see whether to flag directive-like lines or not-if (!exists("hs_allow_hash_operator"))-    syn match	cError		display "^\s*\(%:\|#\).*$"-endif-" Accept %: for # (C99)-syn region	cPreCondit	start="^\s*\(%:\|#\)\s*\(if\|ifdef\|ifndef\|elif\)\>" skip="\\$" end="$" end="//"me=s-1 contains=cComment,cCppString,cCommentError-syn match	cPreCondit	display "^\s*\(%:\|#\)\s*\(else\|endif\)\>"-syn region	cCppOut		start="^\s*\(%:\|#\)\s*if\s\+0\+\>" end=".\@=\|$" contains=cCppOut2-syn region	cCppOut2	contained start="0" end="^\s*\(%:\|#\)\s*\(endif\>\|else\>\|elif\>\)" contains=cCppSkip-syn region	cCppSkip	contained start="^\s*\(%:\|#\)\s*\(if\>\|ifdef\>\|ifndef\>\)" skip="\\$" end="^\s*\(%:\|#\)\s*endif\>" contains=cCppSkip-syn region	cIncluded	display contained start=+"+ skip=+\\\\\|\\"+ end=+"+-syn match	cIncluded	display contained "<[^>]*>"-syn match	cInclude	display "^\s*\(%:\|#\)\s*include\>\s*["<]" contains=cIncluded-syn cluster	cPreProcGroup	contains=cPreCondit,cIncluded,cInclude,cDefine,cCppOut,cCppOut2,cCppSkip,cCommentStartError-syn region	cDefine		matchgroup=cPreCondit start="^\s*\(%:\|#\)\s*\(define\|undef\)\>" skip="\\$" end="$"-syn region	cPreProc	matchgroup=cPreCondit start="^\s*\(%:\|#\)\s*\(pragma\>\|line\>\|warning\>\|warn\>\|error\>\)" skip="\\$" end="$" keepend--syn region	cComment	matchgroup=cCommentStart start="/\*" end="\*/" contains=cCommentStartError,cSpaceError contained-syntax match	cCommentError	display "\*/" contained-syntax match	cCommentStartError display "/\*"me=e-1 contained-syn region	cCppString	start=+L\="+ skip=+\\\\\|\\"\|\\$+ excludenl end=+"+ end='$' contains=cSpecial contained---if version >= 508 || !exists("did_hs_syntax_inits")-  if version < 508-    let did_hs_syntax_inits = 1-    command -nargs=+ HiLink hi link <args>-  else-    command -nargs=+ HiLink hi def link <args>-  endif--  HiLink hs_hlFunctionName    Function-  HiLink hs_HighliteInfixFunctionName Function-  HiLink hs_HlInfixOp       Function-  HiLink hs_OpFunctionName  Function-  HiLink hsTypedef          Typedef-  HiLink hsVarSym           hsOperator-  HiLink hsConSym           hsOperator-  if exists("hs_highlight_delimiters")-    " Some people find this highlighting distracting.-	HiLink hsDelimiter        Delimiter-  endif--  HiLink hsModuleStartLabel Structure-  HiLink hsExportModuleLabel Keyword-  HiLink hsModuleWhereLabel Structure-  HiLink hsModuleName       Normal-  -  HiLink hsImportIllegal    Error-  HiLink hsAsLabel          hsImportLabel-  HiLink hsHidingLabel      hsImportLabel-  HiLink hsImportLabel      Include-  HiLink hsImportMod        Include-  HiLink hsPackageString    hsString--  HiLink hsOperator         Operator--  HiLink hsInfix            Keyword-  HiLink hsStructure        Structure-  HiLink hsStatement        Statement-  HiLink hsConditional      Conditional--  HiLink hsSpecialCharError Error-  HiLink hsSpecialChar      SpecialChar-  HiLink hsString           String-  HiLink hsFFIString        String-  HiLink hsCharacter        Character-  HiLink hsNumber           Number-  HiLink hsFloat            Float--  HiLink hsLiterateComment		  hsComment-  HiLink hsBlockComment     hsComment-  HiLink hsLineComment      hsComment-  HiLink hsModuleCommentA   hsComment-  HiLink hsModuleCommentB   hsComment-  HiLink hsComment          Comment-  HiLink hsCommentTodo      Todo-  HiLink hsPragma           SpecialComment-  HiLink hsBoolean			Boolean--  " Liquid Types-  HiLink hsLiquidAnnot      SpecialComment  "String-  HiLink hsLiquidKeyword    Operator        "Float-  HiLink hsLiquidReftA      Include-  HiLink hsLiquidReftB      Include-  HiLink hsLiquidReftC      Include-  -  if exists("hs_highlight_types")-      HiLink hsDelimTypeExport  hsType-      HiLink hsType             Type-  endif--  HiLink hsDebug            Debug--  HiLink hs_TypeOp          hsOperator--  HiLink cCppString         hsString-  HiLink cCommentStart      hsComment-  HiLink cCommentError      hsError-  HiLink cCommentStartError hsError-  HiLink cInclude           Include-  HiLink cPreProc           PreProc-  HiLink cDefine            Macro-  HiLink cIncluded          hsString-  HiLink cError             Error-  HiLink cPreCondit         PreCondit-  HiLink cComment           Comment-  HiLink cCppSkip           cCppOut-  HiLink cCppOut2           cCppOut-  HiLink cCppOut            Comment--  HiLink hsFFIForeign       Keyword-  HiLink hsFFIImportExport  Structure-  HiLink hsFFICallConvention Keyword-  HiLink hsFFISafety         Keyword--  HiLink hsTHIDTopLevel   Macro-  HiLink hsTHTopLevelName Macro--  HiLink hsQQVarID Keyword-  HiLink hsQQVarIDNew Keyword-  HiLink hsQQEnd   Keyword-  HiLink hsQQContent String--  delcommand HiLink-endif--let b:current_syntax = "haskell"-

@@ -1,270 +0,0 @@-;;; liquid-tip.el --- show inferred liquid-types--;; Copyright (C) 2014 by Ranjit Jhala --;; Author: Ranjit Jhala <jhala@cs.ucsd.edu>-;; Version: 0.0.1-;; Package-Requires: ((flycheck "0.13") (dash "1.2") (emacs "24.1") (pos-tip "0.5.0"))-;;; License:-;; This program is free software: you can redistribute it and/or modify-;; it under the terms of the GNU General Public License as published by-;; the Free Software Foundation, either version 3 of the License, or-;; (at your option) any later version.-;;-;; This program is distributed in the hope that it will be useful,-;; but WITHOUT ANY WARRANTY; without even the implied warranty of-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the-;; GNU General Public License for more details.-;;-;; You should have received a copy of the GNU General Public License-;; along with this program.  If not, see <http://www.gnu.org/licenses/>.--;;; Commentary:-;; see https://github.com/ucsd-progsys/liquidhaskell#emacs--;;; Code:-(eval-when-compile (require 'cl))-(require 'auto-complete)-(require 'json)-(require 'pos-tip nil t)-(require 'thingatpt)-(require 'button-lock)-(require 'hdevtools)--;; -------------------------------------------------------------------------;; A structure to represent positions -;; --------------------------------------------------------------------------(cl-defstruct position file row col)--;; -------------------------------------------------------------------------;; Utilities for reading json/files-;; --------------------------------------------------------------------------(defun get-string-from-file (filePath)-  "Return filePath's file content."-  (with-temp-buffer-    (insert-file-contents filePath)-    (buffer-string)))--(defun get-json-from-file (filePath)-  "Return json object from filePath's content"-  (if (file-exists-p filePath)-      (let* ((json-key-type 'string)-	     (str (get-string-from-file filePath)))-	(json-read-from-string str))-      nil))--;; -------------------------------------------------------------------------;; get/set annot information -;; --------------------------------------------------------------------------(defun gethash-nil (key table) -  (if table -      (gethash key table nil)-      nil))--(defun liquid-annot-filepath-prefix (mode)-  "Return prefix of annotation file using mode"-  (if (equal mode 'flycheck)-      "flycheck_"-      nil))--;; (liquid-annot 'flycheck "/path/to/file.hs") -;;    ==> "/path/to/.liquid/flycheck_file.hs.json"-;;-;; (liquid-annot nil       "/path/to/file.hs") -;;    ==> "/path/to/.liquid/file.hs.json"--(defun liquid-annot-filepath (mode file)-  "Return name of annotation file"-  (let* ((dir    (file-name-directory file))-	 (name   (file-name-nondirectory file))-	 (prefix (liquid-annot-filepath-prefix mode)))-    (concat dir ".liquid/" prefix name ".json")))--(defvar liquid-annot-table (make-hash-table :test 'equal))--;; API-(defun liquid-annot-set (file mode)-  "Load information for file into liquid-annot-table"-  (let* ((file-path        (liquid-annot-filepath mode file))-	 (json-object-type 'hash-table)-	 (file-info        (get-json-from-file file-path)))-    (if file-info (puthash file file-info liquid-annot-table))))--;; API-(defun liquid-annot-get (file row col)-  "Get annotation for identifier at row, col in file"-  (let* ((table (gethash-nil file liquid-annot-table))-	 (r     (format "%d" row))-	 (c     (format "%d" col))-	 (tys   (gethash-nil "types" table))-	 (ro    (gethash-nil r tys)))-    (gethash-nil "ann" (gethash-nil c ro))))--;; -------------------------------------------------------------------------;; Display Annot in Tooltip -;; --------------------------------------------------------------------------;; For simple, ascii popups, use:-;;    (setq liquid-tip-mode 'ascii) -;;-;; For emacs', balloon based popups, use:-;;    (setq liquid-tip-mode 'balloon)--(defvar liquid-tip-mode 'balloon)--(defun pad-line (str)-  (concat " " str " "))--(defun popup-tip-pad (text)-  (let* ((lines     (split-string text "\n"))-         (pad-lines (mapcar 'pad-line lines))-	 (pad-text  (concat "\n" (mapconcat 'identity pad-lines "\n") "\n")))-    (popup-tip pad-text)))--(defun liquid-tip-popup-balloon (text)-  "Display text in a balloon popup"-  (if (and (functionp 'ac-quick-help-use-pos-tip-p)-           (ac-quick-help-use-pos-tip-p))-      (pos-tip-show text 'popup-tip-face nil nil 300 popup-tip-max-width)-    (popup-tip-pad text)))--(defun liquid-tip-popup-ascii (text)- "Display text in ascii popup"-  (popup-tip-pad text))--(defun liquid-tip-popup (text)-  (if (equal liquid-tip-mode 'ascii)-      (liquid-tip-popup-ascii   text)-      (liquid-tip-popup-balloon text)))--;; -- Compute range -----------------------------------------------------------(defvar liquid-id-regexp -  (rx (one-or-more (not (in " \n\t()[]{}")))))--(defun liquid-splitters () -  '( ?\s  ?\t ?\n ?\( ?\) ?\[ ?\] ))--(defun liquid-is-split (c)-  "Is the character `c` a splitter?"-  (member c (liquid-splitters)))--(defun liquid-id-start-pos (low p)-  "Find the largest position less than `p` that is a splitter"-  (let* ((ch (char-before p)))-     (if (or (<= p low) (liquid-is-split ch)) -	 p -         (liquid-id-start-pos low (- p 1)))))---(defun column-number-at-pos (pos)-  "Find the column of position pos"-  (+ (- pos (line-beginning-position)) 1))--(defun start-column-number-at-pos (pos)-  "Find the starting column of identifier at pos"-     (let* ((low   (line-beginning-position))-	    (start (liquid-id-start-pos low pos)))-       (column-number-at-pos start)))--(defsubst liquid-get-position ()-  (save-excursion-    (widen)-    (make-position-     :file (expand-file-name (buffer-file-name))-     :row  (line-number-at-pos)-     :col  (start-column-number-at-pos (point)))))--(defun position-string (pos)-  "position -> string"-  (format "(%s, %s) in [%s]" -	  (position-row pos) -	  (position-col pos)-	  (position-file pos)))--;; DEBUG (defun liquid-annot-at-pos-0 (pos)-;; DEBUG   "Info to display: just the file/line/constant string"-;; DEBUG   (let* ((info  (format "hello!")))-;; DEBUG     (format "the information at %s is %s" -;; DEBUG 	    (position-string pos)-;; DEBUG 	    info)))--;; DEBUG (defun liquid-annot-at-pos-1 (pos)-;; DEBUG   "Info to display: the identifier at the position or NONE" -;; DEBUG   (let* ((ident (liquid-ident-at-pos pos)))-;; DEBUG     (format "the identifier at %s is %s" -;; DEBUG 	    (position-string pos) -;; DEBUG 	    ident)))--(defun liquid-ident-at-pos (pos)-  "Return the identifier at a given position"-  (thing-at-point 'word))--(defun liquid-annot-at-pos-2 (pos)-  "Info to display: type annotation for the identifier at the position or NONE" -  (let* ((file (position-file pos))-	 (row  (position-row  pos))-	 (col  (position-col  pos)))-    (liquid-annot-get file row col)))--(defun liquid-annot-at-pos (pos)-  "Determine info to display"-  (liquid-annot-at-pos-2 pos))--;;;###autoload-(defun liquid-tip-show ()-  "Popup help about anything at point."-  (interactive)-  (let* ((pos    (liquid-get-position))-         (ident  (liquid-ident-at-pos pos))-         (sorry  (format "No information for %s" ident))-         (annot  (liquid-annot-at-pos pos)))-    (if annot -        (liquid-tip-popup annot)-      (hdevtools/show-type-info)-      ;; (liquid-tip-popup sorry)-      )))---;;;###autoload-(defun liquid-tip-init (&optional mode)-  "Initialize liquid-tip by making all identifiers buttons"-  (interactive)-  (progn (if mode (setq liquid-tip-mode mode))-	 (button-lock-mode 1)-	 (button-lock-set-button liquid-id-regexp 'liquid-tip-show :mouse-face nil :face nil :face-policy nil :mouse-binding 'double-mouse-1)-	 ))--;;;###autoload-(defun liquid-tip-update (mode)-  "Update liquid-annot-table by reloading annot file for buffer"-  (interactive)-  (let* ((pos  (liquid-get-position))-	 (file (position-file pos)))-    (liquid-annot-set file mode)))---;; For simple, ascii popups, use:-;;    (liquid-tip-init 'ascii) -;; For emacs', balloon based popups, use:-;;    (liquid-tip-init 'balloon)-;; or just-;;    (liquid-tip-init 'balloon)--;; Reload annotations after check-(add-hook 'flycheck-after-syntax-check-hook-	  (lambda () (liquid-tip-update 'flycheck)))----(provide 'liquid-tip)--;; Local Variables:-;; coding: utf-8-;; mode: emacs-lisp-;; End:--;;; liquid-tip.el ends here

@@ -1,47 +0,0 @@-"============================================================================-"File:        liquid.vim-"Description: LiquidHaskell checking plugin for syntastic.vim-"Maintainer:  Ranjit Jhala <jhala at cs dot ucsd dot edu>-"License:     BSD-"============================================================================--if exists('g:loaded_syntastic_haskell_liquid_checker')-    finish-endif-let g:loaded_syntastic_haskell_liquid_checker = 1---let s:save_cpo = &cpo-set cpo&vim--function! SyntaxCheckers_haskell_liquid_GetLocList() dict-    let makeprg = self.makeprgBuild({-        \ 'fname'    : syntastic#util#shexpand('%:p')})--    let errorformat =-        \ '%E%f:%l:%v: Error: %m,' .-        \ '%E%f:%l:%c-%*[0-9]: Error: %m,' .-        \ '%W%f:%l:%v: Warning: %m,' .-        \ '%C%m'--    let retVals = SyntasticMake({-        \ 'makeprg': makeprg,-        \ 'errorformat': errorformat,-        \ 'defaults': {'vcol': 1},-        \ 'postprocess': ['compressWhitespace'] })--    if exists("g:loaded_vim_annotations")-      call annotations#LoadAnnsDefault()-    endif--    return retVals-endfunction--call g:SyntasticRegistry.CreateAndRegisterChecker({-    \ 'filetype': 'haskell',-    \ 'name': 'liquid'})--let &cpo = s:save_cpo-unlet s:save_cpo--" vim: set et sts=4 sw=4:

@@ -51,9 +51,8 @@       testGroup "pos"         <$> dirTests "tests/pos"                            []           ExitSuccess     , testGroup "neg"         <$> dirTests "tests/neg"                            []           (ExitFailure 1)     , testGroup "crash"       <$> dirTests "tests/crash"                          []           (ExitFailure 2) -    , testGroup "parserpos"   <$> dirTests "tests/parser/pos"                    []           ExitSuccess-    , testGroup "errorcrash"  <$> dirTests "tests/error_messages/crash"           []           (ExitFailure 2)-    , testGroup "errorpos"    <$> dirTests "tests/parser/pos"                     []           ExitSuccess+    , testGroup "parser/pos"  <$> dirTests "tests/parser/pos"                     []           ExitSuccess+    , testGroup "error/crash" <$> dirTests "tests/error_messages/crash"           []           (ExitFailure 2)    ]  benchTests@@ -63,7 +62,8 @@     , testGroup "esop"        <$> dirTests "benchmarks/esop2013-submission"       ["Base0.hs"] ExitSuccess     , testGroup "vect-algs"   <$> dirTests "benchmarks/vector-algorithms-0.5.4.2" []           ExitSuccess     , testGroup "hscolour"    <$> dirTests "benchmarks/hscolour-1.20.0.0"         []           ExitSuccess-+    , testGroup "icfp_pos"    <$> dirTests "benchmarks/icfp15/pos"                []           ExitSuccess+    , testGroup "icfp_neg"    <$> dirTests "benchmarks/icfp15/neg"                ["RIO.hs", "DataBase.hs", "DataBase.Domain.hs"]           (ExitFailure 1)     ]  ---------------------------------------------------------------------------