git.iko.soy/Idris-dev
on bd8ea0a help sign in
Idris-dev/src/Idris/Transforms.hs
109 lines 4.3 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.TT
21transformPats :: IState -> [Either Term (Term, Term)] ->
22 [Either Term (Term, Term)]
23transformPats ist ps = map tClause ps where
24 tClause (Left t) = Left t -- not a clause, leave it alone
25 tClause (Right (lhs, rhs)) -- apply transforms on RHS
26 = let rhs' = applyTransRules ist rhs in
27 Right (lhs, rhs')
29transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->
30 [Either Term (Term, Term)]
31transformPatsWith rs ps = map tClause ps where
32 tClause (Left t) = Left t -- not a clause, leave it alone
33 tClause (Right (lhs, rhs)) -- apply transforms on RHS
34 = let rhs' = applyTransRulesWith rs rhs in
35 Right (lhs, rhs')
37-- | Work on explicitly named terms, so we don't have to manipulate de
38-- Bruijn indices
39applyTransRules :: IState -> Term -> Term
40applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)
42-- | Work on explicitly named terms, so we don't have to manipulate de
43-- Bruijn indices
44applyTransRulesWith :: [(Term, Term)] -> Term -> Term
45applyTransRulesWith rules tm
46 = finalise $ applyAll rules emptyContext (vToP tm)
48applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term
49applyAll extra ts ap@(App s f a)
50 | (P _ fn ty, args) <- unApply ap
51 = let rules = case lookupCtxtExact fn ts of
52 Just r -> extra ++ r
53 Nothing -> extra
54 ap' = App s (applyAll extra ts f) (applyAll extra ts a) in
55 case rules of
56 [] -> ap'
57 rs -> case applyFnRules rs ap of
58 Just tm'@(App s f' a') ->
59 App s (applyAll extra ts f')
60 (applyAll extra ts a')
61 Just tm' -> tm'
62 _ -> App s (applyAll extra ts f)
63 (applyAll extra ts a)
64applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)
65 (applyAll extra ts sc)
66applyAll extra ts t = t
68applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
69applyFnRules [] tm = Nothing
70applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
71 | otherwise = applyFnRules rs tm
73applyRule :: (Term, Term) -> Term -> Maybe Term
74applyRule (lhs, rhs) tm
75 | Just ms <- matchTerm lhs tm
76-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
77-- "\n" ++ show rhs
78-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $
79 = Just $ depat ms rhs
80 | otherwise = Nothing
81-- ASSUMPTION: The names in the transformation rule bindings cannot occur
82-- in the term being transformed.
83-- (In general, this would not be true, but when we elaborate transformation
84-- rules we mangle the names so that it is true. While this feels a bit
85-- hacky, it's much easier to think about than mangling de Bruijn indices).
86 where depat ms (Bind n (PVar _ t) sc)
87 = case lookup n ms of
88 Just tm -> depat ms (subst n tm sc)
89 _ -> depat ms sc -- no occurrence? Shouldn't happen
90 depat ms tm = tm
92matchTerm :: Term -> Term -> Maybe [(Name, Term)]
93matchTerm lhs tm = matchVars [] lhs tm
94 where
95 matchVars acc (Bind n (PVar _ t) sc) tm
96 = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
97 matchVars acc sc tm
98 = -- trace (show acc ++ ": " ++ show (sc, tm)) $
99 doMatch acc sc tm
101 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
102 doMatch ns (P _ n _) tm
103 | n `elem` ns = return [(n, tm)]
104 doMatch ns (App _ f a) (App _ f' a')
105 = do fm <- doMatch ns f f'
106 am <- doMatch ns a a'
107 return (fm ++ am)
108 doMatch ns x y | vToP x == vToP y = return []
109 | otherwise = Nothing