| author | blanchet | 
| Mon, 03 Feb 2014 11:58:38 +0100 | |
| changeset 55280 | f0187a12b8f2 | 
| parent 39444 | beabb8443ee4 | 
| child 72004 | 913162a47d9f | 
| permissions | -rwxr-xr-x | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 1 | #!/usr/bin/perl | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 2 | |
| 39444 | 3 | # Copyright (c) 2006 Joe Hurd, distributed under the BSD License | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 4 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 5 | use strict; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 6 | use warnings; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 7 | use Pod::Usage; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 8 | use Getopt::Std; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 9 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 10 | use vars qw($opt_h $opt_c $opt_r); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 11 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 12 | getopts('hc:r:');
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 13 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 14 | if ($opt_h or scalar @ARGV == 0) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 15 | {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 16 |     pod2usage({-exitval => 2,
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 17 | -verbose => 2}); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 18 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 19 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 20 | if (!$opt_c) { die "mlpp: you must specify the SML compiler\n"; }
 | 
| 39350 | 21 | if ($opt_c ne "mosml" && $opt_c ne "mlton" && $opt_c ne "polyml") {
 | 
| 22 |     die "mlpp: the SML compiler must be one of {mosml,mlton,polyml}.\n";
 | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 23 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 24 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 25 | # Autoflush STDIN | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 26 | $|++; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 27 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 28 | sub unquotify {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 29 |     if (scalar @_ == 0) { return; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 30 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 31 | my $pre = "["; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 32 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 33 |     for my $quote (@_) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 34 | my $nl = chomp $quote; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 35 | my @qs = split (/\^(\w+)/, $quote); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 36 | my @ps = (); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 37 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 38 |         for (my $s = 0; 0 < scalar @qs; $s = 1 - $s) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 39 | my $q = shift @qs; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 40 |             if ($s == 0) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 41 | $q =~ s/\\/\\\\/g; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 42 | $q =~ s/\"/\\\"/g; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 43 | push @ps, "QUOTE \"$q\"" unless ($q eq ""); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 44 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 45 |             elsif ($s == 1) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 46 | push @ps, "ANTIQUOTE $q"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 47 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 48 |             else { die; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 49 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 50 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 51 |         if (0 < $nl) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 52 |             if (0 < scalar @ps) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 53 | my $p = pop @ps; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 54 |                 if ($p =~ /QUOTE \"(.*)\"/) { push @ps, "QUOTE \"$1\\n\""; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 55 |                 else { push @ps, $p; push @ps, "QUOTE \"\\n\""; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 56 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 57 |             else { push @ps, "QUOTE \"\\n\""; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 58 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 59 |         else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 60 | (0 < scalar @ps) or die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 61 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 62 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 63 |         print STDOUT ($pre . join (", ", @ps));
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 64 | $pre = ",\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 65 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 66 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 67 | print STDOUT "]"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 68 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 69 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 70 | sub print_normal {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 71 | (scalar @_ == 1) or die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 72 | my $text = shift @_; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 73 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 74 |     if ($opt_c eq "mosml") {
 | 
| 39350 | 75 | $text =~ s/Array\.copy/Array_copy/g; | 
| 76 | $text =~ s/Array\.foldli/Array_foldli/g; | |
| 77 | $text =~ s/Array\.foldri/Array_foldri/g; | |
| 78 | $text =~ s/Array\.modifyi/Array_modifyi/g; | |
| 79 | $text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g; | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 80 | $text =~ s/PP\.ppstream/ppstream/g; | 
| 39443 
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
 blanchet parents: 
39350diff
changeset | 81 | $text =~ s/String\.concatWith/String_concatWith/g; | 
| 
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
 blanchet parents: 
39350diff
changeset | 82 | $text =~ s/String\.isSubstring/String_isSubstring/g; | 
| 39350 | 83 | $text =~ s/String\.isSuffix/String_isSuffix/g; | 
| 84 | $text =~ s/Substring\.full/Substring_full/g; | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 85 | $text =~ s/TextIO\.inputLine/TextIO_inputLine/g; | 
| 39350 | 86 | $text =~ s/Vector\.foldli/Vector_foldli/g; | 
| 87 | $text =~ s/Vector\.mapi/Vector_mapi/g; | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 88 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 89 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 90 | print STDOUT $text; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 91 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 92 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 93 | sub process_file {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 94 | (scalar @_ == 1) or die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 95 | my $filename = shift @_; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 96 | my $line_num = 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 97 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 98 |     if ($opt_c eq "mlton") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 99 | print STDOUT "(*#line 0.0 \"$filename\"*)\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 100 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 101 | |
| 39350 | 102 | open my $INPUT, "$filename" or | 
| 103 | die "mlpp: couldn't open $filename: $!\n"; | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 104 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 105 | my $state = "normal"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 106 | my $comment = 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 107 | my $revealed_comment = 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 108 | my @quotes = (); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 109 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 110 |     while (my $line = <$INPUT>) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 111 | (chomp ($line) == 1) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 112 | or warn "no terminating newline in $filename\nline = '$line'\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 113 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 114 |         while (1) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 115 |             if ($state eq "quote") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 116 |                 if ($line =~ /(.*?)\`(.*)$/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 117 | push @quotes, $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 118 | $line = $2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 119 | unquotify @quotes; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 120 | @quotes = (); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 121 | $state = "normal"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 122 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 123 |                 else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 124 | push @quotes, "$line\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 125 | last; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 126 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 127 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 128 |             elsif ($state eq "comment") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 129 |                 if ($line =~ /^(.*?)(\(\*|\*\))(.*)$/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 130 | my $leadup = $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 131 | my $pat = $2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 132 | $line = $3; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 133 | print STDOUT $leadup; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 134 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 135 |                     if ($pat eq "(*") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 136 | print STDOUT $pat; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 137 | ++$comment; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 138 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 139 |                     elsif ($pat eq "*)") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 140 | print STDOUT $pat; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 141 | --$comment; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 142 |                         if ($comment == 0) { $state = "normal"; }
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 143 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 144 |                     else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 145 | die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 146 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 147 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 148 |                 else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 149 | print STDOUT "$line\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 150 | last; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 151 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 152 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 153 |             elsif ($state eq "dquote") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 154 |                 if ($line =~ /^(.*?)\"(.*)$/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 155 | my $leadup = $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 156 | $line = $2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 157 | print STDOUT ($leadup . "\""); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 158 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 159 |                     if ($leadup =~ /(\\+)$/ && ((length $1) % 2 == 1)) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 160 | # This is an escaped double quote | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 161 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 162 |                     else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 163 | $state = "normal"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 164 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 165 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 166 |                 else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 167 | die "EOL inside \" quote\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 168 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 169 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 170 |             elsif ($state eq "normal") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 171 |                 if ($line =~ /^ *use *\"([^"]+)\" *; *$/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 172 | my $use_filename = $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 173 |                     if ($use_filename !~ /^\// && $filename =~ /^(.*)\//) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 174 | $use_filename = $1 . '/' . $use_filename; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 175 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 176 | process_file ($use_filename); | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 177 |                     if ($opt_c eq "mlton") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 178 | print STDOUT "(*#line $line_num.0 \"$filename\"*)\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 179 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 180 | print STDOUT "\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 181 | last; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 182 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 183 |                 elsif ($line =~ /^(.*?)(\`|\(\*|\*\)|\")(.*)$/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 184 | my $leadup = $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 185 | my $pat = $2; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 186 | $line = $3; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 187 | print_normal $leadup; | 
| 39350 | 188 | |
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 189 |                     if ($pat eq "`") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 190 | $state = "quote"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 191 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 192 |                     elsif ($pat eq "(*") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 193 | my $is_revealed = 0; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 194 |                         if ($line =~ /^([[:alnum:]_-]+)/) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 195 | my $rev = $1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 196 | if ($rev eq $opt_c || | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 197 |                                 ($opt_r && $rev =~ /^$opt_r$/)) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 198 | my $rev_len = length $rev; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 199 | $line = substr $line, $rev_len; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 200 | ++$revealed_comment; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 201 | $is_revealed = 1; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 202 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 203 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 204 |                         if (!$is_revealed) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 205 | print STDOUT $pat; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 206 | $state = "comment"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 207 | ++$comment; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 208 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 209 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 210 |                     elsif ($pat eq "*)") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 211 |                         if ($revealed_comment == 0) {
 | 
| 39350 | 212 | die "mlpp: too many comment closers.\n" | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 213 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 214 | --$revealed_comment; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 215 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 216 |                     elsif ($pat eq "\"") {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 217 | print STDOUT $pat; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 218 | $state = "dquote"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 219 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 220 |                     else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 221 | die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 222 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 223 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 224 |                 else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 225 | print_normal "$line\n"; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 226 | last; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 227 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 228 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 229 |             else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 230 | die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 231 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 232 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 233 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 234 | ++$line_num; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 235 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 236 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 237 |     if ($state eq "quote") {
 | 
| 39350 | 238 | die "mlpp: EOF inside \` quote\n"; | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 239 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 240 |     elsif ($state eq "dquote") {
 | 
| 39350 | 241 | die "mlpp: EOF inside \" quote\n"; | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 242 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 243 |     elsif ($state eq "comment") {
 | 
| 39350 | 244 | die "mlpp: EOF inside comment\n"; | 
| 23442 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 245 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 246 |     else {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 247 | ($state eq "normal") or die; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 248 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 249 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 250 | close $INPUT; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 251 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 252 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 253 | while (0 < scalar @ARGV) {
 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 254 | my $filename = shift @ARGV; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 255 | process_file $filename; | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 256 | } | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 257 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 258 | __END__ | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 259 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 260 | =pod | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 261 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 262 | =head1 NAME | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 263 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 264 | mlpp - preprocesses SML files for compilation | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 265 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 266 | =head1 SYNOPSIS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 267 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 268 | mlpp [-h] [-c compiler] [-r TAG] sml-file ... > preprocessed-sml-file | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 269 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 270 | =head1 ARGUMENTS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 271 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 272 | The recognized flags are described below: | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 273 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 274 | =over 2 | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 275 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 276 | =item B<-h> | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 277 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 278 | Produce this documentation. | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 279 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 280 | =item B<-c compiler> | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 281 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 282 | Select the SML compiler that will be used. | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 283 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 284 | =item B<-r TAG-REGEX> | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 285 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 286 | Remove all comment brackets tagged like this: (*TAG revealed-code *) | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 287 | where the TAG-REGEX matches the TAG. | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 288 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 289 | =back | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 290 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 291 | =head1 DESCRIPTION | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 292 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 293 | Concatenates the input list of SML source files into a single file | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 294 | ready to be compiled, by expanding quotations and antiquotations, and | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 295 | concatenating into a single file. | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 296 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 297 | =head1 BUGS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 298 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 299 | Waiting to rear their ugly heads. | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 300 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 301 | =head1 AUTHORS | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 302 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 303 | Joe Hurd <joe@gilith.com> | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 304 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 305 | =head1 SEE ALSO | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 306 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 307 | Perl(1). | 
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 308 | |
| 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 wenzelm parents: diff
changeset | 309 | =cut |