From 155afdf9b76e37f4daed6d7d48dfd9e56844964f Mon Sep 17 00:00:00 2001
From: "kr.angelov" <kr.angelov@gmail.com>
Date: Thu, 27 Jun 2013 09:39:15 +0000
Subject: [PATCH] a complete Python API for reading, printing and manipulation
 of abstract trees and types. This includes dependent types, high-order
 abstract syntax and implicit arguments

---
 src/runtime/c/pgf/expr.c            | 607 +++++++++++++++++++++++++---
 src/runtime/c/pgf/expr.h            |  30 +-
 src/runtime/c/pgf/pgf.c             |  11 +
 src/runtime/c/pgf/pgf.h             |   3 +
 src/runtime/c/pgf/printer.c         |  14 +-
 src/runtime/c/pgf/reader.c          |  28 +-
 src/runtime/c/utils/pgf-parse.c     |   2 +-
 src/runtime/c/utils/pgf-translate.c |   2 +-
 src/runtime/python/pypgf.c          | 532 +++++++++++++++++++++++-
 9 files changed, 1148 insertions(+), 81 deletions(-)

diff --git a/src/runtime/c/pgf/expr.c b/src/runtime/c/pgf/expr.c
index 170751b8b..bcbfa0d09 100644
--- a/src/runtime/c/pgf/expr.c
+++ b/src/runtime/c/pgf/expr.c
@@ -88,7 +88,7 @@ GU_DEFINE_TYPE(PgfLiteral, GuVariant,
 GU_DECLARE_TYPE(PgfType, struct);
 
 GU_DEFINE_TYPE(PgfHypo, struct,
-	       GU_MEMBER(PgfHypo, bindtype, PgfBindType),
+	       GU_MEMBER(PgfHypo, bind_type, PgfBindType),
 	       GU_MEMBER(PgfHypo, cid, PgfCId),
 	       GU_MEMBER_P(PgfHypo, type, PgfType));
 
@@ -137,7 +137,16 @@ typedef struct PgfExprParser PgfExprParser;
 typedef enum {
 	PGF_TOKEN_LPAR,
 	PGF_TOKEN_RPAR,
+	PGF_TOKEN_LCURLY,
+	PGF_TOKEN_RCURLY,
 	PGF_TOKEN_QUESTION,
+	PGF_TOKEN_LAMBDA,
+	PGF_TOKEN_RARROW,
+	PGF_TOKEN_LTRIANGLE,
+	PGF_TOKEN_RTRIANGLE,
+	PGF_TOKEN_COMMA,
+	PGF_TOKEN_COLON,
+	PGF_TOKEN_WILD,
 	PGF_TOKEN_IDENT,
 	PGF_TOKEN_INT,
 	PGF_TOKEN_FLT,
@@ -172,11 +181,6 @@ pgf_expr_parser_token(PgfExprParser* parser)
 	while (isspace(parser->ch)) {
 		pgf_expr_parser_getc(parser);
 	}
-	
-	if (parser->tmp_pool != NULL) {
-		gu_pool_free(parser->tmp_pool);
-		parser->tmp_pool = NULL;
-	}
 
 	parser->token_tag   = PGF_TOKEN_UNKNOWN;
 	parser->token_value = gu_null_seq;
@@ -193,12 +197,50 @@ pgf_expr_parser_token(PgfExprParser* parser)
 		pgf_expr_parser_getc(parser);
 		parser->token_tag = PGF_TOKEN_RPAR;
 		break;
+	case '{':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_LCURLY;
+		break;
+	case '}':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_RCURLY;
+		break;
+	case '<':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_LTRIANGLE;
+		break;
+	case '>':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_RTRIANGLE;
+		break;
 	case '?':
 		pgf_expr_parser_getc(parser);
 		parser->token_tag = PGF_TOKEN_QUESTION;
 		break;
+	case '\\':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_LAMBDA;
+		break;
+	case '-':
+		pgf_expr_parser_getc(parser);
+		if (parser->ch == '>') {
+			pgf_expr_parser_getc(parser);
+			parser->token_tag = PGF_TOKEN_RARROW;
+		}
+		break;
+	case ',':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_COMMA;
+		break;
+	case ':':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_COLON;
+		break;
+	case '_':
+		pgf_expr_parser_getc(parser);
+		parser->token_tag = PGF_TOKEN_WILD;
+		break;
 	default: {
-		parser->tmp_pool = gu_new_pool();
 		GuCharBuf* chars = gu_new_buf(char, parser->tmp_pool);
 
 		if (isalpha(parser->ch)) {
@@ -249,9 +291,22 @@ pgf_expr_parser_token(PgfExprParser* parser)
 	}
 }
 
+static bool
+pgf_expr_parser_lookahead(PgfExprParser* parser, int ch)
+{
+	while (isspace(parser->ch)) {
+		pgf_expr_parser_getc(parser);
+	}
+	
+	return (parser->ch == ch);
+}
+
 static PgfExpr
 pgf_expr_parser_expr(PgfExprParser* parser);
 
+static PgfType*
+pgf_expr_parser_type(PgfExprParser* parser);
+
 static PgfExpr
 pgf_expr_parser_term(PgfExprParser* parser)
 {
@@ -266,6 +321,27 @@ pgf_expr_parser_term(PgfExprParser* parser)
 			return gu_null_variant;
 		}
 	}
+	case PGF_TOKEN_LTRIANGLE: {
+		pgf_expr_parser_token(parser);
+		PgfExpr expr = pgf_expr_parser_expr(parser);
+		
+		if (parser->token_tag != PGF_TOKEN_COLON) {
+			return gu_null_variant;
+		}
+		pgf_expr_parser_token(parser);
+
+		PgfType* type = pgf_expr_parser_type(parser);
+
+		if (parser->token_tag != PGF_TOKEN_RTRIANGLE) {
+			return gu_null_variant;
+		}
+		pgf_expr_parser_token(parser);
+
+		return gu_new_variant_i(parser->expr_pool,
+					PGF_EXPR_TYPED,
+					PgfExprTyped,
+					expr, type);
+	}
 	case PGF_TOKEN_QUESTION: {
 		pgf_expr_parser_token(parser);
 		return gu_new_variant_i(parser->expr_pool,
@@ -333,41 +409,354 @@ pgf_expr_parser_term(PgfExprParser* parser)
 	}
 }
 
+static PgfExpr
+pgf_expr_parser_arg(PgfExprParser* parser)
+{
+	PgfExpr arg;
+
+	if (parser->token_tag == PGF_TOKEN_LCURLY) {
+		pgf_expr_parser_token(parser);
+
+		arg = pgf_expr_parser_expr(parser);
+		if (gu_variant_is_null(arg))
+			return gu_null_variant;
+
+		if (parser->token_tag != PGF_TOKEN_RCURLY) {
+			return gu_null_variant;
+		}
+
+		pgf_expr_parser_token(parser);
+
+		arg = gu_new_variant_i(parser->expr_pool,
+				  PGF_EXPR_IMPL_ARG,
+				  PgfExprImplArg,
+				  arg);
+	} else {
+		arg = pgf_expr_parser_term(parser);
+	}
+
+	return arg;
+}
+
+static bool
+pgf_expr_parser_bind(PgfExprParser* parser, GuBuf* binds)
+{
+	PgfCId var;
+	PgfBindType bind_type = PGF_BIND_TYPE_EXPLICIT;
+
+	if (parser->token_tag == PGF_TOKEN_LCURLY) {
+		bind_type = PGF_BIND_TYPE_IMPLICIT;
+		pgf_expr_parser_token(parser);
+	}
+
+	for (;;) {
+		if (parser->token_tag == PGF_TOKEN_IDENT) {
+			char* str = 
+				gu_chars_str(parser->token_value, parser->tmp_pool);
+			var = gu_str_string(str, parser->expr_pool);
+			pgf_expr_parser_token(parser);
+		} else if (parser->token_tag == PGF_TOKEN_WILD) {
+			var = gu_str_string("_", parser->expr_pool);
+			pgf_expr_parser_token(parser);
+		} else {
+			return false;
+		}
+
+		PgfExpr bind =
+			gu_new_variant_i(parser->expr_pool,
+								PGF_EXPR_ABS,
+								PgfExprAbs,
+								bind_type,
+								var,
+								gu_null_variant);
+		gu_buf_push(binds, PgfExpr, bind);
+		
+		if (bind_type == PGF_BIND_TYPE_EXPLICIT ||
+		    parser->token_tag != PGF_TOKEN_COMMA) {
+			break;
+		}
+		
+		pgf_expr_parser_token(parser);
+	}
+
+	if (bind_type == PGF_BIND_TYPE_IMPLICIT) {
+		if (parser->token_tag != PGF_TOKEN_RCURLY)
+			return false;
+		pgf_expr_parser_token(parser);
+	}
+
+	return true;
+}
+
+static GuBuf*
+pgf_expr_parser_binds(PgfExprParser* parser)
+{
+	GuBuf* binds = gu_new_buf(PgfExpr, parser->tmp_pool);
+
+	for (;;) {
+		if (!pgf_expr_parser_bind(parser, binds))
+			return NULL;
+
+		if (parser->token_tag != PGF_TOKEN_COMMA)
+			break;
+
+		pgf_expr_parser_token(parser);
+	}
+
+	return binds;
+}
+
 static PgfExpr
 pgf_expr_parser_expr(PgfExprParser* parser)
 {
-	PgfExpr expr = pgf_expr_parser_term(parser);
-	if (gu_variant_is_null(expr))
-		return expr;
+	if (parser->token_tag == PGF_TOKEN_LAMBDA) {
+		pgf_expr_parser_token(parser);
+		GuBuf* binds = pgf_expr_parser_binds(parser);
+		if (binds == NULL)
+			return gu_null_variant;
 
-	while (true) {
-		PgfExpr arg = pgf_expr_parser_term(parser);
-		if (gu_variant_is_null(arg)) {
-			return expr;
+		if (parser->token_tag != PGF_TOKEN_RARROW) {
+			return gu_null_variant;
 		}
-		expr = gu_new_variant_i(parser->expr_pool,
-					PGF_EXPR_APP,
-					PgfExprApp,
-					expr, arg);
+		pgf_expr_parser_token(parser);
+
+		PgfExpr expr = pgf_expr_parser_expr(parser);
+		if (gu_variant_is_null(expr))
+			return gu_null_variant;
+
+		size_t n_binds = gu_buf_length(binds);
+		for (size_t i = n_binds; i > 0; i--) {
+			PgfExpr bind = gu_buf_get(binds, PgfExpr, i-1);
+
+			((PgfExprAbs*) gu_variant_data(bind))->body = expr;
+			expr = bind;
+		}
+
+		return expr;
+	} else {
+		PgfExpr expr = pgf_expr_parser_term(parser);
+		if (gu_variant_is_null(expr))
+			return gu_null_variant;
+
+		while (parser->token_tag != PGF_TOKEN_EOF &&
+		       parser->token_tag != PGF_TOKEN_RPAR &&
+		       parser->token_tag != PGF_TOKEN_RCURLY &&
+		       parser->token_tag != PGF_TOKEN_RTRIANGLE &&
+		       parser->token_tag != PGF_TOKEN_COLON) {
+			PgfExpr arg = pgf_expr_parser_arg(parser);
+			if (gu_variant_is_null(arg))
+				return gu_null_variant;
+
+			expr = gu_new_variant_i(parser->expr_pool,
+						PGF_EXPR_APP,
+						PgfExprApp,
+						expr, arg);
+		}
+		
+		return expr;
 	}
 }
 
+static bool
+pgf_expr_parser_hypos(PgfExprParser* parser, GuBuf* hypos)
+{
+	PgfCId var;
+	PgfBindType bind_type = PGF_BIND_TYPE_EXPLICIT;
+
+	for (;;) {
+		if (bind_type == PGF_BIND_TYPE_EXPLICIT &&
+		    parser->token_tag == PGF_TOKEN_LCURLY) {
+			bind_type = PGF_BIND_TYPE_IMPLICIT;
+			pgf_expr_parser_token(parser);
+		}
+
+		if (parser->token_tag == PGF_TOKEN_IDENT) {
+			char* str = 
+				gu_chars_str(parser->token_value, parser->tmp_pool);
+			var = gu_str_string(str, parser->expr_pool);
+			pgf_expr_parser_token(parser);
+		} else if (parser->token_tag == PGF_TOKEN_WILD) {
+			var = gu_str_string("_", parser->expr_pool);
+			pgf_expr_parser_token(parser);
+		} else {
+			return false;
+		}
+
+		PgfHypo* hypo = gu_buf_extend(hypos);
+		hypo->bind_type = bind_type;
+		hypo->cid = var;
+		hypo->type = NULL;
+
+		if (bind_type == PGF_BIND_TYPE_IMPLICIT &&
+			parser->token_tag == PGF_TOKEN_RCURLY) {
+			bind_type = PGF_BIND_TYPE_EXPLICIT;
+			pgf_expr_parser_token(parser);
+		}
+
+		if (parser->token_tag != PGF_TOKEN_COMMA) {
+			break;
+		}
+		
+		pgf_expr_parser_token(parser);
+	}
+
+	if (bind_type == PGF_BIND_TYPE_IMPLICIT)
+		return false;
+
+	return true;
+}
+
+static PgfType*
+pgf_expr_parser_atom(PgfExprParser* parser)
+{
+	if (parser->token_tag != PGF_TOKEN_IDENT)
+		return NULL;
+
+	char* str =
+		gu_chars_str(parser->token_value, parser->tmp_pool);
+	PgfCId cid = gu_str_string(str, parser->expr_pool);
+	pgf_expr_parser_token(parser);
+
+	GuBuf* args = gu_new_buf(PgfExpr, parser->tmp_pool);
+	while (parser->token_tag != PGF_TOKEN_EOF &&
+		   parser->token_tag != PGF_TOKEN_RPAR &&
+		   parser->token_tag != PGF_TOKEN_RTRIANGLE &&
+		   parser->token_tag != PGF_TOKEN_RARROW) {
+		PgfExpr arg =
+			pgf_expr_parser_arg(parser);
+		if (gu_variant_is_null(arg))
+			return NULL;
+			
+		gu_buf_push(args, PgfExpr, arg);
+	}
+
+	size_t n_exprs = gu_buf_length(args);
+
+	PgfType* type = gu_new_flex(parser->expr_pool, PgfType, exprs, n_exprs);
+	type->hypos   = gu_empty_seq();
+	type->cid     = cid;
+	type->n_exprs = n_exprs;
+
+	for (size_t i = 0; i < n_exprs; i++) {
+		type->exprs[i] = gu_buf_get(args, PgfExpr, i);
+	}
+	
+	return type;
+}
+
+static PgfType*
+pgf_expr_parser_type(PgfExprParser* parser)
+{
+	PgfType* type = NULL;
+	GuBuf* hypos = gu_new_buf(PgfHypo, parser->expr_pool);
+
+	for (;;) {
+		if (parser->token_tag == PGF_TOKEN_LPAR) {
+			pgf_expr_parser_token(parser);
+
+			size_t n_start = gu_buf_length(hypos);
+
+			if ((parser->token_tag == PGF_TOKEN_IDENT &&
+			     (pgf_expr_parser_lookahead(parser, ',') || 
+				  pgf_expr_parser_lookahead(parser, ':'))) ||
+				(parser->token_tag == PGF_TOKEN_LCURLY) ||
+				(parser->token_tag == PGF_TOKEN_WILD)) {
+
+				if (!pgf_expr_parser_hypos(parser, hypos))
+					return NULL;
+
+				if (parser->token_tag != PGF_TOKEN_COLON)
+					return NULL;
+
+				pgf_expr_parser_token(parser);
+			} else {
+				PgfHypo* hypo = gu_buf_extend(hypos);
+				hypo->bind_type = PGF_BIND_TYPE_EXPLICIT;
+				hypo->cid = gu_str_string("_", parser->expr_pool);
+				hypo->type = NULL;
+			}
+
+			size_t n_end = gu_buf_length(hypos);
+
+			PgfType* type = pgf_expr_parser_type(parser);
+			if (type == NULL)
+				return NULL;
+
+			if (parser->token_tag != PGF_TOKEN_RPAR)
+				return NULL;
+
+			pgf_expr_parser_token(parser);
+
+			if (parser->token_tag != PGF_TOKEN_RARROW)
+				return NULL;
+
+			pgf_expr_parser_token(parser);
+			
+			for (size_t i = n_start; i < n_end; i++) {
+				PgfHypo* hypo = gu_buf_index(hypos, PgfHypo, i);
+				hypo->type = type;
+			}
+		} else {
+			type = pgf_expr_parser_atom(parser);
+			if (type == NULL)
+				return NULL;
+
+			if (parser->token_tag != PGF_TOKEN_RARROW)
+				break;
+
+			pgf_expr_parser_token(parser);
+
+			PgfHypo* hypo = gu_buf_extend(hypos);
+			hypo->bind_type = PGF_BIND_TYPE_EXPLICIT;
+			hypo->cid = gu_str_string("_", parser->expr_pool);
+			hypo->type = type;
+		}
+	}
+
+	type->hypos = gu_buf_seq(hypos);
+
+	return type;
+}
+
+static PgfExprParser*
+pgf_new_parser(GuIn* in, GuPool* pool, GuPool* tmp_pool, GuExn* err)
+{
+	PgfExprParser* parser = gu_new(PgfExprParser, tmp_pool);
+	parser->err = err;
+	parser->in = in;
+	parser->expr_pool = pool;
+	parser->tmp_pool = tmp_pool;
+	parser->ch = ' ';
+	pgf_expr_parser_token(parser);
+	return parser;
+}
+
 PgfExpr
 pgf_read_expr(GuIn* in, GuPool* pool, GuExn* err)
 {
 	GuPool* tmp_pool = gu_new_pool();
-	PgfExprParser* parser = gu_new(PgfExprParser, tmp_pool);
-	parser->err = err;
-	parser->in = in;
-	parser->expr_pool = pool;
-	parser->tmp_pool = NULL;
-	parser->ch = ' ';
-	pgf_expr_parser_token(parser);
+	PgfExprParser* parser = 
+		pgf_new_parser(in, pool, tmp_pool, err);
 	PgfExpr expr = pgf_expr_parser_expr(parser);
+	if (parser->token_tag != PGF_TOKEN_EOF)
+		return gu_null_variant;
 	gu_pool_free(tmp_pool);
 	return expr;
 }
 
+PgfType*
+pgf_read_type(GuIn* in, GuPool* pool, GuExn* err)
+{
+	GuPool* tmp_pool = gu_new_pool();
+	PgfExprParser* parser = 
+		pgf_new_parser(in, pool, tmp_pool, err);
+	PgfType* type = pgf_expr_parser_type(parser);
+	if (parser->token_tag != PGF_TOKEN_EOF)
+		return NULL;
+	gu_pool_free(tmp_pool);
+	return type;
+}
+
 bool
 pgf_literal_eq(PgfLiteral lit1, PgfLiteral lit2)
 {
@@ -470,14 +859,56 @@ pgf_print_literal(PgfLiteral lit,
 }
 
 void
-pgf_print_expr(PgfExpr expr, int prec,
-			  GuWriter* wtr, GuExn* err)
+pgf_print_expr(PgfExpr expr, PgfPrintContext* ctxt, int prec,
+               GuWriter* wtr, GuExn* err)
 {
 	GuVariantInfo ei = gu_variant_open(expr);
 	switch (ei.tag) {
-	case PGF_EXPR_FUN: {
-		PgfExprFun* fun = ei.data;
-		gu_string_write(fun->fun, wtr, err);
+	case PGF_EXPR_ABS: {
+		PgfExprAbs* abs = ei.data;
+
+		if (prec > 1) {
+			gu_puts("(", wtr, err);
+		}
+
+		gu_putc('\\', wtr, err);
+		
+		PgfPrintContext* new_ctxt = ctxt;
+
+		for (;;) {
+			if (abs->bind_type == PGF_BIND_TYPE_IMPLICIT) {
+				gu_putc('{', wtr, err);
+			}
+			gu_string_write(abs->id, wtr, err);
+			if (abs->bind_type == PGF_BIND_TYPE_IMPLICIT) {
+				gu_putc('}', wtr, err);
+			}
+
+			PgfPrintContext* c = malloc(sizeof(PgfPrintContext));
+			c->name = abs->id;
+			c->next = new_ctxt;
+			new_ctxt = c;
+
+			if (gu_variant_tag(abs->body) != PGF_EXPR_ABS)
+				break;
+				
+			gu_putc(',', wtr, err);
+			
+			abs = gu_variant_data(abs->body);
+		}
+
+		gu_puts(" -> ", wtr, err);
+		pgf_print_expr(abs->body, new_ctxt, 1, wtr, err);
+
+		while (new_ctxt != ctxt) {
+			PgfPrintContext* next = new_ctxt->next;
+			free(new_ctxt);
+			new_ctxt = next;
+		}
+
+		if (prec > 1) {
+			gu_puts(")", wtr, err);
+		}
 		break;
 	}
 	case PGF_EXPR_APP: {
@@ -485,9 +916,9 @@ pgf_print_expr(PgfExpr expr, int prec,
 		if (prec > 3) {
 			gu_puts("(", wtr, err);
 		}
-		pgf_print_expr(app->fun, 3, wtr, err);
+		pgf_print_expr(app->fun, ctxt, 3, wtr, err);
 		gu_puts(" ", wtr, err);
-		pgf_print_expr(app->arg, 4, wtr, err);
+		pgf_print_expr(app->arg, ctxt, 4, wtr, err);
 		if (prec > 3) {
 			gu_puts(")", wtr, err);
 		}
@@ -501,25 +932,57 @@ pgf_print_expr(PgfExpr expr, int prec,
 	case PGF_EXPR_META:
 		gu_putc('?', wtr, err);
 		break;
-	case PGF_EXPR_ABS:
-	case PGF_EXPR_VAR:
-	case PGF_EXPR_TYPED:
-	case PGF_EXPR_IMPL_ARG:
-		gu_impossible();
+	case PGF_EXPR_FUN: {
+		PgfExprFun* fun = ei.data;
+		gu_string_write(fun->fun, wtr, err);
 		break;
+	}
+	case PGF_EXPR_VAR: {
+		PgfExprVar* evar = ei.data;
+		
+		int var = evar->var;
+		PgfPrintContext* c = ctxt;
+		while (c != NULL && var > 0) {
+			c = ctxt->next;
+		}
+		
+		if (c == NULL) {
+			gu_printf(wtr, err, "#%d", evar->var);
+		} else {
+			gu_string_write(c->name, wtr, err);
+		}
+		break;
+	}
+	case PGF_EXPR_TYPED: {
+		PgfExprTyped* typed = ei.data;
+		gu_putc('<', wtr, err);
+		pgf_print_expr(typed->expr, ctxt, 0, wtr, err);
+		gu_puts(" : ", wtr, err);
+		pgf_print_type(typed->type, ctxt, 0, wtr, err);
+		gu_putc('>', wtr, err);
+		break;
+	}
+	case PGF_EXPR_IMPL_ARG: {
+		PgfExprImplArg* impl = ei.data;
+		gu_putc('{', wtr, err);
+		pgf_print_expr(impl->expr, ctxt, 0, wtr, err);
+		gu_putc('}', wtr, err);
+		break;
+	}
 	default:
 		gu_impossible();
 	}
 }
 
-void
-pgf_print_hypo(PgfHypo *hypo, int prec, GuWriter *wtr, GuExn *err)
+PgfPrintContext*
+pgf_print_hypo(PgfHypo *hypo, PgfPrintContext* ctxt, int prec,
+               GuWriter *wtr, GuExn *err)
 {
-    if (hypo->bindtype == PGF_BIND_TYPE_IMPLICIT) {
+    if (hypo->bind_type == PGF_BIND_TYPE_IMPLICIT) {
         gu_puts("({", wtr, err);
         gu_string_write(hypo->cid, wtr, err);
         gu_puts("} : ", wtr, err);
-        pgf_print_type(hypo->type, 0, wtr, err);
+        pgf_print_type(hypo->type, ctxt, 0, wtr, err);
         gu_puts(")", wtr, err);
     } else {
         GuPool* tmp_pool = gu_new_pool();
@@ -529,27 +992,34 @@ pgf_print_hypo(PgfHypo *hypo, int prec, GuWriter *wtr, GuExn *err)
             gu_puts("(", wtr, err);
             gu_string_write(hypo->cid, wtr, err);
             gu_puts(" : ", wtr, err);
-            pgf_print_type(hypo->type, 0, wtr, err);
+            pgf_print_type(hypo->type, ctxt, 0, wtr, err);
             gu_puts(")", wtr, err);
         } else {
-            pgf_print_type(hypo->type, prec, wtr, err);
+            pgf_print_type(hypo->type, ctxt, prec, wtr, err);
         }
         
         gu_pool_free(tmp_pool);
     }
+    
+	PgfPrintContext* new_ctxt = malloc(sizeof(PgfPrintContext));
+	new_ctxt->name = hypo->cid;
+	new_ctxt->next = ctxt;
+	return new_ctxt;
 }
 
 void
-pgf_print_type(PgfType *type, int prec, GuWriter *wtr, GuExn *err)
+pgf_print_type(PgfType *type, PgfPrintContext* ctxt, int prec,
+               GuWriter *wtr, GuExn *err)
 {
     size_t n_hypos = gu_seq_length(type->hypos);
     
     if (n_hypos > 0) {
 		if (prec > 0) gu_putc('(', wtr, err);
 		
+		PgfPrintContext* new_ctxt = ctxt;
 		for (size_t i = 0; i < n_hypos; i++) {
 			PgfHypo *hypo = gu_seq_index(type->hypos, PgfHypo, i);
-			pgf_print_hypo(hypo, 1, wtr, err);
+			new_ctxt = pgf_print_hypo(hypo, new_ctxt, 1, wtr, err);
 
 			gu_puts(" -> ", wtr, err);
 		}
@@ -558,9 +1028,15 @@ pgf_print_type(PgfType *type, int prec, GuWriter *wtr, GuExn *err)
     
 		for (size_t i = 0; i < type->n_exprs; i++) {
 			gu_puts(" ", wtr, err);
-			pgf_print_expr(type->exprs[i], 4, wtr, err);
+			pgf_print_expr(type->exprs[i], new_ctxt, 4, wtr, err);
 		}
-		
+
+		while (new_ctxt != ctxt) {
+			PgfPrintContext* next = new_ctxt->next;
+			free(new_ctxt);
+			new_ctxt = next;
+		}
+
 		if (prec > 0) gu_putc(')', wtr, err);
 	} else if (type->n_exprs > 0) {
 		if (prec > 3) gu_putc('(', wtr, err);
@@ -569,7 +1045,7 @@ pgf_print_type(PgfType *type, int prec, GuWriter *wtr, GuExn *err)
     
 		for (size_t i = 0; i < type->n_exprs; i++) {
 			gu_puts(" ", wtr, err);
-			pgf_print_expr(type->exprs[i], 4, wtr, err);
+			pgf_print_expr(type->exprs[i], ctxt, 4, wtr, err);
 		}
 		
 		if (prec > 3) gu_putc(')', wtr, err);
@@ -577,3 +1053,38 @@ pgf_print_type(PgfType *type, int prec, GuWriter *wtr, GuExn *err)
 		gu_string_write(type->cid, wtr, err);
 	}
 }
+
+bool
+pgf_type_eq(PgfType* t1, PgfType* t2)
+{
+	if (gu_seq_length(t1->hypos) != gu_seq_length(t2->hypos))
+		return false;
+
+	size_t n_hypos = gu_seq_length(t1->hypos);
+	for (size_t i = 0; i < n_hypos; i++) {
+		PgfHypo *hypo1 = gu_seq_index(t1->hypos, PgfHypo, i);
+		PgfHypo *hypo2 = gu_seq_index(t1->hypos, PgfHypo, i);
+		
+		if (hypo1->bind_type != hypo2->bind_type)
+			return false;
+			
+		if (!gu_string_eq(hypo1->cid, hypo2->cid))
+			return false;
+			
+		if (!pgf_type_eq(hypo1->type, hypo2->type))
+			return false;
+	}
+    
+	if (!gu_string_eq(t1->cid, t2->cid))
+		return false;
+
+	if (t1->n_exprs != t2->n_exprs)
+		return false;
+
+	for (size_t i = 0; i < t1->n_exprs; i++) {
+		if (!pgf_expr_eq(t1->exprs[i], t2->exprs[i]))
+			return false;
+	}
+
+	return true;
+}
diff --git a/src/runtime/c/pgf/expr.h b/src/runtime/c/pgf/expr.h
index ef2dd013c..3d07ce863 100644
--- a/src/runtime/c/pgf/expr.h
+++ b/src/runtime/c/pgf/expr.h
@@ -53,7 +53,7 @@ typedef struct {
 
 
 struct PgfHypo {
-	PgfBindType bindtype;
+	PgfBindType bind_type;
 
 	PgfCId cid;
 	/**< Locally scoped name for the parameter if dependent types
@@ -87,7 +87,7 @@ typedef enum {
 
 typedef struct {
 	PgfBindType bind_type;
-	PgfCId id; // 
+	PgfCId id;
 	PgfExpr body;
 } PgfExprAbs;
 		
@@ -154,22 +154,38 @@ pgf_expr_unapply(PgfExpr expr, GuPool* pool);
 PgfExpr
 pgf_read_expr(GuIn* in, GuPool* pool, GuExn* err);
 
+PgfType*
+pgf_read_type(GuIn* in, GuPool* pool, GuExn* err);
+
 bool
 pgf_literal_eq(PgfLiteral lit1, PgfLiteral lit2);
 
 bool
 pgf_expr_eq(PgfExpr e1, PgfExpr e2);
 
+bool
+pgf_type_eq(PgfType* t1, PgfType* t2);
+
+typedef struct PgfPrintContext PgfPrintContext;
+
+struct PgfPrintContext {
+	PgfCId name;
+	PgfPrintContext* next;
+};
+
 void
 pgf_print_literal(PgfLiteral lit, GuWriter* wtr, GuExn* err);
 
 void
-pgf_print_expr(PgfExpr expr, int prec, GuWriter* wtr, GuExn* err);
+pgf_print_expr(PgfExpr expr, PgfPrintContext* ctxt, int prec, 
+               GuWriter* wtr, GuExn* err);
+
+PgfPrintContext*
+pgf_print_hypo(PgfHypo *hypo, PgfPrintContext* ctxt, int prec,
+               GuWriter *wtr, GuExn *err);
 
 void
-pgf_print_hypo(PgfHypo *hypo, int prec, GuWriter *wtr, GuExn *err);
-
-void
-pgf_print_type(PgfType *type, int prec, GuWriter *wtr, GuExn *err);
+pgf_print_type(PgfType *type, PgfPrintContext* ctxt, int prec,
+               GuWriter *wtr, GuExn *err);
 
 #endif /* EXPR_H_ */
diff --git a/src/runtime/c/pgf/pgf.c b/src/runtime/c/pgf/pgf.c
index 13066927c..519dfea4a 100644
--- a/src/runtime/c/pgf/pgf.c
+++ b/src/runtime/c/pgf/pgf.c
@@ -178,6 +178,17 @@ pgf_iter_functions_by_cat(PgfPGF* pgf, PgfCId catname,
 	gu_map_iter(pgf->abstract.funs, &clo.fn, err);
 }
 
+PgfType*
+pgf_function_type(PgfPGF* pgf, PgfCId funname) 
+{
+	PgfAbsFun* absfun =
+		gu_map_get(pgf->abstract.funs, &funname, PgfAbsFun*);
+	if (absfun == NULL)
+		return NULL;
+		
+	return absfun->type;
+}
+
 GuString
 pgf_print_name(PgfConcr* concr, PgfCId id)
 {
diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h
index 2e7e43584..bda70315e 100644
--- a/src/runtime/c/pgf/pgf.h
+++ b/src/runtime/c/pgf/pgf.h
@@ -107,6 +107,9 @@ void
 pgf_iter_functions_by_cat(PgfPGF* pgf, PgfCId catname,
                           GuMapItor* fn, GuExn* err);
 
+PgfType*
+pgf_function_type(PgfPGF* pgf, PgfCId funname);
+
 GuString
 pgf_print_name(PgfConcr*, PgfCId id);
 
diff --git a/src/runtime/c/pgf/printer.c b/src/runtime/c/pgf/printer.c
index 4b91a011c..71ccda1f4 100644
--- a/src/runtime/c/pgf/printer.c
+++ b/src/runtime/c/pgf/printer.c
@@ -1,4 +1,5 @@
 #include <pgf/data.h>
+#include <stdlib.h>
 
 typedef struct {
 	GuMapItor fn;
@@ -33,11 +34,18 @@ pgf_print_cat(GuMapItor* fn, const void* key, void* value,
     gu_puts("  cat ", wtr, err);
     gu_string_write(name, wtr, err);
 
+	PgfPrintContext* ctxt = NULL;
     size_t n_hypos = gu_seq_length(cat->context);
     for (size_t i = 0; i < n_hypos; i++) {
-		PgfHypo* hypo = gu_seq_get(cat->context, PgfHypo*, i);
+		PgfHypo* hypo = gu_seq_index(cat->context, PgfHypo, i);
 		gu_putc(' ', wtr, err);
-		pgf_print_hypo(hypo, 4, wtr, err);
+		ctxt = pgf_print_hypo(hypo, ctxt, 4, wtr, err);
+	}
+
+	while (ctxt != NULL) {
+		PgfPrintContext* next = ctxt->next;
+		free(ctxt);
+		ctxt = next;
 	}
 
     gu_printf(wtr, err, " ;   -- %f\n",cat->meta_prob);
@@ -55,7 +63,7 @@ pgf_print_absfun(GuMapItor* fn, const void* key, void* value,
     gu_puts(gu_seq_is_null(fun->defns) ? "  data " : "  fun ", wtr, err);
     gu_string_write(name, wtr, err);
     gu_puts(" : ", wtr, err);
-    pgf_print_type(fun->type, 0, wtr, err);
+    pgf_print_type(fun->type, NULL, 0, wtr, err);
     gu_printf(wtr, err, " ;   -- %f\n", fun->ep.prob);
 }
 static void
diff --git a/src/runtime/c/pgf/reader.c b/src/runtime/c/pgf/reader.c
index 1eccc25e0..a43ebdba0 100644
--- a/src/runtime/c/pgf/reader.c
+++ b/src/runtime/c/pgf/reader.c
@@ -188,7 +188,7 @@ pgf_read_flags(PgfReader* rdr)
 }
 
 static PgfType*
-pgf_read_type(PgfReader* rdr);
+pgf_read_type_(PgfReader* rdr);
 
 static PgfExpr
 pgf_read_expr_(PgfReader* rdr)
@@ -269,7 +269,7 @@ pgf_read_expr_(PgfReader* rdr)
 						   &expr, rdr->opool);
 		etyped->expr = pgf_read_expr_(rdr);
 		gu_return_on_exn(rdr->err, gu_null_variant);
-		etyped->type = pgf_read_type(rdr);
+		etyped->type = pgf_read_type_(rdr);
 		gu_return_on_exn(rdr->err, gu_null_variant);
 		break;
 	}
@@ -292,34 +292,38 @@ pgf_read_expr_(PgfReader* rdr)
 static void
 pgf_read_hypo(PgfReader* rdr, PgfHypo* hypo)
 {
-	hypo->bindtype = pgf_read_tag(rdr);
+	hypo->bind_type = pgf_read_tag(rdr);
 	gu_return_on_exn(rdr->err, );
 	
 	hypo->cid = pgf_read_cid(rdr);
 	gu_return_on_exn(rdr->err, );
 	
-	hypo->type = pgf_read_type(rdr);
+	hypo->type = pgf_read_type_(rdr);
 	gu_return_on_exn(rdr->err, );
 }
 
 static PgfType*
-pgf_read_type(PgfReader* rdr)
+pgf_read_type_(PgfReader* rdr)
 {
-	PgfType* type = gu_new(PgfType, rdr->opool);
-
 	size_t n_hypos = pgf_read_len(rdr);
 	gu_return_on_exn(rdr->err, NULL);
-	type->hypos = gu_new_seq(PgfHypo, n_hypos, rdr->opool);
+	GuSeq hypos = gu_new_seq(PgfHypo, n_hypos, rdr->opool);
 	for (size_t i = 0; i < n_hypos; i++) {
-		PgfHypo* hypo = gu_seq_index(type->hypos, PgfHypo, i);
+		PgfHypo* hypo = gu_seq_index(hypos, PgfHypo, i);
 		pgf_read_hypo(rdr, hypo);
 		gu_return_on_exn(rdr->err, NULL);
 	}
 
-	type->cid = pgf_read_cid(rdr);
+	PgfCId cid = pgf_read_cid(rdr);
 	gu_return_on_exn(rdr->err, NULL);
 
-	type->n_exprs = pgf_read_len(rdr);
+	size_t n_exprs = pgf_read_len(rdr);
+
+	PgfType* type = gu_new_flex(rdr->opool, PgfType, exprs, n_exprs);
+	type->hypos   = hypos;
+	type->cid     = cid;
+	type->n_exprs = n_exprs;
+
 	for (size_t i = 0; i < type->n_exprs; i++) {
 		type->exprs[i] = pgf_read_expr_(rdr);
 		gu_return_on_exn(rdr->err, NULL);
@@ -423,7 +427,7 @@ pgf_read_absfun(PgfReader* rdr)
 	absfun->name = pgf_read_cid(rdr);
 	gu_return_on_exn(rdr->err, NULL);
 
-	absfun->type = pgf_read_type(rdr);
+	absfun->type = pgf_read_type_(rdr);
 	gu_return_on_exn(rdr->err, NULL);
 
 	absfun->arity = pgf_read_int(rdr);
diff --git a/src/runtime/c/utils/pgf-parse.c b/src/runtime/c/utils/pgf-parse.c
index ba1088890..c64b07434 100644
--- a/src/runtime/c/utils/pgf-parse.c
+++ b/src/runtime/c/utils/pgf-parse.c
@@ -132,7 +132,7 @@ int main(int argc, char* argv[]) {
     gu_printf(wtr, err, "%d (%.0f ms): ", ctr, 1000.0 * cpu_time_used);
     if (ep != NULL) {
       gu_printf(wtr, err, "[%.4f] (", ep->prob);
-      pgf_print_expr(ep->expr, 0, wtr, err);
+      pgf_print_expr(ep->expr, NULL, 0, wtr, err);
       gu_printf(wtr, err, ")\n");
     } else {
       gu_printf(wtr, err, "---\n");
diff --git a/src/runtime/c/utils/pgf-translate.c b/src/runtime/c/utils/pgf-translate.c
index f53a847e3..9f12d49e1 100644
--- a/src/runtime/c/utils/pgf-translate.c
+++ b/src/runtime/c/utils/pgf-translate.c
@@ -21,7 +21,7 @@ print_result(PgfExprProb* ep, PgfConcr* to_concr,
 {
 	// Write out the abstract syntax tree
 	gu_printf(wtr, err, " [%f] ", ep->prob);
-	pgf_print_expr(ep->expr, 0, wtr, err);
+	pgf_print_expr(ep->expr, NULL, 0, wtr, err);
 	gu_putc('\n', wtr, err);
 
 	// Enumerate the concrete syntax trees corresponding
diff --git a/src/runtime/python/pypgf.c b/src/runtime/python/pypgf.c
index ea7621afc..916429923 100644
--- a/src/runtime/python/pypgf.c
+++ b/src/runtime/python/pypgf.c
@@ -126,7 +126,7 @@ Expr_repr(ExprObject *self)
 	GuStringBuf* sbuf = gu_string_buf(tmp_pool);
 	GuWriter* wtr = gu_string_buf_writer(sbuf);
 
-	pgf_print_expr(self->expr, 0, wtr, err);
+	pgf_print_expr(self->expr, NULL, 0, wtr, err);
 
 	GuString str = gu_string_buf_freeze(sbuf, tmp_pool);
 	PyObject* pystr = gu2py_string(str);
@@ -140,11 +140,11 @@ Expr_richcompare(ExprObject *e1, ExprObject *e2, int op)
 {
 	bool cmp = pgf_expr_eq(e1->expr,e2->expr);
 	
-	if (op == Py_EQ)
-		return cmp ? Py_True : Py_False;
-	else if (op == Py_NE)
-		return cmp ? Py_False : Py_True;
-	else {
+	if (op == Py_EQ) {
+		if (cmp) Py_RETURN_TRUE;  else Py_RETURN_FALSE;
+	} else if (op == Py_NE) {
+		if (cmp) Py_RETURN_FALSE; else Py_RETURN_TRUE;
+	} else {
 		PyErr_SetString(PyExc_TypeError, "the operation is not supported");
 		return NULL;
 	}
@@ -157,6 +157,34 @@ static PyMethodDef Expr_methods[] = {
     {NULL}  /* Sentinel */
 };
 
+static PyGetSetDef Expr_getseters[] = {
+    {"fun", 
+     NULL, NULL,
+     "this the function in a function application",
+     NULL},
+    {"arg", 
+     NULL, NULL,
+     "this the argument in a function application",
+     NULL},
+    {"val", 
+     NULL, NULL,
+     "this is the value of a literal",
+     NULL},
+    {"id", 
+     NULL, NULL,
+     "this is the id of a meta variable",
+     NULL},
+    {"name", 
+     NULL, NULL,
+     "this is the name of a function",
+     NULL},
+    {"index", 
+     NULL, NULL,
+     "this is the de Bruijn index of a variable",
+     NULL},
+    {NULL}  /* Sentinel */
+};
+
 static PyTypeObject pgf_ExprType = {
     PyObject_HEAD_INIT(NULL)
     0,                         /*ob_size*/
@@ -188,7 +216,7 @@ static PyTypeObject pgf_ExprType = {
     0,		                   /*tp_iternext */
     Expr_methods,              /*tp_methods */
     0,                         /*tp_members */
-    0,                         /*tp_getset */
+    Expr_getseters,            /*tp_getset */
     0,                         /*tp_base */
     0,                         /*tp_dict */
     0,                         /*tp_descr_get */
@@ -297,6 +325,28 @@ Expr_unpack(ExprObject* self, PyObject *fargs)
 	for (;;) {
 		GuVariantInfo i = gu_variant_open(expr);
 		switch (i.tag) {
+		case PGF_EXPR_ABS: {
+			PgfExprAbs* eabs = i.data;
+
+			ExprObject* py_body = (ExprObject*) pgf_ExprType.tp_alloc(&pgf_ExprType, 0);
+			if (py_body == NULL)
+				return NULL;
+			py_body->pool   = NULL;
+			py_body->master = (self->master) ? self->master : (PyObject*) self;
+			py_body->expr   = eabs->body;
+			Py_INCREF(py_body->master);
+
+			PyObject* py_bindtype = 
+				(eabs->bind_type == PGF_BIND_TYPE_EXPLICIT) ? Py_True
+				                                            : Py_False;
+			PyObject* py_var = gu2py_string(eabs->id);
+			PyObject* res = 
+				Py_BuildValue("OOOO", py_bindtype, py_var, py_body, args);
+			Py_DECREF(py_var);
+			Py_DECREF(py_body);
+			Py_DECREF(args);
+			return res;
+		}
 		case PGF_EXPR_APP: {
 			PgfExprApp* eapp = i.data;
 			
@@ -355,6 +405,22 @@ Expr_unpack(ExprObject* self, PyObject *fargs)
 			Py_DECREF(args);
 			return res;
 		}
+		case PGF_EXPR_VAR: {
+			PgfExprVar* evar = i.data;
+			PyObject* res = Py_BuildValue("iO", evar->var, args);
+			Py_DECREF(args);
+			return res;
+		}
+		case PGF_EXPR_TYPED: {
+			PgfExprTyped* etyped = i.data;
+			expr = etyped->expr;
+			break;
+		}
+		case PGF_EXPR_IMPL_ARG: {
+			PgfExprImplArg* eimpl = i.data;
+			expr = eimpl->expr;
+			break;
+		}
 		default:
 			gu_impossible();
 			return NULL;
@@ -367,7 +433,10 @@ static PyObject*
 Expr_getattro(ExprObject *self, PyObject *attr_name) {
 	const char* name = PyString_AsString(attr_name);
 
-    GuVariantInfo i = gu_variant_open(self->expr);
+	PgfExpr expr = self->expr;
+	
+redo:;
+    GuVariantInfo i = gu_variant_open(expr);
     switch (i.tag) {
 	case PGF_EXPR_APP: {
 		PgfExprApp* eapp = i.data;
@@ -419,13 +488,30 @@ Expr_getattro(ExprObject *self, PyObject *attr_name) {
 			return PyInt_FromLong(emeta->id);
 		break;
 	}
-	case PGF_EXPR_FUN: {		
+	case PGF_EXPR_FUN: {
 		PgfExprFun* efun = i.data;
 		if (strcmp(name, "name") == 0) {
 			return gu2py_string(efun->fun);
 		}
 		break;
 	}
+	case PGF_EXPR_VAR: {
+		PgfExprVar* evar = i.data;
+		if (strcmp(name, "index") == 0) {
+			return PyInt_FromLong(evar->var);
+		}
+		break;
+	}
+	case PGF_EXPR_TYPED: {
+		PgfExprTyped* etyped = i.data;
+		expr = etyped->expr;
+		goto redo;
+	}
+	case PGF_EXPR_IMPL_ARG: {
+		PgfExprImplArg* eimpl = i.data;
+		expr = eimpl->expr;
+		goto redo;
+	}
 	default:
 		gu_impossible();
 	}
@@ -433,6 +519,362 @@ Expr_getattro(ExprObject *self, PyObject *attr_name) {
 	return PyObject_GenericGetAttr((PyObject*)self, attr_name);
 }
 
+typedef struct {
+	PyObject_HEAD
+	PyObject* master;
+	GuPool* pool;
+    PgfType* type;
+} TypeObject;
+
+static PyTypeObject pgf_TypeType;
+
+static TypeObject*
+Type_new(PyTypeObject *type, PyObject *args, PyObject *kwds)
+{
+    TypeObject* self = (TypeObject *)type->tp_alloc(type, 0);
+    if (self != NULL) {
+		self->master = NULL;
+		self->pool   = NULL;
+		self->type   = NULL;
+    }
+
+    return self;
+}
+
+static void
+Type_dealloc(TypeObject* self)
+{
+	if (self->master != NULL) {
+		Py_DECREF(self->master);
+	}
+	if (self->pool != NULL) {
+		gu_pool_free(self->pool);
+	}
+
+    self->ob_type->tp_free((PyObject*)self);
+}
+
+static int
+Type_init(TypeObject *self, PyObject *args, PyObject *kwds)
+{
+	PyObject* py_hypos;
+	const char* catname_s;
+	PyObject* py_exprs;
+	size_t n_exprs;
+	size_t n_hypos;
+
+	if (PyTuple_Size(args) == 1) {
+		py_hypos = NULL;
+		py_exprs = NULL;
+		n_exprs  = 0;
+		n_hypos  = 0;
+		if (!PyArg_ParseTuple(args, "s", &catname_s))
+			return -1;
+	} else {
+		if (!PyArg_ParseTuple(args, "O!sO!", 
+				&PyList_Type, &py_hypos, 
+				&catname_s, 
+				&PyList_Type, &py_exprs))
+			return -1;
+			
+		n_exprs = PyList_Size(py_exprs);
+		n_hypos = PyList_Size(py_hypos);
+	}
+
+	self->pool = gu_new_pool();
+	self->master =
+		(n_exprs+n_hypos > 0) ? PyTuple_New(n_exprs+n_hypos) : NULL;
+
+	self->type = gu_new_flex(self->pool, PgfType, exprs, n_exprs);
+
+	self->type->hypos =
+		gu_new_seq(PgfHypo, n_hypos, self->pool);
+
+	for (size_t i = 0; i < n_hypos; i++) {
+		PyObject* obj = PyList_GetItem(py_hypos, i);
+		PyObject* py_bindtype;
+		PgfCId cid;
+		PyObject* py_type;
+
+		if (obj->ob_type == &pgf_TypeType) {
+			py_bindtype = Py_True;
+			cid = gu_str_string("_", self->pool);
+			py_type = obj;
+		} else {
+			if (!PyTuple_Check(obj) ||
+				PyTuple_GET_SIZE(obj) != 3) {
+				PyErr_SetString(PyExc_TypeError, "the arguments in the first list must be triples of (boolean,string,pgf.Type)");
+				return -1;
+			}
+
+			py_bindtype = PyTuple_GetItem(obj, 0);
+			if (!PyBool_Check(py_bindtype)) {
+				PyErr_SetString(PyExc_TypeError, "the arguments in the first list must be triples of (boolean,string,pgf.Type)");
+				return -1;
+			}
+
+			PyObject* py_var = PyTuple_GetItem(obj, 1);
+			if (!PyString_Check(py_var)) {
+				PyErr_SetString(PyExc_TypeError, "the arguments in the first list must be triples of (boolean,string,pgf.Type)");
+				return -1;
+			}
+			cid = gu_str_string(PyString_AsString(py_var), self->pool);
+
+			py_type = PyTuple_GetItem(obj, 2);
+			if (py_type->ob_type != &pgf_TypeType) {
+				PyErr_SetString(PyExc_TypeError, "the arguments in the first list must be triples of (boolean,string,pgf.Type)");
+				return -1;
+			}
+		}
+
+		PgfHypo* hypo = gu_seq_index(self->type->hypos, PgfHypo, i);
+		hypo->bind_type = 
+			(py_bindtype == Py_True) ? PGF_BIND_TYPE_EXPLICIT
+			                         : PGF_BIND_TYPE_IMPLICIT;
+		hypo->cid = cid;
+		hypo->type = ((TypeObject*) py_type)->type;
+
+		PyTuple_SetItem(self->master, i, py_type);
+		Py_INCREF(py_type);
+	}
+
+	self->type->cid = gu_str_string(catname_s, self->pool);
+
+	self->type->n_exprs = n_exprs;
+	for (Py_ssize_t i = 0; i < n_exprs; i++) {
+		PyObject* obj = PyList_GetItem(py_exprs, i);
+		if (obj->ob_type != &pgf_ExprType) {
+			PyErr_SetString(PyExc_TypeError, "the arguments in the second list must be expressions");
+			return -1;
+		}
+
+		PyTuple_SetItem(self->master, n_hypos+i, obj);
+		Py_INCREF(obj);
+
+		self->type->exprs[i] = ((ExprObject*) obj)->expr;
+	}
+
+	return 0;
+}
+
+static PyObject *
+Type_repr(TypeObject *self)
+{
+	GuPool* tmp_pool = gu_local_pool();
+
+	GuExn* err = gu_new_exn(NULL, gu_kind(type), tmp_pool);
+	GuStringBuf* sbuf = gu_string_buf(tmp_pool);
+	GuWriter* wtr = gu_string_buf_writer(sbuf);
+
+	pgf_print_type(self->type, NULL, 0, wtr, err);
+
+	GuString str = gu_string_buf_freeze(sbuf, tmp_pool);
+	PyObject* pystr = gu2py_string(str);
+	
+	gu_pool_free(tmp_pool);
+	return pystr;
+}
+
+PyObject *
+Type_richcompare(TypeObject *t1, TypeObject *t2, int op)
+{
+	bool cmp = pgf_type_eq(t1->type,t2->type);
+
+	if (op == Py_EQ) {
+		if (cmp) Py_RETURN_TRUE;  else Py_RETURN_FALSE;
+	} else if (op == Py_NE) {
+		if (cmp) Py_RETURN_FALSE; else Py_RETURN_TRUE;
+	} else {
+		PyErr_SetString(PyExc_TypeError, "the operation is not supported");
+		return NULL;
+	}
+}
+
+static PyObject*
+Type_getHypos(TypeObject *self, void *closure)
+{
+	PgfType* type = self->type;
+
+	PyObject* py_hypos = PyList_New(0);
+	if (py_hypos == NULL)
+		return NULL;
+
+	size_t n_hypos = gu_seq_length(type->hypos);
+	for (size_t i = 0; i < n_hypos; i++) {
+		PgfHypo* hypo = gu_seq_index(type->hypos, PgfHypo, i);
+
+		PyObject* py_bindtype = 
+			(hypo->bind_type == PGF_BIND_TYPE_EXPLICIT) ? Py_True
+						  							    : Py_False;
+
+		PyObject* py_var = gu2py_string(hypo->cid);
+		if (py_var == NULL)
+			goto fail;
+
+		TypeObject* py_type = (TypeObject*) pgf_TypeType.tp_alloc(&pgf_TypeType, 0);
+		if (py_type == NULL) {
+			Py_DECREF(py_var);
+			goto fail;
+		}
+
+		py_type->pool   = NULL;
+		py_type->master = (PyObject*) self;
+		py_type->type   = hypo->type;
+		Py_INCREF(self);
+
+		PyObject* py_hypo = 
+			Py_BuildValue("OOO", py_bindtype, py_var, py_type);
+		Py_DECREF(py_var);
+		Py_DECREF(py_type);
+
+		if (py_hypo == NULL)
+			goto fail;
+
+		if (PyList_Append(py_hypos, (PyObject*) py_hypo) == -1)
+			goto fail;
+
+		Py_DECREF(py_hypo);
+	}
+
+	return py_hypos;
+	
+fail:
+	Py_DECREF(py_hypos);
+	return NULL;
+}
+
+static PyObject*
+Type_getCat(TypeObject *self, void *closure)
+{
+	return gu2py_string(self->type->cid);
+}
+
+static PyObject*
+Type_getExprs(TypeObject *self, void *closure)
+{
+	PgfType* type = self->type;
+
+	PyObject* py_exprs = PyList_New(0);
+	if (py_exprs == NULL)
+		return NULL;
+
+	for (size_t i = 0; i < type->n_exprs; i++) {
+		ExprObject* py_expr = 
+			(ExprObject*) pgf_ExprType.tp_alloc(&pgf_ExprType, 0);
+		if (py_expr == NULL)
+			goto fail;
+		py_expr->pool   = NULL;
+		py_expr->master = (PyObject*) self;
+		py_expr->expr   = type->exprs[i];
+		Py_INCREF(py_expr->master);
+
+		if (PyList_Append(py_exprs, (PyObject*) py_expr) == -1)
+			goto fail;
+
+		Py_DECREF((PyObject*) py_expr);
+	}
+
+	return py_exprs;
+
+fail:
+	Py_DECREF(py_exprs);
+	return NULL;
+}
+
+static PyObject*
+Type_unpack(TypeObject* self, PyObject *fargs)
+{
+	PyObject* res = NULL;
+	PyObject* py_hypos = NULL;
+	PyObject* py_cat = NULL;
+	PyObject* py_exprs = NULL;
+
+	py_hypos = Type_getHypos(self, NULL);
+	if (py_hypos == NULL)
+		goto fail;
+
+	py_cat = Type_getCat(self, NULL);
+	if (py_cat == NULL)
+		goto fail;
+
+	py_exprs = Type_getExprs(self, NULL);
+	if (py_exprs == NULL)
+		goto fail;
+
+	res = Py_BuildValue("OOO", py_hypos, py_cat, py_exprs);
+
+fail:
+	Py_XDECREF(py_hypos);
+	Py_XDECREF(py_cat);
+	Py_XDECREF(py_exprs);
+	return res;
+}
+
+static PyMethodDef Type_methods[] = {
+    {"unpack", (PyCFunction)Type_unpack, METH_VARARGS,
+     "Decomposes a type into its components"
+    },
+    {NULL}  /* Sentinel */
+};
+
+static PyGetSetDef Type_getseters[] = {
+    {"hypos", 
+     (getter)Type_getHypos, NULL,
+     "this is the list of hypotheses in the type signature",
+     NULL},
+    {"cat", 
+     (getter)Type_getCat, NULL,
+     "this is the name of the category",
+     NULL},
+    {"exprs", 
+     (getter)Type_getExprs, NULL,
+     "this is the list of indices for the category",
+     NULL},
+    {NULL}  /* Sentinel */
+};
+
+static PyTypeObject pgf_TypeType = {
+    PyObject_HEAD_INIT(NULL)
+    0,                         /*ob_size*/
+    "pgf.Type",                /*tp_name*/
+    sizeof(TypeObject),        /*tp_basicsize*/
+    0,                         /*tp_itemsize*/
+    (destructor)Type_dealloc,  /*tp_dealloc*/
+    0,                         /*tp_print*/
+    0,                         /*tp_getattr*/
+    0,                         /*tp_setattr*/
+    0,                         /*tp_compare*/
+    0,                         /*tp_repr*/
+    0,                         /*tp_as_number*/
+    0,                         /*tp_as_sequence*/
+    0,                         /*tp_as_mapping*/
+    0,                         /*tp_hash */
+    0,                         /*tp_call*/
+    (reprfunc) Type_repr,      /*tp_str*/
+    0,                         /*tp_getattro*/
+    0,                         /*tp_setattro*/
+    0,                         /*tp_as_buffer*/
+    Py_TPFLAGS_DEFAULT | Py_TPFLAGS_BASETYPE, /*tp_flags*/
+    "abstract syntax type",    /*tp_doc*/
+    0,		                   /*tp_traverse */
+    0,		                   /*tp_clear */
+    (richcmpfunc) Type_richcompare, /*tp_richcompare */
+    0,		                   /*tp_weaklistoffset */
+    0,		                   /*tp_iter */
+    0,		                   /*tp_iternext */
+    Type_methods,              /*tp_methods */
+    0,                         /*tp_members */
+    Type_getseters,            /*tp_getset */
+    0,                         /*tp_base */
+    0,                         /*tp_dict */
+    0,                         /*tp_descr_get */
+    0,                         /*tp_descr_set */
+    0,                         /*tp_dictoffset */
+    (initproc)Type_init,       /*tp_init */
+    0,                         /*tp_alloc */
+    (newfunc) Type_new,        /*tp_new */
+};
+
 typedef struct IterObject {
     PyObject_HEAD
     PGFObject* grammar;
@@ -1504,6 +1946,37 @@ PGF_functionsByCat(PGFObject* self, PyObject *args)
     return functions;
 }
 
+static TypeObject*
+PGF_functionType(PGFObject* self, PyObject *args)
+{
+	const char *funname_s;
+    if (!PyArg_ParseTuple(args, "s", &funname_s))
+        return NULL;
+
+	GuPool *tmp_pool = gu_local_pool();
+    GuString funname = gu_str_string(funname_s, tmp_pool);
+    
+    PgfType* type =
+		pgf_function_type(self->pgf, funname);
+
+	gu_pool_free(tmp_pool);
+
+	if (type == NULL) {
+		PyErr_Format(PyExc_KeyError, "Function '%s' is not defined", funname_s);
+		return NULL;
+	}
+
+	TypeObject* pytype = (TypeObject*) pgf_TypeType.tp_alloc(&pgf_TypeType, 0);
+	if (pytype == NULL)
+		return NULL;
+	pytype->pool   = NULL;
+	pytype->type   = type;
+	pytype->master = (PyObject*) self;
+	Py_XINCREF(self);
+
+    return pytype;
+}
+
 static IterObject*
 PGF_generate(PGFObject* self, PyObject *args, PyObject *keywds)
 {
@@ -1589,6 +2062,9 @@ static PyMethodDef PGF_methods[] = {
     {"functionsByCat", (PyCFunction)PGF_functionsByCat, METH_VARARGS,
      "Returns the list of functions for a given category"
     },
+    {"functionType", (PyCFunction)PGF_functionType, METH_VARARGS,
+     "Returns the type of a function"
+    },
     {"generate", (PyCFunction)PGF_generate, METH_VARARGS | METH_KEYWORDS,
      "Generates abstract syntax trees of given category in decreasing probability order"
     },
@@ -1703,11 +2179,43 @@ pgf_readExpr(PyObject *self, PyObject *args) {
     return pyexpr;
 }
 
+static TypeObject*
+pgf_readType(PyObject *self, PyObject *args) {
+	size_t len;
+    const uint8_t *buf;
+    if (!PyArg_ParseTuple(args, "s#", &buf, &len))
+        return NULL;
+
+	TypeObject* pytype = (TypeObject*) pgf_TypeType.tp_alloc(&pgf_TypeType, 0);
+	if (pytype == NULL)
+		return NULL;
+
+	GuPool* tmp_pool = gu_local_pool();
+	GuIn* in = gu_data_in(buf, len, tmp_pool);
+	GuExn* err = gu_new_exn(NULL, gu_kind(type), tmp_pool);
+
+	pytype->pool = gu_new_pool();
+	pytype->type = pgf_read_type(in, pytype->pool, err);
+	pytype->master = NULL;
+
+	if (!gu_ok(err) || pytype->type == NULL) {
+		PyErr_SetString(PGFError, "The type cannot be parsed");
+		Py_DECREF(pytype);
+		gu_pool_free(tmp_pool);
+		return NULL;
+	}
+
+	gu_pool_free(tmp_pool);
+    return pytype;
+}
+
 static PyMethodDef module_methods[] = {
     {"readPGF",  (void*)pgf_readPGF,  METH_VARARGS,
      "Reads a PGF file in the memory"},
     {"readExpr", (void*)pgf_readExpr, METH_VARARGS,
      "Parses a string as an abstract tree"},
+    {"readType", (void*)pgf_readType, METH_VARARGS,
+     "Parses a string as an abstract type"},
     {NULL, NULL, 0, NULL}        /* Sentinel */
 };
 
@@ -1728,6 +2236,9 @@ initpgf(void)
     if (PyType_Ready(&pgf_ExprType) < 0)
         return;
 
+    if (PyType_Ready(&pgf_TypeType) < 0)
+        return;
+
 	if (PyType_Ready(&pgf_IterType) < 0)
 		return;
 
@@ -1748,6 +2259,9 @@ initpgf(void)
     PyModule_AddObject(m, "Expr", (PyObject *) &pgf_ExprType);
     Py_INCREF(&pgf_ExprType);
 
+    PyModule_AddObject(m, "Type", (PyObject *) &pgf_TypeType);
+    Py_INCREF(&pgf_TypeType);
+
     Py_INCREF(&pgf_PGFType);
     Py_INCREF(&pgf_ConcrType);
     Py_INCREF(&pgf_IterType);