% $Id: RDFQuery.lsl,v 1.1 2004/09/03 19:32:35 connolly Exp $
%
% RDFQery -- transcription of BRQL spec definitions
%
%html <h2>References</h2>
%html <cite><a href="http://www.w3.org/2001/sw/DataAccess/rq23/">BRQL - A Query Language for RDF</a>
%html Revision: 1.49 of 2004/09/01 16:20:54


RDFQuery: trait
    includes
      RDFAbSyn, RDFCoreMT,
      FiniteMap(Variable, QTerm, Binding for Map[D, R]),
      Set(TriplePattern, GraphPattern for Set[E]) % hmm... clause?

    QTerm union of
	 var: Variable, % hmm... aren't blank nodes variables too?
	 t: Term % RDF 1.0 Term; i.e. uri, lit, or bnode

    TriplePattern tuple of
      subject: QTerm,
      predicate: QTerm,
      object: QTerm



  introduces
    ground : TriplePattern -> Bool
    g : TriplePattern -> triple

    subst : QTerm, Binding -> QTerm
    subst : TriplePattern, Binding -> TriplePattern
    subst : GraphPattern, Binding -> GraphPattern

    matches : TriplePattern, Graph, Binding -> Bool
    matches : GraphPattern, Graph, Binding -> Bool


  asserts
    forall s, p, o, t: QTerm,
           tp, T: TriplePattern,
           B: Binding,
           G: Graph,
           GP: GraphPattern

    ground(tp) <=> (tag(tp.subject) ~= var
                    /\ tag(tp.predicate) ~= var
                    /\ tag(tp.object) ~= var
		    );
    ground(tp) => g(tp) = [tp.subject.t, tp.predicate.t, tp.object.t];

    subst(t, B) = (if (tag(t)=var /\ defined(B, t.var))
		   then apply(B, t.var)
		   else t);
    subst([s, p, o], B) = [subst(s,B), subst(p,B), subst(o,B)];

    % Triple Pattern T matches graph G with binding B
    % if subst(T, B) is a ground triple and, as a triple, is entailed by G.
    matches(T, G, B) <=> (ground(subst(T, B))
			  /\ entails({{g(T)}}, G) );


    subst({}, B) = {};
    subst(insert(T, GP), B) = insert(subst(T, B), GP);
    matches({}, G, B);
    matches(insert(T, GP), G, B) = matches(T, G, B) /\ matches(GP, G, B);


% $Log: RDFQuery.lsl,v $
% Revision 1.1  2004/09/03 19:32:35  connolly
% ok, it sort-checks!
%