{-# language Arrows, NoMonomorphismRestriction, PatternSignatures, OverloadedStrings, LambdaCase #-}

module TPDB.CPF.Proof.Read where

import TPDB.CPF.Proof.Type as Type
import TPDB.Data

{-
import Text.XML.HXT.Arrow.XmlArrow
import Text.XML.HXT.Arrow.XmlState ( runX )
import Text.XML.HXT.Arrow.ReadDocument ( readString )
import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
import Text.XML.HXT.DOM.XmlKeywords (v_0)

import Control.Arrow
import Control.Arrow.ArrowList
import Control.Arrow.ArrowTree

import qualified TPDB.CPF.Proof.Write as W -- for testing
import qualified Text.XML.HXT.Arrow.XmlState as X 

-}

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

{- | dangerous: 
not all constructor arguments will be set.
the function produces something like

      CertificationProblem { input = CertificationProblemInput 
                          , proof = TrsTerminationProof undefined
                          }  
-}

readCP :: T.Text -> Either SomeException [CertificationProblem]
readCP :: Text -> Either SomeException [CertificationProblem]
readCP Text
t = ( Cursor Node -> [CertificationProblem]
fromDoc (Cursor Node -> [CertificationProblem])
-> (Document -> Cursor Node) -> Document -> [CertificationProblem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Document -> Cursor Node
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 :: [Char] -> IO CertificationProblem
readFile [Char]
f = do
  Document
doc  <- ParseSettings -> [Char] -> IO Document
X.readFile ParseSettings
forall a. Default a => a
X.def [Char]
f
  case Cursor Node -> [CertificationProblem]
fromDoc (Cursor Node -> [CertificationProblem])
-> Cursor Node -> [CertificationProblem]
forall a b. (a -> b) -> a -> b
$ Document -> Cursor Node
fromDocument Document
doc of
    [] -> [Char] -> IO CertificationProblem
forall a. HasCallStack => [Char] -> a
error [Char]
"input contains no certification problem"
    [CertificationProblem
cp] -> CertificationProblem -> IO CertificationProblem
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CertificationProblem
cp
    [CertificationProblem]
cps -> [Char] -> IO CertificationProblem
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO CertificationProblem)
-> [Char] -> IO CertificationProblem
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
      ( [Char]
"input contains " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([CertificationProblem] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CertificationProblem]
cps) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" certification problems" )
      [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (CertificationProblem -> [Char])
-> [CertificationProblem] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char])
-> (CertificationProblem -> Doc Any)
-> CertificationProblem
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trs -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Trs -> Doc ann
pretty (Trs -> Doc Any)
-> (CertificationProblem -> Trs) -> CertificationProblem -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertificationProblemInput -> Trs
trsinput_trs (CertificationProblemInput -> Trs)
-> (CertificationProblem -> CertificationProblemInput)
-> CertificationProblem
-> Trs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertificationProblem -> CertificationProblemInput
input ) [CertificationProblem]
cps

element1 :: Name -> Cursor Node -> [Cursor Node]
element1 Name
name Cursor Node
c =
  let info :: [Char]
info = Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take Int
100 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Cursor Node -> [Char]
forall a. Show a => a -> [Char]
show Cursor Node
c
  in  case Name -> Cursor Node -> [Cursor Node]
element Name
name Cursor Node
c of
        [] -> [Char] -> [Cursor Node]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [Cursor Node]) -> [Char] -> [Cursor Node]
forall a b. (a -> b) -> a -> b
$ [Char]
"missing element " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name -> [Char]
forall a. Show a => a -> [Char]
show Name
name [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" in " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
info
        [Cursor Node
e] -> [Cursor Node
e]
        [Cursor Node]
_ -> [Char] -> [Cursor Node]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [Cursor Node]) -> [Char] -> [Cursor Node]
forall a b. (a -> b) -> a -> b
$ [Char]
"more than one element " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name -> [Char]
forall a. Show a => a -> [Char]
show Name
name [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" in " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
info


fromDoc :: Cursor -> [ CertificationProblem ]
fromDoc :: Cursor Node -> [CertificationProblem]
fromDoc = Name -> Cursor Node -> [Cursor Node]
element1 Name
"certificationProblem" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [CertificationProblem])
-> Cursor Node
-> [CertificationProblem]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor Node
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 Node
c Cursor Node
-> (Cursor Node -> [CertificationProblemInput])
-> [CertificationProblemInput]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"input" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [CertificationProblemInput]
getInput )
     [Text -> Proof -> Origin -> CertificationProblem]
-> [Text] -> [Proof -> Origin -> CertificationProblem]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor Node
c Cursor Node -> (Cursor Node -> [Text]) -> [Text]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"cpfVersion" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Text]) -> Cursor Node -> [Text]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Text]
content )
     [Proof -> Origin -> CertificationProblem]
-> [Proof] -> [Origin -> CertificationProblem]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor Node
c Cursor Node -> (Cursor Node -> [Proof]) -> [Proof]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"proof" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Proof]
getProof)
     [Origin -> CertificationProblem]
-> [Origin] -> [CertificationProblem]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor Node
c Cursor Node -> (Cursor Node -> [Origin]) -> [Origin]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"origin" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Origin]) -> Cursor Node -> [Origin]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [Origin] -> Cursor Node -> [Origin]
forall a. a -> Cursor Node -> a
forall (m :: * -> *) a. Monad m => a -> m a
return [Origin
ignoredOrigin] )
  )

getInput :: Cursor Node -> [CertificationProblemInput]
getInput =  Cursor Node -> [CertificationProblemInput]
getTerminationInput
   (Cursor Node -> [CertificationProblemInput])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall a. Semigroup a => a -> a -> a
<> Cursor Node -> [CertificationProblemInput]
getComplexityInput
   (Cursor Node -> [CertificationProblemInput])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall a. Semigroup a => a -> a -> a
<> Cursor Node -> [CertificationProblemInput]
getACTerminationInput

getTerminationInput :: Cursor Node -> [CertificationProblemInput]
getTerminationInput Cursor Node
c = Cursor Node
c Cursor Node
-> (Cursor Node -> [CertificationProblemInput])
-> [CertificationProblemInput]
forall node a. Cursor node -> (Cursor node -> a) -> a
$| Name -> Cursor Node -> [Cursor Node]
element Name
"trsInput" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [[Rule (Term Identifier Symbol)]]
getTrsInput (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> ([Rule (Term Identifier Symbol)] -> CertificationProblemInput)
-> Cursor Node
-> [CertificationProblemInput]
forall node a b.
(Cursor node -> [a]) -> (a -> b) -> Cursor node -> [b]
&| 
   \ [Rule (Term Identifier Symbol)]
i -> Trs -> CertificationProblemInput
TrsInput (Trs -> CertificationProblemInput)
-> Trs -> CertificationProblemInput
forall a b. (a -> b) -> a -> b
$ RS { rules :: [Rule (Term Identifier Symbol)]
rules = [Rule (Term Identifier Symbol)]
i , separate :: Bool
separate = Bool
False }   

getACTerminationInput :: Cursor Node -> [CertificationProblemInput]
getACTerminationInput = Name -> Cursor Node -> [Cursor Node]
element Name
"acRewriteSystem" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor Node
c -> do
    let as :: [Symbol]
as = Cursor Node
c Cursor Node -> (Cursor Node -> [Symbol]) -> [Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"Asymbols" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Symbol]) -> Cursor Node -> [Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Symbol]
getSymbol
        cs :: [Symbol]
cs = Cursor Node
c Cursor Node -> (Cursor Node -> [Symbol]) -> [Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"Csymbols" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Symbol]) -> Cursor Node -> [Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Symbol]
getSymbol
    [Rule (Term Identifier Symbol)]
acrs <- Cursor Node -> [[Rule (Term Identifier Symbol)]]
getTrsInput Cursor Node
c
    CertificationProblemInput -> [CertificationProblemInput]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (CertificationProblemInput -> [CertificationProblemInput])
-> CertificationProblemInput -> [CertificationProblemInput]
forall a b. (a -> b) -> a -> b
$ ACRewriteSystem
      { trsinput_trs :: Trs
trsinput_trs = RS { rules :: [Rule (Term Identifier Symbol)]
rules = [Rule (Term Identifier Symbol)]
acrs, separate :: Bool
separate = Bool
False }
      , asymbols :: [Symbol]
asymbols = [Symbol]
as
      , csymbols :: [Symbol]
csymbols = [Symbol]
cs
      }


getComplexityInput :: Cursor Node -> [CertificationProblemInput]
getComplexityInput = Name -> Cursor Node -> [Cursor Node]
element Name
"input" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [CertificationProblemInput])
-> Cursor Node
-> [CertificationProblemInput]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor Node
c -> do
    [Rule (Term Identifier Symbol)]
trsI <- Cursor Node
c Cursor Node
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> [[Rule (Term Identifier Symbol)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"complexityInput" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> Cursor Node
-> [[Rule (Term Identifier Symbol)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Name -> Cursor Node -> [Cursor Node]
element Name
"trsInput" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> Cursor Node
-> [[Rule (Term Identifier Symbol)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [[Rule (Term Identifier Symbol)]]
getTrsInput
    ComplexityMeasure
cm <- Cursor Node
c Cursor Node
-> (Cursor Node -> [ComplexityMeasure]) -> [ComplexityMeasure]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Cursor Node -> [ComplexityMeasure]
getComplexityMeasure 
    ComplexityClass
cc <- Cursor Node
c Cursor Node
-> (Cursor Node -> [ComplexityClass]) -> [ComplexityClass]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Cursor Node -> [ComplexityClass]
getComplexityClass 
    CertificationProblemInput -> [CertificationProblemInput]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (CertificationProblemInput -> [CertificationProblemInput])
-> CertificationProblemInput -> [CertificationProblemInput]
forall a b. (a -> b) -> a -> b
$ ComplexityInput
        { trsinput_trs :: Trs
trsinput_trs = RS { rules :: [Rule (Term Identifier Symbol)]
rules = [Rule (Term Identifier Symbol)]
trsI, separate :: Bool
separate = Bool
False }
        , complexityMeasure :: ComplexityMeasure
complexityMeasure = ComplexityMeasure
cm
        , complexityClass :: ComplexityClass
complexityClass = ComplexityClass
cc
        }

getComplexityMeasure :: Cursor Node -> [ComplexityMeasure]
getComplexityMeasure = 
        Name -> ComplexityMeasure -> Cursor Node -> [ComplexityMeasure]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"derivationalComplexity" ComplexityMeasure
DerivationalComplexity
    (Cursor Node -> [ComplexityMeasure])
-> (Cursor Node -> [ComplexityMeasure])
-> Cursor Node
-> [ComplexityMeasure]
forall a. Semigroup a => a -> a -> a
<>  Name -> ComplexityMeasure -> Cursor Node -> [ComplexityMeasure]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"runtimeComplexity" ComplexityMeasure
RuntimeComplexity

getComplexityClass :: Cursor Node -> [ComplexityClass]
getComplexityClass = Name -> Cursor Node -> [Cursor Node]
element Name
"polynomial" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [ComplexityClass])
-> Cursor Node
-> [ComplexityClass]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor Node
c ->
  ( \ Text
s -> ComplexityClassPolynomial { degree :: Int
degree = [Char] -> Int
forall a. Read a => [Char] -> a
read ([Char] -> Int) -> [Char] -> Int
forall a b. (a -> b) -> a -> b
$ Text -> [Char]
DT.unpack Text
s } ) (Text -> ComplexityClass) -> [Text] -> [ComplexityClass]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor Node -> [Text]
content Cursor Node
c


getTrsInput :: Cursor Node -> [[Rule (Term Identifier Symbol)]]
getTrsInput Cursor Node
c =
     ( Cursor Node
c Cursor Node
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> [[Rule (Term Identifier Symbol)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"trs" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> Cursor Node
-> [[Rule (Term Identifier Symbol)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/  Relation -> Cursor Node -> [[Rule (Term Identifier Symbol)]]
getRulesWith Relation
TPDB.Data.Strict )
  [[Rule (Term Identifier Symbol)]]
-> [[Rule (Term Identifier Symbol)]]
-> [[Rule (Term Identifier Symbol)]]
forall a. Semigroup a => a -> a -> a
<> ( Cursor Node
c Cursor Node
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> [[Rule (Term Identifier Symbol)]]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"relativeRules" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> Cursor Node
-> [[Rule (Term Identifier Symbol)]]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Relation -> Cursor Node -> [[Rule (Term Identifier Symbol)]]
getRulesWith Relation
TPDB.Data.Weak )


getRulesWith :: Relation -> Cursor Node -> [[Rule (Term Identifier Symbol)]]
getRulesWith Relation
s =  Name -> Cursor Node -> [Cursor Node]
element1 Name
"rules" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [[Rule (Term Identifier Symbol)]])
-> Cursor Node
-> [[Rule (Term Identifier Symbol)]]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor Node
c ->
  [Rule (Term Identifier Symbol)]
-> [[Rule (Term Identifier Symbol)]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Cursor Node
c Cursor Node
-> (Cursor Node -> [Rule (Term Identifier Symbol)])
-> [Rule (Term Identifier Symbol)]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ ( Name -> Cursor Node -> [Cursor Node]
element Name
"rule" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Rule (Term Identifier Symbol)])
-> Cursor Node
-> [Rule (Term Identifier Symbol)]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Relation -> Cursor Node -> [Rule (Term Identifier Symbol)]
getRule Relation
s ) )

getRule :: Relation -> Cursor -> [ Rule (Term Identifier Symbol) ]
getRule :: Relation -> Cursor Node -> [Rule (Term Identifier Symbol)]
getRule Relation
s Cursor Node
c = 
  ( \ Term Identifier Symbol
l Term Identifier Symbol
r -> Rule {lhs :: Term Identifier Symbol
lhs=Term Identifier Symbol
l,relation :: Relation
relation=Relation
s,rhs :: Term Identifier Symbol
rhs=Term Identifier Symbol
r,top :: Bool
top=Bool
False, original_variable :: Maybe Identifier
original_variable=Maybe Identifier
forall a. Maybe a
Nothing})
    (Term Identifier Symbol
 -> Term Identifier Symbol -> Rule (Term Identifier Symbol))
-> [Term Identifier Symbol]
-> [Term Identifier Symbol -> Rule (Term Identifier Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cursor Node
c Cursor Node
-> (Cursor Node -> [Term Identifier Symbol])
-> [Term Identifier Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"lhs" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Term Identifier Symbol]
getTerm) [Term Identifier Symbol -> Rule (Term Identifier Symbol)]
-> [Term Identifier Symbol] -> [Rule (Term Identifier Symbol)]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Cursor Node
c Cursor Node
-> (Cursor Node -> [Term Identifier Symbol])
-> [Term Identifier Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"rhs" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Term Identifier Symbol]
getTerm)

getProof :: Cursor -> [ Proof ]
getProof :: Cursor Node -> [Proof]
getProof Cursor Node
c = Cursor Node
c Cursor Node -> (Cursor Node -> [Proof]) -> [Proof]
forall node a. Cursor node -> (Cursor node -> a) -> a
$|
     (    Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"trsTerminationProof" ( TrsTerminationProof 'Standard -> Proof
TrsTerminationProof TrsTerminationProof 'Standard
forall a. HasCallStack => a
undefined )
       (Cursor Node -> [Proof])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"trsNonterminationProof" ( TrsNonterminationProof 'Standard -> Proof
TrsNonterminationProof TrsNonterminationProof 'Standard
forall a. HasCallStack => a
undefined )
       (Cursor Node -> [Proof])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"relativeTerminationProof" ( TrsTerminationProof 'Relative -> Proof
RelativeTerminationProof TrsTerminationProof 'Relative
forall a. HasCallStack => a
undefined )
       (Cursor Node -> [Proof])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"relativeNonterminationProof" ( TrsNonterminationProof 'Relative -> Proof
RelativeNonterminationProof TrsNonterminationProof 'Relative
forall a. HasCallStack => a
undefined )
       (Cursor Node -> [Proof])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"complexityProof" ( ComplexityProof -> Proof
ComplexityProof ComplexityProof
forall a. HasCallStack => a
undefined )
       (Cursor Node -> [Proof])
-> (Cursor Node -> [Proof]) -> Cursor Node -> [Proof]
forall a. Semigroup a => a -> a -> a
<> Name -> Proof -> Cursor Node -> [Proof]
forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
"acTerminationProof" ( ACTerminationProof -> Proof
ACTerminationProof ACTerminationProof
forall a. HasCallStack => a
undefined )
     )

getDummy :: X.Name -> b -> Cursor -> [ b ]
getDummy :: forall b. Name -> b -> Cursor Node -> [b]
getDummy Name
t b
c Cursor Node
cursor = Cursor Node
cursor Cursor Node -> (Cursor Node -> [b]) -> [b]
forall node a. Cursor node -> (Cursor node -> a) -> a
$| Name -> Cursor Node -> [Cursor Node]
element Name
t (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [b]) -> Cursor Node -> [b]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [b] -> Cursor Node -> [b]
forall a. a -> Cursor Node -> a
forall (m :: * -> *) a. Monad m => a -> m a
return [ b
c]

getTerm :: Cursor -> [ Term Identifier Symbol ]
getTerm :: Cursor Node -> [Term Identifier Symbol]
getTerm = Cursor Node -> [Term Identifier Symbol]
getVar (Cursor Node -> [Term Identifier Symbol])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall a. Semigroup a => a -> a -> a
<> Cursor Node -> [Term Identifier Symbol]
getFunApp

getVar :: Cursor -> [ Term Identifier Symbol ]
getVar :: Cursor Node -> [Term Identifier Symbol]
getVar = Name -> Cursor Node -> [Cursor Node]
element Name
"var" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor Node
c -> ( Identifier -> Term Identifier Symbol
forall v s. v -> Term v s
Var (Identifier -> Term Identifier Symbol)
-> (Text -> Identifier) -> Text -> Term Identifier Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Identifier
mk Int
0 ) (Text -> Term Identifier Symbol)
-> [Text] -> [Term Identifier Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor Node -> [Text]
content Cursor Node
c

getFunApp :: Cursor -> [ Term Identifier Symbol ]
getFunApp :: Cursor Node -> [Term Identifier Symbol]
getFunApp = Name -> Cursor Node -> [Cursor Node]
element Name
"funapp" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ Cursor Node
c -> do
  Symbol
f <- Cursor Node
c Cursor Node -> (Cursor Node -> [Symbol]) -> [Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Cursor Node -> [Symbol]
getSymbol
  let args :: [Term Identifier Symbol]
args = Cursor Node
c Cursor Node
-> (Cursor Node -> [Term Identifier Symbol])
-> [Term Identifier Symbol]
forall node a. Cursor node -> (Cursor node -> [a]) -> [a]
$/ Name -> Cursor Node -> [Cursor Node]
element Name
"arg" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Term Identifier Symbol])
-> Cursor Node
-> [Term Identifier Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ Cursor Node -> [Term Identifier Symbol]
getTerm
      set_arity :: Int -> Identifier -> Identifier
set_arity Int
k Identifier
s = Int -> Text -> Identifier
mk Int
k (Text -> Identifier) -> Text -> Identifier
forall a b. (a -> b) -> a -> b
$ Identifier -> Text
TPDB.Data.name Identifier
s -- FIXME
  Term Identifier Symbol -> [Term Identifier Symbol]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Term Identifier Symbol -> [Term Identifier Symbol])
-> Term Identifier Symbol -> [Term Identifier Symbol]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Term Identifier Symbol] -> Term Identifier Symbol
forall v s. s -> [Term v s] -> Term v s
Node Symbol
f [Term Identifier Symbol]
args


getSymbol :: Cursor -> [ Symbol ]
getSymbol :: Cursor Node -> [Symbol]
getSymbol = Name -> Cursor Node -> [Cursor Node]
element1 Name
"name" (Cursor Node -> [Cursor Node])
-> (Cursor Node -> [Symbol]) -> Cursor Node -> [Symbol]
forall node a.
Axis node -> (Cursor node -> [a]) -> Cursor node -> [a]
&/ \ Cursor Node
c -> (Identifier -> Symbol
SymName (Identifier -> Symbol) -> (Text -> Identifier) -> Text -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Identifier
mk Int
0) (Text -> Symbol) -> [Text] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cursor Node -> [Text]
content Cursor Node
c