lib/scripts/convert.pl
changeset 13076 70704dd48bd5
parent 11329 ad8061b2da6c
child 14362 b378b6faf4a7
equal deleted inserted replaced
13075:d3e1d554cd6d 13076:70704dd48bd5
    75   s/Best_tac 1/best/g;
    75   s/Best_tac 1/best/g;
    76   s/^Best_tac (\d+)/{$prefer="prefer $1 "; "best"}/e;
    76   s/^Best_tac (\d+)/{$prefer="prefer $1 "; "best"}/e;
    77   s/Safe_tac/safe/g;
    77   s/Safe_tac/safe/g;
    78   s/Clarify_tac 1/clarify/g;
    78   s/Clarify_tac 1/clarify/g;
    79 
    79 
    80   s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g;
    80   s/ALLGOALS \(blast_tac \(claset \(\) (.*?)\) \)$/(blast $1)+/g;
    81   s/^blast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e;
    81   s/blast_tac \(claset \(\) (.*?)\) 1/blast $1/g;
    82   s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g;
    82   s/^blast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e;
    83   s/^fast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e;
    83   s/ALLGOALS \(fast_tac \(claset \(\) (.*?)\) \)$/(fast $1)+/g;
    84   s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g;
    84   s/fast_tac \(claset \(\) (.*?)\) 1/fast $1/g;
    85   s/^slow_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e;
    85   s/^fast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e;
    86   s/best_tac \(claset\(\) (.*?)\) 1/best $1/g;
    86   s/slow_tac \(claset \(\) (.*?)\) 1/slow $1/g;
    87   s/^best_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e;
    87   s/^slow_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e;
    88   s/safe_tac \(claset\(\) (.*?)\)/safe $1/g;
    88   s/ALLGOALS \(best_tac \(claset \(\) (.*?)\) \)$/(best $1)+/g;
    89   s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g;
    89   s/best_tac \(claset \(\) (.*?)\) 1/best $1/g;
       
    90   s/^best_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e;
       
    91   s/safe_tac \(claset \(\) (.*?)\)/safe $1/g;
       
    92   s/clarify_tac \(claset \(\) (.*?)\) 1/clarify $1/g;
    90 
    93 
    91   s/Auto_tac/auto/g;
    94   s/Auto_tac/auto/g;
       
    95   s/ALLGOALS Force_tac/force+/g;
    92   s/Force_tac 1/force/g;
    96   s/Force_tac 1/force/g;
    93   s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e;
    97   s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e;
    94   s/Clarsimp_tac 1/clarsimp/g;
    98   s/Clarsimp_tac 1/clarsimp/g;
    95 
    99 
    96   s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g;
   100   s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g;
       
   101   s/ALLGOALS \(force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) \)$/(force $1 $2)+/g;
    97   s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g;
   102   s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g;
    98   s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e;
   103   s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e;
    99   s/clarsimp_tac \(claset \(*\) (.*?), *simpset \(\) (.*?)\) 1/clarsimp $1 $2/g;
   104   s/clarsimp_tac \(claset \(*\) (.*?), *simpset \(\) (.*?)\) 1/clarsimp $1 $2/g;
   100 
   105 
   101   s/Asm_full_simp_tac 1/simp/g;
   106   s/Asm_full_simp_tac 1/simp/g;
   266   s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
   271   s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
   267   s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se;
   272   s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se;
   268   s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se;
   273   s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se;
   269   s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se;
   274   s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se;
   270   s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
   275   s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
   271                              # remove outermost parentheses if around atoms
   276                             # remove outermost parentheses if around atoms
       
   277   s/^(apply +)\(\((.*?)\)([+*]?)\)\s*$/$1($2)$3/;
       
   278                             # remove outermost parentheses if around parentheses
   272   s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg;
   279   s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg;
   273   s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg;
   280   s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg;
   274   s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg;
   281   s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg;
   275   s/^Delsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split del")/seg;
   282   s/^Delsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split del")/seg;
   276   s/^AddIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro")/seg;
   283   s/^AddIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro")/seg;