#!/usr/bin/perl -w
# (C) 2007 Thomas Bleher <ThomasBleher@gmx.de>
# Released under the same license as Isabelle (ie BSD)
#
# Parse theories and create LaTeX commands from all definitions and lemmata.

sub remove_ {
	# only chars are allowed in latex command names, so we substitute numbers and single quotes;
	# all other chars are simply removed, but the char following a removed char is uppercased
	#
	# Example: my_lemma1 becomes myLemmaOne
	my (%replacements) = (0 => "Zero", 1 => "One", 2 => "Two", 3 => "Three", 4 => "Four", 5 => "Five", 6 => "Six", 7 => "Seven", 8 => "Eight", 9 => "Nine", "'" => "SQuote");

	my $text = shift;
	$text =~ s/\Q$_\E/$replacements{$_}_/g for (keys %replacements);
	my @parts = split /[^a-zA-Z0-9]/, $text;
	return (shift @parts).(join '', map {ucfirst} @parts);
}

my %thms;
sub print_format {
	my ($thyname, $thmname, $locale) = @_;
	if ($locale ne '') {
		$locale =~ /\(in (\w+)\)/ or die "Locale-Error: found '$locale'";
		$thmname = "$1.$thmname";
	}
	if ($thms{$thmname}++) {
		$thmname = "$thyname.$thmname";
		die "Multiple theorems named $thmname" if $thms{$thmname}++;
	}
	my $latexname = remove_ $thmname;
	print "text_raw{*\n\\newcommand{\\${latexname}Inline}{\@{thm $thmname [no_vars]}}\n*}\n";
	print "text_raw{*\n\\newcommand{\\$latexname}{\n\@{thm [display] $thmname [no_vars]}\n}\n*}\n\n";
}

my @files = @ARGV;

my (%done) = map {$_ => 1} @files;
while (@files) {
	my $file = shift @files;
	next if {"Main.thy"=>1,"LaTeXsugar.thy"=>1}->{$file}; # these are the base files, don't process them
	open FILE, "<", $file or do { warn "Could not open file '$file'!"; next; };
	$state = 0;
	print "\n\n(* Reading file $file... *)\n\n";
	local $/ = undef;
	my $data = <FILE>;
	$data =~ s/\(\*.*?\*\)//gs; # remove comments
	my $thyname = ($data =~ /^\s*theory\s+(\w+)(?:\s|$)/ms)[0];
	for (split /\n/, $data) { # crudely parse the theory
		if (/(?:theory\s+\w+\s+|^)imports\s+(.+?)(?:\s+begin|$)/) {
			($imports = $1) =~ s/"//g;
			for (map { $_.".thy" } split /\s+/, $imports) {
				push @files, $_ unless $done{$_};
				$done{$_} = 1;
			}
		}

		# lemmas and theorems can be parsed without much state info
		/^(?:lemma|theorem)\s+(\(in \w+\)\s+|)("?)([\w']+)\2(?:\s+\[[a-z,!_ ]+\])?:/ and print_format($thyname, $3, $1);
		# locale parsing is still *very* rudimentary...
		/^locale\s+("?)(\w+)\1\s*=/ and print_format($thyname, $2."_def",'');

		# constdefs, by contrast, need some more state info:
		/^(?:constdefs)(\s+|$)/ and $state = 1;
		/^(?:defs)(\s+|$)/      and $state = 2;
		/^(?:axioms)(\s+|$)/    and $state = 3;

		/^(?:consts|record|lemma|theorem|primrec|declare|recdef|datatype|text|locale)(\s+|$)/ and $state = 0;

		$state == 0 and /^\s*inductive\s+"?(\w+)\s/ and print_format($thyname, $1.".intros",'');
		$state == 1 and /("?)([\w']+)\1\s+::\s/ and print_format($thyname, $2."_def",'');
		$state  > 1 and /("?)([\w']+)\1\s*:\s+"/ and print_format($thyname, $2,'');

		# still missing: named primrec definitions, locale assumes, lots of more esoteric stuff
		
	}
	close FILE;
}