| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types
Contents
- Top level serialization
- Rendering
- Symbols
- Creating Symbols
- Embedding to Fixpoint Types
- Expressions and Predicates
- Generalizing Embedding with Typeclasses
- Constraints and Solutions
- Environments
- Refinements
- Constructing Refinements
- Substitutions
- Visitors
- Functions on
Result - Cut KVars
- Qualifiers
- FQ Definitions
- Located Values
Description
This module contains the data types, operations and serialization functions for representing Fixpoint's implication (i.e. subtyping) and well-formedness constraints in Haskell. The actual constraint solving is done by the `fixpoint.native` which is written in Ocaml.
- class Fixpoint a where
- toFixpoint :: FInfo a -> Doc
- data FInfo a = FI {}
- showFix :: Fixpoint a => a -> String
- traceFix :: Fixpoint a => String -> a -> a
- resultDoc :: (Ord a, Fixpoint a) => FixResult a -> Doc
- data Symbol
- anfPrefix :: Symbol
- tempPrefix :: Symbol
- vv :: Maybe Integer -> Symbol
- intKvar :: Integer -> Symbol
- symChars :: [Char]
- isNonSymbol :: Symbol -> Bool
- nonSymbol :: Symbol
- isNontrivialVV :: Symbol -> Bool
- symbolText :: Symbol -> Text
- symbolString :: Symbol -> String
- dummySymbol :: Symbol
- intSymbol :: Show a => Symbol -> a -> Symbol
- tempSymbol :: Symbol -> Integer -> Symbol
- qualifySymbol :: Symbol -> Symbol -> Symbol
- suffixSymbol :: Symbol -> Text -> Symbol
- data Sort
- data FTycon
- type TCEmb a = HashMap a FTycon
- intFTyCon :: FTycon
- boolFTyCon :: FTycon
- realFTyCon :: FTycon
- strFTyCon :: FTycon
- propFTyCon :: FTycon
- appFTyCon :: FTycon
- fTyconSymbol :: FTycon -> LocSymbol
- symbolFTycon :: LocSymbol -> FTycon
- fApp :: Either FTycon Sort -> [Sort] -> Sort
- fObj :: LocSymbol -> Sort
- data SymConst = SL !Text
- data Constant
- data Bop
- data Brel
- data Expr
- data Pred
- eVar :: Symbolic a => a -> Expr
- eProp :: Symbolic a => a -> Pred
- pAnd :: [Pred] -> Pred
- pOr :: [Pred] -> Pred
- pIte :: Pred -> Pred -> Pred -> Pred
- isTautoPred :: Pred -> Bool
- symConstLits :: FInfo a -> [(Symbol, Sort)]
- class Symbolic a where
- class Expression a where
- class Predicate a where
- data SubC a
- data WfC a
- sid :: SubC a -> Maybe Integer
- 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
- 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
- emptySEnv :: SEnv a
- toListSEnv :: SEnv a -> [(Symbol, a)]
- fromListSEnv :: [(Symbol, a)] -> SEnv a
- mapSEnv :: (a1 -> a) -> SEnv a1 -> SEnv a
- mapSEnvWithKey :: ((Symbol, a1) -> (Symbol, 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
- emptyIBindEnv :: IBindEnv
- insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
- deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
- data BindEnv
- rawBindEnv :: [(BindId, Symbol, SortedReft)] -> BindEnv
- insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
- emptyBindEnv :: BindEnv
- mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
- data Refa
- data SortedReft = RR {}
- newtype Reft = Reft (Symbol, [Refa])
- class (Monoid r, Subable r) => Reftable r where
- trueSortedReft :: Sort -> SortedReft
- trueRefa :: Refa
- trueReft :: Reft
- exprReft :: Expression a => a -> Reft
- notExprReft :: Expression a => a -> Reft
- uexprReft :: 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
- mkSubst :: [(Symbol, Expr)] -> 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 {}
- data Def a
- data Located a = Loc {}
- type LocSymbol = Located Symbol
- type LocText = Located Text
- dummyLoc :: a -> Located a
- dummyPos :: String -> SourcePos
- dummyName :: Symbol
- isDummy :: Symbolic a => a -> Bool
Top level serialization
Minimal complete definition
Instances
| Fixpoint Double | |
| Fixpoint Int | |
| Fixpoint Integer | |
| Fixpoint Text | |
| Fixpoint SourcePos | |
| Fixpoint Symbol | |
| Fixpoint Qualifier | |
| Fixpoint Subst | |
| Fixpoint BindEnv | |
| Fixpoint IBindEnv | |
| Fixpoint FEnv | |
| Fixpoint SortedReft | |
| Fixpoint Reft | |
| Fixpoint Refa | |
| Fixpoint Pred | |
| Fixpoint Expr | |
| Fixpoint Bop | |
| Fixpoint Brel | |
| Fixpoint Constant | |
| Fixpoint SymConst | |
| Fixpoint Sort | |
| Fixpoint FTycon | |
| Fixpoint Kuts | |
| Fixpoint Error | |
| Fixpoint a => Fixpoint [a] | |
| Fixpoint a => Fixpoint (Maybe a) | |
| (Eq a, Hashable a, Fixpoint a) => Fixpoint (HashSet a) | |
| Fixpoint a => Fixpoint (Located a) | |
| (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) | |
| Fixpoint (WfC a) | |
| Fixpoint (SubC a) | |
| Fixpoint a => Fixpoint (SEnv a) | |
| (Fixpoint a, Fixpoint b) => Fixpoint (a, b) |
toFixpoint :: FInfo a -> Doc Source
Constructors
| FI | |
Rendering
Symbols
Instances
| Eq Symbol | |
| Data Symbol | |
| Ord Symbol | |
| Show Symbol | |
| IsString Symbol | |
| Generic Symbol | |
| Monoid Symbol | |
| NFData Symbol | |
| Hashable Symbol | |
| Symbolic Symbol | |
| Subable Symbol | |
| Predicate Symbol | |
| Expression Symbol | The symbol may be an encoding of a SymConst. |
| Fixpoint Symbol | |
| PPrint Symbol | |
| SMTLIB2 Symbol | |
| SMTLIB2 LocSymbol | |
| Inputable Symbol | |
| Typeable * Symbol | |
| Inputable (FixResult Integer, FixSolution) | |
| type Rep Symbol |
isNonSymbol :: Symbol -> Bool Source
isNontrivialVV :: Symbol -> Bool Source
symbolText :: Symbol -> Text Source
symbolString :: Symbol -> String Source
Creating Symbols
tempSymbol :: Symbol -> Integer -> Symbol Source
qualifySymbol :: Symbol -> Symbol -> Symbol Source
suffixSymbol :: Symbol -> Text -> Symbol Source
Embedding to Fixpoint Types
fTyconSymbol :: FTycon -> LocSymbol Source
symbolFTycon :: LocSymbol -> FTycon Source
Expressions and Predicates
Uninterpreted constants that are embedded as "constant symbol : Str"
isTautoPred :: Pred -> Bool Source
symConstLits :: FInfo a -> [(Symbol, Sort)] Source
String Constants -----------------------------------------
Generalizing Embedding with Typeclasses
Values that can be viewed as Symbols
class Expression a where Source
Generalizing Symbol, Expression, Predicate into Classes -----------
Values that can be viewed as Expressions
Instances
| Expression Int | |
| Expression Integer | |
| Expression Text | |
| Expression Symbol | The symbol may be an encoding of a SymConst. |
| Expression Expr | |
| Expression a => Expression (Located a) |
Constraints and Solutions
subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a] Source
type FixSolution = HashMap Symbol Pred Source
trueSubCKvar :: Symbol -> a -> [SubC a] Source
removeLhsKvars :: SubC a -> [Symbol] -> SubC a Source
Environments
toListSEnv :: SEnv a -> [(Symbol, a)] Source
fromListSEnv :: [(Symbol, a)] -> SEnv a Source
insertSEnv :: Symbol -> a -> SEnv a -> SEnv a Source
deleteSEnv :: Symbol -> SEnv a -> SEnv a Source
memberSEnv :: Symbol -> SEnv a -> Bool Source
lookupSEnv :: Symbol -> SEnv v -> Maybe v Source
intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a Source
filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a Source
lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a Source
type FEnv = SEnv SortedReft Source
insertFEnv :: Symbol -> a -> SEnv a -> SEnv a Source
emptyIBindEnv :: IBindEnv Source
Functions for Indexed Bind Environment
insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv Source
deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv Source
rawBindEnv :: [(BindId, Symbol, SortedReft)] -> BindEnv Source
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv) Source
Functions for Global Binder Environment
mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv Source
Refinements
data SortedReft Source
class (Monoid r, Subable r) => Reftable r where Source
A Class Predicates for Valid Refinements Types ---------------------
Instances
Constructing Refinements
trueSortedReft :: Sort -> SortedReft Source
exprReft :: Expression a => a -> Reft Source
notExprReft :: Expression a => a -> Reft Source
uexprReft :: Expression a => a -> Reft Source
symbolReft :: Symbolic a => a -> Reft Source
isTautoReft :: Reft -> Bool Source
isSingletonReft :: Reft -> Maybe Expr Source
flattenRefas :: [Refa] -> [Refa] Source
squishRefas :: [Refa] -> [Refa] Source
Substitutions
substExcept :: Subst -> [Symbol] -> Subst Source
Visitors
Functions on Result
colorResult :: FixResult t -> Moods Source
Cut KVars
Qualifiers
Constructors
| Q | |
FQ Definitions
Entities in Query File --------------------------------------------
Located Values
Located Values ---------------------------------------------------------
Instances
| Functor Located | |
| Foldable Located | |
| Traversable Located | |
| SMTLIB2 LocSymbol | |
| Eq a => Eq (Located a) | |
| Data a => Data (Located a) | |
| Ord a => Ord (Located a) | |
| Show a => Show (Located a) | |
| IsString a => IsString (Located a) | |
| Generic (Located a) | |
| NFData a => NFData (Located a) | |
| Hashable a => Hashable (Located a) | |
| Symbolic a => Symbolic (Located a) | |
| Subable a => Subable (Located a) | |
| Expression a => Expression (Located a) | |
| Fixpoint a => Fixpoint (Located a) | |
| PPrint a => PPrint (Located a) | |
| Typeable (* -> *) Located | |
| type Rep (Located a) |