Putting def definitions in place.

This commit is contained in:
aarne
2003-10-01 12:46:44 +00:00
parent 8ed7749eb6
commit c985dab565
20 changed files with 152 additions and 52 deletions

View File

@@ -24,7 +24,7 @@ type SourceCnc = Module Ident Option Info
-- judgements in abstract syntax
data Info =
AbsCat (Perh Context) (Perh [Fun]) -- constructors
AbsCat (Perh Context) (Perh [Term]) -- constructors; must be Id or QId
| AbsFun (Perh Type) (Perh Term) -- Yes f = canonical
| AbsTrans Ident
@@ -55,6 +55,7 @@ data Term =
Vr Ident -- variable
| Cn Ident -- constant
| Con Ident -- constructor
| EData -- to mark in definition that a fun is a constructor
| Sort String -- basic type
| EInt Int -- integer literal
| K String -- string literal or token: "foo"
@@ -68,8 +69,6 @@ data Term =
-- only used in internal representation
| Typed Term Term -- type-annotated term
| ECase Term [Branch] -- case expression in abstract syntax à la Alfa
-- below this only for concrete syntax
| RecType [Labelling] -- record type: { p : A ; ...}
| R [Assign] -- record: { p = a ; ...}