git.iko.soy/Idris-dev
on e09ef82 help sign in
Idris-dev/src/Idris/Transforms.hs
95 lines 3.7 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Transforms(transformPats,
4 transformPatsWith,
5 applyTransRulesWith,
6 applyTransRules) where
8import Idris.AbsSyntax
9import Idris.Core.CaseTree
10import Idris.Core.TT
12import Debug.Trace
14transformPats :: IState -> [Either Term (Term, Term)] ->
15 [Either Term (Term, Term)]
16transformPats ist ps = map tClause ps where
17 tClause (Left t) = Left t -- not a clause, leave it alone
18 tClause (Right (lhs, rhs)) -- apply transforms on RHS
19 = let rhs' = applyTransRules ist rhs in
20 Right (lhs, rhs')
22transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->
23 [Either Term (Term, Term)]
24transformPatsWith rs ps = map tClause ps where
25 tClause (Left t) = Left t -- not a clause, leave it alone
26 tClause (Right (lhs, rhs)) -- apply transforms on RHS
27 = let rhs' = applyTransRulesWith rs rhs in
28 Right (lhs, rhs')
30-- Work on explicitly named terms, so we don't have to manipulate
31-- de Bruijn indices
32applyTransRules :: IState -> Term -> Term
33applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)
35-- Work on explicitly named terms, so we don't have to manipulate
36-- de Bruijn indices
37applyTransRulesWith :: [(Term, Term)] -> Term -> Term
38applyTransRulesWith rules tm
39 = finalise $ applyAll rules emptyContext (vToP tm)
41applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
42applyAll extra ts ap@(App f a)
43 | (P _ fn ty, args) <- unApply ap
44 = let rules = case lookupCtxtExact fn ts of
45 Just r -> extra ++ r
46 Nothing -> extra in
47 case rules of
48 [] -> App (applyAll extra ts f) (applyAll extra ts a)
49 rs -> case applyFnRules rs ap of
50 Just tm' -> tm'
51 _ -> App (applyAll extra ts f)
52 (applyAll extra ts a)
53applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)
54 (applyAll extra ts sc)
55applyAll extra ts t = t
57applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
58applyFnRules [] tm = Nothing
59applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
60 | otherwise = applyFnRules rs tm
62applyRule :: (Term, Term) -> Term -> Maybe Term
63applyRule (lhs, rhs) tm
64 | Just ms <- matchTerm lhs tm
65-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
66-- "\n" ++ show rhs
67-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
68 = Just $ depat ms rhs
69 | otherwise = Nothing
70 where depat ms (Bind n (PVar t) sc)
71 = case lookup n ms of
72 Just tm -> depat ms (subst n tm sc)
73 _ -> depat ms sc -- no occurrence? Shouldn't happen
74 depat ms tm = tm
76matchTerm :: Term -> Term -> Maybe [(Name, Term)]
77matchTerm lhs tm = matchVars [] lhs tm
78 where
79 matchVars acc (Bind n (PVar t) sc) tm
80 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
81 matchVars acc sc tm
82 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
83 doMatch acc sc tm
85 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
86 doMatch ns (P _ n _) tm
87 | n `elem` ns = return [(n, tm)]
88 doMatch ns (App f a) (App f' a')
89 = do fm <- doMatch ns f f'
90 am <- doMatch ns a a'
91 return (fm ++ am)
92 doMatch ns x y | x == y = return []
93 | otherwise = Nothing