{-# 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 #-} -- | This module should contain all the global type definitions and basic instances. module Language.Haskell.Liquid.Types ( -- * Options Config (..) , HasConfig (..) , hasOpt -- * Ghc Information , GhcInfo (..) , GhcSpec (..) , TargetVars (..) -- * Located Things , Located (..) , dummyLoc -- * Symbols , LocSymbol , LocText -- * Default unknown name , dummyName, 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 (..) , DataConP (..) , 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 -- * ??? , 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 , PPrint (..), pprint , 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 TypeRep hiding (maybeParen, pprArrowChain) import TysPrim (eqPrimTyCon) import TysWiredIn (listTyCon, boolTyCon, eqTyCon) 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 (nub) import Data.Text (Text) import Text.PrettyPrint.HughesPJ hiding (first) import Text.Printf import Language.Fixpoint.Misc import Language.Fixpoint.Types hiding (Error, SrcSpan, Result, Predicate, R) 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 False False False False ppEnvShort :: PPEnv -> PPEnv ppEnvShort pp = pp { ppShort = True } ------------------------------------------------------------------ -- | GHC Information : Code & Spec ------------------------------ ------------------------------------------------------------------ data GhcInfo = GI { target :: !FilePath , targetMod:: !ModuleName , env :: !HscEnv , cbs :: ![CoreBind] , derVars :: ![Var] -- ^ ? , impVars :: ![Var] , defVars :: ![Var] , useVars :: ![Var] , hqFiles :: ![FilePath] , imports :: ![String] , includes :: ![FilePath] , spec :: !GhcSpec } instance HasConfig GhcInfo where getConfig = getConfig . spec -- | 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 :: ![(DataCon, DataConP)] -- ^ 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 :: 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 , gsTgtVars :: ![Var] -- ^ Top-level Binders To Verify (empty means ALL binders) , gsDecr :: ![(Var, [Int])] -- ^ Lexicographically ordered size witnesses for termination , gsTexprs :: ![(Var, [Located Expr])] -- ^ Lexicographically ordered expressions for termination , gsNewTypes :: ![(TyCon, LocSpecType)] -- ^ Mapping of new type 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 axiomatized functions , gsReflects :: [Var] -- [HAxiom] -- ^ Binders for reflected functions , gsLogicMap :: LogicMap , gsProofType :: Maybe Type , gsRTAliases :: !RTEnv -- ^ Refinement type aliases } instance HasConfig GhcSpec where getConfig = gsConfig data LogicMap = LM { logic_map :: M.HashMap Symbol LMap , axiom_map :: M.HashMap Var Symbol } 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 :: LocSymbol , lmArgs :: [Symbol] , lmExpr :: Expr } instance Show LMap where show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap toLogicMap ls = mempty {logic_map = M.fromList $ map toLMap ls} where toLMap (x, ys, e) = (val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e}) eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr eAppWithMap lmap f es def | Just (LMap _ xs e) <- M.lookup (val f) (logic_map lmap) , length xs == length es -- NOPROP , length xs <= length es = subst (mkSubst $ zip xs es) e | Just (LMap _ xs e) <- M.lookup (val f) (logic_map lmap) , isApp e = subst (mkSubst $ zip xs es) $ dropApp e (length xs - length es) | otherwise = def dropApp :: Expr -> Int -> Expr dropApp e i | i <= 0 = e dropApp (EApp e _) i = dropApp e (i-1) dropApp _ _ = errorstar "impossible" isApp :: Expr -> Bool isApp (EApp (EVar _) (EVar _)) = True isApp (EApp e (EVar _)) = isApp e isApp _ = False data TyConP = TyConP { ty_loc :: !SourcePos , freeTyVarsTy :: ![RTyVar] , freePredTy :: ![PVar RSort] , freeLabelTy :: ![Symbol] , varianceTs :: !VarianceInfo , variancePs :: !VarianceInfo , sizeFun :: !(Maybe SizeFun) } deriving (Generic, Data, Typeable) data DataConP = DataConP { dc_loc :: !SourcePos , freeTyVars :: ![RTyVar] , freePred :: ![PVar RSort] , freeLabels :: ![Symbol] , tyConsts :: ![SpecType] -- FIXME: WHAT IS THIS?? , tyArgs :: ![(Symbol, SpecType)] -- FIXME: These are backwards, why?? , tyRes :: !SpecType , dc_locE :: !SourcePos } deriving (Generic, 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, 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 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 . qBody subst = mapQualBody . subst substf = mapQualBody . substf substa = mapQualBody . substa mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier mapQualBody f q = q { qBody = 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 Symbolic BTyVar where symbol (BTV tv) = tv instance Symbolic RTyVar where symbol (RTV tv) = symbol . getName $ tv data BTyCon = BTyCon { btc_tc :: !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 Symbolic BTyCon where symbol = val . btc_tc instance NFData BTyCon instance NFData RTyCon rtyVarUniqueSymbol :: RTyVar -> Symbol rtyVarUniqueSymbol (RTV tv) = tyVarUniqueSymbol tv tyVarUniqueSymbol :: TyVar -> Symbol tyVarUniqueSymbol tv = symbol $ show (getName tv) ++ "_" ++ show (varUnique tv) rtyVarType :: RTyVar -> Type rtyVarType (RTV v) = TyVarTy v mkBTyCon :: LocSymbol -> BTyCon mkBTyCon x = BTyCon x False False mkClassBTyCon :: LocSymbol -> BTyCon mkClassBTyCon x = BTyCon x True False mkPromotedBTyCon :: 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 == eqTyCon) 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