forked from GitHub/gf-core
Changed exp.tr to use layout syntax and the Cat type.
This commit is contained in:
@@ -1,31 +1,30 @@
|
||||
data Stm : Type where {} ;
|
||||
data Exp : Type where {} ;
|
||||
data Var : Type where {} ;
|
||||
data Typ : Type where {} ;
|
||||
data Cat : Type where
|
||||
Stm : Cat
|
||||
Exp : Cat
|
||||
Var : Cat
|
||||
Typ : Cat
|
||||
ListStm : Cat
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
NilStm : Tree ListStm ;
|
||||
ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm ;
|
||||
} ;
|
||||
derive composOp Tree
|
||||
|
||||
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
|
||||
|
||||
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;
|
||||
} ;
|
||||
|
||||
|
||||
Reference in New Issue
Block a user