packages feed

liquidhaskell 0.8.2.2 → 0.8.2.3

raw patch · 60 files changed

+1745/−784 lines, 60 filesdep +gitrevdep +optparse-simpledep ~liquid-fixpoint

Dependencies added: gitrev, optparse-simple

Dependency ranges changed: liquid-fixpoint

Files

devel/Paths_liquidhaskell.hs view
@@ -1,12 +1,18 @@ {-# LANGUAGE TemplateHaskell #-}+ module Paths_liquidhaskell where  import Language.Haskell.TH import System.Directory import System.FilePath+import Data.Version (Version, makeVersion)  getDataFileName :: FilePath -> IO FilePath getDataFileName f = do   let loc = $(do { loc <- location; f <- runIO (canonicalizePath (loc_filename loc)); litE (stringL f); })   let root = takeDirectory (takeDirectory loc)   return (root </> f)++-- | dummy version (devel only)+version :: Version+version = makeVersion [0,0,0,0]
include/Language/Haskell/Liquid/NewProofCombinators.hs view
@@ -18,8 +18,13 @@    -- * These two operators check all intermediate equalities   , (===) -- proof of equality is implicit eg. x === y-  , (==?) -- proof of equality is explitic eg. x ==? y ? p+  , (==?) -- proof of equality is explicit eg. x ==? y ? p+  , (=<=) -- proof of equality is implicit eg. x <= y+  , (=<=?) -- proof of equality is explicit eg. x <= y+  , (=>=)  -- proof of equality is implicit eg. x =>= y +  , (=>=?) -- proof of equality is explicit eg. x =>=? y ? p +   -- Uncheck operator used only for proof debugging   , (==!) -- x ==! y always succeds @@ -95,6 +100,18 @@ (===) :: a -> a -> a x === _  = x +infixl 3 =<=+{-@ (=<=) :: x:a -> y:{a | x <= y} -> {v:a | v == y} @-}+(=<=) :: a -> a -> a+_ =<= y  = y++infixl 3 =>=+{-@ (=>=) :: x:a -> y:{a | x >= y}  -> {v:a | v == y} @-}+(=>=) :: a -> a -> a+_ =>= y  = y+++ ------------------------------------------------------------------------------- -- | Explicit equality -- 	`x ==? y ? p`@@ -103,16 +120,26 @@ -------------------------------------------------------------------------------  infixl 3 ==?-{-@ (==?) :: x:a -> y:a -> {v:Proof | x == y} -> {v:a | v == x && v == y} @-}-(==?) :: a -> a -> Proof -> a+{-@ (==?) :: x:a -> y:a -> {v:_ | x == y} -> {v:a | v == x && v == y} @-}+(==?) :: a -> a -> b -> a (==?) x _ _ = x +infixl 3 =<=?+{-@ (=<=?) :: x:a -> y:a -> {v:_ | x <= y} -> {v:a | v == y} @-}+(=<=?) :: a -> a -> b ->  a+(=<=?) _ y _ = y++infixl 3 =>=?+{-@ (=>=?) :: x:a -> y:a -> {v:_ | x >= y} -> {v:a | v == y} @-}+(=>=?) :: a -> a -> b -> a+(=>=?) _ y _  = y+ ------------------------------------------------------------------------------- -- | `?` is basically Haskell's $ and is used for the right precedence -------------------------------------------------------------------------------  infixl 3 ?-(?) :: (Proof -> a) -> Proof -> a+(?) :: (proof -> a) -> proof -> a f ? y = f y
include/Language/Haskell/Liquid/ProofCombinators.hs view
@@ -105,17 +105,17 @@ -- | Comparison operators requiring proof terms  (<=:) :: a -> a -> Proof -> a-{-@ (<=:) :: x:a -> y:a -> {v:Proof | x <= y } -> {v:a | v == x } @-}-(<=:) x _ _ = x+{-@ (<=:) :: x:a -> y:a -> {v:Proof | x <= y } -> {v:a | v == y } @-}+(<=:) _ y _ = y  (<:) :: a -> a -> Proof -> a-{-@ (<:) :: x:a -> y:a -> {v:Proof | x < y } -> {v:a | v == x } @-}-(<:) x _ _ = x+{-@ (<:) :: x:a -> y:a -> {v:Proof | x < y } -> {v:a | v == y } @-}+(<:) _ y _ = y   (>:) :: a -> a -> Proof -> a-{-@ (>:) :: x:a -> y:a -> {v:Proof | x >y } -> {v:a | v == x } @-}-(>:) x _ _ = x+{-@ (>:) :: x:a -> y:a -> {v:Proof | x > y } -> {v:a | v == y } @-}+(>:) _ y _ = y   (==:) :: a -> a -> Proof -> a@@ -169,30 +169,30 @@  instance (a~b) => OptLEq a (Proof -> b) where {-@ instance OptLEq a (Proof -> b) where-  <=. :: x:a -> y:a -> {v:Proof | x <= y} -> {v:b | v ~~ x }+  <=. :: x:a -> y:a -> {v:Proof | x <= y} -> {v:b | v ~~ y }   @-}-  (<=.) x _ _ = x+  (<=.) _ y _ = y  instance (a~b) => OptLEq a b where {-@ instance OptLEq a b where-  <=. :: x:a -> y:{a | x <= y} -> {v:b | v ~~ x }+  <=. :: x:a -> y:{a | x <= y} -> {v:b | v ~~ y }   @-}-  (<=.) x _ = x+  (<=.) _ y = y  class OptGEq a r where   (>=.) :: a -> a -> r  instance OptGEq a (Proof -> a) where {-@ instance OptGEq a (Proof -> a) where-  >=. :: x:a -> y:a -> {v:Proof| x >= y} -> {v:a | v == x }+  >=. :: x:a -> y:a -> {v:Proof| x >= y} -> {v:a | v == y }   @-}-  (>=.) x _ _ = x+  (>=.) _ y _ = y  instance OptGEq a a where {-@ instance OptGEq a a where-  >=. :: x:a -> y:{a| x >= y} -> {v:a | v == x  }+  >=. :: x:a -> y:{a| x >= y} -> {v:a | v == y  }   @-}-  (>=.) x _ = x+  (>=.) _ y = y   class OptLess a r where@@ -200,15 +200,15 @@  instance (a~b) => OptLess a (Proof -> b) where {-@ instance OptLess a (Proof -> b) where-  <. :: x:a -> y:a -> {v:Proof | x < y} -> {v:b | v ~~ x  }+  <. :: x:a -> y:a -> {v:Proof | x < y} -> {v:b | v ~~ y  }   @-}-  (<.) x _ _ = x+  (<.) _ y _ = y  instance (a~b) => OptLess a b where {-@ instance OptLess a b where-  <. :: x:a -> y:{a| x < y} -> {v:b | v ~~ x  }+  <. :: x:a -> y:{a| x < y} -> {v:b | v ~~ y  }   @-}-  (<.) x _ = x+  (<.) _ x = x   class OptGt a r where@@ -216,15 +216,15 @@  instance (a~b) => OptGt a (Proof -> b) where {-@ instance OptGt a (Proof -> b) where-  >. :: x:a -> y:a -> {v:Proof| x > y} -> {v:b | v ~~ x }+  >. :: x:a -> y:a -> {v:Proof| x > y} -> {v:b | v ~~ y }   @-}-  (>.) x _ _ = x+  (>.) _ y _ = y  instance (a~b) => OptGt a b where {-@ instance OptGt a b where-  >. :: x:a -> y:{a| x > y} -> {v:b | v ~~ x  }+  >. :: x:a -> y:{a| x > y} -> {v:b | v ~~ y  }   @-}-  (>.) x _ = x+  (>.) _ x = x   -------------------------------------------------------------------------------
liquidhaskell.cabal view
@@ -1,7 +1,6 @@ Name:                liquidhaskell-Version:             0.8.2.2+Version:             0.8.2.3 Copyright:           2010-17 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.-build-type:          Simple Synopsis:            Liquid Types for Haskell Description:         Liquid Types for Haskell. Homepage:            https://github.com/ucsd-progsys/liquidhaskell@@ -63,6 +62,10 @@   Description: use in-tree include directory   Default:     False +Flag deterministic-profiling+  Description: Support building against GHC with https://phabricator.haskell.org/D4388 backported+  Default:     False+ Executable liquid   default-language: Haskell98   Build-Depends: base >=4.8.1.0 && <5@@ -73,7 +76,7 @@                , deepseq                , pretty                , process-               , liquid-fixpoint >= 0.7.0.6+               , liquid-fixpoint >= 0.7.0.7                , located-base                , liquidhaskell                , hpc >= 0.6@@ -131,7 +134,7 @@                 , vector >= 0.10                 , hashable >= 1.2                 , unordered-containers >= 0.2-                , liquid-fixpoint >= 0.7.0.6+                , liquid-fixpoint >= 0.7.0.7                 , located-base                 , aeson >= 1.2 && < 1.3                 , bytestring >= 0.10@@ -148,6 +151,8 @@                 , QuickCheck >= 2.7                 , ghc-prim                 , hpc >= 0.6+                , gitrev+                , optparse-simple     hs-source-dirs:  src, include    Exposed-Modules: LiquidHaskell,@@ -280,6 +285,8 @@      hs-source-dirs: devel    if flag(devel)      ghc-options: -Werror+   if flag(deterministic-profiling)+     cpp-options: -DDETERMINISTIC_PROFILING    Default-Extensions: PatternGuards  test-suite test@@ -305,7 +312,7 @@                ,     tasty-rerun >= 1.1                ,     transformers >= 0.3                ,     syb-               ,     liquid-fixpoint >= 0.7.0.6+               ,     liquid-fixpoint >= 0.7.0.7                ,     hpc >= 0.6                ,     text @@ -327,7 +334,7 @@                ,     text                ,     transformers >= 0.3                ,     syb-               ,     liquid-fixpoint >= 0.7.0.6+               ,     liquid-fixpoint >= 0.7.0.7                ,     hpc >= 0.6    if flag(devel)@@ -346,7 +353,7 @@                 , ghc                 , ghc-boot                 , hashable >= 1.2-                , liquid-fixpoint >= 0.7.0.6+                , liquid-fixpoint >= 0.7.0.7                 , pretty                 , syb >= 0.4.4                 , time
src/Language/Haskell/Liquid/Bare.hs view
@@ -5,10 +5,10 @@ {-# LANGUAGE ViewPatterns              #-}  -- | This module contains the functions that convert /from/ descriptions of--- symbols, names and types (over freshly parsed /bare/ Strings),--- /to/ representations connected to GHC vars, names, and types.--- The actual /representations/ of bare and real (refinement) types are all--- in `RefType` -- they are different instances of `RType`+--   symbols, names and types (over freshly parsed /bare/ Strings),+--   /to/ representations connected to GHC vars, names, and types.+--   The actual /representations/ of bare and real (refinement) types are all+--   in `RefType` -- they are different instances of `RType`  module Language.Haskell.Liquid.Bare (     GhcSpec(..)@@ -33,6 +33,9 @@ import           TysWiredIn import           DataCon                                    (DataCon) import           InstEnv+import           FamInstEnv+import           TcRnDriver (runTcInteractive)+import           FamInst    (tcGetFamInstEnvs)  import           Control.Monad.Reader import           Control.Monad.State@@ -97,18 +100,44 @@             -> IO GhcSpec -------------------------------------------------------------------------------- makeGhcSpec cfg file name cbs tcs instenv vars defVars exports env lmap specs = do-  sp         <- throwLeft =<< execBare act initEnv-  let renv    = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) (ghcSpecEnv sp) wiredSortedSyms+  (fiTcs, fie) <- makeFamInstEnv env+  let act       = makeGhcSpec' cfg file cbs fiTcs tcs instenv vars defVars exports specs+  sp           <- throwLeft =<< execBare act (initEnv fie)+  let renv      = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) (ghcSpecEnv sp defVars) wiredSortedSyms   throwLeft . checkGhcSpec specs renv $ postProcess cbs renv sp   where-    act       = makeGhcSpec' cfg file cbs tcs instenv vars defVars exports specs-    throwLeft = either Ex.throw return-    lmap'     = case lmap of { Left e -> Ex.throw e; Right x -> x `mappend` listLMap}-    initEnv   = BE name mempty mempty mempty env lmap' mempty mempty mempty-                    (initAxSymbols name defVars specs)-                    (initPropSymbols specs)-                    cfg 0+    throwLeft   = either Ex.throw return+    lmap'       = case lmap of { Left e -> Ex.throw e; Right x -> x `mappend` listLMap}+    initEnv fie = BE { modName  = name+                     , tcEnv    = mempty+                     , rtEnv    = mempty+                     , varEnv   = mempty+                     , hscEnv   = env+                     , famEnv   = fie+                     , logicEnv = lmap'+                     , dcEnv    = mempty+                     , bounds   = mempty+                     , embeds   = mempty+                     , axSyms   = initAxSymbols name defVars specs+                     , propSyms = initPropSymbols specs+                     , beConfig = cfg+                     , beIndex  = 0+                     } +makeFamInstEnv :: HscEnv -> IO ([TyCon], M.HashMap Symbol DataCon)+makeFamInstEnv env = do+  famInsts <- getFamInstances env+  let fiTcs = [ tc            | FamInst { fi_flavor = DataFamilyInst tc } <- famInsts ]+  let fiDcs = [ (symbol d, d) | tc <- fiTcs, d <- tyConDataCons tc ]+  return      (fiTcs, F.notracepp "FAM-INST-TCS" $ M.fromList fiDcs)++getFamInstances :: HscEnv -> IO [FamInst]+getFamInstances env = do+  (_, Just (pkg_fie, home_fie)) <- runTcInteractive env tcGetFamInstEnvs+  return $ famInstEnvElts home_fie ++ famInstEnvElts pkg_fie+++ initAxSymbols :: ModName -> [Var] -> [(ModName, Ms.BareSpec)] -> M.HashMap Symbol LocSymbol initAxSymbols name vs = locMap .  Ms.reflects . fromMaybe mempty . lookup name   where@@ -160,15 +189,16 @@     addTCI'           = addTyConInfo gsTcEmbeds gsTyconEnv     allowHO           = higherOrderFlag gsConfig -ghcSpecEnv :: GhcSpec -> SEnv SortedReft-ghcSpecEnv sp        = res+ghcSpecEnv :: GhcSpec -> [Var] -> SEnv SortedReft+ghcSpecEnv sp defs   = res   where     res              = fromListSEnv binds     emb              = gsTcEmbeds sp-    binds            =  ([(x,        rSort t) | (x, Loc _ _ t) <- gsMeas sp])-                     ++ [(symbol v, rSort t) | (v, Loc _ _ t)  <- gsCtors sp]-                     ++ [(x,        vSort v) | (x, v)          <- gsFreeSyms sp,-                                                                  isConLikeId v ]+    binds            =  ([(x,       rSort t) | (x, Loc _ _ t) <- gsMeas sp])+                     ++ [(symbol v, rSort t) | (v, Loc _ _ t) <- gsCtors sp]+                     ++ [(x,        vSort v) | (x, v)         <- gsFreeSyms sp,+                                                                 isConLikeId v ]+                     ++ [(symbol x, vSort x) |  x  <- defs]     rSort t          = rTypeSortedReft emb t     vSort            = rSort . varRSort     varRSort         :: Var -> RSort@@ -206,9 +236,9 @@ --   as we need the inlines and aliases to properly `expand` the SpecTypes. -------------------------------------------------------------------------------- -makeLiftedSpec0 :: Config -> TCEmb TyCon -> [CoreBind] -> [TyCon] -> Ms.BareSpec+makeLiftedSpec0 :: Config -> ModName -> TCEmb TyCon -> [CoreBind] -> [TyCon] -> Ms.BareSpec                 -> BareM Ms.BareSpec-makeLiftedSpec0 cfg embs cbs defTcs mySpec = do+makeLiftedSpec0 cfg name embs cbs defTcs mySpec = do   xils      <- makeHaskellInlines  embs cbs mySpec   ms        <- makeHaskellMeasures embs cbs mySpec   let refTcs = reflectedTyCons cfg embs cbs mySpec@@ -217,7 +247,7 @@                 { Ms.ealiases  = lmapEAlias . snd <$> xils                 , Ms.measures  = F.notracepp "MS-MEAS" $ ms                 , Ms.reflects  = F.notracepp "MS-REFLS" $ Ms.reflects mySpec-                , Ms.dataDecls = F.notracepp "MS-DATADECL" $ makeHaskellDataDecls cfg mySpec tcs+                , Ms.dataDecls = F.notracepp "MS-DATADECL" $ makeHaskellDataDecls cfg name mySpec tcs                 }  -- sortUniquable :: (Uniquable a) => [a] -> [a]@@ -377,18 +407,16 @@  -------------------------------------------------------------------------------- makeGhcSpec'-  :: Config -> FilePath -> [CoreBind] -> [TyCon] -> Maybe [ClsInst] -> [Var] -> [Var]+  :: Config -> FilePath -> [CoreBind] -> [TyCon] -> [TyCon] -> Maybe [ClsInst] -> [Var] -> [Var]   -> NameSet -> [(ModName, Ms.BareSpec)]   -> BareM GhcSpec ---------------------------------------------------------------------------------makeGhcSpec' cfg file cbs tcs instenv vars defVars exports specs0 = do+makeGhcSpec' cfg file cbs fiTcs tcs instenv vars defVars exports specs0 = do   -- liftIO $ _dumpSigs specs0   name           <- modName <$> get   let mySpec      = fromMaybe mempty (lookup name specs0)--  embs           <- addClassEmbeds instenv tcs <$> (mconcat <$> mapM makeTyConEmbeds specs0)--  lSpec0         <- makeLiftedSpec0 cfg embs cbs tcs mySpec+  embs           <- addClassEmbeds instenv fiTcs <$> (mconcat <$> mapM makeTyConEmbeds specs0)+  lSpec0         <- makeLiftedSpec0 cfg name embs cbs tcs mySpec   let fullSpec    = mySpec `mappend` lSpec0   lmap           <- lmSymDefs . logicEnv    <$> get   let specs       = insert name fullSpec specs0@@ -418,7 +446,8 @@     -- The lifted-spec is saved in the next step     >>= makeGhcAxioms file name embs cbs su specs lSpec0 invs adts     >>= makeLogicMap-    >>= makeExactDataCons name cfg (snd <$> syms)+    -- RJ: AAAAAAARGHHH: this is duplicate of RT.strengthenDataConType+    -- >>= makeExactDataCons name cfg (snd <$> syms)     -- This step needs the UPDATED logic map, ie should happen AFTER makeLogicMap     >>= makeGhcSpec4 quals defVars specs name su syms     >>= addRTEnv@@ -434,32 +463,19 @@   rt <- rtEnv <$> get   return $ spec { gsRTAliases = rt } -makeExactDataCons :: ModName -> Config -> [Var] -> GhcSpec -> BareM GhcSpec-makeExactDataCons _n cfg vs spec-  | exactDC cfg = return $ spec { gsTySigs = gsTySigs spec ++ xts}-  | otherwise   = return   spec-  where-    xts         = makeDataConCtor <$> filter f vs-    f v         = GM.isDataConId v+-- RJ: AAAAAAARGHHH: this is duplicate of RT.strengthenDataConType+-- // _makeExactDataCons :: ModName -> Config -> [Var] -> GhcSpec -> BareM GhcSpec+-- // _makeExactDataCons _n cfg vs spec+  -- // | exactDC cfg = return $ spec { gsTySigs = gsTySigs spec ++ xts}+  -- // | otherwise   = return   spec+  -- // where+    -- // xts         = makeDataConCtor <$> filter f vs+    -- // f v         = GM.isDataConId v  varInModule :: (Show a, Show a1) => a -> a1 -> Bool varInModule n v = L.isPrefixOf (show n) $ show v -makeDataConCtor :: Var -> (Var, LocSpecType)-makeDataConCtor x = (x, dummyLoc . fromRTypeRep $ trep {ty_res = res, ty_binds = xs})-  where-    t    :: SpecType-    t    = ofType $ varType x-    trep = toRTypeRep t-    xs   = zipWith (\_ i -> (symbol ("x" ++ show i))) (ty_args trep) [1..] -    res  = ty_res trep `strengthen` MkUReft ref mempty mempty-    vv   = vv_-    x'   = symbol x-    ref  = Reft (vv, PAtom Eq (EVar vv) eq)-    eq   | null (ty_vars trep) && null xs = EVar x'-         | otherwise = mkEApp (dummyLoc x') (EVar <$> xs)- getReflects :: [(ModName, Ms.BareSpec)] -> [Symbol] getReflects  = fmap val . S.toList . S.unions . fmap (names . snd)   where@@ -484,7 +500,7 @@   let iAxs = getAxiomEqs specs                              -- axiom-eqs from IMPORTED modules   let axs  = mAxs ++ iAxs   _       <- makeLiftedSpec1 file name lSpec0 xts mAxs invs-  let xts' = xts ++ gsAsmSigs sp+  let xts' = xts ++ F.notracepp "GS-ASMSIGS" (gsAsmSigs sp)   let vts  = [ (v, t)        | (v, t) <- xts', let vx = GM.dropModuleNames $ symbol v, S.member vx rfls ]   let msR  = [ (symbol v, t) | (v, t) <- vts ]   let vs   = [ v             | (v, _) <- vts ]@@ -571,8 +587,8 @@              -> BareM GhcSpec makeGhcSpec1 syms vars defVars embs tyi exports name sigs asms cs' ms' cms' su sp   = do tySigs      <- makePluggedSigs name embs tyi exports $ tx sigs-       asmSigs     <- makePluggedAsmSigs embs tyi           $ tx asms-       ctors       <- makePluggedAsmSigs embs tyi           $ tx cs'+       asmSigs     <- F.notracepp "MAKE-ASSUME-SPEC-3" <$> (makePluggedAsmSigs embs tyi           $ tx asms)+       ctors       <- F.notracepp "MAKE-CTORS-SPEC"    <$> (makePluggedAsmSigs embs tyi           $ tx cs' )        return $ sp { gsTySigs   = filter (\(v,_) -> v `elem` vs) tySigs                    , gsAsmSigs  = filter (\(v,_) -> v `elem` vs) asmSigs                    , gsCtors    = filter (\(v,_) -> v `elem` vs) ctors@@ -744,20 +760,21 @@                           , [(Var, LocSpecType)]                           , [(Var, LocSpecType)] ) makeGhcSpecCHOP3 cfg vars defVars specs name mts embs = do-  sigs'    <- mconcat <$> mapM (makeAssertSpec name cfg vars defVars) specs-  asms'    <- mconcat <$> mapM (makeAssumeSpec name cfg vars defVars) specs+  sigs'    <- F.notracepp "MAKE-ASSERT-SPEC-1" <$> (mconcat <$> mapM (makeAssertSpec name cfg vars defVars) specs)+  asms'    <- F.notracepp "MAKE-ASSUME-SPEC-1" . Misc.fstByRank . mconcat <$> mapM (makeAssumeSpec name cfg vars defVars) specs   invs     <- mconcat <$> mapM makeInvariants specs   ialias   <- mconcat <$> mapM makeIAliases   specs   ntys     <- mconcat <$> mapM makeNewTypes   specs   let dms   = makeDefaultMethods vars mts   tyi      <- gets tcEnv   let sigs  = [ (x, txRefSort tyi embs $ fmap txExpToBind t) | (_, x, t) <- sigs' ++ mts ++ dms ]-  let asms  = [ (x, txRefSort tyi embs $ fmap txExpToBind t) | (_, x, t) <- asms' ]-  let hms   = concatMap (S.toList . Ms.hmeas . snd) (filter ((==name) . fst) specs)+  let asms  = F.notracepp "MAKE-ASSUME-SPEC-2" [ (x, txRefSort tyi embs $ fmap txExpToBind t) | (_, x, t) <- asms' ]+  let hms   = concatMap (S.toList . Ms.hmeas . snd) (filter ((== name) . fst) specs)   let minvs = makeMeasureInvariants sigs hms-  checkDuplicateSigs sigs -- separate checks as assumes are supposed to "override" other sigs. +  checkDuplicateSigs sigs -- separate checks as assumes are supposed to "override" other sigs.   -- checkDuplicateSigs asms   return     (invs ++ minvs, ntys, ialias, sigs, asms)+  checkDuplicateSigs :: [(Var, LocSpecType)] -> BareM () checkDuplicateSigs xts = case Misc.uniqueByKey symXs  of
src/Language/Haskell/Liquid/Bare/Axiom.hs view
@@ -3,6 +3,9 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances    #-} +-- | This module contains the code that DOES reflection; i.e. converts Haskell+--   definitions into refinements.+ module Language.Haskell.Liquid.Bare.Axiom   ( makeHaskellAxioms )   where@@ -84,7 +87,8 @@ mkError x str = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)  makeAssumeType-  :: F.TCEmb TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType ->  Var -> CoreExpr+  :: F.TCEmb TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType+  -> Var -> CoreExpr   -> (LocSpecType, AxiomEq) makeAssumeType tce lmap dm x mbT v def   = (x {val = at `strengthenRes` F.subst su ref},  F.mkEquation (val x) xts le out)
src/Language/Haskell/Liquid/Bare/Check.hs view
@@ -190,7 +190,7 @@     err1s                  = checkDuplicateRTAlias msg as  checkBind :: (PPrint v) => Bool -> String -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> (v, Located SpecType) -> Maybe Error-checkBind allowHO s emb tcEnv env' (v, t) = checkTy allowHO msg emb tcEnv env' t+checkBind allowHO s emb tcEnv env (v, t) = checkTy allowHO msg emb tcEnv env t   where     msg                      = ErrTySpec (fSrcSpan t) (text s <+> pprint v) (val t) @@ -216,6 +216,8 @@  checkTy :: Bool -> (Doc -> Error) -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> Located SpecType -> Maybe Error checkTy allowHO mkE emb tcEnv env t = mkE <$> checkRType allowHO emb env (val $ txRefSort tcEnv emb t)+  where+    _msg =  "CHECKTY: " ++ showpp (val t)  checkDupIntersect     :: [(Var, Located SpecType)] -> [(Var, Located SpecType)] -> [Error] checkDupIntersect xts asmSigs = concatMap mkWrn {- trace msg -} dups@@ -400,7 +402,7 @@ checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))                              => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc checkReft _   _   Nothing _  = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.-checkReft env emb (Just t) _ = (dr $+$) <$> checkSortedReftFull env r+checkReft env emb (Just t) _ = (\z -> dr $+$ z {- $+$ text "In environment" $+$ nest 4 (pprint env) -}) <$> checkSortedReftFull env r   where     r                        = rTypeSortedReft emb t     dr                       = text "Sort Error in Refinement:" <+> pprint r
src/Language/Haskell/Liquid/Bare/DataType.hs view
@@ -67,7 +67,7 @@ -- | makeClassEmbeds: sort-embeddings for numeric, and family-instance tycons -------------------------------------------------------------------------------- addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> F.TCEmb TyCon -> F.TCEmb TyCon-addClassEmbeds instenv tcs = makeFamInstEmbeds tcs . makeNumEmbeds instenv+addClassEmbeds instenv fiTcs = makeFamInstEmbeds fiTcs . makeNumEmbeds instenv  -------------------------------------------------------------------------------- -- | makeFamInstEmbeds : embed family instance tycons, see [NOTE:FamInstEmbeds]@@ -76,18 +76,20 @@ --   with the actual family instance  types that have numeric instances as int [Check!] -------------------------------------------------------------------------------- makeFamInstEmbeds :: [TyCon] -> F.TCEmb TyCon -> F.TCEmb TyCon-makeFamInstEmbeds cs embs = L.foldl' embed embs famInstSorts+makeFamInstEmbeds cs0 embs = L.foldl' embed embs famInstSorts   where     famInstSorts          = F.notracepp "famInstTcs"                             [ (c, RT.typeSort embs ty)-                                | c        <- cs-                                , (c', ts) <- tcInsts c-                                , let n     = tyConArity c-                                , let ty    = famInstType n c' ts ]-    tcInsts               = maybeToList . tyConFamInst_maybe+                                | c   <- cs+                                , ty  <- maybeToList (famInstTyConType c) ]     embed embs (c, t)     = M.insert c t embs-    -- tcSorts               = maybeToList . famInstSort embs+    cs                    = F.notracepp "famInstTcs-all" cs0 +famInstTyConType :: TyCon -> Maybe Type+famInstTyConType c = case tyConFamInst_maybe c of+  Just (c', ts) -> Just (famInstType (tyConArity c) c' ts)+  Nothing       -> Nothing+ famInstType :: Int -> TyCon -> [Type] -> Type famInstType n c ts = Type.mkTyConApp c (take (length ts - n) ts) @@ -297,7 +299,7 @@                -> [F.DataField] makeDataFields tce c as xts = [ F.DField x (fSort t) | (x, t) <- xts]   where-    su                      = zip (rtyVarUniqueSymbol <$> as) [0..]+    su                      = zip ({- rtyVarUniqueSymbol -} F.symbol <$> as) [0..]     fSort                   = muSort c (length as) . F.substVars su . RT.rTypeSort tce  muSort :: F.FTycon -> Int -> F.Sort -> F.Sort@@ -385,7 +387,7 @@               -> BareM ( [(ModName, TyCon, TyConP, Maybe DataPropDecl)]                        , [[(DataCon, Located DataConP)]]) makeConTypes' name dcs vdcs = do-  dcs' <- canonizeDecls dcs+  dcs' <- F.notracepp "CANONIZED-DECLS" <$> canonizeDecls dcs   unzip <$> mapM (uncurry (ofBDataDecl name)) (groupVariances dcs' vdcs)  -- | 'canonizeDecls ds' returns a subset of 'ds' with duplicates, e.g. arising@@ -458,7 +460,7 @@     msg               = ppVar c <+> "is not the type constructor"  checkDataCtor :: DataCtor -> BareM ()-checkDataCtor (DataCtor lc xts _)+checkDataCtor (DataCtor lc _ xts _)   | x : _ <- dups = Ex.throw (err lc x :: UserError)   | otherwise     = return ()     where@@ -557,26 +559,38 @@             -> [PVar RSort]             -> DataCtor             -> BareM (DataCon, DataConP)-ofBDataCtor name l l' tc αs ps ls πs (DataCtor c xts res) = do+ofBDataCtor name l l' tc αs ps ls πs (DataCtor c _ xts res) = do   c'           <- lookupGhcDataCon c   ts'          <- mapM (mkSpecType' l ps) ts   res'         <- mapM (mkSpecType' l ps) res-  let cs        = RT.ofType <$> dataConStupidTheta c'-  let t0'       = dataConResultTy c' αs t0 res'+  let t0'       = F.notracepp ("dataConResultTy c' = " ++ show c' ++ " res' = " ++ show res') $ dataConResultTy c' αs t0 res'   cfg          <- gets beConfig   let (yts, ot) = F.notracepp ("OFBDataCTOR: " ++ show c' ++ " " ++ show (isVanillaDataCon c', res') ++ " " ++ show isGadt)                 $ qualifyDataCtor (exactDC cfg && not isGadt) name dLoc (zip xs ts', t0')   let zts       = zipWith (normalizeField c') [1..] (reverse yts)++  let usedTvs   = S.fromList (ty_var_value <$> concatMap RT.freeTyVars (t0':ts'))+  -- let cs        = RT.ofType <$> dataConStupidTheta c'+  let cs        = [ p | p <- RT.ofType <$> dataConTheta c', keepPredType usedTvs p ]   return          (c', DataConP l αs πs ls cs zts ot isGadt (F.symbol name) l')   where-    (xs, ts) = unzip xts-    t0       = RT.gApp tc αs πs+    (xs, ts)    = unzip xts+    t0          = case famInstTyConType tc of+                    Nothing -> RT.gApp tc αs πs+                    Just ty -> RT.ofType ty     -- nFlds    = length xts     -- rs       = [RT.rVar α | RTV α <- αs]     -- t0       = F.tracepp "t0 = " $ RT.rApp tc rs (rPropP [] . pdVarReft <$> πs) mempty -- 1089 HEREHERE use the SPECIALIZED type?-    isGadt   = isJust res-    dLoc     = F.Loc l l' ()+    isGadt      = isJust res+    dLoc        = F.Loc l l' () ++keepPredType :: S.HashSet RTyVar -> SpecType -> Bool+keepPredType tvs p+  | Just (tv, _) <- eqSubst p = S.member tv tvs+  | otherwise                 = True++ -- | This computes the result of a `DataCon` application. --   For 'isVanillaDataCon' we can just use the `TyCon` --   applied to the relevant tyvars.@@ -588,7 +602,7 @@ dataConResultTy _ _ _ (Just t) = t dataConResultTy c αs t _   | isVanillaDataCon c         = t-  | False                      = F.tracepp "RESULT-TYPE:" $ RT.subsTyVars_meet (gadtSubst αs c) t+  | False                      = F.notracepp "RESULT-TYPE:" $ RT.subsTyVars_meet (gadtSubst αs c) t dataConResultTy c _ _ _        = RT.ofType t   where     (_,_,_,_,_,t)              = {- GM.tracePpr ("FULL-SIG:" ++ show c ++ " -- repr : " ++ GM.showPpr (_tr0, _tr1, _tr2)) $ -} dataConFullSig c@@ -636,17 +650,12 @@  qualifyField :: ModName -> LocSymbol -> (Maybe F.Symbol, F.Symbol) qualifyField name lx- | needsQual = (Just x, F.notracepp msg $ qualifyName name x)+ | needsQual = (Just x, F.notracepp msg $ qualifyModName name x)  | otherwise = (Nothing, x)  where    msg       = "QUALIFY-NAME: " ++ show x ++ " in module " ++ show (F.symbol name)    x         = val lx    needsQual = not (isWiredIn lx)--qualifyName :: ModName -> F.Symbol -> F.Symbol-qualifyName n = GM.qualifySymbol nSym- where-   nSym       = F.symbol n  makeTyConEmbeds :: (ModName,Ms.Spec ty bndr) -> BareM (F.TCEmb TyCon) makeTyConEmbeds (mod, spec)
src/Language/Haskell/Liquid/Bare/Env.hs view
@@ -35,6 +35,7 @@ import           Prelude                              hiding (error) import           Text.Parsec.Pos import           TyCon+import           DataCon import           Var  import           Control.Monad.Except@@ -83,6 +84,7 @@   , rtEnv    :: !RTEnv   , varEnv   :: !(M.HashMap F.Symbol Var)   , hscEnv   :: !(HscEnv)+  , famEnv   :: !(M.HashMap F.Symbol DataCon)     -- ^ see NOTE:Family-Instance-Environment   , logicEnv :: !LogicMap   , dcEnv    :: !DataConMap   , bounds   :: !(RBEnv)@@ -92,6 +94,17 @@   , beConfig :: !Config   , beIndex  :: !Integer   }++{- | [NOTE:Family-Instance-Environment]+     For some reason, the usual lookup machinery (lookupGhcThing) refuses+     to properly lookup _imported_ names of family-instance data-constructors.+     e.g. see tests/pos/ExactGADT8.hs and tests/pos/ExactGADT9.hs; inside the latter,+     the lookupGhcThing fails to resolve the name of `BlobXVal` (but it works just fine+     when BlobXVal is a plain DataCon as in tests/pos/ExactGADT8a.hs+     To get around this hassle, we also save a map from _family instance_ DataCon-names+     to the corresponding family instance Tycon in the `famEnv` field of BareEnv.+     This map is *created* inside the function FIXME, and *used* inside the function FIXME.+ -}  instance Freshable BareM Integer where   fresh = do s <- get
src/Language/Haskell/Liquid/Bare/Expand.hs view
@@ -119,7 +119,7 @@ expandSym' s = do   axs <- gets axSyms   let s' = dropModuleNamesAndUnique s-  return $ if M.member s' axs then {- tracepp "EXPANDSYM" -} s' else s+  return $ if M.member s' axs then s' else s  expandEApp :: F.SourcePos -> (Expr, [Expr]) -> BareM Expr expandEApp sp (EVar f, es) = do
src/Language/Haskell/Liquid/Bare/Lookup.hs view
@@ -95,24 +95,19 @@ lookupGhcThing' _err f ns x = do   be     <- get   let env = hscEnv be---   _      <- liftIO $ putStrLn ("lookupGhcThing: PRE " ++ symbolicString x)   ns     <- liftIO $ lookupName env (modName be) ns x---   _      <- liftIO $ putStrLn ("lookupGhcThing: POST " ++ symbolicString x ++ show ns)-  -- mts    <- liftIO $ mapM (fmap (join . fmap f) . hscTcRcLookupName env) ns   ts     <- liftIO $ catMaybes <$> mapM (hscTcRcLookupName env) ns-  let kts = catMaybes (f <$> ts)+  ts'    <- map (AConLike . RealDataCon)  . lookupEnv x <$> gets famEnv+  -- _      <- liftIO $ putStrLn ("lookupGhcThing: POST " ++ symbolicString x ++ show [(n, getSrcSpan n) | n <- ns] ++ GM.showPpr ts ++ GM.showPpr ts')+  let kts = catMaybes (f <$> (ts ++ ts'))   -- hscTcRcLookupName :: HscEnv -> Name -> IO (Maybe TyThing)   case Misc.nubHashOn showpp (minBy kts) of     []  -> return Nothing     [z] -> return (Just z)     zs  -> uError $ ErrDupNames (srcSpan x) (pprint (F.symbol x)) (pprint <$> zs) -  -- case filterByName x $ nubHashOn showpp $ catMaybes mts of-    -- []  -> return Nothing-    -- [z] -> return (Just z)-    -- zs  -> case filterByName x zs of-             -- [] -> uError $ ErrDupNames (srcSpan x) (pprint (F.symbol x)) (pprint <$> zs)-+lookupEnv :: (GhcLookup a) => a -> M.HashMap F.Symbol b -> [b]+lookupEnv x env = maybeToList (M.lookup (F.symbol x) env)  minBy :: [(Int, a)] -> [a] minBy kvs = case kvs' of@@ -251,7 +246,6 @@     fv (AConLike (RealDataCon x)) = Just (1, dataConWorkId x)     fv _                          = Nothing - lookupGhcDnTyCon :: String -> DataName -> BareM TyCon lookupGhcDnTyCon src (DnName s)                    = lookupGhcThing err ftc (Just tcName) s@@ -259,22 +253,30 @@     err            = "type constructor " ++ src     ftc (ATyCon x) = Just (0, x)     ftc (AConLike (RealDataCon x))-              --      | GM.showPpr x == "GHC.Types.[]"-                   = Just (1, {- GM.tracePpr ("lookupGHCTC1 s =" ++ symbolicIdent s ++ " " ++ show ok) $ -}-                              dataConTyCon x)+                   = Just (1, dataConTyCon x)       where         res        = dataConTyCon x         _ok        = res == listTyCon-    ftc _z         = {- GM.tracePpr ("lookupGhcDnTyCon s = " ++ show s ++ "result = " ++ GM.showPpr z) -}-                     Nothing+    ftc _z         = GM.notracePpr ("lookupGhcDnTyCon 1 s = " ++ show s ++ "result = " ++ GM.showPpr _z)+                     $ Nothing  lookupGhcDnTyCon src (DnCon  s)                    = lookupGhcThing err ftc (Just tcName) s   where-    err            = "type constructor " ++ src+    err            = "type konstructor " ++ src     ftc (AConLike (RealDataCon x))-                   = Just (1, dataConTyCon x)-    ftc _          = Nothing+                   = GM.notracePpr ("lookupGhcDnTyCon 1 s = " ++ show s ++ "result = " ++ GM.showPpr x)+                     $ Just (1, dataConTyCon x)+    ftc (AConLike _z)+                   = GM.notracePpr ("lookupGhcDnTyCon 2 s = " ++ show s ++ "result = " ++ GM.showPpr _z)+                     $ Nothing+    ftc (AnId _z)+                   = GM.notracePpr ("lookupGhcDnTyCon 3 s = " ++ show s ++ "result = " ++ GM.showPpr _z)+                     $ Nothing+    ftc (ATyCon _z) = GM.notracePpr ("lookupGhcDnTyCon 4 s = " ++ show s ++ "result = " ++ GM.showPpr _z)+                     $ Nothing+    ftc _z          = GM.notracePpr ("lookupGhcDnTyCon 5 s = " ++ show s ++ "result = " ++ GM.showPpr _z)+                     $ Nothing  lookupGhcTyCon   ::  GhcLookup a => String -> a -> BareM TyCon lookupGhcTyCon src s = do
src/Language/Haskell/Liquid/Bare/Measure.hs view
@@ -42,20 +42,21 @@ import Data.Traversable (forM, mapM) import Text.PrettyPrint.HughesPJ (text) import Text.Parsec.Pos (SourcePos)-+import Text.Printf     (printf) import qualified Data.List as L  import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S -import Language.Fixpoint.Misc (mlookup, sortNub, groupList, mapSnd, mapFst) import Language.Fixpoint.Types (Symbol, dummySymbol, symbolString, symbol, Expr(..), meet) import Language.Fixpoint.SortCheck (isFirstOrder)  import qualified Language.Fixpoint.Types as F  import           Language.Haskell.Liquid.Transforms.CoreToLogic-import           Language.Haskell.Liquid.Misc+import qualified Language.Fixpoint.Misc                as Misc+import qualified Language.Haskell.Liquid.Misc          as Misc+import           Language.Haskell.Liquid.Misc             ((.||.)) import qualified Language.Haskell.Liquid.GHC.Misc      as GM import qualified Language.Haskell.Liquid.Types.RefType as RT import           Language.Haskell.Liquid.Types@@ -70,11 +71,12 @@ import           Language.Haskell.Liquid.Bare.ToBare  ---------------------------------------------------------------------------------makeHaskellDataDecls :: Config -> Ms.BareSpec -> [TyCon] -> [DataDecl]+makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [TyCon] -> [DataDecl] ---------------------------------------------------------------------------------makeHaskellDataDecls cfg spec tcs+makeHaskellDataDecls cfg name spec tcs   | exactDC cfg = mapMaybe tyConDataDecl-                . zipMap   (hasDataDecl spec . fst)+                . F.notracepp "makeHaskellDataDecls-1"+                . zipMap   (hasDataDecl name spec . fst)                 . liftableTyCons                 . filter isReflectableTyCon                 $ tcs@@ -99,13 +101,22 @@ zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)] zipMapMaybe f = mapMaybe (\x -> (x, ) <$> f x) -hasDataDecl :: Ms.BareSpec -> TyCon -> HasDataDecl-hasDataDecl spec = \tc -> M.lookupDefault def (tcName tc) decls+hasDataDecl :: ModName -> Ms.BareSpec -> TyCon -> HasDataDecl+hasDataDecl mod spec+                 = \tc -> F.notracepp (msg tc) $ M.lookupDefault def (tcName tc) decls   where+    msg tc       = "hasDataDecl " ++ show (tcName tc)     def          = NoDecl Nothing-    tcName       = tyConDataName False-    decls        = M.fromList [ (Just (tycName d), hasDecl d) | d <- Ms.dataDecls spec ]+    tcName       = fmap (qualifiedDataName mod) . tyConDataName True -- False+    dcName       =       qualifiedDataName mod  . tycName+    decls        = M.fromList [ (Just dn, hasDecl d)+                                | d     <- Ms.dataDecls spec+                                , let dn = dcName d] +qualifiedDataName :: ModName -> DataName -> DataName+qualifiedDataName mod (DnName lx) = DnName (qualifyModName mod <$> lx)+qualifiedDataName mod (DnCon  lx) = DnCon  (qualifyModName mod <$> lx)+ {-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-} tyConDataDecl :: ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl tyConDataDecl (_, HasDecl)@@ -132,17 +143,25 @@   where     post       = if full then id else GM.dropModuleNamesAndUnique     vanillaTc  = isVanillaAlgTyCon tc-    dcs        = F.notracepp msg $ tyConDataCons tc-    msg        = "tyConDataCons tc = " ++ F.showpp tc+    dcs        = Misc.sortOn symbol (tyConDataCons tc)  dataConDecl :: DataCon -> DataCtor-dataConDecl d  = DataCtor dx xts Nothing+dataConDecl d     = F.notracepp msg $ DataCtor dx [] xts Nothing+-- dataConDecl d     = F.tracepp msg $ DataCtor dx (RT.bareOfType <$> ps) xts outT   where-    xts        = [(makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]-    dx         = symbol <$> GM.locNamedThing d-    its        = zip [1..] ts-    (_,_,ts,_) = dataConSig d+    isGadt        = not (isVanillaDataCon d)+    msg           = printf "dataConDecl (gadt = %s)" (show isGadt)+    xts           = [(makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]+    dx            = symbol <$> GM.locNamedThing d+    its           = zip [1..] ts+    (_,_ps,ts,t)   = dataConSig d+    _outT :: Maybe BareType+    _outT+      | isGadt    = Just (RT.bareOfType t)+      | otherwise = Nothing ++ -------------------------------------------------------------------------------- makeHaskellMeasures :: F.TCEmb TyCon -> [CoreBind] -> Ms.BareSpec                     -> BareM [Measure (Located BareType) LocSymbol]@@ -206,7 +225,7 @@  strengthenHaskell :: (Var -> SpecType) -> S.HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)] strengthenHaskell strengthen hmeas sigs-  = go <$> groupList (reverse sigs ++ hsigs)+  = go <$> Misc.groupList (reverse sigs ++ hsigs)   where     hsigs      = [(val x, x {val = strengthen $ val x}) | x <- S.toList hmeas]     go (v, xs) = (v,) $ L.foldl1' (flip meetLoc) xs@@ -221,8 +240,8 @@  makeMeasureSelectors :: Config -> DataConMap -> (DataCon, Located DataConP) -> [Measure SpecType DataCon] makeMeasureSelectors cfg dm (dc, Loc l l' (DataConP _ _vs _ps _ _ xts _resTy isGadt _ _))-  = (condNull (exactDC cfg) $ checker : catMaybes (go' <$> fields)) --  internal measures, needed for reflection- ++ (condNull (autofields)  $           catMaybes (go  <$> fields)) --  user-visible measures.+  = (Misc.condNull (exactDC cfg) $ checker : catMaybes (go' <$> fields)) --  internal measures, needed for reflection+ ++ (Misc.condNull (autofields)  $           catMaybes (go  <$> fields)) --  user-visible measures.   where     autofields = not (isGadt || noMeasureFields cfg)     go ((x, t), i)@@ -252,7 +271,7 @@  dataConSel dc n (Proj i) = mkArrow as [] [] [xt] (mempty <$> ti)   where-    ti                   = fromMaybe err $ getNth (i-1) ts+    ti                   = fromMaybe err $ Misc.getNth (i-1) ts     (as, ts, xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon dc n     err                  = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields" @@ -260,7 +279,7 @@ bkDataCon :: (F.Reftable r) => DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (Symbol, RRType r, r)) bkDataCon dc nFlds  = (as, ts, (dummySymbol, t, mempty))   where-    ts                = RT.ofType <$> takeLast nFlds _ts+    ts                = RT.ofType <$> Misc.takeLast nFlds _ts     t                 = {- traceShow ("bkDataConResult" ++ GM.showPpr (_t, t0)) $ -}                         RT.ofType  $ mkTyConApp tc tArgs'     as                = makeRTVar . RT.rTyVar <$> αs@@ -314,7 +333,7 @@  makeMeasureSpec' :: MSpec SpecType DataCon                  -> ([(Var, SpecType)], [(LocSymbol, RRType F.Reft)])-makeMeasureSpec' = mapFst (mapSnd RT.uRType <$>) . Ms.dataConTypes . first (mapReft ur_reft)+makeMeasureSpec' = Misc.mapFst (Misc.mapSnd RT.uRType <$>) . Ms.dataConTypes . first (mapReft ur_reft)  makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t                      -> [(LocSymbol, CMeasure (RType c tv r2))]@@ -332,11 +351,11 @@ mkMeasureDCon_ m ndcs = m' {Ms.ctorMap = cm'}   where     m'                = fmap (tx.val) m-    cm'               = hashMapMapKeys (symbol . tx) $ Ms.ctorMap m'-    tx                = mlookup (M.fromList ndcs)+    cm'               = Misc.hashMapMapKeys (symbol . tx) $ Ms.ctorMap m'+    tx                = Misc.mlookup (M.fromList ndcs)  measureCtors ::  Ms.MSpec t LocSymbol -> [LocSymbol]-measureCtors = sortNub . fmap ctor . concat . M.elems . Ms.ctorMap+measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap  mkMeasureSort ::  Ms.MSpec BareType LocSymbol -> BareM (Ms.MSpec SpecType LocSymbol) mkMeasureSort (Ms.MSpec c mm cm im)@@ -347,9 +366,9 @@        txDef :: Def BareType ctor -> BareM (Def SpecType ctor)       txDef def = liftM3 (\xs t bds-> def{ dparams = xs, dsort = t, binds = bds})-                  (mapM (mapSndM ofMeaSort) (dparams def))+                  (mapM (Misc.mapSndM ofMeaSort) (dparams def))                   (mapM ofMeaSort $ dsort def)-                  (mapM (mapSndM $ mapM ofMeaSort) (binds def))+                  (mapM (Misc.mapSndM $ mapM ofMeaSort) (binds def))   varMeasures :: (Monoid r) => [Var] -> [(Symbol, Located (RRType r))]
src/Language/Haskell/Liquid/Bare/Misc.hs view
@@ -128,9 +128,10 @@ -- Renaming Type Variables in Haskell Signatures ------------------------------ ------------------------------------------------------------------------------- -data MapTyVarST = MTVST { vmap   :: [(Var, RTyVar)]-                        , errmsg :: Error-                        }+data MapTyVarST = MTVST+  { vmap   :: [(Var, RTyVar)]+  , errmsg :: Error+  }  initMapSt :: Error -> MapTyVarST initMapSt = MTVST []
src/Language/Haskell/Liquid/Bare/OfType.hs view
@@ -50,16 +50,18 @@  -------------------------------------------------------------------------------- ofBareType :: SourcePos -> BareType -> BareM SpecType-ofBareType l-  = ofBRType expandRTAliasApp (resolve l <=< expand l)+ofBareType l bt+  = {- F.tracepp msg <$> -} ofBRType expandRTAliasApp (resolve l <=< expand l) bt+  -- where msg = "OF-BARETYPE: " ++ F.showpp bt + ofMeaSort :: BareType -> BareM SpecType ofMeaSort-  = ofBRType failRTAliasApp {- _expandRTAliasApp_ -} return+  = ofBRType failRTAliasApp return  ofBSort :: BSort -> BareM RSort ofBSort-  = ofBRType failRTAliasApp {- _expandRTAliasApp_ -} return+  = ofBRType failRTAliasApp return   --------------------------------------------------------------------------------@@ -195,7 +197,7 @@  _expandRTAliasApp_ :: SourcePos -> RTAlias RTyVar SpecType -> [BSort] -> () -> BareM RSort _expandRTAliasApp_ l rta args _ = do-  res <- expandRTAliasApp l rta ([ const mempty <$> t | t <- args] ) mempty +  res <- expandRTAliasApp l rta ([ const mempty <$> t | t <- args] ) mempty   return (void res)  expandRTAliasApp :: SourcePos -> RTAlias RTyVar SpecType -> [BareType] -> RReft -> BareM SpecType@@ -210,8 +212,8 @@          return  $ F.subst esu . (`strengthen` r) . subsTyVars_meet tsu $ rtBody rta    where-    αs        = rtTArgs rta-    εs        = rtVArgs rta+    (αs, εs)  = F.notracepp _msg (rtTArgs rta, rtVArgs rta)+    _msg      = "EXPAND-RTALIAS-APP: " ++ F.showpp (rtName rta)     err       :: Doc -> Error     err       = ErrAliasApp (sourcePosSrcSpan l)                             (pprint $ rtName rta)
src/Language/Haskell/Liquid/Bare/Plugged.hs view
@@ -28,7 +28,8 @@ import qualified Data.HashMap.Strict as M  import Language.Fixpoint.Types.Names (dummySymbol)-import qualified Language.Fixpoint.Types as F+import qualified Language.Fixpoint.Types         as F+import qualified Language.Fixpoint.Types.Visitor as F -- import Language.Fixpoint.Types (traceFix, showFix) -- import Language.Fixpoint.Misc (traceShow) @@ -42,11 +43,12 @@ import Language.Haskell.Liquid.Bare.Env import Language.Haskell.Liquid.Bare.Misc ---- NOTE: Be *very* careful with the use functions from RType -> GHC.Type,--- e.g. toType, in this module as they cannot handle LH type holes. Since--- this module is responsible for plugging the holes we obviously cannot--- assume, as in e.g. L.H.L.Constraint.* that they do not appear.+--------------------------------------------------------------------------------+-- | NOTE: Be *very* careful with the use functions from RType -> GHC.Type,+--   e.g. toType, in this module as they cannot handle LH type holes. Since+--   this module is responsible for plugging the holes we obviously cannot+--   assume, as in e.g. L.H.L.Constraint.* that they do not appear.+--------------------------------------------------------------------------------  makePluggedSigs :: ModName                 -> F.TCEmb TyCon@@ -104,12 +106,14 @@                                     -- NOTE: this use of toType is safe as rt' is derived from t.   = 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''+                    Right s -> return (vmap s)+       let su    = F.notracepp ("MAKE-ASSUME-SPEC-4: " ++ show x) [(y, rTyVar x) | (x, y) <- tyvsmap]+           coSub = F.notracepp ("MAKE-ASSUME-SPEC-5: " ++ show x) $ M.fromList [(F.symbol y, F.FObj (F.symbol x)) | (y, x) <- su]+           st3   = subts su st''+           st4   = mapExprReft (F.applyCoSub coSub) st3            ps'   = fmap (subts su') <$> ps            su'   = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)]-       Loc l l' . mkArrow (updateRTVar <$> αs) ps' (ls1 ++ ls2) [] . makeCls cs' <$> (go rt' st''')+       Loc l l' . mkArrow (updateRTVar <$> αs) ps' (ls1 ++ ls2) [] . makeCls cs' <$> (go rt' st4)   where     (αs, _, ls1, rt)  = bkUniv (ofType (expandTypeSynonyms t) :: SpecType)     (cs, rt')         = bkClass rt
src/Language/Haskell/Liquid/Bare/Spec.hs view
@@ -44,17 +44,15 @@ import qualified Data.HashSet                               as S import qualified Data.HashMap.Strict                        as M ---import           Language.Fixpoint.Misc                     (group, snd3, groupList)--+import qualified Language.Fixpoint.Misc                     as Misc import qualified Language.Fixpoint.Types                    as F+import qualified Language.Fixpoint.Types.Visitor            as F+ import           Language.Haskell.Liquid.Types.Dictionaries import           Language.Haskell.Liquid.GHC.Misc import           Language.Haskell.Liquid.Misc import           Language.Haskell.Liquid.Types.RefType-import           Language.Haskell.Liquid.Types+import           Language.Haskell.Liquid.Types              hiding (freeTyVars) import           Language.Haskell.Liquid.Types.Bounds  import qualified Language.Haskell.Liquid.Measure            as Ms@@ -145,7 +143,7 @@ varSymbols :: ([Var] -> [Var]) -> [Var] -> [(LocSymbol, a)] -> BareM [(Var, a)] varSymbols f vs = concatMapM go   where-    lvs         = M.map L.sort $ group [(sym v, locVar v) | v <- vs]+    lvs         = M.map L.sort $ Misc.group [(sym v, locVar v) | v <- vs]     sym         = dropModuleNames . F.symbol . showPpr     locVar v    = (getSourcePos v, v)     go (s, ns)  = case M.lookup (val s) lvs of@@ -216,7 +214,7 @@     , "$dm" `F.isPrefixOfSym` dropModuleNames dm     , let mod = takeModuleNames dm     , let method = qualifySymbol mod $ F.dropSym 3 (dropModuleNames dm)-    , let mb = L.find ((method `F.isPrefixOfSym`) . F.symbol . snd3) sigs+    , let mb = L.find ((method `F.isPrefixOfSym`) . F.symbol . Misc.snd3) sigs     , isJust mb     , let Just (m,_,t) = mb     ]@@ -256,13 +254,23 @@       | ignoreUnknown       = return Nothing     handleError err-      = throwError $ F.tracepp "HANDLE-ERROR" err+      = throwError err  mkVarSpec :: (Var, LocSymbol, Located BareType) -> BareM (Var, Located SpecType)-mkVarSpec (v, _, b) = tx <$> mkLSpecType b+mkVarSpec (v, _, b) = (v,) . fmap (txCoerce . generalize) <$> mkLSpecType b   where-    tx              = (v,) . fmap generalize+    coSub           = F.tracepp _msg $ M.fromList [ (F.symbol a, F.FObj (specTvSymbol a)) | a <- tvs ]+    _msg            = "mkVarSpec v = " ++ F.showpp (v, b)+    tvs             = bareTypeVars (val b) -- fmap ty_var_value . fst4 . bkUniv . val $ b+    specTvSymbol    = F.symbol . bareRTyVar+    txCoerce        = mapExprReft (F.applyCoSub coSub) +bareTypeVars :: BareType -> [BTyVar]+bareTypeVars t = Misc.sortNub . fmap ty_var_value $ vs ++ vs'+  where+    vs         = fst4 . bkUniv $ t+    vs'        = freeTyVars    $ t+ makeIAliases :: (ModName, Ms.Spec (Located BareType) bndr)              -> BareM [(Located SpecType, Located SpecType)] makeIAliases (mod, spec)@@ -340,7 +348,7 @@   resolveDictionaries :: [Var] -> [(F.Symbol, M.HashMap F.Symbol (RISig SpecType))] -> [Maybe (Var, M.HashMap F.Symbol (RISig SpecType))]-resolveDictionaries vars ds  = lookupVar <$> concat (go <$> groupList ds)+resolveDictionaries vars ds  = lookupVar <$> concat (go <$> Misc.groupList ds)  where     go (x,is)           = addIndex 0 x $ reverse is
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -45,7 +45,7 @@ import           UniqSet (mkUniqSet) import           Text.PrettyPrint.HughesPJ                     hiding (first) import           Control.Monad.State-import           Data.Maybe                                    (fromMaybe, catMaybes, fromJust, isJust)+import           Data.Maybe                                    (fromMaybe, catMaybes, isJust) import qualified Data.HashMap.Strict                           as M import qualified Data.HashSet                                  as S import qualified Data.List                                     as L@@ -68,7 +68,7 @@ import           Language.Haskell.Liquid.Types.Strata import           Language.Haskell.Liquid.Types.RefType import           Language.Haskell.Liquid.Types.PredType        hiding (freeTyVars)-import           Language.Haskell.Liquid.GHC.Misc          ( isInternal, collectArguments, tickSrcSpan, showPpr )+import qualified Language.Haskell.Liquid.GHC.Misc         as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr ) import           Language.Haskell.Liquid.Misc import           Language.Haskell.Liquid.Types.Literals -- NOPROVER import           Language.Haskell.Liquid.Constraint.Axioms@@ -286,10 +286,10 @@ trustVar cfg info x = trustInternals cfg && derivedVar info x  derivedVar :: GhcInfo -> Var -> Bool-derivedVar info x = x `elem` derVars info || isInternal x+derivedVar info x = x `elem` derVars info || GM.isInternal x  doTermCheck :: S.HashSet Var -> Bind Var -> Bool-doTermCheck lazyVs = not . any (\x -> S.member x lazyVs || isInternal x) . bindersOf+doTermCheck lazyVs = not . any (\x -> S.member x lazyVs || GM.isInternal x) . bindersOf  -- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!! consCBSizedTys :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv@@ -309,14 +309,14 @@        let rts   = (recType autoenv <$>) <$> xeets        let xts   = zip xs ts        γ'       <- foldM extender γ xts-       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . isClassPred . varType) <$> vs)+       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isPredVar {- isClassPred . varType -}) <$> vs)        let xets' = zip3 xs es ts        mapM_ (uncurry $ consBind True) (zip γs xets')        return γ'   where        (xs, es)       = unzip xes        dxs            = F.pprint <$> xs-       collectArgs    = collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate+       collectArgs    = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate        checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]        checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)        checkSameLens  = checkAll err2 length@@ -379,8 +379,8 @@     rts  = zipWith (addObligation OTerm) ts' <$> rss     (xs, es)     = unzip xes     mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys']-    collectArgs  = collectArguments . length . ty_binds . toRTypeRep-    err x        = "Constant: makeTermEnvs: no terminating expression for " ++ showPpr x+    collectArgs  = GM.collectArguments . length . ty_binds . toRTypeRep+    err x        = "Constant: makeTermEnvs: no terminating expression for " ++ GM.showPpr x  addObligation :: Oblig -> SpecType -> RReft -> SpecType addObligation o t r  = mkArrow αs πs ls xts $ RRTy [] r o t2@@ -669,12 +669,12 @@  cconsE' γ e@(Cast e' c) t   = do t' <- castTy γ (exprType e) e' c-       addC (SubC γ t' t) ("cconsE Cast: " ++ showPpr e)+       addC (SubC γ t' t) ("cconsE Cast: " ++ GM.showPpr e)  cconsE' γ e t   = do te  <- consE γ e        te' <- instantiatePreds γ e te >>= addPost γ-       addC (SubC γ te' t) ("cconsE: " ++ showPpr e)+       addC (SubC γ te' t) ("cconsE: " ++ GM.showPpr e)  lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> UReft F.Reft lambdaSingleton γ tce x e@@ -797,33 +797,19 @@          Just (x, _) -> return $ maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)          Nothing     -> return tt --- RJ: The snippet below is *too long*. Please pull stuff from the where-clause--- out to the top-level.-consE γ e'@(App e a) | isDictionary a-  = if isJust tt-      then return $ fromRISig $ fromJust tt-      else do ([], πs, ls, te) <- bkUniv <$> consE γ e-              te0              <- instantiatePreds γ e' $ foldr RAllP te πs-              te'              <- instantiateStrata ls te0-              (γ', te''')      <- dropExists γ te'-              te''             <- dropConstraints γ te'''-              updateLocA {- πs -}  (exprLoc e) te''-              let RFun x tx t _ = checkFun ("Non-fun App with caller ", e') γ te''-              pushConsBind      $ cconsE γ' a tx-              addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)--  where-    tt                           = dhasinfo dinfo $ grepfunname e-    grepfunname (App x (Type _)) = grepfunname x-    grepfunname (Var x)          = x-    grepfunname e                = panic Nothing $ "grepfunname on \t" ++ showPpr e-    isDictionary _               = isJust (mdict a)-    mdict w                      = case w of-                                     Var x          -> case dlookup (denv γ) x of {Just _ -> Just x; Nothing -> Nothing}-                                     Tick _ e       -> mdict e-                                     App a (Type _) -> mdict a-                                     _              -> Nothing-    dinfo                        = dlookup (denv γ) (fromJust (mdict a))+consE γ e'@(App e a) | Just aDict <- getExprDict γ a+  = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of+      Just riSig -> return (fromRISig riSig)+      _          -> do+        ([], πs, ls, te) <- bkUniv <$> consE γ e+        te0              <- instantiatePreds γ e' $ foldr RAllP te πs+        te'              <- instantiateStrata ls te0+        (γ', te''')      <- dropExists γ te'+        te''             <- dropConstraints γ te'''+        updateLocA {- πs -}  (exprLoc e) te''+        let RFun x tx t _ = checkFun ("Non-fun App with caller ", e') γ te''+        pushConsBind      $ cconsE γ' a tx+        addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)   consE γ e'@(App e a)@@ -864,7 +850,7 @@  consE γ (Tick tt e)   = do t <- consE (setLocation γ (Sp.Tick tt)) e-       addLocA Nothing (tickSrcSpan tt) (AnnUse t)+       addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t)        return t  -- See Note [Type classes with a single method]@@ -879,7 +865,7 @@    = trueTy $ exprType e  consE _ e@(Type t)-  = panic Nothing $ "consE cannot handle type " ++ showPpr (e, t)+  = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t)  caseKVKind ::[Alt Var] -> KVKind caseKVKind [(DataAlt _, _, Var _)] = ProjectE@@ -892,6 +878,23 @@   | otherwise   = return γ +getExprFun :: CGEnv -> CoreExpr -> Var+getExprFun γ e          = go e+  where+    go (App x (Type _)) = go x+    go (Var x)          = x+    go _                = panic (Just (getLocation γ)) msg+    msg                 = "getFunName on \t" ++ GM.showPpr e++-- | `exprDict e` returns the dictionary `Var` inside the expression `e`+getExprDict :: CGEnv -> CoreExpr -> Maybe Var+getExprDict γ           =  go+  where+    go (Var x)          = case dlookup (denv γ) x of {Just _ -> Just x; Nothing -> Nothing}+    go (Tick _ e)       = go e+    go (App a (Type _)) = go a+    go _                = Nothing+ -------------------------------------------------------------------------------- -- | Type Synthesis for Special @Pattern@s ------------------------------------- --------------------------------------------------------------------------------@@ -983,7 +986,7 @@   = castTy' γ t e  castTy' _ _ e-  = panic Nothing $ "castTy cannot handle expr " ++ showPpr e+  = panic Nothing $ "castTy cannot handle expr " ++ GM.showPpr e  {- showCoercion :: Coercion -> String@@ -1057,7 +1060,7 @@   | otherwise              = panic (Just $ getLocation γ) msg   where     msg = unlines [ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t-                  , "In", showPpr e, "Arg = " , show a ]+                  , "In", GM.showPpr e, "Arg = " , show a ]   dropExists :: CGEnv -> SpecType -> CG (CGEnv, SpecType)@@ -1101,7 +1104,8 @@        cγ               <- addBinders cγ' x' [(x', xt)]        return $ addArguments cγ ys   where-    ys'' = F.symbol <$> (filter (not . isClassPred . varType) ys)+       ys'' = F.symbol <$> filter (not . GM.isPredVar) ys+    -- ys'' = F.symbol <$> (filter (not . isClassPred . varType) ys)  caseEnv γ x acs a _ _   = do let x'  = F.symbol x@@ -1134,9 +1138,9 @@         -> (SpecType, [SpecType], SpecType) unfoldR td (RApp _ ts rs _) ys = (t3, tvys ++ yts, ignoreOblig rt)   where-        tbody              = instantiatePvs (instantiateTys td ts) $ reverse rs+        tbody              = instantiatePvs (instantiateTys (F.notracepp "UNFOLDR-1" td) ts) $ reverse rs         (ys0, yts', _, rt) = safeBkArrow $ instantiateTys tbody tvs'-        yts''              = zipWith F.subst sus (yts'++[rt])+        yts''              = F.notracepp "UNFOLDR-0" $ zipWith F.subst sus (yts'++[rt])         (t3,yts)           = (last yts'', init yts'')         sus                = F.mkSubst <$> (L.inits [(x, F.EVar y) | (x, y) <- zip ys0 ys'])         (αs, ys')          = mapSnd (F.symbol <$>) $ L.partition isTyVar ys@@ -1169,7 +1173,7 @@ checkAll x g t                = checkErr x g t  checkErr :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType-checkErr (msg, e) γ t         = panic (Just sp) $ msg ++ showPpr e ++ ", type: " ++ showpp t+checkErr (msg, e) γ t         = panic (Just sp) $ msg ++ GM.showPpr e ++ ", type: " ++ showpp t   where     sp                        = getLocation γ @@ -1204,7 +1208,7 @@ argType (TyVarTy x)   = Just $ F.EVar $ F.symbol $ varName x argType t-  | F.symbol (showPpr t) == anyTypeSymbol+  | F.symbol (GM.showPpr t) == anyTypeSymbol   = Just $ F.EVar anyTypeSymbol argType _   = Nothing@@ -1229,7 +1233,7 @@ lamExpr γ (Tick _ e)  = lamExpr γ e lamExpr γ (App e (Type _)) = lamExpr γ e lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of-                              (Just p1, Just p2) | not (isClassPred $ exprType e2)+                              (Just p1, Just p2) | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)                                                  -> Just $ F.EApp p1 p2                               (Just p1, Just _ ) -> Just p1                               _  -> Nothing@@ -1282,7 +1286,7 @@   | higherOrderFlag γ, App f x <- simplify e   = case (funExpr γ f, argExpr γ x) of       (Just f', Just x')-                 | not (isClassPred $ exprType x)+                 | not (GM.isPredExpr x) -- (isClassPred $ exprType x)                  -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x'))       (Just f', Just _)                  -> strengthenMeet t (uTop $ F.exprReft f' )@@ -1302,7 +1306,7 @@  funExpr γ (App e1 e2)   = case (funExpr γ e1, argExpr γ e2) of-      (Just e1', Just e2') | not (isClassPred $ exprType e2)+      (Just e1', Just e2') | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)                            -> Just (F.EApp e1' e2')       (Just e1', Just _)                            -> Just e1'@@ -1348,7 +1352,7 @@ -- | Cleaner Signatures For Rec-bindings --------------------------------------- -------------------------------------------------------------------------------- exprLoc                         :: CoreExpr -> Maybe SrcSpan-exprLoc (Tick tt _)             = Just $ tickSrcSpan tt+exprLoc (Tick tt _)             = Just $ GM.tickSrcSpan tt exprLoc (App e a) | isType a    = exprLoc e exprLoc _                       = Nothing
src/Language/Haskell/Liquid/Constraint/Init.hs view
@@ -69,7 +69,7 @@        let f0'   = if notruetypes $ getConfig sp then [] else f0''        f1       <- refreshArgs'   defaults                            -- default TOP reftype      (for all vars)        f1'      <- refreshArgs' $ makedcs dcsty                       -- data constructors-       f2       <- (refreshArgs' $ assm info)                           -- assumed refinements      (for imported vars)+       f2       <- refreshArgs' $ assm info                           -- assumed refinements      (for imported vars)        f3       <- refreshArgs' $ vals gsAsmSigs sp                   -- assumed refinedments     (with `assume`)        f40      <- makeExactDc <$> (refreshArgs' $ vals gsCtors sp)   -- constructor refinements  (for measures)        f5       <- refreshArgs' $ vals gsInSigs sp                    -- internal refinements     (from Haskell measures)@@ -85,7 +85,7 @@        let lt2s  = [ (F.symbol x, rTypeSort tce t) | (x, t) <- f1' ]        let tcb   = mapSnd (rTypeSort tce) <$> concat bs        let γ0    = measEnv sp (head bs) (cbs info) tcb lt1s lt2s (bs!!3) (bs!!5) hs info-       γ  <- globalize <$> foldM (+=) γ0 [("initEnv", x, y) | (x, y) <- concat $ tail bs]+       γ  <- globalize <$> foldM (+=) γ0 (  [("initEnv", x, y) | (x, y) <- concat $ tail bs])        return γ {invs = is (invs1 ++ invs2)}   where     sp           = spec info
src/Language/Haskell/Liquid/Desugar/Coverage.hs view
@@ -31,6 +31,9 @@ import Name import Bag import CostCentre+#ifdef DETERMINISTIC_PROFILING+import CostCentreState+#endif import CoreSyn import Id import VarSet@@ -38,7 +41,9 @@ import FastString import HscTypes import TyCon+#ifndef DETERMINISTIC_PROFILING import UniqSupply+#endif import BasicTypes import MonadUtils import Maybes@@ -79,7 +84,9 @@     Just orig_file <- ml_hs_file mod_loc,     not ("boot" `isSuffixOf` orig_file) = do +#ifndef DETERMINISTIC_PROFILING      us <- mkSplitUniqSupply 'C' -- for cost centres+#endif      let  orig_file2 = guessSourceFile binds orig_file            tickPass tickish (binds,st) =@@ -102,7 +109,11 @@            initState = TT { tickBoxCount = 0                          , mixEntries   = []+#ifdef DETERMINISTIC_PROFILING+                         , ccIndices    = newCostCentreState+#else                          , uniqSupply   = us+#endif                          }            (binds1,st) = foldr tickPass (binds, initState) passes@@ -1020,7 +1031,11 @@  data TickTransState = TT { tickBoxCount:: Int                          , mixEntries  :: [MixEntry_]+#ifdef DETERMINISTIC_PROFILING+                         , ccIndices   :: CostCentreState+#else                          , uniqSupply  :: UniqSupply+#endif                          }  data TickTransEnv = TTE { fileName     :: FastString@@ -1095,10 +1110,18 @@ instance HasDynFlags TM where   getDynFlags = TM $ \ env st -> (tte_dflags env, noFVs, st) +#ifdef DETERMINISTIC_PROFILING+-- | Get the next HPC cost centre index for a given centre name+getCCIndexM :: FastString -> TM CostCentreIndex+getCCIndexM n = TM $ \_ st -> let (idx, is') = getCCIndex n $+                                                 ccIndices st+                              in (idx, noFVs, st { ccIndices = is' })+#else instance MonadUnique TM where   getUniqueSupplyM = TM $ \_ st -> (uniqSupply st, noFVs, st)   getUniqueM = TM $ \_ st -> let (u, us') = takeUniqFromSupply (uniqSupply st)                              in (u, noFVs, st { uniqSupply = us' })+#endif  getState :: TM TickTransState getState = TM $ \ _ st -> (st, noFVs, st)@@ -1226,8 +1249,14 @@       return $ HpcTick (this_mod env) c      ProfNotes -> do+#ifdef DETERMINISTIC_PROFILING+      let nm = mkFastString cc_name+      flavour <- HpcCC <$> getCCIndexM nm+      let cc = mkUserCC nm (this_mod env) pos flavour+#else       ccUnique <- getUniqueM       let cc = mkUserCC (mkFastString cc_name) (this_mod env) pos ccUnique+#endif           count = countEntries && gopt Opt_ProfCountEntries dflags       return $ ProfNote cc count True{-scopes-}
src/Language/Haskell/Liquid/Desugar/DsExpr.hs view
@@ -383,8 +383,14 @@       then do
         mod_name <- getModule
         count <- goptM Opt_ProfCountEntries
+#ifdef DETERMINISTIC_PROFILING
+        let nm = sl_fs cc
+        flavour <- ExprCC <$> getCCIndexM nm
+        Tick (ProfNote (mkUserCC nm mod_name loc flavour) count True)
+#else
         uniq <- newUnique
         Tick (ProfNote (mkUserCC (sl_fs cc) mod_name loc uniq) count True)
+#endif
                <$> dsLExpr expr
       else dsLExpr expr
src/Language/Haskell/Liquid/Desugar/DsMonad.hs view
@@ -6,7 +6,7 @@ @DsMonad@: monadery used in desugaring -} -{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, FlexibleContexts, CPP #-} {-# OPTIONS_GHC -fno-warn-orphans #-}  -- instance MonadThings is necessarily an orphan  module Language.Haskell.Liquid.Desugar.DsMonad (@@ -85,6 +85,9 @@ import Var (EvVar) import qualified GHC.LanguageExtensions as LangExt import UniqFM ( lookupWithDefaultUFM )+#ifdef DETERMINISTIC_PROFILING+import CostCentreState+#endif  import Data.IORef import Control.Monad@@ -176,6 +179,9 @@                   -> m (DsGblEnv, DsLclEnv) mkDsEnvsFromTcGbl hsc_env msg_var tcg_env   = do { pm_iter_var <- liftIO $ newIORef 0+#ifdef DETERMINISTIC_PROFILING+       ; cc_st_var   <- liftIO $ newIORef newCostCentreState+#endif        ; let dflags   = hsc_dflags hsc_env              this_mod = tcg_mod tcg_env              type_env = tcg_type_env tcg_env@@ -184,7 +190,11 @@              complete_matches = hptCompleteSigs hsc_env                                 ++ tcg_complete_matches tcg_env        ; return $ mkDsEnvs dflags this_mod rdr_env type_env fam_inst_env+#ifdef DETERMINISTIC_PROFILING+                           msg_var pm_iter_var cc_st_var complete_matches+#else                            msg_var pm_iter_var complete_matches+#endif        }  runDs :: HscEnv -> (DsGblEnv, DsLclEnv) -> DsM a -> IO (Messages, Maybe a)@@ -204,6 +214,9 @@ initDsWithModGuts :: HscEnv -> ModGuts -> DsM a -> IO (Messages, Maybe a) initDsWithModGuts hsc_env guts thing_inside   = do { pm_iter_var <- newIORef 0+#ifdef DETERMINISTIC_PROFILING+       ; cc_st_var   <- newIORef newCostCentreState+#endif        ; msg_var <- newIORef emptyMessages        ; let dflags   = hsc_dflags hsc_env              type_env = typeEnvFromEntities ids (mg_tcs guts) (mg_fam_insts guts)@@ -219,7 +232,11 @@               envs  = mkDsEnvs dflags this_mod rdr_env type_env                               fam_inst_env msg_var pm_iter_var+#ifdef DETERMINISTIC_PROFILING+                              cc_st_var complete_matches+#else                               complete_matches+#endif        ; runDs hsc_env envs thing_inside        } @@ -247,9 +264,15 @@          thing_inside }  mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv+#ifdef DETERMINISTIC_PROFILING+         -> IORef Messages -> IORef Int -> IORef CostCentreState+         -> [CompleteMatch] -> (DsGblEnv, DsLclEnv)+mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar cc_st_var+#else          -> IORef Messages -> IORef Int -> [CompleteMatch]          -> (DsGblEnv, DsLclEnv) mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar+#endif          complete_matches   = let if_genv = IfGblEnv { if_doc       = text "mkDsEnvs",                              if_rec_types = Just (mod, return type_env) }@@ -265,6 +288,9 @@                            , ds_dph_env = emptyGlobalRdrEnv                            , ds_parr_bi = panic "DsMonad: uninitialised ds_parr_bi"                            , ds_complete_matches = completeMatchMap+#ifdef DETERMINISTIC_PROFILING+                           , ds_cc_st   = cc_st_var+#endif                            }         lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv                            , dsl_loc     = real_span
src/Language/Haskell/Liquid/GHC/Misc.hs view
@@ -22,6 +22,7 @@ import           FamInstEnv import           Debug.Trace +import qualified CoreUtils import           DataCon                                    (isTupleDataCon) import           Prelude                                    hiding (error) import           Avail                                      (availsToNameSet)@@ -53,7 +54,7 @@   import           RdrName-import           Type                                       (liftedTypeKind)+import           Type                                       (isClassPred, isEqPred, liftedTypeKind) import           TyCoRep import           Var import           IdInfo@@ -212,6 +213,9 @@ -- | Pretty Printers ----------------------------------------------------------- -------------------------------------------------------------------------------- +notracePpr :: Outputable a => String -> a -> a+notracePpr _ x = x+ tracePpr :: Outputable a => String -> a -> a tracePpr s x = trace ("\nTrace: [" ++ s ++ "] : " ++ showPpr x) x @@ -735,3 +739,24 @@ binders :: Bind a -> [a] binders (NonRec z _) = [z] binders (Rec xes)    = fst <$> xes+++--------------------------------------------------------------------------------+-- | The following functions test if a `CoreExpr` or `CoreVar` are just types+--   in disguise, e.g. have `PredType` (in the GHC sense of the word), and so+--   shouldn't appear in refinements.+--------------------------------------------------------------------------------++isPredExpr :: CoreExpr -> Bool+isPredExpr = isPredType . CoreUtils.exprType++isPredVar :: Var -> Bool+isPredVar v = F.notracepp msg . isPredType . varType $ v+  where+    msg     =  "isGoodCaseBind v = " ++ show v++isPredType :: Type -> Bool+isPredType = anyF [ isClassPred, isEqPred ]++anyF :: [a -> Bool] -> a -> Bool+anyF ps x = or [ p x | p <- ps ]
src/Language/Haskell/Liquid/Misc.hs view
@@ -283,3 +283,13 @@   where     bM       = M.fromList bCs     b2cs b   = maybeToList (M.lookup b bM)+++fstByRank :: (Ord r, Hashable k, Eq k) => [(r, k, v)] -> [(r, k, v)]+fstByRank rkvs = [ (r, k, v) | (k, rvs) <- krvss, let (r, v) = getFst rvs ]+  where+    getFst     = head . sortOn fst+    krvss      = groupList [ (k, (r, v)) | (r, k, v) <- rkvs ]++sortOn :: (Ord b) => (a -> b) -> [a] -> [a]+sortOn f = L.sortBy (compare `on` f)
src/Language/Haskell/Liquid/Parse.hs view
@@ -44,7 +44,8 @@ import           Language.Fixpoint.Types                hiding (panic, SVar, DDecl, DataDecl, DataCtor (..), Error, R, Predicate) import           Language.Haskell.Liquid.GHC.Misc import           Language.Haskell.Liquid.Types          -- hiding (Axiom)-import qualified Language.Fixpoint.Misc                 as F           --  (mapSnd)+import qualified Language.Fixpoint.Misc                 as Misc           --  (mapSnd)+import qualified Language.Haskell.Liquid.Misc           as Misc import           Language.Haskell.Liquid.Types.RefType import           Language.Haskell.Liquid.Types.Variance import           Language.Haskell.Liquid.Types.Bounds@@ -598,7 +599,7 @@     safeLast msg _      = panic Nothing $ "safeLast with empty list " ++ msg  propositionSortP :: Parser [(Symbol, BSort)]-propositionSortP = map (F.mapSnd toRSort) <$> propositionTypeP+propositionSortP = map (Misc.mapSnd toRSort) <$> propositionTypeP  propositionTypeP :: Parser [(Symbol, BareType)] propositionTypeP = either parserFail return =<< (mkPropositionType <$> bareTypeP)@@ -996,7 +997,7 @@     <|> (reserved "lazyvar"       >> liftM LVars  lazyVarP  )      <|> (reserved "lazy"          >> liftM Lazy   lazyVarP  )-+    <|> (reserved "ple"           >> liftM Insts autoinstP  )     <|> (reserved "automatic-instances" >> liftM Insts autoinstP  )     <|> (reserved "LIQUID"        >> liftM Pragma pragmaP   )     <|> {- DEFAULT -}                liftM Asrts  tyBindsP@@ -1042,7 +1043,7 @@ asizeP = locParserP binderP  decreaseP :: Parser (LocSymbol, [Int])-decreaseP = F.mapSnd f <$> liftM2 (,) (locParserP binderP) (spaces >> many integer)+decreaseP = Misc.mapSnd f <$> liftM2 (,) (locParserP binderP) (spaces >> many integer)   where     f     = ((\n -> fromInteger n - 1) <$>) @@ -1127,7 +1128,7 @@        body <- bodyP        posE <- getPosition        let (tArgs, vArgs) = partition (isSmall . headSym) args-       return $ RTA name (f <$> tArgs) (f <$> vArgs) body pos posE+       return $ RTA name (f <$> tArgs) vArgs body pos posE  aliasIdP :: Parser Symbol aliasIdP = condIdP (letter <|> char '_') alphaNums (isAlpha . head)@@ -1361,14 +1362,14 @@   x   <- locParserP dataConNameP   spaces   xts <- dataConFieldsP-  return $ DataCtor x xts Nothing+  return $ DataCtor x [] xts Nothing  adtDataConP :: Parser DataCtor adtDataConP = do   x     <- locParserP dataConNameP   dcolon   tr    <- toRTypeRep <$> bareTypeP-  return $ DataCtor x (tRepFields tr) (Just $ ty_res tr)+  return $ DataCtor x [] (tRepFields tr) (Just $ ty_res tr)  tRepFields :: RTypeRep c tv r -> [(Symbol, RType c tv r)] tRepFields tr = zip (ty_binds tr) (ty_args tr)@@ -1421,12 +1422,12 @@   where     msg                  = "You should specify at least one data constructor for a family instance" - dataCtorsP :: Parser (Maybe BareType, [DataCtor])-dataCtorsP-  =  (reservedOp "="     >> ((Nothing, ) <$>                 sepBy dataConP    (reservedOp "|")))- <|> (reserved   "where" >> ((Nothing, ) <$>                 sepBy adtDataConP (reservedOp "|")))- <|> (                      ((,)         <$> dataPropTyP <*> sepBy adtDataConP (reservedOp "|")))+dataCtorsP = do+  (pTy, dcs) <-     (reservedOp "="     >> ((Nothing, ) <$>                 sepBy dataConP    (reservedOp "|")))+                <|> (reserved   "where" >> ((Nothing, ) <$>                 sepBy adtDataConP (reservedOp "|")))+                <|> (                      ((,)         <$> dataPropTyP <*> sepBy adtDataConP (reservedOp "|")))+  return (pTy, Misc.sortOn (val . dcName) dcs)  noWhere :: Parser Symbol noWhere = try $ do
src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs view
@@ -25,7 +25,7 @@ import qualified Var import           Coercion import qualified Pair-+-- import qualified Text.Printf as Printf import qualified CoreSyn                               as C import           Literal import           IdInfo@@ -243,7 +243,7 @@ coercionTypeEq co   | Pair.Pair s t <- {- tracePpr ("coercion-type-eq-1: " ++ showPpr co) $ -}                        coercionKind co-  = (s, t) +  = (s, t)  typeEqToLg :: (Type, Type) -> LogicM (Sort, Sort) typeEqToLg (s, t) = do@@ -270,34 +270,39 @@ casesToLg v e alts   = mapM (altToLg e) alts >>= go   where-    go :: [(DataCon, Expr)] -> LogicM Expr+    go :: [(C.AltCon, Expr)] -> LogicM Expr     go [(_,p)]     = return (p `subst1` su)-    go ((d,p):dps) = do c <- checkDataCon d e+    go ((d,p):dps) = do c <- checkDataAlt d e                         e' <- go dps                         return (EIte c p e' `subst1` su)     go []          = throw "Bah"--    su = (symbol v, e)+    su             = (symbol v, e) -checkDataCon :: DataCon -> Expr -> LogicM Expr-checkDataCon d e-  = return $ EApp (EVar $ makeDataConChecker d) e+checkDataAlt :: C.AltCon -> Expr -> LogicM Expr+checkDataAlt (C.DataAlt d) e = return $ EApp (EVar (makeDataConChecker d)) e+checkDataAlt C.DEFAULT     _ = return PTrue+checkDataAlt (C.LitAlt _)  _ = throw "Oops, not yet handled: checkDataAlt on Lit" -altToLg :: Expr -> C.CoreAlt -> LogicM (DataCon, Expr)-altToLg de (C.DataAlt d, xs, e)+altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)+altToLg de (a@(C.DataAlt d), xs, e)   = do p  <- coreToLg e        dm <- gets lsDCMap        let su = mkSubst $ concat [ f dm x i | (x, i) <- zip xs [1..]]-       return (d, subst su p)+       return (a, subst su p)   where     f dm x i = let t = EApp (EVar $ makeDataConSelector (Just dm) d i) de                in [(symbol x, t), (simplesymbol x, t)]-altToLg _ (C.LitAlt _, _, _)-  = throw "altToLg on Lit"-altToLg _ (C.DEFAULT, _, _)-  = throw ("Cannot reflect functions with Default pattern matching." ++ -           "\n\t Suggestion: Make sure your function is total and is not pattern matching on integer values.") +altToLg _ (a, _, e)+  = (a, ) <$> coreToLg e+++--- altToLg _ (C.LitAlt _, _, _)+  --- = throw "altToLg on Lit"+--- altToLg _ (C.DEFAULT, _, e)+  --- = throw ("Cannot reflect functions with Default pattern matching." +++           --- "\n\t Suggestion: Make sure your function is total and is not pattern matching on integer values.")+ coreToIte :: C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr coreToIte e (efalse, etrue)   = do p  <- coreToLg e@@ -451,8 +456,12 @@ _simpleSymbolVar' = simplesymbol --symbol . {- showPpr . -} getName  isErasable :: Id -> Bool-isErasable v = isPrefixOfSym (symbol ("$"      :: String)) (simpleSymbolVar v)+isErasable v = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v)+  -- where+    -- v         = F.tracepp _msg v0+    -- _msg      = Printf.printf "isErasable: isCoVar %s = %s" (showPpr v0) (show $ isCoVar v0) + isANF :: Id -> Bool isANF      v = isPrefixOfSym (symbol ("lq_anf" :: String)) (simpleSymbolVar v) @@ -539,5 +548,6 @@  instance Simplify C.CoreAlt where   simplify (c, xs, e) = (c, xs, simplify e)-+    -- where xs   = F.tracepp _msg xs0+    --      _msg = "isCoVars? " ++ F.showpp [(x, isCoVar x, varType x) | x <- xs0]   inline p (c, xs, e) = (c, xs, inline p e)
src/Language/Haskell/Liquid/Types.hs view
@@ -52,7 +52,8 @@   , TyConInfo(..), defaultTyConInfo   , rTyConPVs   , rTyConPropVs-  , isClassRTyCon, isClassType, isEqType, isRVar, isBool+  -- , isClassRTyCon+  , isClassType, isEqType, isRVar, isBool    -- * Refinement Types   , RType (..), Ref(..), RTProp, rPropP@@ -124,6 +125,7 @@   -- * Traversing `RType`   , efoldReft, foldReft, foldReft'   , mapReft, mapReftM, mapPropM+  , mapExprReft   , mapBot, mapBind   , foldRType @@ -163,7 +165,7 @@   -- * Modules and Imports   , ModName (..), ModType (..)   , isSrcImport, isSpecImport-  , getModName, getModString+  , getModName, getModString, qualifyModName    -- * Refinement Type Aliases   , RTEnv (..)@@ -217,7 +219,8 @@    , Axiom(..), HAxiom, AxiomEq -- (..) -  , rtyVarUniqueSymbol, tyVarUniqueSymbol, rtyVarType+  -- , rtyVarUniqueSymbol, tyVarUniqueSymbol+  , rtyVarType   )   where @@ -225,7 +228,7 @@ import           CoreSyn                                (CoreBind, CoreExpr) import           Data.String import           DataCon-import           GHC                                    (HscEnv, ModuleName, moduleNameString, getName)+import           GHC                                    (HscEnv, ModuleName, moduleNameString) import           GHC.Generics import           Module                                 (moduleNameFS) import           NameSet@@ -235,7 +238,7 @@ import           TyCon import           Type                                   (getClassPredTys_maybe) import           Language.Haskell.Liquid.GHC.TypeRep                          hiding  (maybeParen, pprArrowChain)-import           TysPrim                                (eqPrimTyCon)+import           TysPrim                                (eqReprPrimTyCon, eqPrimTyCon) import           TysWiredIn                             (listTyCon, boolTyCon) import           Var @@ -286,7 +289,7 @@     deriving (Show)  ppEnv :: PPEnv-ppEnv           = ppEnvCurrent+ppEnv = ppEnvCurrent -- { ppTyVar = True } use True TO SEE UNIQUE SUFFIX ON TYVar  ppEnvCurrent :: PPEnv ppEnvCurrent    = PP False False False False@@ -593,12 +596,19 @@   symbol (BTV tv) = tv  instance F.Symbolic RTyVar where-  symbol (RTV tv) = F.symbol . getName $ tv+  symbol (RTV tv) = F.symbol tv -- tyVarUniqueSymbol tv +-- instance F.Symbolic RTyVar where+  -- symbol (RTV tv) = F.symbol . getName $ tv+-- rtyVarUniqueSymbol  :: RTyVar -> Symbol+-- rtyVarUniqueSymbol (RTV tv) = tyVarUniqueSymbol tv+-- tyVarUniqueSymbol :: TyVar -> Symbol+-- tyVarUniqueSymbol tv = F.symbol $ show (getName tv) ++ "_" ++ show (varUnique tv)+ data BTyCon = BTyCon   { btc_tc    :: !F.LocSymbol    -- ^ TyCon name with location information-  , btc_class :: !Bool         -- ^ Is this a class type constructor?-  , btc_prom  :: !Bool         -- ^ Is Promoted Data Con?+  , btc_class :: !Bool           -- ^ Is this a class type constructor?+  , btc_prom  :: !Bool           -- ^ Is Promoted Data Con?   }   deriving (Generic, Data, Typeable) @@ -618,12 +628,6 @@  instance NFData RTyCon -rtyVarUniqueSymbol  :: RTyVar -> Symbol-rtyVarUniqueSymbol (RTV tv) = tyVarUniqueSymbol tv--tyVarUniqueSymbol :: TyVar -> Symbol-tyVarUniqueSymbol tv = F.symbol $ show (getName tv) ++ "_" ++ show (varUnique tv)- rtyVarType :: RTyVar -> Type rtyVarType (RTV v) = TyVarTy v @@ -650,8 +654,8 @@ isClassBTyCon :: BTyCon -> Bool isClassBTyCon = btc_class -isClassRTyCon :: RTyCon -> Bool-isClassRTyCon x = (isClassTyCon $ rtc_tc x) || (rtc_tc x == eqPrimTyCon)+-- isClassRTyCon :: RTyCon -> Bool+-- isClassRTyCon x = (isClassTyCon $ rtc_tc x) || (rtc_tc x == eqPrimTyCon)  rTyConPVs :: RTyCon -> [RPVar] rTyConPVs     = rtc_pvars@@ -713,9 +717,10 @@ instance Show TyConInfo where   show (TyConInfo x y _) = show x ++ "\n" ++ show y -------------------------------------------------------------------------- Unified Representation of Refinement Types -----------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Unified Representation of Refinement Types --------------------------------+--------------------------------------------------------------------------------+ type RTVU c tv = RTVar tv (RType c tv ()) type PVU  c tv = PVar     (RType c tv ()) @@ -889,8 +894,8 @@  instance B.Binary r => B.Binary (UReft r) -type BRType     = RType BTyCon BTyVar-type RRType     = RType RTyCon RTyVar+type BRType     = RType BTyCon BTyVar       -- ^ "Bare" parsed version+type RRType     = RType RTyCon RTyVar       -- ^ "Resolved" version type RRep       = RTypeRep RTyCon RTyVar  type BSort      = BRType    ()@@ -965,8 +970,8 @@   isFun      = isFunTyCon . rtc_tc   isList     = (listTyCon ==) . rtc_tc   isTuple    = TyCon.isTupleTyCon   . rtc_tc-  isClass    = isClassRTyCon-  isEqual    = (eqPrimTyCon ==) . rtc_tc+  isClass    = isClass . rtc_tc -- isClassRTyCon+  isEqual    = isEqual . rtc_tc   ppTycon    = F.toFix    isNumCls c  = maybe False (isClassOrSubClass isNumericClass)@@ -979,8 +984,8 @@   isFun      = isFunTyCon   isList     = (listTyCon ==)   isTuple    = TyCon.isTupleTyCon-  isClass c  = isClassTyCon c || c == eqPrimTyCon-  isEqual    = (eqPrimTyCon ==)+  isClass c  = isClassTyCon c   || isEqual c -- c == eqPrimTyCon+  isEqual c  = c == eqPrimTyCon || c == eqReprPrimTyCon   ppTycon    = text . showPpr    isNumCls c  = maybe False (isClassOrSubClass isNumericClass)@@ -1045,9 +1050,9 @@ instance Show BTyCon where   show = F.showpp ------------------------------------------------------------------------------ | Refined Instances ------------------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Refined Instances ---------------------------------------------------------+--------------------------------------------------------------------------------  data RInstance t = RI   { riclass :: BTyCon@@ -1084,17 +1089,6 @@  type AxiomEq = F.Equation --- data AxiomEq = AxiomEq---   { axiomName :: Symbol             -- ^ name of function---   , axiomArgs :: [(Symbol, F.Sort)] -- ^ parameters and sorts---   , axiomBody :: Expr               -- ^ TODO:???---   -- , axiomEq   :: Expr               -- ^ TODO:??? What is diff between body and eq?---   , axiomSort :: F.Sort             -- ^ output sort---   } deriving (Generic, Show)--- instance B.Binary AxiomEq--- instance F.PPrint AxiomEq where---   pprintTidy k (AxiomEq n xs b _ _) = text "axeq" <+> F.pprint n <+> F.pprint xs <+> ":=" <+> F.pprintTidy k b- instance Show (Axiom Var Type CoreExpr) where   show (Axiom (n, c) v bs _ts lhs rhs) = "Axiom : " ++                                          "\nFun Name: " ++ (showPpr n) ++@@ -1105,19 +1099,6 @@                                          "\nLHS      :" ++ (showPpr lhs) ++                                          "\nRHS      :" ++ (showPpr rhs) -{---instance F.Subable AxiomEq where-  syms   a = F.syms (axiomBody a) ++ F.syms (axiomEq a)-  subst su = mapAxiomEqExpr (F.subst su)-  substf f = mapAxiomEqExpr (F.substf f)-  substa f = mapAxiomEqExpr (F.substa f)--mapAxiomEqExpr :: (Expr -> Expr) -> AxiomEq -> AxiomEq-mapAxiomEqExpr f a = a { axiomBody = f (axiomBody a)-                       , axiomEq   = f (axiomEq   a) }---} -------------------------------------------------------------------------------- -- | Data type refinements --------------------------------------------------------------------------------@@ -1142,6 +1123,7 @@ -- | Data Constructor data DataCtor = DataCtor   { dcName   :: F.LocSymbol               -- ^ DataCon name+  , dcTheta  :: [BareType]                -- ^ The GHC ThetaType corresponding to DataCon.dataConSig   , dcFields :: [(Symbol, BareType)]      -- ^ [(fieldName, fieldType)]   , dcResult :: Maybe BareType            -- ^ Possible output (if in GADT form)   } deriving (Data, Typeable, Generic)@@ -1171,6 +1153,10 @@   | HasDecl   deriving (Show) +instance F.PPrint HasDataDecl where+  pprintTidy _ HasDecl    = text "HasDecl"+  pprintTidy k (NoDecl z) = text "NoDecl" <+> parens (F.pprintTidy k z)+ hasDecl :: DataDecl -> HasDataDecl hasDecl d   | null (tycDCons d)@@ -1249,17 +1235,17 @@ data RTAlias x a = RTA   { rtName  :: Symbol             -- ^ name of the alias   , rtTArgs :: [x]                -- ^ type parameters-  , rtVArgs :: [x]                -- ^ value parameters+  , rtVArgs :: [Symbol]           -- ^ value parameters   , rtBody  :: a                  -- ^ what the alias expands to-  , rtPos   :: F.SourcePos          -- ^ start position-  , rtPosE  :: F.SourcePos          -- ^ end   position+  , rtPos   :: F.SourcePos        -- ^ start position+  , rtPosE  :: F.SourcePos        -- ^ end   position   } deriving (Data, Typeable, Generic)  instance (B.Binary x, B.Binary a) => B.Binary (RTAlias x a)  mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt-                     , rtVArgs = f <$> rtVArgs rt+                     -- , rtVArgs = f <$> rtVArgs rt                      }  lmapEAlias :: LMap -> RTAlias Symbol Expr@@ -1269,7 +1255,6 @@ -------------------------------------------------------------------------------- -- | Constructor and Destructors for RTypes ------------------------------------ --------------------------------------------------------------------------------- data RTypeRep c tv r = RTypeRep   { ty_vars   :: [RTVar tv (RType c tv ())]   , ty_preds  :: [PVar (RType c tv ())]@@ -1327,11 +1312,11 @@         -> RType c tv r mkUnivs αs πs ls t = foldr RAllT (foldr RAllP (foldr RAllS t ls) πs) αs -bkUniv :: RType t1 a t2 -> ([RTVar a (RType t1 a ())], [PVar (RType t1 a ())], [Symbol], RType t1 a t2)-bkUniv (RAllT α t)      = let (αs, πs, ls, t') = bkUniv t in  (α:αs, πs, ls, t')-bkUniv (RAllP π t)      = let (αs, πs, ls, t') = bkUniv t in  (αs, π:πs, ls, t')-bkUniv (RAllS s t)      = let (αs, πs, ss, t') = bkUniv t in  (αs, πs, s:ss, t')-bkUniv t                = ([], [], [], t)+bkUniv :: RType tv c r -> ([RTVar c (RType tv c ())], [PVar (RType tv c ())], [Symbol], RType tv c r)+bkUniv (RAllT α t) = let (αs, πs, ls, t') = bkUniv t in (α:αs, πs, ls, t')+bkUniv (RAllP π t) = let (αs, πs, ls, t') = bkUniv t in (αs, π:πs, ls, t')+bkUniv (RAllS s t) = let (αs, πs, ss, t') = bkUniv t in (αs, πs, s:ss, t')+bkUniv t           = ([], [], [], t)  bkClass :: TyConable c         => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)@@ -1489,9 +1474,13 @@ pappSym :: Show a => a -> Symbol pappSym n  = F.symbol $ "papp" ++ show n -------------------------------------------------------------------------------------------- Visitors ------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Visitors ------------------------------------------------------------------+--------------------------------------------------------------------------------+mapExprReft :: (Expr -> Expr) -> RType c tv RReft -> RType c tv RReft+mapExprReft f = mapReft g+  where+    g (MkUReft (F.Reft (x, e)) p s) = MkUReft (F.Reft (x, f e)) p s  isTrivial :: (F.Reftable r, TyConable c) => RType c tv r -> Bool isTrivial t = foldReft (\_ r b -> F.isTauto r && b) True t@@ -1529,7 +1518,7 @@     go γ (RApp c ts rs r)   = RApp  c (go γ <$> ts) (mo γ <$> rs) r     go γ (RAllE z t t')     = RAllE z (go γ t) (go γ t')     go γ (REx z t t')       = REx   z (go γ t) (go γ t')-    go γ (RExprArg e)       = RExprArg (f γ <$> F.tracepp "RExprArg" e)+    go γ (RExprArg e)       = RExprArg (f γ <$> F.notracepp "RExprArg" e)     go γ (RAppTy t t' r)    = RAppTy (go γ t) (go γ t') r     go γ (RRTy e r o t)     = RRTy  (mapSnd (go γ) <$> e) r o (go γ t)     mo _ t@(RProp _ (RHole {})) = t@@ -1910,6 +1899,10 @@ getModString :: ModName -> String getModString = moduleNameString . getModName +qualifyModName :: ModName -> Symbol -> Symbol+qualifyModName n = qualifySymbol nSym+  where+    nSym         = F.symbol n  -------------------------------------------------------------------------------- -- | Refinement Type Aliases ---------------------------------------------------@@ -2223,12 +2216,13 @@   pprintTidy _ (BTV α) = text (F.symbolString α)  instance F.PPrint RTyVar where-  pprintTidy _ (RTV α)-   | ppTyVar ppEnv  = ppr_tyvar α+  -- pprintTidy k = pprintTidy k . F.symbol --(RTV α)+  pprintTidy k (RTV α)+   | ppTyVar ppEnv  = F.pprintTidy k (F.symbol α) -- ppr_tyvar α    | otherwise      = ppr_tyvar_short α    where-     ppr_tyvar :: Var -> Doc-     ppr_tyvar       = text . tvId+     -- _ppr_tyvar :: Var -> Doc+     -- _ppr_tyvar       = text . tvId       ppr_tyvar_short :: TyVar -> Doc      ppr_tyvar_short = text . showPpr
src/Language/Haskell/Liquid/Types/Dictionaries.hs view
@@ -18,13 +18,13 @@ import           Data.Hashable import           Prelude                                   hiding (error) import           Var+import           Name                                      (getName) import qualified Language.Fixpoint.Types as F import           Language.Haskell.Liquid.Types.PrettyPrint () import           Language.Haskell.Liquid.GHC.Misc          (dropModuleNamesCorrect) import           Language.Haskell.Liquid.Types import           Language.Haskell.Liquid.Types.RefType () import           Language.Fixpoint.Misc                (mapFst)- import qualified Data.HashMap.Strict                       as M  makeDictionaries :: [RInstance SpecType] -> DEnv F.Symbol SpecType@@ -36,7 +36,9 @@  makeDictionaryName :: Located F.Symbol -> [SpecType] -> F.Symbol makeDictionaryName t ts-  = F.symbol ("$f" ++ F.symbolString (val t) ++ concatMap makeDicTypeName ts)+  = F.notracepp _msg $ F.symbol ("$f" ++ F.symbolString (val t) ++ concatMap makeDicTypeName ts)+  where+    _msg = "MAKE-DICTIONARY " ++ F.showpp (val t, ts)   makeDicTypeName :: SpecType -> String@@ -44,17 +46,18 @@   = "(->)" makeDicTypeName (RApp c _ _ _)   = F.symbolString $ dropModuleNamesCorrect $ F.symbol $ rtc_tc c-makeDicTypeName (RVar a _)-  = show a+-- makeDicTypeName (RVar a _)+  -- = show a+makeDicTypeName (RVar (RTV a) _)+  = show (getName a)      -- RJ: DO NOT use show/symbol here as they add the unique-suffix+                          -- which then breaks the class resolution. makeDicTypeName t   = panic Nothing ("makeDicTypeName: called with invalid type " ++ show t)  --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Dictionay Environment ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Dictionary Environment ----------------------------------------------------+--------------------------------------------------------------------------------   dfromList :: [(Var, M.HashMap F.Symbol (RISig t))] -> DEnv Var t
src/Language/Haskell/Liquid/Types/Meet.hs view
@@ -9,7 +9,6 @@ import           Text.PrettyPrint.HughesPJ (text, Doc) import qualified Language.Fixpoint.Types as F import           Language.Haskell.Liquid.Types- import           Language.Haskell.Liquid.Types.RefType import           Language.Haskell.Liquid.UX.Tidy
src/Language/Haskell/Liquid/Types/PredType.hs view
@@ -74,7 +74,7 @@     wrapT               = dcWrapSpecType dc dcp     workX               = dataConWorkId dc            -- this is the weird one for GADTs     wrapX               = dataConWrapId dc            -- this is what the user expects to see-    isVanilla           = F.notracepp ("IS-Vanilla: " ++ showpp dc) $ isVanillaDataCon dc+    isVanilla           = {- F.notracepp ("IS-Vanilla: " ++ showpp dc) $ -} isVanillaDataCon dc  dcWorkSpecType :: DataCon -> SpecType -> SpecType dcWorkSpecType c wrT    = fromRTypeRep (meetWorkWrapRep c wkR wrR)
src/Language/Haskell/Liquid/Types/RefType.hs view
@@ -93,10 +93,10 @@ import GHC              hiding (Located) import DataCon import qualified TyCon  as TC-import Type             (splitFunTys, expandTypeSynonyms, substTyWith, isClassPred)+import Type             (splitFunTys, expandTypeSynonyms, substTyWith, isClassPred, isEqPred, isNomEqPred) import TysWiredIn       (listTyCon, intDataCon, trueDataCon, falseDataCon,                          intTyCon, charTyCon, typeNatKind, typeSymbolKind, stringTy, intTy)-import TysPrim          (eqPrimTyCon)+-- import TysPrim          (eqPrimTyCon) -- import           Data.Monoid      hiding ((<>)) import           Data.Maybe               (fromMaybe, isJust, fromJust) import           Data.Hashable@@ -120,24 +120,62 @@ import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.Names import Language.Fixpoint.Misc-import Language.Haskell.Liquid.GHC.Misc (locNamedThing, typeUniqueString, showPpr, stringTyVar, tyConTyVarsDef)+import qualified Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.GHC.Play (mapType, stringClassArg) -- , dataConImplicitIds)  import Data.List (sort, foldl') -strengthenDataConType :: Symbolic t-                      => (t, RType c tv (UReft Reft)) -> (t, RType c tv (UReft Reft))-strengthenDataConType (x, t) = (x, fromRTypeRep trep{ty_res = tres})-    where-      trep = toRTypeRep t-      tres = ty_res trep `strengthen` MkUReft (exprReft expr) mempty mempty-      xs   = ty_binds trep-      as   = ty_vars  trep-      x'   = symbol x-      expr | null xs && null as = EVar x'-           | null xs            = mkEApp (dummyLoc x') []-           | otherwise          = mkEApp (dummyLoc x') (EVar <$> xs)+strengthenDataConType :: (Var, SpecType) -> (Var, SpecType)+strengthenDataConType (x, t) = (x, fromRTypeRep trep {ty_res = tres})+  where+    tres     = F.notracepp _msg $ ty_res trep `strengthen` MkUReft (exprReft expr) mempty mempty+    trep     = toRTypeRep t+    _msg     = "STRENGTHEN-DATACONTYPE x = " ++ F.showpp (x, (zip xs ts))+    (xs, ts) = dataConArgs trep+    as       = ty_vars  trep+    x'       = symbol x+    expr | null xs && null as = EVar x'+         | otherwise          = mkEApp (dummyLoc x') (EVar <$> xs) ++dataConArgs :: SpecRep -> ([Symbol], [SpecType])+dataConArgs trep = unzip [ (x, t) | (x, t) <- zip xs ts, isValTy t]+  where+    xs           = ty_binds trep+    -- xs           = zipWith (\_ i -> (symbol ("x" ++ show i))) (ty_args trep) [1..]+    ts           = ty_args trep+    isValTy      = not . GM.isPredType . toType++-- RJ: AAAAAAARGHHH: this is duplicate of RT.strengthenDataConType+{-+makeDataConCtor :: Var -> SpecType+makeDataConCtor x = (dummyLoc . fromRTypeRep $ trep {ty_res = res, ty_binds = xs})+  where+    tres     = F.tracepp _msg $ ty_res trep `strengthen` MkUReft (exprReft expr) mempty mempty+    trep     = toRTypeRep . ofType . varType $ x+    _msg     = "STRENGTHEN-DATACONTYPE x = " ++ F.showpp (x, (zip xs ts))+    (xs, ts) = dataConArgs trep+    as       = ty_vars  trep+    x'       = symbol x+    expr | null xs && null as = EVar x'+         | otherwise          = mkEApp (dummyLoc x') (EVar <$> xs)++makeDataConCtor :: Var -> (Var, LocSpecType)+makeDataConCtor x = (x, dummyLoc . fromRTypeRep $ trep {ty_res = res, ty_binds = xs})+  where+    t    :: SpecType+    t    = ofType $ varType x+    trep = toRTypeRep t+    xs   = zipWith (\_ i -> (symbol ("x" ++ show i))) (ty_args trep) [1..]++    res  = ty_res trep `strengthen` MkUReft ref mempty mempty+    vv   = vv_+    x'   = symbol x+    ref  = Reft (vv, PAtom Eq (EVar vv) eq)+    eq   | null (ty_vars trep) && null xs = EVar x'+         | otherwise = mkEApp (dummyLoc x') (EVar <$> xs)+-}+ pdVar :: PVar t -> Predicate pdVar v        = Pr [uPVar v] @@ -344,7 +382,7 @@  -- MOVE TO TYPES instance Fixpoint Class where-  toFix = text . showPpr+  toFix = text . GM.showPpr  -- MOVE TO TYPES class FreeVar a v where@@ -352,7 +390,7 @@  -- MOVE TO TYPES instance FreeVar RTyCon RTyVar where-  freeVars = (RTV <$>) . tyConTyVarsDef . rtc_tc+  freeVars = (RTV <$>) . GM.tyConTyVarsDef . rtc_tc  -- MOVE TO TYPES instance FreeVar BTyCon BTyVar where@@ -484,7 +522,7 @@ bTyVar      = BTV  symbolRTyVar :: Symbol -> RTyVar-symbolRTyVar = rTyVar . stringTyVar . symbolString+symbolRTyVar = rTyVar . GM.stringTyVar . symbolString  bareRTyVar :: BTyVar -> RTyVar bareRTyVar (BTV tv) = symbolRTyVar tv@@ -525,7 +563,7 @@ bApp c = RApp (tyConBTyCon c)  tyConBTyCon :: TyCon -> BTyCon-tyConBTyCon = mkBTyCon . fmap tyConName . locNamedThing+tyConBTyCon = mkBTyCon . fmap tyConName . GM.locNamedThing -- tyConBTyCon = mkBTyCon . fmap symbol . locNamedThing  --- NV TODO : remove this code!!!@@ -716,7 +754,7 @@     rs'                        = applyNonNull rs0 (rtPropPV rc pvs) rs     rs0                        = rtPropTop <$> pvs     n                          = length fVs-    fVs                        = tyConTyVarsDef $ rtc_tc rc+    fVs                        = GM.tyConTyVarsDef $ rtc_tc rc     as                         = choosen n ts (rVar <$> fVs)      choosen 0 _ _           = []@@ -775,8 +813,8 @@     ps'  = subts (zip (RTV <$> αs) ts') <$> rTyConPVs rc'     ts'  = if null ts then rVar <$> βs else toRSort <$> ts     rc'  = M.lookupDefault rc c tyi-    αs   = tyConTyVarsDef $ rtc_tc rc'-    βs   = tyConTyVarsDef c+    αs   = GM.tyConTyVarsDef $ rtc_tc rc'+    βs   = GM.tyConTyVarsDef c     rc'' = if isNumeric tce rc' then addNumSizeFun rc' else rc'  @@ -1025,7 +1063,7 @@ -- | Type Substitutions -------------------------------------------------------- -------------------------------------------------------------------------------- -subts :: (Foldable t, SubsTy tv ty c) => t (tv, ty) -> c -> c+subts :: (SubsTy tv ty c) => [(tv, ty)] -> c -> c subts = flip (foldr subt)  instance SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar where@@ -1088,15 +1126,15 @@  instance SubsTy Symbol RSort Sort where   subt (v, RVar α _) (FObj s)-    | symbol v == s = FObj $ rTyVarSymbol α+    | symbol v == s = FObj $ symbol {- rTyVarSymbol -} α     | otherwise     = FObj s   subt _ s          = s   instance SubsTy RTyVar RSort Sort where   subt (v, sv) (FObj s)-    | rtyVarUniqueSymbol v == s-      || symbol v == s+    | -- rtyVarUniqueSymbol v == s ||+      symbol v == s     = typeSort M.empty $ toType sv     | otherwise     = FObj s@@ -1385,19 +1423,19 @@     def           = fTyconSort niTc     niTc          = symbolNumInfoFTyCon (dummyLoc $ tyConName c) (isNumCls c) (isFracCls c) -typeUniqueSymbol :: Type -> Symbol-typeUniqueSymbol = symbol . typeUniqueString- tyVarSort :: TyVar -> Sort-tyVarSort = FObj . tyVarUniqueSymbol+tyVarSort = FObj . symbol -- tyVarUniqueSymbol +typeUniqueSymbol :: Type -> Symbol+typeUniqueSymbol = symbol . GM.typeUniqueString+ typeSortForAll :: TCEmb TyCon -> Type -> Sort typeSortForAll tce τ   = genSort $ typeSort tce tbody   where genSort t           = foldl (flip FAbs) (sortSubst su t) [0..n-1]         (as, tbody)         = splitForAllTys τ         su                  = M.fromList $ zip sas (FVar <$>  [0..])-        sas                 = tyVarUniqueSymbol <$> as+        sas                 = {- tyVarUniqueSymbol -} symbol <$> as         n                   = length as  -- RJ: why not make this the Symbolic instance?@@ -1453,22 +1491,60 @@ ----------------------------------------------------------------------------------------- -- | Binders generated by class predicates, typically for constraining tyvars (e.g. FNum) -------------------------------------------------------------------------------------------- classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)] classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)] classBinds _ (RApp c ts _ _)-   | isFracCls c-   = [(rTyVarSymbol a, trueSortedReft FFrac) | (RVar a _) <- ts]-   | isNumCls c-   = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]+  | isFracCls c+  = [(symbol a, trueSortedReft FFrac) | (RVar a _) <- ts]+  | isNumCls c+  = [(symbol a, trueSortedReft FNum) | (RVar a _) <- ts] classBinds emb (RApp c [_, _, (RVar a _), t] _ _)-   | rtc_tc c == eqPrimTyCon-   = [(rTyVarSymbol a, rTypeSortedReft emb t)]-classBinds _ _-  = []+  | isEqual c+  = [(symbol a, rTypeSortedReft emb t)]+classBinds  emb (RApp c [_, (RVar a _), t] _ _)+  | showpp c == "Data.Type.Equality.~"  -- see [NOTE:type-equality-hack]+  = [(symbol a, rTypeSortedReft emb t)]+classBinds _ t+  = notracepp ("CLASSBINDS: " ++ showpp (toType t, isEqualityConstr t)) [] -rTyVarSymbol :: RTyVar -> Symbol-rTyVarSymbol (RTV α) = tyVarUniqueSymbol α+{- | [NOTE:type-equality-hack] +God forgive me for this AWFUL HACK.++How can I “test for” (i.e. write a function of type `Type -> Bool`)++that returns `True` for values (i.e. `Type`s) that print out as:++ ```+     typ ~ GHC.Types.Int+ ```++ or with, which some more detail, looks like++ ```+    (~ (TYPE LiftedRep) typ GHC.Types.Int)+ ```++ and which are generated from Haskell source that looks like++ ```+ instance PersistEntity Blob where+    data EntityField Blob typ+       = typ ~ Int => BlobXVal |+         typ ~ Int => BlobYVal+ ```++ see tests/neg/BinahUpdateLib1.hs++ I would have thought that `Type.isEqPred` or `Type.isNomEqPred` described here++ https://downloads.haskell.org/~ghc/8.2.1/docs/html/libraries/ghc-8.2.1/src/Type.html#isEqPred++ and which is what `isEqualityConstr` below is doing, but alas it doesn't work.+-}++isEqualityConstr :: SpecType -> Bool+isEqualityConstr = (isEqPred  .||. isNomEqPred) . toType+ -------------------------------------------------------------------------------- -- | Termination Predicates ---------------------------------------------------- --------------------------------------------------------------------------------@@ -1574,13 +1650,13 @@ makeTyConVariance :: TyCon -> VarianceInfo makeTyConVariance c = varSignToVariance <$> tvs   where-    tvs = tyConTyVarsDef c+    tvs = GM.tyConTyVarsDef c      varsigns = if TC.isTypeSynonymTyCon c                   then go True (fromJust $ TC.synTyConRhs_maybe c)                   else L.nub $ concatMap goDCon $ TC.tyConDataCons c -    varSignToVariance v = case filter (\p -> showPpr (fst p) == showPpr v) varsigns of+    varSignToVariance v = case filter (\p -> GM.showPpr (fst p) == GM.showPpr v) varsigns of                             []       -> Invariant                             [(_, b)] -> if b then Covariant else Contravariant                             _        -> Bivariant@@ -1648,8 +1724,12 @@                     $+$ nest 4 (vcat $ [ "|" <+> pprintTidy k c | c <- tycDCons dd ])  instance PPrint DataCtor where-  pprintTidy k (DataCtor c xts Nothing)  = pprintTidy k c <+> braces (ppFields k ", " xts)-  pprintTidy k (DataCtor c xts (Just t)) = pprintTidy k c <+> dcolon <+> (ppFields k "->" xts) <+> "->" <+> pprintTidy k t+  pprintTidy k (DataCtor c _   xts Nothing)  = pprintTidy k c <+> braces (ppFields k ", " xts)+  pprintTidy k (DataCtor c ths xts (Just t)) = pprintTidy k c <+> dcolon <+> ppThetas ths <+> (ppFields k "->" xts) <+> "->" <+> pprintTidy k t+    where+      ppThetas [] = empty+      ppThetas ts = parens (hcat $ punctuate ", " (pprintTidy k <$> ts)) <+> "=>"+  ppFields :: (PPrint k, PPrint v) => Tidy -> Doc -> [(k, v)] -> Doc ppFields k sep kvs = hcat $ punctuate sep (F.pprintTidy k <$> kvs)
src/Language/Haskell/Liquid/UX/CmdLine.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TemplateHaskell           #-} {-# LANGUAGE TupleSections             #-} {-# LANGUAGE TypeSynonymInstances      #-} {-# OPTIONS_GHC -fno-cse #-}@@ -39,6 +40,9 @@ import Data.Maybe import Data.Aeson (encode) import qualified Data.ByteString.Lazy.Char8 as B+import Development.GitRev (gitCommitCount)+import Options.Applicative.Simple (simpleVersion)+import qualified Paths_liquidhaskell as Meta import System.Directory import System.Exit import System.Environment@@ -438,11 +442,15 @@     l       = newPos "ENVIRONMENT" 0 0  copyright :: String-copyright = "LiquidHaskell v" ++ myVersion ++ " Copyright 2013-17 Regents of the University of California. All Rights Reserved.\n"+copyright = concat $ concat+  [ ["LiquidHaskell "]+  , [$(simpleVersion Meta.version)]+  -- , [" (" ++ _commitCount ++ " commits)" | _commitCount /= ("1"::String) &&+  --                                          _commitCount /= ("UNKNOWN" :: String)]+  , ["\nCopyright 2013-18 Regents of the University of California. All Rights Reserved.\n"]+  ]   where-    myVersion :: String-    myVersion = "0.8.2.2"-    -- CIRCLE HASSLES: myVersion = showVersion version+    _commitCount = $gitCommitCount  -- NOTE [searchpath] -- 1. we used to add the directory containing the file to the searchpath,
− tests/errors/UnboundVarInAssume1.hs 
@@ -1,15 +0,0 @@-a :: Int-a = 0--{-@ assume b :: { b : Int | a < b } @-}-b :: Int-b = 1--{-@-f :: a : Int -> { b : Int | a < b } -> ()-@-}-f :: Int -> Int -> ()-f _ _ = ()--g :: ()-g = f a b
+ tests/import/client/ExactGADT9.hs view
@@ -0,0 +1,12 @@+{-@ LIQUID "--exact-data-con" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module ExactGADT9 where++import ExactGADT8++{-@ reflect bar @-}+bar :: RefinedFilter Blob typ -> Bool+bar (RefinedFilter BlobXVal) = True+bar (RefinedFilter BlobYVal) = True
+ tests/import/lib/ExactGADT8.hs view
@@ -0,0 +1,47 @@+{-@ LIQUID "--exact-data-con" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++--------------------------------------------------------------------------------+module ExactGADT8 where++{- data Goob a where+       GooX :: (a ~ Int) => Goob a+    |  GooY :: (a ~ Int) => Goob a+  -}++class PersistEntity record where+    data EntityField record :: * -> *++{-@ data Blob  = Bingo { xVal :: Int, yVal :: Int } @-}+data Blob  = Bingo { xVal :: Int, yVal :: Int }++instance PersistEntity Blob where+  {- data EntityField Blob typ where+            ExactGADT8.BlobXVal :: EntityField Blob {v:_ | True }+          | ExectGADT8.BlobYVal :: EntityField Blob {v:_ | True }+    @-}+  -- ORIG+  data EntityField Blob typ where+    BlobXVal :: EntityField Blob Int+    BlobYVal :: EntityField Blob Int++-- TH-GEN+-- data EntityField Blob typ+--  = typ ~ Int => BlobXVal |+--    typ ~ Int => BlobYVal++data RefinedFilter record typ = RefinedFilter+  { refinedFilterField  :: EntityField record typ+  }++{- reflect evalQBlob @-}+evalQBlob :: RefinedFilter Blob typ -> Blob -> Bool+evalQBlob filter blob = case refinedFilterField filter of+  BlobXVal -> True+  BlobYVal -> True++{-@ reflect foo @-}+foo :: RefinedFilter Blob typ -> Blob -> Bool+foo (RefinedFilter BlobXVal) blob = True+foo (RefinedFilter BlobYVal) blob = True
+ tests/neg/BinahQuery.hs view
@@ -0,0 +1,126 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-} ++{-@ infixr === @-}+{-@ infixr >== @-}+{-@ infixr <== @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module Query where++import Prelude hiding (filter)++data PersistFilter = EQUAL | LE | GE++class PersistEntity record where+    data EntityField record :: * -> *++{-@ data Filter record typ = Filter { filterField :: EntityField record typ, filterValue :: typ, filterFilter :: PersistFilter } @-}+data Filter record typ = Filter+    { filterField  :: EntityField record typ+    , filterValue  :: typ+    , filterFilter :: PersistFilter+    } +++{-@ reflect === @-}+(===) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field === value = Filter field value EQUAL++{-@ reflect <== @-}+(<==) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field <== value =+  Filter {+    filterField = field+  , filterValue = value+  , filterFilter = LE +  }++{-@ reflect >== @-}+(>==) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field >== value =+  Filter {+    filterField = field+  , filterValue = value+  , filterFilter = GE +  }++{-@ data Blob  = B { xVal :: Int, yVal :: Int } @-}+data Blob  = B { xVal :: Int, yVal :: Int }++instance PersistEntity Blob where+    {-@ data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+      | BlobYVal :: EntityField Blob Int+    @-}+    data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+        BlobYVal :: EntityField Blob Int++{-@ filter :: f:(a -> Bool) -> [a] -> [{v:a | f v}] @-}+filter :: (a -> Bool) -> [a] -> [a]+filter f (x:xs)+  | f x         = x : filter f xs+  | otherwise   =     filter f xs+filter _ []     = []++{-@ reflect evalQBlobXVal @-}+evalQBlobXVal :: PersistFilter -> Int -> Int -> Bool+evalQBlobXVal EQUAL filter given = filter == given+evalQBlobXVal LE filter given = given <= filter+evalQBlobXVal GE filter given = given >= filter++{-@ reflect evalQBlobYVal @-}+evalQBlobYVal :: PersistFilter -> Int -> Int -> Bool+evalQBlobYVal EQUAL filter given = filter == given+evalQBlobYVal LE filter given = given <= filter+evalQBlobYVal GE filter given = given >= filter++{-@ reflect evalQBlob @-}+evalQBlob :: Filter Blob typ -> Blob -> Bool+evalQBlob filter blob = case filterField filter of+    BlobXVal -> evalQBlobXVal (filterFilter filter) (filterValue filter) (xVal blob)+    BlobYVal -> evalQBlobYVal (filterFilter filter) (filterValue filter) (yVal blob)++{-@ reflect evalQsBlob @-}+evalQsBlob :: [Filter Blob typ] -> Blob -> Bool+evalQsBlob (f:fs) blob = evalQBlob f blob && (evalQsBlob fs blob)+evalQsBlob [] _ = True+++{-@ filterQBlob :: f:(Filter Blob a) -> [Blob] -> [{b:Blob | evalQBlob f b}] @-}+filterQBlob :: Filter Blob a -> [Blob] -> [Blob]+filterQBlob q = filter (evalQBlob q)++{-@ filterQsBlob :: f:[(Filter Blob a)] -> [Blob] -> [{b:Blob | evalQsBlob f b}] @-}+filterQsBlob :: [Filter Blob a] -> [Blob] -> [Blob]+filterQsBlob qs = filter (evalQsBlob qs)++-- select functions++{-@ assume selectBlob :: f:[(Filter Blob a)] -> [{b:Blob | evalQsBlob f b}] @-}+selectBlob :: [Filter Blob a] -> [Blob]+selectBlob fs = undefined ++{-@ getZeros_ :: () -> [{b:Blob | xVal b = 0}] @-}+getZeros_ :: () -> [Blob]+getZeros_ () = selectBlob [(Filter BlobXVal 0 EQUAL)]++{-@ getBiggerThan10 :: () -> [{b:Blob | xVal b >= 10}] @-}+getBiggerThan10 :: () -> [Blob]+getBiggerThan10 () = selectBlob [(Filter BlobXVal 11 GE)]++{-@ getInRange :: () -> [{b:Blob | xVal b >= 10  && xVal b <= 20 && yVal b >= 0 && yVal b <= 10}] @-}+getInRange :: () -> [Blob]+getInRange () = selectBlob [ (BlobXVal >== 10)+                           , (BlobXVal <== 20)+                           , (BlobYVal >== 0)+                           , (BlobYVal <== 11)+                           ]
+ tests/neg/BinahUpdate.hs view
@@ -0,0 +1,38 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-} ++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module BinahUpdate where ++class PersistEntity record where+    data EntityField record :: * -> *++instance PersistEntity Blob where+    {-@ data EntityField Blob typ where+          BlobXVal :: EntityField Blob {v:Int | v >= 10}+        | BlobYVal :: EntityField Blob Int+      @-}+    data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+        BlobYVal :: EntityField Blob Int++{-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}+data Blob  = B { xVal :: Int, yVal :: Int }++data Update record typ = Update +    { updateField :: EntityField record typ+    , updateValue :: typ+    } ++createUpdate :: EntityField record a -> a -> Update record a+createUpdate field value = Update {+      updateField = field+    , updateValue = value+}++testUpdateQuery :: () -> Update Blob Int+testUpdateQuery () = createUpdate BlobXVal 8  -- toggle to 80 to be SAFE
+ tests/neg/BinahUpdateClient.hs view
@@ -0,0 +1,14 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-} ++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module BinahUpdateClient where ++import BinahUpdateLib ++testUpdateQuery :: () -> Update Blob Int+testUpdateQuery () = createUpdate BlobXVal 8  -- toggle to 80 to be SAFE
+ tests/neg/BinahUpdateLib.hs view
@@ -0,0 +1,38 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module BinahUpdateLib where++class PersistEntity record where+    data EntityField record :: * -> *++instance PersistEntity Blob where+    {-@ data EntityField Blob typ where+          BinahUpdateLib.BlobYVal :: EntityField Blob {v:_ | True}+        | BinahUpdateLib.BlobXVal :: EntityField Blob {v:_ | v >= 10}+      @-}+    data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+        BlobYVal :: EntityField Blob Int++{-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}+data Blob  = B { xVal :: Int, yVal :: Int }++data Update record typ = Update+    { updateField :: EntityField record typ+    , updateValue :: typ+    }++createUpdate :: EntityField record a -> a -> Update record a+createUpdate field value = Update {+      updateField = field+    , updateValue = value+}++testUpdateQuery :: () -> Update Blob Int+testUpdateQuery () = createUpdate BlobXVal 8  -- toggle to 80 to be SAFE
+ tests/neg/BinahUpdateLib1.hs view
@@ -0,0 +1,37 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module BinahUpdateLib where++class PersistEntity record where+    data EntityField record :: * -> *++instance PersistEntity Blob where+    {-@ data EntityField Blob typ where+          BinahUpdateLib.BlobYVal :: EntityField Blob {v:_ | True}+        | BinahUpdateLib.BlobXVal :: EntityField Blob {v:_ | v >= 10}+      @-}+   data EntityField Blob typ+      = typ ~ Int => BlobXVal |+        typ ~ Int => BlobYVal++data Blob  = B { xVal :: Int, yVal :: Int }++data Update record typ = Update+    { updateField :: EntityField record typ+    , updateValue :: typ+    }++createUpdate :: EntityField record a -> a -> Update record a+createUpdate field value = Update {+      updateField = field+    , updateValue = value+}++testUpdateQuery :: () -> Update Blob Int+testUpdateQuery () = createUpdate BlobXVal 8  -- toggle to 80 to be SAFE
− tests/neg/binah-EvalQuery.hs 
@@ -1,126 +0,0 @@-{-@ LIQUID "--no-adt" 	                           @-}-{-@ LIQUID "--exact-data-con"                      @-}-{-@ LIQUID "--higherorder"                         @-}-{-@ LIQUID "--no-termination"                      @-}-{-@ LIQUID "--ple" @-} --{-@ infixr === @-}-{-@ infixr >== @-}-{-@ infixr <== @-}--{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--module Query where--import Prelude hiding (filter)--data PersistFilter = EQUAL | LE | GE--class PersistEntity record where-    data EntityField record :: * -> *--{-@ data Filter record typ = Filter { filterField :: EntityField record typ, filterValue :: typ, filterFilter :: PersistFilter } @-}-data Filter record typ = Filter-    { filterField  :: EntityField record typ-    , filterValue  :: typ-    , filterFilter :: PersistFilter-    } ---{-@ reflect === @-}-(===) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field === value = Filter field value EQUAL--{-@ reflect <== @-}-(<==) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field <== value =-  Filter {-    filterField = field-  , filterValue = value-  , filterFilter = LE -  }--{-@ reflect >== @-}-(>==) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field >== value =-  Filter {-    filterField = field-  , filterValue = value-  , filterFilter = GE -  }--{-@ data Blob  = B { xVal :: Int, yVal :: Int } @-}-data Blob  = B { xVal :: Int, yVal :: Int }--instance PersistEntity Blob where-    {-@ data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-      | BlobYVal :: EntityField Blob Int-    @-}-    data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-        BlobYVal :: EntityField Blob Int--{-@ filter :: f:(a -> Bool) -> [a] -> [{v:a | f v}] @-}-filter :: (a -> Bool) -> [a] -> [a]-filter f (x:xs)-  | f x         = x : filter f xs-  | otherwise   =     filter f xs-filter _ []     = []--{-@ reflect evalQBlobXVal @-}-evalQBlobXVal :: PersistFilter -> Int -> Int -> Bool-evalQBlobXVal EQUAL filter given = filter == given-evalQBlobXVal LE filter given = given <= filter-evalQBlobXVal GE filter given = given >= filter--{-@ reflect evalQBlobYVal @-}-evalQBlobYVal :: PersistFilter -> Int -> Int -> Bool-evalQBlobYVal EQUAL filter given = filter == given-evalQBlobYVal LE filter given = given <= filter-evalQBlobYVal GE filter given = given >= filter--{-@ reflect evalQBlob @-}-evalQBlob :: Filter Blob typ -> Blob -> Bool-evalQBlob filter blob = case filterField filter of-    BlobXVal -> evalQBlobXVal (filterFilter filter) (filterValue filter) (xVal blob)-    BlobYVal -> evalQBlobYVal (filterFilter filter) (filterValue filter) (yVal blob)--{-@ reflect evalQsBlob @-}-evalQsBlob :: [Filter Blob typ] -> Blob -> Bool-evalQsBlob (f:fs) blob = evalQBlob f blob && (evalQsBlob fs blob)-evalQsBlob [] _ = True---{-@ filterQBlob :: f:(Filter Blob a) -> [Blob] -> [{b:Blob | evalQBlob f b}] @-}-filterQBlob :: Filter Blob a -> [Blob] -> [Blob]-filterQBlob q = filter (evalQBlob q)--{-@ filterQsBlob :: f:[(Filter Blob a)] -> [Blob] -> [{b:Blob | evalQsBlob f b}] @-}-filterQsBlob :: [Filter Blob a] -> [Blob] -> [Blob]-filterQsBlob qs = filter (evalQsBlob qs)---- select functions--{-@ assume selectBlob :: f:[(Filter Blob a)] -> [{b:Blob | evalQsBlob f b}] @-}-selectBlob :: [Filter Blob a] -> [Blob]-selectBlob fs = undefined --{-@ getZeros_ :: () -> [{b:Blob | xVal b = 0}] @-}-getZeros_ :: () -> [Blob]-getZeros_ () = selectBlob [(Filter BlobXVal 0 EQUAL)]--{-@ getBiggerThan10 :: () -> [{b:Blob | xVal b >= 10}] @-}-getBiggerThan10 :: () -> [Blob]-getBiggerThan10 () = selectBlob [(Filter BlobXVal 11 GE)]--{-@ getInRange :: () -> [{b:Blob | xVal b >= 10  && xVal b <= 20 && yVal b >= 0 && yVal b <= 10}] @-}-getInRange :: () -> [Blob]-getInRange () = selectBlob [ (BlobXVal >== 10)-                           , (BlobXVal <== 20)-                           , (BlobYVal >== 0)-                           , (BlobYVal <== 11)-                           ]
− tests/neg/binah-UpdateQuery.hs 
@@ -1,40 +0,0 @@-{-@ LIQUID "--no-adt" 	                           @-}-{-@ LIQUID "--exact-data-con"                      @-}-{-@ LIQUID "--higherorder"                         @-}-{-@ LIQUID "--no-termination"                      @-}-{-@ LIQUID "--ple" @-} --{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--class PersistEntity record where-    data EntityField record :: * -> *--instance PersistEntity Blob where-    {-@ data EntityField Blob typ where-        BlobXVal :: EntityField Blob {v:Int | v >= 0}-      | BlobYVal :: EntityField Blob Int-    @-}-    data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-        BlobYVal :: EntityField Blob Int--{-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}-data Blob  = B { xVal :: Int, yVal :: Int }--{-@ data Update record typ = Update { updateField :: EntityField record typ, updateValue :: typ } @-}-data Update record typ = Update -    { updateField :: EntityField record typ-    , updateValue :: typ-    } --{-@ data variance Update covariant covariant contravariant @-}--{-@ createUpdate :: EntityField record a -> a -> Update record a @-}-createUpdate :: EntityField record a -> a -> Update record a-createUpdate field value = Update {-      updateField = field-    , updateValue = value-}--testUpdateQuery :: () -> Update Blob Int-testUpdateQuery () = createUpdate BlobXVal (-1)
+ tests/pos/BinahQuery.hs view
@@ -0,0 +1,126 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-} ++{-@ infixr === @-}+{-@ infixr >== @-}+{-@ infixr <== @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module Query where++import Prelude hiding (filter)++data PersistFilter = EQUAL | LE | GE++class PersistEntity record where+    data EntityField record :: * -> *++{-@ data Filter record typ = Filter { filterField :: EntityField record typ, filterValue :: typ, filterFilter :: PersistFilter } @-}+data Filter record typ = Filter+    { filterField  :: EntityField record typ+    , filterValue  :: typ+    , filterFilter :: PersistFilter+    } +++{-@ reflect === @-}+(===) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field === value = Filter field value EQUAL++{-@ reflect <== @-}+(<==) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field <== value =+  Filter {+    filterField = field+  , filterValue = value+  , filterFilter = LE +  }++{-@ reflect >== @-}+(>==) :: (PersistEntity record, Eq typ) => +                 EntityField record typ -> typ -> Filter record typ+field >== value =+  Filter {+    filterField = field+  , filterValue = value+  , filterFilter = GE +  }++{-@ data Blob  = B { xVal :: Int, yVal :: Int } @-}+data Blob  = B { xVal :: Int, yVal :: Int }++instance PersistEntity Blob where+    {- data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+      | BlobYVal :: EntityField Blob Int+    -}+    data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+        BlobYVal :: EntityField Blob Int++{-@ filter :: f:(a -> Bool) -> [a] -> [{v:a | f v}] @-}+filter :: (a -> Bool) -> [a] -> [a]+filter f (x:xs)+  | f x         = x : filter f xs+  | otherwise   =     filter f xs+filter _ []     = []++{-@ reflect evalQBlobXVal @-}+evalQBlobXVal :: PersistFilter -> Int -> Int -> Bool+evalQBlobXVal EQUAL filter given = filter == given+evalQBlobXVal LE filter given = given <= filter+evalQBlobXVal GE filter given = given >= filter++{-@ reflect evalQBlobYVal @-}+evalQBlobYVal :: PersistFilter -> Int -> Int -> Bool+evalQBlobYVal EQUAL filter given = filter == given+evalQBlobYVal LE filter given = given <= filter+evalQBlobYVal GE filter given = given >= filter++{-@ reflect evalQBlob @-}+evalQBlob :: Filter Blob typ -> Blob -> Bool+evalQBlob filter blob = case filterField filter of+    BlobXVal -> evalQBlobXVal (filterFilter filter) (filterValue filter) (xVal blob)+    BlobYVal -> evalQBlobYVal (filterFilter filter) (filterValue filter) (yVal blob)++{-@ reflect evalQsBlob @-}+evalQsBlob :: [Filter Blob typ] -> Blob -> Bool+evalQsBlob (f:fs) blob = evalQBlob f blob && (evalQsBlob fs blob)+evalQsBlob [] _ = True+++{-@ filterQBlob :: f:(Filter Blob a) -> [Blob] -> [{b:Blob | evalQBlob f b}] @-}+filterQBlob :: Filter Blob a -> [Blob] -> [Blob]+filterQBlob q = filter (evalQBlob q)++{-@ filterQsBlob :: f:[(Filter Blob a)] -> [Blob] -> [{b:Blob | evalQsBlob f b}] @-}+filterQsBlob :: [Filter Blob a] -> [Blob] -> [Blob]+filterQsBlob qs = filter (evalQsBlob qs)++-- select functions++{-@ assume selectBlob :: f:[(Filter Blob a)] -> [{b:Blob | evalQsBlob f b}] @-}+selectBlob :: [Filter Blob a] -> [Blob]+selectBlob fs = undefined ++{-@ getZeros_ :: () -> [{b:Blob | xVal b = 0}] @-}+getZeros_ :: () -> [Blob]+getZeros_ () = selectBlob [(Filter BlobXVal 0 EQUAL)]++{-@ getBiggerThan10 :: () -> [{b:Blob | xVal b >= 10}] @-}+getBiggerThan10 :: () -> [Blob]+getBiggerThan10 () = selectBlob [(Filter BlobXVal 11 GE)]++{-@ getInRange :: () -> [{b:Blob | xVal b >= 10  && xVal b <= 20 && yVal b >= 0 && yVal b <= 11}] @-}+getInRange :: () -> [Blob]+getInRange () = selectBlob [ (BlobXVal >== 10)+                           , (BlobXVal <== 20)+                           , (BlobYVal >== 0)+                           , (BlobYVal <== 11)+                           ]
+ tests/pos/BinahUpdate.hs view
@@ -0,0 +1,40 @@+{-@ LIQUID "--no-adt" 	                           @-}+{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--higherorder"                         @-}+{-@ LIQUID "--no-termination"                      @-}+{-@ LIQUID "--ple" @-} ++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++class PersistEntity record where+    data EntityField record :: * -> *++instance PersistEntity Blob where+    {- data EntityField Blob typ where+        BlobXVal :: EntityField Blob {v:Int | v >= 0}+      | BlobYVal :: EntityField Blob Int+      @-}+    data EntityField Blob typ where+        BlobXVal :: EntityField Blob Int+        BlobYVal :: EntityField Blob Int++{-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}+data Blob  = B { xVal :: Int, yVal :: Int }++{-@ data Update record typ = Update { updateField :: EntityField record typ, updateValue :: typ } @-}+data Update record typ = Update +    { updateField :: EntityField record typ+    , updateValue :: typ+    } ++{-@ data variance Update covariant covariant contravariant @-}++{-@ createUpdate :: EntityField record a -> a -> Update record a @-}+createUpdate :: EntityField record a -> a -> Update record a+createUpdate field value = Update {+      updateField = field+    , updateValue = value+}++testUpdateQuery :: () -> Update Blob Int+testUpdateQuery () = createUpdate BlobXVal 3
+ tests/pos/Compiler.hs view
@@ -0,0 +1,108 @@+{-@ LIQUID "--exact-data-con" @-}+{-@ LIQUID "--higherorder"    @-}+{-@ LIQUID "--ple"            @-} +{-@ LIQUID "--no-totality"    @-} ++module Compiler where++import Language.Haskell.Liquid.ProofCombinators++-- | Expressions ---------------------------------------------------------------++{-@ data Expr [eSize] @-}+data Expr+  = Val Int+  | Add Expr Expr++{-@ measure eSize @-}+{-@ eSize :: Expr -> {v:Int | 1 <= v} @-}+eSize :: Expr -> Int+eSize (Val n)     = 1+eSize (Add e1 e2) = 1 + eSize e1 + eSize e2++{-@ invariant {v:Expr | 1 <= eSize v } @-}++-- | Interpreter ---------------------------------------------------------------++{-@ reflect interp @-}+interp :: Expr -> Int+interp (Val n)     = n+interp (Add e1 e2) = interp e1 + interp e2++-- | Code ----------------------------------------------------------------------++{-@ data Code [cSize] @-}+data Code+  = HALT+  | PUSH Int Code+  | ADD      Code++{-@ measure cSize @-}+{-@ cSize :: Code -> Nat @-}+cSize :: Code -> Int+cSize HALT       = 0+cSize (PUSH n c) = 1 + cSize c+cSize (ADD    c) = 1 + cSize c++-- | Stack ---------------------------------------------------------------------+data Stack+  = Emp+  | Arg Int Stack++-- | Compiler ------------------------------------------------------------------++{-@ reflect compileC @-}+compileC :: Expr -> Code -> Code+compileC (Val n) c     = PUSH n c+compileC (Add e1 e2) c = compileC e2 (compileC e1 (ADD c))++{-@ reflect compile @-}+compile :: Expr -> Code+compile e = compileC e HALT++-- | VM ------------------------------------------------------------------------++{-@ reflect run @-}+run :: Code -> Stack -> Int+run HALT       (Arg n s)         = n+run (ADD c)    (Arg n (Arg m s)) = run c (Arg (n + m) s)+run (PUSH n c) s                 = run c (Arg n       s)++{-@ reflect compileAndRun @-}+compileAndRun :: Expr -> Int+compileAndRun e = run (compileC e HALT) Emp++-- | Correctness ---------------------------------------------------------------++{-@ thmCompileC :: e:Expr -> c:Code -> s:Stack ->+      { run (compileC e c) s = run c (Arg (interp e) s) }+  @-}+thmCompileC :: Expr -> Code -> Stack -> Proof+thmCompileC (Val n)     c s =  () +thmCompileC (Add e1 e2) c s =  thmCompileC e2 (compileC e1  (ADD c)) s+                           &&& thmCompileC e1 (ADD c) (Arg (interp e2) s)++{-@ thmCompileAndRun :: e:Expr -> { compileAndRun e == interp e } @-}+thmCompileAndRun :: Expr -> Proof+thmCompileAndRun e = thmCompileC e HALT Emp+++{- thmCompileC (Add e1 e2) c s+   = [ -- run (compileC (Add e1 e2) c) s+      -- ==. run (compileC e2 (compileC e1 (ADD c))) s+      {- ? -} thmCompileC e2 (compileC e1  (ADD c)) s+      -- ==. run (compileC e1 (ADD c)) (Arg (interp e2) s)+    , {- ? -} thmCompileC e1 (ADD c) (Arg (interp e2) s)+      -- ==. run (ADD c) (Arg (interp e1) (Arg (interp e2) s))+      -- ==. run c (Arg (interp e1 + interp e2) s)+      -- ==. run c (Arg (interp (Add e1 e2)) s)+    ] *** QED+ -}++++++++---
tests/pos/ExactGADT1.hs view
@@ -1,4 +1,4 @@-{-@ LIQUID "--exact-data-con"                      @-}+{-@ LIQUID "--exact-data-con" @-}  {-# LANGUAGE  GADTs #-}
tests/pos/ExactGADT5.hs view
@@ -50,10 +50,10 @@ data Blob  = B { xVal :: Int, yVal :: Int }  instance PersistEntity Blob where-  {-@ data EntityField Blob typ where+  {- data EntityField Blob typ where         BlobXVal :: EntityField Blob Int       | BlobYVal :: EntityField Blob Int-    @-}+    -}     data EntityField Blob typ where         BlobXVal :: EntityField Blob Int         BlobYVal :: EntityField Blob Int
+ tests/pos/ExactGADT8a.hs view
@@ -0,0 +1,24 @@+{-@ LIQUID "--exact-data-con" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module ExactGADT8a where++{- data EntityField typ where+            BlobXVal :: EntityField {v:_ | True }+          | BlobYVal :: EntityField {v:_ | True }+ @-}+data EntityField typ where+  BlobXVal :: EntityField Int+  BlobYVal :: EntityField Int++  -- TH-GEN+  -- data EntityField Blob typ+  --  = typ ~ Int => BlobXVal |+  --    typ ~ Int => BlobYVal++{-@ reflect evalQBlob @-}+evalQBlob :: EntityField a -> Bool +evalQBlob BlobXVal = True +evalQBlob BlobYVal = False +
+ tests/pos/ExactGADT9a.hs view
@@ -0,0 +1,13 @@+{-@ LIQUID "--exact-data-con" @-}++{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}++module ExactGADT9a where++import ExactGADT8a++{-@ reflect zoo @-}+zoo :: EntityField a -> Bool +zoo BlobXVal = True +zoo BlobYVal = False +
+ tests/pos/Hutton.hs view
@@ -0,0 +1,110 @@+-- WITH-PLE ++module Hutton where++{-@ LIQUID "--higherorder"    @-}+{-@ LIQUID "--exact-data-con" @-}+{-@ LIQUID "--automatic-instances=liquidinstances" @-}++import Language.Haskell.Liquid.ProofCombinators++import Prelude hiding (length, head, tail, map, (++))++-- need to use a hand-rolled list type, it seems++data L a = N | C {hd :: a, tl :: L a}+{-@ data L [length] a = N | C {hd :: a, tl :: L a} @-}++length :: L a -> Int+{-@ length :: L a -> Nat @-}+{-@ measure length @-}+length N        = 0+length (C _ xs) = 1 + length xs++{-@ infix   ++ @-}+{-@ reflect ++ @-}+(++) :: L a-> L a -> L a+N        ++ ys = ys+(C x xs) ++ ys = C x (xs ++ ys)++-- huttons razor++data Expr = Val Int | Add Expr Expr+{-@ data Expr [height] = Val {theVal :: Int} | Add {summand1 :: Expr, summand2 :: Expr}  @-}+++{-@ height :: Expr -> Nat @-}+{-@ measure height @-}+height :: Expr -> Int+height (Val _) = 0+height (Add e1 e2) = 1 + if height e1 > height e2 then  height e1 else height e2++{- @ eval :: e:Expr -> Int / [height e] @-}+{-@ reflect eval @-}+eval :: Expr -> Int+eval (Val n)   = n+eval (Add x y) = eval x + eval y++type Stack = L Int++type Code = L Op++data Op = PUSH Int | ADD+{-@ data Op = PUSH {thePushed :: Int} | ADD @-}++{-@ reflect exec @-}+exec :: Code -> Stack -> Stack+exec N s                          = s+exec (C (PUSH n) c) s             = exec c (C n s)+exec (C ADD      c) (C m (C n s)) = exec c (C (n+m) s)+exec (C ADD      c) (C n N)       = N -- default case added+exec (C ADD      c) N             = N -- default case added (need to be sparate cases)++{-@ reflect comp @-}+comp :: Expr -> Code+comp (Val n)   = C (PUSH n) N+comp (Add x y) = (comp x ++ comp y) ++ (C ADD N)++-- Proofs++{-@ lemma_assoc4 :: as:L a -> bs:L a -> cs:L a -> ds:L a +                 -> {((as ++ bs) ++ cs) ++ ds  == as ++ (bs ++ (cs ++ ds)) }+  @-}+lemma_assoc4 :: L a -> L a -> L a -> L a -> Proof +lemma_assoc4 _ _ _ _ = undefined++{-@ lemma_app_nil :: x:a -> ys:L a -> { (C x N) ++ ys = C x ys } @-}+lemma_app_nil :: a -> L a -> Proof+lemma_app_nil _ _ = () ++{-@ correctness :: e:Expr -> c:Code -> s:Stack ->+                  { exec (comp e ++ c) s = exec c (C (eval e) s) }+@-}+correctness :: Expr -> Code -> Stack -> Proof+correctness (Val n) c s +  = [+    --   exec (comp (Val n) ++ c) s+    -- ==. exec ((C (PUSH n) N) ++ c) s+    -- ==. exec ((C (PUSH n) (N ++ c))) s+    -- ==. exec (C (PUSH n) c) s+    -- ==. exec c (C n s)+    -- ==. exec c (C (eval (Val n)) s)+    ] *** QED+++correctness (Add e1 e2) c s +  = [ +  --    exec (comp (Add e1 e2) ++ c) s +  -- ==. exec (((comp e1 ++ comp e2) ++ (C ADD N)) ++ c) s+  -- ==. exec (comp e1 ++ (comp e2 ++ ((C ADD N) ++ c))) s+      lemma_assoc4 (comp e1) (comp e2) (C ADD N) c+  -- ==. (exec (comp e2 ++ ((C ADD N) ++ c)) (C (eval e1) s))+    , correctness e1 (comp e2 ++ ((C ADD N) ++ c)) s+  -- ==. exec ((C ADD N) ++ c) (C (eval e2) (C (eval e1) s))+    , correctness e2 ((C ADD N) ++ c) (C (eval e1) s)+  -- ==. exec (C ADD c) (C (eval e2) (C (eval e1) s))+    , lemma_app_nil ADD c+  -- ==. exec c (C (eval e1 + eval e2) s)+  -- ==. exec c (C (eval (Add e1 e2)) s)+  ] *** QED    +
+ tests/pos/MaskError.hs view
@@ -0,0 +1,6 @@+module MaskError where ++{-@ assume Prelude.error :: String -> a @-}++foo :: Int -> Int +foo _ = error "oh no"
+ tests/pos/Streams.hs view
@@ -0,0 +1,107 @@+module Streams where++import Prelude hiding (take, repeat)++import Language.Haskell.Liquid.Prelude++-------------------------------------------------------------------------+-- | Lists +-------------------------------------------------------------------------+ +data List a = N | C { x :: a, xs :: List a }++-- | Associate an abstract refinement with the _tail_ xs++{-@ data List [size] a <p :: List a -> Bool>+      = N | C { x  :: a+              , xs :: List <p> a <<p>>+              }+  @-}++-------------------------------------------------------------------------+-- | Infinite Streams+-------------------------------------------------------------------------++-- | Infinite List = List where _each_ tail is a `kons` ...++{-@ type Stream a = {xs: List <{\v -> kons v}> a | kons xs} @-}++-- | A simple measure for when a `List` is a `Cons`++{-@ measure kons @-}+kons :: List a -> Bool +kons (C x xs) = True +kons (N)      = False ++-------------------------------------------------------------------------+-- | Creating an Infinite Stream+-------------------------------------------------------------------------++{-@ lazy repeat @-}+                 +{-@ repeat :: a -> Stream a @-}+repeat   :: a -> List a+repeat x = x `C` repeat x+++-------------------------------------------------------------------------+-- | Using an Infinite Stream+-------------------------------------------------------------------------++{-@ take        :: n:Nat -> Stream a -> {v:List a | size v = n} @-}+take 0 _        = N+take n (C x xs) = x `C` take (n-1) xs+take _ N        = liquidError "never happens"++-------------------------------------------------------------------------++++++++++++-- | Other specs from before ...++{-@ measure size @-}+{-@ size :: List a -> Nat @-} +size :: List a -> Int +size (N)      = 0+size (C x xs) = (1 + size xs)+++++++++++++++++++++++-----------------------------------------------------+take            :: Int -> List a -> List a+++++++++
tests/pos/T1126.hs view
@@ -7,12 +7,10 @@  instance OptEq a where {-@ instance OptEq a where-  ==. :: x:a -> y:{a| x == y} -> a+      ==. :: x:a -> y:{a| x == y} -> a   @-}   (==.) x _ = x -- class OptEq2 a where   cmp :: a -> a -> a @@ -22,11 +20,10 @@   @-}   cmp x _ = x - {-@ unsound :: x:Int -> {v:Int | v = x} -> Int @-} unsound :: Int -> Int -> Int-unsound x y = x ==. y +unsound x y = x ==. y  {-@ ok :: x:Int -> {v:Int | v = x} -> Int @-} ok :: Int -> Int -> Int-ok x y = x `cmp` y +ok x y = x `cmp` y
+ tests/pos/T1126a.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE FlexibleInstances #-}++module Instances where++class OptEq a where+  zoo :: a -> a -> a++instance OptEq a where+  {-@ instance OptEq a where+	zoo :: x:a -> y:{a | x == y} -> a+    @-}+  zoo x _ = x++instance OptEq Int where+  {-@ instance OptEq Int where+	zoo :: x:Int -> y:{Int| x == y} -> Int+    @-}+  zoo x _ = x+
+ tests/pos/T1220.hs view
@@ -0,0 +1,22 @@+{-@ LIQUID "--exactdc" @-}++module AB where++{-@ unsafe :: {t : AB | not (isA t)} -> {t /= A}  @-}+unsafe :: AB -> ()+unsafe t | isA t = ()+unsafe _ = ()++{-@ safe :: {t : AB | not (isA t)} -> {not (t == A)}  @-}+safe :: AB -> ()+safe t | isA t = ()+safe _ = ()++{-@ measure isA @-}+{-@ assume isA :: AB -> Bool @-}+isA :: AB -> Bool +isA A = True+isA B = False+++data AB = A | B
+ tests/pos/T1223.hs view
@@ -0,0 +1,78 @@+{-@ LIQUID "--exactdc" @-}+{-@ LIQUID "--higherorder" @-}+{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}+{-@ infix   ++ @-}++module Reverse where++import Prelude hiding (reverse, (++))++data Defined = Defined+infixl 2 ^^^+x ^^^ Defined = x +infixl 3 ==., ? ++x ? _ = x ++(==.) :: a -> a -> a +_ ==. x = x + ++++-------------------------------------------------------------------------------+-- | Specification of reverse' ------------------------------------------------+-------------------------------------------------------------------------------++{-@ specReverse' :: xs:[a] -> ys:[a] +                 -> {reverse' xs ys = reverse xs ++ ys} @-}+specReverse' :: [a] -> [a] -> ()+specReverse' _ _ = undefined   ++-------------------------------------------------------------------------------+-- | Derivation of reverse' ---------------------------------------------------+-------------------------------------------------------------------------------++-- LH TODO: LH is not letting you define a measure and a Haskell function+-- with the same name, for now...+{- measure reverse' :: [a] -> [a] -> [a] @-}+reverse' :: [a] -> [a] -> [a]+{-@ reverse' :: xs:[a] -> ys:[a] -> { reverse' xs ys = reverse xs ++ ys } @-}+reverse' [] ys +  =   reverse [] ++ ys +  ==. [] ++ ys ? specReverse' [] ys +  ==. ys +  ^^^ Defined +++reverse' (x:xs) ys +  =   reverse (x:xs) ++ ys  +  ==. (reverse xs ++ [x]) ++ ys ? specReverse' (x:xs) ys+  ==. reverse xs ++ ([x] ++ ys) ? assoc (reverse xs) [x] ys+  ==. reverse xs ++ (x:ys) +  ==. reverse' xs (x:ys)+  ^^^ Defined ++-------------------------------------------------------------------------------+-- | Helpers: Definitions & Theorems Used -------------------------------------+-------------------------------------------------------------------------------++{-@ reflect reverse @-}+reverse :: [a] -> [a]+reverse []     = []+reverse (x:xs) = reverse xs ++ [x]++{-@ reflect ++ @-}+(++) :: [a] -> [a] -> [a]+[]     ++ ys = ys+(x:xs) ++ ys = x:(xs ++ ys)+++{-@ automatic-instances assoc @-}+{-@ assoc :: xs:[a] -> ys:[a] -> zs:[a] +          -> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs }  @-}+assoc :: [a] -> [a] -> [a] -> () +assoc [] _ _       = ()+assoc (x:xs) ys zs = assoc xs ys zs++
− tests/pos/binah-EvalQuery.hs 
@@ -1,126 +0,0 @@-{-@ LIQUID "--no-adt" 	                           @-}-{-@ LIQUID "--exact-data-con"                      @-}-{-@ LIQUID "--higherorder"                         @-}-{-@ LIQUID "--no-termination"                      @-}-{-@ LIQUID "--ple" @-} --{-@ infixr === @-}-{-@ infixr >== @-}-{-@ infixr <== @-}--{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--module Query where--import Prelude hiding (filter)--data PersistFilter = EQUAL | LE | GE--class PersistEntity record where-    data EntityField record :: * -> *--{-@ data Filter record typ = Filter { filterField :: EntityField record typ, filterValue :: typ, filterFilter :: PersistFilter } @-}-data Filter record typ = Filter-    { filterField  :: EntityField record typ-    , filterValue  :: typ-    , filterFilter :: PersistFilter-    } ---{-@ reflect === @-}-(===) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field === value = Filter field value EQUAL--{-@ reflect <== @-}-(<==) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field <== value =-  Filter {-    filterField = field-  , filterValue = value-  , filterFilter = LE -  }--{-@ reflect >== @-}-(>==) :: (PersistEntity record, Eq typ) => -                 EntityField record typ -> typ -> Filter record typ-field >== value =-  Filter {-    filterField = field-  , filterValue = value-  , filterFilter = GE -  }--{-@ data Blob  = B { xVal :: Int, yVal :: Int } @-}-data Blob  = B { xVal :: Int, yVal :: Int }--instance PersistEntity Blob where-    {-@ data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-      | BlobYVal :: EntityField Blob Int-    @-}-    data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-        BlobYVal :: EntityField Blob Int--{-@ filter :: f:(a -> Bool) -> [a] -> [{v:a | f v}] @-}-filter :: (a -> Bool) -> [a] -> [a]-filter f (x:xs)-  | f x         = x : filter f xs-  | otherwise   =     filter f xs-filter _ []     = []--{-@ reflect evalQBlobXVal @-}-evalQBlobXVal :: PersistFilter -> Int -> Int -> Bool-evalQBlobXVal EQUAL filter given = filter == given-evalQBlobXVal LE filter given = given <= filter-evalQBlobXVal GE filter given = given >= filter--{-@ reflect evalQBlobYVal @-}-evalQBlobYVal :: PersistFilter -> Int -> Int -> Bool-evalQBlobYVal EQUAL filter given = filter == given-evalQBlobYVal LE filter given = given <= filter-evalQBlobYVal GE filter given = given >= filter--{-@ reflect evalQBlob @-}-evalQBlob :: Filter Blob typ -> Blob -> Bool-evalQBlob filter blob = case filterField filter of-    BlobXVal -> evalQBlobXVal (filterFilter filter) (filterValue filter) (xVal blob)-    BlobYVal -> evalQBlobYVal (filterFilter filter) (filterValue filter) (yVal blob)--{-@ reflect evalQsBlob @-}-evalQsBlob :: [Filter Blob typ] -> Blob -> Bool-evalQsBlob (f:fs) blob = evalQBlob f blob && (evalQsBlob fs blob)-evalQsBlob [] _ = True---{-@ filterQBlob :: f:(Filter Blob a) -> [Blob] -> [{b:Blob | evalQBlob f b}] @-}-filterQBlob :: Filter Blob a -> [Blob] -> [Blob]-filterQBlob q = filter (evalQBlob q)--{-@ filterQsBlob :: f:[(Filter Blob a)] -> [Blob] -> [{b:Blob | evalQsBlob f b}] @-}-filterQsBlob :: [Filter Blob a] -> [Blob] -> [Blob]-filterQsBlob qs = filter (evalQsBlob qs)---- select functions--{-@ assume selectBlob :: f:[(Filter Blob a)] -> [{b:Blob | evalQsBlob f b}] @-}-selectBlob :: [Filter Blob a] -> [Blob]-selectBlob fs = undefined --{-@ getZeros_ :: () -> [{b:Blob | xVal b = 0}] @-}-getZeros_ :: () -> [Blob]-getZeros_ () = selectBlob [(Filter BlobXVal 0 EQUAL)]--{-@ getBiggerThan10 :: () -> [{b:Blob | xVal b >= 10}] @-}-getBiggerThan10 :: () -> [Blob]-getBiggerThan10 () = selectBlob [(Filter BlobXVal 11 GE)]--{-@ getInRange :: () -> [{b:Blob | xVal b >= 10  && xVal b <= 20 && yVal b >= 0 && yVal b <= 11}] @-}-getInRange :: () -> [Blob]-getInRange () = selectBlob [ (BlobXVal >== 10)-                           , (BlobXVal <== 20)-                           , (BlobYVal >== 0)-                           , (BlobYVal <== 11)-                           ]
− tests/pos/binah-UpdateQuery.hs 
@@ -1,40 +0,0 @@-{-@ LIQUID "--no-adt" 	                           @-}-{-@ LIQUID "--exact-data-con"                      @-}-{-@ LIQUID "--higherorder"                         @-}-{-@ LIQUID "--no-termination"                      @-}-{-@ LIQUID "--ple" @-} --{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--class PersistEntity record where-    data EntityField record :: * -> *--instance PersistEntity Blob where-    {-@ data EntityField Blob typ where-        BlobXVal :: EntityField Blob {v:Int | v >= 0}-      | BlobYVal :: EntityField Blob Int-    @-}-    data EntityField Blob typ where-        BlobXVal :: EntityField Blob Int-        BlobYVal :: EntityField Blob Int--{-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}-data Blob  = B { xVal :: Int, yVal :: Int }--{-@ data Update record typ = Update { updateField :: EntityField record typ, updateValue :: typ } @-}-data Update record typ = Update -    { updateField :: EntityField record typ-    , updateValue :: typ-    } --{-@ data variance Update covariant covariant contravariant @-}--{-@ createUpdate :: EntityField record a -> a -> Update record a @-}-createUpdate :: EntityField record a -> a -> Update record a-createUpdate field value = Update {-      updateField = field-    , updateValue = value-}--testUpdateQuery :: () -> Update Blob Int-testUpdateQuery () = createUpdate BlobXVal 3
+ tests/pos/filterPLE.hs view
@@ -0,0 +1,31 @@+{-@ LIQUID "--no-termination" @-}+{-@ LIQUID "--short-names"    @-}+{-@ LIQUID "--higherorder"    @-}+{-@ LIQUID "--ple"            @-}++module Filter where++import Prelude hiding (filter)++{-@ filter :: f:(a -> Bool) -> [a] -> [{v:a | f v}] @-}+filter :: (a -> Bool) -> [a] -> [a]+filter f (x:xs)+  | f x         = x : filter f xs+  | otherwise   =     filter f xs+filter _ []     = []++{-@ reflect isPos @-} +isPos :: Int -> Bool+isPos n = n > 0++{-@ reflect isNeg @-} +isNeg :: Int -> Bool+isNeg n = n < 0++{-@ positives :: [Int] -> [{v:Int | v > 0}] @-}+positives :: [Int] -> [Int]+positives xs = filter isPos xs++{-@ negatives :: [Int] -> [{v:Int | v < 0}] @-}+negatives :: [Int] -> [Int]+negatives xs = filter isNeg xs
tests/pos/pleORM.hs view
@@ -8,8 +8,8 @@ import Prelude hiding (length, filter)  --  here is a "user" query-{-@ prop0 :: [Row] -> [{v:Row | rowLeft v == 5}] @-}-prop0 :: [Row] -> [Row]+{-@ prop0 :: [Blob] -> [{v:Blob | xVal v == 5}] @-}+prop0 :: [Blob] -> [Blob] prop0 = filterQ (Qry Eq Fst (Const 5))  {-@ prop1 :: [Int] -> [{v:Int | v == 10}] @-}@@ -24,8 +24,8 @@ mkQQ :: Int -> QQ mkQQ n = QQ n -{-@ filterQ :: q:Qry -> [Row] -> [{v:Row | evalQ q v}] @-}-filterQ :: Qry -> [Row] -> [Row]+{-@ filterQ :: q:Qry -> [Blob] -> [{v:Blob | evalQ q v}] @-}+filterQ :: Qry -> [Blob] -> [Blob] filterQ q = filter (evalQ q)  {-@ filterQQ :: q:QQ -> [Int] -> [{v:Int | evalQQ q v}] @-}@@ -44,22 +44,22 @@ data QQ  = QQ Int  -data Row = Row {rowLeft :: Int, rowRight :: Int}-{-@ data Row = Row {rowLeft :: Int, rowRight :: Int} @-}+{-@ data Blob = Blob {xVal :: Int, yVal :: Int} @-}+data Blob = Blob {xVal :: Int, yVal :: Int}  {-@ reflect evalQQ @-} evalQQ :: QQ -> Int -> Bool evalQQ (QQ x) y = x == y  {-@ reflect evalQ @-}-evalQ :: Qry -> Row -> Bool+evalQ :: Qry -> Blob -> Bool evalQ (Qry o v1 v2) r = evalC o (evalV v1 r) (evalV v2 r)  {-@ reflect evalV @-}-evalV :: Val -> Row -> Int+evalV :: Val -> Blob -> Int evalV (Const n) _ = n-evalV Fst       r = rowLeft  r-evalV Snd       r = rowRight r+evalV Fst       r = xVal  r+evalV Snd       r = yVal r  {-@ reflect evalC @-} evalC :: Cmp -> Int -> Int -> Bool
tests/test.hs view
@@ -107,7 +107,7 @@   , errorTest "tests/errors/DupFunSigs.hs"          2 "Multiple specifications for `Main.fromWeekDayNum`"   , errorTest "tests/errors/DupMeasure.hs"          2 "Multiple measures named `lenA`"   , errorTest "tests/errors/ShadowFieldInline.hs"   2 "Malformed application of type alias `Range.pig`"-  , errorTest "tests/errors/ShadowFieldReflect.hs"  2 "Illegal type specification for `assumed type Range.pig`"+  , errorTest "tests/errors/ShadowFieldReflect.hs"  2 "Error: Illegal type specification for `Range.prop`"   , errorTest "tests/errors/ShadowMeasure.hs"       2 "Multiple specifications for `shadow`"   , errorTest "tests/errors/ShadowMeasureVar.hs"    2 "Multiple specifications for `shadow`"   , errorTest "tests/errors/DupData.hs"             2 "Multiple specifications for `OVec`"@@ -120,7 +120,6 @@   , errorTest "tests/errors/UnboundVarInSpec.hs"    2 "Illegal type specification for `Fixme.foo`"   , errorTest "tests/errors/MissingAbsRefArgs.hs"   2 "Illegal type specification for `Fixme.bar`"   , errorTest "tests/errors/UnboundVarInAssume.hs"  2 "Illegal type specification for `Assume.incr`"-  , errorTest "tests/errors/UnboundVarInAssume1.hs" 2 "Illegal type specification for `Main.b`"   , errorTest "tests/errors/UnboundFunInSpec.hs"    2 "Illegal type specification for `Goo.three`"   , errorTest "tests/errors/UnboundFunInSpec1.hs"   2 "Illegal type specification for `Goo.foo`"   , errorTest "tests/errors/UnboundFunInSpec2.hs"   2 "Illegal type specification for `Goo.foo`"