mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
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
This commit is contained in:
kr.angelov
@@ -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 \
|
||||
|
||||
@@ -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_
|
||||
|
||||
581
src/runtime/c/pgf/typechecker.c
Normal file
581
src/runtime/c/pgf/typechecker.c
Normal file
@@ -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);
|
||||
}
|
||||
@@ -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);
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
Reference in New Issue
Block a user