diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 8eff2a1d82c..bf2c1b46650 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ansi_c_typecheck.h"
 #include "ansi_c_parser.h"
 #include "expr2c.h"
+#include "expr2c_class.h"
 #include "c_preprocess.h"
 #include "ansi_c_internal_additions.h"
 #include "type2name.h"
@@ -285,6 +286,24 @@ bool ansi_c_languaget::from_type(
 
 /*******************************************************************\
 
+Function: ansi_c_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+ansi_c_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2ct(ns));
+}
+
+/*******************************************************************\
+
 Function: ansi_c_languaget::type_to_name
 
   Inputs:
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 0dd1d8bb6fa..25312253574 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -53,6 +53,9 @@ class ansi_c_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool type_to_name(
     const typet &type,
     std::string &name,
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index a6975bdab19..5b26d02ce64 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -204,6 +204,7 @@ Function: expr2ct::convert
 
 std::string expr2ct::convert(const typet &src)
 {
+  assert(next_pretty_printer && "Next pretty-printer should be set");
   return convert_rec(src, c_qualifierst(), "");
 }
 
@@ -679,14 +680,7 @@ std::string expr2ct::convert_rec(
     return q+"__attribute__(("+id2string(src.id())+")) void"+d;
   }
 
-  {
-    lispexprt lisp;
-    irep2lisp(src, lisp);
-    std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
-    dest+=d;
-
-    return dest;
-  }
+  return next_pretty_printer->convert(src);
 }
 
 /*******************************************************************\
@@ -5009,7 +5003,7 @@ std::string expr2ct::convert(
     return convert(src.type());
 
   // no C language expression for internal representation
-  return convert_norep(src, precedence);
+  return next_pretty_printer->convert(src);
 }
 
 /*******************************************************************\
@@ -5046,7 +5040,9 @@ std::string expr2c(const exprt &expr, const namespacet &ns)
 {
   std::string code;
   expr2ct expr2c(ns);
+  norep_pretty_printert norep;
   expr2c.get_shorthands(expr);
+  expr2c.set_next_pretty_printer(&norep);
   return expr2c.convert(expr);
 }
 
@@ -5065,6 +5061,8 @@ Function: type2c
 std::string type2c(const typet &type, const namespacet &ns)
 {
   expr2ct expr2c(ns);
+  norep_pretty_printert norep;
+  expr2c.set_next_pretty_printer(&norep);
   // expr2c.get_shorthands(expr);
   return expr2c.convert(type);
 }
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index b0647fb7fbb..bef61fc5f97 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -16,17 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
+#include <langapi/pretty_printer.h>
+
 class c_qualifierst;
 class namespacet;
 
-class expr2ct
+class expr2ct:public pretty_printert
 {
 public:
   explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
   virtual ~expr2ct() { }
 
-  virtual std::string convert(const typet &src);
-  virtual std::string convert(const exprt &src);
+  std::string convert(const typet &src) override;
+  std::string convert(const exprt &src) override;
 
   void get_shorthands(const exprt &expr);
 
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 11ff42414f1..e558f478665 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_internal_additions.h"
 #include "cpp_language.h"
 #include "expr2cpp.h"
+#include "expr2cpp_class.h"
 #include "cpp_parser.h"
 #include "cpp_typecheck.h"
 #include "cpp_type2name.h"
@@ -362,6 +363,24 @@ bool cpp_languaget::from_type(
 
 /*******************************************************************\
 
+Function: cpp_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+cpp_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2cppt(ns));
+}
+
+/*******************************************************************\
+
 Function: cpp_languaget::type_to_name
 
   Inputs:
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 32a4e281f78..b818d64f4d6 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -62,6 +62,9 @@ class cpp_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool type_to_name(
     const typet &type,
     std::string &name,
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
index 052483a06f0..0a12129887e 100644
--- a/src/cpp/expr2cpp.cpp
+++ b/src/cpp/expr2cpp.cpp
@@ -17,44 +17,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <ansi-c/c_misc.h>
 #include <ansi-c/c_qualifiers.h>
-#include <ansi-c/expr2c_class.h>
 
 #include "expr2cpp.h"
-
-class expr2cppt:public expr2ct
-{
-public:
-  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
-
-  std::string convert(const exprt &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-  std::string convert(const typet &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-protected:
-  std::string convert(const exprt &src, unsigned &precedence) override;
-  std::string convert_cpp_this(const exprt &src, unsigned precedence);
-  std::string convert_cpp_new(const exprt &src, unsigned precedence);
-  std::string convert_extractbit(const exprt &src, unsigned precedence);
-  std::string convert_extractbits(const exprt &src, unsigned precedence);
-  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
-  std::string convert_struct(const exprt &src, unsigned &precedence) override;
-  std::string convert_code(const codet &src, unsigned indent) override;
-  // NOLINTNEXTLINE(whitespace/line_length)
-  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
-
-  std::string convert_rec(
-    const typet &src,
-    const c_qualifierst &qualifiers,
-    const std::string &declarator) override;
-
-  typedef std::unordered_set<std::string, string_hash> id_sett;
-};
+#include "expr2cpp_class.h"
 
 /*******************************************************************\
 
@@ -647,6 +612,8 @@ std::string expr2cpp(const exprt &expr, const namespacet &ns)
 {
   expr2cppt expr2cpp(ns);
   expr2cpp.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2cpp.set_next_pretty_printer(&norep);
   return expr2cpp.convert(expr);
 }
 
@@ -665,5 +632,7 @@ Function: type2cpp
 std::string type2cpp(const typet &type, const namespacet &ns)
 {
   expr2cppt expr2cpp(ns);
+  norep_pretty_printert norep;
+  expr2cpp.set_next_pretty_printer(&norep);
   return expr2cpp.convert(type);
 }
diff --git a/src/cpp/expr2cpp_class.h b/src/cpp/expr2cpp_class.h
new file mode 100644
index 00000000000..555404fbbfe
--- /dev/null
+++ b/src/cpp/expr2cpp_class.h
@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@cs.cmu.edu
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPP_EXPR2CPP_CLASS_H
+#define CPROVER_CPP_EXPR2CPP_CLASS_H
+
+#include <ansi-c/expr2c_class.h>
+
+class expr2cppt:public expr2ct
+{
+public:
+  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
+
+  std::string convert(const exprt &src) override
+  {
+    return expr2ct::convert(src);
+  }
+
+  std::string convert(const typet &src) override
+  {
+    return expr2ct::convert(src);
+  }
+
+protected:
+  std::string convert(const exprt &src, unsigned &precedence) override;
+  std::string convert_cpp_this(const exprt &src, unsigned precedence);
+  std::string convert_cpp_new(const exprt &src, unsigned precedence);
+  std::string convert_extractbit(const exprt &src, unsigned precedence);
+  std::string convert_extractbits(const exprt &src, unsigned precedence);
+  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
+  std::string convert_struct(const exprt &src, unsigned &precedence) override;
+  std::string convert_code(const codet &src, unsigned indent) override;
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
+
+  std::string convert_rec(
+    const typet &src,
+    const c_qualifierst &qualifiers,
+    const std::string &declarator) override;
+
+  typedef std::unordered_set<std::string, string_hash> id_sett;
+};
+
+#endif
diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp
index 3cd487e234a..6e5f4536575 100644
--- a/src/java_bytecode/expr2java.cpp
+++ b/src/java_bytecode/expr2java.cpp
@@ -565,6 +565,8 @@ std::string expr2java(const exprt &expr, const namespacet &ns)
 {
   expr2javat expr2java(ns);
   expr2java.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2java.set_next_pretty_printer(&norep);
   return expr2java.convert(expr);
 }
 
@@ -583,5 +585,7 @@ Function: type2java
 std::string type2java(const typet &type, const namespacet &ns)
 {
   expr2javat expr2java(ns);
+  norep_pretty_printert norep;
+  expr2java.set_next_pretty_printer(&norep);
   return expr2java.convert(type);
 }
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 0864c82b160..011b1bc9dd4 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -850,6 +850,24 @@ bool java_bytecode_languaget::from_type(
 
 /*******************************************************************\
 
+Function: java_bytecode_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+java_bytecode_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2javat(ns));
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_languaget::to_expr
 
   Inputs:
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 46a308ca5fd..166bc2931e0 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -70,6 +70,9 @@ class java_bytecode_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool to_expr(
     const std::string &code,
     const std::string &module,
diff --git a/src/jsil/expr2jsil.cpp b/src/jsil/expr2jsil.cpp
index fde6cf87f00..3bb9b410221 100644
--- a/src/jsil/expr2jsil.cpp
+++ b/src/jsil/expr2jsil.cpp
@@ -9,24 +9,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #include <ansi-c/expr2c_class.h>
 
 #include "expr2jsil.h"
-
-class expr2jsilt:public expr2ct
-{
-public:
-  explicit expr2jsilt(const namespacet &_ns):expr2ct(_ns) { }
-
-  virtual std::string convert(const exprt &src)
-  {
-    return expr2ct::convert(src);
-  }
-
-  virtual std::string convert(const typet &src)
-  {
-    return expr2ct::convert(src);
-  }
-
-protected:
-};
+#include "expr2jsil_class.h"
 
 /*******************************************************************\
 
@@ -44,6 +27,8 @@ std::string expr2jsil(const exprt &expr, const namespacet &ns)
 {
   expr2jsilt expr2jsil(ns);
   expr2jsil.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2jsil.set_next_pretty_printer(&norep);
   return expr2jsil.convert(expr);
 }
 
@@ -62,5 +47,7 @@ Function: type2jsil
 std::string type2jsil(const typet &type, const namespacet &ns)
 {
   expr2jsilt expr2jsil(ns);
+  norep_pretty_printert norep;
+  expr2jsil.set_next_pretty_printer(&norep);
   return expr2jsil.convert(type);
 }
diff --git a/src/jsil/expr2jsil_class.h b/src/jsil/expr2jsil_class.h
new file mode 100644
index 00000000000..1ce743c4414
--- /dev/null
+++ b/src/jsil/expr2jsil_class.h
@@ -0,0 +1,33 @@
+
+/*******************************************************************\
+
+Module: Jsil Language
+
+Author: Michael Tautschnig, tautschn@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_JSIL_EXPR2JSIL_CLASS_H
+#define CPROVER_JSIL_EXPR2JSIL_CLASS_H
+
+#include <ansi-c/expr2c_class.h>
+
+class expr2jsilt:public expr2ct
+{
+public:
+  explicit expr2jsilt(const namespacet &_ns):expr2ct(_ns) { }
+
+  virtual std::string convert(const exprt &src)
+  {
+    return expr2ct::convert(src);
+  }
+
+  virtual std::string convert(const typet &src)
+  {
+    return expr2ct::convert(src);
+  }
+
+protected:
+};
+
+#endif
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index e7277e90728..a7469ef3b7a 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -10,6 +10,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #include <util/get_base_name.h>
 
 #include "expr2jsil.h"
+#include "expr2jsil_class.h"
 #include "jsil_convert.h"
 #include "jsil_entry_point.h"
 #include "jsil_internal_additions.h"
@@ -258,6 +259,24 @@ bool jsil_languaget::from_type(
 
 /*******************************************************************\
 
+Function: jsil_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+jsil_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2jsilt(ns));
+}
+
+/*******************************************************************\
+
 Function: jsil_languaget::to_expr
 
   Inputs:
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 39fe8f27808..72e9be1639f 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -48,6 +48,9 @@ class jsil_languaget:public languaget
     std::string &code,
     const namespacet &ns);
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &);
+
   virtual bool to_expr(
     const std::string &code,
     const std::string &module,
diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp
index d8c53ec9341..fcd639827b7 100644
--- a/src/langapi/language_util.cpp
+++ b/src/langapi/language_util.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/language.h>
 #include <util/std_expr.h>
 
+#include "pretty_printer.h"
 #include "language_util.h"
 #include "mode.h"
 
@@ -48,15 +49,114 @@ static languaget* get_language(
   return ptr;
 }
 
+std::vector<pretty_printer_factoryt> registered_pretty_printers;
+
 /*******************************************************************\
 
-Function: from_expr
+Function: register_global_pretty_printer
 
-  Inputs:
+  Inputs: `new_printer`: factory method returning
+             `unique_ptr<pretty_printert>`
 
  Outputs:
 
- Purpose:
+ Purpose: This registers a custom pretty-printer for use printing
+          expressions with `from_expr` and `from_type` also defined
+          in language_util.h. The function given should allocate
+          an instance of the printer and return a unique_ptr that
+          disposes of it appropriately (so if allocated with `new`,
+          ordinary `std::unique_ptr` will do the trick).
+          `from_expr` and `from_type` will always build a stack of
+          printer classes of the form:
+          L -> C1 -> C2 ... Cn -> X
+
+          L is the language frontend pretty-printer associated
+          with an expression, C1 ... Cn are instances of the registered
+          custom printers in order of registration, and X is the fallback
+          irep-to-lisp printer `norep_pretty_printert`. The -> arrows
+          represent `next_pretty_printer` fields used to defer printing
+          of expressions a particular printer can't handle; all printers
+          in the stack also get `top_pretty_printer` set to point at L,
+          which they should use when printing subexpressions to give
+          the whole stack a chance to provide a representation.
+
+          Note at present language custom printers such as `expr2javat`
+          are subclasses of `expr2ct` rather than using this deferral
+          mechanism; thus even when a Java expression is being printed
+          there is still only one L in the stack, rather than
+          expr2javat -> expr2ct -> C1 ... Cn -> X
+          as one might expect. The language printers (in particular
+          expr2ct) always assume they are at the top of the stack
+          (so top_pretty_printer == this), and will need adapting if
+          we want to e.g. place a custom printer *above* expr2ct
+          in the future.
+
+\*******************************************************************/
+
+void register_global_pretty_printer(pretty_printer_factoryt new_printer)
+{
+  registered_pretty_printers.push_back(new_printer);
+}
+
+/*******************************************************************\
+
+Function: get_pretty_printer_stack
+
+  Inputs: `ns`: namespace
+          `language_printer`: pointer to instance of a pretty-printer
+             that should be placed at the head of the printer stack.
+
+ Outputs:
+
+ Purpose: (See `register_global_pretty_printer` above for context)
+          Takes a reference to language-specific pretty-printer L,
+          instantiates custom printers C1 .. Cn if any have been
+          registered, creates the fallback norep pretty-printer X,
+          and sets their next_ and top_pretty_printer pointers.
+          A vector of unique pointers is returned whose back member
+          is the head of the stack (L, in the notation used above).
+
+\*******************************************************************/
+
+static std::vector<std::unique_ptr<pretty_printert>> get_pretty_printer_stack(
+  const namespacet &ns,
+  std::unique_ptr<pretty_printert> language_printer)
+{
+  std::vector<std::unique_ptr<pretty_printert>> ret;
+  ret.push_back(std::unique_ptr<pretty_printert>(new norep_pretty_printert()));
+  for(const auto &factory : registered_pretty_printers)
+    ret.push_back(factory(ns));
+  ret.push_back(std::move(language_printer));
+
+  // Link the printers together (used for deferral of expressions
+  // a particular printer can't handle)
+  for(std::size_t i=0; i<ret.size()-1; ++i)
+    ret[i+1]->set_next_pretty_printer(ret[i].get());
+
+  // Give all printers in the chain a pointer to the top, for use
+  // printing subexpressions that others should have a chance
+  // to handle:
+  for(std::size_t i=0; i<ret.size(); ++i)
+    ret[i]->set_top_pretty_printer(ret.back().get());
+
+  return ret;
+}
+
+/*******************************************************************\
+
+Function: from_expr
+
+  Inputs: `ns`: global namespace
+          `identifier`: symbol-table identifier associated with `expr`
+            or the empty string if none
+          `expr`: expression to print
+
+ Outputs: Returns pretty-printed string equivalent of `expr`.
+
+ Purpose: Pretty-prints an expression. If custom pretty-printers have
+          been registered they will be instantiated and may take part
+          in printing `expr`; see `register_global_pretty_printer` for
+          details.
 
 \*******************************************************************/
 
@@ -66,22 +166,25 @@ std::string from_expr(
   const exprt &expr)
 {
   std::unique_ptr<languaget> p(get_language(ns, identifier));
-
-  std::string result;
-  p->from_expr(expr, result, ns);
-
-  return result;
+  auto printers=get_pretty_printer_stack(ns, p->get_pretty_printer(ns));
+  return printers.back()->convert(expr);
 }
 
 /*******************************************************************\
 
 Function: from_type
 
-  Inputs:
+  Inputs: `ns`: global namespace
+          `identifier`: symbol-table identifier associated with `type`
+            or the empty string if none
+          `type`: type to print
 
- Outputs:
+ Outputs: Returns pretty-printed string equivalent of `type`.
 
- Purpose:
+ Purpose: Pretty-prints an type. If custom pretty-printers have
+          been registered they will be instantiated and may take part
+          in printing `type`; see `register_global_pretty_printer` for
+          details.
 
 \*******************************************************************/
 
@@ -91,11 +194,8 @@ std::string from_type(
   const typet &type)
 {
   std::unique_ptr<languaget> p(get_language(ns, identifier));
-
-  std::string result;
-  p->from_type(type, result, ns);
-
-  return result;
+  auto printers=get_pretty_printer_stack(ns, p->get_pretty_printer(ns));
+  return printers.back()->convert(type);
 }
 
 /*******************************************************************\
diff --git a/src/langapi/language_util.h b/src/langapi/language_util.h
index ded56e9ba04..dd538c0b128 100644
--- a/src/langapi/language_util.h
+++ b/src/langapi/language_util.h
@@ -9,7 +9,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_LANGAPI_LANGUAGE_UTIL_H
 #define CPROVER_LANGAPI_LANGUAGE_UTIL_H
 
+#include <memory>
+#include <functional>
+
 #include <util/irep.h>
+#include <langapi/pretty_printer.h>
 
 class exprt;
 class namespacet;
@@ -29,6 +33,11 @@ std::string from_type(
 
 std::string from_type(const typet &type);
 
+typedef std::function<std::unique_ptr<pretty_printert>(const namespacet &)>
+  pretty_printer_factoryt;
+
+void register_global_pretty_printer(pretty_printer_factoryt);
+
 exprt to_expr(
   const namespacet &ns,
   const irep_idt &identifier,
diff --git a/src/langapi/pretty_printer.h b/src/langapi/pretty_printer.h
new file mode 100644
index 00000000000..a9684533b21
--- /dev/null
+++ b/src/langapi/pretty_printer.h
@@ -0,0 +1,86 @@
+/*******************************************************************\
+
+Module: Generic expression / type pretty-printer
+
+Author: Chris Smowton, chris.smowton@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_LANGAPI_PRETTY_PRINTER_H
+#define CPROVER_LANGAPI_PRETTY_PRINTER_H
+
+#include <util/lispirep.h>
+#include <util/lispexpr.h>
+#include <util/expr.h>
+#include <util/type.h>
+// Borrow MetaString, a simple string-escaping routine
+#include <ansi-c/c_misc.h>
+
+#include <cassert>
+
+/*
+ * Interface to an expression and/or type pretty-printer.
+ * The convert(...) routines should pretty-print the expressions
+ * they know how to deal with, and defer to next_pretty_printer
+ * for those they can't handle, and top_pretty_printer for
+ * subexpressions (whether it understands them or not).
+ * Per default they always defer.
+ * See `util/language_util.h` and particularly
+ * `register_global_pretty_printer` for detail on how these are used.
+ */
+class pretty_printert
+{
+ public:
+  pretty_printert():
+  next_pretty_printer(nullptr),
+  top_pretty_printer(nullptr)
+  {}
+
+  virtual ~pretty_printert() {}
+
+  virtual std::string convert(const typet &src)
+  {
+    assert(next_pretty_printer);
+    return next_pretty_printer->convert(src);
+  }
+  virtual std::string convert(const exprt &src)
+  {
+    assert(next_pretty_printer);
+    return next_pretty_printer->convert(src);
+  }
+
+  void set_next_pretty_printer(
+    pretty_printert *next)
+  {
+    next_pretty_printer=next;
+  }
+  void set_top_pretty_printer(
+    pretty_printert *top)
+  {
+    top_pretty_printer=top;
+  }
+
+ protected:
+  pretty_printert *next_pretty_printer;
+  pretty_printert *top_pretty_printer;
+};
+
+class norep_pretty_printert:public pretty_printert
+{
+ public:
+  std::string convert(const typet &src) override
+  {
+    lispexprt lisp;
+    irep2lisp(src, lisp);
+    return "irep(\""+MetaString(lisp.expr2string())+"\")";
+  }
+
+  std::string convert(const exprt &src) override
+  {
+    lispexprt lisp;
+    irep2lisp(src, lisp);
+    return "irep(\""+MetaString(lisp.expr2string())+"\")";
+  }
+};
+
+#endif
diff --git a/src/util/language.h b/src/util/language.h
index 6a97ec0a917..cc5929d6e21 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -12,6 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <iosfwd>
 #include <string>
+#include <memory>
+
+#include <langapi/pretty_printer.h>
 
 #include "message.h"
 
@@ -87,7 +90,6 @@ class languaget:public messaget
   virtual void show_parse(std::ostream &out)=0;
 
   // conversion of expressions
-
   virtual bool from_expr(
     const exprt &expr,
     std::string &code,
@@ -98,6 +100,9 @@ class languaget:public messaget
     std::string &code,
     const namespacet &ns);
 
+  virtual std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &)=0;
+
   virtual bool type_to_name(
     const typet &type,
     std::string &name,