{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE TupleSections #-} -- | This module should contain all the global type definitions and basic instances. module Language.Haskell.Liquid.Types.Types ( -- * Options module Language.Haskell.Liquid.UX.Config -- * Ghc Information , TargetVars (..) , TyConMap (..) -- * F.Located Things , F.Located (..) , F.dummyLoc -- * Symbols , F.LocSymbol , F.LocText -- * Default unknown name , F.dummyName , F.isDummy -- * Bare Type Constructors and Variables , BTyCon(..) , mkBTyCon -- , mkClassBTyCon, mkPromotedBTyCon , isClassBTyCon , BTyVar(..) -- * Refined Type Constructors , RTyCon (RTyCon, rtc_tc, rtc_info) , TyConInfo(..), defaultTyConInfo , rTyConPVs , rTyConPropVs -- , isClassRTyCon , isClassType, isEqType, isRVar, isBool -- * Refinement Types , RType (..), Ref(..), RTProp, rPropP , RTyVar (..) , RTAlias (..) , OkRT , lmapEAlias , dropImplicits -- * Worlds , HSeg (..) , World (..) -- * Classes describing operations on `RTypes` , TyConable (..) , SubsTy (..) -- * Type Variables , RTVar (..), RTVInfo (..) , makeRTVar, mapTyVarValue , dropTyVarInfo, rTVarToBind -- * Predicate Variables , PVar (PV, pname, parg, ptype, pargs), isPropPV, pvType , PVKind (..) , Predicate (..) -- * Refinements , UReft(..) -- * Parse-time entities describing refined data types , SizeFun (..), szFun , DataDecl (..) , DataName (..), dataNameSymbol , DataCtor (..) , DataConP (..) , HasDataDecl (..), hasDecl , DataDeclKind (..) , TyConP (..) -- * Pre-instantiated RType , RRType, RRProp , BRType, BRProp , BSort, BPVar , RTVU, PVU -- * Instantiated RType , BareType, PrType , SpecType, SpecProp, SpecRTVar , SpecRep , LocBareType, LocSpecType , RSort , UsedPVar, RPVar, RReft , REnv , AREnv (..) -- * Constructing & Destructing RTypes , RTypeRep(..), fromRTypeRep, toRTypeRep , mkArrow, bkArrowDeep, bkArrow, safeBkArrow , mkUnivs, bkUniv, bkClass , rImpF, rFun, rCls, rRCls -- * Manipulating `Predicates` , pvars, pappSym, pApp -- * Some tests on RTypes , isBase , isFunTy , isTrivial , hasHole -- * Traversing `RType` , efoldReft, foldReft, foldReft' , emapReft, mapReft, mapReftM, mapPropM , mapExprReft , mapBot, mapBind , foldRType -- * ??? , Oblig(..) , ignoreOblig , addInvCond -- * Inferred Annotations , AnnInfo (..) , Annot (..) -- * Hole Information , HoleInfo(..) -- * Overall Output , Output (..) -- * Refinement Hole , hole, isHole, hasHoleTy -- * Converting To and From Sort , ofRSort, toRSort , rTypeValueVar , rTypeReft , stripRTypeBase , topRTypeBase -- * Class for values that can be pretty printed , F.PPrint (..) , F.pprint , F.showpp -- * Printer Configuration , PPEnv (..) , ppEnv , ppEnvShort -- * Modules and Imports , ModName (..), ModType (..) , isSrcImport, isSpecImport, isTarget , getModName, getModString, qualifyModName -- * Refinement Type Aliases , RTEnv (..), BareRTEnv, SpecRTEnv, BareRTAlias, SpecRTAlias -- , mapRT, mapRE -- * Errors and Error Messages , module Language.Haskell.Liquid.Types.Errors , Error , ErrorResult -- * Source information (associated with constraints) , Cinfo (..) -- * Measures , Measure (..) , UnSortedExprs, UnSortedExpr , MeasureKind (..) , CMeasure (..) , Def (..) , Body (..) , MSpec (..) -- * 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(..), RISig(..), RILaws(..) , MethodType(..), getMethodType -- * Ureftable Instances , UReftable(..) -- * String Literals , liquidBegin, liquidEnd , Axiom(..), HAxiom -- , rtyVarUniqueSymbol, tyVarUniqueSymbol , rtyVarType ) where -- import qualified ConLike as Ghc -- import InstEnv import Class import CoreSyn (CoreExpr) import Data.String import DataCon import GHC (ModuleName, moduleNameString) import GHC.Generics import Module (moduleNameFS) -- import NameSet import PrelInfo (isNumericClass) import Prelude hiding (error) import qualified Prelude import SrcLoc (SrcSpan) import TyCon import Type (getClassPredTys_maybe) import Language.Haskell.Liquid.GHC.TypeRep hiding (maybeParen) import TysPrim (eqReprPrimTyCon, eqPrimTyCon) import TysWiredIn (listTyCon, boolTyCon) import Var import Control.Monad (liftM, liftM2, liftM3, liftM4) import Control.DeepSeq import Data.Bifunctor --import Data.Bifunctor.TH import Data.Typeable (Typeable) import Data.Generics (Data) import qualified Data.Binary as B 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, mapMaybe) import Data.Function (on) import Data.List (foldl', nub) import Data.Text (Text) import Text.PrettyPrint.HughesPJ hiding (first, (<>)) import Text.Printf import Language.Fixpoint.Misc import qualified Language.Fixpoint.Types as F import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.Types.Variance import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.UX.Config import Data.Default ----------------------------------------------------------------------------- -- | Information about Type Constructors ----------------------------------------------------------------------------- data TyConMap = TyConMap { tcmTyRTy :: M.HashMap TyCon RTyCon -- ^ Map from GHC TyCon to RTyCon , tcmFIRTy :: M.HashMap (TyCon, [F.Sort]) RTyCon -- ^ Map from GHC Family-Instances to RTyCon , tcmFtcArity :: M.HashMap TyCon Int -- ^ Arity of each Family-Tycon } ----------------------------------------------------------------------------- -- | Printer ---------------------------------------------------------------- ----------------------------------------------------------------------------- data PPEnv = PP { ppPs :: Bool -- ^ print "foralls" and abstract-predicates , ppTyVar :: Bool -- ^ print the unique suffix for each tyvar , ppSs :: Bool -- ^ print the strata (?) , ppShort :: Bool -- ^ print the tycons without qualification , ppDebug :: Bool -- ^ gross with full info } deriving (Show) ppEnv :: PPEnv ppEnv = ppEnvDef { ppPs = True } { ppDebug = True } -- RJ: needed for resolution, because pp is used for serialization? {- | [NOTE:ppEnv] For some mysterious reason, `ppDebug` must equal `True` or various tests fail e.g. tests/classes/pos/TypeEquality0{0,1}.hs Yikes. Find out why! -} ppEnvDef :: PPEnv ppEnvDef = PP False False False False False ppEnvShort :: PPEnv -> PPEnv ppEnvShort pp = pp { ppShort = True } ------------------------------------------------------------------ -- Huh? ------------------------------------------------------------------ type Expr = F.Expr type Symbol = F.Symbol -- [NOTE:LIFTED-VAR-SYMBOLS]: Following NOTE:REFLECT-IMPORTS, by default -- each (lifted) `Var` is mapped to its `Symbol` via the `Symbolic Var` -- instance. For _generated_ vars, we may want a custom name e.g. see -- tests/pos/NatClass.hs -- and we maintain that map in `lmVarSyms` with the `Just s` case. -- Ideally, this bandaid should be replaced so we don't have these -- hacky corner cases. data LogicMap = LM { lmSymDefs :: M.HashMap Symbol LMap -- ^ Map from symbols to equations they define , lmVarSyms :: M.HashMap Var (Maybe Symbol) -- ^ Map from (lifted) Vars to `Symbol`; see: -- NOTE:LIFTED-VAR-SYMBOLS and NOTE:REFLECT-IMPORTs } deriving (Show) instance Monoid LogicMap where mempty = LM M.empty M.empty mappend = (<>) instance Semigroup LogicMap where LM x1 x2 <> LM y1 y2 = LM (M.union x1 y1) (M.union x2 y2) data LMap = LMap { lmVar :: F.LocSymbol , lmArgs :: [Symbol] , lmExpr :: Expr } instance Show LMap where show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e toLogicMap :: [(F.LocSymbol, [Symbol], Expr)] -> LogicMap toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls} where toLMap (x, ys, e) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e}) eAppWithMap :: LogicMap -> F.Located Symbol -> [Expr] -> Expr -> Expr eAppWithMap lmap f es def | Just (LMap _ xs e) <- M.lookup (F.val f) (lmSymDefs lmap) , length xs == length es = F.subst (F.mkSubst $ zip xs es) e | Just (LMap _ xs e) <- M.lookup (F.val f) (lmSymDefs lmap) , isApp e = F.subst (F.mkSubst $ zip xs es) $ dropApp e (length xs - length es) | otherwise = def dropApp :: Expr -> Int -> Expr dropApp e i | i <= 0 = e dropApp (F.EApp e _) i = dropApp e (i-1) dropApp _ _ = errorstar "impossible" isApp :: Expr -> Bool isApp (F.EApp (F.EVar _) (F.EVar _)) = True isApp (F.EApp e (F.EVar _)) = isApp e isApp _ = False data TyConP = TyConP { tcpLoc :: !F.SourcePos , tcpCon :: !TyCon , tcpFreeTyVarsTy :: ![RTyVar] , tcpFreePredTy :: ![PVar RSort] , tcpFreeLabelTy :: ![Symbol] , tcpVarianceTs :: !VarianceInfo , tcpVariancePs :: !VarianceInfo , tcpSizeFun :: !(Maybe SizeFun) } deriving (Generic, Data, Typeable) instance F.Loc TyConP where srcSpan tc = F.SS (tcpLoc tc) (tcpLoc tc) -- TODO: just use Located instead of dc_loc, dc_locE data DataConP = DataConP { dcpLoc :: !F.SourcePos , dcpCon :: !DataCon -- ^ Corresponding GHC DataCon , dcpFreeTyVars :: ![RTyVar] -- ^ Type parameters , dcpFreePred :: ![PVar RSort] -- ^ Abstract Refinement parameters , dcpFreeLabels :: ![Symbol] -- ^ ? strata stuff , dcpTyConstrs :: ![SpecType] -- ^ ? Class constraints (via `dataConStupidTheta`) , dcpTyArgs :: ![(Symbol, SpecType)] -- ^ Value parameters , dcpTyRes :: !SpecType -- ^ Result type -- , tyData :: !SpecType -- ^ The 'generic' ADT, see [NOTE:DataCon-Data] , dcpIsGadt :: !Bool -- ^ Was this specified in GADT style (if so, DONT use function names as fields) , dcpModule :: !F.Symbol -- ^ Which module was this defined in , dcpLocE :: !F.SourcePos } deriving (Generic, Data, Typeable) -- | [NOTE:DataCon-Data] for each 'DataConP' we also -- store the type of the constructed data. This is -- *the same as* 'tyRes' for *vanilla* ADTs -- (e.g. List, Maybe etc.) but may differ for GADTs. -- For example, -- -- data Thing a where -- X :: Thing Int -- Y :: Thing Bool -- -- Here the 'DataConP' associated with 'X' (resp. 'Y') -- has 'tyRes' corresponding to 'Thing Int' (resp. 'Thing Bool'), -- but in both cases, the 'tyData' should be 'Thing a'. -- instance F.Loc DataConP where srcSpan d = F.SS (dcpLoc d) (dcpLocE d) -- | 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, Functor) 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 B.Binary t => B.Binary (PVar t) instance NFData t => NFData (PVar t) instance Hashable (PVar a) where hashWithSalt i (PV n _ _ _) = hashWithSalt i n pvType :: PVar t -> t pvType p = case ptype p of PVProp t -> t PVHProp -> panic Nothing "pvType on HProp-PVar" data PVKind t = PVProp t | PVHProp deriving (Generic, Data, Typeable, Functor, F.Foldable, Traversable, Show) instance B.Binary a => B.Binary (PVKind a) instance NFData a => NFData (PVKind a) -------------------------------------------------------------------------------- -- | Predicates ---------------------------------------------------------------- -------------------------------------------------------------------------------- type UsedPVar = PVar () newtype Predicate = Pr [UsedPVar] deriving (Generic, Data, Typeable) instance B.Binary Predicate instance NFData Predicate where rnf _ = () instance Monoid Predicate where mempty = pdTrue mappend = (<>) instance Semigroup Predicate where p <> p' = pdAnd [p, p'] instance Semigroup a => Semigroup (UReft a) where MkUReft x y z <> MkUReft x' y' z' = MkUReft (x <> x') (y <> y') (z <> z') instance (Monoid a) => Monoid (UReft a) where mempty = MkUReft mempty mempty mempty mappend = (<>) pdTrue :: Predicate pdTrue = Pr [] pdAnd :: Foldable t => t Predicate -> Predicate pdAnd ps = Pr (nub $ concatMap pvars ps) pvars :: Predicate -> [UsedPVar] pvars (Pr pvs) = pvs instance F.Subable UsedPVar where syms pv = [ y | (_, x, F.EVar y) <- pargs pv, x /= y ] subst s pv = pv { pargs = mapThd3 (F.subst s) <$> pargs pv } substf f pv = pv { pargs = mapThd3 (F.substf f) <$> pargs pv } substa f pv = pv { pargs = mapThd3 (F.substa f) <$> pargs pv } instance F.Subable Predicate where syms (Pr pvs) = concatMap F.syms pvs subst s (Pr pvs) = Pr (F.subst s <$> pvs) substf f (Pr pvs) = Pr (F.substf f <$> pvs) substa f (Pr pvs) = Pr (F.substa f <$> pvs) instance NFData r => NFData (UReft r) newtype BTyVar = BTV Symbol deriving (Show, Generic, Data, Typeable) newtype RTyVar = RTV TyVar deriving (Generic, Data, Typeable) instance Eq BTyVar where (BTV x) == (BTV y) = x == y instance Ord BTyVar where compare (BTV x) (BTV y) = compare x y instance IsString BTyVar where fromString = BTV . fromString instance B.Binary BTyVar instance Hashable BTyVar instance NFData BTyVar instance NFData RTyVar instance F.Symbolic BTyVar where symbol (BTV tv) = tv instance F.Symbolic RTyVar where 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? } deriving (Generic, Data, Typeable) instance B.Binary BTyCon data RTyCon = RTyCon { rtc_tc :: TyCon -- ^ GHC Type Constructor , rtc_pvars :: ![RPVar] -- ^ Predicate Parameters , rtc_info :: !TyConInfo -- ^ TyConInfo } deriving (Generic, Data, Typeable) instance F.Symbolic RTyCon where symbol = F.symbol . rtc_tc instance F.Symbolic BTyCon where symbol = F.val . btc_tc instance NFData BTyCon instance NFData RTyCon rtyVarType :: RTyVar -> Type rtyVarType (RTV v) = TyVarTy v mkBTyCon :: F.LocSymbol -> BTyCon mkBTyCon x = BTyCon x False False -- | Accessors for @RTyCon@ isBool :: RType RTyCon t t1 -> Bool isBool (RApp (RTyCon{rtc_tc = c}) _ _ _) = c == boolTyCon isBool _ = False isRVar :: RType c tv r -> Bool isRVar (RVar _ _) = True isRVar _ = False isClassBTyCon :: BTyCon -> Bool isClassBTyCon = btc_class -- isClassRTyCon :: RTyCon -> Bool -- isClassRTyCon x = (isClassTyCon $ rtc_tc x) || (rtc_tc x == eqPrimTyCon) rTyConPVs :: RTyCon -> [RPVar] rTyConPVs = rtc_pvars rTyConPropVs :: RTyCon -> [PVar RSort] rTyConPropVs = filter isPropPV . rtc_pvars isPropPV :: PVar t -> Bool isPropPV = isProp . ptype isEqType :: TyConable c => RType c t t1 -> Bool isEqType (RApp c _ _ _) = isEqual c isEqType _ = False isClassType :: TyConable c => RType c t t1 -> Bool isClassType (RApp c _ _ _) = isClass c isClassType _ = False -- rTyConPVHPs = filter isHPropPV . rtc_pvars -- isHPropPV = not . isPropPV isProp :: PVKind t -> Bool isProp (PVProp _) = True isProp _ = False defaultTyConInfo :: TyConInfo 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