src/HOL/TPTP/TPTP_Parser/make_mlyacclib
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46846 9e99afaade17
child 53498 05313b45a5ae
permissions -rwxr-xr-x
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46846
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     1
#!/bin/bash
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     2
#
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     3
# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     4
#
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     5
# This code is based on that used in src/Tools/Metis to adapt Metis for
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     6
# use in Isabelle.
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     7
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     8
MLYACCDIR=./ml-yacc
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
     9
MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    10
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    11
echo "Cleaning"
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    12
rm -f ml_yacc_lib.ML
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    13
echo "Generating ml_yacc_lib.ML"
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    14
(
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    15
  cat <<EOF
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    16
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    17
(******************************************************************)
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    18
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    19
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    20
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    21
(******************************************************************)
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    22
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    23
print_depth 0;
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    24
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    25
(*
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    26
  This file is generated from the contents of ML-Yacc's lib directory.
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    27
  ML-Yacc's COPYRIGHT-file contents follow:
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    28
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    29
EOF
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    30
  perl -pe 'print "  ";' ml-yacc/COPYRIGHT
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    31
  echo "*)"
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    32
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    33
for FILE in $MLYACCLIB_FILES
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    34
do
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    35
  echo
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    36
  echo "(**** Original file: $FILE ****)"
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    37
  echo
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    38
  echo -e "  $FILE" >&2
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    39
  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    40
          -e 's/Unsafe\.(.*)/\1/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    41
          -e 's/\bconcat\b/String.concat/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    42
          -e 's/(?<!List\.)foldr\b/List.foldr/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    43
          -e 's/\bfoldl\b/List.foldl/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    44
          -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    45
          -e 's/\bprint\b/TextIO.print/g;' \
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    46
          $MLYACCDIR/lib/$FILE
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    47
  done
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    48
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    49
  cat <<EOF
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    50
;
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    51
print_depth 10;
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    52
EOF
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    53
9e99afaade17 split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
diff changeset
    54
) > ml_yacc_lib.ML