Language.Fixpoint.Types

Contents

• Top level serialization
• Rendering
• Embedding to Fixpoint Types
• Symbols
• Creating Symbols
• Expressions and Predicates
• Generalizing Embedding with Typeclasses
• Constraints and Solutions
• Environments
• Refinements
• Constructing Refinements
• Substitutions
• Visitors
• Functions on Result
• Cut KVars
• Qualifiers

Description

Synopsis

• class Fixpoint a where
  • toFix :: a -> Doc
  • simplify :: a -> a
• toFixpoint :: FInfo a -> Doc
• data FInfo a = FI {
  • cm :: HashMap Integer (SubC a)
  • ws :: ![WfC a]
  • bs :: !BindEnv
  • gs :: !FEnv
  • lits :: ![(Symbol, Sort)]
  • kuts :: Kuts
  • quals :: ![Qualifier]
  }
• showFix :: Fixpoint a => a -> String
• traceFix :: Fixpoint a => String -> a -> a
• resultDoc :: (Ord a, Fixpoint a) => FixResult a -> Doc
• data Sort
  • = FInt
  • | FNum
  • | FObj Symbol
  • | FVar !Int
  • | FFunc !Int ![Sort]
  • | FApp FTycon [Sort]
• data FTycon
• type TCEmb a = HashMap a FTycon
• intFTyCon :: FTycon
• boolFTyCon :: FTycon
• strFTyCon :: FTycon
• propFTyCon :: FTycon
• stringFTycon :: String -> FTycon
• fTyconString :: FTycon -> String
• data Symbol = S !String
• anfPrefix :: [Char]
• tempPrefix :: [Char]
• vv :: Maybe Integer -> Symbol
• intKvar :: Integer -> Symbol
• symChars :: [Char]
• isNonSymbol :: Symbol -> Bool
• nonSymbol :: Symbol
• isNontrivialVV :: Symbol -> Bool
• stringSymbol :: String -> Symbol
• symbolString :: Symbol -> String
• dummySymbol :: Symbol
• intSymbol :: Show a => [Char] -> a -> Symbol
• tempSymbol :: String -> Integer -> Symbol
• qualifySymbol :: [Char] -> Symbol -> Symbol
• stringSymbolRaw :: String -> Symbol
• suffixSymbol :: Symbol -> [Char] -> Symbol
• data SymConst = SL !String
• data Constant = I !Integer
• data Bop
  • = Plus
  • | Minus
  • | Times
  • | Div
  • | Mod
• data Brel
  • = Eq
  • | Ne
  • | Gt
  • | Ge
  • | Lt
  • | Le
• data Expr
  • = ESym !SymConst
  • | 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
• eVar :: Symbolic a => a -> Expr
• eProp :: Symbolic a => a -> Pred
• pAnd :: [Pred] -> Pred
• pOr :: [Pred] -> Pred
• pIte :: Pred -> Pred -> Pred -> Pred
• isTautoPred :: Pred -> Bool
• class Symbolic a where
  • symbol :: a -> Symbol
• class Expression a where
  • expr :: a -> Expr
• class Predicate a where
  • prop :: a -> Pred
• data SubC a
• data WfC a
• subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
• lhsCs :: SubC a -> Reft
• rhsCs :: SubC a -> Reft
• wfC :: IBindEnv -> SortedReft -> Maybe Integer -> a -> WfC a
• type Tag = [Int]
• data FixResult a
  • = Crash [a] String
  • | Safe
  • | Unsafe ![a]
  • | UnknownError !Doc
• type FixSolution = HashMap Symbol Pred
• addIds :: [SubC a] -> [(Integer, SubC a)]
• sinfo :: SubC a -> a
• trueSubCKvar :: Symbol -> a -> SubC a
• removeLhsKvars :: SubC a -> [Symbol] -> SubC a
• data SEnv a
• data SESearch a
  • = Found a
  • | Alts [Symbol]
• emptySEnv :: SEnv a
• toListSEnv :: SEnv a -> [(Symbol, a)]
• fromListSEnv :: [(Symbol, a)] -> SEnv a
• mapSEnv :: (a1 -> a) -> SEnv a1 -> 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
• intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
• filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a
• lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a
• 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 -> (BindId, BindEnv)
• emptyBindEnv :: BindEnv
• data Refa
  • = RConc !Pred
  • | RKvar !Symbol !Subst
• data SortedReft = RR {
  • sr_sort :: !Sort
  • sr_reft :: !Reft
  }
• newtype Reft = Reft (Symbol, [Refa])
• class (Monoid r, Subable r) => Reftable r where
  • isTauto :: r -> Bool
  • ppTy :: r -> Doc -> Doc
  • top :: r
  • bot :: r -> r
  • meet :: r -> r -> r
  • toReft :: r -> Reft
  • params :: r -> [Symbol]
• trueSortedReft :: Sort -> SortedReft
• trueRefa :: Refa
• exprReft :: Expression a => a -> Reft
• notExprReft :: Expression a => a -> Reft
• symbolReft :: Symbolic a => a -> Reft
• propReft :: Predicate a => a -> Reft
• predReft :: Predicate a => a -> Reft
• isFunctionSortedReft :: SortedReft -> Bool
• isNonTrivialSortedReft :: SortedReft -> Bool
• isTautoReft :: Reft -> Bool
• isSingletonReft :: Reft -> Maybe Expr
• isEVar :: Expr -> Bool
• isFalse :: Falseable a => a -> Bool
• flattenRefas :: [Refa] -> [Refa]
• squishRefas :: [Refa] -> [Refa]
• shiftVV :: Reft -> Symbol -> Reft
• 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
• sortSubst :: HashMap Symbol Sort -> Sort -> Sort
• reftKVars :: Reft -> [Symbol]
• colorResult :: FixResult t -> Moods
• newtype Kuts = KS (HashSet Symbol)
• ksEmpty :: Kuts
• ksUnion :: [Symbol] -> Kuts -> Kuts
• data Qualifier = Q {
  • q_name :: String
  • q_params :: [(Symbol, Sort)]
  • q_body :: Pred
  }

Top level serialization

Rendering

Embedding to Fixpoint Types

Symbols

Creating Symbols

Expressions and Predicates

Generalizing Embedding with Typeclasses

Constraints and Solutions

Environments

Refinements

Constructing Refinements

Substitutions

Visitors

Functions on Result

Cut KVars

Qualifiers