author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 46846 | 9e99afaade17 |
child 53498 | 05313b45a5ae |
permissions | -rwxr-xr-x |
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 |