|
1 #!/bin/bash |
|
2 # |
|
3 # make_tptp_parser - Generates Isabelle-friendly version of ML-Yacc's library, |
|
4 # runs ML-Yacc to generate TPTP parser, and makes the |
|
5 # generated parser Isabelle-friendly. |
|
6 # |
|
7 # This code is based on that used in src/Tools/Metis to adapt Metis for |
|
8 # use in Isabelle. |
|
9 |
|
10 MLYACCDIR=./ml-yacc |
|
11 INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml" |
|
12 MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml" |
|
13 |
|
14 echo "Cleaning" |
|
15 rm -f {tptp_lexyacc,ml_yacc_lib}.ML |
|
16 echo "Generating lexer and parser" |
|
17 ml-lex tptp.lex && ml-yacc tptp.yacc |
|
18 echo "Generating tptp_lexyacc.ML" |
|
19 ( |
|
20 cat <<EOF |
|
21 |
|
22 (******************************************************************) |
|
23 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
24 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
25 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
26 (******************************************************************) |
|
27 |
|
28 (* |
|
29 This file is produced from the parser generated by ML-Yacc from the |
|
30 source files tptp.lex and tptp.yacc. |
|
31 *) |
|
32 EOF |
|
33 |
|
34 for FILE in $INTERMEDIATE_FILES |
|
35 do |
|
36 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE |
|
37 done |
|
38 ) > tptp_lexyacc.ML |
|
39 |
|
40 rm -f $INTERMEDIATE_FILES tptp.yacc.desc |
|
41 |
|
42 #Now patch and collate ML-Yacc's library files |
|
43 echo "Generating ml_yacc_lib.ML" |
|
44 ( |
|
45 cat <<EOF |
|
46 |
|
47 (******************************************************************) |
|
48 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
49 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
50 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) |
|
51 (******************************************************************) |
|
52 |
|
53 print_depth 0; |
|
54 |
|
55 (* |
|
56 This file is generated from the contents of ML-Yacc's lib directory. |
|
57 ML-Yacc's COPYRIGHT-file contents follow: |
|
58 |
|
59 EOF |
|
60 perl -pe 'print " ";' ml-yacc/COPYRIGHT |
|
61 echo "*)" |
|
62 |
|
63 for FILE in $MLYACCLIB_FILES |
|
64 do |
|
65 echo |
|
66 echo "(**** Original file: $FILE ****)" |
|
67 echo |
|
68 echo -e " $FILE" >&2 |
|
69 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ |
|
70 -e 's/Unsafe\.(.*)/\1/g;' \ |
|
71 -e 's/\bconcat\b/String.concat/g;' \ |
|
72 -e 's/(?<!List\.)foldr\b/List.foldr/g;' \ |
|
73 -e 's/\bfoldl\b/List.foldl/g;' \ |
|
74 -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \ |
|
75 -e 's/\bprint\b/TextIO.print/g;' \ |
|
76 $MLYACCDIR/lib/$FILE |
|
77 done |
|
78 |
|
79 cat <<EOF |
|
80 ; |
|
81 print_depth 10; |
|
82 EOF |
|
83 |
|
84 ) > ml_yacc_lib.ML |