git.iko.soy/Idris-dev
on ed0bfca help sign in
Idris-dev/src/Idris/Transforms.hs
96 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
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' -> tm'
52 _ -> App (applyAll extra ts f)
53 (applyAll extra ts a)
54applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)
55 (applyAll extra ts sc)
56applyAll extra ts t = t
58applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
59applyFnRules [] tm = Nothing
60applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
61 | otherwise = applyFnRules rs tm
63applyRule :: (Term, Term) -> Term -> Maybe Term
64applyRule (lhs, rhs) tm
65 | Just ms <- matchTerm lhs tm
66-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
67-- "\n" ++ show rhs
68-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
69 = Just $ depat ms rhs
70 | otherwise = Nothing
71 where depat ms (Bind n (PVar t) sc)
72 = case lookup n ms of
73 Just tm -> depat ms (subst n tm sc)
74 _ -> depat ms sc -- no occurrence? Shouldn't happen
75 depat ms tm = tm
77matchTerm :: Term -> Term -> Maybe [(Name, Term)]
78matchTerm lhs tm = matchVars [] lhs tm
79 where
80 matchVars acc (Bind n (PVar t) sc) tm
81 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
82 matchVars acc sc tm
83 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
84 doMatch acc sc tm
86 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
87 doMatch ns (P _ n _) tm
88 | n `elem` ns = return [(n, tm)]
89 doMatch ns (App f a) (App f' a')
90 = do fm <- doMatch ns f f'
91 am <- doMatch ns a a'
92 return (fm ++ am)
93 doMatch ns x y | x == y = return []
94 | otherwise = Nothing