liquidhaskell 0.2.0.0 → 0.2.1.0
raw patch · 30 files changed
+1815/−591 lines, 30 filesdep −unixdep ~liquid-fixpointdep ~optparse-applicativedep ~tasty
Dependencies removed: unix
Dependency ranges changed: liquid-fixpoint, optparse-applicative, tasty, tasty-hunit
Files
- LICENSE +28/−22
- Liquid.hs +7/−5
- include/Data/Set.spec +7/−3
- include/Data/Vector.spec +6/−5
- include/GHC/Real.spec +6/−7
- include/Language/Haskell/Liquid/List.hs +0/−1
- liquidhaskell.cabal +11/−10
- src/Language/Haskell/Liquid/Annotate.hs +3/−2
- src/Language/Haskell/Liquid/Bare.hs +229/−111
- src/Language/Haskell/Liquid/CmdLine.hs +150/−119
- src/Language/Haskell/Liquid/Constraint.hs +69/−54
- src/Language/Haskell/Liquid/CoreToLogic.hs +171/−0
- src/Language/Haskell/Liquid/Errors.hs +13/−0
- src/Language/Haskell/Liquid/Fresh.hs +6/−0
- src/Language/Haskell/Liquid/GhcInterface.hs +10/−6
- src/Language/Haskell/Liquid/GhcMisc.hs +9/−2
- src/Language/Haskell/Liquid/Measure.hs +16/−2
- src/Language/Haskell/Liquid/Misc.hs +11/−3
- src/Language/Haskell/Liquid/Parse.hs +25/−14
- src/Language/Haskell/Liquid/PredType.hs +0/−11
- src/Language/Haskell/Liquid/PrettyPrint.hs +11/−13
- src/Language/Haskell/Liquid/RefType.hs +26/−83
- src/Language/Haskell/Liquid/Tidy.hs +0/−2
- src/Language/Haskell/Liquid/TransformRec.hs +33/−2
- src/Language/Haskell/Liquid/Types.hs +131/−69
- syntax/flycheck-liquid.el +86/−0
- syntax/haskell.vim +379/−0
- syntax/liquid-tip.el +281/−0
- syntax/liquid.vim +47/−0
- tests/test.hs +44/−45
LICENSE view
@@ -1,24 +1,30 @@-(*- * Copyright © 1990-2009 The Regents of the University of California. All rights reserved. - *- * Permission is hereby granted, without written agreement and without - * license or royalty fees, to use, copy, modify, and distribute this - * software and its documentation for any purpose, provided that the - * above copyright notice and the following two paragraphs appear in - * all copies of this software. - * - * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY - * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES - * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN - * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY - * OF SUCH DAMAGE. - * - * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, - * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY - * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS - * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION - * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.- *- *)+Copyright (c) 2013-2014, Ranjit Jhala +All rights reserved. +Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Ranjit Jhala nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Liquid.hs view
@@ -25,9 +25,11 @@ import Language.Haskell.Liquid.Annotate (mkOutput) main :: IO b-main = do cfg0 <- getOpts- res <- mconcat <$> mapM (checkOne cfg0) (files cfg0)- exitWith $ resultExit $ o_result res+main = do cfg0 <- getOpts+ res <- mconcat <$> mapM (checkOne cfg0) (files cfg0)+ let ecode = resultExit $ {- traceShow "RESULT" $ -} o_result res+ -- putStrLn $ "ExitCode: " ++ show ecode+ exitWith ecode checkOne :: Config -> FilePath -> IO (Output Doc) checkOne cfg0 t = getGhcInfo cfg0 t >>= either errOut (liquidOne t)@@ -81,11 +83,11 @@ solveCs cfg target cgi info dc = do (r, sol) <- solve fx target (hqFiles info) (cgInfoFInfo cgi) let names = checkedNames dc- let warns = logWarn cgi+ let warns = logErrors cgi let annm = annotMap cgi let res = ferr sol r let out0 = mkOutput cfg res sol annm- return $ out0 { o_vars = names } { o_warns = warns} { o_result = res }+ return $ out0 { o_vars = names } { o_errors = warns} { o_result = res } where fx = def { FC.solver = smtsolver cfg, FC.real = real cfg } ferr s r = fmap (tidyError s) $ result $ sinfo <$> r
include/Data/Set.spec view
@@ -13,13 +13,17 @@ measure Set_cap :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a) -- | difference-measure Set_dif :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)+measure Set_dif :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a) -- | singleton-measure Set_sng :: a -> (Data.Set.Set a)+measure Set_sng :: a -> (Data.Set.Set a) -- | emptiness test-measure Set_emp :: (Data.Set.Set a) -> Prop+measure Set_emp :: (Data.Set.Set a) -> Prop++-- | empty set +measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Set a)+ -- | membership test measure Set_mem :: a -> (Data.Set.Set a) -> Prop
include/Data/Vector.spec view
@@ -3,12 +3,13 @@ import GHC.Base measure vlen :: forall a. (Data.Vector.Vector a) -> Int--- measure vlen :: forall a. a -> Int -invariant {v: Data.Vector.Vector a | (vlen v) >= 0 } +invariant {v: Data.Vector.Vector a | 0 <= vlen v } -assume ! :: forall a. x:(Data.Vector.Vector a) -> vec:{v: Int | ((0 <= v) && (v < (vlen x))) } -> a +assume ! :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a -assume fromList :: forall a. x:[a] -> {v: Data.Vector.Vector a | (vlen v) = (len x) }+assume fromList :: forall a. x:[a] -> {v: Data.Vector.Vector a | vlen v = len x } -assume length :: forall a. x:(Data.Vector.Vector a) -> {v: Int | (v = (vlen x) && v >= 0) }+assume length :: forall a. x:(Data.Vector.Vector a) -> {v : Nat | v = vlen x }++assume replicate :: n:Nat -> a -> {v:Data.Vector.Vector a | vlen v = n}
include/GHC/Real.spec view
@@ -3,19 +3,18 @@ GHC.Real.fromIntegral :: (GHC.Real.Integral a, GHC.Num.Num b) => x:a -> {v:b|v=x} - class (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where- GHC.Real.quot :: a -> a -> a- GHC.Real.rem :: a -> a -> a- GHC.Real.mod :: x:a -> y:a -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}- GHC.Real.div :: x:a -> y:a -> {v:a | ((v = (x / y))+ GHC.Real.quot :: a -> {v:a | v /= 0} -> a+ GHC.Real.rem :: a -> {v:a | v /= 0} -> a+ GHC.Real.mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}+ GHC.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v = (x / y)) && (((x>=0) && (y>=0)) => (v>=0)) && (((x>=0) && (y>=1)) => (v<=x))) }- GHC.Real.quotRem :: x:a -> y:a -> ({v:a | ((v = (x / y))+ GHC.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ({v:a | ((v = (x / y)) && (((x>=0) && (y>=0)) => (v>=0)) && (((x>=0) && (y>=1)) => (v<=x)))} ,{v:a | ((v >= 0) && (v < y))})- GHC.Real.divMod :: a -> a -> (a, a)+ GHC.Real.divMod :: a -> {v:a | v /= 0} -> (a, a) GHC.Real.toInteger :: x:a -> {v:GHC.Integer.Type.Integer | v = x} -- fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
include/Language/Haskell/Liquid/List.hs view
@@ -2,7 +2,6 @@ import Data.List hiding (transpose) -{-# ANN transpose "forall a. n:Int -> xs:[{v:[a]|len(v) = n}] -> {v:[[a]] | len(v) = n}" #-} transpose :: Int -> [[a]] -> [[a]] transpose n [] = [] transpose n ([] : xss) = transpose n xss
liquidhaskell.cabal view
@@ -1,11 +1,11 @@ Name: liquidhaskell-Version: 0.2.0.0-Copyright: 2010-13 Ranjit Jhala, University of California, San Diego.+Version: 0.2.1.0+Copyright: 2010-15 Ranjit Jhala, University of California, San Diego. build-type: Simple Synopsis: Liquid Types for Haskell Description: Liquid Types for Haskell. Homepage: http://goto.ucsd.edu/liquidhaskell-License: GPL+License: BSD3 License-file: LICENSE Author: Ranjit Jhala, Niki Vazou, Eric Seidel Maintainer: Ranjit Jhala <jhala@cs.ucsd.edu>@@ -32,6 +32,8 @@ , include/Language/Haskell/Liquid/*.pred , include/System/*.spec , syntax/liquid.css+ , syntax/*.el+ , syntax/*.vim Source-Repository head Type: git@@ -65,7 +67,7 @@ , syb , text , vector- , liquid-fixpoint >= 0.2+ , liquid-fixpoint >= 0.2.1.0 , hashable , unordered-containers , aeson@@ -139,12 +141,11 @@ , process , syb , text- , unix , intern , vector , hashable , unordered-containers- , liquid-fixpoint >= 0.2+ , liquid-fixpoint >= 0.2.1.0 , aeson , bytestring , fingertree@@ -172,6 +173,7 @@ Language.Haskell.Liquid.CmdLine, Language.Haskell.Liquid.GhcMisc, Language.Haskell.Liquid.Misc, + Language.Haskell.Liquid.CoreToLogic, Language.Haskell.Liquid.Qualifier, Language.Haskell.Liquid.TransformRec, Language.Haskell.Liquid.Tidy, @@ -211,9 +213,8 @@ filepath, process, tagged,- unix, liquidhaskell,- optparse-applicative < 0.10,- tasty >= 0.8,- tasty-hunit >= 0.8,+ optparse-applicative == 0.11.*,+ tasty >= 0.10,+ tasty-hunit >= 0.9, tasty-rerun >= 1.1
src/Language/Haskell/Liquid/Annotate.hs view
@@ -64,7 +64,7 @@ -------------------------------------------------------------------------------------------- mkOutput cfg res sol anna = O { o_vars = Nothing- , o_warns = []+ , o_errors = [] , o_types = toDoc <$> annTy , o_templs = toDoc <$> annTmpl , o_bots = mkBots annTy @@ -85,7 +85,7 @@ generateHtml srcF tyHtmlF typAnnMap writeFile vimF $ vimAnnot cfg annTyp B.writeFile jsonF $ encode typAnnMap- forM_ bots (printf "WARNING: Found false in %s\n" . showPpr)+ when showWarns $ forM_ bots (printf "WARNING: Found false in %s\n" . showPpr) where tplAnnMap = mkAnnMap cfg result annTpl typAnnMap = mkAnnMap cfg result annTyp@@ -98,6 +98,7 @@ annF = extFileName Annot srcF jsonF = extFileName Json srcF vimF = extFileName Vim srcF+ showWarns = not $ nowarnings cfg mkBots (AI m) = [ src | (src, (Just _, t) : _) <- sortBy (compare `on` fst) $ M.toList m , isFalse (rTypeReft t) ]
src/Language/Haskell/Liquid/Bare.hs view
@@ -8,6 +8,7 @@ {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE LambdaCase #-} -- | This module contains the functions that convert /from/ descriptions of -- symbols, names and types (over freshly parsed /bare/ Strings),@@ -31,7 +32,7 @@ import PrelNames import PrelInfo (wiredInThings) import Type (expandTypeSynonyms, splitFunTy_maybe)-import DataCon (dataConWorkId, dataConStupidTheta)+import DataCon (dataConWorkId, dataConStupidTheta, dataConName) import TyCon (SynTyConRhs(SynonymTyCon)) import HscMain import TysWiredIn@@ -42,7 +43,8 @@ import Data.Char (isLower, isUpper) import Text.Printf -- import Data.Maybe (listToMaybe, fromMaybe, mapMaybe, catMaybes, isNothing, fromJust)-import Control.Monad.State (get, gets, modify, State, evalState, evalStateT, execState, StateT)+import Control.DeepSeq (force)+import Control.Monad.State (get, gets, modify, put, State, evalState, evalStateT, execState, execStateT, StateT) import Data.Traversable (forM) import Control.Applicative ((<$>), (<*>), (<|>)) import Control.Monad.Reader hiding (forM)@@ -63,9 +65,10 @@ import Language.Haskell.Liquid.GhcMisc hiding (L) import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types-import Language.Haskell.Liquid.RefType+import Language.Haskell.Liquid.RefType hiding (freeTyVars) import Language.Haskell.Liquid.Errors import Language.Haskell.Liquid.PredType hiding (unify)+import Language.Haskell.Liquid.CoreToLogic import qualified Language.Haskell.Liquid.Measure as Ms @@ -88,7 +91,7 @@ = throwOr (throwOr return . checkGhcSpec specs . postProcess cbs) =<< execBare act initEnv where- act = makeGhcSpec' cfg vars defVars exports specs+ act = makeGhcSpec' cfg cbs vars defVars exports specs throwOr = either Ex.throw initEnv = BE name mempty mempty mempty env @@ -100,16 +103,16 @@ -------------------------------------------------------------------------------------------------makeGhcSpec' :: Config -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec+makeGhcSpec' :: Config -> [CoreBind] -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec -------------------------------------------------------------------------------------------------makeGhcSpec' cfg vars defVars exports specs+makeGhcSpec' cfg cbs vars defVars exports specs = do name <- gets modName _ <- makeRTEnv specs- (tycons, datacons, dcSelectors, tyi) <- makeGhcSpecCHOP1 specs+ (tycons, datacons, dcSs, tyi, embs) <- makeGhcSpecCHOP1 specs modify $ \be -> be { tcEnv = tyi } (cls, mts) <- second mconcat . unzip . mconcat <$> mapM (makeClasses cfg vars) specs- (invs, ialias, embs, sigs, asms) <- makeGhcSpecCHOP2 cfg vars defVars specs name cls mts - (measures, cms', ms', cs', xs') <- makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs+ (invs, ialias, sigs, asms) <- makeGhcSpecCHOP2 cfg vars defVars specs name cls mts embs+ (measures, cms', ms', cs', xs') <- makeGhcSpecCHOP3 cfg cbs vars specs dcSs datacons cls embs syms <- makeSymbols (vars ++ map fst cs') xs' (sigs ++ asms ++ cs') ms' (invs ++ (snd <$> ialias)) let su = mkSubst [ (x, mkVarExpr v) | (x, v) <- syms] return (emptySpec cfg)@@ -122,6 +125,7 @@ emptySpec :: Config -> GhcSpec emptySpec cfg = SP [] [] [] [] [] [] [] [] [] mempty [] [] [] [] mempty mempty cfg mempty [] mempty + makeGhcSpec0 cfg defVars exports name sp = do targetVars <- makeTargetVars name defVars $ binders cfg return $ sp { config = cfg @@ -129,13 +133,18 @@ , tgtVars = targetVars } makeGhcSpec1 vars embs tyi exports name sigs asms cs' ms' cms' su sp- = return $ sp { tySigs = makePluggedSigs name embs tyi exports $ tx sigs - , asmSigs = renameTyVars <$> tx asms- , ctors = tx cs'- , meas = tx $ ms' ++ varMeasures vars ++ cms' }+ = do tySigs <- makePluggedSigs name embs tyi exports $ tx sigs+ asmSigs <- makePluggedAsmSigs embs tyi $ tx asms+ ctors <- makePluggedAsmSigs embs tyi $ tx cs'+ return $ sp { tySigs = tySigs+ , asmSigs = asmSigs+ , ctors = ctors+ , meas = tx' $ tx $ ms' ++ varMeasures vars ++ cms' } where tx = fmap . mapSnd . subst $ su+ tx' = fmap (mapSnd $ fmap uRType) + makeGhcSpec2 invs ialias measures su sp = return $ sp { invariants = subst su invs , ialiases = subst su ialias @@ -154,39 +163,43 @@ texprs' <- mconcat <$> mapM (makeTExpr defVars) specs lazies <- mkThing makeLazy lvars' <- mkThing makeLVar+ hmeas <- mkThing makeHMeas quals <- mconcat <$> mapM makeQualifiers specs return $ sp { qualifiers = subst su quals , decr = decr' , texprs = texprs' , lvars = lvars'- , lazy = lazies } + , lazy = lazies + , tySigs = strengthenHaskellMeasures hmeas ++ tySigs sp} where mkThing mk = S.fromList . mconcat <$> sequence [ mk defVars (m, s) | (m, s) <- specs, m == name ] makeGhcSpecCHOP1 specs = do (tcs, dcs) <- mconcat <$> mapM makeConTypes specs let tycons = tcs ++ wiredTyCons - let datacons = mapSnd val <$> (concat dcs ++ wiredDataCons)- let dcSelectors = concat $ map makeMeasureSelectors (concat dcs) let tyi = makeTyConInfo tycons- return $ (tycons, datacons, dcSelectors, tyi) + embs <- mconcat <$> mapM makeTyConEmbeds specs+ datacons <- makePluggedDataCons embs tyi (concat dcs ++ wiredDataCons)+ let dcSelectors = concat $ map makeMeasureSelectors datacons+ return $ (tycons, second val <$> datacons, dcSelectors, tyi, embs) -makeGhcSpecCHOP2 cfg vars defVars specs name cls mts+makeGhcSpecCHOP2 cfg vars defVars specs name cls mts embs = do sigs' <- mconcat <$> mapM (makeAssertSpec name cfg vars defVars) specs asms' <- mconcat <$> mapM (makeAssumeSpec name cfg vars defVars) specs invs <- mconcat <$> mapM makeInvariants specs ialias <- mconcat <$> mapM makeIAliases specs- embs <- mconcat <$> mapM makeTyConEmbeds specs let dms = makeDefaultMethods vars mts tyi <- gets tcEnv let sigs = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- sigs' ++ mts ++ dms ] let asms = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- asms' ]- return (invs, ialias, embs, sigs, asms)+ return (invs, ialias, sigs, asms) -makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs+makeGhcSpecCHOP3 cfg cbs vars specs dcSelectors datacons cls embs = do measures' <- mconcat <$> mapM makeMeasureSpec specs- tyi <- gets tcEnv - let measures = measures' `mappend` Ms.mkMSpec' dcSelectors+ tyi <- gets tcEnv+ name <- gets modName + hmeans <- mapM (makeHaskellMeasures cbs name) specs+ let measures = mconcat (measures':Ms.mkMSpec' dcSelectors:hmeans) let (cs, ms) = makeMeasureSpec' measures let cms = makeClassMeasureSpec measures let cms' = [ (x, Loc l $ cSort t) | (Loc l x, t) <- cms ]@@ -195,6 +208,41 @@ let xs' = val . fst <$> ms return (measures, cms', ms', cs', xs') +makeHaskellMeasures :: [CoreBind] -> ModName -> (ModName, Ms.BareSpec) -> BareM (Ms.MSpec SpecType DataCon)+makeHaskellMeasures cbs name' (name, spec) | name /= name' = return mempty+makeHaskellMeasures cbs _ (name, spec) = Ms.mkMSpec' <$> mapM (makeMeasureDefinition cbs) (S.toList $ Ms.hmeas spec)++makeMeasureDefinition :: [CoreBind] -> LocSymbol -> BareM (Measure SpecType DataCon)+makeMeasureDefinition cbs x + = case (filter ((val x `elem`) . (map (dropModuleNames . simplesymbol)) . binders) cbs) of+ (NonRec v def:_) -> (Ms.mkM x (ofType $ varType v)) <$> coreToDef' x v def+ (Rec [(v, def)]:_) -> (Ms.mkM x (ofType $ varType v)) <$> coreToDef' x v def+ _ -> mkError "Cannot extract measure from haskell function"+ where+ binders (NonRec x _) = [x]+ binders (Rec xes) = fst <$> xes ++ coreToDef' x v def = case (runToLogic $ coreToDef x v def) of + Left x -> return x+ Right (LE str) -> mkError str++ mkError str = throwError $ ErrHMeas (sourcePosSrcSpan $ loc x) (val x) (text str) ++simplesymbol = symbol . getName+++strengthenHaskellMeasures :: S.HashSet Var -> [(Var, Located SpecType)]+strengthenHaskellMeasures hmeas = (\v -> (v, dummyLoc $ strengthenResult v)) <$> (S.toList hmeas)++strengthenResult :: Var -> SpecType+strengthenResult v+ = fromRTypeRep $ rep{ty_res = ty_res rep `strengthen` r}+ where rep = toRTypeRep t+ r = U (exprReft (EApp f [EVar x])) mempty mempty+ x = safeHead "strengthenResult" $ ty_binds rep+ f = dummyLoc $ dropModuleNames $ simplesymbol v+ t = (ofType $ varType v) :: SpecType+ makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon] makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = go <$> zip (reverse xts) [1..] where@@ -203,15 +251,30 @@ dty t = foldr RAllT (RFun dummySymbol r (fmap mempty t) mempty) vs n = length xts - makePluggedSigs name embs tcEnv exports sigs- = [ (x, plugHoles embs tcEnv x r τ t)- | (x, t) <- sigs- , let τ = expandTypeSynonyms $ varType x- , let r = maybeTrue x name exports- ]+ = forM sigs $ \(x,t) -> do+ let τ = expandTypeSynonyms $ varType x+ let r = maybeTrue x name exports+ (x,) <$> plugHoles embs tcEnv x r τ t +makePluggedAsmSigs embs tcEnv sigs+ = forM sigs $ \(x,t) -> do+ let τ = expandTypeSynonyms $ varType x+ let r = killHoles+ (x,) <$> plugHoles embs tcEnv x r τ t +makePluggedDataCons embs tcEnv dcs+ = forM dcs $ \(dc, Loc l dcp) -> do+ let (das, _, dts, dt) = dataConSig dc+ let su = zip (freeTyVars dcp) (map rTyVar das)+ tyArgs <- zipWithM (\t1 (x,t2) -> + (x,) . val <$> plugHoles embs tcEnv (dataConName dc) killHoles t1 (Loc l t2)) + dts (reverse $ tyArgs dcp)+ tyRes <- val <$> plugHoles embs tcEnv (dataConName dc) killHoles dt (Loc l (tyRes dcp))+ return (dc, Loc l dcp { freeTyVars = map rTyVar das+ , freePred = map (subts (zip (freeTyVars dcp) (map (rVar :: TyVar -> RSort) das))) (freePred dcp)+ , tyArgs = reverse tyArgs+ , tyRes = tyRes}) makeMeasureSelector x s dc n i = M {name = x, sort = s, eqns = [eqn]} where eqn = Def x dc (mkx <$> [1 .. n]) (E (EVar $ mkx i)) @@ -221,11 +284,14 @@ makeRTEnv specs = do forM_ rts $ \(mod, rta) -> setRTAlias (rtName rta) $ Left (mod, rta) forM_ pts $ \(mod, pta) -> setRPAlias (rtName pta) $ Left (mod, pta)+ forM_ ets $ \(mod, eta) -> setREAlias (rtName eta) $ Left (mod, eta)+ makeREAliases ets makeRPAliases pts makeRTAliases rts where rts = (concat [(m,) <$> Ms.aliases s | (m, s) <- specs]) pts = (concat [(m,) <$> Ms.paliases s | (m, s) <- specs])+ ets = (concat [(m,) <$> Ms.ealiases s | (m, s) <- specs]) makeRTAliases xts = mapM_ expBody xts where@@ -242,6 +308,14 @@ body <- withVArgs l (rtVArgs xt) $ expandRPAliasE l $ rtBody xt setRPAlias (rtName xt) $ Right $ xt { rtBody = body } +makeREAliases xts = mapM_ expBody xts+ where + expBody (mod, xt) = inModule mod $ do+ let l = rtPos xt+ env <- gets $ exprAliases . rtEnv+ body <- withVArgs l (rtVArgs xt) $ expandREAliasE l $ rtBody xt+ setREAlias (rtName xt) $ Right $ xt { rtBody = body }+ -- | Using the Alias Environment to Expand Definitions expandRTAliasMeasure m = do eqns <- sequence $ expandRTAliasDef <$> (eqns m)@@ -266,21 +340,33 @@ expandRTAlias :: SourcePos -> BareType -> BareM SpecType expandRTAlias l bt = expType =<< expReft bt where - expReft = mapReftM (txPredReft expPred)+ expReft = mapReftM (txPredReft expPred expExpr) expType = expandAlias l [] expPred = expandPAlias l []+ expExpr = expandEAlias l [] -txPredReft :: (Pred -> BareM Pred) -> RReft -> BareM RReft-txPredReft f (U r p l) = (\r -> U r p l) <$> txPredReft' f r+mapPredM f = go+ where+ go (PAnd ps) = PAnd <$> mapM go ps+ go (POr ps) = POr <$> mapM go ps+ go (PNot p) = PNot <$> go p+ go (PImp p q) = PImp <$> go p <*> go q+ go (PIff p q) = PIff <$> go p <*> go q+ go (PBexp e) = PBexp <$> f e+ go (PAtom b e1 e2) = PAtom b <$> f e1 <*> f e2+ go (PAll xs p) = PAll xs <$> go p+ go p = return p+ ++txPredReft :: (Pred -> BareM Pred) -> (Expr -> BareM Expr) -> RReft -> BareM RReft+txPredReft f fe (U r p l) = (\r -> U r p l) <$> txPredReft' f r where txPredReft' f (Reft (v, ras)) = Reft . (v,) <$> mapM (txPredRefa f) ras- txPredRefa f (RConc p) = RConc <$> f p+ txPredRefa f (RConc p) = fmap RConc $ (f <=< mapPredM fe) p txPredRefa _ z = return z -- | Using the Alias Environment to Expand Definitions -expandRPAliasE l = expandPAlias l []- expandAlias :: SourcePos -> [Symbol] -> BareType -> BareM SpecType expandAlias l = go where@@ -296,7 +382,6 @@ go s (RAllT a t) = RAllT (symbolRTyVar a) <$> go s t go s (RAllP a t) = RAllP <$> ofBPVar a <*> go s t go s (RAllS l t) = RAllS l <$> go s t- go s (RCls c ts) = RCls <$> lookupGhcClass c <*> mapM (go s) ts go _ (ROth s) = return $ ROth s go _ (RExprArg e) = return $ RExprArg e go _ (RHole r) = RHole <$> resolve l r@@ -335,25 +420,32 @@ expandRTApp :: SourcePos -> [Symbol] -> RTAlias RTyVar SpecType -> [BareType] -> RReft -> BareM SpecType expandRTApp l s rta args r- | length args == (length αs) + (length εs)+ | length args == length αs + length εs = do args' <- mapM (expandAlias l s) args let ts = take (length αs) args' αts = zipWith (\α t -> (α, toRSort t, t)) αs ts return $ subst su . (`strengthen` r) . subsTyVars_meet αts $ rtBody rta | otherwise- = errortext $ (text msg)+ = Ex.throw err where su = mkSubst $ zip (symbol <$> εs) es αs = rtTArgs rta εs = rtVArgs rta--- msg = rtName rta ++ " " ++ join (map showpp args) es_ = drop (length αs) args- es = map (exprArg msg) es_- msg = "Malformed type alias application at " ++ show l ++ "\n\t"- ++ show (rtName rta) - ++ " defined at " ++ show (rtPos rta)- ++ "\n\texpects " ++ show (length αs + length εs)- ++ " arguments but it is given " ++ show (length args)+ es = map (exprArg $ show err) es_+ msg = show err+ err :: Error+ err = ErrAliasApp (sourcePosSrcSpan l) (length args) (pprint $ rtName rta) (sourcePosSrcSpan $ rtPos rta) (length αs + length εs) ++ -- JUNK msg = "Malformed type alias application at " ++ show l ++ "\n\t"+ -- JUNK ++ show (rtName rta) + -- JUNK ++ " defined at " ++ show (rtPos rta)+ -- JUNK ++ "\n\texpects " ++ show ()+ -- JUNK ++ " arguments but it is given " ++ show (length args)++ -- JUNK Ex.throw $ errOther $ text + -- JUNK $ "Cyclic Reftype Alias Definition: " ++ show (c:s)+ -- | exprArg converts a tyVar to an exprVar because parser cannot tell -- HORRIBLE HACK To allow treating upperCase X as value variables X -- e.g. type Matrix a Row Col = List (List a Row) Col@@ -371,6 +463,8 @@ exprArg msg z = errorstar $ printf "Unexpected expression parameter: %s in %s" (show z) msg +expandRPAliasE l = expandPAlias l []+ expandPAlias :: SourcePos -> [Symbol] -> Pred -> BareM Pred expandPAlias l = go where @@ -383,9 +477,9 @@ body <- inModule mod $ withVArgs l' (rtVArgs rp) $ expandPAlias l' (f':s) $ rtBody rp let rp' = rp { rtBody = body } setRPAlias f' $ Right $ rp'- expandRPApp l (f':s) rp' <$> resolve l es+ expandEApp l (f':s) rp' <$> resolve l es Just (Right rp) ->- withVArgs l (rtVArgs rp) (expandRPApp l (f':s) rp <$> resolve l es)+ withVArgs l (rtVArgs rp) (expandEApp l (f':s) rp <$> resolve l es) Nothing -> fmap PBexp (EApp <$> resolve l f <*> resolve l es) go s (PAnd ps) = PAnd <$> (mapM (go s) ps) go s (POr ps) = POr <$> (mapM (go s) ps)@@ -395,16 +489,40 @@ go s (PAll xts p) = PAll xts <$> (go s p) go _ p = resolve l p -expandRPApp l s rp es- = let su = mkSubst $ safeZipWithError msg (rtVArgs rp) es+expandREAliasE l = expandEAlias l []++expandEAlias :: SourcePos -> [Symbol] -> Expr -> BareM Expr+expandEAlias l = go+ where + --NOTE: don't do any name-resolution here, expandPAlias runs afterwards and+ -- will handle it+ go s e@(EApp f@(Loc l' f') es)+ | f' `elem` s = errorstar $ "Cyclic Predicate Alias Definition: " ++ show (f':s)+ | otherwise = do+ env <- gets (exprAliases.rtEnv)+ case M.lookup f' env of+ Just (Left (mod,re)) -> do+ body <- inModule mod $ withVArgs l' (rtVArgs re) $ expandEAlias l' (f':s) $ rtBody re+ let re' = re { rtBody = body }+ setREAlias f' $ Right $ re'+ expandEApp l (f':s) re' <$> mapM (go (f':s)) es+ Just (Right re) ->+ withVArgs l (rtVArgs re) (expandEApp l (f':s) re <$> mapM (go (f':s)) es)+ Nothing -> EApp f <$> mapM (go s) es+ go s (EBin op e1 e2) = EBin op <$> go s e1 <*> go s e2+ go s (EIte p e1 e2) = EIte p <$> go s e1 <*> go s e2+ go s (ECst e st) = (`ECst` st) <$> go s e+ go _ e = return e++expandEApp l s re es+ = let su = mkSubst $ safeZipWithError msg (rtVArgs re) es msg = "Malformed alias application at " ++ show l ++ "\n\t"- ++ show (rtName rp) - ++ " defined at " ++ show (rtPos rp)- ++ "\n\texpects " ++ show (length $ rtVArgs rp)+ ++ show (rtName re) + ++ " defined at " ++ show (rtPos re)+ ++ "\n\texpects " ++ show (length $ rtVArgs re) ++ " arguments but it is given " ++ show (length es) -- msg = "expandRPApp: " ++ show (EApp (dummyLoc $ symbol $ rtName rp) es)- in subst su $ rtBody rp-+ in subst su $ rtBody re makeQualifiers (mod,spec) = inModule mod mkQuals where@@ -423,17 +541,18 @@ let (dc:_) = tyConDataCons tc let αs = map symbolRTyVar as let as' = [rVar $ symbolTyVar a | a <- as ]- let ms' = [ (s, rFun "" (RCls c (flip RVar mempty <$> as)) t) | (s, t) <- ms]+ let ms' = [ (s, rFun "" (RApp c (flip RVar mempty <$> as) [] mempty) t) | (s, t) <- ms] vts <- makeSpec cfg vs ms' let sts = [(val s, unClass $ val t) | (s, _) <- ms | (_, _, t) <- vts]- let t = RCls (fromJust $ tyConClass_maybe tc) as'+ let t = rCls tc as' let dcp = DataConP l αs [] [] ss' (reverse sts) t return ((dc,dcp),vts) makeHints vs (_, spec) = varSymbols id "Hint" vs $ Ms.decr spec makeLVar vs (_, spec) = fmap fst <$> (varSymbols id "LazyVar" vs $ [(v, ()) | v <- Ms.lvars spec]) makeLazy vs (_, spec) = fmap fst <$> (varSymbols id "Lazy" vs $ [(v, ()) | v <- S.toList $ Ms.lazy spec])+makeHMeas vs (_, spec) = fmap fst <$> (varSymbols id "HMeas" vs $ [(v, loc v) | v <- S.toList $ Ms.hmeas spec]) makeTExpr vs (_, spec) = varSymbols id "TermExpr" vs $ Ms.termexprs spec varSymbols :: ([Var] -> [Var]) -> Symbol -> [Var] -> [(LocSymbol, a)] -> BareM [(Var, a)]@@ -528,26 +647,16 @@ -- Renaming Type Variables in Haskell Signatures ------------------------------ ------------------------------------------------------------------------------- --- This throws an exception if there is a mismatch--- renameTyVars :: (Var, SpecType) -> (Var, SpecType)-renameTyVars (x, lt@(Loc l t)) = (x, Loc l $ mkUnivs (rTyVar <$> αs) [] [] t')- where- t' = subts su $ mkUnivs [] ps ls tbody- su = [(y, rTyVar x) | (x, y) <- tyvsmap]- tyvsmap = vmap $ execState (mapTyVars τbody tbody) initvmap - initvmap = initMapSt err- (αs, τbody) = splitForAllTys $ expandTypeSynonyms $ varType x- (as, ps, ls, tbody) = bkUniv t- err = errTypeMismatch x lt-- data MapTyVarST = MTVST { vmap :: [(Var, RTyVar)] , errmsg :: Error } initMapSt = MTVST [] -mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> State MapTyVarST ()+runMapTyVars :: StateT MapTyVarST (Either Error) () -> MapTyVarST -> Either Error MapTyVarST+runMapTyVars x s = execStateT x s++mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> StateT MapTyVarST (Either Error) () mapTyVars τ (RAllT a t) = mapTyVars τ t mapTyVars (ForAllTy α τ) t @@ -557,13 +666,13 @@ mapTyVars (TyConApp _ τs) (RApp _ ts _ _) = zipWithM_ mapTyVars τs ts mapTyVars (TyVarTy α) (RVar a _) - = modify $ \s -> mapTyRVar α a s+ = do s <- get+ s' <- mapTyRVar α a s+ put s' mapTyVars τ (RAllP _ t) = mapTyVars τ t mapTyVars τ (RAllS _ t) = mapTyVars τ t -mapTyVars τ (RCls _ ts) - = return () mapTyVars τ (RAllE _ _ t) = mapTyVars τ t mapTyVars τ (REx _ _ t)@@ -576,13 +685,13 @@ mapTyVars τ (RHole _) = return () mapTyVars τ t- = Ex.throw =<< errmsg <$> get+ = throwError =<< errmsg <$> get mapTyRVar α a s@(MTVST αas err) = case lookup α αas of- Just a' | a == a' -> s- | otherwise -> Ex.throw err- Nothing -> MTVST ((α,a):αas) err+ Just a' | a == a' -> return s+ | otherwise -> throwError err+ Nothing -> return $ MTVST ((α,a):αas) err mkVarExpr v | isFunVar v = EApp (varFunSymbol v) []@@ -617,7 +726,7 @@ ----------------------------------------------------------------------------------- -- | Error-Reader-IO For Bare Transformation -------------------------------------- ------------------------------------------------------------------------------------+-- FIXME: don't use WriterT [], very slow type BareM a = WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) a type Warn = String@@ -641,7 +750,7 @@ withVArgs l vs act = do old <- gets rtEnv- mapM (mkExprAlias l . symbol . showpp) vs+ mapM_ (mkExprAlias l . symbol . showpp) vs res <- act modify $ \be -> be { rtEnv = old } return res@@ -657,11 +766,14 @@ setRPAlias s a = modify $ \b -> b { rtEnv = mapRP (M.insert s a) $ rtEnv b } +setREAlias s a =+ modify $ \b -> b { rtEnv = mapRE (M.insert s a) $ rtEnv b }+ ------------------------------------------------------------------ execBare :: BareM a -> BareEnv -> IO (Either Error a) ------------------------------------------------------------------ execBare act benv = - do z <- evalStateT (runErrorT (runWriterT act)) benv+ do z <- evalStateT (runErrorT (runWriterT act)) benv `Ex.catch` (return . Left) case z of Left s -> return $ Left s Right (x, ws) -> do forM_ ws $ putStrLn . ("WARNING: " ++) @@ -775,38 +887,39 @@ where tx = (v,) . Loc l . generalize -plugHoles tce tyi x f t (Loc l st) = Loc l $ mkArrow αs ps' (ls1 ++ ls2) cs' $ go rt' st'''+plugHoles tce tyi x f t (Loc l st) + = do tyvsmap <- case runMapTyVars (mapTyVars (toType rt') st'') initvmap of+ Left e -> throwError e+ Right s -> return $ vmap s+ let su = [(y, rTyVar x) | (x, y) <- tyvsmap]+ st''' = subts su st''+ ps' = fmap (subts su') <$> ps+ su' = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]+ Loc l . mkArrow αs ps' (ls1 ++ ls2) cs' <$> go rt' st''' where (αs, _, ls1, rt) = bkUniv (ofType t :: SpecType) (cs, rt') = bkClass rt (_, ps, ls2, st') = bkUniv st (_, st'') = bkClass st'- cs' = [(dummySymbol, RCls c t) | (c,t) <- cs]-- tyvsmap = vmap $ execState (mapTyVars (toType rt') st'') initvmap+ cs' = [(dummySymbol, RApp c t [] mempty) | (c,t) <- cs] initvmap = initMapSt $ ErrMismatch (sourcePosSrcSpan l) (pprint x) t st- su = [(y, rTyVar x) | (x, y) <- tyvsmap]- st''' = subts su st''- ps' = fmap (subts su') <$> ps- su' = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)] - go t (RHole r) = (addHoles t') { rt_reft = f r }+ go :: SpecType -> SpecType -> BareM SpecType+ go t (RHole r) = return $ (addHoles t') { rt_reft = f r } where t' = everywhere (mkT $ addRefs tce tyi) t addHoles = fmap (const $ f $ uReft ("v", [hole]))- go (RVar _ _) v@(RVar _ _) = v- go (RFun _ i o _) (RFun x i' o' r) = RFun x (go i i') (go o o') r- go (RAllT _ t) (RAllT a t') = RAllT a $ 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 (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy (go t1 t1') (go t2 t2') r- go (RApp _ t _ _) (RApp c t' p r) = RApp c (zipWith go t t') p r- go (RCls _ t) (RCls c t') = RCls c $ zipWith go t t'- go t st = Ex.throw err+ go (RVar _ _) v@(RVar _ _) = return v+ 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 t (RAllE b a t') = RAllE b a <$> go t t'+ go t (REx b x t') = REx b x <$> 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 msg- msg = printf "plugHoles: unhandled case!\nt = %s\nst = %s\n" (showpp t) (showpp st)+ err = errOther $ text $ printf "plugHoles: unhandled case!\nt = %s\nst = %s\n" (showpp t) (showpp st) addRefs :: TCEmb TyCon -> M.HashMap TyCon RTyCon@@ -1167,8 +1280,6 @@ ofBareType (RApp tc ts rs r) = do tyi <- tcEnv <$> get liftM3 (bareTCApp tyi r) (lookupGhcTyCon tc) (mapM ofRef rs) (mapM ofBareType ts)-ofBareType (RCls c ts)- = liftM2 RCls (lookupGhcClass c) (mapM ofBareType ts) ofBareType (ROth s) = return $ ROth s ofBareType (RHole r)@@ -1276,7 +1387,11 @@ = addps m pos r ++ getPsSig m pos t1 ++ getPsSig m pos t2 getPsSig m pos (RFun _ t1 t2 r) = addps m pos r ++ getPsSig m pos t2 ++ getPsSig m (not pos) t1-+getPsSig m pos (RHole r)+ = addps m pos r +getPsSig m pos z + = error $ "getPsSig" ++ show z+ getPsSigPs m pos (RPropP _ r) = addps m pos r getPsSigPs m pos (RProp _ t) = getPsSig m pos t@@ -1345,7 +1460,7 @@ checkGhcSpec specs sp = applyNonNull (Right sp) Left errors where errors = mapMaybe (checkBind "constructor" emb tcEnv env) (dcons sp)- ++ mapMaybe (checkBind "measure" emb tcEnv env) (measSpec sp)+ ++ mapMaybe (checkBind "measure" emb tcEnv env) (meas sp) ++ mapMaybe (checkInv emb tcEnv env) (invariants sp) ++ (checkIAl emb tcEnv env) (ialiases sp) ++ checkMeasures emb env ms@@ -1356,20 +1471,24 @@ ++ checkRTAliases "Type Alias" env tAliases ++ checkRTAliases "Pred Alias" env pAliases -- ++ checkDuplicateRTAlias "Predicate Alias" pAliases - -- ++ checkRTAliasSyms "Predicate Alias" (concat [Ms.paliases sp | (_, sp) <- specs])+ -- ++ checkRTAliasSyms "Predicate Alias" (concat [Ms.paliases sp | (_, sp) <- specs]) tAliases = concat [Ms.aliases sp | (_, sp) <- specs] pAliases = concat [Ms.paliases sp | (_, sp) <- specs]- dcons spec = [ (v, Loc l dc) | (v, dc) <- dataConSpec (dconsP spec), let l = getSourcePos v ] + dcons spec = [(v, Loc l t) | (v,t) <- dataConSpec (dconsP spec) + | (_,dcp) <- dconsP spec+ , let l = dc_loc dcp+ ] emb = tcEmbeds sp env = ghcSpecEnv sp tcEnv = tyconEnv sp ms = measures sp- measSpec sp = [(x, uRType <$> t) | (x, t) <- meas sp] sigs = tySigs sp ++ asmSigs sp +-- RJ: This is not nice. More than 3 elements should be a record.+ type ReplaceM = ReaderT ( M.HashMap Symbol Symbol , SEnv SortedReft , TCEmb TyCon@@ -1562,7 +1681,7 @@ checkRType emb env t = efoldReft cb (rTypeSortedReft emb) f insertPEnv env Nothing t where - cb c ts = classBinds (RCls c ts)+ cb c ts = classBinds (rRCls c ts) f env me r err = err <|> checkReft env emb me r insertPEnv p γ = insertsSEnv γ (mapSnd (rTypeSortedReft emb) <$> pbinds p) pbinds p = (pname p, pvarRType p :: RSort) @@ -1662,8 +1781,6 @@ = do ts' <- mapM expToBindT ts rs' <- mapM expToBindReft rs expToBindRef r >>= addExists . RApp c ts' rs'-expToBindT (RCls c ts)- = liftM (RCls c) (mapM expToBindT ts) expToBindT (RAppTy t1 t2 r) = do t1' <- expToBindT t1 t2' <- expToBindT t2@@ -1726,7 +1843,8 @@ inTarget = moduleName (nameModule name) == getModName target name = getName x notExported = not $ getName x `elemNameSet` exports- killHoles r@(U (Reft (v,rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) }++killHoles r@(U (Reft (v,rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) } ------------------------------------------------------------------------------------- -- | Tasteful Error Messages --------------------------------------------------------
src/Language/Haskell/Liquid/CmdLine.hs view
@@ -1,101 +1,111 @@-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-} {-# OPTIONS_GHC -fno-cse #-} --- | This module contains all the code needed to output the result which --- is either: `SAFE` or `WARNING` with some reasonable error message when --- something goes wrong. All forms of errors/exceptions should go through --- here. The idea should be to report the error, the source position that +-- | This module contains all the code needed to output the result which+-- is either: `SAFE` or `WARNING` with some reasonable error message when+-- something goes wrong. All forms of errors/exceptions should go through+-- here. The idea should be to report the error, the source position that -- causes it, generate a suitable .json file and then exit. module Language.Haskell.Liquid.CmdLine (- -- * Get Command Line Configuration + -- * Get Command Line Configuration getOpts, mkOpts -- * Update Configuration With Pragma , withPragmas- + -- * Exit Function , exitWithResult -- * Diff check mode- , diffcheck + , diffcheck ) where -import Control.DeepSeq-import Control.Monad-import Control.Applicative ((<$>))+import Control.Applicative ((<$>))+import Control.DeepSeq+import Control.Monad -import Data.List (foldl', nub)+import qualified Data.HashMap.Strict as M+import Data.List (foldl', nub) import Data.Maybe import Data.Monoid-import qualified Data.HashMap.Strict as M-import qualified Data.Text as T-import qualified Data.Text.IO as TIO+import qualified Data.Text as T+import qualified Data.Text.IO as TIO -import System.Directory (getCurrentDirectory)-import System.FilePath (dropFileName)-import System.Environment (lookupEnv, withArgs)-import System.Console.CmdArgs hiding (Loud) -import System.Console.CmdArgs.Verbosity (whenLoud) +import System.Console.CmdArgs hiding (Loud)+import System.Console.CmdArgs.Verbosity (whenLoud)+import System.Directory (doesDirectoryExist, canonicalizePath, getCurrentDirectory)+import System.Environment (lookupEnv, withArgs)+import System.FilePath (dropFileName, isAbsolute,+ takeDirectory, (</>)) -import Language.Fixpoint.Misc-import Language.Fixpoint.Files-import Language.Fixpoint.Names (dropModuleNames)-import Language.Fixpoint.Types hiding (config)-import Language.Fixpoint.Config hiding (config, Config, real)-import Language.Haskell.Liquid.Annotate-import Language.Haskell.Liquid.Misc-import Language.Haskell.Liquid.PrettyPrint-import Language.Haskell.Liquid.Types hiding (config, typ, name)+import Language.Fixpoint.Config hiding (Config, config,+ real)+import Language.Fixpoint.Files+import Language.Fixpoint.Misc+import Language.Fixpoint.Names (dropModuleNames)+import Language.Fixpoint.Types hiding (config)+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 Name-import SrcLoc (SrcSpan)-import Text.PrettyPrint.HughesPJ -import Text.Parsec.Pos (newPos)+import Name+import SrcLoc (SrcSpan)+import Text.Parsec.Pos (newPos)+import Text.PrettyPrint.HughesPJ --------------------------------------------------------------------------------- -- Parsing Command Line---------------------------------------------------------- --------------------------------------------------------------------------------- -config = cmdArgsMode $ Config { - files - = def &= typ "TARGET" - &= args - &= typFile - - , idirs - = def &= typDir - &= help "Paths to Spec Include Directory " - - , fullcheck - = def - &= help "Full Checking: check all binders (DEFAULT)" - - , diffcheck - = def - &= help "Incremental Checking: only check changed binders" +config = cmdArgsMode $ Config {+ files+ = def &= typ "TARGET"+ &= args+ &= typFile + , idirs+ = def &= typDir+ &= help "Paths to Spec Include Directory "++ , fullcheck+ = def+ &= help "Full Checking: check all binders (DEFAULT)"++ , diffcheck+ = def+ &= help "Incremental Checking: only check changed binders"+ , real- = def - &= help "Supports real number arithmetic" + = def+ &= help "Supports real number arithmetic" , binders = def &= help "Check a specific set of binders" - , noPrune + , noPrune = def &= help "Disable prunning unsorted Predicates" &= name "no-prune-unsorted" - , notermination + , notermination = def &= help "Disable Termination Check" &= name "no-termination-check" + , nowarnings+ = def &= help "Don't display warnings, only show errors"+ &= name "no-warnings"++ , trustinternals+ = def &= help "Trust all ghc auto generated code"+ &= name "trust-interals"+ , nocaseexpand = def &= help "Disable Termination Check" &= name "no-case-expand"@@ -106,25 +116,25 @@ = def &= help "Disable Trueing Top Level Types" &= name "no-true-types" - , totality + , totality = def &= help "Check totality" - , smtsolver - = def &= help "Name of SMT-Solver" + , smtsolver+ = def &= help "Name of SMT-Solver" - , noCheckUnknown + , noCheckUnknown = def &= explicit &= name "no-check-unknown" &= help "Don't complain about specifications for unexported and unused values " - , maxParams + , maxParams = 2 &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)" , shortNames = def &= name "short-names" &= help "Print shortened names, i.e. drop all module qualifiers."- - , shortErrors ++ , shortErrors = def &= name "short-errors" &= help "Don't show long error messages, just line numbers." @@ -137,46 +147,63 @@ = def &= name "c-files" &= typ "OPTION" &= help "Tell GHC to compile and link against these files"- - -- , verbose ++ -- , verbose -- = def &= help "Generate Verbose Output" -- &= name "verbose-output" } &= verbosity- &= program "liquid" - &= help "Refinement Types for Haskell" - &= summary copyright + &= program "liquid"+ &= help "Refinement Types for Haskell"+ &= summary copyright &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" , "" , "To check a Haskell file foo.hs, type:" , " liquid foo.hs " ] -getOpts :: IO Config -getOpts = do cfg0 <- envCfg - cfg1 <- mkOpts =<< cmdArgsRun config +getOpts :: IO Config+getOpts = do cfg0 <- envCfg+ cfg1 <- mkOpts =<< cmdArgsRun config pwd <- getCurrentDirectory cfg <- canonicalizePaths (fixCfg $ mconcat [cfg0, cfg1]) pwd whenNormal $ putStrLn copyright return cfg -fixCfg cfg = cfg { diffcheck = diffcheck cfg && not (fullcheck cfg) } +-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have+-- to worry about relative paths.+canonicalizePaths :: Config -> FilePath -> IO Config+canonicalizePaths cfg tgt+ = do -- st <- getFileStatus tgt+ tgt <- canonicalizePath tgt+ isdir <- doesDirectoryExist tgt+ let canonicalize f+ | isAbsolute f = return f+ | isdir = canonicalizePath (tgt </> f)+ -- | isDirectory st = canonicalizePath (tgt </> f)+ | otherwise = canonicalizePath (takeDirectory tgt </> f)+ is <- mapM canonicalize $ idirs cfg+ cs <- mapM canonicalize $ cFiles cfg+ return $ cfg { idirs = is, cFiles = cs } ++fixCfg cfg = cfg { diffcheck = diffcheck cfg && not (fullcheck cfg) }+ envCfg = do so <- lookupEnv "LIQUIDHASKELL_OPTS" case so of Nothing -> return mempty Just s -> parsePragma $ envLoc s- where + where envLoc = Loc (newPos "ENVIRONMENT" 0 0) -copyright = "LiquidHaskell © Copyright 2009-14 Regents of the University of California. All Rights Reserved.\n"+copyright = "LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.\n" mkOpts :: Config -> IO Config-mkOpts cfg - = do files' <- sortNub . concat <$> mapM getHsTargets (files cfg) +mkOpts cfg+ = do let files' = sortNub $ files cfg -- idirs' <- if null (idirs cfg) then single <$> getIncludeDir else return (idirs cfg)- id0 <- getIncludeDir - return $ cfg { files = files' } + id0 <- getIncludeDir+ return $ cfg { files = files' } { idirs = (dropFileName <$> files') ++ [id0] ++ idirs cfg } -- tests fail if you flip order of idirs' @@ -200,35 +227,37 @@ -- | Monoid instances for updating options --------------------------------------------------------------------------------------- - + instance Monoid Config where- mempty = Config def def def def def def def def def def def def def 2 def def def def def- mappend c1 c2 = Config { files = sortNub $ files c1 ++ files c2 - , idirs = sortNub $ idirs c1 ++ idirs c2 - , fullcheck = fullcheck c1 || fullcheck c2 - , real = real c1 || real c2 - , diffcheck = diffcheck c1 || diffcheck c2 - , binders = sortNub $ binders c1 ++ binders c2 - , noCheckUnknown = noCheckUnknown c1 || noCheckUnknown c2 - , notermination = notermination c1 || notermination c2 - , nocaseexpand = nocaseexpand c1 || nocaseexpand c2 - , strata = strata c1 || strata c2 - , notruetypes = notruetypes c1 || notruetypes c2 - , totality = totality c1 || totality c2 - , noPrune = noPrune c1 || noPrune c2 - , maxParams = maxParams c1 `max` maxParams c2 - , smtsolver = smtsolver c1 `mappend` smtsolver c2 - , shortNames = shortNames c1 || shortNames c2 - , shortErrors = shortErrors c1 || shortErrors c2 + mempty = Config def def def def def def def def def def def def def def def 2 def def def def def+ mappend c1 c2 = Config { files = sortNub $ files c1 ++ files c2+ , idirs = sortNub $ idirs c1 ++ idirs c2+ , fullcheck = fullcheck c1 || fullcheck c2+ , real = real c1 || real c2+ , diffcheck = diffcheck c1 || diffcheck c2+ , binders = sortNub $ binders c1 ++ binders c2+ , noCheckUnknown = noCheckUnknown c1 || noCheckUnknown c2+ , notermination = notermination c1 || notermination c2+ , nowarnings = nowarnings c1 || nowarnings c2+ , trustinternals = trustinternals c1 || trustinternals c2+ , nocaseexpand = nocaseexpand c1 || nocaseexpand c2+ , strata = strata c1 || strata c2+ , notruetypes = notruetypes c1 || notruetypes c2+ , totality = totality c1 || totality c2+ , noPrune = noPrune c1 || noPrune c2+ , maxParams = maxParams c1 `max` maxParams c2+ , smtsolver = smtsolver c1 `mappend` smtsolver c2+ , shortNames = shortNames c1 || shortNames c2+ , shortErrors = shortErrors c1 || shortErrors c2 , ghcOptions = ghcOptions c1 ++ ghcOptions c2 , cFiles = cFiles c1 ++ cFiles c2 } instance Monoid SMTSolver where mempty = def- mappend s1 s2 - | s1 == s2 = s1 - | s2 == def = s1 + mappend s1 s2+ | s1 == s2 = s1+ | s2 == def = s1 | otherwise = s2 @@ -237,34 +266,32 @@ ------------------------------------------------------------------------ -------------------------------------------------------------------------exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc) +exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc) ------------------------------------------------------------------------ exitWithResult cfg target out- = do let r = o_result out - let rs = showFix r- {-# SCC "annotate" #-} annotate cfg target out+ = do {-# SCC "annotate" #-} annotate cfg target out donePhase Loud "annotate" writeCheckVars $ o_vars out- writeWarns $ o_warns out writeResult cfg (colorResult r) r- writeFile (extFileName Result target) rs- return $ out { o_result = if null (o_warns out) then r else Unsafe [] }+ writeFile (extFileName Result target) (showFix r)+ return $ out { o_result = r }+ where+ r = o_result out `addErrors` o_errors out -writeWarns [] = return () -writeWarns ws = colorPhaseLn Angry "Warnings:" "" >> putStrLn (unlines $ nub ws) -writeCheckVars Nothing = return ()-writeCheckVars (Just []) = colorPhaseLn Loud "Checked Binders: None" ""-writeCheckVars (Just ns) = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . symbolString . dropModuleNames . symbol) -writeResult cfg c = mapM_ (writeDoc c) . zip [0..] . resDocs tidy - where - tidy = if shortErrors cfg then Lossy else Full- writeDoc c (i, d) = writeBlock c i $ lines $ render d- writeBlock c _ [] = return ()- writeBlock c 0 ss = forM_ ss (colorPhaseLn c "")- writeBlock c _ ss = forM_ ("\n" : ss) putStrLn+writeCheckVars Nothing = return ()+writeCheckVars (Just []) = colorPhaseLn Loud "Checked Binders: None" ""+writeCheckVars (Just ns) = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . symbolString . dropModuleNames . symbol) +writeResult cfg c = mapM_ (writeDoc c) . zip [0..] . resDocs tidy+ where+ tidy = if shortErrors cfg then Lossy else Full+ writeDoc c (i, d) = writeBlock c i $ lines $ render d+ writeBlock c _ [] = return ()+ writeBlock c 0 ss = forM_ ss (colorPhaseLn c "")+ writeBlock _ _ ss = forM_ ("\n" : ss) putStrLn+ resDocs _ Safe = [text "SAFE"] resDocs k (Crash xs s) = text ("CRASH: " ++ s) : pprManyOrdered k "" xs resDocs k (Unsafe xs) = text "UNSAFE" : pprManyOrdered k "" (nub xs)@@ -273,6 +300,10 @@ reportUrl = text "Please submit a bug report at: https://github.com/ucsd-progsys/liquidhaskell" +addErrors r [] = r+addErrors Safe errs = Unsafe errs+addErrors (Unsafe xs) errs = Unsafe (xs ++ errs)+addErrors r _ = r instance Fixpoint (FixResult Error) where toFix = vcat . resDocs Full
src/Language/Haskell/Liquid/Constraint.hs view
@@ -97,7 +97,11 @@ consAct info = do γ <- initEnv info sflag <- scheck <$> get- foldM_ (consCBTop (derVars info)) γ (cbs info)+ tflag <- trustghc <$> get+ let trustBinding x = if tflag + then (x `elem` (derVars info) || isInternal x) + else False + foldM_ (consCBTop trustBinding) γ (cbs info) hcs <- hsCs <$> get hws <- hsWfs <$> get scss <- sCs <$> get@@ -184,7 +188,7 @@ measEnv sp xts cbs lts asms hs = CGE { loc = noSrcSpan- , renv = fromListREnv $ second (uRType . val) <$> meas sp+ , renv = fromListREnv $ second val <$> meas sp , syenv = F.fromListSEnv $ freeSyms sp , fenv = initFEnv $ lts ++ (second (rTypeSort tce . val) <$> meas sp) , recs = S.empty @@ -350,9 +354,6 @@ splitW (WfC γ t@(RVar _ _)) = bsplitW γ t -splitW (WfC _ (RCls _ _))- = return []- splitW (WfC γ t@(RApp _ ts rs _)) = do ws <- bsplitW γ t γ' <- γ `extendEnvWithVV` t @@ -360,6 +361,18 @@ ws'' <- concat <$> mapM (rsplitW γ) rs return $ ws ++ ws' ++ ws'' +splitW (WfC γ (RAllE x tx t))+ = do ws <- splitW (WfC γ tx) + γ' <- (γ, "splitW") += (x, tx)+ ws' <- splitW (WfC γ' t)+ return $ ws ++ ws'++splitW (WfC γ (REx x tx t))+ = do ws <- splitW (WfC γ tx) + γ' <- (γ, "splitW") += (x, tx)+ ws' <- splitW (WfC γ' t)+ return $ ws ++ ws'+ splitW (WfC _ t) = errorstar $ "splitW cannot handle: " ++ showpp t @@ -440,6 +453,10 @@ = splitS $ SubC γ t1 t2' where t2' = subsTyVar_meet' (α2, RVar α1 mempty) t2 +splitS (SubC γ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2 + = return []++ splitS (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) = do (t1',t2') <- unifyVV t1 t2 cs <- bsplitS t1' t2'@@ -457,9 +474,6 @@ | a1 == a2 = bsplitS t1 t2 -splitS (SubC _ (RCls c1 _) (RCls c2 _)) | c1 == c2- = return []- splitS c@(SubC _ t1 t2) = errorstar $ "(Another Broken Test!!!) splitS unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2 @@ -559,6 +573,10 @@ = splitC $ SubC γ t1 t2' where t2' = subsTyVar_meet' (α2, RVar α1 mempty) t2 ++splitC (SubC γ t1@(RApp c1 _ _ _) t2@(RApp c2 _ _ _)) | isClass c1 && c1 == c2+ = return []+ splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _)) = do (t1',t2') <- unifyVV t1 t2 cs <- bsplitC γ t1' t2'@@ -576,9 +594,6 @@ | a1 == a2 = bsplitC γ t1 t2 -splitC (SubC _ (RCls c1 _) (RCls c2 _)) | c1 == c2- = return []- splitC c@(SubC _ t1 t2) = errorstar $ "(Another Broken Test!!!) splitc unexpected: " ++ showpp t1 ++ "\n\n" ++ showpp t2 @@ -619,8 +634,7 @@ | s1 <:= s2 = return () | otherwise = addWarning wrn where [s1, s2] = getStrata <$> [t1, t2]- wrn = "Stratum Error : " ++ show s1 ++ " > " ++ show s2 ++ - "\tat " ++ show (pprint $ loc γ)+ wrn = ErrOther (loc γ) (text $ "Stratum Error : " ++ show s1 ++ " > " ++ show s2) bsplitC' γ t1 t2 pflag | F.isFunctionSortedReft r1' && F.isNonTrivialSortedReft r2'@@ -682,8 +696,9 @@ , lits :: ![(F.Symbol, F.Sort)] -- ^ ? FIX THIS , tcheck :: !Bool -- ^ Check Termination (?) , scheck :: !Bool -- ^ Check Strata (?)+ , trustghc :: !Bool -- ^ Trust ghc auto generated bindings , pruneRefs :: !Bool -- ^ prune unsorted refinements- , logWarn :: ![String] -- ^ ? FIX THIS+ , logErrors :: ![TError SpecType] -- ^ Errors during coontraint generation , kvProf :: !KVProf -- ^ Profiling distribution of KVars , recCount :: !Int -- ^ number of recursive functions seen (for benchmarks) } -- deriving (Data, Typeable)@@ -733,8 +748,9 @@ , specLazy = lazy spc , tcheck = not $ notermination cfg , scheck = strata cfg+ , trustghc = trustinternals cfg , pruneRefs = not $ noPrune cfg- , logWarn = []+ , logErrors = [] , kvProf = emptyKVProf , recCount = 0 } @@ -772,8 +788,8 @@ let γ' = γ { renv = insertREnv x t (renv γ) } pflag <- pruneRefs <$> get is <- if isBase t - then liftM single $ addBind x $ rTypeSortedReft' pflag γ' t - else addClassBind t + then liftM2 (++) (liftM single $ addBind x $ rTypeSortedReft' pflag γ' t) (addClassBind t)+ else return [] -- addClassBind t return $ γ' { fenv = insertsFEnv (fenv γ) is } (++=) :: CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv@@ -882,8 +898,8 @@ addW :: WfC -> CG () addW !w = modify $ \s -> s { hsWfs = w : (hsWfs s) } -addWarning :: String -> CG () -addWarning w = modify $ \s -> s { logWarn = w : (logWarn s) }+addWarning :: TError SpecType -> CG () +addWarning w = modify $ \s -> s { logErrors = w : (logErrors s) } -- | Used for annotation binders (i.e. at binder sites) @@ -1004,7 +1020,8 @@ makeDecrIndex :: (Var, SpecType)-> CG [Int] makeDecrIndex (x, t) - = do hint <- checkHint' . L.lookup x . specDecr <$> get+ = do spDecr <- specDecr <$> get+ hint <- checkHint' (L.lookup x $ spDecr) case dindex of Nothing -> addWarning msg >> return [] Just i -> return $ fromMaybe [i] hint@@ -1012,7 +1029,7 @@ ts = ty_args $ toRTypeRep t checkHint' = checkHint x ts isDecreasing dindex = L.findIndex isDecreasing ts- msg = printf "%s: No decreasing parameter" $ showPpr (getSrcSpan x) + msg = ErrTermin [x] (getSrcSpan x) (text "No decreasing parameter") recType ((_, []), (_, [], t)) = t@@ -1029,13 +1046,13 @@ loc (showPpr x) (showPpr vs) checkIndex (x, vs, t, index)- = do mapM_ (safeLogIndex msg' vs) index+ = do mapM_ (safeLogIndex msg' vs) index mapM (safeLogIndex msg ts) index where- loc = showPpr (getSrcSpan x)+ loc = getSrcSpan x ts = ty_args $ toRTypeRep t- msg' = printf "%s: No decreasing argument on %s with %s" loc (showPpr x) (showPpr vs)- msg = printf "%s: No decreasing parameter" loc+ msg' = ErrTermin [x] loc (text $ "No decreasing argument on " ++ (showPpr x) ++ " with " ++ (showPpr vs))+ msg = ErrTermin [x] loc (text "No decreasing parameter") makeRecType t vs dxs is = fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}@@ -1050,26 +1067,26 @@ | otherwise = return $ Just $ ls !! n checkHint _ _ _ Nothing - = Nothing+ = return Nothing checkHint x ts f (Just ns) | L.sort ns /= ns- = errorstar $ printf "%s: The hints should be increasing" loc- where loc = showPpr $ getSrcSpan x+ = addWarning (ErrTermin [x] loc (text "The hints should be increasing")) >> return Nothing+ where loc = getSrcSpan x checkHint x ts f (Just ns) - = Just $ catMaybes (checkValidHint x ts f <$> ns)+ = (mapM (checkValidHint x ts f) ns) >>= (return . Just . catMaybes) checkValidHint x ts f n- | n < 0 || n >= length ts = errorstar err- | f (ts L.!! n) = Just n- | otherwise = errorstar err- where err = printf "%s: Invalid Hint %d for %s" loc (n+1) (showPpr x)- loc = showPpr $ getSrcSpan x+ | n < 0 || n >= length ts = addWarning err >> return Nothing+ | f (ts L.!! n) = return $ Just n+ | otherwise = addWarning err >> return Nothing+ where err = ErrTermin [x] loc (text $ "Invalid Hint " ++ show (n+1) ++ " for " ++ (showPpr x) ++ "\nin\n" ++ show (ts))+ loc = getSrcSpan x ------------------------------------------------------------------- -------------------- Generation: Corebind ------------------------- --------------------------------------------------------------------consCBTop :: [Var] -> CGEnv -> CoreBind -> CG CGEnv +consCBTop :: (Var -> Bool) -> CGEnv -> CoreBind -> CG CGEnv consCBLet :: CGEnv -> CoreBind -> CG CGEnv ------------------------------------------------------------------- @@ -1083,14 +1100,13 @@ modify $ \s -> s{tcheck = oldtcheck} return γ' -consCBTop dVs γ cb | isDerived+consCBTop trustBinding γ cb | all trustBinding xs = do ts <- mapM trueTy (varType <$> xs) foldM (\γ xt -> (γ, "derived") += xt) γ (zip xs' ts)- where isDerived = all (`elem` dVs) xs- xs = bindersOf cb- xs' = F.symbol <$> xs+ where xs = bindersOf cb+ xs' = F.symbol <$> xs -consCBTop _ γ cb+consCBTop _ γ cb = do oldtcheck <- tcheck <$> get strict <- specLazy <$> get let tflag = oldtcheck@@ -1115,12 +1131,12 @@ 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 refreshArgs $ (fromAsserted . thd3 <$> xets) let vs = zipWith collectArgs ts' es- is <- checkSameLens <$> mapM makeDecrIndex (zip xs ts')+ 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)- checkEqTypes . L.transpose <$> mapM checkIndex (zip4 xs vs ts is)+ (L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes let rts = (recType <$>) <$> xeets let xts = zip xs (Asserted <$> ts) γ' <- foldM extender γ xts@@ -1131,17 +1147,18 @@ where dmapM f = sequence . (mapM f <$>) (xs, es) = unzip xes- collectArgs = collectArguments . length . ty_binds . toRTypeRep- checkEqTypes = map (checkAll err1 toRSort . catMaybes)- checkSameLens = checkAll err2 length- err1 = printf "%s: The decreasing parameters should be of same type" loc- err2 = printf "%s: All Recursive functions should have the same number of decreasing parameters" loc- loc = showPpr $ getSrcSpan (head xs)+ collectArgs = collectArguments . length . ty_binds . toRTypeRep+ checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]+ checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)+ checkSameLens = checkAll err2 length+ err1 = ErrTermin xs loc $ text "The decreasing parameters should be of same type"+ err2 = ErrTermin xs loc $ text "All Recursive functions should have the same number of decreasing parameters"+ loc = getSrcSpan (head xs) - checkAll _ _ [] = []+ checkAll _ _ [] = return [] checkAll err f (x:xs) - | all (==(f x)) (f <$> xs) = (x:xs)- | otherwise = errorstar err+ | all (==(f x)) (f <$> xs) = return (x:xs)+ | otherwise = addWarning err >> return [] consCBWithExprs γ (Rec xes) = do xets' <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))@@ -1519,7 +1536,6 @@ refreshVV (RAllT a t) = liftM (RAllT a) (refreshVV t) refreshVV (RAllP p t) = liftM (RAllP p) (refreshVV t)-refreshVV (RCls c ts) = liftM (RCls c) (mapM refreshVV ts) refreshVV (REx x t1 t2) = do [t1', t2'] <- mapM refreshVV [t1, t2]@@ -1621,7 +1637,6 @@ show = showPpr checkTyCon _ t@(RApp _ _ _ _) = t-checkTyCon _ t@(RCls cl ts) = classToRApp t checkTyCon x t = checkErr x t --errorstar $ showPpr x ++ "type: " ++ showPpr t -- checkRPred _ t@(RAll _ _) = t
+ src/Language/Haskell/Liquid/CoreToLogic.hs view
@@ -0,0 +1,171 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections #-}++module Language.Haskell.Liquid.CoreToLogic ( coreToDef , mkLit, runToLogic, LError(..) ) where++import GHC hiding (Located)+import Var++import qualified CoreSyn as C+import Literal+import IdInfo++import Control.Applicative ++import Language.Fixpoint.Misc+import Language.Fixpoint.Names (dropModuleNames, isPrefixOfSym)+import Language.Fixpoint.Types hiding (Def, R, simplify)+import qualified Language.Fixpoint.Types as F+import qualified Language.Fixpoint.Types as F+import Language.Haskell.Liquid.GhcMisc hiding (isDictionary)+import Language.Haskell.Liquid.Types hiding (GhcInfo(..), GhcSpec (..))+++import qualified Data.HashMap.Strict as M++import Data.Monoid+import Data.Functor+import Data.Either++newtype LogicM a = LM (Either a LError)+++data LError = LE String++instance Monad LogicM where+ return = LM . Left+ (LM (Left x)) >>= f = f x+ (LM (Right x)) >>= f = LM (Right x)++instance Functor LogicM where+ fmap f (LM (Left x)) = LM $ Left $ f x+ fmap f (LM (Right x)) = LM $ Right x++instance Applicative LogicM where+ pure = LM . Left++ (LM (Left f)) <*> (LM (Left x)) = LM $ Left (f x)+ (LM (Right f)) <*> (LM (Left x)) = LM $ Right f+ (LM (Left f)) <*> (LM (Right x)) = LM $ Right x+ (LM (Right f)) <*> (LM (Right x)) = LM $ Right x++throw :: String -> LogicM a+throw = LM . Right . LE++runToLogic (LM x) = x++coreToDef :: LocSymbol -> Var -> C.CoreExpr -> LogicM [Def DataCon]+coreToDef x v e = go $ simplify e+ where+ go (C.Lam a e) = go e+ go (C.Tick _ e) = go e+ go (C.Case _ _ _ alts) = mapM goalt alts+ go e' = throw "Measure Functions should have a case at top level"++ goalt ((C.DataAlt d), xs, e) = ((Def x d (symbol <$> xs)) . E) <$> coreToLogic e+ goalt alt = throw $ "Bad alternative" ++ showPpr alt+++coreToLogic :: C.CoreExpr -> LogicM Expr+coreToLogic (C.Let b e) = subst1 <$> coreToLogic e <*> makesub b+coreToLogic (C.Tick _ e) = coreToLogic e+coreToLogic (C.App (C.Var v) e) | ignoreVar v = coreToLogic e+coreToLogic (C.Lit l) + = case mkLit l of + Nothing -> throw $ "Bad Literal in measure definition" ++ showPpr l+ Just i -> return i+coreToLogic (C.Var x) = return $ EVar $ symbol x+coreToLogic e@(C.App _ _) = toLogicApp e +coreToLogic e = throw ("Cannot transform to Logic" ++ showPpr e)++toLogicApp :: C.CoreExpr -> LogicM Expr+toLogicApp e + = do let (f, es) = splitArgs e+ args <- reverse <$> (mapM coreToLogic es)+ (`makeApp` args) <$> tosymbol f++makeApp f [e1, e2] | Just op <- M.lookup (val f) bops+ = EBin op e1 e2++makeApp f args + = EApp f args++bops :: M.HashMap Symbol Bop+bops = M.fromList [ (symbol ("+" :: String), Plus)+ , (symbol ("-" :: String), Minus)+ , (symbol ("*" :: String), Times)+ , (symbol ("/" :: String), Div)+ , (symbol ("%" :: String), Mod)+ ] ++splitArgs (C.App (C.Var i) e) | ignoreVar i = splitArgs e+splitArgs (C.App f (C.Var v)) | isDictionary v = splitArgs f+splitArgs (C.App f e) = (f', e:es) where (f', es) = splitArgs f+splitArgs f = (f, [])++tosymbol (C.Var x) = return $ dummyLoc $ simpleSymbolVar x+tosymbol e = throw ("Bad Measure Definition:\n" ++ showPpr e ++ "\t cannot be applied")++makesub (C.NonRec x e) = (symbol x,) <$> coreToLogic e+makesub _ = throw "Cannot make Logical Substitution of Recursive Definitions"++mkLit :: Literal -> Maybe Expr+mkLit (MachInt n) = mkI n+mkLit (MachInt64 n) = mkI n+mkLit (MachWord n) = mkI n+mkLit (MachWord64 n) = mkI n+mkLit (MachFloat n) = mkR n+mkLit (MachDouble n) = mkR n+mkLit (LitInteger n _) = mkI n+mkLit _ = Nothing -- ELit sym sort+mkI = Just . ECon . I +mkR = Just . ECon . F.R . fromRational++ignoreVar i = simpleSymbolVar i `elem` ["I#"]+++simpleSymbolVar = dropModuleNames . symbol . showPpr . getName++isDictionary v = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v)++isDead = isDeadOcc . occInfo . idInfo++class Simplify a where+ simplify :: a -> a ++instance Simplify C.CoreExpr where+ simplify e@(C.Var x) + = e+ simplify e@(C.Lit _) + = e+ simplify (C.App e (C.Type _)) + = simplify e+ simplify (C.App e (C.Var dict)) | isDictionary dict + = simplify e+ simplify (C.App (C.Lam x e) _) | isDead x + = simplify e+ simplify (C.App e1 e2) + = C.App (simplify e1) (simplify e2)+ simplify (C.Lam x e) | isTyVar x + = simplify e+ simplify (C.Lam x e) + = C.Lam x (simplify e)+ simplify (C.Let xes e) + = C.Let (simplify xes) (simplify e)+ simplify (C.Case e x t alts) + = C.Case (simplify e) x t (simplify <$> alts)+ simplify (C.Cast e c) + = simplify e+ simplify (C.Tick _ e) + = simplify e++instance Simplify C.CoreBind where+ simplify (C.NonRec x e) = C.NonRec x (simplify e)+ simplify (C.Rec xes) = C.Rec (mapSnd simplify <$> xes )++instance Simplify C.CoreAlt where+ simplify (c, xs, e) = (c, xs, simplify e) +
src/Language/Haskell/Liquid/Errors.hs view
@@ -192,6 +192,10 @@ = dSp <+> text "Bad Measure Specification" $+$ (nest 4 $ text "measure " <+> pprint t $+$ pprint s) +ppError' _ dSp (ErrHMeas _ t s)+ = dSp <+> text "Cannot promote Haskell function" <+> pprint t <+> text "to logic"+ $+$ (nest 4 $ pprint s)+ ppError' _ dSp (ErrDupSpecs _ v ls) = dSp <+> text "Multiple Specifications for" <+> pprint v <> colon $+$ (nest 4 $ vcat $ pprint <$> ls)@@ -214,8 +218,17 @@ $+$ text "Haskell:" <+> pprint τ $+$ text "Liquid :" <+> pprint t +ppError' _ dSp (ErrAliasApp _ n name dl dn)+ = dSp <+> text "Malformed Type Alias Application"+ $+$ text "Type alias:" <+> pprint name+ $+$ text "Defined at:" <+> pprint dl+ $+$ text "Expects" <+> pprint dn <+> text "arguments, but is given" <+> pprint n + ppError' _ dSp (ErrSaved _ s) = dSp <+> s++ppError' _ dSp (ErrTermin xs _ s)+ = dSp <+> text "Termination Error on" <+> (hsep $ intersperse comma $ map pprint xs) $+$ s ppError' _ _ (ErrOther _ s) = text "Panic!" <+> nest 4 (pprint s)
src/Language/Haskell/Liquid/Fresh.hs view
@@ -67,6 +67,9 @@ trueRefType (RFun _ t t' _) = rFun <$> fresh <*> true t <*> true t' +trueRefType (RApp c ts _ _) | isClass c+ = rRCls c <$> mapM true ts+ trueRefType (RApp c ts rs r) = RApp c <$> mapM true ts <*> mapM trueRef rs <*> true r @@ -95,6 +98,9 @@ refreshRefType (RFun b t t' _) | b == dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t' | otherwise = rFun b <$> refresh t <*> refresh t'++refreshRefType (RApp rc ts _ _) | isClass rc+ = return $ rRCls rc ts refreshRefType (RApp rc ts rs r) = RApp rc <$> mapM refresh ts <*> mapM refreshRef rs <*> refresh r
src/Language/Haskell/Liquid/GhcInterface.hs view
@@ -138,12 +138,12 @@ deps :: [Id] deps = concatMap dep $ (unfoldingInfo . idInfo <$> concatMap bindersOf cbf) - dep (DFunUnfolding _ _ e) = concatMap grapDep e- dep _ = []+ dep (DFunUnfolding _ _ e) = concatMap grapDep e+ dep (CoreUnfolding {uf_tmpl = e}) = grapDep e+ dep f = [] grapDep :: CoreExpr -> [Id]- grapDep (Var x) = [x]- grapDep _ = []+ grapDep e = freeVars S.empty e updateDynFlags cfg = do df <- getSessionDynFlags@@ -203,7 +203,7 @@ Nothing -> exitWithPanic "Ghc Interface: Unable to get GhcModGuts" -getDerivedDictionaries cm mod = filter ((`elem` pdFuns) . shortPpr) dFuns +getDerivedDictionaries cm mod = dFuns -- filter ((`elem` pdFuns) . shortPpr) dFuns where hsmod = unLoc $ pm_parsed_source mod decls = unLoc <$> hsmodDecls hsmod tyClD = [d | TyClD d <- decls]@@ -395,7 +395,11 @@ specIncludes ext paths reqs = do let libFile = extFileNameR ext $ symbolString preludeName let incFiles = catMaybes $ reqFile ext <$> reqs - liftIO $ forM (libFile : incFiles) (`findFileInDirs` paths)+ liftIO $ forM (libFile : incFiles) $ \f -> do+ mfile <- getFileInDirs f paths+ case mfile of+ Just file -> return file+ Nothing -> errorstar $ "cannot find " ++ f ++ " in " ++ show paths reqFile ext s | isExtFile ext s
src/Language/Haskell/Liquid/GhcMisc.hs view
@@ -13,6 +13,9 @@ module Language.Haskell.Liquid.GhcMisc where +import PrelNames (fractionalClassKeys)+import Class (classKey)+ import Debug.Trace import Avail (availsToNameSet)@@ -25,6 +28,7 @@ import NameSet (NameSet) import SrcLoc (mkRealSrcLoc, mkRealSrcSpan, srcSpanFile, srcSpanFileName_maybe, srcSpanStartLine, srcSpanStartCol) +import Language.Fixpoint.Names (dropModuleNames) import Language.Fixpoint.Misc (errorstar, stripParens) import Text.Parsec.Pos (sourceName, sourceLine, sourceColumn, SourcePos, newPos) import Language.Fixpoint.Types hiding (SESearch(..))@@ -162,6 +166,8 @@ unTickExpr (Tick _ e) = unTickExpr e unTickExpr x = x +isFractionalClass clas = classKey clas `elem` fractionalClassKeys+ ----------------------------------------------------------------------- ------------------ Generic Helpers for DataConstructors --------------- -----------------------------------------------------------------------@@ -304,6 +310,7 @@ where go tvs (Lam b e) | isTyVar b = go tvs e go tvs (Lam b e) | isId b = go (b:tvs) e+ go tvs (Tick _ e) = go tvs e go tvs e = (reverse tvs, e) ignoreLetBinds e@(Let (NonRec x xe) e') @@ -311,8 +318,8 @@ ignoreLetBinds e = e -isDictionary x = L.isPrefixOf "$d" (showPpr x)-isInternal x = L.isPrefixOf "$" (showPpr x)+isDictionary x = L.isPrefixOf "$d" (symbolString $ dropModuleNames $ symbol x)+isInternal x = L.isPrefixOf "$" (symbolString $ dropModuleNames $ symbol x) instance Hashable Var where
src/Language/Haskell/Liquid/Measure.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE OverloadedStrings #-} module Language.Haskell.Liquid.Measure ( Spec (..)@@ -19,8 +20,11 @@ import Text.PrettyPrint.HughesPJ hiding (first) import Text.Printf (printf) import DataCon++import qualified Data.List as L import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S +import qualified Data.Text as T import Data.Monoid hiding ((<>)) import Data.List (foldl1', union, nub) import Data.Either (partitionEithers)@@ -50,11 +54,13 @@ , includes :: ![FilePath] -- ^ Included qualifier files , aliases :: ![RTAlias Symbol BareType] -- ^ RefType aliases , paliases :: ![RTAlias Symbol Pred] -- ^ Refinement/Predicate aliases+ , ealiases :: ![RTAlias Symbol Expr] -- ^ Expression aliases , embeds :: !(TCEmb (LocSymbol)) -- ^ GHC-Tycon-to-fixpoint Tycon map , qualifiers :: ![Qualifier] -- ^ Qualifiers in source/spec files , decr :: ![(LocSymbol, [Int])] -- ^ Information on decreasing arguments , lvars :: ![(LocSymbol)] -- ^ Variables that should be checked in the environment they are used , lazy :: !(S.HashSet LocSymbol) -- ^ Ignore Termination Check in these Functions+ , hmeas :: !(S.HashSet LocSymbol) -- ^ Binders to turn into measures using haskell definitions , pragmas :: ![Located String] -- ^ Command-line configurations passed in through source , cmeasures :: ![Measure ty ()] -- ^ Measures attached to a type-class , imeasures :: ![Measure ty bndr] -- ^ Mappings from (measure,type) -> measure@@ -123,6 +129,10 @@ ms' = checkDuplicateMeasure ms -- ms' = checkFail "Duplicate Measure Definition" (distinct . fmap name) ms ++++ checkDuplicateMeasure ms = case M.toList dups of [] -> ms@@ -149,11 +159,13 @@ , includes = sortNub $ includes s1 ++ includes s2 , aliases = aliases s1 ++ aliases s2 , paliases = paliases s1 ++ paliases s2+ , ealiases = ealiases s1 ++ ealiases s2 , embeds = M.union (embeds s1) (embeds s2) , qualifiers = qualifiers s1 ++ qualifiers s2 , decr = decr s1 ++ decr s2 , lvars = lvars s1 ++ lvars s2 , lazy = S.union (lazy s1) (lazy s2)+ , hmeas = S.union (hmeas s1) (hmeas s2) , pragmas = pragmas s1 ++ pragmas s2 , cmeasures = cmeasures s1 ++ cmeasures s2 , imeasures = imeasures s1 ++ imeasures s2@@ -173,11 +185,13 @@ , includes = [] , aliases = [] , paliases = [] + , ealiases = [] , embeds = M.empty , qualifiers = [] , decr = [] , lvars = [] , lazy = S.empty+ , hmeas = S.empty , pragmas = [] , cmeasures = [] , imeasures = []@@ -270,7 +284,7 @@ mapTy :: (tya -> tyb) -> Measure tya c -> Measure tyb c mapTy f (M n ty eqs) = M n (f ty) eqs -dataConTypes :: MSpec RefType DataCon -> ([(Var, RefType)], [(LocSymbol, RefType)])+dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)]) dataConTypes s = (ctorTys, measTys) where measTys = [(name m, sort m) | m <- M.elems (measMap s) ++ imeas s]@@ -280,7 +294,7 @@ defsTy = foldl1' meet . fmap defRefType defsVar = ctor . safeHead "defsVar" -defRefType :: Def DataCon -> RefType+defRefType :: Def DataCon -> RRType Reft defRefType (Def f dc xs body) = mkArrow as [] [] xts t' where as = RTV <$> dataConUnivTyVars dc
src/Language/Haskell/Liquid/Misc.hs view
@@ -48,10 +48,18 @@ 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"-getCssPath = getDataFileName "syntax/liquid.css"-getHqBotPath = getDataFileName "include/Bot.hquals"+getIncludeDir = dropFileName <$> (getDataFileName $ "include" </> "Prelude.spec")+getCssPath = getDataFileName $ "syntax" </> "liquid.css"+getHqBotPath = getDataFileName $ "include" </> "Bot.hquals" ++maximumWithDefault zero [] = zero+maximumWithDefault _ xs = maximum xs++{-@ type ListN a N = {v:[a] | len v = N} @-}+{-@ type ListL a L = ListN a (len L) @-}++{-@ safeZipWithError :: _ -> xs:[a] -> ListL b xs -> ListL (a,b) xs / [xs] @-} safeZipWithError msg (x:xs) (y:ys) = (x,y) : safeZipWithError msg xs ys safeZipWithError _ [] [] = [] safeZipWithError msg _ _ = errorstar msg
src/Language/Haskell/Liquid/Parse.hs view
@@ -100,12 +100,12 @@ --------------------------------------------------------------------------- parseErrorError :: SourceName -> ParseError -> Error ----------------------------------------------------------------------------parseErrorError f e = ErrParse sp msg lpe+parseErrorError f e = ErrParse sp msg e where pos = errorPos e sp = sourcePosSrcSpan pos msg = text $ "Error Parsing Specification from: " ++ f- lpe = LPE pos (eMsgs e)+ -- lpe = LPE pos (eMsgs e) eMsgs = fmap messageString . errorMessages ---------------------------------------------------------------------------@@ -326,15 +326,13 @@ -getClasses (RApp tc ts _ _) +getClasses t@(RApp tc ts _ _) | isTuple tc- = getClass `fmap` ts + = ts+ | otherwise + = [t] getClasses t - = [getClass t]-getClass (RApp c ts _ _)- = RCls c ts-getClass t- = errorstar $ "Cannot convert " ++ (show t) ++ " to Class"+ = [t] dummyP :: Monad m => m (Reft -> b) -> m b dummyP fm @@ -446,11 +444,13 @@ | IAlias (Located ty, Located ty) | Alias (RTAlias Symbol BareType) | PAlias (RTAlias Symbol Pred)+ | EAlias (RTAlias Symbol Expr) | Embed (LocSymbol, FTycon) | Qualif Qualifier | Decr (LocSymbol, [Int]) | LVars LocSymbol | Lazy LocSymbol+ | HMeas LocSymbol | Pragma (Located String) | CMeas (Measure ty ()) | IMeas (Measure ty ctor)@@ -470,11 +470,13 @@ show (IAlias _) = "IAlias" show (Alias _) = "Alias" show (PAlias _) = "PAlias" + show (EAlias _) = "EAlias" show (Embed _) = "Embed" show (Qualif _) = "Qualif" show (Decr _) = "Decr" show (LVars _) = "LVars" show (Lazy _) = "Lazy" + show (HMeas _) = "HMeas" show (Pragma _) = "Pragma" show (CMeas _) = "CMeas" show (IMeas _) = "IMeas" @@ -498,11 +500,13 @@ , Measure.includes = [q | Incl q <- xs] , Measure.aliases = [a | Alias a <- xs] , Measure.paliases = [p | PAlias p <- xs]+ , Measure.ealiases = [e | EAlias e <- xs] , Measure.embeds = M.fromList [e | Embed e <- xs] , Measure.qualifiers = [q | Qualif q <- xs] , Measure.decr = [d | Decr d <- xs] , Measure.lvars = [d | LVars d <- xs]- , Measure.lazy = S.fromList [s | Lazy s <- xs]+ , Measure.lazy = S.fromList [s | Lazy s <- xs]+ , Measure.hmeas = S.fromList [s | HMeas s <- xs] , Measure.pragmas = [s | Pragma s <- xs] , Measure.cmeasures = [m | CMeas m <- xs] , Measure.imeasures = [m | IMeas m <- xs]@@ -515,7 +519,8 @@ = try (reserved "assume" >> liftM Assm tyBindP ) <|> (reserved "assert" >> liftM Asrt tyBindP ) <|> (reserved "Local" >> liftM LAsrt tyBindP )- <|> (reserved "measure" >> liftM Meas measureP ) + <|> try (reserved "measure" >> liftM Meas measureP ) + <|> (reserved "measure" >> liftM HMeas hmeasureP ) <|> try (reserved "class" >> reserved "measure" >> liftM CMeas cMeasureP) <|> (reserved "instance" >> reserved "measure" >> liftM IMeas iMeasureP) <|> (reserved "class" >> liftM Class classP )@@ -526,6 +531,7 @@ <|> (reserved "using" >> liftM IAlias invaliasP ) <|> (reserved "type" >> liftM Alias aliasP ) <|> (reserved "predicate" >> liftM PAlias paliasP )+ <|> (reserved "expression">> liftM EAlias ealiasP ) <|> (reserved "embed" >> liftM Embed embedP ) <|> (reserved "qualif" >> liftM Qualif qualifierP) <|> (reserved "Decrease" >> liftM Decr decreaseP )@@ -544,6 +550,9 @@ lazyVarP :: Parser LocSymbol lazyVarP = locParserP binderP +hmeasureP :: Parser LocSymbol+hmeasureP = locParserP binderP+ decreaseP :: Parser (LocSymbol, [Int]) decreaseP = mapSnd f <$> liftM2 (,) (locParserP binderP) (spaces >> (many integer)) where f = ((\n -> fromInteger n - 1) <$>)@@ -588,6 +597,7 @@ aliasP = rtAliasP id bareTypeP paliasP = rtAliasP symbol predP+ealiasP = rtAliasP symbol exprP rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty) rtAliasP f bodyP@@ -631,9 +641,10 @@ mb Nothing = [] mb (Just xs) = xs superP = maybeP (parens ( liftM (toRCls <$>) (bareTypeP `sepBy1` comma)) <* reserved "=>")- toRCls (RApp c ts rs r) = RCls c ts- toRCls t@(RCls _ _) = t- toRCls t = errorstar $ "Parse.toRCls called with" ++ show t+ toRCls x = x+-- toRCls (RApp c ts rs r) = RCls c ts+-- toRCls t@(RCls _ _) = t+-- toRCls t = errorstar $ "Parse.toRCls called with" ++ show t rawBodyP = braces $ do
src/Language/Haskell/Liquid/PredType.hs view
@@ -109,9 +109,6 @@ = rFun dummySymbol (dataConTy m t1) (dataConTy m t2) dataConTy m (ForAllTy α t) = RAllT (rTyVar α) (dataConTy m t)-dataConTy _ t- | Just t' <- ofPredTree (classifyPredType t)- = t' dataConTy m (TyConApp c ts) = rApp c (dataConTy m <$> ts) [] mempty dataConTy _ _@@ -163,9 +160,6 @@ t2' <- unifyS rt2 pt2 return $ RAppTy t1' t2' (bUnify r p) -unifyS t@(RCls _ _) (RCls _ _)- = return t- unifyS (RVar v a) (RVar _ p) = do modify $ \s -> s `S.union` (S.fromList $ pvars p) return $ RVar v $ bUnify a p@@ -318,7 +312,6 @@ where (r', πs) = splitRPvar π r substPred msg su (RRTy e r o t) = RRTy (mapSnd (substPred msg su) <$> e) r o (substPred msg su t)-substPred msg su (RCls c ts) = RCls c (substPred msg su <$> ts) substPred msg su (RAllE x t t') = RAllE x (substPred msg su t) (substPred msg su t') substPred msg su (REx x t t') = REx x (substPred msg su t) (substPred msg su t') substPred _ _ t = t@@ -370,8 +363,6 @@ = not (p == p') && isPredInType p t isPredInType p (RApp _ ts _ r) = isPredInURef p r || any (isPredInType p) ts-isPredInType p (RCls _ ts) - = any (isPredInType p) ts isPredInType p (RAllE _ t1 t2) = isPredInType p t1 || isPredInType p t2 isPredInType p (RAppTy t1 t2 r) @@ -394,8 +385,6 @@ | otherwise = freeArgsPs p t freeArgsPs p (RApp _ ts _ r) = nub $ freeArgsPsRef p r ++ concatMap (freeArgsPs p) ts-freeArgsPs p (RCls _ ts) - = nub $ concatMap (freeArgsPs p) ts freeArgsPs p (RAllE _ t1 t2) = nub $ freeArgsPs p t1 ++ freeArgsPs p t2 freeArgsPs p (RAppTy t1 t2 r)
src/Language/Haskell/Liquid/PrettyPrint.hs view
@@ -38,7 +38,7 @@ import Language.Fixpoint.Names (dropModuleNames, propConName, hpropConName) import TypeRep hiding (maybeParen, pprArrowChain) import Text.Parsec.Pos (SourcePos, newPos, sourceName, sourceLine, sourceColumn) -import Text.Parsec.Error (ParseError)+import Text.Parsec.Error (ParseError, errorMessages, showErrorMessages) import Var (Var) import Control.Applicative ((<*>), (<$>)) import Data.Maybe (fromMaybe)@@ -50,7 +50,6 @@ import Data.Interned import qualified Data.HashMap.Strict as M - instance PPrint SrcSpan where pprint = pprDoc @@ -63,11 +62,15 @@ instance PPrint SourceError where pprint = text . show --- instance PPrint ParseError where --- pprint = text . show +instance PPrint ParseError where + pprint e = vcat $ tail $ map text ls+ where+ ls = lines $ showErrorMessages "or" "unknown parse error"+ "expecting" "unexpected" "end of input"+ (errorMessages e) -instance PPrint LParseError where- pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs)+-- instance PPrint LParseError where+-- pprint (LPE _ msgs) = text "Parse Error: " <> vcat (map pprint msgs) instance PPrint Var where pprint = pprDoc @@ -105,6 +108,7 @@ ppE Lossy = ppEnvShort ppEnv ppE Full = ppEnv + ppr_rtype bb p t@(RAllT _ _) = ppr_forall bb p t ppr_rtype bb p t@(RAllP _ _) @@ -135,8 +139,6 @@ | otherwise = ppTycon -ppr_rtype bb p (RCls c ts)- = ppr_cls bb p c ts ppr_rtype bb p t@(REx _ _ _) = ppExists bb p t ppr_rtype bb p t@(RAllE _ _ _)@@ -161,7 +163,6 @@ ppSpine (RFun _ i o _) = ppSpine i <+> text "->" <+> ppSpine o ppSpine (RAppTy t t' _) = text "RAppTy" <+> parens (ppSpine t) <+> parens (ppSpine t') ppSpine (RHole r) = text "RHole"-ppSpine (RCls c ts) = text "RCls" <+> parens (ppCls c ts) ppSpine (RApp c ts rs _) = text "RApp" <+> parens (pprint c) ppSpine (RVar v _) = text "RVar" ppSpine (RExprArg _) = text "RExprArg"@@ -315,10 +316,7 @@ ppTable m = vcat $ pprxt <$> xts where pprxt (x,t) = pprint x $$ nest n (colon <+> pprint t) - n = 1 + maximum [ i | (x, _) <- xts, let i = keySize x, i <= thresh ]+ 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 thresh = 6---
src/Language/Haskell/Liquid/RefType.hs view
@@ -34,7 +34,7 @@ , freeTyVars, tyClasses, tyConName -- TODO: categorize these!- , ofType, ofPredTree, toType+ , ofType, toType , rTyVar, rVar, rApp, rEx , addTyConInfo -- , expandRApp@@ -63,11 +63,11 @@ import Literal import GHC hiding (Located) import DataCon-import PrelInfo (isNumericClass) import qualified TyCon as TC import TypeRep hiding (maybeParen, pprArrowChain) import Type (mkClassPred, splitFunTys, expandTypeSynonyms, isPredTy, substTyWith, classifyPredType, PredTree(..), isClassPred)-import TysWiredIn (listTyCon, intDataCon, trueDataCon, falseDataCon)+import TysWiredIn (listTyCon, intDataCon, trueDataCon, falseDataCon, + intTyCon, charTyCon) import qualified Data.Text as T import Data.Interned@@ -94,6 +94,8 @@ import Language.Haskell.Liquid.Types hiding (R, DataConP (..), sort) import Language.Haskell.Liquid.World +import Language.Haskell.Liquid.CoreToLogic (mkLit)+ import Language.Haskell.Liquid.Misc import Language.Fixpoint.Misc import Language.Haskell.Liquid.GhcMisc (pprDoc, sDocDoc, typeUniqueString, tracePpr, tvId, getDataConVarUnique, showSDoc, showPpr, showSDocDump)@@ -210,31 +212,7 @@ bot = errorstar "bot on RType" ----------------------------------------------------------------------------------- | TyConable Instances --------------------------------------------------------------------------------------------------------------------------------------- --- MOVE TO TYPES-instance TyConable RTyCon where- isFun = isFunTyCon . rtc_tc- isList = (listTyCon ==) . rtc_tc- isTuple = TC.isTupleTyCon . rtc_tc - ppTycon = toFix ---- MOVE TO TYPES-instance TyConable Symbol where- isFun s = funConName == s- isList s = listConName == s- isTuple s = tupConName == s- ppTycon = text . symbolString--instance TyConable LocSymbol where- isFun = isFun . val- isList = isList . val- isTuple = isTuple . val- ppTycon = ppTycon . val-- ------------------------------------------------------------------------------- -- | RefTypable Instances ----------------------------------------------------- -------------------------------------------------------------------------------@@ -248,7 +226,7 @@ toFix = text . showPpr -- MOVE TO TYPES-instance (Eq p, PPrint p, TyConable c, Reftable r, PPrint r) => RefTypable p c Symbol r where+instance (Eq p, PPrint p, TyConable c, Reftable r, PPrint r, PPrint c) => RefTypable p c Symbol r where ppCls = ppClassSymbol ppRType = ppr_rtype ppEnv @@ -293,9 +271,7 @@ = eqRSort m t1 t1' && eqRSort m t2 t2' eqRSort m (RAppTy t1 t2 _) (RAppTy t1' t2' _) = eqRSort m t1 t1' && eqRSort m t2 t2'-eqRSort m (RApp c ts _ _) (RApp c' ts' _ _)- = c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts')-eqRSort m (RCls c ts) (RCls c' ts')+eqRSort m t1@(RApp c ts _ _) t2@(RApp c' ts' _ _) = c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts') eqRSort m (RVar a _) (RVar a' _) = a == M.lookupDefault a' a' m @@ -331,9 +307,6 @@ instance Ord RTyCon where compare x y = compare (rtc_tc x) (rtc_tc y) -instance Eq RTyCon where- x == y = rtc_tc x == rtc_tc y- instance Hashable RTyCon where hashWithSalt i = hashWithSalt i . rtc_tc @@ -373,8 +346,6 @@ = (t, ps) nlzP ps (RAllS _ t) = (t, ps)-nlzP ps t@(RCls _ _)- = (t, ps) nlzP ps (RAllP p t) = (t', [p] ++ ps ++ ps') where (t', ps') = nlzP [] t@@ -556,7 +527,6 @@ freeTyVars (RAllT α t) = freeTyVars t L.\\ [α] freeTyVars (RFun _ t t' _) = freeTyVars t `L.union` freeTyVars t' freeTyVars (RApp _ ts _ _) = L.nub $ concatMap freeTyVars ts-freeTyVars (RCls _ ts) = [] freeTyVars (RVar α _) = [α] freeTyVars (RAllE _ _ t) = freeTyVars t freeTyVars (REx _ _ t) = freeTyVars t@@ -573,21 +543,17 @@ tyClasses (REx _ _ t) = tyClasses t tyClasses (RFun _ t t' _) = tyClasses t ++ tyClasses t' tyClasses (RAppTy t t' _) = tyClasses t ++ tyClasses t'-tyClasses (RApp _ ts _ _) = concatMap tyClasses ts -tyClasses (RCls c ts) = (c, ts) : concatMap tyClasses ts +tyClasses (RApp c ts _ _) + | Just cl <- tyConClass_maybe $ rtc_tc c + = [(cl, ts)] + | otherwise + = [] tyClasses (RVar α _) = [] tyClasses (RRTy _ _ _ t) = tyClasses t tyClasses (RHole r) = [] tyClasses t = errorstar ("RefType.tyClasses cannot handle" ++ show t) ----getTyClasses = everything (++) ([] `mkQ` f)--- where f ((RCls c ts) :: SpecType) = [(c, ts)]--- f _ = []--- ---------------------------------------------------------------- ---------------------- Strictness ------------------------------ ----------------------------------------------------------------@@ -603,7 +569,6 @@ rnf (RAllS s t) = rnf s `seq` rnf t rnf (RFun x t t' r) = rnf x `seq` rnf t `seq` rnf t' `seq` rnf r rnf (RApp _ ts rs r) = rnf ts `seq` rnf rs `seq` rnf r- rnf (RCls c ts) = c `seq` rnf ts rnf (RAllE x t t') = rnf x `seq` rnf t `seq` rnf t' rnf (REx x t t') = rnf x `seq` rnf t `seq` rnf t' rnf (ROth s) = rnf s@@ -634,15 +599,6 @@ instance PPrint (RTProp p c tv r) => Show (RTProp p c tv r) where show = showpp -instance Fixpoint RTyCon where- toFix (RTyCon c _ _) = text $ showPpr c -- <+> text "\n<<" <+> hsep (map toFix ts) <+> text ">>\n"--instance PPrint RTyCon where- pprint = toFix--instance Show RTyCon where- show = showpp - instance PPrint REnv where pprint (REnv m) = pprint m @@ -678,8 +634,6 @@ subsFree m s z@(α, τ, _) (RApp c ts rs r) = RApp (subt z' c) (subsFree m s z <$> ts) (subsFreeRef m s z <$> rs) r where z' = (α, τ) -- UNIFY: why instantiating INSIDE parameters?-subsFree m s z (RCls c ts) - = RCls c (subsFree m s z <$> ts) subsFree meet s (α', _, t') t@(RVar α r) | α == α' && not (α `S.member` s) = if meet then t' `strengthen` r else t' @@ -795,9 +749,6 @@ = rFun dummySymbol (ofType_ τ) (ofType_ τ') ofType_ (ForAllTy α τ) = RAllT (rTyVar α) $ ofType_ τ -ofType_ τ- | Just t <- ofPredTree (classifyPredType τ)- = t ofType_ (TyConApp c τs) | Just (αs, τ) <- TC.synTyConDefn_maybe c = ofType_ $ substTyWith αs τs τ@@ -805,13 +756,13 @@ = rApp c (ofType_ <$> τs) [] mempty ofType_ (AppTy t1 t2) = RAppTy (ofType_ t1) (ofType t2) mempty --- ofType_ τ --- = errorstar ("ofType cannot handle: " ++ showPpr τ)--ofPredTree (ClassPred c τs)- = Just $ RCls c (ofType_ <$> τs)-ofPredTree _- = Nothing+ofType_ (LitTy x)+ = fromTyLit x+ where+ fromTyLit (NumTyLit n) = rApp intTyCon [] [] mempty+ fromTyLit (StrTyLit s) = rApp listTyCon [rApp charTyCon [] [] mempty] [] mempty+ofType_ τ + = errorstar ("ofType cannot handle: " ++ showPpr τ) ---------------------------------------------------------------- ------------------- Converting to Fixpoint ---------------------@@ -882,8 +833,6 @@ = TyVarTy α toType (RApp (RTyCon {rtc_tc = c}) ts _ _) = TyConApp c (toType <$> ts)-toType (RCls c ts) - = mkClassPred c (toType <$> ts) toType (RAllE _ _ t) = toType t toType (REx _ _ t)@@ -926,16 +875,6 @@ literalConst tce l = (sort, mkLit l) where sort = typeSort tce $ literalType l - mkLit (MachInt n) = mkI n- mkLit (MachInt64 n) = mkI n- mkLit (MachWord n) = mkI n- mkLit (MachWord64 n) = mkI n- mkLit (MachFloat n) = mkR n- mkLit (MachDouble n) = mkR n- mkLit (LitInteger n _) = mkI n- mkLit _ = Nothing -- ELit sym sort- mkI = Just . ECon . I - mkR = Just . ECon . R . fromRational --------------------------------------------------------------- ---------------- Annotations and Solutions --------------------@@ -1061,9 +1000,13 @@ -- | Binders generated by class predicates, typically for constraining tyvars (e.g. FNum) ----------------------------------------------------------------------------------------- -classBinds (RCls c ts) - | isNumericClass c = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]-classBinds _ = [] +classBinds t@(RApp c ts _ _) + | isFracCls c+ = [(rTyVarSymbol a, trueSortedReft FReal) | (RVar a _) <- ts]+ | isNumCls c+ = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]+classBinds t + = [] rTyVarSymbol (RTV α) = typeUniqueSymbol $ TyVarTy α
src/Language/Haskell/Liquid/Tidy.hs view
@@ -119,7 +119,6 @@ tyVars (RFun _ t t' _) = tyVars t ++ tyVars t' tyVars (RAppTy t t' _) = tyVars t ++ tyVars t' tyVars (RApp _ ts _ _) = concatMap tyVars ts-tyVars (RCls _ ts) = concatMap tyVars ts tyVars (RVar α _) = [α] tyVars (RAllE _ _ t) = tyVars t tyVars (REx _ _ t) = tyVars t@@ -139,7 +138,6 @@ funBinds (RAllS _ t) = funBinds t funBinds (RFun b t1 t2 _) = b : funBinds t1 ++ funBinds t2 funBinds (RApp _ ts _ _) = concatMap funBinds ts-funBinds (RCls _ ts) = concatMap funBinds ts funBinds (RAllE b t1 t2) = b : funBinds t1 ++ funBinds t2 funBinds (REx b t1 t2) = b : funBinds t1 ++ funBinds t2 funBinds (RVar _ _) = []
src/Language/Haskell/Liquid/TransformRec.hs view
@@ -25,20 +25,51 @@ import TypeRep import Unique hiding (deriveUnique) import Var+import Name (isSystemName) import Language.Haskell.Liquid.GhcMisc import Language.Haskell.Liquid.Misc (mapSndM)+import Language.Fixpoint.Misc (mapSnd) import Data.List (foldl', isInfixOf) import Control.Applicative ((<$>)) +import qualified Data.List as L+ transformRecExpr :: CoreProgram -> CoreProgram transformRecExpr cbs | isEmptyBag $ filterBag isTypeError e = {-trace "new cbs"-} pg | otherwise - = error (showPpr pg ++ "Type-check" ++ showSDoc (pprMessageBag e))- where pg = evalState (transPg cbs) initEnv+ = error ("INITIAL\n" ++ showPpr pg0 ++ "\nTRANSFORMED\n" ++ showPpr pg ++ "Type-check" ++ showSDoc (pprMessageBag e))+ where pg0 = evalState (transPg cbs) initEnv (_, e) = lintCoreBindings [] pg+ pg = inlineFailCases pg0+++inlineFailCases :: CoreProgram -> CoreProgram+inlineFailCases = (go [] <$>)+ where + go su (Rec xes) = Rec (mapSnd (go' su) <$> xes)+ go su (NonRec x e) = NonRec x (go' su e)++ go' su (App (Var x) _) | isFailId x, Just e <- getFailExpr x su = e + go' su (Let (NonRec x ex) e) | isFailId x = go' (addFailExpr x (go' su ex) su) e++ go' su (App e1 e2) = App (go' su e1) (go' su e2)+ go' su (Lam x e) = Lam x (go' su e)+ go' su (Let xs e) = Let (go su xs) (go' su e)+ go' su (Case e x t alt) = Case (go' su e) x t (goalt su <$> alt) + go' su (Cast e c) = Cast (go' su e) c+ go' su (Tick t e) = Tick t (go' su e)+ go' su e = e++ goalt su (c, xs, e) = (c, xs, go' su e)++ isFailId x = isLocalId x && (isSystemName $ varName x) && L.isPrefixOf "fail" (show x)+ getFailExpr = L.lookup++ addFailExpr x (Lam _ e) su = (x, e):su + addFailExpr x e _ = error "internal error" -- this cannot happen isTypeError s | isInfixOf "Non term variable" (showSDoc s) = False isTypeError _ = True
src/Language/Haskell/Liquid/Types.hs view
@@ -17,7 +17,7 @@ module Language.Haskell.Liquid.Types ( -- * Options- Config (..), canonicalizePaths+ Config (..) -- * Ghc Information , GhcInfo (..)@@ -40,6 +40,7 @@ , TyConInfo(..) , rTyConPVs , rTyConPropVs+ , isClassRTyCon -- * Refinement Types , RType (..), Ref(..), RTProp (..)@@ -73,7 +74,7 @@ , BSort, BPVar -- * Instantiated RType- , BareType, RefType, PrType+ , BareType, PrType , SpecType, SpecProp , RSort , UsedPVar, RPVar, RReft@@ -83,7 +84,7 @@ , RTypeRep(..), fromRTypeRep, toRTypeRep , mkArrow, bkArrowDeep, bkArrow, safeBkArrow , mkUnivs, bkUniv, bkClass- , rFun+ , rFun, rCls, rRCls -- * Manipulating `Predicates` , pvars, pappSym, pToRef, pApp@@ -139,8 +140,7 @@ -- * Refinement Type Aliases , RTEnv (..) , RTBareOrSpec- , mapRT- , mapRP+ , mapRT, mapRP, mapRE -- * Final Result , Result (..)@@ -149,7 +149,7 @@ , Error , TError (..) , EMsg (..)- , LParseError (..)+ -- , LParseError (..) , ErrorResult , errSpan , errOther@@ -173,7 +173,6 @@ , updKVProf -- extend profile -- * Misc - , classToRApp , mapRTAVars , insertsSEnv @@ -188,7 +187,7 @@ import FastString (fsLit) import SrcLoc (noSrcSpan, mkGeneralSrcSpan, SrcSpan)-import TyCon+import TyCon import DataCon import Name (getName) import NameSet@@ -203,6 +202,10 @@ import GHC.Generics import Language.Haskell.Liquid.GhcMisc +import PrelInfo (isNumericClass)+++import TysWiredIn (listTyCon) import Control.Arrow (second) import Control.Monad (liftM, liftM2, liftM3) import qualified Control.Monad.Error as Ex@@ -229,12 +232,12 @@ import Language.Fixpoint.Misc import Language.Fixpoint.Types hiding (Predicate, Def, R) -- import qualified Language.Fixpoint.Types as F-import Language.Fixpoint.Names (symSepName, isSuffixOfSym, singletonSym)+import Language.Fixpoint.Names (symSepName, isSuffixOfSym, singletonSym, funConName, listConName, tupConName) import CoreSyn (CoreBind) -import System.Directory (canonicalizePath)+import Language.Haskell.Liquid.GhcMisc (isFractionalClass)+ import System.FilePath ((</>), isAbsolute, takeDirectory)-import System.Posix.Files (getFileStatus, isDirectory) import Data.Default -----------------------------------------------------------------------------@@ -251,6 +254,8 @@ , binders :: [String] -- ^ set of binders to check , noCheckUnknown :: Bool -- ^ whether to complain about specifications for unexported and unused values , notermination :: Bool -- ^ disable termination check+ , nowarnings :: Bool -- ^ disable warnings output (only show errors)+ , trustinternals :: Bool -- ^ type all internal variables with true , nocaseexpand :: Bool -- ^ disable case expand , strata :: Bool -- ^ enable strata analysis , notruetypes :: Bool -- ^ disable truing top level types@@ -264,21 +269,7 @@ , cFiles :: [String] -- ^ .c files to compile and link against (for GHC) } deriving (Data, Typeable, Show, Eq) --- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have--- to worry about relative paths.-canonicalizePaths :: Config -> FilePath -> IO Config-canonicalizePaths cfg tgt- = do st <- getFileStatus tgt- tgt <- canonicalizePath tgt- let canonicalize f- | isAbsolute f = return f- | isDirectory st = canonicalizePath (tgt </> f)- | otherwise = canonicalizePath (takeDirectory tgt </> f)- is <- mapM canonicalize $ idirs cfg- cs <- mapM canonicalize $ cFiles cfg- return $ cfg { idirs = is, cFiles = cs } - ----------------------------------------------------------------------------- -- | Printer ---------------------------------------------------------------- -----------------------------------------------------------------------------@@ -346,7 +337,7 @@ , asmSigs :: ![(Var, Located SpecType)] -- ^ Assumed Reftypes , ctors :: ![(Var, Located SpecType)] -- ^ Data Constructor Measure Sigs -- eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }- , meas :: ![(Symbol, Located RefType)] -- ^ Measure Types + , meas :: ![(Symbol, Located SpecType)] -- ^ Measure Types -- eg. len :: [a] -> Int , invariants :: ![Located SpecType] -- ^ Data Type Invariants @@ -386,8 +377,8 @@ , freeTyVars :: ![RTyVar] , freePred :: ![PVar RSort] , freeLabels :: ![Symbol]- , tyConsts :: ![SpecType]- , tyArgs :: ![(Symbol, SpecType)]+ , tyConsts :: ![SpecType] -- ^ FIXME: WHAT IS THIS??+ , tyArgs :: ![(Symbol, SpecType)] -- ^ These are backwards, why?? , tyRes :: !SpecType } deriving (Data, Typeable) @@ -511,6 +502,8 @@ -- | Accessors for @RTyCon@ ++isClassRTyCon = isClassTyCon . rtc_tc rTyConInfo = rtc_info rTyConTc = rtc_tc rTyConPVs = rtc_pvars@@ -599,11 +592,6 @@ , rt_reft :: !r } - | RCls { - rt_class :: !p- , rt_args :: ![RType p c tv r]- }- | RAllE { rt_bind :: !Symbol , rt_allarg :: !(RType p c tv r)@@ -711,7 +699,6 @@ type PrType = RRType Predicate type BareType = BRType RReft type SpecType = RRType RReft -type RefType = RRType Reft type SpecProp = RRProp RReft type RRProp r = Ref RSort r (RRType r) @@ -736,7 +723,15 @@ isList :: c -> Bool isTuple :: c -> Bool ppTycon :: c -> Doc+ isClass :: c -> Bool + isNumCls :: c -> Bool+ isFracCls :: c -> Bool++ isClass = const False+ isNumCls = const False+ isFracCls = const False+ class ( TyConable c , Eq p, Eq c, Eq tv , Hashable tv@@ -747,6 +742,50 @@ ppCls :: p -> [RType p c tv r] -> Doc ppRType :: Prec -> RType p c tv r -> Doc +++-------------------------------------------------------------------------------+-- | TyConable Instances -------------------------------------------------------+-------------------------------------------------------------------------------++-- MOVE TO TYPES+instance TyConable RTyCon where+ isFun = isFunTyCon . rtc_tc+ isList = (listTyCon ==) . rtc_tc+ isTuple = TyCon.isTupleTyCon . rtc_tc + isClass = isClassRTyCon+ ppTycon = toFix ++ isNumCls c = maybe False isNumericClass (tyConClass_maybe $ rtc_tc c)+ isFracCls c = maybe False isFractionalClass (tyConClass_maybe $ rtc_tc c)++-- MOVE TO TYPES+instance TyConable Symbol where+ isFun s = funConName == s+ isList s = listConName == s+ isTuple s = tupConName == s+ ppTycon = text . symbolString++instance TyConable LocSymbol where+ isFun = isFun . val+ isList = isList . val+ isTuple = isTuple . val+ ppTycon = ppTycon . val+++instance Eq RTyCon where+ x == y = rtc_tc x == rtc_tc y++instance Fixpoint RTyCon where+ toFix (RTyCon c _ _) = text $ showPpr c -- <+> text "\n<<" <+> hsep (map toFix ts) <+> text ">>\n"+++instance PPrint RTyCon where+ pprint = toFix++instance Show RTyCon where+ show = showpp + -------------------------------------------------------------------------- -- | Values Related to Specifications ------------------------------------ --------------------------------------------------------------------------@@ -852,10 +891,15 @@ bkUniv (RAllS s t) = let (αs, πs, ss, t') = bkUniv t in (αs, πs, s:ss, t') bkUniv t = ([], [], [], t) -bkClass (RFun _ (RCls c t) t' _) = let (cs, t'') = bkClass t' in ((c, t):cs, t'')-bkClass t = ([], t)+bkClass (RFun _ (RApp c t _ _) t' _) + | isClass c + = let (cs, t'') = bkClass t' in ((c, t):cs, t'')+bkClass t + = ([], t) rFun b t t' = RFun b t t' mempty+rCls c ts = RApp (RTyCon c [] defaultTyConInfo) ts [] mempty+rRCls rc ts = RApp rc ts [] mempty addTermCond = addObligation OTerm @@ -1008,7 +1052,6 @@ emapReft f γ (RAllS p t) = RAllS p (emapReft f γ t) emapReft f γ (RFun x t t' r) = RFun x (emapReft f γ t) (emapReft f (x:γ) t') (f γ r) emapReft f γ (RApp c ts rs r) = RApp c (emapReft f γ <$> ts) (emapRef f γ <$> rs) (f γ r)-emapReft f γ (RCls c ts) = RCls c (emapReft f γ <$> ts) emapReft f γ (RAllE z t t') = RAllE z (emapReft f γ t) (emapReft f γ t') emapReft f γ (REx z t t') = REx z (emapReft f γ t) (emapReft f γ t') emapReft _ _ (RExprArg e) = RExprArg e@@ -1048,7 +1091,6 @@ mapReftM f (RAllS s t) = liftM (RAllS s) (mapReftM f t) mapReftM f (RFun x t t' r) = liftM3 (RFun x) (mapReftM f t) (mapReftM f t') (f r) mapReftM f (RApp c ts rs r) = liftM3 (RApp c) (mapM (mapReftM f) ts) (mapM (mapRefM f) rs) (f r)-mapReftM f (RCls c ts) = liftM (RCls c) (mapM (mapReftM f) ts) mapReftM f (RAllE z t t') = liftM2 (RAllE z) (mapReftM f t) (mapReftM f t') mapReftM f (REx z t t') = liftM2 (REx z) (mapReftM f t) (mapReftM f t') mapReftM _ (RExprArg e) = return $ RExprArg e @@ -1071,11 +1113,11 @@ go γ z (RAllT _ t) = go γ z t go γ z (RAllP p t) = go (fp p γ) z t go γ z (RAllS s t) = go γ z t- go γ z me@(RFun _ (RCls c ts) t' r) = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') + go γ z me@(RFun _ (RApp c ts _ _) t' r) + | isClass c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t') go γ z me@(RFun x t t' r) = f γ (Just me) r (go (insertSEnv x (g t) γ) (go γ z t) t') go γ z me@(RApp _ ts rs r) = f γ (Just me) r (ho' γ (go' (insertSEnv (rTypeValueVar me) (g me) γ) z ts) rs) - go γ z (RCls c ts) = go' γ z ts go γ z (RAllE x t t') = go (insertSEnv x (g t) γ) (go γ z t) t' go γ z (REx x t t') = go (insertSEnv x (g t) γ) (go γ z t) t' go _ z (ROth _) = z @@ -1085,7 +1127,7 @@ go γ z me@(RHole r) = f γ (Just me) r z -- folding over Ref - ho γ z (RPropP ss r) = f (insertsSEnv γ (mapSnd (g . ofRSort) <$> ss)) Nothing r z+ ho γ z (RPropP ss r) = f (insertsSEnv γ (mapSnd (g . ofRSort) <$> ss)) Nothing r z ho γ z (RProp ss t) = go (insertsSEnv γ ((mapSnd (g . ofRSort)) <$> ss)) z t -- folding over [RType]@@ -1101,7 +1143,6 @@ mapBot f (RFun x t t' r) = RFun x (mapBot f t) (mapBot f t') r mapBot f (RAppTy t t' r) = RAppTy (mapBot f t) (mapBot f t') r mapBot f (RApp c ts rs r) = f $ RApp c (mapBot f <$> ts) (mapBotRef f <$> rs) r-mapBot f (RCls c ts) = RCls c (mapBot f <$> ts) mapBot f (REx b t1 t2) = REx b (mapBot f t1) (mapBot f t2) mapBot f (RAllE b t1 t2) = RAllE b (mapBot f t1) (mapBot f t2) mapBot f t' = f t' @@ -1113,7 +1154,6 @@ mapBind f (RAllS s t) = RAllS s (mapBind f t) mapBind f (RFun b t1 t2 r) = RFun (f b) (mapBind f t1) (mapBind f t2) r mapBind f (RApp c ts rs r) = RApp c (mapBind f <$> ts) (mapBindRef f <$> rs) r-mapBind f (RCls c ts) = RCls c (mapBind f <$> ts) mapBind f (RAllE b t1 t2) = RAllE (f b) (mapBind f t1) (mapBind f t2) mapBind f (REx b t1 t2) = REx (f b) (mapBind f t1) (mapBind f t2) mapBind _ (RVar α r) = RVar α r@@ -1142,7 +1182,6 @@ stripQuantifiers (RFun x t t' r) = RFun x (stripQuantifiers t) (stripQuantifiers t') r stripQuantifiers (RAppTy t t' r) = RAppTy (stripQuantifiers t) (stripQuantifiers t') r stripQuantifiers (RApp c ts rs r) = RApp c (stripQuantifiers <$> ts) (stripQuantifiersRef <$> rs) r-stripQuantifiers (RCls c ts) = RCls c (stripQuantifiers <$> ts) stripQuantifiers t = t stripQuantifiersRef (RProp s t) = RProp s $ stripQuantifiers t stripQuantifiersRef r = r@@ -1327,22 +1366,21 @@ -- | INVARIANT : all Error constructors should have a pos field data TError t = - ErrSubType { pos :: !SrcSpan- , msg :: !Doc - , ctx :: !(M.HashMap Symbol t) - , tact :: !t- , texp :: !t- } -- ^ liquid type error-- | ErrAssType { pos :: !SrcSpan- , obl :: !Oblig- , msg :: !Doc- , ref :: !RReft- } -- ^ liquid type error+ ErrSubType { pos :: !SrcSpan+ , msg :: !Doc + , ctx :: !(M.HashMap Symbol t) + , tact :: !t+ , texp :: !t+ } -- ^ liquid type error+ | ErrAssType { pos :: !SrcSpan+ , obl :: !Oblig+ , msg :: !Doc+ , ref :: !RReft+ } -- ^ liquid type error | ErrParse { pos :: !SrcSpan , msg :: !Doc- , err :: !LParseError+ , err :: !ParseError } -- ^ specification parse error | ErrTySpec { pos :: !SrcSpan@@ -1383,6 +1421,11 @@ , msg :: !Doc } -- ^ Measure sort error + | ErrHMeas { pos :: !SrcSpan+ , ms :: !Symbol+ , msg :: !Doc+ } -- ^ Haskell bad Measure error+ | ErrUnbound { pos :: !SrcSpan , var :: !Doc } -- ^ Unbound symbol in specification @@ -1397,17 +1440,30 @@ , texp :: !t } -- ^ Mismatch between Liquid and Haskell types + | ErrAliasApp { pos :: !SrcSpan+ , nargs :: !Int+ , dname :: !Doc+ , dpos :: !SrcSpan+ , dargs :: !Int+ }+ | ErrSaved { pos :: !SrcSpan , msg :: !Doc- } -- ^ Unexpected PANIC - + } -- ^ Previously saved error, that carries over after DiffCheck++ + | ErrTermin { bind :: ![Var]+ , pos :: !SrcSpan+ , msg :: !Doc+ } -- ^ Termination Error + | ErrOther { pos :: !SrcSpan , msg :: !Doc } -- ^ Unexpected PANIC deriving (Typeable, Functor) -data LParseError = LPE !SourcePos [String] - deriving (Data, Typeable, Generic)+-- data LParseError = LPE !SourcePos [String] +-- deriving (Data, Typeable, Generic) instance Eq Error where@@ -1492,16 +1548,22 @@ type RTPredAlias = Either (ModName, RTAlias Symbol Pred) (RTAlias Symbol Pred) +type RTExprAlias = Either (ModName, RTAlias Symbol Expr)+ (RTAlias Symbol Expr)+ data RTEnv = RTE { typeAliases :: M.HashMap Symbol RTBareOrSpec , predAliases :: M.HashMap Symbol RTPredAlias+ , exprAliases :: M.HashMap Symbol RTExprAlias } instance Monoid RTEnv where- (RTE ta1 pa1) `mappend` (RTE ta2 pa2) = RTE (ta1 `M.union` ta2) (pa1 `M.union` pa2)- mempty = RTE M.empty M.empty+ (RTE ta1 pa1 ea1) `mappend` (RTE ta2 pa2 ea2)+ = RTE (ta1 `M.union` ta2) (pa1 `M.union` pa2) (ea1 `M.union` ea2)+ mempty = RTE M.empty M.empty M.empty mapRT f e = e { typeAliases = f $ typeAliases e } mapRP f e = e { predAliases = f $ predAliases e }+mapRE f e = e { exprAliases = f $ exprAliases e } cinfoError (Ci _ (Just e)) = e cinfoError (Ci l _) = errOther $ text $ "Cinfo:" ++ showPpr l@@ -1569,6 +1631,7 @@ subst su (R s e) = R s $ subst su e + data RClass ty = RClass { rcName :: LocSymbol , rcSupers :: [ty]@@ -1579,7 +1642,6 @@ instance Functor RClass where fmap f (RClass n ss tvs ms) = RClass n (fmap f ss) tvs (fmap (second f) ms) - ------------------------------------------------------------------------ -- | Annotations ------------------------------------------------------- ------------------------------------------------------------------------@@ -1613,7 +1675,7 @@ ------------------------------------------------------------------------ data Output a = O { o_vars :: Maybe [String]- , o_warns :: [String]+ , o_errors :: ! [Error] , o_types :: !(AnnInfo a) , o_templs :: !(AnnInfo a) , o_bots :: ![SrcSpan] @@ -1625,7 +1687,7 @@ instance Monoid (Output a) where mempty = emptyOutput mappend o1 o2 = O { o_vars = sortNub <$> mappend (o_vars o1) (o_vars o2)- , o_warns = sortNub $ mappend (o_warns o1) (o_warns o2)+ , o_errors = sortNub $ mappend (o_errors o1) (o_errors o2) , o_types = mappend (o_types o1) (o_types o2) , o_templs = mappend (o_templs o1) (o_templs o2) , o_bots = sortNub $ mappend (o_bots o1) (o_bots o2)@@ -1678,9 +1740,9 @@ hasHole (toReft -> (Reft (_, rs))) = any isHole rs -classToRApp :: SpecType -> SpecType-classToRApp (RCls cl ts) - = RApp (RTyCon (classTyCon cl) def def) ts mempty mempty+-- classToRApp :: SpecType -> SpecType+-- classToRApp (RCls cl ts) +-- = RApp (RTyCon (classTyCon cl) def def) ts mempty mempty instance Symbolic DataCon where symbol = symbol . dataConWorkId
+ syntax/flycheck-liquid.el view
@@ -0,0 +1,86 @@+;;; 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
+ syntax/haskell.vim view
@@ -0,0 +1,379 @@+" 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"+
+ syntax/liquid-tip.el view
@@ -0,0 +1,281 @@+;;; 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 'json)+(require 'pos-tip nil t)+(require 'thingatpt)+(require 'button-lock nil t)++;; (require 'json-mode)+;; (require 'ring)+;; (require 'etags)+;; (require 'flymake)+;; (require 'eldoc)+;; (require 'log4e)+;; (require 'yaxception)++;; ------------------------------------------------------------------------+;; 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)+ (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)+ ;; DEBUG (button-lock-set-button "yoga" 'liquid-tip-show)+ ;; DEBUG (button-lock-set-button "mydiv" 'liquid-tip-show)+ ))++;;;###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)))++;; DEBUG (defface my-tooltip+;; DEBUG '((t+;; DEBUG :background "gray85"+;; DEBUG :foreground "black"+;; DEBUG :inherit variable-pitch))+;; DEBUG "Face for my tooltip.")+;; DEBUG +;; DEBUG (defface my-tooltip-highlight+;; DEBUG '((t+;; DEBUG :background "blue"+;; DEBUG :foreground "white"+;; DEBUG :inherit my-tooltip))+;; DEBUG "Face for my tooltip highlighted.")+;; DEBUG +;; DEBUG (let ((str (propertize "foo\nbar\nbaz" 'face 'my-tooltip)))+;; DEBUG (put-text-property 6 11 'face 'my-tooltip-highlight str)+;; DEBUG (pos-tip-show-no-propertize str 'my-tooltip))++(provide 'liquid-tip)++;; Local Variables:+;; coding: utf-8+;; mode: emacs-lisp+;; End:++;;; liquid-tip.el ends here
+ syntax/liquid.vim view
@@ -0,0 +1,47 @@+"============================================================================+"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:
tests/test.hs view
@@ -1,13 +1,20 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE ScopedTypeVariables #-} module Main where import Control.Applicative import Control.Monad+import Data.Char import Data.Proxy+import Data.Tagged+import Data.Typeable+import Options.Applicative import System.Directory import System.Exit import System.FilePath import System.IO-import qualified System.Posix as Posix+-- import qualified System.Posix as Posix import System.Process import Test.Tasty import Test.Tasty.HUnit@@ -16,44 +23,29 @@ import Test.Tasty.Runners import Text.Printf --- main--- = do pos <- dirTests "tests/pos" [] ExitSuccess--- neg <- dirTests "tests/neg" [] (ExitFailure 1)--- crash <- dirTests "tests/crash" [] (ExitFailure 2)--- -- benchmarks--- text <- dirTests "benchmarks/text-0.11.2.3" textIgnored ExitSuccess--- bs <- dirTests "benchmarks/bytestring-0.9.2.1" [] ExitSuccess--- esop <- dirTests "benchmarks/esop2013-submission" ["Base0.hs"] ExitSuccess--- vector_algs <- dirTests "benchmarks/vector-algorithms-0.5.4.2" [] ExitSuccess--- hscolour <- dirTests "benchmarks/hscolour-1.20.0.0" [] ExitSuccess--- -- TestTrees--- let unit = testGroup "Unit"--- [ testGroup "pos" pos--- , testGroup "neg" neg--- , testGroup "crash" crash--- ]--- let bench = testGroup "Benchmarks"--- [ testGroup "text" text--- , testGroup "bytestring" bs--- , testGroup "esop" esop--- , testGroup "vector-algorithms" vector_algs--- , testGroup "hscolour" hscolour--- ]--- defaultMainWithIngredients--- [ rerunningTests [ listingTests, consoleTestReporter ]--- , includingOptions [ Option (Proxy :: Proxy NumThreads) ]--- ] $ testGroup "Tests" [ unit, bench ]- main :: IO () main = run =<< tests where run = defaultMainWithIngredients [ rerunningTests [ listingTests, consoleTestReporter ]- , includingOptions [ Option (Proxy :: Proxy NumThreads) ]+ , includingOptions [ Option (Proxy :: Proxy NumThreads)+ , Option (Proxy :: Proxy SmtSolver) ] ] tests = group "Tests" [ unitTests, benchTests ] +data SmtSolver = Z3 | CVC4 deriving (Show, Read, Eq, Ord, Typeable)+instance IsOption SmtSolver where+ defaultValue = Z3+ parseValue = safeRead . map toUpper+ optionName = return "smtsolver"+ optionHelp = return "Use this SMT solver"+ optionCLParser =+ option (fmap (read . map toUpper) str)+ ( long (untag (optionName :: Tagged SmtSolver String))+ <> help (untag (optionHelp :: Tagged SmtSolver String))+ )+ unitTests = group "Unit" [ testGroup "pos" <$> dirTests "tests/pos" [] ExitSuccess@@ -82,28 +74,35 @@ isTest :: FilePath -> Bool isTest f = takeExtension f == ".hs" -- `elem` [".hs", ".lhs"] -- --------------------------------------------------------------------------- mkTest :: ExitCode -> FilePath -> FilePath -> TestTree --------------------------------------------------------------------------- mkTest code dir file- = testCase file $ do- createDirectoryIfMissing True $ takeDirectory log- liquid <- canonicalizePath "dist/build/liquid/liquid"- withFile log WriteMode $ \h -> do- let cmd = testCmd liquid dir file- (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}- c <- waitForProcess ph- assertEqual "Wrong exit code" code c+ = askOption $ \(smt :: SmtSolver) -> testCase file $ do+ if test `elem` knownToFail smt+ then do+ printf "%s is known to fail with %s: SKIPPING" test (show smt)+ assertEqual "" True True+ else do+ createDirectoryIfMissing True $ takeDirectory log+ liquid <- canonicalizePath "dist/build/liquid/liquid"+ withFile log WriteMode $ \h -> do+ let cmd = testCmd liquid dir file smt+ (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}+ c <- waitForProcess ph+ assertEqual "Wrong exit code" code c where+ test = dir </> file log = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log" +knownToFail CVC4 = [ "tests/pos/RealProps.hs", "tests/pos/RealProps1.hs", "tests/pos/initarray.hs" ]+knownToFail Z3 = [] ----------------------------------------------------------------------------testCmd :: FilePath -> FilePath -> FilePath -> String+testCmd :: FilePath -> FilePath -> FilePath -> SmtSolver -> String ----------------------------------------------------------------------------testCmd liquid dir file = printf "cd %s && %s --verbose %s" dir liquid file+testCmd liquid dir file smt + = printf "cd %s && %s --verbose --smtsolver %s %s" dir liquid (show smt) file textIgnored = [ "Data/Text/Axioms.hs"@@ -152,7 +151,7 @@ walkDirectory :: FilePath -> IO [FilePath] ---------------------------------------------------------------------------------------- walkDirectory root- = do (ds,fs) <- partitionM isDirectory . candidates =<< getDirectoryContents root+ = do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< getDirectoryContents root (fs++) <$> concatMapM walkDirectory ds where candidates fs = [root </> f | f <- fs, not (isExtSeparator (head f))]@@ -165,8 +164,8 @@ if b then go (x:ls) rs xs else go ls (x:rs) xs -isDirectory :: FilePath -> IO Bool-isDirectory = fmap Posix.isDirectory . Posix.getFileStatus+-- isDirectory :: FilePath -> IO Bool+-- isDirectory = fmap Posix.isDirectory . Posix.getFileStatus concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b] concatMapM f [] = pure []