blob: d6c077c03335320a48061bbc34e11d155348cbba (
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
|
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 composOp Tree
rename : (String -> String) -> (C : Type) -> Tree C -> Tree C
rename f C t = case t of
V x -> V (f x)
_ -> composOp_Tree C (rename f) t
|
