{-# LANGUAGE PatternGuards #-} module Idris.ElabTerm where import Idris.AbsSyntax import Idris.DSL import Idris.Delaborate import Idris.Error import Idris.ProofSearch import Idris.Output (pshow) import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.TT import Idris.Core.Evaluate import Idris.Core.Unify import Idris.Core.Typecheck (check) import Idris.ErrReverse (errReverse) 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) import qualified Data.Set as S import qualified Data.Text as T import Debug.Trace -- Data to pass to recursively called elaborators; e.g. for where blocks, -- paramaterised declarations, etc. data ElabInfo = EInfo { params :: [(Name, PTerm)], inblock :: Ctxt [Name], -- names in the block, and their params liftname :: Name -> Name, namespace :: Maybe [String] } toplevel = EInfo [] emptyContext id Nothing -- 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 -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl]) build ist info pattern opts fn tm = do elab ist info pattern opts fn tm let tmIn = tm let inf = case lookupCtxt fn (idris_tyinfodata ist) of [TIPartial] -> True _ -> False ivs <- get_instances hs <- get_holes 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 7 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 resolveTC 7 g fn ist) ivs tm <- get_term ctxt <- get_context probs <- get_probs u <- getUnifyLog when (not pattern) $ traceWhen u ("Remaining problems:\n" ++ show probs) $ do matchProblems True; unifyProblems probs <- get_probs case probs of [] -> return () ((_,_,_,e,_,_):es) -> if inf then return () else lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred (Just fn) tt) [] log <- getLog if (log /= "") then trace log $ return (tm, ds, is) else return (tm, ds, is) -- 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 -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl]) buildTC ist info pattern 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 pattern opts fn tm probs <- get_probs tm <- get_term case probs of [] -> return () ((_,_,_,e,_,_):es) -> if inf then return () else lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred (Just fn) tt) [] log <- getLog if (log /= "") then trace log $ return (tm, ds, is) else return (tm, ds, is) -- Returns the set of declarations we need to add to complete the definition -- (most likely case blocks to elaborate) elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD () elab ist info pattern opts fn tm = do let loglvl = opt_logLevel (idris_options ist) when (loglvl > 5) $ unifyLog True compute -- expand type synonyms, etc elabE (False, False, False) tm -- (in argument, guarded, in type) end_unify when pattern -- convert remaining holes to pattern vars (do update_term orderPats matchProblems False -- only the ones we matched earlier unifyProblems mkPat) where tcgen = Dictionary `elem` opts reflect = Reflection `elem` opts isph arg = case getTm arg of Placeholder -> (True, priority arg) _ -> (False, priority arg) toElab ina arg = case getTm arg of Placeholder -> Nothing v -> Just (priority arg, elabE ina v) toElab' ina arg = case getTm arg of Placeholder -> Nothing v -> Just (elabE ina v) mkPat = do hs <- get_holes tm <- get_term case hs of (h: hs) -> do patvar h; mkPat [] -> return () elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD () elabE ina t = --do g <- goal --trace ("Elaborating " ++ show t ++ " : " ++ show g) $ do ct <- insertCoerce ina t 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 env) (elab' ina t') (elab' ina (PApp fc (PRef fc (sUN "Force")) [pimp (sUN "t") Placeholder True, pimp (sUN "a") Placeholder True, pexp ct])) True forceErr env (CantUnify _ t t' _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t), ht == txt "Lazy'" = True forceErr env (CantUnify _ t t' _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'), ht == txt "Lazy'" = True forceErr env (InfiniteUnify _ t _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t), ht == txt "Lazy'" = True forceErr env (Elaborating _ _ t) = forceErr env t forceErr env (ElaboratingArg _ _ _ t) = forceErr env t forceErr env (At _ t) = forceErr env t forceErr env t = False 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 PtrType = True constType VoidType = True constType _ = False elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type) -> PTerm -- ^ The term to elaborate -> ElabD () elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step elab' ina PType = do apply RType []; solve -- elab' (_,_,inty) (PConstant c) -- | constType c && pattern && not reflect && not inty -- = lift $ tfail (Msg "Typecase is not allowed") elab' ina (PConstant c) = do apply (RConstant c) []; solve elab' ina (PQuote r) = do fill r; solve elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon)) (elab' ina (PRef fc unitTy)) elab' ina (PFalse fc) = elab' ina (PRef fc falseTy) elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes = do g <- goal; resolveTC 5 g fn ist elab' ina (PResolveTC fc) | True = do c <- getNameFrom (sMN 0 "class") instanceArg c | otherwise = do g <- goal try (resolveTC 2 g fn ist) (do c <- getNameFrom (sMN 0 "class") instanceArg c) elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True, pimp (sMN 0 "x") t False]) elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (sMN 0 "A") Placeholder True, pimp (sMN 0 "B") Placeholder False, pexp l, pexp r]) elab' ina@(_, a, inty) (PPair fc _ l r) = do hnf_compute g <- goal case g of TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy) [pexp l,pexp r]) _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon) [pimp (sMN 0 "A") Placeholder True, pimp (sMN 0 "B") Placeholder True, pexp l, pexp r]) elab' ina (PDPair fc p l@(PRef _ n) t r) = case t of Placeholder -> do hnf_compute g <- goal case g of TType _ -> asType _ -> asValue _ -> asType where asType = elab' ina (PApp fc (PRef fc sigmaTy) [pexp t, pexp (PLam n Placeholder r)]) asValue = elab' ina (PApp fc (PRef fc existsCon) [pimp (sMN 0 "a") t False, pimp (sMN 0 "P") Placeholder True, pexp l, pexp r]) elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon) [pimp (sMN 0 "a") t False, pimp (sMN 0 "P") Placeholder True, pexp l, pexp r]) elab' ina (PAlternative True as) = do hnf_compute ty <- goal ctxt <- get_context let (tc, _) = unApply ty let as' = pruneByType tc ctxt as -- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $ tryAll (zip (map (elab' ina) as') (map showHd as')) where showHd (PApp _ (PRef _ n) _) = show n showHd (PRef _ n) = show n showHd (PApp _ h _) = show h showHd x = show x elab' ina (PAlternative False as) = trySeq as where -- if none work, take the error from the first trySeq (x : xs) = let e1 = elab' ina x in try' e1 (trySeq' e1 xs) True trySeq' deferr [] = proofFail deferr trySeq' deferr (x : xs) = try' (elab' ina x) (trySeq' deferr xs) True elab' ina (PPatvar fc n) | pattern = patvar n -- elab' (_, _, inty) (PRef fc f) -- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty -- = lift $ tfail (Msg "Typecase is not allowed") elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n) = do 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) then erun fc $ patvar n else if (defined && not guarded) then do apply (Var n) []; solve else try (do apply (Var n) []; solve) (patvar n) where inparamBlock n = case lookupCtxtName n (inblock info) of [] -> False _ -> True elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f []) elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve elab' ina@(_, a, inty) (PLam n 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); -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm) elabE (True, a, inty) sc; solve elab' ina@(_, a, inty) (PLam n 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) focus tyn elabE (True, a, True) ty elabE (True, a, inty) sc solve elab' ina@(_, a, _) (PPi _ n Placeholder sc) = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve elab' ina@(_, a, _) (PPi _ n ty sc) = do attack; tyn <- getNameFrom (sMN 0 "ty") claim tyn RType n' <- case n of MN _ _ -> unique_hole n _ -> return n forall n' (Var tyn) focus tyn elabE (True, a, True) ty elabE (True, a, True) sc solve elab' ina@(_, a, inty) (PLet n ty val sc) = do attack; 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) case ty of Placeholder -> return () _ -> do focus tyn explicit tyn elabE (True, a, True) ty focus valn elabE (True, a, True) val env <- get_env elabE (True, a, inty) sc -- 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) solve elab' ina@(_, a, inty) (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 (True, a, True) (PApp fc r [pexp (delab ist rty)]) env <- get_env computeLet n elabE (True, a, inty) sc solve -- elab' ina (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 xt) (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 (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 elab' (_, _, inty) (PApp fc (PRef _ f) args') | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty = lift $ tfail (Msg "Typecase is not allowed") -- if f is local, just do a simple_app elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args) = do env <- get_env if (f `elem` map fst env && length args == 1) then -- simple app, as below do simple_app (elabE (ina, g, inty) (PRef fc f)) (elabE (True, g, inty) (getTm (head args))) (show tm) solve 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 () _ -> mapM_ setInjective (map getTm args) ctxt <- get_context 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 mapM_ checkIfInjective (map snd ns) unifyProblems -- try again with the new information, -- to help with disambiguation -- Sort so that the implicit tactics and alternatives go last let (ns', eargs) = unzip $ sortBy cmpArg (zip ns args) elabArgs ist (ina || not isinf, guarded, inty) [] fc False f ns' (f == sUN "Force") (map (\x -> (lazyarg x, getTm x)) eargs) solve ivs' <- get_instances -- Attempt to resolve any type classes which have 'complete' types, -- i.e. no holes in them when (not pattern || (ina && not tcgen && not guarded)) $ mapM_ (\n -> do focus n g <- goal env <- get_env hs <- get_holes if all (\n -> not (n `elem` hs)) (freeNames g) -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist)) then try (resolveTC 7 g fn ist) (movelast n) else movelast n) (ivs' \\ ivs) where -- normal < alternatives < lambdas < rewrites < tactic < default tactic -- reason for lambdas after alternatives is that having -- the alternative resolved can help with typechecking the lambda -- or the rewrite. Rewrites/tactics need as much information -- as possible about the type. -- FIXME: Better would be to allow alternative resolution to be -- retried after more information is in. cmpArg (_, x) (_, y) = compare (conDepth 0 (getTm x) + priority x + alt x) (conDepth 0 (getTm y) + priority y + alt y) where alt t = case getTm t of PAlternative False _ -> 5 PAlternative True _ -> 1 PLam _ _ _ -> 2 PRewrite _ _ _ _ -> 3 _ -> 0 -- Score a point for every level where there is a non-constructor -- function (so higher score --> done later) -- Only relevant when on lhs conDepth d t | not pattern = 0 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0 | otherwise = max (100 - d) 1 conDepth d (PApp _ f as) = conDepth d f + sum (map (conDepth (d+1)) (map getTm as)) conDepth d (PPatvar _ _) = 0 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as) conDepth d Placeholder = 0 conDepth d t = max (100 - d) 1 checkIfInjective n = do env <- get_env case lookup n env of Nothing -> return () Just b -> case unApply (binderTy b) of (P _ c _, args) -> case lookupCtxt c (idris_classes ist) of [] -> return () _ -> -- type class, set as injective mapM_ setinjArg args _ -> return () setinjArg (P _ n _) = setinj n setinjArg _ = return () tacTm (PTactics _) = True tacTm (PProof _) = True tacTm _ = False setInjective (PRef _ n) = setinj n setInjective (PApp _ (PRef _ n) _) = setinj n setInjective _ = return () elab' ina@(_, a, inty) tm@(PApp fc f [arg]) = erun fc $ do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg)) (show tm) solve elab' ina Placeholder = do (h : hs) <- get_holes movelast h elab' ina (PMetavar n) = let n' = mkN n in do attack; defer n'; solve where mkN n@(NS _ _) = n mkN n = case namespace info of Just xs@(_:_) -> sNS n xs _ -> n elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts elab' ina (PTactics ts) | not pattern = do mapM_ (runTac False ist fn) ts | otherwise = elab' ina Placeholder elab' ina (PElabError e) = fail (pshow ist 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 r compute g <- goal rewrite (Var letn) g' <- goal when (g == g') $ lift $ tfail (NoRewriting g) case newg of Nothing -> elab' ina 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 t focus valn elab' ina sc elab' ina (PRef fc letn) solve elab' ina@(_, a, inty) 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 (True, a, inty) scr args <- get_env cname <- unique_hole' True (mkCaseName fn) let cname' = mkN cname elab' ina (PMetavar cname') -- 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' (map (isScr scr) (reverse args)) opts) -- elaborate case env <- get_env updateAux (newdef : ) -- 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 elab' ina (PUnifyLog t) = do unifyLog True elab' ina t unifyLog False elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x 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 -> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause] caseBlock fc n 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! -- 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 _ mkClause args (l, r) = let args' = map (shadowed (allNamesIn l)) args lhs = PApp (getFC fc l) (PRef (getFC fc l) n) (map (mkLHSarg l) args') in PClause (getFC fc l) n lhs [] r [] 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 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 t] else [mkDelay t, t] case tyh of P _ (UN l) _ | l == txt "Lazy'" -> return (PAlternative False tries) _ -> return t where mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs) mkDelay t = let fc = fileFC "Delay" in addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp 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 False [t , PAlternative True (map (mkCoerce t) cs)] return t' where mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears! addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)]) -- | Elaborate the arguments to a function elabArgs :: IState -- ^ The current Idris state -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type) -> [Bool] -> FC -- ^ Source location -> Bool -> Name -- ^ Name of the function being applied -> [(Name, Name)] -- ^ (Argument Name, Hole Name) -> Bool -- ^ under a 'force' -> [(Bool, PTerm)] -- ^ (Laziness, argument) -> ElabD () elabArgs ist ina failed fc retry f [] force _ = return () elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args) = elabArgs ist ina failed fc r f ns force args elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args) | lazy && not pattern = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy")) [pimp (sUN "a") Placeholder True, pexp t]) | otherwise = elabArg argName holeName t where elabArg argName holeName t = do 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) $ case holeName `elem` hs of True -> do focus holeName; elab ina t; return failed False -> 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 -- 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 f) as) = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as) prune t = t choose f (PAlternative a as) = let as' = fmap (choose f) as fs = filter (headIs f) as' in case fs of [a] -> a _ -> PAlternative 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 :: Term -> Context -> [PTerm] -> [PTerm] pruneByType (P _ n _) c as -- if the goal type is polymorphic, keep e | [] <- lookupTy n c = 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 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 _ _ _ = True -- keep if it's not an application typeHead var f f' = case lookupTy f' c of [ty] -> let ty' = normalise c [] ty in case unApply (getRetTy ty') of (P _ ftyn _, _) -> ftyn == f (V _, _) -> var -- keep, variable _ -> False _ -> False pruneByType t _ as = as findInstances :: IState -> Term -> [Name] findInstances ist t | (P _ n _, _) <- unApply t = case lookupCtxt n (idris_classes ist) of [CI _ _ _ _ _ ins] -> ins _ -> [] | otherwise = [] trivial' ist = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist proofSearch' ist top n hints = proofSearch (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist resolveTC :: Int -> Term -> Name -> IState -> ElabD () resolveTC = resTC' [] resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class" resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True resTC' tcs depth topg fn ist = do hnf_compute g <- goal ptm <- get_term ulog <- getUnifyLog hs <- get_holes traceWhen ulog ("Resolving class " ++ show g) $ try' (trivial' ist) (do t <- goal let (tc, ttypes) = unApply t scopeOnly <- needsDefault t tc ttypes let insts_in = findInstances ist t let insts = if scopeOnly then filter chaser insts_in else insts_in tm <- get_term let depth' = if scopeOnly then 2 else depth blunderbuss t depth' insts) True where elabTC n | n /= fn && tcname n = (resolve n depth, show n) | otherwise = (fail "Can't resolve", show n) -- HACK! Rather than giving a special name, better to have some kind -- of flag in ClassInfo structure chaser (UN nm) | ('@':'@':_) <- str nm = True -- old way chaser (SN (ParentN _ _)) = True chaser (NS n _) = chaser n chaser _ = False numclass = sNS (sUN "Num") ["Classes","Prelude"] needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass = do focus a fill (RConstant (AType (ATInt ITBig))) -- default Integer solve return False needsDefault t f as | all boundVar as = return True -- fail $ "Can't resolve " ++ show t needsDefault t f a = return False -- trace (show t) $ return () boundVar (P Bound _ _) = True boundVar _ = False blunderbuss t d [] = do -- c <- get_env -- ps <- get_probs lift $ tfail $ CantResolve topg blunderbuss t d (n:ns) | n /= fn && tcname n = try' (resolve n d) (blunderbuss t d ns) True | otherwise = blunderbuss t d ns resolve n depth | depth == 0 = fail $ "Can't resolve type class" | otherwise = do t <- goal let (tc, ttypes) = unApply t -- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist -- else do -- if there's a hole in the goal, don't even try let imps = case lookupCtxtName n (idris_implicits ist) of [] -> [] [args] -> map isImp (snd args) -- won't be overloaded! ps <- get_probs tm <- get_term args <- map snd <$> try' (apply (Var n) imps) (match_apply (Var n) imps) True ps' <- get_probs when (length ps < length ps') $ fail "Can't apply type class" -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $ mapM_ (\ (_,n) -> do focus n t' <- goal let (tc', ttype) = unApply t' let got = fst (unApply t) let depth' = if tc' `elem` tcs then depth - 1 else depth resTC' (got : tcs) depth' topg fn ist) (filter (\ (x, y) -> not x) (zip (map fst imps) args)) -- if there's any arguments left, we've failed to resolve hs <- get_holes ulog <- getUnifyLog solve traceWhen ulog ("Got " ++ show n) $ return () where isImp (PImp p _ _ _ _) = (True, p) isImp arg = (False, priority arg) collectDeferred :: Maybe Name -> Term -> State [(Name, (Int, Maybe Name, Type))] Term collectDeferred top (Bind n (GHole i t) app) = do ds <- get t' <- collectDeferred top t when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))]) collectDeferred top app collectDeferred top (Bind n b t) = do b' <- cdb b t' <- collectDeferred top t return (Bind n b' t') where cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v) cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v) cdb b = do ty' <- collectDeferred top (binderTy b) return (b { binderTy = ty' }) collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a) collectDeferred top t = return t -- Running tactics directly -- if a tactic adds unification problems, return an error runTac :: Bool -> IState -> Name -> PTactic -> ElabD () runTac autoSolve ist fn tac = do env <- get_env g <- goal if autoSolve then runT (fmap (addImplBound ist (map fst env)) tac) else no_errors (runT (fmap (addImplBound ist (map fst env)) 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 False [] (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), show 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), show 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 (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 False [] (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 False [] (sMN 0 "tac") tm rewrite (Var letn) when autoSolve solveAll runT (Induction nm) = do induction nm when autoSolve solveAll 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 False [] (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 False [] (sMN 0 "tac") ty focus valn elab ist toplevel False [] (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 top hints) = do proofSearch' ist top fn hints; when autoSolve solveAll runT (Focus n) = focus n 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 False [] (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 (RApp listTy envTupleType)) (RBind (sMN 1 "__pi_arg") (Pi (Var $ reflm "TT")) 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 False [] (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 False [] (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 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 False [] (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 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 x = fail $ "Not implemented " ++ show x runReflected t = do t' <- reify ist t runTac autoSolve ist fn t' -- | Prefix a name with the "Language.Reflection" namespace reflm :: String -> Name reflm n = sNS (sUN n) ["Reflection", "Language"] -- | Reify tactics from their reflected representation reify :: IState -> Term -> ElabD PTactic reify _ (P _ n _) | n == reflm "Intros" = return Intros reify _ (P _ n _) | n == reflm "Trivial" = return Trivial reify _ (P _ n _) | n == reflm "Instance" = return TCInstance reify _ (P _ n _) | n == reflm "Solve" = return Solve reify _ (P _ n _) | n == reflm "Compute" = return Compute reify ist t@(App _ _) | (P _ f _, args) <- unApply t = reifyApp ist f args reify _ t = fail ("Unknown tactic " ++ show t) reifyApp :: IState -> Name -> [Term] -> ElabD PTactic reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r) reifyApp _ t [x] | t == reflm "Refine" = do n <- reifyTTName x return $ Refine n [] reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r) reifyApp ist t [Constant (Str n), x] | t == reflm "GoalType" = liftM (GoalType n) (reify ist x) reifyApp _ t [Constant (Str n)] | t == reflm "Intro" = return $ Intro [sUN n] reifyApp ist t [t'] | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t') reifyApp ist t [t'] | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t') reifyApp ist t [t'] | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t') reifyApp _ t [t'] | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t') reifyApp ist t [t'] | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t') reifyApp ist t [x] | t == reflm "Focus" = liftM Focus (reifyTTName x) reifyApp ist t [t'] | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t') reifyApp ist t [n, t'] | t == reflm "LetTac" = do n' <- reifyTTName n t'' <- reifyTT t' return $ LetTac n' (delab ist t') reifyApp ist t [n, tt', t'] | t == reflm "LetTacTy" = do n' <- reifyTTName n tt'' <- reifyTT tt' t'' <- reifyTT t' return $ LetTacTy n' (delab ist tt'') (delab ist t'') reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen -- | Reify terms from their reflected representation reifyTT :: Term -> ElabD Term reifyTT t@(App _ _) | (P _ f _, args) <- unApply t = reifyTTApp f args reifyTT t@(P _ n _) | n == reflm "Erased" = return $ Erased reifyTT t@(P _ n _) | n == reflm "Impossible" = return $ Impossible reifyTT t = fail ("Unknown reflection term: " ++ show t) reifyTTApp :: Name -> [Term] -> ElabD Term reifyTTApp t [nt, n, x] | t == reflm "P" = do nt' <- reifyTTNameType nt n' <- reifyTTName n x' <- reifyTT x return $ P nt' n' x' reifyTTApp t [Constant (I i)] | t == reflm "V" = return $ V i reifyTTApp t [n, b, x] | t == reflm "Bind" = do n' <- reifyTTName n b' <- reifyTTBinder reifyTT (reflm "TT") b x' <- reifyTT x return $ Bind n' b' x' reifyTTApp t [f, x] | t == reflm "App" = do f' <- reifyTT f x' <- reifyTT x return $ App f' x' reifyTTApp t [c] | t == reflm "TConst" = liftM Constant (reifyTTConst c) reifyTTApp t [t', Constant (I i)] | t == reflm "Proj" = do t'' <- reifyTT t' return $ Proj t'' i reifyTTApp t [tt] | t == reflm "TType" = liftM TType (reifyTTUExp tt) reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args)) -- | Reify raw terms from their reflected representation reifyRaw :: Term -> ElabD Raw reifyRaw t@(App _ _) | (P _ f _, args) <- unApply t = reifyRawApp f args reifyRaw t@(P _ n _) | n == reflm "RType" = return $ RType reifyRaw t = fail ("Unknown reflection raw term: " ++ show t) reifyRawApp :: Name -> [Term] -> ElabD Raw reifyRawApp t [n] | t == reflm "Var" = liftM Var (reifyTTName n) reifyRawApp t [n, b, x] | t == reflm "RBind" = do n' <- reifyTTName n b' <- reifyTTBinder reifyRaw (reflm "Raw") b x' <- reifyRaw x return $ RBind n' b' x' reifyRawApp t [f, x] | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x) reifyRawApp t [t'] | t == reflm "RForce" = liftM RForce (reifyRaw t') reifyRawApp t [c] | t == reflm "RConstant" = liftM RConstant (reifyTTConst c) reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args)) reifyTTName :: Term -> ElabD Name reifyTTName t | (P _ f _, args) <- unApply t = reifyTTNameApp f args reifyTTName t = fail ("Unknown reflection term name: " ++ show t) reifyTTNameApp :: Name -> [Term] -> ElabD Name reifyTTNameApp t [Constant (Str n)] | t == reflm "UN" = return $ sUN n reifyTTNameApp t [n, ns] | t == reflm "NS" = do n' <- reifyTTName n ns' <- reifyTTNamespace ns return $ sNS n' ns' reifyTTNameApp t [Constant (I i), Constant (Str n)] | t == reflm "MN" = return $ sMN i n reifyTTNameApp t [] | t == reflm "NErased" = return NErased reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args)) reifyTTNamespace :: Term -> ElabD [String] reifyTTNamespace t@(App _ _) = case unApply t of (P _ f _, [Constant StrType]) | f == sNS (sUN "Nil") ["List", "Prelude"] -> return [] (P _ f _, [Constant StrType, Constant (Str n), ns]) | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns) _ -> fail ("Unknown reflection namespace arg: " ++ show t) reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t) reifyTTNameType :: Term -> ElabD NameType reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref reifyTTNameType t@(App _ _) = case unApply t of (P _ f _, [Constant (I tag), Constant (I num)]) | f == reflm "DCon" -> return $ DCon tag num | f == reflm "TCon" -> return $ TCon tag num _ -> fail ("Unknown reflection name type: " ++ show t) reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t) reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a) reifyTTBinder reificator binderType t@(App _ _) = case unApply t of (P _ f _, bt:args) | forget bt == Var binderType -> reifyTTBinderApp reificator f args _ -> fail ("Mismatching binder reflection: " ++ show t) reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t) reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a) reifyTTBinderApp reif f [t] | f == reflm "Lam" = liftM Lam (reif t) reifyTTBinderApp reif f [t] | f == reflm "Pi" = liftM Pi (reif t) reifyTTBinderApp reif f [x, y] | f == reflm "Let" = liftM2 Let (reif x) (reif y) reifyTTBinderApp reif f [x, y] | f == reflm "NLet" = liftM2 NLet (reif x) (reif y) reifyTTBinderApp reif f [t] | f == reflm "Hole" = liftM Hole (reif t) reifyTTBinderApp reif f [t] | f == reflm "GHole" = liftM (GHole 0) (reif t) reifyTTBinderApp reif f [x, y] | f == reflm "Guess" = liftM2 Guess (reif x) (reif y) reifyTTBinderApp reif f [t] | f == reflm "PVar" = liftM PVar (reif t) reifyTTBinderApp reif f [t] | f == reflm "PVTy" = liftM PVTy (reif t) reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args)) reifyTTConst :: Term -> ElabD Const reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative)) reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig)) reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat) reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar)) reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8))) reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16))) reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32))) reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64))) reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot reifyTTConst t@(App _ _) | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg reifyTTConst t = fail ("Unknown reflection constant: " ++ show t) reifyTTConstApp :: Name -> Term -> ElabD Const reifyTTConstApp f (Constant c@(I _)) | f == reflm "I" = return $ c reifyTTConstApp f (Constant c@(BI _)) | f == reflm "BI" = return $ c reifyTTConstApp f (Constant c@(Fl _)) | f == reflm "Fl" = return $ c reifyTTConstApp f (Constant c@(I _)) | f == reflm "Ch" = return $ c reifyTTConstApp f (Constant c@(Str _)) | f == reflm "Str" = return $ c reifyTTConstApp f (Constant c@(B8 _)) | f == reflm "B8" = return $ c reifyTTConstApp f (Constant c@(B16 _)) | f == reflm "B16" = return $ c reifyTTConstApp f (Constant c@(B32 _)) | f == reflm "B32" = return $ c reifyTTConstApp f (Constant c@(B64 _)) | f == reflm "B64" = return $ c reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg)) reifyTTUExp :: Term -> ElabD UExp reifyTTUExp t@(App _ _) = case unApply t of (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i _ -> fail ("Unknown reflection type universe expression: " ++ show t) reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t) -- | Create a reflected call to a named function/constructor reflCall :: String -> [Raw] -> Raw reflCall funName args = raw_apply (Var (reflm funName)) args -- | Lift a term into its Language.Reflection.TT representation reflect :: Term -> Raw reflect (P nt n t) = reflCall "P" [reflectNameType nt, reflectName n, reflect t] reflect (V n) = reflCall "V" [RConstant (I n)] reflect (Bind n b x) = reflCall "Bind" [reflectName n, reflectBinder b, reflect x] reflect (App f x) = reflCall "App" [reflect f, reflect x] reflect (Constant c) = reflCall "TConst" [reflectConstant c] reflect (Proj t i) = reflCall "Proj" [reflect t, RConstant (I i)] reflect (Erased) = Var (reflm "Erased") reflect (Impossible) = Var (reflm "Impossible") reflect (TType exp) = reflCall "TType" [reflectUExp exp] reflectNameType :: NameType -> Raw reflectNameType (Bound) = Var (reflm "Bound") reflectNameType (Ref) = Var (reflm "Ref") reflectNameType (DCon x y) = reflCall "DCon" [RConstant (I x), RConstant (I y)] reflectNameType (TCon x y) = reflCall "TCon" [RConstant (I x), RConstant (I y)] reflectName :: Name -> Raw reflectName (UN s) = reflCall "UN" [RConstant (Str (str s))] reflectName (NS n ns) = reflCall "NS" [ reflectName n , foldr (\ n s -> raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] ) [ RConstant StrType, RConstant (Str n), s ]) ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] ) [ RConstant StrType ]) (map str ns) ] reflectName (MN i n) = reflCall "MN" [RConstant (I i), RConstant (Str (str n))] reflectName (NErased) = Var (reflm "NErased") reflectName n = Var (reflm "NErased") -- special name, not yet implemented reflectBinder :: Binder Term -> Raw reflectBinder (Lam t) = reflCall "Lam" [Var (reflm "TT"), reflect t] reflectBinder (Pi t) = reflCall "Pi" [Var (reflm "TT"), reflect t] reflectBinder (Let x y) = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y] reflectBinder (NLet x y) = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y] reflectBinder (Hole t) = reflCall "Hole" [Var (reflm "TT"), reflect t] reflectBinder (GHole _ t) = reflCall "GHole" [Var (reflm "TT"), reflect t] reflectBinder (Guess x y) = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y] reflectBinder (PVar t) = reflCall "PVar" [Var (reflm "TT"), reflect t] reflectBinder (PVTy t) = reflCall "PVTy" [Var (reflm "TT"), reflect t] reflectConstant :: Const -> Raw reflectConstant c@(I _) = reflCall "I" [RConstant c] reflectConstant c@(BI _) = reflCall "BI" [RConstant c] reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c] reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c] reflectConstant c@(Str _) = reflCall "Str" [RConstant c] reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType") reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType") reflectConstant (AType ATFloat) = Var (reflm "FlType") reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType") reflectConstant (StrType) = Var (reflm "StrType") reflectConstant c@(B8 _) = reflCall "B8" [RConstant c] reflectConstant c@(B16 _) = reflCall "B16" [RConstant c] reflectConstant c@(B32 _) = reflCall "B32" [RConstant c] reflectConstant c@(B64 _) = reflCall "B64" [RConstant c] reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type") reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type") reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type") reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type") reflectConstant (PtrType) = Var (reflm "PtrType") reflectConstant (VoidType) = Var (reflm "VoidType") reflectConstant (Forgot) = Var (reflm "Forgot") reflectUExp :: UExp -> Raw reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)] reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)] -- | Reflect the environment of a proof into a List (TTName, Binder TT) reflectEnv :: Env -> Raw reflectEnv = foldr consToEnvList emptyEnvList where consToEnvList :: (Name, Binder Term) -> Raw -> Raw consToEnvList (n, b) l = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ envTupleType , raw_apply (Var pairCon) [ (Var $ reflm "TTName") , (RApp (Var $ reflm "Binder") (Var $ reflm "TT")) , reflectName n , reflectBinder b ] , l ] emptyEnvList :: Raw emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [envTupleType] -- | Reflect an error into the internal datatype of Idris -- TODO rawBool :: Bool -> Raw rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"]) rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"]) rawNil :: Raw -> Raw rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty] rawCons :: Raw -> Raw -> Raw -> Raw rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl] rawList :: Raw -> [Raw] -> Raw rawList ty = foldr (rawCons ty) (rawNil ty) rawPairTy :: Raw -> Raw -> Raw rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2] rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y] reflectCtxt :: [(Name, Type)] -> Raw reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT")) (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT") (reflectName n, reflect t))) ctxt) reflectErr :: Err -> Raw reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)] reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)] reflectErr (CantUnify b t1 t2 e ctxt i) = raw_apply (Var $ reflErrName "CantUnify") [ rawBool b , reflect t1 , reflect t2 , reflectErr e , reflectCtxt ctxt , RConstant (I i)] reflectErr (InfiniteUnify n tm ctxt) = raw_apply (Var $ reflErrName "InfiniteUnify") [ reflectName n , reflect tm , reflectCtxt ctxt ] reflectErr (CantConvert t t' ctxt) = raw_apply (Var $ reflErrName "CantConvert") [ reflect t , reflect t' , reflectCtxt ctxt ] reflectErr (CantSolveGoal t ctxt) = raw_apply (Var $ reflErrName "CantSolveGoal") [ reflect t , reflectCtxt ctxt ] reflectErr (UnifyScope n n' t ctxt) = raw_apply (Var $ reflErrName "UnifyScope") [ reflectName n , reflectName n' , reflect t , reflectCtxt ctxt ] reflectErr (CantInferType str) = raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)] reflectErr (NonFunctionType t t') = raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t'] reflectErr (NotEquality t t') = raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t'] reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n] reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t] reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n] reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n] reflectErr (NotInjective t1 t2 t3) = raw_apply (Var $ reflErrName "NotInjective") [ reflect t1 , reflect t2 , reflect t3 ] reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t] reflectErr (CantResolveAlts ss) = raw_apply (Var $ reflErrName "CantResolve") [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)] reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t] reflectErr UniverseError = Var $ reflErrName "UniverseError" reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment" reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n] reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n] reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n] reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e] reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm] reflectErr (ProviderError str) = raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)] reflectErr (LoadingFailed str err) = raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)] reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x] 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') -- 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 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm) | just == txt "Just" = Just tm fromTTMaybe x = Nothing reflErrName :: String -> Name reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"] -- | Attempt to reify a report part from TT to the internal -- representation. Not in Idris or ElabD monads because it should be usable -- from either. reifyReportPart :: Term -> Either Err ErrorReportPart reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" = Right (TextPart msg) reifyReportPart (App (P (DCon _ _) n _) ttn) | n == reflErrName "NamePart" = case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of Error e -> Left . InternalMsg $ "could not reify name term " ++ show ttn ++ " when reflecting an error:" ++ show e OK (n', _)-> Right $ NamePart n' reifyReportPart (App (P (DCon _ _) n _) tm) | n == reflErrName "TermPart" = case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of Error e -> Left . InternalMsg $ "could not reify reflected term " ++ show tm ++ " when reflecting an error:" ++ show e OK (tm', _) -> Right $ TermPart tm' reifyReportPart (App (P (DCon _ _) n _) tm) | n == reflErrName "SubReport" = case unList tm of Just xs -> do subParts <- mapM reifyReportPart xs Right (SubReport subParts) Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x envTupleType :: Raw envTupleType = raw_apply (Var pairTy) [ (Var $ reflm "TTName") , (RApp (Var $ reflm "Binder") (Var $ reflm "TT")) ] solveAll = try (do solve; solveAll) (return ())