{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Elab.Term where import Idris.AbsSyntax import Idris.AbsSyntaxTree import Idris.DSL import Idris.Delaborate import Idris.Error import Idris.ProofSearch import Idris.Output (pshow) import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs) import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.TT import Idris.Core.Evaluate import Idris.Core.Unify import Idris.Core.ProofTerm (getProofTerm) import Idris.Core.Typecheck (check, recheck, converts, isType) import Idris.Core.WHNF (whnf) import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase) import Idris.ErrReverse (errReverse) import Idris.ElabQuasiquote (extractUnquotes) import Idris.Elab.Utils import Idris.Reflection import qualified Util.Pretty as U import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.List import qualified Data.Map as M import Data.Maybe (mapMaybe, fromMaybe, catMaybes) import qualified Data.Set as S import qualified Data.Text as T import Debug.Trace data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS deriving Eq data ElabResult = ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))] -- ^ Information about new metavariables , resultCaseDecls :: [PDecl] -- ^ Deferred declarations as the meaning of case blocks , resultContext :: Context -- ^ The potentially extended context from new definitions , resultTyDecls :: [RDeclInstructions] -- ^ Meta-info about the new type declarations , resultHighlighting :: [(FC, OutputAnnotation)] } -- Using the elaborator, convert a term in raw syntax to a fully -- elaborated, typechecked term. -- -- If building a pattern match, we convert undeclared variables from -- holes to pattern bindings. -- Also find deferred names in the term and their types build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult build ist info emode opts fn tm = do elab ist info emode opts fn tm let tmIn = tm let inf = case lookupCtxt fn (idris_tyinfodata ist) of [TIPartial] -> True _ -> False hs <- get_holes ivs <- get_instances ptm <- get_term -- Resolve remaining type classes. Two passes - first to get the -- default Num instances, second to clean up the rest when (not pattern) $ mapM_ (\n -> when (n `elem` hs) $ do focus n g <- goal try (resolveTC' True False 10 g fn ist) (movelast n)) ivs ivs <- get_instances hs <- get_holes when (not pattern) $ mapM_ (\n -> when (n `elem` hs) $ do focus n g <- goal ptm <- get_term resolveTC' True True 10 g fn ist) ivs when (not pattern) $ solveAutos ist fn True tm <- get_term ctxt <- get_context probs <- get_probs u <- getUnifyLog hs <- get_holes when (not pattern) $ traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++ "Remaining problems:\n" ++ qshow probs) $ do unify_all; matchProblems True; unifyProblems probs <- get_probs case probs of [] -> return () ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ qshow probs ++ "\nin\n" ++ show tm) $ if inf then return () else lift (Error e) when tydecl (do mkPat update_term liftPats update_term orderPats) EState is _ impls highlights <- getAux tt <- get_term ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) [] log <- getLog if log /= "" then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights) else return (ElabResult tm ds (map snd is) ctxt impls highlights) where pattern = emode == ELHS tydecl = emode == ETyDecl mkPat = do hs <- get_holes tm <- get_term case hs of (h: hs) -> do patvar h; mkPat [] -> return () -- Build a term autogenerated as a typeclass method definition -- (Separate, so we don't go overboard resolving things that we don't -- know about yet on the LHS of a pattern def) buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult buildTC ist info emode opts fn tm = do -- set name supply to begin after highest index in tm let ns = allNamesIn tm let tmIn = tm let inf = case lookupCtxt fn (idris_tyinfodata ist) of [TIPartial] -> True _ -> False initNextNameFrom ns elab ist info emode opts fn tm probs <- get_probs tm <- get_term case probs of [] -> return () ((_,_,_,_,e,_,_):es) -> if inf then return () else lift (Error e) dots <- get_dotterm -- 'dots' are the PHidden things which have not been solved by -- unification when (not (null dots)) $ lift (Error (CantMatch (getInferTerm tm))) EState is _ impls highlights <- getAux tt <- get_term ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) [] log <- getLog if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights) else return (ElabResult tm ds (map snd is) ctxt impls highlights) where pattern = emode == ELHS -- return whether arguments of the given constructor name can be -- matched on. If they're polymorphic, no, unless the type has beed made -- concrete by the time we get around to elaborating the argument. getUnmatchable :: Context -> Name -> [Bool] getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon = case lookupTyExact n ctxt of Nothing -> [] Just ty -> checkArgs [] [] ty where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool] checkArgs env ns (Bind n (Pi _ t _) sc) = let env' = case t of TType _ -> n : env _ -> env in checkArgs env' (intersect env (refsIn t) : ns) (instantiate (P Bound n t) sc) checkArgs env ns t = map (not . null) (reverse ns) getUnmatchable ctxt n = [] data ElabCtxt = ElabCtxt { e_inarg :: Bool, e_isfn :: Bool, -- ^ Function part of application e_guarded :: Bool, e_intype :: Bool, e_qq :: Bool, e_nomatching :: Bool -- ^ can't pattern match } initElabCtxt = ElabCtxt False False False False False False goal_polymorphic :: ElabD Bool goal_polymorphic = do ty <- goal case ty of P _ n _ -> do env <- get_env case lookup n env of Nothing -> return False _ -> return True _ -> return False -- | Returns the set of declarations we need to add to complete the -- definition (most likely case blocks to elaborate) as well as -- declarations resulting from user tactic scripts (%runElab) elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD () elab ist info emode opts fn tm = do let loglvl = opt_logLevel (idris_options ist) when (loglvl > 5) $ unifyLog True compute -- expand type synonyms, etc let fc = maybe "(unknown)" elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote) est <- getAux sequence_ (get_delayed_elab est) end_unify ptm <- get_term when (pattern || intransform) -- convert remaining holes to pattern vars (do update_term orderPats unify_all matchProblems False -- only the ones we matched earlier unifyProblems mkPat) where pattern = emode == ELHS intransform = emode == ETransLHS bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS get_delayed_elab est = let ds = delayed_elab est in map snd $ sortBy (\(p1, _) (p2, _) -> compare p1 p2) ds tcgen = Dictionary `elem` opts reflection = Reflection `elem` opts isph arg = case getTm arg of Placeholder -> (True, priority arg) tm -> (False, priority arg) toElab ina arg = case getTm arg of Placeholder -> Nothing v -> Just (priority arg, elabE ina (elabFC info) v) toElab' ina arg = case getTm arg of Placeholder -> Nothing v -> Just (elabE ina (elabFC info) v) mkPat = do hs <- get_holes tm <- get_term case hs of (h: hs) -> do patvar h; mkPat [] -> return () -- | elabE elaborates an expression, possibly wrapping implicit coercions -- and forces/delays. If you make a recursive call in elab', it is -- normally correct to call elabE - the ones that don't are desugarings -- typically elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD () elabE ina fc' t = do solved <- get_recents as <- get_autos hs <- get_holes -- If any of the autos use variables which have recently been solved, -- have another go at solving them now. mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns && head hs /= a then solveAuto ist fn False a else return ()) as itm <- if not pattern then insertImpLam ina t else return t ct <- insertCoerce ina itm t' <- insertLazy ct g <- goal tm <- get_term ps <- get_probs hs <- get_holes --trace ("Elaborating " ++ show t' ++ " in " ++ show g -- ++ "\n" ++ show tm -- ++ "\nholes " ++ show hs -- ++ "\nproblems " ++ show ps -- ++ "\n-----------\n") $ --trace ("ELAB " ++ show t') $ let fc = fileFC "Force" env <- get_env handleError (forceErr t' env) (elab' ina fc' t') (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force")) [pimp (sUN "t") Placeholder True, pimp (sUN "a") Placeholder True, pexp ct])) forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t), ht == txt "Lazy'" = notDelay orig forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'), ht == txt "Lazy'" = notDelay orig forceErr orig env (InfiniteUnify _ t _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t), ht == txt "Lazy'" = notDelay orig forceErr orig env (Elaborating _ _ t) = forceErr orig env t forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t forceErr orig env (At _ t) = forceErr orig env t forceErr orig env t = False notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False notDelay _ = True local f = do e <- get_env return (f `elem` map fst e) -- | Is a constant a type? constType :: Const -> Bool constType (AType _) = True constType StrType = True constType VoidType = True constType _ = False -- "guarded" means immediately under a constructor, to help find patvars elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote) -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable -> PTerm -- ^ The term to elaborate -> ElabD () elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step elab' ina fc (PType fc') = do apply RType [] solve highlightSource fc' (AnnType "Type" "The type of types") elab' ina fc (PUniverse u) = do apply (RUType u) []; solve -- elab' (_,_,inty) (PConstant c) -- | constType c && pattern && not reflection && not inty -- = lift $ tfail (Msg "Typecase is not allowed") elab' ina fc tm@(PConstant fc' c) | pattern && not reflection && not (e_qq ina) && not (e_intype ina) && isTypeConst c = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm) | pattern && not reflection && not (e_qq ina) && e_nomatching ina = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm) | otherwise = do apply (RConstant c) [] solve highlightSource fc' (AnnConst c) elab' ina fc (PQuote r) = do fill r; solve elab' ina _ (PTrue fc _) = do hnf_compute g <- goal case g of TType _ -> elab' ina (Just fc) (PRef fc [] unitTy) UType _ -> elab' ina (Just fc) (PRef fc [] unitTy) _ -> elab' ina (Just fc) (PRef fc [] unitCon) elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes = do g <- goal; resolveTC' False False 5 g fn ist elab' ina fc (PResolveTC fc') = do c <- getNameFrom (sMN 0 "class") instanceArg c -- Elaborate the equality type first homogeneously, then -- heterogeneously as a fallback elab' ina _ (PApp fc (PRef _ _ n) args) | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args = try (do tyn <- getNameFrom (sMN 0 "aqty") claim tyn RType movelast tyn elab' ina (Just fc) (PApp fc (PRef fc [] eqTy) [pimp (sUN "A") (PRef NoFC [] tyn) True, pimp (sUN "B") (PRef NoFC [] tyn) False, pexp l, pexp r])) (do atyn <- getNameFrom (sMN 0 "aqty") btyn <- getNameFrom (sMN 0 "bqty") claim atyn RType movelast atyn claim btyn RType movelast btyn elab' ina (Just fc) (PApp fc (PRef fc [] eqTy) [pimp (sUN "A") (PRef NoFC [] atyn) True, pimp (sUN "B") (PRef NoFC [] btyn) False, pexp l, pexp r])) elab' ina _ (PPair fc hls _ l r) = do hnf_compute g <- goal let (tc, _) = unApply g case g of TType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairTy) [pexp l,pexp r]) UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy) [pexp l,pexp r]) _ -> case tc of P _ n _ | n == upairTy -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon) [pimp (sUN "A") Placeholder False, pimp (sUN "B") Placeholder False, pexp l, pexp r]) _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairCon) [pimp (sUN "A") Placeholder False, pimp (sUN "B") Placeholder False, pexp l, pexp r]) -- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon) -- [pimp (sUN "A") Placeholder False, -- pimp (sUN "B") Placeholder False, -- pexp l, pexp r])) -- (elab' ina (Just fc) (PApp fc (PRef fc upairCon) -- [pimp (sUN "A") Placeholder False, -- pimp (sUN "B") Placeholder False, -- pexp l, pexp r])) -- True elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r) = case t of Placeholder -> do hnf_compute g <- goal case g of TType _ -> asType _ -> asValue _ -> asType where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy) [pexp t, pexp (PLam fc n nfc Placeholder r)]) asValue = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon) [pimp (sMN 0 "a") t False, pimp (sMN 0 "P") Placeholder True, pexp l, pexp r]) elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon) [pimp (sMN 0 "a") t False, pimp (sMN 0 "P") Placeholder True, pexp l, pexp r]) elab' ina fc (PAlternative ms (ExactlyOne delayok) as) = do as_pruned <- doPrune as -- Finish the mkUniqueNames job with the pruned set, rather than -- the full set. uns <- get_usedns let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned (h : hs) <- get_holes -- trace (show (map showHd as')) $ ty <- goal case as' of [x] -> elab' ina fc x -- If there's options, try now, and if that fails, postpone -- to later. _ -> handleError isAmbiguous (tryAll (zip (map (elab' ina fc) as') (map showHd as'))) (do movelast h delayElab 5 $ do hs <- get_holes when (not (null hs)) $ do focus h as'' <- doPrune as' case as'' of [x] -> elab' ina fc x _ -> tryAll (zip (map (elab' ina fc) as'') (map showHd as''))) where showHd (PApp _ (PRef _ _ n) _) = n showHd (PRef _ _ n) = n showHd (PApp _ h _) = showHd h showHd x = NErased -- We probably should do something better than this here doPrune as = do hnf_compute ty <- goal let (tc, _) = unApply ty env <- get_env return $ pruneByType env tc ist as isAmbiguous (CantResolveAlts _) = delayok isAmbiguous (Elaborating _ _ e) = isAmbiguous e isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e isAmbiguous (At _ e) = isAmbiguous e isAmbiguous _ = False elab' ina fc (PAlternative ms FirstSuccess as_in) = do -- finish the mkUniqueNames job uns <- get_usedns let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in trySeq as where -- if none work, take the error from the first trySeq (x : xs) = let e1 = elab' ina fc x in try' e1 (trySeq' e1 xs) True trySeq [] = fail "Nothing to try in sequence" trySeq' deferr [] = proofFail deferr trySeq' deferr (x : xs) = try' (do elab' ina fc x solveAutos ist fn False) (trySeq' deferr xs) True elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do env <- get_env ty <- goal let doelab = elab' ina fc orig tryCatch doelab (\err -> if recoverableErr err then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++ -- show alts ++ "\n" ++ -- showQuick err) $ -- Prune the coercions so that only the ones -- with the right type to fix the error will be tried! case pruneAlts err alts env of [] -> lift $ tfail err alts' -> try' (elab' ina fc (PAlternative [] (ExactlyOne False) alts')) (lift $ tfail err) -- take error from original if all fail True else lift $ tfail err) where recoverableErr (CantUnify _ _ _ _ _ _) = True recoverableErr (TooManyArguments _) = False recoverableErr (CantSolveGoal _ _) = False recoverableErr (CantResolveAlts _) = False recoverableErr (NoValidAlts _) = True recoverableErr (ProofSearchFail (Msg _)) = True recoverableErr (ProofSearchFail _) = False recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e recoverableErr (At _ e) = recoverableErr e recoverableErr (ElabScriptDebug _ _ _) = False recoverableErr _ = True pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env = case unApply (normalise (tt_ctxt ist) env inc) of (P (TCon _ _) n _, _) -> filter (hasArg n env) alts (Constant _, _) -> alts _ -> filter isLend alts -- special case hack for 'Borrowed' pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env pruneAlts (At _ e) alts env = pruneAlts e alts env pruneAlts (NoValidAlts _) alts env = alts pruneAlts _ alts _ = filter isLend alts hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed' hasArg n env (PApp _ (PRef _ _ a) _) = case lookupTyExact a (tt_ctxt ist) of Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in any (fnIs n) args Nothing -> False hasArg n _ _ = False isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"] isLend _ = False fnIs n ty = case unApply ty of (P _ n' _, _) -> n == n' _ -> False showQuick (CantUnify _ (l, _) (r, _) _ _ _) = show (l, r) showQuick (ElaboratingArg _ _ _ e) = showQuick e showQuick (At _ e) = showQuick e showQuick (ProofSearchFail (Msg _)) = "search fail" showQuick _ = "No chance" elab' ina _ (PPatvar fc n) | bindfree = do patvar n update_term liftPats highlightSource fc (AnnBoundName n False) -- elab' (_, _, inty) (PRef fc f) -- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty -- = lift $ tfail (Msg "Typecase is not allowed") elab' ec _ tm@(PRef fc hl n) | pattern && not reflection && not (e_qq ec) && not (e_intype ec) && isTConName n (tt_ctxt ist) = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm) | pattern && not reflection && not (e_qq ec) && e_nomatching ec = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm) | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec) = do let ina = e_inarg ec guarded = e_guarded ec inty = e_intype ec ctxt <- get_context let defined = case lookupTy n ctxt of [] -> False _ -> True -- this is to stop us resolve type classes recursively -- trace (show (n, guarded)) $ if (tcname n && ina && not intransform) then erun fc $ do patvar n update_term liftPats highlightSource fc (AnnBoundName n False) else if (defined && not guarded) then do apply (Var n) [] annot <- findHighlight n solve highlightSource fc annot else try (do apply (Var n) [] annot <- findHighlight n solve highlightSource fc annot) (do patvar n update_term liftPats highlightSource fc (AnnBoundName n False)) where inparamBlock n = case lookupCtxtName n (inblock info) of [] -> False _ -> True bindable (NS _ _) = False bindable (UN xs) = True bindable n = implicitable n elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f []) elab' ina fc' tm@(PRef fc hls n) | pattern && not reflection && not (e_qq ina) && not (e_intype ina) && isTConName n (tt_ctxt ist) = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm) | pattern && not reflection && not (e_qq ina) && e_nomatching ina = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm) | otherwise = do fty <- get_type (Var n) -- check for implicits ctxt <- get_context env <- get_env let a' = insertScopedImps fc (normalise ctxt env fty) [] if null a' then erun fc $ do apply (Var n) [] hilite <- findHighlight n solve mapM_ (uncurry highlightSource) $ (fc, hilite) : map (\f -> (f, hilite)) hls else elab' ina fc' (PApp fc tm []) elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible" elab' ina _ (PLam fc n nfc Placeholder sc) = do -- if n is a type constructor name, this makes no sense... ctxt <- get_context when (isTConName n ctxt) $ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here") checkPiGoal n attack; intro (Just n); addPSname n -- okay for proof search -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm) elabE (ina { e_inarg = True } ) (Just fc) sc; solve highlightSource nfc (AnnBoundName n False) elab' ec _ (PLam fc n nfc ty sc) = do tyn <- getNameFrom (sMN 0 "lamty") -- if n is a type constructor name, this makes no sense... ctxt <- get_context when (isTConName n ctxt) $ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here") checkPiGoal n claim tyn RType explicit tyn attack ptm <- get_term hs <- get_holes introTy (Var tyn) (Just n) addPSname n -- okay for proof search focus tyn elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty elabE (ec { e_inarg = True }) (Just fc) sc solve highlightSource nfc (AnnBoundName n False) elab' ina fc (PPi p n nfc Placeholder sc) = do attack; arg n (is_scoped p) (sMN 0 "ty") addPSname n -- okay for proof search elabE (ina { e_inarg = True, e_intype = True }) fc sc solve highlightSource nfc (AnnBoundName n False) elab' ina fc (PPi p n nfc ty sc) = do attack; tyn <- getNameFrom (sMN 0 "ty") claim tyn RType n' <- case n of MN _ _ -> unique_hole n _ -> return n forall n' (is_scoped p) (Var tyn) addPSname n' -- okay for proof search focus tyn let ec' = ina { e_inarg = True, e_intype = True } elabE ec' fc ty elabE ec' fc sc solve highlightSource nfc (AnnBoundName n False) elab' ina _ tm@(PLet fc n nfc ty val sc) = do attack ivs <- get_instances tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) explicit valn letbind n (Var tyn) (Var valn) addPSname n case ty of Placeholder -> return () _ -> do focus tyn explicit tyn elabE (ina { e_inarg = True, e_intype = True }) (Just fc) ty focus valn elabE (ina { e_inarg = True, e_intype = True }) (Just fc) val ivs' <- get_instances env <- get_env elabE (ina { e_inarg = True }) (Just fc) sc when (not (pattern || intransform)) $ mapM_ (\n -> do focus n g <- goal hs <- get_holes if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g) then try (resolveTC' True False 10 g fn ist) (movelast n) else movelast n) (ivs' \\ ivs) -- HACK: If the name leaks into its type, it may leak out of -- scope outside, so substitute in the outer scope. expandLet n (case lookup n env of Just (Let t v) -> v other -> error ("Value not a let binding: " ++ show other)) solve highlightSource nfc (AnnBoundName n False) elab' ina _ (PGoal fc r n sc) = do rty <- goal attack tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) letbind n (Var tyn) (Var valn) focus valn elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)]) env <- get_env computeLet n elabE (ina { e_inarg = True }) (Just fc) sc solve -- elab' ina fc (PLet n Placeholder -- (PApp fc r [pexp (delab ist rty)]) sc) elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do rty <- goal ds <- get_deferred ctxt <- get_context -- make a function type a -> b -> c -> ... -> rty for the -- new function name env <- get_env argTys <- claimArgTys env args fn <- getNameFrom (sMN 0 "inf_fn") let fty = fnTy argTys rty -- trace (show (ptm, map fst argTys)) $ focus fn -- build and defer the function application attack; deferType (mkN f) fty (map fst argTys); solve -- elaborate the arguments, to unify their types. They all have to -- be explicit. mapM_ elabIArg (zip argTys args) where claimArgTys env [] = return [] claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg) = do nty <- get_type (Var n) ans <- claimArgTys env xs return ((n, (False, forget nty)) : ans) claimArgTys env (_ : xs) = do an <- getNameFrom (sMN 0 "inf_argTy") aval <- getNameFrom (sMN 0 "inf_arg") claim an RType claim aval (Var an) ans <- claimArgTys env xs return ((aval, (True, (Var an))) : ans) fnTy [] ret = forget ret fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret) localVar env (PRef _ _ x) = case lookup x env of Just _ -> Just x _ -> Nothing localVar env _ = Nothing elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (Just fc) (getTm def) elabIArg _ = return () -- already done, just a name mkN n@(NS _ _) = n mkN n@(SN _) = n mkN n = case namespace info of Just xs@(_:_) -> sNS n xs _ -> n elab' ina _ (PMatchApp fc fn) = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of [(n, args)] -> return (n, map (const True) args) _ -> lift $ tfail (NoSuchVariable fn) ns <- match_apply (Var fn') (map (\x -> (x,0)) imps) solve -- if f is local, just do a simple_app -- FIXME: Anyone feel like refactoring this mess? - EB elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in) | pattern && not reflection && not (e_qq ina) && e_nomatching ina = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm) | otherwise = implicitApp $ do env <- get_env ty <- goal fty <- get_type (Var f) ctxt <- get_context annot <- findHighlight f mapM_ checkKnownImplicit args_in let args = insertScopedImps fc (normalise ctxt env fty) args_in let unmatchableArgs = if pattern then getUnmatchable (tt_ctxt ist) f else [] -- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $ when (pattern && not reflection && not (e_qq ina) && not (e_intype ina) && isTConName f (tt_ctxt ist)) $ lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm) -- trace (show (f, args_in, args)) $ if (f `elem` map fst env && length args == 1 && length args_in == 1) then -- simple app, as below do simple_app False (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f)) (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args))) (show tm) solve mapM (uncurry highlightSource) $ (ffc, annot) : map (\f -> (f, annot)) hls return [] else do ivs <- get_instances ps <- get_probs -- HACK: we shouldn't resolve type classes if we're defining an instance -- function or default definition. let isinf = f == inferCon || tcname f -- if f is a type class, we need to know its arguments so that -- we can unify with them case lookupCtxt f (idris_classes ist) of [] -> return () _ -> do mapM_ setInjective (map getTm args) -- maybe more things are solvable now unifyProblems let guarded = isConName f ctxt -- trace ("args is " ++ show args) $ return () ns <- apply (Var f) (map isph args) -- trace ("ns is " ++ show ns) $ return () -- mark any type class arguments as injective when (not pattern) $ mapM_ checkIfInjective (map snd ns) unifyProblems -- try again with the new information, -- to help with disambiguation ulog <- getUnifyLog annot <- findHighlight f mapM (uncurry highlightSource) $ (ffc, annot) : map (\f -> (f, annot)) hls elabArgs ist (ina { e_inarg = e_inarg ina || not isinf }) [] fc False f (zip ns (unmatchableArgs ++ repeat False)) (f == sUN "Force") (map (\x -> getTm x) args) -- TODO: remove this False arg imp <- if (e_isfn ina) then do guess <- get_guess env <- get_env case safeForgetEnv (map fst env) guess of Nothing -> return [] Just rguess -> do gty <- get_type rguess let ty_n = normalise ctxt env gty return $ getReqImps ty_n else return [] -- Now we find out how many implicits we needed at the -- end of the application by looking at the goal again -- - Have another go, but this time add the -- implicits (can't think of a better way than this...) case imp of rs@(_:_) | not pattern -> return rs -- quit, try again _ -> do solve hs <- get_holes ivs' <- get_instances -- Attempt to resolve any type classes which have 'complete' types, -- i.e. no holes in them when (not pattern || (e_inarg ina && not tcgen && not (e_guarded ina))) $ mapM_ (\n -> do focus n g <- goal env <- get_env hs <- get_holes if all (\n -> not (n `elem` hs)) (freeNames g) then try (resolveTC' False False 10 g fn ist) (movelast n) else movelast n) (ivs' \\ ivs) return [] where -- Run the elaborator, which returns how many implicit -- args were needed, then run it again with those args. We need -- this because we have to elaborate the whole application to -- find out whether any computations have caused more implicits -- to be needed. implicitApp :: ElabD [ImplicitInfo] -> ElabD () implicitApp elab | pattern || intransform = do elab; return () | otherwise = do s <- get imps <- elab case imps of [] -> return () es -> do put s elab' ina topfc (PAppImpl tm es) checkKnownImplicit imp | UnknownImp `elem` argopts imp = lift $ tfail $ UnknownImplicit (pname imp) f checkKnownImplicit _ = return () getReqImps (Bind x (Pi (Just i) ty _) sc) = i : getReqImps sc getReqImps _ = [] checkIfInjective n = do env <- get_env case lookup n env of Nothing -> return () Just b -> case unApply (normalise (tt_ctxt ist) env (binderTy b)) of (P _ c _, args) -> case lookupCtxtExact c (idris_classes ist) of Nothing -> return () Just ci -> -- type class, set as injective do mapM_ setinjArg (getDets 0 (class_determiners ci) args) -- maybe we can solve more things now... ulog <- getUnifyLog probs <- get_probs traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $ unifyProblems probs <- get_probs traceWhen ulog (qshow probs) $ return () _ -> return () setinjArg (P _ n _) = setinj n setinjArg _ = return () getDets i ds [] = [] getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as | otherwise = getDets (i + 1) ds as tacTm (PTactics _) = True tacTm (PProof _) = True tacTm _ = False setInjective (PRef _ _ n) = setinj n setInjective (PApp _ (PRef _ _ n) _) = setinj n setInjective _ = return () elab' ina _ tm@(PApp fc f [arg]) = erun fc $ do simple_app (not $ headRef f) (elabE (ina { e_isfn = True }) (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg)) (show tm) solve where headRef (PRef _ _ _) = True headRef (PApp _ f _) = headRef f headRef (PAlternative _ _ as) = all headRef as headRef _ = False elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look... solve where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits appImpl (e : es) = simple_app False (appImpl es) (elab' ina fc Placeholder) (show f) elab' ina fc Placeholder = do (h : hs) <- get_holes movelast h elab' ina fc (PMetavar nfc n) = do ptm <- get_term -- When building the metavar application, leave out the unique -- names which have been used elsewhere in the term, since we -- won't be able to use them in the resulting application. let unique_used = getUniqueUsed (tt_ctxt ist) ptm let n' = metavarName (namespace info) n attack psns <- getPSnames defer unique_used n' solve highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing) elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts elab' ina fc (PTactics ts) | not pattern = do mapM_ (runTac False ist fc fn) ts | otherwise = elab' ina fc Placeholder elab' ina fc (PElabError e) = lift $ tfail e elab' ina _ (PRewrite fc r sc newg) = do attack tyn <- getNameFrom (sMN 0 "rty") claim tyn RType valn <- getNameFrom (sMN 0 "rval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "_rewrite_rule") letbind letn (Var tyn) (Var valn) focus valn elab' ina (Just fc) r compute g <- goal rewrite (Var letn) g' <- goal when (g == g') $ lift $ tfail (NoRewriting g) case newg of Nothing -> elab' ina (Just fc) sc Just t -> doEquiv t sc solve where doEquiv t sc = do attack tyn <- getNameFrom (sMN 0 "ety") claim tyn RType valn <- getNameFrom (sMN 0 "eqval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "equiv_val") letbind letn (Var tyn) (Var valn) focus tyn elab' ina (Just fc) t focus valn elab' ina (Just fc) sc elab' ina (Just fc) (PRef fc [] letn) solve elab' ina _ c@(PCase fc scr opts) = do attack tyn <- getNameFrom (sMN 0 "scty") claim tyn RType valn <- getNameFrom (sMN 0 "scval") scvn <- getNameFrom (sMN 0 "scvar") claim valn (Var tyn) letbind scvn (Var tyn) (Var valn) focus valn elabE (ina { e_inarg = True }) (Just fc) scr -- Solve any remaining implicits - we need to solve as many -- as possible before making the 'case' type unifyProblems matchProblems True args <- get_env envU <- mapM (getKind args) args let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts -- Drop the unique arguments used in the term already -- and in the scrutinee (since it's -- not valid to use them again anyway) -- -- Also drop unique arguments which don't appear explicitly -- in either case branch so they don't count as used -- unnecessarily (can only do this for unique things, since we -- assume they don't appear implicitly in types) ptm <- get_term let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts) let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr ++ inApp ptm ++ inOpts) let args' = filter (\(n, _) -> n `notElem` argsDropped) args cname <- unique_hole' True (mkCaseName fn) let cname' = mkN cname -- elab' ina fc (PMetavar cname') attack; defer argsDropped cname'; solve -- if the scrutinee is one of the 'args' in env, we should -- inspect it directly, rather than adding it as a new argument let newdef = PClauses fc [] cname' (caseBlock fc cname' scr (map (isScr scr) (reverse args')) opts) -- elaborate case updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } ) -- if we haven't got the type yet, hopefully we'll get it later! movelast tyn solve where mkCaseName (NS n ns) = NS (mkCaseName n) ns mkCaseName n = SN (CaseN n) -- mkCaseName (UN x) = UN (x ++ "_case") -- mkCaseName (MN i x) = MN i (x ++ "_case") mkN n@(NS _ _) = n mkN n = case namespace info of Just xs@(_:_) -> sNS n xs _ -> n inApp (P _ n _) = [n] inApp (App _ f a) = inApp f ++ inApp a inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc inApp (Bind n b sc) = inApp sc inApp _ = [] isUnique envk n = case lookup n envk of Just u -> u _ -> False getKind env (n, _) = case lookup n env of Nothing -> return (n, False) -- can't happen, actually... Just b -> do ty <- get_type (forget (binderTy b)) case ty of UType UniqueType -> return (n, True) UType AllTypes -> return (n, True) _ -> return (n, False) tcName tm | (P _ n _, _) <- unApply tm = case lookupCtxt n (idris_classes ist) of [_] -> True _ -> False tcName _ = False usedIn ns (n, b) = n `elem` ns || any (\x -> x `elem` ns) (allTTNames (binderTy b)) elab' ina fc (PUnifyLog t) = do unifyLog True elab' ina fc t unifyLog False elab' ina fc (PQuasiquote t goalt) = do -- First extract the unquoted subterms, replacing them with fresh -- names in the quasiquoted term. Claim their reflections to be -- an inferred type (to support polytypic quasiquotes). finalTy <- goal (t, unq) <- extractUnquotes 0 t let unquoteNames = map fst unq mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames -- Save the old state - we need a fresh proof state to avoid -- capturing lexically available variables in the quoted term. ctxt <- get_context datatypes <- get_datatypes saveState updatePS (const . newProof (sMN 0 "q") ctxt datatypes $ P Ref (reflm "TT") Erased) -- Re-add the unquotes, letting Idris infer the (fictional) -- types. Here, they represent the real type rather than the type -- of their reflection. mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy") claim ty RType movelast ty claim n (Var ty) movelast n) unquoteNames -- Determine whether there's an explicit goal type, and act accordingly -- Establish holes for the type and value of the term to be -- quasiquoted qTy <- getNameFrom (sMN 0 "qquoteTy") claim qTy RType movelast qTy qTm <- getNameFrom (sMN 0 "qquoteTm") claim qTm (Var qTy) -- Let-bind the result of elaborating the contained term, so that -- the hole doesn't disappear nTm <- getNameFrom (sMN 0 "quotedTerm") letbind nTm (Var qTy) (Var qTm) -- Fill out the goal type, if relevant case goalt of Nothing -> return () Just gTy -> do focus qTy elabE (ina { e_qq = True }) fc gTy -- Elaborate the quasiquoted term into the hole focus qTm elabE (ina { e_qq = True }) fc t end_unify -- We now have an elaborated term. Reflect it and solve the -- original goal in the original proof state, preserving highlighting env <- get_env EState _ _ _ hs <- getAux loadState updateAux (\aux -> aux { highlighting = hs }) let quoted = fmap (explicitNames . binderVal) $ lookup nTm env isRaw = case unApply (normaliseAll ctxt env finalTy) of (P _ n _, []) | n == reflm "Raw" -> True _ -> False case quoted of Just q -> do ctxt <- get_context (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q if pattern then if isRaw then reflectRawQuotePattern unquoteNames (forget q') else reflectTTQuotePattern unquoteNames q' else do if isRaw then -- we forget q' instead of using q to ensure rechecking fill $ reflectRawQuote unquoteNames (forget q') else fill $ reflectTTQuote unquoteNames q' solve Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote" -- Finally fill in the terms or patterns from the unquotes. This -- happens last so that their holes still exist while elaborating -- the main quotation. mapM_ elabUnquote unq where elabUnquote (n, tm) = do focus n elabE (ina { e_qq = False }) fc tm elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote" elab' ina fc (PQuoteName n nfc) = do ctxt <- get_context env <- get_env case lookup n env of Just _ -> do fill $ reflectName n solve highlightSource nfc (AnnBoundName n False) Nothing -> case lookupNameDef n ctxt of [(n', _)] -> do fill $ reflectName n' solve highlightSource nfc (AnnName n' Nothing Nothing Nothing) [] -> lift . tfail . NoSuchVariable $ n more -> lift . tfail . CantResolveAlts $ map fst more elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here" elab' ina fc (PHidden t) | reflection = elab' ina fc t | otherwise = do (h : hs) <- get_holes -- Dotting a hole means that either the hole or any outer -- hole (a hole outside any occurrence of it) -- must be solvable by unification as well as being filled -- in directly. -- Delay dotted things to the end, then when we elaborate them -- we can check the result against what was inferred movelast h delayElab 10 $ do focus h dotterm elab' ina fc t elab' ina fc (PRunElab fc' tm ns) = do attack n <- getNameFrom (sMN 0 "tacticScript") n' <- getNameFrom (sMN 0 "tacticExpr") let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy) claim n scriptTy movelast n letbind n' scriptTy (Var n) focus n elab' ina (Just fc') tm env <- get_env runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns solve elab' ina fc (PConstSugar constFC tm) = -- Here we elaborate the contained term, then calculate -- highlighting for constFC. The highlighting is the -- highlighting for the outermost constructor of the result of -- evaluating the elaborated term, if one exists (it always -- should, but better to fail gracefully for something silly -- like highlighting info). This is how implicit applications of -- fromInteger get highlighted. do saveState -- so we don't pollute the elaborated term n <- getNameFrom (sMN 0 "cstI") n' <- getNameFrom (sMN 0 "cstIhole") g <- forget <$> goal claim n' g movelast n' -- In order to intercept the elaborated value, we need to -- let-bind it. attack letbind n g (Var n') focus n' elab' ina fc tm env <- get_env ctxt <- get_context let v = fmap (normaliseAll ctxt env . finalise . binderVal) (lookup n env) loadState -- we have the highlighting - re-elaborate the value elab' ina fc tm case v of Just val -> highlightConst constFC val Nothing -> return () where highlightConst fc (P _ n _) = highlightSource fc (AnnName n Nothing Nothing Nothing) highlightConst fc (App _ f _) = highlightConst fc f highlightConst fc (Constant c) = highlightSource fc (AnnConst c) highlightConst _ _ = return () elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x -- delay elaboration of 't', with priority 'pri' until after everything -- else is done. -- The delayed things with lower numbered priority will be elaborated -- first. (In practice, this means delayed alternatives, then PHidden -- things.) delayElab pri t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] }) isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term)) isScr (PRef _ _ n) (n', b) = (n', (n == n', b)) isScr _ (n', b) = (n', (False, b)) caseBlock :: FC -> Name -> PTerm -- original scrutinee -> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause] caseBlock fc n scr env opts = let args' = findScr env args = map mkarg (map getNmScr args') in map (mkClause args) opts where -- Find the variable we want as the scrutinee and mark it as -- 'True'. If the scrutinee is in the environment, match on that -- otherwise match on the new argument we're adding. findScr ((n, (True, t)) : xs) = (n, (True, t)) : scrName n xs findScr [(n, (_, t))] = [(n, (True, t))] findScr (x : xs) = x : findScr xs -- [] can't happen since scrutinee is in the environment! findScr [] = error "The impossible happened - the scrutinee was not in the environment" -- To make sure top level pattern name remains in scope, put -- it at the end of the environment scrName n [] = [] scrName n [(_, t)] = [(n, t)] scrName n (x : xs) = x : scrName n xs getNmScr (n, (s, _)) = (n, s) mkarg (n, s) = (PRef fc [] n, s) -- may be shadowed names in the new pattern - so replace the -- old ones with an _ -- Also, names which don't appear on the rhs should not be -- fixed on the lhs, or this restricts the kind of matching -- we can do to non-dependent types. mkClause args (l, r) = let args' = map (shadowed (allNamesIn l)) args args'' = map (implicitable (allNamesIn r ++ keepscrName scr)) args' lhs = PApp (getFC fc l) (PRef NoFC [] n) (map (mkLHSarg l) args'') in PClause (getFC fc l) n lhs [] r [] -- Keep scrutinee available if it's just a name (this makes -- the names in scope look better when looking at a hole on -- the rhs of a case) keepscrName (PRef _ _ n) = [n] keepscrName _ = [] mkLHSarg l (tm, True) = pexp l mkLHSarg l (tm, False) = pexp tm shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s) shadowed new t = t implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s) implicitable rhs t = t getFC d (PApp fc _ _) = fc getFC d (PRef fc _ _) = fc getFC d (PAlternative _ _ (x:_)) = getFC d x getFC d x = d insertLazy :: PTerm -> ElabD PTerm insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t insertLazy (PCoerced t) = return t insertLazy t = do ty <- goal env <- get_env let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty) let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t] case tyh of P _ (UN l) _ | l == txt "Lazy'" -> return (PAlternative [] FirstSuccess tries) _ -> return t where mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs) mkDelay env t = let fc = fileFC "Delay" in addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay")) [pexp t]) -- Don't put implicit coercions around applications which are marked -- as '%noImplicit', or around case blocks, otherwise we get exponential -- blowup especially where there are errors deep in large expressions. notImplicitable (PApp _ f _) = notImplicitable f -- TMP HACK no coercing on bind (make this configurable) notImplicitable (PRef _ _ n) | [opts] <- lookupCtxt n (idris_flags ist) = NoImplicit `elem` opts notImplicitable (PAlternative _ (ExactlyOne _) as) = any notImplicitable as -- case is tricky enough without implicit coercions! If they are needed, -- they can go in the branches separately. notImplicitable (PCase _ _ _) = True notImplicitable _ = False insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs | tcinstance i = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs | otherwise = pimp n Placeholder True : insertScopedImps fc sc xs insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs) = x : insertScopedImps fc sc xs insertScopedImps _ _ xs = xs insertImpLam ina t = do ty <- goal env <- get_env let ty' = normalise (tt_ctxt ist) env ty addLam ty' t where -- just one level at a time addLam (Bind n (Pi (Just _) _ _) sc) t = do impn <- unique_hole n -- (sMN 0 "scoped_imp") if e_isfn ina -- apply to an implicit immediately then return (PApp emptyFC (PLam emptyFC impn NoFC Placeholder t) [pexp Placeholder]) else return (PLam emptyFC impn NoFC Placeholder t) addLam _ t = return t insertCoerce ina t@(PCase _ _ _) = return t insertCoerce ina t | notImplicitable t = return t insertCoerce ina t = do ty <- goal -- Check for possible coercions to get to the goal -- and add them as 'alternatives' env <- get_env let ty' = normalise (tt_ctxt ist) env ty let cs = getCoercionsTo ist ty' let t' = case (t, cs) of (PCoerced tm, _) -> tm (_, []) -> t (_, cs) -> PAlternative [] TryImplicit (t : map (mkCoerce env t) cs) return t' where mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in addImplBound ist (map fst env) (PApp fc (PRef fc [] n) [pexp (PCoerced t)]) -- | Elaborate the arguments to a function elabArgs :: IState -- ^ The current Idris state -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote) -> [Bool] -> FC -- ^ Source location -> Bool -> Name -- ^ Name of the function being applied -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable) -> Bool -- ^ under a 'force' -> [PTerm] -- ^ argument -> ElabD () elabArgs ist ina failed fc retry f [] force _ = return () elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args) = do hs <- get_holes if holeName `elem` hs then do focus holeName case t of Placeholder -> do movelast holeName elabArgs ist ina failed fc r f ns force args _ -> elabArg t else elabArgs ist ina failed fc r f ns force args where elabArg t = do -- solveAutos ist fn False now_elaborating fc f argName wrapErr f argName $ do hs <- get_holes tm <- get_term -- No coercing under an explicit Force (or it can Force/Delay -- recursively!) let elab = if force then elab' else elabE failed' <- -- trace (show (n, t, hs, tm)) $ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $ do focus holeName; g <- goal -- Can't pattern match on polymorphic goals poly <- goal_polymorphic ulog <- getUnifyLog traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $ elab (ina { e_nomatching = unm && poly }) (Just fc) t return failed done_elaborating_arg f argName elabArgs ist ina failed fc r f ns force args wrapErr f argName action = do elabState <- get while <- elaborating_app let while' = map (\(x, y, z)-> (y, z)) while (result, newState) <- case runStateT action elabState of OK (res, newState) -> return (res, newState) Error e -> do done_elaborating_arg f argName lift (tfail (elaboratingArgErr while' e)) put newState return result elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] = fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole -- For every alternative, look at the function at the head. Automatically resolve -- any nested alternatives where that function is also at the head pruneAlt :: [PTerm] -> [PTerm] pruneAlt xs = map prune xs where prune (PApp fc1 (PRef fc2 hls f) as) = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as) prune t = t choose f (PAlternative ms a as) = let as' = fmap (choose f) as fs = filter (headIs f) as' in case fs of [a] -> a _ -> PAlternative ms a as' choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as) choose f t = t headIs f (PApp _ (PRef _ _ f') _) = f == f' headIs f (PApp _ f' _) = headIs f f' headIs f _ = True -- keep if it's not an application -- Rule out alternatives that don't return the same type as the head of the goal -- (If there are none left as a result, do nothing) pruneByType :: Env -> Term -> -- head of the goal IState -> [PTerm] -> [PTerm] -- if an alternative has a locally bound name at the head, take it pruneByType env t c as | Just a <- locallyBound as = [a] where locallyBound [] = Nothing locallyBound (t:ts) | Just n <- getName t, n `elem` map fst env = Just t | otherwise = locallyBound ts getName (PRef _ _ n) = Just n getName (PApp _ f _) = getName f getName (PHidden t) = getName t getName _ = Nothing -- 'n' is the name at the head of the goal type pruneByType env (P _ n _) ist as -- if the goal type is polymorphic, keep everything | Nothing <- lookupTyExact n ctxt = as | otherwise = let asV = filter (headIs True n) as as' = filter (headIs False n) as in case as' of [] -> case asV of [] -> as _ -> asV _ -> as' where ctxt = tt_ctxt ist headIs var f (PRef _ _ f') = typeHead var f f' headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f' headIs var f (PApp _ f' _) = headIs var f f' headIs var f (PPi _ _ _ _ sc) = headIs var f sc headIs var f (PHidden t) = headIs var f t headIs var f t = True -- keep if it's not an application typeHead var f f' = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $ case lookupTyExact f' ctxt of Just ty -> case unApply (getRetTy ty) of (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f _ -> let ty' = normalise ctxt [] ty in case unApply (getRetTy ty') of (P _ ftyn _, _) -> ftyn == f (V _, _) -> -- keep, variable -- trace ("Keeping " ++ show (f', ty') -- ++ " for " ++ show n) $ isPlausible ist var env n ty _ -> False _ -> False pruneByType _ t _ as = as -- Could the name feasibly be the return type? -- If there is a type class constraint on the return type, and no instance -- in the environment or globally for that name, then no -- Otherwise, yes -- (FIXME: This isn't complete, but I'm leaving it here and coming back -- to it later - just returns 'var' for now. EB) isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool isPlausible ist var env n ty = let (hvar, classes) = collectConstraints [] [] ty in case hvar of Nothing -> True Just rth -> var -- trace (show (rth, classes)) var where collectConstraints :: [Name] -> [(Term, [Name])] -> Type -> (Maybe Name, [(Term, [Name])]) collectConstraints env tcs (Bind n (Pi _ ty _) sc) = let tcs' = case unApply ty of (P _ c _, _) -> case lookupCtxtExact c (idris_classes ist) of Just tc -> ((ty, map fst (class_instances tc)) : tcs) Nothing -> tcs _ -> tcs in collectConstraints (n : env) tcs' sc collectConstraints env tcs t | (V i, _) <- unApply t = (Just (env !! i), tcs) | otherwise = (Nothing, tcs) -- | Use the local elab context to work out the highlighting for a name findHighlight :: Name -> ElabD OutputAnnotation findHighlight n = do ctxt <- get_context env <- get_env case lookup n env of Just _ -> return $ AnnBoundName n False Nothing -> case lookupTyExact n ctxt of Just _ -> return $ AnnName n Nothing Nothing Nothing Nothing -> lift . tfail . InternalMsg $ "Can't find name" ++ show n -- Try again to solve auto implicits solveAuto :: IState -> Name -> Bool -> Name -> ElabD () solveAuto ist fn ambigok n = do hs <- get_holes tm <- get_term when (n `elem` hs) $ do focus n g <- goal isg <- is_guess -- if it's a guess, we're working on it recursively, so stop when (not isg) $ proofSearch' ist True ambigok 100 True Nothing fn [] [] solveAutos :: IState -> Name -> Bool -> ElabD () solveAutos ist fn ambigok = do autos <- get_autos mapM_ (solveAuto ist fn ambigok) (map fst autos) trivial' ist = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist trivialHoles' psn h ist = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist proofSearch' ist rec ambigok depth prv top n psns hints = do unifyProblems proofSearch rec prv ambigok (not prv) depth (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist resolveTC' di mv depth tm n ist = resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) = do ds <- get t' <- collectDeferred top casenames ctxt t when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))]) collectDeferred top casenames ctxt app where -- Evaluate the top level functions in arguments, if possible, and if it's -- not a name we're immediately going to define in a case block, so that -- any immediate specialisation of the function applied to constructors -- can be done tidyArg env (Bind n b@(Pi im t k) sc) = Bind n (Pi im (tidy ctxt env t) k) (tidyArg ((n, b) : env) sc) tidyArg env t = tidy ctxt env t tidy ctxt env t = normalise ctxt env t getFn (Bind n (Lam _) t) = getFn t getFn t | (f, a) <- unApply t = f collectDeferred top ns ctxt (Bind n b t) = do b' <- cdb b t' <- collectDeferred top ns ctxt t return (Bind n b' t') where cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v) cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v) cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b) return (b { binderTy = ty' }) collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f) (collectDeferred top ns ctxt a) collectDeferred top ns ctxt t = return t case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD () case_ ind autoSolve ist fn tm = do attack tyn <- getNameFrom (sMN 0 "ity") claim tyn RType valn <- getNameFrom (sMN 0 "ival") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "irule") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel ERHS [] (sMN 0 "tac") tm env <- get_env let (Just binding) = lookup letn env let val = binderVal binding if ind then induction (forget val) else casetac (forget val) when autoSolve solveAll -- | Compute the appropriate name for a top-level metavariable metavarName :: Maybe [String] -> Name -> Name metavarName _ n@(NS _ _) = n metavarName (Just (ns@(_:_))) n = sNS n ns metavarName _ n = n runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term runElabAction ist fc env tm ns = do tm' <- eval tm runTacTm tm' where eval tm = do ctxt <- get_context return $ normaliseAll ctxt env (finalise tm) returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased) patvars :: [Name] -> Term -> ([Name], Term) patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc) patvars ns tm = (ns, tm) pullVars :: (Term, Term) -> ([Name], Term, Term) pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs defineFunction :: RFunDefn -> ElabD () defineFunction (RDefineFun n clauses) = do ctxt <- get_context ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt let info = CaseInfo True True False -- TODO document and figure out clauses' <- forM clauses (\case RMkFunClause lhs rhs -> do (lhs', lty) <- lift $ check ctxt [] lhs (rhs', rty) <- lift $ check ctxt [] rhs lift $ converts ctxt [] lty rty return $ Right (lhs', rhs') RMkImpossibleClause lhs -> do lhs' <- fmap fst . lift $ check ctxt [] lhs return $ Left lhs') let clauses'' = map (\case Right c -> pullVars c Left lhs -> let (ns, lhs') = patvars [] lhs' in (ns, lhs', Impossible)) clauses' ctxt'<- lift $ addCasedef n (const []) info False (STerm Erased) True False -- TODO what are these? (map snd $ getArgTys ty) [] -- TODO inaccessible types clauses' clauses'' clauses'' clauses'' clauses'' ty ctxt set_context ctxt' updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e} return () checkClosed :: Raw -> Elab' aux (Term, Type) checkClosed tm = do ctxt <- get_context (val, ty) <- lift $ check ctxt [] tm return $! (finalise val, finalise ty) -- | Do a step in the reflected elaborator monad. The input is the -- step, the output is the (reflected) term returned. runTacTm :: Term -> ElabD Term runTacTm (unApply -> tac@(P _ n _, args)) | n == tacN "prim__Solve", [] <- args = do solve returnUnit | n == tacN "prim__Goal", [] <- args = do hs <- get_holes case hs of (h : _) -> do t <- goal fmap fst . checkClosed $ rawPair (Var (reflm "TTName"), Var (reflm "TT")) (reflectName h, reflect t) [] -> lift . tfail . Msg $ "Elaboration is complete. There are no goals." | n == tacN "prim__Holes", [] <- args = do hs <- get_holes fmap fst . checkClosed $ mkList (Var $ reflm "TTName") (map reflectName hs) | n == tacN "prim__Guess", [] <- args = do ok <- is_guess if ok then do guess <- fmap forget get_guess fmap fst . get_type_val $ RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"])) (Var (reflm "TT"))) guess else fmap fst . checkClosed $ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"])) (Var (reflm "TT")) | n == tacN "prim__LookupTy", [n] <- args = do n' <- reifyTTName n ctxt <- get_context let getNameTypeAndType = \case Function ty _ -> (Ref, ty) TyDecl nt ty -> (nt, ty) Operator ty _ _ -> (Ref, ty) CaseOp _ ty _ _ _ _ -> (Ref, ty) -- Idris tuples nest to the right reflectTriple (x, y, z) = raw_apply (Var pairCon) [ Var (reflm "TTName") , raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")] , x , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT") , y, z]] let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty) | (n, def) <- lookupNameDef n' ctxt , let (nt, ty) = getNameTypeAndType def ] fmap fst . checkClosed $ rawList (raw_apply (Var pairTy) [ Var (reflm "TTName") , raw_apply (Var pairTy) [ Var (reflm "NameType") , Var (reflm "TT")]]) defs | n == tacN "prim__LookupDatatype", [name] <- args = do n' <- reifyTTName name datatypes <- get_datatypes ctxt <- get_context fmap fst . checkClosed $ rawList (Var (tacN "Datatype")) (map reflectDatatype (buildDatatypes ist n')) | n == tacN "prim__SourceLocation", [] <- args = fmap fst . checkClosed $ reflectFC fc | n == tacN "prim__Namespace", [] <- args = fmap fst . checkClosed $ rawList (RConstant StrType) (map (RConstant . Str) ns) | n == tacN "prim__Env", [] <- args = do env <- get_env fmap fst . checkClosed $ reflectEnv env | n == tacN "prim__Fail", [_a, errs] <- args = do errs' <- eval errs parts <- reifyReportParts errs' lift . tfail $ ReflectionError [parts] (Msg "") | n == tacN "prim__PureElab", [_a, tm] <- args = return tm | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args = do first' <- eval first res <- eval =<< runTacTm first' next <- eval (App Complete andThen res) runTacTm next | n == tacN "prim__Try", [_a, first, alt] <- args = do first' <- eval first alt' <- eval alt try' (runTacTm first') (runTacTm alt') True | n == tacN "prim__Fill", [raw] <- args = do raw' <- reifyRaw =<< eval raw fill raw' returnUnit | n == tacN "prim__Apply" || n == tacN "prim__MatchApply" , [raw, argSpec] <- args = do raw' <- reifyRaw =<< eval raw argSpec' <- reifyList (reifyPair reifyBool reifyInt) argSpec let op = if n == tacN "prim__Apply" then apply else match_apply ns <- op raw' argSpec' fmap fst . checkClosed $ rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TTName")) [ rawPair (Var $ reflm "TTName", Var $ reflm "TTName") (reflectName n1, reflectName n2) | (n1, n2) <- ns ] | n == tacN "prim__Gensym", [hint] <- args = do hintStr <- eval hint case hintStr of Constant (Str h) -> do n <- getNameFrom (sMN 0 h) fmap fst $ get_type_val (reflectName n) _ -> fail "no hint" | n == tacN "prim__Claim", [n, ty] <- args = do n' <- reifyTTName n ty' <- reifyRaw ty claim n' ty' returnUnit | n == tacN "prim__Check", [raw] <- args = do raw' <- reifyRaw =<< eval raw ctxt <- get_context env <- get_env (tm, ty) <- lift $ check ctxt env raw' fmap fst . checkClosed $ rawPair (Var (reflm "TT"), Var (reflm "TT")) (reflect tm, reflect ty) | n == tacN "prim__Forget", [tt] <- args = do tt' <- reifyTT tt fmap fst . checkClosed . reflectRaw $ forget tt' | n == tacN "prim__Attack", [] <- args = do attack returnUnit | n == tacN "prim__Rewrite", [rule] <- args = do r <- reifyRaw rule rewrite r returnUnit | n == tacN "prim__Focus", [what] <- args = do n' <- reifyTTName what hs <- get_holes if elem n' hs then focus n' >> returnUnit else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole" | n == tacN "prim__Unfocus", [what] <- args = do n' <- reifyTTName what movelast n' returnUnit | n == tacN "prim__Intro", [mn] <- args = do n <- case fromTTMaybe mn of Nothing -> return Nothing Just name -> fmap Just $ reifyTTName name intro n returnUnit | n == tacN "prim__Forall", [n, ty] <- args = do n' <- reifyTTName n ty' <- reifyRaw ty forall n' Nothing ty' returnUnit | n == tacN "prim__PatVar", [n] <- args = do n' <- reifyTTName n patvar' n' returnUnit | n == tacN "prim__PatBind", [n] <- args = do n' <- reifyTTName n patbind n' returnUnit | n == tacN "prim__LetBind", [n, ty, tm] <- args = do n' <- reifyTTName n ty' <- reifyRaw ty tm' <- reifyRaw tm letbind n' ty' tm' returnUnit | n == tacN "prim__Compute", [] <- args = do compute ; returnUnit | n == tacN "prim__Normalise", [env, tm] <- args = do env' <- reifyEnv env tm' <- reifyTT tm ctxt <- get_context let out = normaliseAll ctxt env' (finalise tm') fmap fst . checkClosed $ reflect out | n == tacN "prim__Whnf", [tm] <- args = do tm' <- reifyTT tm ctxt <- get_context fmap fst . checkClosed . reflect $ whnf ctxt tm' | n == tacN "prim__DeclareType", [decl] <- args = do (RDeclare n args res) <- reifyTyDecl decl ctxt <- get_context let mkPi arg res = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) res rty = foldr mkPi res args (checked, ty') <- lift $ check ctxt [] rty case normaliseAll ctxt [] (finalise ty') of UType _ -> return () TType _ -> return () ty'' -> lift . tfail . InternalMsg $ show checked ++ " is not a type: it's " ++ show ty'' case lookupDefExact n ctxt of Just _ -> lift . tfail . InternalMsg $ show n ++ " is already defined." Nothing -> return () let decl = TyDecl Ref checked ctxt' = addCtxtDef n decl ctxt set_context ctxt' updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) : new_tyDecls e } aux <- getAux returnUnit | n == tacN "prim__DefineFunction", [decl] <- args = do defn <- reifyFunDefn decl defineFunction defn returnUnit | n == tacN "prim__AddInstance", [cls, inst] <- args = do className <- reifyTTName cls instName <- reifyTTName inst updateAux $ \e -> e { new_tyDecls = RAddInstance className instName : new_tyDecls e} returnUnit | n == tacN "prim__ResolveTC", [fn] <- args = do g <- goal fn <- reifyTTName fn resolveTC' False True 100 g fn ist returnUnit | n == tacN "prim__Search", [depth, hints] <- args = do d <- eval depth hints' <- eval hints case (d, unList hints') of (Constant (I i), Just hs) -> do actualHints <- mapM reifyTTName hs unifyProblems let psElab = elab ist toplevel ERHS [] (sMN 0 "tac") proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist returnUnit (Constant (I _), Nothing ) -> lift . tfail . InternalMsg $ "Not a list: " ++ show hints' (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d | n == tacN "prim__RecursiveElab", [goal, script] <- args = do goal' <- reifyRaw goal ctxt <- get_context script <- eval script (goalTT, goalTy) <- lift $ check ctxt [] goal' lift $ isType ctxt [] goalTy recH <- getNameFrom (sMN 0 "recElabHole") aux <- getAux datatypes <- get_datatypes env <- get_env (_, ES (p, aux') _ _) <- do (ES (current_p, _) _ _) <- get lift $ runElab aux (runElabAction ist fc [] script ns) ((newProof recH ctxt datatypes goalTT) { nextname = nextname current_p}) let tm_out = getProofTerm (pterm p) do (ES (prf, _) s e) <- get let p' = prf { nextname = nextname p } put (ES (p', aux') s e) env' <- get_env (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out let (tm', ty') = (reflect tm, reflect ty) fmap fst . checkClosed $ rawPair (Var $ reflm "TT", Var $ reflm "TT") (tm', ty') | n == tacN "prim__Metavar", [n] <- args = do n' <- reifyTTName n ctxt <- get_context ptm <- get_term -- See documentation above in the elab case for PMetavar let unique_used = getUniqueUsed ctxt ptm let mvn = metavarName (Just ns) n' attack defer unique_used mvn solve returnUnit | n == tacN "prim__Fixity", [op'] <- args = do opTm <- eval op' case opTm of Constant (Str op) -> let opChars = ":!#$%&*+./<=>?@\\^|-~" invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"] fixities = idris_infixes ist in if not (all (flip elem opChars) op) || elem op invalidOperators then lift . tfail . Msg $ "'" ++ op ++ "' is not a valid operator name." else case nub [f | Fix f someOp <- fixities, someOp == op] of [] -> lift . tfail . Msg $ "No fixity found for operator '" ++ op ++ "'." [f] -> fmap fst . checkClosed $ reflectFixity f many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm | n == tacN "prim__Debug", [ty, msg] <- args = do msg' <- eval msg parts <- reifyReportParts msg debugElaborator parts runTacTm x = lift . tfail $ ElabScriptStuck x -- Running tactics directly -- if a tactic adds unification problems, return an error runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD () runTac autoSolve ist perhapsFC fn tac = do env <- get_env g <- goal let tac' = fmap (addImplBound ist (map fst env)) tac if autoSolve then runT tac' else no_errors (runT tac') (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))) where runT (Intro []) = do g <- goal attack; intro (bname g) where bname (Bind n _ _) = Just n bname _ = Nothing runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs runT Intros = do g <- goal attack; intro (bname g) try' (runT Intros) (return ()) True where bname (Bind n _ _) = Just n bname _ = Nothing runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm when autoSolve solveAll runT (MatchRefine fn) = do fnimps <- case lookupCtxtName fn (idris_implicits ist) of [] -> do a <- envArgs fn return [(fn, a)] ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns) let tacs = map (\ (fn', imps) -> (match_apply (Var fn') (map (\x -> (x, 0)) imps), fn')) fnimps tryAll tacs when autoSolve solveAll where envArgs n = do e <- get_env case lookup n e of Just t -> return $ map (const False) (getArgTys (binderTy t)) _ -> return [] runT (Refine fn []) = do fnimps <- case lookupCtxtName fn (idris_implicits ist) of [] -> do a <- envArgs fn return [(fn, a)] ns -> return (map (\ (n, a) -> (n, map isImp a)) ns) let tacs = map (\ (fn', imps) -> (apply (Var fn') (map (\x -> (x, 0)) imps), fn')) fnimps tryAll tacs when autoSolve solveAll where isImp (PImp _ _ _ _ _) = True isImp _ = False envArgs n = do e <- get_env case lookup n e of Just t -> return $ map (const False) (getArgTys (binderTy t)) _ -> return [] runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps) when autoSolve solveAll runT DoUnify = do unify_all when autoSolve solveAll runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal") claim tmHole RType claim n (Var tmHole) focus tmHole elab ist toplevel ERHS [] (sMN 0 "tac") tm focus n runT (Equiv tm) -- let bind tm, then = do attack tyn <- getNameFrom (sMN 0 "ety") claim tyn RType valn <- getNameFrom (sMN 0 "eqval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "equiv_val") letbind letn (Var tyn) (Var valn) focus tyn elab ist toplevel ERHS [] (sMN 0 "tac") tm focus valn when autoSolve solveAll runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that = do attack; -- (h:_) <- get_holes tyn <- getNameFrom (sMN 0 "rty") -- start_unify h claim tyn RType valn <- getNameFrom (sMN 0 "rval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "rewrite_rule") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel ERHS [] (sMN 0 "tac") tm rewrite (Var letn) when autoSolve solveAll runT (Induction tm) -- let bind tm, similar to the others = case_ True autoSolve ist fn tm runT (CaseTac tm) = case_ False autoSolve ist fn tm runT (LetTac n tm) = do attack tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) letn <- unique_hole n letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel ERHS [] (sMN 0 "tac") tm when autoSolve solveAll runT (LetTacTy n ty tm) = do attack tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) letn <- unique_hole n letbind letn (Var tyn) (Var valn) focus tyn elab ist toplevel ERHS [] (sMN 0 "tac") ty focus valn elab ist toplevel ERHS [] (sMN 0 "tac") tm when autoSolve solveAll runT Compute = compute runT Trivial = do trivial' ist; when autoSolve solveAll runT TCInstance = runT (Exact (PResolveTC emptyFC)) runT (ProofSearch rec prover depth top psns hints) = do proofSearch' ist rec False depth prover top fn psns hints when autoSolve solveAll runT (Focus n) = focus n runT Unfocus = do hs <- get_holes case hs of [] -> return () (h : _) -> movelast h runT Solve = solve runT (Try l r) = do try' (runT l) (runT r) True runT (TSeq l r) = do runT l; runT r runT (ApplyTactic tm) = do tenv <- get_env -- store the environment tgoal <- goal -- store the goal attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ... script <- getNameFrom (sMN 0 "script") claim script scriptTy scriptvar <- getNameFrom (sMN 0 "scriptvar" ) letbind scriptvar scriptTy (Var script) focus script elab ist toplevel ERHS [] (sMN 0 "tac") tm (script', _) <- get_type_val (Var scriptvar) -- now that we have the script apply -- it to the reflected goal and context restac <- getNameFrom (sMN 0 "restac") claim restac tacticTy focus restac fill (raw_apply (forget script') [reflectEnv tenv, reflect tgoal]) restac' <- get_guess solve -- normalise the result in order to -- reify it ctxt <- get_context env <- get_env let tactic = normalise ctxt env restac' runReflected tactic where tacticTy = Var (reflm "Tactic") listTy = Var (sNS (sUN "List") ["List", "Prelude"]) scriptTy = (RBind (sMN 0 "__pi_arg") (Pi Nothing (RApp listTy envTupleType) RType) (RBind (sMN 1 "__pi_arg") (Pi Nothing (Var $ reflm "TT") RType) tacticTy)) runT (ByReflection tm) -- run the reflection function 'tm' on the -- goal, then apply the resulting reflected Tactic = do tgoal <- goal attack script <- getNameFrom (sMN 0 "script") claim script scriptTy scriptvar <- getNameFrom (sMN 0 "scriptvar" ) letbind scriptvar scriptTy (Var script) focus script ptm <- get_term elab ist toplevel ERHS [] (sMN 0 "tac") (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)]) (script', _) <- get_type_val (Var scriptvar) -- now that we have the script apply -- it to the reflected goal restac <- getNameFrom (sMN 0 "restac") claim restac tacticTy focus restac fill (forget script') restac' <- get_guess solve -- normalise the result in order to -- reify it ctxt <- get_context env <- get_env let tactic = normalise ctxt env restac' runReflected tactic where tacticTy = Var (reflm "Tactic") scriptTy = tacticTy runT (Reflect v) = do attack -- let x = reflect v in ... tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "letvar") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel ERHS [] (sMN 0 "tac") v (value, _) <- get_type_val (Var letn) ctxt <- get_context env <- get_env let value' = hnf ctxt env value runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value')) runT (Fill v) = do attack -- let x = fill x in ... tyn <- getNameFrom (sMN 0 "letty") claim tyn RType valn <- getNameFrom (sMN 0 "letval") claim valn (Var tyn) letn <- getNameFrom (sMN 0 "letvar") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel ERHS [] (sMN 0 "tac") v (value, _) <- get_type_val (Var letn) ctxt <- get_context env <- get_env let value' = normalise ctxt env value rawValue <- reifyRaw value' runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue) runT (GoalType n tac) = do g <- goal case unApply g of (P _ n' _, _) -> if nsroot n' == sUN n then runT tac else fail "Wrong goal type" _ -> fail "Wrong goal type" runT ProofState = do g <- goal return () runT Skip = return () runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "") runT SourceFC = case perhapsFC of Nothing -> lift . tfail $ Msg "There is no source location available." Just fc -> do fill $ reflectFC fc solve runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover" runT x = fail $ "Not implemented " ++ show x runReflected t = do t' <- reify ist t runTac autoSolve ist perhapsFC fn t' elaboratingArgErr :: [(Name, Name)] -> Err -> Err elaboratingArgErr [] err = err elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err) where rewrite (ElaboratingArg _ _ _ _) = Nothing rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e) rewrite (At fc e) = fmap (At fc) (rewrite e) rewrite err = Just (ElaboratingArg f x during err) withErrorReflection :: Idris a -> Idris a withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror) where handle :: Err -> Idris Err handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result" return e -- Don't do meta-reflection of errors handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure" return e -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them handle e@(At fc err) = do logLvl 3 "Reflecting body of At" err' <- handle err return (At fc err') handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating" err' <- handle err return (Elaborating what n err') handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg" hs <- getFnHandlers f a err' <- if null hs then handle err else applyHandlers err hs return (ElaboratingArg f a prev err') -- ProofSearchFail is an internal detail - so don't expose it handle (ProofSearchFail e) = handle e -- TODO: argument-specific error handlers go here for ElaboratingArg handle e = do ist <- getIState logLvl 2 "Starting error reflection" let handlers = idris_errorhandlers ist applyHandlers e handlers getFnHandlers :: Name -> Name -> Idris [Name] getFnHandlers f arg = do ist <- getIState let funHandlers = maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers $ ist return . maybe [] S.toList . M.lookup arg $ funHandlers applyHandlers e handlers = do ist <- getIState let err = fmap (errReverse ist) e logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers)) let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers -- Typecheck error handlers - if this fails, then something else was wrong earlier! handlers <- case mapM (check (tt_ctxt ist) []) reports of Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e OK hs -> return hs -- Normalize error handler terms to produce the new messages ctxt <- getContext let results = map (normalise ctxt []) (map fst handlers) logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results)) -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results) errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of Left err -> ierror err Right ok -> return ok return $ case errorparts of [] -> e parts -> ReflectionError errorparts e solveAll = try (do solve; solveAll) (return ()) -- | Do the left-over work after creating declarations in reflected -- elaborator scripts processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris () processTacticDecls info steps = -- The order of steps is important: type declarations might -- establish metavars that later function bodies resolve. forM_ (reverse steps) $ \case RTyDeclInstrs n fc impls ty -> do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty logLvl 3 $ " It has impls " ++ show impls updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) } addIBC (IBCImp n) ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))] addIBC (IBCDef n) ctxt <- getContext case lookupDef n ctxt of (TyDecl _ _ : _) -> -- If the function isn't defined at the end of the elab script, -- then it must be added as a metavariable. This needs guarding -- to prevent overwriting case defs with a metavar, if the case -- defs come after the type decl in the same script! let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds in addDeferred ds' _ -> return () RAddInstance className instName -> do -- The type class resolution machinery relies on a special logLvl 2 $ "Adding elab script instance " ++ show instName ++ " for " ++ show className addInstance False True className instName addIBC (IBCInstance False True className instName) RClausesInstrs n cs -> do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n solveDeferred n let lhss = map (\(_, lhs, _) -> lhs) cs let fc = fileFC "elab_reflected" pmissing <- do ist <- getIState possible <- genClauses fc n lhss (map (\lhs -> delab' ist lhs True True) lhss) missing <- filterM (checkPossible n) possible return (filter (noMatch ist lhss) missing) let tot = if null pmissing then Unchecked -- still need to check recursive calls else Partial NotCovering -- missing cases implies not total setTotality n tot updateIState $ \i -> i { idris_patdefs = addDef n (cs, pmissing) $ idris_patdefs i } addIBC (IBCDef n) ctxt <- getContext case lookupDefExact n ctxt of Just (CaseOp _ _ _ _ _ cd) -> -- Here, we populate the call graph with a list of things -- we refer to, so that if they aren't total, the whole -- thing won't be. let (scargs, sc) = cases_compiletime cd (scargs', sc') = cases_runtime cd calls = findCalls sc' scargs used = findUsedArgs sc' scargs' cg = CGInfo scargs' calls [] used [] in do logLvl 2 $ "Called names in reflected elab: " ++ show cg addToCG n cg addToCalledG n (nub (map fst calls)) addIBC $ IBCCG n Just _ -> return () -- TODO throw internal error Nothing -> return () -- checkDeclTotality requires that the call graph be present -- before calling it. -- TODO: reduce code duplication with Idris.Elab.Clause buildSCG (fc, n) -- Actually run the totality checker. In the main clause -- elaborator, this is deferred until after. Here, we run it -- now to get totality information as early as possible. tot' <- checkDeclTotality (fc, n) setTotality n tot' when (tot' /= Unchecked) $ addIBC (IBCTotal n tot') where -- TODO: see if the code duplication with Idris.Elab.Clause can be -- reduced or eliminated. checkPossible :: Name -> PTerm -> Idris Bool checkPossible fname lhs_in = do ctxt <- getContext ist <- getIState let lhs = addImplPat ist lhs_in let fc = fileFC "elab_reflected_totality" let tcgen = False -- TODO: later we may support dictionary generation case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of OK (ElabResult lhs' _ _ _ _ _, _) -> do -- not recursively calling here, because we don't -- want to run infinitely many times let lhs_tm = orderPats (getInferTerm lhs') case recheck ctxt [] (forget lhs_tm) lhs_tm of OK _ -> return True err -> return False -- if it's a recoverable error, the case may become possible Error err -> if tcgen then return (recoverableCoverage ctxt err) else return (validCoverageCase ctxt err || recoverableCoverage ctxt err) -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of Right _ -> False Left _ -> True) cs