module Agda.TypeChecking.InstanceArguments where
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Scope.Base (isNameInScope)
import Agda.TypeChecking.Errors ()
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Conversion
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Functor
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Null (empty)
#include "undefined.h"
import Agda.Utils.Impossible
initialIFSCandidates :: Type -> TCM (Maybe [Candidate])
initialIFSCandidates t = do
cands1 <- getContextVars
otn <- getOutputTypeName t
case otn of
NoOutputTypeName -> typeError $ GenericError $ "Instance search can only be used to find elements in a named type"
OutputTypeNameNotYetKnown -> return Nothing
OutputTypeVar -> return $ Just cands1
OutputTypeName n -> do
cands2 <- getScopeDefs n
return $ Just $ cands1 ++ cands2
where
getContextVars :: TCM [Candidate]
getContextVars = do
ctx <- getContext
let vars = [ Candidate (var i) (raise (i + 1) t) ExplicitStayExplicit (argInfoOverlappable info)
| (Dom info (x, t), i) <- zip ctx [0..]
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
let cxtAndTypes = [ (var i, snd $ unDom $ raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
reportSDoc "tc.instance.fields" 30 $ text "instance field candidates" $$ nest 2 (vcat
[ sep [ (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":"
, nest 2 $ prettyTCM t ] | Candidate v t _ overlap <- fields ])
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ Candidate v t ExplicitStayExplicit False
| (v, Dom info t) <- env
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
return $ vars ++ fields ++ lets
etaExpand etaOnce t =
isEtaRecordType t >>= \case
Nothing | etaOnce -> do
isRecordType t >>= \case
Nothing -> return Nothing
Just (r, vs, _) -> do
m <- currentModule
if qnameToList r `isPrefixOf` mnameToList m
then return (Just (r, vs))
else return Nothing
r -> return r
instanceFields = instanceFields' True
instanceFields' etaOnce (v, t) =
caseMaybeM (etaExpand etaOnce =<< reduce t) (return []) $ \ (r, pars) -> do
(tel, args) <- forceEtaExpandRecord r pars v
let types = map unDom $ applySubst (parallelS $ reverse $ map unArg args) (flattenTel tel)
fmap concat $ forM (zip args types) $ \ (arg, t) ->
([ Candidate (unArg arg) t ExplicitStayExplicit (argInfoOverlappable $ argInfo arg)
| getHiding arg == Instance ] ++) <$>
instanceFields' False (unArg arg, t)
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asks envRelevance
let qs = maybe [] Set.toList $ Map.lookup n instanceDefs
catMaybes <$> mapM (candidate rel) qs
candidate :: Relevance -> QName -> TCM (Maybe Candidate)
candidate rel q =
flip catchError handle $ do
def <- getConstInfo q
let r = defRelevance def
if not (r `moreRelevant` rel) then return Nothing else do
t <- defType <$> instantiateDef def
args <- freeVarsToApply q
let v = case theDef def of
Function{ funProjection = Just p } -> projDropParsApply p ProjSystem args
Constructor{ conSrcCon = c } -> Con c ConOSystem []
_ -> Def q $ map Apply args
inScope <- isNameInScope q <$> getScope
return $ Candidate v t ExplicitToInstance False <$ guard inScope
where
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
findInScope :: MetaId -> Maybe [Candidate] -> TCM ()
findInScope m Nothing = do
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 20 $ "The type of the FindInScope constraint isn't known, trying to find it again."
t <- getMetaType m
cands <- initialIFSCandidates t
case cands of
Nothing -> addConstraint $ FindInScope m Nothing Nothing
Just {} -> findInScope m cands
findInScope m (Just cands) =
whenJustM (findInScope' m cands) $ (\ (cands, b) -> addConstraint $ FindInScope m b $ Just cands)
findInScope' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Maybe MetaId))
findInScope' m cands = ifM (isFrozen m) (return (Just (cands, Nothing))) $ do
ifM (isFullyInstantiatedMeta m) (return Nothing) $ do
mv <- lookupMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 15 $
"findInScope 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
reportSDoc "tc.instance" 60 $ nest 2 $ vcat
[ sep [ (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":"
, nest 2 $ prettyTCM t ] | Candidate v t _ overlap <- cands ]
t <- normalise =<< getMetaTypeInContext m
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ show t
ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> do
reportSLn "tc.instance" 15 "aborting due to non-rigidly constrained metas"
return (Just (cands, Just m))) $ do
mcands <- checkCandidates m t cands
debugConstraints
case mcands of
Just [] -> do
reportSDoc "tc.instance" 15 $
text "findInScope 5: not a single candidate found..."
typeError $ IFSNoCandidateInScope t
Just [Candidate term t' _ _] -> do
reportSDoc "tc.instance" 15 $ vcat
[ text "findInScope 5: solved by instance search using the only candidate"
, nest 2 $ prettyTCM term
, text "of type " <+> prettyTCM t'
, text "for type" <+> prettyTCM t
]
wakeConstraints (return . const True)
solveAwakeConstraints' False
return Nothing
_ -> do
let cs = fromMaybe cands mcands
reportSDoc "tc.instance" 15 $
text ("findInScope 5: refined candidates: ") <+>
prettyTCM (List.map candidateTerm cs)
return (Just (cs, Nothing))
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi t ret =
case ignoreSharing $ unEl t of
Pi a b -> addContext' (absName b, a) $ insidePi (unAbs b) ret
Def{} -> ret t
Var{} -> ret t
Sort{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
rigidlyConstrainedMetas :: TCM [MetaId]
rigidlyConstrainedMetas = do
cs <- (++) <$> use stSleepingConstraints <*> use stAwakeConstraints
catMaybes <$> mapM rigidMetas cs
where
isRigid v = do
bv <- reduceB v
case ignoreSharing <$> bv of
Blocked{} -> return False
NotBlocked _ v -> case v of
MetaV{} -> return False
Def f _ -> return True
Con{} -> return True
Lit{} -> return True
Var{} -> return True
Sort{} -> return True
Pi{} -> return True
Level{} -> return False
DontCare{} -> return False
Lam{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
rigidMetas c =
case clValue $ theConstraint c of
ValueCmp _ _ u v ->
case (ignoreSharing u, ignoreSharing v) of
(MetaV m us, _) | isJust (allApplyElims us) -> ifM (isRigid v) (return $ Just m) (return Nothing)
(_, MetaV m vs) | isJust (allApplyElims vs) -> ifM (isRigid u) (return $ Just m) (return Nothing)
_ -> return Nothing
ElimCmp{} -> return Nothing
TypeCmp{} -> return Nothing
TelCmp{} -> return Nothing
SortCmp{} -> return Nothing
LevelCmp{} -> return Nothing
UnBlock{} -> return Nothing
Guarded{} -> return Nothing
IsEmpty{} -> return Nothing
CheckSizeLtSat{} -> return Nothing
FindInScope{} -> return Nothing
isRigid :: MetaId -> TCM Bool
isRigid i = do
rigid <- rigidlyConstrainedMetas
return (elem i rigid)
areThereNonRigidMetaArguments :: Term -> TCM (Maybe MetaId)
areThereNonRigidMetaArguments t = case ignoreSharing t of
Def n args -> do
TelV tel _ <- telView . defType =<< getConstInfo n
let varOccs EmptyTel = []
varOccs (ExtendTel a btel)
| getRelevance a == Irrelevant = WeaklyRigid : varOccs tel
| otherwise = occurrence 0 tel : varOccs tel
where tel = unAbs btel
rigid StronglyRigid = True
rigid Unguarded = True
rigid WeaklyRigid = True
rigid _ = False
reportSDoc "tc.instance.rigid" 70 $ text "class args:" <+> prettyTCM tel $$
nest 2 (text $ "used: " ++ show (varOccs tel))
areThereNonRigidMetaArgs [ arg | (o, arg) <- zip (varOccs tel) args, not $ rigid o ]
Var n args -> return Nothing
Sort{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
Pi{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
where
areThereNonRigidMetaArgs :: Elims -> TCM (Maybe MetaId)
areThereNonRigidMetaArgs [] = return Nothing
areThereNonRigidMetaArgs (Proj{} : xs) = areThereNonRigidMetaArgs xs
areThereNonRigidMetaArgs (Apply x : xs) = do
ifJustM (isNonRigidMeta $ unArg x) (return . Just) (areThereNonRigidMetaArgs xs)
isNonRigidMeta :: Term -> TCM (Maybe MetaId)
isNonRigidMeta v =
case ignoreSharing v of
Def _ es -> areThereNonRigidMetaArgs es
Var _ es -> areThereNonRigidMetaArgs es
Con _ _ vs-> areThereNonRigidMetaArgs (map Apply vs)
MetaV i _ -> ifM (isRigid i) (return Nothing) $ do
Def lvl [] <- ignoreSharing <$> primLevel
sz <- for (fmap ignoreSharing <$> getBuiltin' builtinSize) $ \case
Just (Def sz []) -> [sz]
Nothing -> []
_ -> __IMPOSSIBLE__
o <- getOutputTypeName . jMetaType . mvJudgement =<< lookupMeta i
case o of
OutputTypeName l | elem l (lvl : sz) -> return Nothing
_ -> return (Just i)
Lam _ t -> isNonRigidMeta (unAbs t)
_ -> return Nothing
filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM [Candidate]
filterResetingState m cands f = disableDestructiveUpdate $ do
ctxArgs <- getContextArgs
let ctxElims = map Apply ctxArgs
tryC c = do
ok <- f c
v <- instantiateFull (MetaV m ctxElims)
a <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
return (ok, v, a)
result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
case [ err | (_, ((HellNo err, _, _), _)) <- result ] of
err : _ -> throwError err
[] -> return ()
let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, not (isNo r) ]
noMaybes = null [ Maybe | (_, ((Maybe, _, _), _)) <- result ]
result <- if noMaybes then dropSameCandidates m result' else return result'
case result of
[(c, _, _, s)] -> [c] <$ put s
_ -> return [ c | (c, _, _, _) <- result ]
dropSameCandidates :: MetaId -> [(Candidate, Term, Type, a)] -> TCM [(Candidate, Term, Type, a)]
dropSameCandidates m cands0 = do
metas <- Set.fromList . Map.keys <$> getMetaStore
let freshMetas x = not $ Set.null $ Set.difference (Set.fromList $ allMetas x) metas
let cands =
case partition (\ (c, _, _, _) -> candidateOverlappable c) cands0 of
(cand : _, []) -> [cand]
_ -> cands0
reportSDoc "tc.instance" 50 $ vcat
[ text "valid candidates:"
, nest 2 $ vcat [ if freshMetas (v, a) then text "(redacted)" else
sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM a ]
| (_, v, a, _) <- cands ] ]
rel <- getMetaRelevance <$> lookupMeta m
case cands of
[] -> return cands
cvd@(_, v, a, _) : vas -> do
if freshMetas (v, a)
then return (cvd : vas)
else (cvd :) <$> dropWhileM equal vas
where
equal _ | isIrrelevant rel = return True
equal (_, v', a', _)
| freshMetas (v', a') = return False
| otherwise =
verboseBracket "tc.instance" 30 "checkEqualCandidates" $ do
reportSDoc "tc.instance" 30 $ sep [ prettyTCM v <+> text "==", nest 2 $ prettyTCM v' ]
localTCState $ dontAssignMetas $ ifNoConstraints_ (equalType a a' >> equalTerm a v v')
(return True)
(\ _ -> return False)
`catchError` (\ _ -> return False)
data YesNoMaybe = Yes | No | Maybe | HellNo TCErr
deriving (Show)
isNo :: YesNoMaybe -> Bool
isNo No = True
isNo _ = False
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe [Candidate])
checkCandidates m t cands = disableDestructiveUpdate $
verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
ifM (anyMetaTypes cands) (return Nothing) $
holdConstraints (\ _ -> isIFSConstraint . clValue . theConstraint) $ Just <$> do
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "candidates"
, vcat [ text "-" <+> (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":" <+> prettyTCM t
| Candidate v t _ overlap <- cands ] ]
cands' <- filterResetingState m cands (checkCandidateForMeta m t)
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "valid candidates"
, vcat [ text "-" <+> (if overlap then text "overlap" else empty) <+> prettyTCM v <+> text ":" <+> prettyTCM t
| Candidate v t _ overlap <- cands' ] ]
return cands'
where
anyMetaTypes :: [Candidate] -> TCM Bool
anyMetaTypes [] = return False
anyMetaTypes (Candidate _ a _ _ : cands) = do
a <- instantiate a
case ignoreSharing $ unEl a of
MetaV{} -> return True
_ -> anyMetaTypes cands
checkDepth :: Term -> Type -> TCM YesNoMaybe -> TCM YesNoMaybe
checkDepth c a k = locally eInstanceDepth succ $ do
d <- view eInstanceDepth
maxDepth <- maxInstanceSearchDepth
when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
k
checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta m t (Candidate term t' eti _) = checkDepth term t' $ do
mv <- lookupMeta m
setCurrentRange mv $ do
debugConstraints
verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $
liftTCM $ runCandidateCheck $ do
reportSLn "tc.instance" 70 $ " t: " ++ show t ++ "\n t':" ++ show t' ++ "\n term: " ++ show term ++ "."
reportSDoc "tc.instance" 20 $ vcat
[ text "checkCandidateForMeta"
, text "t =" <+> prettyTCM t
, text "t' =" <+> prettyTCM t'
, text "term =" <+> prettyTCM term
]
(args, t'') <- implicitArgs (1) (\h -> h /= NotHidden || eti == ExplicitToInstance) t'
reportSDoc "tc.instance" 20 $
text "instance search: checking" <+> prettyTCM t''
<+> text "<=" <+> prettyTCM t
ctxElims <- map Apply <$> getContextArgs
v <- (`applyDroppingParameters` args) =<< reduce term
reportSDoc "tc.instance" 15 $ vcat
[ text "instance search: attempting"
, nest 2 $ prettyTCM m <+> text ":=" <+> prettyTCM v
]
guardConstraint (ValueCmp CmpEq t'' (MetaV m ctxElims) v) $ leqType t'' t
debugConstraints
solveAwakeConstraints' True
verboseS "tc.instance" 15 $ do
sol <- instantiateFull (MetaV m ctxElims)
case sol of
MetaV m' _ | m == m' ->
reportSDoc "tc.instance" 15 $
sep [ text "instance search: maybe solution for" <+> prettyTCM m <> text ":"
, nest 2 $ prettyTCM v ]
_ ->
reportSDoc "tc.instance" 15 $
sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
, nest 2 $ prettyTCM sol ]
where
runCandidateCheck check =
flip catchError handle $
ifNoConstraints_ check
(return Yes)
(\ _ -> Maybe <$ reportSLn "tc.instance" 50 "assignment inconclusive")
hardFailure :: TCErr -> Bool
hardFailure (TypeError _ err) =
case clValue err of
InstanceSearchDepthExhausted{} -> True
_ -> False
hardFailure _ = False
handle :: TCErr -> TCM YesNoMaybe
handle err
| hardFailure err = return $ HellNo err
| otherwise = do
reportSDoc "tc.instance" 50 $
text "assignment failed:" <+> prettyTCM err
return No
isIFSConstraint :: Constraint -> Bool
isIFSConstraint FindInScope{} = True
isIFSConstraint UnBlock{} = True
isIFSConstraint _ = False
applyDroppingParameters :: Term -> Args -> TCM Term
applyDroppingParameters t vs = do
let fallback = return $ t `apply` vs
case ignoreSharing t of
Con c ci [] -> do
def <- theDef <$> getConInfo c
case def of
Constructor {conPars = n} -> return $ Con c ci (genericDrop n vs)
_ -> __IMPOSSIBLE__
Def f [] -> do
mp <- isProjection f
case mp of
Just Projection{projIndex = n} -> do
case drop n vs of
[] -> return t
u : us -> (`apply` us) <$> applyDef ProjPrefix f u
_ -> fallback
_ -> fallback