src/HOL/TPTP/TPTP_Parser/make_tptp_parser

added tptp parser;

#!/bin/bash
#
# make_tptp_parser - Generates Isabelle-friendly version of ML-Yacc's library,
#                    runs ML-Yacc to generate TPTP parser, and makes the
#                    generated parser Isabelle-friendly.
#
# This code is based on that used in src/Tools/Metis to adapt Metis for
# use in Isabelle.

MLYACCDIR=./ml-yacc
INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"
MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"

echo "Cleaning"
rm -f {tptp_lexyacc,ml_yacc_lib}.ML
echo "Generating lexer and parser"
ml-lex tptp.lex && ml-yacc tptp.yacc
echo "Generating tptp_lexyacc.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 *)
(******************************************************************)

(*
  This file is produced from the parser generated by ML-Yacc from the
  source files tptp.lex and tptp.yacc.
*)
EOF

for FILE in $INTERMEDIATE_FILES
do
  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE
done
) > tptp_lexyacc.ML

rm -f $INTERMEDIATE_FILES tptp.yacc.desc

#Now patch and collate ML-Yacc's library files
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