Language.Haskell.Liquid.Fixpoint

Contents

• Top level serialization
• Embedding to Fixpoint Types
• Symbols
• Expressions and Predicates
• Constraints and Solutions
• Environments
• Refinements
• Substitutions
• Visitors
• Functions on Result
• Cut KVars
• Checking Well-Formedness

Description

Synopsis

• toFixpoint :: FInfo a -> SDoc
• class Fixpoint a where
  • toFix :: a -> SDoc
  • simplify :: a -> a
• data Sort
  • = FInt
  • | FNum
  • | FObj Symbol
  • | FVar !Int
  • | FFunc !Int ![Sort]
  • | FApp FTycon [Sort]
• data FTycon
• type TCEmb a = HashMap a FTycon
• stringFTycon :: String -> FTycon
• intFTyCon :: FTycon
• boolFTyCon :: FTycon
• predFTyCon :: FTycon
• typeSort :: TCEmb TyCon -> Type -> Sort
• typeUniqueSymbol :: Type -> Symbol
• data Symbol = S !String
• anfPrefix :: [Char]
• tempPrefix :: [Char]
• vv :: Maybe Integer -> Symbol
• intKvar :: Integer -> Symbol
• symChars :: [Char]
• isNonSymbol :: Symbol -> Bool
• nonSymbol :: Symbol
• dummySymbol :: Symbol
• intSymbol :: Show a => [Char] -> a -> Symbol
• tempSymbol :: String -> Integer -> Symbol
• qualifySymbol :: [Char] -> Symbol -> Symbol
• stringSymbol :: String -> Symbol
• symbolString :: Symbol -> String
• stringSymbolRaw :: String -> Symbol
• isNontrivialVV :: Symbol -> Bool
• data Constant = I !Integer
• data Bop
  • = Plus
  • | Minus
  • | Times
  • | Div
  • | Mod
• data Brel
  • = Eq
  • | Ne
  • | Gt
  • | Ge
  • | Lt
  • | Le
• data Expr
  • = ECon !Constant
  • | EVar !Symbol
  • | ELit !Symbol !Sort
  • | EApp !Symbol ![Expr]
  • | EBin !Bop !Expr !Expr
  • | EIte !Pred !Expr !Expr
  • | ECst !Expr !Sort
  • | EBot
• data Pred
  • = PTrue
  • | PFalse
  • | PAnd ![Pred]
  • | POr ![Pred]
  • | PNot !Pred
  • | PImp !Pred !Pred
  • | PIff !Pred !Pred
  • | PBexp !Expr
  • | PAtom !Brel !Expr !Expr
  • | PAll ![(Symbol, Sort)] !Pred
  • | PTop
• pAnd :: [Pred] -> Pred
• pOr :: [Pred] -> Pred
• pIte :: Pred -> Pred -> Pred -> Pred
• pApp :: Symbol -> [Expr] -> Pred
• isTautoPred :: Pred -> Bool
• data SubC a
• data WfC a
• subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
• wfC :: IBindEnv -> SortedReft -> Maybe Integer -> a -> WfC a
• type Tag = [Int]
• data FixResult a
  • = Crash [a] String
  • | Safe
  • | Unsafe ![a]
  • | UnknownError
• type FixSolution = HashMap Symbol Pred
• data FInfo a = FI {
  • cs :: ![SubC a]
  • ws :: ![WfC a]
  • bs :: !BindEnv
  • gs :: !FEnv
  • lits :: ![(Symbol, Sort)]
  • kuts :: Kuts
  }
• addIds :: [SubC a] -> [(Integer, SubC a)]
• sinfo :: SubC a -> a
• data SEnv a
• emptySEnv :: SEnv a
• fromListSEnv :: [(Symbol, a)] -> SEnv a
• insertSEnv :: Symbol -> a -> SEnv a -> SEnv a
• deleteSEnv :: Symbol -> SEnv a -> SEnv a
• memberSEnv :: Symbol -> SEnv a -> Bool
• lookupSEnv :: Symbol -> SEnv v -> Maybe v
• type FEnv = SEnv SortedReft
• insertFEnv :: Symbol -> a -> SEnv a -> SEnv a
• data IBindEnv
• type BindId = Int
• insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
• deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
• emptyIBindEnv :: IBindEnv
• data BindEnv
• insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (Int, BindEnv)
• emptyBindEnv :: BindEnv
• data Refa
  • = RConc !Pred
  • | RKvar !Symbol !Subst
• data SortedReft = RR {
  • sr_sort :: !Sort
  • sr_reft :: !Reft
  }
• newtype Reft = Reft (Symbol, [Refa])
• trueSortedReft :: Sort -> SortedReft
• trueRefa :: Refa
• exprReft :: Expr -> Reft
• notExprReft :: Expr -> Reft
• symbolReft :: Symbol -> Reft
• isFunctionSortedReft :: SortedReft -> Bool
• isNonTrivialSortedReft :: SortedReft -> Bool
• isTautoReft :: Reft -> Bool
• isSingletonReft :: Reft -> Maybe Expr
• isEVar :: Expr -> Bool
• flattenRefas :: [Refa] -> [Refa]
• shiftVV :: Reft -> Symbol -> Reft
• ppr_reft :: Reft -> SDoc -> SDoc
• ppr_reft_pred :: Reft -> SDoc
• data Subst
• class Subable a where
  • syms :: a -> [Symbol]
  • substa :: (Symbol -> Symbol) -> a -> a
  • substf :: (Symbol -> Expr) -> a -> a
  • subst :: Subst -> a -> a
  • subst1 :: a -> (Symbol, Expr) -> a
• emptySubst :: Subst
• mkSubst :: [(Symbol, Expr)] -> Subst
• catSubst :: Subst -> Subst -> Subst
• substExcept :: Subst -> [Symbol] -> Subst
• substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
• subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a
• reftKVars :: Reft -> [Symbol]
• colorResult :: FixResult t -> Moods
• newtype Kuts = KS (HashSet Symbol)
• ksEmpty :: Kuts
• ksUnion :: [Symbol] -> Kuts -> Kuts
• checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe SDoc

Top level serialization

Embedding to Fixpoint Types

Symbols

Expressions and Predicates

Constraints and Solutions

Environments

Refinements

Substitutions

Visitors

Functions on Result

Cut KVars

Checking Well-Formedness