--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/fixnumerals Fri Jul 23 14:05:50 1999 +0200
@@ -0,0 +1,63 @@
+#!/bin/bash
+#
+# $Id$
+#
+# DESCRIPTION: fix occurences of numerals in HOL/ZF terms
+
+
+## diagnostics
+
+PRG=$(basename $0)
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [FILES|DIRS...]"
+ echo
+ echo " Options are:"
+ echo " -c add '(_::int)' type constraints (for HOL only)"
+ echo
+ echo " Recursively find .thy/.ML files, fixing occurences of"
+ echo " HOL/ZF numerals: #42 becomes 42, #-42 becomes ~42".
+ echo
+ echo " Renames old versions of FILES by appending \"~~\"."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+# options
+
+CONSTRAINTS=false
+
+while getopts "c" OPT
+do
+ case "$OPT" in
+ c)
+ CONSTRAINTS=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -eq 0 ] && usage
+
+SPECS="$@"; shift $#
+
+
+## main
+
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
+ xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixnumerals.pl $CONSTRAINTS
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/fixnumerals.pl Fri Jul 23 14:05:50 1999 +0200
@@ -0,0 +1,64 @@
+#
+# $Id$
+#
+# fixnumerals.pl - fix occurences of numerals in HOL/ZF terms
+#
+# tries to be smart; may produce garbage if nested comments and
+# solitary quotes (") are intermixed badly;
+#
+
+sub fixdots {
+ my ($constr, $file) = @_;
+
+ open (FILE, $file) || die $!;
+ undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
+ close FILE || die $!;
+
+
+ $result = "";
+ $rest = $text;
+
+ while (1) {
+ $_ = $rest;
+ ($pre, $str, $rest) =
+ m/^((?: \(\*.*?\*\) | [^"] )*) # pre: text or (non-nested!) comments
+ "((?: [^"\\] | \\\S | \\\s+\\ )*)" # quoted string
+ (.*)$/sx; # rest of file
+ if ($str) {
+ $_ = $str;
+ if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) { # exclude filenames!
+ if ($constr eq "true") {
+ s/#([0-9]+)/($1::int)/sg;
+ s/#-([0-9]+)/(~$1::int)/sg;
+ } else {
+ s/#([0-9]+)/$1/sg;
+ s/#-([0-9]+)/~$1/sg;
+ }
+ }
+ $result = $result . $pre . '"' . $_ . '"';
+ } else {
+ $result = $result . $_;
+ last;
+ }
+ }
+
+ if ($text ne $result) {
+ print STDERR "fixing $file\n";
+ if (! -f "$file~~") {
+ rename $file, "$file~~" || die $!;
+ }
+ open (FILE, "> $file") || die $!;
+ print FILE $result;
+ close FILE || die $!;
+ }
+}
+
+
+## main
+
+$constr = shift;
+
+foreach $file (@ARGV) {
+ eval { &fixdots($constr, $file); };
+ if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
+}