| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Constraints
Description
This module contains the top-level QUERY data types and elements, including (Horn) implication & well-formedness constraints and sets.
Synopsis
- type FInfo a = GInfo SubC a
- type SInfo a = GInfo SimpC a
- data GInfo c a = FI {
- cm :: !(HashMap SubcId (c a))
- ws :: !(HashMap KVar (WfC a))
- bs :: !(BindEnv a)
- ebinds :: ![BindId]
- gLits :: !(SEnv Sort)
- dLits :: !(SEnv Sort)
- kuts :: !Kuts
- quals :: ![Qualifier]
- bindInfo :: !(HashMap BindId a)
- ddecls :: ![DataDecl]
- hoInfo :: !HOInfo
- asserts :: ![Triggered Expr]
- ae :: AxiomEnv
- lrws :: LocalRewritesEnv
- data FInfoWithOpts a = FIO {}
- convertFormat :: Fixpoint a => FInfo a -> SInfo a
- sinfoToFInfo :: SInfo a -> FInfo 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 :: Fixpoint a => Config -> FInfo a -> IO ()
- fi :: [SubC a] -> [WfC a] -> BindEnv a -> SEnv Sort -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> Bool -> Bool -> [Triggered Expr] -> AxiomEnv -> [DataDecl] -> [BindId] -> 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
- updateSEnv :: TaggedC c a => c a -> (IBindEnv -> IBindEnv) -> c a
- 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
- clhs :: TaggedC c a => BindEnv a -> c a -> [(Symbol, SortedReft)]
- crhs :: TaggedC c a => c a -> Expr
- strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a
- strengthenBinds :: SInfo a -> HashMap BindId 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 {}
- type Qualifier = QualifierV Symbol
- data QualifierV v = Q {}
- data QualParam = QP {}
- data QualPattern
- trueQual :: Qualifier
- qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
- mkQual :: Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
- remakeQual :: Qualifier -> Qualifier
- mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
- qualBinds :: Qualifier -> [(Symbol, Sort)]
- 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
- resNonCutsSolution :: !FixSolution
- gresSolution :: !GFixSolution
- unsafe :: Result a
- isUnsafe :: Result a -> Bool
- isSafe :: 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
- cfgHoInfo :: Config -> HOInfo
- data AxiomEnv = AEnv {
- aenvEqs :: ![Equation]
- aenvSimpl :: ![Rewrite]
- aenvExpand :: HashMap SubcId Bool
- aenvAutoRW :: HashMap SubcId [AutoRewrite]
- type Equation = EquationV Symbol
- data EquationV v = Equ {}
- mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
- data Rewrite = SMeasure {}
- data AutoRewrite = AutoRewrite {}
- dedupAutoRewrites :: HashMap SubcId [AutoRewrite] -> [AutoRewrite]
- newtype LocalRewritesEnv = LocalRewritesMap (HashMap BindId LocalRewrites)
- newtype LocalRewrites = LocalRewrites (HashMap Symbol Expr)
- lookupRewrite :: Symbol -> LocalRewrites -> Maybe Expr
- lookupLocalRewrites :: BindId -> LocalRewritesEnv -> Maybe LocalRewrites
- insertRewrites :: BindId -> LocalRewrites -> LocalRewritesEnv -> LocalRewritesEnv
- substVars :: [(Symbol, Int)] -> Sort -> Sort
- sortVars :: Sort -> [Symbol]
- gSorts :: [Sort] -> [Sort]
Top-level Queries
Constructors
| FI | |
Fields
| |
Instances
data FInfoWithOpts a Source #
Top-level Queries
Instances
| Inputable (FInfoWithOpts ()) Source # | |
Defined in Language.Fixpoint.Parse | |
sinfoToFInfo :: SInfo a -> FInfo 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 a -> SEnv Sort -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> Bool -> Bool -> [Triggered Expr] -> AxiomEnv -> [DataDecl] -> [BindId] -> GInfo SubC a Source #
Constructing Queries
Constraints
Instances
Instances
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
Constraints ---------------------------------------------------------------
Instances
| TaggedC SimpC a Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| TaggedC SubC a Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
Accessing Constraints
Instances
| Generic GWInfo Source # | |
| NFData GWInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Eq GWInfo Source # | |
| Store GWInfo Source # | |
| type Rep GWInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep GWInfo = D1 ('MetaData "GWInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'False) (C1 ('MetaCons "GWInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "gsym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "gsort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "gexpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "ginfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GradInfo)))) | |
Qualifiers
type Qualifier = QualifierV Symbol Source #
Qualifiers ----------------------------------------------------------------
data QualifierV v Source #
Constructors
| Q | |
Instances
Instances
data QualPattern Source #
Constructors
| PatNone | match everything |
| PatPrefix !Symbol !Int | str . $i i.e. match prefix |
| PatSuffix !Int !Symbol | $i . str i.e. match suffix |
| PatExact !Symbol | str i.e. exactly match |
Instances
mkQual :: Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v Source #
constructing qualifiers
remakeQual :: Qualifier -> Qualifier Source #
Results
type GFixSolution = GFixSol Expr Source #
Solutions and Results
Constructors
| Result | |
Fields
| |
Instances
| Functor Result Source # | |
| ToJSON a => ToJSON (Result a) Source # | |
| Monoid (Result a) Source # | |
| Semigroup (Result a) Source # | |
| Generic (Result a) Source # | |
| Show a => Show (Result a) Source # | |
| NFData a => NFData (Result a) Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| type Rep (Result a) Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep (Result a) = D1 ('MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'False) (C1 ('MetaCons "Result" 'PrefixI 'True) ((S1 ('MetaSel ('Just "resStatus") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (FixResult a)) :*: S1 ('MetaSel ('Just "resSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixSolution)) :*: (S1 ('MetaSel ('Just "resNonCutsSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixSolution) :*: S1 ('MetaSel ('Just "gresSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 GFixSolution)))) | |
Cut KVars
Constraint Cut Sets -------------------------------------------------------
Higher Order Logic
Constructors
| HOI | |
Instances
| Monoid HOInfo Source # | |
| Semigroup HOInfo Source # | |
| Generic HOInfo Source # | |
| Show HOInfo Source # | |
| NFData HOInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Eq HOInfo Source # | |
| Store HOInfo Source # | |
| type Rep HOInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep HOInfo = D1 ('MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'False) (C1 ('MetaCons "HOI" 'PrefixI 'True) (S1 ('MetaSel ('Just "hoBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "hoQuals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) | |
allowHOquals :: GInfo c a -> Bool Source #
Axioms
Axiom Instantiation Information --------------------------------------
Constructors
| AEnv | |
Fields
| |
Instances
Constructors
| Equ | |
Instances
Instances
data AutoRewrite Source #
Constructors
| AutoRewrite | |
Instances
dedupAutoRewrites :: HashMap SubcId [AutoRewrite] -> [AutoRewrite] Source #
newtype LocalRewritesEnv Source #
Constructors
| LocalRewritesMap (HashMap BindId LocalRewrites) |
Instances
newtype LocalRewrites Source #
Constructors
| LocalRewrites (HashMap Symbol Expr) |
Instances
lookupRewrite :: Symbol -> LocalRewrites -> Maybe Expr Source #
insertRewrites :: BindId -> LocalRewrites -> LocalRewritesEnv -> LocalRewritesEnv Source #