Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

16 files changed, 0 insertions, 2398 deletions

diff --git a/src/pprint/AUTHORS b/src/pprint/AUTHORS
deleted file mode 100644
index 6060ac93..00000000
--- a/src/pprint/AUTHORS
+++ /dev/null
@@ -1,3 +0,0 @@
-PPrint was written by François Pottier and Nicolas Pouillard, with
-contributions by Yann Régis-Gianas, Gabriel Scherer,  and Jonathan
-Protzenko.
diff --git a/src/pprint/CHANGES b/src/pprint/CHANGES
deleted file mode 100644
index 69747a41..00000000
--- a/src/pprint/CHANGES
+++ /dev/null
@@ -1,27 +0,0 @@
-2014/04/11
-Changed the behavior of [align], which was not consistent with its documentation.
-[align] now sets the indentation level to the current column. In particular, this
-means that [align (align d)] is equivalent to [align d], which was not the case
-previously. Thanks to Dmitry Grebeniuk for reporting this issue.
-
-2014/04/03
-The library is now extensible (in principle). A [custom] document constructor
-allows the user to define her own documents, as long as they fit the manner
-in which the current rendering engine works.
-
-The [compact] rendering engine is now tail-recursive too.
-
-2014/03/21
-Minor optimisation in the smart constructor [group].
-
-2014/03/13
-New (simpler) pretty-printing engine. The representation of documents in
-memory is slightly larger; document construction is perhaps slightly slower,
-while rendering is significantly faster. (Construction dominates rendering.)
-The rendering speed is now guaranteed to be independent of the width
-parameter. The price to pay for this simplification is that the primitive
-document constructors [column] and [nesting] are no longer supported. The
-API is otherwise unchanged.
-
-2013/01/31
-First official release of PPrint.
diff --git a/src/pprint/LICENSE b/src/pprint/LICENSE
deleted file mode 100644
index d6eb151e..00000000
--- a/src/pprint/LICENSE
+++ /dev/null
@@ -1,517 +0,0 @@
-
-CeCILL-C FREE SOFTWARE LICENSE AGREEMENT
-
-
-    Notice
-
-This Agreement is a Free Software license agreement that is the result
-of discussions between its authors in order to ensure compliance with
-the two main principles guiding its drafting:
-
-    * firstly, compliance with the principles governing the distribution
-      of Free Software: access to source code, broad rights granted to
-      users,
-    * secondly, the election of a governing law, French law, with which
-      it is conformant, both as regards the law of torts and
-      intellectual property law, and the protection that it offers to
-      both authors and holders of the economic rights over software.
-
-The authors of the CeCILL-C (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre])
-license are:
-
-Commissariat à l'Energie Atomique - CEA, a public scientific, technical
-and industrial research establishment, having its principal place of
-business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France.
-
-Centre National de la Recherche Scientifique - CNRS, a public scientific
-and technological establishment, having its principal place of business
-at 3 rue Michel-Ange, 75794 Paris cedex 16, France.
-
-Institut National de Recherche en Informatique et en Automatique -
-INRIA, a public scientific and technological establishment, having its
-principal place of business at Domaine de Voluceau, Rocquencourt, BP
-105, 78153 Le Chesnay cedex, France.
-
-
-    Preamble
-
-The purpose of this Free Software license agreement is to grant users
-the right to modify and re-use the software governed by this license.
-
-The exercising of this right is conditional upon the obligation to make
-available to the community the modifications made to the source code of
-the software so as to contribute to its evolution.
-
-In consideration of access to the source code and the rights to copy,
-modify and redistribute granted by the license, users are provided only
-with a limited warranty and the software's author, the holder of the
-economic rights, and the successive licensors only have limited liability.
-
-In this respect, the risks associated with loading, using, modifying
-and/or developing or reproducing the software by the user are brought to
-the user's attention, given its Free Software status, which may make it
-complicated to use, with the result that its use is reserved for
-developers and experienced professionals having in-depth computer
-knowledge. Users are therefore encouraged to load and test the
-suitability of the software as regards their requirements in conditions
-enabling the security of their systems and/or data to be ensured and,
-more generally, to use and operate it in the same conditions of
-security. This Agreement may be freely reproduced and published,
-provided it is not altered, and that no provisions are either added or
-removed herefrom.
-
-This Agreement may apply to any or all software for which the holder of
-the economic rights decides to submit the use thereof to its provisions.
-
-
-    Article 1 - DEFINITIONS
-
-For the purpose of this Agreement, when the following expressions
-commence with a capital letter, they shall have the following meaning:
-
-Agreement: means this license agreement, and its possible subsequent
-versions and annexes.
-
-Software: means the software in its Object Code and/or Source Code form
-and, where applicable, its documentation, "as is" when the Licensee
-accepts the Agreement.
-
-Initial Software: means the Software in its Source Code and possibly its
-Object Code form and, where applicable, its documentation, "as is" when
-it is first distributed under the terms and conditions of the Agreement.
-
-Modified Software: means the Software modified by at least one
-Integrated Contribution.
-
-Source Code: means all the Software's instructions and program lines to
-which access is required so as to modify the Software.
-
-Object Code: means the binary files originating from the compilation of
-the Source Code.
-
-Holder: means the holder(s) of the economic rights over the Initial
-Software.
-
-Licensee: means the Software user(s) having accepted the Agreement.
-
-Contributor: means a Licensee having made at least one Integrated
-Contribution.
-
-Licensor: means the Holder, or any other individual or legal entity, who
-distributes the Software under the Agreement.
-
-Integrated Contribution: means any or all modifications, corrections,
-translations, adaptations and/or new functions integrated into the
-Source Code by any or all Contributors.
-
-Related Module: means a set of sources files including their
-documentation that, without modification to the Source Code, enables
-supplementary functions or services in addition to those offered by the
-Software.
-
-Derivative Software: means any combination of the Software, modified or
-not, and of a Related Module.
-
-Parties: mean both the Licensee and the Licensor.
-
-These expressions may be used both in singular and plural form.
-
-
-    Article 2 - PURPOSE
-
-The purpose of the Agreement is the grant by the Licensor to the
-Licensee of a non-exclusive, transferable and worldwide license for the
-Software as set forth in Article 5 hereinafter for the whole term of the
-protection granted by the rights over said Software. 
-
-
-    Article 3 - ACCEPTANCE
-
-3.1 The Licensee shall be deemed as having accepted the terms and
-conditions of this Agreement upon the occurrence of the first of the
-following events:
-
-    * (i) loading the Software by any or all means, notably, by
-      downloading from a remote server, or by loading from a physical
-      medium;
-    * (ii) the first time the Licensee exercises any of the rights
-      granted hereunder.
-
-3.2 One copy of the Agreement, containing a notice relating to the
-characteristics of the Software, to the limited warranty, and to the
-fact that its use is restricted to experienced users has been provided
-to the Licensee prior to its acceptance as set forth in Article 3.1
-hereinabove, and the Licensee hereby acknowledges that it has read and
-understood it.
-
-
-    Article 4 - EFFECTIVE DATE AND TERM
-
-
-      4.1 EFFECTIVE DATE
-
-The Agreement shall become effective on the date when it is accepted by
-the Licensee as set forth in Article 3.1.
-
-
-      4.2 TERM
-
-The Agreement shall remain in force for the entire legal term of
-protection of the economic rights over the Software.
-
-
-    Article 5 - SCOPE OF RIGHTS GRANTED
-
-The Licensor hereby grants to the Licensee, who accepts, the following
-rights over the Software for any or all use, and for the term of the
-Agreement, on the basis of the terms and conditions set forth hereinafter.
-
-Besides, if the Licensor owns or comes to own one or more patents
-protecting all or part of the functions of the Software or of its
-components, the Licensor undertakes not to enforce the rights granted by
-these patents against successive Licensees using, exploiting or
-modifying the Software. If these patents are transferred, the Licensor
-undertakes to have the transferees subscribe to the obligations set
-forth in this paragraph.
-
-
-      5.1 RIGHT OF USE
-
-The Licensee is authorized to use the Software, without any limitation
-as to its fields of application, with it being hereinafter specified
-that this comprises:
-
-   1. permanent or temporary reproduction of all or part of the Software
-      by any or all means and in any or all form.
-
-   2. loading, displaying, running, or storing the Software on any or
-      all medium.
-
-   3. entitlement to observe, study or test its operation so as to
-      determine the ideas and principles behind any or all constituent
-      elements of said Software. This shall apply when the Licensee
-      carries out any or all loading, displaying, running, transmission
-      or storage operation as regards the Software, that it is entitled
-      to carry out hereunder.
-
-
-      5.2 RIGHT OF MODIFICATION
-
-The right of modification includes the right to translate, adapt,
-arrange, or make any or all modifications to the Software, and the right
-to reproduce the resulting software. It includes, in particular, the
-right to create a Derivative Software.
-
-The Licensee is authorized to make any or all modification to the
-Software provided that it includes an explicit notice that it is the
-author of said modification and indicates the date of the creation thereof.
-
-
-      5.3 RIGHT OF DISTRIBUTION
-
-In particular, the right of distribution includes the right to publish,
-transmit and communicate the Software to the general public on any or
-all medium, and by any or all means, and the right to market, either in
-consideration of a fee, or free of charge, one or more copies of the
-Software by any means.
-
-The Licensee is further authorized to distribute copies of the modified
-or unmodified Software to third parties according to the terms and
-conditions set forth hereinafter.
-
-
-        5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION
-
-The Licensee is authorized to distribute true copies of the Software in
-Source Code or Object Code form, provided that said distribution
-complies with all the provisions of the Agreement and is accompanied by:
-
-   1. a copy of the Agreement,
-
-   2. a notice relating to the limitation of both the Licensor's
-      warranty and liability as set forth in Articles 8 and 9,
-
-and that, in the event that only the Object Code of the Software is
-redistributed, the Licensee allows effective access to the full Source
-Code of the Software at a minimum during the entire period of its
-distribution of the Software, it being understood that the additional
-cost of acquiring the Source Code shall not exceed the cost of
-transferring the data.
-
-
-        5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE
-
-When the Licensee makes an Integrated Contribution to the Software, the
-terms and conditions for the distribution of the resulting Modified
-Software become subject to all the provisions of this Agreement.
-
-The Licensee is authorized to distribute the Modified Software, in
-source code or object code form, provided that said distribution
-complies with all the provisions of the Agreement and is accompanied by:
-
-   1. a copy of the Agreement,
-
-   2. a notice relating to the limitation of both the Licensor's
-      warranty and liability as set forth in Articles 8 and 9,
-
-and that, in the event that only the object code of the Modified
-Software is redistributed, the Licensee allows effective access to the
-full source code of the Modified Software at a minimum during the entire
-period of its distribution of the Modified Software, it being understood
-that the additional cost of acquiring the source code shall not exceed
-the cost of transferring the data.
-
-
-        5.3.3 DISTRIBUTION OF DERIVATIVE SOFTWARE
-
-When the Licensee creates Derivative Software, this Derivative Software
-may be distributed under a license agreement other than this Agreement,
-subject to compliance with the requirement to include a notice
-concerning the rights over the Software as defined in Article 6.4.
-In the event the creation of the Derivative Software required modification 
-of the Source Code, the Licensee undertakes that:
-
-   1. the resulting Modified Software will be governed by this Agreement,
-   2. the Integrated Contributions in the resulting Modified Software
-      will be clearly identified and documented,
-   3. the Licensee will allow effective access to the source code of the
-      Modified Software, at a minimum during the entire period of
-      distribution of the Derivative Software, such that such
-      modifications may be carried over in a subsequent version of the
-      Software; it being understood that the additional cost of
-      purchasing the source code of the Modified Software shall not
-      exceed the cost of transferring the data.
-
-
-        5.3.4 COMPATIBILITY WITH THE CeCILL LICENSE
-
-When a Modified Software contains an Integrated Contribution subject to
-the CeCILL license agreement, or when a Derivative Software contains a
-Related Module subject to the CeCILL license agreement, the provisions
-set forth in the third item of Article 6.4 are optional.
-
-
-    Article 6 - INTELLECTUAL PROPERTY
-
-
-      6.1 OVER THE INITIAL SOFTWARE
-
-The Holder owns the economic rights over the Initial Software. Any or
-all use of the Initial Software is subject to compliance with the terms
-and conditions under which the Holder has elected to distribute its work
-and no one shall be entitled to modify the terms and conditions for the
-distribution of said Initial Software.
-
-The Holder undertakes that the Initial Software will remain ruled at
-least by this Agreement, for the duration set forth in Article 4.2.
-
-
-      6.2 OVER THE INTEGRATED CONTRIBUTIONS
-
-The Licensee who develops an Integrated Contribution is the owner of the
-intellectual property rights over this Contribution as defined by
-applicable law.
-
-
-      6.3 OVER THE RELATED MODULES
-
-The Licensee who develops a Related Module is the owner of the
-intellectual property rights over this Related Module as defined by
-applicable law and is free to choose the type of agreement that shall
-govern its distribution under the conditions defined in Article 5.3.3.
-
-
-      6.4 NOTICE OF RIGHTS
-
-The Licensee expressly undertakes:
-
-   1. not to remove, or modify, in any manner, the intellectual property
-      notices attached to the Software;
-
-   2. to reproduce said notices, in an identical manner, in the copies
-      of the Software modified or not;
-
-   3. to ensure that use of the Software, its intellectual property
-      notices and the fact that it is governed by the Agreement is
-      indicated in a text that is easily accessible, specifically from
-      the interface of any Derivative Software.
-
-The Licensee undertakes not to directly or indirectly infringe the
-intellectual property rights of the Holder and/or Contributors on the
-Software and to take, where applicable, vis-à-vis its staff, any and all
-measures required to ensure respect of said intellectual property rights
-of the Holder and/or Contributors.
-
-
-    Article 7 - RELATED SERVICES
-
-7.1 Under no circumstances shall the Agreement oblige the Licensor to
-provide technical assistance or maintenance services for the Software.
-
-However, the Licensor is entitled to offer this type of services. The
-terms and conditions of such technical assistance, and/or such
-maintenance, shall be set forth in a separate instrument. Only the
-Licensor offering said maintenance and/or technical assistance services
-shall incur liability therefor.
-
-7.2 Similarly, any Licensor is entitled to offer to its licensees, under
-its sole responsibility, a warranty, that shall only be binding upon
-itself, for the redistribution of the Software and/or the Modified
-Software, under terms and conditions that it is free to decide. Said
-warranty, and the financial terms and conditions of its application,
-shall be subject of a separate instrument executed between the Licensor
-and the Licensee.
-
-
-    Article 8 - LIABILITY
-
-8.1 Subject to the provisions of Article 8.2, the Licensee shall be
-entitled to claim compensation for any direct loss it may have suffered
-from the Software as a result of a fault on the part of the relevant
-Licensor, subject to providing evidence thereof.
-
-8.2 The Licensor's liability is limited to the commitments made under
-this Agreement and shall not be incurred as a result of in particular:
-(i) loss due the Licensee's total or partial failure to fulfill its
-obligations, (ii) direct or consequential loss that is suffered by the
-Licensee due to the use or performance of the Software, and (iii) more
-generally, any consequential loss. In particular the Parties expressly
-agree that any or all pecuniary or business loss (i.e. loss of data,
-loss of profits, operating loss, loss of customers or orders,
-opportunity cost, any disturbance to business activities) or any or all
-legal proceedings instituted against the Licensee by a third party,
-shall constitute consequential loss and shall not provide entitlement to
-any or all compensation from the Licensor.
-
-
-    Article 9 - WARRANTY
-
-9.1 The Licensee acknowledges that the scientific and technical
-state-of-the-art when the Software was distributed did not enable all
-possible uses to be tested and verified, nor for the presence of
-possible defects to be detected. In this respect, the Licensee's
-attention has been drawn to the risks associated with loading, using,
-modifying and/or developing and reproducing the Software which are
-reserved for experienced users.
-
-The Licensee shall be responsible for verifying, by any or all means,
-the suitability of the product for its requirements, its good working
-order, and for ensuring that it shall not cause damage to either persons
-or properties.
-
-9.2 The Licensor hereby represents, in good faith, that it is entitled
-to grant all the rights over the Software (including in particular the
-rights set forth in Article 5).
-
-9.3 The Licensee acknowledges that the Software is supplied "as is" by
-the Licensor without any other express or tacit warranty, other than
-that provided for in Article 9.2 and, in particular, without any warranty
-as to its commercial value, its secured, safe, innovative or relevant
-nature.
-
-Specifically, the Licensor does not warrant that the Software is free
-from any error, that it will operate without interruption, that it will
-be compatible with the Licensee's own equipment and software
-configuration, nor that it will meet the Licensee's requirements.
-
-9.4 The Licensor does not either expressly or tacitly warrant that the
-Software does not infringe any third party intellectual property right
-relating to a patent, software or any other property right. Therefore,
-the Licensor disclaims any and all liability towards the Licensee
-arising out of any or all proceedings for infringement that may be
-instituted in respect of the use, modification and redistribution of the
-Software. Nevertheless, should such proceedings be instituted against
-the Licensee, the Licensor shall provide it with technical and legal
-assistance for its defense. Such technical and legal assistance shall be
-decided on a case-by-case basis between the relevant Licensor and the
-Licensee pursuant to a memorandum of understanding. The Licensor
-disclaims any and all liability as regards the Licensee's use of the
-name of the Software. No warranty is given as regards the existence of
-prior rights over the name of the Software or as regards the existence
-of a trademark.
-
-
-    Article 10 - TERMINATION
-
-10.1 In the event of a breach by the Licensee of its obligations
-hereunder, the Licensor may automatically terminate this Agreement
-thirty (30) days after notice has been sent to the Licensee and has
-remained ineffective.
-
-10.2 A Licensee whose Agreement is terminated shall no longer be
-authorized to use, modify or distribute the Software. However, any
-licenses that it may have granted prior to termination of the Agreement
-shall remain valid subject to their having been granted in compliance
-with the terms and conditions hereof.
-
-
-    Article 11 - MISCELLANEOUS
-
-
-      11.1 EXCUSABLE EVENTS
-
-Neither Party shall be liable for any or all delay, or failure to
-perform the Agreement, that may be attributable to an event of force
-majeure, an act of God or an outside cause, such as defective
-functioning or interruptions of the electricity or telecommunications
-networks, network paralysis following a virus attack, intervention by
-government authorities, natural disasters, water damage, earthquakes,
-fire, explosions, strikes and labor unrest, war, etc.
-
-11.2 Any failure by either Party, on one or more occasions, to invoke
-one or more of the provisions hereof, shall under no circumstances be
-interpreted as being a waiver by the interested Party of its right to
-invoke said provision(s) subsequently.
-
-11.3 The Agreement cancels and replaces any or all previous agreements,
-whether written or oral, between the Parties and having the same
-purpose, and constitutes the entirety of the agreement between said
-Parties concerning said purpose. No supplement or modification to the
-terms and conditions hereof shall be effective as between the Parties
-unless it is made in writing and signed by their duly authorized
-representatives.
-
-11.4 In the event that one or more of the provisions hereof were to
-conflict with a current or future applicable act or legislative text,
-said act or legislative text shall prevail, and the Parties shall make
-the necessary amendments so as to comply with said act or legislative
-text. All other provisions shall remain effective. Similarly, invalidity
-of a provision of the Agreement, for any reason whatsoever, shall not
-cause the Agreement as a whole to be invalid.
-
-
-      11.5 LANGUAGE
-
-The Agreement is drafted in both French and English and both versions
-are deemed authentic.
-
-
-    Article 12 - NEW VERSIONS OF THE AGREEMENT
-
-12.1 Any person is authorized to duplicate and distribute copies of this
-Agreement.
-
-12.2 So as to ensure coherence, the wording of this Agreement is
-protected and may only be modified by the authors of the License, who
-reserve the right to periodically publish updates or new versions of the
-Agreement, each with a separate number. These subsequent versions may
-address new issues encountered by Free Software.
-
-12.3 Any Software distributed under a given version of the Agreement may
-only be subsequently distributed under the same version of the Agreement
-or a subsequent version.
-
-
-    Article 13 - GOVERNING LAW AND JURISDICTION
-
-13.1 The Agreement is governed by French law. The Parties agree to
-endeavor to seek an amicable solution to any disagreements or disputes
-that may arise during the performance of the Agreement.
-
-13.2 Failing an amicable solution within two (2) months as from their
-occurrence, and unless emergency proceedings are necessary, the
-disagreements or disputes shall be referred to the Paris Courts having
-jurisdiction, by the more diligent Party.
-
-
-Version 1.0 dated 2006-09-05.
diff --git a/src/pprint/README b/src/pprint/README
deleted file mode 100644
index 7146250a..00000000
--- a/src/pprint/README
+++ /dev/null
@@ -1,13 +0,0 @@
-This is an adaptation of Daan Leijen's "PPrint" library, which itself is based
-on the ideas developed by Philip Wadler in "A Prettier Printer". For more
-information about Wadler's and Leijen's work, please consult the following
-references:
-
-   http://www.cs.uu.nl/~daan/pprint.html
-   http://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
-
-To install PPrint, type "make -C src install". ocamlfind is required.
-
-The documentation for PPrint is built by "make doc" and is found in the
-file doc/index.html.
-
diff --git a/src/pprint/src/META b/src/pprint/src/META
deleted file mode 100755
index 4a966166..00000000
--- a/src/pprint/src/META
+++ /dev/null
@@ -1,5 +0,0 @@
-requires = ""
-description = "The PPrint pretty-printing library"
-archive(byte) = "PPrintLib.cma"
-archive(native) = "PPrintLib.cmxa"
-version = "20171003"
diff --git a/src/pprint/src/Makefile b/src/pprint/src/Makefile
deleted file mode 100644
index 3bfa12df..00000000
--- a/src/pprint/src/Makefile
+++ /dev/null
@@ -1,46 +0,0 @@
-.PHONY: all install uninstall reinstall clean doc test bench
-
-OCAMLBUILD := ocamlbuild -use-ocamlfind -classic-display
-OCAMLFIND  := ocamlfind
-DOCDIR     := doc
-MAIN       := PPrintTest
-TO_BUILD   := PPrintLib.cma PPrintLib.cmxa
-
-all:
-	$(OCAMLBUILD) $(TO_BUILD)
-
-install: all
-	$(OCAMLFIND) install pprint META \
-		$(patsubst %,_build/%,$(TO_BUILD)) \
-		_build/PPrintLib.a _build/*.cmx _build/*.cmi
-
-# [make uninstall] attempts to uninstall, but succeeds even if uninstallation
-# fails (probably because the package was not installed in the first place).
-uninstall:
-	ocamlfind remove pprint || true
-
-reinstall: uninstall
-	@ $(MAKE) install
-
-clean:
-	rm -f *~
-	rm -rf doc
-	$(OCAMLBUILD) -clean
-
-doc: all
-	@rm -rf $(DOCDIR)
-	@mkdir $(DOCDIR)
-	ocamlfind ocamldoc \
-	  -html \
-	  -I _build \
-	  -d $(DOCDIR) \
-	  -charset utf8 \
-	  PPrintRenderer.ml PPrintEngine.mli PPrintCombinators.mli PPrintOCaml.mli PPrint.ml
-
-test: all
-	$(OCAMLBUILD) $(MAIN).native
-	./$(MAIN).native
-
-bench: all
-	$(OCAMLBUILD) -tag use_unix PPrintBench.native
-	time ./PPrintBench.native
diff --git a/src/pprint/src/PPrint.ml b/src/pprint/src/PPrint.ml
deleted file mode 100644
index 46d732b1..00000000
--- a/src/pprint/src/PPrint.ml
+++ /dev/null
@@ -1,18 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** A package of all of the above. *)
-
-include PPrintEngine
-include PPrintCombinators
-module OCaml = PPrintOCaml
diff --git a/src/pprint/src/PPrintCombinators.ml b/src/pprint/src/PPrintCombinators.ml
deleted file mode 100644
index 70499878..00000000
--- a/src/pprint/src/PPrintCombinators.ml
+++ /dev/null
@@ -1,311 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-open PPrintEngine
-
-(* ------------------------------------------------------------------------- *)
-
-(* Predefined single-character documents. *)
-
-let lparen          = char '('
-let rparen          = char ')'
-let langle          = char '<'
-let rangle          = char '>'
-let lbrace          = char '{'
-let rbrace          = char '}'
-let lbracket        = char '['
-let rbracket        = char ']'
-let squote          = char '\''
-let dquote          = char '"'
-let bquote          = char '`'
-let semi            = char ';'
-let colon           = char ':'
-let comma           = char ','
-let space           = char ' '
-let dot             = char '.'
-let sharp           = char '#'
-let slash           = char '/'
-let backslash       = char '\\'
-let equals          = char '='
-let qmark           = char '?'
-let tilde           = char '~'
-let at              = char '@'
-let percent         = char '%'
-let dollar          = char '$'
-let caret           = char '^'
-let ampersand       = char '&'
-let star            = char '*'
-let plus            = char '+'
-let minus           = char '-'
-let underscore      = char '_'
-let bang            = char '!'
-let bar             = char '|'
-
-(* ------------------------------------------------------------------------- *)
-
-(* Repetition. *)
-
-let twice doc =
-  doc ^^ doc
-
-let repeat n doc =
-  let rec loop n doc accu =
-    if n = 0 then
-      accu
-    else
-      loop (n - 1) doc (doc ^^ accu)
-  in
-  loop n doc empty
-
-(* ------------------------------------------------------------------------- *)
-
-(* Delimiters. *)
-
-let precede   l x   = l ^^ x
-let terminate r x   = x ^^ r
-let enclose l r x   = l ^^ x ^^ r
-
-let squotes         = enclose squote squote
-let dquotes         = enclose dquote dquote
-let bquotes         = enclose bquote bquote
-let braces          = enclose lbrace rbrace
-let parens          = enclose lparen rparen
-let angles          = enclose langle rangle
-let brackets        = enclose lbracket rbracket
-
-(* ------------------------------------------------------------------------- *)
-
-(* Some functions on lists. *)
-
-(* A variant of [fold_left] that keeps track of the element index. *)
-
-let foldli (f : int -> 'b -> 'a -> 'b) (accu : 'b) (xs : 'a list) : 'b =
-  let r = ref 0 in
-  List.fold_left (fun accu x ->
-    let i = !r in
-    r := i + 1;
-    f i accu x
-  ) accu xs
-
-(* ------------------------------------------------------------------------- *)
-
-(* Working with lists of documents. *)
-
-let concat docs =
-  (* We take advantage of the fact that [^^] operates in constant
-     time, regardless of the size of its arguments. The document
-     that is constructed is essentially a reversed list (i.e., a
-     tree that is biased towards the left). This is not a problem;
-     when pretty-printing this document, the engine will descend
-     along the left branch, pushing the nodes onto its stack as
-     it goes down, effectively reversing the list again. *)
-  List.fold_left (^^) empty docs
-
-let separate sep docs =
-  foldli (fun i accu doc ->
-    if i = 0 then
-      doc
-    else
-      accu ^^ sep ^^ doc
-  ) empty docs
-
-let concat_map f xs =
-  List.fold_left (fun accu x ->
-    accu ^^ f x
-  ) empty xs
-
-let separate_map sep f xs =
-  foldli (fun i accu x ->
-    if i = 0 then
-      f x
-    else
-      accu ^^ sep ^^ f x
-  ) empty xs
-
-let separate2 sep last_sep docs =
-  let n = List.length docs in
-  foldli (fun i accu doc ->
-    if i = 0 then
-      doc
-    else
-      accu ^^ (if i < n - 1 then sep else last_sep) ^^ doc
-  ) empty docs
-
-let optional f = function
-  | None ->
-      empty
-  | Some x ->
-      f x
-
-(* ------------------------------------------------------------------------- *)
-
-(* Text. *)
-
-(* This variant of [String.index_from] returns an option. *)
-
-let index_from s i c =
-  try
-    Some (String.index_from s i c)
-  with Not_found ->
-    None
-
-(* [lines s] chops the string [s] into a list of lines, which are turned
-   into documents. *)
-
-let lines s =
-  let rec chop accu i =
-    match index_from s i '\n' with
-    | Some j ->
-        let accu = substring s i (j - i) :: accu in
-	chop accu (j + 1)
-    | None ->
-        substring s i (String.length s - i) :: accu
-  in
-  List.rev (chop [] 0)
-
-let arbitrary_string s =
-  separate (break 1) (lines s)
-
-(* [split ok s] splits the string [s] at every occurrence of a character
-   that satisfies the predicate [ok]. The substrings thus obtained are
-   turned into documents, and a list of documents is returned. No information
-   is lost: the concatenation of the documents yields the original string.
-   This code is not UTF-8 aware. *)
-
-let split ok s =
-  let n = String.length s in
-  let rec index_from i =
-    if i = n then
-      None
-    else if ok s.[i] then
-      Some i
-    else
-      index_from (i + 1)
-  in
-  let rec chop accu i =
-    match index_from i with
-    | Some j ->
-        let accu = substring s i (j - i) :: accu in
-	let accu = char s.[j] :: accu in
-	chop accu (j + 1)
-    | None ->
-        substring s i (String.length s - i) :: accu
-  in
-  List.rev (chop [] 0)
-
-(* [words s] chops the string [s] into a list of words, which are turned
-   into documents. *)
-
-let words s =
-  let n = String.length s in
-  (* A two-state finite automaton. *)
-  (* In this state, we have skipped at least one blank character. *)
-  let rec skipping accu i = 
-    if i = n then
-      (* There was whitespace at the end. Drop it. *)
-      accu
-    else match s.[i] with
-    | ' '
-    | '\t'
-    | '\n'
-    | '\r' ->
-        (* Skip more whitespace. *)
-	skipping accu (i + 1)
-    | _ ->
-        (* Begin a new word. *)
-	word accu i (i + 1)
-  (* In this state, we have skipped at least one non-blank character. *)
-  and word accu i j =
-    if j = n then
-      (* Final word. *)
-      substring s i (j - i) :: accu
-    else match s.[j] with
-    | ' '
-    | '\t'
-    | '\n'
-    | '\r' ->
-        (* A new word has been identified. *)
-        let accu = substring s i (j - i) :: accu in	
-	skipping accu (j + 1)
-    | _ ->
-        (* Continue inside the current word. *)
-	word accu i (j + 1)
-  in
-  List.rev (skipping [] 0)
-
-let flow_map sep f docs =
-  foldli (fun i accu doc ->
-    if i = 0 then
-      f doc
-    else
-      accu ^^
-      (* This idiom allows beginning a new line if [doc] does not
-	 fit on the current line. *)
-      group (sep ^^ f doc)
-  ) empty docs  
-
-let flow sep docs =
-  flow_map sep (fun x -> x) docs
-
-let url s =
-  flow (break 0) (split (function '/' | '.' -> true | _ -> false) s)
-
-(* ------------------------------------------------------------------------- *)
-
-(* Alignment and indentation. *)
-
-let hang i d =
-  align (nest i d)
-
-let ( !^ ) = string
-
-let ( ^/^ ) x y =
-  x ^^ break 1 ^^ y
-
-let prefix n b x y =
-  group (x ^^ nest n (break b ^^ y))
-
-let (^//^) =
-  prefix 2 1
-
-let jump n b y =
-  group (nest n (break b ^^ y))
-
-(* Deprecated.
-let ( ^@^  ) x y = group (x ^/^ y)
-let ( ^@@^ ) x y = group (nest 2 (x ^/^ y))
-*)
-
-let infix n b op x y =
-  prefix n b (x ^^ blank b ^^ op) y
-
-let surround n b opening contents closing =
-  group (opening ^^ nest n (       break b  ^^ contents) ^^        break b ^^ closing )
-
-let soft_surround n b opening contents closing =
-  group (opening ^^ nest n (group (break b) ^^ contents) ^^ group (break b ^^ closing))
-
-let surround_separate n b void opening sep closing docs =
-  match docs with
-  | [] ->
-      void
-  | _ :: _ ->
-      surround n b opening (separate sep docs) closing
-
-let surround_separate_map n b void opening sep closing f xs =
-  match xs with
-  | [] ->
-      void
-  | _ :: _ ->
-      surround n b opening (separate_map sep f xs) closing
-
diff --git a/src/pprint/src/PPrintCombinators.mli b/src/pprint/src/PPrintCombinators.mli
deleted file mode 100644
index c538cb35..00000000
--- a/src/pprint/src/PPrintCombinators.mli
+++ /dev/null
@@ -1,236 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-open PPrintEngine
-
-(** A set of high-level combinators for building documents. *)
-
-(** {1 Single characters} *)
-
-(** The following constant documents consist of a single character. *)
-
-val lparen: document
-val rparen: document
-val langle: document
-val rangle: document
-val lbrace: document
-val rbrace: document
-val lbracket: document
-val rbracket: document
-val squote: document
-val dquote: document
-val bquote: document
-val semi: document
-val colon: document
-val comma: document
-val space: document
-val dot: document
-val sharp: document
-val slash: document
-val backslash: document
-val equals: document
-val qmark: document
-val tilde: document
-val at: document
-val percent: document
-val dollar: document
-val caret: document
-val ampersand: document
-val star: document
-val plus: document
-val minus: document
-val underscore: document
-val bang: document
-val bar: document
-
-(** {1 Delimiters} *)
-
-(** [precede l x] is [l ^^ x]. *)
-val precede: document -> document -> document
-
-(** [terminate r x] is [x ^^ r]. *)
-val terminate: document -> document -> document
-
-(** [enclose l r x] is [l ^^ x ^^ r]. *)
-val enclose: document -> document -> document -> document
-
-(** The following combinators enclose a document within a pair of delimiters.
-    They are partial applications of [enclose]. No whitespace or line break is
-    introduced. *)
-
-val squotes: document -> document
-val dquotes: document -> document
-val bquotes: document -> document
-val braces: document -> document
-val parens: document -> document
-val angles: document -> document
-val brackets: document -> document
-
-(** {1 Repetition} *)
-
-(** [twice doc] is the document obtained by concatenating two copies of
-    the document [doc]. *)
-val twice: document -> document
-
-(** [repeat n doc] is the document obtained by concatenating [n] copies of
-    the document [doc]. *)
-val repeat: int -> document -> document
-
-(** {1 Lists and options} *)
-
-(** [concat docs] is the concatenation of the documents in the list [docs]. *)
-val concat: document list -> document
-
-(** [separate sep docs] is the concatenation of the documents in the list
-    [docs]. The separator [sep] is inserted between every two adjacent
-    documents. *)
-val separate: document -> document list -> document
-
-(** [concat_map f xs] is equivalent to [concat (List.map f xs)]. *)
-val concat_map: ('a -> document) -> 'a list -> document
-
-(** [separate_map sep f xs] is equivalent to [separate sep (List.map f xs)]. *)
-val separate_map: document -> ('a -> document) -> 'a list -> document
-
-(** [separate2 sep last_sep docs] is the concatenation of the documents in the
-    list [docs]. The separator [sep] is inserted between every two adjacent
-    documents, except between the last two documents, where the separator
-    [last_sep] is used instead. *)
-val separate2: document -> document -> document list -> document
-
-(** [optional f None] is the empty document. [optional f (Some x)] is
-    the document [f x]. *)
-val optional: ('a -> document) -> 'a option -> document
-
-(** {1 Text} *)
-
-(** [lines s] is the list of documents obtained by splitting [s] at newline
-    characters, and turning each line into a document via [substring]. This
-    code is not UTF-8 aware. *)
-val lines: string -> document list
-
-(** [arbitrary_string s] is equivalent to [separate (break 1) (lines s)].
-    It is analogous to [string s], but is valid even if the string [s]
-    contains newline characters. *)
-val arbitrary_string: string -> document
-
-(** [words s] is the list of documents obtained by splitting [s] at whitespace
-    characters, and turning each word into a document via [substring]. All
-    whitespace is discarded. This code is not UTF-8 aware. *)
-val words: string -> document list
-
-(** [split ok s] splits the string [s] before and after every occurrence of a
-    character that satisfies the predicate [ok]. The substrings thus obtained
-    are turned into documents, and a list of documents is returned. No
-    information is lost: the concatenation of the documents yields the
-    original string. This code is not UTF-8 aware. *)
-val split: (char -> bool) -> string -> document list
-
-(** [flow sep docs] separates the documents in the list [docs] with the
-    separator [sep] and arranges for a new line to begin whenever a document
-    does not fit on the current line. This is useful for typesetting
-    free-flowing, ragged-right text. A typical choice of [sep] is [break b],
-    where [b] is the number of spaces that must be inserted between two
-    consecutive words (when displayed on the same line). *)
-val flow: document -> document list -> document
-
-(** [flow_map sep f docs] is equivalent to [flow sep (List.map f docs)]. *)
-val flow_map: document -> ('a -> document) -> 'a list -> document
-
-(** [url s] is a possible way of displaying the URL [s]. A potential line
-    break is inserted immediately before and immediately after every slash
-    and dot character. *)
-val url: string -> document
-
-(** {1 Alignment and indentation} *)
-
-(* [hang n doc] is analogous to [align], but additionally indents
-   all lines, except the first one, by [n]. Thus, the text in the
-   box forms a hanging indent. *)
-val hang: int -> document -> document
-
-(** [prefix n b left right] has the following flat layout: {[
-left right
-]}
-and the following non-flat layout:
-{[
-left
-  right
-]}
-The parameter [n] controls the nesting of [right] (when not flat).
-The parameter [b] controls the number of spaces between [left] and [right]
-(when flat).
- *)
-val prefix: int -> int -> document -> document -> document
-
-(** [jump n b right] is equivalent to [prefix n b empty right]. *)
-val jump: int -> int -> document -> document
-
-(** [infix n b middle left right] has the following flat layout: {[
-left middle right
-]}
-and the following non-flat layout: {[
-left middle
-  right
-]}
-The parameter [n] controls the nesting of [right] (when not flat).
-The parameter [b] controls the number of spaces between [left] and [middle]
-(always) and between [middle] and [right] (when flat).
-*)
-val infix: int -> int -> document -> document -> document -> document
-
-(** [surround n b opening contents closing] has the following flat layout: {[
-opening contents closing
-]}
-and the following non-flat layout: {[
-opening
-  contents
-closing
-]}
-The parameter [n] controls the nesting of [contents] (when not flat).
-The parameter [b] controls the number of spaces between [opening] and [contents]
-and between [contents] and [closing] (when flat).
-*)
-val surround: int -> int -> document -> document -> document -> document
-
-(** [soft_surround] is analogous to [surround], but involves more than one
-    group, so it offers possibilities other than the completely flat layout
-    (where [opening], [contents], and [closing] appear on a single line) and
-    the completely developed layout (where [opening], [contents], and
-    [closing] appear on separate lines). It tries to place the beginning of
-    [contents] on the same line as [opening], and to place [closing] on the
-    same line as the end of [contents], if possible.
-*)
-val soft_surround: int -> int -> document -> document -> document -> document
-
-(** [surround_separate n b void opening sep closing docs] is equivalent to
-    [surround n b opening (separate sep docs) closing], except when the
-    list [docs] is empty, in which case it reduces to [void]. *)
-val surround_separate: int -> int -> document -> document -> document -> document -> document list -> document
-
-(** [surround_separate_map n b void opening sep closing f xs] is equivalent to
-    [surround_separate n b void opening sep closing (List.map f xs)]. *)
-val surround_separate_map: int -> int -> document -> document -> document -> document -> ('a -> document) -> 'a list -> document
-
-(** {1 Short-hands} *)
-
-(** [!^s] is a short-hand for [string s]. *)
-val ( !^ ) : string -> document
-
-(** [x ^/^ y] separates [x] and [y] with a breakable space.
-    It is a short-hand for [x ^^ break 1 ^^ y]. *)
-val ( ^/^ ) : document -> document -> document
-
-(** [x ^//^ y] is a short-hand for [prefix 2 1 x y]. *)
-val ( ^//^ ) : document -> document -> document
-
diff --git a/src/pprint/src/PPrintEngine.ml b/src/pprint/src/PPrintEngine.ml
deleted file mode 100644
index 2a78363d..00000000
--- a/src/pprint/src/PPrintEngine.ml
+++ /dev/null
@@ -1,642 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ------------------------------------------------------------------------- *)
-
-(* A type of integers with infinity. *)
-
-type requirement =
-    int (* with infinity *)
-
-(* Infinity is encoded as [max_int]. *)
-
-let infinity : requirement =
-  max_int
-
-(* Addition of integers with infinity. *)
-
-let (++) (x : requirement) (y : requirement) : requirement =
-  if x = infinity || y = infinity then
-    infinity
-  else
-    x + y
-
-(* Comparison between an integer with infinity and a normal integer. *)
-
-let (<==) (x : requirement) (y : int) =
-  x <= y
-
-(* ------------------------------------------------------------------------- *)
-
-(* A uniform interface for output channels. *)
-
-class type output = object
-
-  (** [char c] sends the character [c] to the output channel. *)
-  method char: char -> unit
-
-  (** [substring s ofs len] sends the substring of [s] delimited by the
-      offset [ofs] and the length [len] to the output channel. *)
-  method substring: string -> int (* offset *) -> int (* length *) -> unit
-
-end
-
-(* Three kinds of output channels are wrapped so as to satisfy the above
-   interface: OCaml output channels, OCaml memory buffers, and OCaml
-   formatters. *)
-
-class channel_output channel = object
-  method char = output_char channel
-  method substring = output_substring channel
-    (* We used to use [output], but, as of OCaml 4.02 and with -safe-string
-       enabled, the type of [output] has changed: this function now expects
-       an argument of type [bytes]. The new function [output_substring] must
-       be used instead. Furthermore, as of OCaml 4.06, -safe-string is enabled
-       by default. In summary, we require OCaml 4.02, use [output_substring],
-       and enable -safe-string. *)
-end
-
-class buffer_output buffer = object
-  method char = Buffer.add_char buffer
-  method substring = Buffer.add_substring buffer
-end
-
-class formatter_output fmt = object
-  method char = Format.pp_print_char fmt
-  method substring = fst (Format.pp_get_formatter_output_functions fmt ())
-end
-
-(* ------------------------------------------------------------------------- *)
-
-(** The rendering engine maintains the following internal state. Its structure
-    is subject to change in future versions of the library. Nevertheless, it is
-    exposed to the user who wishes to define custom documents. *)
-
-type state = {
-
-    width: int;
-    (** The line width. This parameter is fixed throughout the execution of
-        the renderer. *)
-
-    ribbon: int;
-    (** The ribbon width. This parameter is fixed throughout the execution of
-        the renderer. *)
-
-    mutable last_indent: int;
-    (** The number of blanks that were printed at the beginning of the current
-        line. This field is updated (only) by the function [emit_hardline]. It
-        is used (only) to determine whether the ribbon width constraint is
-        respected. *)
-
-    mutable column: int;
-    (** The current column. This field must be updated whenever something is
-        sent to the output channel. It is used (only) to determine whether the
-        width constraint is respected. *)
-
-  }
-
-(* ------------------------------------------------------------------------- *)
-
-(* [initial rfrac width] creates a fresh initial state. *)
-
-let initial rfrac width = {
-  width = width;
-  ribbon = max 0 (min width (truncate (float_of_int width *. rfrac)));
-  last_indent = 0;
-  column = 0
-}
-
-(* ------------------------------------------------------------------------- *)
-
-(** A custom document is defined by implementing the following methods. *)
-
-class type custom = object
-
-  (** A custom document must publish the width (i.e., the number of columns)
-      that it would like to occupy if it is printed on a single line (that is,
-      in flattening mode). The special value [infinity] means that this
-      document cannot be printed on a single line; this value causes any
-      groups that contain this document to be dissolved. This method should
-      in principle work in constant time. *)
-  method requirement: requirement
-
-  (** The method [pretty] is used by the main rendering algorithm. It has
-      access to the output channel and to the algorithm's internal state, as
-      described above. In addition, it receives the current indentation level
-      and the current flattening mode (on or off). If flattening mode is on,
-      then the document must be printed on a single line, in a manner that is
-      consistent with the requirement that was published ahead of time. If
-      flattening mode is off, then there is no such obligation. The state must
-      be updated in a manner that is consistent with what is sent to the
-      output channel. *)
-  method pretty: output -> state -> int -> bool -> unit
-
-  (** The method [compact] is used by the compact rendering algorithm. It has
-      access to the output channel only. *)
-  method compact: output -> unit
-
-end
-
-(* ------------------------------------------------------------------------- *)
-
-(* Here is the algebraic data type of documents. It is analogous to Daan
-   Leijen's version, but the binary constructor [Union] is replaced with
-   the unary constructor [Group], and the constant [Line] is replaced with
-   more general constructions, namely [IfFlat], which provides alternative
-   forms depending on the current flattening mode, and [HardLine], which
-   represents a newline character, and causes a failure in flattening mode. *)
-
-type document =
-
-  (* [Empty] is the empty document. *)
-
-  | Empty
-
-  (* [Char c] is a document that consists of the single character [c]. We
-     enforce the invariant that [c] is not a newline character. *)
-
-  | Char of char
-
-  (* [String s] is a document that consists of just the string [s]. We
-     assume, but do not check, that this string does not contain a newline
-     character. [String] is a special case of [FancyString], which takes up
-     less space in memory. *)
-
-  | String of string
-
-  (* [FancyString (s, ofs, len, apparent_length)] is a (portion of a) string
-     that may contain fancy characters: color escape characters, UTF-8 or
-     multi-byte characters, etc. Thus, the apparent length (which corresponds
-     to what will be visible on screen) differs from the length (which is a
-     number of bytes, and is reported by [String.length]). We assume, but do
-     not check, that fancystrings do not contain a newline character. *)
-
-  | FancyString of string * int * int * int
-
-  (* [Blank n] is a document that consists of [n] blank characters. *)
-
-  | Blank of int
-
-    (* When in flattening mode, [IfFlat (d1, d2)] turns into the document
-       [d1]. When not in flattening mode, it turns into the document [d2]. *)
-
-  | IfFlat of document * document
-
-  (* When in flattening mode, [HardLine] causes a failure, which requires
-     backtracking all the way until the stack is empty. When not in flattening
-     mode, it represents a newline character, followed with an appropriate
-     number of indentation. A common way of using [HardLine] is to only use it
-     directly within the right branch of an [IfFlat] construct. *)
-
-  | HardLine
-
-  (* The following constructors store their space requirement. This is the
-     document's apparent length, if printed in flattening mode. This
-     information is computed in a bottom-up manner when the document is
-     constructed. *)
-
-  (* In other words, the space requirement is the number of columns that the
-     document needs in order to fit on a single line. We express this value in
-     the set of `integers extended with infinity', and use the value
-     [infinity] to indicate that the document cannot be printed on a single
-     line. *)
-
-  (* Storing this information at [Group] nodes is crucial, as it allows us to
-     avoid backtracking and buffering. *)
-
-  (* Storing this information at other nodes allows the function [requirement]
-     to operate in constant time. This means that the bottom-up computation of
-     requirements takes linear time. *)
-
-  (* [Cat (req, doc1, doc2)] is the concatenation of the documents [doc1] and
-     [doc2]. The space requirement [req] is the sum of the requirements of
-     [doc1] and [doc2]. *)
-
-  | Cat of requirement * document * document
-
-  (* [Nest (req, j, doc)] is the document [doc], in which the indentation
-     level has been increased by [j], that is, in which [j] blanks have been
-     inserted after every newline character. The space requirement [req] is
-     the same as the requirement of [doc]. *)
-
-  | Nest of requirement * int * document
-
-  (* [Group (req, doc)] represents an alternative: it is either a flattened
-     form of [doc], in which occurrences of [Group] disappear and occurrences
-     of [IfFlat] resolve to their left branch, or [doc] itself. The space
-     requirement [req] is the same as the requirement of [doc]. *)
-
-  | Group of requirement * document
-
-  (* [Align (req, doc)] increases the indentation level to reach the current
-     column.  Thus, the document [doc] is rendered within a box whose upper
-     left corner is the current position. The space requirement [req] is the
-     same as the requirement of [doc]. *)
-
-  | Align of requirement * document
-
-  (* [Custom (req, f)] is a document whose appearance is user-defined. *)
-
-  | Custom of custom
-
-(* ------------------------------------------------------------------------- *)
-
-(* Retrieving or computing the space requirement of a document. *)
-
-let rec requirement = function
-  | Empty ->
-      0
-  | Char _ ->
-      1
-  | String s ->
-      String.length s
-  | FancyString (_, _, _, len)
-  | Blank len ->
-      len
-  | IfFlat (doc1, _) ->
-      (* In flattening mode, the requirement of [ifflat x y] is just the
-         requirement of its flat version, [x]. *)
-      (* The smart constructor [ifflat] ensures that [IfFlat] is never nested
-         in the left-hand side of [IfFlat], so this recursive call is not a
-         problem; the function [requirement] has constant time complexity. *)
-      requirement doc1
-  | HardLine ->
-      (* A hard line cannot be printed in flattening mode. *)
-      infinity
-  | Cat (req, _, _)
-  | Nest (req, _, _)
-  | Group (req, _)
-  | Align (req, _) ->
-      (* These nodes store their requirement -- which is computed when the
-         node is constructed -- so as to allow us to answer in constant time
-         here. *)
-      req
-  | Custom c ->
-      c#requirement
-
-(* ------------------------------------------------------------------------- *)
-
-(* The above algebraic data type is not exposed to the user. Instead, we
-   expose the following functions. These functions construct a raw document
-   and compute its requirement, so as to obtain a document. *)
-
-let empty =
-  Empty
-
-let char c =
-  assert (c <> '\n');
-  Char c
-
-let space =
-  char ' '
-
-let string s =
-  String s
-
-let fancysubstring s ofs len apparent_length =
-  if len = 0 then
-    empty
-  else
-    FancyString (s, ofs, len, apparent_length)
-
-let substring s ofs len =
-  fancysubstring s ofs len len
-
-let fancystring s apparent_length =
-  fancysubstring s 0 (String.length s) apparent_length
-
-(* The following function was stolen from [Batteries]. *)
-let utf8_length s =
-  let rec length_aux s c i =
-    if i >= String.length s then c else
-    let n = Char.code (String.unsafe_get s i) in
-    let k =
-      if n < 0x80 then 1 else
-      if n < 0xe0 then 2 else
-      if n < 0xf0 then 3 else 4
-    in
-    length_aux s (c + 1) (i + k)
-  in
-  length_aux s 0 0
-
-let utf8string s =
-  fancystring s (utf8_length s)
-
-let hardline =
-  HardLine
-
-let blank n =
-  match n with
-  | 0 ->
-      empty
-  | 1 ->
-      space
-  | _ ->
-      Blank n
-
-let ifflat doc1 doc2 =
-  (* Avoid nesting [IfFlat] in the left-hand side of [IfFlat], as this
-     is redundant. *)
-  match doc1 with
-  | IfFlat (doc1, _)
-  | doc1 ->
-      IfFlat (doc1, doc2)
-
-let internal_break i =
-  ifflat (blank i) hardline
-
-let break0 =
-  internal_break 0
-
-let break1 =
-  internal_break 1
-
-let break i =
-  match i with
-  | 0 ->
-      break0
-  | 1 ->
-      break1
-  | _ ->
-      internal_break i
-
-let (^^) x y =
-  match x, y with
-  | Empty, _ ->
-      y
-  | _, Empty ->
-      x
-  | _, _ ->
-      Cat (requirement x ++ requirement y, x, y)
-
-let nest i x =
-  assert (i >= 0);
-  Nest (requirement x, i, x)
-
-let group x =
-  let req = requirement x in
-  (* Minor optimisation: an infinite requirement dissolves a group. *)
-  if req = infinity then
-    x
-  else
-    Group (req, x)
-
-let align x =
-  Align (requirement x, x)
-
-let custom c =
-  (* Sanity check. *)
-  assert (c#requirement >= 0);
-  Custom c
-
-(* ------------------------------------------------------------------------- *)
-
-(* Printing blank space (indentation characters). *)
-
-let blank_length =
-  80
-
-let blank_buffer =
-  String.make blank_length ' '
-
-let rec blanks output n =
-  if n <= 0 then
-    ()
-  else if n <= blank_length then
-    output#substring blank_buffer 0 n
-  else begin
-    output#substring blank_buffer 0 blank_length;
-    blanks output (n - blank_length)
-  end
-
-(* ------------------------------------------------------------------------- *)
-
-(* This function expresses the following invariant: if we are in flattening
-   mode, then we must be within bounds, i.e. the width and ribbon width
-   constraints must be respected. *)
-
-let ok state flatten : bool =
-  not flatten ||
-  state.column <= state.width && state.column <= state.last_indent + state.ribbon
-
-(* ------------------------------------------------------------------------- *)
-
-(* The pretty rendering engine. *)
-
-(* The renderer is supposed to behave exactly like Daan Leijen's, although its
-   implementation is quite radically different, and simpler. Our documents are
-   constructed eagerly, as opposed to lazily. This means that we pay a large
-   space overhead, but in return, we get the ability of computing information
-   bottom-up, as described above, which allows to render documents without
-   backtracking or buffering. *)
-
-(* The [state] record is never copied; it is just threaded through. In
-   addition to it, the parameters [indent] and [flatten] influence the
-   manner in which the document is rendered. *)
-
-(* The code is written in tail-recursive style, so as to avoid running out of
-   stack space if the document is very deep. Its explicit continuation can be
-   viewed as a sequence of pending calls to [pretty]. *)
-
-type cont =
-  | KNil
-  | KCons of int * bool * document * cont
-
-let rec pretty
-  (output : output)
-  (state : state)
-  (indent : int)
-  (flatten : bool)
-  (doc : document)
-  (cont : cont)
-: unit =
-  match doc with
-
-  | Empty ->
-      continue output state cont
-
-  | Char c ->
-      output#char c;
-      state.column <- state.column + 1;
-      (* assert (ok state flatten); *)
-      continue output state cont
-
-  | String s ->
-      let len = String.length s in
-      output#substring s 0 len;
-      state.column <- state.column + len;
-      (* assert (ok state flatten); *)
-      continue output state cont
-
-  | FancyString (s, ofs, len, apparent_length) ->
-      output#substring s ofs len;
-      state.column <- state.column + apparent_length;
-      (* assert (ok state flatten); *)
-      continue output state cont
-
-  | Blank n ->
-      blanks output n;
-      state.column <- state.column + n;
-      (* assert (ok state flatten); *)
-      continue output state cont
-
-  | HardLine ->
-      (* We cannot be in flattening mode, because a hard line has an [infinity]
-         requirement, and we attempt to render a group in flattening mode only
-         if this group's requirement is met. *)
-      assert (not flatten);
-      (* Emit a hardline. *)
-      output#char '\n';
-      blanks output indent;
-      state.column <- indent;
-      state.last_indent <- indent;
-      (* Continue. *)
-      continue output state cont
-
-  | IfFlat (doc1, doc2) ->
-      (* Pick an appropriate sub-document, based on the current flattening
-         mode. *)
-      pretty output state indent flatten (if flatten then doc1 else doc2) cont
-
-  | Cat (_, doc1, doc2) ->
-      (* Push the second document onto the continuation. *)
-      pretty output state indent flatten doc1 (KCons (indent, flatten, doc2, cont))
-
-  | Nest (_, j, doc) ->
-      pretty output state (indent + j) flatten doc cont
-
-  | Group (req, doc) ->
-      (* If we already are in flattening mode, stay in flattening mode; we
-         are committed to it. If we are not already in flattening mode, we
-         have a choice of entering flattening mode. We enter this mode only
-         if we know that this group fits on this line without violating the
-         width or ribbon width constraints. Thus, we never backtrack. *)
-      let flatten =
-        flatten ||
-        let column = state.column ++ req in
-        column <== state.width && column <== state.last_indent + state.ribbon
-      in
-      pretty output state indent flatten doc cont
-
-  | Align (_, doc) ->
-      (* The effect of this combinator is to set [indent] to [state.column].
-         Usually [indent] is equal to [state.last_indent], hence setting it
-         to [state.column] increases it. However, if [nest] has been used
-         since the current line began, then this could cause [indent] to
-         decrease. *)
-      (* assert (state.column > state.last_indent); *)
-      pretty output state state.column flatten doc cont
-
-  | Custom c ->
-      (* Invoke the document's custom rendering function. *)
-      c#pretty output state indent flatten;
-      (* Sanity check. *)
-      assert (ok state flatten);
-      (* Continue. *)
-      continue output state cont
-
-and continue output state = function
-  | KNil ->
-      ()
-  | KCons (indent, flatten, doc, cont) ->
-      pretty output state indent flatten doc cont
-
-(* Publish a version of [pretty] that does not take an explicit continuation.
-   This function may be used by authors of custom documents. We do not expose
-   the internal [pretty] -- the one that takes a continuation -- because we
-   wish to simplify the user's life. The price to pay is that calls that go
-   through a custom document cannot be tail calls. *)
-
-let pretty output state indent flatten doc =
-  pretty output state indent flatten doc KNil
-
-(* ------------------------------------------------------------------------- *)
-
-(* The compact rendering algorithm. *)
-
-let rec compact output doc cont =
-  match doc with
-  | Empty ->
-      continue output cont
-  | Char c ->
-      output#char c;
-      continue output cont
-  | String s ->
-      let len = String.length s in
-      output#substring s 0 len;
-      continue output cont
-  | FancyString (s, ofs, len, apparent_length) ->
-      output#substring s ofs len;
-      continue output cont
-  | Blank n ->
-      blanks output n;
-      continue output cont
-  | HardLine ->
-      output#char '\n';
-      continue output cont
-  | Cat (_, doc1, doc2) ->
-      compact output doc1 (doc2 :: cont)
-  | IfFlat (doc, _)
-  | Nest (_, _, doc)
-  | Group (_, doc)
-  | Align (_, doc) ->
-      compact output doc cont
-  | Custom c ->
-      (* Invoke the document's custom rendering function. *)
-      c#compact output;
-      continue output cont
-
-and continue output cont =
-  match cont with
-  | [] ->
-      ()
-  | doc :: cont ->
-      compact output doc cont
-
-let compact output doc =
-  compact output doc []
-
-(* ------------------------------------------------------------------------- *)
-
-(* We now instantiate the renderers for the three kinds of output channels. *)
-
-(* This is just boilerplate. *)
-
-module MakeRenderer (X : sig
-  type channel
-  val output: channel -> output
-end) = struct
-  type channel = X.channel
-  type dummy = document
-  type document = dummy
-  let pretty rfrac width channel doc = pretty (X.output channel) (initial rfrac width) 0 false doc
-  let compact channel doc = compact (X.output channel) doc
-end
-
-module ToChannel =
-  MakeRenderer(struct
-    type channel = out_channel
-    let output = new channel_output
-  end)
-
-module ToBuffer =
-  MakeRenderer(struct
-    type channel = Buffer.t
-    let output = new buffer_output
-  end)
-
-module ToFormatter =
-  MakeRenderer(struct
-    type channel = Format.formatter
-    let output = new formatter_output
-  end)
diff --git a/src/pprint/src/PPrintEngine.mli b/src/pprint/src/PPrintEngine.mli
deleted file mode 100644
index eda61a6c..00000000
--- a/src/pprint/src/PPrintEngine.mli
+++ /dev/null
@@ -1,226 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** A pretty-printing engine and a set of basic document combinators. *)
-
-(** {1 Building documents} *)
-
-(** Documents must be built in memory before they are rendered. This may seem
-    costly, but it is a simple approach, and works well. *)
-
-(** The following operations form a set of basic (low-level) combinators for
-    building documents. On top of these combinators, higher-level combinators
-    can be defined: see {!PPrintCombinators}. *)
-
-(** This is the abstract type of documents. *)
-type document
-
-(** The following basic (low-level) combinators allow constructing documents. *)
-
-(** [empty] is the empty document. *)
-val empty: document
-
-(** [char c] is a document that consists of the single character [c]. This
-    character must not be a newline. *)
-val char: char -> document
-
-(** [string s] is a document that consists of the string [s]. This string must
-    not contain a newline. *)
-val string: string -> document
-
-(** [substring s ofs len] is a document that consists of the portion of the
-    string [s] delimited by the offset [ofs] and the length [len]. This
-    portion must not contain a newline. *)
-val substring: string -> int -> int -> document
-
-(** [fancystring s apparent_length] is a document that consists of the string
-    [s]. This string must not contain a newline. The string may contain fancy
-    characters: color escape characters, UTF-8 or multi-byte characters,
-    etc. Thus, its apparent length (which measures how many columns the text
-    will take up on screen) differs from its length in bytes. *)
-val fancystring: string -> int -> document
-
-(** [fancysubstring s ofs len apparent_length] is a document that consists of
-    the portion of the string [s] delimited by the offset [ofs] and the length
-    [len]. This portion must contain a newline. The string may contain fancy
-    characters. *)
-val fancysubstring : string -> int -> int -> int -> document
-
-(** [utf8string s] is a document that consists of the UTF-8-encoded string [s].
-    This string must not contain a newline. *)
-val utf8string: string -> document
-
-(** [hardline] is a forced newline document. This document forces all enclosing
-    groups to be printed in non-flattening mode. In other words, any enclosing
-    groups are dissolved. *)
-val hardline: document
-
-(** [blank n] is a document that consists of [n] blank characters. *)
-val blank: int -> document
-
-(** [break n] is a document which consists of either [n] blank characters,
-    when forced to display on a single line, or a single newline character,
-    otherwise. Note that there is no choice at this point: choices are encoded
-    by the [group] combinator. *)
-val break: int -> document
-
-(** [doc1 ^^ doc2] is the concatenation of the documents [doc1] and [doc2]. *)
-val (^^): document -> document -> document
-
-(** [nest j doc] is the document [doc], in which the indentation level has
-    been increased by [j], that is, in which [j] blanks have been inserted
-    after every newline character. Read this again: indentation is inserted
-    after every newline character. No indentation is inserted at the beginning
-    of the document. *)
-val nest: int -> document -> document
-
-(** [group doc] encodes a choice. If possible, then the entire document [group
-    doc] is rendered on a single line. Otherwise, the group is dissolved, and
-    [doc] is rendered. There might be further groups within [doc], whose
-    presence will lead to further choices being explored. *)
-val group: document -> document
-
-(** [ifflat doc1 doc2] is rendered as [doc1] if part of a group that can be
-    successfully flattened, and is rendered as [doc2] otherwise. Use this
-    operation with caution. Because the pretty-printer is free to choose
-    between [doc1] and [doc2], these documents should be semantically
-    equivalent. *)
-val ifflat: document -> document -> document
-
-(** [align doc] is the document [doc], in which the indentation level has been
-    set to the current column. Thus, [doc] is rendered within a box whose
-    upper left corner is the current position. *)
-val align: document -> document
-
-(** {1 Rendering documents} *)
-
-(** This renderer sends its output into an output channel. *)
-module ToChannel : PPrintRenderer.RENDERER
-  with type channel = out_channel
-   and type document = document
-
-(** This renderer sends its output into a memory buffer. *)
-module ToBuffer : PPrintRenderer.RENDERER
-  with type channel = Buffer.t
-   and type document = document
-
-(** This renderer sends its output into a formatter channel. *)
-module ToFormatter : PPrintRenderer.RENDERER
-  with type channel = Format.formatter
-   and type document = document
-
-(** {1 Defining custom documents} *)
-
-(** A width requirement is expressed as an integer, where the value [max_int]
-    is reserved and represents infinity. *)
-
-type requirement = int
-val infinity : requirement
-
-(** An output channel is represented abstractly as an object equipped with
-    methods for displaying one character and for displaying a substring. *)
-
-class type output = object
-
-  (** [char c] sends the character [c] to the output channel. *)
-  method char: char -> unit
-
-  (** [substring s ofs len] sends the substring of [s] delimited by the
-      offset [ofs] and the length [len] to the output channel. *)
-  method substring: string -> int (* offset *) -> int (* length *) -> unit
-
-end
-
-(** The rendering engine maintains the following internal state. Its structure
-    is subject to change in future versions of the library. Nevertheless, it is
-    exposed to the user who wishes to define custom documents. *)
-
-type state = {
-
-    width: int;
-    (** The line width. This parameter is fixed throughout the execution of
-        the renderer. *)
-
-    ribbon: int;
-    (** The ribbon width. This parameter is fixed throughout the execution of
-        the renderer. *)
-
-    mutable last_indent: int;
-    (** The number of blanks that were printed at the beginning of the current
-        line. This field is updated (only) by the function [emit_hardline]. It
-        is used (only) to determine whether the ribbon width constraint is
-        respected. *)
-
-    mutable column: int;
-    (** The current column. This field must be updated whenever something is
-        sent to the output channel. It is used (only) to determine whether the
-        width constraint is respected. *)
-
-  }
-
-(** A custom document is defined by implementing the following methods. *)
-
-class type custom = object
-
-  (** A custom document must publish the width (i.e., the number of columns)
-      that it would like to occupy if it is printed on a single line (that is,
-      in flattening mode). The special value [infinity] means that this
-      document cannot be printed on a single line; this value causes any
-      groups that contain this document to be dissolved. This method should
-      in principle work in constant time. *)
-  method requirement: requirement
-
-  (** The method [pretty] is used by the main rendering algorithm. It has
-      access to the output channel and to the algorithm's internal state, as
-      described above. In addition, it receives the current indentation level
-      and the current flattening mode (on or off). If flattening mode is on,
-      then the document must be printed on a single line, in a manner that is
-      consistent with the requirement that was published ahead of time. If
-      flattening mode is off, then there is no such obligation. The state must
-      be updated in a manner that is consistent with what is sent to the
-      output channel. *)
-  method pretty: output -> state -> int -> bool -> unit
-
-  (** The method [compact] is used by the compact rendering algorithm. It has
-      access to the output channel only. *)
-  method compact: output -> unit
-
-end
-
-(** The function [custom] constructs a custom document. In other words, it
-    converts an object of type [custom] to a document. *)
-val custom: custom -> document
-
-(** The key functions of the library are exposed, in the hope that they may be
-    useful to authors of custom (leaf and non-leaf) documents. In the case of
-    a leaf document, they can help perform certain basic functions; for
-    instance, applying the function [pretty] to the document [hardline] is a
-    simple way of printing a hardline, while respecting the indentation
-    parameters and updating the state in a correct manner. Similarly, applying
-    [pretty] to the document [blank n] is a simple way of printing [n] spaces.
-    In the case of a non-leaf document (i.e., one which contains
-    sub-documents), these functions are essential: they allow computing the
-    width requirement of a sub-document and displaying a sub-document. *)
-
-(** [requirement doc] computes the width requirement of the document [doc].
-    It works in constant time. *)
-val requirement: document -> requirement
-
-(** [pretty output state indent flatten doc] prints the document [doc]. See
-    the documentation of the method [pretty]. *)
-val pretty: output -> state -> int -> bool -> document -> unit
-
-(** [compact output doc] prints the document [doc]. See the documentation of
-    the method [compact]. *)
-val compact: output -> document -> unit
-
diff --git a/src/pprint/src/PPrintLib.mllib b/src/pprint/src/PPrintLib.mllib
deleted file mode 100644
index e5de6978..00000000
--- a/src/pprint/src/PPrintLib.mllib
+++ /dev/null
@@ -1,5 +0,0 @@
-PPrint
-PPrintCombinators
-PPrintEngine
-PPrintOCaml
-PPrintRenderer
diff --git a/src/pprint/src/PPrintOCaml.ml b/src/pprint/src/PPrintOCaml.ml
deleted file mode 100644
index bee5f2a3..00000000
--- a/src/pprint/src/PPrintOCaml.ml
+++ /dev/null
@@ -1,158 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Printf
-open PPrintEngine
-open PPrintCombinators
-
-type constructor = string
-type type_name = string
-type record_field = string
-type tag = int
-
-(* ------------------------------------------------------------------------- *)
-
-(* This internal [sprintf]-like function produces a document. We use [string],
-   as opposed to [arbitrary_string], because the strings that we produce will
-   never contain a newline character. *)
-
-let dsprintf format = 
-  ksprintf string format
-
-(* ------------------------------------------------------------------------- *)
-
-(* Nicolas prefers using this code as opposed to just [sprintf "%g"] or
-   [sprintf "%f"]. The latter print [inf] and [-inf], whereas OCaml
-   understands [infinity] and [neg_infinity]. [sprintf "%g"] does not add a
-   trailing dot when the number happens to be an integral number.  [sprintf
-   "%F"] seems to lose precision and ignores the precision modifier. *)
-
-let valid_float_lexeme (s : string) : string =
-  let l = String.length s in
-  let rec loop i =
-    if i >= l then
-      (* If we reach the end of the string and have found only characters in
-	 the set '0' .. '9' and '-', then this string will be considered as an
-	 integer literal by OCaml. Adding a trailing dot makes it a float
-	 literal. *)
-      s ^ "."
-    else
-      match s.[i] with
-      | '0' .. '9' | '-' -> loop (i + 1)
-      | _ -> s
-  in loop 0
-
-(* This function constructs a string representation of a floating point
-   number. This representation is supposed to be accepted by OCaml as a
-   valid floating point literal. *)
-
-let float_representation (f : float) : string =
-  match classify_float f with
-  | FP_nan ->
-    "nan"
-  | FP_infinite ->
-      if f < 0.0 then "neg_infinity" else "infinity"
-  | _ ->
-      (* Try increasing precisions and validate. *)
-      let s = sprintf "%.12g" f in
-      if f = float_of_string s then valid_float_lexeme s else
-      let s = sprintf "%.15g" f in
-      if f = float_of_string s then valid_float_lexeme s else
-      sprintf "%.18g" f
-
-(* ------------------------------------------------------------------------- *)
-
-(* A few constants and combinators, used below. *)
-
-let some =
-  string "Some"
-
-let none =
-  string "None"
-
-let lbracketbar =
-  string "[|"
-
-let rbracketbar =
-  string "|]"
-
-let seq1 opening separator closing =
-  surround_separate 2 0 (opening ^^ closing) opening (separator ^^ break 1) closing
-
-let seq2 opening separator closing =
-  surround_separate_map 2 1 (opening ^^ closing) opening (separator ^^ break 1) closing
-
-(* ------------------------------------------------------------------------- *)
-
-(* The following functions are printers for many types of OCaml values. *)
-
-(* There is no protection against cyclic values. *)
-
-type representation =
-    document
-
-let tuple =
-  seq1 lparen comma rparen
-
-let variant _ cons _ args =
-  match args with
-  | [] ->
-      !^cons
-  | _ :: _ ->
-      !^cons ^^ tuple args
-
-let record _ fields =
-  seq2 lbrace semi rbrace (fun (k, v) -> infix 2 1 equals !^k v) fields
-
-let option f = function
-  | None ->
-      none
-  | Some x ->
-      some ^^ tuple [f x]
-
-let list f xs =
-  seq2 lbracket semi rbracket f xs
-
-let array f xs =
-  seq2 lbracketbar semi rbracketbar f (Array.to_list xs)
-
-let ref f x =
-  record "ref" ["contents", f !x]
-
-let float f =
-  string (float_representation f)
-
-let int =
-  dsprintf "%d"
-
-let int32 =
-  dsprintf "%ld"
-
-let int64 =
-  dsprintf "%Ld"
-
-let nativeint =
-  dsprintf "%nd"
-
-let char =
-  dsprintf "%C"
-
-let bool =
-  dsprintf "%B"
-
-let string =
-  dsprintf "%S"
-
-let unknown tyname _ =
-  dsprintf "<abstr:%s>" tyname
-
diff --git a/src/pprint/src/PPrintOCaml.mli b/src/pprint/src/PPrintOCaml.mli
deleted file mode 100644
index 119bca23..00000000
--- a/src/pprint/src/PPrintOCaml.mli
+++ /dev/null
@@ -1,90 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** A set of functions that construct representations of OCaml values. *)
-
-(** The string representations produced by these functions are supposed to be
-    accepted by the OCaml parser as valid values. *)
-
-(** The signature of this module is compatible with that expected by
-    the [camlp4] generator [Camlp4RepresentationGenerator]. *)
-
-(** These functions do {i not} distinguish between mutable and immutable
-    values. They do {i not} recognize sharing, and do {i not} incorporate a
-    protection against cyclic values. *)
-
-type constructor = string
-type type_name = string
-type record_field = string
-type tag = int
-
-(** A representation of a value is a [PPrint] document. *)
-type representation =
-    PPrintEngine.document
-
-(** [variant _ dc _ args] is a description of a constructed value whose data
-    constructor is [dc] and whose arguments are [args]. The other two
-    parameters are presently unused. *)
-val variant : type_name -> constructor -> tag -> representation list -> representation
-
-(** [record _ fields] is a description of a record value whose fields are
-    [fields]. The other parameter is presently unused. *)
-val record : type_name -> (record_field * representation) list -> representation
-
-(** [tuple args] is a description of a tuple value whose components are [args]. *)
-val tuple : representation list -> representation
-
-(** [string s] is a representation of the string [s]. *)
-val string : string -> representation
-
-(** [int i] is a representation of the integer [i]. *)
-val int : int -> representation
-
-(** [int32 i] is a representation of the 32-bit integer [i]. *)
-val int32 : int32 -> representation
-
-(** [int64 i] is a representation of the 64-bit integer [i]. *)
-val int64 : int64 -> representation
-
-(** [nativeint i] is a representation of the native integer [i]. *)
-val nativeint : nativeint -> representation
-
-(** [float f] is a representation of the floating-point number [f]. *)
-val float : float -> representation
-
-(** [char c] is a representation of the character [c]. *)
-val char : char -> representation
-
-(** [bool b] is a representation of the Boolenan value [b]. *)
-val bool : bool -> representation
-
-(** [option f o] is a representation of the option [o], where the
-    representation of the element, if present, is computed by the function
-    [f]. *)
-val option : ('a -> representation) -> 'a option -> representation
-
-(** [list f xs] is a representation of the list [xs], where the representation
-    of each element is computed by the function [f]. *)
-val list : ('a -> representation) -> 'a list -> representation
-
-(** [array f xs] is a representation of the array [xs], where the
-    representation of each element is computed by the function [f]. *)
-val array : ('a -> representation) -> 'a array -> representation
-
-(** [ref r] is a representation of the reference [r], where the
-    representation of the content is computed by the function [f]. *)
-val ref : ('a -> representation) -> 'a ref -> representation
-
-(** [unknown t _] is a representation of an unknown value of type [t]. *)
-val unknown : type_name -> 'a -> representation
-
diff --git a/src/pprint/src/PPrintRenderer.ml b/src/pprint/src/PPrintRenderer.ml
deleted file mode 100644
index 3449d6c3..00000000
--- a/src/pprint/src/PPrintRenderer.ml
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** A common signature for the multiple document renderers proposed by {!PPrintEngine}. *)
-
-module type RENDERER = sig
-  
-  (** Output channels. *)
-  type channel
-
-  (** Documents. *)
-  type document
-
-  (** [pretty rfrac width channel document] pretty-prints the document
-      [document] into the output channel [channel]. The parameter [width] is
-      the maximum number of characters per line. The parameter [rfrac] is the
-      ribbon width, a fraction relative to [width]. The ribbon width is the
-      maximum number of non-indentation characters per line. *)
-  val pretty: float -> int -> channel -> document -> unit
-
-  (** [compact channel document] prints the document [document] to the output
-      channel [channel]. No indentation is used. All newline instructions are
-      respected, that is, no groups are flattened. *)
-  val compact: channel -> document -> unit
-
-end
-
diff --git a/src/pprint/src/PPrintTest.ml b/src/pprint/src/PPrintTest.ml
deleted file mode 100644
index 37444127..00000000
--- a/src/pprint/src/PPrintTest.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*  PPrint                                                                *)
-(*                                                                        *)
-(*  François Pottier, Inria Paris                                         *)
-(*  Nicolas Pouillard                                                     *)
-(*                                                                        *)
-(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
-(*  distributed under the terms of the GNU Library General Public         *)
-(*  License, with an exception, as described in the file LICENSE.         *)
-(*                                                                        *)
-(**************************************************************************)
-
-open PPrint
-
-(* This is a test file. It is not, strictly speaking, part of the library. *)
-
-let paragraph (s : string) =
-  flow (break 1) (words s)
-
-let document =
-  prefix 2 1
-    (string "TITLE:")
-    (string "PPrint")
-  ^^
-  hardline
-  ^^
-  prefix 2 1
-    (string "AUTHORS:")
-    (utf8string "François Pottier and Nicolas Pouillard")
-  ^^
-  hardline
-  ^^
-  prefix 2 1
-    (string "ABSTRACT:")
-    (
-      paragraph "This is an adaptation of Daan Leijen's \"PPrint\" library,
-        which itself is based on the ideas developed by Philip Wadler in
-        \"A Prettier Printer\". For more information about Wadler's and Leijen's work,
-        please consult the following references:"
-      ^^
-      nest 2 (
-	twice (break 1)
-	^^
-	separate_map (break 1) (fun s -> nest 2 (url s)) [
-	  "http://www.cs.uu.nl/~daan/pprint.html";
-	  "http://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf";
-	]
-      )
-      ^^
-      twice (break 1)
-      ^^
-      paragraph "To install PPrint, type \"make -C src install\". ocamlfind is required."
-      ^^
-      twice (break 1)
-      ^^
-      paragraph "The documentation for PPrint is built by \"make doc\" and is found in the file doc/index.html."
-    )
-  ^^
-  hardline
-
-let () =
-  ToChannel.pretty 0.5 80 stdout document;
-  flush stdout