Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: braibant/invert
base: 009051e7f2
...
head fork: braibant/invert
compare: d51d24956e
  • 2 commits
  • 26 files changed
  • 0 commit comments
  • 1 contributor
View
7 Make
@@ -1,3 +1,10 @@
-R . Invert
+pprint/src/PPrintCombinators.ml
+pprint/src/PPrintOCaml.ml
+pprint/src/PPrintEngine.ml
+pprint/src/PPrintRenderer.ml
+pprint/src/PPrint.ml
+pprint/src/PPrintTest.ml
+print.ml
invert.ml4
test.v
View
4 invert.ml4
@@ -1,3 +1,7 @@
+module P = struct
+ open Print
+end
+
let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
let pp_constr_env env fmt x = Pp.pp_with fmt (Termops.print_constr_env env x)
let pp_gl fmt x = Pp.pp_with fmt (Printer.pr_goal x)
View
3  pprint/AUTHORS
@@ -0,0 +1,3 @@
+PPrint was written by François Pottier and Nicolas Pouillard, with
+contributions by Yann Régis-Gianas, Gabriel Scherer, and Jonathan
+Protzenko.
View
2  pprint/CHANGES
@@ -0,0 +1,2 @@
+2013/01/31
+First official release of PPrint.
View
517 pprint/LICENSE
@@ -0,0 +1,517 @@
+
+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.
View
13 pprint/README
@@ -0,0 +1,13 @@
+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.
+
View
5 pprint/src/META
@@ -0,0 +1,5 @@
+requires = ""
+description = "The PPrint pretty-printing library"
+archive(byte) = "PPrintLib.cma"
+archive(native) = "PPrintLib.cmxa"
+version = "20130131"
View
36 pprint/src/Makefile
@@ -0,0 +1,36 @@
+.PHONY: all install clean doc test
+
+OCAMLBUILD := ocamlbuild -use-ocamlfind -cflags "-g" -lflags "-g" -classic-display
+OCAMLFIND := ocamlfind
+DOCDIR := doc
+MAIN := PPrintTest
+TO_BUILD := PPrintLib.cma PPrintLib.cmxa
+TO_INSTALL := META \
+ $(patsubst %,_build/%,$(TO_BUILD)) \
+ _build/PPrintLib.a \
+ $(wildcard _build/*.cmx) $(wildcard _build/*.cmi)
+
+all:
+ $(OCAMLBUILD) $(TO_BUILD)
+
+install: all
+ $(OCAMLFIND) install pprint $(TO_INSTALL)
+
+clean:
+ rm -f *~ $(MAIN).native
+ rm -rf doc
+ $(OCAMLBUILD) -clean
+
+doc: all
+ @rm -rf $(DOCDIR)
+ @mkdir $(DOCDIR)
+ ocamlfind ocamldoc \
+ -html \
+ -I _build \
+ -d $(DOCDIR) \
+ -charset utf8 \
+ PPrintRenderer.ml *.mli PPrint.ml
+
+test: all
+ $(OCAMLBUILD) $(MAIN).native
+ ./$(MAIN).native
View
18 pprint/src/PPrint.ml
@@ -0,0 +1,18 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, as described *)
+(* in the file LICENSE. *)
+(* *)
+(**************************************************************************)
+
+(** A package of all of the above. *)
+
+include PPrintEngine
+include PPrintCombinators
+module OCaml = PPrintOCaml
View
2  pprint/src/PPrint.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrint.cmo :
+pprint/src/PPrint.cmx :
View
315 pprint/src/PPrintCombinators.ml
@@ -0,0 +1,315 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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 b docs =
+ foldli (fun i accu doc ->
+ if i = 0 then
+ doc
+ else
+ accu ^^
+ (* This idiom allows beginning a new line if [doc] does not
+ fit on the current line. *)
+ group (break b ^^ doc)
+ ) empty docs
+
+let url s =
+ flow 0 (split (function '/' | '.' -> true | _ -> false) s)
+
+(* ------------------------------------------------------------------------- *)
+
+(* Alignment and indentation. *)
+
+let align d =
+ column (fun k ->
+ nesting (fun i ->
+ nest (k - i) d
+ )
+ )
+
+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
+
View
2  pprint/src/PPrintCombinators.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrintCombinators.cmo : pprint/src/PPrintCombinators.cmi
+pprint/src/PPrintCombinators.cmx : pprint/src/PPrintCombinators.cmi
View
238 pprint/src/PPrintCombinators.mli
@@ -0,0 +1,238 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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 b docs] separates the documents in the list [docs] with breakable
+ spaces in such a way that a new line begins whenever a document does not
+ fit on the current line. This is useful for typesetting free-flowing,
+ ragged-right text. The parameter [b] is the number of spaces that must
+ be inserted between two consecutive words (when displayed on the same
+ line). *)
+val flow: int -> document 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} *)
+
+(** [align doc] increases the indentation level to reach the current
+ column. Thus, this document will be rendered within a box whose
+ upper left corner is the current position. *)
+val align: document -> document
+
+(* [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
+
View
703 pprint/src/PPrintEngine.ml
@@ -0,0 +1,703 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, as described *)
+(* in the file LICENSE. *)
+(* *)
+(**************************************************************************)
+
+(* ------------------------------------------------------------------------- *)
+
+(* The last element of a non-empty list. *)
+
+let rec last x xs =
+ match xs with
+ | [] ->
+ x
+ | x :: xs ->
+ last x xs
+
+let last = function
+ | [] ->
+ assert false
+ | x :: xs ->
+ last x xs
+
+(* ------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+
+(* A uniform interface for output channels. *)
+
+module type OUTPUT = sig
+ type channel
+ val char: channel -> char -> unit
+ val substring: channel -> string -> int (* offset *) -> int (* length *) -> unit
+end
+
+(* ------------------------------------------------------------------------- *)
+
+(* Three implementations of the above interface, respectively based on output
+ channels, memory buffers, and formatters. This compensates for the fact
+ that ocaml's standard library does not allow creating an output channel
+ that feeds into a memory buffer (a regrettable omission). *)
+
+module ChannelOutput : OUTPUT with type channel = out_channel = struct
+ type channel = out_channel
+ let char = output_char
+ let substring = output
+end
+
+module BufferOutput : OUTPUT with type channel = Buffer.t = struct
+ type channel = Buffer.t
+ let char = Buffer.add_char
+ let substring = Buffer.add_substring
+end
+
+module FormatterOutput : OUTPUT with type channel = Format.formatter = struct
+ type channel = Format.formatter
+ let char = Format.pp_print_char
+ let substring fmt = fst (Format.pp_get_formatter_output_functions fmt ())
+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, ofs, len)] is a document that consists of the portion of
+ the string [s] delimited by the offset [ofs] and the length [len]. We
+ assume, but do not check, that this portion does not contain a newline
+ character. *)
+
+ | String of string * int * int
+
+ (* [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
+
+ (* [Cat doc1 doc2] is the concatenation of the documents [doc1] and
+ [doc2]. *)
+
+ | Cat of 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. *)
+
+ | Nest of int * document
+
+ (* [Group 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. *)
+
+ | Group of document
+
+ (* [Column f] is the document obtained by applying [f] to the current
+ column number. *)
+
+ | Column of (int -> document)
+
+ (* [Nesting f] is the document obtained by applying [f] to the current
+ indentation level, that is, the number of blanks that were printed
+ at the beginning of the current line. *)
+
+ | Nesting of (int -> document)
+
+(* ------------------------------------------------------------------------- *)
+
+(* The above algebraic data type is not exposed to the user. Instead, we
+ expose the following functions. *)
+
+let empty =
+ Empty
+
+let char c =
+ assert (c <> '\n');
+ Char c
+
+let substring s ofs len =
+ if len = 0 then
+ Empty
+ else
+ String (s, ofs, len)
+
+let string s =
+ substring s 0 (String.length s)
+
+let fancysubstring s ofs len apparent_length =
+ if len = 0 then
+ Empty
+ else
+ FancyString (s, ofs, len, apparent_length)
+
+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 ->
+ Blank 1
+ | _ ->
+ Blank n
+
+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, x
+ | x, Empty ->
+ x
+ | _, _ ->
+ Cat (x, y)
+
+let nest i x =
+ assert (i >= 0);
+ Nest (i, x)
+
+let group x =
+ Group x
+
+let column f =
+ Column f
+
+let nesting f =
+ Nesting f
+
+let ifflat x y =
+ IfFlat (x, y)
+
+(* ------------------------------------------------------------------------- *)
+
+(* The pretty rendering algorithm: preliminary declarations. *)
+
+(* The renderer is supposed to behave exactly like Daan Leijen's, although its
+ implementation is quite radically different. Instead of relying on
+ Haskell's lazy evaluation mechanism, we implement an abstract machine with
+ mutable current state, forking, backtracking (via an explicit stack of
+ choice points), and cut (disposal of earlier choice points). *)
+
+(* The renderer's input consists of an ordered sequence of documents. Each
+ document carries an extra indentation level, akin to an implicit [Nest]
+ constructor, and a ``flattening'' flag, which, if set, means that this
+ document should be printed in flattening mode. *)
+
+(* An alternative coding style would be to avoid decorating each input
+ document with an indentation level and a flattening mode, and allow
+ the input sequence to contain instructions that set the current
+ nesting level or reset the flattening mode. That would perhaps be
+ slightly more readable, and slightly less efficient. *)
+
+type input =
+ | INil
+ | ICons of int * bool * document * input
+
+(* When possible (that is, when the stack is empty), the renderer writes
+ directly to the output channel. Otherwise, output is buffered until either
+ a failure point is reached (then, the buffered output is discarded) or a
+ cut is reached (then, all buffered output is committed to the output
+ channel). At all times, the length of the buffered output is at most one
+ line. *)
+
+(* The buffered output consists of a list of characters and strings. It is
+ stored in reverse order (the head of the list should be printed last). *)
+
+type output =
+ | OEmpty
+ | OChar of char * output
+ | OString of string * int * int * output
+ | OBlank of int * output
+
+(* The renderer maintains the following state record. For efficiency, the
+ record is mutable; it is copied when the renderer forks, that is, at
+ choice points. *)
+
+type 'channel state = {
+
+ (* The line width and ribbon width. *)
+
+ width: int;
+ ribbon: int;
+
+ (* The output channel. *)
+
+ channel: 'channel;
+
+ (* The current indentation level. This is the number of blanks that
+ were printed at the beginning of the current line. *)
+
+ mutable indentation: int;
+
+ (* The current column. *)
+
+ mutable column: int;
+
+ (* The renderer's input. For efficiency, the input is assumed to never be
+ empty, and the leading [ICons] constructor is inlined within the state
+ record. In other words, the fields [nest1], [flatten1], and [input1]
+ concern the first input document, and the field [input] contains the
+ rest of the input sequence. *)
+
+ mutable indent1: int;
+ mutable flatten1: bool;
+ mutable input1: document;
+ mutable input: input;
+
+ (* The renderer's buffer output. *)
+
+ mutable output: output;
+
+ }
+
+(* The renderer maintains a stack of resumptions, that is, states in which
+ execution should be resumed if the current thread of execution fails by
+ lack of space on the current line. *)
+
+(* It is not difficult to prove that the stack is empty if and only if
+ flattening mode is off. Furthermore, when flattening mode is on,
+ all groups are ignored, so no new choice points are pushed onto the
+ stack. As a result, the stack has height one at most at all times,
+ so that the stack height is zero when flattening mode is off and
+ one when flattening mode is on. *)
+
+type 'channel stack =
+ 'channel state list
+
+(* ------------------------------------------------------------------------- *)
+
+(* The pretty rendering algorithm: code. *)
+
+(* The renderer is parameterized over an implementation of output channels. *)
+
+module Renderer (Output : OUTPUT) = struct
+
+ type channel =
+ Output.channel
+
+ type dummy =
+ document
+ type document =
+ dummy
+
+ (* Printing blank space (indentation characters). *)
+
+ let blank_length =
+ 80
+
+ let blank_buffer =
+ String.make blank_length ' '
+
+ let rec blanks channel n =
+ if n <= 0 then
+ ()
+ else if n <= blank_length then
+ Output.substring channel blank_buffer 0 n
+ else begin
+ Output.substring channel blank_buffer 0 blank_length;
+ blanks channel (n - blank_length)
+ end
+
+ (* Committing buffered output to the output channel. The list is printed in
+ reverse order. The code is not tail recursive, but there is no risk of
+ stack overflow, since the length of the buffered output cannot exceed one
+ line. *)
+
+ let rec commit channel = function
+ | OEmpty ->
+ ()
+ | OChar (c, output) ->
+ commit channel output;
+ Output.char channel c
+ | OString (s, ofs, len, output) ->
+ commit channel output;
+ Output.substring channel s ofs len
+ | OBlank (n, output) ->
+ commit channel output;
+ blanks channel n
+
+ (* The renderer's abstract machine. *)
+
+ (* The procedures [run], [shift], [emit_char], [emit_string], and
+ [emit_blanks] are mutually recursive, and are tail recursive. They
+ maintain a stack and a current state. The states in the stack, and the
+ current state, are pairwise distinct, so that the current state can be
+ mutated without affecting the contents of the stack. *)
+
+ (* An invariant is: the buffered output is nonempty only when the stack is
+ nonempty. The contrapositive is: if the stack is empty, then the buffered
+ output is empty. Indeed, the fact that the stack is empty means that no
+ choices were made, so we are not in a speculative mode of execution: as a
+ result, all output can be sent directly to the output channel. On the
+ contrary, when the stack is nonempty, there is a possibility that we
+ might backtrack in the future, so all output should be held in a
+ buffer. *)
+
+ (* [run] is allowed to call itself recursively only when no material is
+ printed. In that case, the check for failure is skipped -- indeed,
+ this test is performed only within [shift]. *)
+
+ let rec run (stack : channel stack) (state : channel state) : unit =
+
+ (* Examine the first piece of input, as well as (in some cases) the
+ current flattening mode. *)
+
+ match state.input1, state.flatten1 with
+
+ (* The first piece of input is an empty document. Discard it
+ and continue. *)
+
+ | Empty, _ ->
+ shift stack state
+
+ (* The first piece of input is a character. Emit it and continue. *)
+
+ | Char c, _ ->
+ emit_char stack state c
+
+ (* The first piece of input is a string. Emit it and continue. *)
+
+ | String (s, ofs, len), _ ->
+ emit_string stack state s ofs len len
+ | FancyString (s, ofs, len, apparent_length), _ ->
+ emit_string stack state s ofs len apparent_length
+ | Blank n, _ ->
+ emit_blanks stack state n
+
+ (* The first piece of input is a hard newline instruction. *)
+
+ (* If flattening mode is off, then we behave as follows. We emit a newline
+ character, followed by the prescribed amount of indentation. We update
+ the current state to record how many indentation characters were
+ printed and to to reflect the new column number. Then, we discard the
+ current piece of input and continue. *)
+
+ | HardLine, false ->
+ assert (stack = []); (* since flattening mode is off, the stack must be empty. *)
+ Output.char state.channel '\n';
+ let i = state.indent1 in
+ blanks state.channel i;
+ state.column <- i;
+ state.indentation <- i;
+ shift stack state
+
+ (* If flattening mode is on, then [HardLine] causes an immediate failure. We
+ backtrack all the way to the state found at the bottom of the stack.
+ (Indeed, if we were to backtrack to the state found at the top of the stack,
+ then we would come back to this point in flattening mode, and fail again.)
+ This will take us back to non-flattening mode, so that, when we come back
+ to this [HardLine], we will be able to honor it. *)
+
+ | HardLine, true ->
+ assert (stack <> []); (* since flattening mode is on, the stack must be non-empty. *)
+ run [] (last stack)
+
+ (* The first piece of input is an [IfFlat] conditional instruction. *)
+
+ | IfFlat (doc, _), true
+ | IfFlat (_, doc), false ->
+ state.input1 <- doc;
+ run stack state
+
+ (* The first piece of input is a concatenation operator. We take it
+ apart and queue both documents in the input sequence. *)
+
+ | Cat (doc1, doc2), _ ->
+ state.input1 <- doc1;
+ state.input <- ICons (state.indent1, state.flatten1, doc2, state.input);
+ run stack state
+
+ (* The first piece of input is a [Nest] operator. We increase the amount
+ of indentation to be applied to the first input document. *)
+
+ | Nest (j, doc), _ ->
+ state.indent1 <- state.indent1 + j;
+ state.input1 <- doc;
+ run stack state
+
+ (* The first piece of input is a [Group] operator, and flattening mode
+ is currently off. This introduces a choice point: either we flatten
+ this whole group, or we don't. We try the former possibility first:
+ this is done by enabling flattening mode. Should this avenue fail,
+ we push the current state, in which flattening mode is disabled,
+ onto the stack. *)
+
+ (* Note that the current state is copied before continuing, so that
+ the state that is pushed on the stack is not affected by future
+ modifications. This is a fork. *)
+
+ | Group doc, false ->
+ state.input1 <- doc;
+ run (state :: stack) { state with flatten1 = true }
+
+ (* The first piece of input is a [Group] operator, and flattening mode
+ is currently on. The operator is ignored. *)
+
+ | Group doc, true ->
+ state.input1 <- doc;
+ run stack state
+
+ (* The first piece of input is a [Column] operator. The current column
+ is fed into it, so as to produce a document, with which we continue. *)
+
+ | Column f, _ ->
+ state.input1 <- f state.column;
+ run stack state
+
+ (* The first piece of input is a [Column] operator. The current
+ indentation level is fed into it, so as to produce a document, with
+ which we continue. *)
+
+ | Nesting f, _ ->
+ state.input1 <- f state.indentation;
+ run stack state
+
+ (* [shift] discards the first document in the input sequence, so that the
+ second input document, if there is one, becomes first. The renderer stops
+ if there is none. *)
+
+ and shift stack state =
+
+ assert (state.output = OEmpty || stack <> []);
+ assert (state.flatten1 = (stack <> []));
+
+ (* If the stack is nonempty and we have exceeded either the width or the
+ ribbon width parameters, then fail. Backtracking is implemented by
+ discarding the current state, popping a state off the stack, and making
+ it the current state. *)
+
+ match stack with
+ | resumption :: stack
+ when state.column > state.width
+ || state.column - state.indentation > state.ribbon ->
+ run stack resumption
+ | _ ->
+
+ match state.input with
+ | INil ->
+
+ (* End of input. Commit any buffered output and stop. *)
+
+ commit state.channel state.output
+
+ | ICons (indent, flatten, head, tail) ->
+
+ (* There is an input document. Move it one slot ahead and
+ check if we are leaving flattening mode. *)
+
+ state.indent1 <- indent;
+ state.input1 <- head;
+ state.input <- tail;
+ if state.flatten1 && not flatten then begin
+
+ (* Leaving flattening mode means success: we have flattened
+ a certain group, and fitted it all on a line, without
+ reaching a failure point. We would now like to commit our
+ decision to flatten this group. This is a Prolog cut. We
+ discard the stack of choice points, replacing it with an
+ empty stack, and commit all buffered output. *)
+
+ state.flatten1 <- flatten; (* false *)
+ commit state.channel state.output;
+ state.output <- OEmpty;
+ run [] state
+
+ end
+ else
+ run stack state
+
+ (* [emit_char] prints a character (either to the output channel or to the
+ output buffer), increments the current column, discards the first piece
+ of input, and continues. *)
+
+ and emit_char stack state c =
+ begin match stack with
+ | [] ->
+ Output.char state.channel c
+ | _ ->
+ state.output <- OChar (c, state.output)
+ end;
+ state.column <- state.column + 1;
+ shift stack state
+
+ (* [emit_string] prints a string (either to the output channel or to the
+ output buffer), updates the current column, discards the first piece of
+ input, and continues. *)
+
+ and emit_string stack state s ofs len apparent_length =
+ begin match stack with
+ | [] ->
+ Output.substring state.channel s ofs len
+ | _ ->
+ state.output <- OString (s, ofs, len, state.output)
+ end;
+ state.column <- state.column + apparent_length;
+ shift stack state
+
+ (* [emit_blanks] prints a blank string (either to the output channel or to
+ the output buffer), updates the current column, discards the first piece
+ of input, and continues. *)
+
+ and emit_blanks stack state n =
+ begin match stack with
+ | [] ->
+ blanks state.channel n
+ | _ ->
+ state.output <- OBlank (n, state.output)
+ end;
+ state.column <- state.column + n;
+ shift stack state
+
+ (* This is the renderer's main entry point. *)
+
+ let pretty rfrac width channel document =
+ run [] {
+ width = width;
+ ribbon = max 0 (min width (truncate (float_of_int width *. rfrac)));
+ channel = channel;
+ indentation = 0;
+ column = 0;
+ indent1 = 0;
+ flatten1 = false;
+ input1 = document;
+ input = INil;
+ output = OEmpty;
+ }
+
+(* ------------------------------------------------------------------------- *)
+
+(* The compact rendering algorithm. *)
+
+ let compact channel document =
+
+ let column =
+ ref 0
+ in
+
+ let rec scan = function
+ | Empty ->
+ ()
+ | Char c ->
+ Output.char channel c;
+ column := !column + 1
+ | String (s, ofs, len) ->
+ Output.substring channel s ofs len;
+ column := !column + len
+ | FancyString (s, ofs, len, apparent_length) ->
+ Output.substring channel s ofs len;
+ column := !column + apparent_length
+ | Blank n ->
+ blanks channel n;
+ column := !column + n
+ | HardLine ->
+ Output.char channel '\n';
+ column := 0
+ | Cat (doc1, doc2) ->
+ scan doc1;
+ scan doc2
+ | IfFlat (doc, _)
+ | Nest (_, doc)
+ | Group doc ->
+ scan doc
+ | Column f ->
+ scan (f !column)
+ | Nesting f ->
+ scan (f 0)
+ in
+
+ scan document
+
+end
+
+(* ------------------------------------------------------------------------- *)
+
+(* Instantiating the renderers for the three kinds of output channels. *)
+
+module ToChannel =
+ Renderer(ChannelOutput)
+
+module ToBuffer =
+ Renderer(BufferOutput)
+
+module ToFormatter =
+ Renderer(FormatterOutput)
+
View
2  pprint/src/PPrintEngine.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrintEngine.cmo : pprint/src/PPrintEngine.cmi
+pprint/src/PPrintEngine.cmx : pprint/src/PPrintEngine.cmi
View
126 pprint/src/PPrintEngine.mli
@@ -0,0 +1,126 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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 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
+
+(** [column f] is the document obtained by applying the function [f] to the
+ current column number. This combinator allows making the construction of
+ a document dependent on the current column number. *)
+val column: (int -> document) -> document
+
+(** [nesting f] is the document obtained by applying the function [f] to the
+ current indentation level, that is, the number of indentation (blank)
+ characters that were inserted at the beginning of the current line. *)
+val nesting: (int -> 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
+
+(** {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
+
View
5 pprint/src/PPrintLib.mllib
@@ -0,0 +1,5 @@
+PPrint
+PPrintCombinators
+PPrintEngine
+PPrintOCaml
+PPrintRenderer
View
158 pprint/src/PPrintOCaml.ml
@@ -0,0 +1,158 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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
+
View
2  pprint/src/PPrintOCaml.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrintOCaml.cmo : pprint/src/PPrintOCaml.cmi
+pprint/src/PPrintOCaml.cmx : pprint/src/PPrintOCaml.cmi
View
90 pprint/src/PPrintOCaml.mli
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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
+
View
37 pprint/src/PPrintRenderer.ml
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, 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
+
View
2  pprint/src/PPrintRenderer.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrintRenderer.cmo :
+pprint/src/PPrintRenderer.cmx :
View
61 pprint/src/PPrintTest.ml
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(* *)
+(* PPrint *)
+(* *)
+(* Francois Pottier, INRIA Paris-Rocquencourt *)
+(* Nicolas Pouillard, IT University of Copenhagen *)
+(* *)
+(* Copyright 2007-2013 INRIA. All rights reserved. This file is *)
+(* distributed under the terms of the CeCILL-C license, as described *)
+(* in the file LICENSE. *)
+(* *)
+(**************************************************************************)
+
+open PPrint
+
+(* This is a test file. It is not, strictly speaking, part of the library. *)
+
+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:")
+ (
+ flow 1 (words "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)
+ ^^
+ flow 1 (words "To install PPrint, type \"make -C src install\". ocamlfind is required.")
+ ^^
+ twice (break 1)
+ ^^
+ flow 1 (words "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
View
2  pprint/src/PPrintTest.ml.d
@@ -0,0 +1,2 @@
+pprint/src/PPrintTest.cmo :
+pprint/src/PPrintTest.cmx :
View
18 print.ml
@@ -0,0 +1,18 @@
+include PPrintEngine
+include PPrintCombinators
+
+let format fmt = Printf.ksprintf string fmt
+
+let int i = string (string_of_int i)
+
+let bool = function true -> string "true"
+ | false -> string "false"
+
+let run out doc = ToChannel.pretty 1. 80 out doc
+