00001
00002
00003
00004
00005
00006 #ifndef lint
00007 static char vcid[] = "$Id: lib.c,v 1.2 1994/12/08 23:26:47 duchier Exp $";
00008 #endif
00009
00010
00011
00012
00013 #include "extern.h"
00014 #include "trees.h"
00015 #include "print.h"
00016 #include "parser.h"
00017 #include "info.h"
00018 #include "login.h"
00019 #include "lefun.h"
00020 #ifndef OS2_PORT
00021 #include "built_ins.h"
00022 #else
00023 #include "built_in.h"
00024 #endif
00025 #include "types.h"
00026 #include "copy.h"
00027 #include "token.h"
00028 #ifndef OS2_PORT
00029 #include "interrupt.h"
00030 #else
00031 #include "interrup.h"
00032 #endif
00033 #include "error.h"
00034 #include "modules.h"
00035
00036 #include "c_life.h"
00037
00038
00039 #ifdef X11
00040 #include "xpred.h"
00041 #endif
00042
00043 #ifdef SOLARIS
00044 #include <stdlib.h>
00045 static unsigned int libseed;
00046 #endif
00047
00048 long noisy=TRUE;
00049 long file_date=3;
00050 long types_done=FALSE;
00051
00052 #ifndef OS2_PORT
00053 struct tms life_start,life_end;
00054 #else
00055 float life_start,life_end;
00056 #endif
00057
00058 float garbage_time=0;
00059
00060 extern int rand_array[256];
00061
00062
00063 int c_query_level;
00064
00065 extern jmp_buf env;
00066
00067
00068
00069 char **group_features(f,n)
00070 char **f;
00071 ptr_node n;
00072 {
00073 *f=NULL;
00074 if(n) {
00075 if(n->left)
00076 f=group_features(f,n->left);
00077 *f=n->key;
00078 f++;
00079 if(n->right)
00080 f=group_features(f,n->right);
00081 }
00082
00083 return f;
00084 }
00085
00086
00087 void exit_if_true(exitflag)
00088 long exitflag;
00089 {
00090 if (exitflag) {
00091 printf("\n\n*** Execution is not allowed to continue.\n");
00092
00093 exit(1);
00094 }
00095 }
00096
00097
00098
00099
00100 void init_io()
00101 {
00102 #ifndef OS2_PORT
00103 struct stat buffer;
00104
00105 fstat(fileno(stdin), &buffer);
00106
00107 stdin_terminal=(S_IFCHR & buffer.st_mode)!=0;
00108 input_state=NULL;
00109 stdin_state=NULL;
00110 output_stream=stdout;
00111 #else
00112 stdin_terminal=TRUE ;
00113 input_state=NULL;
00114 stdin_state=NULL;
00115 output_stream=stdout;
00116 #endif
00117 }
00118
00119
00120 extern char prompt_buffer[];
00121
00122
00123
00124 void init_system()
00125 {
00126 #ifdef X11
00127 x_window_creation=FALSE;
00128 #endif
00129 stack_pointer=mem_base;
00130 goal_stack=NULL;
00131 choice_stack=NULL;
00132 undo_stack=NULL;
00133 var_tree=NULL;
00134
00135
00136 if(current_module==user_module)
00137 prompt=PROMPT;
00138 else {
00139 prompt=prompt_buffer;
00140 sprintf(prompt_buffer,"%s%s",current_module->module_name,PROMPT);
00141 }
00142
00143 resid_aim=NULL;
00144 exit_if_true(!memory_check());
00145
00146 #ifdef X11
00147
00148 xevent_list=stack_nil();
00149 #endif
00150
00151 init_global_vars();
00152 }
00153
00154
00155 extern int rand_array[];
00156
00157
00158
00159
00160
00161
00162
00163 WFInit(argc, argv)
00164
00165 long argc;
00166 char **argv;
00167 {
00168 ptr_psi_term s;
00169 ptr_stack save_undo_stack;
00170 long sort,exitflag;
00171 int c;
00172
00173
00174 int i;
00175 #ifdef SOLARIS
00176 for(i=0;i<256;i++)
00177 rand_array[i]=rand_r(&libseed);
00178 #else
00179 for(i=0;i<256;i++)
00180 rand_array[i]=random();
00181 #endif
00182
00183
00184 arg_c=argc;
00185 arg_v=argv;
00186
00187 quietflag = TRUE;
00188
00189 init_io();
00190 init_memory();
00191 exit_if_true(!mem_base || !other_base);
00192 assert(stack_pointer==mem_base);
00193 init_copy();
00194 assert(stack_pointer==mem_base);
00195 init_print();
00196 assert(stack_pointer==mem_base);
00197
00198
00199 tzset();
00200 times(&life_start);
00201 assert(stack_pointer==mem_base);
00202
00203 init_modules();
00204
00205 init_built_in_types();
00206 assert(stack_pointer==mem_base);
00207 #ifdef X11
00208 x_setup_builtins();
00209 assert(stack_pointer==mem_base);
00210 #endif
00211 init_interrupt();
00212 assert(stack_pointer==mem_base);
00213 title();
00214 assert(stack_pointer==mem_base);
00215 init_trace();
00216 noisy=FALSE;
00217
00218 assert(stack_pointer==mem_base);
00219
00220
00221 set_current_module(user_module);
00222
00223
00224 init_system();
00225
00226 #ifdef ARITY
00227 arity_init();
00228 #endif
00229
00230 #ifndef OS2_PORT
00231 open_input_file("+SETUP+");
00232 #else
00233 open_input_file("~SETUP");
00234 #endif
00235 push_goal(load,input_state,file_date,heap_copy_string("+SETUP+"));
00236 file_date+=2;
00237 main_prove();
00238
00239
00240 setjmp(env);
00241
00242 init_system();
00243 init_trace();
00244 begin_terminal_io();
00245 var_occurred=FALSE;
00246 save_undo_stack=undo_stack;
00247 stdin_cleareof();
00248
00249 c_query_level=0;
00250 }
00251
00252
00253
00254 int WFInput(query)
00255
00256 char *query;
00257 {
00258 ptr_psi_term t;
00259 long sort;
00260 parse_block pb;
00261 int result=WFno;
00262 ptr_stack save_undo_stack;
00263 ptr_choice_point old_choice;
00264
00265
00266 save_undo_stack=undo_stack;
00267 old_choice=choice_stack;
00268
00269
00270 if(!strcmp(query,".")) {
00271 reset_stacks();
00272 result=WFyes;
00273 c_query_level=0;
00274 }
00275 else {
00276 if(!strcmp(query,";")) {
00277 sort=QUERY;
00278 push_goal(fail,NULL,NULL,NULL);
00279 }
00280 else {
00281
00282 save_parse_state(&pb);
00283 init_parse_state();
00284 stringparse=TRUE;
00285 stringinput=query;
00286
00287
00288 var_occurred=FALSE;
00289 t=stack_copy_psi_term(parse(&sort));
00290
00291
00292 if(sort==QUERY) {
00293 ignore_eff=TRUE;
00294 goal_count=0;
00295
00296 push_choice_point(c_what_next,c_query_level,NULL,NULL);
00297 c_query_level++;
00298 push_goal(c_what_next,c_query_level,var_occurred,NULL);
00299 push_goal(prove,t,DEFRULES,NULL);
00300
00301 }
00302 else if (sort==FACT) {
00303 assert_first=FALSE;
00304 assert_clause(t);
00305 if(assert_ok)
00306 result=WFyes;
00307 undo(save_undo_stack);
00308 var_occurred=FALSE;
00309 encode_types();
00310 }
00311 }
00312
00313 if(sort==QUERY) {
00314 start_chrono();
00315 main_prove();
00316
00317 if(goal_stack && goal_stack->type==c_what_next) {
00318
00319 if((int)(goal_stack->a)==c_query_level)
00320 if(choice_stack==old_choice) {
00321 result=WFyes;
00322 c_query_level--;
00323 }
00324 else
00325 result=WFmore;
00326 else {
00327 result=WFno;
00328 c_query_level--;
00329 }
00330
00331 goal_stack=goal_stack->next;
00332 }
00333 }
00334 }
00335
00336 return result;
00337 }
00338
00339
00340
00341 PsiTerm WFGetVar(name)
00342
00343 char *name;
00344 {
00345 ptr_psi_term result=NULL;
00346 ptr_node n;
00347
00348 n=find(strcmp,name,var_tree);
00349 if(n) {
00350 result=(ptr_psi_term)n->data;
00351 if(result)
00352 deref_ptr(result);
00353 }
00354
00355 return result;
00356 }
00357
00358
00359 int WFfeature_count_loop(n)
00360
00361 ptr_node n;
00362 {
00363 int result=0;
00364
00365 if(n) {
00366 if(n->left)
00367 result+=WFfeature_count_loop(n->left);
00368 result++;
00369 if(n->right)
00370 result+=WFfeature_count_loop(n->right);
00371 }
00372
00373 return result;
00374 }
00375
00376
00377
00378 int WFFeatureCount(psi)
00379
00380 ptr_psi_term psi;
00381 {
00382 int result=0;
00383
00384 if(psi) {
00385 deref_ptr(psi);
00386 result=WFfeature_count_loop(psi->attr_list);
00387 }
00388
00389 return result;
00390 }
00391
00392
00393
00394 char *WFType(psi)
00395
00396 ptr_psi_term psi;
00397 {
00398 char *result=NULL;
00399 if(psi) {
00400 deref_ptr(psi);
00401 result=psi->type->keyword->combined_name;
00402 }
00403 return result;
00404 }
00405
00406
00407
00408 char **WFFeatures(psi)
00409
00410 ptr_psi_term psi;
00411 {
00412 char **features=NULL;
00413 int n;
00414
00415 if(psi) {
00416 deref_ptr(psi);
00417
00418 n=WFfeature_count_loop(psi->attr_list);
00419 if(n) {
00420 features=(char **)malloc((n+1)*sizeof(char *));
00421 group_features(features,psi->attr_list);
00422 }
00423 }
00424
00425 return features;
00426 }
00427
00428
00429
00430
00431 double WFGetDouble(psi,ok)
00432 ptr_psi_term psi;
00433 int *ok;
00434 {
00435 double value=0.0;
00436
00437 if(ok)
00438 *ok=FALSE;
00439
00440 if(psi) {
00441 deref_ptr(psi);
00442
00443 if(sub_type(psi->type,real) && psi->value) {
00444 value= *((double *)psi->value);
00445 if(ok)
00446 *ok=TRUE;
00447 }
00448 }
00449 return value;
00450 }
00451
00452
00453
00454 char *WFGetString(psi,ok)
00455 ptr_psi_term psi;
00456 int *ok;
00457 {
00458 char *value=NULL;
00459
00460 if(ok)
00461 *ok=FALSE;
00462
00463 if(psi) {
00464 deref_ptr(psi);
00465
00466 if(sub_type(psi->type,quoted_string) && psi->value) {
00467 value=(char *)psi->value;
00468 if(ok)
00469 *ok=TRUE;
00470 }
00471 }
00472 return value;
00473 }
00474
00475
00476
00477 PsiTerm WFGetFeature(psi,feature)
00478
00479 ptr_psi_term psi;
00480 char *feature;
00481 {
00482 ptr_psi_term result=NULL;
00483 ptr_node n;
00484
00485 if(psi && feature) {
00486 deref_ptr(psi);
00487 n=find(featcmp,feature,psi->attr_list);
00488 if(n)
00489 result=(PsiTerm)n->data;
00490 }
00491
00492 return result;
00493 }