Language.Fixpoint.Horn.Types

This module formalizes the key datatypes needed to represent Horn NNF constraints as described in "Local Refinement Typing", ICFP 2017

Horn Constraints and their components

data Query a

Query is an NNF Horn Constraint.

Constructors

Query

Fields

• qQuals :: ![Qualifier]

  qualifiers over which to solve cstrs

• qVars :: ![Var a]

  kvars, with parameter-sorts

• qCstr :: !(Cstr a)

  list of constraints

• qCon :: HashMap Symbol Sort

  list of constants (uninterpreted functions)

• qDis :: HashMap Symbol Sort

  list of *distinct* constants (uninterpreted functions)

• qEqns :: ![Equation]

  list of equations

• qMats :: ![Rewrite]

  list of match-es

• qData :: ![DataDecl]

  list of data-declarations

• qOpts :: ![String]

  list of fixpoint options

• qNums :: ![Symbol]

  list of numeric TyCon (?)

Instances

Functor Query

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser (Query a)

parseJSONList :: Value -> Parser [Query a]

omittedField :: Maybe (Query a)

ToJSON a => ToJSON (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Query a -> Value

toEncoding :: Query a -> Encoding

toJSONList :: [Query a] -> Value

toEncodingList :: [Query a] -> Encoding

omitField :: Query a -> Bool

Data a => Data (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Query a -> Constr

dataTypeOf :: Query a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Query a -> Query a

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

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

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

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

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

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

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

Generic (Query a)

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Query a) :: Type -> Type

Methods

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

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

ToHornSMT (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Query a -> Doc

PPrint (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Query a -> Doc

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

type Rep (Query a)

Defined in Language.Fixpoint.Horn.Types

type Rep (Query a) = D1 ('MetaData "Query" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) (C1 ('MetaCons "Query" 'PrefixI 'True) (((S1 ('MetaSel ('Just "qQuals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :*: S1 ('MetaSel ('Just "qVars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Var a])) :*: (S1 ('MetaSel ('Just "qCstr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a)) :*: (S1 ('MetaSel ('Just "qCon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Sort)) :*: S1 ('MetaSel ('Just "qDis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Sort))))) :*: ((S1 ('MetaSel ('Just "qEqns") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]) :*: S1 ('MetaSel ('Just "qMats") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Rewrite])) :*: (S1 ('MetaSel ('Just "qData") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :*: (S1 ('MetaSel ('Just "qOpts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [String]) :*: S1 ('MetaSel ('Just "qNums") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol]))))))

data Cstr a

Constructors

Head !Pred !a

p

CAnd ![Cstr a]

c1 ... cn

All !(Bind a) !(Cstr a)

all x:t. p => c

Any !(Bind a) !(Cstr a)

exi x:t. p / c or is it exi x:t. p => c?

Instances

Functor Cstr

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser (Cstr a)

parseJSONList :: Value -> Parser [Cstr a]

omittedField :: Maybe (Cstr a)

ToJSON a => ToJSON (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Cstr a -> Value

toEncoding :: Cstr a -> Encoding

toJSONList :: [Cstr a] -> Value

toEncodingList :: [Cstr a] -> Encoding

omitField :: Cstr a -> Bool

Data a => Data (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Cstr a -> Constr

dataTypeOf :: Cstr a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Cstr a -> Cstr a

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

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

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

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

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

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

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

Generic (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Cstr a) :: Type -> Type

Methods

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

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

Show (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Cstr a -> ShowS

show :: Cstr a -> String

showList :: [Cstr a] -> ShowS

Eq a => Eq (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

ToHornSMT (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Cstr a -> Doc

PPrint (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Cstr a -> Doc

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

Visitable (Cstr a)

Defined in Language.Fixpoint.Horn.Transformations

Methods

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

type Rep (Cstr a)

Defined in Language.Fixpoint.Horn.Types

type Rep (Cstr a) = D1 ('MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) ((C1 ('MetaCons "Head" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pred) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)) :+: C1 ('MetaCons "CAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Cstr a]))) :+: (C1 ('MetaCons "All" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Bind a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a))) :+: C1 ('MetaCons "Any" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Bind a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a)))))

data Pred

HPred is a Horn predicate that appears as LHS (body) or RHS (head) of constraints

Constructors

Reft !Expr

r

Var !Symbol ![Symbol]

$k(y1..yn)

PAnd ![Pred]

p1 ... pn

Instances

FromJSON Pred

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser Pred

parseJSONList :: Value -> Parser [Pred]

omittedField :: Maybe Pred

ToJSON Pred

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Pred -> Value

toEncoding :: Pred -> Encoding

toJSONList :: [Pred] -> Value

toEncodingList :: [Pred] -> Encoding

omitField :: Pred -> Bool

Data Pred

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Pred -> Constr

dataTypeOf :: Pred -> DataType

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

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

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

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

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

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

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

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

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

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

Monoid Pred

Defined in Language.Fixpoint.Horn.Types

Methods

mempty :: Pred

mappend :: Pred -> Pred -> Pred

mconcat :: [Pred] -> Pred

Semigroup Pred

Defined in Language.Fixpoint.Horn.Types

Methods

(<>) :: Pred -> Pred -> Pred

sconcat :: NonEmpty Pred -> Pred

stimes :: Integral b => b -> Pred -> Pred

Generic Pred

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep Pred :: Type -> Type

Methods

from :: Pred -> Rep Pred x

to :: Rep Pred x -> Pred

Show Pred

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Pred -> ShowS

show :: Pred -> String

showList :: [Pred] -> ShowS

Eq Pred

Defined in Language.Fixpoint.Horn.Types

Methods

(==) :: Pred -> Pred -> Bool

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

ToHornSMT Pred

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Pred -> Doc

PPrint Pred

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Pred -> Doc

pprintPrec :: Int -> Tidy -> Pred -> Doc

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

Visitable Pred

Defined in Language.Fixpoint.Horn.Transformations

Methods

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

type Rep Pred

Defined in Language.Fixpoint.Horn.Types

type Rep Pred = D1 ('MetaData "Pred" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol])) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Pred]))))

data Bind a

Cst is an NNF Horn Constraint.

Constructors

Bind

Fields

• bSym :: !Symbol
• bSort :: !Sort
• bPred :: !Pred
• bMeta :: !a

Instances

Functor Bind

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser (Bind a)

parseJSONList :: Value -> Parser [Bind a]

omittedField :: Maybe (Bind a)

ToJSON a => ToJSON (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Bind a -> Value

toEncoding :: Bind a -> Encoding

toJSONList :: [Bind a] -> Value

toEncodingList :: [Bind a] -> Encoding

omitField :: Bind a -> Bool

Data a => Data (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Bind a -> Constr

dataTypeOf :: Bind a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Bind a -> Bind a

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

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

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

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

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

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

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

Generic (Bind a)

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Bind a) :: Type -> Type

Methods

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

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

Show (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Bind a -> ShowS

show :: Bind a -> String

showList :: [Bind a] -> ShowS

Eq a => Eq (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

ToHornSMT (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Bind a -> Doc

PPrint (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Bind a -> Doc

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

Subable (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Bind a -> [Symbol]

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

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

subst :: Subst -> Bind a -> Bind a

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

type Rep (Bind a)

Defined in Language.Fixpoint.Horn.Types

type Rep (Bind a) = D1 ('MetaData "Bind" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) (C1 ('MetaCons "Bind" 'PrefixI 'True) ((S1 ('MetaSel ('Just "bSym") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "bSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "bPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pred) :*: S1 ('MetaSel ('Just "bMeta") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))))

data Var a

HVar is a Horn variable

Constructors

HVar

Fields

• hvName :: !Symbol

  name of the variable $k1, $k2 etc.

• hvArgs :: ![Sort]

  sorts of its parameters i.e. of the relation defined by the HVar

• hvMeta :: a

  meta-data

Instances

Functor Var

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser (Var a)

parseJSONList :: Value -> Parser [Var a]

omittedField :: Maybe (Var a)

ToJSON a => ToJSON (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Var a -> Value

toEncoding :: Var a -> Encoding

toJSONList :: [Var a] -> Value

toEncodingList :: [Var a] -> Encoding

omitField :: Var a -> Bool

Data a => Data (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Var a -> Constr

dataTypeOf :: Var a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a

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

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

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

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

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

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

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

Generic (Var a)

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Var a) :: Type -> Type

Methods

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

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

Show (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Var a -> ShowS

show :: Var a -> String

showList :: [Var a] -> ShowS

Eq a => Eq (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

Ord a => Ord (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

compare :: Var a -> Var a -> Ordering

(<) :: Var a -> Var a -> Bool

(<=) :: Var a -> Var a -> Bool

(>) :: Var a -> Var a -> Bool

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

max :: Var a -> Var a -> Var a

min :: Var a -> Var a -> Var a

ToHornSMT (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Var a -> Doc

PPrint (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Var a -> Doc

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

type Rep (Var a)

Defined in Language.Fixpoint.Horn.Types

type Rep (Var a) = D1 ('MetaData "Var" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) (C1 ('MetaCons "HVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "hvName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Just "hvArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Sort]) :*: S1 ('MetaSel ('Just "hvMeta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

Raw Query

data Tag

Constructors

NoTag

Tag String

Instances

FromJSON Tag

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser Tag

parseJSONList :: Value -> Parser [Tag]

omittedField :: Maybe Tag

ToJSON Tag

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Tag -> Value

toEncoding :: Tag -> Encoding

toJSONList :: [Tag] -> Value

toEncodingList :: [Tag] -> Encoding

omitField :: Tag -> Bool

Data Tag

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

toConstr :: Tag -> Constr

dataTypeOf :: Tag -> DataType

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

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

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

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

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

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

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

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

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

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

Generic Tag

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep Tag :: Type -> Type

Methods

from :: Tag -> Rep Tag x

to :: Rep Tag x -> Tag

Show Tag

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Tag -> ShowS

show :: Tag -> String

showList :: [Tag] -> ShowS

NFData Tag

Defined in Language.Fixpoint.Horn.Types

Methods

rnf :: Tag -> ()

ToHornSMT Tag

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Tag -> Doc

Fixpoint Tag

Defined in Language.Fixpoint.Horn.Types

Methods

toFix :: Tag -> Doc

simplify :: Tag -> Tag

PPrint Tag

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Tag -> Doc

pprintPrec :: Int -> Tidy -> Tag -> Doc

Loc Tag

Defined in Language.Fixpoint.Horn.Types

Methods

srcSpan :: Tag -> SrcSpan

type Rep Tag

Defined in Language.Fixpoint.Horn.Types

type Rep Tag = D1 ('MetaData "Tag" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" 'False) (C1 ('MetaCons "NoTag" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Tag" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

type TagVar = Var Tag

Tag each query with a possible string denoting "provenance"

type TagQuery = Query Tag

accessing constraint labels

cLabel :: Cstr a -> a

invariants (refinements) on constraints

okCstr :: Cstr a -> Bool

extract qualifiers

quals :: Cstr a -> [Qualifier]

SMTLIB style render

class ToHornSMT a where

Methods

toHornSMT :: a -> Doc

Instances

ToHornSMT Pred

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Pred -> Doc

ToHornSMT Tag

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Tag -> Doc

ToHornSMT Equation

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Equation -> Doc

ToHornSMT QualParam

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: QualParam -> Doc

ToHornSMT Qualifier

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Qualifier -> Doc

ToHornSMT Rewrite

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Rewrite -> Doc

ToHornSMT Symbol

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Symbol -> Doc

ToHornSMT Expr

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Expr -> Doc

ToHornSMT KVar

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: KVar -> Doc

ToHornSMT Subst

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Subst -> Doc

ToHornSMT DataCtor

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataCtor -> Doc

ToHornSMT DataDecl

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataDecl -> Doc

ToHornSMT DataField

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataField -> Doc

ToHornSMT FTycon

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: FTycon -> Doc

ToHornSMT Sort

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Sort -> Doc

ToHornSMT (Bind a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Bind a -> Doc

ToHornSMT (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Cstr a -> Doc

ToHornSMT (Query a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Query a -> Doc

ToHornSMT (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Var a -> Doc

ToHornSMT a => ToHornSMT (Located a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Located a -> Doc

ToHornSMT a => ToHornSMT [a]

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: [a] -> Doc

ToHornSMT a => ToHornSMT (Symbol, a)

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: (Symbol, a) -> Doc