# Test whether a schema mentions the classes used in this data
#  This involves searching in files for statements being present or absent.
 
@prefix rdf:  <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix s: <http://www.w3.org/2000/01/rdf-schema#> .
# @prefix dpo:  <http://www.daml.org/2001/03/daml+oil#> .
@prefix log:  <http://www.w3.org/2000/10/swap/log#> .
@prefix os:  <http://www.w3.org/2000/10/swap/os#> .

@prefix : <validate.n3#>.  # Local stuff

@prefix val: <validate.n3#>.  # Local stuff

# Usage:   TARGET=myfile.n3 cwm check.n3 -think -purge
#
# Output should not incldue any error messages.
#

@forAll :c, :d, :o, :p, :s, :S, :s1, :x, :y, :F, :G, :H.

#  Some internal terms we will be using in this document:

:usedAsClassIn a rdf:Property;
    s:comment "This term is used as a Class in the given document.";
    a log:Chaff.  # Internal use only, may be purged.

:within a rdf:Property;
    s:comment "relationship between a subforumula and the document it was found in";
    a log:Chaff.  # Internal use only, may be purged.

:targetDocument a s:Class;
    s:comment "Documents which this run is checking for schema validity";
    a log:Chaff.  # Internal use only, may be purged.

:schema a rdf:Property;
    s:comment "The schema for a Class is the document which defines it.".


:ERROR_NO_SCHEMA_OR_CLASS_NOT_DECLARED a rdf:Property;
    s:comment """The document used this as a predicate and there is no
schema which declares it as a Property""".

:ERROR_CLASS_NOT_DECLARED 	   a rdf:Property.

# Target formulae are the top level formula we are pointed at,
#  and any subformulae.

{ :d log:uri [is os:environ of "TARGET"]  } log:implies { :d a :targetDocument }.

{ :d a :targetDocument. :d log:semantics :F } log:implies { :F :within :d }.

# Define subforumulae which are within the target documents:

{ :d a :targetDocument.
  :F :within :d.
  :F log:includes { :s :p :o}.
  :s log:rawType  log:Formula   } log:implies { :s :within :d } .

{ :d a :targetDocument.
  :F :within :d.
  :F log:includes { :s :p :o}.
  :o log:rawType  log:Formula   } log:implies { :o :within :d } .

# Anything used as a predicate in any target formula should be checked.
# We don't bother bout the pseudoproperties log:forSome and log:forAll.

{ :d a :targetDocument.
  :F :within :d.
  :F log:includes { :s a :c}.
  :c log:rawType log:Other.    # Ignore lists
 } log:implies { :c :usedAsClassIn :d } .

#  Let's see what happens when we dereference a class:

{ :d a :targetDocument.
  :c :usedAsClassIn :d.
  :c log:semanticsOrError :x } log:implies  { :c :classSemanticsOrError :x }.

{ :d a :targetDocument.
  :c :usedAsClassIn :d.
  :c :classSemanticsOrError :x.
  :x log:rawType log:Literal } log:implies { :d :ERROR_IN_SCHEMA_ACCESS_FOR_CLASS :c.
                                             :c :CLASS_HAS_SCHEMA_ACCESS_ERROR :x }.
{ :c :classSemanticsOrError :x.
  :x log:rawType log:Formula } log:implies { :c :semanticsOK :x }.

#  The RDFS spec implies the following algorithm for the definitive schema corresponding
#  to a Property :p.  (From Ralph Swick, whiteboard conversation)
#  This is the equivalent for a Class :c
#  Maybe we should simplify it to the schema being the result of dereferencing the Class?
#  I think the counterexample is the dublin core, but it may not work anyway.
# Actually, the dublic core uses a redirect!!! We need to be aware of the
#  existence of redirects like that @@

{ :d a :targetDocument.
  :c :usedAsClassIn :d.
  :c :semanticsOK [log:includes { :c s:isDefinedBy :s }] } log:implies {:c :schema :s}.

# We actually need the formula the schema parses to:

{ :c :schema [ :semanticsOK :F ] } log:implies { :c :classSchemaFormula :F }. 


# Alternatively, the schema can just be the document we pick up
# directly  This is much simpler!
#
   { :c  :usedAsClassIn :d .
     :d  a :targetDocument.
     :c  :semanticsOK :F.
     :F  log:includes { :c a s:Class } } log:implies { :c :classSchemaFormula :F.
                                                             :c a :classDeclaredInDirectSchema  }. 

#  If there is no indirect schema pointer or direct declaration found, then we flag a problem

{ :d a :targetDocument.
  :d log:semantics :G.    #  These 2 lines and one below suppress error messages
  :G log:notEqualTo :F.    #  about undeclared locals in the same file.
  :c :usedAsClassIn :d.
  :c :semanticsOK :F.
  :F log:notIncludes { :c s:isDefinedBy [] }.   # No indirect Schema
  :F log:notIncludes { :c a s:Class }.      # Not a direct schema
} log:implies { :d :ERROR_DEREF_DOC_DOES_NOT_DECLARE_CLASS :c }.


# It is an error, we say, for something to be used as a Property but
# not *explicitly* declared as such in the schema:

{:c :classSchemaFormula :F.
 :F log:notIncludes { :c a s:Class }}log:implies { :d :ERROR_CLASS_NOT_DECLARED :c } .
 

#   (b)when the document is combined with the above, no condradiction
#      can be found from anything being (eg) member of disjoint sets.
#
# @@ to come.
  
################################################################### Clean up

{:d a :targetDocument. :F :within :d } log:implies { :F a log:Chaff }. # Clear our formulae

log:Chaff is rdf:type of
    rdf:type,      # Seriously ...
    s:comment,
    log:forAll,
    log:implies,   #  Clear out rules on -purge
    :within, :classSchemaFormula, :schema, :classSemanticsOrError, :semanticsOK,
#    :targetDocument,
    :usedAsPropertyIn.
 
#ends