-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Liquid Types for Haskell -- @package liquidhaskell @version 0.2.1.0 module Language.Haskell.Liquid.Desugar.Coverage addTicksToBinds :: DynFlags -> Module -> ModLocation -> NameSet -> [TyCon] -> LHsBinds Id -> IO (LHsBinds Id, HpcInfo, ModBreaks) hpcInitCode :: Module -> HpcInfo -> SDoc instance Eq TickDensity instance Monad TM instance Applicative TM instance Functor TM module Language.Haskell.Liquid.Desugar.DsForeign dsForeigns :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding) dsForeigns' :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding) dsFImport :: Id -> Coercion -> ForeignImport -> DsM ([Binding], SDoc, SDoc) dsCImport :: Id -> Coercion -> CImportSpec -> CCallConv -> Safety -> Maybe Header -> DsM ([Binding], SDoc, SDoc) dsFCall :: Id -> Coercion -> ForeignCall -> Maybe Header -> DsM ([(Id, Expr TyVar)], SDoc, SDoc) dsPrimCall :: Id -> Coercion -> ForeignCall -> DsM ([(Id, Expr TyVar)], SDoc, SDoc) dsFExport :: Id -> Coercion -> CLabelString -> CCallConv -> Bool -> DsM (SDoc, SDoc, String, Int) dsFExportDynamic :: Id -> Coercion -> CCallConv -> DsM ([Binding], SDoc, SDoc) mkFExportCBits :: DynFlags -> FastString -> Maybe Id -> [Type] -> Type -> Bool -> CCallConv -> (SDoc, SDoc, String, Int) toCType :: Type -> (Maybe Header, SDoc) foreignExportInitialiser :: Id -> SDoc -- | Utility functions for constructing Core syntax, principally for -- desugaring module Language.Haskell.Liquid.Desugar.DsUtils data EquationInfo :: * EqnInfo :: [Pat Id] -> MatchResult -> EquationInfo eqn_pats :: EquationInfo -> [Pat Id] eqn_rhs :: EquationInfo -> MatchResult firstPat :: EquationInfo -> Pat Id shiftEqns :: [EquationInfo] -> [EquationInfo] data MatchResult :: * MatchResult :: CanItFail -> (CoreExpr -> DsM CoreExpr) -> MatchResult data CanItFail :: * CanFail :: CanItFail CantFail :: CanItFail data CaseAlt a MkCaseAlt :: a -> [CoreBndr] -> HsWrapper -> MatchResult -> CaseAlt a alt_pat :: CaseAlt a -> a alt_bndrs :: CaseAlt a -> [CoreBndr] alt_wrapper :: CaseAlt a -> HsWrapper alt_result :: CaseAlt a -> MatchResult cantFailMatchResult :: CoreExpr -> MatchResult alwaysFailMatchResult :: MatchResult extractMatchResult :: MatchResult -> CoreExpr -> DsM CoreExpr combineMatchResults :: MatchResult -> MatchResult -> MatchResult adjustMatchResult :: DsWrapper -> MatchResult -> MatchResult adjustMatchResultDs :: (CoreExpr -> DsM CoreExpr) -> MatchResult -> MatchResult mkCoLetMatchResult :: CoreBind -> MatchResult -> MatchResult mkViewMatchResult :: Id -> CoreExpr -> Id -> MatchResult -> MatchResult mkGuardedMatchResult :: CoreExpr -> MatchResult -> MatchResult matchCanFail :: MatchResult -> Bool mkEvalMatchResult :: Id -> Type -> MatchResult -> MatchResult mkCoPrimCaseMatchResult :: Id -> Type -> [(Literal, MatchResult)] -> MatchResult mkCoAlgCaseMatchResult :: DynFlags -> Id -> Type -> [CaseAlt DataCon] -> MatchResult mkCoSynCaseMatchResult :: Id -> Type -> CaseAlt PatSyn -> MatchResult wrapBind :: Var -> Var -> CoreExpr -> CoreExpr wrapBinds :: [(Var, Var)] -> CoreExpr -> CoreExpr mkErrorAppDs :: Id -> Type -> SDoc -> DsM CoreExpr mkCoreAppDs :: CoreExpr -> CoreExpr -> CoreExpr mkCoreAppsDs :: CoreExpr -> [CoreExpr] -> CoreExpr seqVar :: Var -> CoreExpr -> CoreExpr mkLHsVarPatTup :: [Id] -> LPat Id mkLHsPatTup :: [LPat Id] -> LPat Id mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id mkBigLHsVarTup :: [Id] -> LHsExpr Id mkBigLHsTup :: [LHsExpr Id] -> LHsExpr Id mkBigLHsVarPatTup :: [Id] -> LPat Id mkBigLHsPatTup :: [LPat Id] -> LPat Id mkSelectorBinds :: [Maybe (Tickish Id)] -> LPat Id -> CoreExpr -> DsM [(Id, CoreExpr)] selectSimpleMatchVarL :: LPat Id -> DsM Id selectMatchVars :: [Pat Id] -> DsM [Id] selectMatchVar :: Pat Id -> DsM Id mkOptTickBox :: Maybe (Tickish Id) -> CoreExpr -> CoreExpr mkBinaryTickBox :: Int -> Int -> CoreExpr -> DsM CoreExpr module Language.Haskell.Liquid.Desugar.MatchLit dsLit :: HsLit -> DsM CoreExpr dsOverLit :: HsOverLit Id -> DsM CoreExpr hsLitKey :: DynFlags -> HsLit -> Literal hsOverLitKey :: OutputableBndr a => HsOverLit a -> Bool -> Literal tidyLitPat :: HsLit -> Pat Id tidyNPat :: (HsLit -> Pat Id) -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> SyntaxExpr Id -> Pat Id matchLiterals :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult matchNPlusKPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult matchNPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult warnAboutIdentities :: DynFlags -> CoreExpr -> Type -> DsM () warnAboutEmptyEnumerations :: DynFlags -> LHsExpr Id -> Maybe (LHsExpr Id) -> LHsExpr Id -> DsM () module Language.Haskell.Liquid.Desugar.DsGRHSs dsGuarded :: GRHSs Id (LHsExpr Id) -> Type -> DsM CoreExpr dsGRHSs :: HsMatchContext Name -> [Pat Id] -> GRHSs Id (LHsExpr Id) -> Type -> DsM MatchResult dsGRHS :: HsMatchContext Name -> Type -> LGRHS Id (LHsExpr Id) -> DsM MatchResult module Language.Haskell.Liquid.Desugar.DsBinds dsTopLHsBinds :: LHsBinds Id -> DsM (OrdList (Id, CoreExpr)) dsLHsBinds :: LHsBinds Id -> DsM [(Id, CoreExpr)] decomposeRuleLhs :: [Var] -> CoreExpr -> Either SDoc ([Var], Id, [CoreExpr]) dsSpec :: Maybe CoreExpr -> Located TcSpecPrag -> DsM (Maybe (OrdList (Id, CoreExpr), CoreRule)) dsHsWrapper :: HsWrapper -> CoreExpr -> DsM CoreExpr dsTcEvBinds :: TcEvBinds -> DsM [CoreBind] dsEvBinds :: Bag EvBind -> DsM [CoreBind] module Language.Haskell.Liquid.Desugar.Check check :: [EquationInfo] -> ([ExhaustivePat], [EquationInfo]) type ExhaustivePat = ([WarningPat], [(Name, [HsLit])]) module Language.Haskell.Liquid.Desugar.MatchCon matchConFamily :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult matchPatSyn :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult module Language.Haskell.Liquid.Desugar.Match match :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult matchEquations :: HsMatchContext Name -> [Id] -> [EquationInfo] -> Type -> DsM CoreExpr matchWrapper :: HsMatchContext Name -> MatchGroup Id (LHsExpr Id) -> DsM ([Id], CoreExpr) matchSimply :: CoreExpr -> HsMatchContext Name -> LPat Id -> CoreExpr -> CoreExpr -> DsM CoreExpr matchSinglePat :: CoreExpr -> HsMatchContext Name -> LPat Id -> Type -> MatchResult -> DsM MatchResult module Language.Haskell.Liquid.Desugar.DsListComp dsListComp :: [ExprLStmt Id] -> Type -> DsM CoreExpr dsPArrComp :: [ExprStmt Id] -> DsM CoreExpr dsMonadComp :: [ExprLStmt Id] -> DsM CoreExpr module Language.Haskell.Liquid.Desugar.DsArrows dsProcExpr :: LPat Id -> LHsCmdTop Id -> DsM CoreExpr module Paths_liquidhaskell version :: Version getBinDir :: IO FilePath getLibDir :: IO FilePath getDataDir :: IO FilePath getLibexecDir :: IO FilePath getDataFileName :: FilePath -> IO FilePath getSysconfDir :: IO FilePath -- | This module contains a wrappers and utility functions for accessing -- GHC module information. It should NEVER depend on ANY module inside -- the Language.Haskell.Liquid.* tree. module Language.Haskell.Liquid.GhcMisc data MGIModGuts MI :: !CoreProgram -> !Module -> !Dependencies -> !ImportedMods -> !GlobalRdrEnv -> ![TyCon] -> ![FamInst] -> !NameSet -> !(Maybe [DFunId]) -> MGIModGuts mgi_binds :: MGIModGuts -> !CoreProgram mgi_module :: MGIModGuts -> !Module mgi_deps :: MGIModGuts -> !Dependencies mgi_dir_imps :: MGIModGuts -> !ImportedMods mgi_rdr_env :: MGIModGuts -> !GlobalRdrEnv mgi_tcs :: MGIModGuts -> ![TyCon] mgi_fam_insts :: MGIModGuts -> ![FamInst] mgi_exports :: MGIModGuts -> !NameSet mgi_is_dfun :: MGIModGuts -> !(Maybe [DFunId]) miModGuts :: Maybe [DFunId] -> ModGuts -> MGIModGuts srcSpanTick :: Module -> SrcSpan -> Tickish a tickSrcSpan :: Outputable a => Tickish a -> SrcSpan stringTyVar :: String -> TyVar stringTyCon :: Char -> Int -> String -> TyCon hasBaseTypeVar :: Var -> Bool isBaseType :: Type -> Bool validTyVar :: String -> Bool tvId :: Var -> [Char] tracePpr :: Outputable a => [Char] -> a -> a pprShow :: Show a => a -> SDoc tidyCBs :: [Bind b] -> [Bind b] unTick :: Bind b -> Bind b unTickExpr :: Expr b -> Expr b isFractionalClass :: Class -> Bool getDataConVarUnique :: Var -> Unique newtype Loc L :: (Int, Int) -> Loc unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) realSrcSpan :: String -> Int -> Int -> Int -> Int -> RealSrcSpan toFixSDoc :: Fixpoint a => a -> Doc sDocDoc :: SDoc -> Doc pprDoc :: Outputable a => a -> Doc showPpr :: Outputable a => a -> String showSDoc :: SDoc -> String showSDocDump :: SDoc -> String typeUniqueString :: Outputable a => a -> String sourcePosSrcSpan :: SourcePos -> SrcSpan sourcePosSrcLoc :: SourcePos -> SrcLoc srcSpanSourcePos :: SrcSpan -> SourcePos srcSpanFilename :: SrcSpan -> String srcSpanStartLoc :: RealSrcSpan -> Loc srcSpanEndLoc :: RealSrcSpan -> Loc oneLine :: RealSrcSpan -> Bool lineCol :: RealSrcSpan -> (Int, Int) realSrcSpanSourcePos :: RealSrcSpan -> SourcePos getSourcePos :: NamedThing a => a -> SourcePos collectArguments :: Int -> CoreExpr -> [Var] collectValBinders' :: Expr Var -> ([Var], Expr Var) ignoreLetBinds :: Expr t -> Expr t isDictionary :: Symbolic a => a -> Bool isInternal :: Symbolic a => a -> Bool uniqueHash :: Uniquable a => Int -> a -> Int lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name) addContext :: GhcMonad m => InteractiveImport -> m () qualImportDecl :: ModuleName -> ImportDecl name ignoreInline :: ParsedModule -> ParsedModule symbolTyCon :: Char -> Int -> Symbol -> TyCon symbolTyVar :: Symbol -> TyVar qualifiedNameSymbol :: Name -> Symbol fastStringText :: FastString -> Text symbolFastString :: Symbol -> FastString instance Eq Loc instance Ord Loc instance Show Loc instance Symbolic FastString instance Symbolic Name instance Symbolic TyCon instance Hashable TyCon instance Hashable Var instance Show TyCon instance Show Class instance Show Var instance Show Name instance Fixpoint Type instance Fixpoint Name instance Fixpoint Var instance FromJSON SrcSpan instance ToJSON SrcSpan instance FromJSON RealSrcSpan instance ToJSON RealSrcSpan instance Outputable a => Outputable (HashSet a) instance Hashable SrcSpan instance Hashable Loc -- | This module should contain all the global type definitions and basic -- instances. module Language.Haskell.Liquid.Types -- | Command Line Config Options -- -------------------------------------------- data Config Config :: [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> SMTSolver -> Bool -> Bool -> [String] -> [String] -> Config -- | source files to check files :: Config -> [FilePath] -- | path to directory for including specs idirs :: Config -> [FilePath] -- | check subset of binders modified (+ dependencies) since last check diffcheck :: Config -> Bool -- | supports real number arithmetic real :: Config -> Bool -- | check all binders (overrides diffcheck) fullcheck :: Config -> Bool -- | set of binders to check binders :: Config -> [String] -- | whether to complain about specifications for unexported and unused -- values noCheckUnknown :: Config -> Bool -- | disable termination check notermination :: Config -> Bool -- | disable warnings output (only show errors) nowarnings :: Config -> Bool -- | type all internal variables with true trustinternals :: Config -> Bool -- | disable case expand nocaseexpand :: Config -> Bool -- | enable strata analysis strata :: Config -> Bool -- | disable truing top level types notruetypes :: Config -> Bool -- | check totality in definitions totality :: Config -> Bool -- | disable prunning unsorted Refinements noPrune :: Config -> Bool -- | the maximum number of parameters to accept when mining qualifiers maxParams :: Config -> Int -- | name of smtsolver to use [default: z3-API] smtsolver :: Config -> SMTSolver -- | drop module qualifers from pretty-printed names. shortNames :: Config -> Bool -- | don't show subtyping errors and contexts. shortErrors :: Config -> Bool -- | command-line options to pass to GHC ghcOptions :: Config -> [String] -- | .c files to compile and link against (for GHC) cFiles :: Config -> [String] -- | GHC Information : Code & Spec ------------------------------ data GhcInfo GI :: !HscEnv -> ![CoreBind] -> ![Var] -> ![Var] -> ![Var] -> ![Var] -> ![FilePath] -> ![String] -> ![FilePath] -> !GhcSpec -> GhcInfo env :: GhcInfo -> !HscEnv cbs :: GhcInfo -> ![CoreBind] derVars :: GhcInfo -> ![Var] impVars :: GhcInfo -> ![Var] defVars :: GhcInfo -> ![Var] useVars :: GhcInfo -> ![Var] hqFiles :: GhcInfo -> ![FilePath] imports :: GhcInfo -> ![String] includes :: GhcInfo -> ![FilePath] spec :: GhcInfo -> !GhcSpec -- | The following is the overall type for specifications obtained -- from parsing the target source and dependent libraries data GhcSpec SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> GhcSpec -- | Asserted Reftypes eg. see include/Prelude.spec tySigs :: GhcSpec -> ![(Var, Located SpecType)] -- | Assumed Reftypes asmSigs :: GhcSpec -> ![(Var, Located SpecType)] -- | Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int -- | v = 1 + len(xs) } ctors :: GhcSpec -> ![(Var, Located SpecType)] -- | Measure Types eg. len :: [a] -> Int meas :: GhcSpec -> ![(Symbol, Located SpecType)] -- | Data Type Invariants invariants :: GhcSpec -> ![Located SpecType] -- | Data Type Invariant Aliases eg. forall a. {v: [a] | len(v) >= 0} ialiases :: GhcSpec -> ![(Located SpecType, Located SpecType)] -- | Predicated Data-Constructors e.g. see testsposMap.hs dconsP :: GhcSpec -> ![(DataCon, DataConP)] -- | Predicated Type-Constructors eg. see testsposMap.hs tconsP :: GhcSpec -> ![(TyCon, TyConP)] -- | List of Symbol free in spec and corresponding GHC var eg. -- (Cons, Cons#7uz) from testsposex1.hs freeSyms :: GhcSpec -> ![(Symbol, Var)] -- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as -- Set_set" from includeDataSet.spec tcEmbeds :: GhcSpec -> TCEmb TyCon -- | Qualifiers in Source/Spec files e.g testsposqualTest.hs qualifiers :: GhcSpec -> ![Qualifier] -- | Top-level Binders To Verify (empty means ALL binders) tgtVars :: GhcSpec -> ![Var] -- | Lexicographically ordered size witnesses for termination decr :: GhcSpec -> ![(Var, [Int])] -- | Lexicographically ordered expressions for termination texprs :: GhcSpec -> ![(Var, [Expr])] -- | Variables that should be checked in the environment they are used lvars :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking lazy :: GhcSpec -> !(HashSet Var) -- | Configuration Options config :: GhcSpec -> !Config -- | Names exported by the module being verified exports :: GhcSpec -> !NameSet measures :: GhcSpec -> [Measure SpecType DataCon] tyconEnv :: GhcSpec -> HashMap TyCon RTyCon -- | Which Top-Level Binders Should be Verified data TargetVars AllVars :: TargetVars Only :: ![Var] -> TargetVars -- | Located Values -- --------------------------------------------------------- data Located a :: * -> * Loc :: SrictNotUnpackedSourcePos -> a -> Located a loc :: Located a -> SrictNotUnpackedSourcePos val :: Located a -> a dummyLoc :: a -> Located a type LocSymbol = Located Symbol type LocText = Located Text dummyName :: Symbol isDummy :: Symbolic a => a -> Bool data RTyCon RTyCon :: !TyCon -> ![RPVar] -> !TyConInfo -> RTyCon -- | 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 :: b - Prop, q :: Int -> Prop, r :: a -> -- Prop> = F (ar -> bp) | Q (c -> a) | G -- (Intq -> ar) -- -- there will be: -- -- covariantTyArgs = [0, 1, 3], for type arguments a, b and d -- contravariantTyArgs = [0, 2, 3], for type arguments a, c and d -- covariantPsArgs = [0, 2], for predicate arguments p and r -- contravariantPsArgs = [1, 2], for predicate arguments q and r -- -- does not appear in the data definition, we enforce BOTH con - contra -- variance data TyConInfo TyConInfo :: ![Int] -> ![Int] -> ![Int] -> ![Int] -> !(Maybe (Symbol -> Expr)) -> TyConInfo -- | indexes of covariant type arguments covariantTyArgs :: TyConInfo -> ![Int] -- | indexes of contravariant type arguments contravariantTyArgs :: TyConInfo -> ![Int] -- | indexes of covariant predicate arguments covariantPsArgs :: TyConInfo -> ![Int] -- | indexes of contravariant predicate arguments contravariantPsArgs :: TyConInfo -> ![Int] sizeFunction :: TyConInfo -> !(Maybe (Symbol -> Expr)) rTyConPVs :: RTyCon -> [RPVar] rTyConPropVs :: RTyCon -> [PVar RSort] -- | Accessors for RTyCon isClassRTyCon :: RTyCon -> Bool data RType p c tv r RVar :: !tv -> !r -> RType p c tv r rt_var :: RType p c tv r -> !tv rt_reft :: RType p c tv r -> !r RFun :: !Symbol -> !(RType p c tv r) -> !(RType p c tv r) -> !r -> RType p c tv r rt_bind :: RType p c tv r -> !Symbol rt_in :: RType p c tv r -> !(RType p c tv r) rt_out :: RType p c tv r -> !(RType p c tv r) rt_reft :: RType p c tv r -> !r RAllT :: !tv -> !(RType p c tv r) -> RType p c tv r rt_tvbind :: RType p c tv r -> !tv rt_ty :: RType p c tv r -> !(RType p c tv r) RAllP :: !(PVar (RType p c tv ())) -> !(RType p c tv r) -> RType p c tv r rt_pvbind :: RType p c tv r -> !(PVar (RType p c tv ())) rt_ty :: RType p c tv r -> !(RType p c tv r) RAllS :: !(Symbol) -> !(RType p c tv r) -> RType p c tv r rt_sbind :: RType p c tv r -> !(Symbol) rt_ty :: RType p c tv r -> !(RType p c tv r) RApp :: !c -> ![RType p c tv r] -> ![RTProp p c tv r] -> !r -> RType p c tv r rt_tycon :: RType p c tv r -> !c rt_args :: RType p c tv r -> ![RType p c tv r] rt_pargs :: RType p c tv r -> ![RTProp p c tv r] rt_reft :: RType p c tv r -> !r RAllE :: !Symbol -> !(RType p c tv r) -> !(RType p c tv r) -> RType p c tv r rt_bind :: RType p c tv r -> !Symbol rt_allarg :: RType p c tv r -> !(RType p c tv r) rt_ty :: RType p c tv r -> !(RType p c tv r) REx :: !Symbol -> !(RType p c tv r) -> !(RType p c tv r) -> RType p c tv r rt_bind :: RType p c tv r -> !Symbol rt_exarg :: RType p c tv r -> !(RType p c tv r) rt_ty :: RType p c tv r -> !(RType p c tv r) -- | For expression arguments to type aliases see testsposvector2.hs RExprArg :: Expr -> RType p c tv r RAppTy :: !(RType p c tv r) -> !(RType p c tv r) -> !r -> RType p c tv r rt_arg :: RType p c tv r -> !(RType p c tv r) rt_res :: RType p c tv r -> !(RType p c tv r) rt_reft :: RType p c tv r -> !r RRTy :: ![(Symbol, RType p c tv r)] -> !r -> !Oblig -> !(RType p c tv r) -> RType p c tv r rt_env :: RType p c tv r -> ![(Symbol, RType p c tv r)] rt_ref :: RType p c tv r -> !r rt_obl :: RType p c tv r -> !Oblig rt_ty :: RType p c tv r -> !(RType p c tv r) ROth :: !Symbol -> RType p c tv r -- | let LH match against the Haskell type and add k-vars, e.g. `x:_` see -- testsposHoles.hs RHole :: r -> RType p c tv r -- | Ref describes `Prop τ` and HProp arguments applied -- to type constructors. For example, in [a]- v > h}>, we -- apply (via RApp) * the RProp denoted by `{h -> v > -- h}` to * the RTyCon denoted by `[]`. Thus, Ref is used -- for abstract-predicate (arguments) that are associated with _type -- constructors_ i.e. whose semantics are _dependent upon_ the data-type. -- In contrast, the Predicate argument in ur_pred in the -- UReft applies directly to any type and has semantics -- _independent of_ the data-type. data Ref τ r t -- | Parse-time RProp RPropP :: [(Symbol, τ)] -> r -> Ref τ r t rf_args :: Ref τ r t -> [(Symbol, τ)] rf_reft :: Ref τ r t -> r -- | Abstract refinement associated with RTyCon RProp :: [(Symbol, τ)] -> t -> Ref τ r t rf_args :: Ref τ r t -> [(Symbol, τ)] rf_body :: Ref τ r t -> t -- | Abstract heap-refinement associated with RTyCon RHProp :: [(Symbol, τ)] -> World t -> Ref τ r t rf_args :: Ref τ r t -> [(Symbol, τ)] rf_heap :: Ref τ r t -> World t -- | RTProp is a convenient alias for Ref that will save -- a bunch of typing. In general, perhaps we need not expose Ref -- directly at all. type RTProp p c tv r = Ref (RType p c tv ()) r (RType p c tv r) newtype RTyVar RTV :: TyVar -> RTyVar -- | Refinement Type Aliases data RTAlias tv ty RTA :: Symbol -> [tv] -> [tv] -> ty -> SourcePos -> RTAlias tv ty rtName :: RTAlias tv ty -> Symbol rtTArgs :: RTAlias tv ty -> [tv] rtVArgs :: RTAlias tv ty -> [tv] rtBody :: RTAlias tv ty -> ty rtPos :: RTAlias tv ty -> SourcePos data HSeg t HBind :: !Symbol -> t -> HSeg t hs_addr :: HSeg t -> !Symbol hs_val :: HSeg t -> t HVar :: UsedPVar -> HSeg t -- | A World is a Separation Logic predicate that is essentially a -- sequence of binders that satisfies two invariants (TODO:LIQUID): 1. -- Each `hs_addr :: Symbol` appears at most once, 2. There is at most one -- HVar in a list. newtype World t World :: [HSeg t] -> World t class Eq c => TyConable c where isClass = const False isNumCls = const False isFracCls = const False isFun :: TyConable c => c -> Bool isList :: TyConable c => c -> Bool isTuple :: TyConable c => c -> Bool ppTycon :: TyConable c => c -> Doc isClass :: TyConable c => c -> Bool isNumCls :: TyConable c => c -> Bool isFracCls :: TyConable c => c -> Bool class (TyConable c, Eq p, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable p c tv r ppCls :: RefTypable p c tv r => p -> [RType p c tv r] -> Doc ppRType :: RefTypable p c tv r => Prec -> RType p c tv r -> Doc class SubsTy tv ty a subt :: SubsTy tv ty a => (tv, ty) -> a -> a -- | Abstract Predicate Variables ---------------------------------- data PVar t PV :: !Symbol -> !(PVKind t) -> !Symbol -> ![(t, Symbol, Expr)] -> PVar t pname :: PVar t -> !Symbol ptype :: PVar t -> !(PVKind t) parg :: PVar t -> !Symbol pargs :: PVar t -> ![(t, Symbol, Expr)] isPropPV :: PVar t -> Bool pvType :: PVar t -> t data PVKind t PVProp :: t -> PVKind t PVHProp :: PVKind t newtype Predicate Pr :: [UsedPVar] -> Predicate data UReft r U :: !r -> !Predicate -> !Strata -> UReft r ur_reft :: UReft r -> !r ur_pred :: UReft r -> !Predicate ur_strata :: UReft r -> !Strata -- | Values Related to Specifications ------------------------------------ -- -- Data type refinements data DataDecl D :: LocSymbol -> [Symbol] -> [PVar BSort] -> [Symbol] -> [(LocSymbol, [(Symbol, BareType)])] -> !SourcePos -> (Maybe (Symbol -> Expr)) -> DataDecl -- | Type Constructor Name tycName :: DataDecl -> LocSymbol -- | Tyvar Parameters tycTyVars :: DataDecl -> [Symbol] -- | PVar Parameters tycPVars :: DataDecl -> [PVar BSort] -- | PLabel Parameters tycTyLabs :: DataDecl -> [Symbol] -- | tycDCons :: DataDecl -> [(LocSymbol, [(Symbol, BareType)])] -- | Source Position tycSrcPos :: DataDecl -> !SourcePos -- | Measure that should decrease in recursive calls tycSFun :: DataDecl -> (Maybe (Symbol -> Expr)) data DataConP DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> DataConP dc_loc :: DataConP -> !SourcePos freeTyVars :: DataConP -> ![RTyVar] freePred :: DataConP -> ![PVar RSort] freeLabels :: DataConP -> ![Symbol] -- | FIXME: WHAT IS THIS?? tyConsts :: DataConP -> ![SpecType] -- | These are backwards, why?? tyArgs :: DataConP -> ![(Symbol, SpecType)] tyRes :: DataConP -> !SpecType data TyConP TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![Int] -> ![Int] -> !(Maybe (Symbol -> Expr)) -> TyConP freeTyVarsTy :: TyConP -> ![RTyVar] freePredTy :: TyConP -> ![PVar RSort] freeLabelTy :: TyConP -> ![Symbol] -- | indexes of covariant predicate arguments covPs :: TyConP -> ![Int] -- | indexes of contravariant predicate arguments contravPs :: TyConP -> ![Int] sizeFun :: TyConP -> !(Maybe (Symbol -> Expr)) type RRType = RType Class RTyCon RTyVar type BRType = RType LocSymbol LocSymbol Symbol type RRProp r = Ref RSort r (RRType r) type BSort = BRType () type BPVar = PVar BSort type BareType = BRType RReft type PrType = RRType Predicate type SpecType = RRType RReft type SpecProp = RRProp RReft type RSort = RRType () type UsedPVar = PVar () type RPVar = PVar RSort type RReft = UReft Reft -- | Error Data Type --------------------------------------------------- -- -- The type used during constraint generation, used also to define -- contexts for errors, hence in this file, and NOT in Constraint.hs newtype REnv REnv :: (HashMap Symbol SpecType) -> REnv -- | Datacons -- -- Constructor and Destructors for RTypes ---------------------------- data RTypeRep p c tv r RTypeRep :: [tv] -> [PVar (RType p c tv ())] -> [Symbol] -> [Symbol] -> [RType p c tv r] -> (RType p c tv r) -> RTypeRep p c tv r ty_vars :: RTypeRep p c tv r -> [tv] ty_preds :: RTypeRep p c tv r -> [PVar (RType p c tv ())] ty_labels :: RTypeRep p c tv r -> [Symbol] ty_binds :: RTypeRep p c tv r -> [Symbol] ty_args :: RTypeRep p c tv r -> [RType p c tv r] ty_res :: RTypeRep p c tv r -> (RType p c tv r) fromRTypeRep :: Monoid r => RTypeRep p c tv r -> RType p c tv r toRTypeRep :: RType p c tv r -> RTypeRep p c tv r mkArrow :: Monoid r => [a] -> [PVar (RType p c a ())] -> [Symbol] -> [(Symbol, RType p c a r)] -> RType p c a r -> RType p c a r bkArrowDeep :: RType t t1 t2 t3 -> ([Symbol], [RType t t1 t2 t3], RType t t1 t2 t3) bkArrow :: RType t t1 t2 t3 -> ([Symbol], [RType t t1 t2 t3], RType t t1 t2 t3) safeBkArrow :: RType t t1 t2 t3 -> ([Symbol], [RType t t1 t2 t3], RType t t1 t2 t3) mkUnivs :: [a] -> [PVar (RType p c a ())] -> [Symbol] -> RType p c a r -> RType p c a r bkUniv :: RType t t1 a t2 -> ([a], [PVar (RType t t1 a ())], [Symbol], RType t t1 a t2) bkClass :: TyConable t3 => RType t t3 t1 t2 -> ([(t3, [RType t t3 t1 t2])], RType t t3 t1 t2) rFun :: Monoid r => Symbol -> RType p c tv r -> RType p c tv r -> RType p c tv r rCls :: Monoid r => TyCon -> [RType p RTyCon tv r] -> RType p RTyCon tv r rRCls :: Monoid r => c -> [RType p c tv r] -> RType p c tv r pvars :: Predicate -> [UsedPVar] pappSym :: Show a => a -> Symbol pToRef :: PVar a -> Refa pApp :: Symbol -> [Expr] -> Pred isBase :: RType t t1 t2 t3 -> Bool isFunTy :: RType t t1 t2 t3 -> Bool isTrivial :: (TyConable c, Reftable r) => RType p c tv r -> Bool efoldReft :: (TyConable c, Reftable r) => (c -> [RType p c tv r] -> [(Symbol, a)]) -> (RType p c tv r -> a) -> (SEnv a -> Maybe (RType p c tv r) -> r -> c1 -> c1) -> (PVar (RType p c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> c1 -> RType p c tv r -> c1 foldReft :: (TyConable c, Reftable r) => (r -> c1 -> c1) -> c1 -> RType p c tv r -> c1 mapReft :: (r1 -> r2) -> RType p c tv r1 -> RType p c tv r2 mapReftM :: Monad m => (r1 -> m r2) -> RType p c tv r1 -> m (RType p c tv r2) mapBot :: (RType p c tv s -> RType p c tv s) -> RType p c tv s -> RType p c tv s mapBind :: (Symbol -> Symbol) -> RType p c tv r -> RType p c tv r data Oblig -- | Obligation that proves termination OTerm :: Oblig -- | Obligation that proves invariants OInv :: Oblig ignoreOblig :: RType t t1 t2 t3 -> RType t t1 t2 t3 addTermCond :: SpecType -> RReft -> SpecType addInvCond :: SpecType -> RReft -> SpecType -- | Annotations ------------------------------------------------------- newtype AnnInfo a AI :: (HashMap SrcSpan [(Maybe Text, a)]) -> AnnInfo a data Annot t AnnUse :: t -> Annot t AnnDef :: t -> Annot t AnnRDf :: t -> Annot t AnnLoc :: SrcSpan -> Annot t -- | Output ------------------------------------------------------------ data Output a O :: Maybe [String] -> ![Error] -> !(AnnInfo a) -> !(AnnInfo a) -> ![SrcSpan] -> FixResult Error -> Output a o_vars :: Output a -> Maybe [String] o_errors :: Output a -> ![Error] o_types :: Output a -> !(AnnInfo a) o_templs :: Output a -> !(AnnInfo a) o_bots :: Output a -> ![SrcSpan] o_result :: Output a -> FixResult Error hole :: Refa isHole :: Refa -> Bool hasHole :: Reftable r => r -> Bool ofRSort :: Reftable r => RType p c tv () -> RType p c tv r toRSort :: RType p c tv r -> RType p c tv () rTypeValueVar :: Reftable r => RType p c tv r -> Symbol rTypeReft :: Reftable r => RType p c tv r -> Reft stripRTypeBase :: RType t t1 t2 a -> Maybe a class PPrint a where pprintTidy _ = pprint pprint :: PPrint a => a -> Doc pprintTidy :: PPrint a => Tidy -> a -> Doc showpp :: PPrint a => a -> String data PPEnv PP :: Bool -> Bool -> Bool -> Bool -> PPEnv ppPs :: PPEnv -> Bool ppTyVar :: PPEnv -> Bool ppSs :: PPEnv -> Bool ppShort :: PPEnv -> Bool -- | Printer -- ---------------------------------------------------------------- data Tidy Lossy :: Tidy Full :: Tidy ppEnv :: PPEnv ppEnvShort :: PPEnv -> PPEnv data ModName ModName :: !ModType -> !ModuleName -> ModName data ModType Target :: ModType SrcImport :: ModType SpecImport :: ModType isSrcImport :: ModName -> Bool isSpecImport :: ModName -> Bool getModName :: ModName -> ModuleName getModString :: ModName -> String data RTEnv RTE :: HashMap Symbol RTBareOrSpec -> HashMap Symbol RTPredAlias -> HashMap Symbol RTExprAlias -> RTEnv typeAliases :: RTEnv -> HashMap Symbol RTBareOrSpec predAliases :: RTEnv -> HashMap Symbol RTPredAlias exprAliases :: RTEnv -> HashMap Symbol RTExprAlias type RTBareOrSpec = Either (ModName, RTAlias Symbol BareType) (RTAlias RTyVar SpecType) mapRT :: (HashMap Symbol RTBareOrSpec -> HashMap Symbol RTBareOrSpec) -> RTEnv -> RTEnv mapRP :: (HashMap Symbol RTPredAlias -> HashMap Symbol RTPredAlias) -> RTEnv -> RTEnv mapRE :: (HashMap Symbol RTExprAlias -> HashMap Symbol RTExprAlias) -> RTEnv -> RTEnv -- | Converting Results To Answers ------------------------------------- class Result a result :: Result a => a -> FixResult Error -- | In the below, we use EMsg instead of, say, SpecType because the latter -- is impossible to serialize, as it contains GHC internals like TyCon -- and Class inside it. type Error = TError SpecType -- | INVARIANT : all Error constructors should have a pos field data TError t -- | liquid type error ErrSubType :: !SrcSpan -> !Doc -> !(HashMap Symbol t) -> !t -> !t -> TError t pos :: TError t -> !SrcSpan msg :: TError t -> !Doc ctx :: TError t -> !(HashMap Symbol t) tact :: TError t -> !t texp :: TError t -> !t -- | liquid type error ErrAssType :: !SrcSpan -> !Oblig -> !Doc -> !RReft -> TError t pos :: TError t -> !SrcSpan obl :: TError t -> !Oblig msg :: TError t -> !Doc ref :: TError t -> !RReft -- | specification parse error ErrParse :: !SrcSpan -> !Doc -> !ParseError -> TError t pos :: TError t -> !SrcSpan msg :: TError t -> !Doc err :: TError t -> !ParseError -- | sort error in specification ErrTySpec :: !SrcSpan -> !Doc -> !t -> !Doc -> TError t pos :: TError t -> !SrcSpan var :: TError t -> !Doc typ :: TError t -> !t msg :: TError t -> !Doc -- | multiple alias with same name error ErrDupAlias :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t pos :: TError t -> !SrcSpan var :: TError t -> !Doc kind :: TError t -> !Doc locs :: TError t -> ![SrcSpan] -- | multiple specs for same binder error ErrDupSpecs :: !SrcSpan -> !Doc -> ![SrcSpan] -> TError t pos :: TError t -> !SrcSpan var :: TError t -> !Doc locs :: TError t -> ![SrcSpan] -- | Invariant sort error ErrInvt :: !SrcSpan -> !t -> !Doc -> TError t pos :: TError t -> !SrcSpan inv :: TError t -> !t msg :: TError t -> !Doc -- | Using sort error ErrIAl :: !SrcSpan -> !t -> !Doc -> TError t pos :: TError t -> !SrcSpan inv :: TError t -> !t msg :: TError t -> !Doc -- | Incompatible using error ErrIAlMis :: !SrcSpan -> !t -> !t -> !Doc -> TError t pos :: TError t -> !SrcSpan t1 :: TError t -> !t t2 :: TError t -> !t msg :: TError t -> !Doc -- | Measure sort error ErrMeas :: !SrcSpan -> !Symbol -> !Doc -> TError t pos :: TError t -> !SrcSpan ms :: TError t -> !Symbol msg :: TError t -> !Doc -- | Haskell bad Measure error ErrHMeas :: !SrcSpan -> !Symbol -> !Doc -> TError t pos :: TError t -> !SrcSpan ms :: TError t -> !Symbol msg :: TError t -> !Doc -- | Unbound symbol in specification ErrUnbound :: !SrcSpan -> !Doc -> TError t pos :: TError t -> !SrcSpan var :: TError t -> !Doc -- | GHC error: parsing or type checking ErrGhc :: !SrcSpan -> !Doc -> TError t pos :: TError t -> !SrcSpan msg :: TError t -> !Doc -- | Mismatch between Liquid and Haskell types ErrMismatch :: !SrcSpan -> !Doc -> !Type -> !t -> TError t pos :: TError t -> !SrcSpan var :: TError t -> !Doc hs :: TError t -> !Type texp :: TError t -> !t ErrAliasApp :: !SrcSpan -> !Int -> !Doc -> !SrcSpan -> !Int -> TError t pos :: TError t -> !SrcSpan nargs :: TError t -> !Int dname :: TError t -> !Doc dpos :: TError t -> !SrcSpan dargs :: TError t -> !Int -- | Previously saved error, that carries over after DiffCheck ErrSaved :: !SrcSpan -> !Doc -> TError t pos :: TError t -> !SrcSpan msg :: TError t -> !Doc -- | Termination Error ErrTermin :: ![Var] -> !SrcSpan -> !Doc -> TError t bind :: TError t -> ![Var] pos :: TError t -> !SrcSpan msg :: TError t -> !Doc -- | Unexpected PANIC ErrOther :: !SrcSpan -> !Doc -> TError t pos :: TError t -> !SrcSpan msg :: TError t -> !Doc newtype EMsg EMsg :: String -> EMsg type ErrorResult = FixResult Error errSpan :: TError a -> SrcSpan errOther :: Doc -> Error -- | Source Information Associated With Constraints -------------------- data Cinfo Ci :: !SrcSpan -> !(Maybe Error) -> Cinfo ci_loc :: Cinfo -> !SrcSpan ci_err :: Cinfo -> !(Maybe Error) data Measure ty ctor M :: LocSymbol -> ty -> [Def ctor] -> Measure ty ctor name :: Measure ty ctor -> LocSymbol sort :: Measure ty ctor -> ty eqns :: Measure ty ctor -> [Def ctor] data CMeasure ty CM :: LocSymbol -> ty -> CMeasure ty cName :: CMeasure ty -> LocSymbol cSort :: CMeasure ty -> ty data Def ctor Def :: LocSymbol -> ctor -> [Symbol] -> Body -> Def ctor measure :: Def ctor -> LocSymbol ctor :: Def ctor -> ctor binds :: Def ctor -> [Symbol] body :: Def ctor -> Body data Body -- | Measure Refinement: {v | v = e } E :: Expr -> Body -- | Measure Refinement: {v | (? v) = p } P :: Pred -> Body -- | Measure Refinement: {v | p} R :: Symbol -> Pred -> Body data RClass ty RClass :: LocSymbol -> [ty] -> [Symbol] -> [(LocSymbol, ty)] -> RClass ty rcName :: RClass ty -> LocSymbol rcSupers :: RClass ty -> [ty] rcTyVars :: RClass ty -> [Symbol] rcMethods :: RClass ty -> [(LocSymbol, ty)] -- | KVar Profile ----------------------------------------- data KVKind RecBindE :: KVKind NonRecBindE :: KVKind TypeInstE :: KVKind PredInstE :: KVKind LamE :: KVKind CaseE :: KVKind LetE :: KVKind data KVProf emptyKVProf :: KVProf updKVProf :: KVKind -> [Symbol] -> KVProf -> KVProf mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a data Stratum SVar :: Symbol -> Stratum SDiv :: Stratum SWhnf :: Stratum SFin :: Stratum type Strata = [Stratum] isSVar :: Stratum -> Bool getStrata :: RType t t1 t2 (UReft r) -> [Stratum] makeDivType :: SpecType -> SpecType makeFinType :: SpecType -> SpecType instance [overlap ok] Typeable Config instance [overlap ok] Typeable PVKind instance [overlap ok] Typeable PVar instance [overlap ok] Typeable Predicate instance [overlap ok] Typeable RTyVar instance [overlap ok] Typeable TyConInfo instance [overlap ok] Typeable Oblig instance [overlap ok] Typeable HSeg instance [overlap ok] Typeable World instance [overlap ok] Typeable Ref instance [overlap ok] Typeable RType instance [overlap ok] Typeable RTyCon instance [overlap ok] Typeable TyConP instance [overlap ok] Typeable Stratum instance [overlap ok] Typeable UReft instance [overlap ok] Typeable DataConP instance [overlap ok] Typeable EMsg instance [overlap ok] Typeable TError instance [overlap ok] Typeable Body instance [overlap ok] Typeable Def instance [overlap ok] Typeable Measure instance [overlap ok] Typeable KVKind instance [overlap ok] Eq ctor => Eq (Def ctor) instance [overlap ok] Data Config instance [overlap ok] Show Config instance [overlap ok] Eq Config instance [overlap ok] Eq Tidy instance [overlap ok] Ord Tidy instance [overlap ok] Generic (PVKind t) instance [overlap ok] Data t => Data (PVKind t) instance [overlap ok] Foldable PVKind instance [overlap ok] Traversable PVKind instance [overlap ok] Show t => Show (PVKind t) instance [overlap ok] Generic (PVar t) instance [overlap ok] Data t => Data (PVar t) instance [overlap ok] Show t => Show (PVar t) instance [overlap ok] Generic Predicate instance [overlap ok] Data Predicate instance [overlap ok] Generic RTyVar instance [overlap ok] Data RTyVar instance [overlap ok] Generic TyConInfo instance [overlap ok] Data TyConInfo instance [overlap ok] Generic Oblig instance [overlap ok] Data Oblig instance [overlap ok] Generic (HSeg t) instance [overlap ok] Data t => Data (HSeg t) instance [overlap ok] Generic (World t) instance [overlap ok] Data t => Data (World t) instance [overlap ok] Generic (Ref τ r t) instance [overlap ok] (Data τ, Data r, Data t) => Data (Ref τ r t) instance [overlap ok] Generic (RType p c tv r) instance [overlap ok] (Data p, Data c, Data tv, Data r) => Data (RType p c tv r) instance [overlap ok] Generic RTyCon instance [overlap ok] Data RTyCon instance [overlap ok] Data TyConP instance [overlap ok] Generic Stratum instance [overlap ok] Data Stratum instance [overlap ok] Eq Stratum instance [overlap ok] Generic (UReft r) instance [overlap ok] Data r => Data (UReft r) instance [overlap ok] Data DataConP instance [overlap ok] Generic EMsg instance [overlap ok] Data EMsg instance [overlap ok] Functor TError instance [overlap ok] Eq Cinfo instance [overlap ok] Ord Cinfo instance [overlap ok] Eq ModType instance [overlap ok] Ord ModType instance [overlap ok] Eq ModName instance [overlap ok] Ord ModName instance [overlap ok] Show Body instance [overlap ok] Eq Body instance [overlap ok] Data Body instance [overlap ok] Show ctor => Show (Def ctor) instance [overlap ok] Data ctor => Data (Def ctor) instance [overlap ok] (Data ty, Data ctor) => Data (Measure ty ctor) instance [overlap ok] Show ty => Show (RClass ty) instance [overlap ok] Generic (AnnInfo a) instance [overlap ok] Generic (Output a) instance [overlap ok] Generic KVKind instance [overlap ok] Eq KVKind instance [overlap ok] Ord KVKind instance [overlap ok] Show KVKind instance [overlap ok] Enum KVKind instance [overlap ok] Data KVKind instance Datatype D1PVKind instance Constructor C1_0PVKind instance Constructor C1_1PVKind instance Datatype D1PVar instance Constructor C1_0PVar instance Selector S1_0_0PVar instance Selector S1_0_1PVar instance Selector S1_0_2PVar instance Selector S1_0_3PVar instance Datatype D1Predicate instance Constructor C1_0Predicate instance Datatype D1RTyVar instance Constructor C1_0RTyVar instance Datatype D1TyConInfo instance Constructor C1_0TyConInfo instance Selector S1_0_0TyConInfo instance Selector S1_0_1TyConInfo instance Selector S1_0_2TyConInfo instance Selector S1_0_3TyConInfo instance Selector S1_0_4TyConInfo instance Datatype D1Oblig instance Constructor C1_0Oblig instance Constructor C1_1Oblig instance Datatype D1HSeg instance Constructor C1_0HSeg instance Constructor C1_1HSeg instance Selector S1_0_0HSeg instance Selector S1_0_1HSeg instance Datatype D1World instance Constructor C1_0World instance Datatype D1Ref instance Constructor C1_0Ref instance Constructor C1_1Ref instance Constructor C1_2Ref instance Selector S1_0_0Ref instance Selector S1_0_1Ref instance Selector S1_1_0Ref instance Selector S1_1_1Ref instance Selector S1_2_0Ref instance Selector S1_2_1Ref instance Datatype D1RType instance Constructor C1_0RType instance Constructor C1_1RType instance Constructor C1_2RType instance Constructor C1_3RType instance Constructor C1_4RType instance Constructor C1_5RType instance Constructor C1_6RType instance Constructor C1_7RType instance Constructor C1_8RType instance Constructor C1_9RType instance Constructor C1_10RType instance Constructor C1_11RType instance Constructor C1_12RType instance Selector S1_0_0RType instance Selector S1_0_1RType instance Selector S1_1_0RType instance Selector S1_1_1RType instance Selector S1_1_2RType instance Selector S1_1_3RType instance Selector S1_2_0RType instance Selector S1_2_1RType instance Selector S1_3_0RType instance Selector S1_3_1RType instance Selector S1_4_0RType instance Selector S1_4_1RType instance Selector S1_5_0RType instance Selector S1_5_1RType instance Selector S1_5_2RType instance Selector S1_5_3RType instance Selector S1_6_0RType instance Selector S1_6_1RType instance Selector S1_6_2RType instance Selector S1_7_0RType instance Selector S1_7_1RType instance Selector S1_7_2RType instance Selector S1_9_0RType instance Selector S1_9_1RType instance Selector S1_9_2RType instance Selector S1_10_0RType instance Selector S1_10_1RType instance Selector S1_10_2RType instance Selector S1_10_3RType instance Datatype D1RTyCon instance Constructor C1_0RTyCon instance Selector S1_0_0RTyCon instance Selector S1_0_1RTyCon instance Selector S1_0_2RTyCon instance Datatype D1Stratum instance Constructor C1_0Stratum instance Constructor C1_1Stratum instance Constructor C1_2Stratum instance Constructor C1_3Stratum instance Datatype D1UReft instance Constructor C1_0UReft instance Selector S1_0_0UReft instance Selector S1_0_1UReft instance Selector S1_0_2UReft instance Datatype D1EMsg instance Constructor C1_0EMsg instance Datatype D1AnnInfo instance Constructor C1_0AnnInfo instance Datatype D1Output instance Constructor C1_0Output instance Selector S1_0_0Output instance Selector S1_0_1Output instance Selector S1_0_2Output instance Selector S1_0_3Output instance Selector S1_0_4Output instance Selector S1_0_5Output instance Datatype D1KVKind instance Constructor C1_0KVKind instance Constructor C1_1KVKind instance Constructor C1_2KVKind instance Constructor C1_3KVKind instance Constructor C1_4KVKind instance Constructor C1_5KVKind instance Constructor C1_6KVKind instance [overlap ok] Show DataCon instance [overlap ok] PPrint DataCon instance [overlap ok] Symbolic Var instance [overlap ok] Symbolic DataCon instance [overlap ok] NFData KVProf instance [overlap ok] PPrint KVProf instance [overlap ok] PPrint KVKind instance [overlap ok] NFData KVKind instance [overlap ok] Hashable KVKind instance [overlap ok] Monoid (Output a) instance [overlap ok] NFData (Annot a) instance [overlap ok] NFData a => NFData (AnnInfo a) instance [overlap ok] Functor AnnInfo instance [overlap ok] Monoid (AnnInfo a) instance [overlap ok] Functor RClass instance [overlap ok] Subable Body instance [overlap ok] Subable (Def ctor) instance [overlap ok] Subable (Measure ty ctor) instance [overlap ok] Monoid RTEnv instance [overlap ok] Symbolic ModuleName instance [overlap ok] Symbolic ModName instance [overlap ok] Show ModName instance [overlap ok] Result (FixResult Cinfo) instance [overlap ok] Result Error instance [overlap ok] Result [Error] instance [overlap ok] NFData Cinfo instance [overlap ok] Error Error instance [overlap ok] Ord Error instance [overlap ok] Eq Error instance [overlap ok] PPrint EMsg instance [overlap ok] PPrint SortedReft instance [overlap ok] PPrint Reft instance [overlap ok] PPrint Refa instance [overlap ok] PPrint Predicate instance [overlap ok] PPrint a => PPrint (PVar a) instance [overlap ok] PPrint Pred instance [overlap ok] PPrint SymConst instance [overlap ok] PPrint Expr instance [overlap ok] PPrint Symbol instance [overlap ok] PPrint Sort instance [overlap ok] PPrint Bop instance [overlap ok] PPrint Brel instance [overlap ok] PPrint Constant instance [overlap ok] PPrint Integer instance [overlap ok] PPrint Int instance [overlap ok] PPrint a => PPrint (Located a) instance [overlap ok] PPrint Text instance [overlap ok] PPrint String instance [overlap ok] PPrint () instance [overlap ok] PPrint SourcePos instance [overlap ok] PPrint Strata instance [overlap ok] PPrint Stratum instance [overlap ok] Show Stratum instance [overlap ok] Functor (RType a b c) instance [overlap ok] Functor UReft instance [overlap ok] Reftable Predicate instance [overlap ok] (Subable r, RefTypable p c tv r) => Subable (RType p c tv r) instance [overlap ok] (Reftable r, RefTypable p c tv r) => Subable (RTProp p c tv r) instance [overlap ok] Subable r => Subable (UReft r) instance [overlap ok] (PPrint r, Reftable r) => Reftable (UReft r) instance [overlap ok] Reftable Strata instance [overlap ok] Subable Strata instance [overlap ok] Subable Stratum instance [overlap ok] Show DataDecl instance [overlap ok] Show RTyCon instance [overlap ok] PPrint RTyCon instance [overlap ok] Fixpoint RTyCon instance [overlap ok] Eq RTyCon instance [overlap ok] TyConable LocSymbol instance [overlap ok] TyConable Symbol instance [overlap ok] TyConable RTyCon instance [overlap ok] Monoid Strata instance [overlap ok] PPrint Oblig instance [overlap ok] Show Oblig instance [overlap ok] Default TyConInfo instance [overlap ok] Symbolic RTyVar instance [overlap ok] NFData RTyVar instance [overlap ok] NFData PrType instance [overlap ok] NFData Strata instance [overlap ok] NFData r => NFData (UReft r) instance [overlap ok] Subable Qualifier instance [overlap ok] Subable Predicate instance [overlap ok] Subable UsedPVar instance [overlap ok] Monoid a => Monoid (UReft a) instance [overlap ok] Monoid Predicate instance [overlap ok] NFData Predicate instance [overlap ok] Hashable (PVar a) instance [overlap ok] NFData a => NFData (PVar a) instance [overlap ok] NFData a => NFData (PVKind a) instance [overlap ok] Functor PVar instance [overlap ok] Functor PVKind instance [overlap ok] Ord (PVar t) instance [overlap ok] Eq (PVar t) instance [overlap ok] (PPrint a, PPrint b) => PPrint (a, b) instance [overlap ok] PPrint a => PPrint [a] instance [overlap ok] PPrint a => PPrint (Maybe a) module Language.Haskell.Liquid.Fresh class (Applicative m, Monad m) => Freshable m a where true = return . id refresh = return . id fresh :: Freshable m a => m a true :: Freshable m a => a -> m a refresh :: Freshable m a => a -> m a instance (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) instance Freshable m Integer => Freshable m Strata instance Freshable m Integer => Freshable m RReft instance Freshable m Integer => Freshable m Reft instance Freshable m Integer => Freshable m [Refa] instance Freshable m Integer => Freshable m Refa instance Freshable m Integer => Freshable m Symbol module Language.Haskell.Liquid.Strata class SubStratum a where subsS su x = foldr subS x su subS :: SubStratum a => (Symbol, Stratum) -> a -> a subsS :: SubStratum a => [(Symbol, Stratum)] -> a -> a solveStrata :: [([Stratum], [Stratum])] -> [(Symbol, Stratum)] (<:=) :: [Stratum] -> [Stratum] -> Bool instance SubStratum SpecType instance SubStratum (Annot SpecType) instance SubStratum a => SubStratum [a] instance (SubStratum a, SubStratum b) => SubStratum (a, b) instance SubStratum Stratum -- | This module contains various functions for operating on the -- World type defined in Language.Haskell.Liquid.Types module Language.Haskell.Liquid.World empty :: World t instance Monoid (World t) module Language.Haskell.Liquid.CoreToLogic coreToDef :: LocSymbol -> Var -> CoreExpr -> LogicM [Def DataCon] mkLit :: Literal -> Maybe Expr runToLogic :: LogicM t -> Either t LError data LError LE :: String -> LError instance Simplify CoreAlt instance Simplify CoreBind instance Simplify CoreExpr instance Applicative LogicM instance Functor LogicM instance Monad LogicM -- | Formats Haskell source code as HTML with CSS and Mouseover Type -- Annotations module Language.Haskell.Liquid.ACSS -- | Formats Haskell source code using HTML and mouse-over annotations hscolour :: Bool -> Bool -> String -> String -- | Formats Haskell source code using HTML and mouse-over annotations hsannot :: Bool -> CommentTransform -> Bool -> (String, AnnMap) -> String data AnnMap Ann :: HashMap Loc (String, String) -> [(Loc, Loc, String)] -> !Status -> AnnMap -- | Loc -> (Var, Type) types :: AnnMap -> HashMap Loc (String, String) -- | List of error intervals errors :: AnnMap -> [(Loc, Loc, String)] status :: AnnMap -> !Status breakS :: [Char] srcModuleName :: String -> String data Status Safe :: Status Unsafe :: Status Error :: Status Crash :: Status instance Eq Status instance Ord Status instance Show Status instance Show Annotation instance Show Lit instance Show AnnMap module Language.Haskell.Liquid.Desugar.DsExpr dsExpr :: HsExpr Id -> DsM CoreExpr dsLExpr :: LHsExpr Id -> DsM CoreExpr dsLocalBinds :: HsLocalBinds Id -> CoreExpr -> DsM CoreExpr dsValBinds :: HsValBinds Id -> CoreExpr -> DsM CoreExpr dsLit :: HsLit -> DsM CoreExpr module Language.Haskell.Liquid.Desugar.Desugar -- | Main entry point to the desugarer. deSugarWithLoc :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts) -- | Main entry point to the desugarer. deSugar :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts) deSugarExpr :: HscEnv -> LHsExpr Id -> IO (Messages, Maybe CoreExpr) -- | Main API for compiling plain Haskell source code. -- -- This module implements compilation of a Haskell source. It is -- not concerned with preprocessing of source files; this is -- handled in DriverPipeline. -- -- There are various entry points depending on what mode we're in: -- "batch" mode (--make), "one-shot" mode (-c, -- -S etc.), and "interactive" mode (GHCi). There are also entry -- points for individual passes: parsing, typechecking/renaming, -- desugaring, and simplification. -- -- All the functions here take an HscEnv as a parameter, but none -- of them return a new one: HscEnv is treated as an immutable -- value from here on in (although it has mutable components, for the -- caches). -- -- Warning messages are dealt with consistently throughout this API: -- during compilation warnings are collected, and before any function in -- HscMain returns, the warnings are either printed, or turned -- into a real compialtion error if the -Werror flag is enabled. -- -- (c) The GRASP/AQUA Project, Glasgow University, 1993-2000 module Language.Haskell.Liquid.Desugar.HscMain -- | Convert a typechecked module to Core hscDesugarWithLoc :: HscEnv -> ModSummary -> TcGblEnv -> IO ModGuts module Language.Haskell.Liquid.Desugar.DsMeta dsBracket :: HsBracket Name -> [PendingTcSplice] -> DsM CoreExpr templateHaskellNames :: [Name] qTyConName :: Name nameTyConName :: Name liftName :: Name liftStringName :: Name expQTyConName :: Name patQTyConName :: Name decQTyConName :: Name decsQTyConName :: Name typeQTyConName :: Name decTyConName :: Name typeTyConName :: Name mkNameG_dName :: Name mkNameG_vName :: Name mkNameG_tcName :: Name quoteExpName :: Name quotePatName :: Name quoteDecName :: Name quoteTypeName :: Name tExpTyConName :: Name tExpDataConName :: Name unTypeName :: Name unTypeQName :: Name unsafeTExpCoerceName :: Name module Language.Haskell.Liquid.Misc safeIndex :: [Char] -> Int -> [c] -> c (!?) :: [a] -> Int -> Maybe a safeFromJust :: [Char] -> Maybe t -> t addFst3 :: t -> (t1, t2) -> (t, t1, t2) dropFst3 :: (t, t1, t2) -> (t1, t2) dropThd3 :: (t1, t2, t) -> (t1, t2) replaceN :: (Num a, Eq a, Enum a) => a -> t -> [t] -> [t] fourth4 :: (t, t1, t2, t3) -> t3 third4 :: (t, t1, t2, t3) -> t2 mapSndM :: Monad m => (t -> m a) -> (t1, t) -> m (t1, a) firstM :: Functor f => (t -> f a) -> (t, t1) -> f (a, t1) secondM :: Functor f => (t -> f a) -> (t1, t) -> f (t1, a) first3M :: Functor f => (t -> f a) -> (t, t1, t2) -> f (a, t1, t2) second3M :: Functor f => (t -> f a) -> (t1, t, t2) -> f (t1, a, t2) third3M :: Functor f => (t -> f a) -> (t1, t2, t) -> f (t1, t2, a) third3 :: (t -> t3) -> (t1, t2, t) -> (t1, t2, t3) zip4 :: [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)] getIncludeDir :: IO FilePath getCssPath :: IO FilePath getHqBotPath :: IO FilePath maximumWithDefault :: Ord a => a -> [a] -> a safeZipWithError :: [Char] -> [t] -> [t1] -> [(t, t1)] mapNs :: (Num a, Eq a) => [a] -> (a1 -> a1) -> [a1] -> [a1] mapN :: (Num a, Eq a) => a -> (a1 -> a1) -> [a1] -> [a1] pad :: [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a]) module Language.Haskell.Liquid.TransformRec transformRecExpr :: CoreProgram -> CoreProgram transformScope :: [Bind Id] -> [Bind Id] instance Subable Type instance Subable (Bind Var) instance Subable Var instance Subable (Alt Var) instance Subable Coercion instance Subable CoreExpr instance Freshable Var instance Freshable Unique instance Freshable Int module Language.Haskell.Liquid.ANFTransform anormalize :: Bool -> HscEnv -> MGIModGuts -> IO [CoreBind] instance Functor DsM instance Monad DsM instance MonadUnique DsM instance Applicative DsM -- | Module with all the printing and serialization routines module Language.Haskell.Liquid.PrettyPrint -- | Printer -- ---------------------------------------------------------------- data Tidy Lossy :: Tidy Full :: Tidy -- | Pretty Printing RefType ---------------------------------- rtypeDoc :: (PPrint (RType p a tv ()), PPrint (RType p a tv r), PPrint a, PPrint r, PPrint tv, TyConable a, Reftable (RTProp p a tv r), Reftable r) => Tidy -> RType p a tv r -> Doc ppr_rtype :: (PPrint (RType p a tv ()), PPrint (RType p a tv r), PPrint a, PPrint r, PPrint tv, TyConable a, Reftable (RTProp p a tv r), Reftable r) => PPEnv -> Prec -> RType p a tv r -> Doc -- | Printing an Ordered List pprManyOrdered :: (PPrint a, Ord a) => Tidy -> String -> [a] -> [Doc] pprintLongList :: PPrint a => [a] -> Doc ppSpine :: PPrint a => RType t a t1 t2 -> Doc instance (Ord k, PPrint k, PPrint v) => PPrint (HashMap k v) instance PPrint a => PPrint (AnnInfo a) instance PPrint t => PPrint (Annot t) instance (PPrint r, Reftable r) => PPrint (UReft r) instance (Reftable s, PPrint s, PPrint p, Reftable p, PPrint t, PPrint (RType a b c p)) => PPrint (Ref t s (RType a b c p)) instance PPrint RTyVar instance Show Predicate instance PPrint Class instance PPrint Type instance PPrint Name instance PPrint Var instance PPrint ParseError instance PPrint SourceError instance PPrint ErrMsg instance PPrint Doc instance PPrint SrcSpan -- | Refinement Types. Mostly mirroring the GHC Type definition, but with -- room for refinements of various sorts. module Language.Haskell.Liquid.RefType uTop :: r -> UReft r uReft :: (Symbol, [Refa]) -> UReft Reft -- | Various functions for converting vanilla Reft to Spec uRType :: RType p c tv a -> RType p c tv (UReft a) uRType' :: RType p c tv (UReft a) -> RType p c tv a uRTypeGen :: Reftable b => RType p c tv a -> RType p c tv b uPVar :: PVar t -> UsedPVar applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType isDecreasing :: RType t RTyCon t1 t2 -> Bool makeDecrType :: Symbolic a => [(a, (Symbol, RType p RTyCon tv (UReft Reft)))] -> (Symbol, RType p RTyCon tv (UReft Reft)) makeLexRefa :: [Expr] -> [Expr] -> UReft Reft pdVar :: PVar t -> Predicate findPVar :: [PVar (RType p c tv ())] -> UsedPVar -> PVar (RType p c tv ()) freeTyVars :: RefTypable t t1 a t2 => RType t t1 a t2 -> [a] tyClasses :: RefTypable t RTyCon t1 t2 => RType t RTyCon t1 t2 -> [(Class, [RType t RTyCon t1 t2])] tyConName :: TyCon -> Symbol ofType :: Monoid r => Type -> RType p RTyCon RTyVar r toType :: (Reftable r, PPrint r) => RRType r -> Type rTyVar :: TyVar -> RTyVar rVar :: Monoid r => TyVar -> RType p c RTyVar r rApp :: TyCon -> [RType p RTyCon tv r] -> [RTProp p RTyCon tv r] -> r -> RType p RTyCon tv r rEx :: [(Symbol, RType p c tv r)] -> RType p c tv r -> RType p c tv r addTyConInfo :: (PPrint r, Reftable r) => (HashMap TyCon FTycon) -> (HashMap TyCon RTyCon) -> RRType r -> RRType r appRTyCon :: SubsTy RTyVar (RType p c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType p c RTyVar r] -> RTyCon typeSort :: TCEmb TyCon -> Type -> Sort typeUniqueSymbol :: Type -> Symbol strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv r generalize :: RefTypable c p tv r => RType c p tv r -> RType c p tv r normalizePds :: RefTypable p c tv r => RType p c tv r -> RType p c tv r subts :: SubsTy tv ty c => [(tv, ty)] -> c -> c subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType p c tv (), RType p c tv s) -> RType p c tv s -> RType p c tv s subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType p c tv (), RType p c tv s)] -> RType p c tv s -> RType p c tv s dataConSymbol :: DataCon -> Symbol dataConMsReft :: Reftable r => RType p c tv r -> [Symbol] -> Reft dataConReft :: DataCon -> [Symbol] -> Reft literalFRefType :: TCEmb TyCon -> Literal -> RType p RTyCon RTyVar Reft literalFReft :: TCEmb TyCon -> Literal -> Reft -- | literalConst returns Nothing for unhandled lits because -- otherwise string-literals show up as global int-constants which blow -- up qualifier instantiation. literalConst :: TCEmb TyCon -> Literal -> (Sort, Maybe Expr) -- | Binders generated by class predicates, typically for constraining -- tyvars (e.g. FNum) classBinds :: TyConable c => RType t c RTyVar t1 -> [(Symbol, SortedReft)] rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft rTypeSort :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> Sort shiftVV :: SpecType -> Symbol -> SpecType mkDataConIdsTy :: (PPrint r, Reftable r) => (DataCon, RType Class RTyCon RTyVar r) -> [(Var, RType Class RTyCon RTyVar r)] mkTyConInfo :: TyCon -> [Int] -> [Int] -> (Maybe (Symbol -> Expr)) -> TyConInfo instance [incoherent] (Show tv, Show ty) => Show (RTAlias tv ty) instance [incoherent] Expression Var instance [incoherent] (SubsTy tv ty (UReft r), SubsTy tv ty (RType p c tv ())) => SubsTy tv ty (RTProp p c tv (UReft r)) instance [incoherent] SubsTy Symbol BSort BSort instance [incoherent] SubsTy Symbol BSort LocSymbol instance [incoherent] SubsTy RTyVar RSort RSort instance [incoherent] SubsTy RTyVar RTyVar SpecType instance [incoherent] SubsTy RTyVar RSort SpecType instance [incoherent] SubsTy RTyVar RSort PrType instance [incoherent] SubsTy RTyVar RSort RTyCon instance [incoherent] SubsTy tv ty ty => SubsTy tv ty (PVar ty) instance [incoherent] SubsTy tv ty ty => SubsTy tv ty (PVKind ty) instance [incoherent] SubsTy tv ty Reft instance [incoherent] SubsTy tv ty () instance [incoherent] PPrint REnv instance [incoherent] PPrint (RTProp p c tv r) => Show (RTProp p c tv r) instance [incoherent] PPrint (RType p c tv r) => Show (RType p c tv r) instance [incoherent] RefTypable p c tv r => PPrint (RType p c tv r) instance [incoherent] PPrint (UReft r) => Show (UReft r) instance [incoherent] Show RTyVar instance [incoherent] (NFData a, NFData b, NFData c, NFData e) => NFData (RType a b c e) instance [incoherent] (NFData a, NFData b, NFData t) => NFData (Ref t a b) instance [incoherent] Hashable RTyCon instance [incoherent] Ord RTyCon instance [incoherent] Hashable RTyVar instance [incoherent] Ord RTyVar instance [incoherent] Eq RTyVar instance [incoherent] Eq Predicate instance [incoherent] RefTypable p c tv () => Eq (RType p c tv ()) instance [incoherent] FreeVar LocSymbol Symbol instance [incoherent] FreeVar RTyCon RTyVar instance [incoherent] (Reftable r, PPrint r) => RefTypable Class RTyCon RTyVar r instance [incoherent] (Eq p, PPrint p, TyConable c, Reftable r, PPrint r, PPrint c) => RefTypable p c Symbol r instance [incoherent] Fixpoint Class instance [incoherent] Fixpoint String instance [incoherent] (PPrint r, Reftable r) => Reftable (RType Class RTyCon RTyVar r) instance [incoherent] Subable (RRProp Reft) instance [incoherent] (Reftable r, RefTypable p c tv r, RefTypable p c tv ()) => Reftable (RTProp p c tv r) instance [incoherent] (Monoid r, Reftable r, RefTypable a b c r, RefTypable a b c ()) => Monoid (RTProp a b c r) instance [incoherent] (SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, Reftable r, RefTypable p c tv (), RefTypable p c tv (UReft r)) => Monoid (Ref (RType p c tv ()) r (RType p c tv (UReft r))) instance [incoherent] (SubsTy tv (RType p c tv ()) (RType p c tv ()), SubsTy tv (RType p c tv ()) c, RefTypable p c tv (), RefTypable p c tv r, PPrint (RType p c tv r)) => Monoid (RType p c tv r) module Language.Haskell.Liquid.PredType type PrType = RRType Predicate data TyConP TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![Int] -> ![Int] -> !(Maybe (Symbol -> Expr)) -> TyConP freeTyVarsTy :: TyConP -> ![RTyVar] freePredTy :: TyConP -> ![PVar RSort] freeLabelTy :: TyConP -> ![Symbol] -- | indexes of covariant predicate arguments covPs :: TyConP -> ![Int] -- | indexes of contravariant predicate arguments contravPs :: TyConP -> ![Int] sizeFun :: TyConP -> !(Maybe (Symbol -> Expr)) data DataConP DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> DataConP dc_loc :: DataConP -> !SourcePos freeTyVars :: DataConP -> ![RTyVar] freePred :: DataConP -> ![PVar RSort] freeLabels :: DataConP -> ![Symbol] -- | FIXME: WHAT IS THIS?? tyConsts :: DataConP -> ![SpecType] -- | These are backwards, why?? tyArgs :: DataConP -> ![(Symbol, SpecType)] tyRes :: DataConP -> !SpecType dataConTy :: Monoid r => HashMap RTyVar (RType p RTyCon RTyVar r) -> Type -> RType p RTyCon RTyVar r dataConPSpecType :: DataCon -> DataConP -> SpecType makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon -- | Unify PrType with SpecType ------------------------------------------- unify :: Maybe PrType -> SpecType -> SpecType -- | Instantiate PVar with RTProp -- ----------------------------------------------- -- -- replacePreds is the main function used to substitute an -- (abstract) predicate with a concrete Ref, that is either an -- RProp or RHProp type. The substitution is invoked to -- obtain the SpecType resulting at predicate application -- sites in Constraint. The range of the PVar substitutions -- are fresh or true RefType. That is, there are -- no further _quantified_ PVar in the target. replacePreds :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Refa) -> UReft Reft -> UReft Reft pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Refa exprType :: CoreExpr -> Type -- | Interface: Modified CoreSyn.exprType due to predApp -- ------------------- predType :: Type -- | pvarRType π returns a trivial RType corresponding to -- the function signature for a PVar π. For example, if -- π :: T1 -> T2 -> T3 -> Prop then pvarRType -- π returns an RType with an RTycon called -- predRTyCon `RApp predRTyCon [T1, T2, T3]` pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate pApp :: Symbol -> [Expr] -> Pred wiredSortedSyms :: [(Symbol, Sort)] instance Show DataConP instance PPrint DataConP instance Show TyConP instance PPrint TyConP module Language.Haskell.Liquid.Measure data Spec ty bndr Spec :: ![Measure ty bndr] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![Located ty] -> ![(Located ty, Located ty)] -> ![Symbol] -> ![DataDecl] -> ![FilePath] -> ![RTAlias Symbol BareType] -> ![RTAlias Symbol Pred] -> ![RTAlias Symbol Expr] -> !(TCEmb (LocSymbol)) -> ![Qualifier] -> ![(LocSymbol, [Int])] -> ![(LocSymbol)] -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> ![Located String] -> ![Measure ty ()] -> ![Measure ty bndr] -> ![RClass ty] -> ![(LocSymbol, [Expr])] -> Spec ty bndr -- | User-defined properties for ADTs measures :: Spec ty bndr -> ![Measure ty bndr] -- | Assumed (unchecked) types asmSigs :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Imported functions and types sigs :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Local type signatures localSigs :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Data type invariants invariants :: Spec ty bndr -> ![Located ty] -- | Data type invariants to be checked ialiases :: Spec ty bndr -> ![(Located ty, Located ty)] -- | Loaded spec module names imports :: Spec ty bndr -> ![Symbol] -- | Predicated data definitions dataDecls :: Spec ty bndr -> ![DataDecl] -- | Included qualifier files includes :: Spec ty bndr -> ![FilePath] -- | RefType aliases aliases :: Spec ty bndr -> ![RTAlias Symbol BareType] -- | Refinement/Predicate aliases paliases :: Spec ty bndr -> ![RTAlias Symbol Pred] -- | Expression aliases ealiases :: Spec ty bndr -> ![RTAlias Symbol Expr] -- | GHC-Tycon-to-fixpoint Tycon map embeds :: Spec ty bndr -> !(TCEmb (LocSymbol)) -- | Qualifiers in source/spec files qualifiers :: Spec ty bndr -> ![Qualifier] -- | Information on decreasing arguments decr :: Spec ty bndr -> ![(LocSymbol, [Int])] -- | Variables that should be checked in the environment they are used lvars :: Spec ty bndr -> ![(LocSymbol)] -- | Ignore Termination Check in these Functions lazy :: Spec ty bndr -> !(HashSet LocSymbol) -- | Binders to turn into measures using haskell definitions hmeas :: Spec ty bndr -> !(HashSet LocSymbol) -- | Command-line configurations passed in through source pragmas :: Spec ty bndr -> ![Located String] -- | Measures attached to a type-class cmeasures :: Spec ty bndr -> ![Measure ty ()] -- | Mappings from (measure,type) -> measure imeasures :: Spec ty bndr -> ![Measure ty bndr] -- | Refined Type-Classes classes :: Spec ty bndr -> ![RClass ty] -- | Terminating Conditions for functions termexprs :: Spec ty bndr -> ![(LocSymbol, [Expr])] type BareSpec = Spec BareType LocSymbol data MSpec ty ctor MSpec :: HashMap Symbol [Def ctor] -> HashMap LocSymbol (Measure ty ctor) -> HashMap LocSymbol (Measure ty ()) -> ![Measure ty ctor] -> MSpec ty ctor ctorMap :: MSpec ty ctor -> HashMap Symbol [Def ctor] measMap :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor) cmeasMap :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ()) imeas :: MSpec ty ctor -> ![Measure ty ctor] mkM :: LocSymbol -> ty -> [Def bndr] -> Measure ty bndr mkMSpec :: [Measure ty (Located Symbol)] -> [Measure ty ()] -> [Measure ty (Located Symbol)] -> MSpec ty (Located Symbol) mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr mapTy :: (tya -> tyb) -> Measure tya c -> Measure tyb c dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)]) defRefType :: Def DataCon -> RRType Reft instance PPrint (CMeasure t) => Show (CMeasure t) instance PPrint t => PPrint (CMeasure t) instance PPrint (Measure t a) => Show (Measure t a) instance (PPrint t, PPrint a) => PPrint (MSpec t a) instance (PPrint t, PPrint a) => PPrint (Measure t a) instance PPrint a => PPrint (Def a) instance PPrint Body instance Bifunctor Spec instance Bifunctor MSpec instance Bifunctor Measure instance Functor (MSpec t) instance Functor CMeasure instance Functor (Measure t) instance Functor Def instance Monoid (Spec ty bndr) instance Eq ctor => Monoid (MSpec ty ctor) instance (Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) module Language.Haskell.Liquid.Parse hsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) lhsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) -- | Used to parse .spec files specSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) instance Inputable (Measure BareType LocSymbol) instance Inputable BareType instance Show (Pspec a b) -- | This module contains functions for cleaning up types before they are -- rendered, e.g. in error messages or annoations. module Language.Haskell.Liquid.Tidy tidySpecType :: Tidy -> SpecType -> SpecType tidySymbol :: Symbol -> Symbol isTmpSymbol :: Symbol -> Bool -- | This module contains the functions related to Error type, in -- particular, to tidyError using a solution, and -- pprint errors. module Language.Haskell.Liquid.Errors tidyError :: FixSolution -> Error -> Error instance FromJSON Error instance ToJSON Error instance Exception [Error] instance Exception Error instance Show Error instance PPrint Error -- | This module contains the functions that convert from -- descriptions of symbols, names and types (over freshly parsed -- bare Strings), to representations connected to GHC vars, -- names, and types. The actual representations of bare and real -- (refinement) types are all in RefType -- they are different -- instances of RType module Language.Haskell.Liquid.Bare -- | The following is the overall type for specifications obtained -- from parsing the target source and dependent libraries data GhcSpec SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> GhcSpec -- | Asserted Reftypes eg. see include/Prelude.spec tySigs :: GhcSpec -> ![(Var, Located SpecType)] -- | Assumed Reftypes asmSigs :: GhcSpec -> ![(Var, Located SpecType)] -- | Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int -- | v = 1 + len(xs) } ctors :: GhcSpec -> ![(Var, Located SpecType)] -- | Measure Types eg. len :: [a] -> Int meas :: GhcSpec -> ![(Symbol, Located SpecType)] -- | Data Type Invariants invariants :: GhcSpec -> ![Located SpecType] -- | Data Type Invariant Aliases eg. forall a. {v: [a] | len(v) >= 0} ialiases :: GhcSpec -> ![(Located SpecType, Located SpecType)] -- | Predicated Data-Constructors e.g. see testsposMap.hs dconsP :: GhcSpec -> ![(DataCon, DataConP)] -- | Predicated Type-Constructors eg. see testsposMap.hs tconsP :: GhcSpec -> ![(TyCon, TyConP)] -- | List of Symbol free in spec and corresponding GHC var eg. -- (Cons, Cons#7uz) from testsposex1.hs freeSyms :: GhcSpec -> ![(Symbol, Var)] -- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as -- Set_set" from includeDataSet.spec tcEmbeds :: GhcSpec -> TCEmb TyCon -- | Qualifiers in Source/Spec files e.g testsposqualTest.hs qualifiers :: GhcSpec -> ![Qualifier] -- | Top-level Binders To Verify (empty means ALL binders) tgtVars :: GhcSpec -> ![Var] -- | Lexicographically ordered size witnesses for termination decr :: GhcSpec -> ![(Var, [Int])] -- | Lexicographically ordered expressions for termination texprs :: GhcSpec -> ![(Var, [Expr])] -- | Variables that should be checked in the environment they are used lvars :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking lazy :: GhcSpec -> !(HashSet Var) -- | Configuration Options config :: GhcSpec -> !Config -- | Names exported by the module being verified exports :: GhcSpec -> !NameSet measures :: GhcSpec -> [Measure SpecType DataCon] tyconEnv :: GhcSpec -> HashMap TyCon RTyCon makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> [(ModName, BareSpec)] -> IO GhcSpec instance Resolvable () instance Resolvable t => Resolvable (PVar t) instance Resolvable Predicate instance Resolvable Reft instance Resolvable (UReft Reft) instance Resolvable Sort instance Resolvable Symbol instance Resolvable LocSymbol instance Resolvable Expr instance Resolvable Pred instance Resolvable Qualifier instance Resolvable a => Resolvable [a] instance GhcLookup Name instance GhcLookup (Located Symbol) -- | This module contains the code that uses the inferred types to generate -- 1. HTMLized source with Inferred Types in mouseover annotations. 2. -- Annotations files (e.g. for vim/emacs) 3. JSON files for the web-demo -- etc. module Language.Haskell.Liquid.Annotate -- | output creates the pretty printed output mkOutput :: Config -> FixResult Error -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc -- | annotate actually renders the output to files annotate :: Config -> FilePath -> Output Doc -> IO () instance ToJSON AnnMap instance (Show k, ToJSON a) => ToJSON (Assoc k a) instance ToJSON AnnErrors instance ToJSON Loc instance ToJSON Annot1 instance ToJSON Status -- | This module contains all the code needed to output the result which is -- either: SAFE or WARNING with some reasonable error -- message when something goes wrong. All forms of errors/exceptions -- should go through here. The idea should be to report the error, the -- source position that causes it, generate a suitable .json file and -- then exit. module Language.Haskell.Liquid.CmdLine getOpts :: IO Config mkOpts :: Config -> IO Config -- | Updating options withPragmas :: Config -> FilePath -> [Located String] -> IO Config -- | Exit Function ----------------------------------------------------- exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc) -- | check subset of binders modified (+ dependencies) since last check diffcheck :: Config -> Bool instance Fixpoint (FixResult Error) instance Monoid SMTSolver instance Monoid Config module Language.Haskell.Liquid.GhcInterface getGhcInfo :: Config -> FilePath -> IO (Either ErrorResult GhcInfo) class CBVisitable a freeVars :: CBVisitable a => HashSet Var -> a -> [Var] readVars :: CBVisitable a => a -> [Var] letVars :: CBVisitable a => a -> [Var] literals :: CBVisitable a => a -> [Literal] instance Result SourceError instance PPrint TargetVars instance PPrint [CoreBind] instance Show GhcInfo instance PPrint GhcInfo instance PPrint GhcSpec instance NFData SrcSpan instance NFData Var instance CBVisitable AltCon instance CBVisitable (Alt Var) instance CBVisitable (Expr Var) instance CBVisitable CoreBind instance CBVisitable [CoreBind] -- | This module contains the code for generating "tags" for constraints -- based on their source, i.e. the top-level binders under which the -- constraint was generated. These tags are used by fixpoint to -- prioritize constraints by the "source-level" function. module Language.Haskell.Liquid.CTags -- | The TagKey is the top-level binder, and Tag is a -- singleton Int list type TagKey = Var type TagEnv = HashMap TagKey Tag defaultTag :: Tag makeTagEnv :: [CoreBind] -> TagEnv getTag :: TagKey -> TagEnv -> Tag memTagEnv :: TagKey -> TagEnv -> Bool module Language.Haskell.Liquid.Qualifier specificationQualifiers :: Int -> GhcInfo -> [Qualifier] -- | This module defines the representation of Subtyping and WF -- Constraints, and the code for syntax-directed constraint generation. module Language.Haskell.Liquid.Constraint data CGInfo CGInfo :: ![SubC] -> ![WfC] -> ![SubC] -> ![FixSubC] -> ![Bool] -> ![FixWfC] -> !FEnv -> !Integer -> !BindEnv -> !(AnnInfo (Annot SpecType)) -> !(HashMap TyCon RTyCon) -> ![Qualifier] -> ![(Var, [Int])] -> !(HashMap Var [Expr]) -> !(HashSet Var) -> !(HashSet Var) -> !(TCEmb TyCon) -> !(Kuts) -> ![(Symbol, Sort)] -> !Bool -> !Bool -> !Bool -> !Bool -> ![TError SpecType] -> !KVProf -> !Int -> CGInfo -- | subtyping constraints over RType hsCs :: CGInfo -> ![SubC] -- | wellformedness constraints over RType hsWfs :: CGInfo -> ![WfC] -- | additional stratum constrains for let bindings sCs :: CGInfo -> ![SubC] -- | subtyping over Sort (post-splitting) fixCs :: CGInfo -> ![FixSubC] -- | tracks constraints that come from let-bindings isBind :: CGInfo -> ![Bool] -- | wellformedness constraints over Sort (post-splitting) fixWfs :: CGInfo -> ![FixWfC] -- | ? global measures globals :: CGInfo -> !FEnv -- | counter for generating fresh KVars freshIndex :: CGInfo -> !Integer -- | set of environment binders binds :: CGInfo -> !BindEnv -- | source-position annotation map annotMap :: CGInfo -> !(AnnInfo (Annot SpecType)) -- | information about type-constructors tyConInfo :: CGInfo -> !(HashMap TyCon RTyCon) -- | ? qualifiers in source files specQuals :: CGInfo -> ![Qualifier] -- | ? FIX THIS specDecr :: CGInfo -> ![(Var, [Int])] -- | Terminating Metrics for Recursive functions termExprs :: CGInfo -> !(HashMap Var [Expr]) -- | Set of variables to ignore for termination checking specLVars :: CGInfo -> !(HashSet Var) -- | ? FIX THIS specLazy :: CGInfo -> !(HashSet Var) -- | primitive Sorts into which TyCons should be embedded tyConEmbed :: CGInfo -> !(TCEmb TyCon) -- | Fixpoint Kut variables (denoting "back-edges"/recursive KVars) kuts :: CGInfo -> !(Kuts) -- | ? FIX THIS lits :: CGInfo -> ![(Symbol, Sort)] -- | Check Termination (?) tcheck :: CGInfo -> !Bool -- | Check Strata (?) scheck :: CGInfo -> !Bool -- | Trust ghc auto generated bindings trustghc :: CGInfo -> !Bool -- | prune unsorted refinements pruneRefs :: CGInfo -> !Bool -- | Errors during coontraint generation logErrors :: CGInfo -> ![TError SpecType] -- | Profiling distribution of KVars kvProf :: CGInfo -> !KVProf -- | number of recursive functions seen (for benchmarks) recCount :: CGInfo -> !Int generateConstraints :: GhcInfo -> CGInfo cgInfoFInfo :: CGInfo -> FInfo Cinfo cgInfoFInfoBot :: CGInfo -> FInfo Cinfo cgInfoFInfoKvars :: CGInfo -> [Symbol] -> FInfo Cinfo instance Show a => Show (Template a) instance Functor Template instance NFData REnv instance NFData CGInfo instance NFData WfC instance NFData Type instance NFData RTyCon instance NFData Class instance NFData SubC instance NFData FEnv instance NFData CGEnv instance Show CoreExpr instance Freshable CG Integer instance PPrint CGInfo instance SubStratum SubC instance PPrint WfC instance PPrint SubC instance Show CGEnv instance PPrint CGEnv -- | This module contains the code for Incremental checking, which finds -- the part of a target file (the subset of the [CoreBind] that -- have been modified since it was last checked, as determined by a diff -- against a saved version of the file. module Language.Haskell.Liquid.DiffCheck -- | Main type of value returned for diff-check. data DiffCheck DC :: [CoreBind] -> !(Output Doc) -> DiffCheck newBinds :: DiffCheck -> [CoreBind] oldOutput :: DiffCheck -> !(Output Doc) -- | slice returns a subset of the [CoreBind] of the input -- target file which correspond to top-level binders whose code -- has changed and their transitive dependencies. slice :: FilePath -> [CoreBind] -> IO (Maybe DiffCheck) -- | thin returns a subset of the [CoreBind] given which -- correspond to those binders that depend on any of the Vars -- provided. thin :: [CoreBind] -> [Var] -> [CoreBind] -- | save creates an .saved version of the target file, -- which will be used to find what has changed the next time -- target is checked. saveResult :: FilePath -> Output Doc -> IO () instance Eq Def instance Ord Def instance FromJSON (Output Doc) instance ToJSON (Output Doc) instance FromJSON a => FromJSON (AnnInfo a) instance ToJSON a => ToJSON (AnnInfo a) instance (Eq k, Hashable k, FromJSON k, FromJSON v) => FromJSON (HashMap k v) instance (ToJSON k, ToJSON v) => ToJSON (HashMap k v) instance FromJSON Doc instance ToJSON Doc instance FromJSON (FixResult Error) instance ToJSON (FixResult Error) instance FromJSON SourcePos instance ToJSON SourcePos instance Functor Diff instance Show Def module Language.Haskell.Liquid.List transpose :: Int -> [[a]] -> [[a]] module Language.Haskell.Liquid.Foreign intCSize :: Int -> CSize cSizeInt :: CSize -> Int mkPtr :: Addr# -> Ptr b isNullPtr :: Ptr a -> Bool fpLen :: ForeignPtr a -> Int pLen :: Ptr a -> Int deref :: Ptr a -> a eqPtr :: Ptr a -> Ptr a -> Bool module Language.Haskell.Liquid.Prelude plus :: Int -> Int -> Int minus :: Int -> Int -> Int times :: Int -> Int -> Int eq :: Int -> Int -> Bool neq :: Int -> Int -> Bool leq :: Int -> Int -> Bool geq :: Int -> Int -> Bool lt :: Int -> Int -> Bool gt :: Int -> Int -> Bool liquidAssertB :: Bool -> Bool liquidAssert :: Bool -> a -> a liquidAssume :: Bool -> a -> a liquidAssumeB :: (a -> Bool) -> a -> a liquidError :: String -> a crash :: Bool -> a force :: t -> Bool choose :: Int -> Int isEven :: Int -> Bool isOdd :: Int -> Bool safeZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]