author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 47316 | 15428dd82b54 |
child 53498 | 05313b45a5ae |
permissions | -rwxr-xr-x |
46844 | 1 |
#!/bin/bash |
2 |
# |
|
46846
9e99afaade17
split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
46844
diff
changeset
|
3 |
# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it |
9e99afaade17
split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
46844
diff
changeset
|
4 |
# Isabelle-friendly. |
46844 | 5 |
# |
6 |
# This code is based on that used in src/Tools/Metis to adapt Metis for |
|
7 |
# use in Isabelle. |
|
8 |
||
9 |
INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml" |
|
10 |
||
11 |
echo "Cleaning" |
|
46846
9e99afaade17
split make_tptp_parser into two scripts, for parser and lib respectively;
sultana
parents:
46844
diff
changeset
|
12 |
rm -f tptp_lexyacc.ML |
46844 | 13 |
echo "Generating lexer and parser" |
14 |
ml-lex tptp.lex && ml-yacc tptp.yacc |
|
15 |
echo "Generating tptp_lexyacc.ML" |
|
16 |
( |
|
17 |
cat <<EOF |
|
18 |
||
19 |
(******************************************************************) |
|
20 |
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
21 |
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
22 |
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
23 |
(******************************************************************) |
|
24 |
||
25 |
(* |
|
26 |
This file is produced from the parser generated by ML-Yacc from the |
|
27 |
source files tptp.lex and tptp.yacc. |
|
28 |
*) |
|
29 |
EOF |
|
30 |
||
31 |
for FILE in $INTERMEDIATE_FILES |
|
32 |
do |
|
47316
15428dd82b54
removed use of CharVector in generated parser, to make SMLNJ happy
sultana
parents:
46846
diff
changeset
|
33 |
perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ |
15428dd82b54
removed use of CharVector in generated parser, to make SMLNJ happy
sultana
parents:
46846
diff
changeset
|
34 |
-e 's/Unsafe\.(.*)/\1/g;' \ |
15428dd82b54
removed use of CharVector in generated parser, to make SMLNJ happy
sultana
parents:
46846
diff
changeset
|
35 |
-e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE |
46844 | 36 |
done |
37 |
) > tptp_lexyacc.ML |
|
38 |
||
39 |
rm -f $INTERMEDIATE_FILES tptp.yacc.desc |