-- | Passes
module Tip.Passes
  (
  -- * Running passes in the Fresh monad
    freshPass

  -- * Simplifications
  , simplifyTheory, gently, aggressively, SimplifyOpts(..)
  , removeNewtype
  , uncurryTheory

  -- * Simplifyng conjectures
  , module Tip.Pass.Conjecture
  , module Tip.Pass.Concretise

  -- * Changing status of conjectures
  , makeConjecture
  , selectConjecture
  , provedConjecture
  , deleteConjecture

  -- * Boolean builtins
  , ifToBoolOp
  , boolOpToIf
  , theoryBoolOpToIf
  , removeBuiltinBool
  , boolOpLift

  -- * Match expressions
  , addMatch
  , commuteMatch
  , removeMatch
  , cseMatch
  , cseMatchNormal
  , cseMatchWhy3
  , fillInCases

  -- * Duplicated functions
  , collapseEqual
  , removeAliases

  -- * Lambda and let lifting
  , lambdaLift
  , letLift
  , axiomatizeLambdas

  -- * Function definitions
  , axiomatizeFuncdefs
  , axiomatizeFuncdefs2

  -- * Data types
  , axiomatizeDatadecls

  -- * Monomorphisation
  , monomorphise

  -- * Induction
  , induction

  -- * Miscellaneous
  , uniqLocals
  , dropSuffix

  -- * Building pass pipelines
  , 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

-- | The passes in the standard Tip distribution
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"
      ]