1
/* Copyright (C) 2006, 2007 William McCune
3
This file is part of the LADR Deduction Library.
5
The LADR Deduction Library is free software; you can redistribute it
6
and/or modify it under the terms of the GNU General Public License,
9
The LADR Deduction Library is distributed in the hope that it will be
10
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12
GNU General Public License for more details.
14
You should have received a copy of the GNU General Public License
15
along with the LADR Deduction Library; if not, write to the Free Software
16
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
25
This package has routines for reading and writing terms in
26
human-readable form. Binary function symbols can be declared
27
to be infix with a precedence and left or right association,
28
so that many parentheses can be omitted. Unary symbols
29
can be declared to be prefix or postfix.
30
In addition, prolog-style list-notation and quantified formulas are
33
The symbol declarations and parse rules are similar to the method
34
used by many Prolog systems (although we use mnemonic names
35
instead of xfy, yfx, yf, etc.). The symbol declarations
36
are made with set_parse_type().
38
This package is based on code taked form Otter and EQP, but there
39
are some important differences. Detailed documentation should
40
be available elsewhere.
42
The intension is to use this package for reading
43
and writing all types of data (terms, clauses, formulas, control
44
information, etc.), with outside routines to translate to/from
45
the appropriate internal data structure when necessary.
48
/* Public definitions */
50
/* End of public definitions */
52
/* Public function prototypes from parse.c */
54
void fprint_parse_mem(FILE *fp, BOOL heading);
56
void p_parse_mem(void);
58
void translate_neg_equalities(BOOL flag);
60
BOOL ordinary_constant_string(char *s);
62
Term sread_term(String_buf sb, FILE *fout);
64
Term read_term(FILE *fin, FILE *fout);
66
Term parse_term_from_string(char *s);
68
void sb_write_term(String_buf sb, Term t);
70
void fwrite_term(FILE *fp, Term t);
72
void fwrite_term_nl(FILE *fp, Term t);
74
char *process_quoted_symbol(char *str);
76
void declare_parse_type(char *str, int precedence, Parsetype type);
78
void declare_quantifier_precedence(int prec);
80
void declare_standard_parse_types(void);
82
BOOL redeclare_symbol_and_copy_parsetype(char *operation, char *str,
83
BOOL echo, FILE *fout);
85
void skip_to_nl(FILE *fp);
87
Plist split_string(char *onlys);
89
void set_cons_char(char c);
91
char get_cons_char(void);
93
void set_quote_char(char c);
95
char get_quote_char(void);
97
void parenthesize(BOOL setting);
99
void check_for_illegal_symbols(BOOL setting);
101
#endif /* conditional compilation of whole file */
added
removed
ladr/parse.h.bak
