Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Since 0.3.0.0
Synopsis
- pluginWith :: TcPluginM Translation -> Plugin
- defaultTranslation :: TcPluginM Translation
- data Translation = Translation {
- isEmpty :: [TyCon]
- ordCond :: [TyCon]
- assertTy :: [TyCon]
- isTrue :: [TyCon]
- trueData :: [TyCon]
- falseData :: [TyCon]
- voids :: [TyCon]
- tyEq :: [TyCon]
- tyEqBool :: [TyCon]
- tyEqWitness :: [TyCon]
- tyNot :: [TyCon]
- tyAnd :: [TyCon]
- tyOr :: [TyCon]
- tyIf :: [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]
- natMin :: [TyCon]
- natMax :: [TyCon]
- orderingLT :: [TyCon]
- orderingGT :: [TyCon]
- orderingEQ :: [TyCon]
- natCompare :: [TyCon]
- parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
- parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr
- type ParseEnv = Map TypeEq TyVar
- type Machine = MaybeT (StateT ParseEnv TcPluginM)
- data Expr
- data Prop
- data PropSet
- noProps :: PropSet
- assert :: Prop -> PropSet -> PropSet
- checkSat :: PropSet -> Maybe [(Int, Integer)]
- toName :: Int -> Name
Documentation
pluginWith :: TcPluginM Translation -> Plugin Source #
data Translation Source #
Translation | |
|
Instances
Monoid Translation Source # | |
Defined in GHC.TypeLits.Presburger.Types mempty :: Translation # mappend :: Translation -> Translation -> Translation # mconcat :: [Translation] -> Translation # | |
Semigroup Translation Source # | |
Defined in GHC.TypeLits.Presburger.Types (<>) :: Translation -> Translation -> Translation # sconcat :: NonEmpty Translation -> Translation # stimes :: Integral b => b -> Translation -> Translation # |
The type of integer expressions. Variable names must be non-negative.
(:+) infixl 6 | |
(:-) infixl 6 | |
(:*) infixl 7 | |
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 |
Min Expr Expr | Minimum of two arguments |
Max Expr Expr | Maximum of two arguments |
The type of proposition.
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 |
A collection of propositions.