{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DerivingVia #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -- | 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, isEmbeddedClass -- * 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 , setRtvPol -- * Predicate Variables , PVar (PV, pname, parg, ptype, pargs), isPropPV, pvType , PVKind (..) , Predicate (..) -- * Refinements , UReft(..) -- * Relational predicates , RelExpr (..) -- * 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, bkUnivClass, bkUnivClass' , rImpF, rFun, rFun', rCls, rRCls, rFunDebug -- * 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, mapRFInfo , 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 -- * Diagnostics, Warnings, Errors and Error Messages , module Language.Haskell.Liquid.Types.Errors , Error , ErrorResult , Warning , mkWarning , Diagnostics , mkDiagnostics , emptyDiagnostics , noErrors , allWarnings , allErrors , printWarning -- * Source information (associated with constraints) , Cinfo (..) -- * Measures , Measure (..) , UnSortedExprs, UnSortedExpr , MeasureKind (..) , CMeasure (..) , Def (..) , Body (..) , MSpec (..) -- * Scoping Info , BScope -- * Type Classes , RClass (..) -- * KV Profiling , KVKind (..) -- types of kvars , KVProf -- profile table , emptyKVProf -- empty profile , updKVProf -- extend profile -- * Misc , mapRTAVars , insertsSEnv -- * 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, tyVarVar -- * Refined Function Info , RFInfo(..), defRFInfo, mkRFInfo, classRFInfo, classRFInfoType , ordSrcSpan ) where import Liquid.GHC.API as Ghc hiding ( Expr , Target , isFunTy , LM , ($+$) , nest , text , blankLine , (<+>) , vcat , hsep , comma , colon , parens , empty , char , panic , int , hcat , showPpr , punctuate , mapSndM , ($$) , braces , angleBrackets , brackets ) import Data.String import GHC.Generics import Prelude hiding (error) import qualified Prelude import Control.Monad (liftM2, liftM3, liftM4, void) import Control.DeepSeq import Data.Bifunctor 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 qualified Data.List as L import Data.Maybe (mapMaybe) import Data.Function (on) import Data.List as L (foldl', nub, null) 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.Types.Generics import Liquid.GHC.Misc import Liquid.GHC.Logging as GHC 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 scope Binders Scope in ----------------------------------------------------------------------------- {- In types with base refinement, e.g., {out:T {inner:a | ri} | ro } If BScope = True , then the outer binder out is in scope on ri If BScope = False, then the outer binder out is not in scope on ri -} type BScope = Bool ----------------------------------------------------------------------------- -- | 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 } newtype RFInfo = RFInfo {permitTC :: Maybe Bool } deriving (Generic, Data, Typeable, Show, Eq) defRFInfo :: RFInfo defRFInfo = RFInfo Nothing classRFInfo :: Bool -> RFInfo classRFInfo b = RFInfo (Just b) classRFInfoType :: Bool -> RType c tv r -> RType c tv r classRFInfoType b = fromRTypeRep . (\trep@RTypeRep{..} -> trep{ty_info = map (\i -> i{permitTC = pure b}) ty_info}) . toRTypeRep mkRFInfo :: Config -> RFInfo mkRFInfo cfg = RFInfo $ Just (typeclass cfg) instance Hashable RFInfo instance NFData RFInfo instance B.Binary RFInfo ----------------------------------------------------------------------------- -- | Printer ---------------------------------------------------------------- ----------------------------------------------------------------------------- data PPEnv = PP { ppPs :: Bool -- ^ print abstract-predicates , ppTyVar :: Bool -- ^ print the unique suffix for each tyvar , 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 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] , 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 , dcpTyConstrs :: ![SpecType] -- ^ ? Class constraints (via `dataConStupidTheta`) , dcpTyArgs :: ![(Symbol, SpecType)] -- ^ Value parameters , dcpTyRes :: !SpecType -- ^ Result type , 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) deriving Hashable via Generically Predicate instance Eq Predicate where (Pr vs) == (Pr ws) = and $ (length vs' == length ws') : [v == w | (v, w) <- zip vs' ws'] where vs' = L.sort vs ws' = L.sort ws 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 <> MkUReft x' y' = MkUReft (x <> x') (y <> y') instance (Monoid a) => Monoid (UReft a) where mempty = MkUReft 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) data RelExpr = ERBasic F.Expr | ERChecked Expr RelExpr | ERUnChecked Expr RelExpr deriving (Eq, Show, Data, Generic) instance B.Binary RelExpr instance F.PPrint RelExpr where pprintTidy k (ERBasic e) = F.pprintTidy k e pprintTidy k (ERChecked e r) = F.pprintTidy k e <+> "!=>" <+> F.pprintTidy k r pprintTidy k (ERUnChecked e r) = F.pprintTidy k e <+> ":=>" <+> F.pprintTidy k 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) deriving Hashable via Generically BTyCon 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 tyVarVar :: RTVar RTyVar c -> Var tyVarVar (RTVar (RTV v) _) = 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 isEmbeddedClass :: TyConable c => RType c t t1 -> Bool isEmbeddedClass (RApp c _ _ _) = isEmbeddedDict c isEmbeddedClass _ = 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