{-# 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 ( -- * Options Config (..) , HasConfig (..) -- * Ghc Information , GhcInfo (..) , GhcSpec (..) , TargetVars (..) -- * 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 -- * 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 (..) , DataCtor (..) , DataConP (..) , HasDataDecl (..), hasDecl , DataDeclKind (..) , TyConP (..) -- * Pre-instantiated RType , RRType, RRProp , BRType, BRProp , BSort, BPVar , RTVU, PVU -- * Instantiated RType , BareType, PrType , SpecType, SpecProp , LocBareType, LocSpecType , 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, foldReft' , mapReft, mapReftM, mapPropM , mapBot, mapBind , foldRType -- * ??? , Oblig(..) , ignoreOblig , addInvCond -- * Inferred Annotations , AnnInfo (..) , Annot (..) -- * Overall Output , Output (..) -- * Refinement Hole , hole, isHole, hasHole -- * 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 , getModName, getModString -- * Refinement Type Aliases , RTEnv (..) , mapRT, mapRE -- * Errors and Error Messages , module Language.Haskell.Liquid.Types.Errors , Error , ErrorResult -- * Source information (associated with constraints) , Cinfo (..) -- * Measures , Measure (..) , 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(..) -- * Ureftable Instances , UReftable(..) -- * String Literals , liquidBegin, liquidEnd , Axiom(..), HAxiom, AxiomEq(..) , rtyVarUniqueSymbol, tyVarUniqueSymbol, rtyVarType ) where import Class import CoreSyn (CoreBind, CoreExpr) import Data.String import DataCon import GHC (HscEnv, ModuleName, moduleNameString, getName) import GHC.Generics import Module (moduleNameFS) import NameSet import PrelInfo (isNumericClass) import Prelude hiding (error) import SrcLoc (SrcSpan) import TyCon import Type (getClassPredTys_maybe) import Language.Haskell.Liquid.GHC.TypeRep hiding (maybeParen, pprArrowChain) import TysPrim (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.List (foldl', nub) import Data.Text (Text) import Text.PrettyPrint.HughesPJ hiding (first) import Text.Printf import Language.Fixpoint.Misc -- import Language.Fixpoint.Types hiding (SmtSort (..), DataDecl, Error, SrcSpan, Result, Predicate, R) 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 ----------------------------------------------------------------------------- -- | Printer ---------------------------------------------------------------- ----------------------------------------------------------------------------- data PPEnv = PP { ppPs :: Bool , ppTyVar :: Bool -- TODO if set to True all Bare fails , ppSs :: Bool , ppShort :: Bool } deriving (Show) ppEnv :: PPEnv ppEnv = ppEnvCurrent ppEnvCurrent :: PPEnv ppEnvCurrent = PP False False False False _ppEnvPrintPreds :: PPEnv _ppEnvPrintPreds = PP True False False False ppEnvShort :: PPEnv -> PPEnv ppEnvShort pp = pp { ppShort = True } ------------------------------------------------------------------ -- | GHC Information : Code & Spec ------------------------------ ------------------------------------------------------------------ data GhcInfo = GI { target :: !FilePath -- ^ Source file for module , targetMod:: !ModuleName -- ^ Name for module , env :: !HscEnv -- ^ GHC Env used to resolve names for module , cbs :: ![CoreBind] -- ^ Source Code , derVars :: ![Var] -- ^ ? , impVars :: ![Var] -- ^ Binders that are _read_ in module (but not defined?) , defVars :: ![Var] -- ^ (Top-level) binders that are _defined_ in module , useVars :: ![Var] -- ^ Binders that are _read_ in module -- , tyCons :: ![TyCon] -- ^ Types that are defined inside module , hqFiles :: ![FilePath] -- ^ Imported .hqual files , imports :: ![String] -- ^ ??? dead? , includes :: ![FilePath] -- ^ ??? dead? , spec :: !GhcSpec -- ^ All specification information for module } instance HasConfig GhcInfo where getConfig = getConfig . spec type Expr = F.Expr type Symbol = F.Symbol type Qualifier = F.Qualifier -- | The following is the overall type for /specifications/ obtained from -- parsing the target source and dependent libraries data GhcSpec = SP { gsTySigs :: ![(Var, LocSpecType)] -- ^ Asserted Reftypes , gsAsmSigs :: ![(Var, LocSpecType)] -- ^ Assumed Reftypes , gsInSigs :: ![(Var, LocSpecType)] -- ^ Auto generated Signatures , gsCtors :: ![(Var, LocSpecType)] -- ^ Data Constructor Measure Sigs , gsLits :: ![(Symbol, LocSpecType)] -- ^ Literals/Constants -- e.g. datacons: EQ, GT, string lits: "zombie",... , gsMeas :: ![(Symbol, LocSpecType)] -- ^ Measure Types -- eg. len :: [a] -> Int , gsInvariants :: ![(Maybe Var, LocSpecType)] -- ^ Data Type Invariants that came from the definition of var measure -- eg. forall a. {v: [a] | len(v) >= 0} , gsIaliases :: ![(LocSpecType, LocSpecType)]-- ^ Data Type Invariant Aliases , gsDconsP :: ![F.Located DataCon] -- ^ Predicated Data-Constructors -- e.g. see tests/pos/Map.hs , gsTconsP :: ![(TyCon, TyConP)] -- ^ Predicated Type-Constructors -- eg. see tests/pos/Map.hs , gsFreeSyms :: ![(Symbol, Var)] -- ^ List of `Symbol` free in spec and corresponding GHC var -- eg. (Cons, Cons#7uz) from tests/pos/ex1.hs , gsTcEmbeds :: F.TCEmb TyCon -- ^ How to embed GHC Tycons into fixpoint sorts -- e.g. "embed Set as Set_set" from include/Data/Set.spec , gsQualifiers :: ![Qualifier] -- ^ Qualifiers in Source/Spec files -- e.g tests/pos/qualTest.hs , gsADTs :: ![F.DataDecl] -- ^ ADTs extracted from Haskell 'data' definitions , gsTgtVars :: ![Var] -- ^ Top-level Binders To Verify (empty means ALL binders) , gsDecr :: ![(Var, [Int])] -- ^ Lexicographically ordered size witnesses for termination , gsTexprs :: ![(Var, [F.Located Expr])] -- ^ Lexicographically ordered expressions for termination , gsNewTypes :: ![(TyCon, LocSpecType)] -- ^ Mapping of 'newtype' type constructors with their refined types. , gsLvars :: !(S.HashSet Var) -- ^ Variables that should be checked in the environment they are used , gsLazy :: !(S.HashSet Var) -- ^ Binders to IGNORE during termination checking , gsAutosize :: !(S.HashSet TyCon) -- ^ Binders to IGNORE during termination checking , gsAutoInst :: !(M.HashMap Var (Maybe Int)) -- ^ Binders to expand with automatic axiom instances maybe with specified fuel , gsConfig :: !Config -- ^ Configuration Options , gsExports :: !NameSet -- ^ `Name`s exported by the module being verified , gsMeasures :: [Measure SpecType DataCon] , gsTyconEnv :: M.HashMap TyCon RTyCon , gsDicts :: DEnv Var SpecType -- ^ Dictionary Environment , gsAxioms :: [AxiomEq] -- ^ Axioms from reflected functions , gsReflects :: [Var] -- ^ Binders for reflected functions , gsLogicMap :: LogicMap , gsProofType :: Maybe Type , gsRTAliases :: !RTEnv -- ^ Refinement type aliases } instance HasConfig GhcSpec where getConfig = gsConfig -- axiom_map ===> lmVarSyms -- [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 (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 { ty_loc :: !F.SourcePos , freeTyVarsTy :: ![RTyVar] , freePredTy :: ![PVar RSort] , freeLabelTy :: ![Symbol] , varianceTs :: !VarianceInfo , variancePs :: !VarianceInfo , sizeFun :: !(Maybe SizeFun) } deriving (Generic, Data, Typeable) -- TODO: just use Located instead of dc_loc, dc_locE data DataConP = DataConP { dc_loc :: !F.SourcePos , freeTyVars :: ![RTyVar] -- ^ Type parameters , freePred :: ![PVar RSort] -- ^ Abstract Refinement parameters , freeLabels :: ![Symbol] -- ^ ? strata stuff , tyConsts :: ![SpecType] -- ^ ? Class constraints , tyArgs :: ![(Symbol, SpecType)] -- ^ Value parameters , tyRes :: !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 , dc_locE :: !F.SourcePos } deriving (Generic, Data, Typeable) instance F.Loc DataConP where srcSpan d = F.SS (dc_loc d) (dc_locE 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 p p' = pdAnd [p, p'] instance (Monoid a) => Monoid (UReft a) where mempty = MkUReft mempty mempty mempty mappend (MkUReft x y z) (MkUReft x' y' z') = MkUReft (mappend x x') (mappend y y') (mappend z z') 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 F.Subable Qualifier where syms = F.syms . F.qBody subst = mapQualBody . F.subst substf = mapQualBody . F.substf substa = mapQualBody . F.substa mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier mapQualBody f q = q { F.qBody = f (F.qBody q) } 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 . getName $ 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 BTyCon where symbol = F.val . btc_tc instance NFData BTyCon 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 mkBTyCon :: F.LocSymbol -> BTyCon mkBTyCon x = BTyCon x False False mkClassBTyCon :: F.LocSymbol -> BTyCon mkClassBTyCon x = BTyCon x True False mkPromotedBTyCon :: F.LocSymbol -> BTyCon mkPromotedBTyCon x = BTyCon x False True -- | 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