#!/usr/bin/runhaskell

import Prelude hiding (fail, uncurry)
import Tct.Configuration
import Tct.Interactive
import Tct.Instances
import Tct.Processor.Args.Instances (Nat (..))
import qualified Tct.Instances as Instance
import qualified Tct.Processors as Processor
import qualified Termlib.Repl as TR

-- import Control.Monad.IO.Class (liftIO)
import qualified Tct.Processor as P
import qualified Tct.Certificate as Cert
import Data.List (subsequences)

config :: Config
config = defaultConfig { processors = procs 
                       , recompile = False } 
  where procs = mycomp "matrix" (\ i -> mx i i)
                <|> mycomp "poly" polys
                <|> mycomp "both" (\ i -> polys i `orFaster` mx i i)
                <|> bs "popstar" popstarSmall
                <|> bs "popstarps" popstarSmallPS
                <|> processors defaultConfig
        bs n f = 
          fromAction Description { as = "bsearch-" ++ n
                                 , descr = []
                                 , args = Unit }
          (\ () -> bsearch f)
        mycomp n f = 
          fromInstance Description { as = "compose-" ++ n
                                   , descr = []
                                   , args = naturalArg { name = "steps" } }
          (mycompose f)

main :: IO ()
main = tct config

--------------------------------------------------------------------------------
-- abbreviations

dos dim deg = defaultOptions { cbits = Just (bits + 1)
                             , bits = bits
                             , cert = Automaton
                             , dim = dim'
                             , degree = if dim' > deg' then Just deg' else Nothing }
    where bits | dim <= 2 = 3
               | dim <= 4 = 2
               | otherwise = 1
          dim' = max 1 dim
          deg' = max 0 deg

wg dim deg = weightgap $ dos dim deg
mx dim deg = matrix $ dos dim deg

t >>! p = t >>| empty `before` p 
t >>!! p = t >>|| empty `before` p 

-- base processors
matchbounds = bounds Minimal Match `orFaster` bounds PerSymbol Match

matrices i = fastest [ mx i i, mx (i + 2) i]

-- transformations
dpi = dependencyTuples >>> dpsimps

polys 1 = poly linearPolynomial
polys n = poly $ customPolynomial inter
  where inter vs = [mono [v^^^1 | v <- vs'] | vs' <- subsequences vs
                                           , length vs <= n]
--                   ++ [mono [v^^^2] | v <- vs] 
  -- where inter vs = [mono []]
  --                  ++ [mono [v^^^1] | v <- vs] 
  --                  ++ [mono [v^^^2] | v <- vs] 
  --                  ++ [mono [v^^^1,w^^^1] | v <- vs, w <- vs, v < w]

   
mycompose direct (Nat steps) = try irr >>| (forDegree 1 `orFaster` (dpi >>| step [0..steps] (try . trans) forDegree))
    where forDegree 0 = some $ named "For Degree 0" empty
          forDegree 1 = some $ named "For Degree 1" $ mx 1 1 `orFaster` timeout 3 matchbounds
          forDegree i = some $ named ("For Degree " ++ show i) proc
              where proc = direct i
                           `orFaster` (comp >>| forDegree (i - 1)) -- step [ (k,j) | k <- [1], j <- [i - k]] comp procA
                    comp  = composeRC composeRCselect `solveBWith` forDegree 1
                    procA     (_,j) = try (trans j) >>| forDegree j
                    procB     (k,_) = try (trans k) >>| forDegree k -- step [1..k] trans forDegree
          trans i = try (exhaustively (try removeTails >>> try simpDPRHS >>> simpKP)) >>> usableRules -- try $ try (wgs i) >>> exhaustively (dpsimps >>> wgs i)
          wgs i = (wg i i) -- <> wg (i + 2) i


bsearch :: (P.SolverM m, P.Processor proc) => (Maybe Int -> P.InstanceOf proc) -> TR.Problem -> m (P.ProofOf proc)
bsearch mkinst prob = 
  do proof <- P.solve (mkinst Nothing) prob
     case ub proof of 
       Just 0 -> return proof
       Just n -> search proof 0 (n - 1)
       _      -> return proof
    where search proof l u 
            | l > u = return proof
            | otherwise = 
              do let mean = floor $ (fromIntegral $ u + l) / 2 
--                 liftIO $ putStrLn $ (show l ++ "/" ++ show mean ++ "/" ++ show u)
                 proof' <- P.solve (mkinst $ Just mean) prob
                 case ub proof' of 
                   Just n  -> search proof' l (n - 1)
                   Nothing -> search proof (mean + 1) u
          ub proof = 
            case Cert.upperBound $ P.certificate proof of 
              Cert.Poly b -> b
              _           -> Nothing