{-# language Arrows, NoMonomorphismRestriction, PatternSignatures, OverloadedStrings, LambdaCase #-}
module TPDB.CPF.Proof.Read where
import TPDB.CPF.Proof.Type
import TPDB.Data
import qualified Text.XML as X
import Text.XML.Cursor
import qualified Data.Text as DT
import qualified Data.Text.Lazy as T
import qualified Data.Text.Lazy.IO as T
import Control.Monad.Catch
import TPDB.Pretty
readCP :: T.Text -> Either SomeException [CertificationProblem]
readCP :: Text -> Either SomeException [CertificationProblem]
readCP Text
t = ( Cursor -> [CertificationProblem]
fromDoc (Cursor -> [CertificationProblem])
-> (Document -> Cursor) -> Document -> [CertificationProblem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Document -> Cursor
fromDocument ) (Document -> [CertificationProblem])
-> Either SomeException Document
-> Either SomeException [CertificationProblem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParseSettings -> Text -> Either SomeException Document
X.parseText ParseSettings
forall a. Default a => a
X.def Text
t
readFile :: FilePath -> IO CertificationProblem
readFile :: FilePath -> IO CertificationProblem
readFile FilePath
f = do
Document
doc <- ParseSettings -> FilePath -> IO Document
X.readFile ParseSettings
forall a. Default a => a
X.def FilePath
f
case Cursor -> [CertificationProblem]
fromDoc (Cursor -> [CertificationProblem])
-> Cursor -> [CertificationProblem]
forall a b. (a -> b) -> a -> b
$ Document -> Cursor
fromDocument Document
doc of
[] -> FilePath -> IO CertificationProblem
forall a. HasCallStack => FilePath -> a
error FilePath
"input contains no certification problem"
[CertificationProblem
cp] -> CertificationProblem -> IO CertificationProblem
forall (m :: * -> *) a. Monad m => a -> m a
return CertificationProblem
cp
[CertificationProblem]
cps -> FilePath -> IO CertificationProblem
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO CertificationProblem)
-> FilePath -> IO CertificationProblem
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
( FilePath
"input contains " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show ([CertificationProblem] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CertificationProblem]
cps) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" certification problems" )
FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: (CertificationProblem -> FilePath)
-> [CertificationProblem] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Any -> FilePath
forall a. Show a => a -> FilePath
show (Doc Any -> FilePath)
-> (CertificationProblem -> Doc Any)
-> CertificationProblem
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TRS Identifier Identifier -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty (TRS Identifier Identifier -> Doc Any)
-> (CertificationProblem -> TRS Identifier Identifier)
-> CertificationProblem
-> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertificationProblemInput -> TRS Identifier Identifier
trsinput_trs (CertificationProblemInput -> TRS Identifier Identifier)
-> (CertificationProblem -> CertificationProblemInput)
-> CertificationProblem
-> TRS Identifier Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertificationProblem -> CertificationProblemInput
input ) [CertificationProblem]
cps
element1 :: Name -> Cursor -> [Cursor]
element1 Name
name Cursor
c =
let info :: FilePath
info = Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take Int
100 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Cursor -> FilePath
forall a. Show a => a -> FilePath
show Cursor
c
in case Name -> Cursor -> [Cursor]
element Name
name Cursor
c of
[] -> FilePath -> [Cursor]
forall a. HasCallStack => FilePath -> a
error (FilePath -> [Cursor]) -> FilePath -> [Cursor]
forall a b. (a -> b) -> a -> b
$ FilePath
"missing element " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Name -> FilePath
forall a. Show a => a -> FilePath
show Name
name FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" in " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
info
[Cursor
e] -> [Cursor
e]
[Cursor]
_ -> FilePath -> [Cursor]
forall a. HasCallStack => FilePath -> a
error (FilePath -> [Cursor]) -> FilePath -> [Cursor]
forall a b. (a -> b) -> a -> b
$ FilePath
"more than one element " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Name -> FilePath
forall a. Show a => a -> FilePath
show Name
name FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" in " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
info
fromDoc :: Cursor -> [ CertificationProblem ]
fromDoc :: Cursor -> [CertificationProblem]
fromDoc = Name -> Cursor -> [Cursor]
element1 Name
"certificationProblem" (Cursor -> [Cursor])
-> (Cursor -> [CertificationProblem])
-> Cursor
-> [CertificationProblem]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor
c ->
( CertificationProblemInput
-> Text -> Proof -> Origin -> CertificationProblem
CertificationProblem
(CertificationProblemInput
-> Text -> Proof -> Origin -> CertificationProblem)
-> [CertificationProblemInput]
-> [Text -> Proof -> Origin -> CertificationProblem]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cursor
c Cursor
-> (Cursor -> [CertificationProblemInput])
-> [CertificationProblemInput]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"input" (Cursor -> [Cursor])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [CertificationProblemInput]
getInput )
[Text -> Proof -> Origin -> CertificationProblem]
-> [Text] -> [Proof -> Origin -> CertificationProblem]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor
c Cursor -> (Cursor -> [Text]) -> [Text]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"cpfVersion" (Cursor -> [Cursor]) -> (Cursor -> [Text]) -> Cursor -> [Text]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Text]
content )
[Proof -> Origin -> CertificationProblem]
-> [Proof] -> [Origin -> CertificationProblem]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor
c Cursor -> (Cursor -> [Proof]) -> [Proof]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"proof" (Cursor -> [Cursor]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Proof]
getProof)
[Origin -> CertificationProblem]
-> [Origin] -> [CertificationProblem]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor
c Cursor -> (Cursor -> [Origin]) -> [Origin]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"origin" (Cursor -> [Cursor]) -> (Cursor -> [Origin]) -> Cursor -> [Origin]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [Origin] -> Cursor -> [Origin]
forall (m :: * -> *) a. Monad m => a -> m a
return [Origin
ignoredOrigin] )
)
getInput :: Cursor -> [CertificationProblemInput]
getInput = Cursor -> [CertificationProblemInput]
getTerminationInput
(Cursor -> [CertificationProblemInput])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall a. Semigroup a => a -> a -> a
<> Cursor -> [CertificationProblemInput]
getComplexityInput
(Cursor -> [CertificationProblemInput])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall a. Semigroup a => a -> a -> a
<> Cursor -> [CertificationProblemInput]
getACTerminationInput
getTerminationInput :: Cursor -> [CertificationProblemInput]
getTerminationInput Cursor
c = Cursor
c Cursor
-> (Cursor -> [CertificationProblemInput])
-> [CertificationProblemInput]
forall node a. Cursor node -> (Cursor node -> a) -> a
$| Name -> Cursor -> [Cursor]
element Name
"trsInput" (Cursor -> [Cursor])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [[Rule (Term Identifier Identifier)]]
getTrsInput (Cursor -> [[Rule (Term Identifier Identifier)]])
-> ([Rule (Term Identifier Identifier)]
-> CertificationProblemInput)
-> Cursor
-> [CertificationProblemInput]
forall node a b.
(Cursor node -> [a]) -> (a -> b) -> Cursor node -> [b]
&|
\ [Rule (Term Identifier Identifier)]
i -> TRS Identifier Identifier -> CertificationProblemInput
TrsInput (TRS Identifier Identifier -> CertificationProblemInput)
-> TRS Identifier Identifier -> CertificationProblemInput
forall a b. (a -> b) -> a -> b
$ RS :: forall s r. [s] -> [Rule r] -> Bool -> RS s r
RS { rules :: [Rule (Term Identifier Identifier)]
rules = [Rule (Term Identifier Identifier)]
i , separate :: Bool
separate = Bool
False }
getACTerminationInput :: Cursor -> [CertificationProblemInput]
getACTerminationInput = Name -> Cursor -> [Cursor]
element Name
"acRewriteSystem" (Cursor -> [Cursor])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor
c -> do
let as :: [Identifier]
as = Cursor
c Cursor -> (Cursor -> [Identifier]) -> [Identifier]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"Asymbols" (Cursor -> [Cursor])
-> (Cursor -> [Identifier]) -> Cursor -> [Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Identifier]
getSymbol
cs :: [Identifier]
cs = Cursor
c Cursor -> (Cursor -> [Identifier]) -> [Identifier]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"Csymbols" (Cursor -> [Cursor])
-> (Cursor -> [Identifier]) -> Cursor -> [Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Identifier]
getSymbol
[Rule (Term Identifier Identifier)]
acrs <- Cursor -> [[Rule (Term Identifier Identifier)]]
getTrsInput Cursor
c
CertificationProblemInput -> [CertificationProblemInput]
forall (m :: * -> *) a. Monad m => a -> m a
return (CertificationProblemInput -> [CertificationProblemInput])
-> CertificationProblemInput -> [CertificationProblemInput]
forall a b. (a -> b) -> a -> b
$ ACRewriteSystem :: TRS Identifier Identifier
-> [Identifier] -> [Identifier] -> CertificationProblemInput
ACRewriteSystem
{ trsinput_trs :: TRS Identifier Identifier
trsinput_trs = RS :: forall s r. [s] -> [Rule r] -> Bool -> RS s r
RS { rules :: [Rule (Term Identifier Identifier)]
rules = [Rule (Term Identifier Identifier)]
acrs, separate :: Bool
separate = Bool
False }
, asymbols :: [Identifier]
asymbols = [Identifier]
as
, csymbols :: [Identifier]
csymbols = [Identifier]
cs
}
getSymbol :: Cursor -> [Identifier]
getSymbol = Name -> Cursor -> [Cursor]
element1 Name
"name" (Cursor -> [Cursor])
-> (Cursor -> [Identifier]) -> Cursor -> [Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor
c -> Int -> Text -> Identifier
mk Int
0 (Text -> Identifier) -> [Text] -> [Identifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor -> [Text]
content Cursor
c
getComplexityInput :: Cursor -> [CertificationProblemInput]
getComplexityInput = Name -> Cursor -> [Cursor]
element Name
"input" (Cursor -> [Cursor])
-> (Cursor -> [CertificationProblemInput])
-> Cursor
-> [CertificationProblemInput]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor
c -> do
[Rule (Term Identifier Identifier)]
trsI <- Cursor
c Cursor
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> [[Rule (Term Identifier Identifier)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"complexityInput" (Cursor -> [Cursor])
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> Cursor
-> [[Rule (Term Identifier Identifier)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Name -> Cursor -> [Cursor]
element Name
"trsInput" (Cursor -> [Cursor])
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> Cursor
-> [[Rule (Term Identifier Identifier)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [[Rule (Term Identifier Identifier)]]
getTrsInput
ComplexityMeasure
cm <- Cursor
c Cursor -> (Cursor -> [ComplexityMeasure]) -> [ComplexityMeasure]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Cursor -> [ComplexityMeasure]
getComplexityMeasure
ComplexityClass
cc <- Cursor
c Cursor -> (Cursor -> [ComplexityClass]) -> [ComplexityClass]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Cursor -> [ComplexityClass]
getComplexityClass
CertificationProblemInput -> [CertificationProblemInput]
forall (m :: * -> *) a. Monad m => a -> m a
return (CertificationProblemInput -> [CertificationProblemInput])
-> CertificationProblemInput -> [CertificationProblemInput]
forall a b. (a -> b) -> a -> b
$ ComplexityInput :: TRS Identifier Identifier
-> ComplexityMeasure
-> ComplexityClass
-> CertificationProblemInput
ComplexityInput
{ trsinput_trs :: TRS Identifier Identifier
trsinput_trs = RS :: forall s r. [s] -> [Rule r] -> Bool -> RS s r
RS { rules :: [Rule (Term Identifier Identifier)]
rules = [Rule (Term Identifier Identifier)]
trsI, separate :: Bool
separate = Bool
False }
, complexityMeasure :: ComplexityMeasure
complexityMeasure = ComplexityMeasure
cm
, complexityClass :: ComplexityClass
complexityClass = ComplexityClass
cc
}
getComplexityMeasure :: Cursor -> [ComplexityMeasure]
getComplexityMeasure =
Name -> ComplexityMeasure -> Cursor -> [ComplexityMeasure]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"derivationalComplexity" ComplexityMeasure
DerivationalComplexity
(Cursor -> [ComplexityMeasure])
-> (Cursor -> [ComplexityMeasure]) -> Cursor -> [ComplexityMeasure]
forall a. Semigroup a => a -> a -> a
<> Name -> ComplexityMeasure -> Cursor -> [ComplexityMeasure]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"runtimeComplexity" ComplexityMeasure
RuntimeComplexity
getComplexityClass :: Cursor -> [ComplexityClass]
getComplexityClass = Name -> Cursor -> [Cursor]
element Name
"polynomial" (Cursor -> [Cursor])
-> (Cursor -> [ComplexityClass]) -> Cursor -> [ComplexityClass]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor
c ->
( \ Text
s -> ComplexityClassPolynomial :: Int -> ComplexityClass
ComplexityClassPolynomial { degree :: Int
degree = FilePath -> Int
forall a. Read a => FilePath -> a
read (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
DT.unpack Text
s } ) (Text -> ComplexityClass) -> [Text] -> [ComplexityClass]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor -> [Text]
content Cursor
c
getTrsInput :: Cursor -> [[Rule (Term Identifier Identifier)]]
getTrsInput Cursor
c =
( Cursor
c Cursor
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> [[Rule (Term Identifier Identifier)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"trs" (Cursor -> [Cursor])
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> Cursor
-> [[Rule (Term Identifier Identifier)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Relation -> Cursor -> [[Rule (Term Identifier Identifier)]]
getRulesWith Relation
Strict )
[[Rule (Term Identifier Identifier)]]
-> [[Rule (Term Identifier Identifier)]]
-> [[Rule (Term Identifier Identifier)]]
forall a. Semigroup a => a -> a -> a
<> ( Cursor
c Cursor
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> [[Rule (Term Identifier Identifier)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"relativeRules" (Cursor -> [Cursor])
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> Cursor
-> [[Rule (Term Identifier Identifier)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Relation -> Cursor -> [[Rule (Term Identifier Identifier)]]
getRulesWith Relation
Weak )
getRulesWith :: Relation -> Cursor -> [[Rule (Term Identifier Identifier)]]
getRulesWith Relation
s = Name -> Cursor -> [Cursor]
element1 Name
"rules" (Cursor -> [Cursor])
-> (Cursor -> [[Rule (Term Identifier Identifier)]])
-> Cursor
-> [[Rule (Term Identifier Identifier)]]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor
c ->
[Rule (Term Identifier Identifier)]
-> [[Rule (Term Identifier Identifier)]]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Cursor
c Cursor
-> (Cursor -> [Rule (Term Identifier Identifier)])
-> [Rule (Term Identifier Identifier)]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ ( Name -> Cursor -> [Cursor]
element Name
"rule" (Cursor -> [Cursor])
-> (Cursor -> [Rule (Term Identifier Identifier)])
-> Cursor
-> [Rule (Term Identifier Identifier)]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Relation -> Cursor -> [Rule (Term Identifier Identifier)]
getRule Relation
s ) )
getRule :: Relation -> Cursor -> [ Rule (Term Identifier Identifier) ]
getRule :: Relation -> Cursor -> [Rule (Term Identifier Identifier)]
getRule Relation
s Cursor
c =
( \ Term Identifier Identifier
l Term Identifier Identifier
r -> Rule :: forall a. a -> a -> Relation -> Bool -> Rule a
Rule {lhs :: Term Identifier Identifier
lhs=Term Identifier Identifier
l,relation :: Relation
relation=Relation
s,rhs :: Term Identifier Identifier
rhs=Term Identifier Identifier
r,top :: Bool
top=Bool
False})
(Term Identifier Identifier
-> Term Identifier Identifier -> Rule (Term Identifier Identifier))
-> [Term Identifier Identifier]
-> [Term Identifier Identifier
-> Rule (Term Identifier Identifier)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cursor
c Cursor
-> (Cursor -> [Term Identifier Identifier])
-> [Term Identifier Identifier]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"lhs" (Cursor -> [Cursor])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Term Identifier Identifier]
getTerm) [Term Identifier Identifier -> Rule (Term Identifier Identifier)]
-> [Term Identifier Identifier]
-> [Rule (Term Identifier Identifier)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor
c Cursor
-> (Cursor -> [Term Identifier Identifier])
-> [Term Identifier Identifier]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"rhs" (Cursor -> [Cursor])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Term Identifier Identifier]
getTerm)
getProof :: Cursor -> [ Proof ]
getProof :: Cursor -> [Proof]
getProof Cursor
c = Cursor
c Cursor -> (Cursor -> [Proof]) -> [Proof]
forall node a. Cursor node -> (Cursor node -> a) -> a
$|
( Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"trsTerminationProof" ( TrsTerminationProof -> Proof
TrsTerminationProof TrsTerminationProof
forall a. HasCallStack => a
undefined )
(Cursor -> [Proof]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"trsNonterminationProof" ( TrsNonterminationProof -> Proof
TrsNonterminationProof TrsNonterminationProof
forall a. HasCallStack => a
undefined )
(Cursor -> [Proof]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"relativeTerminationProof" ( TrsTerminationProof -> Proof
RelativeTerminationProof TrsTerminationProof
forall a. HasCallStack => a
undefined )
(Cursor -> [Proof]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"relativeNonterminationProof" ( TrsNonterminationProof -> Proof
RelativeNonterminationProof TrsNonterminationProof
forall a. HasCallStack => a
undefined )
(Cursor -> [Proof]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"complexityProof" ( ComplexityProof -> Proof
ComplexityProof ComplexityProof
forall a. HasCallStack => a
undefined )
(Cursor -> [Proof]) -> (Cursor -> [Proof]) -> Cursor -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor -> [Proof]
forall b. Name -> b -> Cursor -> [b]
getDummy Name
"acTerminationProof" ( ACTerminationProof -> Proof
ACTerminationProof ACTerminationProof
forall a. HasCallStack => a
undefined )
)
getDummy :: X.Name -> b -> Cursor -> [ b ]
getDummy :: Name -> b -> Cursor -> [b]
getDummy Name
t b
c Cursor
cursor = Cursor
cursor Cursor -> (Cursor -> [b]) -> [b]
forall node a. Cursor node -> (Cursor node -> a) -> a
$| Name -> Cursor -> [Cursor]
element Name
t (Cursor -> [Cursor]) -> (Cursor -> [b]) -> Cursor -> [b]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [b] -> Cursor -> [b]
forall (m :: * -> *) a. Monad m => a -> m a
return [ b
c]
getTerm :: Cursor -> [ Term Identifier Identifier ]
getTerm :: Cursor -> [Term Identifier Identifier]
getTerm = Cursor -> [Term Identifier Identifier]
getVar (Cursor -> [Term Identifier Identifier])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall a. Semigroup a => a -> a -> a
<> Cursor -> [Term Identifier Identifier]
getFunApp
getVar :: Cursor -> [ Term Identifier Identifier ]
getVar :: Cursor -> [Term Identifier Identifier]
getVar = Name -> Cursor -> [Cursor]
element Name
"var" (Cursor -> [Cursor])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor
c -> ( Identifier -> Term Identifier Identifier
forall v s. v -> Term v s
Var (Identifier -> Term Identifier Identifier)
-> (Text -> Identifier) -> Text -> Term Identifier Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Identifier
mk Int
0 ) (Text -> Term Identifier Identifier)
-> [Text] -> [Term Identifier Identifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor -> [Text]
content Cursor
c
getFunApp :: Cursor -> [ Term Identifier Identifier ]
getFunApp :: Cursor -> [Term Identifier Identifier]
getFunApp = Name -> Cursor -> [Cursor]
element Name
"funapp" (Cursor -> [Cursor])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor
c -> do
Text
nm <- Cursor
c Cursor -> (Cursor -> [Text]) -> [Text]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"name" (Cursor -> [Cursor]) -> (Cursor -> [Text]) -> Cursor -> [Text]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Text]
content
let args :: [Term Identifier Identifier]
args = Cursor
c Cursor
-> (Cursor -> [Term Identifier Identifier])
-> [Term Identifier Identifier]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor -> [Cursor]
element Name
"arg" (Cursor -> [Cursor])
-> (Cursor -> [Term Identifier Identifier])
-> Cursor
-> [Term Identifier Identifier]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor -> [Term Identifier Identifier]
getTerm
f :: Identifier
f = Int -> Text -> Identifier
mk ([Term Identifier Identifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term Identifier Identifier]
args) (Text -> Identifier) -> Text -> Identifier
forall a b. (a -> b) -> a -> b
$ Text
nm
Term Identifier Identifier -> [Term Identifier Identifier]
forall (m :: * -> *) a. Monad m => a -> m a
return (Term Identifier Identifier -> [Term Identifier Identifier])
-> Term Identifier Identifier -> [Term Identifier Identifier]
forall a b. (a -> b) -> a -> b
$ Identifier
-> [Term Identifier Identifier] -> Term Identifier Identifier
forall v s. s -> [Term v s] -> Term v s
Node Identifier
f [Term Identifier Identifier]
args