#
# Preprocesses a text and it changes
# \begin{deputycode}[comma_separated_options]
# ...
# \end{deputycode}
#
# The following options are supported:
#   local   - the code is generated inside a "main" function. By default the
#             code goes at global scope
#   fails   - the processing is expected to fail
#   norun   - show just the code, not the Deputy output
#
# into the verbatim environment and add the option to see the Deputy output for
# it.
# Invoke: deputycode.pl in.tex out.tex
use strict;
use Data::Dumper;
use File::Copy;

open(IN, "<$ARGV[0]") || (&help(), die "Cannot open file \"$ARGV[0]\"");
open(OUT, ">$ARGV[1]") || (&help(), die "Cannot open file \"$ARGV[1]\"");
sub help {
    print "Invoke deputycode.pl in.tex out.tex";
}

my $doexamples = ! defined($ENV{'NO_EXAMPLES'});

my $testnr = 1;
my $tmpdir  = "deputycode.tmp";
my $htmloutdir = "examples";
my $outdir  = "html/deputy/$htmloutdir";

my @ccured = ('perl', '../bin/deputy', '--deputyopt=3', '--noPrintLn', 
              '--save-temps');

my $preambleLocal = <<EOF;
int main(void) {
\# 1
EOF

my $preambleGlobal = <<EOF;
EOF

my $postambleGlobal = "";
my $postambleLocal = <<EOF;
}
EOF

if(! -d $tmpdir) {
    mkdir $tmpdir || die "Cannot make $tmpdir\n";

}
my $incode = 0;
my @opt; # Array of , separated options passed to ccuredcode environment


my $lineno = 0;
while(<IN>) {
    # Strip extra \n\r at the end
    if($_ =~ m|^([^\n\r]*)[\n\r]*|) {
        $_ = "$1\n"; # And add one
    }
    $lineno ++;
    if(! $incode && $_ =~ m|^\\begin{deputycode}(\[(.*)\])?|) {
        @opt = split(/[ ,]/, $2); # The options
        $incode = 1;
        print STDERR "\n***Found Deputy code (ex$testnr) at line $lineno, with options=",
                     join(',',@opt), "\n";
        if(! grep(/norun/, @opt)) {
            open(TSTSRC, ">$tmpdir/ex$testnr.c") 
                || die "Cannot create source $testnr";
            if(grep(/local/, @opt)) {
                print TSTSRC $preambleLocal;
            } else {
                print TSTSRC $preambleGlobal;
            }
        }
        print OUT "\\begin{code}\n";
        next;
    }
    if($incode && $_ =~ m|^\\end{deputycode}|) {
        $incode = 0;
        print OUT "\n\\end{verbatim}\\end{code}\n";
        if(! grep(/norun/, @opt)) {
            if(grep(/local/, @opt)) {
                print TSTSRC $postambleLocal;
            } else {
                print TSTSRC $postambleGlobal;
            }
            close(TSTSRC);
            if($doexamples) { 
                print OUT "The \\ahref{$htmloutdir/ex${testnr}.deputy.txt}{Deputy output} for this code fragment\n";

                # Now run ccured. Pass all the options that start with --
                my @ccuredOpt = grep(/^--/, @opt);
                my $fails = 
                    0 !=
                    system(@ccured, @ccuredOpt,
                           '-c', "$tmpdir/ex$testnr.c",
                           '-o', "$tmpdir/ex$testnr.o",
                           "--save-temps=$tmpdir");
                my $shouldfail = 0 != grep(/fails/, @opt);
                if($fails != $shouldfail) {
                    die "Error running Deputy for $tmpdir/ex$testnr.c (fails=$fails, shouldfail=$shouldfail)";
                }
                # Now copy the CCured file
                my $cilfile = "$tmpdir/ex$testnr.cil.c";
                my $exfile = "$outdir/ex$testnr.deputy.txt";
                if(! File::Copy::copy($cilfile, $exfile)) {
                    die "Cannot copy $cilfile to $exfile";
                }
                # And copy the browser directory 
                # system("cp -r $tmpdir/ex$testnr.browser $outdir");
            }
        } else {
            print OUT "(Code generation was turned off for this document)\n";
        }
        $testnr ++;
        next;
    }
    if($incode) {
        print TSTSRC $_;
    } 
    print OUT $_;
}


