{-# LANGUAGE PatternGuards #-} module Idris.ElabTerm where import Idris.AbsSyntax import Idris.DSL import Idris.Delaborate import Core.Elaborate hiding (Tactic(..)) import Core.TT import Core.Evaluate import Control.Monad import Control.Monad.State import Data.List 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 type ElabD a = Elab' [PDecl] a -- 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 -> Name -> PTerm -> ElabD (Term, [(Name, Type)], [PDecl]) build ist info pattern fn tm = do elab ist info pattern False 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 try (resolveTC 7 fn ist) (movelast n)) ivs ivs <- get_instances hs <- get_holes when (not pattern) $ mapM_ (\n -> when (n `elem` hs) $ do focus n resolveTC 7 fn ist) ivs probs <- get_probs tm <- get_term ctxt <- get_context case probs of [] -> return () ((_,_,_,e):es) -> lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred 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 -> Bool -> Name -> PTerm -> ElabD (Term, [(Name, Type)], [PDecl]) buildTC ist info pattern tcgen fn tm = do elab ist info pattern tcgen 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 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 -> Bool -> Name -> PTerm -> ElabD () elab ist info pattern tcgen fn tm = do let loglvl = opt_logLevel (idris_options ist) when (loglvl > 5) $ unifyLog True elabE (False, False) tm -- (in argument, guarded) end_unify when pattern -- convert remaining holes to pattern vars (do update_term orderPats tm <- get_term mkPat) where 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 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") $ elab' ina t' local f = do e <- get_env return (f `elem` map fst e) elab' ina PType = do apply RType []; solve 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 = resolveTC 5 fn ist elab' ina (PResolveTC fc) | True = do c <- unique_hole (MN 0 "class") instanceArg c | otherwise = do g <- goal try (resolveTC 2 fn ist) (do c <- unique_hole (MN 0 "class") instanceArg c) elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder, pimp (MN 0 "x") t]) elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder, pimp (MN 0 "b") Placeholder, pexp l, pexp r]) elab' ina@(_, a) (PPair fc l r) = do hnf_compute g <- goal case g of TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy) [pexp l,pexp r]) _ -> elabE (True, a) (PApp fc (PRef fc pairCon) [pimp (MN 0 "A") Placeholder, pimp (MN 0 "B") Placeholder, 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 (MN 0 "a") t, pimp (MN 0 "P") Placeholder, pexp l, pexp r]) elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon) [pimp (MN 0 "a") t, pimp (MN 0 "P") Placeholder, 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 -- case as' of -- [a] -> elab' ina a -- as -> lift $ tfail $ CantResolveAlts (map showHd as) tryAll (zip (map (elab' ina) as') (map showHd as')) where 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' (ina, guarded) (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) (PLam n Placeholder sc) = do -- n' <- unique_hole n -- let sc' = mapPT (repN n n') sc ptm <- get_term g <- goal checkPiGoal n attack; intro (Just n); -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm) elabE (True, a) sc; solve where repN n n' (PRef fc x) | x == n' = PRef fc n' repN _ _ t = t elab' ina@(_, a) (PLam n ty sc) = do hsin <- get_holes ptmin <- get_term tyn <- unique_hole (MN 0 "lamty") checkPiGoal n claim tyn RType attack ptm <- get_term hs <- get_holes -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++ -- "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $ introTy (Var tyn) (Just n) -- end_unify focus tyn ptm <- get_term hs <- get_holes elabE (True, a) ty elabE (True, a) sc solve elab' ina@(_,a) (PPi _ n Placeholder sc) = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve elab' ina@(_,a) (PPi _ n ty sc) = do attack; tyn <- unique_hole (MN 0 "ty") claim tyn RType n' <- case n of MN _ _ -> unique_hole n _ -> return n forall n' (Var tyn) focus tyn elabE (True, a) ty elabE (True, a) sc solve elab' ina@(_,a) (PLet n ty val sc) = do attack; tyn <- unique_hole (MN 0 "letty") claim tyn RType valn <- unique_hole (MN 0 "letval") claim valn (Var tyn) letbind n (Var tyn) (Var valn) case ty of Placeholder -> return () _ -> do focus tyn elabE (True, a) ty focus valn elabE (True, a) val env <- get_env elabE (True, a) 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 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 <- unique_hole (MN 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 <- unique_hole (MN 0 "inf_argTy") aval <- unique_hole (MN 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 = case namespace info of Just xs@(_:_) -> NS n xs _ -> n elab' (ina, g) (PMatchApp fc fn) = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of [(n, args)] -> return (n, map (const True) args) _ -> lift $ tfail (NoSuchVariable fn) ns <- match_apply (Var fn') (map (\x -> (x,0)) imps) solve -- if f is local, just do a simple_app elab' (ina, g) tm@(PApp fc (PRef _ f) args') = do let args = {- case lookupCtxt f (inblock info) of Just ps -> (map (pexp . (PRef fc)) ps ++ args') _ -> -} args' -- newtm <- mkSpecialised ist fc f (map getTm args') tm env <- get_env if (f `elem` map fst env && length args' == 1) then -- simple app, as below do simple_app (elabE (ina, g) (PRef fc f)) (elabE (True, g) (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 ns <- apply (Var f) (map isph args) ptm <- get_term g <- goal let (ns', eargs) = unzip $ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y)) (zip ns args) elabArgs (ina || not isinf, guarded) [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs) mkSpecialised ist fc f (map getTm args') tm solve ptm <- get_term ivs' <- get_instances ps' <- get_probs -- 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 fn ist) (movelast n) else movelast n) (ivs' \\ ivs) where tcArg (n, PConstraint _ _ Placeholder _) = True tcArg _ = False tacTm (PTactics _) = True tacTm (PProof _) = True tacTm _ = False setInjective (PRef _ n) = setinj n setInjective (PApp _ (PRef _ n) _) = setinj n setInjective _ = return () elab' ina@(_, a) tm@(PApp fc f [arg]) = erun fc $ do simple_app (elabE ina f) (elabE (True, a) (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@(_:_) -> NS 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 <- unique_hole (MN 0 "rty") claim tyn RType valn <- unique_hole (MN 0 "rval") claim valn (Var tyn) letn <- unique_hole (MN 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 <- unique_hole (MN 0 "ety") claim tyn RType valn <- unique_hole (MN 0 "eqval") claim valn (Var tyn) letn <- unique_hole (MN 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) c@(PCase fc scr opts) = do attack tyn <- unique_hole (MN 0 "scty") claim tyn RType valn <- unique_hole (MN 0 "scval") scvn <- unique_hole (MN 0 "scvar") claim valn (Var tyn) letbind scvn (Var tyn) (Var valn) focus valn elabE (True, a) scr args <- get_env cname <- unique_hole' True (mkCaseName fn) let cname' = mkN cname elab' ina (PMetavar cname') let newdef = PClauses fc [] cname' (caseBlock fc cname' (reverse args) opts) -- elaborate case env <- get_env g <- goal 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 (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@(_:_) -> NS n xs _ -> n elab' ina (PUnifyLog t) = do unifyLog True elab' ina t unifyLog False elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?" caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause] caseBlock fc n env opts = let args = map mkarg (map fst (init env)) in map (mkClause args) opts where -- mkarg (MN _ _) = Placeholder mkarg n = PRef fc n -- 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 fc (PRef fc n) (map pexp args' ++ [pexp l]) in PClause fc n lhs [] r [] shadowed new (PRef _ n) | n `elem` new = Placeholder shadowed new t = 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 = FC "Coercion" 0 in -- line never appears! addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)]) elabArgs ina failed fc retry [] _ -- | retry = let (ns, ts) = unzip (reverse failed) in -- elabArgs ina [] False ns ts | otherwise = return () elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args) = elabArgs ina failed fc r ns args elabArgs ina failed fc r (n:ns) ((lazy, t) : args) | lazy && not pattern = do elabArg n (PApp bi (PRef bi (UN "lazy")) [pimp (UN "a") Placeholder, pexp t]); | otherwise = elabArg n t where elabArg n t = 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 n `elem` hs of True -> -- if r -- then try (do focus n; elabE ina t; return failed) -- (return ((n,(lazy, t)):failed)) do focus n; elabE ina t; return failed False -> return failed elabArgs ina failed fc r ns args -- 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 trivial :: IState -> ElabD () trivial ist = try' (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0) Placeholder) return ()) (do env <- get_env g <- goal tryAll env return ()) True where tryAll [] = fail "No trivial solution" tryAll ((x, b):xs) = do -- if type of x has any holes in it, move on hs <- get_holes g <- goal if all (\n -> not (n `elem` hs)) (freeNames (binderTy b)) then try' (elab ist toplevel False False (MN 0 "tac") (PRef (FC "prf" 0) x)) (tryAll xs) True else tryAll xs findInstances :: IState -> Term -> [Name] findInstances ist t | (P _ n _, _) <- unApply t = case lookupCtxt n (idris_classes ist) of [CI _ _ _ _ ins] -> ins _ -> [] | otherwise = [] resolveTC :: Int -> Name -> IState -> ElabD () resolveTC 0 fn ist = fail $ "Can't resolve type class" resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True resolveTC depth fn ist = do hnf_compute g <- goal ptm <- get_term hs <- get_holes if True -- all (\n -> not (n `elem` hs)) (freeNames g) then 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 -- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $ -- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist))))) -- if scopeOnly then fail "Can't resolve" else let depth' = if scopeOnly then 2 else depth blunderbuss t depth' insts) True else do try' (trivial ist) (do g <- goal fail $ "Can't resolve " ++ show g) True -- tm <- get_term -- fail $ "Can't resolve yet in " ++ show tm 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 ('@':'@':_)) = True chaser (NS n _) = chaser n chaser _ = False needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _] = 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 t 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 args <- apply (Var n) imps 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' 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 solve where isImp (PImp p _ _ _ _) = (True, p) isImp arg = (False, priority arg) collectDeferred :: Term -> State [(Name, Type)] Term collectDeferred (Bind n (GHole t) app) = do ds <- get when (not (n `elem` map fst ds)) $ put ((n, t) : ds) collectDeferred app collectDeferred (Bind n b t) = do b' <- cdb b t' <- collectDeferred t return (Bind n b' t') where cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v) cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v) cdb b = do ty' <- collectDeferred (binderTy b) return (b { binderTy = ty' }) collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a) collectDeferred 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 no_errors $ runT (fmap (addImplBound ist (map fst env)) tac) 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 False (MN 0 "tac") tm when autoSolve solveAll runT (MatchRefine fn) = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of [] -> do a <- envArgs fn return (fn, a) [(n, args)] -> return $ (n, map (const True) args) ns <- match_apply (Var fn') (map (\x -> (x, 0)) imps) 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 (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of [] -> do a <- envArgs fn return (fn, a) -- FIXME: resolve ambiguities [(n, args)] -> return $ (n, map isImp args) ns <- apply (Var fn') (map (\x -> (x, 0)) imps) 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 <- unique_hole (MN 0 "ety") claim tyn RType valn <- unique_hole (MN 0 "eqval") claim valn (Var tyn) letn <- unique_hole (MN 0 "equiv_val") letbind letn (Var tyn) (Var valn) focus tyn elab ist toplevel False False (MN 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 <- unique_hole (MN 0 "rty") -- start_unify h claim tyn RType valn <- unique_hole (MN 0 "rval") claim valn (Var tyn) letn <- unique_hole (MN 0 "rewrite_rule") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel False False (MN 0 "tac") tm rewrite (Var letn) when autoSolve solveAll runT (LetTac n tm) = do attack tyn <- unique_hole (MN 0 "letty") claim tyn RType valn <- unique_hole (MN 0 "letval") claim valn (Var tyn) letn <- unique_hole n letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel False False (MN 0 "tac") tm when autoSolve solveAll runT (LetTacTy n ty tm) = do attack tyn <- unique_hole (MN 0 "letty") claim tyn RType valn <- unique_hole (MN 0 "letval") claim valn (Var tyn) letn <- unique_hole n letbind letn (Var tyn) (Var valn) focus tyn elab ist toplevel False False (MN 0 "tac") ty focus valn elab ist toplevel False False (MN 0 "tac") tm when autoSolve solveAll runT Compute = compute runT Trivial = do trivial ist; 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 <- unique_hole (MN 0 "script") claim script scriptTy scriptvar <- unique_hole (MN 0 "scriptvar" ) letbind scriptvar scriptTy (Var script) focus script elab ist toplevel False False (MN 0 "tac") tm (script', _) <- get_type_val (Var scriptvar) -- now that we have the script apply -- it to the reflected goal and context restac <- unique_hole (MN 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 (NS (UN "List") ["List", "Prelude"]) scriptTy = (RBind (UN "__pi_arg") (Pi (RApp listTy envTupleType)) (RBind (UN "__pi_arg1") (Pi (Var $ reflm "TT")) tacticTy)) runT (Reflect v) = do attack -- let x = reflect v in ... tyn <- unique_hole (MN 0 "letty") claim tyn RType valn <- unique_hole (MN 0 "letval") claim valn (Var tyn) letn <- unique_hole (MN 0 "letvar") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel False False (MN 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 <- unique_hole (MN 0 "letty") claim tyn RType valn <- unique_hole (MN 0 "letval") claim valn (Var tyn) letn <- unique_hole (MN 0 "letvar") letbind letn (Var tyn) (Var valn) focus valn elab ist toplevel False False (MN 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' == UN n then runT tac else fail "Wrong goal type" _ -> fail "Wrong goal type" runT x = fail $ "Not implemented " ++ show x runReflected t = do t' <- reify ist t runTac autoSolve ist t' -- | Prefix a name with the "Reflection.Language" namespace reflm :: String -> Name reflm n = NS (UN 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 "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 [UN 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@(App _ _) | (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 $ UN n reifyTTNameApp t [n, ns] | t == reflm "NS" = do n' <- reifyTTName n ns' <- reifyTTNamespace ns return $ NS n' ns' reifyTTNameApp t [Constant (I i), Constant (Str n)] | t == reflm "MN" = return $ MN 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 == NS (UN "Nil") ["List", "Prelude"] -> return [] (P _ f _, [Constant StrType, Constant (Str n), ns]) | f == NS (UN "::") ["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 (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 str) = reflCall "UN" [RConstant (Str str)] reflectName (NS n ns) = reflCall "NS" [ reflectName n , foldr (\ n s -> raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] ) [ RConstant StrType, RConstant (Str n), s ]) ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] ) [ RConstant StrType ]) ns ] reflectName (MN i n) = reflCall "MN" [RConstant (I i), RConstant (Str n)] reflectName (NErased) = Var (reflm "NErased") 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 (NS (UN "::") ["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 (NS (UN "Nil") ["List", "Prelude"])) [envTupleType] envTupleType :: Raw envTupleType = raw_apply (Var pairTy) [ (Var $ reflm "TTName") , (RApp (Var $ reflm "Binder") (Var $ reflm "TT")) ] solveAll = try (do solve; solveAll) (return ()) -- If the function application is specialisable, make a new -- top level function by normalising the application -- and elaborating the new expression. mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm mkSpecialised i fc n args def = do let tm' = def case lookupCtxt n (idris_statics i) of [] -> return tm' [as] -> if (not (or as)) then return tm' else mkSpecDecl i n (zip args as) tm' mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm mkSpecDecl i n pargs tm' = do t <- goal g <- get_guess let (f, args) = unApply g let sargs = zip args (map snd pargs) let staticArgs = map fst (filter (\ (_,x) -> x) sargs) let ns = group (sort (concatMap staticFnNames staticArgs)) let ntimes = map (\xs -> (head xs, length xs - 1)) ns if (not (null ns)) then do env <- get_env let g' = g -- specialise ctxt env ntimes g return tm' -- trace (show t ++ "\n" ++ -- show ntimes ++ "\n" ++ -- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO else return tm' where ctxt = tt_ctxt i cg = idris_callgraph i staticFnNames tm | (P _ f _, as) <- unApply tm = if not (isFnName f ctxt) then [] else case lookupCtxt f cg of [ns] -> f : f : [] --(ns \\ [f]) [] -> [f,f] _ -> [] staticFnNames _ = []