# HG changeset patch
# User wenzelm
# Date 932731550 -7200
# Node ID aa1d0d620031367a7f959157e1e3230ead28e509
# Parent  b053e0ab9f607e93b317e7491a38559c56b757b5
fix occurences of numerals in HOL/ZF terms;

diff -r b053e0ab9f60 -r aa1d0d620031 lib/Tools/fixnumerals
--- /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
diff -r b053e0ab9f60 -r aa1d0d620031 lib/scripts/fixnumerals.pl
--- /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"; }
+}