content: {-# LANGUAGE BangPatterns              #-}
  {-# LANGUAGE FlexibleInstances         #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE RecordWildCards           #-}
  {-# LANGUAGE UndecidableInstances      #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  {-# LANGUAGE PatternGuards             #-}
  {-# LANGUAGE DoAndIfThenElse           #-}
  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
  {-# HLINT ignore "Use isNothing" #-}
  
  -- | This module contains an SMTLIB2 interface for
  --   1. checking the validity, and,
  --   2. computing satisfying assignments
  --   for formulas.
  --   By implementing a binary interface over the SMTLIB2 format defined at
  --   http://www.smt-lib.org/
  --   http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf
  
  module Language.Fixpoint.Smt.Interface (
  
      -- * Commands
        Command  (..)
  
      -- * Responses
      , Response (..)
  
      -- * Typeclass for SMTLIB2 conversion
      , SMTLIB2 (..)
  
      -- * Creating and killing SMTLIB2 Process
      , Context (..)
      , makeContext
      , makeContextNoLog
      , makeContextWithSEnv
      , cleanupContext
  
      -- * Execute Queries
      , command
      , smtSetMbqi
  
      -- * Query API
      , smtDecl
      , smtDecls
      , smtDefineFunc
      , smtAssert
      , smtAssertDecl
      , smtFuncDecl
      , smtAssertAxiom
      , smtCheckUnsat
      , smtCheckSat
      , smtBracket, smtBracketAt
      , smtDistinct
      , smtPush, smtPop
  
      -- * Check Validity
      , checkValid
      , checkValid'
      , checkValidWithContext
      , checkValids
  
      , funcSortVars
  
      ) where
  
  import           Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags
                                                  , Config (solver, smtTimeout, gradual, stringTheory, save, allowHO))
  import qualified Language.Fixpoint.Misc          as Misc
  import           Language.Fixpoint.Types.Errors
  import           Language.Fixpoint.Utils.Files
  import           Language.Fixpoint.Types         hiding (allowHO)
  import qualified Language.Fixpoint.Types         as F
  import           Language.Fixpoint.Smt.Types
  import qualified Language.Fixpoint.Smt.Theories as Thy
  import           Language.Fixpoint.Smt.Serialize ()
  import           Control.Applicative      ((<|>))
  import           Control.Monad
  import           Control.Monad.State
  import           Control.Exception
  import           Data.ByteString.Builder (Builder)
  import qualified Data.ByteString.Builder as BS
  import qualified Data.ByteString.Lazy as LBS
  import qualified Data.ByteString.Lazy.Char8 as Char8
  import           Data.Char
  import qualified Data.HashMap.Strict      as M
  import           Data.List                (uncons)
  import           Data.Maybe              (fromMaybe)
  import qualified Data.Text                as T
  import qualified Data.Text.Encoding       as TE
  import qualified Data.Text.IO
  -- import           Data.Text.Format
  import qualified Data.Text.Lazy.IO        as LTIO
  import           System.Directory
  import           System.Console.CmdArgs.Verbosity
  import           System.FilePath
  import           System.IO
  import qualified Data.Attoparsec.Text     as A
  -- import qualified Data.HashMap.Strict      as M
  import           Data.Attoparsec.Internal.Types (Parser)
  import           Text.PrettyPrint.HughesPJ (text)
  import           Language.Fixpoint.SortCheck
  import           Language.Fixpoint.Utils.Builder as Builder
  -- import qualified Language.Fixpoint.Types as F
  -- import           Language.Fixpoint.Types.PrettyPrint (tracepp)
  import qualified SMTLIB.Backends
  import qualified SMTLIB.Backends.Process as Process
  import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
  import Control.Concurrent.Async (async)
  
  {-
  runFile f
    = readFile f >>= runString
  
  runString str
    = runCommands $ rr str
  
  runCommands cmds
    = do me   <- makeContext Z3
         mapM_ (T.putStrLn . smt2) cmds
         zs   <- mapM (command me) cmds
         return zs
  -}
  
  checkValidWithContext :: [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
  checkValidWithContext xts p q =
    smtBracket "checkValidWithContext" $
      checkValid' xts p q
  
  -- | type ClosedPred E = {v:Pred | subset (vars v) (keys E) }
  -- checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool
  checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
  checkValid cfg f xts p q = do
    me <- makeContext cfg f
    evalStateT (checkValid' xts p q) me
  
  checkValid' :: [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
  checkValid' xts p q = do
    smtDecls xts
    smtAssertDecl $ pAnd [p, PNot q]
    smtCheckUnsat
  
  -- | If you already HAVE a context, where all the variables have declared types
  --   (e.g. if you want to make MANY repeated Queries)
  
  -- checkValid :: e:Env -> [ClosedPred e] -> IO [Bool]
  checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
  checkValids cfg f xts ps = do
    me <- makeContext cfg f
    evalStateT (checkValids' xts ps) me
  
  checkValids' :: [(Symbol, Sort)] -> [Expr] -> SmtM [Bool]
  checkValids' xts ps = do
    smtDecls xts
    forM ps $ \p ->
       smtBracket "checkValids" $
         smtAssert (PNot p) >> smtCheckUnsat
  
  -- debugFile :: FilePath
  -- debugFile = "DEBUG.smt2"
  
  --------------------------------------------------------------------------------
  -- | SMT IO --------------------------------------------------------------------
  --------------------------------------------------------------------------------
  
  commandRaw :: Maybe Handle -> SMTLIB.Backends.Solver -> Bool -> Builder -> IO Response
  commandRaw ctxLog ctxSolver ctxVerbose cmdBS = do
    resp <- SMTLIB.Backends.command ctxSolver cmdBS
    let respTxt =
          TE.decodeUtf8With (const $ const $ Just ' ') $
          LBS.toStrict resp
    case A.parseOnly responseP respTxt of
      Left e  -> Misc.errorstar $ "SMTREAD:" ++ e
      Right r -> do
        let textResponse = "; SMT Says: " <> T.pack (show r)
        forM_ ctxLog $ \h ->
          Data.Text.IO.hPutStrLn h textResponse
        when ctxVerbose $
          Data.Text.IO.putStrLn textResponse
        return r
  
  --------------------------------------------------------------------------------
  {-# SCC command #-}
  command  :: Command -> SmtM Response
  --------------------------------------------------------------------------------
  command !cmd       = do
    -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
    --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
    ctxLog <- gets ctxLog
    ctxSolver <- gets ctxSolver
    ctxVerbose <- gets ctxVerbose
    cmdBS <- liftSym $ runSmt2 cmd
    forM_ ctxLog $ \h -> lift $ do
      BS.hPutBuilder h cmdBS
      LBS.hPutStr h "\n"
    lift $ case cmd of
      CheckSat   -> commandRaw ctxLog ctxSolver ctxVerbose cmdBS
      GetValue _ -> commandRaw ctxLog ctxSolver ctxVerbose cmdBS
      _          -> SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok
  
  -- | A variant of `command` that accepts a pre-built command
  commandB :: Builder -> SmtM Response
  --------------------------------------------------------------------------------
  commandB cmdBS       = do
    ctxLog <- gets ctxLog
    ctxSolver <- gets ctxSolver
    forM_ ctxLog $ \h -> lift $ do
      BS.hPutBuilder h cmdBS
      LBS.hPutStr h "\n"
    lift $ SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok
  
  smtSetMbqi :: SmtM ()
  smtSetMbqi = interact' SetMbqi
  
  type SmtParser a = Parser T.Text a
  
  responseP :: SmtParser Response
  responseP = {- SCC "responseP" -} A.char '(' *> sexpP
           <|> A.string "sat"     *> return Sat
           <|> A.string "unsat"   *> return Unsat
           <|> A.string "unknown" *> return Unknown
  
  sexpP :: SmtParser Response
  sexpP = {- SCC "sexpP" -} A.string "error" *> (Error <$> errorP)
       <|> Values <$> valuesP
  
  errorP :: SmtParser T.Text
  errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
  
  valuesP :: SmtParser [(Symbol, T.Text)]
  valuesP = A.many1' pairP <* A.char ')'
  
  pairP :: SmtParser (Symbol, T.Text)
  pairP = {- SCC "pairP" -}
    do A.skipSpace
       _ <- A.char '('
       !x <- symbolP
       A.skipSpace
       !v <- valueP
       _ <- A.char ')'
       return (x,v)
  
  symbolP :: SmtParser Symbol
  symbolP = {- SCC "symbolP" -} symbol <$> A.takeWhile1 (not . isSpace)
  
  valueP :: SmtParser T.Text
  valueP = {- SCC "valueP" -} negativeP
        <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
  
  negativeP :: SmtParser T.Text
  negativeP
    = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
         return $ "(" <> v <> ")"
  
  --------------------------------------------------------------------------
  -- | SMT Context ---------------------------------------------------------
  --------------------------------------------------------------------------
  
  --------------------------------------------------------------------------
  makeContext :: Config -> FilePath -> IO Context
  --------------------------------------------------------------------------
  makeContext cfg f
    = do mb_hLog <- if not (save cfg) then pure Nothing else do
             createDirectoryIfMissing True $ takeDirectory smtFile
             hLog <- openFile smtFile WriteMode
             hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64
             return $ Just hLog
         me   <- makeContext' cfg mb_hLog
         pre  <- smtPreamble cfg (solver cfg) me
         forM_ pre $ \line -> do
             SMTLIB.Backends.command_ (ctxSolver me) line
             forM_ mb_hLog $ \hLog -> do
                 BS.hPutBuilder hLog line
                 LBS.hPutStr hLog "\n"
         return me
      where
         smtFile = extFileName Smt2 f
  
  makeContextWithSEnv :: Config -> FilePath -> SymEnv -> DefinedFuns -> IO Context
  makeContextWithSEnv cfg f env defns = do
    ctx      <- makeContext cfg f
    let ctx' = ctx {ctxSymEnv = env, ctxDefines = defns}
    execStateT declare ctx'
  
  makeContextNoLog :: Config -> IO Context
  makeContextNoLog cfg = do
    me  <- makeContext' cfg Nothing
    pre <- smtPreamble cfg (solver cfg) me
    mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre
    return me
  
  makeProcess
    :: Maybe Handle
    -> Process.Config
    -> IO (SMTLIB.Backends.Backend, IO ())
  makeProcess ctxLog cfg
    = do handl@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg
         case ctxLog of
           Nothing -> return ()
           Just hLog -> void $ async $ forever
             (do errTxt <- LTIO.hGetLine hErr
                 LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> errTxt
             ) `catch` \ SomeException {} -> return ()
         let backend = Process.toBackend handl
         hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64
         hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64
         return (backend, Process.close handl)
  
  makeContext' :: Config -> Maybe Handle -> IO Context
  makeContext' cfg ctxLog
    = do let slv = solver cfg
         (backend, closeIO) <- case slv of
           Z3      ->
             {- "z3 -smt2 -in"                   -}
             {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
             {- "z3 -smtc -in MBQI=false"        -}
             makeProcess ctxLog $ Process.defaultConfig
                               { Process.exe = "z3"
                               , Process.args = ["-smt2", "-in"] }
           Z3mem   -> Conditional.Z3.makeZ3
           Mathsat -> makeProcess ctxLog $ Process.defaultConfig
                               { Process.exe = "mathsat"
                               , Process.args = ["-input=smt2"] }
           Cvc4    -> makeProcess ctxLog $
                        Process.defaultConfig
                               { Process.exe = "cvc4"
                               , Process.args = ["-L", "smtlib2"] }
           Cvc5    -> makeProcess ctxLog $
                        Process.defaultConfig
                               { Process.exe = "cvc5"
                               , Process.args = ["-L", "smtlib2", "--arrays-exp"] }
         solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend
         loud <- isLoud
         return Ctx { ctxSolver    = solver
                    , ctxElabF     = solverFlags slv
                    , ctxClose     = closeIO
                    , ctxLog       = ctxLog
                    , ctxVerbose   = loud
                    , ctxSymEnv    = mempty
                    , ctxIxs       = []
                    , ctxDefines   = mempty
                    -- This is a heurstic to avoid generating large sequences of unused `lam_arg` symbols
                    -- when there's no higher-order reasoning. It might require some tuning on larger codebases
                    -- if `unknown function/constant lam_arg$XXX` errors are encountered.
                    , ctxLams      = allowHO cfg
                    }
  
  -- | Close file handles and release the solver backend's resources.
  cleanupContext :: Context -> IO ()
  cleanupContext Ctx {..} = do
    maybe (return ()) (hCloseMe "ctxLog") ctxLog
    ctxClose
  
  hCloseMe :: String -> Handle -> IO ()
  hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)
  
  smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
  smtPreamble cfg s me
    | s == Z3 || s == Z3mem
      = do v <- getZ3Version me
           checkValidStringFlag Z3 v cfg
           return $ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
    | otherwise
      = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)
  
  getZ3Version :: Context -> IO [Int]
  getZ3Version me
    = do -- resp is like (:version "4.8.15")
         resp <- SMTLIB.Backends.command (ctxSolver me) "(get-info :version)"
         case Char8.split '"' resp of
           _:rText:_ -> do
             -- strip off potential " - build hashcode ..." suffix
             let vText = Char8.takeWhile (not . isSpace) rText
             let parsedComponents = [ reads (Char8.unpack cText) | cText <- Char8.split '.' vText ]
             sequence
               [ case pComponent of
                   [(c, "")] -> return c
                   xs -> error $ "Can't parse z3 version: " ++ show xs
               | pComponent <- parsedComponents
               ]
           xs -> error $ "Can't parse z3 (get-info :version): " ++ show xs
  
  checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
  checkValidStringFlag smt v cfg
    = when (noString smt v cfg) $
        die $ err dummySpan (text "stringTheory is only supported by z3 version >=4.2.2")
  
  noString :: SMTSolver -> [Int] -> Config -> Bool
  noString smt v cfg
    =  stringTheory cfg
    && not (smt == Z3 && (v >= [4, 4, 2]))
  
  -----------------------------------------------------------------------------
  -- | SMT Commands -----------------------------------------------------------
  -----------------------------------------------------------------------------
  
  smtPush, smtPop :: SmtM ()
  smtPush = interact' Push
  smtPop  = interact' Pop
  
  smtDecls :: [(Symbol, Sort)] -> SmtM ()
  smtDecls = mapM_ $ uncurry smtDecl
  
  smtDecl :: Symbol -> Sort -> SmtM ()
  smtDecl x t = do
    me <- get
    let env = seData (ctxSymEnv me)
    let ins' = sortSmtSort False env <$> ins
    let out' = sortSmtSort False env     out
    interact' (notracepp _msg $ Declare (symbolSafeText x) ins' out')
    where
      (ins, out) = deconSort t
      _msg       = "smtDecl: " ++ showpp (x, t, ins, out)
  
  smtFuncDecl :: T.Text -> ([SmtSort],  SmtSort) -> SmtM ()
  smtFuncDecl x (ts, t) = interact' (Declare x ts t)
  
  smtDataDecl :: [DataDecl] -> SmtM ()
  smtDataDecl ds = interact' (DeclData ds)
  
  deconSort :: Sort -> ([Sort], Sort)
  deconSort t = case functionSort t of
                  Just (_, ins, out) -> (ins, out)
                  Nothing            -> ([], t)
  
  -- hack now this is used only for checking gradual condition.
  smtCheckSat :: Expr -> SmtM Bool
  smtCheckSat p
   = smtAssert p >> (ans <$> command CheckSat)
   where
     ans Sat = True
     ans _   = False
  
  smtAssert :: Expr -> SmtM ()
  smtAssert p = interact' (Assert Nothing p)
  
  -- the following three functions will emit additional `apply`,
  -- `coerce`, and `lambda` symbols for fresh function sorts as needed
  smtAssertDecl :: Expr -> SmtM ()
  smtAssertDecl p = interactDecl' (Assert Nothing p)
  
  smtDefineEqn :: Equation -> SmtM ()
  smtDefineEqn Equ {..} = smtDefineFunc eqName eqArgs eqSort eqBody
  
  smtDefineFunc :: Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> SmtM ()
  smtDefineFunc name symList rsort e =
    do env <- gets (seData . ctxSymEnv)
       interactDecl' $
          DefineFunc
            name
            (map (sortSmtSort False env <$>) symList)
            (sortSmtSort False env rsort)
            e
  
  -----------------------------------------------------------------
  
  smtAssertAxiom :: Triggered Expr -> SmtM ()
  smtAssertAxiom p  = interact' (AssertAx p)
  
  smtDistinct :: [Expr] -> SmtM ()
  smtDistinct az = interact' (Distinct az)
  
  smtCheckUnsat :: SmtM Bool
  smtCheckUnsat = respSat <$> command CheckSat
  
  smtBracketAt :: SrcSpan -> String -> SmtM a -> SmtM a
  smtBracketAt sp _msg a =
    smtBracket _msg a `catchSMT` dieAt sp
  
  -- | `smtBracket` adds a new level to the apply stack and saves the last fresh index
  --   on the index stack before the action, and reverts these changes after the action.
  smtBracket :: String -> SmtM a -> SmtM a
  smtBracket _msg a = do
    smtPush
    modify $ \ctx ->
      let env = ctxSymEnv ctx in
      ctx { ctxSymEnv = env { seAppls = pushAppls (seAppls env) }
          , ctxIxs = seIx env : ctxIxs ctx}
    r <- a
    smtPop
    modify $ \ctx ->
      let env = ctxSymEnv ctx
          (i , is) = fromMaybe (0, []) (uncons $ ctxIxs ctx)
        in
      ctx { ctxSymEnv = env {seAppls = popAppls (seAppls env) , seIx = i}
          , ctxIxs = is}
    return r
  
  respSat :: Response -> Bool
  respSat Unsat   = True
  respSat Sat     = False
  respSat Unknown = False
  respSat r       = die $ err dummySpan $ text ("crash: SMTLIB2 respSat = " ++ show r)
  
  interact' :: Command -> SmtM ()
  interact' cmd  = void $ command cmd
  
  -- | a variant of `interact'` which also emits fresh
  --   `apply`, `coerce`, and `lambda` symbols
  interactDecl' :: Command -> SmtM ()
  interactDecl' cmd  = do
    cmdBS <- liftSym $ runSmt2 cmd
    ctx <- get
    let env = ctxSymEnv ctx
    let ats = funcSortVars (ctxLams ctx) env
    forM_ ats $ uncurry smtFuncDecl
    put (ctx {ctxSymEnv = env {seAppls = mergeTopAppls (seApplsCur env) (seAppls env), seApplsCur = M.empty} })
    void $ commandB cmdBS
  
  makeTimeout :: Config -> [Builder]
  makeTimeout cfg
    | Just i <- smtTimeout cfg = [ "\n(set-option :timeout " <> fromString (show i) <> ")\n"]
    | otherwise                = [""]
  
  
  makeMbqi :: Config -> [Builder]
  makeMbqi cfg
    | gradual cfg = [""]
    | otherwise   = ["\n(set-option :smt.mbqi false)"]
  
  
  --------------------------------------------------------------------------------
  declare :: SmtM ()
  --------------------------------------------------------------------------------
  declare = do
    me <- get
    let env        = ctxSymEnv me
    let xts        = symbolSorts (F.seSort env)
    let tx         = elaborate (ElabParam (ctxElabF me) "declare" env)
    let lts        = F.toListSEnv . F.seLits $ env
    let dss        = dataDeclarations          env
    let thyXTs     =             [ (x, t) | (x, t) <- xts, symKind env x == Just F.Uninterp ]
    let qryXTs     = fmap tx <$> [ (x, t) | (x, t) <- xts, symKind env x == Nothing ]
    -- let isKind n   = (n ==)  . symKind env . fst
    let MkDefinedFuns defs = ctxDefines me
    let ess        = distinctLiterals  lts
    let axs        = Thy.axiomLiterals lts
    forM_ dss              smtDataDecl
    forM_ thyXTs $ uncurry smtDecl
    forM_ qryXTs $ uncurry smtDecl
    forM_ defs             smtDefineEqn
    forM_ ess              smtDistinct
    forM_ axs              smtAssert
  
  symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
  symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ]
   where
    tx t@(FObj a) = fromMaybe t (F.lookupSEnv a env)
    tx t          = t
  
  dataDeclarations :: SymEnv -> [[DataDecl]]
  dataDeclarations = orderDeclarations . map snd . F.toListSEnv . F.seData
  
  funcSortVars :: Bool -> F.SymEnv -> [(T.Text, ([F.SmtSort], F.SmtSort))]
  funcSortVars lams env =
    -- TODO It would probably be even faster (if slightly) to convert `seApplsCur`
    -- to a key-value list and iterate over it, at least this way we can get rid of
    -- the unreachable `error` below.
                    [(var applyName  t       , appSort t) | t <- ts]
    ++              [(var coerceName t       , ([t1],t2)) | t@(t1, t2) <- ts]
    ++              [(var lambdaName t       , lamSort t) | t <- ts]
    ++ if lams then [(var (lamArgSymbol i) t , argSort t) | t@(_,F.SInt) <- ts, i <- [1..Thy.maxLamArg] ] else []
    where
      var :: F.Symbol -> F.FuncSort -> T.Text
      var n t       =
        case M.lookup t (F.seApplsCur env) of
          Just i  -> symbolAtSortIndex n i
          Nothing -> error "funcSortVars: no index for sort in seApplsCur"
      ts            = M.keys $ F.seApplsCur env
      appSort (s,t) = ([F.SInt, s], t)
      lamSort (s,t) = ([s, t], F.SInt)
      argSort (s,_) = ([]    , s)
  
  symKind :: F.SymEnv -> F.Symbol -> Maybe Sem
  symKind env x = F.tsInterp <$> F.symEnvTheory x env
  
  -- | `distinctLiterals` is used solely to determine the set of literals
  --   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,
  --   or string literals "cat", "dog", "mouse". These should only include
  --   non-function sorted values.
  distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
  distinctLiterals xts = [ es | (_, es) <- tess ]
     where
      tess             = Misc.groupList [(t, F.expr x) | (x, t) <- xts, notFun t]
      notFun           = not . F.isFunctionSortedReft . (`F.RR` F.trueReft)
      -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)
  