git.iko.soy/Idris-dev
on 034b415 help sign in
Idris-dev/src/Idris/Transforms.hs
99 lines 3.9 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 where depat ms (Bind n (PVar t) sc)
75 = case lookup n ms of
76 Just tm -> depat ms (subst n tm sc)
77 _ -> depat ms sc -- no occurrence? Shouldn't happen
78 depat ms tm = tm
80matchTerm :: Term -> Term -> Maybe [(Name, Term)]
81matchTerm lhs tm = matchVars [] lhs tm
82 where
83 matchVars acc (Bind n (PVar t) sc) tm
84 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
85 matchVars acc sc tm
86 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
87 doMatch acc sc tm
89 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
90 doMatch ns (P _ n _) tm
91 | n `elem` ns = return [(n, tm)]
92 doMatch ns (App f a) (App f' a')
93 = do fm <- doMatch ns f f'
94 am <- doMatch ns a a'
95 return (fm ++ am)
96 doMatch ns x y | x == y = return []
97 | otherwise = Nothing