git.iko.soy/Idris-dev
on 86e32fb help sign in
Idris-dev/src/Idris/Transforms.hs
57 lines 1.8 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Transforms where
5import Idris.AbsSyntax
6import Core.CaseTree
7import Core.TT
9data TTOpt = TermTrans (TT Name -> TT Name) -- term transform
10 | CaseTrans (SC -> SC) -- case expression transform
12class Transform a where
13 transform :: TTOpt -> a -> a
15instance Transform (TT Name) where
16 transform o@(TermTrans t) tm = trans t tm where
17 trans t (Bind n b tm) = t $ Bind n (transform o b) (trans t tm)
18 trans t (App f a) = t $ App (trans t f) (trans t a)
19 trans t tm = t tm
20 transform _ tm = tm
22instance Transform a => Transform (Binder a) where
23 transform t (Let ty v) = Let (transform t ty) (transform t v)
24 transform t b = b { binderTy = transform t (binderTy b) }
26instance Transform SC where
27 transform o@(CaseTrans t) sc = trans t sc where
28 trans t (Case n alts) = t (Case n (map (transform o) alts))
29 trans t x = t x
30 transform o@(TermTrans t) sc = trans t sc where
31 trans t (Case n alts) = Case n (map (transform o) alts)
32 trans t (STerm tm) = STerm (t tm)
33 trans t x = x
35instance Transform CaseAlt where
36 transform o (ConCase n i ns sc) = ConCase n i ns (transform o sc)
37 transform o (ConstCase c sc) = ConstCase c (transform o sc)
38 transform o (DefaultCase sc) = DefaultCase (transform o sc)
40natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]
42zname = NS (UN "Z") ["Nat","Prelude"]
43sname = NS (UN "S") ["Nat","Prelude"]
45zero :: TT Name -> TT Name
46zero (P _ n _) | n == zname
47 = Constant (BI 0)
48zero x = x
50suc :: TT Name -> TT Name
51suc (App (P _ s _) a) | s == sname
52 = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]
53suc x = x
55natcase :: SC -> SC
56natcase = undefined