@@ -0,0 +1,44 @@
1+{-# LANGUAGE PatternGuards #-}
3+module Idris.Transforms where
9+class Transform a where
10+ transform :: (a -> a) -> a -> a
12+instance Transform (TT Name) where
13+ transform t x = t (trans' x) where
14+ trans' (Bind n b sc) = Bind n (fmap (transform t) b) (transform t sc)
15+ trans' (App f a) = App (transform t f) (transform t a)
18+type TTOpt = TT Name -> TT Name
20+optimisations :: [TTOpt]
21+optimisations = [zero, suc]
23+instance Transform SC where
24+ transform t x = t (trans' x) where
25+ trans' (Case n alts) = Case n (map transAlt alts)
28+ transAlt (ConCase n i as sc) = ConCase n i as (trans' sc)
29+ transAlt (ConstCase c sc) = ConstCase c (trans' sc)
30+ transAlt (DefaultCase sc) = DefaultCase (trans' sc)
32+type CaseOpt = SC -> SC
35+zero (P _ n _) | n == NS (UN "O") ["nat","prelude"]
40+suc (App (P _ s _) a) | s == NS (UN "S") ["nat","prelude"]
41+ = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]