Language.Fixpoint.Types.Refinements

This module has the types for representing terms in the refinement logic.

Representing Terms

data SymConst

Expressions ---------------------------------------------------------------

Uninterpreted constants that are embedded as "constant symbol : Str"

Constructors

SL !Text

Instances

Eq SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: SymConst -> SymConst -> Bool

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

Data SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: SymConst -> Constr

dataTypeOf :: SymConst -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymConst)

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

gmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst

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

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

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

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

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

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

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

Ord SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: SymConst -> SymConst -> Ordering

(<) :: SymConst -> SymConst -> Bool

(<=) :: SymConst -> SymConst -> Bool

(>) :: SymConst -> SymConst -> Bool

(>=) :: SymConst -> SymConst -> Bool

max :: SymConst -> SymConst -> SymConst

min :: SymConst -> SymConst -> SymConst

Show SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> SymConst -> ShowS

show :: SymConst -> String

showList :: [SymConst] -> ShowS

Generic SymConst

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SymConst :: Type -> Type

Methods

from :: SymConst -> Rep SymConst x

to :: Rep SymConst x -> SymConst

Binary SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SymConst -> Put

get :: Get SymConst

putList :: [SymConst] -> Put

NFData SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SymConst -> ()

Hashable SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> SymConst -> Int

hash :: SymConst -> Int

PPrint SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> SymConst -> Doc

pprintPrec :: Int -> Tidy -> SymConst -> Doc

Fixpoint SymConst

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: SymConst -> Doc

simplify :: SymConst -> SymConst

Symbolic SymConst

String Constants ----------------------------------------------------------

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

Defined in Language.Fixpoint.Types.Refinements

Methods

symbol :: SymConst -> Symbol

SMTLIB2 SymConst

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> SymConst -> Builder

type Rep SymConst

Defined in Language.Fixpoint.Types.Refinements

type Rep SymConst = D1 ('MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)))

data Constant

Constructors

I !Integer

R !Double

L !Text !Sort

Instances

Eq Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Constant -> Constant -> Bool

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

Data Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Constant -> Constr

dataTypeOf :: Constant -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constant)

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

gmapT :: (forall b. Data b => b -> b) -> Constant -> Constant

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

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

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

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

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

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

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

Ord Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Constant -> Constant -> Ordering

(<) :: Constant -> Constant -> Bool

(<=) :: Constant -> Constant -> Bool

(>) :: Constant -> Constant -> Bool

(>=) :: Constant -> Constant -> Bool

max :: Constant -> Constant -> Constant

min :: Constant -> Constant -> Constant

Show Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Constant -> ShowS

show :: Constant -> String

showList :: [Constant] -> ShowS

Generic Constant

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Constant :: Type -> Type

Methods

from :: Constant -> Rep Constant x

to :: Rep Constant x -> Constant

Binary Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Constant -> Put

get :: Get Constant

putList :: [Constant] -> Put

NFData Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Constant -> ()

Hashable Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Constant -> Int

hash :: Constant -> Int

PPrint Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Constant -> Doc

pprintPrec :: Int -> Tidy -> Constant -> Doc

Fixpoint Constant

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Constant -> Doc

simplify :: Constant -> Constant

SMTLIB2 Constant

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Constant -> Builder

Inputable Constant

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Constant

rr' :: String -> String -> Constant

type Rep Constant

Defined in Language.Fixpoint.Types.Refinements

type Rep Constant = D1 ('MetaData "Constant" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer)) :+: (C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Double)) :+: C1 ('MetaCons "L" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

data Bop

Constructors

Plus

Minus

Times

Div

Mod

RTimes

RDiv

Instances

Eq Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Bop -> Bop -> Bool

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

Data Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Bop -> Constr

dataTypeOf :: Bop -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Bop)

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

gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop

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

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

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

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

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

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

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

Ord Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Bop -> Bop -> Ordering

(<) :: Bop -> Bop -> Bool

(<=) :: Bop -> Bop -> Bool

(>) :: Bop -> Bop -> Bool

(>=) :: Bop -> Bop -> Bool

max :: Bop -> Bop -> Bop

min :: Bop -> Bop -> Bop

Show Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Bop -> ShowS

show :: Bop -> String

showList :: [Bop] -> ShowS

Generic Bop

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Bop :: Type -> Type

Methods

from :: Bop -> Rep Bop x

to :: Rep Bop x -> Bop

Binary Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Bop -> Put

get :: Get Bop

putList :: [Bop] -> Put

NFData Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Bop -> ()

Hashable Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Bop -> Int

hash :: Bop -> Int

PPrint Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Bop -> Doc

pprintPrec :: Int -> Tidy -> Bop -> Doc

Fixpoint Bop

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Bop -> Doc

simplify :: Bop -> Bop

SMTLIB2 Bop

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Bop -> Builder

type Rep Bop

Defined in Language.Fixpoint.Types.Refinements

type Rep Bop = D1 ('MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) ((C1 ('MetaCons "Plus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Minus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Times" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTimes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RDiv" 'PrefixI 'False) (U1 :: Type -> Type))))

data Brel

Constructors

Eq

Ne

Gt

Ge

Lt

Le

Ueq

Une

Instances

Eq Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Brel -> Brel -> Bool

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

Data Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Brel -> Constr

dataTypeOf :: Brel -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Brel)

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

gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel

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

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

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

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

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

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

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

Ord Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Brel -> Brel -> Ordering

(<) :: Brel -> Brel -> Bool

(<=) :: Brel -> Brel -> Bool

(>) :: Brel -> Brel -> Bool

(>=) :: Brel -> Brel -> Bool

max :: Brel -> Brel -> Brel

min :: Brel -> Brel -> Brel

Show Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Brel -> ShowS

show :: Brel -> String

showList :: [Brel] -> ShowS

Generic Brel

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Brel :: Type -> Type

Methods

from :: Brel -> Rep Brel x

to :: Rep Brel x -> Brel

Binary Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Brel -> Put

get :: Get Brel

putList :: [Brel] -> Put

NFData Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Brel -> ()

Hashable Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Brel -> Int

hash :: Brel -> Int

PPrint Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Brel -> Doc

pprintPrec :: Int -> Tidy -> Brel -> Doc

Fixpoint Brel

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Brel -> Doc

simplify :: Brel -> Brel

SMTLIB2 Brel

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Brel -> Builder

type Rep Brel

Defined in Language.Fixpoint.Types.Refinements

type Rep Brel = D1 ('MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (((C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ne" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ge" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ueq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Une" 'PrefixI 'False) (U1 :: Type -> Type))))

data Expr

Constructors

ESym !SymConst

ECon !Constant

EVar !Symbol

EApp !Expr !Expr

ENeg !Expr

EBin !Bop !Expr !Expr

EIte !Expr !Expr !Expr

ECst !Expr !Sort

ELam !(Symbol, Sort) !Expr

ETApp !Expr !Sort

ETAbs !Expr !Symbol

PAnd ![Expr]

POr ![Expr]

PNot !Expr

PImp !Expr !Expr

PIff !Expr !Expr

PAtom !Brel !Expr !Expr

PKVar !KVar !Subst

PAll ![(Symbol, Sort)] !Expr

PExist ![(Symbol, Sort)] !Expr

PGrad !KVar !Subst !GradInfo !Expr

ECoerc !Sort !Sort !Expr

Instances

Eq Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Expr -> Expr -> Bool

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

Data Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Expr -> Constr

dataTypeOf :: Expr -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr)

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

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr

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

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

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

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

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

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

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

Show Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Show GFixSolution

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> GFixSolution -> ShowS

show :: GFixSolution -> String

showList :: [GFixSolution] -> ShowS

Generic Expr

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Expr :: Type -> Type

Methods

from :: Expr -> Rep Expr x

to :: Rep Expr x -> Expr

Semigroup Expr

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Expr -> Expr -> Expr

sconcat :: NonEmpty Expr -> Expr

stimes :: Integral b => b -> Expr -> Expr

Monoid Expr

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Expr

mappend :: Expr -> Expr -> Expr

mconcat :: [Expr] -> Expr

Binary Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Expr -> Put

get :: Get Expr

putList :: [Expr] -> Put

Binary GFixSolution

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: GFixSolution -> Put

get :: Get GFixSolution

putList :: [GFixSolution] -> Put

NFData Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Expr -> ()

NFData GFixSolution

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: GFixSolution -> ()

Hashable Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Expr -> Int

hash :: Expr -> Int

PPrint Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Expr -> Doc

pprintPrec :: Int -> Tidy -> Expr -> Doc

PPrint GFixSolution

Defined in Language.Fixpoint.Types.Constraints

Methods

pprintTidy :: Tidy -> GFixSolution -> Doc

pprintPrec :: Int -> Tidy -> GFixSolution -> Doc

Fixpoint Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Expr -> Doc

simplify :: Expr -> Expr

Subable Expr

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Expr -> [Symbol]

substa :: (Symbol -> Symbol) -> Expr -> Expr

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

subst :: Subst -> Expr -> Expr

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

Predicate Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr

Expression Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr

HasGradual Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: Expr -> Bool

gVars :: Expr -> [KVar]

ungrad :: Expr -> Expr

SymConsts Expr

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Expr -> [SymConst]

Visitable Expr

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr

SMTLIB2 Expr

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Expr -> Builder

Elaborate Expr

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Expr -> Expr

Inputable Expr

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Expr

rr' :: String -> String -> Expr

Gradual Expr

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Expr -> Expr

Defunc Expr

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Expr -> DF Expr

SMTLIB2 (Triggered Expr)

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Triggered Expr -> Builder

Inputable (FixResult Integer, FixSolution)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> (FixResult Integer, FixSolution)

rr' :: String -> String -> (FixResult Integer, FixSolution)

type Rep Expr

Defined in Language.Fixpoint.Types.Refinements

type Rep Expr = D1 ('MetaData "Expr" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) ((((C1 ('MetaCons "ESym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymConst)) :+: C1 ('MetaCons "ECon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Constant))) :+: (C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: C1 ('MetaCons "ENeg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))))) :+: ((C1 ('MetaCons "EBin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bop) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))) :+: (C1 ('MetaCons "EIte" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))) :+: C1 ('MetaCons "ECst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)))) :+: (C1 ('MetaCons "ELam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Symbol, Sort)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: (C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :+: C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)))))) :+: (((C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Expr])) :+: C1 ('MetaCons "POr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Expr]))) :+: (C1 ('MetaCons "PNot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: (C1 ('MetaCons "PImp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: C1 ('MetaCons "PIff" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))))) :+: ((C1 ('MetaCons "PAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Brel) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))) :+: (C1 ('MetaCons "PKVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Subst)) :+: C1 ('MetaCons "PAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)))) :+: (C1 ('MetaCons "PExist" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: (C1 ('MetaCons "PGrad" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Subst)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 GradInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))) :+: C1 ('MetaCons "ECoerc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr))))))))

type Pred = Expr

data GradInfo

Constructors

GradInfo

Fields

• gsrc :: SrcSpan
• gused :: Maybe SrcSpan

Instances

Eq GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: GradInfo -> GradInfo -> Bool

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

Data GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: GradInfo -> Constr

dataTypeOf :: GradInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GradInfo)

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

gmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo

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

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

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

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

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

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

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

Show GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> GradInfo -> ShowS

show :: GradInfo -> String

showList :: [GradInfo] -> ShowS

Generic GradInfo

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep GradInfo :: Type -> Type

Methods

from :: GradInfo -> Rep GradInfo x

to :: Rep GradInfo x -> GradInfo

Binary GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: GradInfo -> Put

get :: Get GradInfo

putList :: [GradInfo] -> Put

NFData GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: GradInfo -> ()

Hashable GradInfo

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> GradInfo -> Int

hash :: GradInfo -> Int

type Rep GradInfo

Defined in Language.Fixpoint.Types.Refinements

type Rep GradInfo = D1 ('MetaData "GradInfo" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "GradInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "gsrc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "gused") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SrcSpan))))

pattern PTrue :: Expr

pattern PTop :: Expr

pattern PFalse :: Expr

pattern EBot :: Expr

pattern ETimes :: Expr -> Expr -> Expr

pattern ERTimes :: Expr -> Expr -> Expr

pattern EDiv :: Expr -> Expr -> Expr

pattern ERDiv :: Expr -> Expr -> Expr

pattern EEq :: Expr -> Expr -> Expr

newtype KVar

Kvars ---------------------------------------------------------------------

Constructors

KV

Fields

• kv :: Symbol

Instances

Eq KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: KVar -> KVar -> Bool

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

Data KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: KVar -> Constr

dataTypeOf :: KVar -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVar)

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

gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar

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

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

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

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

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

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

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

Ord KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: KVar -> KVar -> Ordering

(<) :: KVar -> KVar -> Bool

(<=) :: KVar -> KVar -> Bool

(>) :: KVar -> KVar -> Bool

(>=) :: KVar -> KVar -> Bool

max :: KVar -> KVar -> KVar

min :: KVar -> KVar -> KVar

Show KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVar -> ShowS

show :: KVar -> String

showList :: [KVar] -> ShowS

IsString KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

fromString :: String -> KVar

Generic KVar

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVar :: Type -> Type

Methods

from :: KVar -> Rep KVar x

to :: Rep KVar x -> KVar

Binary KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: KVar -> Put

get :: Get KVar

putList :: [KVar] -> Put

NFData KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: KVar -> ()

Hashable KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> KVar -> Int

hash :: KVar -> Int

PPrint KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVar -> Doc

pprintPrec :: Int -> Tidy -> KVar -> Doc

Fixpoint KVar

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: KVar -> Doc

simplify :: KVar -> KVar

Inputable (FixResult Integer, FixSolution)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> (FixResult Integer, FixSolution)

rr' :: String -> String -> (FixResult Integer, FixSolution)

type Rep KVar

Defined in Language.Fixpoint.Types.Refinements

type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'True) (C1 ('MetaCons "KV" 'PrefixI 'True) (S1 ('MetaSel ('Just "kv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

newtype Subst

Substitutions -------------------------------------------------------------

Constructors

Su (HashMap Symbol Expr)

Instances

Eq Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Subst -> Subst -> Bool

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

Data Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Subst -> Constr

dataTypeOf :: Subst -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Subst)

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

gmapT :: (forall b. Data b => b -> b) -> Subst -> Subst

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

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

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

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

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

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

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

Show Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Subst -> ShowS

show :: Subst -> String

showList :: [Subst] -> ShowS

Generic Subst

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Subst :: Type -> Type

Methods

from :: Subst -> Rep Subst x

to :: Rep Subst x -> Subst

Semigroup Subst

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Subst -> Subst -> Subst

sconcat :: NonEmpty Subst -> Subst

stimes :: Integral b => b -> Subst -> Subst

Monoid Subst

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Subst

mappend :: Subst -> Subst -> Subst

mconcat :: [Subst] -> Subst

Binary Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Subst -> Put

get :: Get Subst

putList :: [Subst] -> Put

NFData Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Subst -> ()

Hashable Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Subst -> Int

hash :: Subst -> Int

PPrint Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> Subst -> Doc

pprintPrec :: Int -> Tidy -> Subst -> Doc

Fixpoint Subst

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Subst -> Doc

simplify :: Subst -> Subst

type Rep Subst

Defined in Language.Fixpoint.Types.Refinements

type Rep Subst = D1 ('MetaData "Subst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'True) (C1 ('MetaCons "Su" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Expr))))

data KVSub

Constructors

KVS

Fields

• ksuVV :: Symbol
• ksuSort :: Sort
• ksuKVar :: KVar
• ksuSubst :: Subst

Instances

Eq KVSub

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: KVSub -> KVSub -> Bool

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

Data KVSub

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: KVSub -> Constr

dataTypeOf :: KVSub -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVSub)

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

gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub

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

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

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

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

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

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

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

Show KVSub

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVSub -> ShowS

show :: KVSub -> String

showList :: [KVSub] -> ShowS

Generic KVSub

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVSub :: Type -> Type

Methods

from :: KVSub -> Rep KVSub x

to :: Rep KVSub x -> KVSub

PPrint KVSub

Defined in Language.Fixpoint.Types.Refinements

Methods

pprintTidy :: Tidy -> KVSub -> Doc

pprintPrec :: Int -> Tidy -> KVSub -> Doc

type Rep KVSub

Defined in Language.Fixpoint.Types.Refinements

type Rep KVSub = D1 ('MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "KVS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ksuVV") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ksuSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "ksuKVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KVar) :*: S1 ('MetaSel ('Just "ksuSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Subst))))

newtype Reft

Parsed refinement of Symbol as Expr e.g. in '{v: _ | e }' v is the Symbol and e the Expr

Constructors

Reft (Symbol, Expr)

Instances

Eq Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: Reft -> Reft -> Bool

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

Data Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: Reft -> Constr

dataTypeOf :: Reft -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Reft)

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

gmapT :: (forall b. Data b => b -> b) -> Reft -> Reft

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

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

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

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

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

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

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

Show Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

showsPrec :: Int -> Reft -> ShowS

show :: Reft -> String

showList :: [Reft] -> ShowS

Generic Reft

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Reft :: Type -> Type

Methods

from :: Reft -> Rep Reft x

to :: Rep Reft x -> Reft

Semigroup Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Reft -> Reft -> Reft

sconcat :: NonEmpty Reft -> Reft

stimes :: Integral b => b -> Reft -> Reft

Monoid Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Reft

mappend :: Reft -> Reft -> Reft

mconcat :: [Reft] -> Reft

Binary Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Reft -> Put

get :: Get Reft

putList :: [Reft] -> Put

NFData Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Reft -> ()

Hashable Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Reft -> Int

hash :: Reft -> Int

PPrint Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

pprintTidy :: Tidy -> Reft -> Doc

pprintPrec :: Int -> Tidy -> Reft -> Doc

Fixpoint Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

toFix :: Reft -> Doc

simplify :: Reft -> Reft

Reftable Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

isTauto :: Reft -> Bool

ppTy :: Reft -> Doc -> Doc

top :: Reft -> Reft

bot :: Reft -> Reft

meet :: Reft -> Reft -> Reft

toReft :: Reft -> Reft

ofReft :: Reft -> Reft

params :: Reft -> [Symbol]

Subable Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Reft -> [Symbol]

substa :: (Symbol -> Symbol) -> Reft -> Reft

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

subst :: Subst -> Reft -> Reft

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

Expression Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr

HasGradual Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: Reft -> Bool

gVars :: Reft -> [KVar]

ungrad :: Reft -> Reft

SymConsts Reft

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Reft -> [SymConst]

Visitable Reft

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Reft -> VisitM a Reft

Gradual Reft

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Reft -> Reft

Defunc Reft

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Reft -> DF Reft

type Rep Reft

Defined in Language.Fixpoint.Types.Refinements

type Rep Reft = D1 ('MetaData "Reft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'True) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, Expr))))

data SortedReft

Constructors

RR

Fields

• sr_sort :: !Sort
• sr_reft :: !Reft

Instances

Eq SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

(==) :: SortedReft -> SortedReft -> Bool

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

Data SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

toConstr :: SortedReft -> Constr

dataTypeOf :: SortedReft -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SortedReft)

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

gmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft

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

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

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

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

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

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

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

Show SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

showsPrec :: Int -> SortedReft -> ShowS

show :: SortedReft -> String

showList :: [SortedReft] -> ShowS

Generic SortedReft

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SortedReft :: Type -> Type

Methods

from :: SortedReft -> Rep SortedReft x

to :: Rep SortedReft x -> SortedReft

Semigroup SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: SortedReft -> SortedReft -> SortedReft

sconcat :: NonEmpty SortedReft -> SortedReft

stimes :: Integral b => b -> SortedReft -> SortedReft

Semigroup BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: BindEnv -> BindEnv -> BindEnv

sconcat :: NonEmpty BindEnv -> BindEnv

stimes :: Integral b => b -> BindEnv -> BindEnv

Monoid SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: SortedReft

mappend :: SortedReft -> SortedReft -> SortedReft

mconcat :: [SortedReft] -> SortedReft

Monoid BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: BindEnv

mappend :: BindEnv -> BindEnv -> BindEnv

mconcat :: [BindEnv] -> BindEnv

Binary SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SortedReft -> Put

get :: Get SortedReft

putList :: [SortedReft] -> Put

Binary BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

put :: BindEnv -> Put

get :: Get BindEnv

putList :: [BindEnv] -> Put

NFData SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SortedReft -> ()

NFData BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv -> ()

Hashable SortedReft

Defined in Language.Fixpoint.Types.Constraints

Methods

hashWithSalt :: Int -> SortedReft -> Int

hash :: SortedReft -> Int

PPrint SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

pprintTidy :: Tidy -> SortedReft -> Doc

pprintPrec :: Int -> Tidy -> SortedReft -> Doc

Fixpoint SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

toFix :: SortedReft -> Doc

simplify :: SortedReft -> SortedReft

Fixpoint BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: BindEnv -> Doc

simplify :: BindEnv -> BindEnv

Reftable SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

isTauto :: SortedReft -> Bool

ppTy :: SortedReft -> Doc -> Doc

top :: SortedReft -> SortedReft

bot :: SortedReft -> SortedReft

meet :: SortedReft -> SortedReft -> SortedReft

toReft :: SortedReft -> Reft

ofReft :: Reft -> SortedReft

params :: SortedReft -> [Symbol]

Subable SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: SortedReft -> [Symbol]

substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft

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

subst :: Subst -> SortedReft -> SortedReft

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

Expression SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr

HasGradual SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: SortedReft -> Bool

gVars :: SortedReft -> [KVar]

ungrad :: SortedReft -> SortedReft

SymConsts SortedReft

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SortedReft -> [SymConst]

SymConsts BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv -> [SymConst]

Visitable SortedReft

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> SortedReft -> VisitM a SortedReft

Visitable BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> BindEnv -> VisitM a BindEnv

Elaborate SortedReft

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SortedReft -> SortedReft

Elaborate BindEnv

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> BindEnv -> BindEnv

Gradual SortedReft

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> SortedReft -> SortedReft

Gradual BindEnv

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv -> BindEnv

Defunc SortedReft

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: SortedReft -> DF SortedReft

Defunc BindEnv

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv -> DF BindEnv

Expression (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr

Visitable (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> (Symbol, SortedReft) -> VisitM a (Symbol, SortedReft)

Defunc (Symbol, SortedReft)

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft)

type Rep SortedReft

Defined in Language.Fixpoint.Types.Refinements

type Rep SortedReft = D1 ('MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "RR" 'PrefixI 'True) (S1 ('MetaSel ('Just "sr_sort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "sr_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Reft)))

Constructing Terms

eVar :: Symbolic a => a -> Expr

elit :: Located Symbol -> Sort -> Expr

eProp :: Symbolic a => a -> Expr

pAnd :: ListNE Pred -> Pred

pOr :: ListNE Pred -> Pred

pIte :: Pred -> Expr -> Expr -> Expr

(&.&) :: Pred -> Pred -> Pred

(|.|) :: Pred -> Pred -> Pred

pExist :: [(Symbol, Sort)] -> Pred -> Pred

mkEApp :: LocSymbol -> [Expr] -> Expr

mkProp :: Expr -> Pred

intKvar :: Integer -> KVar

vv_ :: Symbol

Generalizing Embedding with Typeclasses

class Expression a where

Generalizing Symbol, Expression, Predicate into Classes -----------

Values that can be viewed as Constants

Values that can be viewed as Expressions

Methods

expr :: a -> Expr

Instances

Expression Int

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Int -> Expr

Expression Integer

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Integer -> Expr

Expression Text

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Text -> Expr

Expression Symbol

The symbol may be an encoding of a SymConst.

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr

Expression SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr

Expression Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr

Expression Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr

Expression Bv

Construct an Expr using a raw string, e.g. (Bv S32 "#x02000000")

Defined in Language.Fixpoint.Smt.Bitvector

Methods

expr :: Bv -> Expr

Expression a => Expression (Located a)

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr

Expression (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr

class Predicate a where

Values that can be viewed as Predicates

Methods

prop :: a -> Expr

Instances

Predicate Bool

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Bool -> Expr

Predicate Symbol

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr

Predicate Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr

class Subable a where

Class Predicates for Valid Refinements -----------------------------

Minimal complete definition

syms, substa, substf, subst

Methods

syms

Arguments

:: a

-> [Symbol]

free symbols of a

substa :: (Symbol -> Symbol) -> a -> a

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

subst :: Subst -> a -> a

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

Instances

Subable ()

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: () -> [Symbol]

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

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

subst :: Subst -> () -> ()

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

Subable Symbol

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Symbol -> [Symbol]

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

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

subst :: Subst -> Symbol -> Symbol

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

Subable SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: SortedReft -> [Symbol]

substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft

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

subst :: Subst -> SortedReft -> SortedReft

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

Subable Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Reft -> [Symbol]

substa :: (Symbol -> Symbol) -> Reft -> Reft

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

subst :: Subst -> Reft -> Reft

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

Subable Expr

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Expr -> [Symbol]

substa :: (Symbol -> Symbol) -> Expr -> Expr

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

subst :: Subst -> Expr -> Expr

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

Subable Equation

Defined in Language.Fixpoint.Types.Constraints

Methods

syms :: Equation -> [Symbol]

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

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

subst :: Subst -> Equation -> Equation

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

Subable Qualifier

Defined in Language.Fixpoint.Types.Constraints

Methods

syms :: Qualifier -> [Symbol]

substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier

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

subst :: Subst -> Qualifier -> Qualifier

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

Subable Bind

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Bind -> [Symbol]

substa :: (Symbol -> Symbol) -> Bind -> Bind

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

subst :: Subst -> Bind -> Bind

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

Subable Pred

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Pred -> [Symbol]

substa :: (Symbol -> Symbol) -> Pred -> Pred

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

subst :: Subst -> Pred -> Pred

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

Subable a => Subable [a]

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: [a] -> [Symbol]

substa :: (Symbol -> Symbol) -> [a] -> [a]

substf :: (Symbol -> Expr) -> [a] -> [a]

subst :: Subst -> [a] -> [a]

subst1 :: [a] -> (Symbol, Expr) -> [a]

Subable a => Subable (Maybe a)

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Maybe a -> [Symbol]

substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a

substf :: (Symbol -> Expr) -> Maybe a -> Maybe a

subst :: Subst -> Maybe a -> Maybe a

subst1 :: Maybe a -> (Symbol, Expr) -> Maybe a

Subable a => Subable (Located a)

Defined in Language.Fixpoint.Types.Refinements

Methods

syms :: Located a -> [Symbol]

substa :: (Symbol -> Symbol) -> Located a -> Located a

substf :: (Symbol -> Expr) -> Located a -> Located a

subst :: Subst -> Located a -> Located a

subst1 :: Located a -> (Symbol, Expr) -> Located a

(Subable a, Subable b) => Subable (a, b)

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: (a, b) -> [Symbol]

substa :: (Symbol -> Symbol) -> (a, b) -> (a, b)

substf :: (Symbol -> Expr) -> (a, b) -> (a, b)

subst :: Subst -> (a, b) -> (a, b)

subst1 :: (a, b) -> (Symbol, Expr) -> (a, b)

Subable a => Subable (HashMap k a)

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: HashMap k a -> [Symbol]

substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a

substf :: (Symbol -> Expr) -> HashMap k a -> HashMap k a

subst :: Subst -> HashMap k a -> HashMap k a

subst1 :: HashMap k a -> (Symbol, Expr) -> HashMap k a

class (Monoid r, Subable r) => Reftable r where

Minimal complete definition

isTauto, ppTy, bot, toReft, ofReft, params

Methods

isTauto :: r -> Bool

ppTy :: r -> Doc -> Doc

top :: r -> r

bot :: r -> r

meet :: r -> r -> r

toReft :: r -> Reft

ofReft :: Reft -> r

params

Arguments

:: r

-> [Symbol]

parameters for Reft, vv + others

Instances

Reftable ()

Defined in Language.Fixpoint.Types.Substitutions

Methods

isTauto :: () -> Bool

ppTy :: () -> Doc -> Doc

top :: () -> ()

bot :: () -> ()

meet :: () -> () -> ()

toReft :: () -> Reft

ofReft :: Reft -> ()

params :: () -> [Symbol]

Reftable SortedReft

Defined in Language.Fixpoint.Types.Substitutions

Methods

isTauto :: SortedReft -> Bool

ppTy :: SortedReft -> Doc -> Doc

top :: SortedReft -> SortedReft

bot :: SortedReft -> SortedReft

meet :: SortedReft -> SortedReft -> SortedReft

toReft :: SortedReft -> Reft

ofReft :: Reft -> SortedReft

params :: SortedReft -> [Symbol]

Reftable Reft

Defined in Language.Fixpoint.Types.Substitutions

Methods

isTauto :: Reft -> Bool

ppTy :: Reft -> Doc -> Doc

top :: Reft -> Reft

bot :: Reft -> Reft

meet :: Reft -> Reft -> Reft

toReft :: Reft -> Reft

ofReft :: Reft -> Reft

params :: Reft -> [Symbol]

Constructors

reft :: Symbol -> Expr -> Reft

trueSortedReft :: Sort -> SortedReft

trueReft :: Reft

falseReft :: Reft

exprReft :: Expression a => a -> Reft

notExprReft :: Expression a => a -> Reft

uexprReft :: Expression a => a -> Reft

symbolReft :: Symbolic a => a -> Reft

Generally Useful Refinements --------------------------

usymbolReft :: Symbolic a => a -> Reft

propReft :: Predicate a => a -> Reft

predReft :: Predicate a => a -> Reft

reftPred :: Reft -> Expr

reftBind :: Reft -> Symbol

Predicates

isFunctionSortedReft :: SortedReft -> Bool

Refinements ----------------------------------------------

functionSort :: Sort -> Maybe ([Int], [Sort], Sort)

isNonTrivial :: Reftable r => r -> Bool

isContraPred :: Expr -> Bool

isTautoPred :: Expr -> Bool

isSingletonExpr :: Symbol -> Expr -> Maybe Expr

isSingletonReft :: Reft -> Maybe Expr

Predicates ----------------------------------------------------------------

isFalse :: Falseable a => a -> Bool

Destructing

flattenRefas :: [Expr] -> [Expr]

conjuncts :: Expr -> [Expr]

eApps :: Expr -> [Expr] -> Expr

eAppC :: Sort -> Expr -> Expr -> Expr

splitEApp :: Expr -> (Expr, [Expr])

splitPAnd :: Expr -> [Expr]

reftConjuncts :: Reft -> [Reft]

Transforming

mapPredReft :: (Expr -> Expr) -> Reft -> Reft

pprintReft :: Tidy -> Reft -> Doc

debruijnIndex :: Expr -> Int

Gradual Type Manipulation

pGAnds :: [Expr] -> Expr

Gradual Type Manipulation ----------------------------

pGAnd :: Expr -> Expr -> Expr

class HasGradual a where

Minimal complete definition

isGradual

Methods

isGradual :: a -> Bool

gVars :: a -> [KVar]

ungrad :: a -> a

Instances

HasGradual SortedReft

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: SortedReft -> Bool

gVars :: SortedReft -> [KVar]

ungrad :: SortedReft -> SortedReft

HasGradual Reft

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: Reft -> Bool

gVars :: Reft -> [KVar]

ungrad :: Reft -> Reft

HasGradual Expr

Defined in Language.Fixpoint.Types.Refinements

Methods

isGradual :: Expr -> Bool

gVars :: Expr -> [KVar]

ungrad :: Expr -> Expr

HasGradual (WfC a)

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: WfC a -> Bool

gVars :: WfC a -> [KVar]

ungrad :: WfC a -> WfC a

HasGradual (GInfo c a)

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: GInfo c a -> Bool

gVars :: GInfo c a -> [KVar]

ungrad :: GInfo c a -> GInfo c a

srcGradInfo :: SourcePos -> GradInfo

Orphan instances

Binary SrcSpan

Methods

put :: SrcSpan -> Put

get :: Get SrcSpan

putList :: [SrcSpan] -> Put

NFData SrcSpan

Methods

rnf :: SrcSpan -> ()

PPrint Sort

Methods

pprintTidy :: Tidy -> Sort -> Doc

pprintPrec :: Int -> Tidy -> Sort -> Doc

(Eq a, Hashable a, Binary a) => Binary (TCEmb a)

Methods

put :: TCEmb a -> Put

get :: Get (TCEmb a)

putList :: [TCEmb a] -> Put

PPrint a => PPrint (TCEmb a)

Methods

pprintTidy :: Tidy -> TCEmb a -> Doc

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

(Hashable k, Eq k, Binary k, Binary v) => Binary (HashMap k v)

Methods

put :: HashMap k v -> Put

get :: Get (HashMap k v)

putList :: [HashMap k v] -> Put