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(..))
etaExpansionDummy :: Term
etaExpansionDummy :: Term
etaExpansionDummy = String -> Elims -> Term
Dummy String
"eta-record argument in instance head" []
termKeyElims
:: Bool
-> TCM Type
-> [Arg Term]
-> TCM (Int, [Term])
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
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
| Bool
maybeEta = Term
etaExpansionDummy
| Bool
otherwise = Term
a
(k, there) <- addContext dom (go (unAbs ty') as)
pure (k + 1, here: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
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
| 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 ()
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
(b, 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 tm' of
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
info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case theDef 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
(arity, 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
pure (RigidK q arity, as, neverUnblock)
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
(arity, as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
precise TCM Type
ty [Arg Term]
as
pure (LocalK (i - local) arity, as, neverUnblock)
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
(arity, as) <- Bool -> TCM Type -> [Arg Term] -> TCM (Int, [Term])
termKeyElims Bool
precise TCM Type
ty [Arg Term]
as
pure (RigidK q arity, as, neverUnblock)
Pi Dom Type
dom Abs Type
ret ->
let
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
| 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)
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
(k, as, _) <-
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
reportSDoc "tc.instance.discrim.add" 666 $ vcat
[ "k: " <+> prettyTCM k
, "as: " <+> prettyTCM as
]
termPath False local (k:acc) (as <> todo)
insertDT
:: (Ord a, PrettyTCM a)
=> Int
-> Term
-> 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
path <- Bool -> Int -> [Key] -> [Term] -> TCM [Key]
termPath Bool
True Int
local [] [Term
key]
let it = [Key] -> a -> DiscrimTree a
forall a. [Key] -> a -> DiscrimTree a
singletonDT [Key]
path a
val
reportSDoc "tc.instance.discrim.add" 20 $ vcat
[ "added value" <+> prettyTCM val <+> "to discrimination tree with case"
, nest 2 (prettyTCM it)
, "its type:"
, nest 2 (prettyTCM key)
, "its path:"
, nest 2 (prettyTCM path)
]
pure $ mergeDT it tree
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
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
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
-> Term
-> 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
ctx <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
splitTermKey False ctx 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
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
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
]
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
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
rest <- match False ts rest
pure $! rest <> branches <> blockerResult 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
branch <- Key -> [Term] -> TCM (QueryResult a)
visit Key
k [Term]
sp'
rest <- match False ts rest
pure $! rest <> 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
]
TCM (QueryResult a)
forall a. HasCallStack => a
__IMPOSSIBLE__
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
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'