1 /*
2 * ivy.c - part of the otter/ivy interface.
3 *
4 */
5
6 #include "header.h"
7 #include "lisp.h"
8 #include "check.h"
9
10 static struct proof_object *Initial_proof_object = NULL;
11
12 /*************************************************************************/
13
bnode_to_natural(Bnode b)14 static int bnode_to_natural(Bnode b)
15 {
16 if (!atom(b))
17 return -1;
18 else {
19 int i;
20 if (str_int(b->label, &i))
21 return (i < 0 ? -1 : i);
22 else
23 return -1;
24 }
25 } /* bnode_to_natural */
26
27 /*************************************************************************/
28
bnode_to_otterterm(Bnode b,char ** varnames)29 static struct term *bnode_to_otterterm(Bnode b,
30 char **varnames)
31 {
32 if (atom(b)) {
33 int i = 0;
34 char *str;
35 struct term *t = get_term();
36 t->type = VARIABLE;
37 t->sym_num = str_to_sn(b->label, 0);
38 str = sn_to_str(t->sym_num);
39 while (i < MAX_VARS && varnames[i] != NULL &&
40 varnames[i] != sn_to_str(t->sym_num))
41 i++;
42 if (i == MAX_VARS)
43 return NULL;
44 else {
45 if (varnames[i] == NULL)
46 varnames[i] = sn_to_str(t->sym_num);
47 t->varnum = i;
48 }
49 return t;
50 }
51 else if (length(b) == 1) {
52 struct term *t = get_term();
53 t->type = NAME;
54 t->sym_num = str_to_sn(car(b)->label, 0);
55 return t;
56 }
57 else {
58 struct rel *r1, *r2;
59 char *label = car(b)->label;
60 int arity = length(b) - 1;
61 struct term *t = get_term();
62 t->type = COMPLEX;
63 t->sym_num = str_to_sn(label, arity);
64
65 r2 = NULL;
66 for (b = cdr(b) ; !atom(b); b = cdr(b)) {
67 r1 = get_rel();
68 r1->argval = bnode_to_otterterm(b->car, varnames);
69 if (r2 == NULL)
70 t->farg = r1;
71 else
72 r2->narg = r1;
73 r2 = r1;
74 }
75 return t;
76 }
77 } /* bnode_to_otterterm */
78
79 /*************************************************************************/
80 /* This is different from is_symbol in that it works for variables. */
81
special_is_symbol(struct term * t,char * str,int arity)82 int special_is_symbol(struct term *t, char *str, int arity)
83 {
84 return(sn_to_arity(t->sym_num) == arity &&
85 str_ident(sn_to_str(t->sym_num), str));
86 } /* special_is_symbol */
87
88 /*************************************************************************/
89
trans_logic_symbols(struct term * t)90 void trans_logic_symbols(struct term *t)
91 {
92 if (special_is_symbol(t, "TRUE", 0)) {
93 t->sym_num = str_to_sn("$T", 0);
94 t->type = NAME;
95 }
96 else if (special_is_symbol(t, "FALSE", 0)) {
97 t->sym_num = str_to_sn("$F", 0);
98 t->type = NAME;
99 }
100 else if (is_symbol(t, "NOT", 1)) {
101 t->sym_num = str_to_sn("-", 1);
102 trans_logic_symbols(t->farg->argval);
103 }
104 else if (is_symbol(t, "OR", 2)) {
105 t->sym_num = str_to_sn("|", 2);
106 trans_logic_symbols(t->farg->argval);
107 trans_logic_symbols(t->farg->narg->argval);
108 }
109 } /* trans_logic_symbols */
110
111 /*************************************************************************/
112
bnode_to_clause(Bnode b)113 static struct clause *bnode_to_clause(Bnode b)
114 {
115 struct term *t;
116 char *varnames[MAX_VARS];
117 int i;
118
119 for (i=0; i<MAX_VARS; i++)
120 varnames[i] = NULL;
121 t = bnode_to_otterterm(b, varnames);
122 if (t == NULL)
123 return NULL;
124 else {
125 struct clause *c;
126 trans_logic_symbols(t);
127 c = term_to_clause(t);
128 /* lit_t_f_reduce(c); don't do this, because of test in derive */
129 return c;
130 }
131 } /* bnode_to_clause */
132
133 /*************************************************************************/
134
parse_initial_proof_object(FILE * fp)135 struct proof_object *parse_initial_proof_object(FILE *fp)
136 {
137 struct proof_object *po = get_proof_object();
138 Bnode lisp_proof_object = parse_lisp(fp);
139 Bnode b;
140 Bnode lisp_step;
141 if (lisp_proof_object == NULL)
142 abend("parse_proof_object: parse_listp returns NULL");
143 if (!true_listp(lisp_proof_object))
144 abend("parse_proof_object: parse_listp nonlist");
145
146 for (b = lisp_proof_object; !nullp(b); b = b->cdr) {
147 struct proof_object_node *pn = connect_new_node(po);
148 Bnode e1, e2, e3;
149 char *label;
150 lisp_step = b->car;
151 if (length(lisp_step) < 3)
152 abend("parse_proof_object: step length < 3");
153 e1 = car(lisp_step);
154 e2 = cadr(lisp_step);
155 e3 = caddr(lisp_step);
156 pn->id = bnode_to_natural(e1);
157 if (length(e2) < 1 || !atom(car(e2)))
158 abend("parse_proof_object: bad justification (1)");
159 label = car(e2)->label;
160 if (str_ident(label, "INPUT"))
161 pn->rule = P_RULE_INPUT;
162 else if (str_ident(label, "EQ-AXIOM"))
163 pn->rule = P_RULE_EQ_AXIOM;
164 else
165 abend("parse_proof_object: bad justification (2)");
166 pn->c = bnode_to_clause(e3);
167 if (!pn->c)
168 abend("parse_proof_object: NULL clause");
169 } /* for each step */
170 return po;
171 } /* parse_proof_object */
172
173 /*************************************************************************/
174
init_proof_object(FILE * fin,FILE * fout)175 struct list *init_proof_object(FILE *fin,
176 FILE *fout)
177 {
178 struct proof_object *obj;
179 init_proof_object_environment();
180 obj = parse_initial_proof_object(fin);
181 if (obj == NULL) {
182 fprintf(fout, "error parsing initial proof object\n");
183 return NULL;
184 }
185 else {
186 struct proof_object_node *pn;
187 struct list *lst = get_list();
188 print_proof_object(fout, obj);
189 for (pn = obj->first; pn != NULL; pn = pn->next)
190 append_cl(lst, cl_copy(pn->c)); /* this gets rid of variable names */
191 Initial_proof_object = obj; /* save it for construction of final version */
192 return lst;
193 }
194 } /* init_proof_object */
195
196 /*************************************************************************/
197
retrieve_initial_proof_object(void)198 struct proof_object *retrieve_initial_proof_object(void)
199 {
200 return Initial_proof_object;
201 } /* retrieve_initial_proof_object */
202