diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/_tags | 3 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/myocamlbuild.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 29 | ||||
| -rw-r--r-- | src/pprint/AUTHORS | 3 | ||||
| -rw-r--r-- | src/pprint/CHANGES | 27 | ||||
| -rw-r--r-- | src/pprint/LICENSE | 517 | ||||
| -rw-r--r-- | src/pprint/README | 13 | ||||
| -rwxr-xr-x | src/pprint/src/META | 5 | ||||
| -rw-r--r-- | src/pprint/src/Makefile | 35 | ||||
| -rw-r--r-- | src/pprint/src/PPrint.ml | 18 | ||||
| -rw-r--r-- | src/pprint/src/PPrintCombinators.ml | 311 | ||||
| -rw-r--r-- | src/pprint/src/PPrintCombinators.mli | 236 | ||||
| -rw-r--r-- | src/pprint/src/PPrintEngine.ml | 637 | ||||
| -rw-r--r-- | src/pprint/src/PPrintEngine.mli | 226 | ||||
| -rw-r--r-- | src/pprint/src/PPrintLib.mllib | 5 | ||||
| -rw-r--r-- | src/pprint/src/PPrintOCaml.ml | 158 | ||||
| -rw-r--r-- | src/pprint/src/PPrintOCaml.mli | 90 | ||||
| -rw-r--r-- | src/pprint/src/PPrintRenderer.ml | 37 | ||||
| -rw-r--r-- | src/pprint/src/PPrintTest.ml | 64 | ||||
| -rw-r--r-- | src/pretty_print.ml | 525 | ||||
| -rw-r--r-- | src/pretty_print.mli | 7 | ||||
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 16 |
24 files changed, 2947 insertions, 19 deletions
@@ -1,7 +1,8 @@ true: -traverse, debug <**/*.ml>: bin_annot, annot <lem_interp> or <test>: include +<sail.{byte,native}>: use_pprint +<pprint> or <pprint/src>: include # see http://caml.inria.fr/mantis/view.php?id=4943 <lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem <test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str - diff --git a/src/lexer.mll b/src/lexer.mll index 988ddb7c..ad6ea0d9 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -218,6 +218,7 @@ rule token = parse | "*_u" { (StarUnderU(r"*_u")) } | "*_ui" { (StarUnderUi(r"*_ui")) } | "2^" { (TwoCarrot(r"2^")) } + | "2**" { TwoStarStar } | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index 70e2b633..4c5505ee 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -36,6 +36,7 @@ dispatch begin function | After_rules -> (* ocaml_lib "lem_interp/interp"; *) ocaml_lib ~extern:true ~dir:lem_libdir ~tag_name:"use_lem" lem_lib; + ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib"; rule "lem -> ml" ~prod: "%.ml" diff --git a/src/parser.mly b/src/parser.mly index 3c3cf8e0..75cdcf7d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -367,6 +367,7 @@ app_num_typ: | Num { tloc (ATyp_constant $1) } +/* XXX this part of the parser makes absolutely no sense to me */ star_typ_list: | app_num_typ { [$1] } @@ -378,6 +379,8 @@ star_typ: { match $1 with | [] -> assert false | [t] -> t + (* XXX why is ATyp_tup star-separated here, but comma-separated + below? *) | ts -> tloc (ATyp_tup(ts)) } exp_typ: @@ -386,6 +389,7 @@ exp_typ: | TwoStarStar nexp_typ { tloc (ATyp_exp($2)) } +/* XXX this is wrong - for instance, 2** 3 + 5 is parsed as 2** (3+5) */ nexp_typ: | exp_typ { $1 } @@ -532,6 +536,9 @@ atomic_exp: { eloc (E_cast($2,$4)) } | Lparen comma_exps Rparen { eloc (E_tuple($2)) } + /* XXX creates many conflicts + | Lcurly semi_exps Rcurly + { eloc (E_record($2)) } */ | Lcurly exp With semi_exps Rcurly { eloc (E_record_update($2,$4)) } | Lsquare Rsquare @@ -568,6 +575,7 @@ app_exp: { $1 } | id Lparen Rparen { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) } + /* we wrap into a tuple here, but this is unwrapped in initial_check.ml */ | id Lparen exp Rparen { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) } | id Lparen comma_exps Rparen @@ -614,6 +622,9 @@ starstar_exp: | starstar_exp StarStar app_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } +/* this is where we diverge from the non-right_atomic path; + here we go directly to right_atomic whereas the other one + goes through app_exp, vaccess_exp and field_exp too. */ starstar_right_atomic_exp: | right_atomic_exp { $1 } @@ -661,8 +672,12 @@ star_right_atomic_exp: { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) } | star_exp StarUnderS starstar_right_atomic_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderSi starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } | star_exp StarUnderU starstar_right_atomic_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderUi starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } plus_exp: | star_exp @@ -718,6 +733,8 @@ cons_right_atomic_exp: { $1 } | shift_exp ColonColon cons_right_atomic_exp { eloc (E_cons($1,$3)) } + | shift_exp Colon cons_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id(":"), locn 2 2), $3)) } at_exp: | cons_exp @@ -740,10 +757,13 @@ at_right_atomic_exp: { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } | cons_exp Carrot at_right_atomic_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp TildeCarrot at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } eq_exp: | at_exp { $1 } + /* XXX check for consistency */ | eq_exp Eq at_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } | eq_exp EqEq at_exp @@ -774,6 +794,8 @@ eq_exp: { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } | eq_exp LtUnderU at_exp { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + /* XXX assignement should not have the same precedence as equal, + otherwise a := b > c requires extra parens... */ | eq_exp ColonEq at_exp { eloc (E_assign($1,$3)) } @@ -918,7 +940,7 @@ fun_def: { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } | Function_ Rec funcl_ands { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) } - | Function_ typquant atomic_typ Effect effect_typ funcl_ands + | Function_ typquant typ Effect effect_typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) } | Function_ typquant typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) } @@ -992,7 +1014,10 @@ typquant: name_sect: | Lsquare Id Eq String Rsquare - { Name_sect_aux(Name_sect_some($4), loc ()) } + { + if $2 <> "name" then + raise (Parse_error_locn ((loc ()),"Unexpected id \""^$2^"\" in name_sect (should be \"name\")")); + Name_sect_aux(Name_sect_some($4), loc ()) } c_def_body: | typ id diff --git a/src/pprint/AUTHORS b/src/pprint/AUTHORS new file mode 100644 index 00000000..6060ac93 --- /dev/null +++ b/src/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. diff --git a/src/pprint/CHANGES b/src/pprint/CHANGES new file mode 100644 index 00000000..69747a41 --- /dev/null +++ b/src/pprint/CHANGES @@ -0,0 +1,27 @@ +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 new file mode 100644 index 00000000..d6eb151e --- /dev/null +++ b/src/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. diff --git a/src/pprint/README b/src/pprint/README new file mode 100644 index 00000000..7146250a --- /dev/null +++ b/src/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. + diff --git a/src/pprint/src/META b/src/pprint/src/META new file mode 100755 index 00000000..b7d43d40 --- /dev/null +++ b/src/pprint/src/META @@ -0,0 +1,5 @@ +requires = "" +description = "The PPrint pretty-printing library" +archive(byte) = "PPrintLib.cma" +archive(native) = "PPrintLib.cmxa" +version = "20140424" diff --git a/src/pprint/src/Makefile b/src/pprint/src/Makefile new file mode 100644 index 00000000..f56f4d88 --- /dev/null +++ b/src/pprint/src/Makefile @@ -0,0 +1,35 @@ +.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 + +all: + $(OCAMLBUILD) $(TO_BUILD) + +install: all + $(OCAMLFIND) install pprint META \ + $(patsubst %,_build/%,$(TO_BUILD)) \ + _build/PPrintLib.a _build/*.cmx _build/*.cmi + +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 + diff --git a/src/pprint/src/PPrint.ml b/src/pprint/src/PPrint.ml new file mode 100644 index 00000000..ae1ff709 --- /dev/null +++ b/src/pprint/src/PPrint.ml @@ -0,0 +1,18 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 diff --git a/src/pprint/src/PPrintCombinators.ml b/src/pprint/src/PPrintCombinators.ml new file mode 100644 index 00000000..39b99b9c --- /dev/null +++ b/src/pprint/src/PPrintCombinators.ml @@ -0,0 +1,311 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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_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 new file mode 100644 index 00000000..ef2b44ea --- /dev/null +++ b/src/pprint/src/PPrintCombinators.mli @@ -0,0 +1,236 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 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 new file mode 100644 index 00000000..cfa8474a --- /dev/null +++ b/src/pprint/src/PPrintEngine.ml @@ -0,0 +1,637 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) +(* distributed under the terms of the CeCILL-C license, 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 channel +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, 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 + + (* 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 (_, _, len) + | 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 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 -> + 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, ofs, len) -> + output#substring s ofs 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, ofs, len) -> + output#substring s ofs 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 new file mode 100644 index 00000000..7f6fcf35 --- /dev/null +++ b/src/pprint/src/PPrintEngine.mli @@ -0,0 +1,226 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 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 new file mode 100644 index 00000000..e5de6978 --- /dev/null +++ b/src/pprint/src/PPrintLib.mllib @@ -0,0 +1,5 @@ +PPrint +PPrintCombinators +PPrintEngine +PPrintOCaml +PPrintRenderer diff --git a/src/pprint/src/PPrintOCaml.ml b/src/pprint/src/PPrintOCaml.ml new file mode 100644 index 00000000..88e039ce --- /dev/null +++ b/src/pprint/src/PPrintOCaml.ml @@ -0,0 +1,158 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 + diff --git a/src/pprint/src/PPrintOCaml.mli b/src/pprint/src/PPrintOCaml.mli new file mode 100644 index 00000000..e1395203 --- /dev/null +++ b/src/pprint/src/PPrintOCaml.mli @@ -0,0 +1,90 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 + diff --git a/src/pprint/src/PPrintRenderer.ml b/src/pprint/src/PPrintRenderer.ml new file mode 100644 index 00000000..9096eada --- /dev/null +++ b/src/pprint/src/PPrintRenderer.ml @@ -0,0 +1,37 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 + diff --git a/src/pprint/src/PPrintTest.ml b/src/pprint/src/PPrintTest.ml new file mode 100644 index 00000000..3e4fb2c9 --- /dev/null +++ b/src/pprint/src/PPrintTest.ml @@ -0,0 +1,64 @@ +(**************************************************************************) +(* *) +(* PPrint *) +(* *) +(* Francois Pottier, INRIA Paris-Rocquencourt *) +(* Nicolas Pouillard, IT University of Copenhagen *) +(* *) +(* Copyright 2007-2014 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 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 diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 759e2f4a..9f0382f5 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -133,7 +133,7 @@ let pp_format_nexp_constraint (NC_aux(nc,_)) = | NC_bounded_le(n1,n2) -> pp_format_nexp n1 ^ " <= " ^ pp_format_nexp n2 | NC_nat_set_bounded(var,bounds) -> pp_format_var var ^ - " In {" ^ + " IN {" ^ list_format ", " string_of_int bounds ^ "}" @@ -167,8 +167,8 @@ let pp_typscm ppf ts = base ppf (pp_format_typscm ts) let pp_format_lit (L_aux(l,_)) = match l with | L_unit -> "()" - | L_zero -> "0" - | L_one -> "1" + | L_zero -> "bitzero" + | L_one -> "bitone" | L_true -> "true" | L_false -> "false" | L_num(i) -> string_of_int i @@ -255,6 +255,9 @@ and pp_exp ppf (E_aux(e,(_,annot))) = | E_case(exp,pexps) -> fprintf ppf "@[<0>%a %a %a %a %a@]" kwd "switch " pp_exp exp kwd "{" (list_pp pp_case pp_case) pexps kwd "}" | E_let(leb,exp) -> fprintf ppf "@[<0>%a@ %a@ %a@]" pp_let leb kwd "in" pp_exp exp | E_assign(lexp,exp) -> fprintf ppf "@[<0>%a%a%a@]" pp_lexp lexp kwd " := " pp_exp exp + (* XXX missing cases *) + | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false + and pp_semi_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_exp e kwd ";" @@ -603,6 +606,8 @@ let pp_format_annot = function | NoTyp -> "Nothing" | Base((_,t),tag,nes,efct) -> "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))" + (* XXX missing case *) + | Overload _ -> assert false let pp_annot ppf ant = base ppf (pp_format_annot ant) @@ -689,6 +694,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot + (* XXX missing cases *) + | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false in print_e ppf e @@ -814,3 +821,515 @@ let pp_lem_def ppf d = let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs + + +(** PPrint based source-to-source pretty-printer *) + +open PPrint + +let doc_id (Id_aux(i,_)) = + match i with + | Id i -> string i + | DeIid x -> + (* add an extra space through empty to avoid a closing-comment + * token in case of x ending with star. *) + parens (separate space [string "deinfix"; string x; empty]) + +let doc_var (Kid_aux(Var v,_)) = string v + +let doc_int i = string (string_of_int i) + +let doc_bkind (BK_aux(k,_)) = + string (match k with + | BK_type -> "Type" + | BK_nat -> "Nat" + | BK_order -> "Order" + | BK_effect -> "Effect") + +let doc_op symb a b = infix 2 1 symb a b +let doc_unop symb a = prefix 2 1 symb a + +let arrow = string "->" +let dotdot = string ".." +let coloneq = string ":=" +let lsquarebarbar = string "[||" +let rsquarebarbar = string "||]" +let squarebarbars = enclose lsquarebarbar rsquarebarbar +let spaces op = enclose space space op +let semi_sp = semi ^^ space +let comma_sp = comma ^^ space +let colon_sp = spaces colon + +let doc_kind (K_aux(K_kind(klst),_)) = + separate_map (spaces arrow) doc_bkind klst + +let doc_effect (BE_aux (e,_)) = + string (match e with + | BE_rreg -> "rreg" + | BE_wreg -> "wreg" + | BE_rmem -> "rmem" + | BE_wmem -> "wmem" + | BE_undef -> "undef" + | BE_unspec -> "unspec" + | BE_nondet -> "nondet") + +let doc_effects (Effect_aux(e,_)) = match e with + | Effect_var v -> doc_var v + | Effect_set [] -> string "pure" + | Effect_set s -> braces (separate_map comma_sp doc_effect s) + +let doc_ord (Ord_aux(o,_)) = match o with + | Ord_var v -> doc_var v + | Ord_inc -> string "inc" + | Ord_dec -> string "dec" + +let doc_typ, doc_atomic_typ, doc_nexp = + (* following the structure of parser for precedence *) + let rec typ ty = fn_typ ty + and fn_typ ((Typ_aux (t, _)) as ty) = match t with + | Typ_fn(arg,ret,efct) -> + separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct] + | _ -> tup_typ ty + and tup_typ ((Typ_aux (t, _)) as ty) = match t with + | Typ_tup typs -> parens (separate_map comma_sp app_typ typs) + | _ -> app_typ ty + and app_typ ((Typ_aux (t, _)) as ty) = match t with + | Typ_app(id,args) -> + (* trailing space to avoid >> token in case of nested app types *) + (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space + | _ -> atomic_typ ty (* for simplicity, skip vec_typ - which is only sugar *) + and atomic_typ ((Typ_aux (t, _)) as ty) = match t with + | Typ_id id -> doc_id id + | Typ_var v -> doc_var v + | Typ_wild -> underscore + | Typ_app _ | Typ_tup _ | Typ_fn _ -> + (* exhaustiveness matters here to avoid infinite loops + * if we add a new Typ constructor *) + group (parens (typ ty)) + and doc_typ_arg (Typ_arg_aux(t,_)) = match t with + (* Be careful here because typ_arg is implemented as nexp in the + * parser - in practice falling through app_typ after all the proper nexp + * cases; so Typ_arg_typ has the same precedence as a Typ_app *) + | Typ_arg_typ t -> app_typ t + | Typ_arg_nexp n -> nexp n + | Typ_arg_order o -> doc_ord o + | Typ_arg_effect e -> doc_effects e + + (* same trick to handle precedence of nexp *) + and nexp ne = sum_typ ne + and sum_typ ((Nexp_aux(n,_)) as ne) = match n with + | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2) + | _ -> star_typ ne + and star_typ ((Nexp_aux(n,_)) as ne) = match n with + | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2) + | _ -> exp_typ ne + and exp_typ ((Nexp_aux(n,_)) as ne) = match n with + | Nexp_exp n1 -> doc_unop (string "2**") (neg_typ n1) + | _ -> neg_typ ne + and neg_typ ((Nexp_aux(n,_)) as ne) = match n with + | Nexp_neg n1 -> + (* XXX this is not valid Sail, only an internal representation - + * work around by commenting it *) + let minus = concat [string "(*"; minus; string "*)"] in + minus ^^ (atomic_nexp_typ n1) + | _ -> atomic_nexp_typ ne + and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with + | Nexp_var v -> doc_var v + | Nexp_constant i -> doc_int i + | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ -> + group (parens (nexp ne)) + + (* expose doc_typ, doc_atomic_typ and doc_nexp *) + in typ, atomic_typ, nexp + +let doc_nexp_constraint (NC_aux(nc,_)) = match nc with + | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2) + | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2) + | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_nexp n2) + | NC_nat_set_bounded(v,bounds) -> + doc_op (string "IN") (doc_var v) + (braces (separate_map comma_sp doc_int bounds)) + +let doc_qi (QI_aux(qi,_)) = match qi with + | QI_const n_const -> doc_nexp_constraint n_const + | QI_id(KOpt_aux(ki,_)) -> + match ki with + | KOpt_none v -> doc_var v + | KOpt_kind(k,v) -> separate space [doc_kind k; doc_var v] + +(* typ_doc is the doc for the type being quantified *) +let doc_typquant (TypQ_aux(tq,_)) typ_doc = match tq with + | TypQ_no_forall -> typ_doc + | TypQ_tq [] -> failwith "TypQ_tq with empty list" + | TypQ_tq qlist -> + (* include trailing break because the caller doesn't know if tq is empty *) + doc_op dot + (separate space [string "forall"; separate_map comma_sp doc_qi qlist]) + typ_doc + +let doc_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) = + (doc_typquant tq (doc_typ t)) + +let doc_typscm_atomic (TypSchm_aux(TypSchm_ts(tq,t),_)) = + (doc_typquant tq (doc_atomic_typ t)) + +let doc_lit (L_aux(l,_)) = + utf8string (match l with + | L_unit -> "()" + | L_zero -> "bitzero" + | L_one -> "bitone" + | L_true -> "true" + | L_false -> "false" + | L_num i -> string_of_int i + | L_hex n -> "0x" ^ n + | L_bin n -> "0b" ^ n + | L_undef -> "undefined" + | L_string s -> "\"" ^ s ^ "\"") + +let doc_pat, doc_atomic_pat = + let rec pat pa = pat_colons pa + and pat_colons ((P_aux(p,l)) as pa) = match p with + | P_vector_concat pats -> separate_map colon_sp atomic_pat pats + | _ -> app_pat pa + and app_pat ((P_aux(p,l)) as pa) = match p with + | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id id) (parens (separate_map comma_sp atomic_pat pats)) + | _ -> atomic_pat pa + and atomic_pat ((P_aux(p,l)) as pa) = match p with + | P_lit lit -> doc_lit lit + | P_wild -> underscore + | P_id id -> doc_id id + | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id id]) + | P_typ(typ,p) -> separate space [parens (doc_typ typ); atomic_pat p] + | P_app(id,[]) -> doc_id id + | P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats) + | P_vector pats -> brackets (separate_map comma_sp atomic_pat pats) + | P_vector_indexed ipats -> brackets (separate_map comma_sp npat ipats) + | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) + | P_list pats -> squarebarbars (separate_map semi_sp atomic_pat pats) + | P_app(_, _ :: _) | P_vector_concat _ -> + group (parens (pat pa)) + and fpat (FP_aux(FP_Fpat(id,fpat),_)) = doc_op equals (doc_id id) (pat fpat) + and npat (i,p) = doc_op equals (doc_int i) (pat p) + + (* expose doc_pat and doc_atomic_pat *) + in pat, atomic_pat + +let doc_exp, doc_let = + let rec exp e = group (or_exp e) + and or_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) -> + doc_op (doc_id op) (and_exp l) (or_exp r) + | _ -> and_exp expr + and and_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) -> + doc_op (doc_id op) (eq_exp l) (and_exp r) + | _ -> eq_exp expr + and eq_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ( + (* XXX this is not very consistent - is the parser bogus here? *) + "=" | "==" | "!=" + | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" + | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" + ),_) as op),r) -> + doc_op (doc_id op) (eq_exp l) (at_exp r) + (* XXX assignment should not have the same precedence as equal etc. *) + | E_assign(le,exp) -> doc_op coloneq (doc_lexp le) (at_exp exp) + | _ -> at_exp expr + and at_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) -> + doc_op (doc_id op) (cons_exp l) (at_exp r) + | _ -> cons_exp expr + and cons_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id (":"),_) as op),r) -> + doc_op (doc_id op) (shift_exp l) (cons_exp r) + | E_cons(l,r) -> + doc_op colon (shift_exp l) (cons_exp r) + | _ -> shift_exp expr + and shift_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) -> + doc_op (doc_id op) (shift_exp l) (plus_exp r) + | _ -> plus_exp expr + and plus_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ("+" | "-"),_) as op),r) -> + doc_op (doc_id op) (plus_exp l) (star_exp r) + | _ -> star_exp expr + and star_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id ( + "*" | "/" + | "div" | "quot" | "rem" | "mod" + | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) -> + doc_op (doc_id op) (star_exp l) (starstar_exp r) + | _ -> starstar_exp expr + and starstar_exp ((E_aux(e,_)) as expr) = match e with + | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> + doc_op (doc_id op) (starstar_exp l) (app_exp r) + | E_if _ | E_for _ | E_let _ -> right_atomic_exp expr + | _ -> app_exp expr + and right_atomic_exp ((E_aux(e,_)) as expr) = match e with + (* Special case: omit "else ()" when the else branch is empty. *) + | E_if(c,t,E_aux(E_block [], _)) -> + string "if" ^^ space ^^ group (exp c) ^/^ + string "then" ^^ space ^^ group (exp t) + | E_if(c,t,e) -> + string "if" ^^ space ^^ group (exp c) ^/^ + string "then" ^^ space ^^ group (exp t) ^/^ + string "else" ^^ space ^^ group (exp e) + | E_for(id,exp1,exp2,exp3,order,exp4) -> + string "foreach" ^^ space ^^ + group (parens ( + separate (break 1) [ + doc_id id; + string "from " ^^ atomic_exp exp1; + string "to " ^^ atomic_exp exp2; + string "by " ^^ atomic_exp exp3; + string "in " ^^ doc_ord order + ] + )) ^/^ + exp exp4 + | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) + | _ -> group (parens (exp expr)) + and app_exp ((E_aux(e,_)) as expr) = match e with + | E_app(f,args) -> + doc_unop (doc_id f) (parens (separate_map comma exp args)) + | _ -> vaccess_exp expr + and vaccess_exp ((E_aux(e,_)) as expr) = match e with + | E_vector_access(v,e) -> + atomic_exp v ^^ brackets (exp e) + | E_vector_subrange(v,e1,e2) -> + atomic_exp v ^^ brackets (doc_op dotdot (exp e1) (exp e2)) + | _ -> field_exp expr + and field_exp ((E_aux(e,_)) as expr) = match e with + | E_field(fexp,id) -> atomic_exp fexp ^^ dot ^^ doc_id id + | _ -> atomic_exp expr + and atomic_exp ((E_aux(e,_)) as expr) = match e with + (* Special case: an empty block is equivalent to unit, but { } would + * be parsed as a struct. *) + | E_block [] -> string "()" + | E_block exps -> + let exps_doc = separate_map (semi ^^ hardline) exp exps in + surround 2 1 lbrace exps_doc rbrace + | E_id id -> doc_id id + | E_lit lit -> doc_lit lit + | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e)) + | E_internal_cast((_,NoTyp),e) -> atomic_exp e + | E_internal_cast((_,Base((_,t),_,_,_)), (E_aux(_,(_,eannot)) as e)) -> + (match t.t,eannot with + (* XXX I don't understand why we can hide the internal cast here *) + | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) + when nexp_eq n1 n2 -> atomic_exp e + | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e))) + | E_tuple exps -> + parens (separate_map comma exp exps) + | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + (* XXX E_record is not handled by parser currently *) + braces (separate_map semi_sp doc_fexp fexps) + | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> + braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) + | E_vector exps -> + brackets (separate_map comma exp exps) + | E_vector_indexed (iexps, default) -> + (* XXX TODO print default when it is non-empty *) + let iexp (i,e) = doc_op equals (doc_int i) (exp e) in + brackets (separate_map comma iexp iexps) + | E_vector_update(v,e1,e2) -> + brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2))) + | E_vector_update_subrange(v,e1,e2,e3) -> + brackets ( + doc_op (string "with") (exp v) + (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3))) + | E_list exps -> + squarebarbars (separate_map comma exp exps) + | E_case(e,pexps) -> + let opening = separate space [string "switch"; exp e; lbrace] in + let cases = separate_map (break 1) doc_case pexps in + surround 2 1 opening cases rbrace + (* adding parens and loop for lower precedence *) + | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) + | E_cons (_, _)|E_field (_, _)|E_assign (_, _) + | E_app_infix (_, + (* for every app_infix operator caught at a higher precedence, + * we need to wrap around with parens *) + (Id_aux(Id("|" | "||" + | "&" | "&&" + | "=" | "==" | "!=" + | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" + | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" + | "@" | "^^" | "^" | "~^" + | ":" + | ">>" | ">>>" | "<<" | "<<<" + | "+" | "-" + | "*" | "/" + | "div" | "quot" | "rem" | "mod" + | "*_s" | "*_si" | "*_u" | "*_ui" + | "**"), _)) + , _) -> + group (parens (exp expr)) + (* XXX default precedence for app_infix? *) + | E_app_infix(l,op,r) -> + failwith ("unexpected app_infix operator " ^ (pp_format_id op)) + (* doc_op (doc_id op) (exp l) (exp r) *) + (* XXX missing case *) + | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false + + and let_exp (LB_aux(lb,_)) = match lb with + | LB_val_explicit(ts,pat,e) -> + prefix 2 1 + (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals]) + (exp e) + | LB_val_implicit(pat,e) -> + prefix 2 1 + (separate space [string "let"; doc_atomic_pat pat; equals]) + (exp e) + + and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) + + and doc_case (Pat_aux(Pat_exp(pat,e),_)) = + doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e)) + + (* lexps are parsed as eq_exp - we need to duplicate the precedence + * structure for them *) + and doc_lexp le = app_lexp le + and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args) + | _ -> vaccess_lexp le + and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e) + | LEXP_vector_range(v,e1,e2) -> + atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) + | _ -> field_lexp le + and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id + | _ -> atomic_lexp le + and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with + | LEXP_id id -> doc_id id + | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) + | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ + | LEXP_field _ -> group (parens (doc_lexp le)) + + (* expose doc_exp and doc_let *) + in exp, let_exp + +let doc_default (DT_aux(df,_)) = match df with + | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v] + | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id] + +let doc_spec (VS_aux(v,_)) = match v with + | VS_val_spec(ts,id) -> + separate space [string "val"; doc_typscm ts; doc_id id] + | VS_extern_no_rename(ts,id) -> + separate space [string "val"; string "extern"; doc_typscm ts; doc_id id] + | VS_extern_spec(ts,id,s) -> + separate space [string "val"; string "extern"; doc_typscm ts; + doc_op equals (doc_id id) (dquotes (string s))] + +let doc_namescm (Name_sect_aux(ns,_)) = match ns with + | Name_sect_none -> empty + (* include leading space because the caller doesn't know if ns is + * empty, and trailing break already added by the following equals *) + | Name_sect_some s -> space ^^ brackets (doc_op equals (string "name") (dquotes (string s))) + +let rec doc_range (BF_aux(r,_)) = match r with + | BF_single i -> doc_int i + | BF_range(i1,i2) -> doc_op dotdot (doc_int i1) (doc_int i2) + | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) + +let doc_type_union (Tu_aux(typ_u,_)) = match typ_u with + | Tu_ty_id(typ,id) -> concat [doc_typ typ; space; doc_id id; semi] + | Tu_id id -> doc_id id ^^ semi + +let doc_typdef (TD_aux(td,_)) = match td with + | TD_abbrev(id,nm,typschm) -> + doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (doc_typscm typschm) + | TD_record(id,nm,typq,fs,_) -> + let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in + let fs_doc = group (separate_map (break 1) f_pp fs) in + doc_op equals + (concat [string "typedef"; space; doc_id id; doc_namescm nm]) + (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc)) + | TD_variant(id,nm,typq,ar,_) -> + let ar_doc = group (separate_map (break 1) doc_type_union ar) in + doc_op equals + (concat [string "typedef"; space; doc_id id; doc_namescm nm]) + (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc)) + | TD_enum(id,nm,enums,_) -> + let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in + doc_op equals + (concat [string "typedef"; space; doc_id id; doc_namescm nm]) + (string "enumerate" ^^ space ^^ braces enums_doc) + | TD_register(id,n1,n2,rs) -> + let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in + let doc_rids = group (separate_map (break 1) doc_rid rs) in + doc_op equals + (string "typedef" ^^ space ^^ doc_id id) + (separate space [ + string "register bits"; + brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2); + braces doc_rids; + ]) + +let doc_rec (Rec_aux(r,_)) = match r with + | Rec_nonrec -> empty + (* include trailing space because caller doesn't know if we return + * empty *) + | Rec_rec -> string "rec" ^^ space + +let doc_tannot_opt (Typ_annot_opt_aux(t,_)) = match t with + | Typ_annot_opt_some(tq,typ) -> doc_typquant tq (doc_typ typ) + +let doc_effects_opt (Effect_opt_aux(e,_)) = match e with + | Effect_opt_pure -> string "pure" + | Effect_opt_effect e -> doc_effects e + +let doc_funcl (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp exp)) + +let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) = + match fcls with + | [] -> failwith "FD_function with empty function list" + | _ -> + let sep = hardline ^^ string "and" ^^ space in + let clauses = separate_map sep doc_funcl fcls in + separate space [string "function"; + doc_rec r ^^ doc_tannot_opt typa; + string "effect"; doc_effects_opt efa; + clauses] + +let doc_dec (DEC_aux(DEC_reg(typ,id),_)) = + separate space [string "register"; doc_atomic_typ typ; doc_id id] + +let doc_scattered (SD_aux (sdef, _)) = match sdef with + | SD_scattered_function (r, typa, efa, id) -> + separate space [ + string "scattered function"; + doc_rec r ^^ doc_tannot_opt typa; + string "effect"; doc_effects_opt efa; + doc_id id] + | SD_scattered_variant (id, ns, tq) -> + doc_op equals + (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns) + (doc_typquant tq empty) + | SD_scattered_funcl funcl -> + string "function clause" ^^ space ^^ doc_funcl funcl + | SD_scattered_unioncl (id, tu) -> + separate space [string "union"; doc_id id; + string "member"; doc_type_union tu] + | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id + +let doc_def def = group (match def with + | DEF_default df -> doc_default df + | DEF_spec v_spec -> doc_spec v_spec + | DEF_type t_def -> doc_typdef t_def + | DEF_fundef f_def -> doc_fundef f_def + | DEF_val lbind -> doc_let lbind + | DEF_reg_dec dec -> doc_dec dec + | DEF_scattered sdef -> doc_scattered sdef + ) ^^ hardline + +let doc_defs (Defs(defs)) = + separate_map hardline doc_def defs + +let print ?(len=80) channel doc = ToChannel.pretty 1. len channel doc +let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc + +let pp_defs f d = print f (doc_defs d) +let pp_exp b e = to_buf b (doc_exp e) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index bf32a805..3fdf7841 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -1,10 +1,9 @@ open Ast open Type_internal -open Format -(* Prints on formatter the defs following source syntax *) -val pp_defs : Format.formatter -> tannot defs -> unit -val pp_exp : Format.formatter -> exp -> unit +(* Prints the defs following source syntax *) +val pp_defs : out_channel -> tannot defs -> unit +val pp_exp : Buffer.t -> exp -> unit (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit diff --git a/src/sail.ml b/src/sail.ml index b0957f91..a3a52c1b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -399,7 +399,7 @@ let main() = let chkedasts = (List.map (fun (f,(ast,kenv)) -> (f,check_ast ast kenv)) asts) in begin (if !(opt_print_verbose) - then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd chkedasts))) + then ((Pretty_print.pp_defs stdout) (snd (List.hd chkedasts))) else ()); (if !(opt_print_lem) then output "" Lem_ast_out chkedasts diff --git a/src/type_check.ml b/src/type_check.ml index 218efb84..5499c3e2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -547,7 +547,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (match (select_overload_variant d_env variants arg_t) with | NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) | Base((params,t),tag,cs,ef) -> - let _ = Printf.printf "Selected an overloaded function for %s, variant with function type %s\n" i (t_to_string t) in + let _ = Printf.eprintf "Selected an overloaded function for %s, variant with function type %s\n" i (t_to_string t) in (match t.t with | Tfn(arg,ret,ef') -> (match arg.t,arg_t.t with @@ -660,7 +660,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element" in - (*let _ = Printf.printf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*) + (*let _ = Printf.eprintf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*) let t',cs',e'=type_coerce (Expr l) d_env item_t (E_aux(E_vector_access(vec',i'),(l,Base(([],item_t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i) | E_vector_subrange(vec,i1,i2) -> @@ -907,12 +907,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | E_case(exp,pexps) -> (*let check_t = new_t() in*) let (e',t',_,cs,ef) = check_exp envs (new_t()) exp in - (*let _ = Printf.printf "Type of pattern after expression check %s\n" (t_to_string t') in*) + (*let _ = Printf.eprintf "Type of pattern after expression check %s\n" (t_to_string t') in*) let t' = match t'.t with | Tapp("register",[TA_typ t]) -> t | _ -> t' in - (*let _ = Printf.printf "Type of pattern after register check %s\n" (t_to_string t') in*) + (*let _ = Printf.eprintf "Type of pattern after register check %s\n" (t_to_string t') in*) let (pexps',t,cs',ef') = check_cases envs t' expect_t pexps in (E_aux(E_case(e',pexps'),(l,Base(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef') | E_let(lbind,body) -> @@ -968,7 +968,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan let t_actual = match t.t with | Tabbrev(i,t) -> t | _ -> t in - (*let _ = Printf.printf "Assigning to %s, t is %s\n" i (t_to_string t_actual) in*) + (*let _ = Printf.eprintf "Assigning to %s, t is %s\n" i (t_to_string t_actual) in*) (match t_actual.t,is_top with | Tapp("register",[TA_typ u]),_ -> let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in @@ -1304,15 +1304,15 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) -> let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in - (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*) + (*let _ = Printf.eprintf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*) let exp',_,_,cs_e,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) ret_t exp in - (*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) + (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) (*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*) let cs = [CondCons(Fun l,cs_p,cs_e)] in (FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in match (in_env,tannot) with | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') -> - (*let _ = Printf.printf "Function %s is in env\n" id in*) + (*let _ = Printf.eprintf "Function %s is in env\n" id in*) let u,constraints,eft = subst params u constraints eft in let t',cs = type_consistent (Specc l) d_env t u in let t_env = if is_rec then t_env else Envmap.remove t_env id in |