started on the typechecker

This commit is contained in:
krangelov
2021-11-19 10:39:06 +01:00
parent 1107b245da
commit fa1d7cf859
7 changed files with 212 additions and 2 deletions

View File

@@ -9,6 +9,7 @@
#include "reader.h"
#include "writer.h"
#include "printer.h"
#include "typechecker.h"
static void
pgf_exn_clear(PgfExn* err)
@@ -861,6 +862,60 @@ PgfText *pgf_print_lin_seq_internal(object o, size_t i, size_t j)
return printer.get_text();
}
PGF_API
void pgf_check_expr(PgfDB *db, PgfRevision revision,
PgfExpr* pe, PgfType ty,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err)
{
PGF_API_BEGIN {
DB_scope scope(db, READER_SCOPE);
ref<PgfPGF> pgf = PgfDB::revision2pgf(revision);
PgfTypechecker checker(pgf,u);
*pe = m->match_expr(&checker, *pe);
} PGF_API_END
}
PGF_API
PgfType pgf_infer_expr(PgfDB *db, PgfRevision revision,
PgfExpr* pe,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err)
{
PGF_API_BEGIN {
DB_scope scope(db, READER_SCOPE);
ref<PgfPGF> pgf = PgfDB::revision2pgf(revision);
PgfTypechecker checker(pgf,u);
*pe = m->match_expr(&checker, *pe);
} PGF_API_END
PgfText *cat = (PgfText *) alloca(sizeof(PgfText)+2);
cat->size = 1;
cat->text[0] = 'S';
cat->text[1] = 0;
return u->dtyp(0,NULL,cat,0,NULL);
}
PGF_API
void pgf_check_type(PgfDB *db, PgfRevision revision,
PgfType* pty,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err)
{
PGF_API_BEGIN {
DB_scope scope(db, READER_SCOPE);
ref<PgfPGF> pgf = PgfDB::revision2pgf(revision);
PgfTypechecker checker(pgf,u);
*pty = m->match_type(&checker, *pty);
} PGF_API_END
}
PGF_API
PgfRevision pgf_clone_revision(PgfDB *db, PgfRevision revision,
PgfText *name,

View File

@@ -403,6 +403,24 @@ PgfText *pgf_print_lin_sig_internal(object o, size_t i);
PGF_API_DECL
PgfText *pgf_print_lin_seq_internal(object o, size_t i, size_t j);
PGF_API_DECL
void pgf_check_expr(PgfDB *db, PgfRevision revision,
PgfExpr* pe, PgfType ty,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err);
PGF_API_DECL
PgfType pgf_infer_expr(PgfDB *db, PgfRevision revision,
PgfExpr* pe,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err);
PGF_API_DECL
void pgf_check_type(PgfDB *db, PgfRevision revision,
PgfType* pty,
PgfMarshaller *m, PgfUnmarshaller *u,
PgfExn *err);
PGF_API_DECL
PgfRevision pgf_clone_revision(PgfDB *db, PgfRevision revision,
PgfText *name,

View File

@@ -0,0 +1,69 @@
#include "data.h"
#include "typechecker.h"
PgfExpr PgfTypechecker::eabs(PgfBindType btype, PgfText *name, PgfExpr body)
{
return u->eabs(btype,name,body);
}
PgfExpr PgfTypechecker::eapp(PgfExpr fun, PgfExpr arg)
{
return u->eapp(fun, arg);
}
PgfExpr PgfTypechecker::elit(PgfLiteral lit)
{
return u->elit(lit);
}
PgfExpr PgfTypechecker::emeta(PgfMetaId meta)
{
return u->emeta(meta);
}
PgfExpr PgfTypechecker::efun(PgfText *name)
{
return u->efun(name);
}
PgfExpr PgfTypechecker::evar(int index)
{
return u->evar(index);
}
PgfExpr PgfTypechecker::etyped(PgfExpr expr, PgfType ty)
{
return u->etyped(expr,ty);
}
PgfExpr PgfTypechecker::eimplarg(PgfExpr expr)
{
return u->eimplarg(expr);
}
PgfLiteral PgfTypechecker::lint(size_t size, uintmax_t *v)
{
return u->lint(size,v);
}
PgfLiteral PgfTypechecker::lflt(double v)
{
return u->lflt(v);
}
PgfLiteral PgfTypechecker::lstr(PgfText *v)
{
return u->lstr(v);
}
PgfType PgfTypechecker::dtyp(size_t n_hypos, PgfTypeHypo *hypos,
PgfText *cat,
size_t n_exprs, PgfExpr *exprs)
{
return u->dtyp(n_hypos, hypos, cat, n_exprs, exprs);
}
void PgfTypechecker::free_ref(object x)
{
u->free_ref(x);
}

View File

@@ -0,0 +1,31 @@
#ifndef TYPECHECKER_H
#define TYPECHECKER_H
class PGF_INTERNAL_DECL PgfTypechecker : public PgfUnmarshaller {
ref<PgfPGF> gr;
PgfUnmarshaller *u;
public:
PgfTypechecker(ref<PgfPGF> gr, PgfUnmarshaller *u) {
this->gr = gr;
this->u = u;
};
virtual PgfExpr eabs(PgfBindType btype, PgfText *name, PgfExpr body);
virtual PgfExpr eapp(PgfExpr fun, PgfExpr arg);
virtual PgfExpr elit(PgfLiteral lit);
virtual PgfExpr emeta(PgfMetaId meta);
virtual PgfExpr efun(PgfText *name);
virtual PgfExpr evar(int index);
virtual PgfExpr etyped(PgfExpr expr, PgfType typ);
virtual PgfExpr eimplarg(PgfExpr expr);
virtual PgfLiteral lint(size_t size, uintmax_t *v);
virtual PgfLiteral lflt(double v);
virtual PgfLiteral lstr(PgfText *v);
virtual PgfType dtyp(size_t n_hypos, PgfTypeHypo *hypos,
PgfText *cat,
size_t n_exprs, PgfExpr *exprs);
virtual void free_ref(object x);
};
#endif