Safe Haskell | None |
---|---|
Language | Haskell98 |
- Top level serialization
- Rendering
- Symbols
- Creating Symbols
- Embedding to Fixpoint Types
- Expressions and Predicates
- Generalizing Embedding with Typeclasses
- Constraints
- Accessing Constraints
- Solutions
- Environments
- Refinements
- Constructing Refinements
- Substitutions
- Functions on
Result
- Cut KVars
- Qualifiers
- FQ Definitions
- Located Values
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
- newtype KVar = KV {}
- anfPrefix :: Symbol
- tempPrefix :: Symbol
- vv :: Maybe Integer -> Symbol
- vv_ :: Symbol
- intKvar :: Integer -> KVar
- 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
- listFTyCon :: FTycon
- appFTyCon :: FTycon
- fTyconSymbol :: FTycon -> Located Symbol
- symbolFTycon :: LocSymbol -> FTycon
- strSort :: Sort
- fApp :: Either FTycon Sort -> [Sort] -> Sort
- fObj :: LocSymbol -> Sort
- isListTC :: FTycon -> Bool
- isFAppTyTC :: FTycon -> Bool
- 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 WfC a = WfC {}
- data SubC a
- sid :: SubC a -> Maybe Integer
- sgrd :: SubC a -> Pred
- senv :: SubC a -> IBindEnv
- slhs :: SubC a -> SortedReft
- srhs :: SubC a -> SortedReft
- 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]
- envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
- addIds :: [SubC a] -> [(Integer, SubC a)]
- sinfo :: SubC a -> a
- trueSubCKvar :: KVar -> a -> [SubC a]
- removeLhsKvars :: t -> t1 -> t2
- type Result a = (FixResult (SubC a), HashMap KVar Pred)
- data FixResult a
- type FixSolution = HashMap KVar Pred
- data SEnv a
- data SESearch a
- emptySEnv :: SEnv a
- toListSEnv :: SEnv a -> [(Symbol, a)]
- fromListSEnv :: [(Symbol, a)] -> 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
- type BindMap a = HashMap BindId a
- emptyIBindEnv :: IBindEnv
- insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
- deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
- elemsIBindEnv :: IBindEnv -> [BindId]
- data BindEnv
- insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
- emptyBindEnv :: BindEnv
- lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
- mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
- bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
- bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]
- unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
- newtype Refa = Refa {}
- data SortedReft = RR {}
- newtype Reft = Reft (Symbol, Refa)
- class (Monoid r, Subable r) => Reftable r where
- refa :: [Pred] -> Refa
- reft :: Symbol -> Pred -> Reft
- 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
- usymbolReft :: Symbolic a => a -> Reft
- propReft :: Predicate a => a -> Reft
- predReft :: Predicate a => a -> Reft
- reftPred :: Reft -> Pred
- reftBind :: Reft -> Symbol
- isFunctionSortedReft :: SortedReft -> Bool
- functionSort :: Sort -> Maybe (Int, [Sort], Sort)
- isNonTrivial :: Reftable r => r -> Bool
- isSingletonReft :: Reft -> Maybe Expr
- isEVar :: Expr -> Bool
- isFalse :: Falseable a => a -> Bool
- flattenRefas :: [Refa] -> [Refa]
- squishRefas :: [Refa] -> [Refa]
- conjuncts :: Pred -> [Pred]
- shiftVV :: Reft -> Symbol -> Reft
- mapPredReft :: (Pred -> Pred) -> Reft -> Reft
- newtype Subst = Su [(Symbol, Expr)]
- class Subable a where
- mkSubst :: [(Symbol, Expr)] -> Subst
- isEmptySubst :: Subst -> Bool
- substExcept :: Subst -> [Symbol] -> Subst
- substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
- subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a
- sortSubst :: HashMap Symbol Sort -> Sort -> Sort
- targetSubstSyms :: Subst -> [Symbol]
- colorResult :: FixResult t -> Moods
- newtype Kuts = KS {}
- ksEmpty :: Kuts
- ksUnion :: [KVar] -> 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
Fixpoint Double | |
Fixpoint Int | |
Fixpoint Integer | |
Fixpoint Text | |
Fixpoint SourcePos | |
Fixpoint Symbol | |
Fixpoint Qualifier | |
Fixpoint Subst | |
Fixpoint BindEnv | |
Fixpoint IBindEnv | |
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 KVar | |
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
Rendering
Symbols
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 | |
Solvable (Symbol, SortedReft) | |
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 -> Located Symbol Source
symbolFTycon :: LocSymbol -> FTycon Source
isFAppTyTC :: FTycon -> Bool Source
Expressions and Predicates
Uninterpreted constants that are embedded as "constant symbol : Str"
Eq SymConst | |
Data SymConst | |
Ord SymConst | |
Show SymConst | |
Generic SymConst | |
NFData SymConst | |
Hashable SymConst | |
Symbolic SymConst | Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq. |
Fixpoint SymConst | |
PPrint SymConst | |
SMTLIB2 SymConst | |
Typeable * SymConst | |
type Rep SymConst |
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 Constants
Values that can be viewed as Expressions
Expression Int | |
Expression Integer | |
Expression Text | |
Expression Symbol | The symbol may be an encoding of a SymConst. |
Expression Expr | |
Expression Bv | Construct an |
Expression a => Expression (Located a) |
Constraints
slhs :: SubC a -> SortedReft Source
srhs :: SubC a -> SortedReft Source
subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a] Source
Accessing Constraints
trueSubCKvar :: KVar -> a -> [SubC a] Source
removeLhsKvars :: t -> t1 -> t2 Source
Solutions
type FixSolution = HashMap KVar Pred Source
Environments
toListSEnv :: SEnv a -> [(Symbol, a)] Source
Environments ---------------------------------------------
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
elemsIBindEnv :: IBindEnv -> [BindId] Source
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv) Source
Functions for Global Binder Environment
lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft) Source
mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv Source
bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv Source
bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)] Source
unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv Source
Refinements
data SortedReft Source
class (Monoid r, Subable r) => Reftable r where Source
A Class Predicates for Valid Refinements Types ---------------------
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
usymbolReft :: Symbolic a => a -> Reft Source
isNonTrivial :: Reftable r => r -> Bool Source
isSingletonReft :: Reft -> Maybe Expr Source
flattenRefas :: [Refa] -> [Refa] Source
squishRefas :: [Refa] -> [Refa] Source
Substitutions
isEmptySubst :: Subst -> Bool Source
substExcept :: Subst -> [Symbol] -> Subst Source
targetSubstSyms :: Subst -> [Symbol] Source
Functions on Result
colorResult :: FixResult t -> Moods Source
Cut KVars
Qualifiers
FQ Definitions
Entities in Query File --------------------------------------------
Located Values
Located Values ---------------------------------------------------------
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) |