1.1 --- a/lib/scripts/convert.pl	Thu Feb 01 17:03:19 2001 +0100
     1.2 +++ b/lib/scripts/convert.pl	Thu Feb 01 18:13:06 2001 +0100
     1.3 @@ -17,6 +17,28 @@
     1.4    $s;
     1.5  }
     1.6  
     1.7 +sub subst_RS {
     1.8 +  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
     1.9 +  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
    1.10 +  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
    1.11 +  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
    1.12 +  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
    1.13 +  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
    1.14 +  s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
    1.15 +  s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
    1.16 +}
    1.17 +
    1.18 +sub decl {
    1.19 +  my $s = shift;
    1.20 +  my $a = shift;
    1.21 +  $_ = $s;
    1.22 +  subst_RS();
    1.23 +  s/, */ [$a] /g;
    1.24 +  s/$/ [$a]/;
    1.25 +  s/\] *\[/, /g;
    1.26 +  "declare $_";
    1.27 +}
    1.28 +
    1.29  sub process_tac {
    1.30    my $lead = shift;
    1.31    my $t = shift;
    1.32 @@ -97,14 +119,7 @@
    1.33  
    1.34    s/THEN /, /g;
    1.35    s/ORELSE/|/g;
    1.36 -  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
    1.37 -  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
    1.38 -  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
    1.39 -  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
    1.40 -  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
    1.41 -  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
    1.42 -  s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
    1.43 -  s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
    1.44 +  subst_RS();
    1.45  
    1.46    s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
    1.47    s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
    1.48 @@ -221,17 +236,17 @@
    1.49    s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
    1.50    s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
    1.51                               # remove outermost parentheses if around atoms
    1.52 -  s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
    1.53 -  s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
    1.54 -  s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
    1.55 -  s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
    1.56 -  s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
    1.57 -  s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
    1.58 -  s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
    1.59 -  s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
    1.60 -  s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
    1.61 -  s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
    1.62 -  s/^AddIffs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
    1.63 +  s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"simp")/seg;
    1.64 +  s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"simp del")/seg;
    1.65 +  s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"split")/seg;
    1.66 +  s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"split del")/seg;
    1.67 +  s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"intro")/seg;
    1.68 +  s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"intro!")/seg;
    1.69 +  s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"elim")/seg;
    1.70 +  s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"elim!")/seg;
    1.71 +  s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"dest")/seg;
    1.72 +  s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"dest!")/seg;
    1.73 +  s/^AddIffs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"iff")/seg;
    1.74    print "$_$tail";
    1.75    if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
    1.76  }