{-# LANGUAGE PatternGuards #-} module Idris.ElabTerm where import Idris.AbsSyntax import Idris.DSL import Idris.Delaborate import Idris.Error import Idris.ProofSearch import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.TT import Idris.Core.Evaluate import Idris.Core.Typecheck (check) import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.List import qualified Data.Map as M import Data.Maybe (mapMaybe) 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 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 when (not pattern) $ do matchProblems; unifyProblems probs <- get_probs case probs of [] -> return () ((_,_,_,e):es) -> 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 initNextNameFrom ns elab ist info pattern opts fn tm probs <- get_probs tm <- get_term case probs of [] -> return () ((_,_,_,e):es) -> 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 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 tm <- get_term trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm) $ -} do t' <- insertCoerce ina t 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') $ elab' ina t' 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 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 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 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 () -- 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' (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 tcArg (n, PConstraint _ _ Placeholder _) = True tcArg _ = False -- normal < tactic < default tactic cmpArg (_, x) (_, y) = compare (priority x + alt x) (priority y + alt y) where alt t = case getTm t of PAlternative False _ -> 5 _ -> 0 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) ts elab' ina (PTactics ts) | not pattern = do mapM_ (runTac False ist) 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 " ++ show 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 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, PTerm)] -- ^ (Laziness, argument) -> ElabD () elabArgs ist ina failed fc retry f [] _ -- | retry = let (ns, ts) = unzip (reverse failed) in -- elabArgs ina [] False ns ts | otherwise = return () elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args) = elabArgs ist ina failed fc r f ns args elabArgs ist ina failed fc r f ((argName, holeName):ns) ((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 = reflectFunctionErrors ist f argName $ do hs <- get_holes tm <- get_term 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; elabE ina t; return failed False -> return failed elabArgs ist ina failed fc r f ns args -- | Perform error reflection for function applicaitons with specific error handlers reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a reflectFunctionErrors ist f arg action = do elabState <- get (result, newState) <- case runStateT action elabState of OK (res, newState) -> return (res, newState) Error e@(ReflectionError _ _) -> (lift . tfail) e Error e@(ReflectionFailed _ _) -> (lift . tfail) e Error e -> handle e >>= lift . tfail put newState return result where handle :: Err -> ElabD Err handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist handlers = (maybe [] S.toList . M.lookup arg) funhandlers reports = map (\n -> RApp (Var n) (reflectErr e)) handlers -- Typecheck error handlers - if this fails, then something else was wrong earlier! handlers <- case mapM (check (tt_ctxt ist) []) reports of Error e -> lift . tfail $ ReflectionFailed "Type error while constructing reflected error" e OK hs -> return hs -- Normalize error handler terms to produce the new messages let ctxt = tt_ctxt ist results = map (normalise ctxt []) (map fst handlers) -- 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 -> lift (tfail err) Right ok -> return ok return $ case errorparts of [] -> e parts -> ReflectionError errorparts e -- 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 0 topg fn ist = fail $ "Can't resolve type class" resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True resolveTC 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 depth' = if t == t' then depth - 1 else depth resolveTC 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 when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds) 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 -> PTactic -> ElabD () runTac autoSolve ist tac = do env <- get_env g <- goal 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 n hints) = do proofSearch' ist top n 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 (sUN "__pi_arg") (Pi (RApp listTy envTupleType)) (RBind (sUN "__pi_arg1") (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 (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 (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 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 _ 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 (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err] where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc") [ RConstant (Str source) , RConstant (I line) , RConstant (I col) ] reflectErr (Elaborating str n e) = raw_apply (Var $ reflErrName "Elaborating") [ RConstant (Str str) , reflectName n , reflectErr e ] 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] 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 handle e = do ist <- getIState logLvl 2 "Starting error reflection" let handlers = idris_errorhandlers ist logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers)) let reports = map (\n -> RApp (Var n) (reflectErr e)) 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 ())