-- | Imperfect discrimination trees for indexing data by internal
-- syntax.
module Agda.TypeChecking.DiscrimTree
  ( insertDT
  , lookupDT, lookupUnifyDT, QueryResult(..)
  , deleteFromDT
  )
  where

import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Foldable
import Data.Maybe

import Control.Monad.Trans.Maybe
import Control.Monad.Trans
import Control.Monad

import Agda.Syntax.Internal
import Agda.Syntax.Common

import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free

import Agda.TypeChecking.DiscrimTree.Types

import qualified Agda.Utils.ProfileOptions as Profile

import Agda.Utils.Impossible
import Agda.Utils.Trie (Trie(..))

-- | Dummy term to use as a stand-in for expanded eta-records while
-- building instance trees.
etaExpansionDummy :: Term
etaExpansionDummy :: Term
etaExpansionDummy = String -> Elims -> Term
Dummy String
"eta-record argument in instance head" []

-- | Extract a list of arguments from the list of eliminations; If
-- called while *adding* an instance, additionally replace any arguments
-- that might belong to an eta-record by dummy terms.
termKeyElims
  :: Bool      -- ^ Are we adding or looking up an instance?
  -> TCM Type  -- ^ Continuation to compute the type of the arguments in the spine.
  -> [Arg Term] -- ^ The spine.
  -> TCM (Int, [Term])

-- Since the case tree was generated with wildcards everywhere an eta
-- record appeared, if we're *looking up* an instance, we don't have to
-- do the censorship again.
termKeyElims :: Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
False TCM Type
_ [Arg Term]
es = (Int, [Term]) -> TCM (Int, [Term])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
es, (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
es)

termKeyElims Bool
precise TCM Type
ty [Arg Term]
args = do
  let
    go :: Type -> [Arg Term] -> m (a, [Term])
go Type
ty (Arg ArgInfo
_ Term
a:[Arg Term]
as) = ((Dom Type -> Abs Type -> m (a, [Term]))
 -> (Blocked Type -> m (a, [Term])) -> m (a, [Term]))
-> (Blocked Type -> m (a, [Term]))
-> (Dom Type -> Abs Type -> m (a, [Term]))
-> m (a, [Term])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type
-> (Dom Type -> Abs Type -> m (a, [Term]))
-> (Blocked Type -> m (a, [Term]))
-> m (a, [Term])
forall (m :: * -> *) a.
MonadReduce m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiTypeB Type
ty) (Blocker -> m (a, [Term])
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> m (a, [Term]))
-> (Blocked Type -> Blocker) -> Blocked Type -> m (a, [Term])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked Type -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker) \Dom Type
dom Abs Type
ty' -> do

      -- Is this argument an eta record type --- or a blocked value? In
      -- either case, we replace this position by a dummy, to make sure
      -- that eta-equality is respected.
      Bool
maybeEta <- Type
-> (Blocker -> Type -> m Bool)
-> (NotBlocked -> Type -> m Bool)
-> m Bool
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) (\Blocker
_ Type
_ -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) \NotBlocked
_ Type
tm ->
        Maybe (QName, [Arg Term]) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, [Arg Term]) -> Bool)
-> m (Maybe (QName, [Arg Term])) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Maybe (QName, [Arg Term]))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, [Arg Term]))
isEtaRecordType Type
tm

      let
        here :: Term
here
          | Bool
maybeEta  = Term
etaExpansionDummy
          | Bool
otherwise = Term
a

      (a
k, [Term]
there) <- Dom Type -> m (a, [Term]) -> m (a, [Term])
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
dom (Type -> [Arg Term] -> m (a, [Term])
go (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
ty') [Arg Term]
as)
      (a, [Term]) -> m (a, [Term])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
k a -> a -> a
forall a. Num a => a -> a -> a
+ a
1, Term
hereTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
there)

    go Type
_ [] = (a, [Term]) -> m (a, [Term])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
0, [])

  TCM Type
ty TCM Type -> (Type -> TCM (Int, [Term])) -> TCM (Int, [Term])
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Type -> [Arg Term] -> TCM (Int, [Term]))
-> [Arg Term] -> Type -> TCM (Int, [Term])
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> [Arg Term] -> TCM (Int, [Term])
forall {m :: * -> *} {a}.
(MonadReduce m, MonadBlock m, HasConstInfo m, MonadAddContext m,
 Num a) =>
Type -> [Arg Term] -> m (a, [Term])
go [Arg Term]
args

-- | Ticky profiling for the reason behind "inexactness" in instance
-- search. If at some point while narrowing the set of candidates we had
-- to go through all the possibilities, one of these counters is
-- incremented.
tickExplore :: Term -> TCM ()
tickExplore :: Term -> TCM ()
tickExplore Term
tm = ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Instances do
  String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"flex term blocking instance"

  case Term
tm of
    Def{}      -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Def"
    Var{}      -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Var"
    Lam ArgInfo
_ Abs Term
v
      -- These two are a hunch: just like FunK, it might be worth
      -- optimising for the case where a lambda is constant (which is
      -- easy to handle, by just pretending the term is something else).
      -- These would come up in e.g. Dec (PathP (λ i → Nat) x y)
      | NoAbs{} <- Abs Term
v -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: constant function"
      | Abs String
_ Term
b <- Abs Term
v, Bool -> Bool
not (Int
0 Int -> Term -> Bool
forall a. Free a => Int -> a -> Bool
`freeIn` Term
b) -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: constant function"

      | Bool
otherwise    -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Lam"
    Lit{}      -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Lit"
    Sort{}     -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Sort"
    Level{}    -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Level"
    MetaV{}    -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: Meta"
    DontCare{} -> String -> TCM ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"explore: DontCare"
    Term
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Split a term into a 'Key' and some arguments. The 'Key' indicates
-- whether or not the 'Term' is in head-normal form, and provides a
-- quick way to match on the head.
--
-- The 'Int' argument indicates how free a variable must be to be
-- considered a 'LocalK'.
--
-- Presently, non-head-normal terms end up with an empty argument list.
splitTermKey :: Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey :: Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey Bool
precise Int
local Term
tm = (Blocker -> TCM (Key, [Term], Blocker))
-> TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (\Blocker
b -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
FlexK, [], Blocker
b)) do
  (NotBlocked
b, Term
tm') <- Term
-> (Blocker -> Term -> TCMT IO (NotBlocked, Term))
-> (NotBlocked -> Term -> TCMT IO (NotBlocked, Term))
-> TCMT IO (NotBlocked, Term)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
tm (\Blocker
b Term
_ -> Blocker -> TCMT IO (NotBlocked, Term)
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
b) (\NotBlocked
b -> (Term -> (NotBlocked, Term))
-> TCMT IO Term -> TCMT IO (NotBlocked, Term)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NotBlocked
b,) (TCMT IO Term -> TCMT IO (NotBlocked, Term))
-> (Term -> TCMT IO Term) -> Term -> TCMT IO (NotBlocked, Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm)

  case Term
tm' of
    -- Adding a 'Def' to the key poses a few problems when opacity (or
    -- abstractness) are involved (see issue #7304). Suppose we have an
    -- opaque binding `X = Y`, and an opaque instance `C X`. The problem
    -- is as follows:
    --
    --   if we unfold X → Y when adding the instance, then it will not
    --   get recorded as an instance for C X, only C Y; this is 7304b.
    --
    --   if we *don't* unfold X → Y, then it only gets added as an
    --   instance of C X; in opaque blocks where X is allowed to unfold,
    --   we *won't* find it, because we're looking for C Y.
    --
    -- The solution is to throw our hands up and say "not our problem".
    -- The discrimination tree is allowed to return more results than
    -- strictly necessary, after all, so the solution is to add an
    -- instance for *neither* of C X or C Y, but instead, to treat all
    -- 'Def's headed by 'AbstractDefn' as though they were flexible
    -- (think "as though they were metas").
    Def QName
q Elims
as | NotBlocked
ReallyNotBlocked <- NotBlocked
b, ([Arg Term]
as, Elims
_) <- Elims -> ([Arg Term], Elims)
forall a. [Elim' a] -> ([Arg a], [Elim' a])
splitApplyElims Elims
as -> do
      Definition
info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      case Definition -> Defn
theDef Definition
info of
        AbstractDefn{} -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
FlexK, [], Blocker
neverUnblock)
        Defn
_ -> do
          (Int
arity, [Term]
as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
precise (Type -> TCM Type
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Definition -> Type
defType Definition
info)) [Arg Term]
as
          (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Int -> Key
RigidK QName
q Int
arity, [Term]
as, Blocker
neverUnblock)

    -- When adding a quantified instance, we record how many 'Pi's we went
    -- under, and only variables beyond those are considered LocalK. The
    -- others are considered FlexK since they're "pattern variables" of
    -- the instance.
    Var Int
i Elims
as | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
local, Just [Arg Term]
as <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as -> do
      let ty :: TCM Type
ty = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> TCMT IO (Dom Type) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
      (Int
arity, [Term]
as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
precise TCM Type
ty [Arg Term]
as
      (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Key
LocalK (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
local) Int
arity, [Term]
as, Blocker
neverUnblock)

    -- When looking up an instance, it's better to treat variables and
    -- neutral definitions as rigid things regardless of their spines
    -- (especially if they have projections), than it is to try to
    -- represent them accurately.
    Def QName
q Elims
as | Bool -> Bool
not Bool
precise             -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Int -> Key
RigidK QName
q Int
0, [], Blocker
neverUnblock)
    Var Int
i Elims
as | Bool -> Bool
not Bool
precise, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
local -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Key
LocalK (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
local) Int
0, [], Blocker
neverUnblock)

    Con ConHead
ch ConInfo
_ Elims
as | Just [Arg Term]
as <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as -> do
      let
        q :: QName
q  = ConHead -> QName
conName ConHead
ch
        ty :: TCM Type
ty = Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM 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
q
      (Int
arity, [Term]
as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
precise TCM Type
ty [Arg Term]
as
      (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Int -> Key
RigidK QName
q Int
arity, [Term]
as, Blocker
neverUnblock)

    Pi Dom Type
dom Abs Type
ret ->
      let
        -- If we're looking at a non-dependent function type, then we
        -- might as well represent the codomain accurately; Otherwise,
        -- turn the codomain into a wildcard.
        --
        -- The use of a dummy term *shouldn't* leak to the user, because
        -- when we call splitTermKey again, it'll be handled by the last
        -- case, and become a FlexK.
        ret' :: Term
ret' = case Abs Term -> Maybe Term
forall a. (Free a, Subst a) => Abs a -> Maybe a
isNoAbs (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Abs Type -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
ret) of
          Just Term
b  -> Term
b
          Maybe Term
Nothing -> Term
HasCallStack => Term
__DUMMY_TERM__
      in (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
PiK, [Type -> Term
forall t a. Type'' t a -> a
unEl (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom), Term
ret'], Blocker
neverUnblock)

    Lam ArgInfo
_ Abs Term
body
      -- Constant lambdas come up quite a bit, particularly (in cubical
      -- mode) as the domain of a PathP. Having this trick improves the
      -- indexing of 'Dec' instances in the 1Lab significantly.
      | Just Term
b <- Abs Term -> Maybe Term
forall a. (Free a, Subst a) => Abs a -> Maybe a
isNoAbs Abs Term
body -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
ConstK, [Term
b], Blocker
neverUnblock)

    -- Probably not a good idea for accurate indexing if universes
    -- overlap literally everything else.
    Sort Sort
_ -> (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
SortK, [], Blocker
neverUnblock)

    Term
_ -> do
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.split" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
tm
      (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Key
FlexK, [], Blocker
neverUnblock)

termPath :: Bool -> Int -> [Key] -> [Term] -> TCM [Key]
termPath :: Bool -> Int -> [Key] -> [Term] -> TCM [Key]
termPath Bool
toplevel Int
local [Key]
acc []        = [Key] -> TCM [Key]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Key] -> TCM [Key]) -> [Key] -> TCM [Key]
forall a b. (a -> b) -> a -> b
$! [Key] -> [Key]
forall a. [a] -> [a]
reverse [Key]
acc
termPath Bool
toplevel Int
local [Key]
acc (Term
tm:[Term]
todo) = do

  -- We still want to ignore abstractness at the very top-level of
  -- instance heads, for issue #6941, to ensure that each instance ends
  -- up in the right 'class'. See the comment in `splitTermKey` about
  -- abstract definitions.
  (Key
k, [Term]
as, Blocker
_) <-
    if Bool
toplevel
      then TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey Bool
True Int
local Term
tm)
      else Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey Bool
True Int
local Term
tm

  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.add" Int
666 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"k:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Key -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Key -> m Doc
prettyTCM Key
k
    , TCMT IO Doc
"as: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
as
    ]
  Bool -> Int -> [Key] -> [Term] -> TCM [Key]
termPath Bool
False Int
local (Key
kKey -> [Key] -> [Key]
forall a. a -> [a] -> [a]
:[Key]
acc) ([Term]
as [Term] -> [Term] -> [Term]
forall a. Semigroup a => a -> a -> a
<> [Term]
todo)

-- | Insert a value into the discrimination tree, turning variables into
-- rigid locals or wildcards depending on the given scope.
insertDT
  :: (Ord a, PrettyTCM a)
  => Int   -- ^ Number of variables to consider wildcards, e.g. the number of leading invisible pis in an instance type.
  -> Term  -- ^ The term to use as a key
  -> a
  -> DiscrimTree a
  -> TCM (DiscrimTree a)
insertDT :: forall a.
(Ord a, PrettyTCM a) =>
Int -> Term -> a -> DiscrimTree a -> TCM (DiscrimTree a)
insertDT Int
local Term
key a
val DiscrimTree a
tree = do
  [Key]
path <- Bool -> Int -> [Key] -> [Term] -> TCM [Key]
termPath Bool
True Int
local [] [Term
key]
  let it :: DiscrimTree a
it = [Key] -> a -> DiscrimTree a
forall a. [Key] -> a -> DiscrimTree a
singletonDT [Key]
path a
val
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.add" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"added value" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
val TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"to discrimination tree with case"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (DiscrimTree a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
prettyTCM DiscrimTree a
it)
    , TCMT IO Doc
"its type:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
key)
    , TCMT IO Doc
"its path:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([Key] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Key] -> m Doc
prettyTCM [Key]
path)
    ]
  DiscrimTree a -> TCM (DiscrimTree a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DiscrimTree a -> TCM (DiscrimTree a))
-> DiscrimTree a -> TCM (DiscrimTree a)
forall a b. (a -> b) -> a -> b
$ DiscrimTree a -> DiscrimTree a -> DiscrimTree a
forall a. Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a
mergeDT DiscrimTree a
it DiscrimTree a
tree

-- | If a term matches this key, how many arguments does it place on the
-- spine?
keyArity :: Key -> Int
keyArity :: Key -> Int
keyArity = \case
  RigidK QName
_ Int
a -> Int
a
  LocalK Int
_ Int
a -> Int
a
  Key
PiK        -> Int
2
  Key
ConstK     -> Int
1
  Key
SortK      -> Int
0
  Key
FlexK      -> Int
0

data QueryResult a = QueryResult
  { forall a. QueryResult a -> Set a
resultValues  :: Set.Set a
  , forall a. QueryResult a -> Blocker
resultBlocker :: Blocker
  }

instance Ord a => Semigroup (QueryResult a) where
  QueryResult Set a
s Blocker
b <> :: QueryResult a -> QueryResult a -> QueryResult a
<> QueryResult Set a
s' Blocker
b' = Set a -> Blocker -> QueryResult a
forall a. Set a -> Blocker -> QueryResult a
QueryResult (Set a
s Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> Set a
s') (Blocker
b Blocker -> Blocker -> Blocker
`unblockOnEither` Blocker
b')

instance Ord a => Monoid (QueryResult a) where
  mempty :: QueryResult a
mempty = Set a -> Blocker -> QueryResult a
forall a. Set a -> Blocker -> QueryResult a
QueryResult Set a
forall a. Monoid a => a
mempty Blocker
neverUnblock

setResult :: Set.Set a -> QueryResult a
setResult :: forall a. Set a -> QueryResult a
setResult = (Set a -> Blocker -> QueryResult a)
-> Blocker -> Set a -> QueryResult a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Set a -> Blocker -> QueryResult a
forall a. Set a -> Blocker -> QueryResult a
QueryResult Blocker
neverUnblock

blockerResult :: Blocker -> QueryResult a
blockerResult :: forall a. Blocker -> QueryResult a
blockerResult = Set a -> Blocker -> QueryResult a
forall a. Set a -> Blocker -> QueryResult a
QueryResult Set a
forall a. Set a
Set.empty

-- | Look up a 'Term' in the given discrimination tree, treating local
-- variables as rigid symbols. The returned set is guaranteed to contain
-- everything that could overlap the given key.
lookupDT :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT :: forall a.
(Ord a, PrettyTCM a) =>
Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT = Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
forall a.
(Ord a, PrettyTCM a) =>
Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT' Bool
True

-- | Look up a 'Term' in the given discrimination tree, treating local
-- variables as wildcards.
lookupUnifyDT :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
lookupUnifyDT :: forall a.
(Ord a, PrettyTCM a) =>
Term -> DiscrimTree a -> TCM (QueryResult a)
lookupUnifyDT = Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
forall a.
(Ord a, PrettyTCM a) =>
Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT' Bool
False

lookupDT'
  :: forall a. (Ord a, PrettyTCM a)
  => Bool -- ^ Should local variables be treated as rigid?
  -> Term -- ^ The term to use as key
  -> DiscrimTree a
  -> TCM (QueryResult a)
lookupDT' :: forall a.
(Ord a, PrettyTCM a) =>
Bool -> Term -> DiscrimTree a -> TCM (QueryResult a)
lookupDT' Bool
localsRigid Term
term DiscrimTree a
tree = Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
True [Term
term] DiscrimTree a
tree where

  split :: Term -> TCM (Key, [Term], Blocker)
  split :: Term -> TCM (Key, [Term], Blocker)
split Term
tm | Bool
localsRigid = Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey Bool
False Int
0 Term
tm
  split Term
tm = do
    Int
ctx <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
    Bool -> Int -> Term -> TCM (Key, [Term], Blocker)
splitTermKey Bool
False Int
ctx Term
tm

  ignoreAbstractMaybe :: forall a. Bool -> TCM a -> TCM a
  ignoreAbstractMaybe :: forall a. Bool -> TCM a -> TCM a
ignoreAbstractMaybe Bool
True  = TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode
  ignoreAbstractMaybe Bool
False = TCMT IO a -> TCMT IO a
forall a. a -> a
id

  -- Match a spine against *all* clauses.
  explore :: [Term] -> [Term] -> [Term] -> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
  explore :: [Term]
-> [Term]
-> [Term]
-> [(Key, DiscrimTree a)]
-> TCM (QueryResult a)
explore [Term]
sp0 [Term]
sp1 [Term]
args [(Key, DiscrimTree a)]
bs = do
    let
      cont :: (Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a)
cont (Key
key, DiscrimTree a
trie) QueryResult a
res = do
        -- At the moment, explore will always be called with empty args.
        -- But even if this restriction is lifted in the future, we have
        -- to be careful about exploring. Consider:
        --
        --   instance
        --     _ : Foo (con x)
        --
        --   ⊢ Foo ?0
        --
        -- Since ?0 might be applied to more or less arguments than the
        -- one argument that is expected to be between sp0 and sp1 after
        -- matching con, we need to make sure that the spine has the
        -- right number of arguments, otherwise the (sp0, t:sp1) pattern
        -- for a Case will fail.
        let
          dummy :: a -> Term
dummy a
n = String -> Elims -> Term
Dummy (String
"_pad" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
n) []
          args' :: [Term]
args' = Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take (Key -> Int
keyArity Key
key) ([Term]
args [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [ Integer -> Term
forall {a}. Show a => a -> Term
dummy Integer
n | Integer
n <- [Integer
0..] ])

        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.lookup" Int
99 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"explore" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Key -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Key -> m Doc
prettyTCM Key
key TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Key -> Int
keyArity Key
key) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args)
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (DiscrimTree a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
prettyTCM DiscrimTree a
trie)
          , TCMT IO Doc
"sp0:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
sp0
          , TCMT IO Doc
"sp1:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
sp1
          , TCMT IO Doc
"args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
args
          , TCMT IO Doc
"args':" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
args'
          ]
        (QueryResult a -> QueryResult a -> QueryResult a
forall a. Semigroup a => a -> a -> a
<> QueryResult a
res) (QueryResult a -> QueryResult a)
-> TCM (QueryResult a) -> TCM (QueryResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
False ([Term]
sp0 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
args' [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
sp1) DiscrimTree a
trie

    ((Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a))
-> QueryResult a -> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (Key, DiscrimTree a) -> QueryResult a -> TCM (QueryResult a)
cont QueryResult a
forall a. Monoid a => a
mempty [(Key, DiscrimTree a)]
bs

  match :: Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
  match :: Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
toplevel [Term]
ts DiscrimTree a
EmptyDT    = QueryResult a -> TCM (QueryResult a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QueryResult a
forall a. Monoid a => a
mempty
  match Bool
toplevel [Term]
ts (DoneDT Set a
t) = Set a -> QueryResult a
forall a. Set a -> QueryResult a
setResult Set a
t QueryResult a -> TCM () -> TCM (QueryResult a)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.lookup" Int
99 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"done" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
ts
      , TCMT IO Doc
"  →" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Set a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set a -> m Doc
prettyTCM Set a
t
      ]

  match Bool
toplevel [Term]
ts tree :: DiscrimTree a
tree@(CaseDT Int
i Map Key (DiscrimTree a)
branches DiscrimTree a
rest) | ([Term]
sp0, Term
t:[Term]
sp1) <- Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [Term]
ts = do
    let
      ([Term]
sp0, Term
t:[Term]
sp1) = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [Term]
ts
      visit :: Key -> [Term] -> TCM (QueryResult a)
visit Key
k [Term]
sp' = case Key -> Map Key (DiscrimTree a) -> Maybe (DiscrimTree a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Key
k Map Key (DiscrimTree a)
branches of
        Just DiscrimTree a
m  -> Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
False [Term]
sp' DiscrimTree a
m
        Maybe (DiscrimTree a)
Nothing -> QueryResult a -> TCM (QueryResult a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QueryResult a
forall a. Monoid a => a
mempty

    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
toplevel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.lookup" Int
99 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"match" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
sp0 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc
"«" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"»") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
sp1
      , DiscrimTree a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
prettyTCM DiscrimTree a
tree
      ]

    -- TODO (Amy, 2024-02-12): Could use reduceB in splitTermKey, and
    -- the blocker here, to suspend instances more precisely when there
    -- is an ambiguity.
    Bool -> TCM (Key, [Term], Blocker) -> TCM (Key, [Term], Blocker)
forall a. Bool -> TCM a -> TCM a
ignoreAbstractMaybe Bool
toplevel (Term -> TCM (Key, [Term], Blocker)
split Term
t) TCM (Key, [Term], Blocker)
-> ((Key, [Term], Blocker) -> TCM (QueryResult a))
-> TCM (QueryResult a)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (Key
FlexK, [Term]
args, Blocker
blocker) -> do

        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.lookup" Int
99 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"flexible term was forced"
          , TCMT IO Doc
"t:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
t)
          , TCMT IO Doc
"will explore" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Map Key (DiscrimTree a) -> Int
forall a. Map Key a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Key (DiscrimTree a)
branches Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"branches"
          ]
        Term -> TCM ()
tickExplore Term
t

        -- If we have a "flexible head" at this position then instance
        -- search *at this point* degenerates to looking for all
        -- possible matches.
        --
        -- In any nested CaseDTs, however, it's possible for us to
        -- recover and go back to productively matching. Consider:
        --
        --    instance
        --      xa : X T1 A
        --      xb : X T2 B
        --
        --    ⊢ X ?0 A
        --
        -- Since ?0 is way too flabby to narrow which of T1 or T2 should
        -- be taken, we take both. But then we match A against A and B:
        -- this query will only return {xa}.

        QueryResult a
branches <- [Term]
-> [Term]
-> [Term]
-> [(Key, DiscrimTree a)]
-> TCM (QueryResult a)
explore [Term]
sp0 [Term]
sp1 [Term]
args ([(Key, DiscrimTree a)] -> TCM (QueryResult a))
-> [(Key, DiscrimTree a)] -> TCM (QueryResult a)
forall a b. (a -> b) -> a -> b
$ Map Key (DiscrimTree a) -> [(Key, DiscrimTree a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Key (DiscrimTree a)
branches
        QueryResult a
rest <- Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
False [Term]
ts DiscrimTree a
rest

        QueryResult a -> TCM (QueryResult a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QueryResult a -> TCM (QueryResult a))
-> QueryResult a -> TCM (QueryResult a)
forall a b. (a -> b) -> a -> b
$! QueryResult a
rest QueryResult a -> QueryResult a -> QueryResult a
forall a. Semigroup a => a -> a -> a
<> QueryResult a
branches QueryResult a -> QueryResult a -> QueryResult a
forall a. Semigroup a => a -> a -> a
<> Blocker -> QueryResult a
forall a. Blocker -> QueryResult a
blockerResult Blocker
blocker

      (Key
k, [Term]
args, Blocker
blocker) -> do
        let sp' :: [Term]
sp' = [Term]
sp0 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
args [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
sp1

        -- Actually take the branch corresponding to our rigid head.
        QueryResult a
branch <- Key -> [Term] -> TCM (QueryResult a)
visit Key
k [Term]
sp'

        -- When exploring the rest of the tree, the value we cased on
        -- has to be put back in the tree. mergeDT does not perform
        -- commuting conversions to ensure that variables aren't
        -- repeatedly cased on.
        QueryResult a
rest <- Bool -> [Term] -> DiscrimTree a -> TCM (QueryResult a)
match Bool
False [Term]
ts DiscrimTree a
rest

        QueryResult a -> TCM (QueryResult a)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QueryResult a -> TCM (QueryResult a))
-> QueryResult a -> TCM (QueryResult a)
forall a b. (a -> b) -> a -> b
$! QueryResult a
rest QueryResult a -> QueryResult a -> QueryResult a
forall a. Semigroup a => a -> a -> a
<> QueryResult a
branch

  match Bool
_ [Term]
ts tree :: DiscrimTree a
tree@(CaseDT Int
i Map Key (DiscrimTree a)
_ DiscrimTree a
rest) = do
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.instance.discrim.lookup" Int
99 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"IMPOSSIBLE match" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
ts
      , DiscrimTree a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DiscrimTree a -> m Doc
prettyTCM DiscrimTree a
tree
      ]
    -- This really is impossible: since each branch is annotated with
    -- its arity, we only take branches corresponding to neutrals which
    -- exploded into enough arguments.
    TCM (QueryResult a)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Smart constructor for a leaf node.
doneDT :: Set.Set a -> DiscrimTree a
doneDT :: forall a. Set a -> DiscrimTree a
doneDT Set a
s | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s = DiscrimTree a
forall a. DiscrimTree a
EmptyDT
doneDT Set a
s = Set a -> DiscrimTree a
forall a. Set a -> DiscrimTree a
DoneDT Set a
s

-- | Remove a set of values from the discrimination tree. The tree is
-- rebuilt so that cases with no leaves are removed.
deleteFromDT :: Ord a => DiscrimTree a -> Set.Set a -> DiscrimTree a
deleteFromDT :: forall a. Ord a => DiscrimTree a -> Set a -> DiscrimTree a
deleteFromDT DiscrimTree a
dt Set a
gone = case DiscrimTree a
dt of
  DiscrimTree a
EmptyDT -> DiscrimTree a
forall a. DiscrimTree a
EmptyDT
  DoneDT Set a
s ->
    let s' :: Set a
s' = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set a
s Set a
gone
     in Set a -> DiscrimTree a
forall a. Set a -> DiscrimTree a
doneDT Set a
s'
  CaseDT Int
i Map Key (DiscrimTree a)
s DiscrimTree a
k ->
    let
      del :: DiscrimTree a -> Maybe (DiscrimTree a)
del DiscrimTree a
x = case DiscrimTree a -> Set a -> DiscrimTree a
forall a. Ord a => DiscrimTree a -> Set a -> DiscrimTree a
deleteFromDT DiscrimTree a
x Set a
gone of
        DiscrimTree a
EmptyDT -> Maybe (DiscrimTree a)
forall a. Maybe a
Nothing
        DiscrimTree a
dt'     -> DiscrimTree a -> Maybe (DiscrimTree a)
forall a. a -> Maybe a
Just DiscrimTree a
dt'

      s' :: Map Key (DiscrimTree a)
s' = (DiscrimTree a -> Maybe (DiscrimTree a))
-> Map Key (DiscrimTree a) -> Map Key (DiscrimTree a)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe DiscrimTree a -> Maybe (DiscrimTree a)
del Map Key (DiscrimTree a)
s
      k' :: DiscrimTree a
k' = DiscrimTree a -> Set a -> DiscrimTree a
forall a. Ord a => DiscrimTree a -> Set a -> DiscrimTree a
deleteFromDT DiscrimTree a
k Set a
gone
    in if | Map Key (DiscrimTree a) -> Bool
forall k a. Map k a -> Bool
Map.null Map Key (DiscrimTree a)
s' -> DiscrimTree a
k'
          | Bool
otherwise   -> Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
forall a.
Int -> Map Key (DiscrimTree a) -> DiscrimTree a -> DiscrimTree a
CaseDT Int
i Map Key (DiscrimTree a)
s' DiscrimTree a
k'