1% This file is part of the Attempto Parsing Engine (APE).
    2% Copyright 2008-2013, Attempto Group, University of Zurich (see http://attempto.ifi.uzh.ch).
    3%
    4% The Attempto Parsing Engine (APE) is free software: you can redistribute it and/or modify it
    5% under the terms of the GNU Lesser General Public License as published by the Free Software
    6% Foundation, either version 3 of the License, or (at your option) any later version.
    7%
    8% The Attempto Parsing Engine (APE) is distributed in the hope that it will be useful, but WITHOUT
    9% ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
   10% PURPOSE. See the GNU Lesser General Public License for more details.
   11%
   12% You should have received a copy of the GNU Lesser General Public License along with the Attempto
   13% Parsing Engine (APE). If not, see http://www.gnu.org/licenses/.
   14
   15:- module(drs_to_tptp, [
   16		drs_to_tptp/2,
   17		drs_to_tptplist/2,
   18		tptp_pp/1,
   19		tptplist_pp/1
   20	]).   21
   22:- use_module(drs_to_drslist, [
   23		drs_to_drslist/2
   24	]).

 drs_to_tptplist(+Drs:drs, -TptpList:list) is det

Arguments:

Drs	- is an Attempto DRS
TptpList	- is a list of TPTP formulas

   65drs_to_tptplist(Drs, TptpList) :-
   66	drs_to_drslist(Drs, DrsList),
   67	maplist(drs_to_tptp, DrsList, TptpList).

 drs_to_tptp(+Drs:drs, -Tptp:tptp) is det

Arguments:

Drs	- is an Attempto DRS
Tptp	- is a TPTP formula

   75drs_to_tptp(drs([], [question(drs(Dom, Conds))]), fof(conjecture, Expr)) :-
   76	!,
   77	drs_to_tptp_x(drs(Dom, Conds), Expr).
   78
   79drs_to_tptp(drs(Dom, Conds), fof(axiom, Expr)) :-
   80	drs_to_tptp_x(drs(Dom, Conds), Expr).
   81
   82
   83drs_to_tptp_x(drs(Dom, Conds), Expr) :-
   84	conds_tptp(Dom, Conds, NDom, NConds),
   85	get_quantifier_expression('?', NDom, NConds, Expr).

 conds_tptp(+Dom:list, +Conds:list, -NDom:list, -Tptp:term) is det

   90conds_tptp(Dom, [Cond], NDom, NCond) :-
   91	tptp(Dom, Cond, NDom, NCond).
   92
   93conds_tptp(Dom, [Cond1, Cond2 | Tail], NDom, '&'(NCond1, NTail)) :-
   94	tptp(Dom, Cond1, NDomTmp, NCond1),
   95	conds_tptp(NDomTmp, [Cond2 | Tail], NDom, NTail).

 get_quantifier_expression(Quant, Vars, Expr, QExpr)

  100get_quantifier_expression(_, [], Expr, Expr) :- !.
  101get_quantifier_expression('?', Vars, Expr, ':'('?'(Vars), Expr)).
  102get_quantifier_expression('!', Vars, Expr, ':'('!'(Vars), Expr)).

 tptp

  107tptp(
  108	UpperDom,
  109	'=>'(drs(Dom1, Conds1), drs(Dom2, Conds2)),
  110	UpperDom,
  111	Expr
  112) :-
  113	!,
  114	conds_tptp(Dom1, Conds1, NDom1, NConds1),
  115	conds_tptp(Dom2, Conds2, NDom2, NConds2),
  116	get_quantifier_expression('?', NDom2, NConds2, Expr2),
  117	get_quantifier_expression('!', NDom1, '=>'(NConds1, Expr2), Expr).
  118
  119tptp(
  120	UpperDom,
  121	'v'(drs(Dom1, Conds1), drs(Dom2, Conds2)),
  122	UpperDom,
  123	Expr
  124) :-
  125	!,
  126	conds_tptp(Dom1, Conds1, NDom1, NConds1),
  127	conds_tptp(Dom2, Conds2, NDom2, NConds2),
  128	get_quantifier_expression('?', NDom2, NConds2, Expr2),
  129	get_quantifier_expression('?', NDom1, '|'(NConds1, Expr2), Expr).
  130
  131tptp(
  132	UpperDom,
  133	'-'(drs(Dom, Conds)),
  134	UpperDom,
  135	'~'(QExpr)
  136) :-
  137	!,
  138	conds_tptp(Dom, Conds, NDom, NConds),
  139	get_quantifier_expression('?', NDom, NConds, QExpr).
  140
  141tptp(Dom, predicate(X, be, A, B)-_, NDom, '='(NA, NB)) :-
  142	!,
  143	exclude(==(X), Dom, NDom),
  144	arg_to_tptp(A, NA),
  145	arg_to_tptp(B, NB).
  146
  147tptp(Dom, object(_, Lemma, _, _, _, _)-_, Dom, $true) :-
  148	is_thing(Lemma),
  149	!.
  150
  151tptp(Dom, object(Var, Lemma, _, _, eq, 1)-_, Dom, Pred) :-
  152	!,
  153	Pred =.. [Lemma, Var].
  154
  155% The rest of the atomic conditions are kept as they are.
  156tptp(Dom, Cond-_, Dom, Tptp) :-
  157	!,
  158	cond_to_tptp(Cond, Tptp).
  159
  160tptp(_, Term, _, _) :-
  161	functor(Term, Functor, _),
  162	concat_atom(['DRS condition not supported', Functor], ': ', Message),
  163	throw(error(Message, context(tptp/4, Term))).

 cond_to_tptp

  169cond_to_tptp(formula(R1, Symbol, R2), Pred) :-
  170	arg_to_tptp(R1, NR1),
  171	arg_to_tptp(R2, NR2),
  172	atom(Symbol),
  173	member(Symbol, ['<', '>', '=', '\\=', '>=', '=<']),
  174	Pred =.. [Symbol, NR1, NR2].
  175
  176cond_to_tptp(object(A, B, C, D, E, F), object(A, B, C, D, E, F)).
  177
  178cond_to_tptp(modifier_adv(R, Lexem, Degree), modifier_adv(R, Lexem, Degree)) :-
  179	var(R),
  180	atom(Degree),
  181	member(Degree, [pos, comp, sup]),
  182	atom(Lexem).
  183
  184cond_to_tptp(modifier_pp(R1, Prep, R2), modifier_pp(R1, Prep, NR2)) :-
  185	var(R1),
  186	atom(Prep),
  187	arg_to_tptp(R2, NR2).
  188
  189cond_to_tptp(property(R, Lexem, Comp), property1(R, Lexem, Comp)) :-
  190	var(R),
  191	atom(Comp),
  192	member(Comp, [pos, comp, sup]),
  193	atom(Lexem).
  194
  195cond_to_tptp(property(R1, Lexem, Comp, R2), property2(R1, Lexem, Comp, NR2)) :-
  196	var(R1),
  197	arg_to_tptp(R2, NR2),
  198	atom(Comp),
  199	member(Comp, [pos, pos_as, comp, comp_than, sup]),
  200	atom(Lexem).
  201
  202cond_to_tptp(property(R1, Lexem, R2, Comp, SubjObj, R3), property3(R1, Lexem, NR2, Comp, SubjObj, NR3)) :-
  203	var(R1),
  204	arg_to_tptp(R2, NR2),
  205	arg_to_tptp(R3, NR3),
  206	atom(Comp),
  207	member(Comp, [pos_as, comp_than]),
  208	atom(SubjObj),
  209	member(SubjObj, [subj, obj]),
  210	atom(Lexem).
  211
  212cond_to_tptp(predicate(R1, Lexem, R2), predicate1(R1, Lexem, NR2)) :-
  213	var(R1),
  214	arg_to_tptp(R2, NR2),
  215	atom(Lexem).
  216
  217cond_to_tptp(predicate(R1, Lexem, R2, R3), predicate2(R1, Lexem, NR2, NR3)) :-
  218	var(R1),
  219	arg_to_tptp(R2, NR2),
  220	arg_to_tptp(R3, NR3),
  221	atom(Lexem).
  222
  223cond_to_tptp(predicate(R1, Lexem, R2, R3, R4), predicate3(R1, Lexem, NR2, NR3, NR4)) :-
  224	var(R1),
  225	arg_to_tptp(R2, NR2),
  226	arg_to_tptp(R3, NR3),
  227	arg_to_tptp(R4, NR4),
  228	atom(Lexem).
  229
  230cond_to_tptp(relation(R1, of, R2), relation(R1, of, NR2)) :-
  231	var(R1),
  232	arg_to_tptp(R2, NR2).
  233
  234cond_to_tptp(has_part(R1, R2), has_part(R1, NR2)) :-
  235	var(R1),
  236	arg_to_tptp(R2, NR2).
  237
  238cond_to_tptp(query(R, Lexem), _) :-
  239	throw(error('DRS query/2 not supported', context(cond_to_tptp/2, query(R, Lexem)))).

 arg_to_tptp

  245arg_to_tptp(Arg, Arg) :-
  246	var(Arg),
  247	!.
  248
  249arg_to_tptp(named(Arg), Arg) :-
  250	atom(Arg).
  251
  252arg_to_tptp(int(Arg), Arg) :-
  253	integer(Arg).
  254
  255arg_to_tptp(real(Arg), Arg) :-
  256	float(Arg).
  257
  258arg_to_tptp(int(Arg, Unit), int(Arg, Unit)) :-
  259	integer(Arg),
  260	atom(Unit).
  261
  262arg_to_tptp(real(Arg, Unit), real(Arg, Unit)) :-
  263	float(Arg),
  264	atom(Unit).
  265
  266arg_to_tptp(string(Arg), string(Arg)) :-
  267	atomic(Arg).
  268
  269arg_to_tptp(list(List), _) :-
  270	throw(error('DRS function list/1 not supported', context(arg_to_tptp/2, list(List)))).
  271
  272arg_to_tptp(set(Set), _) :-
  273	throw(error('DRS function set/1 not supported', context(arg_to_tptp/2, set(Set)))).
  274
  275arg_to_tptp(expr('&', Arg1, Arg2), _) :-
  276	throw(error('DRS operator \'&\' not supported', context(arg_to_tptp/2, expr('&', Arg1, Arg2)))).
  277
  278arg_to_tptp(expr(Op, Arg1, Arg2), Expr) :-
  279	arg_to_tptp(Arg1, NArg1),
  280	arg_to_tptp(Arg2, NArg2),
  281	atom(Op),
  282	member(Op, ['+', '-', '*', '/']),
  283	Expr =.. [Op, NArg1, NArg2].

 is_thing

  289is_thing(somebody).
  290is_thing(something).

 tptplist_pp(+TptpList:list)

Pretty-prints a list of TPTP formulas. The input formulas are expected not to have names, the names will be assigned using the scheme: 'f1', 'f2', 'f3', ...

  300tptplist_pp(TptpList) :-
  301	tptplist_pp(1, f, TptpList).

 tptplist_pp(+Index:integer, +Prefix:atom, +TptpList:list)

Pretty-prints a list of TPTP formulas. The input formulas are expected not to have names, i.e. they must have the form fof(Role, Expr), where Role is either 'axiom' or 'conjecture', and Expr is the FOL formula. Names are assigned to the formulas during pretty-printing. The names are constructed by concatenating Prefix with Index. The Index is increased by one for the next formula.

  314tptplist_pp(_, _, []).
  315
  316tptplist_pp(Index, Prefix, [Tptp]) :-
  317	tptp_pp(Index, Prefix, Tptp).
  318
  319tptplist_pp(Index, Prefix, [Tptp1, Tptp2 | Rest]) :-
  320	tptp_pp(Index, Prefix, Tptp1),
  321	nl, nl,
  322	NewIndex is Index + 1,
  323	tptplist_pp(NewIndex, Prefix, [Tptp2 | Rest]).

 tptp_pp(+Index:integer, +Prefix:atom, +Tptp:term)

  327tptp_pp(Index, Prefix, fof(Role, Expr)) :-
  328	concat_atom([Prefix, Index], Name),
  329	tptp_pp(fof(Name, Role, Expr)).

 tptp_pp(+Tptp:term)

TPTP pretty-printer. BUG: Should be replaced with something prettier.

  336tptp_pp(fof(Role, Expr)) :-
  337	tptp_pp(fof(name, Role, Expr)).
  338
  339tptp_pp(fof(Name, Role, Expr)) :-
  340	format("fof(~w, ~w, (~n", [Name, Role]),
  341	numbervars(Expr, 0, _),
  342	tptp_pp_(Expr),
  343	format(")).", []),
  344	fail ; true.
  345
  346tptp_pp_(':'('?'(Vars), F)) :-
  347	!,
  348	write_term('?', [quoted(true)]),
  349	write(' '),
  350	write_term(Vars, [numbervars(true), quoted(true)]),
  351	write(' : '),
  352	tptp_pp_wrap(F).
  353
  354tptp_pp_(':'('!'(Vars), F)) :-
  355	!,
  356	write_term('!', [quoted(true)]),
  357	format(" ", []),
  358	write_term(Vars, [numbervars(true), quoted(true)]),
  359	format(" : ", []),
  360	tptp_pp_wrap(F).
  361
  362tptp_pp_('=>'(A, B)) :-
  363	!,
  364	tptp_pp_wrap(A),
  365	format("~n=> ", []),
  366	tptp_pp_wrap(B).
  367
  368tptp_pp_('|'(A, B)) :-
  369	!,
  370	tptp_pp_wrap(A),
  371	format("~n| ", []),
  372	tptp_pp_wrap(B).
  373
  374tptp_pp_('&'(A, B)) :-
  375	!,
  376	tptp_pp_wrap(A),
  377	format(" &~n", []),
  378	tptp_pp_wrap(B).
  379
  380tptp_pp_('~'(A)) :-
  381	!,
  382	write('~'),
  383	tptp_pp_wrap(A).
  384
  385tptp_pp_(A) :-
  386	write_term(A, [numbervars(true), quoted(true)]).
  387
  388
  389tptp_pp_wrap(A) :-
  390	write('('),
  391	tptp_pp_(A),
  392	write(')')