Language.Haskell.Liquid.Bare.Spec

Documentation

makeClasses :: ModName -> Config -> [Var] -> (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [((DataCon, DataConP), [(ModName, Var, Located SpecType)])]

makeQualifiers :: (ModName, Spec ty bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Qualifier]

makeHints :: [Var] -> Spec ty bndr -> BareM [(Var, [Int])]

makeLVar :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Var]

makeLazy :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Var]

makeHIMeas :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Located Var]

makeTExpr :: [Var] -> Spec ty bndr -> BareM [(Var, [Expr])]

makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var]

API: Bare Refinement Types ----------------------------------

makeAssertSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)]

makeAssumeSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)]

makeDefaultMethods :: [Var] -> [(ModName, Var, Located SpecType)] -> [(ModName, Var, Located SpecType)]

makeIAliases :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [(Located SpecType, Located SpecType)]

makeInvariants :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Located SpecType]

makeSpecDictionaries :: HashMap TyCon FTycon -> [Var] -> [(t, Spec BareType bndr)] -> GhcSpec -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) GhcSpec

makeBounds :: Eq a => a -> [Var] -> CoreProgram -> [(a, Spec BareType bndr)] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) ()

makeHBounds :: [Var] -> Spec ty bndr -> BareM [(Var, LocSymbol)]