From a3203143ba7f22666f42350a69842fc161cad536 Mon Sep 17 00:00:00 2001 From: "John J. Camilleri" Date: Fri, 17 Sep 2021 11:27:19 +0200 Subject: [PATCH] Add Type constructor, showType, mk[Dep]Hypo, bind type constants --- src/runtime/python/expr.c | 49 ++++++++++++++++++-- src/runtime/python/pypgf.c | 78 +++++++++++++++++++++++++++++++- src/runtime/python/test_suite.py | 60 ++++++++++++++++++++---- 3 files changed, 172 insertions(+), 15 deletions(-) diff --git a/src/runtime/python/expr.c b/src/runtime/python/expr.c index 95f048f43..6ee0ff5ba 100644 --- a/src/runtime/python/expr.c +++ b/src/runtime/python/expr.c @@ -8,6 +8,48 @@ // ---------------------------------------------------------------------------- +static TypeObject * +Type_new(PyTypeObject *subtype, PyObject *args, PyObject *kwds) +{ + TypeObject* self = (TypeObject *)subtype->tp_alloc(subtype, 0); + return self; +} + +static int +Type_init(TypeObject *self, PyObject *args, PyObject *kwds) +{ + PyObject* hypos; + PyObject* cat; + PyObject* exprs; + if (!PyArg_ParseTuple(args, "O!UO!", &PyList_Type, &hypos, &cat, &PyList_Type, &exprs)) { + return -1; + } + + for (Py_ssize_t i = 0; i < PyList_Size(hypos); i++) { + if (!PyObject_TypeCheck(PyList_GetItem(hypos, i), &PyTuple_Type)) { + PyErr_SetString(PyExc_TypeError, "invalid hypo in Type_init"); + return -1; + } + // TODO check tuple elements + // Py_INCREF(&hypos[i]); + } + for (Py_ssize_t i = 0; i < PyList_Size(exprs); i++) { + if (!PyObject_TypeCheck(PyList_GetItem(exprs, i), &pgf_ExprType)) { + PyErr_SetString(PyExc_TypeError, "invalid expression in Type_init"); + return -1; + } + // Py_INCREF(&exprs[i]); + } + self->hypos = hypos; + self->cat = cat; + self->exprs = exprs; + Py_INCREF(hypos); + // Py_INCREF(cat); + Py_INCREF(exprs); + + return 0; +} + static PyObject * Type_str(TypeObject *self) { @@ -17,8 +59,7 @@ Type_str(TypeObject *self) return str; } -// static -PyObject * +static PyObject * Type_richcompare(TypeObject *t1, PyObject *p2, int op) { bool same = false; @@ -120,9 +161,9 @@ PyTypeObject pgf_TypeType = { 0, /*tp_descr_get */ 0, /*tp_descr_set */ 0, /*tp_dictoffset */ - 0, //(initproc) Type_init, /*tp_init */ + (initproc) Type_init, /*tp_init */ 0, /*tp_alloc */ - 0, //(newfunc) Type_new, /*tp_new */ + (newfunc) Type_new, /*tp_new */ }; // ---------------------------------------------------------------------------- diff --git a/src/runtime/python/pypgf.c b/src/runtime/python/pypgf.c index 2f91c5a62..15d7ff7da 100644 --- a/src/runtime/python/pypgf.c +++ b/src/runtime/python/pypgf.c @@ -2614,6 +2614,70 @@ pgf_readType(PyObject *self, PyObject *args) return (TypeObject *)type; } +static PyObject * +pgf_showType(PyObject *self, PyObject *args) +{ + PyObject *pylist; + PyObject *pytype; + if (!PyArg_ParseTuple(args, "O!O!", &PyList_Type, &pylist, &pgf_TypeType, &pytype)) + return NULL; + + PgfPrintContext *ctxt = NULL; + for (Py_ssize_t i = PyList_Size(pylist); i > 0 ; i--) { + PyObject *item = PyList_GetItem(pylist, i-1); + if (!PyUnicode_Check(item)) { + PyErr_SetString(PyExc_TypeError, "invalid variable argument in showType"); + return NULL; + } + PgfText *input = PyUnicode_AsPgfText(item); + + // TODO a better way to copy into this->name? + PgfPrintContext *this = (PgfPrintContext *)PyMem_Malloc(sizeof(PgfPrintContext *) + sizeof(PgfText) + input->size + 1); + this->next = ctxt; + memcpy(&this->name, input, sizeof(PgfText) + input->size + 1); + ctxt = this; + } + + PgfText *s = pgf_print_type((PgfType) pytype, ctxt, 0, &marshaller); + PyObject *str = PyUnicode_FromStringAndSize(s->text, s->size); + free(s); + return str; +} + +static PyObject * +pgf_mkHypo(PyObject *self, PyObject *args) +{ + PyObject *type; + if (!PyArg_ParseTuple(args, "O!", &pgf_TypeType, &type)) + return NULL; + + PyObject *tup = PyTuple_New(3); + PyTuple_SetItem(tup, 0, PyLong_FromLong(0)); // explicit + PyTuple_SetItem(tup, 1, PyUnicode_FromStringAndSize("_", 1)); + PyTuple_SetItem(tup, 2, type); + Py_INCREF(type); + + return tup; +} + +static PyObject * +pgf_mkDepHypo(PyObject *self, PyObject *args) +{ + PyObject *var; + PyObject *type; + if (!PyArg_ParseTuple(args, "UO!", &var, &pgf_TypeType, &type)) + return NULL; + + PyObject *tup = PyTuple_New(3); + PyTuple_SetItem(tup, 0, PyLong_FromLong(0)); // explicit + PyTuple_SetItem(tup, 1, var); + PyTuple_SetItem(tup, 2, type); + Py_INCREF(var); + Py_INCREF(type); + + return tup; +} + static PyMethodDef module_methods[] = { {"readPGF", (void*)pgf_readPGF, METH_VARARGS, "Reads a PGF file into memory"}, @@ -2627,6 +2691,13 @@ static PyMethodDef module_methods[] = { "Renders an expression as a string"}, {"readType", (void*)pgf_readType, METH_VARARGS, "Parses a string as an abstract type"}, + {"showType", (void*)pgf_showType, METH_VARARGS, + "Renders a type as a string"}, + + {"mkHypo", (void*)pgf_mkHypo, METH_VARARGS, + "Creates hypothesis for non-dependent type i.e. A"}, + {"mkDepHypo", (void*)pgf_mkDepHypo, METH_VARARGS, + "Creates hypothesis for dependent type i.e. (x : A)"}, {NULL, NULL, 0, NULL} /* Sentinel */ }; @@ -2695,8 +2766,7 @@ MOD_INIT(pgf) // if (PyType_Ready(&pgf_IterType) < 0) // return MOD_ERROR_VAL; - MOD_DEF(m, "pgf", "The Runtime for Portable Grammar Format in Python", - module_methods); + MOD_DEF(m, "pgf", "The Runtime for Portable Grammar Format in Python", module_methods); if (m == NULL) return MOD_ERROR_VAL; @@ -2759,5 +2829,9 @@ MOD_INIT(pgf) // PyModule_AddObject(m, "BIND", (PyObject *) &pgf_BINDType); // Py_INCREF(&pgf_BINDType); + PyModule_AddIntConstant(m, "BIND_TYPE_EXPLICIT", 0); + + PyModule_AddIntConstant(m, "BIND_TYPE_IMPLICIT", 1); + return MOD_SUCCESS_VAL(m); } diff --git a/src/runtime/python/test_suite.py b/src/runtime/python/test_suite.py index 9c9e0c69f..1be97efe3 100644 --- a/src/runtime/python/test_suite.py +++ b/src/runtime/python/test_suite.py @@ -154,6 +154,42 @@ def test_functionType_wrong(PGF): def test_startCat(PGF): assert PGF.startCat == pgf.readType("S") +def test_showType_1(PGF): + assert pgf.showType([], pgf.Type([], "N", [])) == "N" + # ,TestCase (assertEqual "show type 1" "N" (showType [] (DTyp [] "N" []))) + +def test_showType_2(PGF): + assert pgf.showType([], pgf.Type([pgf.mkHypo(pgf.Type([], "N", []))], "N", [])) == "N -> N" + # ,TestCase (assertEqual "show type 2" "N -> N" (showType [] (DTyp [(Explicit,"_",DTyp [] "N" [])] "N" []))) + +def test_showType_3(PGF): + assert pgf.showType([], pgf.Type([pgf.mkHypo(pgf.Type([pgf.mkHypo(pgf.Type([], "N", []))], "N", []))], "N", [])) == "(N -> N) -> N" + # ,TestCase (assertEqual "show type 3" "(N -> N) -> N" (showType [] (DTyp [(Explicit,"_",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "N" []))) + +# def test_showType_4(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "(x : N) -> P x" +# # ,TestCase (assertEqual "show type 4" "(x : N) -> P x" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" [])] "P" [EVar 0]))) +# +# def test_showType_5(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "(f : N -> N) -> P (f z)" +# # ,TestCase (assertEqual "show type 5" "(f : N -> N) -> P (f z)" (showType [] (DTyp [(Explicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EFun "z")]))) +# +# def test_showType_6(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "(f : N -> N) -> P (f n)" +# # ,TestCase (assertEqual "show type 6" "(f : N -> N) -> P (f n)" (showType ["n"] (DTyp [(Explicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EVar 1)]))) +# +# def test_showType_7(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "({f} : N -> N) -> P (f n)" +# # ,TestCase (assertEqual "show type 7" "({f} : N -> N) -> P (f n)" (showType ["n"] (DTyp [(Implicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EVar 1)]))) +# +# def test_showType_8(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "(x : N) -> P x -> S" +# # ,TestCase (assertEqual "show type 8" "(x : N) -> P x -> S" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" []),(Explicit,"_",DTyp [] "P" [EVar 0])] "S" []))) +# +# def test_showType_9(PGF): +# assert pgf.showType([], pgf.Type([], "N", [])) == "(x : N) -> (y : P x) -> S" +# # ,TestCase (assertEqual "show type 9" "(x : N) -> (y : P x) -> S" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" []),(Explicit,"y",DTyp [] "P" [EVar 0])] "S" []))) + # expressions def test_readExpr_invalid(): @@ -210,9 +246,15 @@ def test_readExpr_lint_str_big3_neg(): def test_readExpr_lflt_str(): assert str(pgf.readExpr("3.142")) == "3.142" -def test_readExpr_lstr_str(): +def test_readExpr_lstr_str_unicode(): assert str(pgf.readExpr("\"açġħ\"")) == "\"açġħ\"" +def test_readExpr_lstr_null(): + assert str(pgf.ExprLit("ab\0c")) == "\"ab\\0c\"" + +def test_readExpr_lstr_newline(): + assert str(pgf.ExprLit("ab\nc")) == "\"ab\\nc\"" + # expressions: functions def test_readExpr_efun_equality_1(): @@ -283,35 +325,35 @@ def test_showExpr_evar_4(): # expressions: lambda abstractions def test_showExpr_eabs_1(): - expr = pgf.ExprAbs(0, "w", pgf.ExprVar(0)) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "w", pgf.ExprVar(0)) assert pgf.showExpr(["z", "y", "x"], expr) == "\\w->w" def test_showExpr_eabs_2(): - expr = pgf.ExprAbs(0, "v", pgf.ExprAbs(0, "w", pgf.ExprVar(2))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "w", pgf.ExprVar(2))) assert pgf.showExpr(["z", "y", "x"], expr) == "\\v,w->z" def test_showExpr_eabs_3(): - expr = pgf.ExprAbs(0, "v", pgf.ExprAbs(1, "w", pgf.ExprVar(2))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "w", pgf.ExprVar(2))) assert pgf.showExpr(["z", "y", "x"], expr) == "\\v,{w}->z" def test_showExpr_eabs_4(): - expr = pgf.ExprAbs(0, "v", pgf.ExprAbs(1, "w", pgf.ExprAbs(0, "z", pgf.ExprVar(0)))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "w", pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "z", pgf.ExprVar(0)))) assert pgf.showExpr(["y", "x"], expr) == "\\v,{w},z->z" def test_showExpr_eabs_5(): - expr = pgf.ExprAbs(0, "v", pgf.ExprAbs(1, "w", pgf.ExprAbs(1, "z", pgf.ExprVar(2)))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "w", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "z", pgf.ExprVar(2)))) assert pgf.showExpr(["y", "x"], expr) == "\\v,{w,z}->v" def test_showExpr_eabs_6(): - expr = pgf.ExprAbs(0, "v", pgf.ExprAbs(1, "w", pgf.ExprAbs(1, "z", pgf.ExprAbs(0, "t", pgf.ExprVar(3))))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "w", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "z", pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "t", pgf.ExprVar(3))))) assert pgf.showExpr(["y", "x"], expr) == "\\v,{w,z},t->v" def test_showExpr_eabs_7(): - expr = pgf.ExprAbs(0, "u", pgf.ExprAbs(0, "v", pgf.ExprAbs(1, "w", pgf.ExprAbs(1, "z", pgf.ExprAbs(0, "t", pgf.ExprVar(3)))))) + expr = pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "u", pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "v", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "w", pgf.ExprAbs(pgf.BIND_TYPE_IMPLICIT, "z", pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "t", pgf.ExprVar(3)))))) assert pgf.showExpr(["y", "x"], expr) == "\\u,v,{w,z},t->v" def test_showExpr_eabs_8(): - expr = pgf.ExprApp(pgf.ExprFun("f"), pgf.ExprAbs(0, "x", pgf.ExprVar(0))) + expr = pgf.ExprApp(pgf.ExprFun("f"), pgf.ExprAbs(pgf.BIND_TYPE_EXPLICIT, "x", pgf.ExprVar(0))) assert pgf.showExpr([], expr) == "f (\\x->x)" # expressions: meta variables