annotate tools/bsd_license.ml @ 563:af97676583f3

Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -0500
parents 306539f29eea
children 3fc43e261f67
rev   line source
amp@546 1 let read_line () =
amp@546 2 try
amp@546 3 Some (read_line ())
amp@546 4 with End_of_file -> None
amp@546 5
amp@546 6 let print_bsd_licence () = begin
amp@546 7 print_endline " * Three-clause BSD Licence";
amp@546 8 print_endline " *";
amp@546 9 print_endline " * All rights reserved.";
amp@546 10 print_endline " *";
amp@546 11 print_endline " * Redistribution and use in source and binary forms, with or without";
amp@546 12 print_endline " * modification, are permitted provided that the following conditions are met:";
amp@546 13 print_endline " *";
amp@546 14 print_endline " * - Redistributions of source code must retain the above copyright notice,";
amp@546 15 print_endline " * this list of conditions and the following disclaimer.";
amp@546 16 print_endline " * - Redistributions in binary form must reproduce the above copyright notice,";
amp@546 17 print_endline " * this list of conditions and the following disclaimer in the documentation";
amp@546 18 print_endline " * and/or other materials provided with the distribution.";
amp@546 19 print_endline " * - The names of contributors may not be used to endorse or promote products";
amp@546 20 print_endline " * derived from this software without specific prior written permission.";
amp@546 21 print_endline " *";
amp@546 22 print_endline " * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS \"AS IS\"";
amp@546 23 print_endline " * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE";
amp@546 24 print_endline " * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE";
amp@546 25 print_endline " * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE";
amp@546 26 print_endline " * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR ";
amp@546 27 print_endline " * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF";
amp@546 28 print_endline " * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS";
amp@546 29 print_endline " * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN";
amp@546 30 print_endline " * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)";
amp@546 31 print_endline " * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE";
amp@546 32 print_endline " * POSSIBILITY OF SUCH DAMAGE."
amp@546 33 end
amp@546 34
amp@546 35 let rec initial () =
amp@546 36 match read_line () with
amp@546 37 | None -> ()
amp@546 38 | Some line ->
amp@546 39 let trimmed = String.trim line in
amp@546 40 if String.length trimmed >= 12 && String.sub trimmed 0 12 = "(* Copyright" then begin
amp@546 41 print_endline line;
amp@546 42 copyright_block ()
amp@546 43 end else
amp@546 44 print_endline line;
amp@546 45 initial ()
amp@546 46
amp@546 47 and copyright_block () =
amp@546 48 match read_line () with
amp@546 49 | None -> ()
amp@546 50 | Some line ->
amp@546 51 let trimmed = String.trim line in
amp@546 52 if String.length trimmed >= 2 && String.sub trimmed 0 2 = "*)" then begin
amp@546 53 print_endline line;
amp@546 54 initial ()
amp@546 55 end else if String.length trimmed >= 31 && String.sub trimmed 0 31 = "* This work is licensed under a" then begin
amp@546 56 print_endline line;
amp@546 57 print_bsd_licence ();
amp@546 58 drop_to_end_comment ()
amp@546 59 end else
amp@546 60 print_endline line;
amp@546 61 copyright_block ()
amp@546 62
amp@546 63 and drop_to_end_comment () =
amp@546 64 match read_line () with
amp@546 65 | None -> ()
amp@546 66 | Some line ->
amp@546 67 let trimmed = String.trim line in
amp@546 68 if String.length trimmed >= 2 && String.sub trimmed 0 2 = "*)" then begin
amp@546 69 print_endline line;
amp@546 70 initial ()
amp@546 71 end else
amp@546 72 drop_to_end_comment ()
amp@546 73
amp@546 74 let () = initial ()