Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Horn.Types

Contents

Horn Constraints and their components
Raw Query
accessing constraint labels
invariants (refinements) on constraints
extract qualifiers

Description

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

Synopsis

data Query a = Query {
- qQuals :: ![Qualifier]
- qVars :: ![Var a]
- qCstr :: !(Cstr a)
- qCon :: HashMap Symbol Sort
- qDis :: HashMap Symbol Sort
- qEqns :: ![Equation]
- qDefs :: ![Equation]
- qMats :: ![Rewrite]
- qData :: ![DataDecl]
- qOpts :: ![String]
- qNums :: ![Symbol]
}
data Cstr a
- = Head !Pred !a
- | CAnd ![Cstr a]
- | All !(Bind a) !(Cstr a)
data Pred
- = Reft !Expr
- | Var !Symbol ![Expr]
- | PAnd ![Pred]
data Bind a = Bind {
- bSym :: !Symbol
- bSort :: !Sort
- bPred :: !Pred
- bMeta :: !a
}
data Var a = HVar {
- hvName :: !Symbol
- hvArgs :: ![Sort]
- hvMeta :: a
}
data Tag
- = NoTag
- | Tag String
type TagVar = Var Tag
type TagQuery = Query Tag
cLabel :: Cstr a -> a
okCstr :: Cstr a -> Bool
quals :: Cstr a -> [Qualifier]

Horn Constraints and their components

data Query a Source #

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 (un/interpreted functions)
qDis :: HashMap Symbol Sort
list of *distinct* constants (uninterpreted functions)
qEqns :: ![Equation]
list of equations
qDefs :: ![Equation]
list of equations to be sent to SMT as define-fun
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

Instances details

Functor Query Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Query a) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Query a)

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint (Query a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Query a -> Doc Source #

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

ToHornSMT (Query a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Query a -> Doc Source #

type Rep (Query a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

data Cstr a Source #

Constructors

Head !Pred !a	p
CAnd ![Cstr a]	c1 ... cn
All !(Bind a) !(Cstr a)	all x:t. p => c

Instances

Instances details

Functor Cstr Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Cstr a) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Cstr a)

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Cstr a) = D1 ('MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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)))))

Methods

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

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

Show (Cstr a) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint (Cstr a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Cstr a -> Doc Source #

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

ToHornSMT (Cstr a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Cstr a -> Doc Source #

Foldable (Cstr a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Transformations

Methods

foldE :: Monoid a0 => Folder a0 c -> c -> Cstr a -> FoldM a0 (Cstr a) Source #

type Rep (Cstr a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Cstr a) = D1 ('MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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)))))

data Pred Source #

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

Constructors

Reft !Expr	r
Var !Symbol ![Expr]	$k(y1..yn)
PAnd ![Pred]	p1 ... pn

Instances

Instances details

FromJSON Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser Pred #

parseJSONList :: Value -> Parser [Pred] #

omittedField :: Maybe Pred #

ToJSON Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Pred -> Value #

toEncoding :: Pred -> Encoding #

toJSONList :: [Pred] -> Value #

toEncodingList :: [Pred] -> Encoding #

omitField :: Pred -> Bool #

Data Pred Source #

Instance details

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 #

Generic Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep Pred

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep Pred = D1 ('MetaData "Pred" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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 [Expr])) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Pred]))))

Methods

from :: Pred -> Rep Pred x #

to :: Rep Pred x -> Pred #

Show Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Pred -> ShowS #

show :: Pred -> String #

showList :: [Pred] -> ShowS #

Eq Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Pred -> Doc Source #

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

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 #

ToHornSMT Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Pred -> Doc Source #

Foldable Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Transformations

Methods

foldE :: Monoid a => Folder a c -> c -> Pred -> FoldM a Pred Source #

type Rep Pred Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep Pred = D1 ('MetaData "Pred" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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 [Expr])) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Pred]))))

data Bind a Source #

Cst is an NNF Horn Constraint.

Constructors

Bind
Fields bSym :: !Symbol bSort :: !Sort bPred :: !Pred bMeta :: !a

Instances

Instances details

Functor Bind Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Bind a) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Bind a)

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Bind a) = D1 ('MetaData "Bind" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

Methods

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

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

Show (Bind a) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint (Bind a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Bind a -> Doc Source #

pprintPrec :: Int -> Tidy -> Bind a -> Doc 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 #

ToHornSMT (Bind a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Bind a -> Doc Source #

type Rep (Bind a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Bind a) = D1 ('MetaData "Bind" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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 Source #

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

Instances details

Functor Var Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

FromJSON a => FromJSON (Var a) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep (Var a)

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Var a) = D1 ('MetaData "Var" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

Methods

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

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

Show (Var a) Source #

Instance details

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) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

Ord a => Ord (Var a) Source #

Instance details

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 #

PPrint (Var a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Var a -> Doc Source #

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

ToHornSMT (Var a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Var a -> Doc Source #

type Rep (Var a) Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep (Var a) = D1 ('MetaData "Var" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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 Source #

Constructors

NoTag
Tag String

Instances

Instances details

FromJSON Tag Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

parseJSON :: Value -> Parser Tag #

parseJSONList :: Value -> Parser [Tag] #

omittedField :: Maybe Tag #

ToJSON Tag Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

toJSON :: Tag -> Value #

toEncoding :: Tag -> Encoding #

toJSONList :: [Tag] -> Value #

toEncodingList :: [Tag] -> Encoding #

omitField :: Tag -> Bool #

Data Tag Source #

Instance details

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 Source #

Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

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