--- a/lib/Tools/fixclasimp Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: fix references to implicit claset and simpset
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .ML files, fixing references to"
- echo " implicit claset and simpset."
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
--- a/lib/Tools/fixdatatype Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: adapt theories and proof scripts to new datatype package
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files, adapting them to"
- echo " the new datatype package"
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && 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/fixdatatype.pl"
--- a/lib/Tools/fixdots Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: ensure that dots in formulas are followed by non-idents
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files, patching them to ensure that"
- echo " dots in formulas are followed by non-idents."
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && 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/fixdots.pl"
--- a/lib/Tools/fixgoal Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: replace goal(w) commands by implicit versions Goal(w)
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .ML files, replacing goal(w)"
- echo " commands by implicit versions Goal(w)"
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
--- a/lib/Tools/fixseq Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: fix references to obsolete Pure/Sequence structure
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .ML files, fixing references to"
- echo " the obsolete Pure/Sequence structure."
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
--- a/lib/scripts/fixclasimp.pl Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixclasimp.pl - fix references to implicit claset and simpset
-#
-
-sub fixclasimp {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/set_current_thy\s*"([^"]*)"/context $1.thy/sg;
-
- s/!\s*simpset/simpset()/sg;
- s/simpset\s*:=/simpset_ref() :=/sg;
- s/simpset_of\s*"([^"]*)"/simpset_of $1.thy/sg;
-
- s/!\s*claset/claset()/sg;
- s/claset\s*:=/claset_ref() :=/sg;
- s/claset_of\s*"([^"]*)"/claset_of $1.thy/sg;
-
-
- $result = $_;
-
- 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
-
-foreach $file (@ARGV) {
- eval { &fixclasimp($file); };
- if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixdatatype.pl Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixdatatype.pl - adapt theories and proof scripts to new datatype package
-#
-
-sub fixdatatype {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- ## convert split_type_case[_asm] to type.split[_asm]
- s/([^"])\bsplit_([\w]+)_case\b/$1$2.split/sg;
- s/([^"])\bsplit_([\w]+)_case_asm\b/$1$2.split_asm/sg;
-
- ## delete function name and type after "primrec"
- s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg;
-
- ## replace specific induct_tac by generic induct_tac
- s/[\w\.]+\.induct_tac/induct_tac/sg;
-
- ## replace res_inst_tac ... natE by case_tac
- s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
-
- $result = $_;
-
- 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
-
-foreach $file (@ARGV) {
- eval { &fixdatatype($file); };
- if ($@) { print STDERR "*** fixdatatype $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixdots.pl Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixdots.pl - ensure that dots in formulas are followed by non-idents
-#
-# tries to be smart; may produce garbage if nested comments and
-# solitary quotes (") are intermixed badly;
-#
-
-sub fixdots {
- my ($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!
- s/([a-zA-Z][a-zA-Z0-9_']*)\.([a-zA-Z])/$1\. $2/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
-
-foreach $file (@ARGV) {
- eval { &fixdots($file); };
- if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixgoal.pl Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixgoal.pl - replace goal(w) commands by implicit versions Goal(w)
-#
-
-sub fixgoal {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- ($path, $thy, $ext) = ($file =~ m,^(.*/)?(\w+)(\.\w+)?$,);
-
- $_ = $text;
-
- s/^[ \t]*goalw\b\s*\bthy\b/Goalw/mg;
- s/^[ \t]*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
- s/^[ \t]*goal\b\s*\bthy\b/Goal/mg;
- s/^[ \t]*goal\b\s*\b$thy\.thy\b/Goal/mg;
-
-
- $result = $_;
-
- 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
-
-foreach $file (@ARGV) {
- eval { &fixgoal($file); };
- if ($@) { print STDERR "*** fixgoal $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixseq.pl Mon Aug 01 11:39:33 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixseq.pl - fix references to obsolete Pure/Sequence structure
-#
-
-sub fixseq {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
-
- s/Sequence\.tl/Seq.tl/sg;
- s/Sequence\.single/Seq.single/sg;
- s/Sequence\.seqof/Seq.make/sg;
- s/Sequence\.seq/Seq.seq/sg;
- s/Sequence\.s_of_list/Seq.of_list/sg;
- s/Sequence\.pull/Seq.pull/sg;
- s/Sequence\.prints/Seq.print/sg;
- s/Sequence\.null/Seq.empty/sg;
- s/Sequence\.maps/Seq.map/sg;
- s/Sequence\.mapp/Seq.mapp/sg;
- s/Sequence\.list_of_s/Seq.list_of/sg;
- s/Sequence\.its_right/Seq.it_right/sg;
- s/Sequence\.interleave/Seq.interleave/sg;
- s/Sequence\.hd/Seq.hd/sg;
- s/Sequence\.flats/Seq.flat/sg;
- s/Sequence\.filters/Seq.filter/sg;
- s/Sequence\.cons/Seq.cons/sg;
- s/Sequence\.chop/Seq.chop/sg;
- s/Sequence\.append/Seq.append/sg;
-
-
- $result = $_;
-
- 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
-
-foreach $file (@ARGV) {
- eval { &fixseq($file); };
- if ($@) { print STDERR "*** fixseq $file: ", $@, "\n"; }
-}