:- ensure_loaded(common).
cvs_id('$Id: vrdf.pl,v 1.4 2004/11/04 18:59:28 sandro Exp $').
/*

  The "Virtual RDF" (VRDF) API

  This is a layer over library('semweb/rdf_db') that supports
  various additional features.

     - rdf content produced by prolog rules
     - rdf content present in static prolog clauses
     - rdf content where terms are suitable prolog terms
     - rdf content loaded on-demand from disk (and maybe the web?)
     - rdf content produced by RDF rules (???)

  It is intended to replace rdfq/4, eventually.  This is the RDF API
  which most of SemWalker should be using.


  
*/

:- use_module(library('semweb/rdf_db')).
:- use_module(library(debug)).
:- debug(vrdf).
	
:- multi_dynamic(vrdf_provide_by_predicate/4).
:- multi_dynamic(vrdf_provide_by_subject/4).
:- multifile(vrdf_predicate_map/4).
:- thread_local(vrdf_proof_rejected/1).

%%  vrdf(?Subj, ?Pred, ?Obj, ?Proof) + thread_locals as below
%%
%%  thread_locals:
%%
%%      vrdf_proof_rejected(Proof)      if this succeeds this
%%                                      proof is discarded.  can
%%                                      be used to prune proof
%%                                      branches before a whole
%%                                      tree gets built
%%      vrdf_stop                       if this succeeds, stop looking
%%                                      for stuff.   [Does this belong
%%                                      here, or in the caller???]
%%  

vrdf(Subj, Pred, Obj, Proof) :-
	between(3,10,Depth),
	call_with_depth_limit(vrdf_nested(Subj, Pred, Obj, Proof),
			      Depth,
			      Status),
	(   Status = depth_limit_exceeded
	->  debug(vrdf, 'depth limit ~w exceeded; retry', [Depth]),
	    fail
	;   debug(vrdf, 'a result at depth limit ~w', [Status])
	),
	\+ vrdf_proof_rejected(Proof).
	

vrdf_nested(Subj, Pred, Obj, Proof) :-
	% somehow map term args to rdf-terms here....?
	(atom(Subj) ; var(Subj)),
	(atom(Pred) ; var(Pred)),
	( atom(Obj) ; Obj=literal(_) ; var(Obj) ),
	(   ground(Proof)
	->  Proof = in_representation_chunk(Graph)
	;   true
	),
	rdf(Subj, Pred, Obj, Graph),
	Proof = in_representation_chunk(Graph),
	\+ vrdf_proof_rejected(Proof).

%vrdf(Subj, Pred, Obj, Proof) :-
%	vrdf_predicate_map(Pred, PrologPred/Arity, ArgNum, Style),
%	throw(not_implemented),
%	Proof = from_prolog_database(PrologPred),
%	\+ vrdf_proof_rejected(Proof).
%vrdf(Subj, Pred, Obj, Proof) :-
%	% maybe loop back through vrdf after pagein...?
%	rdf_with_pagein(Subj, Pred, Obj, Graph),
%	Proof = in_representation_chunk(Graph),
%	\+ vrdf_proof_rejected(Proof).
% some kind of rules....?     maybe just vrdf_provide_by_predicate ?

%%
%%  Call this version of vrdf/4 if you're inside some code which is
%%  providing vrdf/4 data on demand (backward chaining), since
%%  supports breadth-first searching.
%%

vrdf_nested(Subj, Pred, Obj, Proof) :-
	ground(Subj),
	vrdf_provide_by_subject(Subj, Pred, Obj, Proof).
vrdf_nested(Subj, Pred, Obj, Proof) :-
	ground(Pred),
	vrdf_provide_by_predicate(Pred, Subj, Obj, Proof).
vrdf_nested(Subj, Pred, Obj, Proof) :-
	vrdf_provide(Subj, Pred, Obj, Proof).

vrdf_provide_by_predicate(rdf:type, Subj, Obj, Proof) :-
	vrdf_provide_by_class(Obj, Subj, Proof).

:- multifile(vrdf_provide_by_predicate/4).
:- multifile(vrdf_provide_by_subject/4).
:- multifile(vrdf_provide_by_class/3).
:- multifile(vrdf_provide/4).


%%  vrdf_attach(+URI)
%%  vrdf_detach(+URI)     [?]
%%  vrdf_attached(?URI, ?Status)
%%
%%  URIs passed to vrdf/4 are automatically attached.
%%  URIs returned from vrdf/4 are not at this time.
%%

vrdf_add_rule(_Rule, _Source) :-
	true.

%%  vrdf_otter_rule(?Otter, ?Prolog)
%%

vrdf_assert_otter(Otter, Tag) :-
	%Proof=otter_rule,
	vrdf_otter_split(Otter, HeadList, BodyListX),
	rewrite_goal_list(BodyListX, BodyList, Subs),
	free_variables(BodyListX, Vars),   % don't include proof vars
	Proof = external_rule(Tag, sub(Subs), vars(Vars)),
	!,
	(   HeadList = [ HeadX ]
	->  rewrite_head(HeadX, Proof, Head1),
	    !,
	    expand_goal(Head1, Head),
	    !,
	    conjoin(BodyList, Body),
	    !,
	    assert(( Head :- Body ))
	;   %print_message(warning, not_horn((HeadListX, BodyListX))),
	    fail
	).

vrdf_otter_split(-Term|Rest, RestHead, [Term | RestBody]) :-
	\+ Term = (_|_),
	vrdf_otter_split(Rest, RestHead, RestBody).
vrdf_otter_split(Term|Rest, [Term | RestHead], RestBody) :-
	\+ Term = -_,
	\+ Term = (_|_),
	vrdf_otter_split(Rest, RestHead, RestBody).
vrdf_otter_split(-Term, [], [Term]) :-
	\+ Term = (_|_).
vrdf_otter_split(Term, [Term], []) :-
	\+ Term = (_|_),
	\+ Term = -_.

qtest :-
	true.

rewrite_goal_list([], [], []).
rewrite_goal_list([Tin|T], [Tout|TRest], [Proof|PX]) :-
	Tin =.. [Fin | Args],
	append(Args, [Proof], ArgsOut),
	rewrite_goal_functor(Fin, Fout),
	Tout1 =.. [Fout | ArgsOut],
	expand_goal(Tout1, Tout),
	rewrite_goal_list(T, TRest, PX).

rewrite_goal_functor(rdf, vrdf_nested).
rewrite_goal_functor(=, equal).
rewrite_goal_functor(\=, not_equal).
rewrite_goal_functor(X, Y) :-
	atom_concat(loaded_rule__, X, Y).

rewrite_head(rdf(S,P,O), Proof, vrdf_provide_by_predicate(P,S,O,Proof)) :-
	ground(P).
rewrite_head(rdf(S,P,O), Proof, vrdf_provide_by_subject(S,P,O,Proof)) :-
	ground(S).
rewrite_head(Old, Proof, New) :-
	Old =.. [FH | Args],
	rewrite_head_functor(FH, NFH),
	append(Args, [Proof], NewArgs),
	New =.. [NFH | NewArgs].

rewrite_head_functor(rdf, vrdf_provide).
rewrite_head_functor(=, equal).
rewrite_head_functor(\=, not_equal).
rewrite_head_functor(X, Y) :-
	atom_concat(loaded_rule__, X, Y).


conjoin([Clause], Clause).
conjoin([Clause|Clauses], (Clause, X)) :-
	Clauses \= [],
	conjoin(Clauses, X).
conjoin([], true).



load_surnia :-
	open('/tmp/owlAx.clause', read, Stream),
	repeat,
	read_term(Stream, X, [term_position(Pos)]),
	Pos = '$stream_position'(_Char, Line, _),
	atom_number(LineAtom, Line),
	concat_atom(['clause#', LineAtom], Source),
	vrdf_assert_otter(X, surnia:Source),
	at_end_of_stream(Stream),
	!,
	close(Stream),
	print_message(informational, format('Surnia axioms loaded.', [])).

%%  proof_sources(+Proof, -SourceGraphs)
%%
%%  traverse a Proof and find the SourceGraphs in it
%%
%%  these things in turn lead to retrievals, addresses, etc.

proof_sources(Proof, Sources) :-
	proof_list_sources([Proof], UnsortedSources),
	sort(UnsortedSources, Sources).

proof_list_sources([], []).
proof_list_sources([in_representation_chunk(Graph)|Px], [Graph|Gx]) :-
	proof_list_sources(Px, Gx).
proof_list_sources([external_rule(_Tag, sub(Subs), vars(_))|Px], G) :-
	% also use Tag as a source???
	proof_list_sources(Subs, G1),
	proof_list_sources(Px, G2),
	append(G1, G2, G).

/*


bash-2.05b$ cd /home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/surnia

otter < otter/owlAx.otter | fgrep '[]' | sed -e 's/[0-9]* \[\] //' -e 's/!=/ \\= /g' -e 's/\bx\([0-9]*\)\b/X\1/g' -e 's/\bowl_/owl:/g' -e's/\brdf_/rdf:/g' -e's/\brdfs_/rdfs:/g' -e's/\bi\([0-9]*\)\b/\1/g' > /tmp/owlAx.clause

    SED BUG!   leaves some _'s

    -rdf(X144,owl:differentFrom,X145)|rdf(X145, owl_differentFrom,X144).

otter < otter/owlAx.otter | fgrep '[]' | sed -e 's/[0-9]* \[\] //' -e 's/!=/ \\= /g' -e 's/\bx\([0-9]*\)\b/X\1/g' -e 's/\bowl_/owl:/g' -e's/\brdf_/rdf:/g' -e's/\brdfs_/rdfs:/g' -e's/\bi\([0-9]*\)\b/\1/g' -e "s/:\([A-Za-z0-9_]*\)/:'\1'/g" -e "s/'foo:'succ''/foo:succ/g" -e "s/'foo:'zero''/foo:zero/g" -e 's/_/:/g' > /tmp/owlAx.clause
  
?- see('/tmp/owlAx.clause'), repeat, read(X), write(X), nl, X=end_of_file, seen.

see('/tmp/owlAx.clause'), repeat, read_term(X, [term_position(Pos)]), vrdf_assert_otter(X, surnia_axioms(Pos)),  X=end_of_file, seen.


   X :- Z.
->
   not(Z) :- not(X).


   X or Y :- Z

->

    X :- Z, not(Y).
    Y 
	    
*/
