% ============================================================ % Generate *all* solution labels. % ============================================================ % 08-04-98 Switches off all early label failure then generates % and shows all normal labels for a proof net. % Because of the involved computational price, it is % mostly useful as a debugging tool for grammar % fragments which allows you to spot unwanted % alternative solutions. :- format1('1. === Retracting Mode Declarations~n',[]), retract_all_decls, format1('2. === Disabling Early Failure~n',[]), assert(lazy_dl(_)), assert(lazy_dr(_)), assert(lazy_unpack(_)). normalize(Node,Answer) :- create_rewrite_window, my_tk_interpreter(Interp), tcl_eval(Interp,'set rewritestate $defaultrewrite',_), display_label(Node,0), tcl_eval(Interp,'.stats.txt configure -text "Rewriting"',_), tcl_eval(Interp,'incr labelgen',_), findall(Normal,normalize_all(Node,Normal),Ns), tcl_eval(Interp,'.stats.txt configure -text "Linking" if {[winfo exists .rewrite]} { .rewrite.c dtag node .rewrite.exit configure -state disabled }',_), ( select(Answer,Ns,Ms), normal(Answer) -> format('Solution:~n~p~nAlternatives:~n',[Answer]), as_portray_list(Ms), display_label(Answer,0), length(Ms,L), retract('alternatives found'(M0)), M is M0+L, assert('alternatives found'(M)) ; format('Failed:~n',[]), as_portray_list(Ns), fail ). normalize_all(Node,Answer) :- breadth_star_all([],1,[Node|B],B,node(Node,0,empty,empty),Answer). breadth_star_all([],N0,[Node|F],B,Closed,Answer) :- N0 > 0, N is N0-1, my_tk_interpreter(Interp), tcl_eval(Interp,'incr labelcount',_), ( normal_all(Node), Answer = Node ; children(Node,Children), union1(Children,Closed,Closed1,Children1,[]), breadth_star_all(Children1,N,F,B,Closed1,Answer) ). breadth_star_all([X|Xs],N0,F,[X|B],Closed,Answer) :- N is N0+1, my_tk_interpreter(Interp), tcl_eval(Interp,'incr labelgen',_), breadth_star_all(Xs,N,F,B,Closed,Answer). normal_all(_-_). normal_all(p(I,A,B)) :- external(I), normal_all(A), normal_all(B). normal_all(zip(I,A)) :- external_dia(I), normal_all(A). init(X,Goal) :- garbage_collect, my_tk_interpreter(Interp), tcl_eval(Interp,'set solutionsfound 0',_), tcl_eval(Interp,'set labelcount 0',_), tcl_eval(Interp,'set labelgen 0',_), tcl_eval(Interp,'set totallinks 0',_), tcl_eval(Interp,'set planarlinks 0',_), tcl_eval(Interp,'set acclinks 0',_), tcl_eval(Interp,'set labellinks 0',_), tcl_eval(Interp,'set lookups 0',_), retractall('solutions found'(_)), retractall('alternatives found'(_)), retractall('start time'(_)), retractall('garbage collection'(_)), retractall('rd_table'(_,_)), assert('solutions found'(-1)), assert('alternatives found'(0)), statistics(runtime,[T0|_]), assert('start time'(T0)), statistics(garbage_collection,GC0), assert('garbage collection'(GC0)), format1('~N===~n~p => ~p~n===~n',[X,Goal]). write_solutions(N) :- retract('solutions found'(N)), ( N= -1 -> format('Lexicon error!~n',[]) ; N= 0 -> format('No solutions!~n',[]) ; N= 1 -> format('1 solution found.~n',[]) ; format('~w solutions found.~n',[N]) ), ( N> 0 -> retract('alternatives found'(M)), ( M = 0 -> format('No alternatives.~n',[]) ; M = 1 -> format('1 alternative found.~n',[]) ; format('~w alternatives found.~n',[M]) ) ; true ). as_portray_list([]) :- format('empty~n',[]). as_portray_list([A|As]) :- as_portray_list1(As, A). as_portray_list1([], A) :- format('~p~n===~n',[A]). as_portray_list1([A|As], A0) :- format('~p~n',[A0]), as_portray_list1(As, A).