Programmer 7500

home *** CD-ROM | disk | FTP | other *** search

/ Programmer 7500 / MAX_PROGRAMMERS.iso / CLIPPER / MISC / FUZZY.ZIP / PROVER.B < prev next >

Wrap

Text File | 1986-11-30 | 37.0 KB | 973 lines

------------------------------------------------------------------------------- -- -- -- Library Unit: Prover -- Prove or process user requests -- -- -- -- Author: Bradley L. Richards -- -- -- -- Version Date Notes . . . -- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- -- 1.0 - - - - - Never existed. First version implemented after -- -- Parser et al reached version 2.0 -- -- 2.0 20 Jun 86 Initial Version -- -- 2.05 13 Jul 86 Split into separate spec and package files -- -- 2.1 21 Jul 86 Demonstration version -- initial predicates -- -- implemented; initial debugging completed -- -- 2.2 28 Jul 86 Initial operational version -- 20 predicates -- -- implemented, plus lots of squashed bugs -- -- 2.3 19 Aug 86 Use AVL trees for rule_base, add many reserved -- -- predicates, and split output routines into -- -- package print_stuff. -- -- 2.4 31 Aug 86 Split do_reserved into separate file -- -- 2.5 1 Sep 86 Split execute into separate file -- -- 3.0 10 Oct 86 Final thesis product -- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- -- -- -- Description: This package contains only one visible routine: Prove. -- -- Prove is nothing but a shell for the primary resolution routine -- -- Seek. After Proveand the AVL comparison routines, all routines -- -- appear in alphabetical order. -- -- -- -- Seek (and many other routines herein) is a recursive routine. It -- -- accepts an initial goal_tree from Prove and resolves a single -- -- predicate. It then passes the revised goal_tree (possibly -- -- heavily modified due to new goals, etc.) to a recursive call of -- -- itself. -- -- -- -- Other important routines: Unify attempts to unify two predicates -- -- and their arguments, creating bindings as necessary. Do_reserved -- -- processes reserved predicates. Execute executes operators of all -- -- types (arithmetic, comparison, logical). -- -- -- -- Most of the routines in this package are recursive. In order -- -- to successfully backtrack, it is critical that each time a routine -- -- is called it creates a local copy of anything it plans to modify -- -- Two important examples are the goal_tree and the binding list. -- -- -- ------------------------------------------------------------------------------- -- -- -- Package Body -- -- -- ------------------------------------------------------------------------------- package body prover is aborting, cutting, trace_mode : boolean := false; cutting_level : integer; current_truth : float; quote : constant boolean := true; no_quote : constant boolean := false; threshold : fuzzy_values; rule_base : tree_ptr := init_tree; -- -- Specifications for all procedures. Forward referencing all procedures -- saves the headache of figuring out which ones need forward references. -- procedure find_bond(var_name : name_ptr; var_level : natural; bindings : binding_list; value : out argument_ptr; value_level : out integer); procedure find_first(goal_tree, modify, place : in out AST_ptr; bindings : in out binding_list; res_level : in out natural; failed : in out boolean); procedure insert(goal_tree, replace : in out AST_ptr; modify, new_goals : in AST_ptr; level : natural); procedure lookup(arg_node : AST_ptr; level : natural; bindings : binding_list; value_out : out argument_ptr; level_out : out integer); procedure lookup(args : argument_ptr; level : natural; bindings : binding_list; value_out : out argument_ptr; level_out : out integer ); procedure release(bindings, stop : binding_list); function seek(goal_tree_in : in AST_ptr; bindings_in : binding_list; level : natural) return boolean; procedure start_prover; procedure stop_prover; procedure trace(set_trace : boolean); procedure trace_entry(pred, goal_tree : AST_ptr; bindings : binding_list; level, res_level : natural; failed : in out boolean); procedure trace_exit(pred, goal_tree : AST_ptr; bindings : binding_list; level, res_level : natural; failed : in out boolean); procedure trace_fail(pred, goal_tree : AST_ptr; bindings : binding_list; level, res_level : natural; failed : in out boolean); procedure trace_print(goal_tree : AST_ptr; bindings : binding_list; failed : in out boolean); procedure unify(predicate1, predicate2 : AST_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean); procedure unify_list(predicate1, predicate2 : p_list_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean); procedure unify_arg(arg_node1, arg_node2 : AST_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean); procedure unify_arg(arg1, arg2 : argument_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean); -- -- Forward references for separate routines. -- -- Do_reserved is in file do_reservedB.a -- procedure do_reserved(pred, goal_tree : AST_ptr; result_node : out AST_ptr; bindings : in out binding_list; level : natural; failed : in out boolean); -- -- Execute is in file executeB.a -- procedure execute(operator : in out AST_ptr; bindings : in out binding_list; level : natural; failed : in out boolean); -- -- These print routines are in file print_stuffB.a -- procedure print_argument( argument : argument_ptr; bindings : binding_list; level : natural; quotes : boolean ); procedure print_arguments( in_arguments : argument_ptr; bindings : binding_list; level : natural; quotes : boolean ); procedure print_AST( ast_node : AST_ptr; indent : integer ); procedure print_bin_op( operator : binary_operators ); procedure put_bin_op( operator : binary_operators ); procedure print_bindings(bindings_in : binding_list; indent : natural ); procedure print_clause( clause : AST_ptr ); procedure print_list( in_list : p_list_ptr; bindings : binding_list; level : natural; quotes : boolean ); procedure print_list_tail( in_list : p_list_ptr; bindings : binding_list; level : natural; quotes : boolean ); procedure print_predicate( node : AST_ptr; indent : natural; bindings : binding_list; level : natural ); procedure print_reserved( node : AST_ptr; indent : natural; bindings : binding_list; level : natural ); procedure put_reserved( reserved_predicate : reserved_predicates ); procedure print_result( bindings_in : binding_list; done : out boolean); procedure print_un_op(operator : unary_operators); procedure put_un_op(operator : unary_operators); procedure space(number : natural); -- -- Routines for processing reserved words are maintained in a separate -- file. They are not kept as a separate package because their processing -- really is an implicit part of the Prover's task. -- procedure do_reserved(pred, goal_tree : AST_ptr; result_node : out AST_ptr; bindings : in out binding_list; level : natural; failed : in out boolean) is separate; -- -- Routines for executing operators are kept in a separate file. The real -- reason for all these separate files is to keep individual file size -- (and compilation time) down, and to enhance readability of the listings. -- procedure execute(operator : in out AST_ptr; bindings : in out binding_list; level : natural; failed : in out boolean) is separate; -- -- Print routines are maintained in a separate file -- procedure print_argument( argument : argument_ptr; bindings : binding_list; level : natural; quotes : boolean ) is separate; procedure print_arguments( in_arguments : argument_ptr; bindings : binding_list; level : natural; quotes : boolean ) is separate; procedure print_AST( ast_node : AST_ptr; indent : integer ) is separate; procedure print_bin_op( operator : binary_operators ) is separate; procedure put_bin_op( operator : binary_operators ) is separate; procedure print_bindings(bindings_in : binding_list; indent : natural ) is separate; procedure print_clause( clause : AST_ptr ) is separate; procedure print_list( in_list : p_list_ptr; bindings : binding_list; level : natural; quotes : boolean ) is separate; procedure print_list_tail( in_list : p_list_ptr; bindings : binding_list; level : natural; quotes : boolean ) is separate; procedure print_predicate( node : AST_ptr; indent : natural; bindings : binding_list; level : natural ) is separate; procedure print_reserved( node : AST_ptr; indent : natural; bindings : binding_list; level : natural ) is separate; procedure put_reserved(reserved_predicate : reserved_predicates) is separate; procedure print_result( bindings_in : binding_list; done : out boolean) is separate; procedure print_un_op(operator : unary_operators) is separate; procedure put_un_op(operator : unary_operators) is separate; procedure space(number : natural) is separate; -- -- Procedures for use by the AVL package when comparing clauses -- function clause_equal( a, b : AST_ptr ) return boolean is begin return(a.head.name.name = b.head.name.name); end clause_equal; function clause_less_than( a, b : AST_ptr ) return boolean is begin return(a.head.name.name < b.head.name.name); end clause_less_than; -- -- Prove -- accept a goal from the calling unit and process it. -- procedure prove( goal : in AST_ptr ) is begin -- -- goal must be an AST_ptr which points to a predicate or reserved -- predicate of some sort. Reserved predicates require special -- processing of some sort. -- start_prover; if seek(goal, null, 1) then put_line("yes"); else put_line("no"); end if; stop_prover; end prove; -- -- Find_bond -- Given a variable name and its level, return what it is -- bound to. If it is not bound, return null. -- procedure find_bond( var_name : name_ptr; var_level : natural; bindings : binding_list; value : out argument_ptr; value_level : out integer ) is binding : binding_list := bindings; begin while binding /= null loop if binding.name.name = var_name.name and binding.level = var_level then -- -- we've found the binding -- value := binding.value; value_level := binding.value_level; exit; end if; binding := binding.next_binding; end loop; if binding = null then -- not found value := null; value_level := 0; end if; end find_bond; -- -- Find_first -- Given a goal_tree, do a pre-order walk through it looking -- for the first predicate which still needs resolved. When -- walking the tree, execute any operators which are ready -- (i.e. have their operands defined). -- Comparison and arithmetic operators will always be -- executed when found. Logic operators will be executed only -- if their operands have been resolved to fuzzy_value nodes. -- On return, "place" points to the unresolved -- predicate if one was found. If this predicate is not at -- the top of the tree then "modify" points to its parent. -- procedure find_first(goal_tree, modify, place : in out AST_ptr; bindings : in out binding_list; res_level : in out natural; failed : in out boolean ) is temp : AST_ptr; temp_level : natural; begin if goal_tree.node_type = fuzzy_value then current_truth := goal_tree.fuzzy_num; place := null; -- at the bottom of the tree elsif goal_tree.node_type = threshold_marker then current_truth := goal_tree.fuzzy_value; place := null; -- at the bottom of the tree elsif (goal_tree.node_type = predicate) or (goal_tree.node_type = reserved_predicate) then place := goal_tree; modify := null; elsif goal_tree.node_type = unary_operator then place := null; if goal_tree.unary_op = rw_not then -- a logic operator find_first(goal_tree.operand,modify,place, bindings, res_level, failed); end if; if (place = null) and (not failed) then -- operand is ready, so execute execute(goal_tree, bindings, res_level, failed); elsif (modify = null) and (not failed) then -- unresolved predicate is the -- child of "goal_tree" modify := goal_tree; end if; -- otherwise just pass back what was found lower in goal_tree elsif goal_tree.node_type = binary_operator then -- -- Don't look below comparison or arithmetic operators -- place := null; if goal_tree.binary_op in binary_logic_operators then find_first(goal_tree.left_operand,modify,place,bindings,res_level, failed); end if; if (place = null) and (not failed) then -- left operand is resolved if goal_tree.binary_op in binary_logic_operators then find_first(goal_tree.right_operand,modify,place,bindings,res_level, failed); end if; if (place = null) and (not failed) then -- both operands resolved execute(goal_tree, bindings, res_level, failed); elsif (modify = null) and (not failed) then modify := goal_tree; end if; elsif (modify = null) and (not failed) then modify := goal_tree; end if; elsif goal_tree.node_type = resolution_marker then temp_level := goal_tree.level; threshold := goal_tree.old_threshold; find_first(goal_tree.subgoals, modify, place, bindings, temp_level, failed); if (place = null) and (not failed) then -- throw away the marker node threshold := goal_tree.old_threshold; -- but first restore threshold temp := goal_tree; goal_tree := goal_tree.subgoals; release(temp, temp.subgoals); if goal_tree.node_type = threshold_marker then -- Cannot allow upward propogation of thresholds temp := new AST'(fuzzy_value, goal_tree.fuzzy_value); release(goal_tree, null); goal_tree := temp; end if; elsif (not failed) then if goal_tree.level /= temp_level then -- found a new level lower down res_level := temp_level; else -- this marker node is the lowest one res_level := goal_tree.level; end if; if modify = null then modify := goal_tree; end if; end if; else -- we're apparently at a leaf node in the depths of the tree place := null; end if; end find_first; procedure insert( goal_tree, replace : in out AST_ptr; modify, new_goals : in AST_ptr; level : natural) is goals : AST_ptr := new AST'(resolution_marker, level, threshold, new_goals); begin if modify = null then -- modify top of tree goal_tree := goals; elsif modify.node_type = unary_operator then modify.operand := goals; elsif modify.node_type = binary_operator then if modify.left_operand = replace then modify.left_operand := goals; else -- right_operand modify.right_operand := goals; end if; elsif modify.node_type = resolution_marker then modify.subgoals := goals; else error(no_pointer,"insert: Modify points to invalid node type"); end if; replace := goals; end insert; procedure lookup( arg_node : AST_ptr; level : natural; bindings : binding_list; value_out : out argument_ptr; level_out : out integer) is template : constant argument_ptr := new argument'(variable, null, null); begin case arg_node.node_type is when character_lit => value_out := new argument'(character_lit, null, arg_node.char); level_out := level; when float_num => value_out := new argument'(float_num, null, arg_node.fp_num); level_out := level; when integer_num => value_out := new argument'(integer_num, null, arg_node.int_num); level_out := level; when predicate => value_out := new argument'(predicate, null, arg_node.name, arg_node.p_arguments); level_out := level; when variable => template.v_name := arg_node.var_name; lookup(template, level, bindings, value_out, level_out); when fuzzy_value => value_out := new argument'(float_num, null, arg_node.fuzzy_num); level_out := level; when others => error(no_pointer, "invalid node to lookup"); end case; end lookup; procedure lookup( args : argument_ptr; level : natural; bindings : binding_list; value_out : out argument_ptr; level_out : out integer) is value : argument_ptr; value_level : natural; begin if args.is_a /= variable then value_out := args; level_out := level; else -- it is a variable if args.v_name = null then -- it's anonymous value_out := args; level_out := level; else find_bond(args.v_name, level, bindings, value, value_level); if value /= null then -- it does have a binding, so go look IT up lookup(value, value_level, bindings, value_out, level_out); else value_out := args; level_out := level; end if; end if; end if; end lookup; -- -- Release -- Return memory to the system using UNCHECKED_DEALLOCATION. -- Release routines are necessary since the current Verdix -- Compiler does not include an automatic garbage collector. -- Releases all items within the structure UP TO the "stop" -- value. -- procedure release(bindings, stop : binding_list) is ptr : binding_list := bindings; rid : binding_list; begin while ptr /= stop loop rid := ptr; ptr := ptr.next_binding; free_binding(rid); end loop; end release; -- -- Seek -- Attempt to justify the goals based on the rule_base. This is -- a highly recursive routine. Backtracking is accomplished by -- returning with the value false. Returning with the value true -- indicates a successful resolution. -- function seek(goal_tree_in : in AST_ptr; bindings_in : binding_list; level : natural) return boolean is db_ptr : AST_ptr; modify, pred, replace : AST_ptr := null; goal_tree, new_goals : AST_ptr; bindings_ff : binding_list := bindings_in; bindings : binding_list; been_here, done, failed : boolean := false; is_NOT, unified : boolean; res_level : natural := 0; template : constant AST_ptr := new AST'(implication, new AST'(predicate, null, null), null, null, null); function replicate (in_tree : AST_ptr) return AST_ptr is begin if in_tree = null then return null; else case in_tree.node_type is when implication => return new AST'(implication, replicate(in_tree.head), replicate(in_tree.tail), in_tree.prev, in_tree.next); when binary_operator => return new AST'(binary_operator, in_tree.binary_op, replicate(in_tree.left_operand), replicate(in_tree.right_operand)); when unary_operator => return new AST'(unary_operator, in_tree.unary_op, replicate(in_tree.operand)); when resolution_marker => return new AST'(resolution_marker, in_tree.level, in_tree.old_threshold, replicate(in_tree.subgoals)); when others => return new AST'(in_tree.all); end case; end if; end replicate; begin -- seek -- -- Since we plan to modify the goal tree, we need our own local copy -- to allow successful backtracking -- goal_tree := replicate(goal_tree_in); -- -- Do a pre-order walk through the goal-tree looking for a predicate to -- resolve. Enroute execute any operators we can. In some cases such -- as "=" this may modify the bindings. On return, predicate points to -- the predicate needing resolution, and modify points to its parent -- find_first(goal_tree, modify, pred, bindings_ff, res_level, failed); -- -- executing comparators may have changed bindings, so save the _ff version -- bindings := bindings_ff; if current_truth < threshold then failed := true; end if; if (pred = null) and (not failed) then -- no more unresolved predicates if goal_tree.node_type = fuzzy_value then print_result(bindings, done); else raise prover_error; end if; elsif not failed then replace := pred; while (not done) and (not failed) loop if trace_mode then trace_entry(pred, goal_tree, bindings, level, res_level, failed); exit when aborting; end if; if pred.node_type = reserved_predicate then if been_here then failed := true; -- can never resatisfy built-in predicates if pred.predicate = cut then cutting := true; cutting_level := res_level; end if; else do_reserved(pred,goal_tree, new_goals, bindings, res_level, failed); if pred.predicate /= rw_repeat then been_here := true; end if; end if; else -- -- Search through the database for something which unifies with it -- if not been_here then template.head.name := pred.name; db_ptr := fetch_node(rule_base, template); been_here := true; end if; while db_ptr /= null loop unify(pred, db_ptr.head, res_level, level, bindings, unified); exit when unified; -- -- We may have made a few bindings before running into a dead end -- release(bindings, bindings_ff); bindings := bindings_ff; db_ptr := db_ptr.next; end loop; if db_ptr = null then -- we failed to unify it with anything failed := true; else current_truth := 1.0; -- successful resolution new_goals := db_ptr.tail; db_ptr := db_ptr.next; -- advance to next in case of backtracking end if; end if; -- -- Failed requires special logic. In Prolog the NOT operator affects -- its operand immediately; e.g. if the operand can be resolved, NOT -- makes it appear as though it could not be resolved. With the fuzzy -- values in Fuzzy Prolog this becomes a significant exception to the -- logic. To maintain compatibility with Prolog, Seek is modified to -- process predicates who parent is a NOT specially. If the parent -- fails, the result becomes fuzzy(0.0) for a single pass through the -- logic (the while loop catches the failure on the next pass). If the -- child succeeds with resolution (or do_reserved), the complement of -- the current truth value is immediately compared with the threshold -- to see if processing should be allowed to continue. -- is_NOT := (modify /= null) and then (modify.node_type = unary_operator) and then (modify.unary_op = rw_not); if (failed and (not is_NOT)) or ((not failed) and then is_NOT and then (pred.node_type = reserved_predicate) and then (pred.predicate /= rw_call)) then done := false; if trace_mode then if failed then trace_fail(pred, goal_tree, bindings, level, res_level, failed ); else trace_exit(pred, goal_tree, bindings, level, res_level, failed ); end if; end if; exit; else if failed then -- we are underneath a NOT operator current_truth := 1.0; -- like successful resolution new_goals := new AST'(fuzzy_value, 0.0); -- which NOT will invert end if; -- -- Insert the new goals associated with this beast into the goal tree -- insert(goal_tree, replace, modify, new_goals, level); done := seek(goal_tree, bindings, (level+1)); exit when aborting; if trace_mode then if failed then trace_fail(pred, goal_tree, bindings, level, res_level, failed ); else trace_exit(pred, goal_tree, bindings, level, res_level, failed ); end if; exit when aborting; -- -- restore the goal tree so that trace_entry prints meaningful info -- insert(goal_tree, replace, modify, pred, level); end if; if pred.node_type = reserved_predicate then -- -- new_goals was constructed, and should now be discarded -- if trace_mode then release(new_goals, null); -- partial release else release(replace, null); -- full release end if; end if; -- -- We've appended bindings to the front of the binding list. Release -- these, but don't release any that were in bindings_ff -- release(bindings, bindings_ff); if cutting then if res_level >= cutting_level then -- yes, it means us exit; else cutting := false; exit; -- can't resatisfy this predicate end if; end if; bindings := bindings_ff; end if; end loop; end if; -- -- The goal_tree is drastically altered as predicates are resolved and -- operators executed. Hence the need for our own local copy of the -- complete AST structure which is the goal_tree. However, replicate -- does not copy any structure referenced by the goal_tree (e.g. string -- records and argument lists); rather it just points to the existing -- ones. It is important that these items not be released when the local -- copy of the goal tree is discarded. Also, when adding goals to the -- tree as a result of resolution, rather than making an immediate copy -- of these, a pointer into the rule_base is used. It would be disastrous -- to destroy part of the rule base, so this part of the local goal_tree -- (new_goals and lower) must not be released. release(goal_tree, new_goals); -- we're done with our goal_tree release(pred, null); -- a divorced segment of our goal_tree -- -- Release all bindings created by this routine, but don't touch any -- that were present when we were called -- release(bindings, bindings_in); return done; end seek; procedure start_prover is begin current_truth := 1.0; threshold := 0.1; -- default value cutting := false; aborting := false; end start_prover; procedure stop_prover is begin null; end stop_prover; procedure trace( set_trace : boolean ) is begin trace_mode := set_trace; end trace; procedure trace_entry( pred, goal_tree : AST_ptr; bindings : binding_list ; level, res_level : natural; failed : in out boolean ) is value : float; begin new_line; put(level,4); put('('); put(res_level,4); put(')'); put(": "); put("Entering "); if pred.node_type = predicate then print_predicate(pred, 0, bindings, res_level); else -- reserved_predicate print_reserved(pred, 0, bindings, res_level); end if; space(13); put("Current truth/threshold: "); put(current_truth); put('/'); put(threshold); new_line; trace_print(goal_tree, bindings, failed); end trace_entry; procedure trace_exit( pred, goal_tree : AST_ptr; bindings : binding_list ; level, res_level : natural; failed : in out boolean ) is value : float; begin put(level,4); put('('); put(res_level,4); put(')'); put(": "); put("Exiting "); if pred.node_type = predicate then print_predicate(pred, 0, bindings, res_level); else -- reserved_predicate print_reserved(pred, 0, bindings, res_level); end if; space(13); put("Current truth/threshold: "); put(current_truth); put('/'); put(threshold); new_line; trace_print(goal_tree, bindings, failed); end trace_exit; procedure trace_fail( pred, goal_tree : AST_ptr; bindings : binding_list ; level, res_level : natural; failed : in out boolean ) is begin put(level,4); put('('); put(res_level,4); put(')'); put(": "); put("Fail "); if pred.node_type = predicate then print_predicate(pred, 0, bindings, res_level); else -- reserved_predicate print_reserved(pred, 0, bindings, res_level); end if; space(13); put("Current truth/threshold: "); put(current_truth); put('/'); put(threshold); new_line; trace_print(goal_tree, bindings, failed); end trace_fail; procedure trace_print( goal_tree : AST_ptr; bindings : binding_list; failed : in out boolean ) is ans : string(1..70); length : integer; begin loop put("Trace -> "); get_line(ans, length); if length = 0 then exit; end if; case ans(1) is when ' ' | 'C' | 'c' => exit; when 'A' | 'a' => aborting := true; failed := true; exit; when 'F' | 'f' => failed := true; exit; when 'B' | 'b' => put_line("Current bindings are"); print_bindings(bindings, 4); when 'G' | 'g' => put_line("Current goal tree is"); print_AST(goal_tree, 4); when 'H' | 'h' | '?' => put_line("Trace commands are"); put_line(" <c/r>, <space>, or continue: continue execution"); put_line(" abort: abort current proof and return to prompt"); put_line(" bindings: print current binding list"); put_line(" fail: fail current goal and backtrack"); put_line(" goals: print current goal tree"); put_line(" help or ?: print this menu"); put_line(" notrace: turn off trace mode"); put_line(" truth: print current truth value and threshold"); new_line; when 'N' | 'n' => trace_mode := false; exit; when 'T' | 't' => put("Current truth/threshold: "); put(current_truth); put('/'); put(threshold); new_line; when others => put_line("Invalid command; enter ? for help"); end case; end loop; end trace_print; procedure unify(predicate1, predicate2 : AST_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean) is args1 : argument_ptr := predicate1.p_arguments; args2 : argument_ptr := predicate2.p_arguments; value1, value2 : argument_ptr; level1, level2 : natural; matched : boolean := true; begin if predicate1.name.name = predicate2.name.name then -- there's a chance while (args1 /= null) and matched loop if args2 = null then matched := false; else unify_arg(args1, args2, res_level, level, bindings, matched); args1 := args1.next_arg; args2 := args2.next_arg; end if; end loop; if args2 /= null then matched := false; end if; unified := matched; end if; end unify; procedure unify_list(predicate1, predicate2 : p_list_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean) is list1 : p_list_ptr := predicate1; list2 : p_list_ptr := predicate2; template : constant argument_ptr := new argument(prolog_list); matched : boolean := true; begin if list1 = null then if list2 = null then matched := true; else matched := false; end if; end if; while (list1 /= null) and matched loop if list2 = null then matched := false; else unify_arg(list1.elt, list2.elt, res_level, level, bindings, matched); if matched then if list1.has_tail then if list2.has_tail then unify_arg(list1.tail,list2.tail,res_level,level,bindings,matched); else template.list := list2.next_elt; unify_arg(list1.tail,template,res_level,level,bindings,matched); end if; exit; elsif list2.has_tail then template.list := list1.next_elt; unify_arg(template,list2.tail,res_level,level,bindings,matched); exit; else list1 := list1.next_elt; list2 := list2.next_elt; end if; end if; end if; end loop; if matched and (list1 = null) and (list2 /= null) then matched := false; end if; unified := matched; end unify_list; procedure unify_arg(arg_node1, arg_node2 : AST_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean) is temp_1, temp_2 : argument_ptr; begin case arg_node1.node_type is when character_lit => temp_1 := new argument'(character_lit, null, arg_node1.char); when variable => temp_1 := new argument'(variable, null, arg_node1.var_name); when integer_num => temp_1 := new argument'(integer_num, null, arg_node1.int_num); when float_num => temp_1 := new argument'(float_num, null, arg_node1.fp_num); when fuzzy_value => temp_1 := new argument'(float_num, null, arg_node1.fuzzy_num); when predicate => temp_1 := new argument'(predicate, null, arg_node1.name, arg_node1.p_arguments); when others => error(no_pointer, "invalid node to unify"); end case; case arg_node2.node_type is when character_lit => temp_2 := new argument'(character_lit, null, arg_node2.char); when variable => temp_2 := new argument'(variable, null, arg_node2.var_name); when integer_num => temp_2 := new argument'(integer_num, null, arg_node2.int_num); when float_num => temp_2 := new argument'(float_num, null, arg_node2.fp_num); when fuzzy_value => temp_2 := new argument'(float_num, null, arg_node2.fuzzy_num); when predicate => temp_2 := new argument'(predicate, null, arg_node2.name, arg_node2.p_arguments); when others => error(no_pointer, "invalid node to unify"); end case; unify_arg(temp_1, temp_2, level, level, bindings, unified); end unify_arg; procedure unify_arg(arg1, arg2 : argument_ptr; res_level, level : natural; bindings : in out binding_list; unified : out boolean) is value1, value2 : argument_ptr; level1, level2 : natural; template1, template2 : AST_ptr := new AST'(predicate, null, null); begin lookup(arg1, res_level, bindings, value1, level1); lookup(arg2, level, bindings, value2, level2); if (value1.is_a = variable) then if value1.v_name /= null then -- not anonymous if not ( (value2.is_a = variable) and then (value2.v_name = null) ) then bindings := new binding'(value1.v_name,level1,value2,level2,bindings); end if; end if; unified := true; elsif value2.is_a = variable then if value2.v_name /= null then -- not anonymous bindings := new binding'(value2.v_name, level2, value1, level1, bindings); end if; unified := true; elsif value1.is_a = value2.is_a then case value1.is_a is when character_lit => unified := (value1.char = value2.char); when predicate => -- unify functors if value1.name.name = value2.name.name then -- there's a chance template1.name := value1.name; template1.p_arguments := value1.p_arguments; template2.name := value2.name; template2.p_arguments := value2.p_arguments; unify(template1, template2, level1, level2, bindings, unified); else unified := false; end if; when float_num => unified := (value1.fp_num = value2.fp_num); when integer_num => unified := (value1.int_num = value2.int_num); when prolog_list => unify_list(value1.list, value2.list, level1, level2, bindings, unified); when variable => -- something is seriously wrong error(no_pointer, "System error in Unify_Arg"); unified := false; end case; else unified := false; end if; end unify_arg; end prover;