Language.Fixpoint.Types.Graduals

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

Documentation

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

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

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

data GSol

Instances

Show GSol

Defined in Language.Fixpoint.Types.Graduals

Methods

showsPrec :: Int -> GSol -> ShowS

show :: GSol -> String

showList :: [GSol] -> ShowS

Semigroup GSol

Defined in Language.Fixpoint.Types.Graduals

Methods

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

sconcat :: NonEmpty GSol -> GSol

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

Monoid GSol

Defined in Language.Fixpoint.Types.Graduals

Methods

mempty :: GSol

mappend :: GSol -> GSol -> GSol

mconcat :: [GSol] -> GSol

class Gradual a where

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

Methods

gsubst :: GSol -> a -> a

Instances

Gradual SortedReft

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> SortedReft -> SortedReft

Gradual Reft

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Reft -> Reft

Gradual Expr

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> Expr -> Expr

Gradual BindEnv

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv -> BindEnv

Gradual (SInfo a)

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Gradual (SimpC a)

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Gradual v => Gradual (HashMap k v)

Defined in Language.Fixpoint.Types.Graduals

Methods

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