Language.Fixpoint.Types.Constraints

This module contains the top-level QUERY data types and elements, including (Horn) implication & well-formedness constraints and sets.

Top-level Queries

type FInfo a = GInfo SubC a

type SInfo a = GInfo SimpC a

data GInfo c a

Constructors

FI

Fields

• cm :: !(HashMap SubcId (c a))

  cst id |-> Horn Constraint

• ws :: !(HashMap KVar (WfC a))

  Kvar |-> WfC defining its scope/args

• bs :: !BindEnv

  Bind |-> (Symbol, SortedReft)

• gLits :: !(SEnv Sort)

  Global Constant symbols

• dLits :: !(SEnv Sort)

  Distinct Constant symbols

• kuts :: !Kuts

  Set of KVars *not* to eliminate

• quals :: ![Qualifier]

  Abstract domain

• bindInfo :: !(HashMap BindId a)

  Metadata about binders

• ddecls :: ![DataDecl]

  User-defined data declarations

• hoInfo :: !HOInfo

  Higher Order info

• asserts :: ![Triggered Expr]
• ae :: AxiomEnv

Instances

Functor c => Functor (GInfo c)

Methods

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

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

PTable (SInfo a)

Methods

ptable :: SInfo a -> DocTable

Inputable (FInfo ())

Methods

rr :: String -> FInfo ()

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

Elaborate (SInfo a)

Methods

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

Gradual (SInfo a)

Methods

gsubst :: GSol -> SInfo a -> SInfo a

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

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)

Methods

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

show :: GInfo c a -> String

showList :: [GInfo c a] -> ShowS

Generic (GInfo c a)

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)

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)

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)

Methods

rnf :: GInfo c a -> ()

HasGradual (GInfo c a)

Methods

isGradual :: GInfo c a -> Bool

gVars :: GInfo c a -> [KVar]

ungrad :: GInfo c a -> GInfo c a

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

Methods

symConsts :: GInfo c a -> [SymConst]

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

Methods

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

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

Methods

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

type Rep (GInfo c a)

type Rep (GInfo c a) = D1 * (MetaData "GInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" 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

Top-level Queries

Constructors

FIO

Fields

• fioFI :: FInfo a
• fioOpts :: [String]

Instances

Inputable (FInfoWithOpts ())

Methods

rr :: String -> FInfoWithOpts ()

rr' :: String -> String -> FInfoWithOpts ()

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

Query Conversions: FInfo to SInfo

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

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

Serializing

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

Rendering Queries

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

saveQuery :: Config -> FInfo a -> IO ()

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

Constructing Queries

Constraints

data WfC a

Constructors

WfC

Fields

• wenv :: !IBindEnv
• wrft :: (Symbol, Sort, KVar)
• winfo :: !a

GWfC

Fields

• wenv :: !IBindEnv
• wrft :: !(Symbol, Sort, KVar)
• winfo :: !a
• wexpr :: !Expr
• wloc :: !GradInfo

Instances

Functor WfC

Methods

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

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

Eq a => Eq (WfC a)

Methods

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

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

Fixpoint a => Show (WfC a)

Methods

showsPrec :: Int -> WfC a -> ShowS

show :: WfC a -> String

showList :: [WfC a] -> ShowS

Generic (WfC a)

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)

Methods

put :: WfC a -> Put

get :: Get (WfC a)

putList :: [WfC a] -> Put

NFData a => NFData (WfC a)

Methods

rnf :: WfC a -> ()

Fixpoint a => PPrint (WfC a)

Methods

pprintTidy :: Tidy -> WfC a -> Doc

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

Fixpoint a => Fixpoint (WfC a)

Methods

toFix :: WfC a -> Doc

simplify :: WfC a -> WfC a

HasGradual (WfC a)

Methods

isGradual :: WfC a -> Bool

gVars :: WfC a -> [KVar]

ungrad :: WfC a -> WfC a

Defunc (WfC a)

Methods

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

type Rep (WfC a)

type Rep (WfC a) = D1 * (MetaData "WfC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) ((:+:) * (C1 * (MetaCons "WfC" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "wenv") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * IBindEnv)) ((:*:) * (S1 * (MetaSel (Just Symbol "wrft") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Symbol, Sort, KVar))) (S1 * (MetaSel (Just Symbol "winfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * a))))) (C1 * (MetaCons "GWfC" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "wenv") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * IBindEnv)) (S1 * (MetaSel (Just Symbol "wrft") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (Symbol, Sort, KVar)))) ((:*:) * (S1 * (MetaSel (Just Symbol "winfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * a)) ((:*:) * (S1 * (MetaSel (Just Symbol "wexpr") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Expr)) (S1 * (MetaSel (Just Symbol "wloc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * GradInfo)))))))

isGWfc :: WfC a -> Bool

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

data SubC a

Instances

Functor SubC

Methods

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

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

TaggedC SubC a

Methods

senv :: SubC a -> IBindEnv

sid :: SubC a -> Maybe Integer

stag :: SubC a -> Tag

sinfo :: SubC a -> a

clhs :: BindEnv -> SubC a -> [(Symbol, SortedReft)]

crhs :: SubC a -> Expr

Eq a => Eq (SubC a)

Methods

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

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

Fixpoint a => Show (SubC a)

Methods

showsPrec :: Int -> SubC a -> ShowS

show :: SubC a -> String

showList :: [SubC a] -> ShowS

Generic (SubC a)

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)

Methods

put :: SubC a -> Put

get :: Get (SubC a)

putList :: [SubC a] -> Put

NFData a => NFData (SubC a)

Methods

rnf :: SubC a -> ()

Fixpoint a => PPrint (SubC a)

Methods

pprintTidy :: Tidy -> SubC a -> Doc

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

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

Methods

toFix :: FixResult (SubC a) -> Doc

simplify :: FixResult (SubC a) -> FixResult (SubC a)

Fixpoint a => Fixpoint (SubC a)

Methods

toFix :: SubC a -> Doc

simplify :: SubC a -> SubC a

SymConsts (SubC a)

Methods

symConsts :: SubC a -> [SymConst]

Visitable (SubC a)

Methods

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

Inputable (FInfo ())

Methods

rr :: String -> FInfo ()

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

type Rep (SubC a)

type Rep (SubC a) = D1 * (MetaData "SubC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "SubC" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "_senv") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * IBindEnv)) ((:*:) * (S1 * (MetaSel (Just Symbol "slhs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SortedReft)) (S1 * (MetaSel (Just Symbol "srhs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SortedReft)))) ((:*:) * (S1 * (MetaSel (Just Symbol "_sid") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (Maybe SubcId))) ((:*:) * (S1 * (MetaSel (Just Symbol "_stag") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Tag)) (S1 * (MetaSel (Just Symbol "_sinfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * 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]

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

data SimpC a

Constructors

SimpC

Fields

• _cenv :: !IBindEnv
• _crhs :: !Expr
• _cid :: !(Maybe Integer)
• _cbind :: !BindId

  Id of lhs/rhs binder

• _ctag :: !Tag
• _cinfo :: !a

Instances

Functor SimpC

Methods

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

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

TaggedC SimpC a

Methods

senv :: SimpC a -> IBindEnv

sid :: SimpC a -> Maybe Integer

stag :: SimpC a -> Tag

sinfo :: SimpC a -> a

clhs :: BindEnv -> SimpC a -> [(Symbol, SortedReft)]

crhs :: SimpC a -> Expr

Fixpoint a => Show (SimpC a)

Methods

showsPrec :: Int -> SimpC a -> ShowS

show :: SimpC a -> String

showList :: [SimpC a] -> ShowS

Generic (SimpC a)

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)

Methods

put :: SimpC a -> Put

get :: Get (SimpC a)

putList :: [SimpC a] -> Put

NFData a => NFData (SimpC a)

Methods

rnf :: SimpC a -> ()

PTable (SInfo a)

Methods

ptable :: SInfo a -> DocTable

Fixpoint a => PPrint (SimpC a)

Methods

pprintTidy :: Tidy -> SimpC a -> Doc

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

Fixpoint a => Fixpoint (SimpC a)

Methods

toFix :: SimpC a -> Doc

simplify :: SimpC a -> SimpC a

SymConsts (SimpC a)

Methods

symConsts :: SimpC a -> [SymConst]

Visitable (SimpC a)

Methods

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

Elaborate (SInfo a)

Methods

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

Elaborate (SimpC a)

Methods

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

Gradual (SInfo a)

Methods

gsubst :: GSol -> SInfo a -> SInfo a

Gradual (SimpC a)

Methods

gsubst :: GSol -> SimpC a -> SimpC a

Defunc (SimpC a)

Methods

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

type Rep (SimpC a)

type Rep (SimpC a) = D1 * (MetaData "SimpC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "SimpC" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "_cenv") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * IBindEnv)) ((:*:) * (S1 * (MetaSel (Just Symbol "_crhs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Expr)) (S1 * (MetaSel (Just Symbol "_cid") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (Maybe Integer))))) ((:*:) * (S1 * (MetaSel (Just Symbol "_cbind") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * BindId)) ((:*:) * (S1 * (MetaSel (Just Symbol "_ctag") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Tag)) (S1 * (MetaSel (Just Symbol "_cinfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * a))))))

type Tag = [Int]

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

class TaggedC c a where

Minimal complete definition

senv, sid, stag, sinfo, clhs, crhs

Methods

senv :: c a -> IBindEnv

sid :: c a -> Maybe Integer

stag :: c a -> Tag

sinfo :: c a -> a

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

crhs :: c a -> Expr

Instances

TaggedC SimpC a

Methods

senv :: SimpC a -> IBindEnv

sid :: SimpC a -> Maybe Integer

stag :: SimpC a -> Tag

sinfo :: SimpC a -> a

clhs :: BindEnv -> SimpC a -> [(Symbol, SortedReft)]

crhs :: SimpC a -> Expr

TaggedC SubC a

Methods

senv :: SubC a -> IBindEnv

sid :: SubC a -> Maybe Integer

stag :: SubC a -> Tag

sinfo :: SubC a -> a

clhs :: BindEnv -> SubC a -> [(Symbol, SortedReft)]

crhs :: SubC a -> Expr

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

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

strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a

Accessing Constraints

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

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

shiftVV :: Reft -> Symbol -> Reft

gwInfo :: WfC a -> GWInfo

data GWInfo

Constructors

GWInfo

Fields

• gsym :: Symbol
• gsort :: Sort
• gexpr :: Expr
• ginfo :: GradInfo

Instances

Eq GWInfo

Methods

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

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

Generic GWInfo

Associated Types

type Rep GWInfo :: * -> *

Methods

from :: GWInfo -> Rep GWInfo x

to :: Rep GWInfo x -> GWInfo

Binary GWInfo

Methods

put :: GWInfo -> Put

get :: Get GWInfo

putList :: [GWInfo] -> Put

NFData GWInfo

Methods

rnf :: GWInfo -> ()

type Rep GWInfo

type Rep GWInfo = D1 * (MetaData "GWInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "GWInfo" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "gsym") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Symbol)) (S1 * (MetaSel (Just Symbol "gsort") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Sort))) ((:*:) * (S1 * (MetaSel (Just Symbol "gexpr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Just Symbol "ginfo") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * GradInfo)))))

Qualifiers

data Qualifier

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

Constructors

Q

Fields

• qName :: !Symbol

  Name

• qParams :: [(Symbol, Sort)]

  Parameters

• qBody :: !Expr

  Predicate

• qPos :: !SourcePos

  Source Location

Instances

Eq Qualifier

Methods

(==) :: Qualifier -> Qualifier -> Bool

(/=) :: Qualifier -> Qualifier -> Bool

Data Qualifier

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

Methods

showsPrec :: Int -> Qualifier -> ShowS

show :: Qualifier -> String

showList :: [Qualifier] -> ShowS

Generic Qualifier

Associated Types

type Rep Qualifier :: * -> *

Methods

from :: Qualifier -> Rep Qualifier x

to :: Rep Qualifier x -> Qualifier

Binary Qualifier

Methods

put :: Qualifier -> Put

get :: Get Qualifier

putList :: [Qualifier] -> Put

NFData Qualifier

Methods

rnf :: Qualifier -> ()

PPrint Qualifier

Methods

pprintTidy :: Tidy -> Qualifier -> Doc

pprintPrec :: Int -> Tidy -> Qualifier -> Doc

Fixpoint Qualifier

Methods

toFix :: Qualifier -> Doc

simplify :: Qualifier -> Qualifier

Loc Qualifier

Methods

srcSpan :: Qualifier -> SrcSpan

type Rep Qualifier

type Rep Qualifier = D1 * (MetaData "Qualifier" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "Q" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "qName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Symbol)) (S1 * (MetaSel (Just Symbol "qParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Symbol, Sort)]))) ((:*:) * (S1 * (MetaSel (Just Symbol "qBody") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Expr)) (S1 * (MetaSel (Just Symbol "qPos") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SourcePos)))))

trueQual :: Qualifier

qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier

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

constructing qualifiers

remakeQual :: Qualifier -> Qualifier

Results

type FixSolution = HashMap KVar Expr

type GFixSolution = GFixSol Expr

Solutions and Results

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

data Result a

Constructors

Result

Fields

• resStatus :: !(FixResult a)
• resSolution :: !FixSolution
• gresSolution :: !GFixSolution

Instances

Show a => Show (Result a)

Methods

showsPrec :: Int -> Result a -> ShowS

show :: Result a -> String

showList :: [Result a] -> ShowS

Generic (Result a)

Associated Types

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

Methods

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

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

Monoid (Result a)

Methods

mempty :: Result a

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

mconcat :: [Result a] -> Result a

NFData a => NFData (Result a)

Methods

rnf :: Result a -> ()

type Rep (Result a)

type Rep (Result a) = D1 * (MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" 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)))))

unsafe :: Result a

isUnsafe :: Result a -> Bool

isSafe :: Result a -> Bool

safe :: Result a

Cut KVars

newtype Kuts

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

Constructors

KS

Fields

• ksVars :: HashSet KVar

Instances

Eq Kuts

Methods

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

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

Show Kuts

Methods

showsPrec :: Int -> Kuts -> ShowS

show :: Kuts -> String

showList :: [Kuts] -> ShowS

Generic Kuts

Associated Types

type Rep Kuts :: * -> *

Methods

from :: Kuts -> Rep Kuts x

to :: Rep Kuts x -> Kuts

Monoid Kuts

Methods

mempty :: Kuts

mappend :: Kuts -> Kuts -> Kuts

mconcat :: [Kuts] -> Kuts

Binary Kuts

Methods

put :: Kuts -> Put

get :: Get Kuts

putList :: [Kuts] -> Put

NFData Kuts

Methods

rnf :: Kuts -> ()

Fixpoint Kuts

Methods

toFix :: Kuts -> Doc

simplify :: Kuts -> Kuts

type Rep Kuts

type Rep Kuts = D1 * (MetaData "Kuts" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" True) (C1 * (MetaCons "KS" PrefixI True) (S1 * (MetaSel (Just Symbol "ksVars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (HashSet KVar))))

ksMember :: KVar -> Kuts -> Bool

Higher Order Logic

data HOInfo

Constructors

HOI

Fields

• hoBinds :: Bool

  Allow higher order binds in the environemnt

• hoQuals :: Bool

  Allow higher order quals

Instances

Eq HOInfo

Methods

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

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

Show HOInfo

Methods

showsPrec :: Int -> HOInfo -> ShowS

show :: HOInfo -> String

showList :: [HOInfo] -> ShowS

Generic HOInfo

Associated Types

type Rep HOInfo :: * -> *

Methods

from :: HOInfo -> Rep HOInfo x

to :: Rep HOInfo x -> HOInfo

Monoid HOInfo

Methods

mempty :: HOInfo

mappend :: HOInfo -> HOInfo -> HOInfo

mconcat :: [HOInfo] -> HOInfo

Binary HOInfo

Methods

put :: HOInfo -> Put

get :: Get HOInfo

putList :: [HOInfo] -> Put

NFData HOInfo

Methods

rnf :: HOInfo -> ()

type Rep HOInfo

type Rep HOInfo = D1 * (MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" 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))))

allowHO :: GInfo c a -> Bool

allowHOquals :: GInfo c a -> Bool

Axioms

data AxiomEnv

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

Constructors

AEnv

Fields

• aenvEqs :: ![Equation]
• aenvSimpl :: ![Rewrite]
• aenvExpand :: HashMap SubcId Bool

Instances

Eq AxiomEnv

Methods

(==) :: AxiomEnv -> AxiomEnv -> Bool

(/=) :: AxiomEnv -> AxiomEnv -> Bool

Show AxiomEnv

Methods

showsPrec :: Int -> AxiomEnv -> ShowS

show :: AxiomEnv -> String

showList :: [AxiomEnv] -> ShowS

Generic AxiomEnv

Associated Types

type Rep AxiomEnv :: * -> *

Methods

from :: AxiomEnv -> Rep AxiomEnv x

to :: Rep AxiomEnv x -> AxiomEnv

Monoid AxiomEnv

Methods

mempty :: AxiomEnv

mappend :: AxiomEnv -> AxiomEnv -> AxiomEnv

mconcat :: [AxiomEnv] -> AxiomEnv

Binary AxiomEnv

Methods

put :: AxiomEnv -> Put

get :: Get AxiomEnv

putList :: [AxiomEnv] -> Put

NFData AxiomEnv

Methods

rnf :: AxiomEnv -> ()

PPrint AxiomEnv

Methods

pprintTidy :: Tidy -> AxiomEnv -> Doc

pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc

Fixpoint AxiomEnv

Methods

toFix :: AxiomEnv -> Doc

simplify :: AxiomEnv -> AxiomEnv

type Rep AxiomEnv

type Rep AxiomEnv = D1 * (MetaData "AxiomEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "AEnv" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "aenvEqs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * [Equation])) ((:*:) * (S1 * (MetaSel (Just Symbol "aenvSimpl") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * [Rewrite])) (S1 * (MetaSel (Just Symbol "aenvExpand") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (HashMap SubcId Bool))))))

data Equation

Constructors

Equ

Fields

• eqName :: !Symbol

  name of reflected function

• eqArgs :: [(Symbol, Sort)]

  names of parameters

• eqBody :: !Expr

  definition of body

• eqSort :: !Sort

  sort of body

• eqRec :: !Bool

  is this a recursive definition

Instances

Eq Equation

Methods

(==) :: Equation -> Equation -> Bool

(/=) :: Equation -> Equation -> Bool

Show Equation

Methods

showsPrec :: Int -> Equation -> ShowS

show :: Equation -> String

showList :: [Equation] -> ShowS

Generic Equation

Associated Types

type Rep Equation :: * -> *

Methods

from :: Equation -> Rep Equation x

to :: Rep Equation x -> Equation

Binary Equation

Methods

put :: Equation -> Put

get :: Get Equation

putList :: [Equation] -> Put

NFData Equation

Methods

rnf :: Equation -> ()

PPrint Equation

Methods

pprintTidy :: Tidy -> Equation -> Doc

pprintPrec :: Int -> Tidy -> Equation -> Doc

Fixpoint Equation

Methods

toFix :: Equation -> Doc

simplify :: Equation -> Equation

Subable Equation

Methods

syms :: Equation -> [Symbol]

substa :: (Symbol -> Symbol) -> Equation -> Equation

substf :: (Symbol -> Expr) -> Equation -> Equation

subst :: Subst -> Equation -> Equation

subst1 :: Equation -> (Symbol, Expr) -> Equation

type Rep Equation

type Rep Equation = D1 * (MetaData "Equation" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "Equ" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "eqName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Symbol)) (S1 * (MetaSel (Just Symbol "eqArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [(Symbol, Sort)]))) ((:*:) * (S1 * (MetaSel (Just Symbol "eqBody") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Expr)) ((:*:) * (S1 * (MetaSel (Just Symbol "eqSort") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Sort)) (S1 * (MetaSel (Just Symbol "eqRec") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Bool))))))

mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation

data Rewrite

Constructors

SMeasure

Fields

• smName :: Symbol
• smDC :: Symbol
• smArgs :: [Symbol]
• smBody :: Expr

Instances

Eq Rewrite

Methods

(==) :: Rewrite -> Rewrite -> Bool

(/=) :: Rewrite -> Rewrite -> Bool

Show Rewrite

Methods

showsPrec :: Int -> Rewrite -> ShowS

show :: Rewrite -> String

showList :: [Rewrite] -> ShowS

Generic Rewrite

Associated Types

type Rep Rewrite :: * -> *

Methods

from :: Rewrite -> Rep Rewrite x

to :: Rep Rewrite x -> Rewrite

Binary Rewrite

Methods

put :: Rewrite -> Put

get :: Get Rewrite

putList :: [Rewrite] -> Put

NFData Rewrite

Methods

rnf :: Rewrite -> ()

PPrint Rewrite

Methods

pprintTidy :: Tidy -> Rewrite -> Doc

pprintPrec :: Int -> Tidy -> Rewrite -> Doc

Fixpoint Rewrite

Methods

toFix :: Rewrite -> Doc

simplify :: Rewrite -> Rewrite

type Rep Rewrite

type Rep Rewrite = D1 * (MetaData "Rewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) (C1 * (MetaCons "SMeasure" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "smName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Symbol)) (S1 * (MetaSel (Just Symbol "smDC") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Symbol))) ((:*:) * (S1 * (MetaSel (Just Symbol "smArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Symbol])) (S1 * (MetaSel (Just Symbol "smBody") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))))

Misc [should be elsewhere but here due to dependencies]

substVars :: [(Symbol, Int)] -> Sort -> Sort

Orphan instances

Binary Eliminate

Methods

put :: Eliminate -> Put

get :: Get Eliminate

putList :: [Eliminate] -> Put

Binary SMTSolver

Methods

put :: SMTSolver -> Put

get :: Get SMTSolver

putList :: [SMTSolver] -> Put

NFData Eliminate

Methods

rnf :: Eliminate -> ()

NFData SMTSolver

Methods

rnf :: SMTSolver -> ()

Fixpoint Doc

Methods

toFix :: Doc -> Doc

simplify :: Doc -> Doc