From 2455b73559560a24205f3c8d32ab86736a3cc5e8 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 28 Nov 2005 21:24:31 +0000 Subject: [PATCH] Changed exp.tr to use layout syntax and the Cat type. --- transfer/examples/exp.tr | 49 ++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 25 deletions(-) diff --git a/transfer/examples/exp.tr b/transfer/examples/exp.tr index b7202fedf..980c5d724 100644 --- a/transfer/examples/exp.tr +++ b/transfer/examples/exp.tr @@ -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; - } ;