equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # make_tptp_parser - Generates Isabelle-friendly version of ML-Yacc's library, |
3 # make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it |
4 # runs ML-Yacc to generate TPTP parser, and makes the |
4 # Isabelle-friendly. |
5 # generated parser Isabelle-friendly. |
|
6 # |
5 # |
7 # This code is based on that used in src/Tools/Metis to adapt Metis for |
6 # This code is based on that used in src/Tools/Metis to adapt Metis for |
8 # use in Isabelle. |
7 # use in Isabelle. |
9 |
8 |
10 MLYACCDIR=./ml-yacc |
|
11 INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml" |
9 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 |
10 |
14 echo "Cleaning" |
11 echo "Cleaning" |
15 rm -f {tptp_lexyacc,ml_yacc_lib}.ML |
12 rm -f tptp_lexyacc.ML |
16 echo "Generating lexer and parser" |
13 echo "Generating lexer and parser" |
17 ml-lex tptp.lex && ml-yacc tptp.yacc |
14 ml-lex tptp.lex && ml-yacc tptp.yacc |
18 echo "Generating tptp_lexyacc.ML" |
15 echo "Generating tptp_lexyacc.ML" |
19 ( |
16 ( |
20 cat <<EOF |
17 cat <<EOF |
36 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE |
33 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE |
37 done |
34 done |
38 ) > tptp_lexyacc.ML |
35 ) > tptp_lexyacc.ML |
39 |
36 |
40 rm -f $INTERMEDIATE_FILES tptp.yacc.desc |
37 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 |
|