# HG changeset patch # User wenzelm # Date 1122900021 -7200 # Node ID 40759607c5905155ff17722085a2d3aacaa2db3f # Parent 37e34f315057cada50b2f66ece7b87976cacf35e obsolete; diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixclasimp --- 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" diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixdatatype --- 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" diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixdots --- 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" diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixgoal --- 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" diff -r 37e34f315057 -r 40759607c590 lib/Tools/fixseq --- 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" diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixclasimp.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 = ; $/ = "\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"; } -} diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixdatatype.pl --- 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 = ; $/ = "\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"; } -} diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixdots.pl --- 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 = ; $/ = "\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"; } -} diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixgoal.pl --- 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 = ; $/ = "\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"; } -} diff -r 37e34f315057 -r 40759607c590 lib/scripts/fixseq.pl --- 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 = ; $/ = "\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"; } -}