# HG changeset patch # User oheimb # Date 1017822073 -7200 # Node ID 70704dd48bd54afa16b7d3a6ae08f2ee65ffece3 # Parent d3e1d554cd6dbd0d1787149c23d726db4c3d0201 bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc. diff -r d3e1d554cd6d -r 70704dd48bd5 lib/scripts/convert.pl --- a/lib/scripts/convert.pl Tue Apr 02 14:28:28 2002 +0200 +++ b/lib/scripts/convert.pl Wed Apr 03 10:21:13 2002 +0200 @@ -77,23 +77,28 @@ s/Safe_tac/safe/g; s/Clarify_tac 1/clarify/g; - s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g; - s/^blast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e; - s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g; - s/^fast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e; - s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g; - s/^slow_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e; - s/best_tac \(claset\(\) (.*?)\) 1/best $1/g; - s/^best_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e; - s/safe_tac \(claset\(\) (.*?)\)/safe $1/g; - s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g; + s/ALLGOALS \(blast_tac \(claset \(\) (.*?)\) \)$/(blast $1)+/g; + s/blast_tac \(claset \(\) (.*?)\) 1/blast $1/g; + s/^blast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e; + s/ALLGOALS \(fast_tac \(claset \(\) (.*?)\) \)$/(fast $1)+/g; + s/fast_tac \(claset \(\) (.*?)\) 1/fast $1/g; + s/^fast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e; + s/slow_tac \(claset \(\) (.*?)\) 1/slow $1/g; + s/^slow_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e; + s/ALLGOALS \(best_tac \(claset \(\) (.*?)\) \)$/(best $1)+/g; + s/best_tac \(claset \(\) (.*?)\) 1/best $1/g; + s/^best_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e; + s/safe_tac \(claset \(\) (.*?)\)/safe $1/g; + s/clarify_tac \(claset \(\) (.*?)\) 1/clarify $1/g; s/Auto_tac/auto/g; + s/ALLGOALS Force_tac/force+/g; s/Force_tac 1/force/g; s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e; s/Clarsimp_tac 1/clarsimp/g; s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g; + s/ALLGOALS \(force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) \)$/(force $1 $2)+/g; s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g; s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e; s/clarsimp_tac \(claset \(*\) (.*?), *simpset \(\) (.*?)\) 1/clarsimp $1 $2/g; @@ -268,7 +273,9 @@ s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se; s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se; s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/; - # remove outermost parentheses if around atoms + # remove outermost parentheses if around atoms + s/^(apply +)\(\((.*?)\)([+*]?)\)\s*$/$1($2)$3/; + # remove outermost parentheses if around parentheses s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg; s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg; s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg; diff -r d3e1d554cd6d -r 70704dd48bd5 lib/scripts/feeder --- a/lib/scripts/feeder Tue Apr 02 14:28:28 2002 +0200 +++ b/lib/scripts/feeder Wed Apr 03 10:21:13 2002 +0200 @@ -77,6 +77,6 @@ ## main #set by configure -AUTO_PERL=perl +AUTO_PERL=/usr/bin/perl exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"