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.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Tuple


insertAbsurdPattern :: String -> String
insertAbsurdPattern :: String -> String
insertAbsurdPattern [] = []
insertAbsurdPattern s :: String
s@(Char
_:String
_) | Int -> String -> String
forall a. Int -> [a] -> [a]
take (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
abspatvarname) String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
abspatvarname = String
"()" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
abspatvarname) String
s
insertAbsurdPattern (Char
c:String
s) = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
insertAbsurdPattern String
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 String
autoMessage  :: Maybe String
  }

stopWithMsg :: String -> TCM AutoResult
stopWithMsg :: String -> TCM AutoResult
stopWithMsg String
msg = AutoResult -> TCM AutoResult
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe String -> AutoResult
AutoResult ([(InteractionId, String)] -> AutoProgress
Solutions []) (String -> Maybe String
forall a. a -> Maybe a
Just String
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 :: InteractionId -> Range -> String -> tcm AutoResult
auto InteractionId
ii Range
rng String
argstr = TCM AutoResult -> tcm AutoResult
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 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 = String -> AutoOptions
parseArgs String
argstr
  let hints :: [String]
hints    = AutoOptions
autoOptions AutoOptions -> Lens' [String] AutoOptions -> [String]
forall o i. o -> Lens' i o -> i
^. Lens' [String] AutoOptions
aoHints
  let timeout :: TimeOut
timeout  = AutoOptions
autoOptions AutoOptions -> Lens' TimeOut AutoOptions -> TimeOut
forall o i. o -> Lens' i o -> i
^. Lens' TimeOut AutoOptions
aoTimeOut
  let pick :: Int
pick     = AutoOptions
autoOptions AutoOptions -> Lens' Int AutoOptions -> Int
forall o i. o -> Lens' i o -> i
^. Lens' Int AutoOptions
aoPick
  let mode :: Mode
mode     = AutoOptions
autoOptions AutoOptions -> Lens' Mode AutoOptions -> Mode
forall o i. o -> Lens' i o -> i
^. Lens' Mode AutoOptions
aoMode
  let hintmode :: AutoHintMode
hintmode = AutoOptions
autoOptions AutoOptions -> Lens' AutoHintMode AutoOptions -> AutoHintMode
forall o i. o -> Lens' i o -> i
^. Lens' AutoHintMode AutoOptions
aoHintMode
  [Expr]
ahints <- case Mode
mode of
    MRefine{} -> [Expr] -> TCMT IO [Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Mode
_         -> (String -> TCMT IO Expr) -> [String] -> TCMT IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId -> Range -> String -> TCMT IO Expr
parseExprIn InteractionId
ii Range
rng) [String]
hints
  let failHints :: TCM AutoResult
failHints = String -> TCM AutoResult
stopWithMsg String
"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)
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 (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', [MExp O]
mymrectyp, Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons, [(Bool, MExp O, MExp O)]
eqcons, Map QName (TMode, ConstRef O)
cmap) <- MetaId
-> [Hint]
-> [Type]
-> TCM
     ([ConstRef O], [MExp O],
      Map
        MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]),
      [(Bool, MExp O, MExp 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 (t :: * -> *) a. Foldable t => t a -> Int
length [ConstRef O]
myhints' Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Hint] -> 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 -> MExp O -> EE (MyPB O)
tcSearchSC Bool
isdep Ctx O
ctx CExp O
typ MExp 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 -> MExp O -> EE (MyPB O)
forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState EqReasoningConsts O
eqr MExp O
trm) EE (MyPB O)
a
          where a :: EE (MyPB O)
a = Bool -> Ctx O -> CExp O -> MExp 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 MExp O
trm

    let (Metavar (Exp O) (RefInfo O)
mainm, MExp O
_, [MExp O]
_, [MetaId]
_) = Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
-> MetaId
-> (Metavar (Exp O) (RefInfo O), MExp O, [MExp 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 (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 (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 String [Term]
trms <- ExceptT String IO [Term] -> IO (Either String [Term])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
                       (ExceptT String IO [Term] -> IO (Either String [Term]))
-> ExceptT String IO [Term] -> IO (Either String [Term])
forall a b. (a -> b) -> a -> b
$ ((Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
 -> ExceptT String IO Term)
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
-> ExceptT String IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Metavar (Exp O) (RefInfo O)
m , MExp O
_, [MExp O]
_, [MetaId]
_) -> MExp O -> ExceptT String IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Metavar (Exp O) (RefInfo O) -> MExp 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), MExp O, [MExp O], [MetaId])]
 -> ExceptT String IO [Term])
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
-> ExceptT String IO [Term]
forall a b. (a -> b) -> a -> b
$ Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons
               case Either String [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 (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 (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 :: forall o.
[(ConstRef o, HintMode)]
-> Int -> Maybe (EqReasoningConsts o) -> RefInfo o
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 (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), MExp O, [MExp O], [MetaId])
-> [MetaId]
forall k a. Map k a -> [k]
Map.keys Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp 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 -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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)
reify Term
e
               (MetaId, Expr) -> TCMT IO (MetaId, Expr)
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] TCM [(MetaId, Expr)]
loop MetaId
midx = do
                   let (Metavar (Exp O) (RefInfo O)
m, MExp O
_, [MExp O]
_, [MetaId]
deps) = Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
-> MetaId
-> (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
forall k a. Ord k => Map k a -> k -> a
Map.! MetaId
midx
                   [[(MetaId, Expr)]]
asolss <- (MetaId -> StateT [MetaId] TCM [(MetaId, Expr)])
-> [MetaId] -> StateT [MetaId] TCM [[(MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM MetaId -> StateT [MetaId] TCM [(MetaId, Expr)]
loop [MetaId]
deps
                   [MetaId]
dones  <- StateT [MetaId] TCM [MetaId]
forall s (m :: * -> *). MonadState s m => m s
get
                   [(MetaId, Expr)]
asols  <- if MetaId
midx MetaId -> [MetaId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaId]
dones then [(MetaId, Expr)] -> StateT [MetaId] TCM [(MetaId, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                     [MetaId] -> StateT [MetaId] TCM ()
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] TCM [(MetaId, Expr)]
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] TCM [(MetaId, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(MetaId, Expr)] -> StateT [MetaId] TCM [(MetaId, Expr)])
-> [(MetaId, Expr)] -> StateT [MetaId] TCM [(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] TCM [(MetaId, Expr)]
-> [MetaId] -> TCM ([(MetaId, Expr)], [MetaId])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (MetaId -> StateT [MetaId] TCM [(MetaId, Expr)]
loop MetaId
mi) []
             [(MetaId, Expr)] -> TCM [(MetaId, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(MetaId, Expr)]
asols

        if Bool
disprove then
          case [(Bool, MExp O, MExp O)]
eqcons of
           [] -> case Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons of
            (Metavar (Exp O) (RefInfo O)
m, MExp O
mytype, [MExp 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 (m :: * -> *) a. Monad m => a -> m a
return Int
0
                ConstRef O
ee <- IO (ConstRef O) -> TCMT IO (ConstRef O)
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 :: forall o. String -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: String
cdname = String
"T", cdorigin :: O
cdorigin = O
forall a. HasCallStack => a
__IMPOSSIBLE__, cdtype :: MExp O
cdtype = Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp 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 ([MExp O]
restargs, [MExp O]
modargs) = Int -> [MExp O] -> ([MExp O], [MExp O])
forall a. Int -> [a] -> ([a], [a])
splitAt ([MExp O] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MExp O]
mylocalVars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
defdfv) [MExp O]
mylocalVars
                    mytype' :: MExp O
mytype' = (MExp O -> MExp O -> MExp O) -> MExp O -> [MExp O] -> MExp O
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MExp O
x MExp O
y -> Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> Hiding -> Bool -> MExp O -> Abs (MExp 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 -> MExp O -> Bool
forall o. Int -> MExp o -> Bool
freeIn Int
0 MExp O
y) MExp O
y (MId -> MExp O -> Abs (MExp O)
forall a. MId -> a -> Abs a
Abs MId
NoId MExp O
x)) MExp O
mytype [MExp O]
restargs
                    htyp :: MExp O
htyp = ConstRef O -> MExp O -> MExp O
forall o. ConstRef o -> MExp o -> MExp o
negtype ConstRef O
ee MExp O
mytype'
                    sctx :: Ctx O
sctx = (String -> MId
Id String
"h", MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
htyp) (MId, CExp O) -> Ctx O -> Ctx O
forall a. a -> [a] -> [a]
: (MExp O -> (MId, CExp O)) -> [MExp O] -> Ctx O
forall a b. (a -> b) -> [a] -> [b]
map (\MExp O
x -> (MId
NoId, MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
x)) [MExp O]
modargs
                    ntt :: CExp O
ntt = MExp O -> CExp O
forall o. MExp o -> CExp o
closify (Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp 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 -> MExp O -> EE (MyPB O)
tcSearchSC Bool
False Ctx O
sctx CExp O
ntt (Metavar (Exp O) (RefInfo O) -> MExp 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 (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 (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 (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
                  String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
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)
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)
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 -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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 -> String
ss = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') (String -> String) -> (Expr -> String) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') (String -> String) -> (Expr -> String) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> String
forall a. Pretty a => a -> String
prettyShow
                      disp :: [(MetaId, Expr)] -> String
disp [(MetaId
_, Expr
cexpr)] = Expr -> String
ss Expr
cexpr
                      disp [(MetaId, Expr)]
cexprs = ((MetaId, Expr) -> String) -> [(MetaId, Expr)] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (MetaId
mi, Expr
cexpr) -> Expr -> String
ss Expr
cexpr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ") [(MetaId, Expr)]
cexprs
                  Int
ticks <- IO Int -> TCMT IO Int
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
                  String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    (String
"Listing disproof(s) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
pick String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Term]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Term]]
rsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                    [([(MetaId, Expr)], Int)]
-> (([(MetaId, Expr)], Int) -> String) -> [String]
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 -> String
forall a. Show a => a -> String
show Int
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(MetaId, Expr)] -> String
disp [(MetaId, Expr)]
x)
            [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
_ -> String -> TCM AutoResult
stopWithMsg String
"Metavariable dependencies not allowed in disprove mode"
           [(Bool, MExp O, MExp O)]
_ -> String -> TCM AutoResult
stopWithMsg String
"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 [MExp O
rectyp'] = [MExp 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 (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 :: forall o. String -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: String
cdname = String
"", cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName
def), cdtype :: MExp O
cdtype = MExp 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 (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 (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), MExp O, [MExp O])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MExp O
mytype, [MExp O]
mylocalVars) Bool
isdep = Bool -> Ctx O -> CExp O -> MExp O -> EE (MyPB O)
tcSearchSC Bool
isdep ((MExp O -> (MId, CExp O)) -> [MExp O] -> Ctx O
forall a b. (a -> b) -> [a] -> [b]
map (\MExp O
x -> (MId
NoId, MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
x)) [MExp O]
mylocalVars) (MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
mytype) (Metavar (Exp O) (RefInfo O) -> MExp 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, MExp O, MExp O) -> EE (MyPB O))
-> EE (MyPB O) -> [(Bool, MExp O, MExp O)] -> EE (MyPB O)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\EE (MyPB O)
x (Bool
ineq, MExp O
e, MExp 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 (MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
e) (MExp O -> CExp O
forall o. MExp o -> CExp o
closify MExp O
i)))
                 ((EE (MyPB O)
 -> (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
 -> EE (MyPB O))
-> EE (MyPB O)
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
-> EE (MyPB O)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\EE (MyPB O)
x (Metavar (Exp O) (RefInfo O)
m, MExp O
mt, [MExp 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 -> MExp 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) -> MExp O
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m))
                                            ((Metavar (Exp O) (RefInfo O), MExp O, [MExp O])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MExp O
mt, [MExp 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), MExp O, [MExp O])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MExp O
mt, [MExp 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), MExp O, [MExp O])
-> Bool -> EE (MyPB O)
tc (Metavar (Exp O) (RefInfo O)
m, MExp O
mt, [MExp 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), MExp O, [MExp O], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons)
                 ) [(Bool, MExp O, MExp 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 :: String
timeoutString | Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Bool
res = String
" after timeout (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TimeOut -> String
forall a. Show a => a -> String
show TimeOut
timeout String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"ms)"
                            | Bool
otherwise     = String
""
          if Bool
listmode then do
            [[Term]]
rsols <- ([[Term]] -> [[Term]]) -> TCMT IO [[Term]] -> TCMT IO [[Term]]
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 (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 (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
              String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
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') String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
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)
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)
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 -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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 (m :: * -> *) a. Monad m => a -> m a
return (MetaId
mi, Expr
e')
              let disp :: [(MetaId, Expr)] -> String
disp [(MetaId
_, Expr
cexpr)] = Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
cexpr
                  disp [(MetaId, Expr)]
cexprs = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [(MetaId, Expr)] -> ((MetaId, Expr) -> String) -> [String]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [(MetaId, Expr)]
cexprs (((MetaId, Expr) -> String) -> [String])
-> ((MetaId, Expr) -> String) -> [String]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Expr
cexpr) ->
                    String
-> (InteractionId -> String) -> Maybe InteractionId -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (MetaId -> String
forall a. Show a => a -> String
show MetaId
mi) InteractionId -> String
forall a. Show a => a -> String
show (MetaId -> [(MetaId, InteractionId)] -> Maybe InteractionId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
mi [(MetaId, InteractionId)]
riis)
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
cexpr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
              Int
ticks <- IO Int -> TCMT IO Int
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
              String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ String
"Listing solution(s) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
pick String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
pick Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Term]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Term]]
rsols Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
timeoutString String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (([(MetaId, Expr)] -> Int -> String)
-> [[(MetaId, Expr)]] -> [Int] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[(MetaId, Expr)]
x Int
y -> Int -> String
forall a. Show a => a -> String
show Int
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(MetaId, Expr)] -> String
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 (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
              String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
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') String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
timeoutString
             Just Bool
depthreached -> do
              Int
ticks <- IO Int -> TCMT IO Int
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 (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 (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
                  String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
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 (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe String -> AutoResult
AutoResult ([(InteractionId, String)] -> AutoProgress
Solutions []) (String -> Maybe String
forall a. a -> Maybe a
Just String
"")
                  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 e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (\ TCErr
e -> do String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"auto" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Solution failed:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCM.<?> TCErr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
                      String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"auto" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Trying solution " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCM.<+> [(MetaId, Expr)] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCM.prettyTCM [(MetaId, Expr)]
exprs
                      [(Maybe (InteractionId, String), Maybe String)]
giveress <- [(MetaId, Expr)]
-> ((MetaId, Expr)
    -> TCMT IO (Maybe (InteractionId, String), Maybe String))
-> TCMT IO [(Maybe (InteractionId, String), Maybe String)]
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, String), Maybe String))
 -> TCMT IO [(Maybe (InteractionId, String), Maybe String)])
-> ((MetaId, Expr)
    -> TCMT IO (Maybe (InteractionId, String), Maybe String))
-> TCMT IO [(Maybe (InteractionId, String), Maybe String)]
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, String), Maybe String)
-> TCMT IO (Maybe (InteractionId, String), Maybe String)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Maybe (InteractionId, String), Maybe String)
-> TCMT IO (Maybe (InteractionId, String), Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (InteractionId, String)
forall a. Maybe a
Nothing, Maybe String
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 -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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 :: String
cmnt = if InteractionId
ii' InteractionId -> InteractionId -> Bool
forall a. Eq a => a -> a -> Bool
== InteractionId
ii then Int -> String
forall p p. IsString p => p -> p
agsyinfo Int
ticks else String
""
                                        (Maybe (InteractionId, String), Maybe String)
-> TCMT IO (Maybe (InteractionId, String), Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return ((InteractionId, String) -> Maybe (InteractionId, String)
forall a. a -> Maybe a
Just (InteractionId
ii', Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
ce String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmnt), Maybe String
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 String
msg = if [(MetaId, Expr)] -> 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 String
forall a. Maybe a
Nothing
                                else
                                 String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Also gave solution(s) for hole(s)" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                         ((MetaId, Expr) -> String) -> [(MetaId, Expr)] -> String
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 String
"" else (String
" " String -> String -> String
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 -> String
forall a. Show a => a -> String
show MetaId
mi'; Just InteractionId
ii -> InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii})
                                         ) [(MetaId, Expr)]
exprs
                      let msgs :: [String]
msgs = [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> [String]) -> [Maybe String] -> [String]
forall a b. (a -> b) -> a -> b
$ Maybe String
msg Maybe String -> [Maybe String] -> [Maybe String]
forall a. a -> [a] -> [a]
: ((Maybe (InteractionId, String), Maybe String) -> Maybe String)
-> [(Maybe (InteractionId, String), Maybe String)]
-> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (InteractionId, String), Maybe String) -> Maybe String
forall a b. (a, b) -> b
snd [(Maybe (InteractionId, String), Maybe String)]
giveress
                          msg' :: Maybe String
msg' = [String] -> String
unlines [String]
msgs String -> Maybe () -> Maybe String
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
$ [String] -> Bool
forall a. Null a => a -> Bool
null [String]
msgs)
                      AutoResult -> TCM AutoResult
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe String -> AutoResult
AutoResult ([(InteractionId, String)] -> AutoProgress
Solutions ([(InteractionId, String)] -> AutoProgress)
-> [(InteractionId, String)] -> AutoProgress
forall a b. (a -> b) -> a -> b
$ ((Maybe (InteractionId, String), Maybe String)
 -> Maybe (InteractionId, String))
-> [(Maybe (InteractionId, String), Maybe String)]
-> [(InteractionId, String)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (InteractionId, String), Maybe String)
-> Maybe (InteractionId, String)
forall a b. (a, b) -> a
fst [(Maybe (InteractionId, String), Maybe String)]
giveress) Maybe String
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), MExp O, [MExp O], [MetaId])
-> [(Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])]
forall k a. Map k a -> [a]
Map.elems Map
  MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
tccons of
         [(Metavar (Exp O) (RefInfo O)
m, MExp O
mytype, [MExp O]
mylocalVars, [MetaId]
_)] | [(Bool, MExp O, MExp O)] -> Bool
forall a. Null a => a -> Bool
null [(Bool, MExp O, MExp 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, MExp O)]
ctx = ((Hiding, MId) -> MExp O -> HI (MId, MExp O))
-> [(Hiding, MId)] -> [MExp O] -> [HI (MId, MExp O)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Hiding
hid, MId
id) MExp O
t -> Hiding -> (MId, MExp O) -> HI (MId, MExp O)
forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp O
t)) [(Hiding, MId)]
ids [MExp O]
mylocalVars
          IORef Int
ticks <- IO (IORef Int) -> TCMT IO (IORef Int)
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 [MExp O
rectyp'] = [MExp 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 (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 :: forall o. String -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: String
cdname = String
"", cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName
def), cdtype :: MExp O
cdtype = MExp 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 (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 (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, MExp O)]
-> MExp 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, MExp O)]
ctx MExp 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 (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.
(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 String [Clause]
cls' <- IO (Either String [Clause]) -> TCMT IO (Either String [Clause])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String [Clause]) -> TCMT IO (Either String [Clause]))
-> IO (Either String [Clause]) -> TCMT IO (Either String [Clause])
forall a b. (a -> b) -> a -> b
$ ExceptT String IO [Clause] -> IO (Either String [Clause])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ((([HI (MId, MExp O)], [CSPat O], Maybe (MExp O))
 -> ExceptT String IO Clause)
-> Sol O -> ExceptT String IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([HI (MId, MExp O)], [CSPat O], Maybe (MExp O))
-> ExceptT String IO Clause
frommyClause Sol O
cls)
            case Either String [Clause]
cls' of
             Left{} -> String -> TCM AutoResult
stopWithMsg String
"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) -> 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
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 (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)
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
-> 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
              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.
(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
addContext Telescope
moduleTel (TCMT IO [Doc] -> TCMT IO [Doc]) -> TCMT IO [Doc] -> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> TCM 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 (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 (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe String -> AutoResult
AutoResult ([String] -> AutoProgress
FunClauses ([String] -> AutoProgress) -> [String] -> AutoProgress
forall a b. (a -> b) -> a -> b
$ (Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
insertAbsurdPattern (String -> String) -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> Doc -> String
PP.renderStyle (Style
PP.style { mode :: Mode
PP.mode = Mode
PP.OneLineMode })) [Doc]
pcs) Maybe String
forall a. Maybe a
Nothing

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

     MRefine Bool
listmode -> do
      MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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
       Args
vs <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
       Type
targettype <- Type
tt Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) Args
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 (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

      [(String, (Int, Int))]
hits <- if String
"-a" String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
hints then do
        TCState
st <- TCM TCState -> TCM TCState
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 (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 (String, (Int, Int))] -> [(String, (Int, Int))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (String, (Int, Int))] -> [(String, (Int, Int))])
-> TCMT IO [Maybe (String, (Int, Int))]
-> TCMT IO [(String, (Int, Int))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (Maybe (String, (Int, Int))))
-> [QName] -> TCMT IO [Maybe (String, (Int, Int))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 (String, (Int, Int)) -> TCMT IO (Maybe (String, (Int, Int)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, (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 (String, (Int, Int)) -> TCMT IO (Maybe (String, (Int, Int)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, (Int, Int))
forall a. Maybe a
Nothing
            else do
              Definition
c <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
n
              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 (String, (Int, Int)) -> TCMT IO (Maybe (String, (Int, Int)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, (Int, Int))
 -> TCMT IO (Maybe (String, (Int, Int))))
-> Maybe (String, (Int, Int))
-> TCMT IO (Maybe (String, (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 (String, (Int, Int))
forall a. Maybe a
Nothing
               Just (Int, Int)
score -> (String, (Int, Int)) -> Maybe (String, (Int, Int))
forall a. a -> Maybe a
Just (QName -> String
forall a. Pretty a => a -> String
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. [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 (String, (Int, Int))] -> [(String, (Int, Int))]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (String, (Int, Int))] -> [(String, (Int, Int))])
-> TCMT IO [Maybe (String, (Int, Int))]
-> TCMT IO [(String, (Int, Int))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, QName) -> TCMT IO (Maybe (String, (Int, Int))))
-> [(Name, QName)] -> TCMT IO [Maybe (String, (Int, Int))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Name
cn, QName
n) -> do
          Definition
c <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
n
          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 (String, (Int, Int)) -> TCMT IO (Maybe (String, (Int, Int)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, (Int, Int))
 -> TCMT IO (Maybe (String, (Int, Int))))
-> Maybe (String, (Int, Int))
-> TCMT IO (Maybe (String, (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 (String, (Int, Int))
forall a. Maybe a
Nothing
           Just (Int, Int)
score -> (String, (Int, Int)) -> Maybe (String, (Int, Int))
forall a. a -> Maybe a
Just (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
cn, (Int, Int)
score)
         ) [(Name, QName)]
modnames

      let sorthits :: [(String, (Int, Int))]
sorthits = ((String, (Int, Int)) -> (String, (Int, Int)) -> Ordering)
-> [(String, (Int, Int))] -> [(String, (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (\(String
_, (Int
pa1, Int
pb1)) (String
_, (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}) [(String, (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
>= [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
sorthits then
             String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
insuffcands (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
sorthits
            else
             let showhits :: [(String, (Int, Int))]
showhits = Int -> [(String, (Int, Int))] -> [(String, (Int, Int))]
forall a. Int -> [a] -> [a]
take Int
10 ([(String, (Int, Int))] -> [(String, (Int, Int))])
-> [(String, (Int, Int))] -> [(String, (Int, Int))]
forall a b. (a -> b) -> a -> b
$ Int -> [(String, (Int, Int))] -> [(String, (Int, Int))]
forall a. Int -> [a] -> [a]
drop Int
pick' [(String, (Int, Int))]
sorthits
             in String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ String
"Listing candidate(s) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
pick' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
pick' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
showhits Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
sorthits) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in total)\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                           [String] -> String
unlines ((Int -> (String, (Int, Int)) -> String)
-> [Int] -> [(String, (Int, Int))] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i (String
cn, (Int, Int)
_) -> Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cn) [Int
pick'..Int
pick' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
showhits Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [(String, (Int, Int))]
showhits)
       else
        if Int
pick Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
sorthits then
         String -> TCM AutoResult
stopWithMsg (String -> TCM AutoResult) -> String -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ Int -> String
insuffcands (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [(String, (Int, Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, Int))]
sorthits
        else
         AutoResult -> TCM AutoResult
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoResult -> TCM AutoResult) -> AutoResult -> TCM AutoResult
forall a b. (a -> b) -> a -> b
$ AutoProgress -> Maybe String -> AutoResult
AutoResult (String -> AutoProgress
Refinement (String -> AutoProgress) -> String -> AutoProgress
forall a b. (a -> b) -> a -> b
$ (String, (Int, Int)) -> String
forall a b. (a, b) -> a
fst ((String, (Int, Int)) -> String) -> (String, (Int, Int)) -> String
forall a b. (a -> b) -> a -> b
$ [(String, (Int, Int))]
sorthits [(String, (Int, Int))] -> Int -> (String, (Int, Int))
forall a. [a] -> Int -> a
!! Int
pick) Maybe String
forall a. Maybe a
Nothing
  where
    agsyinfo :: p -> p
agsyinfo p
ticks = p
""

-- 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)
-> TCMT IO MetaVariable -> TCMT IO ScopeInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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. [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 -> do
      Definition
c <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
n
      case Definition -> Defn
theDef Definition
c of
        Axiom{}    -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        AbstractDefn{} -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Function{} -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Defn
_          -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

autohints AutoHintMode
_ MetaId
_ Maybe QName
_ = [Hint] -> TCM [Hint]
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 :: [String]
eqCombinators = [String
"_≡_", String
"begin_", String
"_≡⟨_⟩_", String
"_∎", String
"sym", String
"cong"]
  [Expr]
raw <- (String -> TCMT IO Expr) -> [String] -> TCMT IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId -> Range -> String -> TCMT IO Expr
parseExprIn InteractionId
ii Range
rng) [String]
eqCombinators TCMT IO [Expr] -> (TCErr -> TCMT IO [Expr]) -> TCMT IO [Expr]
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 (f :: * -> *) a. Applicative f => a -> f a
pure [])
  [Hint] -> TCM [Hint]
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)
mapM Expr -> Maybe Hint
getHeadAsHint [Expr]
raw

-- | Templates for error messages

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

insuffsols :: Int -> String
insuffsols :: Int -> String
insuffsols  = String -> Int -> String
genericNotEnough String
"solution"

insuffcands :: Int -> String
insuffcands :: Int -> String
insuffcands = String -> Int -> String
genericNotEnough String
"candidate"