00001
00002
00003
00004
00005
00006 #ifndef lint
00007 static char vcid[] = "$Id: life.c,v 1.2 1994/12/08 23:27:02 duchier Exp $";
00008 #endif
00009
00010 #include "extern.h"
00011 #include "trees.h"
00012 #include "print.h"
00013 #include "parser.h"
00014 #include "info.h"
00015 #include "login.h"
00016 #include "lefun.h"
00017 #ifndef OS2_PORT
00018 #include "built_ins.h"
00019 #else
00020 #include "built_in.h"
00021 #endif
00022
00023 #include "types.h"
00024 #include "copy.h"
00025 #include "token.h"
00026 #ifndef OS2_PORT
00027 #include "interrupt.h"
00028 #else
00029 #include "interrup.h"
00030 #endif
00031 #include "error.h"
00032 #include "modules.h"
00033 #include "memory.h"
00034
00035 #ifdef X11
00036 #include "xpred.h"
00037 #endif
00038
00039 #ifdef SOLARIS
00040 #include <stdlib.h>
00041 static unsigned int lifeseed;
00042 #endif
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060 extern jmp_buf env;
00061
00062 extern int rand_array[];
00063
00064
00065
00066
00067
00068 main(argc, argv)
00069 long argc;
00070 #ifndef OS2_PORT
00071 char **argv;
00072 #else
00073 char *argv[];
00074 #endif
00075 {
00076 ptr_psi_term s;
00077 ptr_stack save_undo_stack;
00078 long sort,exitflag;
00079 long c;
00080
00081 int i;
00082 #ifdef SOLARIS
00083 for(i=0;i<256;i++)
00084 rand_array[i]=rand_r(&lifeseed);
00085 #else
00086 for(i=0;i<256;i++)
00087 rand_array[i]=random();
00088 #endif
00089
00090
00091 arg_c=argc;
00092 arg_v=argv;
00093
00094 quietflag = GetBoolOption("q");
00095
00096 init_io();
00097 init_memory();
00098 exit_if_true(!mem_base || !other_base);
00099 assert(stack_pointer==mem_base);
00100 init_copy();
00101 assert(stack_pointer==mem_base);
00102 init_print();
00103 assert(stack_pointer==mem_base);
00104
00105
00106 tzset();
00107 times(&life_start);
00108 assert(stack_pointer==mem_base);
00109
00110 init_modules();
00111
00112 init_built_in_types();
00113 assert(stack_pointer==mem_base);
00114 #ifdef X11
00115 x_setup_builtins();
00116 assert(stack_pointer==mem_base);
00117 #endif
00118 init_interrupt();
00119 assert(stack_pointer==mem_base);
00120 title();
00121 assert(stack_pointer==mem_base);
00122 init_trace();
00123 noisy=FALSE;
00124
00125 assert(stack_pointer==mem_base);
00126
00127
00128 set_current_module(user_module);
00129
00130
00131 init_system();
00132
00133 #ifdef ARITY
00134 arity_init();
00135 #endif
00136
00137 #ifndef OS2_PORT
00138 open_input_file("+SETUP+");
00139 #else
00140 open_input_file("~SETUP");
00141 #endif
00142 push_goal(load,input_state,file_date,heap_copy_string("+SETUP+"));
00143 file_date+=2;
00144 main_prove();
00145
00146
00147
00148 do {
00149 setjmp(env);
00150
00151 init_system();
00152 init_trace();
00153
00154 begin_terminal_io();
00155 var_occurred=FALSE;
00156 save_undo_stack=undo_stack;
00157 stdin_cleareof();
00158 c=read_char();
00159
00160 while (c!=EOF && !(c>32 && c!='.' && c!=';')) c=read_char();
00161 if (c==EOF)
00162 exitflag=TRUE;
00163 else {
00164 put_back_char(c);
00165 s=stack_copy_psi_term(parse(&sort));
00166 exitflag=(s->type==eof);
00167 }
00168 end_terminal_io();
00169
00170 if (!exitflag) {
00171 if (sort==QUERY) {
00172
00173
00174
00175 push_goal(what_next,TRUE,var_occurred,1);
00176 ignore_eff=TRUE;
00177 goal_count=0;
00178 push_goal(prove,s,DEFRULES,NULL);
00179 reset_step();
00180 start_chrono();
00181 main_prove();
00182
00183
00184 if (undo_stack) {
00185 undo(NULL);
00186 Errorline("non-NULL undo stack.\n");
00187 }
00188
00189 }
00190 else if (sort==FACT) {
00191 assert_first=FALSE;
00192 assert_clause(s);
00193 undo(save_undo_stack);
00194 var_occurred=FALSE;
00195 encode_types();
00196 Infoline(assert_ok?"\n*** Yes\n":"\n*** No\n");
00197 }
00198 }
00199 } while (!exitflag);
00200
00201
00202
00203 exit_life(TRUE);
00204 }
00205 #ifdef OS2_PORT
00206 float times(float *fit)
00207 {
00208 clock_t it;
00209
00210 it = clock();
00211 *fit = (((float)it)/CLOCKS_PER_SEC);
00212 return (*fit);
00213 }
00214 void tzset()
00215 {
00216 }
00217
00218 #endif