From 546c7ac85950f98212e08a2ba93795d225fb19e6 Mon Sep 17 00:00:00 2001 From: "kr.angelov" Date: Mon, 4 Nov 2013 17:10:46 +0000 Subject: [PATCH] A simple type checker in the C runtime. Dependent types are not supported yet but HOAS is implemented. The API is accessible from Python as well --- src/runtime/c/Makefile.am | 1 + src/runtime/c/pgf/pgf.h | 13 + src/runtime/c/pgf/typechecker.c | 581 ++++++++++++++++++++++++++++++++ src/runtime/python/pypgf.c | 152 +++++++++ src/ui/android/jni/Android.mk | 2 +- 5 files changed, 748 insertions(+), 1 deletion(-) create mode 100644 src/runtime/c/pgf/typechecker.c diff --git a/src/runtime/c/Makefile.am b/src/runtime/c/Makefile.am index 6716ec042..79a581ee5 100644 --- a/src/runtime/c/Makefile.am +++ b/src/runtime/c/Makefile.am @@ -97,6 +97,7 @@ libpgf_la_SOURCES = \ pgf/reader.h \ pgf/reader.c \ pgf/linearizer.c \ + pgf/typechecker.c \ pgf/reasoner.c \ pgf/printer.c \ pgf/graphviz.c \ diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h index 9ec63c4d6..61b8bea6c 100644 --- a/src/runtime/c/pgf/pgf.h +++ b/src/runtime/c/pgf/pgf.h @@ -39,6 +39,7 @@ typedef GuString PgfToken; extern GU_DECLARE_TYPE(PgfExn, abstract); extern GU_DECLARE_TYPE(PgfParseError, abstract); +extern GU_DECLARE_TYPE(PgfTypeError, abstract); /// @name PGF Grammar objects /// @{ @@ -171,4 +172,16 @@ pgf_complete(PgfConcr* concr, PgfCId cat, GuString string, void pgf_print(PgfPGF* pgf, GuOut* out, GuExn* err); +void +pgf_check_expr(PgfPGF* gr, PgfExpr* pe, PgfType* ty, + GuExn* exn, GuPool* pool); + +PgfType* +pgf_infer_expr(PgfPGF* gr, PgfExpr* pe, + GuExn* exn, GuPool* pool); + +void +pgf_check_type(PgfPGF* gr, PgfType** ty, + GuExn* exn, GuPool* pool); + #endif // PGF_H_ diff --git a/src/runtime/c/pgf/typechecker.c b/src/runtime/c/pgf/typechecker.c new file mode 100644 index 000000000..ea092b2c5 --- /dev/null +++ b/src/runtime/c/pgf/typechecker.c @@ -0,0 +1,581 @@ +#include "pgf.h" +#include "data.h" +#include "gu/mem.h" +#include "gu/string.h" + +typedef struct PgfCFHypos PgfCFHypos; +struct PgfCFHypos { + PgfType* ty; + PgfCFHypos* next; +}; + +typedef struct PgfContext PgfContext; +struct PgfContext { + PgfCId var; + PgfType* ty; + PgfContext* next; +}; + +typedef struct { + PgfCFHypos* hypos; + PgfCId cat; +} PgfCFType; + +typedef struct { + PgfAbstr* abstr; + GuExn* exn; + GuPool* pool; + GuPool* tmp_pool; +} PgfTypeChecker; + +static PgfCFType null_cf_type = { .hypos = NULL, .cat = NULL }; + +static PgfCFType +pgf_ty2cfty(PgfTypeChecker* checker, PgfType* ty) +{ + PgfCFHypos* hypos = NULL; + size_t n_hypos = gu_seq_length(ty->hypos); + while (n_hypos-- > 0) { + PgfHypo* hypo = gu_seq_index(ty->hypos, PgfHypo, n_hypos); + + PgfCFHypos* new_hypos = gu_new(PgfCFHypos, checker->tmp_pool); + new_hypos->ty = hypo->type; + new_hypos->next = hypos; + hypos = new_hypos; + } + return ((PgfCFType) { .hypos = hypos, .cat = ty->cid }); +} + +static PgfType* +pgf_cfty2ty(PgfTypeChecker* checker, PgfCFType cf_ty) +{ + PgfCFHypos* hypos; + + size_t n_hypos = 0; + hypos = cf_ty.hypos; + while (hypos != NULL) { + n_hypos++; + hypos = hypos->next; + } + + PgfType* ty = gu_new(PgfType, checker->pool); + ty->hypos = gu_new_seq(PgfHypo, n_hypos, checker->pool); + ty->cid = cf_ty.cat; + ty->n_exprs = 0; + + size_t i = 0; + hypos = cf_ty.hypos; + while (hypos != NULL) { + PgfHypo* hypo = gu_seq_index(ty->hypos, PgfHypo, i++); + hypo->bind_type = PGF_BIND_TYPE_EXPLICIT; + hypo->cid = "_"; + hypo->type = pgf_cfty2ty(checker, pgf_ty2cfty(checker, hypos->ty)); + hypos = hypos->next; + } + + return ty; +} + +GU_DEFINE_TYPE(PgfTypeError, abstract, _); + +static PgfPrintContext* +pgf_tc_mk_print_context(PgfTypeChecker* checker, PgfContext* ctxt) +{ + PgfPrintContext* pctxt = NULL; + PgfPrintContext** pprev = &pctxt; + + while (ctxt != NULL) { + PgfPrintContext* new_pctxt = + gu_new(PgfPrintContext, checker->tmp_pool); + new_pctxt->name = ctxt->var; + new_pctxt->next = NULL; + + *pprev = new_pctxt; + pprev = &new_pctxt->next; + + ctxt = ctxt->next; + } + + return pctxt; +} + +static void +pgf_tc_err_cannot_infer(PgfTypeChecker* checker, PgfContext* ctxt, PgfExpr e) +{ + GuStringBuf* sbuf = gu_string_buf(checker->tmp_pool); + GuOut* out = gu_string_buf_out(sbuf); + GuExn* err = gu_exn(NULL, type, checker->tmp_pool); + + gu_puts("Cannot infer the type of expression ", out, err); + pgf_print_expr(e, pgf_tc_mk_print_context(checker, ctxt), 0, out, err); + + GuExnData* exn = gu_raise(checker->exn, PgfTypeError); + exn->data = (void*) + gu_string_buf_freeze(sbuf, exn->pool); +} + +static void +pgf_tc_err_exp_fun_type_1(PgfTypeChecker* checker, PgfContext* ctxt, + PgfExpr e, PgfType* ty) +{ + GuStringBuf* sbuf = gu_string_buf(checker->tmp_pool); + GuOut* out = gu_string_buf_out(sbuf); + GuExn* err = gu_exn(NULL, type, checker->tmp_pool); + + PgfPrintContext* pctxt = pgf_tc_mk_print_context(checker, ctxt); + gu_puts("The expression ", out, err); + pgf_print_expr(e, pctxt, 0, out, err); + gu_puts(" is of function type but ", out, err); + pgf_print_type(ty, pctxt, 0, out, err); + gu_puts(" is expected", out, err); + + GuExnData* exn = gu_raise(checker->exn, PgfTypeError); + exn->data = (void*) + gu_string_buf_freeze(sbuf, exn->pool); +} + +static void +pgf_tc_err_exp_fun_type_2(PgfTypeChecker* checker, PgfContext* ctxt, + PgfExpr e, PgfType* ty) +{ + GuStringBuf* sbuf = gu_string_buf(checker->tmp_pool); + GuOut* out = gu_string_buf_out(sbuf); + GuExn* err = gu_exn(NULL, type, checker->tmp_pool); + + PgfPrintContext* pctxt = pgf_tc_mk_print_context(checker, ctxt); + gu_puts("A function type is expected for the expression ", out, err); + pgf_print_expr(e, pctxt, 0, out, err); + gu_puts(" instead of type ", out, err); + pgf_print_type(ty, pctxt, 0, out, err); + + GuExnData* exn = gu_raise(checker->exn, PgfTypeError); + exn->data = (void*) + gu_string_buf_freeze(sbuf, exn->pool); +} + +static void +pgf_tc_err_n_args(PgfTypeChecker* checker, + PgfAbsCat* abs_cat, size_t n_args) +{ + GuExnData* exn = gu_raise(checker->exn, PgfTypeError); + exn->data = (void*) + gu_format_string(exn->pool, + "The category %s has %d indices but %d are given", + abs_cat->name, + gu_seq_length(abs_cat->context), + n_args); +} + +static void +pgf_tc_err_type_mismatch(PgfTypeChecker* checker, + PgfContext* ctxt, + PgfExpr e, PgfCFType ty1, PgfCFType ty2) +{ + GuStringBuf* sbuf = gu_string_buf(checker->tmp_pool); + GuOut* out = gu_string_buf_out(sbuf); + GuExn* err = gu_exn(NULL, type, checker->tmp_pool); + + PgfPrintContext* pctxt = pgf_tc_mk_print_context(checker, ctxt); + gu_puts("The expected type of the expression ", out, err); + pgf_print_expr(e, pctxt, 0, out, err); + gu_puts(" is ", out, err); + pgf_print_type(pgf_cfty2ty(checker, ty1), pctxt, 0, out, err); + gu_puts(" but ", out, err); + pgf_print_type(pgf_cfty2ty(checker, ty2), pctxt, 0, out, err); + gu_puts(" is infered", out, err); + + GuExnData* exn = gu_raise(checker->exn, PgfTypeError); + exn->data = (void*) + gu_string_buf_freeze(sbuf, exn->pool); +} + +static bool +pgf_unify_types(PgfTypeChecker* checker, PgfCFType ty1, PgfCFType ty2) +{ + if (strcmp(ty1.cat, ty2.cat) != 0) + return false; + + while (ty1.hypos != NULL && ty2.hypos != NULL) { + if (!pgf_unify_types(checker, + pgf_ty2cfty(checker, ty1.hypos->ty), + pgf_ty2cfty(checker, ty2.hypos->ty))) + return false; + + ty1.hypos = ty1.hypos->next; + ty2.hypos = ty2.hypos->next; + } + + if (ty1.hypos != NULL || ty2.hypos != NULL) + return false; + + return true; +} + +static PgfCFType +pgf_inf_expr(PgfTypeChecker* checker, PgfContext* ctxt, PgfExpr* pe); + +static void +pgf_tc_expr(PgfTypeChecker* checker, + PgfContext* ctxt, PgfExpr* pe, PgfCFType ty) +{ + GuVariantInfo i = gu_variant_open(*pe); + switch (i.tag) { + case PGF_EXPR_ABS: { + PgfExprAbs* eabs = i.data; + + if (ty.hypos == NULL) { + pgf_tc_err_exp_fun_type_1(checker, ctxt, *pe, pgf_cfty2ty(checker, ty)); + return; + } + + PgfContext* new_ctxt = gu_new(PgfContext, checker->tmp_pool); + new_ctxt->var = eabs->id; + new_ctxt->ty = ty.hypos->ty; + new_ctxt->next = ctxt; + + PgfExprAbs* new_eabs = + gu_new_variant(PGF_EXPR_ABS, + PgfExprAbs, + pe, checker->pool); + new_eabs->bind_type = eabs->bind_type; + new_eabs->id = gu_string_copy(eabs->id, checker->pool); + new_eabs->body = eabs->body; + + PgfCFType new_ty = { .hypos = ty.hypos->next, .cat = ty.cat }; + pgf_tc_expr(checker, new_ctxt, &new_eabs->body, new_ty); + break; + } + case PGF_EXPR_LIT: + case PGF_EXPR_APP: + case PGF_EXPR_FUN: + case PGF_EXPR_VAR: + case PGF_EXPR_TYPED: { + PgfCFType inf_ty = + pgf_inf_expr(checker, ctxt, pe); + if (!gu_ok(checker->exn)) + return; + if (!pgf_unify_types(checker, ty, inf_ty)) { + pgf_tc_err_type_mismatch(checker, ctxt, *pe, ty, inf_ty); + return; + } + break; + } + case PGF_EXPR_META: { + break; + } + case PGF_EXPR_IMPL_ARG: { + PgfExprImplArg* eimpl = i.data; + + PgfExprImplArg* new_eimpl = + gu_new_variant(PGF_EXPR_IMPL_ARG, + PgfExprImplArg, + pe, checker->pool); + new_eimpl->expr = eimpl->expr; + pgf_tc_expr(checker, ctxt, &new_eimpl->expr, ty); + break; + } + default: + gu_impossible(); + } +} + +static void +pgf_tc_type(PgfTypeChecker* checker, PgfType** pty) +{ + PgfType* ty = *pty; + + PgfAbsCat* abs_cat = + gu_map_get(checker->abstr->cats, ty->cid, PgfAbsCat*); + if (abs_cat == NULL) { + GuExnData* exn = gu_raise(checker->exn, PgfExn); + exn->data = (void*) + gu_format_string(exn->pool, + "Unknown category \"%s\"", ty->cid); + return; + } + + PgfContext* ctxt = NULL; + + size_t n_hypos = gu_seq_length(ty->hypos); + PgfHypos* new_hypos = gu_new_seq(PgfHypo, n_hypos, checker->pool); + for (size_t i = 0; i < n_hypos; i++) { + PgfHypo* hypo = gu_seq_index(ty->hypos, PgfHypo, i); + PgfHypo* new_hypo = gu_seq_index(new_hypos, PgfHypo, i); + + new_hypo->bind_type = hypo->bind_type; + new_hypo->cid = gu_string_copy(hypo->cid, checker->pool); + new_hypo->type = hypo->type; + + pgf_tc_type(checker, &new_hypo->type); + if (!gu_ok(checker->exn)) + return; + + PgfContext* new_ctxt = gu_new(PgfContext, checker->tmp_pool); + new_ctxt->var = hypo->cid; + new_ctxt->ty = hypo->type; + new_ctxt->next = ctxt; + ctxt = new_ctxt; + } + + PgfType *new_ty = + gu_new_flex(checker->pool, PgfType, exprs, ty->n_exprs); + new_ty->hypos = new_hypos; + new_ty->cid = gu_string_copy(ty->cid, checker->pool); + new_ty->n_exprs = ty->n_exprs; + + if (gu_seq_length(abs_cat->context) != ty->n_exprs) { + pgf_tc_err_n_args(checker, abs_cat, ty->n_exprs); + return; + } + + for (size_t i = 0; i < ty->n_exprs; i++) { + PgfHypo* hypo = gu_seq_index(abs_cat->context, PgfHypo, i); + + new_ty->exprs[i] = ty->exprs[i]; + pgf_tc_expr(checker, ctxt, &new_ty->exprs[i], pgf_ty2cfty(checker, hypo->type)); + if (!gu_ok(checker->exn)) + return; + } + + *pty = new_ty; +} + +static PgfCFType +pgf_inf_expr(PgfTypeChecker* checker, PgfContext* ctxt, PgfExpr* pe) +{ + GuVariantInfo i = gu_variant_open(*pe); + switch (i.tag) { + case PGF_EXPR_ABS: { + pgf_tc_err_cannot_infer(checker, ctxt, *pe); + return null_cf_type; + } + case PGF_EXPR_APP: { + PgfExprApp* eapp = i.data; + + PgfExprApp* new_eapp = + gu_new_variant(PGF_EXPR_APP, + PgfExprApp, + pe, checker->pool); + new_eapp->fun = eapp->fun; + new_eapp->arg = eapp->arg; + + PgfCFType fun_ty = + pgf_inf_expr(checker, ctxt, &new_eapp->fun); + if (!gu_ok(checker->exn)) + return null_cf_type; + if (fun_ty.hypos == NULL) { + pgf_tc_err_exp_fun_type_2(checker, + ctxt, + eapp->fun, pgf_cfty2ty(checker, fun_ty)); + return null_cf_type; + } + + pgf_tc_expr(checker, ctxt, &new_eapp->arg, pgf_ty2cfty(checker, fun_ty.hypos->ty)); + return ((PgfCFType) { .hypos = fun_ty.hypos->next, + .cat = fun_ty.cat + }); + } + case PGF_EXPR_LIT: { + PgfExprLit* elit = i.data; + + PgfExprLit* new_elit = + gu_new_variant(PGF_EXPR_LIT, + PgfExprLit, + pe, checker->pool); + + GuVariantInfo i = gu_variant_open(elit->lit); + switch (i.tag) { + case PGF_LITERAL_STR: { + PgfLiteralStr* lstr = i.data; + + PgfLiteralStr* new_lstr = + gu_new_flex_variant(PGF_LITERAL_STR, + PgfLiteralStr, + val, strlen(lstr->val)+1, + &new_elit->lit, checker->pool); + strcpy(new_lstr->val, lstr->val); + + return ((PgfCFType) { .hypos = NULL, .cat = "String" }); + } + case PGF_LITERAL_INT: { + PgfLiteralInt* lint = i.data; + + PgfLiteralInt* new_lint = + gu_new_variant(PGF_LITERAL_INT, + PgfLiteralInt, + &new_elit->lit, checker->pool); + new_lint->val = lint->val; + + return ((PgfCFType) { .hypos = NULL, .cat = "Int" }); + } + case PGF_LITERAL_FLT: { + PgfLiteralFlt* lflt = i.data; + + PgfLiteralFlt* new_lflt = + gu_new_variant(PGF_LITERAL_FLT, + PgfLiteralFlt, + &new_elit->lit, checker->pool); + new_lflt->val = lflt->val; + + return ((PgfCFType) { .hypos = NULL, .cat = "Float" }); + } + default: + gu_impossible(); + } + break; + } + case PGF_EXPR_META: { + pgf_tc_err_cannot_infer(checker, ctxt, *pe); + return null_cf_type; + } + case PGF_EXPR_FUN: { + PgfExprFun* efun = i.data; + + PgfType* ty = NULL; + + int var = 0; + PgfContext* var_ctxt = ctxt; + while (var_ctxt != NULL) { + if (strcmp(var_ctxt->var, efun->fun) == 0) { + PgfExprVar* new_evar = + gu_new_variant(PGF_EXPR_VAR, + PgfExprVar, + pe, checker->pool); + new_evar->var = var; + ty = var_ctxt->ty; + break; + } + + var++; + var_ctxt = var_ctxt->next; + } + + if (ty == NULL) { + PgfAbsFun* abs_fun = + gu_map_get(checker->abstr->funs, efun->fun, PgfAbsFun*); + if (abs_fun == NULL) { + GuExnData* exn = gu_raise(checker->exn, PgfExn); + exn->data = (void*) + gu_format_string(exn->pool, + "Unknown function \"%s\"", efun->fun); + return null_cf_type; + } else { + PgfExprFun *new_efun = + gu_new_flex_variant(PGF_EXPR_FUN, + PgfExprFun, + fun, strlen(efun->fun)+1, + pe, checker->pool); + strcpy(new_efun->fun, efun->fun); + ty = abs_fun->type; + } + } + + return pgf_ty2cfty(checker, ty); + } + case PGF_EXPR_VAR: { + PgfExprVar* evar = i.data; + + int var = evar->var; + PgfContext* var_ctxt = ctxt; + assert(var_ctxt != NULL); + while (var > 0) { + var--; + var_ctxt = var_ctxt->next; + assert(var_ctxt != NULL); + } + + return pgf_ty2cfty(checker, var_ctxt->ty); + } + case PGF_EXPR_TYPED: { + PgfExprTyped* etyped = i.data; + + PgfExprTyped* new_etyped = + gu_new_variant(PGF_EXPR_TYPED, + PgfExprTyped, + pe, checker->pool); + new_etyped->expr = etyped->expr; + new_etyped->type = etyped->type; + + pgf_tc_type(checker, &new_etyped->type); + if (!gu_ok(checker->exn)) + return null_cf_type; + + PgfCFType cf_ty = pgf_ty2cfty(checker, new_etyped->type); + + pgf_tc_expr(checker, ctxt, &new_etyped->expr, cf_ty); + return cf_ty; + } + case PGF_EXPR_IMPL_ARG: { + PgfExprImplArg* eimpl = i.data; + + PgfExprImplArg* new_eimpl = + gu_new_variant(PGF_EXPR_IMPL_ARG, + PgfExprImplArg, + pe, checker->pool); + new_eimpl->expr = eimpl->expr; + return pgf_inf_expr(checker, ctxt, &new_eimpl->expr); + } + default: + gu_impossible(); + } + + return null_cf_type; +} + +void +pgf_check_expr(PgfPGF* gr, PgfExpr* pe, PgfType* ty, + GuExn* exn, GuPool* pool) +{ + GuPool* tmp_pool = gu_new_pool(); + + PgfTypeChecker* checker = gu_new(PgfTypeChecker, tmp_pool); + checker->abstr = &gr->abstract; + checker->exn = exn; + checker->pool = pool; + checker->tmp_pool = tmp_pool; + + pgf_tc_expr(checker, NULL, pe, pgf_ty2cfty(checker, ty)); + + gu_pool_free(tmp_pool); +} + +PgfType* +pgf_infer_expr(PgfPGF* gr, PgfExpr* pe, + GuExn* exn, GuPool* pool) +{ + GuPool* tmp_pool = gu_new_pool(); + + PgfTypeChecker* checker = gu_new(PgfTypeChecker, tmp_pool); + checker->abstr = &gr->abstract; + checker->exn = exn; + checker->pool = pool; + checker->tmp_pool = tmp_pool; + + PgfCFType cf_ty = pgf_inf_expr(checker, NULL, pe); + + PgfType* ty = NULL; + if (gu_ok(exn)) { + ty = pgf_cfty2ty(checker, cf_ty); + } + + gu_pool_free(tmp_pool); + + return ty; +} + +void +pgf_check_type(PgfPGF* gr, PgfType** pty, + GuExn* exn, GuPool* pool) +{ + GuPool* tmp_pool = gu_new_pool(); + + PgfTypeChecker* checker = gu_new(PgfTypeChecker, tmp_pool); + checker->abstr = &gr->abstract; + checker->exn = exn; + checker->pool = pool; + checker->tmp_pool = tmp_pool; + + pgf_tc_type(checker, pty); + + gu_pool_free(tmp_pool); +} diff --git a/src/runtime/python/pypgf.c b/src/runtime/python/pypgf.c index 21db6741a..8fe4256e2 100644 --- a/src/runtime/python/pypgf.c +++ b/src/runtime/python/pypgf.c @@ -12,6 +12,8 @@ static PyObject* PGFError; static PyObject* ParseError; +static PyObject* TypeError; + typedef struct { PyObject_HEAD GuPool* pool; @@ -2036,6 +2038,143 @@ PGF_compute(PGFObject* self, PyObject *args) return py_expr; } +static ExprObject* +PGF_checkExpr(PGFObject* self, PyObject *args) +{ + ExprObject* py_expr = NULL; + TypeObject* py_type = NULL; + if (!PyArg_ParseTuple(args, "O!O!", &pgf_ExprType, &py_expr, &pgf_TypeType, &py_type)) + return NULL; + + ExprObject* new_pyexpr = (ExprObject*) pgf_ExprType.tp_alloc(&pgf_ExprType, 0); + if (new_pyexpr == NULL) + return NULL; + + new_pyexpr->pool = gu_new_pool(); + new_pyexpr->expr = py_expr->expr; + new_pyexpr->master = NULL; + + GuPool* tmp_pool = gu_local_pool(); + GuExn* exn = gu_new_exn(NULL, gu_kind(type), tmp_pool); + + pgf_check_expr(self->pgf, &new_pyexpr->expr, py_type->type, + exn, new_pyexpr->pool); + if (!gu_ok(exn)) { + if (gu_exn_caught(exn) == gu_type(PgfExn)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(PGFError, msg); + } else if (gu_exn_caught(exn) == gu_type(PgfTypeError)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(TypeError, msg); + } + + Py_DECREF(new_pyexpr); + gu_pool_free(tmp_pool); + return NULL; + } + + gu_pool_free(tmp_pool); + + return new_pyexpr; +} + +static PyObject* +PGF_inferExpr(PGFObject* self, PyObject *args) +{ + ExprObject* py_expr = NULL; + if (!PyArg_ParseTuple(args, "O!", &pgf_ExprType, &py_expr)) + return NULL; + + ExprObject* new_pyexpr = (ExprObject*) pgf_ExprType.tp_alloc(&pgf_ExprType, 0); + if (new_pyexpr == NULL) + return NULL; + + new_pyexpr->pool = gu_new_pool(); + new_pyexpr->expr = py_expr->expr; + new_pyexpr->master = NULL; + + TypeObject* new_pytype = (TypeObject*) pgf_TypeType.tp_alloc(&pgf_TypeType, 0); + if (new_pytype == NULL) { + Py_DECREF(new_pyexpr); + return NULL; + } + + new_pytype->pool = NULL; + new_pytype->type = NULL; + new_pytype->master = (PyObject*) new_pyexpr; + Py_INCREF(new_pyexpr); + + GuPool* tmp_pool = gu_local_pool(); + GuExn* exn = gu_new_exn(NULL, gu_kind(type), tmp_pool); + + new_pytype->type = + pgf_infer_expr(self->pgf, &new_pyexpr->expr, + exn, new_pyexpr->pool); + if (!gu_ok(exn)) { + if (gu_exn_caught(exn) == gu_type(PgfExn)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(PGFError, msg); + } else if (gu_exn_caught(exn) == gu_type(PgfTypeError)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(TypeError, msg); + } + + Py_DECREF(new_pyexpr); + Py_DECREF(new_pytype); + gu_pool_free(tmp_pool); + return NULL; + } + + gu_pool_free(tmp_pool); + + PyObject* res = + Py_BuildValue("OO", new_pyexpr, new_pytype); + + Py_DECREF(new_pyexpr); + Py_DECREF(new_pytype); + + return res; +} + +static TypeObject* +PGF_checkType(PGFObject* self, PyObject *args) +{ + TypeObject* py_type = NULL; + if (!PyArg_ParseTuple(args, "O!", &pgf_TypeType, &py_type)) + return NULL; + + TypeObject* new_pytype = (TypeObject*) pgf_TypeType.tp_alloc(&pgf_TypeType, 0); + if (new_pytype == NULL) { + return NULL; + } + + new_pytype->pool = gu_new_pool(); + new_pytype->type = py_type->type; + new_pytype->master = NULL; + + GuPool* tmp_pool = gu_local_pool(); + GuExn* exn = gu_new_exn(NULL, gu_kind(type), tmp_pool); + + pgf_check_type(self->pgf, &new_pytype->type, + exn, new_pytype->pool); + if (!gu_ok(exn)) { + if (gu_exn_caught(exn) == gu_type(PgfExn)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(PGFError, msg); + } else if (gu_exn_caught(exn) == gu_type(PgfTypeError)) { + GuString msg = (GuString) gu_exn_caught_data(exn); + PyErr_SetString(TypeError, msg); + } + + gu_pool_free(tmp_pool); + return NULL; + } + + gu_pool_free(tmp_pool); + + return new_pytype; +} + static PyObject* PGF_graphvizAbstractTree(PGFObject* self, PyObject *args) { ExprObject* pyexpr; @@ -2101,6 +2240,15 @@ static PyMethodDef PGF_methods[] = { {"compute", (PyCFunction)PGF_compute, METH_VARARGS, "Computes the normal form of an abstract syntax tree" }, + {"checkExpr", (PyCFunction)PGF_checkExpr, METH_VARARGS, + "Type checks an abstract syntax expression and returns the updated expression" + }, + {"inferExpr", (PyCFunction)PGF_inferExpr, METH_VARARGS, + "Type checks an abstract syntax expression and returns the updated expression" + }, + {"checkType", (PyCFunction)PGF_checkType, METH_VARARGS, + "Type checks an abstract syntax type and returns the updated type" + }, {"graphvizAbstractTree", (PyCFunction)PGF_graphvizAbstractTree, METH_VARARGS, "Renders an abstract syntax tree in a Graphviz format" }, @@ -2289,6 +2437,10 @@ initpgf(void) PyModule_AddObject(m, "ParseError", ParseError); Py_INCREF(ParseError); + TypeError = PyErr_NewException("pgf.TypeError", NULL, NULL); + PyModule_AddObject(m, "TypeError", TypeError); + Py_INCREF(TypeError); + PyModule_AddObject(m, "Expr", (PyObject *) &pgf_ExprType); Py_INCREF(&pgf_ExprType); diff --git a/src/ui/android/jni/Android.mk b/src/ui/android/jni/Android.mk index 29808222a..7064ac673 100644 --- a/src/ui/android/jni/Android.mk +++ b/src/ui/android/jni/Android.mk @@ -3,7 +3,7 @@ LOCAL_PATH := $(call my-dir) include $(CLEAR_VARS) jni_c_files := jpgf.c -pgf_c_files := data.c expr.c graphviz.c linearizer.c literals.c parser.c parseval.c pgf.c printer.c reader.c reasoner.c jit.c +pgf_c_files := data.c expr.c graphviz.c linearizer.c literals.c parser.c parseval.c pgf.c printer.c reader.c reasoner.c jit.c typechecker.c gu_c_files := assert.c choice.c exn.c fun.c in.c map.c out.c str.c type.c utf8.c \ bits.c defs.c enum.c file.c hash.c mem.c prime.c seq.c string.c ucs.c variant.c