mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 19:42:50 -06:00
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 Cat : Type where
|
||||||
data Exp : Type where {} ;
|
Stm : Cat
|
||||||
data Var : Type where {} ;
|
Exp : Cat
|
||||||
data Typ : Type where {} ;
|
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 {
|
NilStm : Tree ListStm
|
||||||
SDecl : Tree Typ -> Tree Var -> Tree Stm ;
|
ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm
|
||||||
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 ;
|
derive composOp Tree
|
||||||
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
|
||||||
|
|
||||||
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