{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -- | This module should contain all the global type definitions and basic instances. module Language.Haskell.Liquid.Types ( -- * Options Config (..) -- * Ghc Information , GhcInfo (..) , GhcSpec (..) , TargetVars (..) -- * Located Things , Located (..) , dummyLoc -- * Symbols , LocSymbol , LocText -- * Default unknown name , dummyName, isDummy -- * Refined Type Constructors , RTyCon (RTyCon, rtc_tc, rtc_info) , TyConInfo(..), defaultTyConInfo , rTyConPVs , rTyConPropVs , isClassRTyCon, isClassType -- * Refinement Types , RType (..), Ref(..), RTProp , RTyVar (..) , RTAlias (..) -- * Worlds , HSeg (..) , World (..) -- * Classes describing operations on `RTypes` , TyConable (..) , RefTypable (..) , SubsTy (..) -- * Predicate Variables , PVar (PV, pname, parg, ptype, pargs), isPropPV, pvType , PVKind (..) , Predicate (..) -- * Refinements , UReft(..) -- * Parse-time entities describing refined data types , DataDecl (..) , DataConP (..) , TyConP (..) -- * Pre-instantiated RType , RRType, BRType, RRProp , BSort, BPVar -- * Instantiated RType , BareType, PrType , SpecType, SpecProp , RSort , UsedPVar, RPVar, RReft , REnv (..) -- * Constructing & Destructing RTypes , RTypeRep(..), fromRTypeRep, toRTypeRep , mkArrow, bkArrowDeep, bkArrow, safeBkArrow , mkUnivs, bkUniv, bkClass , rFun, rCls, rRCls -- * Manipulating `Predicates` , pvars, pappSym, pApp -- * Some tests on RTypes , isBase , isFunTy , isTrivial -- * Traversing `RType` , efoldReft, foldReft , mapReft, mapReftM , mapBot, mapBind -- * ??? , Oblig(..) , ignoreOblig , addTermCond , addInvCond -- * Inferred Annotations , AnnInfo (..) , Annot (..) -- * Overall Output , Output (..) -- * Refinement Hole , hole, isHole, hasHole -- * Converting To and From Sort , ofRSort, toRSort , rTypeValueVar , rTypeReft , stripRTypeBase -- * Class for values that can be pretty printed , PPrint (..) , showpp -- * Printer Configuration , PPEnv (..) , Tidy (..) , ppEnv , ppEnvShort -- * Modules and Imports , ModName (..), ModType (..) , isSrcImport, isSpecImport , getModName, getModString -- * Refinement Type Aliases , RTEnv (..) , mapRT, mapRP, mapRE -- * Final Result , Result (..) -- * Errors and Error Messages , Error , TError (..) , EMsg (..) -- , LParseError (..) , ErrorResult , errSpan , errOther , errToFCrash -- * Source information (associated with constraints) , Cinfo (..) -- * Measures , Measure (..) , CMeasure (..) , Def (..) , Body (..) -- * Type Classes , RClass (..) -- * KV Profiling , KVKind (..) -- types of kvars , KVProf -- profile table , emptyKVProf -- empty profile , updKVProf -- extend profile -- * Misc , mapRTAVars , insertsSEnv -- * Strata , Stratum(..), Strata , isSVar , getStrata , makeDivType, makeFinType -- * CoreToLogic , LogicMap, toLogicMap, eAppWithMap, LMap(..) -- * Refined Instances , RDEnv, DEnv(..), RInstance(..) -- * Ureftable Instances , UReftable(..) ) where import SrcLoc (noSrcSpan, SrcSpan) import TyCon import DataCon import NameSet import Module (moduleNameFS) import TypeRep hiding (maybeParen, pprArrowChain) import Var import Text.Printf import GHC (HscEnv, ModuleName, moduleNameString) import GHC.Generics import Language.Haskell.Liquid.GhcMisc import PrelInfo (isNumericClass) import TysWiredIn (listTyCon) import Control.Arrow (second) import Control.Monad (liftM, liftM2, liftM3, liftM4) import qualified Control.Monad.Error as Ex import Control.DeepSeq import Control.Applicative ((<$>)) import Data.Typeable (Typeable) import Data.Generics (Data) import Data.Monoid hiding ((<>)) import qualified Data.Foldable as F import Data.Hashable import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import Data.Maybe (fromMaybe) import Data.Traversable hiding (mapM) import Data.List (nub) import Data.Text (Text) import qualified Data.Text as T import Text.Parsec.Pos (SourcePos) import Text.Parsec.Error (ParseError) import Text.PrettyPrint.HughesPJ import Language.Fixpoint.Config hiding (Config) import Language.Fixpoint.Misc import Language.Fixpoint.Types hiding (Result, Predicate, Def, R) import Language.Fixpoint.Names (funConName, listConName, tupConName) import qualified Language.Fixpoint.PrettyPrint as F import CoreSyn (CoreBind) import Language.Haskell.Liquid.Variance import Language.Haskell.Liquid.Misc (mapSndM, safeZip3WithError) import Data.Default ----------------------------------------------------------------------------- -- | Command Line Config Options -------------------------------------------- ----------------------------------------------------------------------------- -- NOTE: adding strictness annotations breaks the help message data Config = Config { files :: [FilePath] -- ^ source files to check , idirs :: [FilePath] -- ^ path to directory for including specs , diffcheck :: Bool -- ^ check subset of binders modified (+ dependencies) since last check , real :: Bool -- ^ supports real number arithmetic , fullcheck :: Bool -- ^ check all binders (overrides diffcheck) , native :: Bool -- ^ use native (Haskell) fixpoint constraint solver , binders :: [String] -- ^ set of binders to check , noCheckUnknown :: Bool -- ^ whether to complain about specifications for unexported and unused values , notermination :: Bool -- ^ disable termination check , nowarnings :: Bool -- ^ disable warnings output (only show errors) , trustinternals :: Bool -- ^ type all internal variables with true , nocaseexpand :: Bool -- ^ disable case expand , strata :: Bool -- ^ enable strata analysis , notruetypes :: Bool -- ^ disable truing top level types , totality :: Bool -- ^ check totality in definitions , noPrune :: Bool -- ^ disable prunning unsorted Refinements , maxParams :: Int -- ^ the maximum number of parameters to accept when mining qualifiers , smtsolver :: Maybe SMTSolver -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order] , shortNames :: Bool -- ^ drop module qualifers from pretty-printed names. , shortErrors :: Bool -- ^ don't show subtyping errors and contexts. , ghcOptions :: [String] -- ^ command-line options to pass to GHC , cFiles :: [String] -- ^ .c files to compile and link against (for GHC) } deriving (Data, Typeable, Show, Eq) ----------------------------------------------------------------------------- -- | Printer ---------------------------------------------------------------- ----------------------------------------------------------------------------- data Tidy = Lossy | Full deriving (Eq, Ord) class PPrint a where pprint :: a -> Doc pprintTidy :: Tidy -> a -> Doc pprintTidy _ = pprint showpp :: (PPrint a) => a -> String showpp = render . pprint instance PPrint a => PPrint (Maybe a) where pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint) instance PPrint a => PPrint [a] where pprint = brackets . intersperse comma . map pprint instance (PPrint a, PPrint b) => PPrint (a,b) where pprint (x, y) = pprint x <+> text ":" <+> pprint y data PPEnv = PP { ppPs :: Bool , ppTyVar :: Bool -- TODO if set to True all Bare fails , ppSs :: Bool , ppShort :: Bool } ppEnv = ppEnvPrintPreds _ppEnvCurrent = PP False False False False ppEnvPrintPreds = PP False False False False ppEnvShort pp = pp { ppShort = True } ------------------------------------------------------------------ -- | GHC Information : Code & Spec ------------------------------ ------------------------------------------------------------------ data GhcInfo = GI { env :: !HscEnv , cbs :: ![CoreBind] , derVars :: ![Var] , impVars :: ![Var] , defVars :: ![Var] , useVars :: ![Var] , hqFiles :: ![FilePath] , imports :: ![String] , includes :: ![FilePath] , spec :: !GhcSpec } -- | The following is the overall type for /specifications/ obtained from -- parsing the target source and dependent libraries data GhcSpec = SP { tySigs :: ![(Var, Located SpecType)] -- ^ Asserted Reftypes -- eg. see include/Prelude.spec , asmSigs :: ![(Var, Located SpecType)] -- ^ Assumed Reftypes , ctors :: ![(Var, Located SpecType)] -- ^ Data Constructor Measure Sigs -- eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) } , meas :: ![(Symbol, Located SpecType)] -- ^ Measure Types -- eg. len :: [a] -> Int , invariants :: ![Located SpecType] -- ^ Data Type Invariants -- eg. forall a. {v: [a] | len(v) >= 0} , ialiases :: ![(Located SpecType, Located SpecType)] -- ^ Data Type Invariant Aliases , dconsP :: ![(DataCon, DataConP)] -- ^ Predicated Data-Constructors -- e.g. see tests/pos/Map.hs , tconsP :: ![(TyCon, TyConP)] -- ^ Predicated Type-Constructors -- eg. see tests/pos/Map.hs , freeSyms :: ![(Symbol, Var)] -- ^ List of `Symbol` free in spec and corresponding GHC var -- eg. (Cons, Cons#7uz) from tests/pos/ex1.hs , tcEmbeds :: TCEmb TyCon -- ^ How to embed GHC Tycons into fixpoint sorts -- e.g. "embed Set as Set_set" from include/Data/Set.spec , qualifiers :: ![Qualifier] -- ^ Qualifiers in Source/Spec files -- e.g tests/pos/qualTest.hs , tgtVars :: ![Var] -- ^ Top-level Binders To Verify (empty means ALL binders) , decr :: ![(Var, [Int])] -- ^ Lexicographically ordered size witnesses for termination , texprs :: ![(Var, [Expr])] -- ^ Lexicographically ordered expressions for termination , lvars :: !(S.HashSet Var) -- ^ Variables that should be checked in the environment they are used , lazy :: !(S.HashSet Var) -- ^ Binders to IGNORE during termination checking , config :: !Config -- ^ Configuration Options , exports :: !NameSet -- ^ `Name`s exported by the module being verified , measures :: [Measure SpecType DataCon] , tyconEnv :: M.HashMap TyCon RTyCon , dicts :: DEnv Var SpecType -- ^ Dictionary Environment } type LogicMap = M.HashMap Symbol LMap data LMap = LMap { lvar :: Symbol , largs :: [Symbol] , lexpr :: Expr } instance Show LMap where show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t|->\t" ++ show e toLogicMap = M.fromList . map toLMap where toLMap (x, xs, e) = (x, LMap {lvar = x, largs = xs, lexpr = e}) eAppWithMap lmap f es def | Just (LMap _ xs e) <- M.lookup (val f) lmap = subst (mkSubst $ zip xs es) e | otherwise = def data TyConP = TyConP { freeTyVarsTy :: ![RTyVar] , freePredTy :: ![PVar RSort] , freeLabelTy :: ![Symbol] , varianceTs :: !VarianceInfo , variancePs :: !VarianceInfo , sizeFun :: !(Maybe (Symbol -> Expr)) } deriving (Data, Typeable) data DataConP = DataConP { dc_loc :: !SourcePos , freeTyVars :: ![RTyVar] , freePred :: ![PVar RSort] , freeLabels :: ![Symbol] , tyConsts :: ![SpecType] -- ^ FIXME: WHAT IS THIS?? , tyArgs :: ![(Symbol, SpecType)] -- ^ These are backwards, why?? , tyRes :: !SpecType , dc_locE :: !SourcePos } deriving (Data, Typeable) -- | Which Top-Level Binders Should be Verified data TargetVars = AllVars | Only ![Var] -------------------------------------------------------------------- -- | Abstract Predicate Variables ---------------------------------- -------------------------------------------------------------------- data PVar t = PV { pname :: !Symbol , ptype :: !(PVKind t) , parg :: !Symbol , pargs :: ![(t, Symbol, Expr)] } deriving (Generic, Data, Typeable, Show) pvType p = case ptype p of PVProp t -> t PVHProp -> errorstar "pvType on HProp-PVar" data PVKind t = PVProp t | PVHProp deriving (Generic, Data, Typeable, F.Foldable, Traversable, Show) instance Eq (PVar t) where pv == pv' = pname pv == pname pv' {- UNIFY: What about: && eqArgs pv pv' -} instance Ord (PVar t) where compare (PV n _ _ _) (PV n' _ _ _) = compare n n' instance Functor PVKind where fmap f (PVProp t) = PVProp (f t) fmap _ (PVHProp) = PVHProp instance Functor PVar where fmap f (PV x t v txys) = PV x (f <$> t) v (mapFst3 f <$> txys) instance (NFData a) => NFData (PVKind a) where rnf (PVProp t) = rnf t rnf (PVHProp) = () instance (NFData a) => NFData (PVar a) where rnf (PV n t v txys) = rnf n `seq` rnf v `seq` rnf t `seq` rnf txys instance Hashable (PVar a) where hashWithSalt i (PV n _ _ _) = hashWithSalt i n -------------------------------------------------------------------- ------ Strictness -------------------------------------------------- -------------------------------------------------------------------- instance NFData Var where rnf x = seq x () instance NFData SrcSpan where rnf x = seq x () -------------------------------------------------------------------- ------------------ Predicates -------------------------------------- -------------------------------------------------------------------- type UsedPVar = PVar () newtype Predicate = Pr [UsedPVar] deriving (Generic, Data, Typeable) instance NFData Predicate where rnf _ = () instance Monoid Predicate where mempty = pdTrue mappend p p' = pdAnd [p, p'] instance (Monoid a) => Monoid (UReft a) where mempty = U mempty mempty mempty mappend (U x y z) (U x' y' z') = U (mappend x x') (mappend y y') (mappend z z') pdTrue = Pr [] pdAnd ps = Pr (nub $ concatMap pvars ps) pvars (Pr pvs) = pvs instance Subable UsedPVar where syms pv = [ y | (_, x, EVar y) <- pargs pv, x /= y ] subst s pv = pv { pargs = mapThd3 (subst s) <$> pargs pv } substf f pv = pv { pargs = mapThd3 (substf f) <$> pargs pv } substa f pv = pv { pargs = mapThd3 (substa f) <$> pargs pv } instance Subable Predicate where syms (Pr pvs) = concatMap syms pvs subst s (Pr pvs) = Pr (subst s <$> pvs) substf f (Pr pvs) = Pr (substf f <$> pvs) substa f (Pr pvs) = Pr (substa f <$> pvs) instance Subable Qualifier where syms = syms . q_body subst = mapQualBody . subst substf = mapQualBody . substf substa = mapQualBody . substa mapQualBody f q = q { q_body = f (q_body q) } instance NFData r => NFData (UReft r) where rnf (U r p s) = rnf r `seq` rnf p `seq` rnf s instance NFData Strata where rnf _ = () instance NFData PrType where rnf _ = () instance NFData RTyVar where rnf _ = () -- MOVE TO TYPES newtype RTyVar = RTV TyVar deriving (Generic, Data, Typeable) instance Symbolic RTyVar where symbol (RTV tv) = symbol . T.pack . showPpr $ tv data RTyCon = RTyCon { rtc_tc :: TyCon -- ^ GHC Type Constructor , rtc_pvars :: ![RPVar] -- ^ Predicate Parameters , rtc_info :: !TyConInfo -- ^ TyConInfo } deriving (Generic, Data, Typeable) -- | Accessors for @RTyCon@ isClassRTyCon = isClassTyCon . rtc_tc rTyConPVs = rtc_pvars rTyConPropVs = filter isPropPV . rtc_pvars isPropPV = isProp . ptype isClassType (RApp c _ _ _) = isClass c isClassType _ = False -- rTyConPVHPs = filter isHPropPV . rtc_pvars -- isHPropPV = not . isPropPV isProp (PVProp _) = True isProp _ = False defaultTyConInfo = TyConInfo [] [] Nothing instance Default TyConInfo where def = defaultTyConInfo ----------------------------------------------------------------------- -- | Co- and Contra-variance for TyCon -------------------------------- ----------------------------------------------------------------------- -- | Indexes start from 0 and type or predicate arguments can be both -- covariant and contravaariant e.g., for the below Foo dataType -- -- data Foo a b c d
Prop, q :: Int -> Prop, r :: a -> Prop>
-- = F (a ) | Q (c -> a) | G (Int -> a