lib/Tools/update_op

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_op	Wed Jan 10 15:21:49 2018 +0100
@@ -0,0 +1,97 @@
+#!/usr/bin/env bash
+#
+# Author: Tobias Nipkow, TU Muenchen
+#
+# DESCRIPTION: update "op _" syntax
+
+## diagnostics
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
+  echo
+  echo "  Options are:"
+  echo "    -m           ignore .ML files"
+  echo
+  echo "  Update the old \"op _\" syntax in theory and ML files."
+  echo
+  exit 1
+}
+
+
+IGNORE_ML=""
+
+while getopts "m" OPT
+do
+  case "$OPT" in
+    m)
+      IGNORE_ML="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+DIR="."
+if [ -n "$1" ]; then
+  DIR="$1"
+fi
+
+read -r -d '' THY_SCRIPT <<'EOF'
+# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
+s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
+# op *XY -> ( *XY)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
+# op *X -> ( *X)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
+# op *R -> ( *R)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
+# op *\<cdot> -> ( *\<cdot>)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
+# op ** -> ( ** )
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
+# op * -> ( * )
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
+# (op +) -> (+)
+s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
+# (op + -> ((+)
+s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
+# op + -> (+)
+s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
+s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
+# op+ -> (+)
+s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
+s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
+s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
+EOF
+
+read -r -d '' ML_SCRIPT <<'EOF'
+# op * -> ( * )
+s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
+s/"op[ ]*\*/"( \* )/g
+# (op +) -> (+)
+s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
+s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
+# (op + -> ((+)
+s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
+# op + -> (+)
+s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
+s/"op [ ]*\([^ )("]*\)/"(\1)/g
+# op+ -> (+)
+s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
+s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
+# is there \<...\> on the line (indicating Isabelle source):
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
+s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
+EOF
+
+find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
+
+[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
+