{-# LANGUAGE PatternSynonyms #-}
module Agda.TypeChecking.Implicit where
import Control.Monad
import Control.Monad.Except
import Control.Monad.IO.Class
import Agda.Syntax.Position (beginningOf, getRange)
import Agda.Syntax.Common
import Agda.Syntax.Abstract (Binder, mkBinder_)
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (unquoteTactic)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Telescope
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Tuple
insertImplicitBindersT
:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
=> [NamedArg Binder]
-> Type
-> m [NamedArg Binder]
insertImplicitBindersT :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
[NamedArg Binder] -> Type -> m [NamedArg Binder]
insertImplicitBindersT = \case
[] -> \ Type
_ -> [NamedArg Binder] -> m [NamedArg Binder]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
NamedArg Binder
b : [NamedArg Binder]
bs -> List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
List1 (NamedArg Binder) -> [NamedArg Binder]
forall l. IsList l => l -> [Item l]
List1.toList (List1 (NamedArg Binder) -> [NamedArg Binder])
-> (Type -> m (List1 (NamedArg Binder)))
-> Type
-> m [NamedArg Binder]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
insertImplicitBindersT1 (NamedArg Binder
b NamedArg Binder -> [NamedArg Binder] -> List1 (NamedArg Binder)
forall a. a -> [a] -> NonEmpty a
:| [NamedArg Binder]
bs)
insertImplicitBindersT1
:: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
=> List1 (NamedArg Binder)
-> Type
-> m (List1 (NamedArg Binder))
insertImplicitBindersT1 :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
insertImplicitBindersT1 bs :: List1 (NamedArg Binder)
bs@(NamedArg Binder
b :| [NamedArg Binder]
_) Type
a = NamedArg Binder
-> m (List1 (NamedArg Binder)) -> m (List1 (NamedArg Binder))
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Binder
b (m (List1 (NamedArg Binder)) -> m (List1 (NamedArg Binder)))
-> m (List1 (NamedArg Binder)) -> m (List1 (NamedArg Binder))
forall a b. (a -> b) -> a -> b
$ do
TelV Tele (Dom Type)
tel Type
ty0 <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
a
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda.imp" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
"insertImplicitBindersT"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"bs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma (NonEmpty (TCMT IO Doc) -> [TCMT IO Doc])
-> NonEmpty (TCMT IO Doc) -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Binder -> TCMT IO Doc)
-> List1 (NamedArg Binder) -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Binder -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
bs
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
tel
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ty = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty0)
]
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda.imp" Int
70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
"insertImplicitBindersT"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"bs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (List1 (NamedArg Binder) -> ArgName)
-> List1 (NamedArg Binder)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg Binder] -> ArgName
forall a. Show a => a -> ArgName
show ([NamedArg Binder] -> ArgName)
-> (List1 (NamedArg Binder) -> [NamedArg Binder])
-> List1 (NamedArg Binder)
-> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
List1 (NamedArg Binder) -> [NamedArg Binder]
forall l. IsList l => l -> [Item l]
List1.toList) List1 (NamedArg Binder)
bs
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Tele (Dom Type) -> ArgName) -> Tele (Dom Type) -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> ArgName
forall a. Show a => a -> ArgName
show) Tele (Dom Type)
tel
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ty = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Type -> ArgName) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ArgName
forall a. Show a => a -> ArgName
show) Type
ty0
]
[NamedArg Binder]
hs <- NamedArg Binder -> Tele (Dom Type) -> m [NamedArg Binder]
forall {m :: * -> *} {e} {t}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
MonadFresh NameId m, HasRange e) =>
NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
insImp NamedArg Binder
b Tele (Dom Type)
tel
let bs0 :: List1 (NamedArg Binder)
bs0@(NamedArg Binder
b1 :| [NamedArg Binder]
bs1) = [NamedArg Binder]
-> List1 (NamedArg Binder) -> List1 (NamedArg Binder)
forall a. [a] -> NonEmpty a -> NonEmpty a
List1.prependList [NamedArg Binder]
hs List1 (NamedArg Binder)
bs
Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a m Type
-> (Type -> m (Either (Dom Type, Abs Type) Type))
-> m (Either (Dom Type, Abs Type) Type)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath m (Either (Dom Type, Abs Type) Type)
-> (Either (Dom Type, Abs Type) Type
-> m (List1 (NamedArg Binder)))
-> m (List1 (NamedArg Binder))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left (Dom Type
_, Abs Type
ty) -> (NamedArg Binder
b1 NamedArg Binder -> [NamedArg Binder] -> List1 (NamedArg Binder)
forall a. a -> [a] -> NonEmpty a
:|) ([NamedArg Binder] -> List1 (NamedArg Binder))
-> m [NamedArg Binder] -> m (List1 (NamedArg Binder))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Binder] -> Type -> m [NamedArg Binder]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
[NamedArg Binder] -> Type -> m [NamedArg Binder]
insertImplicitBindersT [NamedArg Binder]
bs1 (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
ty)
Right{} -> List1 (NamedArg Binder) -> m (List1 (NamedArg Binder))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return List1 (NamedArg Binder)
bs0
where
insImp :: NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
insImp NamedArg e
b Tele (Dom t)
EmptyTel = [NamedArg Binder] -> m [NamedArg Binder]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
insImp NamedArg e
b Tele (Dom t)
tel = case NamedArg e -> [Dom (ArgName, t)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg e
b ([Dom (ArgName, t)] -> ImplicitInsertion)
-> [Dom (ArgName, t)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Tele (Dom t) -> [Dom (ArgName, t)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
tel of
ImplicitInsertion
BadImplicits -> TypeError -> m [NamedArg Binder]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
NoSuchName ArgName
x -> TypeError -> m [NamedArg Binder]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
ImpInsert [Dom ()]
doms -> (Dom () -> m (NamedArg Binder)) -> [Dom ()] -> m [NamedArg Binder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Dom () -> m (NamedArg Binder)
implicitArg [Dom ()]
doms
where
implicitArg :: Dom () -> m (NamedArg Binder)
implicitArg Dom ()
d = Origin -> NamedArg Binder -> NamedArg Binder
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (NamedArg Binder -> NamedArg Binder)
-> (Name -> NamedArg Binder) -> Name -> NamedArg Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg (Dom () -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom ()
d) (Binder -> NamedArg Binder)
-> (Name -> Binder) -> Name -> NamedArg Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Binder
mkBinder_ (Name -> NamedArg Binder) -> m Name -> m (NamedArg Binder)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Range -> m Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName (Range -> m Name) -> Range -> m Name
forall a b. (a -> b) -> a -> b
$ Range -> Range
beginningOf (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ NamedArg e -> Range
forall a. HasRange a => a -> Range
getRange NamedArg e
b
implicitArgs
:: (PureTCM m, MonadMetaSolver m, MonadTCM m)
=> Int
-> (Hiding -> Bool)
-> Type
-> m (Args, Type)
implicitArgs :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs Int
n Hiding -> Bool
expand Type
t = ([Arg (Named NamedName Term)] -> Args)
-> ([Arg (Named NamedName Term)], Type) -> (Args, Type)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst ((Arg (Named NamedName Term) -> Arg Term)
-> [Arg (Named NamedName Term)] -> Args
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Term -> Term)
-> Arg (Named NamedName Term) -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Term -> Term
forall name a. Named name a -> a
namedThing)) (([Arg (Named NamedName Term)], Type) -> (Args, Type))
-> m ([Arg (Named NamedName Term)], Type) -> m (Args, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n (\ Hiding
h ArgName
x -> Hiding -> Bool
expand Hiding
h) Type
t
implicitNamedArgs
:: (PureTCM m, MonadMetaSolver m, MonadTCM m)
=> Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m (NamedArgs, Type)
implicitNamedArgs :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
0 Hiding -> ArgName -> Bool
expand Type
t0 = ([Arg (Named NamedName Term)], Type)
-> m ([Arg (Named NamedName Term)], Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0)
implicitNamedArgs Int
n Hiding -> ArgName -> Bool
expand Type
t0 = do
Type
t0' <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t0
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"implicitNamedArgs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0'
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args" Int
80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"implicitNamedArgs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type -> ArgName
forall a. Show a => a -> ArgName
show Type
t0')
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t0' of
Pi dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, domTactic :: forall t e. Dom' t e -> Maybe t
domTactic = Maybe Term
tac, unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Abs Type
b
| let x :: ArgName
x = ArgName -> Dom Type -> ArgName
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Dom Type
dom, Hiding -> ArgName -> Bool
expand (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) ArgName
x -> do
ArgInfo
info' <- if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
hidden ArgInfo
info then ArgInfo -> m ArgInfo
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info else do
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.ifs" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"inserting instance meta for type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
ArgName -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.ifs" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"x = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> ArgName
forall a. Show a => a -> ArgName
show ArgName
x)
, TCMT IO Doc
"hiding = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Hiding -> ArgName
forall a. Show a => a -> ArgName
show (Hiding -> ArgName) -> Hiding -> ArgName
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info)
]
ArgInfo -> m ArgInfo
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> m ArgInfo) -> ArgInfo -> m ArgInfo
forall a b. (a -> b) -> a -> b
$ ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
makeInstance ArgInfo
info
(MetaId
_, Term
v) <- ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg ArgInfo
info' ArgName
x Comparison
CmpLeq Type
a
Maybe Term -> (Term -> m ()) -> m ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Term
tac ((Term -> m ()) -> m ()) -> (Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
tac -> TCM () -> m ()
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> m ()) -> TCM () -> m ()
forall a b. (a -> b) -> a -> b
$
ArgInfo -> TCM () -> TCM ()
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
v Type
a
let narg :: Arg (Named NamedName Term)
narg = ArgInfo -> Named NamedName Term -> Arg (Named NamedName Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe NamedName -> Term -> Named NamedName Term
forall name a. Maybe name -> a -> Named name a
Named (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged ArgName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
forall a b. (a -> b) -> a -> b
$ ArgName -> Ranged ArgName
forall a. a -> Ranged a
unranged ArgName
x) Term
v)
([Arg (Named NamedName Term)] -> [Arg (Named NamedName Term)])
-> ([Arg (Named NamedName Term)], Type)
-> ([Arg (Named NamedName Term)], Type)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Arg (Named NamedName Term)
narg Arg (Named NamedName Term)
-> [Arg (Named NamedName Term)] -> [Arg (Named NamedName Term)]
forall a. a -> [a] -> [a]
:) (([Arg (Named NamedName Term)], Type)
-> ([Arg (Named NamedName Term)], Type))
-> m ([Arg (Named NamedName Term)], Type)
-> m ([Arg (Named NamedName Term)], Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Hiding -> ArgName -> Bool
expand (Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
SubstArg Type
v)
Term
_ -> ([Arg (Named NamedName Term)], Type)
-> m ([Arg (Named NamedName Term)], Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0')
newMetaArg
:: (PureTCM m, MonadMetaSolver m)
=> ArgInfo
-> ArgName
-> Comparison
-> Type
-> m (MetaId, Term)
newMetaArg :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg ArgInfo
info ArgName
x Comparison
cmp Type
a = do
Either Blocker Bool
prp <- BlockT m Bool -> m (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT m Bool -> m (Either Blocker Bool))
-> BlockT m Bool -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type -> BlockT m Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
a
let irrelevantIfProp :: m (MetaId, Term) -> m (MetaId, Term)
irrelevantIfProp =
Bool
-> (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term)
-> m (MetaId, Term)
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Either Blocker Bool
prp Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) ((m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term))
-> (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term)
-> m (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ Relevance -> m (MetaId, Term) -> m (MetaId, Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
Irrelevant
ArgInfo -> m (MetaId, Term) -> m (MetaId, Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ m (MetaId, Term) -> m (MetaId, Term)
irrelevantIfProp (m (MetaId, Term) -> m (MetaId, Term))
-> m (MetaId, Term) -> m (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
Hiding -> ArgName -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
Hiding -> ArgName -> Type -> m (MetaId, Term)
newMeta (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgName -> ArgName
argNameToString ArgName
x) Type
a
where
newMeta :: MonadMetaSolver m => Hiding -> String -> Type -> m (MetaId, Term)
newMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Hiding -> ArgName -> Type -> m (MetaId, Term)
newMeta Instance{} ArgName
n = ArgName -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
ArgName -> Type -> m (MetaId, Term)
newInstanceMeta ArgName
n
newMeta Hiding
Hidden ArgName
n = RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
newMeta Hiding
NotHidden ArgName
n = RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
newInteractionMetaArg
:: ArgInfo
-> ArgName
-> Comparison
-> Type
-> TCM (MetaId, Term)
newInteractionMetaArg :: ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg ArgInfo
info ArgName
x Comparison
cmp Type
a = do
ArgInfo -> TCM (MetaId, Term) -> TCM (MetaId, Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCM (MetaId, Term) -> TCM (MetaId, Term))
-> TCM (MetaId, Term) -> TCM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
Hiding -> ArgName -> Type -> TCM (MetaId, Term)
newMeta (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgName -> ArgName
argNameToString ArgName
x) Type
a
where
newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
newMeta :: Hiding -> ArgName -> Type -> TCM (MetaId, Term)
newMeta Instance{} ArgName
n = ArgName -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
ArgName -> Type -> m (MetaId, Term)
newInstanceMeta ArgName
n
newMeta Hiding
Hidden ArgName
n = RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
newMeta Hiding
NotHidden ArgName
n = RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
data ImplicitInsertion
= ImpInsert [Dom ()]
| BadImplicits
| NoSuchName ArgName
deriving (Int -> ImplicitInsertion -> ArgName -> ArgName
[ImplicitInsertion] -> ArgName -> ArgName
ImplicitInsertion -> ArgName
(Int -> ImplicitInsertion -> ArgName -> ArgName)
-> (ImplicitInsertion -> ArgName)
-> ([ImplicitInsertion] -> ArgName -> ArgName)
-> Show ImplicitInsertion
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
showsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
$cshow :: ImplicitInsertion -> ArgName
show :: ImplicitInsertion -> ArgName
$cshowList :: [ImplicitInsertion] -> ArgName -> ArgName
showList :: [ImplicitInsertion] -> ArgName -> ArgName
Show)
pattern NoInsertNeeded :: ImplicitInsertion
pattern $mNoInsertNeeded :: forall {r}. ImplicitInsertion -> ((# #) -> r) -> ((# #) -> r) -> r
$bNoInsertNeeded :: ImplicitInsertion
NoInsertNeeded = ImpInsert []
insertImplicit
:: NamedArg e
-> [Dom a]
-> ImplicitInsertion
insertImplicit :: forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg e
a [Dom a]
doms = NamedArg e -> [Dom ArgName] -> ImplicitInsertion
forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
insertImplicit' NamedArg e
a ([Dom ArgName] -> ImplicitInsertion)
-> [Dom ArgName] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
[Dom a] -> (Dom a -> Dom ArgName) -> [Dom ArgName]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom a]
doms ((Dom a -> Dom ArgName) -> [Dom ArgName])
-> (Dom a -> Dom ArgName) -> [Dom ArgName]
forall a b. (a -> b) -> a -> b
$ \ Dom a
dom ->
Dom a
dom Dom a -> ArgName -> Dom ArgName
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ArgName -> Dom a -> ArgName
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Dom a
dom
insertImplicit'
:: NamedArg e
-> [Dom ArgName]
-> ImplicitInsertion
insertImplicit' :: forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
insertImplicit' NamedArg e
_ [] = ImplicitInsertion
BadImplicits
insertImplicit' NamedArg e
a [Dom ArgName]
ts
| NamedArg e -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg e
a = [Dom ()] -> ImplicitInsertion
ImpInsert ([Dom ()] -> ImplicitInsertion) -> [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ (Dom () -> Bool) -> [Dom ()] -> [Dom ()]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Dom () -> Bool
forall a. LensHiding a => a -> Bool
notVisible ([Dom ()] -> [Dom ()]) -> [Dom ()] -> [Dom ()]
forall a b. (a -> b) -> a -> b
$ (Dom ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map Dom ArgName -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom ArgName]
ts
| Just ArgName
x <- NamedArg e -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg e
a = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArgName -> ImplicitInsertion
NoSuchName ArgName
x) [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
(Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (\ Dom ArgName
t -> ArgName
x ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== Dom ArgName -> ArgName
forall t e. Dom' t e -> e
unDom Dom ArgName
t Bool -> Bool -> Bool
&& NamedArg e -> Dom ArgName -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a Dom ArgName
t) [Dom ArgName]
ts
| Bool
otherwise = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ImplicitInsertion
BadImplicits [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
(Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (NamedArg e -> Dom ArgName -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a) [Dom ArgName]
ts
where
takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil Dom ArgName -> Bool
p [Dom ArgName]
ts =
case [Dom ArgName]
ts2 of
[] -> Maybe [Dom ()]
forall a. Maybe a
Nothing
(Dom ArgName
t : [Dom ArgName]
_) -> if Dom ArgName -> Bool
forall a. LensHiding a => a -> Bool
visible Dom ArgName
t then Maybe [Dom ()]
forall a. Maybe a
Nothing else [Dom ()] -> Maybe [Dom ()]
forall a. a -> Maybe a
Just ([Dom ()] -> Maybe [Dom ()]) -> [Dom ()] -> Maybe [Dom ()]
forall a b. (a -> b) -> a -> b
$ (Dom ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map Dom ArgName -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom ArgName]
ts1
where
([Dom ArgName]
ts1, [Dom ArgName]
ts2) = (Dom ArgName -> Bool)
-> [Dom ArgName] -> ([Dom ArgName], [Dom ArgName])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ Dom ArgName
t -> Dom ArgName -> Bool
p Dom ArgName
t Bool -> Bool -> Bool
|| Dom ArgName -> Bool
forall a. LensHiding a => a -> Bool
visible Dom ArgName
t) [Dom ArgName]
ts