| Safe Haskell | None |
|---|---|
| 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 {}
- 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] -> [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
- 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 -> 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 {}
- data Qualifier = Q {}
- data QualParam = QP {}
- data QualPattern
- trueQual :: Qualifier
- qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier
- mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
- 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
- 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
- data AxiomEnv = AEnv {
- aenvEqs :: ![Equation]
- aenvSimpl :: ![Rewrite]
- aenvExpand :: HashMap SubcId Bool
- aenvAutoRW :: HashMap SubcId [AutoRewrite]
- data Equation = Equ {}
- mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
- data Rewrite = SMeasure {}
- data AutoRewrite = AutoRewrite {}
- 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 | |
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] -> [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 ---------------------------------------------------------------
Accessing Constraints
Instances
| Eq GWInfo Source # | |
| Generic GWInfo Source # | |
| Binary GWInfo Source # | |
| NFData GWInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| type Rep GWInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep GWInfo = D1 ('MetaData "GWInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" '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
Qualifiers ----------------------------------------------------------------
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
remakeQual :: Qualifier -> Qualifier Source #
Results
type FixSolution = HashMap KVar Expr Source #
type GFixSolution = GFixSol Expr Source #
Solutions and Results
Constructors
| Result | |
Fields
| |
Instances
| Functor Result Source # | |
| Show a => Show (Result a) Source # | |
| Generic (Result a) Source # | |
| Semigroup (Result a) Source # | |
| Monoid (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.8.10.2-inplace" '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 "gresSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 GFixSolution)))) | |
Cut KVars
Constraint Cut Sets -------------------------------------------------------
Higher Order Logic
Constructors
| HOI | |
Instances
| Eq HOInfo Source # | |
| Show HOInfo Source # | |
| Generic HOInfo Source # | |
| Semigroup HOInfo Source # | |
| Monoid HOInfo Source # | |
| Binary HOInfo Source # | |
| NFData HOInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| type Rep HOInfo Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep HOInfo = D1 ('MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" '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
| Eq Rewrite Source # | |
| Show Rewrite Source # | |
| Generic Rewrite Source # | |
| Binary Rewrite Source # | |
| NFData Rewrite Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| PPrint Rewrite Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Fixpoint Rewrite Source # | |
| Visitable Rewrite Source # | |
| Elaborate Rewrite Source # | |
| type Rep Rewrite Source # | |
Defined in Language.Fixpoint.Types.Constraints type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "SMeasure" 'PrefixI 'True) ((S1 ('MetaSel ('Just "smName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "smDC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :*: (S1 ('MetaSel ('Just "smArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "smBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) | |
data AutoRewrite Source #
Constructors
| AutoRewrite | |