diff --git a/devel/Paths_liquidhaskell.hs b/devel/Paths_liquidhaskell.hs --- a/devel/Paths_liquidhaskell.hs +++ b/devel/Paths_liquidhaskell.hs @@ -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] diff --git a/include/Language/Haskell/Liquid/NewProofCombinators.hs b/include/Language/Haskell/Liquid/NewProofCombinators.hs --- a/include/Language/Haskell/Liquid/NewProofCombinators.hs +++ b/include/Language/Haskell/Liquid/NewProofCombinators.hs @@ -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 diff --git a/include/Language/Haskell/Liquid/ProofCombinators.hs b/include/Language/Haskell/Liquid/ProofCombinators.hs --- a/include/Language/Haskell/Liquid/ProofCombinators.hs +++ b/include/Language/Haskell/Liquid/ProofCombinators.hs @@ -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 ------------------------------------------------------------------------------- diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs --- a/src/Language/Haskell/Liquid/Bare.hs +++ b/src/Language/Haskell/Liquid/Bare.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs --- a/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs --- a/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/src/Language/Haskell/Liquid/Bare/Check.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/DataType.hs b/src/Language/Haskell/Liquid/Bare/DataType.hs --- a/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Bare/Env.hs b/src/Language/Haskell/Liquid/Bare/Env.hs --- a/src/Language/Haskell/Liquid/Bare/Env.hs +++ b/src/Language/Haskell/Liquid/Bare/Env.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs --- a/src/Language/Haskell/Liquid/Bare/Expand.hs +++ b/src/Language/Haskell/Liquid/Bare/Expand.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Lookup.hs b/src/Language/Haskell/Liquid/Bare/Lookup.hs --- a/src/Language/Haskell/Liquid/Bare/Lookup.hs +++ b/src/Language/Haskell/Liquid/Bare/Lookup.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs --- a/src/Language/Haskell/Liquid/Bare/Measure.hs +++ b/src/Language/Haskell/Liquid/Bare/Measure.hs @@ -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))] diff --git a/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs --- a/src/Language/Haskell/Liquid/Bare/Misc.hs +++ b/src/Language/Haskell/Liquid/Bare/Misc.hs @@ -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 [] diff --git a/src/Language/Haskell/Liquid/Bare/OfType.hs b/src/Language/Haskell/Liquid/Bare/OfType.hs --- a/src/Language/Haskell/Liquid/Bare/OfType.hs +++ b/src/Language/Haskell/Liquid/Bare/OfType.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs --- a/src/Language/Haskell/Liquid/Bare/Plugged.hs +++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Spec.hs b/src/Language/Haskell/Liquid/Bare/Spec.hs --- a/src/Language/Haskell/Liquid/Bare/Spec.hs +++ b/src/Language/Haskell/Liquid/Bare/Spec.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Constraint/Init.hs b/src/Language/Haskell/Liquid/Constraint/Init.hs --- a/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Desugar/Coverage.hs b/src/Language/Haskell/Liquid/Desugar/Coverage.hs --- a/src/Language/Haskell/Liquid/Desugar/Coverage.hs +++ b/src/Language/Haskell/Liquid/Desugar/Coverage.hs @@ -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-} diff --git a/src/Language/Haskell/Liquid/Desugar/DsExpr.hs b/src/Language/Haskell/Liquid/Desugar/DsExpr.hs --- a/src/Language/Haskell/Liquid/Desugar/DsExpr.hs +++ b/src/Language/Haskell/Liquid/Desugar/DsExpr.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Desugar/DsMonad.hs b/src/Language/Haskell/Liquid/Desugar/DsMonad.hs --- a/src/Language/Haskell/Liquid/Desugar/DsMonad.hs +++ b/src/Language/Haskell/Liquid/Desugar/DsMonad.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/GHC/Misc.hs b/src/Language/Haskell/Liquid/GHC/Misc.hs --- a/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -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 ] diff --git a/src/Language/Haskell/Liquid/Misc.hs b/src/Language/Haskell/Liquid/Misc.hs --- a/src/Language/Haskell/Liquid/Misc.hs +++ b/src/Language/Haskell/Liquid/Misc.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Parse.hs b/src/Language/Haskell/Liquid/Parse.hs --- a/src/Language/Haskell/Liquid/Parse.hs +++ b/src/Language/Haskell/Liquid/Parse.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Types.hs b/src/Language/Haskell/Liquid/Types.hs --- a/src/Language/Haskell/Liquid/Types.hs +++ b/src/Language/Haskell/Liquid/Types.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Types/Dictionaries.hs b/src/Language/Haskell/Liquid/Types/Dictionaries.hs --- a/src/Language/Haskell/Liquid/Types/Dictionaries.hs +++ b/src/Language/Haskell/Liquid/Types/Dictionaries.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Types/Meet.hs b/src/Language/Haskell/Liquid/Types/Meet.hs --- a/src/Language/Haskell/Liquid/Types/Meet.hs +++ b/src/Language/Haskell/Liquid/Types/Meet.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Types/PredType.hs b/src/Language/Haskell/Liquid/Types/PredType.hs --- a/src/Language/Haskell/Liquid/Types/PredType.hs +++ b/src/Language/Haskell/Liquid/Types/PredType.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -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) diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -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, diff --git a/tests/errors/UnboundVarInAssume1.hs b/tests/errors/UnboundVarInAssume1.hs deleted file mode 100644 --- a/tests/errors/UnboundVarInAssume1.hs +++ /dev/null @@ -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 diff --git a/tests/import/client/ExactGADT9.hs b/tests/import/client/ExactGADT9.hs new file mode 100644 --- /dev/null +++ b/tests/import/client/ExactGADT9.hs @@ -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 diff --git a/tests/import/lib/ExactGADT8.hs b/tests/import/lib/ExactGADT8.hs new file mode 100644 --- /dev/null +++ b/tests/import/lib/ExactGADT8.hs @@ -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 diff --git a/tests/neg/BinahQuery.hs b/tests/neg/BinahQuery.hs new file mode 100644 --- /dev/null +++ b/tests/neg/BinahQuery.hs @@ -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) + ] diff --git a/tests/neg/BinahUpdate.hs b/tests/neg/BinahUpdate.hs new file mode 100644 --- /dev/null +++ b/tests/neg/BinahUpdate.hs @@ -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 diff --git a/tests/neg/BinahUpdateClient.hs b/tests/neg/BinahUpdateClient.hs new file mode 100644 --- /dev/null +++ b/tests/neg/BinahUpdateClient.hs @@ -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 diff --git a/tests/neg/BinahUpdateLib.hs b/tests/neg/BinahUpdateLib.hs new file mode 100644 --- /dev/null +++ b/tests/neg/BinahUpdateLib.hs @@ -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 diff --git a/tests/neg/BinahUpdateLib1.hs b/tests/neg/BinahUpdateLib1.hs new file mode 100644 --- /dev/null +++ b/tests/neg/BinahUpdateLib1.hs @@ -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 diff --git a/tests/neg/binah-EvalQuery.hs b/tests/neg/binah-EvalQuery.hs deleted file mode 100644 --- a/tests/neg/binah-EvalQuery.hs +++ /dev/null @@ -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) - ] diff --git a/tests/neg/binah-UpdateQuery.hs b/tests/neg/binah-UpdateQuery.hs deleted file mode 100644 --- a/tests/neg/binah-UpdateQuery.hs +++ /dev/null @@ -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) diff --git a/tests/pos/BinahQuery.hs b/tests/pos/BinahQuery.hs new file mode 100644 --- /dev/null +++ b/tests/pos/BinahQuery.hs @@ -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) + ] diff --git a/tests/pos/BinahUpdate.hs b/tests/pos/BinahUpdate.hs new file mode 100644 --- /dev/null +++ b/tests/pos/BinahUpdate.hs @@ -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 diff --git a/tests/pos/Compiler.hs b/tests/pos/Compiler.hs new file mode 100644 --- /dev/null +++ b/tests/pos/Compiler.hs @@ -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 + -} + + + + + + + +--- diff --git a/tests/pos/ExactGADT1.hs b/tests/pos/ExactGADT1.hs --- a/tests/pos/ExactGADT1.hs +++ b/tests/pos/ExactGADT1.hs @@ -1,4 +1,4 @@ -{-@ LIQUID "--exact-data-con" @-} +{-@ LIQUID "--exact-data-con" @-} {-# LANGUAGE GADTs #-} diff --git a/tests/pos/ExactGADT5.hs b/tests/pos/ExactGADT5.hs --- a/tests/pos/ExactGADT5.hs +++ b/tests/pos/ExactGADT5.hs @@ -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 diff --git a/tests/pos/ExactGADT8a.hs b/tests/pos/ExactGADT8a.hs new file mode 100644 --- /dev/null +++ b/tests/pos/ExactGADT8a.hs @@ -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 + diff --git a/tests/pos/ExactGADT9a.hs b/tests/pos/ExactGADT9a.hs new file mode 100644 --- /dev/null +++ b/tests/pos/ExactGADT9a.hs @@ -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 + diff --git a/tests/pos/Hutton.hs b/tests/pos/Hutton.hs new file mode 100644 --- /dev/null +++ b/tests/pos/Hutton.hs @@ -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 + diff --git a/tests/pos/MaskError.hs b/tests/pos/MaskError.hs new file mode 100644 --- /dev/null +++ b/tests/pos/MaskError.hs @@ -0,0 +1,6 @@ +module MaskError where + +{-@ assume Prelude.error :: String -> a @-} + +foo :: Int -> Int +foo _ = error "oh no" diff --git a/tests/pos/Streams.hs b/tests/pos/Streams.hs new file mode 100644 --- /dev/null +++ b/tests/pos/Streams.hs @@ -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

Bool> + = N | C { x :: a + , xs :: List

a <

> + } + @-} + +------------------------------------------------------------------------- +-- | 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 + + + + + + + + + diff --git a/tests/pos/T1126.hs b/tests/pos/T1126.hs --- a/tests/pos/T1126.hs +++ b/tests/pos/T1126.hs @@ -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 diff --git a/tests/pos/T1126a.hs b/tests/pos/T1126a.hs new file mode 100644 --- /dev/null +++ b/tests/pos/T1126a.hs @@ -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 + diff --git a/tests/pos/T1220.hs b/tests/pos/T1220.hs new file mode 100644 --- /dev/null +++ b/tests/pos/T1220.hs @@ -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 diff --git a/tests/pos/T1223.hs b/tests/pos/T1223.hs new file mode 100644 --- /dev/null +++ b/tests/pos/T1223.hs @@ -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 + + diff --git a/tests/pos/binah-EvalQuery.hs b/tests/pos/binah-EvalQuery.hs deleted file mode 100644 --- a/tests/pos/binah-EvalQuery.hs +++ /dev/null @@ -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) - ] diff --git a/tests/pos/binah-UpdateQuery.hs b/tests/pos/binah-UpdateQuery.hs deleted file mode 100644 --- a/tests/pos/binah-UpdateQuery.hs +++ /dev/null @@ -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 diff --git a/tests/pos/filterPLE.hs b/tests/pos/filterPLE.hs new file mode 100644 --- /dev/null +++ b/tests/pos/filterPLE.hs @@ -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 diff --git a/tests/pos/pleORM.hs b/tests/pos/pleORM.hs --- a/tests/pos/pleORM.hs +++ b/tests/pos/pleORM.hs @@ -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 diff --git a/tests/test.hs b/tests/test.hs --- a/tests/test.hs +++ b/tests/test.hs @@ -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`"