| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Tip.Passes
Contents
Description
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
- remove_variable_scrutinee_in_branches :: Bool
- should_inline :: Occurrences -> Maybe (Scope a) -> Expr a -> Bool
- inline_match :: Bool
- removeNewtype :: Name a => Theory a -> Theory a
- uncurryTheory :: Name a => Theory a -> Fresh (Theory a)
- splitConjecture :: Theory a -> [Theory a]
- skolemiseConjecture :: Name a => Theory a -> Fresh [Theory a]
- skolemiseConjecture' :: Name a => Theory a -> Fresh (Theory a)
- skolemise :: Expr a -> Writer ([Local a], [Expr a]) (Expr a)
- negateConjecture :: Name a => Theory a -> Fresh (Theory a)
- typeSkolemConjecture :: Name a => Theory a -> Fresh (Theory a)
- intToNat :: forall a. Name a => Theory a -> Fresh (Theory a)
- sortsToNat :: forall a. Name a => Theory a -> Fresh (Theory a)
- makeConjecture :: Int -> Theory a -> Theory a
- selectConjecture :: Int -> Theory a -> Theory a
- provedConjecture :: Int -> Theory a -> Theory a
- deleteConjecture :: Int -> Theory a -> 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
- removeBuiltinBool :: Name a => Theory a -> Fresh (Theory a)
- boolOpLift :: Name a => Theory a -> Fresh (Theory a)
- addMatch :: Name a => Theory a -> Fresh (Theory a)
- commuteMatch :: forall a f. (Name a, TransformBiM Fresh (Expr a) (f a)) => Maybe (Theory 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 :: Ord 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)
- axiomatizeFuncdefs :: Theory a -> Theory a
- axiomatizeFuncdefs2 :: Name a => Theory a -> Theory a
- axiomatizeDatadecls :: Name a => Bool -> Theory a -> Fresh (Theory a)
- monomorphise :: forall a. Name a => Bool -> Theory a -> Fresh (Theory a)
- induction :: (Name a, Ord a) => [Int] -> Theory a -> Fresh [Theory a]
- uniqLocals :: forall a. Name a => Theory a -> Fresh (Theory a)
- dropSuffix :: forall f a. (Traversable f, Name a) => String -> f a -> Fresh (f a)
- data StandardPass
- = SimplifyGently
- | SimplifyAggressively
- | RemoveNewtype
- | UncurryTheory
- | NegateConjecture
- | TypeSkolemConjecture
- | IntToNat
- | SortsToNat
- | SplitConjecture
- | SkolemiseConjecture
- | IfToBoolOp
- | BoolOpToIf
- | RemoveBuiltinBool
- | BoolOpLift
- | AddMatch
- | CommuteMatch
- | RemoveMatch
- | CollapseEqual
- | RemoveAliases
- | LambdaLift
- | LetLift
- | AxiomatizeLambdas
- | AxiomatizeFuncdefs
- | AxiomatizeFuncdefs2
- | AxiomatizeDatadecls
- | AxiomatizeDatadeclsUEQ
- | Monomorphise Bool
- | CSEMatch
- | CSEMatchWhy3
- | EliminateDeadCode
- | MakeConjecture Int
- | SelectConjecture Int
- | ProvedConjecture Int
- | DeleteConjecture Int
- | DropSuffix String
- | UniqLocals
- | Induction [Int]
- class Pass p where
- unitPass :: Pass p => p -> Mod FlagFields () -> Parser p
- lintMany :: (Name a, Monad m) => String -> [Theory a] -> m [Theory a]
- 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]
- continuePasses :: forall p a. (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
Constructors
| SimplifyOpts | |
Fields
| |
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.
Simplifyng conjectures
splitConjecture :: Theory a -> [Theory a] Source
Splits a theory with many goals into many theories each with one goal
skolemiseConjecture :: Name a => Theory a -> Fresh [Theory a] Source
Splits, type skolems and skolemises conjectures!
skolemiseConjecture' :: Name a => Theory a -> Fresh (Theory a) Source
Skolemises a conjecture, assuming that there is just one goal and that it has no type variables.
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.
(runs typeSkolemConjecture)
typeSkolemConjecture :: Name a => Theory a -> Fresh (Theory a) Source
Introduce skolem types in case the goal is polymorphic.
intToNat :: forall a. Name a => Theory a -> Fresh (Theory a) Source
Replaces the builtin Int to natural numbers, if the only operations performed on are related to int ordering
sortsToNat :: forall a. Name a => Theory a -> Fresh (Theory a) Source
Replaces abstract sorts with natural numbers
Changing status of conjectures
makeConjecture :: Int -> Theory a -> Theory a Source
selectConjecture :: Int -> Theory a -> Theory a Source
provedConjecture :: Int -> Theory a -> Theory a Source
deleteConjecture :: Int -> Theory a -> Theory a Source
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 distinct 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.
boolOpLift :: Name a => Theory a -> Fresh (Theory a) Source
Lifts boolean operators to the top level
replaces (and r s t) with f r s t and f x y z = and x y z
Run CollapseEqual and BoolOpToIf afterwards
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 :: forall a f. (Name a, TransformBiM Fresh (Expr a) (f a)) => Maybe (Theory 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 :: Ord a => Theory a -> Theory a Source
If we have
g [a] x y = f [T1 a,T2 a] x y
then we remove g [t] and replace it with f [T1 t,T2 t] 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])
Function definitions
axiomatizeFuncdefs :: Theory a -> Theory a Source
Transforms define-fun to declare-fun in the most straightforward way. All parts of the right hand side is preserved, including match and if-then-else.
axiomatizeFuncdefs2 :: Name a => Theory a -> Theory a Source
Makes function definitions into case by converting case to left hand side pattern matching.
Data types
Monomorphisation
Induction
induction :: (Name a, Ord a) => [Int] -> Theory a -> Fresh [Theory a] Source
Applies induction at the given coordinates to the first goal
Miscellaneous
dropSuffix :: forall f a. (Traversable f, Name a) => String -> f a -> Fresh (f a) Source
Building pass pipelines
data StandardPass Source
The passes in the standard Tip distribution
Constructors
parsePasses :: Pass p => Parser [p] Source