liquid-fixpoint-0.7.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

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.

Synopsis

Top-level Queries

type FInfo a = GInfo SubC a Source #

type SInfo a = GInfo SimpC a Source #

data GInfo c a Source #

Constructors

FI 

Fields

Instances

Functor c => Functor (GInfo c) Source # 

Methods

fmap :: (a -> b) -> GInfo c a -> GInfo c b #

(<$) :: a -> GInfo c b -> GInfo c a #

PTable (SInfo a) Source # 

Methods

ptable :: SInfo a -> DocTable Source #

Inputable (FInfo ()) Source # 

Methods

rr :: String -> FInfo () Source #

rr' :: String -> String -> FInfo () Source #

Elaborate (SInfo a) Source # 

Methods

elaborate :: String -> SymEnv -> SInfo a -> SInfo a Source #

Gradual (SInfo a) Source # 

Methods

gsubst :: GSol -> SInfo a -> SInfo a Source #

(Eq (c a), Eq a) => Eq (GInfo c a) Source # 

Methods

(==) :: GInfo c a -> GInfo c a -> Bool #

(/=) :: GInfo c a -> GInfo c a -> Bool #

(Show (c a), Show a, Fixpoint a) => Show (GInfo c a) Source # 

Methods

showsPrec :: Int -> GInfo c a -> ShowS #

show :: GInfo c a -> String #

showList :: [GInfo c a] -> ShowS #

Generic (GInfo c a) Source # 

Associated Types

type Rep (GInfo c a) :: * -> * #

Methods

from :: GInfo c a -> Rep (GInfo c a) x #

to :: Rep (GInfo c a) x -> GInfo c a #

Monoid (GInfo c a) Source # 

Methods

mempty :: GInfo c a #

mappend :: GInfo c a -> GInfo c a -> GInfo c a #

mconcat :: [GInfo c a] -> GInfo c a #

(Binary (c a), Binary a) => Binary (GInfo c a) Source # 

Methods

put :: GInfo c a -> Put #

get :: Get (GInfo c a) #

putList :: [GInfo c a] -> Put #

(NFData (c a), NFData a) => NFData (GInfo c a) Source # 

Methods

rnf :: GInfo c a -> () #

SymConsts (c a) => SymConsts (GInfo c a) Source # 

Methods

symConsts :: GInfo c a -> [SymConst] Source #

Visitable (c a) => Visitable (GInfo c a) Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> GInfo c a -> VisitM a (GInfo c a) Source #

(Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source # 

Methods

defunc :: GInfo c a -> DF (GInfo c a) Source #

type Rep (GInfo c a) Source # 
type Rep (GInfo c a) = D1 (MetaData "GInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "FI" PrefixI True) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "cm") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashMap SubcId (c a)))) ((:*:) (S1 (MetaSel (Just Symbol "ws") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashMap KVar (WfC a)))) (S1 (MetaSel (Just Symbol "bs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 BindEnv)))) ((:*:) (S1 (MetaSel (Just Symbol "gLits") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SEnv Sort))) ((:*:) (S1 (MetaSel (Just Symbol "dLits") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SEnv Sort))) (S1 (MetaSel (Just Symbol "kuts") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Kuts))))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "quals") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Qualifier])) ((:*:) (S1 (MetaSel (Just Symbol "bindInfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashMap BindId a))) (S1 (MetaSel (Just Symbol "ddecls") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [DataDecl])))) ((:*:) (S1 (MetaSel (Just Symbol "hoInfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 HOInfo)) ((:*:) (S1 (MetaSel (Just Symbol "asserts") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Triggered Expr])) (S1 (MetaSel (Just Symbol "ae") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 AxiomEnv)))))))

data FInfoWithOpts a Source #

Top-level Queries

Constructors

FIO 

Fields

convertFormat :: Fixpoint a => FInfo a -> SInfo a Source #

Query Conversions: FInfo to SInfo

type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) Source #

Top level Solvers ----------------------------------------------------

Serializing

toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc Source #

Rendering Queries

writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO () Source #

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

data WfC a Source #

Constructors

WfC 

Fields

GWfC 

Fields

Instances

Functor WfC Source # 

Methods

fmap :: (a -> b) -> WfC a -> WfC b #

(<$) :: a -> WfC b -> WfC a #

Eq a => Eq (WfC a) Source # 

Methods

(==) :: WfC a -> WfC a -> Bool #

(/=) :: WfC a -> WfC a -> Bool #

Fixpoint a => Show (WfC a) Source # 

Methods

showsPrec :: Int -> WfC a -> ShowS #

show :: WfC a -> String #

showList :: [WfC a] -> ShowS #

Generic (WfC a) Source # 

Associated Types

type Rep (WfC a) :: * -> * #

Methods

from :: WfC a -> Rep (WfC a) x #

to :: Rep (WfC a) x -> WfC a #

Binary a => Binary (WfC a) Source # 

Methods

put :: WfC a -> Put #

get :: Get (WfC a) #

putList :: [WfC a] -> Put #

NFData a => NFData (WfC a) Source # 

Methods

rnf :: WfC a -> () #

Fixpoint a => PPrint (WfC a) Source # 

Methods

pprintTidy :: Tidy -> WfC a -> Doc Source #

pprintPrec :: Int -> Tidy -> WfC a -> Doc Source #

Fixpoint a => Fixpoint (WfC a) Source # 

Methods

toFix :: WfC a -> Doc Source #

simplify :: WfC a -> WfC a Source #

Defunc (WfC a) Source # 

Methods

defunc :: WfC a -> DF (WfC a) Source #

type Rep (WfC a) Source # 

updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a Source #

data SubC a Source #

Instances

Functor SubC Source # 

Methods

fmap :: (a -> b) -> SubC a -> SubC b #

(<$) :: a -> SubC b -> SubC a #

TaggedC SubC a Source # 
Eq a => Eq (SubC a) Source # 

Methods

(==) :: SubC a -> SubC a -> Bool #

(/=) :: SubC a -> SubC a -> Bool #

Fixpoint a => Show (SubC a) Source # 

Methods

showsPrec :: Int -> SubC a -> ShowS #

show :: SubC a -> String #

showList :: [SubC a] -> ShowS #

Generic (SubC a) Source # 

Associated Types

type Rep (SubC a) :: * -> * #

Methods

from :: SubC a -> Rep (SubC a) x #

to :: Rep (SubC a) x -> SubC a #

Binary a => Binary (SubC a) Source # 

Methods

put :: SubC a -> Put #

get :: Get (SubC a) #

putList :: [SubC a] -> Put #

NFData a => NFData (SubC a) Source # 

Methods

rnf :: SubC a -> () #

Fixpoint a => PPrint (SubC a) Source # 

Methods

pprintTidy :: Tidy -> SubC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SubC a -> Doc Source #

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Fixpoint a => Fixpoint (SubC a) Source # 

Methods

toFix :: SubC a -> Doc Source #

simplify :: SubC a -> SubC a Source #

Inputable (FInfo ()) Source # 

Methods

rr :: String -> FInfo () Source #

rr' :: String -> String -> FInfo () Source #

SymConsts (SubC a) Source # 

Methods

symConsts :: SubC a -> [SymConst] Source #

Visitable (SubC a) Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> SubC a -> VisitM a (SubC a) Source #

type Rep (SubC a) Source # 

subcId :: TaggedC c a => c a -> SubcId Source #

sid :: TaggedC c a => c a -> Maybe Integer Source #

senv :: TaggedC c a => c a -> IBindEnv Source #

stag :: TaggedC c a => c a -> Tag Source #

wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a] Source #

"Smart Constructors" for Constraints ---------------------------------

data SimpC a Source #

Constructors

SimpC 

Fields

Instances

Functor SimpC Source # 

Methods

fmap :: (a -> b) -> SimpC a -> SimpC b #

(<$) :: a -> SimpC b -> SimpC a #

TaggedC SimpC a Source # 
Fixpoint a => Show (SimpC a) Source # 

Methods

showsPrec :: Int -> SimpC a -> ShowS #

show :: SimpC a -> String #

showList :: [SimpC a] -> ShowS #

Generic (SimpC a) Source # 

Associated Types

type Rep (SimpC a) :: * -> * #

Methods

from :: SimpC a -> Rep (SimpC a) x #

to :: Rep (SimpC a) x -> SimpC a #

Binary a => Binary (SimpC a) Source # 

Methods

put :: SimpC a -> Put #

get :: Get (SimpC a) #

putList :: [SimpC a] -> Put #

NFData a => NFData (SimpC a) Source # 

Methods

rnf :: SimpC a -> () #

PTable (SInfo a) Source # 

Methods

ptable :: SInfo a -> DocTable Source #

Fixpoint a => PPrint (SimpC a) Source # 

Methods

pprintTidy :: Tidy -> SimpC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SimpC a -> Doc Source #

Fixpoint a => Fixpoint (SimpC a) Source # 

Methods

toFix :: SimpC a -> Doc Source #

simplify :: SimpC a -> SimpC a Source #

SymConsts (SimpC a) Source # 

Methods

symConsts :: SimpC a -> [SymConst] Source #

Visitable (SimpC a) Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> SimpC a -> VisitM a (SimpC a) Source #

Elaborate (SInfo a) Source # 

Methods

elaborate :: String -> SymEnv -> SInfo a -> SInfo a Source #

Elaborate (SimpC a) Source # 

Methods

elaborate :: String -> SymEnv -> SimpC a -> SimpC a Source #

Gradual (SInfo a) Source # 

Methods

gsubst :: GSol -> SInfo a -> SInfo a Source #

Gradual (SimpC a) Source # 

Methods

gsubst :: GSol -> SimpC a -> SimpC a Source #

Defunc (SimpC a) Source # 

Methods

defunc :: SimpC a -> DF (SimpC a) Source #

type Rep (SimpC a) Source # 

type Tag = [Int] Source #

Constraints ---------------------------------------------------------------

class TaggedC c a where Source #

Minimal complete definition

senv, sid, stag, sinfo, clhs, crhs

Methods

senv :: c a -> IBindEnv Source #

sid :: c a -> Maybe Integer Source #

stag :: c a -> Tag Source #

sinfo :: c a -> a Source #

clhs :: BindEnv -> c a -> [(Symbol, SortedReft)] Source #

crhs :: c a -> Expr Source #

clhs :: TaggedC c a => BindEnv -> c a -> [(Symbol, SortedReft)] Source #

crhs :: TaggedC c a => c a -> Expr Source #

Accessing Constraints

addIds :: [SubC a] -> [(Integer, SubC a)] Source #

sinfo :: TaggedC c a => c a -> a Source #

data GWInfo Source #

Constructors

GWInfo 

Fields

Instances

Eq GWInfo Source # 

Methods

(==) :: GWInfo -> GWInfo -> Bool #

(/=) :: GWInfo -> GWInfo -> Bool #

Generic GWInfo Source # 

Associated Types

type Rep GWInfo :: * -> * #

Methods

from :: GWInfo -> Rep GWInfo x #

to :: Rep GWInfo x -> GWInfo #

Binary GWInfo Source # 

Methods

put :: GWInfo -> Put #

get :: Get GWInfo #

putList :: [GWInfo] -> Put #

NFData GWInfo Source # 

Methods

rnf :: GWInfo -> () #

type Rep GWInfo Source # 

Qualifiers

data Qualifier Source #

Qualifiers ----------------------------------------------------------------

Constructors

Q 

Fields

Instances

Eq Qualifier Source # 
Data Qualifier Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Qualifier -> c Qualifier #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Qualifier #

toConstr :: Qualifier -> Constr #

dataTypeOf :: Qualifier -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Qualifier) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier) #

gmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Qualifier -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Qualifier -> r #

gmapQ :: (forall d. Data d => d -> u) -> Qualifier -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Qualifier -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

Show Qualifier Source # 
Generic Qualifier Source # 

Associated Types

type Rep Qualifier :: * -> * #

Binary Qualifier Source # 
NFData Qualifier Source # 

Methods

rnf :: Qualifier -> () #

PPrint Qualifier Source # 
Fixpoint Qualifier Source # 
Loc Qualifier Source # 
type Rep Qualifier Source # 

mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier Source #

constructing qualifiers

Results

type GFixSolution = GFixSol Expr Source #

Solutions and Results

toGFixSol :: HashMap KVar (e, [e]) -> GFixSol e Source #

data Result a Source #

Instances

Show a => Show (Result a) Source # 

Methods

showsPrec :: Int -> Result a -> ShowS #

show :: Result a -> String #

showList :: [Result a] -> ShowS #

Generic (Result a) Source # 

Associated Types

type Rep (Result a) :: * -> * #

Methods

from :: Result a -> Rep (Result a) x #

to :: Rep (Result a) x -> Result a #

Monoid (Result a) Source # 

Methods

mempty :: Result a #

mappend :: Result a -> Result a -> Result a #

mconcat :: [Result a] -> Result a #

NFData a => NFData (Result a) Source # 

Methods

rnf :: Result a -> () #

type Rep (Result a) Source # 
type Rep (Result a) = D1 (MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "Result" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "resStatus") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (FixResult a))) ((:*:) (S1 (MetaSel (Just Symbol "resSolution") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 FixSolution)) (S1 (MetaSel (Just Symbol "gresSolution") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 GFixSolution)))))

Cut KVars

newtype Kuts Source #

Constraint Cut Sets -------------------------------------------------------

Constructors

KS 

Fields

Instances

Eq Kuts Source # 

Methods

(==) :: Kuts -> Kuts -> Bool #

(/=) :: Kuts -> Kuts -> Bool #

Show Kuts Source # 

Methods

showsPrec :: Int -> Kuts -> ShowS #

show :: Kuts -> String #

showList :: [Kuts] -> ShowS #

Generic Kuts Source # 

Associated Types

type Rep Kuts :: * -> * #

Methods

from :: Kuts -> Rep Kuts x #

to :: Rep Kuts x -> Kuts #

Monoid Kuts Source # 

Methods

mempty :: Kuts #

mappend :: Kuts -> Kuts -> Kuts #

mconcat :: [Kuts] -> Kuts #

Binary Kuts Source # 

Methods

put :: Kuts -> Put #

get :: Get Kuts #

putList :: [Kuts] -> Put #

NFData Kuts Source # 

Methods

rnf :: Kuts -> () #

Fixpoint Kuts Source # 
type Rep Kuts Source # 
type Rep Kuts = D1 (MetaData "Kuts" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "KS" PrefixI True) (S1 (MetaSel (Just Symbol "ksVars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (HashSet KVar))))

Higher Order Logic

data HOInfo Source #

Constructors

HOI 

Fields

Instances

Eq HOInfo Source # 

Methods

(==) :: HOInfo -> HOInfo -> Bool #

(/=) :: HOInfo -> HOInfo -> Bool #

Show HOInfo Source # 
Generic HOInfo Source # 

Associated Types

type Rep HOInfo :: * -> * #

Methods

from :: HOInfo -> Rep HOInfo x #

to :: Rep HOInfo x -> HOInfo #

Monoid HOInfo Source # 
Binary HOInfo Source # 

Methods

put :: HOInfo -> Put #

get :: Get HOInfo #

putList :: [HOInfo] -> Put #

NFData HOInfo Source # 

Methods

rnf :: HOInfo -> () #

type Rep HOInfo Source # 
type Rep HOInfo = D1 (MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "HOI" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "hoBinds") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "hoQuals") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))

Axioms

data AxiomEnv Source #

Axiom Instantiation Information --------------------------------------

Instances

Eq AxiomEnv Source # 
Show AxiomEnv Source # 
Generic AxiomEnv Source # 

Associated Types

type Rep AxiomEnv :: * -> * #

Methods

from :: AxiomEnv -> Rep AxiomEnv x #

to :: Rep AxiomEnv x -> AxiomEnv #

Monoid AxiomEnv Source # 
Binary AxiomEnv Source # 

Methods

put :: AxiomEnv -> Put #

get :: Get AxiomEnv #

putList :: [AxiomEnv] -> Put #

NFData AxiomEnv Source # 

Methods

rnf :: AxiomEnv -> () #

Fixpoint AxiomEnv Source # 
type Rep AxiomEnv Source # 

data Rewrite Source #

Constructors

SMeasure 

Fields

Misc [should be elsewhere but here due to dependencies]

Orphan instances