46844
|
1 |
(* Title: HOL/TPTP/TPTP_Parser.thy
|
|
2 |
Author: Nik Sultana, Cambridge University Computer Laboratory
|
|
3 |
|
|
4 |
Importing TPTP files into Isabelle/HOL:
|
|
5 |
* parsing TPTP formulas;
|
|
6 |
* interpreting TPTP formulas as HOL terms (i.e. importing types, and
|
|
7 |
type-checking the terms);
|
|
8 |
*)
|
|
9 |
|
|
10 |
theory TPTP_Parser
|
|
11 |
imports Main
|
46951
|
12 |
keywords "import_tptp" :: thy_decl
|
46844
|
13 |
uses
|
|
14 |
"TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
|
|
15 |
|
|
16 |
"TPTP_Parser/tptp_syntax.ML"
|
|
17 |
"TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
|
|
18 |
"TPTP_Parser/tptp_parser.ML"
|
|
19 |
"TPTP_Parser/tptp_problem_name.ML"
|
|
20 |
"TPTP_Parser/tptp_interpret.ML"
|
|
21 |
|
|
22 |
begin
|
|
23 |
|
|
24 |
text {*The TPTP parser was generated using ML-Yacc, and needs the
|
|
25 |
ML-Yacc library to operate. This library is included with the parser,
|
|
26 |
and we include the next section in accordance with ML-Yacc's terms of
|
|
27 |
use.*}
|
|
28 |
|
|
29 |
section "ML-YACC COPYRIGHT NOTICE, LICENSE AND DISCLAIMER."
|
|
30 |
text {*
|
|
31 |
Copyright 1989, 1990 by David R. Tarditi Jr. and Andrew W. Appel
|
|
32 |
|
|
33 |
Permission to use, copy, modify, and distribute this software and its
|
|
34 |
documentation for any purpose and without fee is hereby granted,
|
|
35 |
provided that the above copyright notice appear in all copies and that
|
|
36 |
both the copyright notice and this permission notice and warranty
|
|
37 |
disclaimer appear in supporting documentation, and that the names of
|
|
38 |
David R. Tarditi Jr. and Andrew W. Appel not be used in advertising or
|
|
39 |
publicity pertaining to distribution of the software without specific,
|
|
40 |
written prior permission.
|
|
41 |
|
|
42 |
David R. Tarditi Jr. and Andrew W. Appel disclaim all warranties with
|
|
43 |
regard to this software, including all implied warranties of
|
|
44 |
merchantability and fitness. In no event shall David R. Tarditi
|
|
45 |
Jr. and Andrew W. Appel be liable for any special, indirect or
|
|
46 |
consequential damages or any damages whatsoever resulting from loss of
|
|
47 |
use, data or profits, whether in an action of contract, negligence or
|
|
48 |
other tortious action, arising out of or in connection with the use or
|
|
49 |
performance of this software.
|
|
50 |
*}
|
|
51 |
|
|
52 |
end |