pretty printing for expressions and types

src/runtime/c/Makefile.am

@@ -15,6 +15,8 @@ libpgf_la_SOURCES = \
 	pgf/pgf.cxx \
 	pgf/reader.cxx \
 	pgf/reader.h \
+	pgf/printer.cxx \
+	pgf/printer.h \
 	pgf/data.h \
 	pgf/expr.cxx \
 	pgf/expr.h \

src/runtime/c/pgf/expr.cxx

@@ -473,7 +473,7 @@ uintptr_t PgfExprParser::parse_arg()
 	return arg;
 }
 
-PgfText wildcard = {size: 1, text: {'_','0'}};
+PGF_INTERNAL PgfText wildcard = {size: 1, text: {'_','0'}};
 
 PgfBind *PgfExprParser::parse_bind(PgfBind *next)
 {

src/runtime/c/pgf/expr.h

@@ -169,4 +169,6 @@ public:
     bool eof();
 };
 
+PGF_INTERNAL_DECL extern PgfText wildcard;
+
 #endif /* EXPR_H_ */

src/runtime/c/pgf/pgf.cxx

@@ -2,6 +2,7 @@
 #include <math.h>
 #include "data.h"
 #include "reader.h"
+#include "printer.h"
 
 static void
 pgf_exn_clear(PgfExn* err)
@@ -314,6 +315,16 @@ prob_t pgf_function_prob(PgfPGF *pgf, PgfText *funname)
 	return absfun->ep.prob;
 }
 
+PGF_API
+PgfText *pgf_print_expr(uintptr_t e,
+                        PgfPrintContext *ctxt, int prio,
+                        PgfMarshaller *m)
+{
+    PgfPrinter printer(ctxt,prio,m);
+    m->match_expr(&printer, e);
+    return printer.get_text();
+}
+
 PGF_API uintptr_t
 pgf_read_expr(PgfText *input, PgfUnmarshaller *u)
 {
@@ -326,6 +337,16 @@ pgf_read_expr(PgfText *input, PgfUnmarshaller *u)
     return res;
 }
 
+PGF_API
+PgfText *pgf_print_type(uintptr_t ty,
+                        PgfPrintContext *ctxt, int prio,
+                        PgfMarshaller *m)
+{
+    PgfPrinter printer(ctxt,prio,m);
+    m->match_type(&printer, ty);
+    return printer.get_text();
+}
+
 PGF_API uintptr_t
 pgf_read_type(PgfText *input, PgfUnmarshaller *u)
 {

src/runtime/c/pgf/pgf.h

@@ -232,9 +232,26 @@ int pgf_function_is_constructor(PgfPGF *pgf, PgfText *funname);
 PGF_API_DECL
 prob_t pgf_function_prob(PgfPGF *pgf, PgfText *funname);
 
+typedef struct PgfPrintContext PgfPrintContext;
+
+struct PgfPrintContext {
+	PgfPrintContext* next;
+	PgfText name;
+};
+
+PGF_API_DECL
+PgfText *pgf_print_expr(uintptr_t e,
+                        PgfPrintContext *ctxt, int prio,
+                        PgfMarshaller *m);
+
 PGF_API_DECL
 uintptr_t pgf_read_expr(PgfText *input, PgfUnmarshaller *u);
 
+PGF_API_DECL
+PgfText *pgf_print_type(uintptr_t ty,
+                        PgfPrintContext *ctxt, int prio,
+                        PgfMarshaller *m);
+
 PGF_API_DECL
 uintptr_t pgf_read_type(PgfText *input, PgfUnmarshaller *u);
 

src/runtime/c/pgf/printer.cxx

@@ -0,0 +1,362 @@
+#include <stdarg.h>
+#include "data.h"
+#include "printer.h"
+
+PgfPrinter::PgfPrinter(PgfPrintContext *context, int priority,
+                       PgfMarshaller *marshaller)
+{
+    ctxt             = context;
+    printing_lambdas = false;
+
+    prio = priority;
+
+    res      = NULL;
+
+    m    = marshaller;
+}
+
+void PgfPrinter::puts(PgfText *s)
+{
+    if (res) {
+        size_t size = res->size+s->size;
+
+        res = (PgfText *) realloc(res, sizeof(PgfText)+size+1);
+        memcpy(res->text+res->size, s->text, s->size+1);
+        res->size = size;
+    } else {
+        res = textdup(s);
+    }
+}
+
+void PgfPrinter::puts(const char *s)
+{
+    size_t len = strlen(s);
+
+    if (res) {
+        size_t size = res->size+len;
+
+        res = (PgfText *) realloc(res, sizeof(PgfText)+size+1);
+        memcpy(res->text+res->size, s, len+1);
+        res->size = size;
+    } else {
+        res = (PgfText *) malloc(sizeof(PgfText)+len+1);
+        memcpy(res->text, s, len+1);
+        res->size = len;
+    }
+}
+
+void PgfPrinter::nprintf(size_t buf_size, const char *format, ...)
+{
+    if (res) {
+        size_t size = res->size+buf_size;
+        res = (PgfText *) realloc(res, sizeof(PgfText)+size+1);
+    } else {
+        res = (PgfText *) malloc(sizeof(PgfText)+buf_size+1);
+        res->size = 0;
+    }
+
+    va_list ap;
+    va_start(ap, format);
+    res->size +=
+        vsnprintf(res->text+res->size, buf_size, format, ap);
+    va_end(ap);
+}
+
+PgfText *PgfPrinter::get_text()
+{
+    return res;
+}
+
+void PgfPrinter::flush_lambdas()
+{
+    if (!printing_lambdas)
+        return;
+
+    if (this->btype == PGF_BIND_TYPE_IMPLICIT) {
+        puts("}");
+    }
+    puts("->");
+    printing_lambdas = false;
+}
+
+void PgfPrinter::push_variable(PgfText *name)
+{
+    PgfPrintContext *c = (PgfPrintContext *)
+        malloc(sizeof(PgfPrintContext)+name->size+1);
+    c->next = ctxt;
+    c->name.size = name->size;
+    memcpy(c->name.text, name->text, name->size+1);
+
+    int i = 0;
+    bool clash;
+    do {
+        clash = false;
+        PgfPrintContext *c2 = ctxt;
+        while (c2 != NULL) {
+            if (textcmp(&c->name, &c2->name) == 0) {
+                clash = true;
+                if (i == 0) {
+                    // the first time when we encounter a clash,
+                    // we ensure enough space to add a number to the name.
+                    c =  (PgfPrintContext *)
+                        realloc(c,sizeof(PgfPrintContext)+name->size+1+15);
+                }
+                i++;
+                char *buffer = c->name.text+name->size;
+                snprintf(buffer,15,"%d",i);
+                c->name.size = name->size+strlen(buffer);
+                break;
+            }
+            c2 = c2->next;
+        }
+    } while (clash);
+
+	ctxt = c;
+}
+
+void PgfPrinter::pop_variable()
+{
+    PgfPrintContext *tmp = ctxt;
+    ctxt = ctxt->next;
+    free(tmp);
+}
+
+uintptr_t PgfPrinter::eabs(PgfBindType btype, PgfText *name, uintptr_t body)
+{
+    bool p = (prio > 1);
+    if (p) puts("(");
+
+    push_variable(name);
+
+    if (!printing_lambdas) {
+        // This is the outermost lambda possibly in a chain of nested lambdas
+        printing_lambdas = true;
+        puts("\\");
+        if (btype == PGF_BIND_TYPE_IMPLICIT) {
+            puts("{");
+        }
+    } else {
+        if (btype       == PGF_BIND_TYPE_EXPLICIT &&
+            this->btype == PGF_BIND_TYPE_IMPLICIT) {
+            puts("}");
+        }
+        puts(",");
+        if (btype       == PGF_BIND_TYPE_IMPLICIT &&
+            this->btype == PGF_BIND_TYPE_EXPLICIT) {
+            puts("{");
+        }
+    }
+    this->btype = btype;
+    puts(&ctxt->name);
+
+    prio = 1;
+    m->match_expr(this, body);
+
+    pop_variable();
+
+    if (p) puts(")");
+
+    return 0;
+}
+
+uintptr_t PgfPrinter::eapp(uintptr_t fun, uintptr_t arg)
+{
+    flush_lambdas();
+
+    bool p = (prio > 3);
+    if (p) puts("(");
+
+    prio = 3;
+    m->match_expr(this, fun);
+
+    puts(" ");
+
+    prio = 4;
+    m->match_expr(this, arg);
+
+    if (p) puts(")");
+
+    return 0;
+}
+
+uintptr_t PgfPrinter::elit(uintptr_t lit)
+{
+    flush_lambdas();
+    return m->match_lit(this, lit);
+}
+
+uintptr_t PgfPrinter::emeta(PgfMetaId meta)
+{
+    flush_lambdas();
+
+    if (meta == 0) {
+        puts("?");
+    } else {
+        nprintf(16, "?%d", meta);
+    }
+
+    return 0;
+}
+
+uintptr_t PgfPrinter::efun(PgfText *name)
+{
+    flush_lambdas();
+
+    puts(name);
+    return 0;
+}
+
+uintptr_t PgfPrinter::evar(int index)
+{
+    flush_lambdas();
+
+    PgfPrintContext *var = ctxt;
+    for (int i = 0; i < index; i++) {
+        if (var == NULL)
+            break;
+        var = var->next;
+    }
+    if (var == NULL) {
+        nprintf(16, "#%d", index);
+    } else {
+        puts(&var->name);
+    }
+    return 0;
+}
+
+uintptr_t PgfPrinter::etyped(uintptr_t expr, uintptr_t ty)
+{
+    flush_lambdas();
+
+    puts("<");
+    prio = 0;
+    m->match_expr(this, expr);
+    puts(" : ");
+    prio = 0;
+    m->match_type(this, ty);
+    puts(">");
+    return 0;
+}
+
+uintptr_t PgfPrinter::eimplarg(uintptr_t expr)
+{
+    flush_lambdas();
+
+    puts("{");
+    prio = 0;
+    m->match_expr(this, expr);
+    puts("}");
+    return 0;
+}
+
+uintptr_t PgfPrinter::lint(int v)
+{
+    nprintf(16, "%d", v);
+    return 0;
+}
+
+uintptr_t PgfPrinter::lflt(double v)
+{
+    nprintf(16,"%lg",v);
+    return 0;
+}
+
+uintptr_t PgfPrinter::lstr(PgfText *v)
+{
+    PgfText *charbuf = (PgfText *) alloca(sizeof(PgfText)+7);
+
+    puts("\"");
+    const uint8_t* start = (uint8_t*) v->text;
+    const uint8_t* end   = start + v->size;
+    while (start < end) {
+        const uint8_t* s = start;
+        uint32_t c = pgf_utf8_decode(&s);
+        switch (c) {
+        case '\\':
+            puts("\\\\");
+            break;
+        case '"':
+            puts("\\\"");
+            break;
+        case '\n':
+            puts("\\n");
+            break;
+        case '\r':
+            puts("\\r");
+            break;
+        case '\b':
+            puts("\\b");
+            break;
+        case '\t':
+            puts("\\t");
+            break;
+        case '\0':
+            puts("\\0");
+            break;
+        default:
+            charbuf->size = s-start;
+            memcpy(charbuf->text, start, charbuf->size);
+            charbuf->text[charbuf->size] = 0;
+            puts(charbuf);
+        }
+        start = s;
+    }
+    puts("\"");
+    return 0;
+}
+
+uintptr_t PgfPrinter::dtyp(int n_hypos, PgfTypeHypo *hypos,
+                           PgfText *cat,
+                           int n_exprs, uintptr_t *exprs)
+{
+    bool p = (prio > 0 && n_hypos > 0) ||
+             (prio > 3 && n_exprs > 0);
+    if (p) puts("(");
+
+    PgfPrintContext *save_ctxt = ctxt;
+
+    for (int i = 0; i < n_hypos; i++) {
+        if (textcmp(hypos[i].cid, &wildcard) == 0) {
+            prio = 1;
+            m->match_type(this, hypos[i].type);
+        } else {
+            push_variable(hypos[i].cid);
+
+            puts("(");
+            if (hypos[i].bind_type == PGF_BIND_TYPE_IMPLICIT)
+                puts("{");
+            puts(&ctxt->name);
+            if (hypos[i].bind_type == PGF_BIND_TYPE_IMPLICIT)
+                puts("}");
+            puts(" : ");
+            m->match_type(this, hypos[i].type);
+            puts(")");
+        }
+
+        puts(" -> ");
+    }
+
+    puts(cat);
+
+    for (int i = 0; i < n_exprs; i++) {
+        puts(" ");
+        prio = 4;
+        m->match_expr(this, exprs[i]);
+    }
+
+    while (ctxt != save_ctxt) {
+        pop_variable();
+    }
+
+    if (p) puts(")");
+
+    return 0;
+}
+
+void PgfPrinter::free_ref(uintptr_t x)
+{
+}
+
+void PgfPrinter::free_me()
+{
+}

src/runtime/c/pgf/printer.h

@@ -0,0 +1,66 @@
+#ifndef PRINTER_H
+#define PRINTER_H
+
+class PGF_INTERNAL_DECL PgfPrinter : public PgfUnmarshaller {
+    // List of free variables in order reverse to the order of binding
+    PgfPrintContext *ctxt;
+
+    // Each lambda abstraction is a separate object, but when we print
+    // them we want to colapse them into one abstraction with
+    // several variables. For that reason, if we are in the process
+    // of printing nested lambda abstractions, printing_lambdas is true
+    // and btype is the binding type for the last variable.
+    bool printing_lambdas;
+    PgfBindType btype;
+
+    // This method should be called before printing any other form of
+    // expression but a lambda. In this way the printing of a chain
+    // of lambda expressions is finished.
+    void flush_lambdas();
+
+    // Push a new variable in the printing context. If the name
+    // collides with an existing variable, the variable is renamed
+    // by adding a number.
+    void push_variable(PgfText *name);
+
+    // Pop the last variable name from the context.
+    void pop_variable();
+
+    // The current operator priority
+    int prio;
+
+    // The generated text
+    PgfText *res;
+
+    // The marshaller for pattern matching
+    PgfMarshaller *m;
+
+public:
+    PgfPrinter(PgfPrintContext *context, int priority,
+               PgfMarshaller *marshaller);
+
+    void puts(PgfText *s);
+    void puts(const char *s);
+    void nprintf(size_t buf_size, const char *format, ...) __attribute__ ((format (printf, 3, 4)));
+
+    PgfText *get_text();
+
+    virtual uintptr_t eabs(PgfBindType btype, PgfText *name, uintptr_t body);
+    virtual uintptr_t eapp(uintptr_t fun, uintptr_t arg);
+    virtual uintptr_t elit(uintptr_t lit);
+    virtual uintptr_t emeta(PgfMetaId meta);
+    virtual uintptr_t efun(PgfText *name);
+    virtual uintptr_t evar(int index);
+    virtual uintptr_t etyped(uintptr_t expr, uintptr_t typ);
+    virtual uintptr_t eimplarg(uintptr_t expr);
+    virtual uintptr_t lint(int v);
+    virtual uintptr_t lflt(double v);
+    virtual uintptr_t lstr(PgfText *v);
+    virtual uintptr_t dtyp(int n_hypos, PgfTypeHypo *hypos,
+                           PgfText *cat,
+                           int n_exprs, uintptr_t *exprs);
+    virtual void free_ref(uintptr_t x);
+    virtual void free_me();
+};
+
+#endif

src/runtime/c/pgf/text.cxx

@@ -19,9 +19,9 @@ int textcmp(PgfText *t1, PgfText *t2)
 PGF_INTERNAL
 PgfText* textdup(PgfText *t1)
 {
-    PgfText *t2 = (PgfText *) malloc(sizeof(PgfText) + t1->size + 1);
-    t2->size = t1->size;
-    memcpy(t2->text, t1->text, t1->size+1);
+    size_t size = sizeof(PgfText)+t1->size+1;
+    PgfText *t2 = (PgfText *) malloc(size);
+    memcpy(t2, t1, size);
     return t2;
 }
 

src/runtime/haskell/PGF2.hsc

@@ -24,7 +24,7 @@ module PGF2 (-- * PGF
              Fun, functions, functionsByCat,
              functionType, functionIsConstructor, functionProb,
              -- ** Expressions
-             Expr(..), Literal(..), readExpr,
+             Expr(..), Literal(..), showExpr, readExpr,
              mkAbs,    unAbs,
              mkApp,    unApp, unapply,
              mkStr,    unStr,
@@ -34,7 +34,7 @@ module PGF2 (-- * PGF
              mkMeta,   unMeta,
              -- ** Types
              Type(..), Hypo, BindType(..), startCat,
-             readType,
+             readType, showType,
              mkType, unType,
              mkHypo, mkDepHypo, mkImplHypo,
 
@@ -277,6 +277,33 @@ functionsByCat p cat =
 -----------------------------------------------------------------------
 -- Expressions & types
 
+-- | renders an expression as a 'String'. The list
+-- of identifiers is the list of all free variables
+-- in the expression in order reverse to the order
+-- of binding.
+showExpr :: [Var] -> Expr -> String
+showExpr scope e =
+  unsafePerformIO $
+  bracket mkMarshaller freeMarshaller $ \m ->
+  bracket (newPrintCtxt scope) freePrintCtxt $ \pctxt ->
+  bracket (newStablePtr e) freeStablePtr $ \c_e ->
+  bracket (pgf_print_expr c_e pctxt 1 m) free $ \c_text ->
+    peekText c_text
+
+newPrintCtxt :: [Var] -> IO (Ptr PgfPrintContext)
+newPrintCtxt []     = return nullPtr
+newPrintCtxt (x:xs) = do
+  pctxt <- newTextEx (#offset PgfPrintContext, name) x
+  newPrintCtxt xs >>= (#poke PgfPrintContext, next) pctxt
+  return pctxt
+
+freePrintCtxt :: Ptr PgfPrintContext -> IO ()
+freePrintCtxt pctxt
+  | pctxt == nullPtr = return ()
+  | otherwise        = do
+      (#peek PgfPrintContext, next) pctxt >>= freePrintCtxt
+      free pctxt
+
 -- | parses a 'String' as an expression
 readExpr :: String -> Maybe Expr
 readExpr str =
@@ -290,6 +317,19 @@ readExpr str =
               freeStablePtr c_expr
               return (Just expr)
 
+-- | renders a type as a 'String'. The list
+-- of identifiers is the list of all free variables
+-- in the type in order reverse to the order
+-- of binding.
+showType :: [Var] -> Type -> String
+showType scope ty =
+  unsafePerformIO $
+  bracket mkMarshaller freeMarshaller $ \m ->
+  bracket (newPrintCtxt scope) freePrintCtxt $ \pctxt ->
+  bracket (newStablePtr ty) freeStablePtr $ \c_ty ->
+  bracket (pgf_print_type c_ty pctxt 0 m) free $ \c_text ->
+    peekText c_text
+
 -- | parses a 'String' as a type
 readType :: String -> Maybe Type
 readType str =

src/runtime/haskell/PGF2/FFI.hsc

@@ -25,6 +25,7 @@ data PgfExn
 data PgfText
 data PgfItor
 data PgfPGF
+data PgfPrintContext
 data PgfConcr
 data PgfTypeHypo
 data PgfMarshaller
@@ -51,9 +52,15 @@ foreign import ccall "&pgf_free"
 foreign import ccall "pgf_abstract_name"
   pgf_abstract_name :: Ptr PgfPGF -> IO (Ptr PgfText)
 
+foreign import ccall "pgf_print_expr"
+  pgf_print_expr :: StablePtr Expr -> Ptr PgfPrintContext -> CInt -> Ptr PgfMarshaller -> IO (Ptr PgfText)
+
 foreign import ccall "pgf_read_expr"
   pgf_read_expr :: Ptr PgfText -> Ptr PgfUnmarshaller -> IO (StablePtr Expr)
 
+foreign import ccall "pgf_print_type"
+  pgf_print_type :: StablePtr Type -> Ptr PgfPrintContext -> CInt -> Ptr PgfMarshaller -> IO (Ptr PgfText)
+
 foreign import ccall "pgf_read_type"
   pgf_read_type :: Ptr PgfText -> Ptr PgfUnmarshaller -> IO (StablePtr Type)
 
@@ -105,6 +112,16 @@ peekText ptr =
                 cs <- decode pptr end
                 return (((toEnum . fromEnum) x) : cs)
 
+newTextEx :: Int -> String -> IO (Ptr a)
+newTextEx offs s = do
+  ptr <- mallocBytes (offs + (#size PgfText) + size + 1)
+  let ptext = ptr `plusPtr` offs
+  (#poke PgfText, size) ptext (fromIntegral size :: CSize)
+  pokeUtf8CString s (ptext `plusPtr` (#const offsetof(PgfText, text)))
+  return ptr
+  where
+    size = utf8Length s
+
 newText :: String -> IO (Ptr PgfText)
 newText s = do
   ptr <- mallocBytes ((#size PgfText) + size + 1)

src/runtime/haskell/tests/basic.hs

@@ -4,10 +4,11 @@ import PGF2
 
 main = do
   x  <- testLoadFailure "non-existing.pgf"
-  x  <- testLoadFailure "tests/basic.gf"
+  y  <- testLoadFailure "tests/basic.gf"
   gr <- readPGF "tests/basic.pgf"
   runTestTTAndExit $
-    TestList [TestCase (assertBool  "loading failure handled" x)
+    TestList [TestCase (assertBool  "missing file" x)
+             ,TestCase (assertBool  "frong file format" y)
              ,TestCase (assertEqual "abstract names" "basic" (abstractName gr))
              ,TestCase (assertEqual "abstract categories" ["Float","Int","N","P","S","String"] (categories gr))
              ,TestCase (assertEqual "abstract functions" ["c","ind","s","z"] (functions gr))
@@ -18,13 +19,46 @@ main = do
              ,TestCase (assertBool  "type of s" (eqJust (readType "N->N") (functionType gr "s")))
              ,TestCase (assertBool  "type of c" (eqJust (readType "N->S") (functionType gr "c")))
              ,TestCase (assertEqual "category context 1"  [] (categoryContext gr "N"))
-             ,TestCase (assertEqual "category context 1"  [] (categoryContext gr "S"))
-             ,TestCase (assertEqual "category context 1"  [(Explicit,"_",DTyp [] "N" [])] (categoryContext gr "P"))
-             ,TestCase (assertEqual "category context 1"  [] (categoryContext gr "X")) -- no such category
+             ,TestCase (assertEqual "category context 2"  [] (categoryContext gr "S"))
+             ,TestCase (assertEqual "category context 3"  [(Explicit,"_",DTyp [] "N" [])] (categoryContext gr "P"))
+             ,TestCase (assertEqual "category context 4"  [] (categoryContext gr "X")) -- no such category
              ,TestCase (assertEqual "function is constructor 1"  True  (functionIsConstructor gr "s"))
              ,TestCase (assertEqual "function is constructor 2"  True  (functionIsConstructor gr "z"))
              ,TestCase (assertEqual "function is constructor 3"  True  (functionIsConstructor gr "c"))
              ,TestCase (assertEqual "function is constructor 4"  False (functionIsConstructor gr "ind"))
+             ,TestCase (assertEqual "show expression 1" "f x y" (showExpr [] (EApp (EApp (EFun "f") (EFun "x")) (EFun "y"))))
+             ,TestCase (assertEqual "show expression 2" "f (g x)" (showExpr [] (EApp (EFun "f") (EApp (EFun "g") (EFun "x")))))
+             ,TestCase (assertEqual "show expression 3" "f {g x}" (showExpr [] (EApp (EFun "f") (EImplArg (EApp (EFun "g") (EFun "x"))))))
+             ,TestCase (assertEqual "show expression 4" "x" (showExpr ["x"] (EVar 0)))
+             ,TestCase (assertEqual "show expression 5" "#1" (showExpr ["x"] (EVar 1)))
+             ,TestCase (assertEqual "show expression 6" "z" (showExpr ["z","y","x"] (EVar 0)))
+             ,TestCase (assertEqual "show expression 7" "y" (showExpr ["z","y","x"] (EVar 1)))
+             ,TestCase (assertEqual "show expression 8" "\\w->w" (showExpr ["z","y","x"] (EAbs Explicit "w" (EVar 0))))
+             ,TestCase (assertEqual "show expression 9" "\\v,w->z" (showExpr ["z","y","x"] (EAbs Explicit "v" (EAbs Explicit "w" (EVar 2)))))
+             ,TestCase (assertEqual "show expression 10" "\\v,{w}->z" (showExpr ["z","y","x"] (EAbs Explicit "v" (EAbs Implicit "w" (EVar 2)))))
+             ,TestCase (assertEqual "show expression 11" "\\v,{w},z->z" (showExpr ["y","x"] (EAbs Explicit "v" (EAbs Implicit "w" (EAbs Explicit "z" (EVar 0))))))
+             ,TestCase (assertEqual "show expression 12" "\\v,{w,z}->v" (showExpr ["y","x"] (EAbs Explicit "v" (EAbs Implicit "w" (EAbs Implicit "z" (EVar 2))))))
+             ,TestCase (assertEqual "show expression 13" "\\v,{w,z},t->v" (showExpr ["y","x"] (EAbs Explicit "v" (EAbs Implicit "w" (EAbs Implicit "z" (EAbs Explicit "t" (EVar 3)))))))
+             ,TestCase (assertEqual "show expression 14" "\\u,v,{w,z},t->v" (showExpr ["y","x"] (EAbs Explicit "u" (EAbs Explicit "v" (EAbs Implicit "w" (EAbs Implicit "z" (EAbs Explicit "t" (EVar 3))))))))
+             ,TestCase (assertEqual "show expression 15" "f (\\x->x)" (showExpr [] (EApp (EFun "f") (EAbs Explicit "x" (EVar 0)))))
+             ,TestCase (assertEqual "show expression 16" "?" (showExpr [] (EMeta 0)))
+             ,TestCase (assertEqual "show expression 17" "?42" (showExpr [] (EMeta 42)))
+             ,TestCase (assertEqual "show expression 18" "<z : N>" (showExpr [] (ETyped (EFun "z") (DTyp [] "N" []))))
+             ,TestCase (assertEqual "show expression 19" "42" (showExpr [] (ELit (LInt 42))))
+             ,TestCase (assertEqual "show expression 20" "3.14" (showExpr [] (ELit (LFlt 3.14))))
+             ,TestCase (assertEqual "show expression 21" "\"abc\"" (showExpr [] (ELit (LStr "abc"))))
+             ,TestCase (assertEqual "show expression 22" "\"ab\\0c\"" (showExpr [] (ELit (LStr "ab\0c"))))
+             ,TestCase (assertEqual "show expression 23" "\"ab\\nc\"" (showExpr [] (ELit (LStr "ab\nc"))))
+             ,TestCase (assertEqual "show type 1" "N" (showType [] (DTyp [] "N" [])))
+             ,TestCase (assertEqual "show type 2" "N -> N" (showType [] (DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])))
+             ,TestCase (assertEqual "show type 3" "(N -> N) -> N" (showType [] (DTyp [(Explicit,"_",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "N" [])))
+             ,TestCase (assertEqual "show type 4" "(x : N) -> P x" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" [])] "P" [EVar 0])))
+             ,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")])))
+             ,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)])))
+             ,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)])))
+             ,TestCase (assertEqual "fresh variables 1" "\\v,v1->v1" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EVar 0)))))
+             ,TestCase (assertEqual "fresh variables 2" "\\v,v1->v" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EVar 1)))))
+             ,TestCase (assertEqual "fresh variables 3" "\\v,v1,v2->v1" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EAbs Explicit "v" (EVar 1))))))
              ]
 
 testLoadFailure fpath = do