Safe Haskell | None |
---|---|
Language | Haskell2010 |
Passes
- freshPass :: (Foldable f, Name a) => (f a -> Fresh b) -> f a -> b
- simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)
- gently :: SimplifyOpts a
- aggressively :: Name a => SimplifyOpts a
- data SimplifyOpts a = SimplifyOpts {
- touch_lets :: Bool
- should_inline :: Maybe (Scope a) -> Expr a -> Bool
- inline_match :: Bool
- removeNewtype :: Name a => Theory a -> Theory a
- uncurryTheory :: Name a => Theory a -> Fresh (Theory a)
- negateConjecture :: Name a => Theory a -> Fresh (Theory a)
- ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a
- boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a
- theoryBoolOpToIf :: Ord a => Theory a -> Theory a
- addMatch :: Name a => Theory a -> Fresh (Theory a)
- commuteMatch :: (Name a, TransformBiM Fresh (Expr a) (f a)) => f a -> Fresh (f a)
- removeMatch :: Name a => Theory a -> Fresh (Theory a)
- cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a
- cseMatchNormal :: CSEMatchOpts
- cseMatchWhy3 :: CSEMatchOpts
- fillInCases :: (Ord a, PrettyVar a) => (Type a -> Expr a) -> Theory a -> Theory a
- collapseEqual :: forall a. Ord a => Theory a -> Theory a
- removeAliases :: Eq a => Theory a -> Theory a
- lambdaLift :: Name a => Theory a -> Fresh (Theory a)
- letLift :: Name a => Theory a -> Fresh (Theory a)
- axiomatizeLambdas :: forall a. Name a => Theory a -> Fresh (Theory a)
- data StandardPass
- class Pass p where
- unitPass :: Pass p => p -> Mod FlagFields () -> Parser p
- runPassLinted :: (Pass p, Name a) => p -> Theory a -> Fresh (Theory a)
- data Choice a b
- choice :: (a -> c) -> (b -> c) -> Choice a b -> c
- runPasses :: (Pass p, Name a) => [p] -> Theory a -> Fresh (Theory a)
- parsePasses :: Pass p => Parser [p]
Running passes in the Fresh monad
freshPass :: (Foldable f, Name a) => (f a -> Fresh b) -> f a -> b Source
Continues making unique names after the highest numbered name in a foldable value.
Simplifications
simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a) Source
Simplify an entire theory
gently :: SimplifyOpts a Source
Gentle options: if there is risk for code duplication, only inline atomic expressions
aggressively :: Name a => SimplifyOpts a Source
Aggressive options: inline everything that might plausibly lead to simplification
data SimplifyOpts a Source
Options for the simplifier
SimplifyOpts | |
|
removeNewtype :: Name a => Theory a -> Theory a Source
Remove datatypes that have only one constructor with one field.
Can only be run after the addMatch
pass.
uncurryTheory :: Name a => Theory a -> Fresh (Theory a) Source
Replace "fat arrow", =>
, functions with normal functions wherever possible.
negateConjecture :: Name a => Theory a -> Fresh (Theory a) Source
Negates the conjecture: changes assert-not into assert, and introduce skolem types in case the goal is polymorphic.
Boolean builtins
ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a Source
Transforms ite
(match
) on boolean literals in the branches
into the corresponding builtin boolean function.
boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a Source
Transforms and
, or
, =>
, not
and =
and distict
on Bool
into ite
(i.e. match
)
theoryBoolOpToIf :: Ord a => Theory a -> Theory a Source
Transforms boolean operators to if, but not in expression contexts.
Match expressions
addMatch :: Name a => Theory a -> Fresh (Theory a) Source
Replace SMTLIB-style selector and discriminator functions
(is-nil
, head
, tail
) with case expressions.
commuteMatch :: (Name a, TransformBiM Fresh (Expr a) (f a)) => f a -> Fresh (f a) Source
Makes an effort to move match statements upwards: moves match above function applications, and moves matches inside scrutinees outside.
Does not move past quantifiers, lets, and lambdas.
removeMatch :: Name a => Theory a -> Fresh (Theory a) Source
Turn case expressions into is-Cons
, head
, tail
etc.
cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a Source
Look for expressions of the form
(match x (case P ...P...) ...)
and replace them with
(match x (case P ...x...) ...)
.
This helps Why3's termination checker in some cases.
cseMatchNormal :: CSEMatchOpts Source
cseMatchWhy3 :: CSEMatchOpts Source
Duplicated functions
collapseEqual :: forall a. Ord a => Theory a -> Theory a Source
If we have
f x = E[x] g y = E[y]
then we remove g
and replace it with f
everywhere
removeAliases :: Eq a => Theory a -> Theory a Source
If we have
g x y = f x y
then we remove g
and replace it with f
everywhere
Lambda and let lifting
lambdaLift :: Name a => Theory a -> Fresh (Theory a) Source
Defunctionalization.
f x = ... \ y -> e [ x ] ...
becomes
f x = ... g x ... g x = \ y -> e [ x ]
where g
is a fresh function.
After this pass, lambdas only exist at the top level of functions.
letLift :: Name a => Theory a -> Fresh (Theory a) Source
Lift lets to the top level.
let x = b[fvs] in e[x]
becomes
e[f fvs] f fvs = b[fvs]
axiomatizeLambdas :: forall a. Name a => Theory a -> Fresh (Theory a) Source
Axiomatize lambdas.
f x = \ y -> E[x,y]
becomes
declare-fun f ... assert (forall x y . @ (f x) y = E[x,y])
Building pass pipelines
data StandardPass Source
The passes in the standard Tip distribution
parsePasses :: Pass p => Parser [p] Source