src/HOL/TPTP/TPTP_Parser/make_mlyacclib

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Fri Mar 09 15:39:06 2012 +0000
@@ -0,0 +1,54 @@
+#!/bin/bash
+#
+# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
+#
+# This code is based on that used in src/Tools/Metis to adapt Metis for
+# use in Isabelle.
+
+MLYACCDIR=./ml-yacc
+MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
+
+echo "Cleaning"
+rm -f ml_yacc_lib.ML
+echo "Generating ml_yacc_lib.ML"
+(
+  cat <<EOF
+
+(******************************************************************)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(******************************************************************)
+
+print_depth 0;
+
+(*
+  This file is generated from the contents of ML-Yacc's lib directory.
+  ML-Yacc's COPYRIGHT-file contents follow:
+
+EOF
+  perl -pe 'print "  ";' ml-yacc/COPYRIGHT
+  echo "*)"
+
+for FILE in $MLYACCLIB_FILES
+do
+  echo
+  echo "(**** Original file: $FILE ****)"
+  echo
+  echo -e "  $FILE" >&2
+  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
+          -e 's/Unsafe\.(.*)/\1/g;' \
+          -e 's/\bconcat\b/String.concat/g;' \
+          -e 's/(?<!List\.)foldr\b/List.foldr/g;' \
+          -e 's/\bfoldl\b/List.foldl/g;' \
+          -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
+          -e 's/\bprint\b/TextIO.print/g;' \
+          $MLYACCDIR/lib/$FILE
+  done
+
+  cat <<EOF
+;
+print_depth 10;
+EOF
+
+) > ml_yacc_lib.ML
\ No newline at end of file