1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%%                                                                           %%
    3%%      Version:  1.00   Date: 20/02/95   File: tom_inference.pl             %%
    4%% Last Version:                          File:                              %%
    5%% Changes:                                                                  %%
    6%% 20/02/95 Created                                                          %%
    7%%                                                                           %%
    8%% Purpose:                                                                  %%
    9%%                                                                           %%
   10%% Author:  Zoltan Rigo                                                      %%
   11%%                                                                           %%
   12%% Usage:   prolog tom_inference.pl                                          %%
   13%%                                                                           %%
   14%%                                                                           %%
   15%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   16
   17/*%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   18\chapter
   19[Die Datei {\tt tom\_inference}]
   20{Die Datei {\Huge \tt tom\_inference}}
   21
   22This file provides the predicates for the approach that generates inference
   23rules from certain modal axioms. The first two preciates are the ones
   24called in |tom.pl|.
   25
   26\PL*/
   27
   28write_matrix(OutStream):-
   29	is_option('Tom:special_path_term',NormalPathPredicate),
   30	( NormalPathPredicate = off ->
   31	    true
   32	; concat_atom([NormalPathPredicate,'.pl'],FullFileName),
   33	  compile(FullFileName)
   34	),
   35	( setof(Types,A ^ constraint(Types,A,matrix),ListOfTypes)
   36	; writeln(OutStream,"
   37% The matrix is empty. If I were you, I'd doublecheck what I did.")
   38        ),
   39	( member((Functor / Arity),ListOfTypes),
   40	  constraint((Functor / Arity),AxiomClause,matrix),
   41	  ( NormalPathPredicate = off ->
   42	      FinalClause = AxiomClause
   43	  ; CallPredicate =.. [NormalPathPredicate,AxiomClause,FinalClause],
   44	    call(CallPredicate)
   45	  ),
   46	  writeclause(OutStream,FinalClause),
   47	  fail
   48	; true
   49	).
   50
   51
   52write_extras(InputFileNameAtom):-
   53	concat_atom([InputFileNameAtom,'_descriptors'],DescriptorFile),
   54	open(DescriptorFile,write,DescriptorStream),
   55	write_general_part(DescriptorStream,DescriptorFile),
   56	write_query_specific_part(DescriptorStream),
   57	set_option(prover = procom(DescriptorFile)),
   58	close(DescriptorStream),
   59	( setof(AType, A ^ B ^ constraint(AType,A,B), ListOfATypes),
   60	  set_option('ProCom:extra_procedures' = ListOfATypes )
   61	; true
   62	).
   63/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   64
   65\Predicate write_general_part/2 (+Stream, +DescriptorFileName).
   66
   67This predicate writes the general part of a descriptor set to |Stream| which
   68represents a descriptor file. Because of the \ProCom{} convention, we have
   69to give the file name in the file itself, therefore, we need the additional
   70argument.
   71\PL*/
   72
   73write_general_part(Stream, DescriptorFileName):-
   74	writeclause(Stream, :- module(DescriptorFileName)),
   75	nl(Stream),
   76	writeclause(Stream, :- compile(library(capri))),
   77	writeclause(Stream, :- lib(literal)),
   78	writeclause(Stream, :- lib(matrix)),
   79	nl(Stream),
   80	set_options(Stream),
   81	nl(Stream),
   82	writeclause(Stream, make_pred(A, B, C) :-
   83	( A =.. [D, E],
   84	functor(E, F, G),
   85	functor(H, F, G),
   86	(
   87	    D = (--)
   88	->
   89	    I = (++)
   90	;
   91	    (
   92		D = (++)
   93	    ->
   94		I = (--)
   95	    )
   96	),
   97	C =.. [I, H],
   98	B =.. [D, H])),
   99
  100	writeclause(Stream, look_for_entry(A, B, C, D) :-
  101	(make_pred(A, B, C),
  102	'Contrapositive'(C,_, D))),
  103	nl(Stream),
  104	is_option('Tom:special_unification',Unification),
  105	( Unification = off ->
  106	    Unifier1 = true
  107	; Unifier1 =.. [Unification, AAA, CCC]
  108	),
  109	writeclause(Stream, descriptor((proof(reduction(Index,AAA -> BDD)),
  110	   template(AAA, goal),
  111	   call(make_pred(AAA, CCC, BDD)),
  112	   template(BDD, path(Index)),
  113	   constructor(Unifier1)))),
  114	nl(Stream),
  115	( Unification = off ->
  116	    Unifier2 = true
  117	; Unifier2 =.. [Unification, BBB, DDD]
  118	),
  119	writeclause(Stream, descriptor((proof(connection(ADD, BBB -> CDD)),
  120	   template(BBB, goal),
  121	   call(look_for_entry(BBB, DDD, CDD, ADD)),
  122	   constructor(Unifier2),
  123	   template(CDD, extension(A))))),
  124	nl(Stream).
  125
  126/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  127
  128\Predicate write_query_specific_part/1 (+Stream).
  129
  130This predicate writes the query specific part to |Stream| which represents a
  131descriptor file.
  132\PL*/
  133
  134write_query_specific_part(Stream):-
  135	( constraint(_Type, Clause, Sort),
  136	  write_descriptor(Sort, Clause, Stream),
  137	  fail
  138	; true).
  139/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  140
  141\Predicate write_descriptor/3 (+Sort, +Clause, +Stream).
  142
  143This predicate produces the descriptor for |Clause| according to its |Sort|
  144to |Stream| which represents the descriptor file.
  145\PL*/
  146
  147write_descriptor(interaction, (Head :- Body), Stream):-
  148	functor(Head,HFunctor,Arity),
  149	functor(NewHead, HFunctor,Arity),
  150	arg(1, Head, HArgument),
  151	arg(1, NewHead, NewArgument),
  152	is_option('Tom:special_unification',Unification),
  153	( Unification = off ->
  154	    Unifier = true
  155	; Unifier =.. [Unification, HArgument, NewArgument]
  156	),
  157	nl(Stream),
  158	writeclause(Stream, descriptor((proof(interaction(Head :- Body)),
  159	   template(-- (NewHead), goal),
  160	   constructor((nonvar(NewArgument),
  161	                Unifier)),
  162	   template(-- (Body), residue)))).
  163
  164write_descriptor(transitive, (Head :- (Part1, Part2)), Stream):-
  165	functor(Head,HFunctor,Arity),
  166	functor(NewHead, HFunctor,Arity),
  167	arg(1, Head, HArgument),
  168	arg(1, NewHead, NewArgument),
  169	is_option('Tom:special_unification',Unification),
  170	( Unification = off ->
  171	    Unifier = true
  172	; Unifier =.. [Unification, HArgument, NewArgument]
  173	),
  174	nl(Stream),
  175	writeclause(Stream, descriptor((proof(transitive(Head:-(Part1,Part2))),
  176	   template(-- (NewHead), goal),
  177	   constructor((nonvar(NewArgument),
  178	                Unifier)),
  179	   template(-- (Part1), residue),
  180	   template(-- (Part2), residue)))).
  181	
  182/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  183
  184\Predicate set_options/1 (+DescriptorFile).
  185
  186We compel the descriptors to set the options. Of course, the unification
  187file is derived from the option |'Tom:special_unification'|. All other options
  188are found by trial and error. If you don't like them, change them.
  189
  190They are written to the descriptor file as the user might want to re-use
  191the descriptor file.
  192
  193\PL*/
  194
  195set_options(Stream):-
  196	is_option('Tom:special_unification',Unification),
  197	( Unification = off ->
  198	    true
  199	; concat_atom([Unification,'.pl'],Unificator),
  200	  writeclause(Stream,force_option('ProCom::post_link',[[Unificator]]))
  201	),
  202	writeclause(Stream,force_option('ProCom::path',['path.pl'])),
  203	writeclause(Stream,force_option(equality,[off])),
  204	writeclause(Stream,force_option(remove_unreached_clauses,[off])),
  205	writeclause(Stream,force_option(find_all_connections,[on])),
  206	writeclause(Stream,force_option(connect_weak_unifiable,[off])),
  207	writeclause(Stream,force_option(reductions,[[]])),
  208	writeclause(Stream,force_option(search,[iterative_deepening(1, 1, 1)])).
  209/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  210
  211\EndProlog */