module Tip.Passes
(
freshPass
, simplifyTheory, gently, aggressively, SimplifyOpts(..)
, removeNewtype
, uncurryTheory
, module Tip.Pass.Conjecture
, module Tip.Pass.Concretise
, makeConjecture
, selectConjecture
, provedConjecture
, deleteConjecture
, ifToBoolOp
, boolOpToIf
, theoryBoolOpToIf
, removeBuiltinBool
, boolOpLift
, addMatch
, commuteMatch
, removeMatch
, cseMatch
, cseMatchNormal
, cseMatchWhy3
, fillInCases
, collapseEqual
, removeAliases
, lambdaLift
, letLift
, axiomatizeLambdas
, axiomatizeFuncdefs
, axiomatizeFuncdefs2
, axiomatizeDatadecls
, monomorphise
, induction
, uniqLocals
, dropSuffix
, StandardPass(..)
, module Tip.Pass.Pipeline
) where
import Tip.Simplify
import Tip.Pass.AddMatch
import Tip.Pass.CommuteMatch
import Tip.Pass.RemoveMatch
import Tip.Pass.CSEMatch
import Tip.Pass.Uncurry
import Tip.Pass.RemoveNewtype
import Tip.Pass.Conjecture
import Tip.Pass.Concretise
import Tip.Pass.EqualFunctions
import Tip.Pass.Lift
import Tip.Pass.Monomorphise
import Tip.Pass.Booleans
import Tip.Pass.EliminateDeadCode
import Tip.Pass.FillInCases
import Tip.Pass.AxiomatizeFuncdefs
import Tip.Pass.AxiomatizeDatadecls
import Tip.Pass.SelectConjecture
import Tip.Pass.DropSuffix
import Tip.Pass.UniqLocals
import Tip.Pass.Induction
import Tip.Fresh
import Tip.Pass.Pipeline
import Options.Applicative
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]
deriving (Eq,Ord,Show,Read)
instance Pass StandardPass where
passName = show
runPass p = case p of
SimplifyGently -> single $ simplifyTheory gently
SimplifyAggressively -> single $ simplifyTheory aggressively
RemoveNewtype -> single $ return . removeNewtype
UncurryTheory -> single $ uncurryTheory
NegateConjecture -> single $ negateConjecture
TypeSkolemConjecture -> single $ typeSkolemConjecture
IntToNat -> single $ intToNat
SortsToNat -> single $ sortsToNat
SplitConjecture -> return . splitConjecture
SkolemiseConjecture -> skolemiseConjecture
IfToBoolOp -> single $ return . ifToBoolOp
BoolOpToIf -> single $ return . theoryBoolOpToIf
RemoveBuiltinBool -> single $ removeBuiltinBool
BoolOpLift -> single $ boolOpLift
AddMatch -> single $ addMatch
CommuteMatch -> single $ commuteMatchTheory
RemoveMatch -> single $ removeMatch
CollapseEqual -> single $ return . collapseEqual
RemoveAliases -> single $ return . removeAliases
LambdaLift -> single $ lambdaLift
LetLift -> single $ letLift
AxiomatizeLambdas -> single $ axiomatizeLambdas
AxiomatizeFuncdefs -> single $ return . axiomatizeFuncdefs
AxiomatizeFuncdefs2 -> single $ return . axiomatizeFuncdefs2
AxiomatizeDatadecls -> single $ axiomatizeDatadecls False
AxiomatizeDatadeclsUEQ -> single $ axiomatizeDatadecls True
Monomorphise b -> single $ monomorphise b
CSEMatch -> single $ return . cseMatch cseMatchNormal
CSEMatchWhy3 -> single $ return . cseMatch cseMatchWhy3
EliminateDeadCode -> single $ return . eliminateDeadCode
MakeConjecture n -> single $ return . makeConjecture n
SelectConjecture n -> single $ return . selectConjecture n
ProvedConjecture n -> single $ return . provedConjecture n
DeleteConjecture n -> single $ return . deleteConjecture n
DropSuffix cs -> single $ dropSuffix cs
UniqLocals -> single $ uniqLocals
Induction coords -> induction coords
where single m thy = do x <- m thy; return [x]
parsePass =
foldr (<|>) empty [
unitPass SimplifyGently $
help "Simplify the problem, trying not to increase its size",
unitPass SimplifyAggressively $
help "Simplify the problem even at the cost of making it bigger",
unitPass RemoveNewtype $
help "Eliminate single-constructor, single-argument datatypes",
unitPass UncurryTheory $
help "Eliminate unnecessary use of higher-order functions",
unitPass NegateConjecture $
help "Transform the goal into a negated conjecture",
unitPass TypeSkolemConjecture $
help "Skolemise the types in the conjecture",
unitPass IntToNat $
help "Replace builtin Integer with a a unary nat datatype nat (if only ordering is used)",
unitPass SortsToNat $
help "Replace abstract sorts with a unary nat datatype.",
unitPass SplitConjecture $
help "Puts goals in separate theories",
unitPass SkolemiseConjecture $
help "Skolemise the conjecture",
unitPass IfToBoolOp $
help "Replace if-then-else by and/or where appropriate",
unitPass BoolOpToIf $
help "Replace and/or by if-then-else",
unitPass RemoveBuiltinBool $
help "Replace the builtin bool with a datatype",
unitPass BoolOpLift $
help "Lift boolean operators to the top level",
unitPass AddMatch $
help "Transform SMTLIB-style datatype access into pattern matching",
unitPass CommuteMatch $
help "Eliminate matches that occur in weird positions (e.g. as arguments to function calls)",
unitPass RemoveMatch $
help "Replace pattern matching with SMTLIB-style datatype access",
unitPass CollapseEqual $
help "Merge functions with equal definitions",
unitPass RemoveAliases $
help "Eliminate any function defined simply as f(x) = g(x)",
unitPass LambdaLift $
help "Lift lambdas to the top level",
unitPass LetLift $
help "Lift let-expressions to the top level",
unitPass AxiomatizeLambdas $
help "Eliminate lambdas by axiomatisation (requires --lambda-lift)",
unitPass AxiomatizeFuncdefs $
help "Transform function definitions to axioms in the most straightforward way",
unitPass AxiomatizeFuncdefs2 $
help "Transform function definitions to axioms with left hand side pattern matching instead of match",
unitPass AxiomatizeDatadecls $
help "Transform data declarations to axioms",
unitPass AxiomatizeDatadeclsUEQ $
help "Transform data declarations to unit equality axioms (incomplete)",
flag' () (long ("monomorphise") <> help "Try to monomorphise the problem") *> pure (Monomorphise False),
flag' () (long ("monomorphise-verbose") <> help "Try to monomorphise the problem verbosely") *> pure (Monomorphise True),
unitPass CSEMatch $
help "Perform CSE on match scrutinees",
unitPass CSEMatchWhy3 $
help "Aggressively perform CSE on match scrutinees (helps Why3's termination checker)",
unitPass EliminateDeadCode $
help "Dead code elimination (doesn't work on dead recursive functions)",
fmap MakeConjecture $
option auto $
long "make-conjecture" <>
metavar "CONJECTURE-NUMBER" <>
help "Make an assert into an assert-not",
fmap SelectConjecture $
option auto $
long "select-conjecture" <>
metavar "CONJECTURE-NUMBER" <>
help "Choose a particular conjecture from the problem",
fmap ProvedConjecture $
option auto $
long "proved-conjecture" <>
metavar "CONJECTURE-NUMBER" <>
help "Mark a particular conjecture as proved",
fmap DeleteConjecture $
option auto $
long "delete-conjecture" <>
metavar "CONJECTURE-NUMBER" <>
help "Delete a particular conjecture",
fmap DropSuffix $
option str $
long "drop-suffix" <>
metavar "SUFFIX-CHARS" <>
help "Drop the suffix delimited by some character set",
unitPass UniqLocals $
help "Make all local variables unique",
fmap Induction $
option auto $
long "induction" <>
metavar "VAR-COORD" <>
help "Perform induction on the variable coordinates"
]