module Agda.TypeChecking.InstanceArguments where
import Control.Applicative
import Control.Monad.Error
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.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.Maybe
import Agda.Utils.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
type Candidates = [(Term, Type)]
initialIFSCandidates :: TCM Candidates
initialIFSCandidates = do
cands1 <- getContextVars
cands2 <- getScopeDefs
return $ 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 :: TCM Candidates
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 Candidates
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 v = case theDef def of
Function{ funProjection = Just p } -> Def q $ map Apply $ genericDrop (projIndex p 1) args
Constructor{} -> Con (ConHead q []) []
_ -> Def q $ map Apply args
return [(v, 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 -> Candidates -> TCM ()
findInScope m cands = whenJustM (findInScope' m cands) $ addConstraint . FindInScope m
findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
findInScope' m cands = ifM (isFrozen m) (return (Just cands)) $ do
ifM (isInstantiatedMeta m) (return Nothing) $ do
reportSDoc "tc.constr.findInScope" 15 $ text ("findInScope 2: constraint: " ++ show m ++ "; candidates left: " ++ show (length cands))
t <- normalise =<< 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 DirEq 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)
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' =
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
]
localTCState $ 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 DirEq 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
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
solveIrrelevantMetas :: TCM ()
solveIrrelevantMetas = mapM_ solveMetaIfIrrelevant =<< getOpenMetas
solveMetaIfIrrelevant :: MetaId -> TCM ()
solveMetaIfIrrelevant x = do
m <- lookupMeta x
unless (isSortMeta_ m) $ do
when (irrelevantOrUnused (getMetaRelevance m)) $ do
let t = jMetaType $ mvJudgement m
cl = miClosRange $ mvInfo m
reportSDoc "tc.conv.irr" 20 $ sep
[ text "instance search for solution of irrelevant meta"
, prettyTCM x, colon, prettyTCM $ t
]
enterClosure cl $ \ r -> do
flip catchError (const $ return ()) $ do
findInScope' x =<< initialIFSCandidates
return ()