obsolete (incompatible with Isabelle2019);
authorwenzelm
Tue May 14 10:28:07 2019 +0200 (4 months ago)
changeset 70280a3862cf94e73
parent 70279 02920bc314ee
child 70281 110df6f91376
obsolete (incompatible with Isabelle2019);
lib/Tools/update_op
     1.1 --- a/lib/Tools/update_op	Mon May 13 13:39:59 2019 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,97 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Tobias Nipkow, TU Muenchen
     1.7 -#
     1.8 -# DESCRIPTION: update "op _" syntax
     1.9 -
    1.10 -## diagnostics
    1.11 -
    1.12 -function usage()
    1.13 -{
    1.14 -  echo
    1.15 -  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    1.16 -  echo
    1.17 -  echo "  Options are:"
    1.18 -  echo "    -m           ignore .ML files"
    1.19 -  echo
    1.20 -  echo "  Update the old \"op _\" syntax in theory and ML files."
    1.21 -  echo
    1.22 -  exit 1
    1.23 -}
    1.24 -
    1.25 -
    1.26 -IGNORE_ML=""
    1.27 -
    1.28 -while getopts "m" OPT
    1.29 -do
    1.30 -  case "$OPT" in
    1.31 -    m)
    1.32 -      IGNORE_ML="true"
    1.33 -      ;;
    1.34 -    \?)
    1.35 -      usage
    1.36 -      ;;
    1.37 -  esac
    1.38 -done
    1.39 -
    1.40 -shift $(($OPTIND - 1))
    1.41 -
    1.42 -DIR="."
    1.43 -if [ -n "$1" ]; then
    1.44 -  DIR="$1"
    1.45 -fi
    1.46 -
    1.47 -read -r -d '' THY_SCRIPT <<'EOF'
    1.48 -# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
    1.49 -s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
    1.50 -# op *XY -> ( *XY)
    1.51 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
    1.52 -# op *X -> ( *X)
    1.53 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
    1.54 -# op *R -> ( *R)
    1.55 -s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
    1.56 -# op *\<cdot> -> ( *\<cdot>)
    1.57 -s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
    1.58 -# op ** -> ( ** )
    1.59 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
    1.60 -# op * -> ( * )
    1.61 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
    1.62 -# (op +) -> (+)
    1.63 -s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
    1.64 -# (op + -> ((+)
    1.65 -s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
    1.66 -# op + -> (+)
    1.67 -s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
    1.68 -s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
    1.69 -# op+ -> (+)
    1.70 -s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
    1.71 -s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
    1.72 -s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
    1.73 -EOF
    1.74 -
    1.75 -read -r -d '' ML_SCRIPT <<'EOF'
    1.76 -# op * -> ( * )
    1.77 -s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
    1.78 -s/"op[ ]*\*/"( \* )/g
    1.79 -# (op +) -> (+)
    1.80 -s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
    1.81 -s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
    1.82 -# (op + -> ((+)
    1.83 -s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
    1.84 -# op + -> (+)
    1.85 -s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
    1.86 -s/"op [ ]*\([^ )("]*\)/"(\1)/g
    1.87 -# op+ -> (+)
    1.88 -s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
    1.89 -s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
    1.90 -# is there \<...\> on the line (indicating Isabelle source):
    1.91 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
    1.92 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
    1.93 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
    1.94 -s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
    1.95 -EOF
    1.96 -
    1.97 -find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
    1.98 -
    1.99 -[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
   1.100 -