#include "extern.h"#include "login.h"#include "trees.h"#include "copy.h"#include "parser.h"#include "token.h"#include "print.h"#include "built_ins.h"#include "types.h"#include "lefun.h"#include "memory.h"#include "error.h"#include "xpred.h"#include "modules.h"#include "interrupt.h"Go to the source code of this file.
| #define RESTORE_TIME_STAMP |
Value:
| #define TRAIL_TS |
| #define TRAIL_TS |
| void add_rule | ( | ptr_psi_term | head, | |
| ptr_psi_term | body, | |||
| def_type | typ | |||
| ) |
Definition at line 204 of file login.c.
References wl_pair_list::a, assert_first, assert_ok, wl_psi_term::attr_list, wl_pair_list::b, clear_copy(), wl_keyword::combined_name, wl_psi_term::coref, current_module, deref_ptr, Errorline(), HEAP, HEAP_ALLOC, wl_definition::keyword, MAX_BUILT_INS, wl_module::module_name, wl_pair_list::next, NULL, predicate, quote_copy(), redefine(), wl_psi_term::resid, wl_definition::rule, succeed, wl_keyword::symbol, TRUE, wl_definition::type, wl_psi_term::type, undef, and wl_psi_term::value.
Referenced by assert_attributes(), assert_clause(), assert_complicated_type(), and assert_rule().
| void assert_clause | ( | ptr_psi_term | t | ) |
Definition at line 323 of file login.c.
References add_rule(), assert_attributes(), assert_complicated_type(), assert_ok, assert_rule(), deref_ptr, equ_tok, FALSE, function, NULL, and predicate.
Referenced by c_assert_first(), c_assert_last(), load_aim(), main(), WFInput(), and what_next_aim().
Definition at line 293 of file login.c.
References add_rule(), get_two_args(), and Syntaxerrorline().
Referenced by assert_clause().
| void backtrack | ( | ) |
Definition at line 776 of file login.c.
References wl_choice_point::goal_stack, wl_choice_point::next, NULL, resid_aim, stack_pointer, wl_choice_point::stack_top, undo(), and wl_choice_point::undo_point.
Referenced by main_prove().
| long clause_aim | ( | long | r | ) |
Definition at line 1830 of file login.c.
References wl_goal::a, wl_psi_term::attr_list, wl_goal::b, wl_goal::c, clause, clear_copy(), del_clause, Errorline(), FALSE, i_eval_args(), wl_definition::keyword, MAX_BUILT_INS, NULL, push_choice_point(), push_goal(), quote_copy(), retract, STACK, wl_psi_term::status, wl_keyword::symbol, Traceline, TRUE, wl_psi_term::type, and unify.
Referenced by main_prove().
| static void clean_trail | ( | ptr_choice_point | cutpt | ) | [static] |
Definition at line 809 of file login.c.
References wl_stack::a, clean_iter, clean_succ, mem_base, wl_stack::next, NULL, stack_pointer, wl_stack::type, undo_action, and VALID_RANGE.
Referenced by c_set_choice(), main_prove(), and prove_aim().
| void clean_undo_window | ( | long | disp, | |
| long | wind | |||
| ) |
Definition at line 844 of file login.c.
References wl_stack::a, wl_stack::b, wl_choice_point::next, wl_stack::next, wl_stack::type, undo_action, and wl_choice_point::undo_point.
| long disjunct_aim | ( | ) |
| int dummy_printf | ( | char * | f, | |
| char * | s, | |||
| char * | t | |||
| ) |
| void fetch_def | ( | ptr_psi_term | u, | |
| long | allflag | |||
| ) |
Definition at line 1181 of file login.c.
References wl_triple_list::a, wl_psi_term::attr_list, wl_triple_list::b, wl_triple_list::c, clear_copy(), DEFRULES, deref_ptr, eval_copy(), i_eval_args(), int_ptr, wl_triple_list::next, NULL, prove, push2_ptr_value(), push_goal(), RMASK, SMASK, STACK, wl_psi_term::status, Traceline, wl_definition::type, and unify.
Referenced by check_type(), and type_disj_aim().
| void fetch_def_lazy | ( | ptr_psi_term | u, | |
| ptr_definition | old1, | |||
| ptr_definition | old2, | |||
| ptr_node | old1attr, | |||
| ptr_node | old2attr, | |||
| long | old1stat, | |||
| long | old2stat | |||
| ) |
Definition at line 1241 of file login.c.
References wl_triple_list::a, wl_definition::always_check, wl_psi_term::attr_list, wl_triple_list::b, wl_triple_list::c, clear_copy(), DEFRULES, deref_ptr, eval_copy(), FALSE, i_eval_args(), int_ptr, matches(), wl_triple_list::next, NULL, prove, push_goal(), push_ptr_value(), STACK, wl_psi_term::status, Traceline, and unify.
Referenced by c_project().
| void get_one_arg | ( | ptr_node | t, | |
| ptr_psi_term * | a | |||
| ) |
Definition at line 142 of file login.c.
References wl_node::data, featcmp(), find(), NULL, and one.
Referenced by c_assert_first(), c_assert_last(), c_bit_not(), c_boolpred(), c_copy_pointer(), c_copy_term(), c_freeze_inner(), c_int2string(), c_is_function(), c_is_persistent(), c_is_predicate(), c_is_sort(), c_log(), c_nonvar(), c_not(), c_parse(), c_psi2string(), c_read(), c_residList(), c_set_choice(), c_sqrt(), c_trig(), c_var(), and check_func().
| void get_one_arg_addr | ( | ptr_node | t, | |
| ptr_psi_term ** | a | |||
| ) |
| void get_two_args | ( | ptr_node | t, | |
| ptr_psi_term * | a, | |||
| ptr_psi_term * | b | |||
| ) |
Definition at line 93 of file login.c.
References wl_node::data, featcmp(), find(), wl_node::key, NULL, one, wl_node::right, and two.
Referenced by all_public_symbols(), assert_attributes(), assert_complicated_type(), assert_rule(), assert_type(), c_add(), c_alias(), c_ascii(), c_assign(), c_bit_and(), c_bit_or(), c_bk_assign(), c_call(), c_char(), c_chdir(), c_children(), c_clause(), c_close(), c_combined_name(), c_diff(), c_diff_address(), c_disj(), c_display_modules(), c_display_persistent(), c_div(), c_equal(), c_eval(), c_eval_disjunction(), c_eval_inplace(), c_exist_feature(), c_exists_choice(), c_exp(), c_feature_values(), c_features(), c_floor_ceiling(), c_funct(), c_get(), c_glb(), c_global_assign(), c_gt(), c_gtoe(), c_intdiv(), c_is_number(), c_is_value(), c_isa_main(), c_isa_subsort(), c_listing(), c_load(), c_logical_main(), c_lt(), c_ltoe(), c_lub(), c_mod(), c_module_name(), c_mresiduate(), c_mult(), c_open_in(), c_open_out(), c_page_width(), c_parents(), c_pred(), c_print_depth(), c_project(), c_put_main(), c_quote(), c_replace(), c_retract(), c_rootsort(), c_same_address(), c_set_input(), c_set_module(), c_set_output(), c_setq(), c_shift(), c_split_double(), c_string2psi(), c_string_address(), c_strip(), c_sub(), c_such_that(), c_trace(), c_trace_input(), c_undo(), c_unify_func(), c_unify_pred(), c_xor(), declare_operator(), global_error_check(), global_one(), pred_clause(), pretty_list(), pretty_psi_with_ops(), and prove_aim().
| int global_unify | ( | ) |
Referenced by global_unify_attr().
| int global_unify_attr | ( | ) |
Referenced by global_unify(), and global_unify_attr().
| long load_aim | ( | ) |
Definition at line 2149 of file login.c.
References wl_goal::a, abort_life(), assert_clause(), assert_first, wl_goal::b, wl_goal::c, CURRENT_MODULE, DEFRULES, encode_types(), eof, FACT, FALSE, file_date, find_module(), general_cut, get_attr(), input_state, input_stream, load, noisy, NULL, open_input_file(), parse(), prove, push_choice_point(), push_goal(), QUERY, restore_state(), save_state(), set_current_module(), stack_copy_psi_term(), TRUE, wl_psi_term::type, var_occurred, and var_tree.
Referenced by main_prove().
| void main_prove | ( | ) |
Definition at line 2250 of file login.c.
References wl_goal::a, wl_goal::b, backtrack(), wl_goal::c, c_what_next, clause, clause_aim(), clean_trail(), curried, cut_to, del_clause, disj, disjunct_aim(), do_currying(), do_residuation_user(), Errorline(), eval, eval_aim(), eval_cut, fail, FALSE, freeze_cut, function, GC_THRESHOLD, general_cut, goal_count, handle_interrupt(), heap_pointer, i_check_out(), implies_cut, Infoline, interrupted, load, load_aim(), main_loop_ok, match, match_aim(), memory_check(), wl_goal::next, NULL, prove, prove_aim(), release_resid(), resid_aim, resid_vars, restore_resid(), retract, show_count(), stack_pointer, stepcount, stepflag, steptrace, Traceline, TRUE, type, wl_goal::type, type_disj, type_disj_aim(), undo(), unify, unify_aim(), unify_aim_noeval(), unify_noeval, Warningline, what_next, what_next_aim(), xcount, XEVENTDELAY, and xeventdelay.
Definition at line 936 of file login.c.
References deref2_rec_eval(), featcmp(), wl_node::left, NULL, and wl_node::right.
Referenced by merge_unify().
| long no_choices | ( | ) |
| long num_choices | ( | ) |
Definition at line 1900 of file login.c.
References wl_choice_point::goal_stack, NULL, wl_goal::type, and what_next.
| long prove_aim | ( | ) |
Definition at line 1600 of file login.c.
References wl_pair_list::a, wl_goal::a, and, wl_psi_term::attr_list, wl_pair_list::b, wl_goal::b, boolpredsym, c_rule, call_handlersym, can_curry, clean_trail(), clear_copy(), wl_psi_term::coref, curried, cut, cut_to, wl_node::data, DEFRULES, deref_args, deref_ptr, do_currying(), do_residuation_user(), eval_copy(), FALSE, function, get_two_args(), goal_count, i_check_out(), i_eval_args(), wl_node::key, wl_node::left, life_or, MAX_BUILT_INS, merge(), wl_pair_list::next, wl_goal::next, NULL, one, predicate, wl_definition::protected, prove, push_choice_point(), push_goal(), push_psi_ptr_value(), quote_copy(), resid_aim, resid_vars, wl_node::right, wl_definition::rule, set_empty, STACK, stack_add_psi_attr(), STACK_ALLOC, stack_psi_term(), wl_psi_term::status, sub_type(), succeed, Traceline, tracesym, TRUE, type, wl_definition::type, wl_psi_term::type, undef, and wl_psi_term::value.
Referenced by main_prove().
Definition at line 583 of file login.c.
References wl_stack::a, wl_stack::b, wl_stack::next, STACK_ALLOC, stack_pointer, and wl_stack::type.
Referenced by check_type(), eval_aim(), and fetch_def().
| void push_choice_point | ( | goals | t, | |
| ptr_psi_term | a, | |||
| ptr_psi_term | b, | |||
| GENERIC | c | |||
| ) |
Definition at line 643 of file login.c.
References wl_goal::a, wl_goal::b, wl_goal::c, FALSE, global_time_stamp, wl_choice_point::goal_stack, wl_choice_point::next, wl_goal::next, wl_goal::pending, STACK_ALLOC, stack_pointer, wl_choice_point::stack_top, wl_choice_point::time_stamp, top, wl_goal::type, and wl_choice_point::undo_point.
Referenced by c_call(), c_disj(), c_eval_disjunction(), c_freeze_inner(), c_glb(), c_lub(), c_repeat(), c_undo(), call_once_internal(), clause_aim(), eval_aim(), load_aim(), prove_aim(), type_disj_aim(), WFInput(), and what_next_aim().
| void push_def_ptr_value | ( | ptr_psi_term | q, | |
| GENERIC * | p | |||
| ) |
Definition at line 445 of file login.c.
References wl_stack::a, assert, wl_stack::b, def_ptr, global_time_stamp, heap_pointer, int_ptr, wl_stack::next, push_ptr_value(), STACK_ALLOC, stack_pointer, wl_stack::type, and VALID_ADDRESS.
| void push_goal | ( | goals | t, | |
| ptr_psi_term | a, | |||
| ptr_psi_term | b, | |||
| GENERIC | c | |||
| ) |
Definition at line 607 of file login.c.
References wl_goal::a, wl_goal::b, wl_goal::c, FALSE, wl_goal::next, wl_goal::pending, STACK_ALLOC, and wl_goal::type.
Referenced by abort_life(), accept_internal(), all_public_symbols(), apply1_internal(), bitvector_binop_code(), bitvector_bit_code(), bitvector_unop_code(), c_add(), c_apply(), c_args(), c_boolpred(), c_call(), c_char(), c_children(), c_combined_name(), c_cond(), c_copy_pointer(), c_copy_term(), c_current_module(), c_diff_address(), c_disj(), c_div(), c_eval(), c_eval_disjunction(), c_eval_inplace(), c_exist_feature(), c_exists_choice(), c_feature_values(), c_features(), c_freeze_inner(), c_get(), c_get_choice(), c_glb(), c_int2string(), c_intdiv(), c_is_function(), c_is_predicate(), c_is_sort(), c_load(), c_localtime(), c_logical_main(), c_lub(), c_module_name(), c_mult(), c_nonvar(), c_ops(), c_page_width(), c_parents(), c_parse(), c_print_depth(), c_project(), c_psi2string(), c_quiet(), c_quote(), c_random(), c_read(), c_rootsort(), c_same_address(), c_smallest(), c_string2psi(), c_string_address(), c_sub(), c_such_that(), c_unify_func(), c_unify_pred(), c_var(), c_xor(), call_once_internal(), check_disj(), check_func(), clause_aim(), cuserid_internal(), dbmfetch_internal(), dbmfirstkey_internal(), dbmnextkey_internal(), do_currying(), errmsg_internal(), errno_internal(), eval_aim(), fetch_def(), fetch_def_lazy(), fopen_internal(), get_buffer_internal(), get_record_internal(), gethostname_internal(), int2stream_internal(), lazy_project_internal(), load_aim(), main(), make_bitvector_internal(), match_attr1(), my_wait_on_feature_internal(), pred_clause(), prove_aim(), regexp_compile_internal(), regexp_execute_internal(), set_parse_queryflag(), socket_internal(), stream2sys_stream_internal(), sys_stream2stream_internal(), unify_bool(), unify_bool_result(), unify_pterm_result(), wait_on_feature_internal(), WFInit(), WFInput(), and what_next_aim().
| void push_psi_ptr_value | ( | ptr_psi_term | q, | |
| GENERIC * | p | |||
| ) |
Definition at line 497 of file login.c.
References wl_stack::a, assert, wl_stack::b, global_time_stamp, int_ptr, wl_stack::next, psi_term_ptr, push_ptr_value(), STACK_ALLOC, stack_pointer, wl_stack::type, and VALID_ADDRESS.
Referenced by c_bk_assign(), c_global_assign(), c_open_in(), c_open_out(), c_project(), check_func(), eval_global_var(), global_unify(), make_life_form(), and prove_aim().
Definition at line 416 of file login.c.
References wl_stack::a, assert, wl_stack::b, heap_pointer, wl_stack::next, STACK_ALLOC, stack_pointer, wl_stack::type, and VALID_ADDRESS.
Referenced by append_resid(), bk_mark_quote(), c_cond(), deref_eval(), deref_rec_body(), fetch_def_lazy(), general_insert(), get_bool_value(), get_real_value(), push_def_ptr_value(), push_psi_ptr_value(), rec_replace(), release_resid_main(), residuateGoalOnVar(), type_disj_aim(), and unify_real_result().
| void push_window | ( | long | type, | |
| long | disp, | |||
| long | wind | |||
| ) |
Definition at line 562 of file login.c.
References wl_stack::a, assert, wl_stack::b, wl_stack::next, STACK_ALLOC, wl_stack::type, and undo_action.
| void reset_stacks | ( | ) |
| void show_count | ( | ) |
Definition at line 1136 of file login.c.
References end_time, goal_count, heap_pointer, mem_base, mem_limit, NOTQUIET, stack_info(), stack_pointer, and verbose.
Referenced by handle_interrupt(), main_prove(), and what_next_aim().
| void start_chrono | ( | ) |
| ptr_choice_point topmost_what_next | ( | ) |
| void type_disj_aim | ( | ) |
Definition at line 1799 of file login.c.
References wl_goal::a, wl_definition::always_check, wl_psi_term::attr_list, wl_goal::b, def_ptr, FALSE, fetch_def(), wl_definition::keyword, wl_int_list::next, NULL, push_choice_point(), push_ptr_value(), wl_psi_term::status, wl_keyword::symbol, Traceline, wl_psi_term::type, type_disj, and wl_int_list::value.
Referenced by main_prove().
| void undo | ( | ptr_stack | limit | ) |
Definition at line 698 of file login.c.
References wl_stack::a, wl_stack::b, destroy_window, hide_subwindow, hide_window, wl_stack::next, show_subwindow, show_window, wl_stack::type, and undo_action.
Referenced by abort_life(), backtrack(), main(), main_prove(), undo_actions(), WFInput(), and what_next_aim().
| void undo_actions | ( | ) |
| long unify_aim | ( | ) |
| long unify_aim_noeval | ( | ) |
| long unify_body | ( | ) |
| long what_next_aim | ( | ) |
Definition at line 1997 of file login.c.
References wl_goal::a, assert_clause(), assert_first, wl_goal::b, begin_terminal_io(), wl_goal::c, current_module, cut, DEFRULES, encode_types(), end_terminal_io(), eof, EOLN, FACT, FALSE, Infoline, level, MAX_LEVEL, wl_module::module_name, no_choices(), NOTQUIET, NULL, parse(), print_variables(), prompt, PROMPT, prompt_buffer, prove, push_choice_point(), push_goal(), put_back_char(), QUERY, read_char(), release_resid(), reset_stacks(), reset_step(), show_count(), stack_copy_psi_term(), start_chrono(), stdin_cleareof(), TRUE, TRUEMASK, wl_psi_term::type, undo(), user_module, var_occurred, what_next, and what_next_cut().
Referenced by main_prove().
| long what_next_cut | ( | ) |
Definition at line 53 of file login.c.
Referenced by all_public_symbols(), c_add(), c_alias(), c_append_file(), c_apply(), c_args(), c_ascii(), c_assert_first(), c_assert_last(), c_assign(), c_bit_and(), c_bit_not(), c_bit_or(), c_bk_assign(), c_boolpred(), c_call(), c_char(), c_chdir(), c_children(), c_clause(), c_close(), c_combined_name(), c_concatenate(), c_cond(), c_copy_pointer(), c_copy_term(), c_cputime(), c_current_module(), c_declaration(), c_delay_check(), c_deref_length(), c_diff(), c_diff_address(), c_disj(), c_display_modules(), c_display_persistent(), c_div(), c_dynamic(), c_equal(), c_eval(), c_eval_disjunction(), c_eval_inplace(), c_exist_feature(), c_exists(), c_exists_choice(), c_exp(), c_feature_values(), c_features(), c_floor_ceiling(), c_freeze_inner(), c_funct(), c_get(), c_get_choice(), c_get_raw(), c_glb(), c_global(), c_global_assign(), c_gt(), c_gtoe(), c_in_raw(), c_initrandom(), c_int2string(), c_intdiv(), c_is_function(), c_is_number(), c_is_persistent(), c_is_predicate(), c_is_sort(), c_is_value(), c_isa_main(), c_isa_subsort(), c_listing(), c_load(), c_localtime(), c_log(), c_logical_main(), c_lt(), c_ltoe(), c_lub(), c_maxint(), c_mod(), c_module_access(), c_module_name(), c_mresiduate(), c_mult(), c_non_strict(), c_nonvar(), c_not(), c_not_implemented(), c_op(), c_open_in(), c_open_module(), c_open_out(), c_ops(), c_page_width(), c_parents(), c_parse(), c_persistent(), c_pred(), c_print_codes(), c_print_depth(), c_private(), c_private_feature(), c_project(), c_psi2string(), c_public(), c_put_main(), c_quiet(), c_quote(), c_random(), c_read(), c_realtime(), c_repeat(), c_replace(), c_reset_window_flag(), c_residList(), c_retract(), c_rootsort(), c_same_address(), c_set_choice(), c_set_input(), c_set_module(), c_set_output(), c_setq(), c_shift(), c_smallest(), c_split_double(), c_sqrt(), c_static(), c_step(), c_string2psi(), c_string_address(), c_string_length(), c_strip(), c_sub(), c_sub_string(), c_succeed(), c_such_that(), c_tprove(), c_trace(), c_trace_input(), c_trig(), c_undo(), c_unify_func(), c_unify_pred(), c_var(), c_verbose(), c_warning(), c_window_flag(), c_xor(), call_primitive(), check(), deref_args_eval(), deref_eval(), deref_rec_eval(), eval_aim(), generic_write(), and match_aim().
| long assert_first |
Definition at line 63 of file login.c.
Referenced by add_rule(), c_assert_first(), c_assert_last(), load_aim(), main(), WFInput(), and what_next_aim().
| long assert_ok |
Definition at line 64 of file login.c.
Referenced by add_rule(), assert_clause(), assert_complicated_type(), assert_type(), c_assert_first(), c_assert_last(), main(), and WFInput().
Definition at line 45 of file login.c.
Referenced by c_call(), c_exists_choice(), c_freeze_inner(), c_get_choice(), c_set_choice(), call_once_internal(), check(), check_goal_stack(), check_psi_term(), check_resid(), check_special_addresses(), copy(), depth_cs(), eval_aim(), fail_all(), init_system(), pchoices(), and WFInput().
| long clean_iter = 0 |
| long clean_succ = 0 |
| struct tms start_time end_time |
| unsigned long global_time_stamp = INIT_TIME_STAMP |
Definition at line 50 of file login.c.
Referenced by c_get_choice(), copy(), distinct_copy(), heap_copy_psi_term(), heap_psi_term(), push_choice_point(), push_def_ptr_value(), push_psi_ptr_value(), real_stack_psi_term(), stack_copy_psi_term(), and stack_psi_term().
| long goal_count |
Definition at line 56 of file login.c.
Referenced by main(), main_prove(), prove_aim(), show_count(), and WFInput().
Definition at line 53 of file login.c.
Referenced by c_cond(), check(), depth_gs(), deref_args_eval(), deref_eval(), deref_rec_eval(), do_currying(), do_residuation_user(), fail_all(), init_system(), release_resid_main(), and WFInput().
| long ignore_eff |
| long main_loop_ok |
| long more_u_attr |
| long more_v_attr |
| char prompt_buffer[PROMPT_BUFFER] |
Definition at line 44 of file login.c.
Referenced by bounds_undo_stack(), check(), check_special_addresses(), depth_ts(), eval_global_var(), fail_all(), init_system(), main(), print_undo_stack(), WFInit(), and WFInput().
char vcid[] = "$Id: login.c,v 1.4 1995/01/14 00:25:33 duchier Exp $" [static] |
| long xcount |
| long xeventdelay |
1.5.4