1#!/usr/bin/env bash
2#
3# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it
4#                    Isabelle-friendly.
5#
6# This code is based on that used in src/Tools/Metis to adapt Metis for
7# use in Isabelle.
8
9INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"
10
11echo "Cleaning"
12rm -f tptp_lexyacc.ML
13echo "Generating lexer and parser"
14ml-lex tptp.lex && ml-yacc tptp.yacc
15echo "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*)
29EOF
30
31for FILE in $INTERMEDIATE_FILES
32do
33  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
34          -e 's/Unsafe\.(.*)/\1/g;' \
35          -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
36done
37) | expand -t8 > tptp_lexyacc.ML
38
39rm -f $INTERMEDIATE_FILES tptp.yacc.desc
40