git.iko.soy/Idris-dev
on cbbdb3e help sign in
Idris-dev/src/Idris/Transforms.hs
104 lines 4.3 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
47 ap' = App (applyAll extra ts f) (applyAll extra ts a) in
48 case rules of
49 [] -> ap'
50 rs -> case applyFnRules rs ap of
51 Just tm'@(App f' a') ->
52 App (applyAll extra ts f')
53 (applyAll extra ts a')
54 Just tm' -> tm'
55 _ -> App (applyAll extra ts f)
56 (applyAll extra ts a)
57applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)
58 (applyAll extra ts sc)
59applyAll extra ts t = t
61applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
62applyFnRules [] tm = Nothing
63applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
64 | otherwise = applyFnRules rs tm
66applyRule :: (Term, Term) -> Term -> Maybe Term
67applyRule (lhs, rhs) tm
68 | Just ms <- matchTerm lhs tm
69-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
70-- "\n" ++ show rhs
71-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
72 = Just $ depat ms rhs
73 | otherwise = Nothing
74-- ASSUMPTION: The names in the transformation rule bindings cannot occur
75-- in the term being transformed.
76-- (In general, this would not be true, but when we elaborate transformation
77-- rules we mangle the names so that it is true. While this feels a bit
78-- hacky, it's much easier to think about than mangling de Bruijn indices).
79 where depat ms (Bind n (PVar t) sc)
80 = case lookup n ms of
81 Just tm -> depat ms (subst n tm sc)
82 _ -> depat ms sc -- no occurrence? Shouldn't happen
83 depat ms tm = tm
85matchTerm :: Term -> Term -> Maybe [(Name, Term)]
86matchTerm lhs tm = matchVars [] lhs tm
87 where
88 matchVars acc (Bind n (PVar t) sc) tm
89 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
90 matchVars acc sc tm
91 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
92 doMatch acc sc tm
94 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
95 doMatch ns (P _ n _) tm
96 | n `elem` ns = return [(n, tm)]
97 doMatch ns (App f a) (App f' a')
98 = do fm <- doMatch ns f f'
99 am <- doMatch ns a a'
100 return (fm ++ am)
101 doMatch ns x y | vToP x == vToP y = return []
102 | otherwise = Nothing