| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Constraints
Contents
Description
This module contains the top-level QUERY data types and elements, including (Horn) implication & well-formedness constraints and sets.
- type FInfo a = GInfo SubC a
- type SInfo a = GInfo SimpC a
- data GInfo c a = FI {}
- data FInfoWithOpts a = FIO {}
- convertFormat :: Fixpoint a => FInfo a -> SInfo a
- type Solver a = Config -> FInfo a -> IO (Result (Integer, a))
- toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc
- writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO ()
- saveQuery :: Config -> FInfo a -> IO ()
- fi :: [SubC a] -> [WfC a] -> BindEnv -> SEnv Sort -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> Bool -> Bool -> [Triggered Expr] -> AxiomEnv -> [DataDecl] -> GInfo SubC a
- data WfC a
- isGWfc :: WfC a -> Bool
- updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a
- data SubC a
- type SubcId = Integer
- mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
- subcId :: TaggedC c a => c a -> SubcId
- sid :: TaggedC c a => c a -> Maybe Integer
- senv :: TaggedC c a => c a -> IBindEnv
- slhs :: SubC a -> SortedReft
- srhs :: SubC a -> SortedReft
- stag :: TaggedC c a => c a -> Tag
- subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
- wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
- data SimpC a = SimpC {}
- type Tag = [Int]
- class TaggedC c a where
- clhs :: TaggedC c a => BindEnv -> c a -> [(Symbol, SortedReft)]
- crhs :: TaggedC c a => c a -> Expr
- strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a
- addIds :: [SubC a] -> [(Integer, SubC a)]
- sinfo :: TaggedC c a => c a -> a
- shiftVV :: Reft -> Symbol -> Reft
- gwInfo :: WfC a -> GWInfo
- data GWInfo = GWInfo {}
- data Qualifier = Q {}
- trueQual :: Qualifier
- qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
- mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
- remakeQual :: Qualifier -> Qualifier
- type FixSolution = HashMap KVar Expr
- type GFixSolution = GFixSol Expr
- toGFixSol :: HashMap KVar (e, [e]) -> GFixSol e
- data Result a = Result {
- resStatus :: !(FixResult a)
- resSolution :: !FixSolution
- gresSolution :: !GFixSolution
- unsafe :: Result a
- isUnsafe :: Result a -> Bool
- safe :: Result a
- newtype Kuts = KS {}
- ksMember :: KVar -> Kuts -> Bool
- data HOInfo = HOI {}
- allowHO :: GInfo c a -> Bool
- allowHOquals :: GInfo c a -> Bool
- data AxiomEnv = AEnv {}
- data Equation = Equ {}
- data Rewrite = SMeasure {}
- getEqBody :: Equation -> Maybe Expr
- substVars :: [(Symbol, Int)] -> Sort -> Sort
Top-level Queries
Constructors
| FI | |
Fields
| |
Instances
| Functor c => Functor (GInfo c) Source # | |
| PTable (SInfo a) Source # | |
| Inputable (FInfo ()) Source # | |
| Elaborate (SInfo a) Source # | |
| Gradual (SInfo a) Source # | |
| (Eq (c a), Eq a) => Eq (GInfo c a) Source # | |
| (Show (c a), Show a, Fixpoint a) => Show (GInfo c a) Source # | |
| Generic (GInfo c a) Source # | |
| Monoid (GInfo c a) Source # | |
| (Binary (c a), Binary a) => Binary (GInfo c a) Source # | |
| (NFData (c a), NFData a) => NFData (GInfo c a) Source # | |
| SymConsts (c a) => SymConsts (GInfo c a) Source # | |
| Visitable (c a) => Visitable (GInfo c a) Source # | |
| (Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source # | |
| type Rep (GInfo c a) Source # | |
type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) Source #
Top level Solvers ----------------------------------------------------
Serializing
Constructing Queries
fi :: [SubC a] -> [WfC a] -> BindEnv -> SEnv Sort -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> Bool -> Bool -> [Triggered Expr] -> AxiomEnv -> [DataDecl] -> GInfo SubC a Source #
Constructing Queries
Constraints
Instances
| Functor WfC Source # | |
| Eq a => Eq (WfC a) Source # | |
| Fixpoint a => Show (WfC a) Source # | |
| Generic (WfC a) Source # | |
| Binary a => Binary (WfC a) Source # | |
| NFData a => NFData (WfC a) Source # | |
| Fixpoint a => PPrint (WfC a) Source # | |
| Fixpoint a => Fixpoint (WfC a) Source # | |
| Defunc (WfC a) Source # | |
| type Rep (WfC a) Source # | |
Instances
| Functor SubC Source # | |
| TaggedC SubC a Source # | |
| Eq a => Eq (SubC a) Source # | |
| Fixpoint a => Show (SubC a) Source # | |
| Generic (SubC a) Source # | |
| Binary a => Binary (SubC a) Source # | |
| NFData a => NFData (SubC a) Source # | |
| Fixpoint a => PPrint (SubC a) Source # | |
| (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # | |
| Fixpoint a => Fixpoint (SubC a) Source # | |
| Inputable (FInfo ()) Source # | |
| SymConsts (SubC a) Source # | |
| Visitable (SubC a) Source # | |
| type Rep (SubC a) Source # | |
mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a Source #
slhs :: SubC a -> SortedReft Source #
srhs :: SubC a -> SortedReft Source #
subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a] Source #
wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a] Source #
"Smart Constructors" for Constraints ---------------------------------
Constructors
| SimpC | |
Instances
| Functor SimpC Source # | |
| TaggedC SimpC a Source # | |
| Fixpoint a => Show (SimpC a) Source # | |
| Generic (SimpC a) Source # | |
| Binary a => Binary (SimpC a) Source # | |
| NFData a => NFData (SimpC a) Source # | |
| PTable (SInfo a) Source # | |
| Fixpoint a => PPrint (SimpC a) Source # | |
| Fixpoint a => Fixpoint (SimpC a) Source # | |
| SymConsts (SimpC a) Source # | |
| Visitable (SimpC a) Source # | |
| Elaborate (SInfo a) Source # | |
| Elaborate (SimpC a) Source # | |
| Gradual (SInfo a) Source # | |
| Gradual (SimpC a) Source # | |
| Defunc (SimpC a) Source # | |
| type Rep (SimpC a) Source # | |
Constraints ---------------------------------------------------------------
Accessing Constraints
Qualifiers
Qualifiers ----------------------------------------------------------------
Constructors
| Q | |
mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier Source #
constructing qualifiers
remakeQual :: Qualifier -> Qualifier Source #
Results
type GFixSolution = GFixSol Expr Source #
Solutions and Results
Constructors
| Result | |
Fields
| |
Cut KVars
Constraint Cut Sets -------------------------------------------------------
Higher Order Logic
Constructors
| HOI | |
allowHOquals :: GInfo c a -> Bool Source #
Axioms
Axiom Instantiation Information --------------------------------------
Constructors
| AEnv | |