#!/usr/bin/env perl
use strict;
use warnings;
use Getopt::Long qw(GetOptions);

my $input  = 'library/naprochelibrary.tex';
my $output = 'informath/munkres0.dkgf';
my $help   = 0;

GetOptions(
    'input=s'  => \$input,
    'output=s' => \$output,
    'help'     => \$help,
) or usage();

usage() if $help;

my $tex = slurp($input);
$tex = strip_comments($tex);

my @entries;
my @warnings;
my %seen_label;
my $definition_count = 0;

while ($tex =~ /\\begin\{definition\}(.*?)\\end\{definition\}/sg) {
    my $body = $1;
    ++$definition_count;

    my ($label) = $body =~ /\\label\{([^{}]+)\}/;
    if (!defined $label) {
        push @warnings, "definition $definition_count has no label";
        next;
    }
    if ($seen_label{$label}++) {
        push @warnings, "duplicate label '$label'";
        next;
    }

    $body =~ s/^.*?\\label\{[^{}]+\}//s;
    $body = normalize_space($body);

    my $pattern = extract_pattern($label, $body);
    if (!defined $pattern || $pattern eq '') {
        push @warnings, "could not extract a pattern for '$label'";
        next;
    }

    push @entries, "$label : " . quote_pattern($pattern);
}

if (@warnings) {
    warn "warning: $_\n" for @warnings;
    die "Aborting: extracted " . scalar(@entries) . " entries from $definition_count definitions.\n";
}

open my $out_fh, '>', $output or die "Cannot write $output: $!";
print {$out_fh} join("\n", @entries), "\n";
close $out_fh or die "Cannot close $output: $!";

print STDERR "Wrote " . scalar(@entries) . " entries to $output from $definition_count definitions.\n";

sub usage {
    die "Usage: $0 [--input FILE] [--output FILE]\n";
}

sub slurp {
    my ($path) = @_;
    open my $fh, '<', $path or die "Cannot read $path: $!";
    local $/;
    my $content = <$fh>;
    close $fh or die "Cannot close $path: $!";
    return $content;
}

sub strip_comments {
    my ($text) = @_;
    $text =~ s/(^|[^\\])%[^\n]*/$1/gm;
    return $text;
}

sub normalize_space {
    my ($text) = @_;
    $text =~ s/\s+/ /g;
    $text =~ s/^\s+//;
    $text =~ s/\s+$//;
    return $text;
}

sub extract_pattern {
    my ($label, $body) = @_;

    if (my ($before_iff) = split_before_iff($body)) {
        my $clause = last_sentence_clause($before_iff);
        return pattern_from_iff_clause($label, $clause);
    }

    if (my $lhs = first_equation_lhs($body)) {
        return symbolic_pattern($label, $lhs);
    }

    return undef;
}

sub split_before_iff {
    my ($text) = @_;
    my @separators = (
        qr/\\iff\b/,
        qr/\bif\s+and\s+only\s+if\b/i,
        qr/\biff\b/i,
        qr/\bdenote\b/i,
        qr/\bstand\s+for\b/i,
    );

    my ($best_start, $best_len);
    for my $re (@separators) {
        if ($text =~ /$re/) {
            if (!defined $best_start || $-[0] < $best_start) {
                $best_start = $-[0];
                $best_len   = $+[0] - $-[0];
            }
        }
    }

    return if !defined $best_start;
    return substr($text, 0, $best_start);
}

sub last_sentence_clause {
    my ($text) = @_;
    $text =~ s/\s+$//;

    my $last_cut;
    while ($text =~ /\.\s*/g) {
        $last_cut = $+[0];
    }

    my $clause = defined $last_cut ? substr($text, $last_cut) : $text;
    return normalize_space($clause);
}

sub pattern_from_iff_clause {
    my ($label, $clause) = @_;
    my $slots = new_slot_state();

    if ($clause =~ /^\s*\$([^\$]+)\$\s*$/s) {
        return symbolic_pattern($label, $1);
    }

    if ($clause =~ /^\s*((?:an?|the)\s+[\w'-]+(?:\s+[\w'-]+)*?)\s+(\$[^\$]+\$)\s+is\s+(.+)$/is) {
        return clean_pattern(render_with_slots($2, $slots) . ' is ' . render_with_slots($3, $slots));
    }

    if ($clause =~ /^\s*(\$[^\$]+\$)\s+is\s+(a|an)\s+(.+)$/is) {
        return clean_pattern(render_with_slots($1, $slots) . ' is ' . lc($2) . ' ' . render_with_slots($3, $slots));
    }

    if ($clause =~ /^\s*(\$[^\$]+\$)\s+is\s+(.+)$/is) {
        return clean_pattern(render_with_slots($1, $slots) . ' is ' . render_with_slots($2, $slots));
    }

    if ($clause =~ /^\s*(\$[^\$]+\$)\s+(.+)$/is) {
        return clean_pattern(render_with_slots($1, $slots) . ' ' . render_with_slots($2, $slots));
    }

    return undef;
}

sub first_equation_lhs {
    my ($body) = @_;

    while ($body =~ /\$([^\$]*)\$/sg) {
        my $math = $1;
        if ($math =~ /^(.*?)=/s) {
            my $lhs = normalize_space($1);
            return $lhs if $lhs ne '';
        }
    }

    return undef;
}

sub symbolic_pattern {
    my ($label, $math) = @_;
    $math = normalize_space($math);

    my @args = macro_args($math);
    my $base = label_words($label);
    return $base if !@args;

    my $slots = new_slot_state();
    my @slot_names = map { slot_for_math($slots, $_) } @args;
    return clean_pattern($base . ' of ' . join(' and ', @slot_names));
}

sub macro_args {
    my ($math) = @_;

    return if $math !~ /^\s*\\[A-Za-z]+\b/;

    my @args;
    while ($math =~ /\{([^{}]*)\}/g) {
        push @args, normalize_space($1);
    }
    return @args;
}

sub label_words {
    my ($label) = @_;
    my @parts = grep { $_ ne '' } split /_+/, lc($label);
    pop @parts if @parts && $parts[-1] eq 'pred';
    return join(' ', @parts);
}

sub render_with_slots {
    my ($text, $slots) = @_;
    my $out = '';
    my $pos = 0;

    while ($text =~ /\$([^\$]+)\$/sg) {
        $out .= lc(substr($text, $pos, $-[0] - $pos));
        $out .= slot_for_math($slots, $1);
        $pos = $+[0];
    }

    $out .= lc(substr($text, $pos));
    return clean_pattern($out);
}

sub clean_pattern {
    my ($text) = @_;
    $text =~ s/\\([a-z]+)\{\}/$1/g;
    $text =~ s/\\([a-z]+)/$1/g;
    $text =~ s/[{}]//g;
    $text =~ s/\s+/ /g;
    $text =~ s/\s+-/-/g;
    $text =~ s/-\s+/-/g;
    $text =~ s/\s+([,.;:!?])/$1/g;
    $text =~ s/^\s+//;
    $text =~ s/\s+$//;
    return $text;
}

sub new_slot_state {
    return { names => {}, next => 0 };
}

sub slot_for_math {
    my ($state, $math) = @_;
    my $key = normalize_math_key($math);
    return $state->{names}{$key} if exists $state->{names}{$key};

    my $slot = slot_name($state->{next});
    ++$state->{next};
    $state->{names}{$key} = $slot;
    return $slot;
}

sub normalize_math_key {
    my ($math) = @_;
    $math = normalize_space($math);
    $math =~ s/\s+//g;
    return $math;
}

sub slot_name {
    my ($index) = @_;
    my @preferred = qw(X Y Z U V W A B C D E F G H I J K L M N O P Q R S T);
    return $preferred[$index] if $index < @preferred;
    return 'X' . ($index - @preferred + 1);
}

sub quote_pattern {
    my ($pattern) = @_;
    $pattern =~ s/\\/\\\\/g;
    $pattern =~ s/"/\\"/g;
    return '"' . $pattern . '"';
}