#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 Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Errors ()
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Rules.Term (checkArguments)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Conversion
import Agda.Utils.Except ( MonadError(catchError, throwError), runExceptT )
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
#include "undefined.h"
import Agda.Utils.Impossible
type Candidate = (Term, Type)
type Candidates = [Candidate]
initialIFSCandidates :: Type -> TCM (Maybe Candidates)
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
OutputTypeName n -> do
cands2 <- getScopeDefs n
return $ Just $ cands1 ++ cands2
where
getContextVars :: TCM Candidates
getContextVars = do
ctx <- getContext
let vars = [ (var i, raise (i + 1) t)
| (Dom info (x, t), i) <- zip ctx [0..]
, not (unusableRelevance $ argInfoRelevance info)
]
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ (v,t)
| (v, Dom info t) <- env
, not (unusableRelevance $ argInfoRelevance info)
]
return $ vars ++ lets
getScopeDefs :: QName -> TCM Candidates
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
return $ Just (v, t)
where
handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
initializeIFSMeta :: String -> Type -> TCM Term
initializeIFSMeta s t = do
t <- reduce t
cands <- initialIFSCandidates t
newIFSMeta s t cands
findInScope :: MetaId -> Maybe Candidates -> 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
Just {} -> findInScope m cands
findInScope m (Just cands) = whenJustM (findInScope' m cands) $ addConstraint . FindInScope m . Just
findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
findInScope' m cands = ifM (isFrozen m) (return (Just cands)) $ 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)
t <- normalise =<< getMetaTypeInContext m
reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ show t
isRec <- orM $ map (isRecursive . unEl . snd) cands
let shouldFreeze rigid m
| elem m rigid = return False
| otherwise = not <$> isFrozen m
metas <- if not isRec then return [] else do
rigid <- rigidlyConstrainedMetas
filterM (shouldFreeze rigid) (allMetas t)
forM_ metas $ \ m -> updateMetaVar m $ \ mv -> mv { mvFrozen = Frozen }
cands <- checkCandidates m t cands
reportSLn "tc.instance" 15 $
"findInScope 4: cands left: " ++ show (length cands)
unfreezeMeta metas
case cands of
[] -> do
reportSDoc "tc.instance" 15 $
text "findInScope 5: not a single candidate found..."
typeError $ IFSNoCandidateInScope t
[(term, t')] -> do
reportSDoc "tc.instance" 15 $ vcat
[ text "findInScope 5: found one candidate"
, nest 2 $ prettyTCM term
, text "of type " <+> prettyTCM t'
, text "for type" <+> prettyTCM t
]
(args, t'') <- implicitArgs (1) notVisible t'
leqType t'' t
ctxArgs <- getContextArgs
v <- (`applyDroppingParameters` args) =<< reduce term
assignV DirEq m ctxArgs v
reportSDoc "tc.instance" 10 $ vcat
[ text "solved by instance search:"
, prettyTCM m <+> text ":=" <+> prettyTCM v
]
return Nothing
cs -> do
reportSDoc "tc.instance" 15 $
text ("findInScope 5: more than one candidate found: ") <+>
prettyTCM (List.map fst cs)
return (Just cs)
where
isRecursive :: Term -> TCM Bool
isRecursive v = do
v <- reduce v
case ignoreSharing v of
Pi (Dom info _) t ->
if getHiding info == Instance then return True else
isRecursive $ unEl $ unAbs t
_ -> return False
rigidlyConstrainedMetas :: TCM [MetaId]
rigidlyConstrainedMetas = do
cs <- (++) <$> use stSleepingConstraints <*> use stAwakeConstraints
catMaybes <$> mapM rigidMetas cs
where
isRigid v =
case v of
Def f _ -> return True
Con{} -> return True
Lit{} -> return True
Var{} -> return True
_ -> return False
rigidMetas c =
case clValue $ theConstraint c of
ValueCmp _ _ u v ->
case (u, v) of
(MetaV m _, _) -> ifM (isRigid v) (return $ Just m) (return Nothing)
(_, MetaV m _) -> 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
checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates
checkCandidates m t cands = localTCState $ disableDestructiveUpdate $ do
dropConstraints (isIFSConstraint . clValue . theConstraint)
cands <- filterM (uncurry $ checkCandidateForMeta m t) cands
dropSameCandidates cands
where
checkCandidateForMeta :: MetaId -> Type -> Term -> Type -> TCM Bool
checkCandidateForMeta m t term t' = do
mv <- lookupMeta m
setCurrentRange mv $ do
verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do
liftTCM $ flip catchError handle $ 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
]
localTCState $ do
(args, t'') <- implicitArgs (1) notVisible t'
reportSDoc "tc.instance" 20 $
text "instance search: checking" <+> prettyTCM t''
<+> text "<=" <+> prettyTCM t
flip (ifNoConstraints_ $ leqType t'' t) (const $ return True) $ do
ctxArgs <- getContextArgs
v <- (`applyDroppingParameters` args) =<< reduce term
reportSDoc "tc.instance" 15 $ vcat
[ text "instance search: attempting"
, nest 2 $ prettyTCM m <+> text ":=" <+> prettyTCM v
]
assign DirEq m ctxArgs v
solveAwakeConstraints' True
return True
where
handle :: TCErr -> TCM Bool
handle err = do
reportSDoc "tc.instance" 50 $
text "assignment failed:" <+> prettyTCM err
return False
isIFSConstraint :: Constraint -> Bool
isIFSConstraint FindInScope{} = True
isIFSConstraint UnBlock{} = True
isIFSConstraint _ = False
dropSameCandidates :: Candidates -> TCM Candidates
dropSameCandidates cands = do
case cands of
[] -> return cands
c@(v,a) : vas -> (c:) <$> dropWhileM equal vas
where
equal (v',a') = dontAssignMetas $ ifNoConstraints_ (equalType a a' >> equalTerm a v v')
(return True)
(\ _ -> return False)
`catchError` (\ _ -> return 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