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

module TPDB.CPF.Proof.Read where

import TPDB.CPF.Proof.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 -> [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