git.iko.soy/Idris-dev
on 2be265d help sign in
Idris-dev/src/Idris/Transforms.hs
112 lines 4.4 kB history raw
1{-|
2Module : Idris.Transforms
3Description : A collection of transformations.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE PatternGuards #-}
11module Idris.Transforms(
12 transformPats
13 , transformPatsWith
14 , applyTransRulesWith
15 , applyTransRules
16 ) where
18import Idris.AbsSyntax
19import Idris.Core.CaseTree
20import Idris.Core.TT
22import Debug.Trace
24transformPats :: IState -> [Either Term (Term, Term)] ->
25 [Either Term (Term, Term)]
26transformPats ist ps = map tClause ps where
27 tClause (Left t) = Left t -- not a clause, leave it alone
28 tClause (Right (lhs, rhs)) -- apply transforms on RHS
29 = let rhs' = applyTransRules ist rhs in
30 Right (lhs, rhs')
32transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->
33 [Either Term (Term, Term)]
34transformPatsWith rs ps = map tClause ps where
35 tClause (Left t) = Left t -- not a clause, leave it alone
36 tClause (Right (lhs, rhs)) -- apply transforms on RHS
37 = let rhs' = applyTransRulesWith rs rhs in
38 Right (lhs, rhs')
40-- | Work on explicitly named terms, so we don't have to manipulate de
41-- Bruijn indices
42applyTransRules :: IState -> Term -> Term
43applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)
45-- | Work on explicitly named terms, so we don't have to manipulate de
46-- Bruijn indices
47applyTransRulesWith :: [(Term, Term)] -> Term -> Term
48applyTransRulesWith rules tm
49 = finalise $ applyAll rules emptyContext (vToP tm)
51applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
52applyAll extra ts ap@(App s f a)
53 | (P _ fn ty, args) <- unApply ap
54 = let rules = case lookupCtxtExact fn ts of
55 Just r -> extra ++ r
56 Nothing -> extra
57 ap' = App s (applyAll extra ts f) (applyAll extra ts a) in
58 case rules of
59 [] -> ap'
60 rs -> case applyFnRules rs ap of
61 Just tm'@(App s f' a') ->
62 App s (applyAll extra ts f')
63 (applyAll extra ts a')
64 Just tm' -> tm'
65 _ -> App s (applyAll extra ts f)
66 (applyAll extra ts a)
67applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)
68 (applyAll extra ts sc)
69applyAll extra ts t = t
71applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
72applyFnRules [] tm = Nothing
73applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
74 | otherwise = applyFnRules rs tm
76applyRule :: (Term, Term) -> Term -> Maybe Term
77applyRule (lhs, rhs) tm
78 | Just ms <- matchTerm lhs tm
79-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
80-- "\n" ++ show rhs
81-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
82 = Just $ depat ms rhs
83 | otherwise = Nothing
84-- ASSUMPTION: The names in the transformation rule bindings cannot occur
85-- in the term being transformed.
86-- (In general, this would not be true, but when we elaborate transformation
87-- rules we mangle the names so that it is true. While this feels a bit
88-- hacky, it's much easier to think about than mangling de Bruijn indices).
89 where depat ms (Bind n (PVar t) sc)
90 = case lookup n ms of
91 Just tm -> depat ms (subst n tm sc)
92 _ -> depat ms sc -- no occurrence? Shouldn't happen
93 depat ms tm = tm
95matchTerm :: Term -> Term -> Maybe [(Name, Term)]
96matchTerm lhs tm = matchVars [] lhs tm
97 where
98 matchVars acc (Bind n (PVar t) sc) tm
99 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
100 matchVars acc sc tm
101 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
102 doMatch acc sc tm
104 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
105 doMatch ns (P _ n _) tm
106 | n `elem` ns = return [(n, tm)]
107 doMatch ns (App _ f a) (App _ f' a')
108 = do fm <- doMatch ns f f'
109 am <- doMatch ns a a'
110 return (fm ++ am)
111 doMatch ns x y | vToP x == vToP y = return []
112 | otherwise = Nothing