| products/sources/formale sprachen/Coq/doc/sphinx/proof-engine/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: make_tptp_parser Sprache: ScalaOriginal von: Isabelle© |
|
||||||
|
#!/usr/bin/env bash
# # make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it # Isabelle-friendly. # # This code is based on that used in src/Tools/Metis to adapt Metis for # use in Isabelle. INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml" echo "Cleaning" rm -f tptp_lexyacc.ML echo "Generating lexer and parser" ml-lex tptp.lex && ml-yacc tptp.yacc echo "Generating tptp_lexyacc.ML" ( cat <<EOF (******************************************************************) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (******************************************************************) (* This file is produced from the parser generated by ML-Yacc from the source files tptp.lex and tptp.yacc. *) EOF for FILE in $INTERMEDIATE_FILES do perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ -e 's/Unsafe\.(.*)/\1/g;' \ -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE done ) | expand -t8 > tptp_lexyacc.ML rm -f $INTERMEDIATE_FILES tptp.yacc.desc ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
