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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Graduals

Description

This module contains the top-level SOLUTION data types, including various indices used for solving.

Synopsis

Documentation

uniquify :: (NFData a, Fixpoint a, Loc a) => SInfo a -> SInfo a Source #

Make each gradual appearence unique -------------------------------------

makeSolutions :: (NFData a, Fixpoint a, Show a) => Config -> SInfo a -> [(KVar, (GWInfo, [[Expr]]))] -> Maybe [GSol] Source #

data GSol Source #

Instances
Show GSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

showsPrec :: Int -> GSol -> ShowS #

show :: GSol -> String #

showList :: [GSol] -> ShowS #

Semigroup GSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

(<>) :: GSol -> GSol -> GSol #

sconcat :: NonEmpty GSol -> GSol #

stimes :: Integral b => b -> GSol -> GSol #

Monoid GSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

mempty :: GSol #

mappend :: GSol -> GSol -> GSol #

mconcat :: [GSol] -> GSol #

class Gradual a where Source #

Substitute Gradual Solution ---------------------------------------------

Methods

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

Instances
Gradual SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Gradual Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Reft -> Reft Source #

Gradual Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Expr -> Expr Source #

Gradual BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv -> BindEnv Source #

Gradual (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Gradual (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Gradual v => Gradual (HashMap k v) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> HashMap k v -> HashMap k v Source #