Add Type constructor, showType, mk[Dep]Hypo, bind type constants

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 */
 };
 
 // ----------------------------------------------------------------------------

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);
 }

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