#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.InstanceArguments where
import Control.Applicative
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.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)
#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
| (Dom info (x, t), i) <- zip ctx [0..]
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ Candidate v t ExplicitStayExplicit
| (v, Dom info t) <- env
, getHiding info == Instance
, not (unusableRelevance $ argInfoRelevance info)
]
return $ vars ++ lets
getScopeDefs :: QName -> TCM [Candidate]
getScopeDefs n = do
instanceDefs <- getInstanceDefs
rel <- asks envRelevance
let qs = fromMaybe [] $ 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 } -> projDropPars p `apply` args
Constructor{ conSrcCon = c } -> Con c []
_ -> Def q $ map Apply args
inScope <- isNameInScope q <$> getScope
return $ Candidate v t ExplicitToInstance <$ 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 (isInstantiatedMeta 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" 70 $ nest 2 $ vcat
[ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM t ] | Candidate v t _ <- 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 -> 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 _ btel) = 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
let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, r /= No ]
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 cands = do
metas <- Set.fromList . Map.keys <$> getMetaStore
let freshMetas x = not $ Set.null $ Set.difference (Set.fromList $ allMetas x) metas
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
deriving (Show, Eq)
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 "-" <+> prettyTCM v <+> text ":" <+> prettyTCM t | Candidate v t _ <- cands ] ]
cands' <- filterResetingState m cands (checkCandidateForMeta m t)
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ text "valid candidates"
, vcat [ text "-" <+> prettyTCM v <+> text ":" <+> prettyTCM t | Candidate v t _ <- 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
checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
checkCandidateForMeta m t (Candidate term t' eti) = 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")
handle :: TCErr -> TCM YesNoMaybe
handle err = 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 [] -> do
def <- theDef <$> getConInfo c
case def of
Constructor {conPars = n} -> return $ Con c (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 f u
_ -> fallback
_ -> fallback