Safe Haskell	None
Language	Haskell2010

GHC.TypeLits.Presburger.Types

Description

Since 0.3.0.0

Synopsis

pluginWith :: TcPluginM Translation -> Plugin
defaultTranslation :: TcPluginM Translation
data Translation = Translation {
- isEmpty :: [TyCon]
- isTrue :: [TyCon]
- trueData :: [TyCon]
- falseData :: [TyCon]
- voids :: [TyCon]
- tyEq :: [TyCon]
- tyEqBool :: [TyCon]
- tyEqWitness :: [TyCon]
- tyNeqBool :: [TyCon]
- natPlus :: [TyCon]
- natMinus :: [TyCon]
- natExp :: [TyCon]
- natTimes :: [TyCon]
- natLeq :: [TyCon]
- natLeqBool :: [TyCon]
- natGeq :: [TyCon]
- natGeqBool :: [TyCon]
- natLt :: [TyCon]
- natLtBool :: [TyCon]
- natGt :: [TyCon]
- natGtBool :: [TyCon]
- orderingLT :: [TyCon]
- orderingGT :: [TyCon]
- orderingEQ :: [TyCon]
- natCompare :: [TyCon]
- parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
- parseExpr :: Type -> Machine Expr
}
type ParseEnv = Map TypeEq TyVar
type Machine = MaybeT (StateT ParseEnv TcPluginM)
data Expr
- = Expr :+ Expr
- | Expr :- Expr
- | Integer :* Expr
- | Negate Expr
- | Var Name
- | K Integer
- | If Prop Expr Expr
- | Div Expr Integer
- | Mod Expr Integer
data Prop
- = PTrue
- | PFalse
- | Prop :|| Prop
- | Prop :&& Prop
- | Not Prop
- | Expr :== Expr
- | Expr :/= Expr
- | Expr :< Expr
- | Expr :> Expr
- | Expr :<= Expr
- | Expr :>= Expr
data PropSet
noProps :: PropSet
assert :: Prop -> PropSet -> PropSet
checkSat :: PropSet -> Maybe [(Int, Integer)]
toName :: Int -> Name

Documentation

pluginWith :: TcPluginM Translation -> Plugin Source #

defaultTranslation :: TcPluginM Translation Source #

data Translation Source #

Constructors

Translation

Fields

isEmpty :: [TyCon]
isTrue :: [TyCon]
trueData :: [TyCon]
falseData :: [TyCon]
voids :: [TyCon]
tyEq :: [TyCon]
tyEqBool :: [TyCon]
tyEqWitness :: [TyCon]
tyNeqBool :: [TyCon]
natPlus :: [TyCon]
natMinus :: [TyCon]
natExp :: [TyCon]
natTimes :: [TyCon]
natLeq :: [TyCon]
natLeqBool :: [TyCon]
natGeq :: [TyCon]
natGeqBool :: [TyCon]
natLt :: [TyCon]
natLtBool :: [TyCon]
natGt :: [TyCon]
natGtBool :: [TyCon]
orderingLT :: [TyCon]
orderingGT :: [TyCon]
orderingEQ :: [TyCon]
natCompare :: [TyCon]
parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
parseExpr :: Type -> Machine Expr

Instances

Semigroup Translation Source #
Instance details Defined in GHC.TypeLits.Presburger.Types Methods (<>) :: Translation -> Translation -> Translation # sconcat :: NonEmpty Translation -> Translation # stimes :: Integral b => b -> Translation -> Translation #
Monoid Translation Source #
Instance details Defined in GHC.TypeLits.Presburger.Types Methods mempty :: Translation # mappend :: Translation -> Translation -> Translation # mconcat :: [Translation] -> Translation #

type ParseEnv = Map TypeEq TyVar Source #

type Machine = MaybeT (StateT ParseEnv TcPluginM) Source #

data Expr Source #

The type of integer expressions. Variable names must be non-negative.

Constructors

Expr :+ Expr infixl 6	Addition
Expr :- Expr infixl 6	Subtraction
Integer :* Expr infixl 7	Multiplication by a constant
Negate Expr	Negation
Var Name	Variable
K Integer	Constant
If Prop Expr Expr	A conditional expression
Div Expr Integer	Division, rounds down
Mod Expr Integer	Non-negative remainder

Instances

Eq Expr Source #
Instance details Defined in Data.Integer.SAT Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Ord Expr Source #
Instance details Defined in Data.Integer.SAT Methods compare :: Expr -> Expr -> Ordering # (<) :: Expr -> Expr -> Bool # (<=) :: Expr -> Expr -> Bool # (>) :: Expr -> Expr -> Bool # (>=) :: Expr -> Expr -> Bool # max :: Expr -> Expr -> Expr # min :: Expr -> Expr -> Expr #
Read Expr Source #
Instance details Defined in Data.Integer.SAT Methods readsPrec :: Int -> ReadS Expr # readList :: ReadS [Expr] # readPrec :: ReadPrec Expr # readListPrec :: ReadPrec [Expr] #
Show Expr Source #
Instance details Defined in Data.Integer.SAT Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #

data Prop Source #

The type of proposition.

Constructors

PTrue
PFalse
Prop :\|\| Prop infixr 2
Prop :&& Prop infixr 3
Not Prop
Expr :== Expr infix 4
Expr :/= Expr infix 4
Expr :< Expr infix 4
Expr :> Expr infix 4
Expr :<= Expr infix 4
Expr :>= Expr infix 4

Instances

Eq Prop Source #
Instance details Defined in Data.Integer.SAT Methods (==) :: Prop -> Prop -> Bool # (/=) :: Prop -> Prop -> Bool #
Ord Prop Source #
Instance details Defined in Data.Integer.SAT Methods compare :: Prop -> Prop -> Ordering # (<) :: Prop -> Prop -> Bool # (<=) :: Prop -> Prop -> Bool # (>) :: Prop -> Prop -> Bool # (>=) :: Prop -> Prop -> Bool # max :: Prop -> Prop -> Prop # min :: Prop -> Prop -> Prop #
Read Prop Source #
Instance details Defined in Data.Integer.SAT Methods readsPrec :: Int -> ReadS Prop # readList :: ReadS [Prop] # readPrec :: ReadPrec Prop # readListPrec :: ReadPrec [Prop] #
Show Prop Source #
Instance details Defined in Data.Integer.SAT Methods showsPrec :: Int -> Prop -> ShowS # show :: Prop -> String # showList :: [Prop] -> ShowS #

data PropSet Source #

A collection of propositions.

Instances

Show PropSet Source #
Instance details Defined in Data.Integer.SAT Methods showsPrec :: Int -> PropSet -> ShowS # show :: PropSet -> String # showList :: [PropSet] -> ShowS #

noProps :: PropSet Source #

An empty collection of propositions.

assert :: Prop -> PropSet -> PropSet Source #

Add a new proposition to an existing collection.

checkSat :: PropSet -> Maybe [(Int, Integer)] Source #

Extract a model from a consistent set of propositions. Returns Nothing if the assertions have no model. If a variable does not appear in the assignment, then it is 0 (?).

toName :: Int -> Name Source #