diff --git a/Swish/RDF/Datatype.hs b/Swish/RDF/Datatype.hs --- a/Swish/RDF/Datatype.hs +++ b/Swish/RDF/Datatype.hs @@ -766,32 +766,33 @@ -- calculated, then the relation is presumed to be underdetermined, -- and @Just []@ is returned. -- --- [@fnss@] is a list of argument value predicates and --- function descriptors. The predicate indicates any --- additional constraints on argument values (e.g. the result --- of abs must be positive). Use @(const True)@ for the predicate --- associated with unconstrained relation arguments. --- For each argument, a list of function descriptors is --- supplied corresponding to alternative values (e.g. a square --- relation would offer two alternative values for the root.) --- --- [@apfn@] is a function that takes an argument value predicate, --- a function descriptor and applies it to a supplied argument --- list to return: --- @Just a@ calculated list of one or more possible argument values, --- @Just []@ indicating insufficient information provided, or --- @Nothing@ indicating inconsistent information provided. --- May be one of 'unaryFnApp', 'binaryFnApp', 'listFnApp' or --- some other caller-supplied value. --- The value used must match the type of @fnss@ used. --- --- Returns a @'DatatypeRelFn' vt@ value that can be used as the --- 'dtRelFunc' component of a 'DatatypeRel' value. --- -altArgs :: (Eq vt) - => DatatypeRelPr vt -> [(vt->Bool,[b])] - -> ((vt->Bool)->b->[Maybe vt]->Maybe [vt]) - -> DatatypeRelFn vt +altArgs :: + (Eq vt) + => DatatypeRelPr vt + -> [(vt->Bool,[b])] + -- ^ a list of argument value predicates and + -- function descriptors. The predicate indicates any + -- additional constraints on argument values (e.g. the result + -- of abs must be positive). Use @(const True)@ for the predicate + -- associated with unconstrained relation arguments. + -- For each argument, a list of function descriptors is + -- supplied corresponding to alternative values (e.g. a square + -- relation would offer two alternative values for the root.) + + -> ((vt->Bool)->b->[Maybe vt]->Maybe [vt]) + -- ^ a function that takes an argument value predicate, + -- a function descriptor and applies it to a supplied argument + -- list to return: + -- @Just a@ calculated list of one or more possible argument values, + -- @Just []@ indicating insufficient information provided, or + -- @Nothing@ indicating inconsistent information provided. + -- May be one of 'unaryFnApp', 'binaryFnApp', 'listFnApp' or + -- some other caller-supplied value. + + -> DatatypeRelFn vt + -- ^ The return value can be used as the + -- 'dtRelFunc' component of a 'DatatypeRel' value. + altArgs pr fnss apfn args = cvals4 cvals3 where -- Calculate new value(s) for each argument from supplied values, and diff --git a/Swish/RDF/MapXsdInteger.hs b/Swish/RDF/MapXsdInteger.hs --- a/Swish/RDF/MapXsdInteger.hs +++ b/Swish/RDF/MapXsdInteger.hs @@ -58,9 +58,7 @@ go (x:xs) ys | x `elem` ['0'..'9'] = go xs (x:ys) | otherwise = Nothing - in case f of - True -> val - False -> fmap ((-1) *) val + in if f then val else fmap ((-1) *) val -------------------------------------------------------------------------------- -- diff --git a/Swish/RDF/N3Parser.hs b/Swish/RDF/N3Parser.hs --- a/Swish/RDF/N3Parser.hs +++ b/Swish/RDF/N3Parser.hs @@ -865,6 +865,12 @@ | void -} +restoreState :: N3State -> N3Parser N3State +restoreState origState = do + oldState <- getState + setState $ origState { nodeGen = nodeGen oldState } + return oldState + {- We create a subgraph and assign it to a blank node, returning the blank node. At present it is a combination of the subgraph and formula @@ -879,10 +885,8 @@ let fstate = pstate { graphState = emptyRDFGraph, thisNode = bNode } setState fstate statementList - fstate' <- getState - let nstate = pstate { nodeGen = nodeGen fstate' } - setState nstate - updateState $ updateGraph $ setFormula (Formula bNode (graphState fstate')) + oldState <- restoreState pstate + updateState $ updateGraph $ setFormula (Formula bNode (graphState oldState)) return bNode subgraph :: RDFLabel -> N3Parser RDFGraph @@ -891,11 +895,9 @@ let fstate = pstate { graphState = emptyRDFGraph, thisNode = this } setState fstate -- switch new state into parser statementsOptional -- parse statements of formula - fstate' <- getState - let nstate = pstate { nodeGen = nodeGen fstate' } - setState nstate -- swap back state, with updated nodeGen - return (graphState fstate') - + oldState <- restoreState pstate + return $ graphState oldState + statementList :: N3Parser () statementList = ignore $ sepEndBy (lexeme statement) fullStop diff --git a/Swish/RDF/Proof.hs b/Swish/RDF/Proof.hs --- a/Swish/RDF/Proof.hs +++ b/Swish/RDF/Proof.hs @@ -99,7 +99,7 @@ checkStep rules prev st && checkProof1 rules (formExpr (stepCon st):prev) steps res --- A proof step is valid if rule is in list of rules +-- | A proof step is valid if rule is in list of rules -- and the antecedents are sufficient to obtain the conclusion -- and the antecedents are in the list of formulae already proven. -- @@ -107,7 +107,19 @@ -- unique among all rules. In particular the name of the step rule -- being in correspondence with the name of one of the indicated -- valid rules of inference. -checkStep :: (Expression ex) => [Rule ex] -> [ex] -> Step ex -> Bool +checkStep :: + (Expression ex) + => [Rule ex] -- ^ rules + -> [ex] -- ^ a ntecedants + -> Step ex -- ^ the step to validate + -> Bool -- ^ @True@ if the step is valid + +checkStep rules prev step = maybe True (const False) $ explainStep rules prev step + +{- + +Is the following an optimisation of the above? + checkStep rules prev step = -- Rule name is one of supplied rules, and (ruleName srul `elem` map ruleName rules) && @@ -122,6 +134,7 @@ sant = map formExpr $ stepAnt step -- Consequentent expression from proof step: scon = formExpr $ stepCon step +-} {- @@ -142,7 +155,8 @@ sbwd = bwdApply srul (formExpr $ stepCon step) -} --- |Check proof, and return identification of failing step. +-- |Check proof. If there is an error then return information +-- about the failing step. explainProof :: (Expression ex) => Proof ex -> Maybe String explainProof pr = @@ -160,7 +174,7 @@ Nothing -> explainProof1 rules (formExpr (stepCon st):prev) steps res Just ex -> Just ("Invalid step: "++show (formName $ stepCon st)++": "++ex) --- A proof step is valid if rule is in list of rules +-- | A proof step is valid if rule is in list of rules -- and the antecedents are sufficient to obtain the conclusion -- and the antecedents are in the list of formulae already proven. -- @@ -169,9 +183,12 @@ -- being in correspondence with the name of one of the indicated -- valid rules of inference. -- --- Return Nothing if step is OK, or Just string describing failure --- -explainStep :: (Expression ex) => [Rule ex] -> [ex] -> Step ex -> Maybe String +explainStep :: + (Expression ex) + => [Rule ex] -- ^ rules + -> [ex] -- ^ previous + -> Step ex -- ^ step + -> Maybe String -- ^ @Nothing@ if step is okay, otherwise a string indicating the error explainStep rules prev step = if null errors then Nothing else Just $ intercalate ", " errors where @@ -207,7 +224,11 @@ -- formatted text, and may include any desired indentation, and -- -- (3) no newline is output following the final line of text. -showsProof :: (ShowM ex) => String -> Proof ex -> ShowS +showsProof :: + (ShowM ex) + => String -- ^ newline string + -> Proof ex + -> ShowS showsProof newline proof = if null axioms then shProof else shAxioms . shProof where @@ -222,7 +243,11 @@ showsSteps newline (proofChain proof) -- |Returns a simple string representation of a proof. -showProof :: (ShowM ex) => String -> Proof ex -> String +showProof :: + (ShowM ex) + => String -- ^ newline string + -> Proof ex + -> String showProof newline proof = showsProof newline proof "" -- |Create a displayable form of a list of labelled proof steps diff --git a/Swish/RDF/RDFGraph.hs b/Swish/RDF/RDFGraph.hs --- a/Swish/RDF/RDFGraph.hs +++ b/Swish/RDF/RDFGraph.hs @@ -431,7 +431,7 @@ instance T.Traversable NSGraph where traverse f (NSGraph ns fml stmts) = - (NSGraph ns) <$> formulaeMapA f fml <*> (T.traverse $ T.traverse f) stmts + NSGraph ns <$> formulaeMapA f fml <*> (T.traverse $ T.traverse f) stmts instance (Label lb) => Eq (NSGraph lb) where (==) = grEq @@ -557,11 +557,16 @@ mapFind nv nv (LookupMap (maplist dupbn allbn cnvbn [])) -- | Construct a list of (oldnode,newnode) values to be used for --- graph label remapping. The function operates recursiovely, adding --- new nodes generated to the mapping list (mapbn') and also to the --- list of nodes to be avoided (allbn'). +-- graph label remapping. The function operates recursively, adding +-- new nodes generated to the accumulator and also to the +-- list of nodes to be avoided. maplist :: - (Label lb) => [lb] -> [lb] -> (lb -> lb) -> [(lb,lb)] -> [(lb,lb)] + (Label lb) + => [lb] -- ^ oldnode values + -> [lb] -- ^ nodes to be avoided + -> (lb -> lb) + -> [(lb,lb)] -- ^ accumulator + -> [(lb,lb)] maplist [] _ _ mapbn = mapbn maplist (dn:dupbn) allbn cnvbn mapbn = maplist dupbn allbn' cnvbn mapbn' where diff --git a/Swish/RDF/RDFProof.hs b/Swish/RDF/RDFProof.hs --- a/Swish/RDF/RDFProof.hs +++ b/Swish/RDF/RDFProof.hs @@ -157,7 +157,10 @@ -- -- > allNodes (not . labelIsVar) graph -- -makeRdfInstanceEntailmentRule :: ScopedName -> [RDFLabel] -> RDFRule +makeRdfInstanceEntailmentRule :: + ScopedName -- ^ name + -> [RDFLabel] -- ^ vocabulary + -> RDFRule makeRdfInstanceEntailmentRule name vocab = newrule where newrule = Rule diff --git a/Swish/RDF/RDFProofContext.hs b/Swish/RDF/RDFProofContext.hs --- a/Swish/RDF/RDFProofContext.hs +++ b/Swish/RDF/RDFProofContext.hs @@ -302,7 +302,8 @@ -- RDF entailment rules (from RDF semantics document section 7.2) -- -- (Note, statements with property rdf:_allocatedTo are introduced to --- track bnodes introduced according to rule rdflf.) +-- track bnodes introduced according to rule rdflf [presumably this +-- is actually rdflg?]) -- rdfr1 :: RDFRule rdfr1 = makeN3ClosureSimpleRule scopeRDF "r1" @@ -559,7 +560,8 @@ -- RDFS entailment rules (from RDF semantics document section 7.2) -- -- (Note, statements with property rdf:_allocatedTo are introduced to --- track bnodes introduced according to rule rdflf.) +-- track bnodes introduced according to rule rdflf [presumably this +-- is actually rdflg?]) -- rdfsr1 :: RDFRule rdfsr1 = makeN3ClosureRule scopeRDFS "r1" diff --git a/Swish/RDF/RDFRuleset.hs b/Swish/RDF/RDFRuleset.hs --- a/Swish/RDF/RDFRuleset.hs +++ b/Swish/RDF/RDFRuleset.hs @@ -11,7 +11,7 @@ -- Portability : H98 -- -- This module defines some datatypes and functions that are --- used to define rules and rulesets over RDF graphs +-- used to define rules and rulesets over RDF graphs. -- -------------------------------------------------------------------------------- @@ -23,12 +23,13 @@ , makeRDFGraphFromN3String , makeRDFFormula , makeRDFClosureRule + -- * Create rules using Notation3 statements , makeN3ClosureRule , makeN3ClosureSimpleRule , makeN3ClosureModifyRule , makeN3ClosureAllocatorRule , makeNodeAllocTo - -- for debugging + -- * Debugging , graphClosureFwdApply, graphClosureBwdApply ) where @@ -111,6 +112,7 @@ -- Declare null RDF formula ------------------------------------------------------------ +-- | The null RDF formula. nullRDFFormula :: Formula RDFGraph nullRDFFormula = Formula { formName = ScopedName nullScope "nullRDFGraph" @@ -162,11 +164,14 @@ , checkInference = fwdCheckInference newrule } --- Forward chaining function based on RDF graph closure description +-- | Forward chaining function based on RDF graph closure description -- -- Note: antecedents here are presumed to share bnodes. -- -graphClosureFwdApply :: GraphClosure RDFLabel -> [RDFGraph] -> [RDFGraph] +graphClosureFwdApply :: + GraphClosure RDFLabel + -> [RDFGraph] + -> [RDFGraph] graphClosureFwdApply grc grs = let gr = if null grs then emptyRDFGraph else foldl1 add grs vars = queryFind (ruleAnt grc) gr @@ -186,7 +191,7 @@ if null cons then [] else [foldl1 add cons] -- cons {- don't merge results -} --- Backward chaining function based on RDF graph closure description +-- | Backward chaining function based on RDF graph closure description graphClosureBwdApply :: GraphClosure RDFLabel -> RDFGraph -> [[RDFGraph]] graphClosureBwdApply grc gr = let vars = rdfQueryBackModify (ruleModify grc) $ @@ -241,8 +246,8 @@ -- |Create an RDF formula. makeRDFFormula :: - Namespace - -> String -- ^ local name + Namespace -- ^ namespace to which the formula is allocated + -> String -- ^ local name for the formula in the namespace -> String -- ^ graph in Notation 3 format -> RDFFormula makeRDFFormula scope local gr = Formula @@ -300,11 +305,6 @@ -- implementation of most of the inference rules given in the -- RDF formal semantics document. -- --- scope is a namespace to which the rule is allocated --- local is a local name for the rule in the given namespace --- ant is a string containing --- con is a string containing --- makeN3ClosureRule :: Namespace -- ^ namespace to which the rule is allocated -> String -- ^ local name for the rule in the namespace @@ -325,7 +325,8 @@ -- into an inference process. -- -- If no additional constraints or variable bindings are - -- to be applied, use value 'varBindingId' + -- to be applied, use a value of 'varBindingId', or use + -- 'makeN3ClosureSimpleRule'. -> RDFRule makeN3ClosureRule scope local ant con = makeRDFClosureRule (ScopedName scope local) [antgr] congr @@ -337,7 +338,14 @@ -- additional node allocations or variable binding constraints. -- makeN3ClosureSimpleRule :: - Namespace -> String -> String -> String -> RDFRule + Namespace -- ^ namespace to which the rule is allocated + -> String -- ^ local name for the rule in the namepace + -> String + -- ^ the Notation3 representation + -- of the antecedent graph. (Note: multiple antecedents + -- can be handled by combining multiple graphs.) + -> String -- ^ the Notation3 representation of the consequent graph. + -> RDFRule makeN3ClosureSimpleRule scope local ant con = makeN3ClosureRule scope local ant con varBindingId @@ -387,13 +395,6 @@ -- the variable binding modifier is a function from the variables in -- the variables and bnodes contained in the antecedent graph. -- --- scope is a --- local is a --- ant is a string containing --- con is a string containing --- vflt is a --- aloc is a --- makeN3ClosureAllocatorRule :: Namespace -- ^ namespace to which the rule is allocated -> String -- ^ local name for the rule in the given namespace @@ -430,7 +431,7 @@ -- Query binding modifier for "allocated to" logic ------------------------------------------------------------ --- |This function defines a variable binding mofifier that +-- |This function defines a variable binding modifier that -- allocates a new blank node for each value bound to -- a query variable, and binds it to another variable -- in each query binding. @@ -457,15 +458,15 @@ -- giving: -- -- > Jimmy hasFather _:f . --- > _:f hasBrother Fred . --- > _:f hasBrother Bob . +-- > _:f hasBrother Fred . +-- > _:f hasBrother Bob . -- -- rather than: -- -- > Jimmy hasFather _:f1 . --- > _:f1 hasBrother Fred . +-- > _:f1 hasBrother Fred . -- > Jimmy hasFather _:f2 . --- > _:f2 hasBrother Bob . +-- > _:f2 hasBrother Bob . -- -- This form of constrained allocation of bnodes is also required for -- some of the inference patterns described by the RDF formal semantics, diff --git a/Swish/RDF/Rule.hs b/Swish/RDF/Rule.hs --- a/Swish/RDF/Rule.hs +++ b/Swish/RDF/Rule.hs @@ -72,10 +72,11 @@ newEntry (_,form) = form keyVal form = (formName form, form) --- | The namespace @http://id.ninebynine.org/2003/Ruleset/null@ +-- | The namespace @http:\/\/id.ninebynine.org\/2003\/Ruleset\/null@ nullScope :: Namespace nullScope = Namespace "null" "http://id.ninebynine.org/2003/Ruleset/null" +-- | The null formula. nullFormula :: Formula ex nullFormula = Formula { formName = ScopedName nullScope "nullFormula" @@ -86,7 +87,12 @@ -- testf2 = Formula "f2" ('f',2) -- |Return a displayable form of a list of labelled formulae -showsFormulae :: (ShowM ex) => String -> [Formula ex] -> String -> ShowS +showsFormulae :: + (ShowM ex) + => String -- ^ newline + -> [Formula ex] -- ^ the formulae to show + -> String -- ^ text to be placed after the formulae + -> ShowS showsFormulae _ [] _ = id showsFormulae newline [f] after = showsFormula newline f . showString after @@ -95,7 +101,11 @@ showsFormulae newline fs after -- |Create a displayable form of a labelled formula -showsFormula :: (ShowM ex) => String -> Formula ex -> ShowS +showsFormula :: + (ShowM ex) + => String -- ^ newline + -> Formula ex -- ^ formula + -> ShowS showsFormula newline f = showsWidth 16 ("["++show (formName f)++"] ") . showms (newline ++ replicate 16 ' ') (formExpr f) @@ -160,15 +170,28 @@ type RuleMap ex = LookupMap (Rule ex) -fwdCheckInference :: (Eq ex) => Rule ex -> [ex] -> ex -> Bool +-- | Checks that consequence is a result of +-- applying the rule to the antecedants. +fwdCheckInference :: + (Eq ex) + => Rule ex -- ^ rule + -> [ex] -- ^ antecedants + -> ex -- ^ consequence + -> Bool fwdCheckInference rule ante cons = cons `elem` fwdApply rule ante -bwdCheckInference :: (Eq ex) => Rule ex -> [ex] -> ex -> Bool +bwdCheckInference :: + (Eq ex) + => Rule ex -- ^ rule + -> [ex] -- ^ antecedants + -> ex -- ^ consequence + -> Bool bwdCheckInference rule ante cons = any checkAnts (bwdApply rule cons) where checkAnts = all (`elem` ante) +-- | The null rule. nullRule :: Rule ex nullRule = Rule { ruleName = ScopedName nullScope "nullRule" diff --git a/Swish/RDF/SwishCommands.hs b/Swish/RDF/SwishCommands.hs --- a/Swish/RDF/SwishCommands.hs +++ b/Swish/RDF/SwishCommands.hs @@ -80,7 +80,7 @@ import System.IO.Error -import Data.Maybe (isJust) +import Data.Maybe (isJust, fromMaybe) ------------------------------------------------------------ -- Set file format to supplied value @@ -215,7 +215,7 @@ Maybe FilePath -- ^ file name -> SwishStateIO QName -- ^ base URI -calculateBaseURI Nothing = maybe defURI id `liftM` gets base +calculateBaseURI Nothing = fromMaybe defURI `liftM` gets base calculateBaseURI (Just fnam) = do mbase <- gets base @@ -310,7 +310,7 @@ swishReadFile conv errVal fnam = let reader (h,f,i) = do res <- conv fnam i - when (f) $ lift $ hClose h + when f $ lift $ hClose h return res in swishOpenFile fnam >>= maybe (return errVal) reader @@ -363,7 +363,7 @@ Right res -> return $ Just res case fmt of - N3 -> readIn (flip parseN3 (Just buri)) + N3 -> readIn (`parseN3` (Just buri)) NT -> readIn parseNT {- _ -> swishError ("Unsupported file format: "++show fmt) SwishArgumentError >> @@ -375,7 +375,7 @@ -> Maybe String -> SwishStateIO () swishWriteFile conv fnam = - let hdlr (h, c) = conv fnam h >> when (c) (lift $ hClose h) + let hdlr (h, c) = conv fnam h >> when c (lift $ hClose h) in swishCreateWriteableFile fnam >>= maybe (return ()) hdlr -- | Open file for writing, returning its handle, or Nothing @@ -389,7 +389,7 @@ if hwt then return $ Just (stdout, False) else do - swishError ("Cannot write to standard output") SwishDataAccessError + swishError "Cannot write to standard output" SwishDataAccessError return Nothing swishCreateWriteableFile (Just fnam) = do diff --git a/Swish/RDF/SwishScript.hs b/Swish/RDF/SwishScript.hs --- a/Swish/RDF/SwishScript.hs +++ b/Swish/RDF/SwishScript.hs @@ -1,27 +1,73 @@ -------------------------------------------------------------------------------- -- See end of this file for licence information. -------------------------------------------------------------------------------- --- | --- Module : SwishScript --- Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke --- License : GPL V2 --- --- Maintainer : Douglas Burke --- Stability : experimental --- Portability : H98 --- --- This module implements the Swish script processor: it parses a script --- from a supplied string, and returns a list of Swish state transformer --- functions whose effect, when applied to a state value, is to implement --- the supplied script. --- --- The script syntax is based loosely on Notation3, and the script parser is an --- extension of the Notation3 parser in the module "Swish.RDF.N3Parser". --- --------------------------------------------------------------------------------- +{- | +Module : SwishScript +Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke +License : GPL V2 +Maintainer : Douglas Burke +Stability : experimental +Portability : H98 + +This module implements the Swish script processor: it parses a script +from a supplied string, and returns a list of Swish state transformer +functions whose effect, when applied to a state value, is to implement +the supplied script. + +-} + module Swish.RDF.SwishScript - ( parseScriptFromString ) + ( + -- * Syntax + -- $syntax + + -- ** Defining a prefix + -- $prefixLine + + -- ** Naming a graph + -- $nameItem + + -- ** Reading and writing graphs + + -- $readGraph + + -- $writeGraph + + -- ** Merging graphs + -- $mergeGraphs + + -- ** Comparing graphs + + -- $compareGraphs + + -- $assertEquiv + + -- $assertMember + + -- ** Defining rules + + -- $defineRule + + -- $defineRuleset + + -- $defineConstraints + + -- ** Apply a rule + -- $fwdChain + + -- $bwdChain + + -- ** Define a proof + -- $proof + + -- * An example script + -- $exampleScript + + -- * Parsing + + parseScriptFromString + ) where import Swish.RDF.SwishMonad @@ -105,15 +151,19 @@ ( equiv, flist ) import Text.ParserCombinators.Parsec - ( (), (<|>) - , many, manyTill, option, sepBy, between, try, notFollowedBy + ( () + -- , (<|>) + -- , many + , manyTill + , option, sepBy, between, try, notFollowedBy , string, anyChar , getState ) +import Control.Applicative + import Control.Monad.State ( modify, gets, lift - -- , StateT(..), execStateT ) import Control.Monad (unless, when, liftM) @@ -133,13 +183,31 @@ -- -- | Parser for Swish script processor -parseScriptFromString :: Maybe QName -> String -> Either String [SwishStateIO ()] +parseScriptFromString :: + Maybe QName -- ^ Default base for the script + -> String -- ^ Swish script + -> Either String [SwishStateIO ()] parseScriptFromString = parseAnyfromString script ---------------------------------------------------------------------- -- Syntax productions ---------------------------------------------------------------------- +n3SymLex :: N3Parser ScopedName +n3SymLex = lexeme n3symbol + +setTo :: N3Parser () +setTo = isymbol ":-" + +semicolon :: N3Parser () +semicolon = isymbol ";" + +comma :: N3Parser () +comma = isymbol "," + +commentText :: N3Parser String +commentText = semicolon *> restOfLine + script :: N3Parser [SwishStateIO ()] script = do whiteSpace @@ -176,85 +244,65 @@ isymbol "." return $ return () +-- name :- graph +-- name :- ( graph* ) nameItem :: N3Parser (SwishStateIO ()) -nameItem = - -- name :- graph - -- name :- ( graph* ) - do { u <- lexeme n3symbol - ; isymbol ":-" - ; g <- graphOrList - ; return $ ssAddGraph u g - } +nameItem = + ssAddGraph <$> n3SymLex <*> (symbol ":-" *> graphOrList) + +maybeURI :: N3Parser (Maybe String) +maybeURI = (Just <$> lexUriRef) <|> return Nothing +-- @read name [ ] readGraph :: N3Parser (SwishStateIO ()) -readGraph = - -- @read name [ ] - do { commandName "@read" - ; n <- lexeme n3symbol - ; u <- option "" $ lexUriRef - ; return $ ssRead n (if null u then Nothing else Just u) - } +readGraph = commandName "@read" *> (ssRead <$> n3SymLex <*> maybeURI) +-- @write name [ ] ; Comment writeGraph :: N3Parser (SwishStateIO ()) writeGraph = - -- @write name [ ] ; Comment do { commandName "@write" - ; n <- lexeme n3symbol + ; n <- n3SymLex ; let gs = ssGetList n :: SwishStateIO (Either String [RDFGraph]) - ; u <- option "" lexUriRef - ; isymbol ";" - ; c <- restOfLine - ; let muri = if null u then Nothing else Just u + ; muri <- maybeURI + ; c <- commentText ; return $ ssWriteList muri gs c } +-- @merge ( name* ) => name mergeGraphs :: N3Parser (SwishStateIO ()) -mergeGraphs = - -- @merge ( name* ) => name - do { commandName "@merge" - ; gs <- graphList - ; isymbol "=>" - ; n <- lexeme n3symbol - ; return $ ssMerge n gs - } +mergeGraphs = do + commandName "@merge" + gs <- graphList + isymbol "=>" + n <- n3SymLex + return $ ssMerge n gs +-- @compare name name compareGraphs :: N3Parser (SwishStateIO ()) compareGraphs = - -- @compare name name - do { commandName "@compare" - ; n1 <- lexeme n3symbol - ; n2 <- lexeme n3symbol - ; return $ ssCompare n1 n2 - } - + commandName "@compare" *> (ssCompare <$> n3SymLex <*> n3SymLex) + +-- @ name name ; Comment +assertArgs :: (ScopedName -> ScopedName -> String -> SwishStateIO ()) + -> String -> N3Parser (SwishStateIO ()) +assertArgs assertFunc cName = do + commandName $ '@':cName + assertFunc <$> n3SymLex <*> n3SymLex <*> commentText + +-- @asserteq name name ; Comment assertEquiv :: N3Parser (SwishStateIO ()) -assertEquiv = - -- @asserteq name name ; Comment - do { commandName "@asserteq" - ; n1 <- lexeme n3symbol - ; n2 <- lexeme n3symbol - ; isymbol ";" - ; c <- restOfLine - ; return $ ssAssertEq n1 n2 c - } - +assertEquiv = assertArgs ssAssertEq "asserteq" + +-- @assertin name name ; Comment assertMember :: N3Parser (SwishStateIO ()) -assertMember = - -- @assertin name name ; Comment - do { commandName "@assertin" - ; n1 <- lexeme n3symbol - ; n2 <- lexeme n3symbol - ; isymbol ";" - ; c <- restOfLine - ; return $ ssAssertIn n1 n2 c - } - +assertMember = assertArgs ssAssertIn "assertin" + +-- @rule name :- ( name* ) => name [ | ( (name var*)* ) ] defineRule :: N3Parser (SwishStateIO ()) defineRule = - -- @rule name :- ( name* ) => name [ | ( (name var*)* ) ] do { commandName "@rule" - ; rn <- lexeme n3symbol - ; isymbol ":-" + ; rn <- n3SymLex + ; setTo ; ags <- graphOrList ; isymbol "=>" ; cg <- graphExpr @@ -262,38 +310,26 @@ ; return $ ssDefineRule rn ags cg vms } +-- @ruleset name :- ( name* ) ; ( name* ) defineRuleset :: N3Parser (SwishStateIO ()) defineRuleset = - -- @ruleset name :- ( name* ) ; ( name* ) - do { commandName "@ruleset" - ; sn <- lexeme n3symbol - ; isymbol ":-" - ; ags <- nameList - ; isymbol ";" - ; rns <- nameList - ; return $ ssDefineRuleset sn ags rns - } - + commandName "@ruleset" *> + (ssDefineRuleset <$> n3SymLex <*> (setTo *> nameList) <*> (semicolon *> nameList)) + +-- @constraints pref :- ( name* ) | ( name* ) defineConstraints :: N3Parser (SwishStateIO ()) defineConstraints = - -- @constraints pref :- ( name* ) | ( name* ) - do { commandName "@constraints" - ; sn <- lexeme n3symbol - ; isymbol ":-" - ; cgs <- graphOrList - ; isymbol "|" - ; cns <- nameOrList - ; return $ ssDefineConstraints sn cgs cns - } - + commandName "@constraints" *> + (ssDefineConstraints <$> n3SymLex <*> (setTo *> graphOrList) <*> (symbol "|" *> nameOrList)) + +-- @proof name ( name* ) +-- @input name +-- @step name ( name* ) => name # rule-name, antecedents, consequent +-- @result name checkProofCmd :: N3Parser (SwishStateIO ()) checkProofCmd = - -- @proof name ( name* ) - -- @input name - -- @step name ( name* ) => name # rule-name, antecedents, consequent - -- @result name do { commandName "@proof" - ; pn <- lexeme n3symbol + ; pn <- n3SymLex ; sns <- nameList ; commandName "@input" ; igf <- formulaExpr @@ -307,39 +343,34 @@ N3Parser (Either String [RDFRuleset] -> SwishStateIO (Either String RDFProofStep)) checkStep = - do { commandName "@step" - ; rn <- lexeme n3symbol - ; agfs <- formulaList - ; isymbol "=>" - ; cgf <- formulaExpr - ; return $ ssCheckStep rn agfs cgf - } + commandName "@step" *> + (ssCheckStep <$> n3SymLex <*> formulaList <*> (symbol "=>" *> formulaExpr)) +-- # ruleset rule (antecedents) => result +-- @fwdchain pref name ( name* ) => name fwdChain :: N3Parser (SwishStateIO ()) fwdChain = - -- # ruleset rule (antecedents) => result - -- @fwdchain pref name ( name* ) => name do { commandName "@fwdchain" - ; sn <- lexeme n3symbol - ; rn <- lexeme n3symbol + ; sn <- n3SymLex + ; rn <- n3SymLex ; ags <- graphOrList ; isymbol "=>" - ; cn <- lexeme n3symbol + ; cn <- n3SymLex ; s <- getState :: N3Parser N3State ; let prefs = prefixUris s :: NamespaceMap ; return $ ssFwdChain sn rn ags cn prefs } +-- # ruleset rule consequent <= (antecedent-alts) +-- @bwdchain pref name graph <= name bwdChain :: N3Parser (SwishStateIO ()) bwdChain = - -- # ruleset rule consequent <= (antecedent-alts) - -- @bwdchain pref name graph <= name do { commandName "@bwdchain" - ; sn <- lexeme n3symbol - ; rn <- lexeme n3symbol + ; sn <- n3SymLex + ; rn <- n3SymLex ; cg <- graphExpr ; isymbol "<=" - ; an <- lexeme n3symbol + ; an <- n3SymLex ; s <- getState :: N3Parser N3State ; let prefs = prefixUris s :: NamespaceMap ; return $ ssBwdChain sn rn cg an prefs @@ -350,43 +381,32 @@ ---------------------------------------------------------------------- commandName :: String -> N3Parser () -commandName cmd = try $ - do { _ <- string cmd - ; notFollowedBy identLetter - ; whiteSpace - } +commandName cmd = try (string cmd *> notFollowedBy identLetter *> whiteSpace) --- taken ftom NTParser +-- taken from NTParser eoln :: N3Parser () -- eoln = ignore (newline <|> (lineFeed *> optional newline)) eoln = (try (string "\r\n") <|> string "\r" <|> string "\n") >> return () "new line" restOfLine :: N3Parser String -restOfLine = - do { s <- manyTill anyChar eoln - ; whiteSpace - ; return s - } +restOfLine = manyTill anyChar eoln <* whiteSpace + +br :: N3Parser a -> N3Parser a +br = between (symbol "(") (symbol ")") nameList :: N3Parser [ScopedName] -nameList = - do { isymbol "(" - ; ns <- many (lexeme n3symbol) - ; isymbol ")" - ; return ns - } - +nameList = br $ many n3SymLex + +toList :: a -> [a] +toList = (:[]) + nameOrList :: N3Parser [ScopedName] nameOrList = - do { n <- lexeme n3symbol - ; return [n] - } - <|> - nameList - - "Name, or list of names" - + (toList <$> n3SymLex) + <|> nameList + "Name, or list of names" + graphExpr :: N3Parser (SwishStateIO (Either String RDFGraph)) graphExpr = graphOnly @@ -409,64 +429,39 @@ } graphList :: N3Parser [SwishStateIO (Either String RDFGraph)] -graphList = between (symbol "(") (symbol ")") (many graphExpr) - - "List of graphs" +graphList = br (many graphExpr) + "List of graphs" graphOrList :: N3Parser [SwishStateIO (Either String RDFGraph)] graphOrList = - do { g <- graphExpr - ; return [g] - } - <|> - graphList - - "Graph, or list of graphs" + (toList <$> graphExpr) + <|> graphList + "Graph, or list of graphs" formulaExpr :: N3Parser (SwishStateIO (Either String RDFFormula)) -formulaExpr = - do { n <- lexeme n3symbol - ; namedGraph n - } - "Formula (name or named graph)" +formulaExpr = + (n3SymLex >>= namedGraph) + "Formula (name or named graph)" namedGraph :: ScopedName -> N3Parser (SwishStateIO (Either String RDFFormula)) namedGraph n = - do { isymbol ":-" - ; g <- graphOnly - ; return $ ssAddReturnFormula n g - } - <|> - return (ssGetFormula n) + (ssAddReturnFormula n <$> (setTo *> graphOnly)) + <|> return (ssGetFormula n) formulaList :: N3Parser [SwishStateIO (Either String RDFFormula)] formulaList = between (symbol "(") (symbol ")") (many formulaExpr) - - "List of formulae (names or named graphs)" + "List of formulae (names or named graphs)" varModifiers :: N3Parser [(ScopedName,[RDFLabel])] -varModifiers = - do { isymbol "|" - ; varModList - } +varModifiers = symbol "|" *> varModList varModList :: N3Parser [(ScopedName,[RDFLabel])] -varModList = - do { isymbol "(" - ; vms <- sepBy varMod (symbol ",") - ; isymbol ")" - ; return vms - } - <|> - do { vm <- lexeme varMod - ; return [vm] - } +varModList = + br (sepBy varMod comma) + <|> toList <$> lexeme varMod varMod :: N3Parser (ScopedName,[RDFLabel]) -varMod = do - rn <- lexeme n3symbol - vns <- many $ lexeme quickVariable - return (rn,vns) +varMod = (,) <$> n3SymLex <*> many (lexeme quickVariable) ---------------------------------------------------------------------- -- SwishState helper functions @@ -514,11 +509,8 @@ } ssGetGraph :: ScopedName -> SwishStateIO (Either String RDFGraph) -ssGetGraph nam = - do { grs <- ssGetList nam - ; return $ liftM head grs - } - +ssGetGraph nam = liftM head <$> ssGetList nam + ssGetFormula :: ScopedName -> SwishStateIO (Either String RDFFormula) ssGetFormula nam = gets find where @@ -551,11 +543,10 @@ do { esgs <- gf ; case esgs of Left er -> modify $ setError ("Cannot write list: "++er) + Right [] -> putResourceData Nothing (("# " ++ comment ++ "\n+ Swish: Writing empty list")++) Right [gr] -> ssWriteGraph muri gr comment - Right grs -> sequence_ writegrs where - writegrs = if null grs - then [putResourceData Nothing ("+ Swish: Writing empty list"++)] - else map writegr (zip [(0::Int)..] grs) + Right grs -> mapM_ writegr (zip [(0::Int)..] grs) + where writegr (n,gr) = ssWriteGraph (murin muri n) gr ("["++show n++"] "++comment) murin Nothing _ = Nothing @@ -836,7 +827,7 @@ -> SwishStateIO (Either String RDFFormula) -- consequent graph formula -> Either String [RDFRuleset] -- rulesets -> SwishStateIO (Either String RDFProofStep) -- resulting proof step -ssCheckStep _ _ _ (Left er) = return $ Left er +ssCheckStep _ _ _ (Left er) = return $ Left er ssCheckStep rn eagf ecgf (Right rss) = let errmsg1 = "Rule not in proof step ruleset(s): " @@ -968,6 +959,579 @@ toUri uri | "file://" `isPrefixOf` uri = writeFile (drop 7 uri) gstr | otherwise = error $ "Unsupported file name for write: " ++ uri gstr = gsh "\n" + +{- $syntax + +The script syntax is based loosely on Notation3, and the script parser is an +extension of the Notation3 parser in the module "Swish.RDF.N3Parser". +The comment character is @#@ and white space is ignored. + +> script := command * +> command := prefixLine | +> nameItem | +> readGraph | +> writeGraph | +> mergeGraphs | +> compareGraphs | +> assertEquiv | +> assertMember | +> defineRule | +> defineRuleset | +> defineConstraints | +> checkProofCmd | +> fwdChain | +> bwdChain + +-} + +{- $prefixLine + +> prefixLine := @prefix []: . + +Define a namespace prefix and URI. + +The prefix thus defined is available for use in any subsequent script +command, and also in any graphs contained within the script file. (So, +prefix declarations do not need to be repeated for each graph +contained within the script.) + +Graphs read from external files must contain their own prefix +declarations. + +Example: + + > @prefix gex: . + > @prefix : . + +-} + +{- $nameItem + +> nameItem := name :- graph | +> name :- ( graph* ) + +Graphs or lists of graphs can be given a name for use in other +statements. A name is a qname (prefix:local) or a URI enclosed in +angle + +Example: + +> @prefix ex1: . +> @prefix ex2: . +> +> ex1:gr1 :- { +> ex2:foo a ex2:Foo . +> ex2:bar a ex2:Bar . +> ex2:Bar rdfs:subClassOf ex2:Foo . +> } + +-} + +{- $readGraph + +> readGraph := @read name [] + +The @\@read@ command reads in the contents of the given URI +- which at present only supports reading local files, so +no HTTP access - and stores it under the given name. + +If no URI is given then the file is read from standard input. + +Example: + + > @prefix ex: . + > @read ex:foo + +-} + +{- $writeGraph + +> writeGraph := @write name [] ; comment + +The @\@write@ command writes out the contents of the given graph +- which at present only supports writing local files, so +no HTTP access. The comment text is written as a comment line +preceeding the graph contents. + +If no URI is given then the file is written to the standard output. + +Example: + + > @prefix ex: . + > @read ex:gr1 + > @read ex:gr2 + > @merge (ex:gr1 ex:gr2) => ex:gr3 + > @write ex:gr3 ; the merged data + > @write ex:gr3 ; merge of graph1.n3 and graph2.n3 + +-} + +{- $mergeGraphs + +> mergeGraphs := @merge ( name* ) => name + +Create a new named graph that is the merge two or more graphs, +renaming bnodes as required to avoid node-merging. + +When the merge command is run, the message + + > # Merge: + +will be created on the standard output channel. + +Example: + + > @prefix gex: . + > @prefix ex: . + > gex:gr1 :- { ex:foo ex:bar _:b1 . } + > gex:gr2 :- { _:b1 ex:foobar 23. } + > @merge (gex:gr1 gex:gr2) => gex:gr3 + > @write gex:gr3 ; merged graphs + +When run in Swish, this creates the following output (along with +several other namespace declarations): + + > # merged graphs + > @prefix ex: . + > ex:foo ex:bar [] . + > [ + > ex:foobar "23"^^xsd:integer + > ] . + +-} + +{- $compareGraphs + +> compareGraphs := @compare name name + +Compare two graphs for isomorphism, setting the Swish exit status to +reflect the result. + +When the compare command is run, the message + + > # Compare: + +will be created on the standard output channel. + +Example: + + > @prefix gex: . + > @read gex:gr1 + > @read gex:gr2 + > @compare gex:gr1 gex:gr2 + +-} + +{- $assertEquiv + +> assertEquiv := @asserteq name name ; comment + +Test two graphs or lists of graphs for isomorphism, reporting if they +differ. The comment text is included with any report generated. + +When the command is run, the message + + > # AssertEq: + +will be created on the standard output channel. + +Example: + + > @prefix ex: . + > + > # Set up the graphs for the rules + > ex:Rule01Ant :- { ?p ex:son ?o . } + > ex:Rule01Con :- { ?o a ex:Male ; ex:parent ?p . } + > + > # Create a rule and a ruleset + > @rule ex:Rule01 :- ( ex:Rule01Ant ) => ex:Rule01Con + > @ruleset ex:rules :- (ex:TomSonDick ex:TomSonHarry) ; (ex:Rule01) + > + > # Apply the rule + > @fwdchain ex:rules ex:Rule01 { :Tom ex:son :Charles . } => ex:Rule01fwd + > + > # Compare the results to the expected value + > ex:ExpectedRule01fwd :- { :Charles a ex:Male ; ex:parent :Tom . } + > @asserteq ex:Rule01fwd ex:ExpectedRule01fwd + > ; Infer that Charles is male and has parent Tom + +-} + +{- $assertMember + +> assertMember := @assertin name name ; comment + +Test if a graph is isomorphic to a member of a list of graphs, +reporting if no match is found. The comment text is included with any +report generated. + +Example: + +> @bwdchain pv:rules :PassengerVehicle ex:Test01Inp <= :t1b +> +> @assertin ex:Test01Bwd0 :t1b ; Backward chain component test (0) +> @assertin ex:Test01Bwd1 :t1b ; Backward chain component test (1) + +-} + +{- $defineRule + +> defineRule := @rule name :- ( name* ) => name +> defineRule := @rule name :- ( name* ) => name +> | ( (name var*)* ) + +Define a named Horn-style rule. + +The list of names preceding and following @=>@ are the antecedent and consequent +graphs, respectivelu. Both sets may contain variable nodes of the form +@?var@. + +The optional part, after the @|@ separator, is a list of variable +binding modifiers, each of which consists of a name and a list of +variables (@?var@) to which the modifier is applied. Variable binding +modifiers are built in to Swish, and are used to incorporate datatype +value inferences into a rule. + +-} + +{- $defineRuleset + +> defineRuleset := @ruleset name :- ( name* ) ; ( name* ) + +Define a named ruleset (a collection of axioms and rules). The first +list of names are the axioms that are part of the ruleset, and the +second list are the rules. + +-} + +{- $defineConstraints + +> defineConstraints := @constraints pref :- ( name* ) | [ name | ( name* ) ] + +Define a named ruleset containing class-restriction rules based on a +datatype value constraint. The first list of +names is a list of graphs that together comprise the class-restriction +definitions (rule names are the names of the corresponding restriction +classes). The second list of names is a list of datatypes whose +datatype relations are referenced by the class restriction +definitions. + +-} + +{- $fwdChain + +> fwdChain := @fwdchain pref name ( name* ) => name + +Define a new graph obtained by forward-chaining a rule. The first name +is the ruleset to be used. The second name is the rule name. The list +of names are the antecedent graphs to which the rule is applied. The +name following the @=>@ names a new graph that is the result of formward +chaining from the given antecedents using the indicated rule. + +-} + +{- $bwdChain + +> bwdChain := @bwdchain pref name graph <= name + +Define a new list of alternative graphs obtained by backward-chaining +a rule. The first name is the ruleset to be used. The second name is +the rule name. The third name (before the @<=@) is the name of a goal graph +from which to backward chain. The final name (after the @<=@) names a new +list of graphs, each of which is an alternative antecedent from which +the given goal can be deduced using the indicated rule. + + +-} + +{- $proof + +> checkProofCmd := proofLine nl +> inputLine nl +> (stepLine nl)* +> resultLine +> proofLine := @proof name ( name* ) + +Check a proof, reporting the step that fails, if any. + +The @\@proof@ line names the proof and specifies a list rulesets +(proof context) used. The remaining lines specify the input +expression (@\@input@), proof steps (@\@step@) and the final result +(@\@result@) that is demonstrated by the proof. + +> inputLine := @input name + +In a proof, indicates an input expression upon which the proof is +based. Exactly one of these immediately follows the @\@proof@ command. + +> stepLine := @step name ( name* ) => name + +This defines a step of the proof; any number of these immediately +follow the @\@input@ command. + +It indicates the name of the rule applied for this step, a list of +antecedent graphs, and a named graph that is deduced by this step. +For convenience, the deduced graph may introduce a new named graph +using an expression of the form: + + > name :- { statements } + +> resultLine := @result name + +This defines the goal of the proof, and completes a proof +definition. Exactly one of these immediately follows the @\@step@ +commands. For convenience, the result statement may introduce a new +named graph using an expression of the form: + + > name :- { statements } + +-} + +{- $exampleScript + +This is the example script taken from + +with the proof step adjusted so that it passes. + +> # -- Example Swish script -- +> # +> # Comment lines start with a '#' +> # +> # The script syntax is loosely based on Notation3, but it is a quite +> # different language, except that embedded graphs (enclosed in {...}) +> # are encoded using Notation3 syntax. +> # +> # -- Prefix declarations -- +> # +> # As well as being used for all labels defined and used by the script +> # itself, these are applied to all graph expressions within the script +> # file, and to graphs created by scripted inferences, +> # but are not applied to any graphs read in from an external source. +> +> @prefix ex: . +> @prefix pv: . +> @prefix xsd: . +> @prefix xsd_integer: . +> @prefix rs_rdf: . +> @prefix rs_rdfs: . +> @prefix : . +> +> # Additionally, prefix declarations are provided automatically for: +> # @prefix rdf: . +> # @prefix rdfs: . +> # @prefix rdfd: . +> # @prefix rdfo: . +> # @prefix owl: . +> +> # -- Simple named graph declarations -- +> +> ex:Rule01Ant :- { ?p ex:son ?o . } +> +> ex:Rule01Con :- { ?o a ex:Male ; ex:parent ?p . } +> +> ex:TomSonDick :- { :Tom ex:son :Dick . } +> ex:TomSonHarry :- { :Tom ex:son :Harry . } +> +> # -- Named rule definition -- +> +> @rule ex:Rule01 :- ( ex:Rule01Ant ) => ex:Rule01Con +> +> # -- Named ruleset definition -- +> # +> # A 'ruleset' is a collection of axioms and rules. +> # +> # Currently, the ruleset is identified using the namespace alone; +> # i.e. the 'rules' in 'ex:rules' below is not used. +> # This is under review. +> +> @ruleset ex:rules :- (ex:TomSonDick ex:TomSonHarry) ; (ex:Rule01) +> +> # -- Forward application of rule -- +> # +> # The rule is identified here by ruleset and a name within the ruleset. +> +> @fwdchain ex:rules ex:Rule01 { :Tom ex:son :Charles . } => ex:Rule01fwd +> +> # -- Compare graphs -- +> # +> # Compare result of inference with expected result. +> # This is a graph isomorphism test rather than strict equality, +> # to allow for bnode renaming. +> # If the graphs are not equal, a message is generated, which +> # includes the comment (';' to end of line) +> +> ex:ExpectedRule01fwd :- { :Charles a ex:Male ; ex:parent :Tom . } +> +> @asserteq ex:Rule01fwd ex:ExpectedRule01fwd +> ; Infer that Charles is male and has parent Tom +> +> # -- Display graph (to screen and a file) -- +> # +> # The comment is included in the output. +> +> @write ex:Rule01fwd ; Charles is male and has parent Tom +> @write ex:Rule01fwd ; Charles is male and has parent Tom +> +> # -- Read graph from file -- +> # +> # Creates a new named graph in the Swish environment. +> +> @read ex:Rule01inp +> +> # -- Proof check -- +> # +> # This proof uses the built-in RDF and RDFS rulesets, +> # which are the RDF- and RDFS- entailment rules described in the RDF +> # formal semantics document. +> # +> # To prove: +> # ex:foo ex:prop "a" . +> # RDFS-entails +> # ex:foo ex:prop _:x . +> # _:x rdf:type rdfs:Resource . +> # +> # If the proof is not valid according to the axioms and rules of the +> # ruleset(s) used and antecedents given, then an error is reported +> # indicating the failed proof step. +> +> ex:Input :- { ex:foo ex:prop "a" . } +> ex:Result :- { ex:foo ex:prop _:a . _:a rdf:type rdfs:Resource . } +> +> @proof ex:Proof ( rs_rdf:rules rs_rdfs:rules ) +> @input ex:Input +> @step rs_rdfs:r3 ( rs_rdfs:a10 rs_rdfs:a39 ) +> => ex:Stepa :- { rdfs:Literal rdf:type rdfs:Class . } +> @step rs_rdfs:r8 ( ex:Stepa ) +> => ex:Stepb :- { rdfs:Literal rdfs:subClassOf rdfs:Resource . } +> @step rs_rdf:lg ( ex:Input ) +> => ex:Stepc :- { ex:foo ex:prop _:a . _:a rdf:_allocatedTo "a" . } +> @step rs_rdfs:r1 ( ex:Stepc ) +> => ex:Stepd :- { _:a rdf:type rdfs:Literal . } +> @step rs_rdfs:r9 ( ex:Stepb ex:Stepd ) +> => ex:Stepe :- { _:a rdf:type rdfs:Resource . } +> @step rs_rdf:se ( ex:Stepc ex:Stepd ex:Stepe ) +> => ex:Result +> @result ex:Result +> +> # -- Restriction based datatype inferencing -- +> # +> # Datatype inferencing based on a general class restriction and +> # a predefined relation (per idea noted by Pan and Horrocks). +> +> ex:VehicleRule :- +> { :PassengerVehicle a rdfd:GeneralRestriction ; +> rdfd:onProperties (:totalCapacity :seatedCapacity :standingCapacity) ; +> rdfd:constraint xsd_integer:sum ; +> rdfd:maxCardinality "1"^^xsd:nonNegativeInteger . } +> +> # Define a new ruleset based on a declaration of a constraint class +> # and reference to built-in datatype. +> # The datatype constraint xsd_integer:sum is part of the definition +> # of datatype xsd:integer that is cited in the constraint ruleset +> # declaration. It relates named properties of a class instance. +> +> @constraints pv:rules :- ( ex:VehicleRule ) | xsd:integer +> +> # Input data for test cases: +> +> ex:Test01Inp :- +> { _:a1 a :PassengerVehicle ; +> :seatedCapacity "30"^^xsd:integer ; +> :standingCapacity "20"^^xsd:integer . } +> +> # Forward chaining test case: +> +> ex:Test01Fwd :- { _:a1 :totalCapacity "50"^^xsd:integer . } +> +> @fwdchain pv:rules :PassengerVehicle ex:Test01Inp => :t1f +> @asserteq :t1f ex:Test01Fwd ; Forward chain test +> +> # Backward chaining test case: +> # +> # Note that the result of backward chaining is a list of alternatives, +> # any one of which is sufficient to derive the given conclusion. +> +> ex:Test01Bwd0 :- +> { _:a1 a :PassengerVehicle . +> _:a1 :totalCapacity "50"^^xsd:integer . +> _:a1 :seatedCapacity "30"^^xsd:integer . } +> +> ex:Test01Bwd1 :- +> { _:a1 a :PassengerVehicle . +> _:a1 :totalCapacity "50"^^xsd:integer . +> _:a1 :standingCapacity "20"^^xsd:integer . } +> +> # Declare list of graphs: +> +> ex:Test01Bwd :- ( ex:Test01Bwd0 ex:Test01Bwd1 ) +> +> @bwdchain pv:rules :PassengerVehicle ex:Test01Inp <= :t1b +> @asserteq :t1b ex:Test01Bwd ; Backward chain test +> +> # Can test for graph membership in a list +> +> @assertin ex:Test01Bwd0 :t1b ; Backward chain component test (0) +> @assertin ex:Test01Bwd1 :t1b ; Backward chain component test (1) +> +> # -- Merge graphs -- +> # +> # Merging renames bnodes to avoid collisions. +> +> @merge ( ex:Test01Bwd0 ex:Test01Bwd1 ) => ex:Merged +> +> # This form of comparison sets the Swish exit status based on the result. +> +> ex:ExpectedMerged :- +> { _:a1 a :PassengerVehicle . +> _:a1 :totalCapacity "50"^^xsd:integer . +> _:a1 :seatedCapacity "30"^^xsd:integer . +> _:a2 a :PassengerVehicle . +> _:a2 :totalCapacity "50"^^xsd:integer . +> _:a2 :standingCapacity "20"^^xsd:integer . } +> +> @compare ex:Merged ex:ExpectedMerged +> +> # End of example script + +If saved in the file example.ss, then it can be evaluated by saying +either of: + +> % Swish -s=example.ss + +or, from @ghci@: + +> Prelude> :m + Swish.RDF.SwishMain +> Prelude Swish.RDF.SwishMain> :set prompt "Swish> " +> Swish> runSwish "-s=example.ss" + +and the output is + +> # AssertEq: Infer that Charles is male and has parent Tom +> # Charles is male and has parent Tom +> @prefix rdf: . +> @prefix rdfs: . +> @prefix rdfd: . +> @prefix owl: . +> @prefix log: . +> @prefix : . +> @prefix ex: . +> @prefix pv: . +> @prefix xsd: . +> @prefix xsd_integer: . +> @prefix rs_rdf: . +> @prefix rs_rdfs: . +> :Charles ex:parent :Tom ; +> a ex:Male . +> +> Proof satisfied: ex:Proof +> # AssertEq: Forward chain test +> # AssertEq: Backward chain test +> # AssertIn: Backward chain component test (0) +> # AssertIn: Backward chain component test (1) +> # Merge: ex:Merged +> # Compare: ex:Merged ex:ExpectedMerged + +-} -------------------------------------------------------------------------------- -- diff --git a/scripts/SwishExample.ss b/scripts/SwishExample.ss --- a/scripts/SwishExample.ss +++ b/scripts/SwishExample.ss @@ -123,17 +123,37 @@ ex:Result :- { ex:foo ex:prop _:a . _:a rdf:type rdfs:Resource . } +# This is the version from +# http://www.ninebynine.org/RDFNotes/Swish/Intro.html#ScriptExample +# which does not work. It appears that ex:Step01c can not be proved, +# so we split it into two steps in the version below. +# +#@proof ex:Proof01 ( rs_rdf:rules rs_rdfs:rules ) +# @input ex:Input01 +# @step rs_rdfs:r3 ( rs_rdfs:a10 rs_rdfs:a39 ) +# => ex:Step01a :- { rdfs:Literal rdf:type rdfs:Class . } +# @step rs_rdfs:r8 ( ex:Step01a ) +# => ex:Step01b :- { rdfs:Literal rdfs:subClassOf rdfs:Resource . } +# @step rs_rdfs:r1 ( ex:Input01 ) +# => ex:Step01c :- { ex:foo ex:prop _:a . _:a rdf:type rdfs:Literal . } +# @step rs_rdfs:r9 ( ex:Step01b ex:Step01c ) +# => ex:Step01d :- { _:a rdf:type rdfs:Resource . } +# @step rs_rdf:se ( ex:Step01c ex:Step01d ) => ex:Result +# @result ex:Result + @proof ex:Proof01 ( rs_rdf:rules rs_rdfs:rules ) @input ex:Input01 @step rs_rdfs:r3 ( rs_rdfs:a10 rs_rdfs:a39 ) => ex:Step01a :- { rdfs:Literal rdf:type rdfs:Class . } @step rs_rdfs:r8 ( ex:Step01a ) => ex:Step01b :- { rdfs:Literal rdfs:subClassOf rdfs:Resource . } - @step rs_rdfs:r1 ( ex:Input01 ) - => ex:Step01c :- { ex:foo ex:prop _:a . _:a rdf:type rdfs:Literal . } - @step rs_rdfs:r9 ( ex:Step01b ex:Step01c ) + @step rs_rdf:lg ( ex:Input01 ) + => ex:Step01c1 :- { ex:foo ex:prop _:a . _:a rdf:_allocatedTo "a" . } + @step rs_rdfs:r1 ( ex:Step01c1 ) + => ex:Step01c2 :- { _:a rdf:type rdfs:Literal . } + @step rs_rdfs:r9 ( ex:Step01b ex:Step01c2 ) => ex:Step01d :- { _:a rdf:type rdfs:Resource . } - @step rs_rdf:se ( ex:Step01c ex:Step01d ) => ex:Result + @step rs_rdf:se ( ex:Step01c1 ex:Step01c2 ex:Step01d ) => ex:Result @result ex:Result # -- Restriction based datatype inferencing -- diff --git a/swish.cabal b/swish.cabal --- a/swish.cabal +++ b/swish.cabal @@ -1,5 +1,5 @@ Name: swish -Version: 0.3.0.2 +Version: 0.3.0.3 Stability: experimental License: LGPL License-file: LICENSE @@ -44,6 +44,11 @@ * Complete, ready-to-run, command-line and script-driven programs. . Major Changes: + . + [Version 0.3.0.3] Changed @scripts/SwishExample.ss@ script so that the + proof succeeds. Some documentation improvements, including a discussion + of the Swish script format (see "Swish.RDF.SwishScript"). Very minor + changes to behavior of Swish in several edge cases. . [Version 0.3.0.2] Bugfix: stop losing triples with a bnode subject when using the N3Formatter; this also makes the @scripts/SwishTest.ss@ test