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.Annotated as PP
import qualified Agda.TypeChecking.Pretty as TCM
import Agda.Syntax.Position
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcreteScope, abstractToConcrete_, runAbsToCon, toConcrete)
import Agda.Interaction.Base
import Agda.Interaction.BasicOps hiding (refine)
import Agda.TypeChecking.Reduce (normalise)
import Agda.Syntax.Common
import qualified Agda.Syntax.Scope.Base as Scope
import Agda.Syntax.Scope.Monad (withCurrentModule)
import qualified Agda.Syntax.Abstract.Name as AN
import qualified Agda.TypeChecking.Monad.Base as TCM
import Agda.TypeChecking.EtaContract (etaContract)

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

import Agda.Auto.CaseSplit

import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple


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

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

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

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

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

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

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

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

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

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

  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (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 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 <- 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 forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do AutoHintMode -> MetaId -> Maybe QName -> TCM [Hint]
autohints AutoHintMode
hintmode MetaId
mi forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b c. (a, b, c) -> a
fst3 Maybe (QName, Clause, Bool)
thisdefinfo

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

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

    let ([ConstRef O]
myhints, [ConstRef O]
c1to6) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstRef O]
myhints' forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Hint]
eqstuff) [ConstRef O]
myhints'
        meqr :: Maybe (EqReasoningConsts O)
meqr = forall a b. Null a => a -> b -> (a -> b) -> b
ifNull [Hint]
eqstuff forall a. Maybe a
Nothing 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  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall o.
ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> ConstRef o
-> EqReasoningConsts o
EqReasoningConsts ConstRef O
c1 ConstRef O
c2 ConstRef O
c3 ConstRef O
c4 ConstRef O
c5 ConstRef O
c6


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

    let (Metavar (Exp O) (RefInfo O)
mainm, MM (Exp O) (RefInfo O)
_, [MM (Exp O) (RefInfo O)]
_, [MetaId]
_) = Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef ([] :: [[I.Term]])
        IORef Int
nsol <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ Int
pick forall a. Num a => a -> a -> a
+ Int
numsols
        let hsol :: IO ()
hsol = do
             Int
nsol' <- forall a. IORef a -> IO a
readIORef IORef Int
nsol
             let cond :: Bool
cond = Int
nsol' forall a. Ord a => a -> a -> Bool
<= Int
numsols
             forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cond forall a b. (a -> b) -> a -> b
$ do
               Either [Char] [Term]
trms <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
                       forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Metavar (Exp O) (RefInfo O)
m , MM (Exp O) (RefInfo O)
_, [MM (Exp O) (RefInfo O)]
_, [MetaId]
_) -> forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m) :: MOT I.Term)
                       forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons
               case Either [Char] [Term]
trms of
                 Left{}     -> forall a. IORef a -> a -> IO ()
writeIORef IORef Int
nsol forall a b. (a -> b) -> a -> b
$! Int
nsol' forall a. Num a => a -> a -> a
+ Int
1
                 Right [Term]
trms -> forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[Term]]
sols ([Term]
trms forall a. a -> [a] -> [a]
:)
                 -- Right trms -> if listmode then modifyIORef sols (trms :)
                 --                           else writeIORef sols [trms]
        IORef Int
ticks <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 =
             forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Int -> IO a -> IO (Maybe a)
System.Timeout.timeout (TimeOut -> Int
getTimeOut TimeOut
timeout forall a. Num a => a -> a -> a
* Int
1000)
                    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) forall a. a -> [a] -> [a]
: [(ConstRef O, HintMode)]
x
                     env :: RefInfo O
env = RIEnv { rieHints :: [(ConstRef O, HintMode)]
rieHints             = [(ConstRef O, HintMode)] -> [(ConstRef O, HintMode)]
rechint forall a b. (a -> b) -> a -> b
$ 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 <- 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' <- forall a. IORef a -> IO a
readIORef IORef Int
nsol
                 if Int
nsol' forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Bool
depreached then Cost -> IO Bool
loop (Cost
d forall a. Num a => a -> a -> a
+ Cost
costIncrease) else 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip (forall k a. Map k a -> [k]
Map.keys Map
  MetaId
  (Metavar (Exp O) (RefInfo O), MM (Exp O) (RefInfo O),
   [MM (Exp O) (RefInfo O)], [MetaId])
tccons) [Term]
sol) forall a b. (a -> b) -> a -> b
$ \ (MetaId
mi, Term
e) -> do
               MetaVariable
mv   <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
               Term
e    <- forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
e
               Expr
expr <- Expr -> Expr
modifyAbstractExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
e
               forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
mi, Expr
expr)

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

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

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


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

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

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

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

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

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

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



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

getEqCombinators :: InteractionId -> Range -> TCM [Hint]
getEqCombinators :: InteractionId -> Range -> TCM [Hint]
getEqCombinators InteractionId
ii Range
rng = do
  let eqCombinators :: [[Char]]
eqCombinators = [[Char]
"_≡_", [Char]
"begin_", [Char]
"_≡⟨_⟩_", [Char]
"_∎", [Char]
"sym", [Char]
"cong"]
  [Expr]
raw <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId -> Range -> [Char] -> TCM Expr
parseExprIn InteractionId
ii Range
rng) [[Char]]
eqCombinators forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ 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 :: [Char] -> Int -> [Char]
genericNotEnough [Char]
str Int
n = [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$ case Int
n of
  Int
0 -> [[Char]
"No", [Char]
str, [Char]
"found"]
  Int
1 -> [[Char]
"Only 1", [Char]
str, [Char]
"found"]
  Int
_ -> [[Char]
"Only", forall a. Show a => a -> [Char]
show Int
n, [Char]
str forall a. [a] -> [a] -> [a]
++ [Char]
"s", [Char]
"found"]

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

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