module Agda.Auto.Auto
      (auto
      , AutoResult(..)
      , AutoProgress(..)
      ) where

import Prelude hiding ((!!), null)

import Control.Monad          ( filterM, forM, guard, join, when )
import Control.Monad.Except
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.State

import qualified Data.List as List
import qualified Data.Map as Map
import Data.IORef
import qualified System.Timeout
import Data.Maybe
import qualified Data.Traversable as Trav
import qualified Data.HashMap.Strict as HMap

import Agda.Utils.Permutation (permute, takeP)
import Agda.TypeChecking.Monad hiding (withCurrentModule)
import Agda.TypeChecking.Telescope
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty (prettyA)
import qualified Agda.Syntax.Concrete.Name as C
import qualified Text.PrettyPrint as PP
import qualified Agda.TypeChecking.Pretty as TCM
import Agda.Syntax.Position
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcreteScope, abstractToConcrete_, runAbsToCon, toConcrete)
import Agda.Interaction.Base
import Agda.Interaction.BasicOps hiding (refine)
import Agda.TypeChecking.Reduce (normalise)
import Agda.Syntax.Common
import qualified Agda.Syntax.Scope.Base as Scope
import Agda.Syntax.Scope.Monad (withCurrentModule)
import qualified Agda.Syntax.Abstract.Name as AN
import qualified Agda.TypeChecking.Monad.Base as TCM
import Agda.TypeChecking.EtaContract (etaContract)

import Agda.Auto.Options
import Agda.Auto.Convert
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.SearchControl
import Agda.Auto.Typecheck

import Agda.Auto.CaseSplit

import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Tuple


insertAbsurdPattern :: String -> String
insertAbsurdPattern :: [Char] -> [Char]
insertAbsurdPattern [] = []
insertAbsurdPattern s :: [Char]
s@(Char
_:[Char]
_) | Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
abspatvarname) [Char]
s [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
abspatvarname = [Char]
"()" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
abspatvarname) [Char]
s
insertAbsurdPattern (Char
c:[Char]
s) = Char
c Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
insertAbsurdPattern [Char]
s

getHeadAsHint :: A.Expr -> Maybe Hint
getHeadAsHint :: Expr -> Maybe Hint
getHeadAsHint (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Maybe Hint
getHeadAsHint Expr
e
getHeadAsHint (A.Def QName
qname)      = Hint -> Maybe Hint
forall a. a -> Maybe a
Just (Hint -> Maybe Hint) -> Hint -> Maybe Hint
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Hint
Hint Bool
False QName
qname
getHeadAsHint (A.Proj ProjOrigin
_ AmbiguousQName
qname)   = Hint -> Maybe Hint
forall a. a -> Maybe a
Just (Hint -> Maybe Hint) -> Hint -> Maybe Hint
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Hint
Hint Bool
False (QName -> Hint) -> QName -> Hint
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
AN.headAmbQ AmbiguousQName
qname
getHeadAsHint (A.Con AmbiguousQName
qname)      = Hint -> Maybe Hint
forall a. a -> Maybe a
Just (Hint -> Maybe Hint) -> Hint -> Maybe Hint
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Hint
Hint Bool
True  (QName -> Hint) -> QName -> Hint
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
AN.headAmbQ AmbiguousQName
qname
getHeadAsHint Expr
_ = Maybe Hint
forall a. Maybe a
Nothing

-- | Result type: Progress & potential Message for the user
--
--   The  of the Auto tactic can be one of the following three:
--
--   1. @Solutions [(ii,s)]@
--      A list of solutions @s@ for interaction ids @ii@.
--      In particular, @Solutions []@ means Agsy found no solution.
--
--   2. @FunClauses cs@
--      A list of clauses for the interaction id @ii@ in which Auto
--      was invoked with case-splitting turned on.
--
--   3. @Refinement s@
--      A refinement for the interaction id @ii@ in which Auto was invoked.

data AutoProgress =
    Solutions  [(InteractionId, String)]
  | FunClauses [String]
  | Refinement String

data AutoResult = AutoResult
  { AutoResult -> AutoProgress
autoProgress :: AutoProgress
  , AutoResult -> Maybe [Char]
autoMessage  :: Maybe String
  }

stopWithMsg :: String -> TCM AutoResult
stopWithMsg :: [Char] -> TCM AutoResult
stopWithMsg [Char]
msg = AutoResult -> TCM AutoResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe [Char] -> AutoResult
AutoResult ([(InteractionId, [Char])] -> AutoProgress
Solutions []) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
msg)

-- | Entry point for Auto tactic (Agsy).
--
--   If the @autoMessage@ part of the result is set to @Just msg@, the
--   message @msg@ produced by Agsy should be displayed to the user.

{-# SPECIALIZE auto :: InteractionId -> Range -> String -> TCM AutoResult #-}
auto
  :: MonadTCM tcm
  => InteractionId
  -> Range
  -> String
  -> tcm AutoResult
auto :: forall (tcm :: * -> *).
MonadTCM tcm =>
InteractionId -> Range -> [Char] -> tcm AutoResult
auto InteractionId
ii Range
rng [Char]
argstr = TCM AutoResult -> tcm AutoResult
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM AutoResult -> tcm AutoResult)
-> TCM AutoResult -> tcm AutoResult
forall a b. (a -> b) -> a -> b
$ Lens' Bool TCEnv
-> (Bool -> Bool) -> TCM AutoResult -> TCM AutoResult
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' Bool TCEnv
eMakeCase (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCM AutoResult -> TCM AutoResult)
-> TCM AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ do

  -- Parse hints and other configuration.
  let autoOptions :: AutoOptions
autoOptions = [Char] -> AutoOptions
parseArgs [Char]
argstr
  let hints :: [[Char]]
hints    = AutoOptions
autoOptions AutoOptions -> Lens' [[Char]] AutoOptions -> [[Char]]
forall o i. o -> Lens' i o -> i
^. ([[Char]] -> f [[Char]]) -> AutoOptions -> f AutoOptions
Lens' [[Char]] AutoOptions
aoHints
  let timeout :: TimeOut
timeout  = AutoOptions
autoOptions AutoOptions -> Lens' TimeOut AutoOptions -> TimeOut
forall o i. o -> Lens' i o -> i
^. (TimeOut -> f TimeOut) -> AutoOptions -> f AutoOptions
Lens' TimeOut AutoOptions
aoTimeOut
  let pick :: Int
pick     = AutoOptions
autoOptions AutoOptions -> Lens' Int AutoOptions -> Int
forall o i. o -> Lens' i o -> i
^. (Int -> f Int) -> AutoOptions -> f AutoOptions
Lens' Int AutoOptions
aoPick
  let mode :: Mode
mode     = AutoOptions
autoOptions AutoOptions -> Lens' Mode AutoOptions -> Mode
forall o i. o -> Lens' i o -> i
^. (Mode -> f Mode) -> AutoOptions -> f AutoOptions
Lens' Mode AutoOptions
aoMode
  let hintmode :: AutoHintMode
hintmode = AutoOptions
autoOptions AutoOptions -> Lens' AutoHintMode AutoOptions -> AutoHintMode
forall o i. o -> Lens' i o -> i
^. (AutoHintMode -> f AutoHintMode) -> AutoOptions -> f AutoOptions
Lens' AutoHintMode AutoOptions
aoHintMode
  [Expr]
ahints <- case Mode
mode of
    MRefine{} -> [Expr] -> TCMT IO [Expr]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Mode
_         -> ([Char] -> TCMT IO Expr) -> [[Char]] -> TCMT IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (InteractionId -> Range -> [Char] -> TCMT IO Expr
parseExprIn InteractionId
ii Range
rng) [[Char]]
hints
  let failHints :: TCM AutoResult
failHints = [Char] -> TCM AutoResult
stopWithMsg [Char]
"Hints must be a list of constant names"

  [Hint]
eqstuff <- InteractionId -> Range -> TCM [Hint]
getEqCombinators InteractionId
ii Range
rng

  Maybe [Hint]
-> TCM AutoResult -> ([Hint] -> TCM AutoResult) -> TCM AutoResult
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((Expr -> Maybe Hint) -> [Expr] -> Maybe [Hint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> Maybe Hint
getHeadAsHint [Expr]
ahints) TCM AutoResult
failHints (([Hint] -> TCM AutoResult) -> TCM AutoResult)
-> ([Hint] -> TCM AutoResult) -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ \ [Hint]
ehints -> do

    -- Get the meta variable for the interaction point we are trying to fill.
    -- Add the @autohints@ for that meta to the hints collection.
    MetaId
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
    Maybe (QName, Clause, Bool)
thisdefinfo <- InteractionId -> TCM (Maybe (QName, Clause, Bool))
findClauseDeep InteractionId
ii
    [Hint]
ehints <- ([Hint]
ehints [Hint] -> [Hint] -> [Hint]
forall a. [a] -> [a] -> [a]
++) ([Hint] -> [Hint]) -> TCM [Hint] -> TCM [Hint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do AutoHintMode -> MetaId -> Maybe QName -> TCM [Hint]
autohints AutoHintMode
hintmode MetaId
mi (Maybe QName -> TCM [Hint]) -> Maybe QName -> TCM [Hint]
forall a b. (a -> b) -> a -> b
$ ((QName, Clause, Bool) -> QName)
-> Maybe (QName, Clause, Bool) -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName, Clause, Bool) -> QName
forall a b c. (a, b, c) -> a
fst3 Maybe (QName, Clause, Bool)
thisdefinfo

    -- If @thisdefinfo /= Nothing@ get the its type (normalized).
    [Type]
mrectyp <- Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Maybe Type -> [Type]) -> TCMT IO (Maybe Type) -> TCMT IO [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Maybe (QName, Clause, Bool)
-> ((QName, Clause, Bool) -> TCMT IO Type) -> TCMT IO (Maybe Type)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe (QName, Clause, Bool)
thisdefinfo (((QName, Clause, Bool) -> TCMT IO Type) -> TCMT IO (Maybe Type))
-> ((QName, Clause, Bool) -> TCMT IO Type) -> TCMT IO (Maybe Type)
forall a b. (a -> b) -> a -> b
$ \ (QName
def, Clause
_, Bool
_) -> do
        Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do Definition -> Type
TCM.defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
def

    ([ConstRef O]
myhints', [MM (Exp O) (RefInfo O)]
mymrectyp, Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons, [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
eqcons, Map QName (TMode, ConstRef O)
cmap) <- MetaId
-> [Hint]
-> [Type]
-> TCM
     ([ConstRef O], [MM (Exp O) (RefInfo O)],
      Map
        MetaId
        (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
         [MM (Exp O) (RefInfo O)], [MetaId]),
      [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))],
      Map QName (TMode, ConstRef O))
tomy MetaId
mi ([Hint]
ehints [Hint] -> [Hint] -> [Hint]
forall a. [a] -> [a] -> [a]
++ [Hint]
eqstuff) [Type]
mrectyp

    let ([ConstRef O]
myhints, [ConstRef O]
c1to6) = Int -> [ConstRef O] -> ([ConstRef O], [ConstRef O])
forall a. Int -> [a] -> ([a], [a])
splitAt ([ConstRef O] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstRef O]
myhints' Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Hint] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Hint]
eqstuff) [ConstRef O]
myhints'
        meqr :: Maybe (EqReasoningConsts O)
meqr = [Hint]
-> Maybe (EqReasoningConsts O)
-> ([Hint] -> Maybe (EqReasoningConsts O))
-> Maybe (EqReasoningConsts O)
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull [Hint]
eqstuff Maybe (EqReasoningConsts O)
forall a. Maybe a
Nothing (([Hint] -> Maybe (EqReasoningConsts O))
 -> Maybe (EqReasoningConsts O))
-> ([Hint] -> Maybe (EqReasoningConsts O))
-> Maybe (EqReasoningConsts O)
forall a b. (a -> b) -> a -> b
$ \ [Hint]
_ -> {- else -}
                 let [ConstRef O
c1, ConstRef O
c2, ConstRef O
c3, ConstRef O
c4, ConstRef O
c5, ConstRef O
c6] = [ConstRef O]
c1to6
                 in  EqReasoningConsts O -> Maybe (EqReasoningConsts O)
forall a. a -> Maybe a
Just (EqReasoningConsts O -> Maybe (EqReasoningConsts O))
-> EqReasoningConsts O -> Maybe (EqReasoningConsts O)
forall a b. (a -> b) -> a -> b
$ ConstRef O
-> ConstRef O
-> ConstRef O
-> ConstRef O
-> ConstRef O
-> ConstRef O
-> EqReasoningConsts O
forall o.
ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> EqReasoningConsts o
EqReasoningConsts ConstRef O
c1 ConstRef O
c2 ConstRef O
c3 ConstRef O
c4 ConstRef O
c5 ConstRef O
c6


    let tcSearchSC :: Bool -> Ctx O -> CExp O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
tcSearchSC Bool
isdep Ctx O
ctx CExp O
typ MM (Exp O) (RefInfo O)
trm = Maybe (EqReasoningConsts O)
-> EE (MyPB O)
-> (EqReasoningConsts O -> EE (MyPB O))
-> EE (MyPB O)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (EqReasoningConsts O)
meqr EE (MyPB O)
a ((EqReasoningConsts O -> EE (MyPB O)) -> EE (MyPB O))
-> (EqReasoningConsts O -> EE (MyPB O)) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ \ EqReasoningConsts O
eqr ->
          Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo O) -> EE (MyPB O))
-> Prop (RefInfo O) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ EE (MyPB O) -> EE (MyPB O) -> Prop (RefInfo O)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (EqReasoningConsts O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState EqReasoningConsts O
eqr MM (Exp O) (RefInfo O)
trm) EE (MyPB O)
a
          where a :: EE (MyPB O)
a = Bool -> Ctx O -> CExp O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch Bool
isdep Ctx O
ctx CExp O
typ MM (Exp O) (RefInfo O)
trm

    let (Metavar (Exp O) (RefInfo O)
mainm, MM (Exp O) (RefInfo O)
_, [MM (Exp O) (RefInfo O)]
_, [MetaId]
_) = Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> MetaId
-> (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
    [MM (Exp O) (RefInfo O)], [MetaId])
forall k a. Ord k => Map k a -> k -> a
Map.! MetaId
mi
    case Mode
mode of
     MNormal Bool
listmode Bool
disprove -> do
        let numsols :: Int
numsols = if Bool
listmode then Int
10 else Int
1
          -- Andreas, 2015-05-17 Issue 1504:
          -- wish to produce several solutions, as
          -- the first one might be ill-typed.
          -- However, currently changing the 1 to something higher makes Agsy loop.
        IORef [[Term]]
sols <- IO (IORef [[Term]]) -> TCMT IO (IORef [[Term]])
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef [[Term]]) -> TCMT IO (IORef [[Term]]))
-> IO (IORef [[Term]]) -> TCMT IO (IORef [[Term]])
forall a b. (a -> b) -> a -> b
$ [[Term]] -> IO (IORef [[Term]])
forall a. a -> IO (IORef a)
newIORef ([] :: [[I.Term]])
        IORef Int
nsol <- IO (IORef Int) -> TCMT IO (IORef Int)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef Int) -> TCMT IO (IORef Int))
-> IO (IORef Int) -> TCMT IO (IORef Int)
forall a b. (a -> b) -> a -> b
$ Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef (Int -> IO (IORef Int)) -> Int -> IO (IORef Int)
forall a b. (a -> b) -> a -> b
$ Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numsols
        let hsol :: IO ()
hsol = do
             Int
nsol' <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
             let cond :: Bool
cond = Int
nsol' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
numsols
             Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cond (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
               Either [Char] [Term]
trms <- ExceptT [Char] IO [Term] -> IO (Either [Char] [Term])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
                       (ExceptT [Char] IO [Term] -> IO (Either [Char] [Term]))
-> ExceptT [Char] IO [Term] -> IO (Either [Char] [Term])
forall a b. (a -> b) -> a -> b
$ ((Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
  [MM (Exp O) (RefInfo O)], [MetaId])
 -> ExceptT [Char] IO Term)
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
-> ExceptT [Char] IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ (Metavar (Exp O) (RefInfo O)
m , MM (Exp O) (RefInfo O)
_, [MM (Exp O) (RefInfo O)]
_, [MetaId]
_) -> MM (Exp O) (RefInfo O) -> ExceptT [Char] IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Metavar (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O)
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m) :: MOT I.Term)
                       ([(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])]
 -> ExceptT [Char] IO [Term])
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
-> ExceptT [Char] IO [Term]
forall a b. (a -> b) -> a -> b
$ Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons
               case Either [Char] [Term]
trms of
                 Left{}     -> IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
nsol (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$! Int
nsol' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                 Right [Term]
trms -> IORef [[Term]] -> ([[Term]] -> [[Term]]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[Term]]
sols ([Term]
trms [Term] -> [[Term]] -> [[Term]]
forall a. a -> [a] -> [a]
:)
                 -- Right trms -> if listmode then modifyIORef sols (trms :)
                 --                           else writeIORef sols [trms]
        IORef Int
ticks <- IO (IORef Int) -> TCMT IO (IORef Int)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef Int) -> TCMT IO (IORef Int))
-> IO (IORef Int) -> TCMT IO (IORef Int)
forall a b. (a -> b) -> a -> b
$ Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0

        let exsearch :: EE (MyPB O)
-> Maybe ([CSPat O], ConstRef O) -> Int -> TCMT IO (Maybe Bool)
exsearch EE (MyPB O)
initprop Maybe ([CSPat O], ConstRef O)
recinfo Int
defdfv =
             IO (Maybe Bool) -> TCMT IO (Maybe Bool)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Bool) -> TCMT IO (Maybe Bool))
-> IO (Maybe Bool) -> TCMT IO (Maybe Bool)
forall a b. (a -> b) -> a -> b
$ Int -> IO Bool -> IO (Maybe Bool)
forall a. Int -> IO a -> IO (Maybe a)
System.Timeout.timeout (TimeOut -> Int
getTimeOut TimeOut
timeout Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000)
                    (IO Bool -> IO (Maybe Bool)) -> IO Bool -> IO (Maybe Bool)
forall a b. (a -> b) -> a -> b
$ Cost -> IO Bool
loop Cost
0
             where
               loop :: Cost -> IO Bool
loop Cost
d = do
                 let rechint :: [(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)]
rechint [(ConstRef O, HintMode)]
x = case Maybe ([CSPat O], ConstRef O)
recinfo of
                                  Maybe ([CSPat O], ConstRef O)
Nothing -> [(ConstRef O, HintMode)]
x
                                  Just ([CSPat O]
_, ConstRef O
recdef) -> (ConstRef O
recdef, HintMode
HMRecCall) (ConstRef O, HintMode)
-> [(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)]
forall a. a -> [a] -> [a]
: [(ConstRef O, HintMode)]
x
                     env :: RefInfo O
env = RIEnv { rieHints :: [(ConstRef O, HintMode)]
rieHints             = [(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)]
rechint ([(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)])
-> [(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)]
forall a b. (a -> b) -> a -> b
$ (ConstRef O -> (ConstRef O, HintMode))
-> [ConstRef O] -> [(ConstRef O, HintMode)]
forall a b. (a -> b) -> [a] -> [b]
map (,HintMode
HMNormal) [ConstRef O]
myhints
                                 , rieDefFreeVars :: Int
rieDefFreeVars       = Int
defdfv
                                 , rieEqReasoningConsts :: Maybe (EqReasoningConsts O)
rieEqReasoningConsts = Maybe (EqReasoningConsts O)
meqr
                                 }
                 Bool
depreached <- IORef Int
-> IORef Int
-> IO ()
-> RefInfo O
-> EE (MyPB O)
-> Cost
-> Cost
-> IO Bool
forall blk.
IORef Int
-> IORef Int
-> IO ()
-> blk
-> MetaEnv (PB blk)
-> Cost
-> Cost
-> IO Bool
topSearch IORef Int
ticks IORef Int
nsol IO ()
hsol RefInfo O
env (EE (MyPB O)
initprop) Cost
d Cost
costIncrease
                 Int
nsol' <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
                 if Int
nsol' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Bool
depreached then Cost -> IO Bool
loop (Cost
d Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
+ Cost
costIncrease) else Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
depreached

        let getsols :: [I.Term] -> TCM [(MetaId, A.Expr)]
            getsols :: [Term] -> TCM [(MetaId, Expr)]
getsols [Term]
sol = do
             [(MetaId, Expr)]
exprs <- [(MetaId, Term)]
-> ((MetaId, Term) -> TCMT IO (MetaId, Expr))
-> TCM [(MetaId, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([MetaId] -> [Term] -> [(MetaId, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> [MetaId]
forall k a. Map k a -> [k]
Map.keys Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons) [Term]
sol) (((MetaId, Term) -> TCMT IO (MetaId, Expr))
 -> TCM [(MetaId, Expr)])
-> ((MetaId, Term) -> TCMT IO (MetaId, Expr))
-> TCM [(MetaId, Expr)]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Term
e) -> do
               MetaVariable
mv   <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
               Term
e    <- Term -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
e
               Expr
expr <- Expr -> Expr
modifyAbstractExpr (Expr -> Expr) -> TCMT IO Expr -> TCMT IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Closure Range -> TCMT IO Expr -> TCMT IO Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO Expr -> TCMT IO Expr) -> TCMT IO Expr -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
e
               (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
mi, Expr
expr)

             let loop :: I.MetaId -> StateT [I.MetaId] TCM [(I.MetaId, A.Expr)]
                 loop :: MetaId -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
loop MetaId
midx = do
                   let (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
_, [MM (Exp O) (RefInfo O)]
_, [MetaId]
deps) = Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> MetaId
-> (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
    [MM (Exp O) (RefInfo O)], [MetaId])
forall k a. Ord k => Map k a -> k -> a
Map.! MetaId
midx
                   [[(MetaId, Expr)]]
asolss <- (MetaId -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)])
-> [MetaId] -> StateT [MetaId] (TCMT IO) [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MetaId -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
loop [MetaId]
deps
                   [MetaId]
dones  <- StateT [MetaId] (TCMT IO) [MetaId]
forall s (m :: * -> *). MonadState s m => m s
get
                   [(MetaId, Expr)]
asols  <- if MetaId
midx MetaId -> [MetaId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaId]
dones then [(MetaId, Expr)] -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
forall a. a -> StateT [MetaId] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                     [MetaId] -> StateT [MetaId] (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MetaId
midx MetaId -> [MetaId] -> [MetaId]
forall a. a -> [a] -> [a]
: [MetaId]
dones)
                     [(MetaId, Expr)] -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
forall a. a -> StateT [MetaId] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(MetaId
midx, Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe Expr
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Expr -> Expr) -> Maybe Expr -> Expr
forall a b. (a -> b) -> a -> b
$ MetaId -> [(MetaId, Expr)] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
midx [(MetaId, Expr)]
exprs)]
                   [(MetaId, Expr)] -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
forall a. a -> StateT [MetaId] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(MetaId, Expr)] -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)])
-> [(MetaId, Expr)] -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
forall a b. (a -> b) -> a -> b
$ [[(MetaId, Expr)]] -> [(MetaId, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(MetaId, Expr)]]
asolss [(MetaId, Expr)] -> [(MetaId, Expr)] -> [(MetaId, Expr)]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Expr)]
asols
             ([(MetaId, Expr)]
asols, [MetaId]
_) <- StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
-> [MetaId] -> TCMT IO ([(MetaId, Expr)], [MetaId])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (MetaId -> StateT [MetaId] (TCMT IO) [(MetaId, Expr)]
loop MetaId
mi) []
             [(MetaId, Expr)] -> TCM [(MetaId, Expr)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(MetaId, Expr)]
asols

        if Bool
disprove then
          case [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
eqcons of
           [] -> case Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons of
            (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mytype, [MM (Exp O) (RefInfo O)]
mylocalVars, [MetaId]
_) : [] -> do
                Int
defdfv <- case Maybe (QName, Clause, Bool)
thisdefinfo of
                           Just (QName
def, Clause
_, Bool
_) -> MetaId -> QName -> TCMT IO Int
getdfv MetaId
mi QName
def
                           Maybe (QName, Clause, Bool)
Nothing -> Int -> TCMT IO Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
                ConstRef O
ee <- IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCMT IO (ConstRef O))
-> IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef O -> IO (ConstRef O)) -> ConstDef O -> IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef {cdname :: [Char]
cdname = [Char]
"T", cdorigin :: O
cdorigin = O
forall a. HasCallStack => a
__IMPOSSIBLE__, cdtype :: MM (Exp O) (RefInfo O)
cdtype = Exp O -> MM (Exp O) (RefInfo O)
forall a blk. a -> MM a blk
NotM (Exp O -> MM (Exp O) (RefInfo O))
-> Exp O -> MM (Exp O) (RefInfo O)
forall a b. (a -> b) -> a -> b
$ Sort -> Exp O
forall o. Sort -> Exp o
Sort (Int -> Sort
Set Int
0), cdcont :: DeclCont O
cdcont = DeclCont O
forall o. DeclCont o
Postulate, cddeffreevars :: Int
cddeffreevars = Int
0}
                let ([MM (Exp O) (RefInfo O)]
restargs, [MM (Exp O) (RefInfo O)]
modargs) = Int
-> [MM (Exp O) (RefInfo O)]
-> ([MM (Exp O) (RefInfo O)], [MM (Exp O) (RefInfo O)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([MM (Exp O) (RefInfo O)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MM (Exp O) (RefInfo O)]
mylocalVars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
defdfv) [MM (Exp O) (RefInfo O)]
mylocalVars
                    mytype' :: MM (Exp O) (RefInfo O)
mytype' = (MM (Exp O) (RefInfo O)
 -> MM (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O))
-> MM (Exp O) (RefInfo O)
-> [MM (Exp O) (RefInfo O)]
-> MM (Exp O) (RefInfo O)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MM (Exp O) (RefInfo O)
x MM (Exp O) (RefInfo O)
y -> Exp O -> MM (Exp O) (RefInfo O)
forall a blk. a -> MM a blk
NotM (Exp O -> MM (Exp O) (RefInfo O))
-> Exp O -> MM (Exp O) (RefInfo O)
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> Hiding
-> Bool
-> MM (Exp O) (RefInfo O)
-> Abs (MM (Exp O) (RefInfo O))
-> Exp O
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing Hiding
NotHidden (Int -> MM (Exp O) (RefInfo O) -> Bool
forall o. Int -> MExp o -> Bool
freeIn Int
0 MM (Exp O) (RefInfo O)
y) MM (Exp O) (RefInfo O)
y (MId -> MM (Exp O) (RefInfo O) -> Abs (MM (Exp O) (RefInfo O))
forall a. MId -> a -> Abs a
Abs MId
NoId MM (Exp O) (RefInfo O)
x)) MM (Exp O) (RefInfo O)
mytype [MM (Exp O) (RefInfo O)]
restargs
                    htyp :: MM (Exp O) (RefInfo O)
htyp = ConstRef O -> MM (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O)
forall o. ConstRef o -> MExp o -> MExp o
negtype ConstRef O
ee MM (Exp O) (RefInfo O)
mytype'
                    sctx :: Ctx O
sctx = ([Char] -> MId
Id [Char]
"h", MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
htyp) (MId, CExp O) -> Ctx O -> Ctx O
forall a. a -> [a] -> [a]
: (MM (Exp O) (RefInfo O) -> (MId, CExp O))
-> [MM (Exp O) (RefInfo O)] -> Ctx O
forall a b. (a -> b) -> [a] -> [b]
map (\MM (Exp O) (RefInfo O)
x -> (MId
NoId, MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
x)) [MM (Exp O) (RefInfo O)]
modargs
                    ntt :: CExp O
ntt = MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify (Exp O -> MM (Exp O) (RefInfo O)
forall a blk. a -> MM a blk
NotM (Exp O -> MM (Exp O) (RefInfo O))
-> Exp O -> MM (Exp O) (RefInfo O)
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> OKHandle (RefInfo O) -> Elr O -> MArgList O -> Exp O
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo O)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (ConstRef O -> Elr O
forall o. ConstRef o -> Elr o
Const ConstRef O
ee) (ArgList O -> MArgList O
forall a blk. a -> MM a blk
NotM ArgList O
forall o. ArgList o
ALNil))
                Maybe Bool
res <- EE (MyPB O)
-> Maybe ([CSPat O], ConstRef O) -> Int -> TCMT IO (Maybe Bool)
exsearch (Bool -> Ctx O -> CExp O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
tcSearchSC Bool
False Ctx O
sctx CExp O
ntt (Metavar (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O)
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m)) Maybe ([CSPat O], ConstRef O)
forall a. Maybe a
Nothing Int
defdfv
                [[Term]]
rsols <- ([[Term]] -> [[Term]]) -> TCMT IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Term]] -> [[Term]]
forall a. [a] -> [a]
reverse (TCMT IO [[Term]] -> TCMT IO [[Term]])
-> TCMT IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> a -> b
$ IO [[Term]] -> TCMT IO [[Term]]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [[Term]] -> TCMT IO [[Term]])
-> IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> a -> b
$ IORef [[Term]] -> IO [[Term]]
forall a. IORef a -> IO a
readIORef IORef [[Term]]
sols
                if [[Term]] -> Bool
forall a. Null a => a -> Bool
null [[Term]]
rsols then do
                  Int
nsol' <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
                  [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffsols (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nsol')
                 else do
                  [[(MetaId, Expr)]]
aexprss <- ([Term] -> TCM [(MetaId, Expr)])
-> [[Term]] -> TCMT IO [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [Term] -> TCM [(MetaId, Expr)]
getsols [[Term]]
rsols
                  [[(MetaId, Expr)]]
cexprss <- [[(MetaId, Expr)]]
-> ([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> TCMT IO [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[(MetaId, Expr)]]
aexprss (([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
 -> TCMT IO [[(MetaId, Expr)]])
-> ([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> TCMT IO [[(MetaId, Expr)]]
forall a b. (a -> b) -> a -> b
$ ((MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> [(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((MetaId, Expr) -> TCMT IO (MetaId, Expr))
 -> [(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> ((MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> [(MetaId, Expr)]
-> TCMT IO [(MetaId, Expr)]
forall a b. (a -> b) -> a -> b
$ \(MetaId
mi, Expr
e) -> do
                    MetaVariable
mv <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
                    Closure Range -> TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall a b. (a -> b) -> a -> b
$ do
                      (MetaId
mi,) (Expr -> (MetaId, Expr)) -> TCMT IO Expr -> TCMT IO (MetaId, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Expr
e
                  let ss :: Expr -> [Char]
ss = (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') ([Char] -> [Char]) -> (Expr -> [Char]) -> Expr -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') ([Char] -> [Char]) -> (Expr -> [Char]) -> Expr -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow
                      disp :: [(MetaId, Expr)] -> [Char]
disp [(MetaId
_, Expr
cexpr)] = Expr -> [Char]
ss Expr
cexpr
                      disp [(MetaId, Expr)]
cexprs = ((MetaId, Expr) -> [Char]) -> [(MetaId, Expr)] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (MetaId
mi, Expr
cexpr) -> Expr -> [Char]
ss Expr
cexpr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ") [(MetaId, Expr)]
cexprs
                  Int
ticks <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ticks
                  [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
                    ([Char]
"Listing disproof(s) " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
pick [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Term]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Term]]
rsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
                    [([(MetaId, Expr)], Int)]
-> (([(MetaId, Expr)], Int) -> [Char]) -> [[Char]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for ([[(MetaId, Expr)]] -> [Int] -> [([(MetaId, Expr)], Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[(MetaId, Expr)]]
cexprss [Int
pick..]) (\ ([(MetaId, Expr)]
x, Int
y) -> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Expr)] -> [Char]
disp [(MetaId, Expr)]
x)
            [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
  [MM (Exp O) (RefInfo O)], [MetaId])]
_ -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"Metavariable dependencies not allowed in disprove mode"
           [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
_ -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"Metavariable dependencies not allowed in disprove mode"
         else do
          (Maybe ([CSPat O], ConstRef O)
recinfo, Int
defdfv) <-
           case Maybe (QName, Clause, Bool)
thisdefinfo of
            Just (QName
def, Clause
clause, Bool
_) -> do
             let [MM (Exp O) (RefInfo O)
rectyp'] = [MM (Exp O) (RefInfo O)]
mymrectyp
             Int
defdfv <- MetaId -> QName -> TCMT IO Int
getdfv MetaId
mi QName
def
             ConstRef O
myrecdef <- IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCMT IO (ConstRef O))
-> IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef O -> IO (ConstRef O)) -> ConstDef O -> IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef {cdname :: [Char]
cdname = [Char]
"", cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName
def), cdtype :: MM (Exp O) (RefInfo O)
cdtype = MM (Exp O) (RefInfo O)
rectyp', cdcont :: DeclCont O
cdcont = DeclCont O
forall o. DeclCont o
Postulate, cddeffreevars :: Int
cddeffreevars = Int
defdfv}
             ([(Hiding, MId)]
_, [CSPat O]
pats) <- Map QName (TMode, ConstRef O)
-> MetaId -> Clause -> TCM ([(Hiding, MId)], [CSPat O])
constructPats Map QName (TMode, ConstRef O)
cmap MetaId
mi Clause
clause
             Int
defdfv <- MetaId -> QName -> TCMT IO Int
getdfv MetaId
mi QName
def
             (Maybe ([CSPat O], ConstRef O), Int)
-> TCMT IO (Maybe ([CSPat O], ConstRef O), Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe ([CSPat O], ConstRef O), Int)
 -> TCMT IO (Maybe ([CSPat O], ConstRef O), Int))
-> (Maybe ([CSPat O], ConstRef O), Int)
-> TCMT IO (Maybe ([CSPat O], ConstRef O), Int)
forall a b. (a -> b) -> a -> b
$ if [CSPat O] -> Bool
contains_constructor [CSPat O]
pats then
               (([CSPat O], ConstRef O) -> Maybe ([CSPat O], ConstRef O)
forall a. a -> Maybe a
Just ([CSPat O]
pats, ConstRef O
myrecdef), Int
defdfv)
              else
               (Maybe ([CSPat O], ConstRef O)
forall a. Maybe a
Nothing, Int
defdfv)
            Maybe (QName, Clause, Bool)
Nothing -> (Maybe ([CSPat O], ConstRef O), Int)
-> TCMT IO (Maybe ([CSPat O], ConstRef O), Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([CSPat O], ConstRef O)
forall a. Maybe a
Nothing, Int
0)
          let tc :: (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
 [MM (Exp O) (RefInfo O)])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mytype, [MM (Exp O) (RefInfo O)]
mylocalVars) Bool
isdep = Bool -> Ctx O -> CExp O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
tcSearchSC Bool
isdep ((MM (Exp O) (RefInfo O) -> (MId, CExp O))
-> [MM (Exp O) (RefInfo O)] -> Ctx O
forall a b. (a -> b) -> [a] -> [b]
map (\MM (Exp O) (RefInfo O)
x -> (MId
NoId, MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
x)) [MM (Exp O) (RefInfo O)]
mylocalVars) (MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
mytype) (Metavar (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O)
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m)
              initprop :: EE (MyPB O)
initprop =
                (EE (MyPB O)
 -> (Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))
 -> EE (MyPB O))
-> EE (MyPB O)
-> [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
-> EE (MyPB O)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\EE (MyPB O)
x (Bool
ineq, MM (Exp O) (RefInfo O)
e, MM (Exp O) (RefInfo O)
i) -> Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo O) -> EE (MyPB O))
-> Prop (RefInfo O) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ Maybe [Term (RefInfo O)]
-> EE (MyPB O) -> EE (MyPB O) -> Prop (RefInfo O)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And Maybe [Term (RefInfo O)]
forall a. Maybe a
Nothing EE (MyPB O)
x (Bool -> CExp O -> CExp O -> EE (MyPB O)
forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)
comp' Bool
ineq (MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
e) (MM (Exp O) (RefInfo O) -> CExp O
forall o. MExp o -> CExp o
closify MM (Exp O) (RefInfo O)
i)))
                 ((EE (MyPB O)
 -> (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])
 -> EE (MyPB O))
-> EE (MyPB O)
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
-> EE (MyPB O)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\EE (MyPB O)
x (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mt, [MM (Exp O) (RefInfo O)]
mlv, [MetaId]
_) ->
                   if Metavar (Exp O) (RefInfo O) -> Metavar (Exp O) (RefInfo O) -> Bool
forall a1 blk1 a2 bkl2. Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
hequalMetavar Metavar (Exp O) (RefInfo O)
m Metavar (Exp O) (RefInfo O)
mainm then
                    case Maybe ([CSPat O], ConstRef O)
recinfo of
                     Just ([CSPat O]
recpats, ConstRef O
recdef) ->
                      Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo O) -> EE (MyPB O))
-> Prop (RefInfo O) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ EE (MyPB O) -> EE (MyPB O) -> Prop (RefInfo O)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (([Int], Int, [Int])
-> ConstRef O -> MM (Exp O) (RefInfo O) -> EE (MyPB O)
forall o.
([Int], Int, [Int]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([CSPat O] -> ([Int], Int, [Int])
forall o. [CSPat o] -> ([Int], Int, [Int])
localTerminationEnv [CSPat O]
recpats) ConstRef O
recdef (Metavar (Exp O) (RefInfo O) -> MM (Exp O) (RefInfo O)
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m))
                                            ((Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
 [MM (Exp O) (RefInfo O)])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mt, [MM (Exp O) (RefInfo O)]
mlv) Bool
False)
                     Maybe ([CSPat O], ConstRef O)
Nothing -> Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo O) -> EE (MyPB O))
-> Prop (RefInfo O) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ Maybe [Term (RefInfo O)]
-> EE (MyPB O) -> EE (MyPB O) -> Prop (RefInfo O)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And Maybe [Term (RefInfo O)]
forall a. Maybe a
Nothing EE (MyPB O)
x ((Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
 [MM (Exp O) (RefInfo O)])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mt, [MM (Exp O) (RefInfo O)]
mlv) Bool
False)
                   else
                    Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo O) -> EE (MyPB O))
-> Prop (RefInfo O) -> EE (MyPB O)
forall a b. (a -> b) -> a -> b
$ Maybe [Term (RefInfo O)]
-> EE (MyPB O) -> EE (MyPB O) -> Prop (RefInfo O)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And Maybe [Term (RefInfo O)]
forall a. Maybe a
Nothing EE (MyPB O)
x ((Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
 [MM (Exp O) (RefInfo O)])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mt, [MM (Exp O) (RefInfo O)]
mlv) Bool
True)
                  )
                  (Prop (RefInfo O) -> EE (MyPB O)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo O)
forall blk. Prop blk
OK)
                  (Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons)
                 ) [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
eqcons
          Maybe Bool
res <- EE (MyPB O)
-> Maybe ([CSPat O], ConstRef O) -> Int -> TCMT IO (Maybe Bool)
exsearch EE (MyPB O)
initprop Maybe ([CSPat O], ConstRef O)
recinfo Int
defdfv
          [(MetaId, InteractionId)]
riis <- ((InteractionId, MetaId) -> (MetaId, InteractionId))
-> [(InteractionId, MetaId)] -> [(MetaId, InteractionId)]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, MetaId) -> (MetaId, InteractionId)
forall a b. (a, b) -> (b, a)
swap ([(InteractionId, MetaId)] -> [(MetaId, InteractionId)])
-> TCMT IO [(InteractionId, MetaId)]
-> TCMT IO [(MetaId, InteractionId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
          let timeoutString :: [Char]
timeoutString | Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Bool
res = [Char]
" after timeout (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TimeOut -> [Char]
forall a. Show a => a -> [Char]
show TimeOut
timeout [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"ms)"
                            | Bool
otherwise     = [Char]
""
          if Bool
listmode then do
            [[Term]]
rsols <- ([[Term]] -> [[Term]]) -> TCMT IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Term]] -> [[Term]]
forall a. [a] -> [a]
reverse (TCMT IO [[Term]] -> TCMT IO [[Term]])
-> TCMT IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> a -> b
$ IO [[Term]] -> TCMT IO [[Term]]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [[Term]] -> TCMT IO [[Term]])
-> IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> a -> b
$ IORef [[Term]] -> IO [[Term]]
forall a. IORef a -> IO a
readIORef IORef [[Term]]
sols
            if [[Term]] -> Bool
forall a. Null a => a -> Bool
null [[Term]]
rsols then do
              Int
nsol' <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
              [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffsols (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nsol') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
timeoutString
             else do
              [[(MetaId, Expr)]]
aexprss <- ([Term] -> TCM [(MetaId, Expr)])
-> [[Term]] -> TCMT IO [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [Term] -> TCM [(MetaId, Expr)]
getsols [[Term]]
rsols
              -- cexprss <- mapM (mapM (\(mi, e) -> lookupMeta mi >>= \mv -> withMetaInfo (getMetaInfo mv) $ abstractToConcrete_ e >>= \e' -> return (mi, e'))) aexprss
              [[(MetaId, Expr)]]
cexprss <- [[(MetaId, Expr)]]
-> ([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> TCMT IO [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[(MetaId, Expr)]]
aexprss (([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
 -> TCMT IO [[(MetaId, Expr)]])
-> ([(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> TCMT IO [[(MetaId, Expr)]]
forall a b. (a -> b) -> a -> b
$ do
                ((MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> [(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((MetaId, Expr) -> TCMT IO (MetaId, Expr))
 -> [(MetaId, Expr)] -> TCMT IO [(MetaId, Expr)])
-> ((MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> [(MetaId, Expr)]
-> TCMT IO [(MetaId, Expr)]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Expr
e) -> do
                  MetaVariable
mv <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
                  Closure Range -> TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr))
-> TCMT IO (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall a b. (a -> b) -> a -> b
$ do
                    Expr
e' <- Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Expr
e
                    (MetaId, Expr) -> TCMT IO (MetaId, Expr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
mi, Expr
e')
              let disp :: [(MetaId, Expr)] -> [Char]
disp [(MetaId
_, Expr
cexpr)] = Expr -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Expr
cexpr
                  disp [(MetaId, Expr)]
cexprs = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [(MetaId, Expr)] -> ((MetaId, Expr) -> [Char]) -> [[Char]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [(MetaId, Expr)]
cexprs (((MetaId, Expr) -> [Char]) -> [[Char]])
-> ((MetaId, Expr) -> [Char]) -> [[Char]]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Expr
cexpr) ->
                    [Char]
-> (InteractionId -> [Char]) -> Maybe InteractionId -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (MetaId -> [Char]
forall a. Show a => a -> [Char]
show MetaId
mi) InteractionId -> [Char]
forall a. Show a => a -> [Char]
show (MetaId -> [(MetaId, InteractionId)] -> Maybe InteractionId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
mi [(MetaId, InteractionId)]
riis)
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" := " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Expr
cexpr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
              Int
ticks <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ticks
              [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ [Char]
"Listing solution(s) " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
pick [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Term]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Term]]
rsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
timeoutString [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                        [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines (([(MetaId, Expr)] -> Int -> [Char])
-> [[(MetaId, Expr)]] -> [Int] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[(MetaId, Expr)]
x Int
y -> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Expr)] -> [Char]
disp [(MetaId, Expr)]
x) [[(MetaId, Expr)]]
cexprss [Int
pick..])
           else {- not listmode -}
            case Maybe Bool
res of
             Maybe Bool
Nothing -> do
              Int
nsol' <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
              [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffsols (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nsol') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
timeoutString
             Just Bool
depthreached -> do
              Int
ticks <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ticks
              [[Term]]
rsols <- IO [[Term]] -> TCMT IO [[Term]]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [[Term]] -> TCMT IO [[Term]])
-> IO [[Term]] -> TCMT IO [[Term]]
forall a b. (a -> b) -> a -> b
$ IORef [[Term]] -> IO [[Term]]
forall a. IORef a -> IO a
readIORef IORef [[Term]]
sols
              case [[Term]]
rsols of
                [] -> do
                  Int
nsol' <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
nsol
                  [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffsols (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nsol')
                [[Term]]
terms -> [[Term]] -> TCM AutoResult
loop [[Term]]
terms where
                  -- Andreas, 2015-05-17  Issue 1504
                  -- If giving a solution failed (e.g. ill-typed)
                  -- we could try the next one.
                  -- However, currently @terms@ is always a singleton list.
                  -- Thus, the following @loop@ is not doing something very
                  -- meaningful.
                  loop :: [[I.Term]] -> TCM AutoResult
                  loop :: [[Term]] -> TCM AutoResult
loop [] = AutoResult -> TCM AutoResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe [Char] -> AutoResult
AutoResult ([(InteractionId, [Char])] -> AutoProgress
Solutions []) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"")
                  loop ([Term]
term : [[Term]]
terms') = do
                    -- On exception, try next solution
                    (TCM AutoResult -> (TCErr -> TCM AutoResult) -> TCM AutoResult)
-> (TCErr -> TCM AutoResult) -> TCM AutoResult -> TCM AutoResult
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM AutoResult -> (TCErr -> TCM AutoResult) -> TCM AutoResult
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (\ TCErr
e -> do [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"auto" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Solution failed:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCM.<?> TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
TCM.prettyTCM TCErr
e
                                               [[Term]] -> TCM AutoResult
loop [[Term]]
terms') (TCM AutoResult -> TCM AutoResult)
-> TCM AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ do
                      [(MetaId, Expr)]
exprs <- [Term] -> TCM [(MetaId, Expr)]
getsols [Term]
term
                      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"auto" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying solution " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCM.<+> [(MetaId, Expr)] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [(MetaId, Expr)] -> m Doc
TCM.prettyTCM [(MetaId, Expr)]
exprs
                      [(Maybe (InteractionId, [Char]), Maybe [Char])]
giveress <- [(MetaId, Expr)]
-> ((MetaId, Expr)
    -> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char]))
-> TCMT IO [(Maybe (InteractionId, [Char]), Maybe [Char])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(MetaId, Expr)]
exprs (((MetaId, Expr)
  -> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char]))
 -> TCMT IO [(Maybe (InteractionId, [Char]), Maybe [Char])])
-> ((MetaId, Expr)
    -> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char]))
-> TCMT IO [(Maybe (InteractionId, [Char]), Maybe [Char])]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Expr
expr0) -> do
                        let expr :: Expr
expr = Expr -> Expr
forall a. KillRange a => KillRangeT a
killRange Expr
expr0
                        case MetaId -> [(MetaId, InteractionId)] -> Maybe InteractionId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
mi [(MetaId, InteractionId)]
riis of
                         Maybe InteractionId
Nothing ->
                          -- catchError
                           (UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCMT IO Term
giveExpr UseForce
WithoutForce Maybe InteractionId
forall a. Maybe a
Nothing MetaId
mi Expr
expr TCMT IO Term
-> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char])
-> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char])
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Maybe (InteractionId, [Char]), Maybe [Char])
-> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (InteractionId, [Char])
forall a. Maybe a
Nothing, Maybe [Char]
forall a. Maybe a
Nothing))
                           -- (const retry)
                           -- (\_ -> return (Nothing, Just ("Failed to give expr for side solution of " ++ show mi)))
                         Just InteractionId
ii' -> do Expr
ae <- UseForce -> InteractionId -> Maybe Range -> Expr -> TCMT IO Expr
give UseForce
WithoutForce InteractionId
ii' Maybe Range
forall a. Maybe a
Nothing Expr
expr
                                        MetaVariable
mv <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
                                        let scope :: ScopeInfo
scope = MetaVariable -> ScopeInfo
getMetaScope MetaVariable
mv
                                        Expr
ce <- ScopeInfo -> Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteScope ScopeInfo
scope Expr
ae
                                        let cmnt :: [Char]
cmnt = if InteractionId
ii' InteractionId -> InteractionId -> Bool
forall a. Eq a => a -> a -> Bool
== InteractionId
ii then Int -> [Char]
forall {a} {p}. IsString a => p -> a
agsyinfo Int
ticks else [Char]
""
                                        (Maybe (InteractionId, [Char]), Maybe [Char])
-> TCMT IO (Maybe (InteractionId, [Char]), Maybe [Char])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((InteractionId, [Char]) -> Maybe (InteractionId, [Char])
forall a. a -> Maybe a
Just (InteractionId
ii', Expr -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Expr
ce [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
cmnt), Maybe [Char]
forall a. Maybe a
Nothing)
                           -- Andreas, 2015-05-17, Issue 1504
                           -- When Agsy produces an ill-typed solution, return nothing.
                           -- TODO: try other solution.
                           -- `catchError` const retry -- (return (Nothing, Nothing))
                      let msg :: Maybe [Char]
msg = if [(MetaId, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(MetaId, Expr)]
exprs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
                                 Maybe [Char]
forall a. Maybe a
Nothing
                                else
                                 [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"Also gave solution(s) for hole(s)" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                         ((MetaId, Expr) -> [Char]) -> [(MetaId, Expr)] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(MetaId
mi', Expr
_) ->
                                          if MetaId
mi' MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
mi then [Char]
"" else ([Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ case MetaId -> [(MetaId, InteractionId)] -> Maybe InteractionId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
mi' [(MetaId, InteractionId)]
riis of {Maybe InteractionId
Nothing -> MetaId -> [Char]
forall a. Show a => a -> [Char]
show MetaId
mi'; Just InteractionId
ii -> InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii})
                                         ) [(MetaId, Expr)]
exprs
                      let msgs :: [[Char]]
msgs = [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe [Char]] -> [[Char]]) -> [Maybe [Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Maybe [Char]
msg Maybe [Char] -> [Maybe [Char]] -> [Maybe [Char]]
forall a. a -> [a] -> [a]
: ((Maybe (InteractionId, [Char]), Maybe [Char]) -> Maybe [Char])
-> [(Maybe (InteractionId, [Char]), Maybe [Char])]
-> [Maybe [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (InteractionId, [Char]), Maybe [Char]) -> Maybe [Char]
forall a b. (a, b) -> b
snd [(Maybe (InteractionId, [Char]), Maybe [Char])]
giveress
                          msg' :: Maybe [Char]
msg' = [[Char]] -> [Char]
unlines [[Char]]
msgs [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Bool
forall a. Null a => a -> Bool
null [[Char]]
msgs)
                      AutoResult -> TCM AutoResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe [Char] -> AutoResult
AutoResult ([(InteractionId, [Char])] -> AutoProgress
Solutions ([(InteractionId, [Char])] -> AutoProgress)
-> [(InteractionId, [Char])] -> AutoProgress
forall a b. (a -> b) -> a -> b
$ ((Maybe (InteractionId, [Char]), Maybe [Char])
 -> Maybe (InteractionId, [Char]))
-> [(Maybe (InteractionId, [Char]), Maybe [Char])]
-> [(InteractionId, [Char])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (InteractionId, [Char]), Maybe [Char])
-> Maybe (InteractionId, [Char])
forall a b. (a, b) -> a
fst [(Maybe (InteractionId, [Char]), Maybe [Char])]
giveress) Maybe [Char]
msg'

     Mode
MCaseSplit -> do
      case Maybe (QName, Clause, Bool)
thisdefinfo of
       Just (QName
def, Clause
clause, Bool
True) ->
        case Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
     [MM (Exp O) (RefInfo O)], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons of
         [(Metavar (Exp O) (RefInfo O)
m, MM (Exp O) (RefInfo O)
mytype, [MM (Exp O) (RefInfo O)]
mylocalVars, [MetaId]
_)] | [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))] -> Bool
forall a. Null a => a -> Bool
null [(Bool, MM (Exp O) (RefInfo O), MM (Exp O) (RefInfo O))]
eqcons -> do
          ([(Hiding, MId)]
ids, [CSPat O]
pats) <- Map QName (TMode, ConstRef O)
-> MetaId -> Clause -> TCM ([(Hiding, MId)], [CSPat O])
constructPats Map QName (TMode, ConstRef O)
cmap MetaId
mi Clause
clause
          let ctx :: [HI (MId, MM (Exp O) (RefInfo O))]
ctx = ((Hiding, MId)
 -> MM (Exp O) (RefInfo O) -> HI (MId, MM (Exp O) (RefInfo O)))
-> [(Hiding, MId)]
-> [MM (Exp O) (RefInfo O)]
-> [HI (MId, MM (Exp O) (RefInfo O))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Hiding
hid, MId
id) MM (Exp O) (RefInfo O)
t -> Hiding
-> (MId, MM (Exp O) (RefInfo O))
-> HI (MId, MM (Exp O) (RefInfo O))
forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MM (Exp O) (RefInfo O)
t)) [(Hiding, MId)]
ids [MM (Exp O) (RefInfo O)]
mylocalVars
          IORef Int
ticks <- IO (IORef Int) -> TCMT IO (IORef Int)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef Int) -> TCMT IO (IORef Int))
-> IO (IORef Int) -> TCMT IO (IORef Int)
forall a b. (a -> b) -> a -> b
$ Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
          let [MM (Exp O) (RefInfo O)
rectyp'] = [MM (Exp O) (RefInfo O)]
mymrectyp
          Int
defdfv <- MetaId -> QName -> TCMT IO Int
getdfv MetaId
mi QName
def
          ConstRef O
myrecdef <- IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCMT IO (ConstRef O))
-> IO (ConstRef O) -> TCMT IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef O -> IO (ConstRef O)) -> ConstDef O -> IO (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef {cdname :: [Char]
cdname = [Char]
"", cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName
def), cdtype :: MM (Exp O) (RefInfo O)
cdtype = MM (Exp O) (RefInfo O)
rectyp', cdcont :: DeclCont O
cdcont = DeclCont O
forall o. DeclCont o
Postulate, cddeffreevars :: Int
cddeffreevars = Int
defdfv}
          Maybe [Sol O]
sols <- IO (Maybe [Sol O]) -> TCMT IO (Maybe [Sol O])
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe [Sol O]) -> TCMT IO (Maybe [Sol O]))
-> IO (Maybe [Sol O]) -> TCMT IO (Maybe [Sol O])
forall a b. (a -> b) -> a -> b
$ Int -> IO [Sol O] -> IO (Maybe [Sol O])
forall a. Int -> IO a -> IO (Maybe a)
System.Timeout.timeout (TimeOut -> Int
getTimeOut TimeOut
timeout Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000) (
             let r :: Cost -> IO [Sol O]
r Cost
d = do
                  [Sol O]
sols <- IO [Sol O] -> IO [Sol O]
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Sol O] -> IO [Sol O]) -> IO [Sol O] -> IO [Sol O]
forall a b. (a -> b) -> a -> b
$ IORef Int
-> Int
-> [ConstRef O]
-> Maybe (EqReasoningConsts O)
-> Int
-> Cost
-> ConstRef O
-> [HI (MId, MM (Exp O) (RefInfo O))]
-> MM (Exp O) (RefInfo O)
-> [CSPat O]
-> IO [Sol O]
forall o.
IORef Int
-> Int
-> [ConstRef o]
-> Maybe (EqReasoningConsts o)
-> Int
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch IORef Int
ticks Int
forall a. HasCallStack => a
__IMPOSSIBLE__ [ConstRef O]
myhints Maybe (EqReasoningConsts O)
meqr Int
forall a. HasCallStack => a
__IMPOSSIBLE__ Cost
d ConstRef O
myrecdef [HI (MId, MM (Exp O) (RefInfo O))]
ctx MM (Exp O) (RefInfo O)
mytype [CSPat O]
pats
                  case [Sol O]
sols of
                   [] -> Cost -> IO [Sol O]
r (Cost
d Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
+ Cost
costIncrease)
                   (Sol O
_:[Sol O]
_) -> [Sol O] -> IO [Sol O]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Sol O]
sols
             in Cost -> IO [Sol O]
r Cost
0)
          case Maybe [Sol O]
sols of
           Just (Sol O
cls : [Sol O]
_) -> InteractionId -> TCM AutoResult -> TCM AutoResult
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM AutoResult -> TCM AutoResult)
-> TCM AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ do
            Either [Char] [Clause]
cls' <- IO (Either [Char] [Clause]) -> TCMT IO (Either [Char] [Clause])
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either [Char] [Clause]) -> TCMT IO (Either [Char] [Clause]))
-> IO (Either [Char] [Clause]) -> TCMT IO (Either [Char] [Clause])
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] IO [Clause] -> IO (Either [Char] [Clause])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ((([HI (MId, MM (Exp O) (RefInfo O))], [CSPat O],
  Maybe (MM (Exp O) (RefInfo O)))
 -> ExceptT [Char] IO Clause)
-> Sol O -> ExceptT [Char] IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([HI (MId, MM (Exp O) (RefInfo O))], [CSPat O],
 Maybe (MM (Exp O) (RefInfo O)))
-> ExceptT [Char] IO Clause
frommyClause Sol O
cls)
            case Either [Char] [Clause]
cls' of
             Left{} -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"No solution found"
             Right [Clause]
cls' -> do
              [Clause]
cls'' <- [Clause] -> (Clause -> TCMT IO Clause) -> TCMT IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Clause]
cls' ((Clause -> TCMT IO Clause) -> TCMT IO [Clause])
-> (Clause -> TCMT IO Clause) -> TCMT IO [Clause]
forall a b. (a -> b) -> a -> b
$ \ (I.Clause Range
_ Range
_ Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
reachable ExpandedEllipsis
ell Maybe ModuleName
wm) -> do
                ModuleName -> TCMT IO Clause -> TCMT IO Clause
forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
AN.qnameModule QName
def) (TCMT IO Clause -> TCMT IO Clause)
-> TCMT IO Clause -> TCMT IO Clause
forall a b. (a -> b) -> a -> b
$ do
                 -- Normalise the dot patterns
                 NAPs
ps <- Telescope -> TCMT IO NAPs -> TCMT IO NAPs
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO NAPs -> TCMT IO NAPs) -> TCMT IO NAPs -> TCMT IO NAPs
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO NAPs
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise NAPs
ps
                 Maybe Term
body <- Maybe Term -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Maybe Term
body
                 (Clause -> Clause) -> TCMT IO Clause -> TCMT IO Clause
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Clause
modifyAbstractClause (TCMT IO Clause -> TCMT IO Clause)
-> TCMT IO Clause -> TCMT IO Clause
forall a b. (a -> b) -> a -> b
$ TCMT IO Clause -> TCMT IO Clause
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Clause -> TCMT IO Clause)
-> TCMT IO Clause -> TCMT IO Clause
forall a b. (a -> b) -> a -> b
$ QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify (QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause)))
-> QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
AN.QNamed QName
def (Clause -> QNamed Clause) -> Clause -> QNamed Clause
forall a b. (a -> b) -> a -> b
$ Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
I.Clause Range
forall a. Range' a
noRange Range
forall a. Range' a
noRange Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
reachable ExpandedEllipsis
ell Maybe ModuleName
wm
              Telescope
moduleTel <- ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (QName -> ModuleName
AN.qnameModule QName
def)
              [Doc]
pcs <- InteractionId -> TCMT IO [Doc] -> TCMT IO [Doc]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO [Doc] -> TCMT IO [Doc]) -> TCMT IO [Doc] -> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ TCMT IO [Doc] -> TCMT IO [Doc]
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO [Doc] -> TCMT IO [Doc]) -> TCMT IO [Doc] -> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO [Doc] -> TCMT IO [Doc]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
moduleTel (TCMT IO [Doc] -> TCMT IO [Doc]) -> TCMT IO [Doc] -> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Doc) -> [Clause] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Clause -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cls''
              Int
ticks <- IO Int -> TCMT IO Int
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TCMT IO Int) -> IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ticks


              AutoResult -> TCM AutoResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe [Char] -> AutoResult
AutoResult ([[Char]] -> AutoProgress
FunClauses ([[Char]] -> AutoProgress) -> [[Char]] -> AutoProgress
forall a b. (a -> b) -> a -> b
$ (Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char]
insertAbsurdPattern ([Char] -> [Char]) -> (Doc -> [Char]) -> Doc -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> Doc -> [Char]
PP.renderStyle (Style
PP.style { mode :: Mode
PP.mode = Mode
PP.OneLineMode })) [Doc]
pcs) Maybe [Char]
forall a. Maybe a
Nothing

           Just [] -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"No solution found" -- case not possible at the moment because case split doesnt care about search exhaustiveness
           Maybe [Sol O]
Nothing -> [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ [Char]
"No solution found at time out (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TimeOut -> [Char]
forall a. Show a => a -> [Char]
show TimeOut
timeout [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s)"
         [(Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
  [MM (Exp O) (RefInfo O)], [MetaId])]
_ -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"Metavariable dependencies not allowed in case split mode"
       Maybe (QName, Clause, Bool)
_ -> [Char] -> TCM AutoResult
stopWithMsg [Char]
"Metavariable is not at top level of clause RHS"

     MRefine Bool
listmode -> do
      MetaVariable
mv <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
      let tt :: Type
tt = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
          minfo :: Closure Range
minfo = MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv
      Type
targettyp <- Closure Range -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
minfo (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ do
       [Arg Term]
vs <- TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
       Type
targettype <- Type
tt Type -> [Arg Term] -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> [Arg Term] -> m Type
`piApplyM` Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
vs) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) [Arg Term]
vs
       Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
targettype
      let tctx :: Int
tctx = [ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([ContextEntry] -> Int) -> [ContextEntry] -> Int
forall a b. (a -> b) -> a -> b
$ TCEnv -> [ContextEntry]
envContext (TCEnv -> [ContextEntry]) -> TCEnv -> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Range
minfo

      [([Char], (Int, Int))]
hits <- if [Char]
"-a" [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
hints then do
        TCState
st <- TCM TCState -> TCM TCState
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM TCState -> TCM TCState) -> TCM TCState -> TCM TCState
forall a b. (a -> b) -> a -> b
$ TCMT IO (TCM TCState) -> TCM TCState
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TCMT IO (TCM TCState) -> TCM TCState)
-> TCMT IO (TCM TCState) -> TCM TCState
forall a b. (a -> b) -> a -> b
$ (TCState -> TCEnv -> TCM TCState) -> TCMT IO (TCM TCState)
forall (m :: * -> *) a.
MonadIO m =>
(TCState -> TCEnv -> a) -> TCMT m a
pureTCM ((TCState -> TCEnv -> TCM TCState) -> TCMT IO (TCM TCState))
-> (TCState -> TCEnv -> TCM TCState) -> TCMT IO (TCM TCState)
forall a b. (a -> b) -> a -> b
$ \TCState
st TCEnv
_ -> TCState -> TCM TCState
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TCState
st
        let defs :: HashMap QName Definition
defs = TCState
stTCState
-> Lens' (HashMap QName Definition) TCState
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^.(Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stSignature((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
            idefs :: HashMap QName Definition
idefs = TCState
stTCState
-> Lens' (HashMap QName Definition) TCState
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^.(Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stImports((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
            alldefs :: [QName]
alldefs = HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
defs [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
idefs
        [Maybe ([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ([Char], (Int, Int))] -> [([Char], (Int, Int))])
-> TCMT IO [Maybe ([Char], (Int, Int))]
-> TCMT IO [([Char], (Int, Int))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (Maybe ([Char], (Int, Int))))
-> [QName] -> TCMT IO [Maybe ([Char], (Int, Int))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\QName
n ->
          case Maybe (QName, Clause, Bool)
thisdefinfo of
           Just (QName
def, Clause
_, Bool
_) | QName
def QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
n -> Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
           Maybe (QName, Clause, Bool)
_ -> do
            QName
cn <- Closure Range -> TCMT IO QName -> TCMT IO QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
minfo (TCMT IO QName -> TCMT IO QName) -> TCMT IO QName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ AbsToCon QName -> TCMT IO QName
forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon (AbsToCon QName -> TCMT IO QName)
-> AbsToCon QName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ QName -> AbsToCon (ConOfAbs QName)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
n
            if QName -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope QName
cn NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope then
              Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
            else QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
n TCMT IO (Either SigError Definition)
-> (Either SigError Definition
    -> TCMT IO (Maybe ([Char], (Int, Int))))
-> TCMT IO (Maybe ([Char], (Int, Int)))
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Left{} -> Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
              Right Definition
c -> do
                Type
ctyp <- Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
c
                Int
cdfv <- Closure Range -> TCMT IO Int -> TCMT IO Int
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
minfo (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
n
                Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Char], (Int, Int))
 -> TCMT IO (Maybe ([Char], (Int, Int))))
-> Maybe ([Char], (Int, Int))
-> TCMT IO (Maybe ([Char], (Int, Int)))
forall a b. (a -> b) -> a -> b
$ case Int -> Int -> Type -> Type -> Maybe (Int, Int)
matchType Int
cdfv Int
tctx Type
ctyp Type
targettyp of
                  Maybe (Int, Int)
Nothing -> Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
                  Just (Int, Int)
score -> ([Char], (Int, Int)) -> Maybe ([Char], (Int, Int))
forall a. a -> Maybe a
Just (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
cn, (Int, Int)
score)
         ) [QName]
alldefs
       else do
        let scopeinfo :: ScopeInfo
scopeinfo = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv)
            namespace :: NameSpace
namespace = ScopeInfo -> NameSpace
Scope.everythingInScope ScopeInfo
scopeinfo
            names :: NamesInScope
names = NameSpace -> NamesInScope
Scope.nsNames NameSpace
namespace
            qnames :: [(Name, QName)]
qnames = ((Name, [AbstractName]) -> (Name, QName))
-> [(Name, [AbstractName])] -> [(Name, QName)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
x, [AbstractName]
y) -> (Name
x, AbstractName -> QName
Scope.anameName (AbstractName -> QName) -> AbstractName -> QName
forall a b. (a -> b) -> a -> b
$ [AbstractName] -> AbstractName
forall a. HasCallStack => [a] -> a
head [AbstractName]
y)) ([(Name, [AbstractName])] -> [(Name, QName)])
-> [(Name, [AbstractName])] -> [(Name, QName)]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [(Name, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
names
            modnames :: [(Name, QName)]
modnames = case Maybe (QName, Clause, Bool)
thisdefinfo of
                        Just (QName
def, Clause
_, Bool
_) -> ((Name, QName) -> Bool) -> [(Name, QName)] -> [(Name, QName)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
_, QName
n) -> QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
def) [(Name, QName)]
qnames
                        Maybe (QName, Clause, Bool)
Nothing -> [(Name, QName)]
qnames
        [Maybe ([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ([Char], (Int, Int))] -> [([Char], (Int, Int))])
-> TCMT IO [Maybe ([Char], (Int, Int))]
-> TCMT IO [([Char], (Int, Int))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, QName) -> TCMT IO (Maybe ([Char], (Int, Int))))
-> [(Name, QName)] -> TCMT IO [Maybe ([Char], (Int, Int))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Name
cn, QName
n) -> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
n TCMT IO (Either SigError Definition)
-> (Either SigError Definition
    -> TCMT IO (Maybe ([Char], (Int, Int))))
-> TCMT IO (Maybe ([Char], (Int, Int)))
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Left{} -> Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
          Right Definition
c -> do
            Type
ctyp <- Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
c
            Int
cdfv <- Closure Range -> TCMT IO Int -> TCMT IO Int
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
minfo (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
n
            Maybe ([Char], (Int, Int)) -> TCMT IO (Maybe ([Char], (Int, Int)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Char], (Int, Int))
 -> TCMT IO (Maybe ([Char], (Int, Int))))
-> Maybe ([Char], (Int, Int))
-> TCMT IO (Maybe ([Char], (Int, Int)))
forall a b. (a -> b) -> a -> b
$ case Int -> Int -> Type -> Type -> Maybe (Int, Int)
matchType Int
cdfv Int
tctx Type
ctyp Type
targettyp of
              Maybe (Int, Int)
Nothing -> Maybe ([Char], (Int, Int))
forall a. Maybe a
Nothing
              Just (Int, Int)
score -> ([Char], (Int, Int)) -> Maybe ([Char], (Int, Int))
forall a. a -> Maybe a
Just (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
cn, (Int, Int)
score)
         ) [(Name, QName)]
modnames

      let sorthits :: [([Char], (Int, Int))]
sorthits = (([Char], (Int, Int)) -> ([Char], (Int, Int)) -> Ordering)
-> [([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (\([Char]
_, (Int
pa1, Int
pb1)) ([Char]
_, (Int
pa2, Int
pb2)) -> case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
pa2 Int
pa1 of {Ordering
EQ -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
pb1 Int
pb2; Ordering
o -> Ordering
o}) [([Char], (Int, Int))]
hits
      if Bool
listmode Bool -> Bool -> Bool
|| Int
pick Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (-Int
1) then
        let pick' :: Int
pick' = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 Int
pick
        in if Int
pick' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
sorthits then
             [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffcands (Int -> [Char]) -> Int -> [Char]
forall a b. (a -> b) -> a -> b
$ [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
sorthits
            else
             let showhits :: [([Char], (Int, Int))]
showhits = Int -> [([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a. Int -> [a] -> [a]
take Int
10 ([([Char], (Int, Int))] -> [([Char], (Int, Int))])
-> [([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a b. (a -> b) -> a -> b
$ Int -> [([Char], (Int, Int))] -> [([Char], (Int, Int))]
forall a. Int -> [a] -> [a]
drop Int
pick' [([Char], (Int, Int))]
sorthits
             in [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ [Char]
"Listing candidate(s) " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
pick' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
pick' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
showhits Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (found " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
sorthits) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in total)\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                           [[Char]] -> [Char]
unlines ((Int -> ([Char], (Int, Int)) -> [Char])
-> [Int] -> [([Char], (Int, Int))] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i ([Char]
cn, (Int, Int)
_) -> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
cn) [Int
pick'..Int
pick' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
showhits Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [([Char], (Int, Int))]
showhits)
       else
        if Int
pick Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
sorthits then
         [Char] -> TCM AutoResult
stopWithMsg ([Char] -> TCM AutoResult) -> [Char] -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
insuffcands (Int -> [Char]) -> Int -> [Char]
forall a b. (a -> b) -> a -> b
$ [([Char], (Int, Int))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([Char], (Int, Int))]
sorthits
        else
         AutoResult -> TCM AutoResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe [Char] -> AutoResult
AutoResult ([Char] -> AutoProgress
Refinement ([Char] -> AutoProgress) -> [Char] -> AutoProgress
forall a b. (a -> b) -> a -> b
$ ([Char], (Int, Int)) -> [Char]
forall a b. (a, b) -> a
fst (([Char], (Int, Int)) -> [Char]) -> ([Char], (Int, Int)) -> [Char]
forall a b. (a -> b) -> a -> b
$ [([Char], (Int, Int))]
sorthits [([Char], (Int, Int))] -> Int -> ([Char], (Int, Int))
forall a. HasCallStack => [a] -> Int -> a
!! Int
pick) Maybe [Char]
forall a. Maybe a
Nothing
  where
    agsyinfo :: p -> a
agsyinfo p
ticks = a
""

-- Get the functions and axioms defined in the same module as @def@.
autohints :: AutoHintMode -> I.MetaId -> Maybe AN.QName -> TCM [Hint]
autohints :: AutoHintMode -> MetaId -> Maybe QName -> TCM [Hint]
autohints AutoHintMode
AHMModule MetaId
mi (Just QName
def) = do
  ScopeInfo
scope <- Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo)
-> (MetaVariable -> Closure Range) -> MetaVariable -> ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> ScopeInfo)
-> TCM MetaVariable -> TCMT IO ScopeInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
  let names :: NamesInScope
names     = NameSpace -> NamesInScope
Scope.nsNames (NameSpace -> NamesInScope) -> NameSpace -> NamesInScope
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> NameSpace
Scope.everythingInScope ScopeInfo
scope
      qnames :: [QName]
qnames    = ([AbstractName] -> QName) -> [[AbstractName]] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (AbstractName -> QName
Scope.anameName (AbstractName -> QName)
-> ([AbstractName] -> AbstractName) -> [AbstractName] -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AbstractName] -> AbstractName
forall a. HasCallStack => [a] -> a
head) ([[AbstractName]] -> [QName]) -> [[AbstractName]] -> [QName]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [[AbstractName]]
forall k a. Map k a -> [a]
Map.elems NamesInScope
names
      modnames :: [QName]
modnames  = (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (\QName
n -> QName -> ModuleName
AN.qnameModule QName
n ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== QName -> ModuleName
AN.qnameModule QName
def Bool -> Bool -> Bool
&& QName
n QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
def) [QName]
qnames
  (QName -> Hint) -> [QName] -> [Hint]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> QName -> Hint
Hint Bool
False) ([QName] -> [Hint]) -> TCMT IO [QName] -> TCM [Hint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    ((QName -> TCMT IO Bool) -> [QName] -> TCMT IO [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
`filterM` [QName]
modnames) ((QName -> TCMT IO Bool) -> TCMT IO [QName])
-> (QName -> TCMT IO Bool) -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ \ QName
n -> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
n TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO Bool) -> TCMT IO Bool
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left{} -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Right Definition
c -> case Definition -> Defn
theDef Definition
c of
        Axiom{}    -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        AbstractDefn{} -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Function{} -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Defn
_          -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

autohints AutoHintMode
_ MetaId
_ Maybe QName
_ = [Hint] -> TCM [Hint]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []



-- | Names for the equality reasoning combinators
--   Empty if any of these names is not defined.

getEqCombinators :: InteractionId -> Range -> TCM [Hint]
getEqCombinators :: InteractionId -> Range -> TCM [Hint]
getEqCombinators InteractionId
ii Range
rng = do
  let eqCombinators :: [[Char]]
eqCombinators = [[Char]
"_≡_", [Char]
"begin_", [Char]
"_≡⟨_⟩_", [Char]
"_∎", [Char]
"sym", [Char]
"cong"]
  [Expr]
raw <- ([Char] -> TCMT IO Expr) -> [[Char]] -> TCMT IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (InteractionId -> Range -> [Char] -> TCMT IO Expr
parseExprIn InteractionId
ii Range
rng) [[Char]]
eqCombinators TCMT IO [Expr] -> (TCErr -> TCMT IO [Expr]) -> TCMT IO [Expr]
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCMT IO [Expr] -> TCErr -> TCMT IO [Expr]
forall a b. a -> b -> a
const ([Expr] -> TCMT IO [Expr]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
  [Hint] -> TCM [Hint]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Hint] -> TCM [Hint]) -> [Hint] -> TCM [Hint]
forall a b. (a -> b) -> a -> b
$ [Hint] -> Maybe [Hint] -> [Hint]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Hint] -> [Hint]) -> Maybe [Hint] -> [Hint]
forall a b. (a -> b) -> a -> b
$ (Expr -> Maybe Hint) -> [Expr] -> Maybe [Hint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> Maybe Hint
getHeadAsHint [Expr]
raw

-- | Templates for error messages

genericNotEnough :: String -> Int -> String
genericNotEnough :: [Char] -> Int -> [Char]
genericNotEnough [Char]
str Int
n = [[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ case Int
n of
  Int
0 -> [[Char]
"No", [Char]
str, [Char]
"found"]
  Int
1 -> [[Char]
"Only 1", [Char]
str, [Char]
"found"]
  Int
_ -> [[Char]
"Only", Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n, [Char]
str [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"s", [Char]
"found"]

insuffsols :: Int -> String
insuffsols :: Int -> [Char]
insuffsols  = [Char] -> Int -> [Char]
genericNotEnough [Char]
"solution"

insuffcands :: Int -> String
insuffcands :: Int -> [Char]
insuffcands = [Char] -> Int -> [Char]
genericNotEnough [Char]
"candidate"