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 qualified 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
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 -> Just <$> getContextVars
OutputTypeName n -> Just <$> do (++) <$> getContextVars <*> getScopeDefs n
where
getContextVars :: TCM [Candidate]
getContextVars = do
ctx <- getContext
reportSDoc "tc.instance.cands" 40 $ hang (text "Getting candidates from context") 2 (inTopContext $ prettyTCM ctx)
let varsAndRaisedTypes = [ (var i, raise (i + 1) t) | (i, t) <- zip [0..] ctx ]
vars = [ Candidate x t ExplicitStayExplicit (isOverlappable info)
| (x, Dom info (_, t)) <- varsAndRaisedTypes
, isInstance info
, not (unusableRelevance $ argInfoRelevance info)
]
let cxtAndTypes = [ (x, t) | (x, Dom _ (_, t)) <- varsAndRaisedTypes ]
fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
reportSDoc "tc.instance.fields" 30 $
if null fields then text "no instance field candidates" else
text "instance field candidates" $$ do
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
, isInstance info
, 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 `List.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 (isOverlappable arg)
| isInstance arg ] ++) <$>
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 = ifNotM (isNameInScope q <$> getScope) (return Nothing) $ do
flip catchError handle $ do
def <- getConstInfo q
if not (defRelevance def `moreRelevant` rel) then return Nothing else do
args <- freeVarsToApply q
let t = defType def `piApply` args
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
return $ Just $ Candidate v t ExplicitToInstance False
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 <- instantiate =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInScope 1: t: " ++ prettyShow t
TelV tel t <- telView t
cands <- addContext' tel $ initialIFSCandidates t
case cands of
Nothing -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
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) (do
reportSLn "tc.instance" 20 "Refusing to solve frozen instance meta."
return (Just (cands, Nothing))) $ do
ifM (isFullyInstantiatedMeta m) (Nothing <$ reportSLn "tc.instance" 20 "Instance meta already solved.") $ 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 ]
reportSDoc "tc.instance" 70 $ text "raw" $$ do
nest 2 $ vcat
[ sep [ (if overlap then text "overlap" else empty) <+> pretty v <+> text ":"
, nest 2 $ pretty t ] | Candidate v t _ overlap <- cands ]
t <- normalise =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInScope 2: t: " ++ prettyShow t
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ prettyShow t
let abortNonRigid m = do
reportSLn "tc.instance" 15 $
"aborting due to non-rigidly constrained meta " ++ show m
return $ Just (cands, Just m)
ifJustM (areThereNonRigidMetaArguments (unEl t)) abortNonRigid $ 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 (absBody 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
mlvl <- getBuiltinDefName builtinLevel
(msz, mszlt) <- getBuiltinSize
let ok = catMaybes [ mlvl, msz ]
o <- getOutputTypeName . jMetaType . mvJudgement =<< lookupMeta i
case o of
OutputTypeName l | elem l ok -> 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 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
metas <- Set.fromList . Map.keys <$> getMetaStore
let freshMetas x = not $ Set.null $ Set.difference (Set.fromList $ allMetas x) metas
let cands =
case List.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 : _ | isIrrelevant rel -> do
reportSLn "tc.instance" 30 "Meta is irrelevant so any candidate will do."
return [cvd]
cvd@(_, v, a, _) : vas -> do
if freshMetas (v, a)
then return (cvd : vas)
else (cvd :) <$> dropWhileM equal vas
where
equal (_, v', a', _)
| freshMetas (v', a') = return False
| otherwise =
verboseBracket "tc.instance" 30 "comparingCandidates" $ 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: " ++ prettyShow t ++ "\n t':" ++ prettyShow t' ++ "\n term: " ++ prettyShow 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 -> notVisible h || eti == ExplicitToInstance) t'
reportSDoc "tc.instance" 20 $
text "instance search: checking" <+> prettyTCM t''
<+> text "<=" <+> prettyTCM t
reportSDoc "tc.instance" 70 $ vcat
[ text "instance search: checking (raw)"
, nest 4 $ pretty t''
, nest 2 $ text "<="
, nest 4 $ pretty t
]
v <- (`applyDroppingParameters` args) =<< reduce term
reportSDoc "tc.instance" 15 $ vcat
[ text "instance search: attempting"
, nest 2 $ prettyTCM m <+> text ":=" <+> prettyTCM v
]
reportSDoc "tc.instance" 70 $ nest 2 $
text "candidate v = " <+> pretty v
ctxElims <- map Apply <$> getContextArgs
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 (drop 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