module Agda.TypeChecking.InstanceArguments where
import Control.Applicative
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import 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
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Rules.Term (checkArguments)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Conversion
import Agda.Utils.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
initialIFSCandidates :: TCM [(Term, Type)]
initialIFSCandidates = do
cands1 <- getContextVars
cands2 <- getScopeDefs
return $ cands1 ++ cands2
where
getContextVars :: TCM [(Term, Type)]
getContextVars = do
ctx <- getContext
let vars = [ (var i, raise (i + 1) t)
| (Dom h r (x, t), i) <- zip ctx [0..], not (unusableRelevance r)
]
env <- asks envLetBindings
env <- mapM (getOpen . snd) $ Map.toList env
let lets = [ (v,t) | (v, Dom h r t) <- env, not (unusableRelevance r) ]
return $ vars ++ lets
getScopeDefs :: TCM [(Term, Type)]
getScopeDefs = do
scopeInfo <- gets stScope
let ns = everythingInScope scopeInfo
let nsList = Map.toList $ nsNames ns
let qs = List.map anameName $ snd =<< nsList
rel <- asks envRelevance
cands <- mapM (candidate rel) qs
return $ concat cands
candidate :: Relevance -> QName -> TCM [(Term, Type)]
candidate rel q =
flip catchError handle $ do
def <- getConstInfo q
let r = defRelevance def
if not (r `moreRelevant` rel) then return [] else do
t <- defType <$> instantiateDef def
args <- freeVarsToApply q
let vs = case theDef def of
Function{ funProjection = Just (_,i) } -> genericDrop (i 1) args
_ -> args
return [(Def q vs, t)]
where
handle (TypeError _ (Closure {clValue = InternalError _})) = return []
handle err = throwError err
initializeIFSMeta :: String -> Type -> TCM Term
initializeIFSMeta s t = do
cands <- initialIFSCandidates
newIFSMeta s t cands
findInScope :: MetaId -> [(Term, Type)] -> TCM ()
findInScope m cands = whenJustM (findInScope' m cands) $ addConstraint . FindInScope m
findInScope' :: MetaId -> [(Term, Type)] -> TCM (Maybe [(Term, Type)])
findInScope' m cands = ifM (isFrozen m) (return (Just cands)) $ do
reportSDoc "tc.constr.findInScope" 15 $ text ("findInScope 2: constraint: " ++ show m ++ "; candidates left: " ++ show (length cands))
t <- getMetaTypeInContext m
reportSDoc "tc.constr.findInScope" 15 $ text "findInScope 3: t =" <+> prettyTCM t
reportSLn "tc.constr.findInScope" 70 $ "findInScope 3: t: " ++ show t
mv <- lookupMeta m
cands <- checkCandidates m t cands
reportSLn "tc.constr.findInScope" 15 $ "findInScope 4: cands left: " ++ show (length cands)
case cands of
[] -> do
reportSDoc "tc.constr.findInScope" 15 $ text "findInScope 5: not a single candidate found..."
typeError $ IFSNoCandidateInScope t
[(term, t')] -> do
reportSDoc "tc.constr.findInScope" 15 $ text (
"findInScope 5: one candidate found for type '") <+>
prettyTCM t <+> text "': '" <+> prettyTCM term <+>
text "', of type '" <+> prettyTCM t' <+> text "'."
ca <- liftTCM $ runErrorT $ checkArguments ExpandLast DontExpandInstanceArguments (getRange mv) [] t' t
case ca of
Left _ -> __IMPOSSIBLE__
Right (args, t'') -> do
leqType t'' t
ctxArgs <- getContextArgs
v <- (`applyDroppingParameters` args) =<< reduce term
assignV m ctxArgs v
reportSDoc "tc.constr.findInScope" 10 $
text "solved by instance search:" <+> prettyTCM m
<+> text ":=" <+> prettyTCM v
return Nothing
cs -> do
reportSDoc "tc.constr.findInScope" 15 $
text ("findInScope 5: more than one candidate found: ") <+>
prettyTCM (List.map fst cs)
return (Just cs)
getMetaTypeInContext :: MetaId -> TCM Type
getMetaTypeInContext m = do
mv <- lookupMeta m
let j = mvJudgement mv
tj <- getMetaType m
ctxArgs <- getContextArgs
normalise $ tj `piApply` ctxArgs
checkCandidates :: MetaId -> Type -> [(Term, Type)] -> TCM [(Term, Type)]
checkCandidates m t cands = localState $ disableDestructiveUpdate $ do
dropConstraints (isIFSConstraint . clValue . theConstraint)
filterM (uncurry $ checkCandidateForMeta m t) cands
where
checkCandidateForMeta :: MetaId -> Type -> Term -> Type -> TCM Bool
checkCandidateForMeta m t term t' =
verboseBracket "tc.constr.findInScope" 20 ("checkCandidateForMeta " ++ show m) $ do
liftTCM $ flip catchError handle $ do
reportSLn "tc.constr.findInScope" 70 $ " t: " ++ show t ++ "\n t':" ++ show t' ++ "\n term: " ++ show term ++ "."
reportSDoc "tc.constr.findInScope" 20 $ vcat
[ text "checkCandidateForMeta"
, text "t =" <+> prettyTCM t
, text "t' =" <+> prettyTCM t'
, text "term =" <+> prettyTCM term
]
localState $ do
ca <- runErrorT $ checkArguments ExpandLast DontExpandInstanceArguments noRange [] t' t
case ca of
Left _ -> return False
Right (args, t'') -> do
reportSDoc "tc.constr.findInScope" 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.constr.findInScope" 10 $
text "instance search: attempting" <+> prettyTCM m
<+> text ":=" <+> prettyTCM v
assign m ctxArgs v
solveAwakeConstraints' True
return True
where
handle err = do
reportSDoc "tc.constr.findInScope" 50 $ text "assignment failed:" <+> prettyTCM err
return False
isIFSConstraint :: Constraint -> Bool
isIFSConstraint FindInScope{} = True
isIFSConstraint UnBlock{} = True
isIFSConstraint _ = False
applyDroppingParameters :: Term -> Args -> TCM Term
applyDroppingParameters t vs =
case ignoreSharing t of
Con c [] -> do
def <- theDef <$> getConstInfo c
case def of
Constructor {conPars = n} -> return $ Con c (genericDrop n vs)
_ -> __IMPOSSIBLE__
_ -> return $ t `apply` vs
solveIrrelevantMetas :: TCM ()
solveIrrelevantMetas = mapM_ solveMetaIfIrrelevant =<< getOpenMetas
solveMetaIfIrrelevant :: MetaId -> TCM ()
solveMetaIfIrrelevant x = do
m <- lookupMeta x
when (irrelevantOrUnused (getMetaRelevance m)) $ do
reportSDoc "tc.conv.irr" 20 $ sep
[ text "instance search for solution of irrelevant meta"
, prettyTCM x, colon, prettyTCM $ jMetaType $ mvJudgement m
]
flip catchError (const $ return ()) $ do
findInScope' x =<< initialIFSCandidates
return ()