transfer/examples/exp.tr


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

data Stm : Type where {} ;
data Exp : Type where {} ;
data Var : Type where {} ;
data Typ : Type where {} ;

data ListStm : Type where {} ;

data Tree : Type -> 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;
                 } ;