Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Refinements

Contents

Representing Terms
Constructing Terms
Generalizing Embedding with Typeclasses
Constructors
Predicates
Destructing
Transforming
Gradual Type Manipulation
Orphan instances

Description

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

Synopsis

newtype SymConst = SL Text
data Constant
- = I !Integer
- | R !Double
- | L !Text !Sort
data Bop
- = Plus
- | Minus
- | Times
- | Div
- | Mod
- | RTimes
- | RDiv
data Brel
- = Eq
- | Ne
- | Gt
- | Ge
- | Lt
- | Le
- | Ueq
- | Une
data ExprV v
- = ESym !SymConst
- | ECon !Constant
- | EVar !v
- | EApp !(ExprV v) !(ExprV v)
- | ENeg !(ExprV v)
- | EBin !Bop !(ExprV v) !(ExprV v)
- | EIte !(ExprV v) !(ExprV v) !(ExprV v)
- | ECst !(ExprV v) !Sort
- | ELam !(Symbol, Sort) !(ExprV v)
- | ETApp !(ExprV v) !Sort
- | ETAbs !(ExprV v) !Symbol
- | PAnd ![ExprV v]
- | POr ![ExprV v]
- | PNot !(ExprV v)
- | PImp !(ExprV v) !(ExprV v)
- | PIff !(ExprV v) !(ExprV v)
- | PAtom !Brel !(ExprV v) !(ExprV v)
- | PKVar !KVar !(SubstV v)
- | PAll ![(Symbol, Sort)] !(ExprV v)
- | PExist ![(Symbol, Sort)] !(ExprV v)
- | PGrad !KVar !(SubstV v) !GradInfo !(ExprV v)
- | ECoerc !Sort !Sort !(ExprV v)
type Pred = Expr
type Expr = ExprV Symbol
data GradInfo = GradInfo {
- gsrc :: SrcSpan
- gused :: Maybe SrcSpan
}
pattern PTrue :: ExprV v
pattern PTop :: ExprV v
pattern PFalse :: ExprV v
pattern EBot :: ExprV v
pattern ETimes :: ExprV v -> ExprV v -> ExprV v
pattern ERTimes :: ExprV v -> ExprV v -> ExprV v
pattern EDiv :: ExprV v -> ExprV v -> ExprV v
pattern ERDiv :: ExprV v -> ExprV v -> ExprV v
pattern EEq :: ExprV v -> ExprV v -> ExprV v
newtype KVar = KV {
- kv :: Symbol
}
type Subst = SubstV Symbol
newtype SubstV v = Su (HashMap Symbol (ExprV v))
data KVSub = KVS {
- ksuVV :: Symbol
- ksuSort :: Sort
- ksuKVar :: KVar
- ksuSubst :: Subst
}
type Reft = ReftV Symbol
newtype ReftV v = Reft (Symbol, ExprV v)
data SortedReft = RR {
- sr_sort :: !Sort
- sr_reft :: !Reft
}
eVar :: Symbolic a => a -> Expr
elit :: Located Symbol -> Sort -> Expr
eProp :: Symbolic a => a -> Expr
conj :: [Pred] -> Pred
pAnd :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pOr :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v
pAndNoDedup :: ListNE Pred -> Pred
(&.&) :: Pred -> Pred -> Pred
(|.|) :: Pred -> Pred -> Pred
pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v
mkEApp :: LocSymbol -> [Expr] -> Expr
mkProp :: Expr -> Pred
intKvar :: Integer -> KVar
vv_ :: Symbol
class Expression a where
- expr :: a -> Expr
class Predicate a where
- prop :: a -> Expr
class Subable a where
- syms :: a -> [Symbol]
- substa :: (Symbol -> Symbol) -> a -> a
- substf :: (Symbol -> Expr) -> a -> a
- subst :: Subst -> a -> a
- subst1 :: a -> (Symbol, Expr) -> a
reft :: Symbol -> ExprV v -> ReftV v
trueSortedReft :: Sort -> SortedReft
trueReft :: ReftV v
falseReft :: ReftV v
exprReft :: Expression a => a -> Reft
notExprReft :: Expression a => a -> Reft
uexprReft :: Expression a => a -> Reft
symbolReft :: Symbolic a => a -> Reft
usymbolReft :: Symbolic a => a -> Reft
propReft :: Predicate a => a -> Reft
predReft :: Predicate a => a -> Reft
reftPred :: ReftV v -> ExprV v
reftBind :: ReftV v -> Symbol
isFunctionSortedReft :: SortedReft -> Bool
functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
isNonTrivial :: SortedReft -> Bool
isContraPred :: Eq v => ExprV v -> Bool
isTautoPred :: Eq v => ExprV v -> Bool
isTautoReft :: Eq v => ReftV v -> Bool
isSingletonExpr :: Symbol -> Expr -> Maybe Expr
isSingletonReft :: Reft -> Maybe Expr
isFalse :: Falseable a => a -> Bool
flattenRefas :: [ExprV v] -> [ExprV v]
conjuncts :: Eq v => ExprV v -> [ExprV v]
concConjuncts :: Expr -> [Expr]
dropECst :: Expr -> Expr
eApps :: ExprV v -> [ExprV v] -> ExprV v
eAppC :: Sort -> Expr -> Expr -> Expr
eCst :: Expr -> Sort -> Expr
exprKVars :: Expr -> HashMap KVar [Subst]
exprSymbolsSet :: Expr -> HashSet Symbol
splitEApp :: ExprV v -> (ExprV v, [ExprV v])
splitEAppThroughECst :: Expr -> (Expr, [Expr])
splitPAnd :: Expr -> [Expr]
reftConjuncts :: Reft -> [Reft]
sortedReftSymbols :: SortedReft -> HashSet Symbol
substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
sortSubstInExpr :: SortSubst -> Expr -> Expr
mapPredReft :: (Expr -> Expr) -> Reft -> Reft
onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
pprintReft :: (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc
debruijnIndex :: Expr -> Int
pGAnds :: (Fixpoint v, Ord v) => [ExprV v] -> ExprV v
pGAnd :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v
class HasGradual a where
- isGradual :: a -> Bool
- gVars :: a -> [KVar]
- ungrad :: a -> a
srcGradInfo :: SourcePos -> GradInfo

Representing Terms

newtype SymConst Source #

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

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

Constructors

SL Text

Instances

Instances details

FromJSON SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser SymConst # parseJSONList :: Value -> Parser [SymConst] # omittedField :: Maybe SymConst #
ToJSON SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: SymConst -> Value # toEncoding :: SymConst -> Encoding # toJSONList :: [SymConst] -> Value # toEncodingList :: [SymConst] -> Encoding # omitField :: SymConst -> Bool #
Data SymConst Source #
Instance details 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 #
Generic SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep SymConst :: Type -> Type # Methods from :: SymConst -> Rep SymConst x # to :: Rep SymConst x -> SymConst #
Show SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> SymConst -> ShowS # show :: SymConst -> String # showList :: [SymConst] -> ShowS #
Binary SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: SymConst -> Put # get :: Get SymConst # putList :: [SymConst] -> Put #
NFData SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: SymConst -> () #
Eq SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: SymConst -> SymConst -> Bool # (/=) :: SymConst -> SymConst -> Bool #
Ord SymConst Source #
Instance details 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 #
Hashable SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> SymConst -> Int # hash :: SymConst -> Int #
SMTLIB2 SymConst Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> SymConst -> Builder Source #
Symbolic SymConst Source #	String Constants ---------------------------------------------------------- Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.
Instance details Defined in Language.Fixpoint.Types.Refinements Methods symbol :: SymConst -> Symbol Source #
Fixpoint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: SymConst -> Doc Source # simplify :: SymConst -> SymConst Source #
PPrint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc Source # pprintPrec :: Int -> Tidy -> SymConst -> Doc Source #
Store SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size SymConst # poke :: SymConst -> Poke () # peek :: Peek SymConst #
type Rep SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep SymConst = D1 ('MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'True) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

data Constant Source #

Constructors

I !Integer
R !Double
L !Text !Sort

Instances

Instances details

FromJSON Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser Constant # parseJSONList :: Value -> Parser [Constant] # omittedField :: Maybe Constant #
ToJSON Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: Constant -> Value # toEncoding :: Constant -> Encoding # toJSONList :: [Constant] -> Value # toEncodingList :: [Constant] -> Encoding # omitField :: Constant -> Bool #
Data Constant Source #
Instance details 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 #
Generic Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep Constant :: Type -> Type # Methods from :: Constant -> Rep Constant x # to :: Rep Constant x -> Constant #
Show Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Constant -> ShowS # show :: Constant -> String # showList :: [Constant] -> ShowS #
Binary Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: Constant -> Put # get :: Get Constant # putList :: [Constant] -> Put #
NFData Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: Constant -> () #
Eq Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Constant -> Constant -> Bool # (/=) :: Constant -> Constant -> Bool #
Ord Constant Source #
Instance details 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 #
Hashable Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Constant -> Int # hash :: Constant -> Int #
Inputable Constant Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Constant Source # rr' :: String -> String -> Constant Source #
SMTLIB2 Constant Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Constant -> Builder Source #
Fixpoint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Constant -> Doc Source # simplify :: Constant -> Constant Source #
PPrint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc Source # pprintPrec :: Int -> Tidy -> Constant -> Doc Source #
Store Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Constant # poke :: Constant -> Poke () # peek :: Peek Constant #
type Rep Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep Constant = D1 ('MetaData "Constant" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 Source #

Constructors

Plus
Minus
Times
Div
Mod
RTimes
RDiv

Instances

Instances details

FromJSON Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser Bop # parseJSONList :: Value -> Parser [Bop] # omittedField :: Maybe Bop #
ToJSON Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: Bop -> Value # toEncoding :: Bop -> Encoding # toJSONList :: [Bop] -> Value # toEncodingList :: [Bop] -> Encoding # omitField :: Bop -> Bool #
Data Bop Source #
Instance details 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 #
Generic Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep Bop :: Type -> Type # Methods from :: Bop -> Rep Bop x # to :: Rep Bop x -> Bop #
Show Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Bop -> ShowS # show :: Bop -> String # showList :: [Bop] -> ShowS #
Binary Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: Bop -> Put # get :: Get Bop # putList :: [Bop] -> Put #
NFData Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: Bop -> () #
Eq Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Bop -> Bop -> Bool # (/=) :: Bop -> Bop -> Bool #
Ord Bop Source #
Instance details 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 #
Hashable Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Bop -> Int # hash :: Bop -> Int #
SMTLIB2 Bop Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Bop -> Builder Source #
Fixpoint Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Bop -> Doc Source # simplify :: Bop -> Bop Source #
PPrint Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Bop -> Doc Source # pprintPrec :: Int -> Tidy -> Bop -> Doc Source #
Store Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Bop # poke :: Bop -> Poke () # peek :: Peek Bop #
type Rep Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep Bop = D1 ('MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 Source #

Constructors

Eq
Ne
Gt
Ge
Lt
Le
Ueq
Une

Instances

Instances details

FromJSON Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser Brel # parseJSONList :: Value -> Parser [Brel] # omittedField :: Maybe Brel #
ToJSON Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: Brel -> Value # toEncoding :: Brel -> Encoding # toJSONList :: [Brel] -> Value # toEncodingList :: [Brel] -> Encoding # omitField :: Brel -> Bool #
Data Brel Source #
Instance details 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 #
Generic Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep Brel :: Type -> Type # Methods from :: Brel -> Rep Brel x # to :: Rep Brel x -> Brel #
Show Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Brel -> ShowS # show :: Brel -> String # showList :: [Brel] -> ShowS #
Binary Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: Brel -> Put # get :: Get Brel # putList :: [Brel] -> Put #
NFData Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: Brel -> () #
Eq Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Brel -> Brel -> Bool # (/=) :: Brel -> Brel -> Bool #
Ord Brel Source #
Instance details 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 #
Hashable Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Brel -> Int # hash :: Brel -> Int #
SMTLIB2 Brel Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Brel -> Builder Source #
Fixpoint Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Brel -> Doc Source # simplify :: Brel -> Brel Source #
PPrint Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc Source # pprintPrec :: Int -> Tidy -> Brel -> Doc Source #
Store Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Brel # poke :: Brel -> Poke () # peek :: Peek Brel #
type Rep Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep Brel = D1 ('MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 ExprV v Source #

Constructors

ESym !SymConst
ECon !Constant
EVar !v
EApp !(ExprV v) !(ExprV v)
ENeg !(ExprV v)
EBin !Bop !(ExprV v) !(ExprV v)
EIte !(ExprV v) !(ExprV v) !(ExprV v)
ECst !(ExprV v) !Sort
ELam !(Symbol, Sort) !(ExprV v)
ETApp !(ExprV v) !Sort
ETAbs !(ExprV v) !Symbol
PAnd ![ExprV v]
POr ![ExprV v]
PNot !(ExprV v)
PImp !(ExprV v) !(ExprV v)
PIff !(ExprV v) !(ExprV v)
PAtom !Brel !(ExprV v) !(ExprV v)
PKVar !KVar !(SubstV v)
PAll ![(Symbol, Sort)] !(ExprV v)
PExist ![(Symbol, Sort)] !(ExprV v)
PGrad !KVar !(SubstV v) !GradInfo !(ExprV v)
ECoerc !Sort !Sort !(ExprV v)

Instances

Instances details

FromJSON Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser Expr # parseJSONList :: Value -> Parser [Expr] # omittedField :: Maybe Expr #
ToJSON Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: Expr -> Value # toEncoding :: Expr -> Encoding # toJSONList :: [Expr] -> Value # toEncodingList :: [Expr] -> Encoding # omitField :: Expr -> Bool #
Foldable ExprV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fold :: Monoid m => ExprV m -> m # foldMap :: Monoid m => (a -> m) -> ExprV a -> m # foldMap' :: Monoid m => (a -> m) -> ExprV a -> m # foldr :: (a -> b -> b) -> b -> ExprV a -> b # foldr' :: (a -> b -> b) -> b -> ExprV a -> b # foldl :: (b -> a -> b) -> b -> ExprV a -> b # foldl' :: (b -> a -> b) -> b -> ExprV a -> b # foldr1 :: (a -> a -> a) -> ExprV a -> a # foldl1 :: (a -> a -> a) -> ExprV a -> a # toList :: ExprV a -> [a] # null :: ExprV a -> Bool # length :: ExprV a -> Int # elem :: Eq a => a -> ExprV a -> Bool # maximum :: Ord a => ExprV a -> a # minimum :: Ord a => ExprV a -> a # sum :: Num a => ExprV a -> a # product :: Num a => ExprV a -> a #
Traversable ExprV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods traverse :: Applicative f => (a -> f b) -> ExprV a -> f (ExprV b) # sequenceA :: Applicative f => ExprV (f a) -> f (ExprV a) # mapM :: Monad m => (a -> m b) -> ExprV a -> m (ExprV b) # sequence :: Monad m => ExprV (m a) -> m (ExprV a) #
Functor ExprV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fmap :: (a -> b) -> ExprV a -> ExprV b # (<$) :: a -> ExprV b -> ExprV a #
Show GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods showsPrec :: Int -> GFixSolution -> ShowS # show :: GFixSolution -> String # showList :: [GFixSolution] -> ShowS #
NFData GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods rnf :: GFixSolution -> () #
Defunc Expr Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Expr -> DF Expr Source #
ToHornSMT Expr Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Expr -> Doc Source #
Inputable Expr Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Expr Source # rr' :: String -> String -> Expr Source #
SMTLIB2 Expr Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Expr -> Builder Source #
Simplifiable Expr Source #
Instance details Defined in Language.Fixpoint.Solver.Interpreter Methods simplify :: Knowledge -> ICtx -> Expr -> Expr Source #
Elaborate Expr Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: ElabParam -> Expr -> Expr Source #
Gradual Expr Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: ElabFlags -> GSol -> Expr -> Expr Source #
PPrint GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc Source # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc Source #
Expression Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Expr -> Expr Source #
HasGradual Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: Expr -> Bool Source # gVars :: Expr -> [KVar] Source # ungrad :: Expr -> Expr Source #
Predicate Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Expr -> Expr Source #
Subable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Expr -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Expr -> Expr Source # substf :: (Symbol -> Expr) -> Expr -> Expr Source # subst :: Subst -> Expr -> Expr Source # subst1 :: Expr -> (Symbol, Expr) -> Expr Source #
Foldable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Expr -> FoldM a Expr Source #
SymConsts Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Expr -> [SymConst] Source #
Visitable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Expr -> Expr Source #
Store GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods size :: Size GFixSolution # poke :: GFixSolution -> Poke () # peek :: Peek GFixSolution #
Store Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Expr # poke :: Expr -> Poke () # peek :: Peek Expr #
Data v => Data (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExprV v -> c (ExprV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ExprV v) # toConstr :: ExprV v -> Constr # dataTypeOf :: ExprV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ExprV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v)) # gmapT :: (forall b. Data b => b -> b) -> ExprV v -> ExprV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprV v -> r # gmapQ :: (forall d. Data d => d -> u) -> ExprV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v) #
Generic (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep (ExprV v) :: Type -> Type # Methods from :: ExprV v -> Rep (ExprV v) x # to :: Rep (ExprV v) x -> ExprV v #
(Show v, Fixpoint v, Ord v) => Show (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> ExprV v -> ShowS # show :: ExprV v -> String # showList :: [ExprV v] -> ShowS #
Binary v => Binary (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: ExprV v -> Put # get :: Get (ExprV v) # putList :: [ExprV v] -> Put #
NFData v => NFData (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: ExprV v -> () #
Eq v => Eq (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: ExprV v -> ExprV v -> Bool # (/=) :: ExprV v -> ExprV v -> Bool #
Ord v => Ord (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: ExprV v -> ExprV v -> Ordering # (<) :: ExprV v -> ExprV v -> Bool # (<=) :: ExprV v -> ExprV v -> Bool # (>) :: ExprV v -> ExprV v -> Bool # (>=) :: ExprV v -> ExprV v -> Bool # max :: ExprV v -> ExprV v -> ExprV v # min :: ExprV v -> ExprV v -> ExprV v #
Hashable v => Hashable (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> ExprV v -> Int # hash :: ExprV v -> Int #
SMTLIB2 (Triggered Expr) Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
(Ord v, Fixpoint v) => Fixpoint (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: ExprV v -> Doc Source # simplify :: ExprV v -> ExprV v Source #
(Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> ExprV v -> Doc Source # pprintPrec :: Int -> Tidy -> ExprV v -> Doc Source #
Inputable (FixResult Integer, FixSolution) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
type Rep (ExprV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep (ExprV v) = D1 ('MetaData "ExprV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 v)) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "ENeg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "EBin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bop) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: (C1 ('MetaCons "EIte" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: C1 ('MetaCons "ECst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: 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 (ExprV v))) :+: (C1 ('MetaCons "ETApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :+: C1 ('MetaCons "ETAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)))))) :+: (((C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v])) :+: C1 ('MetaCons "POr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [ExprV v]))) :+: (C1 ('MetaCons "PNot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: (C1 ('MetaCons "PImp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v))) :+: C1 ('MetaCons "PIff" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))))) :+: ((C1 ('MetaCons "PAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Brel) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: (C1 ('MetaCons "PKVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SubstV v))) :+: 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 (ExprV v))))) :+: (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 (ExprV v))) :+: (C1 ('MetaCons "PGrad" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SubstV v))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 GradInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)))) :+: 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 (ExprV v)))))))))

type Pred = Expr Source #

type Expr = ExprV Symbol Source #

data GradInfo Source #

Constructors

GradInfo
Fields gsrc :: SrcSpan gused :: Maybe SrcSpan

Instances

Instances details

FromJSON GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser GradInfo # parseJSONList :: Value -> Parser [GradInfo] # omittedField :: Maybe GradInfo #
ToJSON GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: GradInfo -> Value # toEncoding :: GradInfo -> Encoding # toJSONList :: [GradInfo] -> Value # toEncodingList :: [GradInfo] -> Encoding # omitField :: GradInfo -> Bool #
Data GradInfo Source #
Instance details 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 #
Generic GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep GradInfo :: Type -> Type # Methods from :: GradInfo -> Rep GradInfo x # to :: Rep GradInfo x -> GradInfo #
Show GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> GradInfo -> ShowS # show :: GradInfo -> String # showList :: [GradInfo] -> ShowS #
Binary GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: GradInfo -> Put # get :: Get GradInfo # putList :: [GradInfo] -> Put #
NFData GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: GradInfo -> () #
Eq GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: GradInfo -> GradInfo -> Bool # (/=) :: GradInfo -> GradInfo -> Bool #
Ord GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: GradInfo -> GradInfo -> Ordering # (<) :: GradInfo -> GradInfo -> Bool # (<=) :: GradInfo -> GradInfo -> Bool # (>) :: GradInfo -> GradInfo -> Bool # (>=) :: GradInfo -> GradInfo -> Bool # max :: GradInfo -> GradInfo -> GradInfo # min :: GradInfo -> GradInfo -> GradInfo #
Hashable GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> GradInfo -> Int # hash :: GradInfo -> Int #
Store GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size GradInfo # poke :: GradInfo -> Poke () # peek :: Peek GradInfo #
type Rep GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep GradInfo = D1 ('MetaData "GradInfo" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 :: ExprV v Source #

pattern PTop :: ExprV v Source #

pattern PFalse :: ExprV v Source #

pattern EBot :: ExprV v Source #

pattern ETimes :: ExprV v -> ExprV v -> ExprV v Source #

pattern ERTimes :: ExprV v -> ExprV v -> ExprV v Source #

pattern EDiv :: ExprV v -> ExprV v -> ExprV v Source #

pattern ERDiv :: ExprV v -> ExprV v -> ExprV v Source #

pattern EEq :: ExprV v -> ExprV v -> ExprV v Source #

newtype KVar Source #

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

Constructors

KV
Fields kv :: Symbol

Instances

Instances details

FromJSON KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser KVar # parseJSONList :: Value -> Parser [KVar] # omittedField :: Maybe KVar #
ToJSON KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: KVar -> Value # toEncoding :: KVar -> Encoding # toJSONList :: [KVar] -> Value # toEncodingList :: [KVar] -> Encoding # omitField :: KVar -> Bool #
Data KVar Source #
Instance details 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 #
IsString KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fromString :: String -> KVar #
Generic KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep KVar :: Type -> Type # Methods from :: KVar -> Rep KVar x # to :: Rep KVar x -> KVar #
Show KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> KVar -> ShowS # show :: KVar -> String # showList :: [KVar] -> ShowS #
Binary KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: KVar -> Put # get :: Get KVar # putList :: [KVar] -> Put #
NFData KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: KVar -> () #
Eq KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: KVar -> KVar -> Bool # (/=) :: KVar -> KVar -> Bool #
Ord KVar Source #
Instance details 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 #
Hashable KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> KVar -> Int # hash :: KVar -> Int #
ToHornSMT KVar Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: KVar -> Doc Source #
Fixpoint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: KVar -> Doc Source # simplify :: KVar -> KVar Source #
PPrint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc Source # pprintPrec :: Int -> Tidy -> KVar -> Doc Source #
Store KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size KVar # poke :: KVar -> Poke () # peek :: Peek KVar #
Inputable (FixResult Integer, FixSolution) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
type Rep KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'True) (C1 ('MetaCons "KV" 'PrefixI 'True) (S1 ('MetaSel ('Just "kv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

type Subst = SubstV Symbol Source #

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

newtype SubstV v Source #

Constructors

Su (HashMap Symbol (ExprV v))

Instances

Instances details

FromJSON Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods parseJSON :: Value -> Parser Subst # parseJSONList :: Value -> Parser [Subst] # omittedField :: Maybe Subst #
ToJSON Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toJSON :: Subst -> Value # toEncoding :: Subst -> Encoding # toJSONList :: [Subst] -> Value # toEncodingList :: [Subst] -> Encoding # omitField :: Subst -> Bool #
Foldable SubstV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fold :: Monoid m => SubstV m -> m # foldMap :: Monoid m => (a -> m) -> SubstV a -> m # foldMap' :: Monoid m => (a -> m) -> SubstV a -> m # foldr :: (a -> b -> b) -> b -> SubstV a -> b # foldr' :: (a -> b -> b) -> b -> SubstV a -> b # foldl :: (b -> a -> b) -> b -> SubstV a -> b # foldl' :: (b -> a -> b) -> b -> SubstV a -> b # foldr1 :: (a -> a -> a) -> SubstV a -> a # foldl1 :: (a -> a -> a) -> SubstV a -> a # toList :: SubstV a -> [a] # null :: SubstV a -> Bool # length :: SubstV a -> Int # elem :: Eq a => a -> SubstV a -> Bool # maximum :: Ord a => SubstV a -> a # minimum :: Ord a => SubstV a -> a # sum :: Num a => SubstV a -> a # product :: Num a => SubstV a -> a #
Traversable SubstV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods traverse :: Applicative f => (a -> f b) -> SubstV a -> f (SubstV b) # sequenceA :: Applicative f => SubstV (f a) -> f (SubstV a) # mapM :: Monad m => (a -> m b) -> SubstV a -> m (SubstV b) # sequence :: Monad m => SubstV (m a) -> m (SubstV a) #
Functor SubstV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fmap :: (a -> b) -> SubstV a -> SubstV b # (<$) :: a -> SubstV b -> SubstV a #
Monoid Subst Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods mempty :: Subst # mappend :: Subst -> Subst -> Subst # mconcat :: [Subst] -> Subst #
Semigroup Subst Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods (<>) :: Subst -> Subst -> Subst # sconcat :: NonEmpty Subst -> Subst # stimes :: Integral b => b -> Subst -> Subst #
ToHornSMT Subst Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toHornSMT :: Subst -> Doc Source #
Store Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Subst # poke :: Subst -> Poke () # peek :: Peek Subst #
Data v => Data (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SubstV v -> c (SubstV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SubstV v) # toConstr :: SubstV v -> Constr # dataTypeOf :: SubstV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SubstV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v)) # gmapT :: (forall b. Data b => b -> b) -> SubstV v -> SubstV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SubstV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SubstV v -> r # gmapQ :: (forall d. Data d => d -> u) -> SubstV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SubstV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v) #
Generic (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep (SubstV v) :: Type -> Type # Methods from :: SubstV v -> Rep (SubstV v) x # to :: Rep (SubstV v) x -> SubstV v #
(Fixpoint v, Ord v, Show v) => Show (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> SubstV v -> ShowS # show :: SubstV v -> String # showList :: [SubstV v] -> ShowS #
Binary v => Binary (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: SubstV v -> Put # get :: Get (SubstV v) # putList :: [SubstV v] -> Put #
NFData v => NFData (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: SubstV v -> () #
Eq v => Eq (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: SubstV v -> SubstV v -> Bool # (/=) :: SubstV v -> SubstV v -> Bool #
Ord v => Ord (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: SubstV v -> SubstV v -> Ordering # (<) :: SubstV v -> SubstV v -> Bool # (<=) :: SubstV v -> SubstV v -> Bool # (>) :: SubstV v -> SubstV v -> Bool # (>=) :: SubstV v -> SubstV v -> Bool # max :: SubstV v -> SubstV v -> SubstV v # min :: SubstV v -> SubstV v -> SubstV v #
Hashable v => Hashable (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> SubstV v -> Int # hash :: SubstV v -> Int #
(Ord v, Fixpoint v) => Fixpoint (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: SubstV v -> Doc Source # simplify :: SubstV v -> SubstV v Source #
(Ord v, Fixpoint v) => PPrint (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SubstV v -> Doc Source # pprintPrec :: Int -> Tidy -> SubstV v -> Doc Source #
type Rep (SubstV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep (SubstV v) = D1 ('MetaData "SubstV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'True) (C1 ('MetaCons "Su" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol (ExprV v)))))

data KVSub Source #

Constructors

KVS
Fields ksuVV :: Symbol ksuSort :: Sort ksuKVar :: KVar ksuSubst :: Subst

Instances

Instances details

Data KVSub Source #
Instance details 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 #
Generic KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep KVSub :: Type -> Type # Methods from :: KVSub -> Rep KVSub x # to :: Rep KVSub x -> KVSub #
Show KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> KVSub -> ShowS # show :: KVSub -> String # showList :: [KVSub] -> ShowS #
Eq KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: KVSub -> KVSub -> Bool # (/=) :: KVSub -> KVSub -> Bool #
PPrint KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVSub -> Doc Source # pprintPrec :: Int -> Tidy -> KVSub -> Doc Source #
type Rep KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep KVSub = D1 ('MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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))))

type Reft = ReftV Symbol Source #

newtype ReftV v Source #

Refinement of v satisfying a predicate e.g. in '{x: _ | e }' x is the Symbol and e the ExprV v

Constructors

Reft (Symbol, ExprV v)

Instances

Instances details

Foldable ReftV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fold :: Monoid m => ReftV m -> m # foldMap :: Monoid m => (a -> m) -> ReftV a -> m # foldMap' :: Monoid m => (a -> m) -> ReftV a -> m # foldr :: (a -> b -> b) -> b -> ReftV a -> b # foldr' :: (a -> b -> b) -> b -> ReftV a -> b # foldl :: (b -> a -> b) -> b -> ReftV a -> b # foldl' :: (b -> a -> b) -> b -> ReftV a -> b # foldr1 :: (a -> a -> a) -> ReftV a -> a # foldl1 :: (a -> a -> a) -> ReftV a -> a # toList :: ReftV a -> [a] # null :: ReftV a -> Bool # length :: ReftV a -> Int # elem :: Eq a => a -> ReftV a -> Bool # maximum :: Ord a => ReftV a -> a # minimum :: Ord a => ReftV a -> a # sum :: Num a => ReftV a -> a # product :: Num a => ReftV a -> a #
Traversable ReftV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods traverse :: Applicative f => (a -> f b) -> ReftV a -> f (ReftV b) # sequenceA :: Applicative f => ReftV (f a) -> f (ReftV a) # mapM :: Monad m => (a -> m b) -> ReftV a -> m (ReftV b) # sequence :: Monad m => ReftV (m a) -> m (ReftV a) #
Functor ReftV Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods fmap :: (a -> b) -> ReftV a -> ReftV b # (<$) :: a -> ReftV b -> ReftV a #
Show Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods showsPrec :: Int -> Reft -> ShowS # show :: Reft -> String # showList :: [Reft] -> ShowS #
Defunc Reft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Reft -> DF Reft Source #
Gradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: ElabFlags -> GSol -> Reft -> Reft Source #
Fixpoint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: Reft -> Doc Source # simplify :: Reft -> Reft Source #
Expression Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Reft -> Expr Source #
HasGradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: Reft -> Bool Source # gVars :: Reft -> [KVar] Source # ungrad :: Reft -> Reft Source #
Subable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Reft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Reft -> Reft Source # substf :: (Symbol -> Expr) -> Reft -> Reft Source # subst :: Subst -> Reft -> Reft Source # subst1 :: Reft -> (Symbol, Expr) -> Reft Source #
Foldable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> Reft -> FoldM a Reft Source #
SymConsts Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: Reft -> [SymConst] Source #
Visitable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> Reft -> Reft Source #
Store Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Reft # poke :: Reft -> Poke () # peek :: Peek Reft #
Data v => Data (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ReftV v -> c (ReftV v) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ReftV v) # toConstr :: ReftV v -> Constr # dataTypeOf :: ReftV v -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ReftV v)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v)) # gmapT :: (forall b. Data b => b -> b) -> ReftV v -> ReftV v # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ReftV v -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ReftV v -> r # gmapQ :: (forall d. Data d => d -> u) -> ReftV v -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ReftV v -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v) #
Generic (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep (ReftV v) :: Type -> Type # Methods from :: ReftV v -> Rep (ReftV v) x # to :: Rep (ReftV v) x -> ReftV v #
Binary v => Binary (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: ReftV v -> Put # get :: Get (ReftV v) # putList :: [ReftV v] -> Put #
NFData v => NFData (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: ReftV v -> () #
Eq v => Eq (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: ReftV v -> ReftV v -> Bool # (/=) :: ReftV v -> ReftV v -> Bool #
Ord v => Ord (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: ReftV v -> ReftV v -> Ordering # (<) :: ReftV v -> ReftV v -> Bool # (<=) :: ReftV v -> ReftV v -> Bool # (>) :: ReftV v -> ReftV v -> Bool # (>=) :: ReftV v -> ReftV v -> Bool # max :: ReftV v -> ReftV v -> ReftV v # min :: ReftV v -> ReftV v -> ReftV v #
Hashable v => Hashable (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> ReftV v -> Int # hash :: ReftV v -> Int #
(PPrint v, Fixpoint v, Ord v) => PPrint (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> ReftV v -> Doc Source # pprintPrec :: Int -> Tidy -> ReftV v -> Doc Source #
type Rep (ReftV v) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep (ReftV v) = D1 ('MetaData "ReftV" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" 'True) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, ExprV v))))

data SortedReft Source #

Constructors

RR
Fields sr_sort :: !Sort sr_reft :: !Reft

Instances

Instances details

Data SortedReft Source #
Instance details 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 #
Generic SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep SortedReft :: Type -> Type # Methods from :: SortedReft -> Rep SortedReft x # to :: Rep SortedReft x -> SortedReft #
Show SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods showsPrec :: Int -> SortedReft -> ShowS # show :: SortedReft -> String # showList :: [SortedReft] -> ShowS #
NFData SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: SortedReft -> () #
Eq SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: SortedReft -> SortedReft -> Bool # (/=) :: SortedReft -> SortedReft -> Bool #
Ord SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: SortedReft -> SortedReft -> Ordering # (<) :: SortedReft -> SortedReft -> Bool # (<=) :: SortedReft -> SortedReft -> Bool # (>) :: SortedReft -> SortedReft -> Bool # (>=) :: SortedReft -> SortedReft -> Bool # max :: SortedReft -> SortedReft -> SortedReft # min :: SortedReft -> SortedReft -> SortedReft #
Hashable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> SortedReft -> Int # hash :: SortedReft -> Int #
Defunc SortedReft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SortedReft -> DF SortedReft Source #
Elaborate SortedReft Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: ElabParam -> SortedReft -> SortedReft Source #
Gradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: ElabFlags -> GSol -> SortedReft -> SortedReft Source #
Fixpoint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
PPrint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
Expression SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: SortedReft -> Expr Source #
HasGradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: SortedReft -> Bool Source # gVars :: SortedReft -> [KVar] Source # ungrad :: SortedReft -> SortedReft Source #
Subable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: SortedReft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft Source # substf :: (Symbol -> Expr) -> SortedReft -> SortedReft Source # subst :: Subst -> SortedReft -> SortedReft Source # subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft Source #
Foldable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a => Folder a c -> c -> SortedReft -> FoldM a SortedReft Source #
SymConsts SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SortedReft -> [SymConst] Source #
Visitable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> SortedReft -> SortedReft Source #
Store SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size SortedReft # poke :: SortedReft -> Poke () # peek :: Peek SortedReft #
Monoid (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: BindEnv a # mappend :: BindEnv a -> BindEnv a -> BindEnv a # mconcat :: [BindEnv a] -> BindEnv a #
Semigroup (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (<>) :: BindEnv a -> BindEnv a -> BindEnv a # sconcat :: NonEmpty (BindEnv a) -> BindEnv a # stimes :: Integral b => b -> BindEnv a -> BindEnv a #
NFData a => NFData (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods rnf :: BindEnv a -> () #
Defunc (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: BindEnv a -> DF (BindEnv a) Source #
Loc a => Elaborate (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: ElabParam -> BindEnv a -> BindEnv a Source #
Gradual (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: ElabFlags -> GSol -> BindEnv a -> BindEnv a Source #
Fixpoint (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: BindEnv a -> Doc Source # simplify :: BindEnv a -> BindEnv a Source #
Foldable (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> BindEnv a -> FoldM a0 (BindEnv a) Source #
SymConsts (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: BindEnv a -> [SymConst] Source #
Visitable (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> BindEnv a -> BindEnv a Source #
Store a => Store (BindEnv a) Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods size :: Size (BindEnv a) # poke :: BindEnv a -> Poke () # peek :: Peek (BindEnv a) #
Defunc (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) Source #
Expression (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods expr :: (Symbol, SortedReft) -> Expr Source #
Foldable (Symbol, SortedReft, a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods foldE :: Monoid a0 => Folder a0 c -> c -> (Symbol, SortedReft, a) -> FoldM a0 (Symbol, SortedReft, a) Source #
Visitable (Symbol, SortedReft, a) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods transE :: (Expr -> Expr) -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a) Source #
type Rep SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep SortedReft = D1 ('MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.6.3.2-4tsgPlidRgw727KfDpGHMc" '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 Source #

elit :: Located Symbol -> Sort -> Expr Source #

eProp :: Symbolic a => a -> Expr Source #

conj :: [Pred] -> Pred Source #

conj is a fast version of pAnd needed for the ebind tests

pAnd :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v Source #

NOTE: pAnd-SLOW: pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

pOr :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v Source #

NOTE: pAnd-SLOW: pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v Source #

pAndNoDedup :: ListNE Pred -> Pred Source #

(&.&) :: Pred -> Pred -> Pred infixl 9 Source #

(|.|) :: Pred -> Pred -> Pred infixl 9 Source #

pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v Source #

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

mkProp :: Expr -> Pred Source #

intKvar :: Integer -> KVar Source #

vv_ :: Symbol Source #

Generalizing Embedding with Typeclasses

class Expression a where Source #

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

Values that can be viewed as Constants

Values that can be viewed as Expressions

Methods

expr :: a -> Expr Source #

Instances

Instances details

Expression Symbol Source #	The symbol may be an encoding of a SymConst.
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Symbol -> Expr Source #
Expression Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Expr -> Expr Source #
Expression Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Reft -> Expr Source #
Expression SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: SortedReft -> Expr Source #
Expression Text Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Text -> Expr Source #
Expression Integer Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Integer -> Expr Source #
Expression Int Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Int -> Expr Source #
Expression a => Expression (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Located a -> Expr Source #
Expression (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods expr :: (Symbol, SortedReft) -> Expr Source #

class Predicate a where Source #

Values that can be viewed as Predicates

Methods

prop :: a -> Expr Source #

Instances

Instances details

Predicate Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Symbol -> Expr Source #
Predicate Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Expr -> Expr Source #
Predicate Bool Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Bool -> Expr Source #

class Subable a where Source #

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

Minimal complete definition

syms, substa, substf, subst

Methods

syms Source #

Arguments

:: a
-> [Symbol]	free symbols of a

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

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

subst :: Subst -> a -> a Source #

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

Instances

Instances details

Subable Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Pred -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Pred -> Pred Source # substf :: (Symbol -> Expr) -> Pred -> Pred Source # subst :: Subst -> Pred -> Pred Source # subst1 :: Pred -> (Symbol, Expr) -> Pred Source #
Subable Equation Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods syms :: Equation -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Equation -> Equation Source # substf :: (Symbol -> Expr) -> Equation -> Equation Source # subst :: Subst -> Equation -> Equation Source # subst1 :: Equation -> (Symbol, Expr) -> Equation Source #
Subable Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods syms :: Qualifier -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier Source # substf :: (Symbol -> Expr) -> Qualifier -> Qualifier Source # subst :: Subst -> Qualifier -> Qualifier Source # subst1 :: Qualifier -> (Symbol, Expr) -> Qualifier Source #
Subable Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Symbol -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Symbol -> Symbol Source # substf :: (Symbol -> Expr) -> Symbol -> Symbol Source # subst :: Subst -> Symbol -> Symbol Source # subst1 :: Symbol -> (Symbol, Expr) -> Symbol Source #
Subable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Expr -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Expr -> Expr Source # substf :: (Symbol -> Expr) -> Expr -> Expr Source # subst :: Subst -> Expr -> Expr Source # subst1 :: Expr -> (Symbol, Expr) -> Expr Source #
Subable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Reft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Reft -> Reft Source # substf :: (Symbol -> Expr) -> Reft -> Reft Source # subst :: Subst -> Reft -> Reft Source # subst1 :: Reft -> (Symbol, Expr) -> Reft Source #
Subable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: SortedReft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft Source # substf :: (Symbol -> Expr) -> SortedReft -> SortedReft Source # subst :: Subst -> SortedReft -> SortedReft Source # subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft Source #
Subable () Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: () -> [Symbol] Source # substa :: (Symbol -> Symbol) -> () -> () Source # substf :: (Symbol -> Expr) -> () -> () Source # subst :: Subst -> () -> () Source # subst1 :: () -> (Symbol, Expr) -> () Source #
Subable (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Bind a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Bind a -> Bind a Source # substf :: (Symbol -> Expr) -> Bind a -> Bind a Source # subst :: Subst -> Bind a -> Bind a Source # subst1 :: Bind a -> (Symbol, Expr) -> Bind a Source #
Subable a => Subable (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods syms :: Located a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Located a -> Located a Source # substf :: (Symbol -> Expr) -> Located a -> Located a Source # subst :: Subst -> Located a -> Located a Source # subst1 :: Located a -> (Symbol, Expr) -> Located a Source #
Subable a => Subable (Maybe a) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Maybe a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a Source # substf :: (Symbol -> Expr) -> Maybe a -> Maybe a Source # subst :: Subst -> Maybe a -> Maybe a Source # subst1 :: Maybe a -> (Symbol, Expr) -> Maybe a Source #
Subable a => Subable [a] Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: [a] -> [Symbol] Source # substa :: (Symbol -> Symbol) -> [a] -> [a] Source # substf :: (Symbol -> Expr) -> [a] -> [a] Source # subst :: Subst -> [a] -> [a] Source # subst1 :: [a] -> (Symbol, Expr) -> [a] Source #
Subable a => Subable (HashMap k a) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: HashMap k a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a Source # substf :: (Symbol -> Expr) -> HashMap k a -> HashMap k a Source # subst :: Subst -> HashMap k a -> HashMap k a Source # subst1 :: HashMap k a -> (Symbol, Expr) -> HashMap k a Source #
(Subable a, Subable b) => Subable (a, b) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: (a, b) -> [Symbol] Source # substa :: (Symbol -> Symbol) -> (a, b) -> (a, b) Source # substf :: (Symbol -> Expr) -> (a, b) -> (a, b) Source # subst :: Subst -> (a, b) -> (a, b) Source # subst1 :: (a, b) -> (Symbol, Expr) -> (a, b) Source #

Constructors

reft :: Symbol -> ExprV v -> ReftV v Source #

trueSortedReft :: Sort -> SortedReft Source #

trueReft :: ReftV v Source #

falseReft :: ReftV v Source #

exprReft :: Expression a => a -> Reft Source #

notExprReft :: Expression a => a -> Reft Source #

uexprReft :: Expression a => a -> Reft Source #

symbolReft :: Symbolic a => a -> Reft Source #

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

usymbolReft :: Symbolic a => a -> Reft Source #

propReft :: Predicate a => a -> Reft Source #

predReft :: Predicate a => a -> Reft Source #

reftPred :: ReftV v -> ExprV v Source #

reftBind :: ReftV v -> Symbol Source #

Predicates

isFunctionSortedReft :: SortedReft -> Bool Source #

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

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

isNonTrivial :: SortedReft -> Bool Source #

isContraPred :: Eq v => ExprV v -> Bool Source #

isTautoPred :: Eq v => ExprV v -> Bool Source #

isTautoReft :: Eq v => ReftV v -> Bool Source #

isSingletonExpr :: Symbol -> Expr -> Maybe Expr Source #

isSingletonReft :: Reft -> Maybe Expr Source #

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

isFalse :: Falseable a => a -> Bool Source #

Destructing

flattenRefas :: [ExprV v] -> [ExprV v] Source #

conjuncts :: Eq v => ExprV v -> [ExprV v] Source #

concConjuncts :: Expr -> [Expr] Source #

dropECst :: Expr -> Expr Source #

eApps :: ExprV v -> [ExprV v] -> ExprV v Source #

eAppC :: Sort -> Expr -> Expr -> Expr Source #

eCst :: Expr -> Sort -> Expr Source #

Eliminates redundant casts

exprKVars :: Expr -> HashMap KVar [Subst] Source #

exprSymbolsSet :: Expr -> HashSet Symbol Source #

splitEApp :: ExprV v -> (ExprV v, [ExprV v]) Source #

splitEAppThroughECst :: Expr -> (Expr, [Expr]) Source #

splitPAnd :: Expr -> [Expr] Source #

reftConjuncts :: Reft -> [Reft] Source #

sortedReftSymbols :: SortedReft -> HashSet Symbol Source #

substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr Source #

sortSubstInExpr :: SortSubst -> Expr -> Expr Source #

Transforming

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

onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr Source #

pprintReft :: (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc Source #

debruijnIndex :: Expr -> Int Source #

Gradual Type Manipulation

pGAnds :: (Fixpoint v, Ord v) => [ExprV v] -> ExprV v Source #

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

pGAnd :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v Source #

class HasGradual a where Source #

Minimal complete definition

isGradual

Methods

isGradual :: a -> Bool Source #

gVars :: a -> [KVar] Source #

ungrad :: a -> a Source #

Instances

Instances details

HasGradual Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: Expr -> Bool Source # gVars :: Expr -> [KVar] Source # ungrad :: Expr -> Expr Source #
HasGradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: Reft -> Bool Source # gVars :: Reft -> [KVar] Source # ungrad :: Reft -> Reft Source #
HasGradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: SortedReft -> Bool Source # gVars :: SortedReft -> [KVar] Source # ungrad :: SortedReft -> SortedReft Source #
HasGradual (WfC a) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods isGradual :: WfC a -> Bool Source # gVars :: WfC a -> [KVar] Source # ungrad :: WfC a -> WfC a Source #
HasGradual (GInfo c a) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods isGradual :: GInfo c a -> Bool Source # gVars :: GInfo c a -> [KVar] Source # ungrad :: GInfo c a -> GInfo c a Source #

srcGradInfo :: SourcePos -> GradInfo Source #

Orphan instances

Fixpoint Doc Source #
Instance details Methods toFix :: Doc -> Doc Source # simplify :: Doc -> Doc Source #
(Hashable a, Eq a, Binary a) => Binary (HashSet a) Source #
Instance details Methods put :: HashSet a -> Put # get :: Get (HashSet a) # putList :: [HashSet a] -> Put #
(Hashable k, Eq k, Binary k, Binary v) => Binary (HashMap k v) Source #
Instance details Methods put :: HashMap k v -> Put # get :: Get (HashMap k v) # putList :: [HashMap k v] -> Put #