git.iko.soy/Idris-dev
on 02003d7 help sign in
Idris-dev/src/Idris/Transforms.hs
44 lines 1.1 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Transforms where
5import Idris.AbsSyntax
6import Core.CaseTree
7import Core.TT
9class Transform a where
10 transform :: (a -> a) -> a -> a
12instance 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
18type TTOpt = TT Name -> TT Name
20optimisations :: [TTOpt]
21optimisations = [zero, suc]
23instance 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
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)
32type CaseOpt = SC -> SC
34zero :: TTOpt
35zero (P _ n _) | n == NS (UN "O") ["nat","prelude"]
36 = Constant (BI 0)
37zero x = x
39suc :: TTOpt
40suc (App (P _ s _) a) | s == NS (UN "S") ["nat","prelude"]
41 = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]
42suc x = x