{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module Swish.Script
(
parseScriptFromText
)
where
import Swish.Datatype (typeMkRules)
import Swish.Monad ( SwishStateIO, SwishStatus(..))
import Swish.Monad (modGraphs, findGraph, findFormula
, modRules, findRule
, modRulesets, findRuleset
, findOpenVarModify, findDatatype
, setInfo, setError, setStatus)
import Swish.Proof (explainProof, showsProof)
import Swish.Rule (Formula(..), Rule(..))
import Swish.Ruleset (makeRuleset, getRulesetRule, getRulesetNamespace, getMaybeContextRule)
import Swish.VarBinding (composeSequence)
import Swish.RDF.Datatype (RDFDatatype)
import Swish.RDF.Ruleset (RDFFormula, RDFRule, RDFRuleset)
import Swish.RDF.Ruleset (makeRDFClosureRule)
import Swish.RDF.Proof (RDFProofStep)
import Swish.RDF.Proof (makeRDFProof, makeRDFProofStep)
import Swish.RDF.VarBinding (RDFVarBindingModify)
import Swish.RDF.GraphShowLines ()
import Swish.RDF.Graph
( RDFGraph, RDFLabel(..)
, NamespaceMap
, setNamespaces
, merge, addGraphs
)
import Swish.RDF.Parser.Utils (whiteSpace, lexeme, symbol, eoln, manyTill)
import Swish.RDF.Parser.N3
( parseAnyfromText
, parseN3
, N3Parser, N3State(..)
, getPrefix
, subgraph
, n3symbol
, quickVariable
, lexUriRef
, newBlankNode
)
import Swish.Namespace (ScopedName, getScopeNamespace)
import Swish.QName (QName, qnameFromURI)
import Swish.RDF.Formatter.N3 (formatGraphAsBuilder)
import Swish.Utils.ListHelpers (flist)
import Text.ParserCombinators.Poly.StateText
import Control.Monad (unless, when, liftM, void)
import Control.Monad.State (modify, gets, lift)
#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 710)
import Data.Monoid (Monoid(..))
#endif
#if MIN_VERSION_base(4, 7, 0)
import Data.Functor (($>))
#endif
import Network.URI (URI(..))
import qualified Control.Exception as CE
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.Text.Lazy as L
import qualified Data.Text.Lazy.Builder as B
import qualified Data.Text.Lazy.IO as LIO
import qualified System.IO.Error as IO
#if !MIN_VERSION_base(4, 7, 0)
($>) :: Functor f => f a -> b -> f b
($>) = flip (<$)
#endif
parseScriptFromText ::
Maybe QName
-> L.Text
-> Either String [SwishStateIO ()]
parseScriptFromText :: Maybe QName -> Text -> Either String [SwishStateIO ()]
parseScriptFromText = N3Parser [SwishStateIO ()]
-> Maybe QName -> Text -> Either String [SwishStateIO ()]
forall a. N3Parser a -> Maybe QName -> Text -> Either String a
parseAnyfromText N3Parser [SwishStateIO ()]
script
between :: Parser s lbr -> Parser s rbr -> Parser s a -> Parser s a
between :: Parser s lbr -> Parser s rbr -> Parser s a -> Parser s a
between = Parser s lbr -> Parser s rbr -> Parser s a -> Parser s a
forall (p :: * -> *) bra ket a.
PolyParse p =>
p bra -> p ket -> p a -> p a
bracket
n3SymLex :: N3Parser ScopedName
n3SymLex :: N3Parser ScopedName
n3SymLex = N3Parser ScopedName -> N3Parser ScopedName
forall s a. Parser s a -> Parser s a
lexeme N3Parser ScopedName
n3symbol
setTo :: N3Parser ()
setTo :: N3Parser ()
setTo = String -> N3Parser ()
isymbol ":-"
semicolon :: N3Parser ()
semicolon :: N3Parser ()
semicolon = String -> N3Parser ()
isymbol ";"
comma :: N3Parser ()
comma :: N3Parser ()
comma = String -> N3Parser ()
isymbol ","
commentText :: N3Parser String
= N3Parser ()
semicolon N3Parser () -> N3Parser String -> N3Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> N3Parser String
restOfLine
script :: N3Parser [SwishStateIO ()]
script :: N3Parser [SwishStateIO ()]
script = do
N3Parser ()
forall s. Parser s ()
whiteSpace
[SwishStateIO ()]
scs <- Parser N3State (SwishStateIO ()) -> N3Parser [SwishStateIO ()]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser N3State (SwishStateIO ())
command
N3Parser ()
forall s. Parser s ()
eof
[SwishStateIO ()] -> N3Parser [SwishStateIO ()]
forall (m :: * -> *) a. Monad m => a -> m a
return [SwishStateIO ()]
scs
isymbol :: String -> N3Parser ()
isymbol :: String -> N3Parser ()
isymbol = N3Parser String -> N3Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (N3Parser String -> N3Parser ())
-> (String -> N3Parser String) -> String -> N3Parser ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> N3Parser String
forall s. String -> Parser s String
symbol
command :: N3Parser (SwishStateIO ())
command :: Parser N3State (SwishStateIO ())
command =
Parser N3State (SwishStateIO ())
prefixLine
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
nameItem
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
readGraph
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
writeGraph
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
mergeGraphs
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
compareGraphs
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
assertEquiv
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
assertMember
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
defineRule
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
defineRuleset
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
defineConstraints
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
checkProofCmd
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
fwdChain
Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State (SwishStateIO ())
bwdChain
prefixLine :: N3Parser (SwishStateIO ())
prefixLine :: Parser N3State (SwishStateIO ())
prefixLine = do
String -> N3Parser ()
isymbol "@prefix"
N3Parser ()
getPrefix
N3Parser ()
forall s. Parser s ()
whiteSpace
String -> N3Parser ()
isymbol "."
SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ () -> SwishStateIO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
nameItem :: N3Parser (SwishStateIO ())
nameItem :: Parser N3State (SwishStateIO ())
nameItem =
ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssAddGraph (ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser
N3State
([SwishStateIO (Either String RDFGraph)] -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser
N3State
([SwishStateIO (Either String RDFGraph)] -> SwishStateIO ())
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> N3Parser String
forall s. String -> Parser s String
symbol ":-" N3Parser String
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser N3State [SwishStateIO (Either String RDFGraph)]
graphOrList)
maybeURI :: N3Parser (Maybe URI)
maybeURI :: N3Parser (Maybe URI)
maybeURI = (URI -> Maybe URI
forall a. a -> Maybe a
Just (URI -> Maybe URI) -> Parser N3State URI -> N3Parser (Maybe URI)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser N3State URI
lexUriRef) N3Parser (Maybe URI)
-> N3Parser (Maybe URI) -> N3Parser (Maybe URI)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe URI -> N3Parser (Maybe URI)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe URI
forall a. Maybe a
Nothing
readGraph :: N3Parser (SwishStateIO ())
readGraph :: Parser N3State (SwishStateIO ())
readGraph = String -> N3Parser ()
commandName "@read" N3Parser ()
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (ScopedName -> Maybe URI -> SwishStateIO ()
ssRead (ScopedName -> Maybe URI -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser N3State (Maybe URI -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser N3State (Maybe URI -> SwishStateIO ())
-> N3Parser (Maybe URI) -> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> N3Parser (Maybe URI)
maybeURI)
writeGraph :: N3Parser (SwishStateIO ())
writeGraph :: Parser N3State (SwishStateIO ())
writeGraph =
do { String -> N3Parser ()
commandName "@write"
; ScopedName
n <- N3Parser ScopedName
n3SymLex
; let gs :: SwishStateIO (Either String [RDFGraph])
gs = ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList ScopedName
n :: SwishStateIO (Either String [RDFGraph])
; Maybe URI
muri <- N3Parser (Maybe URI)
maybeURI
; String
c <- N3Parser String
commentText
; SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ Maybe URI
-> SwishStateIO (Either String [RDFGraph])
-> String
-> SwishStateIO ()
ssWriteList Maybe URI
muri SwishStateIO (Either String [RDFGraph])
gs String
c
}
mergeGraphs :: N3Parser (SwishStateIO ())
mergeGraphs :: Parser N3State (SwishStateIO ())
mergeGraphs = do
String -> N3Parser ()
commandName "@merge"
[SwishStateIO (Either String RDFGraph)]
gs <- Parser N3State [SwishStateIO (Either String RDFGraph)]
graphList
String -> N3Parser ()
isymbol "=>"
ScopedName
n <- N3Parser ScopedName
n3SymLex
SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssMerge ScopedName
n [SwishStateIO (Either String RDFGraph)]
gs
compareGraphs :: N3Parser (SwishStateIO ())
compareGraphs :: Parser N3State (SwishStateIO ())
compareGraphs =
String -> N3Parser ()
commandName "@compare" N3Parser ()
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (ScopedName -> ScopedName -> SwishStateIO ()
ssCompare (ScopedName -> ScopedName -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser N3State (ScopedName -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser N3State (ScopedName -> SwishStateIO ())
-> N3Parser ScopedName -> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> N3Parser ScopedName
n3SymLex)
assertArgs :: (ScopedName -> ScopedName -> String -> SwishStateIO ())
-> String -> N3Parser (SwishStateIO ())
assertArgs :: (ScopedName -> ScopedName -> String -> SwishStateIO ())
-> String -> Parser N3State (SwishStateIO ())
assertArgs assertFunc :: ScopedName -> ScopedName -> String -> SwishStateIO ()
assertFunc cName :: String
cName = do
String -> N3Parser ()
commandName (String -> N3Parser ()) -> String -> N3Parser ()
forall a b. (a -> b) -> a -> b
$ '@'Char -> String -> String
forall a. a -> [a] -> [a]
:String
cName
ScopedName -> ScopedName -> String -> SwishStateIO ()
assertFunc (ScopedName -> ScopedName -> String -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser N3State (ScopedName -> String -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser N3State (ScopedName -> String -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser N3State (String -> SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> N3Parser ScopedName
n3SymLex Parser N3State (String -> SwishStateIO ())
-> N3Parser String -> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> N3Parser String
commentText
assertEquiv :: N3Parser (SwishStateIO ())
assertEquiv :: Parser N3State (SwishStateIO ())
assertEquiv = (ScopedName -> ScopedName -> String -> SwishStateIO ())
-> String -> Parser N3State (SwishStateIO ())
assertArgs ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertEq "asserteq"
assertMember :: N3Parser (SwishStateIO ())
assertMember :: Parser N3State (SwishStateIO ())
assertMember = (ScopedName -> ScopedName -> String -> SwishStateIO ())
-> String -> Parser N3State (SwishStateIO ())
assertArgs ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertIn "assertin"
defineRule :: N3Parser (SwishStateIO ())
defineRule :: Parser N3State (SwishStateIO ())
defineRule =
do { String -> N3Parser ()
commandName "@rule"
; ScopedName
rn <- N3Parser ScopedName
n3SymLex
; N3Parser ()
setTo
; [SwishStateIO (Either String RDFGraph)]
ags <- Parser N3State [SwishStateIO (Either String RDFGraph)]
graphOrList
; String -> N3Parser ()
isymbol "=>"
; SwishStateIO (Either String RDFGraph)
cg <- N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr
; [(ScopedName, [RDFLabel])]
vms <- N3Parser [(ScopedName, [RDFLabel])]
varModifiers N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(ScopedName, [RDFLabel])] -> N3Parser [(ScopedName, [RDFLabel])]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
; SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> SwishStateIO (Either String RDFGraph)
-> [(ScopedName, [RDFLabel])]
-> SwishStateIO ()
ssDefineRule ScopedName
rn [SwishStateIO (Either String RDFGraph)]
ags SwishStateIO (Either String RDFGraph)
cg [(ScopedName, [RDFLabel])]
vms
}
defineRuleset :: N3Parser (SwishStateIO ())
defineRuleset :: Parser N3State (SwishStateIO ())
defineRuleset =
String -> N3Parser ()
commandName "@ruleset" N3Parser ()
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
(ScopedName -> [ScopedName] -> [ScopedName] -> SwishStateIO ()
ssDefineRuleset (ScopedName -> [ScopedName] -> [ScopedName] -> SwishStateIO ())
-> N3Parser ScopedName
-> Parser N3State ([ScopedName] -> [ScopedName] -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser N3State ([ScopedName] -> [ScopedName] -> SwishStateIO ())
-> Parser N3State [ScopedName]
-> Parser N3State ([ScopedName] -> SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (N3Parser ()
setTo N3Parser ()
-> Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser N3State [ScopedName]
nameList) Parser N3State ([ScopedName] -> SwishStateIO ())
-> Parser N3State [ScopedName] -> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (N3Parser ()
semicolon N3Parser ()
-> Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser N3State [ScopedName]
nameList))
defineConstraints :: N3Parser (SwishStateIO ())
defineConstraints :: Parser N3State (SwishStateIO ())
defineConstraints =
String -> N3Parser ()
commandName "@constraints" N3Parser ()
-> Parser N3State (SwishStateIO ())
-> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
(ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> [ScopedName]
-> SwishStateIO ()
ssDefineConstraints (ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> [ScopedName]
-> SwishStateIO ())
-> N3Parser ScopedName
-> Parser
N3State
([SwishStateIO (Either String RDFGraph)]
-> [ScopedName] -> SwishStateIO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser
N3State
([SwishStateIO (Either String RDFGraph)]
-> [ScopedName] -> SwishStateIO ())
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State ([ScopedName] -> SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (N3Parser ()
setTo N3Parser ()
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser N3State [SwishStateIO (Either String RDFGraph)]
graphOrList) Parser N3State ([ScopedName] -> SwishStateIO ())
-> Parser N3State [ScopedName] -> Parser N3State (SwishStateIO ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> N3Parser String
forall s. String -> Parser s String
symbol "|" N3Parser String
-> Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser N3State [ScopedName]
nameOrList))
checkProofCmd :: N3Parser (SwishStateIO ())
checkProofCmd :: Parser N3State (SwishStateIO ())
checkProofCmd =
do { String -> N3Parser ()
commandName "@proof"
; ScopedName
pn <- N3Parser ScopedName
n3SymLex
; [ScopedName]
sns <- Parser N3State [ScopedName]
nameList
; String -> N3Parser ()
commandName "@input"
; SwishStateIO (Either String RDFFormula)
igf <- N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr
; [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
sts <- Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
-> Parser
N3State
[Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
checkStep
; String -> N3Parser ()
commandName "@result"
; SwishStateIO (Either String RDFFormula)
rgf <- N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr
; SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ ScopedName
-> [ScopedName]
-> SwishStateIO (Either String RDFFormula)
-> [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO (Either String RDFFormula)
-> SwishStateIO ()
ssCheckProof ScopedName
pn [ScopedName]
sns SwishStateIO (Either String RDFFormula)
igf [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
sts SwishStateIO (Either String RDFFormula)
rgf
}
checkStep ::
N3Parser (Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
checkStep :: Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
checkStep =
String -> N3Parser ()
commandName "@step" N3Parser ()
-> Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
-> Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
(ScopedName
-> [SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)
ssCheckStep (ScopedName
-> [SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
-> N3Parser ScopedName
-> Parser
N3State
([SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser
N3State
([SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
-> Parser N3State [SwishStateIO (Either String RDFFormula)]
-> Parser
N3State
(SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser N3State [SwishStateIO (Either String RDFFormula)]
formulaList Parser
N3State
(SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
-> N3Parser (SwishStateIO (Either String RDFFormula))
-> Parser
N3State
(Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> N3Parser String
forall s. String -> Parser s String
symbol "=>" N3Parser String
-> N3Parser (SwishStateIO (Either String RDFFormula))
-> N3Parser (SwishStateIO (Either String RDFFormula))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr))
fwdChain :: N3Parser (SwishStateIO ())
fwdChain :: Parser N3State (SwishStateIO ())
fwdChain =
do { String -> N3Parser ()
commandName "@fwdchain"
; ScopedName
sn <- N3Parser ScopedName
n3SymLex
; ScopedName
rn <- N3Parser ScopedName
n3SymLex
; [SwishStateIO (Either String RDFGraph)]
ags <- Parser N3State [SwishStateIO (Either String RDFGraph)]
graphOrList
; String -> N3Parser ()
isymbol "=>"
; ScopedName
cn <- N3Parser ScopedName
n3SymLex
; N3State
s <- Parser N3State N3State
forall s. Parser s s
stGet
; let prefs :: NamespaceMap
prefs = N3State -> NamespaceMap
prefixUris N3State
s
; SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ ScopedName
-> ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssFwdChain ScopedName
sn ScopedName
rn [SwishStateIO (Either String RDFGraph)]
ags ScopedName
cn NamespaceMap
prefs
}
bwdChain :: N3Parser (SwishStateIO ())
bwdChain :: Parser N3State (SwishStateIO ())
bwdChain =
do { String -> N3Parser ()
commandName "@bwdchain"
; ScopedName
sn <- N3Parser ScopedName
n3SymLex
; ScopedName
rn <- N3Parser ScopedName
n3SymLex
; SwishStateIO (Either String RDFGraph)
cg <- N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr
; String -> N3Parser ()
isymbol "<="
; ScopedName
an <- N3Parser ScopedName
n3SymLex
; N3State
s <- Parser N3State N3State
forall s. Parser s s
stGet
; let prefs :: NamespaceMap
prefs = N3State -> NamespaceMap
prefixUris N3State
s
; SwishStateIO () -> Parser N3State (SwishStateIO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO () -> Parser N3State (SwishStateIO ()))
-> SwishStateIO () -> Parser N3State (SwishStateIO ())
forall a b. (a -> b) -> a -> b
$ ScopedName
-> ScopedName
-> SwishStateIO (Either String RDFGraph)
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssBwdChain ScopedName
sn ScopedName
rn SwishStateIO (Either String RDFGraph)
cg ScopedName
an NamespaceMap
prefs
}
commandName :: String -> N3Parser ()
commandName :: String -> N3Parser ()
commandName cmd :: String
cmd = String -> N3Parser String
forall s. String -> Parser s String
symbol String
cmd N3Parser String -> () -> N3Parser ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()
restOfLine :: N3Parser String
restOfLine :: N3Parser String
restOfLine = Parser N3State Char -> N3Parser () -> N3Parser String
forall s a b. Parser s a -> Parser s b -> Parser s [a]
manyTill ((Char -> Bool) -> Parser N3State Char
forall s. (Char -> Bool) -> Parser s Char
satisfy (Bool -> Char -> Bool
forall a b. a -> b -> a
const Bool
True)) N3Parser ()
forall s. Parser s ()
eoln N3Parser String -> N3Parser () -> N3Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* N3Parser ()
forall s. Parser s ()
whiteSpace
br :: N3Parser a -> N3Parser a
br :: N3Parser a -> N3Parser a
br = N3Parser String -> N3Parser String -> N3Parser a -> N3Parser a
forall s lbr rbr a.
Parser s lbr -> Parser s rbr -> Parser s a -> Parser s a
between (String -> N3Parser String
forall s. String -> Parser s String
symbol "(") (String -> N3Parser String
forall s. String -> Parser s String
symbol ")")
nameList :: N3Parser [ScopedName]
nameList :: Parser N3State [ScopedName]
nameList = Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall a. N3Parser a -> N3Parser a
br (Parser N3State [ScopedName] -> Parser N3State [ScopedName])
-> Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall a b. (a -> b) -> a -> b
$ N3Parser ScopedName -> Parser N3State [ScopedName]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many N3Parser ScopedName
n3SymLex
toList :: a -> [a]
toList :: a -> [a]
toList = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[])
nameOrList :: N3Parser [ScopedName]
nameOrList :: Parser N3State [ScopedName]
nameOrList =
(ScopedName -> [ScopedName]
forall a. a -> [a]
toList (ScopedName -> [ScopedName])
-> N3Parser ScopedName -> Parser N3State [ScopedName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex)
Parser N3State [ScopedName]
-> Parser N3State [ScopedName] -> Parser N3State [ScopedName]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State [ScopedName]
nameList
graphExpr :: N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr :: N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr =
N3Parser (SwishStateIO (Either String RDFGraph))
graphOnly
N3Parser (SwishStateIO (Either String RDFGraph))
-> N3Parser (SwishStateIO (Either String RDFGraph))
-> N3Parser (SwishStateIO (Either String RDFGraph))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(Either String RDFFormula -> Either String RDFGraph)
-> SwishStateIO (Either String RDFFormula)
-> SwishStateIO (Either String RDFGraph)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RDFFormula -> RDFGraph)
-> Either String RDFFormula -> Either String RDFGraph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RDFFormula -> RDFGraph
forall ex. Formula ex -> ex
formExpr) (SwishStateIO (Either String RDFFormula)
-> SwishStateIO (Either String RDFGraph))
-> N3Parser (SwishStateIO (Either String RDFFormula))
-> N3Parser (SwishStateIO (Either String RDFGraph))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr
graphOnly :: N3Parser (SwishStateIO (Either String RDFGraph))
graphOnly :: N3Parser (SwishStateIO (Either String RDFGraph))
graphOnly =
do { String -> N3Parser ()
isymbol "{"
; RDFLabel
b <- N3Parser RDFLabel
newBlankNode
; RDFGraph
g <- RDFLabel -> N3Parser RDFGraph
subgraph RDFLabel
b
; String -> N3Parser ()
isymbol "}"
; N3State
s <- Parser N3State N3State
forall s. Parser s s
stGet
; let gp :: RDFGraph
gp = NamespaceMap -> RDFGraph -> RDFGraph
forall lb. NamespaceMap -> NSGraph lb -> NSGraph lb
setNamespaces (N3State -> NamespaceMap
prefixUris N3State
s) RDFGraph
g
; SwishStateIO (Either String RDFGraph)
-> N3Parser (SwishStateIO (Either String RDFGraph))
forall (m :: * -> *) a. Monad m => a -> m a
return (SwishStateIO (Either String RDFGraph)
-> N3Parser (SwishStateIO (Either String RDFGraph)))
-> SwishStateIO (Either String RDFGraph)
-> N3Parser (SwishStateIO (Either String RDFGraph))
forall a b. (a -> b) -> a -> b
$ Either String RDFGraph -> SwishStateIO (Either String RDFGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (RDFGraph -> Either String RDFGraph
forall a b. b -> Either a b
Right RDFGraph
gp)
}
graphList :: N3Parser [SwishStateIO (Either String RDFGraph)]
graphList :: Parser N3State [SwishStateIO (Either String RDFGraph)]
graphList = Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall a. N3Parser a -> N3Parser a
br (N3Parser (SwishStateIO (Either String RDFGraph))
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr)
graphOrList :: N3Parser [SwishStateIO (Either String RDFGraph)]
graphOrList :: Parser N3State [SwishStateIO (Either String RDFGraph)]
graphOrList =
(SwishStateIO (Either String RDFGraph)
-> [SwishStateIO (Either String RDFGraph)]
forall a. a -> [a]
toList (SwishStateIO (Either String RDFGraph)
-> [SwishStateIO (Either String RDFGraph)])
-> N3Parser (SwishStateIO (Either String RDFGraph))
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser (SwishStateIO (Either String RDFGraph))
graphExpr)
Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
-> Parser N3State [SwishStateIO (Either String RDFGraph)]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser N3State [SwishStateIO (Either String RDFGraph)]
graphList
formulaExpr :: N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr :: N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr = N3Parser ScopedName
n3SymLex N3Parser ScopedName
-> (ScopedName
-> N3Parser (SwishStateIO (Either String RDFFormula)))
-> N3Parser (SwishStateIO (Either String RDFFormula))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ScopedName -> N3Parser (SwishStateIO (Either String RDFFormula))
namedGraph
namedGraph :: ScopedName -> N3Parser (SwishStateIO (Either String RDFFormula))
namedGraph :: ScopedName -> N3Parser (SwishStateIO (Either String RDFFormula))
namedGraph n :: ScopedName
n =
(ScopedName
-> SwishStateIO (Either String RDFGraph)
-> SwishStateIO (Either String RDFFormula)
ssAddReturnFormula ScopedName
n (SwishStateIO (Either String RDFGraph)
-> SwishStateIO (Either String RDFFormula))
-> N3Parser (SwishStateIO (Either String RDFGraph))
-> N3Parser (SwishStateIO (Either String RDFFormula))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (N3Parser ()
setTo N3Parser ()
-> N3Parser (SwishStateIO (Either String RDFGraph))
-> N3Parser (SwishStateIO (Either String RDFGraph))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> N3Parser (SwishStateIO (Either String RDFGraph))
graphOnly))
N3Parser (SwishStateIO (Either String RDFFormula))
-> N3Parser (SwishStateIO (Either String RDFFormula))
-> N3Parser (SwishStateIO (Either String RDFFormula))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SwishStateIO (Either String RDFFormula)
-> N3Parser (SwishStateIO (Either String RDFFormula))
forall (m :: * -> *) a. Monad m => a -> m a
return (ScopedName -> SwishStateIO (Either String RDFFormula)
ssGetFormula ScopedName
n)
formulaList :: N3Parser [SwishStateIO (Either String RDFFormula)]
formulaList :: Parser N3State [SwishStateIO (Either String RDFFormula)]
formulaList = N3Parser String
-> N3Parser String
-> Parser N3State [SwishStateIO (Either String RDFFormula)]
-> Parser N3State [SwishStateIO (Either String RDFFormula)]
forall s lbr rbr a.
Parser s lbr -> Parser s rbr -> Parser s a -> Parser s a
between (String -> N3Parser String
forall s. String -> Parser s String
symbol "(") (String -> N3Parser String
forall s. String -> Parser s String
symbol ")") (N3Parser (SwishStateIO (Either String RDFFormula))
-> Parser N3State [SwishStateIO (Either String RDFFormula)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many N3Parser (SwishStateIO (Either String RDFFormula))
formulaExpr)
varModifiers :: N3Parser [(ScopedName,[RDFLabel])]
varModifiers :: N3Parser [(ScopedName, [RDFLabel])]
varModifiers = String -> N3Parser String
forall s. String -> Parser s String
symbol "|" N3Parser String
-> N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> N3Parser [(ScopedName, [RDFLabel])]
varModList
varModList :: N3Parser [(ScopedName,[RDFLabel])]
varModList :: N3Parser [(ScopedName, [RDFLabel])]
varModList =
N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
forall a. N3Parser a -> N3Parser a
br (Parser N3State (ScopedName, [RDFLabel])
-> N3Parser () -> N3Parser [(ScopedName, [RDFLabel])]
forall (p :: * -> *) a sep. PolyParse p => p a -> p sep -> p [a]
sepBy Parser N3State (ScopedName, [RDFLabel])
varMod N3Parser ()
comma)
N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
-> N3Parser [(ScopedName, [RDFLabel])]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ScopedName, [RDFLabel]) -> [(ScopedName, [RDFLabel])]
forall a. a -> [a]
toList ((ScopedName, [RDFLabel]) -> [(ScopedName, [RDFLabel])])
-> Parser N3State (ScopedName, [RDFLabel])
-> N3Parser [(ScopedName, [RDFLabel])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser N3State (ScopedName, [RDFLabel])
-> Parser N3State (ScopedName, [RDFLabel])
forall s a. Parser s a -> Parser s a
lexeme Parser N3State (ScopedName, [RDFLabel])
varMod
varMod :: N3Parser (ScopedName,[RDFLabel])
varMod :: Parser N3State (ScopedName, [RDFLabel])
varMod = (,) (ScopedName -> [RDFLabel] -> (ScopedName, [RDFLabel]))
-> N3Parser ScopedName
-> Parser N3State ([RDFLabel] -> (ScopedName, [RDFLabel]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> N3Parser ScopedName
n3SymLex Parser N3State ([RDFLabel] -> (ScopedName, [RDFLabel]))
-> Parser N3State [RDFLabel]
-> Parser N3State (ScopedName, [RDFLabel])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> N3Parser RDFLabel -> Parser N3State [RDFLabel]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (N3Parser RDFLabel -> N3Parser RDFLabel
forall s a. Parser s a -> Parser s a
lexeme N3Parser RDFLabel
quickVariable)
ssReport ::
String
-> SwishStateIO ()
ssReport :: String -> SwishStateIO ()
ssReport msg :: String
msg = (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setInfo (String -> SwishState -> SwishState)
-> String -> SwishState -> SwishState
forall a b. (a -> b) -> a -> b
$ "# " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
ssReportLabel ::
String
-> String
-> SwishStateIO ()
ssReportLabel :: String -> String -> SwishStateIO ()
ssReportLabel lbl :: String
lbl msg :: String
msg = String -> SwishStateIO ()
ssReport (String -> SwishStateIO ()) -> String -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String
lbl String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
ssAddReturnFormula ::
ScopedName -> SwishStateIO (Either String RDFGraph)
-> SwishStateIO (Either String RDFFormula)
ssAddReturnFormula :: ScopedName
-> SwishStateIO (Either String RDFGraph)
-> SwishStateIO (Either String RDFFormula)
ssAddReturnFormula nam :: ScopedName
nam gf :: SwishStateIO (Either String RDFGraph)
gf =
do { Either String RDFGraph
egr <- SwishStateIO (Either String RDFGraph)
gf
; ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssAddGraph ScopedName
nam [Either String RDFGraph -> SwishStateIO (Either String RDFGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return Either String RDFGraph
egr]
; Either String RDFFormula -> SwishStateIO (Either String RDFFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String RDFFormula
-> SwishStateIO (Either String RDFFormula))
-> Either String RDFFormula
-> SwishStateIO (Either String RDFFormula)
forall a b. (a -> b) -> a -> b
$ (RDFGraph -> RDFFormula)
-> Either String RDFGraph -> Either String RDFFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopedName -> RDFGraph -> RDFFormula
forall ex. ScopedName -> ex -> Formula ex
Formula ScopedName
nam) Either String RDFGraph
egr
}
ssAddGraph ::
ScopedName -> [SwishStateIO (Either String RDFGraph)]
-> SwishStateIO ()
ssAddGraph :: ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssAddGraph nam :: ScopedName
nam gf :: [SwishStateIO (Either String RDFGraph)]
gf =
let errmsg :: String
errmsg = "Graph/list not added: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
namString -> String -> String
forall a. [a] -> [a] -> [a]
++"; "
in
do { [Either String RDFGraph]
esg <- [SwishStateIO (Either String RDFGraph)]
-> StateT SwishState IO [Either String RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFGraph)]
gf
; let egs :: Either String [RDFGraph]
egs = [Either String RDFGraph] -> Either String [RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFGraph]
esg
; let fgs :: SwishState -> SwishState
fgs = case Either String [RDFGraph]
egs of
Left er :: String
er -> String -> SwishState -> SwishState
setError (String
errmsgString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
Right gs :: [RDFGraph]
gs -> (NamedGraphMap -> NamedGraphMap) -> SwishState -> SwishState
modGraphs (ScopedName -> [RDFGraph] -> NamedGraphMap -> NamedGraphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ScopedName
nam [RDFGraph]
gs)
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
fgs
}
ssGetGraph :: ScopedName -> SwishStateIO (Either String RDFGraph)
ssGetGraph :: ScopedName -> SwishStateIO (Either String RDFGraph)
ssGetGraph nam :: ScopedName
nam = ([RDFGraph] -> RDFGraph)
-> Either String [RDFGraph] -> Either String RDFGraph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [RDFGraph] -> RDFGraph
forall a. [a] -> a
head (Either String [RDFGraph] -> Either String RDFGraph)
-> SwishStateIO (Either String [RDFGraph])
-> SwishStateIO (Either String RDFGraph)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList ScopedName
nam
ssGetFormula :: ScopedName -> SwishStateIO (Either String RDFFormula)
ssGetFormula :: ScopedName -> SwishStateIO (Either String RDFFormula)
ssGetFormula nam :: ScopedName
nam = (SwishState -> Either String RDFFormula)
-> SwishStateIO (Either String RDFFormula)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String RDFFormula
find
where
find :: SwishState -> Either String RDFFormula
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe RDFFormula
findFormula ScopedName
nam SwishState
st of
Nothing -> String -> Either String RDFFormula
forall a b. a -> Either a b
Left ("Formula not present: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
Just gr :: RDFFormula
gr -> RDFFormula -> Either String RDFFormula
forall a b. b -> Either a b
Right RDFFormula
gr
ssGetList :: ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList :: ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList nam :: ScopedName
nam = (SwishState -> Either String [RDFGraph])
-> SwishStateIO (Either String [RDFGraph])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String [RDFGraph]
find
where
find :: SwishState -> Either String [RDFGraph]
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe [RDFGraph]
findGraph ScopedName
nam SwishState
st of
Nothing -> String -> Either String [RDFGraph]
forall a b. a -> Either a b
Left ("Graph or list not present: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
Just grs :: [RDFGraph]
grs -> [RDFGraph] -> Either String [RDFGraph]
forall a b. b -> Either a b
Right [RDFGraph]
grs
ssRead :: ScopedName -> Maybe URI -> SwishStateIO ()
ssRead :: ScopedName -> Maybe URI -> SwishStateIO ()
ssRead nam :: ScopedName
nam muri :: Maybe URI
muri = ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssAddGraph ScopedName
nam [Maybe URI -> SwishStateIO (Either String RDFGraph)
ssReadGraph Maybe URI
muri]
ssReadGraph :: Maybe URI -> SwishStateIO (Either String RDFGraph)
ssReadGraph :: Maybe URI -> SwishStateIO (Either String RDFGraph)
ssReadGraph muri :: Maybe URI
muri =
let gf :: Either String Text -> Either String RDFGraph
gf inp :: Either String Text
inp = case Either String Text
inp of
Left es :: String
es -> String -> Either String RDFGraph
forall a b. a -> Either a b
Left String
es
Right is :: Text
is -> Text -> Maybe QName -> Either String RDFGraph
parseN3 Text
is (Maybe URI
muri Maybe URI -> (URI -> Maybe QName) -> Maybe QName
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= URI -> Maybe QName
qnameFromURI)
in Either String Text -> Either String RDFGraph
gf (Either String Text -> Either String RDFGraph)
-> StateT SwishState IO (Either String Text)
-> SwishStateIO (Either String RDFGraph)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Maybe URI -> StateT SwishState IO (Either String Text)
getResourceData Maybe URI
muri
ssWriteList ::
Maybe URI -> SwishStateIO (Either String [RDFGraph]) -> String
-> SwishStateIO ()
ssWriteList :: Maybe URI
-> SwishStateIO (Either String [RDFGraph])
-> String
-> SwishStateIO ()
ssWriteList muri :: Maybe URI
muri gf :: SwishStateIO (Either String [RDFGraph])
gf comment :: String
comment = do
Either String [RDFGraph]
esgs <- SwishStateIO (Either String [RDFGraph])
gf
case Either String [RDFGraph]
esgs of
Left er :: String
er -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError ("Cannot write list: "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
Right [] -> Maybe URI -> Builder -> SwishStateIO ()
putResourceData Maybe URI
forall a. Maybe a
Nothing (Text -> Builder
B.fromLazyText ([Text] -> Text
L.concat ["# ", String -> Text
L.pack String
comment, "\n+ Swish: Writing empty list"]))
Right [gr :: RDFGraph
gr] -> Maybe URI -> RDFGraph -> String -> SwishStateIO ()
ssWriteGraph Maybe URI
muri RDFGraph
gr String
comment
Right grs :: [RDFGraph]
grs -> ((Int, RDFGraph) -> SwishStateIO ())
-> [(Int, RDFGraph)] -> SwishStateIO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int, RDFGraph) -> SwishStateIO ()
forall a. Show a => (a, RDFGraph) -> SwishStateIO ()
writegr ([Int] -> [RDFGraph] -> [(Int, RDFGraph)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(0::Int)..] [RDFGraph]
grs)
where
writegr :: (a, RDFGraph) -> SwishStateIO ()
writegr (n :: a
n,gr :: RDFGraph
gr) = Maybe URI -> RDFGraph -> String -> SwishStateIO ()
ssWriteGraph (Maybe URI -> a -> Maybe URI
forall a. Show a => Maybe URI -> a -> Maybe URI
murin Maybe URI
muri a
n) RDFGraph
gr
("["String -> String -> String
forall a. [a] -> [a] -> [a]
++a -> String
forall a. Show a => a -> String
show a
nString -> String -> String
forall a. [a] -> [a] -> [a]
++"] "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
comment)
murin :: Maybe URI -> a -> Maybe URI
murin Nothing _ = Maybe URI
forall a. Maybe a
Nothing
murin (Just uri :: URI
uri) n :: a
n =
let rp :: String
rp = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ URI -> String
uriPath URI
uri
(rLastSet :: String
rLastSet, rRest :: String
rRest) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='/') String
rp
(before :: String
before, after :: String
after) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='.') (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
rLastSet
newPath :: String
newPath = String -> String
forall a. [a] -> [a]
reverse String
rRest String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
before String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
after
in case String
rLastSet of
"" -> String -> Maybe URI
forall a. HasCallStack => String -> a
error (String -> Maybe URI) -> String -> Maybe URI
forall a b. (a -> b) -> a -> b
$ "Invalid URI (path ends in /): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ URI -> String
forall a. Show a => a -> String
show URI
uri
_ -> URI -> Maybe URI
forall a. a -> Maybe a
Just (URI -> Maybe URI) -> URI -> Maybe URI
forall a b. (a -> b) -> a -> b
$ URI
uri { uriPath :: String
uriPath = String
newPath }
ssWriteGraph :: Maybe URI -> RDFGraph -> String -> SwishStateIO ()
ssWriteGraph :: Maybe URI -> RDFGraph -> String -> SwishStateIO ()
ssWriteGraph muri :: Maybe URI
muri gr :: RDFGraph
gr comment :: String
comment =
Maybe URI -> Builder -> SwishStateIO ()
putResourceData Maybe URI
muri (Builder
c Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend` RDFGraph -> Builder
formatGraphAsBuilder RDFGraph
gr)
where
c :: Builder
c = Text -> Builder
B.fromLazyText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
L.concat ["# ", String -> Text
L.pack String
comment, "\n"]
ssMerge ::
ScopedName -> [SwishStateIO (Either String RDFGraph)]
-> SwishStateIO ()
ssMerge :: ScopedName
-> [SwishStateIO (Either String RDFGraph)] -> SwishStateIO ()
ssMerge nam :: ScopedName
nam gfs :: [SwishStateIO (Either String RDFGraph)]
gfs =
let errmsg :: String
errmsg = "Graph merge not defined: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
namString -> String -> String
forall a. [a] -> [a] -> [a]
++"; "
in
do { String -> String -> SwishStateIO ()
ssReportLabel "Merge" (ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
; [Either String RDFGraph]
esg <- [SwishStateIO (Either String RDFGraph)]
-> StateT SwishState IO [Either String RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFGraph)]
gfs
; let egs :: Either String [RDFGraph]
egs = [Either String RDFGraph] -> Either String [RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFGraph]
esg
; let fgs :: SwishState -> SwishState
fgs = case Either String [RDFGraph]
egs of
Left er :: String
er -> String -> SwishState -> SwishState
setError (String
errmsgString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
Right [] -> String -> SwishState -> SwishState
setError (String
errmsgString -> String -> String
forall a. [a] -> [a] -> [a]
++"No graphs to merge")
Right gs :: [RDFGraph]
gs -> (NamedGraphMap -> NamedGraphMap) -> SwishState -> SwishState
modGraphs (ScopedName -> [RDFGraph] -> NamedGraphMap -> NamedGraphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ScopedName
nam [RDFGraph
g])
where g :: RDFGraph
g = (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
gs
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
fgs
}
ssCompare :: ScopedName -> ScopedName -> SwishStateIO ()
ssCompare :: ScopedName -> ScopedName -> SwishStateIO ()
ssCompare n1 :: ScopedName
n1 n2 :: ScopedName
n2 =
do { String -> String -> SwishStateIO ()
ssReportLabel "Compare" (ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n2)
; Either String RDFGraph
g1 <- ScopedName -> SwishStateIO (Either String RDFGraph)
ssGetGraph ScopedName
n1
; Either String RDFGraph
g2 <- ScopedName -> SwishStateIO (Either String RDFGraph)
ssGetGraph ScopedName
n2
; Bool -> SwishStateIO () -> SwishStateIO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Either String RDFGraph
g1 Either String RDFGraph -> Either String RDFGraph -> Bool
forall a. Eq a => a -> a -> Bool
/= Either String RDFGraph
g2) ((SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ SwishStatus -> SwishState -> SwishState
setStatus SwishStatus
SwishGraphCompareError)
}
ssAssertEq :: ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertEq :: ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertEq n1 :: ScopedName
n1 n2 :: ScopedName
n2 comment :: String
comment =
let er1 :: String
er1 = ":\n Graph or list compare not performed: invalid graph/list."
in
do { String -> String -> SwishStateIO ()
ssReportLabel "AssertEq" String
comment
; Either String [RDFGraph]
g1 <- ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList ScopedName
n1
; Either String [RDFGraph]
g2 <- ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList ScopedName
n2
; case (Either String [RDFGraph]
g1,Either String [RDFGraph]
g2) of
(Left er :: String
er,_) -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er1String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er1String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right gr1 :: [RDFGraph]
gr1,Right gr2 :: [RDFGraph]
gr2) ->
Bool -> SwishStateIO () -> SwishStateIO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([RDFGraph] -> Set RDFGraph
forall a. Ord a => [a] -> Set a
S.fromList [RDFGraph]
gr1 Set RDFGraph -> Set RDFGraph -> Bool
forall a. Eq a => a -> a -> Bool
/= [RDFGraph] -> Set RDFGraph
forall a. Ord a => [a] -> Set a
S.fromList [RDFGraph]
gr2) (SwishStateIO () -> SwishStateIO ())
-> SwishStateIO () -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$
String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++":\n Graph "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n1
String -> String -> String
forall a. [a] -> [a] -> [a]
++" differs from "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n2String -> String -> String
forall a. [a] -> [a] -> [a]
++".")
}
ssAssertIn :: ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertIn :: ScopedName -> ScopedName -> String -> SwishStateIO ()
ssAssertIn n1 :: ScopedName
n1 n2 :: ScopedName
n2 comment :: String
comment =
let er1 :: String
er1 = ":\n Membership test not performed: invalid graph."
er2 :: String
er2 = ":\n Membership test not performed: invalid list."
in
do { String -> String -> SwishStateIO ()
ssReportLabel "AssertIn" String
comment
; Either String RDFGraph
g1 <- ScopedName -> SwishStateIO (Either String RDFGraph)
ssGetGraph ScopedName
n1
; Either String [RDFGraph]
g2 <- ScopedName -> SwishStateIO (Either String [RDFGraph])
ssGetList ScopedName
n2
; case (Either String RDFGraph
g1,Either String [RDFGraph]
g2) of
(Left er :: String
er,_) -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er1String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++String
er2String -> String -> String
forall a. [a] -> [a] -> [a]
++"\n "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right gr :: RDFGraph
gr,Right gs :: [RDFGraph]
gs) ->
Bool -> SwishStateIO () -> SwishStateIO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RDFGraph
gr RDFGraph -> [RDFGraph] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RDFGraph]
gs) (SwishStateIO () -> SwishStateIO ())
-> SwishStateIO () -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$
String -> SwishState -> SwishState
setError (String
commentString -> String -> String
forall a. [a] -> [a] -> [a]
++":\n Graph "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n1
String -> String -> String
forall a. [a] -> [a] -> [a]
++" not a member of "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
n2)
}
ssDefineRule ::
ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> SwishStateIO (Either String RDFGraph)
-> [(ScopedName,[RDFLabel])]
-> SwishStateIO ()
ssDefineRule :: ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> SwishStateIO (Either String RDFGraph)
-> [(ScopedName, [RDFLabel])]
-> SwishStateIO ()
ssDefineRule rn :: ScopedName
rn agfs :: [SwishStateIO (Either String RDFGraph)]
agfs cgf :: SwishStateIO (Either String RDFGraph)
cgf vmds :: [(ScopedName, [RDFLabel])]
vmds =
let errmsg1 :: String
errmsg1 = "Rule definition error in antecedent graph(s): "
errmsg2 :: String
errmsg2 = "Rule definition error in consequent graph: "
errmsg3 :: String
errmsg3 = "Rule definition error in variable modifier(s): "
errmsg4 :: String
errmsg4 = "Incompatible variable binding modifier sequence"
in
do { [Either String RDFGraph]
aesg <- [SwishStateIO (Either String RDFGraph)]
-> StateT SwishState IO [Either String RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFGraph)]
agfs
; let ags :: Either String [RDFGraph]
ags = [Either String RDFGraph] -> Either String [RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFGraph]
aesg :: Either String [RDFGraph]
; Either String RDFGraph
cg <- SwishStateIO (Either String RDFGraph)
cgf
; let vmfs :: [SwishStateIO (Either String RDFVarBindingModify)]
vmfs = ((ScopedName, [RDFLabel])
-> SwishStateIO (Either String RDFVarBindingModify))
-> [(ScopedName, [RDFLabel])]
-> [SwishStateIO (Either String RDFVarBindingModify)]
forall a b. (a -> b) -> [a] -> [b]
map (ScopedName, [RDFLabel])
-> SwishStateIO (Either String RDFVarBindingModify)
ssFindVarModify [(ScopedName, [RDFLabel])]
vmds
; [Either String RDFVarBindingModify]
evms <- [SwishStateIO (Either String RDFVarBindingModify)]
-> StateT SwishState IO [Either String RDFVarBindingModify]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFVarBindingModify)]
vmfs
; let vms :: Either String [RDFVarBindingModify]
vms = [Either String RDFVarBindingModify]
-> Either String [RDFVarBindingModify]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFVarBindingModify]
evms :: Either String [RDFVarBindingModify]
; let frl :: SwishState -> SwishState
frl = case (Either String [RDFGraph]
ags,Either String RDFGraph
cg,Either String [RDFVarBindingModify]
vms) of
(Left er :: String
er,_,_) -> String -> SwishState -> SwishState
setError (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er,_) -> String -> SwishState -> SwishState
setError (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,_,Left er :: String
er) -> String -> SwishState -> SwishState
setError (String
errmsg3String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right agrs :: [RDFGraph]
agrs,Right cgr :: RDFGraph
cgr,Right vbms :: [RDFVarBindingModify]
vbms) ->
let
newRule :: RDFVarBindingModify -> RDFRule
newRule = ScopedName
-> [RDFGraph] -> RDFGraph -> RDFVarBindingModify -> RDFRule
makeRDFClosureRule ScopedName
rn [RDFGraph]
agrs RDFGraph
cgr
in
case [RDFVarBindingModify] -> Maybe RDFVarBindingModify
forall a b.
Eq a =>
[VarBindingModify a b] -> Maybe (VarBindingModify a b)
composeSequence [RDFVarBindingModify]
vbms of
Just vm :: RDFVarBindingModify
vm -> let nr :: RDFRule
nr = RDFVarBindingModify -> RDFRule
newRule RDFVarBindingModify
vm in (RDFRuleMap -> RDFRuleMap) -> SwishState -> SwishState
modRules (ScopedName -> RDFRule -> RDFRuleMap -> RDFRuleMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (RDFRule -> ScopedName
forall ex. Rule ex -> ScopedName
ruleName RDFRule
nr) RDFRule
nr)
Nothing -> String -> SwishState -> SwishState
setError String
errmsg4
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
frl
}
ssFindVarModify ::
(ScopedName,[RDFLabel]) -> SwishStateIO (Either String RDFVarBindingModify)
ssFindVarModify :: (ScopedName, [RDFLabel])
-> SwishStateIO (Either String RDFVarBindingModify)
ssFindVarModify (nam :: ScopedName
nam,lbs :: [RDFLabel]
lbs) = (SwishState -> Either String RDFVarBindingModify)
-> SwishStateIO (Either String RDFVarBindingModify)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((SwishState -> Either String RDFVarBindingModify)
-> SwishStateIO (Either String RDFVarBindingModify))
-> (SwishState -> Either String RDFVarBindingModify)
-> SwishStateIO (Either String RDFVarBindingModify)
forall a b. (a -> b) -> a -> b
$ \st :: SwishState
st ->
case ScopedName -> SwishState -> Maybe RDFOpenVarBindingModify
findOpenVarModify ScopedName
nam SwishState
st of
Just ovbm :: RDFOpenVarBindingModify
ovbm -> RDFVarBindingModify -> Either String RDFVarBindingModify
forall a b. b -> Either a b
Right (RDFOpenVarBindingModify
ovbm [RDFLabel]
lbs)
Nothing -> String -> Either String RDFVarBindingModify
forall a b. a -> Either a b
Left ("Undefined modifier: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
ssDefineRuleset ::
ScopedName
-> [ScopedName]
-> [ScopedName]
-> SwishStateIO ()
ssDefineRuleset :: ScopedName -> [ScopedName] -> [ScopedName] -> SwishStateIO ()
ssDefineRuleset sn :: ScopedName
sn ans :: [ScopedName]
ans rns :: [ScopedName]
rns =
let errmsg1 :: String
errmsg1 = "Error in ruleset axiom(s): "
errmsg2 :: String
errmsg2 = "Error in ruleset rule(s): "
in
do { let agfs :: SwishStateIO [Either String RDFFormula]
agfs = (ScopedName -> SwishStateIO (Either String RDFFormula))
-> [ScopedName] -> SwishStateIO [Either String RDFFormula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ScopedName -> SwishStateIO (Either String RDFFormula)
ssGetFormula [ScopedName]
ans
:: SwishStateIO [Either String RDFFormula]
; [Either String RDFFormula]
aesg <- SwishStateIO [Either String RDFFormula]
agfs
; let eags :: Either String [RDFFormula]
eags = [Either String RDFFormula] -> Either String [RDFFormula]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFFormula]
aesg :: Either String [RDFFormula]
; let erlf :: SwishStateIO [Either String RDFRule]
erlf = (ScopedName -> StateT SwishState IO (Either String RDFRule))
-> [ScopedName] -> SwishStateIO [Either String RDFRule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ScopedName -> StateT SwishState IO (Either String RDFRule)
ssFindRule [ScopedName]
rns
:: SwishStateIO [Either String RDFRule]
; [Either String RDFRule]
rles <- SwishStateIO [Either String RDFRule]
erlf
; let erls :: Either String [RDFRule]
erls = [Either String RDFRule] -> Either String [RDFRule]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFRule]
rles :: Either String [RDFRule]
; let frs :: SwishState -> SwishState
frs = case (Either String [RDFFormula]
eags,Either String [RDFRule]
erls) of
(Left er :: String
er,_) -> String -> SwishState -> SwishState
setError (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> String -> SwishState -> SwishState
setError (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right ags :: [RDFFormula]
ags,Right rls :: [RDFRule]
rls) ->
(RDFRulesetMap -> RDFRulesetMap) -> SwishState -> SwishState
modRulesets (Namespace -> RDFRuleset -> RDFRulesetMap -> RDFRulesetMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (RDFRuleset -> Namespace
forall ex. Ruleset ex -> Namespace
getRulesetNamespace RDFRuleset
rs) RDFRuleset
rs)
where
rs :: RDFRuleset
rs = Namespace -> [RDFFormula] -> [RDFRule] -> RDFRuleset
forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset (ScopedName -> Namespace
getScopeNamespace ScopedName
sn) [RDFFormula]
ags [RDFRule]
rls
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
frs
}
ssFindRule :: ScopedName -> SwishStateIO (Either String RDFRule)
ssFindRule :: ScopedName -> StateT SwishState IO (Either String RDFRule)
ssFindRule nam :: ScopedName
nam = (SwishState -> Either String RDFRule)
-> StateT SwishState IO (Either String RDFRule)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String RDFRule
find
where
find :: SwishState -> Either String RDFRule
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe RDFRule
findRule ScopedName
nam SwishState
st of
Nothing -> String -> Either String RDFRule
forall a b. a -> Either a b
Left ("Rule not found: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
Just rl :: RDFRule
rl -> RDFRule -> Either String RDFRule
forall a b. b -> Either a b
Right RDFRule
rl
ssDefineConstraints ::
ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> [ScopedName]
-> SwishStateIO ()
ssDefineConstraints :: ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> [ScopedName]
-> SwishStateIO ()
ssDefineConstraints sn :: ScopedName
sn cgfs :: [SwishStateIO (Either String RDFGraph)]
cgfs dtns :: [ScopedName]
dtns =
let errmsg1 :: String
errmsg1 = "Error in constraint graph(s): "
errmsg2 :: String
errmsg2 = "Error in datatype(s): "
in
do { [Either String RDFGraph]
cges <- [SwishStateIO (Either String RDFGraph)]
-> StateT SwishState IO [Either String RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFGraph)]
cgfs
; let ecgs :: Either String [RDFGraph]
ecgs = [Either String RDFGraph] -> Either String [RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFGraph]
cges :: Either String [RDFGraph]
; let ecgr :: Either String RDFGraph
ecgr = case Either String [RDFGraph]
ecgs of
Left er :: String
er -> String -> Either String RDFGraph
forall a b. a -> Either a b
Left String
er
Right [] -> RDFGraph -> Either String RDFGraph
forall a b. b -> Either a b
Right RDFGraph
forall a. Monoid a => a
mempty
Right grs :: [RDFGraph]
grs -> RDFGraph -> Either String RDFGraph
forall a b. b -> Either a b
Right (RDFGraph -> Either String RDFGraph)
-> RDFGraph -> Either String RDFGraph
forall a b. (a -> b) -> a -> b
$ (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
grs
; [Either String RDFDatatype]
edtf <- (ScopedName -> StateT SwishState IO (Either String RDFDatatype))
-> [ScopedName] -> StateT SwishState IO [Either String RDFDatatype]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ScopedName -> StateT SwishState IO (Either String RDFDatatype)
ssFindDatatype [ScopedName]
dtns
; let edts :: Either String [RDFDatatype]
edts = [Either String RDFDatatype] -> Either String [RDFDatatype]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFDatatype]
edtf :: Either String [RDFDatatype]
; let frs :: SwishState -> SwishState
frs = case (Either String RDFGraph
ecgr,Either String [RDFDatatype]
edts) of
(Left er :: String
er,_) -> String -> SwishState -> SwishState
setError (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> String -> SwishState -> SwishState
setError (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right cgr :: RDFGraph
cgr,Right dts :: [RDFDatatype]
dts) ->
(RDFRulesetMap -> RDFRulesetMap) -> SwishState -> SwishState
modRulesets (Namespace -> RDFRuleset -> RDFRulesetMap -> RDFRulesetMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (RDFRuleset -> Namespace
forall ex. Ruleset ex -> Namespace
getRulesetNamespace RDFRuleset
rs) RDFRuleset
rs)
where
rs :: RDFRuleset
rs = Namespace -> [RDFFormula] -> [RDFRule] -> RDFRuleset
forall ex. Namespace -> [Formula ex] -> [Rule ex] -> Ruleset ex
makeRuleset (ScopedName -> Namespace
getScopeNamespace ScopedName
sn) [] [RDFRule]
rls
rls :: [RDFRule]
rls = (RDFDatatype -> [RDFRule]) -> [RDFDatatype] -> [RDFRule]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (RDFDatatype -> RDFGraph -> [RDFRule]
forall ex lb vn. Datatype ex lb vn -> ex -> [Rule ex]
`typeMkRules` RDFGraph
cgr) [RDFDatatype]
dts
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
frs
}
ssFindDatatype :: ScopedName -> SwishStateIO (Either String RDFDatatype)
ssFindDatatype :: ScopedName -> StateT SwishState IO (Either String RDFDatatype)
ssFindDatatype nam :: ScopedName
nam = (SwishState -> Either String RDFDatatype)
-> StateT SwishState IO (Either String RDFDatatype)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String RDFDatatype
find
where
find :: SwishState -> Either String RDFDatatype
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe RDFDatatype
findDatatype ScopedName
nam SwishState
st of
Nothing -> String -> Either String RDFDatatype
forall a b. a -> Either a b
Left ("Datatype not found: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
nam)
Just dt :: RDFDatatype
dt -> RDFDatatype -> Either String RDFDatatype
forall a b. b -> Either a b
Right RDFDatatype
dt
ssCheckProof ::
ScopedName
-> [ScopedName]
-> SwishStateIO (Either String RDFFormula)
-> [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO (Either String RDFFormula)
-> SwishStateIO ()
ssCheckProof :: ScopedName
-> [ScopedName]
-> SwishStateIO (Either String RDFFormula)
-> [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO (Either String RDFFormula)
-> SwishStateIO ()
ssCheckProof pn :: ScopedName
pn sns :: [ScopedName]
sns igf :: SwishStateIO (Either String RDFFormula)
igf stfs :: [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
stfs rgf :: SwishStateIO (Either String RDFFormula)
rgf =
let
infmsg1 :: String
infmsg1 = "Proof satisfied: "
errmsg1 :: String
errmsg1 = "Error in proof ruleset(s): "
errmsg2 :: String
errmsg2 = "Error in proof input: "
errmsg3 :: String
errmsg3 = "Error in proof step(s): "
errmsg4 :: String
errmsg4 = "Error in proof goal: "
errmsg5 :: String
errmsg5 = "Proof not satisfied: "
proofname :: String
proofname = " (Proof "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
pnString -> String -> String
forall a. [a] -> [a] -> [a]
++")"
in
do { let rs1 :: [SwishStateIO (Either String RDFRuleset)]
rs1 = (ScopedName -> SwishStateIO (Either String RDFRuleset))
-> [ScopedName] -> [SwishStateIO (Either String RDFRuleset)]
forall a b. (a -> b) -> [a] -> [b]
map ScopedName -> SwishStateIO (Either String RDFRuleset)
ssFindRuleset [ScopedName]
sns :: [SwishStateIO (Either String RDFRuleset)]
; [Either String RDFRuleset]
rs2 <- [SwishStateIO (Either String RDFRuleset)]
-> StateT SwishState IO [Either String RDFRuleset]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFRuleset)]
rs1
; let erss :: Either String [RDFRuleset]
erss = [Either String RDFRuleset] -> Either String [RDFRuleset]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFRuleset]
rs2 :: Either String [RDFRuleset]
; Either String RDFFormula
eig <- SwishStateIO (Either String RDFFormula)
igf
; let st1 :: SwishStateIO [Either String RDFProofStep]
st1 = [SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO [Either String RDFProofStep]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO [Either String RDFProofStep])
-> [SwishStateIO (Either String RDFProofStep)]
-> SwishStateIO [Either String RDFProofStep]
forall a b. (a -> b) -> a -> b
$ [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
-> Either String [RDFRuleset]
-> [SwishStateIO (Either String RDFProofStep)]
forall a b. [a -> b] -> a -> [b]
flist [Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)]
stfs Either String [RDFRuleset]
erss :: SwishStateIO [Either String RDFProofStep]
; [Either String RDFProofStep]
st2 <- SwishStateIO [Either String RDFProofStep]
st1
; let ests :: Either String [RDFProofStep]
ests = [Either String RDFProofStep] -> Either String [RDFProofStep]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFProofStep]
st2 :: Either String [RDFProofStep]
; Either String RDFFormula
erg <- SwishStateIO (Either String RDFFormula)
rgf
; let proof :: Either String RDFProof
proof = case (Either String [RDFRuleset]
erss,Either String RDFFormula
eig,Either String [RDFProofStep]
ests,Either String RDFFormula
erg) of
(Left er :: String
er,_,_,_) -> String -> Either String RDFProof
forall a b. a -> Either a b
Left (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
erString -> String -> String
forall a. [a] -> [a] -> [a]
++String
proofname)
(_,Left er :: String
er,_,_) -> String -> Either String RDFProof
forall a b. a -> Either a b
Left (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
erString -> String -> String
forall a. [a] -> [a] -> [a]
++String
proofname)
(_,_,Left er :: String
er,_) -> String -> Either String RDFProof
forall a b. a -> Either a b
Left (String
errmsg3String -> String -> String
forall a. [a] -> [a] -> [a]
++String
erString -> String -> String
forall a. [a] -> [a] -> [a]
++String
proofname)
(_,_,_,Left er :: String
er) -> String -> Either String RDFProof
forall a b. a -> Either a b
Left (String
errmsg4String -> String -> String
forall a. [a] -> [a] -> [a]
++String
erString -> String -> String
forall a. [a] -> [a] -> [a]
++String
proofname)
(Right rss :: [RDFRuleset]
rss, Right ig :: RDFFormula
ig, Right sts :: [RDFProofStep]
sts, Right rg :: RDFFormula
rg) ->
RDFProof -> Either String RDFProof
forall a b. b -> Either a b
Right ([RDFRuleset]
-> RDFFormula -> RDFFormula -> [RDFProofStep] -> RDFProof
makeRDFProof [RDFRuleset]
rss RDFFormula
ig RDFFormula
rg [RDFProofStep]
sts)
; Bool -> SwishStateIO () -> SwishStateIO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
False (SwishStateIO () -> SwishStateIO ())
-> SwishStateIO () -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ case Either String RDFProof
proof of
(Left _) -> () -> SwishStateIO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Right pr :: RDFProof
pr) -> Maybe URI -> Builder -> SwishStateIO ()
putResourceData Maybe URI
forall a. Maybe a
Nothing (Builder -> SwishStateIO ()) -> Builder -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$
Text -> Builder
B.fromLazyText ([Text] -> Text
L.concat ["Proof ", String -> Text
L.pack (ScopedName -> String
forall a. Show a => a -> String
show ScopedName
pn), "\n"])
Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend`
String -> Builder
B.fromString (String -> RDFProof -> String -> String
forall ex. ShowLines ex => String -> Proof ex -> String -> String
showsProof "\n" RDFProof
pr "\n")
; let checkproof :: SwishState -> SwishState
checkproof = case Either String RDFProof
proof of
(Left er :: String
er) -> String -> SwishState -> SwishState
setError String
er
(Right pr :: RDFProof
pr) ->
case RDFProof -> Maybe String
forall ex. (Expression ex, Ord ex) => Proof ex -> Maybe String
explainProof RDFProof
pr of
Nothing -> String -> SwishState -> SwishState
setInfo (String
infmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
pn)
Just ex :: String
ex -> String -> SwishState -> SwishState
setError (String
errmsg5String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
pnString -> String -> String
forall a. [a] -> [a] -> [a]
++", "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
ex)
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
checkproof
}
ssCheckStep ::
ScopedName
-> [SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)
ssCheckStep :: ScopedName
-> [SwishStateIO (Either String RDFFormula)]
-> SwishStateIO (Either String RDFFormula)
-> Either String [RDFRuleset]
-> SwishStateIO (Either String RDFProofStep)
ssCheckStep _ _ _ (Left er :: String
er) = Either String RDFProofStep
-> SwishStateIO (Either String RDFProofStep)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String RDFProofStep
-> SwishStateIO (Either String RDFProofStep))
-> Either String RDFProofStep
-> SwishStateIO (Either String RDFProofStep)
forall a b. (a -> b) -> a -> b
$ String -> Either String RDFProofStep
forall a b. a -> Either a b
Left String
er
ssCheckStep rn :: ScopedName
rn eagf :: [SwishStateIO (Either String RDFFormula)]
eagf ecgf :: SwishStateIO (Either String RDFFormula)
ecgf (Right rss :: [RDFRuleset]
rss) =
let
errmsg1 :: String
errmsg1 = "Rule not in proof step ruleset(s): "
errmsg2 :: String
errmsg2 = "Error in proof step antecedent graph(s): "
errmsg3 :: String
errmsg3 = "Error in proof step consequent graph: "
in
do { let mrul :: Maybe RDFRule
mrul = ScopedName -> [RDFRuleset] -> Maybe RDFRule
forall ex. ScopedName -> [Ruleset ex] -> Maybe (Rule ex)
getMaybeContextRule ScopedName
rn [RDFRuleset]
rss :: Maybe RDFRule
; [Either String RDFFormula]
esag <- [SwishStateIO (Either String RDFFormula)]
-> SwishStateIO [Either String RDFFormula]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFFormula)]
eagf
; let eags :: Either String [RDFFormula]
eags = [Either String RDFFormula] -> Either String [RDFFormula]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFFormula]
esag :: Either String [RDFFormula]
; Either String RDFFormula
ecg <- SwishStateIO (Either String RDFFormula)
ecgf
; let est :: Either String RDFProofStep
est = case (Maybe RDFRule
mrul,Either String [RDFFormula]
eags,Either String RDFFormula
ecg) of
(Nothing,_,_) -> String -> Either String RDFProofStep
forall a b. a -> Either a b
Left (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
rn)
(_,Left er :: String
er,_) -> String -> Either String RDFProofStep
forall a b. a -> Either a b
Left (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,_,Left er :: String
er) -> String -> Either String RDFProofStep
forall a b. a -> Either a b
Left (String
errmsg3String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Just rul :: RDFRule
rul,Right ags :: [RDFFormula]
ags,Right cg :: RDFFormula
cg) ->
RDFProofStep -> Either String RDFProofStep
forall a b. b -> Either a b
Right (RDFProofStep -> Either String RDFProofStep)
-> RDFProofStep -> Either String RDFProofStep
forall a b. (a -> b) -> a -> b
$ RDFRule -> [RDFFormula] -> RDFFormula -> RDFProofStep
makeRDFProofStep RDFRule
rul [RDFFormula]
ags RDFFormula
cg
; Either String RDFProofStep
-> SwishStateIO (Either String RDFProofStep)
forall (m :: * -> *) a. Monad m => a -> m a
return Either String RDFProofStep
est
}
ssFwdChain ::
ScopedName
-> ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssFwdChain :: ScopedName
-> ScopedName
-> [SwishStateIO (Either String RDFGraph)]
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssFwdChain sn :: ScopedName
sn rn :: ScopedName
rn agfs :: [SwishStateIO (Either String RDFGraph)]
agfs cn :: ScopedName
cn prefs :: NamespaceMap
prefs =
let
errmsg1 :: String
errmsg1 = "FwdChain rule error: "
errmsg2 :: String
errmsg2 = "FwdChain antecedent error: "
in
do { Either String RDFRule
erl <- ScopedName
-> ScopedName -> StateT SwishState IO (Either String RDFRule)
ssFindRulesetRule ScopedName
sn ScopedName
rn
; [Either String RDFGraph]
aesg <- [SwishStateIO (Either String RDFGraph)]
-> StateT SwishState IO [Either String RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SwishStateIO (Either String RDFGraph)]
agfs
; let eags :: Either String [RDFGraph]
eags = [Either String RDFGraph] -> Either String [RDFGraph]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Either String RDFGraph]
aesg :: Either String [RDFGraph]
; let fcr :: SwishState -> SwishState
fcr = case (Either String RDFRule
erl,Either String [RDFGraph]
eags) of
(Left er :: String
er,_) -> String -> SwishState -> SwishState
setError (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> String -> SwishState -> SwishState
setError (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right rl :: RDFRule
rl,Right ags :: [RDFGraph]
ags) ->
(NamedGraphMap -> NamedGraphMap) -> SwishState -> SwishState
modGraphs (ScopedName -> [RDFGraph] -> NamedGraphMap -> NamedGraphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ScopedName
cn [RDFGraph
cg])
where
cg :: RDFGraph
cg = case RDFRule -> [RDFGraph] -> [RDFGraph]
forall ex. Rule ex -> [ex] -> [ex]
fwdApply RDFRule
rl [RDFGraph]
ags of
[] -> RDFGraph
forall a. Monoid a => a
mempty
grs :: [RDFGraph]
grs -> NamespaceMap -> RDFGraph -> RDFGraph
forall lb. NamespaceMap -> NSGraph lb -> NSGraph lb
setNamespaces NamespaceMap
prefs (RDFGraph -> RDFGraph) -> RDFGraph -> RDFGraph
forall a b. (a -> b) -> a -> b
$ (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [RDFGraph]
grs
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
fcr
}
ssFindRulesetRule ::
ScopedName -> ScopedName -> SwishStateIO (Either String RDFRule)
ssFindRulesetRule :: ScopedName
-> ScopedName -> StateT SwishState IO (Either String RDFRule)
ssFindRulesetRule sn :: ScopedName
sn rn :: ScopedName
rn = (SwishState -> Either String RDFRule)
-> StateT SwishState IO (Either String RDFRule)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String RDFRule
find
where
find :: SwishState -> Either String RDFRule
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe RDFRuleset
findRuleset ScopedName
sn SwishState
st of
Nothing -> String -> Either String RDFRule
forall a b. a -> Either a b
Left ("Ruleset not found: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
sn)
Just rs :: RDFRuleset
rs -> RDFRuleset -> Either String RDFRule
forall ex. Ruleset ex -> Either String (Rule ex)
find1 RDFRuleset
rs
find1 :: Ruleset ex -> Either String (Rule ex)
find1 rs :: Ruleset ex
rs = case ScopedName -> Ruleset ex -> Maybe (Rule ex)
forall ex. ScopedName -> Ruleset ex -> Maybe (Rule ex)
getRulesetRule ScopedName
rn Ruleset ex
rs of
Nothing -> String -> Either String (Rule ex)
forall a b. a -> Either a b
Left ("Rule not in ruleset: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
snString -> String -> String
forall a. [a] -> [a] -> [a]
++": "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
rn)
Just rl :: Rule ex
rl -> Rule ex -> Either String (Rule ex)
forall a b. b -> Either a b
Right Rule ex
rl
ssFindRuleset ::
ScopedName -> SwishStateIO (Either String RDFRuleset)
ssFindRuleset :: ScopedName -> SwishStateIO (Either String RDFRuleset)
ssFindRuleset sn :: ScopedName
sn = (SwishState -> Either String RDFRuleset)
-> SwishStateIO (Either String RDFRuleset)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets SwishState -> Either String RDFRuleset
find
where
find :: SwishState -> Either String RDFRuleset
find st :: SwishState
st = case ScopedName -> SwishState -> Maybe RDFRuleset
findRuleset ScopedName
sn SwishState
st of
Nothing -> String -> Either String RDFRuleset
forall a b. a -> Either a b
Left ("Ruleset not found: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ScopedName -> String
forall a. Show a => a -> String
show ScopedName
sn)
Just rs :: RDFRuleset
rs -> RDFRuleset -> Either String RDFRuleset
forall a b. b -> Either a b
Right RDFRuleset
rs
ssBwdChain ::
ScopedName
-> ScopedName
-> SwishStateIO (Either String RDFGraph)
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssBwdChain :: ScopedName
-> ScopedName
-> SwishStateIO (Either String RDFGraph)
-> ScopedName
-> NamespaceMap
-> SwishStateIO ()
ssBwdChain sn :: ScopedName
sn rn :: ScopedName
rn cgf :: SwishStateIO (Either String RDFGraph)
cgf an :: ScopedName
an prefs :: NamespaceMap
prefs =
let
errmsg1 :: String
errmsg1 = "BwdChain rule error: "
errmsg2 :: String
errmsg2 = "BwdChain goal error: "
in
do { Either String RDFRule
erl <- ScopedName
-> ScopedName -> StateT SwishState IO (Either String RDFRule)
ssFindRulesetRule ScopedName
sn ScopedName
rn
; Either String RDFGraph
ecg <- SwishStateIO (Either String RDFGraph)
cgf
; let fcr :: SwishState -> SwishState
fcr = case (Either String RDFRule
erl,Either String RDFGraph
ecg) of
(Left er :: String
er,_) -> String -> SwishState -> SwishState
setError (String
errmsg1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(_,Left er :: String
er) -> String -> SwishState -> SwishState
setError (String
errmsg2String -> String -> String
forall a. [a] -> [a] -> [a]
++String
er)
(Right rl :: RDFRule
rl,Right cg :: RDFGraph
cg) ->
(NamedGraphMap -> NamedGraphMap) -> SwishState -> SwishState
modGraphs (ScopedName -> [RDFGraph] -> NamedGraphMap -> NamedGraphMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ScopedName
an [RDFGraph]
ags)
where
ags :: [RDFGraph]
ags = ([RDFGraph] -> RDFGraph) -> [[RDFGraph]] -> [RDFGraph]
forall a b. (a -> b) -> [a] -> [b]
map [RDFGraph] -> RDFGraph
forall lb. Label lb => [NSGraph lb] -> NSGraph lb
mergegr (RDFRule -> RDFGraph -> [[RDFGraph]]
forall ex. Rule ex -> ex -> [[ex]]
bwdApply RDFRule
rl RDFGraph
cg)
mergegr :: [NSGraph lb] -> NSGraph lb
mergegr grs :: [NSGraph lb]
grs = case [NSGraph lb]
grs of
[] -> NSGraph lb
forall a. Monoid a => a
mempty
_ -> NamespaceMap -> NSGraph lb -> NSGraph lb
forall lb. NamespaceMap -> NSGraph lb -> NSGraph lb
setNamespaces NamespaceMap
prefs (NSGraph lb -> NSGraph lb) -> NSGraph lb -> NSGraph lb
forall a b. (a -> b) -> a -> b
$ (NSGraph lb -> NSGraph lb -> NSGraph lb)
-> [NSGraph lb] -> NSGraph lb
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NSGraph lb -> NSGraph lb -> NSGraph lb
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [NSGraph lb]
grs
; (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify SwishState -> SwishState
fcr
}
getResourceData :: Maybe URI -> SwishStateIO (Either String L.Text)
getResourceData :: Maybe URI -> StateT SwishState IO (Either String Text)
getResourceData muri :: Maybe URI
muri =
case Maybe URI
muri of
Nothing -> StateT SwishState IO (Either String Text)
forall a. StateT SwishState IO (Either a Text)
fromStdin
Just uri :: URI
uri -> URI -> StateT SwishState IO (Either String Text)
forall a. URI -> StateT SwishState IO (Either a Text)
fromUri URI
uri
where
fromStdin :: StateT SwishState IO (Either a Text)
fromStdin = Text -> Either a Text
forall a b. b -> Either a b
Right (Text -> Either a Text)
-> StateT SwishState IO Text
-> StateT SwishState IO (Either a Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Text -> StateT SwishState IO Text
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IO Text
LIO.getContents
fromUri :: URI -> StateT SwishState IO (Either a Text)
fromUri = URI -> StateT SwishState IO (Either a Text)
forall (t :: (* -> *) -> * -> *) a.
(Functor (t IO), MonadTrans t) =>
URI -> t IO (Either a Text)
fromFile
fromFile :: URI -> t IO (Either a Text)
fromFile uri :: URI
uri | URI -> String
uriScheme URI
uri String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "file:" = Text -> Either a Text
forall a b. b -> Either a b
Right (Text -> Either a Text) -> t IO Text -> t IO (Either a Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` IO Text -> t IO Text
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> IO Text
LIO.readFile (String -> IO Text) -> String -> IO Text
forall a b. (a -> b) -> a -> b
$ URI -> String
uriPath URI
uri)
| Bool
otherwise = String -> t IO (Either a Text)
forall a. HasCallStack => String -> a
error (String -> t IO (Either a Text)) -> String -> t IO (Either a Text)
forall a b. (a -> b) -> a -> b
$ "Unsupported file name for read: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ URI -> String
forall a. Show a => a -> String
show URI
uri
putResourceData :: Maybe URI -> B.Builder -> SwishStateIO ()
putResourceData :: Maybe URI -> Builder -> SwishStateIO ()
putResourceData muri :: Maybe URI
muri gsh :: Builder
gsh = do
Either IOError ()
ios <- IO (Either IOError ()) -> StateT SwishState IO (Either IOError ())
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Either IOError ())
-> StateT SwishState IO (Either IOError ()))
-> (IO () -> IO (Either IOError ()))
-> IO ()
-> StateT SwishState IO (Either IOError ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> IO (Either IOError ())
forall e a. Exception e => IO a -> IO (Either e a)
CE.try (IO () -> StateT SwishState IO (Either IOError ()))
-> IO () -> StateT SwishState IO (Either IOError ())
forall a b. (a -> b) -> a -> b
$ IO () -> (URI -> IO ()) -> Maybe URI -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
toStdout URI -> IO ()
toUri Maybe URI
muri
case Either IOError ()
ios of
Left ioe :: IOError
ioe -> (SwishState -> SwishState) -> SwishStateIO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SwishState -> SwishState) -> SwishStateIO ())
-> (SwishState -> SwishState) -> SwishStateIO ()
forall a b. (a -> b) -> a -> b
$ String -> SwishState -> SwishState
setError
("Error writing graph: "String -> String -> String
forall a. [a] -> [a] -> [a]
++
IOError -> String
IO.ioeGetErrorString IOError
ioe)
Right _ -> () -> SwishStateIO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
toStdout :: IO ()
toStdout = Text -> IO ()
LIO.putStrLn Text
gstr
toUri :: URI -> IO ()
toUri uri :: URI
uri | URI -> String
uriScheme URI
uri String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "file:" = String -> Text -> IO ()
LIO.writeFile (URI -> String
uriPath URI
uri) Text
gstr
| Bool
otherwise = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Unsupported scheme for write: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ URI -> String
forall a. Show a => a -> String
show URI
uri
gstr :: Text
gstr = Builder -> Text
B.toLazyText Builder
gsh