src/Tools/Metis/scripts/mlpp
author wenzelm
Mon, 25 Mar 2019 17:21:26 +0100
changeset 69981 3dced198b9ec
parent 39444 beabb8443ee4
child 72004 913162a47d9f
permissions -rwxr-xr-x
more strict AFP properties;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39443
diff changeset
     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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    21
if ($opt_c ne "mosml" && $opt_c ne "mlton" && $opt_c ne "polyml") {
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    75
        $text =~ s/Array\.copy/Array_copy/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    76
        $text =~ s/Array\.foldli/Array_foldli/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    77
        $text =~ s/Array\.foldri/Array_foldri/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    78
        $text =~ s/Array\.modifyi/Array_modifyi/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    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: 39350
diff 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: 39350
diff changeset
    82
        $text =~ s/String\.isSubstring/String_isSubstring/g;
39350
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    83
        $text =~ s/String\.isSuffix/String_isSuffix/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    86
        $text =~ s/Vector\.foldli/Vector_foldli/g;
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
    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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   102
    open my $INPUT, "$filename" or
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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
a47de56ae6c2 update scripts
blanchet
parents: 23442
diff changeset
   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