@@ -0,0 +1,44 @@
1+{-# LANGUAGE PatternGuards #-}
2+
3+module Idris.Transforms where
4+
5+import Idris.AbsSyntax
6+import Core.CaseTree
7+import Core.TT
8+
9+class Transform a where
10+ transform :: (a -> a) -> a -> a
11+
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)
16+ trans' x = x
17+
18+type TTOpt = TT Name -> TT Name
19+
20+optimisations :: [TTOpt]
21+optimisations = [zero, suc]
22+
23+instance Transform SC where
24+ transform t x = t (trans' x) where
25+ trans' (Case n alts) = Case n (map transAlt alts)
26+ trans' t = t
27+
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)
31+
32+type CaseOpt = SC -> SC
33+
34+zero :: TTOpt
35+zero (P _ n _) | n == NS (UN "O") ["nat","prelude"]
36+ = Constant (BI 0)
37+zero x = x
38+
39+suc :: TTOpt
40+suc (App (P _ s _) a) | s == NS (UN "S") ["nat","prelude"]
41+ = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]
42+suc x = x
43+
44+