msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

gfcc in Types

Browse Source
This commit is contained in:
aarne
2004-12-20 07:57:05 +00:00
parent 8caa3ed737
commit 6e1f41b26a
7 changed files with 125 additions and 153 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
examples/gfcc/Imper.gf
View File

@@ -4,10 +4,9 @@ abstract Imper = {
Program ;
Rec ListTyp ;
Typ ;
NumTyp ;
IsNum Typ ;
ListTyp ;
Fun ListTyp Typ ;
Body ListTyp ;
Stm ;
Exp Typ ;
Var Typ ;
@@ -25,8 +24,8 @@ abstract Imper = {
Decl : (A : Typ) -> (Var A -> Stm) -> Stm ;
Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ;
While : Exp (TNum TInt) -> Stm -> Stm -> Stm ;
IfElse : Exp (TNum TInt) -> Stm -> Stm -> Stm -> Stm ;
While : Exp TInt -> Stm -> Stm -> Stm ;
IfElse : Exp TInt -> Stm -> Stm -> Stm -> Stm ;
Block : Stm -> Stm -> Stm ;
Printf : (A : Typ) -> Exp A -> Stm -> Stm ;
Return : (A : Typ) -> Exp A -> Stm ;
@@ -34,15 +33,15 @@ abstract Imper = {
End : Stm ;
EVar : (A : Typ) -> Var A -> Exp A ;
EInt : Int -> Exp (TNum TInt) ;
EFloat : Int -> Int -> Exp (TNum TFloat) ;
ELt : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Exp (TNum TInt) ;
EAdd, EMul, ESub : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Ex ;
EInt : Int -> Exp TInt ;
EFloat : Int -> Int -> Exp TFloat ;
ELt : (n : Typ) -> IsNum n -> Exp n -> Exp n -> Exp TInt ;
EAdd, EMul, ESub : (n : Typ) -> IsNum n -> Exp n -> Exp n -> Exp n ;
EAppNil : (V : Typ) -> Fun NilTyp V -> Exp V ;
EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ;
TNum : NumTyp -> Typ ;
TInt, TFloat : NumTyp ;
TInt, TFloat : Typ ;
isNumInt : IsNum TInt ; isNumFloat : IsNum TFloat ;
NilTyp : ListTyp ;
ConsTyp : Typ -> ListTyp -> ListTyp ;