blob: e54b820550a8196da9f3656e1714f4d1cf1751a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
import prelude
data Cat : Type where
Stm : Cat
Exp : Cat
Var : Cat
Typ : Cat
ListStm : Cat
data Tree : Cat -> Type where
SDecl : Tree Typ -> Tree Var -> Tree Stm
SAss : Tree Var -> Tree Exp -> Tree Stm
SBlock : Tree ListStm -> Tree Stm
EAdd : Tree Exp -> Tree Exp -> Tree Exp
EStm : Tree Stm -> Tree Exp
EVar : Tree Var -> Tree Exp
EInt : Integer -> Tree Exp
V : String -> Tree Var
TInt : Tree Typ
TFloat : Tree Typ
NilStm : Tree ListStm
ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm
derive Compos Tree
rename : (String -> String) -> (C : Type) -> Tree C -> Tree C
rename f C t = case t of
V x -> V (f x)
_ -> composOp ? ? compos_Tree C (rename f) t
main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2)))
|
