{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Static/DgUtils.hs
Description :  auxiliary datastructures for development graphs
Copyright   :  (c) DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

-}

module Static.DgUtils where

import qualified Common.Lib.Rel as Rel
import Common.IRI
import Common.Id
import Common.Utils
import Common.LibName
import Common.Consistency
import qualified Control.Monad.Fail as Fail

import Data.Data
import Data.List
import Data.Maybe

import qualified Data.Map as Map
import qualified Data.Set as Set

-- ** node label types

data XPathPart = ElemName String | ChildIndex Int deriving (Int -> XPathPart -> ShowS
[XPathPart] -> ShowS
XPathPart -> String
(Int -> XPathPart -> ShowS)
-> (XPathPart -> String)
-> ([XPathPart] -> ShowS)
-> Show XPathPart
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [XPathPart] -> ShowS
$cshowList :: [XPathPart] -> ShowS
show :: XPathPart -> String
$cshow :: XPathPart -> String
showsPrec :: Int -> XPathPart -> ShowS
$cshowsPrec :: Int -> XPathPart -> ShowS
Show, Typeable, Typeable XPathPart
Constr
DataType
Typeable XPathPart =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> XPathPart -> c XPathPart)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c XPathPart)
-> (XPathPart -> Constr)
-> (XPathPart -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c XPathPart))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XPathPart))
-> ((forall b. Data b => b -> b) -> XPathPart -> XPathPart)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> XPathPart -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> XPathPart -> r)
-> (forall u. (forall d. Data d => d -> u) -> XPathPart -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> XPathPart -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart)
-> Data XPathPart
XPathPart -> Constr
XPathPart -> DataType
(forall b. Data b => b -> b) -> XPathPart -> XPathPart
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XPathPart -> c XPathPart
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XPathPart
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> XPathPart -> u
forall u. (forall d. Data d => d -> u) -> XPathPart -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XPathPart
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XPathPart -> c XPathPart
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XPathPart)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XPathPart)
$cChildIndex :: Constr
$cElemName :: Constr
$tXPathPart :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
gmapMp :: (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
gmapM :: (forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XPathPart -> m XPathPart
gmapQi :: Int -> (forall d. Data d => d -> u) -> XPathPart -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> XPathPart -> u
gmapQ :: (forall d. Data d => d -> u) -> XPathPart -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> XPathPart -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> XPathPart -> r
gmapT :: (forall b. Data b => b -> b) -> XPathPart -> XPathPart
$cgmapT :: (forall b. Data b => b -> b) -> XPathPart -> XPathPart
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XPathPart)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XPathPart)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c XPathPart)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XPathPart)
dataTypeOf :: XPathPart -> DataType
$cdataTypeOf :: XPathPart -> DataType
toConstr :: XPathPart -> Constr
$ctoConstr :: XPathPart -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XPathPart
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XPathPart
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XPathPart -> c XPathPart
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XPathPart -> c XPathPart
$cp1Data :: Typeable XPathPart
Data)

{- | name of a node in a DG; auxiliary nodes may have extension string
     and non-zero number (for these, names are usually hidden). -}
data NodeName = NodeName
  { NodeName -> IRI
getName :: IRI
  , NodeName -> String
extString :: String
  , NodeName -> Int
extIndex :: Int
  , NodeName -> [XPathPart]
xpath :: [XPathPart]
  , NodeName -> Range
srcRange :: Range
  } deriving (Int -> NodeName -> ShowS
[NodeName] -> ShowS
NodeName -> String
(Int -> NodeName -> ShowS)
-> (NodeName -> String) -> ([NodeName] -> ShowS) -> Show NodeName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeName] -> ShowS
$cshowList :: [NodeName] -> ShowS
show :: NodeName -> String
$cshow :: NodeName -> String
showsPrec :: Int -> NodeName -> ShowS
$cshowsPrec :: Int -> NodeName -> ShowS
Show, Typeable, Typeable NodeName
Constr
DataType
Typeable NodeName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> NodeName -> c NodeName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NodeName)
-> (NodeName -> Constr)
-> (NodeName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NodeName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeName))
-> ((forall b. Data b => b -> b) -> NodeName -> NodeName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NodeName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NodeName -> r)
-> (forall u. (forall d. Data d => d -> u) -> NodeName -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> NodeName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NodeName -> m NodeName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NodeName -> m NodeName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NodeName -> m NodeName)
-> Data NodeName
NodeName -> Constr
NodeName -> DataType
(forall b. Data b => b -> b) -> NodeName -> NodeName
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeName -> c NodeName
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeName
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NodeName -> u
forall u. (forall d. Data d => d -> u) -> NodeName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NodeName -> m NodeName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeName -> m NodeName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeName -> c NodeName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NodeName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeName)
$cNodeName :: Constr
$tNodeName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NodeName -> m NodeName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeName -> m NodeName
gmapMp :: (forall d. Data d => d -> m d) -> NodeName -> m NodeName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeName -> m NodeName
gmapM :: (forall d. Data d => d -> m d) -> NodeName -> m NodeName
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NodeName -> m NodeName
gmapQi :: Int -> (forall d. Data d => d -> u) -> NodeName -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NodeName -> u
gmapQ :: (forall d. Data d => d -> u) -> NodeName -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NodeName -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeName -> r
gmapT :: (forall b. Data b => b -> b) -> NodeName -> NodeName
$cgmapT :: (forall b. Data b => b -> b) -> NodeName -> NodeName
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeName)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NodeName)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NodeName)
dataTypeOf :: NodeName -> DataType
$cdataTypeOf :: NodeName -> DataType
toConstr :: NodeName -> Constr
$ctoConstr :: NodeName -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeName
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeName -> c NodeName
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeName -> c NodeName
$cp1Data :: Typeable NodeName
Data)

instance Ord NodeName where
  compare :: NodeName -> NodeName -> Ordering
compare n1 :: NodeName
n1 n2 :: NodeName
n2 = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NodeName -> String
showName NodeName
n1) (NodeName -> String
showName NodeName
n2)

instance Eq NodeName where
  n1 :: NodeName
n1 == :: NodeName -> NodeName -> Bool
== n2 :: NodeName
n2 = NodeName -> NodeName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NodeName
n1 NodeName
n2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

readXPath :: Fail.MonadFail m => String -> m [XPathPart]
readXPath :: String -> m [XPathPart]
readXPath = (String -> m XPathPart) -> [String] -> m [XPathPart]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> m XPathPart
forall (m :: * -> *). MonadFail m => String -> m XPathPart
readXPathComp ([String] -> m [XPathPart])
-> (String -> [String]) -> String -> m [XPathPart]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn '/'

readXPathComp :: Fail.MonadFail m => String -> m XPathPart
readXPathComp :: String -> m XPathPart
readXPathComp s :: String
s = case Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 5 String
s of
  ("Spec[", s' :: String
s') -> case String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Int) -> String -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ']') String
s' of
        Just i :: Int
i -> XPathPart -> m XPathPart
forall (m :: * -> *) a. Monad m => a -> m a
return (XPathPart -> m XPathPart) -> XPathPart -> m XPathPart
forall a b. (a -> b) -> a -> b
$ Int -> XPathPart
ChildIndex Int
i
        Nothing -> String -> m XPathPart
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot read nodes ChildIndex"
  _ -> XPathPart -> m XPathPart
forall (m :: * -> *) a. Monad m => a -> m a
return (XPathPart -> m XPathPart) -> XPathPart -> m XPathPart
forall a b. (a -> b) -> a -> b
$ String -> XPathPart
ElemName String
s

isInternal :: NodeName -> Bool
isInternal :: NodeName -> Bool
isInternal n :: NodeName
n = NodeName -> Int
extIndex NodeName
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0 Bool -> Bool -> Bool
|| Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ NodeName -> String
extString NodeName
n)

-- | test if a conservativity is open, return input for None
hasOpenConsStatus :: Bool -> ConsStatus -> Bool
hasOpenConsStatus :: Bool -> ConsStatus -> Bool
hasOpenConsStatus b :: Bool
b (ConsStatus cons :: Conservativity
cons _ thm :: ThmLinkStatus
thm) = case Conservativity
cons of
    None -> Bool
b
    _ -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ThmLinkStatus -> Bool
isProvenThmLinkStatus ThmLinkStatus
thm

data DGNodeType = DGNodeType
  { DGNodeType -> Bool
isRefType :: Bool
  , DGNodeType -> Bool
isProvenNode :: Bool
  , DGNodeType -> Bool
isProvenCons :: Bool
  , DGNodeType -> Bool
isInternalSpec :: Bool }
  deriving (Int -> DGNodeType -> ShowS
[DGNodeType] -> ShowS
DGNodeType -> String
(Int -> DGNodeType -> ShowS)
-> (DGNodeType -> String)
-> ([DGNodeType] -> ShowS)
-> Show DGNodeType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGNodeType] -> ShowS
$cshowList :: [DGNodeType] -> ShowS
show :: DGNodeType -> String
$cshow :: DGNodeType -> String
showsPrec :: Int -> DGNodeType -> ShowS
$cshowsPrec :: Int -> DGNodeType -> ShowS
Show, DGNodeType -> DGNodeType -> Bool
(DGNodeType -> DGNodeType -> Bool)
-> (DGNodeType -> DGNodeType -> Bool) -> Eq DGNodeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGNodeType -> DGNodeType -> Bool
$c/= :: DGNodeType -> DGNodeType -> Bool
== :: DGNodeType -> DGNodeType -> Bool
$c== :: DGNodeType -> DGNodeType -> Bool
Eq, Eq DGNodeType
Eq DGNodeType =>
(DGNodeType -> DGNodeType -> Ordering)
-> (DGNodeType -> DGNodeType -> Bool)
-> (DGNodeType -> DGNodeType -> Bool)
-> (DGNodeType -> DGNodeType -> Bool)
-> (DGNodeType -> DGNodeType -> Bool)
-> (DGNodeType -> DGNodeType -> DGNodeType)
-> (DGNodeType -> DGNodeType -> DGNodeType)
-> Ord DGNodeType
DGNodeType -> DGNodeType -> Bool
DGNodeType -> DGNodeType -> Ordering
DGNodeType -> DGNodeType -> DGNodeType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DGNodeType -> DGNodeType -> DGNodeType
$cmin :: DGNodeType -> DGNodeType -> DGNodeType
max :: DGNodeType -> DGNodeType -> DGNodeType
$cmax :: DGNodeType -> DGNodeType -> DGNodeType
>= :: DGNodeType -> DGNodeType -> Bool
$c>= :: DGNodeType -> DGNodeType -> Bool
> :: DGNodeType -> DGNodeType -> Bool
$c> :: DGNodeType -> DGNodeType -> Bool
<= :: DGNodeType -> DGNodeType -> Bool
$c<= :: DGNodeType -> DGNodeType -> Bool
< :: DGNodeType -> DGNodeType -> Bool
$c< :: DGNodeType -> DGNodeType -> Bool
compare :: DGNodeType -> DGNodeType -> Ordering
$ccompare :: DGNodeType -> DGNodeType -> Ordering
$cp1Ord :: Eq DGNodeType
Ord, Typeable, Typeable DGNodeType
Constr
DataType
Typeable DGNodeType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DGNodeType -> c DGNodeType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DGNodeType)
-> (DGNodeType -> Constr)
-> (DGNodeType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DGNodeType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DGNodeType))
-> ((forall b. Data b => b -> b) -> DGNodeType -> DGNodeType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DGNodeType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DGNodeType -> r)
-> (forall u. (forall d. Data d => d -> u) -> DGNodeType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DGNodeType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType)
-> Data DGNodeType
DGNodeType -> Constr
DGNodeType -> DataType
(forall b. Data b => b -> b) -> DGNodeType -> DGNodeType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGNodeType -> c DGNodeType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGNodeType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DGNodeType -> u
forall u. (forall d. Data d => d -> u) -> DGNodeType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGNodeType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGNodeType -> c DGNodeType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGNodeType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGNodeType)
$cDGNodeType :: Constr
$tDGNodeType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
gmapMp :: (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
gmapM :: (forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGNodeType -> m DGNodeType
gmapQi :: Int -> (forall d. Data d => d -> u) -> DGNodeType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DGNodeType -> u
gmapQ :: (forall d. Data d => d -> u) -> DGNodeType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DGNodeType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGNodeType -> r
gmapT :: (forall b. Data b => b -> b) -> DGNodeType -> DGNodeType
$cgmapT :: (forall b. Data b => b -> b) -> DGNodeType -> DGNodeType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGNodeType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGNodeType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DGNodeType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGNodeType)
dataTypeOf :: DGNodeType -> DataType
$cdataTypeOf :: DGNodeType -> DataType
toConstr :: DGNodeType -> Constr
$ctoConstr :: DGNodeType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGNodeType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGNodeType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGNodeType -> c DGNodeType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGNodeType -> c DGNodeType
$cp1Data :: Typeable DGNodeType
Data)

listDGNodeTypes :: [DGNodeType]
listDGNodeTypes :: [DGNodeType]
listDGNodeTypes = let bs :: [Bool]
bs = [Bool
False, Bool
True] in
  [ DGNodeType :: Bool -> Bool -> Bool -> Bool -> DGNodeType
DGNodeType
    { isRefType :: Bool
isRefType = Bool
ref
    , isProvenNode :: Bool
isProvenNode = Bool
isEmpty'
    , isProvenCons :: Bool
isProvenCons = Bool
proven
    , isInternalSpec :: Bool
isInternalSpec = Bool
spec }
  | Bool
ref <- [Bool]
bs
  , Bool
isEmpty' <- [Bool]
bs
  , Bool
proven <- [Bool]
bs
  , Bool
spec <- [Bool]
bs ]

-- | node modifications
data NodeMod = NodeMod
  { NodeMod -> Bool
delAx :: Bool
  , NodeMod -> Bool
delTh :: Bool
  , NodeMod -> Bool
addSen :: Bool
  , NodeMod -> Bool
delSym :: Bool
  , NodeMod -> Bool
addSym :: Bool }
  deriving (Int -> NodeMod -> ShowS
[NodeMod] -> ShowS
NodeMod -> String
(Int -> NodeMod -> ShowS)
-> (NodeMod -> String) -> ([NodeMod] -> ShowS) -> Show NodeMod
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeMod] -> ShowS
$cshowList :: [NodeMod] -> ShowS
show :: NodeMod -> String
$cshow :: NodeMod -> String
showsPrec :: Int -> NodeMod -> ShowS
$cshowsPrec :: Int -> NodeMod -> ShowS
Show, NodeMod -> NodeMod -> Bool
(NodeMod -> NodeMod -> Bool)
-> (NodeMod -> NodeMod -> Bool) -> Eq NodeMod
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeMod -> NodeMod -> Bool
$c/= :: NodeMod -> NodeMod -> Bool
== :: NodeMod -> NodeMod -> Bool
$c== :: NodeMod -> NodeMod -> Bool
Eq, Eq NodeMod
Eq NodeMod =>
(NodeMod -> NodeMod -> Ordering)
-> (NodeMod -> NodeMod -> Bool)
-> (NodeMod -> NodeMod -> Bool)
-> (NodeMod -> NodeMod -> Bool)
-> (NodeMod -> NodeMod -> Bool)
-> (NodeMod -> NodeMod -> NodeMod)
-> (NodeMod -> NodeMod -> NodeMod)
-> Ord NodeMod
NodeMod -> NodeMod -> Bool
NodeMod -> NodeMod -> Ordering
NodeMod -> NodeMod -> NodeMod
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NodeMod -> NodeMod -> NodeMod
$cmin :: NodeMod -> NodeMod -> NodeMod
max :: NodeMod -> NodeMod -> NodeMod
$cmax :: NodeMod -> NodeMod -> NodeMod
>= :: NodeMod -> NodeMod -> Bool
$c>= :: NodeMod -> NodeMod -> Bool
> :: NodeMod -> NodeMod -> Bool
$c> :: NodeMod -> NodeMod -> Bool
<= :: NodeMod -> NodeMod -> Bool
$c<= :: NodeMod -> NodeMod -> Bool
< :: NodeMod -> NodeMod -> Bool
$c< :: NodeMod -> NodeMod -> Bool
compare :: NodeMod -> NodeMod -> Ordering
$ccompare :: NodeMod -> NodeMod -> Ordering
$cp1Ord :: Eq NodeMod
Ord, Typeable, Typeable NodeMod
Constr
DataType
Typeable NodeMod =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> NodeMod -> c NodeMod)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NodeMod)
-> (NodeMod -> Constr)
-> (NodeMod -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NodeMod))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeMod))
-> ((forall b. Data b => b -> b) -> NodeMod -> NodeMod)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NodeMod -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NodeMod -> r)
-> (forall u. (forall d. Data d => d -> u) -> NodeMod -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> NodeMod -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod)
-> Data NodeMod
NodeMod -> Constr
NodeMod -> DataType
(forall b. Data b => b -> b) -> NodeMod -> NodeMod
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeMod -> c NodeMod
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeMod
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NodeMod -> u
forall u. (forall d. Data d => d -> u) -> NodeMod -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeMod
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeMod -> c NodeMod
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NodeMod)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeMod)
$cNodeMod :: Constr
$tNodeMod :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
gmapMp :: (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
gmapM :: (forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NodeMod -> m NodeMod
gmapQi :: Int -> (forall d. Data d => d -> u) -> NodeMod -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NodeMod -> u
gmapQ :: (forall d. Data d => d -> u) -> NodeMod -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NodeMod -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NodeMod -> r
gmapT :: (forall b. Data b => b -> b) -> NodeMod -> NodeMod
$cgmapT :: (forall b. Data b => b -> b) -> NodeMod -> NodeMod
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeMod)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NodeMod)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NodeMod)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NodeMod)
dataTypeOf :: NodeMod -> DataType
$cdataTypeOf :: NodeMod -> DataType
toConstr :: NodeMod -> Constr
$ctoConstr :: NodeMod -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeMod
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NodeMod
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeMod -> c NodeMod
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NodeMod -> c NodeMod
$cp1Data :: Typeable NodeMod
Data)

-- | an unmodified node
unMod :: NodeMod
unMod :: NodeMod
unMod = Bool -> Bool -> Bool -> Bool -> Bool -> NodeMod
NodeMod Bool
False Bool
False Bool
False Bool
False Bool
False

delAxMod :: NodeMod
delAxMod :: NodeMod
delAxMod = NodeMod
unMod { delAx :: Bool
delAx = Bool
True }

delThMod :: NodeMod
delThMod :: NodeMod
delThMod = NodeMod
unMod { delTh :: Bool
delTh = Bool
True }

delSenMod :: NodeMod
delSenMod :: NodeMod
delSenMod = NodeMod
delAxMod { delTh :: Bool
delTh = Bool
True }

addSenMod :: NodeMod
addSenMod :: NodeMod
addSenMod = NodeMod
unMod { addSen :: Bool
addSen = Bool
True }

senMod :: NodeMod
senMod :: NodeMod
senMod = NodeMod
delSenMod { addSen :: Bool
addSen = Bool
True }

delSymMod :: NodeMod
delSymMod :: NodeMod
delSymMod = NodeMod
unMod { delSym :: Bool
delSym = Bool
True }

addSymMod :: NodeMod
addSymMod :: NodeMod
addSymMod = NodeMod
unMod { addSym :: Bool
addSym = Bool
True }

symMod :: NodeMod
symMod :: NodeMod
symMod = NodeMod
delSymMod { addSym :: Bool
addSym = Bool
True }

mergeNodeMod :: NodeMod -> NodeMod -> NodeMod
mergeNodeMod :: NodeMod -> NodeMod -> NodeMod
mergeNodeMod NodeMod
    { delAx :: NodeMod -> Bool
delAx = Bool
delAx1
    , delTh :: NodeMod -> Bool
delTh = Bool
delTh1
    , addSen :: NodeMod -> Bool
addSen = Bool
addSen1
    , delSym :: NodeMod -> Bool
delSym = Bool
delSym1
    , addSym :: NodeMod -> Bool
addSym = Bool
addSym1 }
    NodeMod
    { delAx :: NodeMod -> Bool
delAx = Bool
delAx2
    , delTh :: NodeMod -> Bool
delTh = Bool
delTh2
    , addSen :: NodeMod -> Bool
addSen = Bool
addSen2
    , delSym :: NodeMod -> Bool
delSym = Bool
delSym2
    , addSym :: NodeMod -> Bool
addSym = Bool
addSym2 }
    = let delSym3 :: Bool
delSym3 = Bool
delSym1 Bool -> Bool -> Bool
|| Bool
delSym2
          setSenMod :: Bool -> Bool -> Bool
setSenMod a :: Bool
a b :: Bool
b = Bool -> Bool
not Bool
delSym3 Bool -> Bool -> Bool
&& (Bool
a Bool -> Bool -> Bool
|| Bool
b)
    in NodeMod :: Bool -> Bool -> Bool -> Bool -> Bool -> NodeMod
NodeMod
    { delAx :: Bool
delAx = Bool -> Bool -> Bool
setSenMod Bool
delAx1 Bool
delAx2
    , delTh :: Bool
delTh = Bool -> Bool -> Bool
setSenMod Bool
delTh1 Bool
delTh2
    , addSen :: Bool
addSen = Bool -> Bool -> Bool
setSenMod Bool
addSen1 Bool
addSen2
    , delSym :: Bool
delSym = Bool
delSym3
    , addSym :: Bool
addSym = Bool
addSym1 Bool -> Bool -> Bool
|| Bool
addSym2 }

-- ** edge types

-- | unique number for edges
newtype EdgeId = EdgeId { EdgeId -> Int
getEdgeNum :: Int }
  deriving (EdgeId -> EdgeId -> Bool
(EdgeId -> EdgeId -> Bool)
-> (EdgeId -> EdgeId -> Bool) -> Eq EdgeId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EdgeId -> EdgeId -> Bool
$c/= :: EdgeId -> EdgeId -> Bool
== :: EdgeId -> EdgeId -> Bool
$c== :: EdgeId -> EdgeId -> Bool
Eq, Eq EdgeId
Eq EdgeId =>
(EdgeId -> EdgeId -> Ordering)
-> (EdgeId -> EdgeId -> Bool)
-> (EdgeId -> EdgeId -> Bool)
-> (EdgeId -> EdgeId -> Bool)
-> (EdgeId -> EdgeId -> Bool)
-> (EdgeId -> EdgeId -> EdgeId)
-> (EdgeId -> EdgeId -> EdgeId)
-> Ord EdgeId
EdgeId -> EdgeId -> Bool
EdgeId -> EdgeId -> Ordering
EdgeId -> EdgeId -> EdgeId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EdgeId -> EdgeId -> EdgeId
$cmin :: EdgeId -> EdgeId -> EdgeId
max :: EdgeId -> EdgeId -> EdgeId
$cmax :: EdgeId -> EdgeId -> EdgeId
>= :: EdgeId -> EdgeId -> Bool
$c>= :: EdgeId -> EdgeId -> Bool
> :: EdgeId -> EdgeId -> Bool
$c> :: EdgeId -> EdgeId -> Bool
<= :: EdgeId -> EdgeId -> Bool
$c<= :: EdgeId -> EdgeId -> Bool
< :: EdgeId -> EdgeId -> Bool
$c< :: EdgeId -> EdgeId -> Bool
compare :: EdgeId -> EdgeId -> Ordering
$ccompare :: EdgeId -> EdgeId -> Ordering
$cp1Ord :: Eq EdgeId
Ord, Typeable, Typeable EdgeId
Constr
DataType
Typeable EdgeId =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EdgeId -> c EdgeId)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EdgeId)
-> (EdgeId -> Constr)
-> (EdgeId -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EdgeId))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EdgeId))
-> ((forall b. Data b => b -> b) -> EdgeId -> EdgeId)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EdgeId -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EdgeId -> r)
-> (forall u. (forall d. Data d => d -> u) -> EdgeId -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> EdgeId -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId)
-> Data EdgeId
EdgeId -> Constr
EdgeId -> DataType
(forall b. Data b => b -> b) -> EdgeId -> EdgeId
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EdgeId -> c EdgeId
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EdgeId
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> EdgeId -> u
forall u. (forall d. Data d => d -> u) -> EdgeId -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EdgeId
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EdgeId -> c EdgeId
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EdgeId)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EdgeId)
$cEdgeId :: Constr
$tEdgeId :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
gmapMp :: (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
gmapM :: (forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EdgeId -> m EdgeId
gmapQi :: Int -> (forall d. Data d => d -> u) -> EdgeId -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EdgeId -> u
gmapQ :: (forall d. Data d => d -> u) -> EdgeId -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EdgeId -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EdgeId -> r
gmapT :: (forall b. Data b => b -> b) -> EdgeId -> EdgeId
$cgmapT :: (forall b. Data b => b -> b) -> EdgeId -> EdgeId
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EdgeId)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EdgeId)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EdgeId)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EdgeId)
dataTypeOf :: EdgeId -> DataType
$cdataTypeOf :: EdgeId -> DataType
toConstr :: EdgeId -> Constr
$ctoConstr :: EdgeId -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EdgeId
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EdgeId
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EdgeId -> c EdgeId
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EdgeId -> c EdgeId
$cp1Data :: Typeable EdgeId
Data)

instance Show EdgeId where
  show :: EdgeId -> String
show = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (EdgeId -> Int) -> EdgeId -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> Int
getEdgeNum

-- | next edge id
incEdgeId :: EdgeId -> EdgeId
incEdgeId :: EdgeId -> EdgeId
incEdgeId (EdgeId i :: Int
i) = Int -> EdgeId
EdgeId (Int -> EdgeId) -> Int -> EdgeId
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1

-- | the first edge in a graph
startEdgeId :: EdgeId
startEdgeId :: EdgeId
startEdgeId = Int -> EdgeId
EdgeId 0

showEdgeId :: EdgeId -> String
showEdgeId :: EdgeId -> String
showEdgeId (EdgeId i :: Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i

-- | a set of used edges
newtype ProofBasis = ProofBasis { ProofBasis -> Set EdgeId
proofBasis :: Set.Set EdgeId }
    deriving (ProofBasis -> ProofBasis -> Bool
(ProofBasis -> ProofBasis -> Bool)
-> (ProofBasis -> ProofBasis -> Bool) -> Eq ProofBasis
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofBasis -> ProofBasis -> Bool
$c/= :: ProofBasis -> ProofBasis -> Bool
== :: ProofBasis -> ProofBasis -> Bool
$c== :: ProofBasis -> ProofBasis -> Bool
Eq, Eq ProofBasis
Eq ProofBasis =>
(ProofBasis -> ProofBasis -> Ordering)
-> (ProofBasis -> ProofBasis -> Bool)
-> (ProofBasis -> ProofBasis -> Bool)
-> (ProofBasis -> ProofBasis -> Bool)
-> (ProofBasis -> ProofBasis -> Bool)
-> (ProofBasis -> ProofBasis -> ProofBasis)
-> (ProofBasis -> ProofBasis -> ProofBasis)
-> Ord ProofBasis
ProofBasis -> ProofBasis -> Bool
ProofBasis -> ProofBasis -> Ordering
ProofBasis -> ProofBasis -> ProofBasis
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProofBasis -> ProofBasis -> ProofBasis
$cmin :: ProofBasis -> ProofBasis -> ProofBasis
max :: ProofBasis -> ProofBasis -> ProofBasis
$cmax :: ProofBasis -> ProofBasis -> ProofBasis
>= :: ProofBasis -> ProofBasis -> Bool
$c>= :: ProofBasis -> ProofBasis -> Bool
> :: ProofBasis -> ProofBasis -> Bool
$c> :: ProofBasis -> ProofBasis -> Bool
<= :: ProofBasis -> ProofBasis -> Bool
$c<= :: ProofBasis -> ProofBasis -> Bool
< :: ProofBasis -> ProofBasis -> Bool
$c< :: ProofBasis -> ProofBasis -> Bool
compare :: ProofBasis -> ProofBasis -> Ordering
$ccompare :: ProofBasis -> ProofBasis -> Ordering
$cp1Ord :: Eq ProofBasis
Ord, Typeable, Typeable ProofBasis
Constr
DataType
Typeable ProofBasis =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProofBasis -> c ProofBasis)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProofBasis)
-> (ProofBasis -> Constr)
-> (ProofBasis -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProofBasis))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ProofBasis))
-> ((forall b. Data b => b -> b) -> ProofBasis -> ProofBasis)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofBasis -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProofBasis -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProofBasis -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProofBasis -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis)
-> Data ProofBasis
ProofBasis -> Constr
ProofBasis -> DataType
(forall b. Data b => b -> b) -> ProofBasis -> ProofBasis
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofBasis -> c ProofBasis
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofBasis
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProofBasis -> u
forall u. (forall d. Data d => d -> u) -> ProofBasis -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofBasis
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofBasis -> c ProofBasis
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofBasis)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofBasis)
$cProofBasis :: Constr
$tProofBasis :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
gmapMp :: (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
gmapM :: (forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProofBasis -> m ProofBasis
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofBasis -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProofBasis -> u
gmapQ :: (forall d. Data d => d -> u) -> ProofBasis -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProofBasis -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProofBasis -> r
gmapT :: (forall b. Data b => b -> b) -> ProofBasis -> ProofBasis
$cgmapT :: (forall b. Data b => b -> b) -> ProofBasis -> ProofBasis
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofBasis)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofBasis)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProofBasis)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProofBasis)
dataTypeOf :: ProofBasis -> DataType
$cdataTypeOf :: ProofBasis -> DataType
toConstr :: ProofBasis -> Constr
$ctoConstr :: ProofBasis -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofBasis
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProofBasis
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofBasis -> c ProofBasis
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProofBasis -> c ProofBasis
$cp1Data :: Typeable ProofBasis
Data)

instance Show ProofBasis where
  show :: ProofBasis -> String
show = [EdgeId] -> String
forall a. Show a => a -> String
show ([EdgeId] -> String)
-> (ProofBasis -> [EdgeId]) -> ProofBasis -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList (Set EdgeId -> [EdgeId])
-> (ProofBasis -> Set EdgeId) -> ProofBasis -> [EdgeId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofBasis -> Set EdgeId
proofBasis

{- | Rules in the development graph calculus,
   Sect. IV:4.4 of the CASL Reference Manual explains them in depth
-}
data DGRule =
    DGRule String
  | DGRuleWithEdge String EdgeId
  | DGRuleLocalInference [(String, String)] -- renamed theorems
  | Composition [EdgeId]
    deriving (Int -> DGRule -> ShowS
[DGRule] -> ShowS
DGRule -> String
(Int -> DGRule -> ShowS)
-> (DGRule -> String) -> ([DGRule] -> ShowS) -> Show DGRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGRule] -> ShowS
$cshowList :: [DGRule] -> ShowS
show :: DGRule -> String
$cshow :: DGRule -> String
showsPrec :: Int -> DGRule -> ShowS
$cshowsPrec :: Int -> DGRule -> ShowS
Show, DGRule -> DGRule -> Bool
(DGRule -> DGRule -> Bool)
-> (DGRule -> DGRule -> Bool) -> Eq DGRule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGRule -> DGRule -> Bool
$c/= :: DGRule -> DGRule -> Bool
== :: DGRule -> DGRule -> Bool
$c== :: DGRule -> DGRule -> Bool
Eq, Eq DGRule
Eq DGRule =>
(DGRule -> DGRule -> Ordering)
-> (DGRule -> DGRule -> Bool)
-> (DGRule -> DGRule -> Bool)
-> (DGRule -> DGRule -> Bool)
-> (DGRule -> DGRule -> Bool)
-> (DGRule -> DGRule -> DGRule)
-> (DGRule -> DGRule -> DGRule)
-> Ord DGRule
DGRule -> DGRule -> Bool
DGRule -> DGRule -> Ordering
DGRule -> DGRule -> DGRule
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DGRule -> DGRule -> DGRule
$cmin :: DGRule -> DGRule -> DGRule
max :: DGRule -> DGRule -> DGRule
$cmax :: DGRule -> DGRule -> DGRule
>= :: DGRule -> DGRule -> Bool
$c>= :: DGRule -> DGRule -> Bool
> :: DGRule -> DGRule -> Bool
$c> :: DGRule -> DGRule -> Bool
<= :: DGRule -> DGRule -> Bool
$c<= :: DGRule -> DGRule -> Bool
< :: DGRule -> DGRule -> Bool
$c< :: DGRule -> DGRule -> Bool
compare :: DGRule -> DGRule -> Ordering
$ccompare :: DGRule -> DGRule -> Ordering
$cp1Ord :: Eq DGRule
Ord, Typeable, Typeable DGRule
Constr
DataType
Typeable DGRule =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DGRule -> c DGRule)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DGRule)
-> (DGRule -> Constr)
-> (DGRule -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DGRule))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGRule))
-> ((forall b. Data b => b -> b) -> DGRule -> DGRule)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DGRule -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DGRule -> r)
-> (forall u. (forall d. Data d => d -> u) -> DGRule -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DGRule -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DGRule -> m DGRule)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGRule -> m DGRule)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGRule -> m DGRule)
-> Data DGRule
DGRule -> Constr
DGRule -> DataType
(forall b. Data b => b -> b) -> DGRule -> DGRule
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGRule -> c DGRule
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGRule
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DGRule -> u
forall u. (forall d. Data d => d -> u) -> DGRule -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGRule -> m DGRule
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGRule -> m DGRule
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGRule
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGRule -> c DGRule
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGRule)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGRule)
$cComposition :: Constr
$cDGRuleLocalInference :: Constr
$cDGRuleWithEdge :: Constr
$cDGRule :: Constr
$tDGRule :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DGRule -> m DGRule
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGRule -> m DGRule
gmapMp :: (forall d. Data d => d -> m d) -> DGRule -> m DGRule
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGRule -> m DGRule
gmapM :: (forall d. Data d => d -> m d) -> DGRule -> m DGRule
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGRule -> m DGRule
gmapQi :: Int -> (forall d. Data d => d -> u) -> DGRule -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DGRule -> u
gmapQ :: (forall d. Data d => d -> u) -> DGRule -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DGRule -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DGRule -> r
gmapT :: (forall b. Data b => b -> b) -> DGRule -> DGRule
$cgmapT :: (forall b. Data b => b -> b) -> DGRule -> DGRule
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGRule)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGRule)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DGRule)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGRule)
dataTypeOf :: DGRule -> DataType
$cdataTypeOf :: DGRule -> DataType
toConstr :: DGRule -> Constr
$ctoConstr :: DGRule -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGRule
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGRule
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGRule -> c DGRule
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGRule -> c DGRule
$cp1Data :: Typeable DGRule
Data)

-- | proof status of a link
data ThmLinkStatus = LeftOpen | Proven DGRule ProofBasis
  deriving (Int -> ThmLinkStatus -> ShowS
[ThmLinkStatus] -> ShowS
ThmLinkStatus -> String
(Int -> ThmLinkStatus -> ShowS)
-> (ThmLinkStatus -> String)
-> ([ThmLinkStatus] -> ShowS)
-> Show ThmLinkStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThmLinkStatus] -> ShowS
$cshowList :: [ThmLinkStatus] -> ShowS
show :: ThmLinkStatus -> String
$cshow :: ThmLinkStatus -> String
showsPrec :: Int -> ThmLinkStatus -> ShowS
$cshowsPrec :: Int -> ThmLinkStatus -> ShowS
Show, ThmLinkStatus -> ThmLinkStatus -> Bool
(ThmLinkStatus -> ThmLinkStatus -> Bool)
-> (ThmLinkStatus -> ThmLinkStatus -> Bool) -> Eq ThmLinkStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c/= :: ThmLinkStatus -> ThmLinkStatus -> Bool
== :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c== :: ThmLinkStatus -> ThmLinkStatus -> Bool
Eq, Eq ThmLinkStatus
Eq ThmLinkStatus =>
(ThmLinkStatus -> ThmLinkStatus -> Ordering)
-> (ThmLinkStatus -> ThmLinkStatus -> Bool)
-> (ThmLinkStatus -> ThmLinkStatus -> Bool)
-> (ThmLinkStatus -> ThmLinkStatus -> Bool)
-> (ThmLinkStatus -> ThmLinkStatus -> Bool)
-> (ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus)
-> (ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus)
-> Ord ThmLinkStatus
ThmLinkStatus -> ThmLinkStatus -> Bool
ThmLinkStatus -> ThmLinkStatus -> Ordering
ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
$cmin :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
max :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
$cmax :: ThmLinkStatus -> ThmLinkStatus -> ThmLinkStatus
>= :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c>= :: ThmLinkStatus -> ThmLinkStatus -> Bool
> :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c> :: ThmLinkStatus -> ThmLinkStatus -> Bool
<= :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c<= :: ThmLinkStatus -> ThmLinkStatus -> Bool
< :: ThmLinkStatus -> ThmLinkStatus -> Bool
$c< :: ThmLinkStatus -> ThmLinkStatus -> Bool
compare :: ThmLinkStatus -> ThmLinkStatus -> Ordering
$ccompare :: ThmLinkStatus -> ThmLinkStatus -> Ordering
$cp1Ord :: Eq ThmLinkStatus
Ord, Typeable, Typeable ThmLinkStatus
Constr
DataType
Typeable ThmLinkStatus =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ThmLinkStatus)
-> (ThmLinkStatus -> Constr)
-> (ThmLinkStatus -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ThmLinkStatus))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ThmLinkStatus))
-> ((forall b. Data b => b -> b) -> ThmLinkStatus -> ThmLinkStatus)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r)
-> (forall u. (forall d. Data d => d -> u) -> ThmLinkStatus -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ThmLinkStatus -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus)
-> Data ThmLinkStatus
ThmLinkStatus -> Constr
ThmLinkStatus -> DataType
(forall b. Data b => b -> b) -> ThmLinkStatus -> ThmLinkStatus
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmLinkStatus
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ThmLinkStatus -> u
forall u. (forall d. Data d => d -> u) -> ThmLinkStatus -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmLinkStatus
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ThmLinkStatus)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ThmLinkStatus)
$cProven :: Constr
$cLeftOpen :: Constr
$tThmLinkStatus :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
gmapMp :: (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
gmapM :: (forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ThmLinkStatus -> m ThmLinkStatus
gmapQi :: Int -> (forall d. Data d => d -> u) -> ThmLinkStatus -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ThmLinkStatus -> u
gmapQ :: (forall d. Data d => d -> u) -> ThmLinkStatus -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ThmLinkStatus -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmLinkStatus -> r
gmapT :: (forall b. Data b => b -> b) -> ThmLinkStatus -> ThmLinkStatus
$cgmapT :: (forall b. Data b => b -> b) -> ThmLinkStatus -> ThmLinkStatus
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ThmLinkStatus)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ThmLinkStatus)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ThmLinkStatus)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ThmLinkStatus)
dataTypeOf :: ThmLinkStatus -> DataType
$cdataTypeOf :: ThmLinkStatus -> DataType
toConstr :: ThmLinkStatus -> Constr
$ctoConstr :: ThmLinkStatus -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmLinkStatus
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmLinkStatus
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmLinkStatus -> c ThmLinkStatus
$cp1Data :: Typeable ThmLinkStatus
Data)

isProvenThmLinkStatus :: ThmLinkStatus -> Bool
isProvenThmLinkStatus :: ThmLinkStatus -> Bool
isProvenThmLinkStatus tls :: ThmLinkStatus
tls = case ThmLinkStatus
tls of
  LeftOpen -> Bool
False
  _ -> Bool
True

proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
proofBasisOfThmLinkStatus tls :: ThmLinkStatus
tls = case ThmLinkStatus
tls of
  LeftOpen -> ProofBasis
emptyProofBasis
  Proven _ pB :: ProofBasis
pB -> ProofBasis
pB

updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
updProofBasisOfThmLinkStatus tls :: ThmLinkStatus
tls pB :: ProofBasis
pB = case ThmLinkStatus
tls of
  LeftOpen -> ThmLinkStatus
tls
  Proven r :: DGRule
r _ -> DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
r ProofBasis
pB

data Scope = Local | Global deriving (Int -> Scope -> ShowS
[Scope] -> ShowS
Scope -> String
(Int -> Scope -> ShowS)
-> (Scope -> String) -> ([Scope] -> ShowS) -> Show Scope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Scope] -> ShowS
$cshowList :: [Scope] -> ShowS
show :: Scope -> String
$cshow :: Scope -> String
showsPrec :: Int -> Scope -> ShowS
$cshowsPrec :: Int -> Scope -> ShowS
Show, Scope -> Scope -> Bool
(Scope -> Scope -> Bool) -> (Scope -> Scope -> Bool) -> Eq Scope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Scope -> Scope -> Bool
$c/= :: Scope -> Scope -> Bool
== :: Scope -> Scope -> Bool
$c== :: Scope -> Scope -> Bool
Eq, Eq Scope
Eq Scope =>
(Scope -> Scope -> Ordering)
-> (Scope -> Scope -> Bool)
-> (Scope -> Scope -> Bool)
-> (Scope -> Scope -> Bool)
-> (Scope -> Scope -> Bool)
-> (Scope -> Scope -> Scope)
-> (Scope -> Scope -> Scope)
-> Ord Scope
Scope -> Scope -> Bool
Scope -> Scope -> Ordering
Scope -> Scope -> Scope
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Scope -> Scope -> Scope
$cmin :: Scope -> Scope -> Scope
max :: Scope -> Scope -> Scope
$cmax :: Scope -> Scope -> Scope
>= :: Scope -> Scope -> Bool
$c>= :: Scope -> Scope -> Bool
> :: Scope -> Scope -> Bool
$c> :: Scope -> Scope -> Bool
<= :: Scope -> Scope -> Bool
$c<= :: Scope -> Scope -> Bool
< :: Scope -> Scope -> Bool
$c< :: Scope -> Scope -> Bool
compare :: Scope -> Scope -> Ordering
$ccompare :: Scope -> Scope -> Ordering
$cp1Ord :: Eq Scope
Ord, Typeable, Typeable Scope
Constr
DataType
Typeable Scope =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Scope -> c Scope)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Scope)
-> (Scope -> Constr)
-> (Scope -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Scope))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope))
-> ((forall b. Data b => b -> b) -> Scope -> Scope)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r)
-> (forall u. (forall d. Data d => d -> u) -> Scope -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Scope -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Scope -> m Scope)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Scope -> m Scope)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Scope -> m Scope)
-> Data Scope
Scope -> Constr
Scope -> DataType
(forall b. Data b => b -> b) -> Scope -> Scope
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scope -> c Scope
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scope
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Scope -> u
forall u. (forall d. Data d => d -> u) -> Scope -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scope -> m Scope
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scope -> m Scope
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scope
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scope -> c Scope
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scope)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope)
$cGlobal :: Constr
$cLocal :: Constr
$tScope :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Scope -> m Scope
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scope -> m Scope
gmapMp :: (forall d. Data d => d -> m d) -> Scope -> m Scope
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scope -> m Scope
gmapM :: (forall d. Data d => d -> m d) -> Scope -> m Scope
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scope -> m Scope
gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scope -> u
gmapQ :: (forall d. Data d => d -> u) -> Scope -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Scope -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r
gmapT :: (forall b. Data b => b -> b) -> Scope -> Scope
$cgmapT :: (forall b. Data b => b -> b) -> Scope -> Scope
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Scope)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scope)
dataTypeOf :: Scope -> DataType
$cdataTypeOf :: Scope -> DataType
toConstr :: Scope -> Constr
$ctoConstr :: Scope -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scope
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scope
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scope -> c Scope
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scope -> c Scope
$cp1Data :: Typeable Scope
Data)

data LinkKind = DefLink | ThmLink ThmLinkStatus
  deriving (Int -> LinkKind -> ShowS
[LinkKind] -> ShowS
LinkKind -> String
(Int -> LinkKind -> ShowS)
-> (LinkKind -> String) -> ([LinkKind] -> ShowS) -> Show LinkKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LinkKind] -> ShowS
$cshowList :: [LinkKind] -> ShowS
show :: LinkKind -> String
$cshow :: LinkKind -> String
showsPrec :: Int -> LinkKind -> ShowS
$cshowsPrec :: Int -> LinkKind -> ShowS
Show, LinkKind -> LinkKind -> Bool
(LinkKind -> LinkKind -> Bool)
-> (LinkKind -> LinkKind -> Bool) -> Eq LinkKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LinkKind -> LinkKind -> Bool
$c/= :: LinkKind -> LinkKind -> Bool
== :: LinkKind -> LinkKind -> Bool
$c== :: LinkKind -> LinkKind -> Bool
Eq, Eq LinkKind
Eq LinkKind =>
(LinkKind -> LinkKind -> Ordering)
-> (LinkKind -> LinkKind -> Bool)
-> (LinkKind -> LinkKind -> Bool)
-> (LinkKind -> LinkKind -> Bool)
-> (LinkKind -> LinkKind -> Bool)
-> (LinkKind -> LinkKind -> LinkKind)
-> (LinkKind -> LinkKind -> LinkKind)
-> Ord LinkKind
LinkKind -> LinkKind -> Bool
LinkKind -> LinkKind -> Ordering
LinkKind -> LinkKind -> LinkKind
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LinkKind -> LinkKind -> LinkKind
$cmin :: LinkKind -> LinkKind -> LinkKind
max :: LinkKind -> LinkKind -> LinkKind
$cmax :: LinkKind -> LinkKind -> LinkKind
>= :: LinkKind -> LinkKind -> Bool
$c>= :: LinkKind -> LinkKind -> Bool
> :: LinkKind -> LinkKind -> Bool
$c> :: LinkKind -> LinkKind -> Bool
<= :: LinkKind -> LinkKind -> Bool
$c<= :: LinkKind -> LinkKind -> Bool
< :: LinkKind -> LinkKind -> Bool
$c< :: LinkKind -> LinkKind -> Bool
compare :: LinkKind -> LinkKind -> Ordering
$ccompare :: LinkKind -> LinkKind -> Ordering
$cp1Ord :: Eq LinkKind
Ord, Typeable, Typeable LinkKind
Constr
DataType
Typeable LinkKind =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LinkKind -> c LinkKind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LinkKind)
-> (LinkKind -> Constr)
-> (LinkKind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LinkKind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LinkKind))
-> ((forall b. Data b => b -> b) -> LinkKind -> LinkKind)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LinkKind -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LinkKind -> r)
-> (forall u. (forall d. Data d => d -> u) -> LinkKind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LinkKind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind)
-> Data LinkKind
LinkKind -> Constr
LinkKind -> DataType
(forall b. Data b => b -> b) -> LinkKind -> LinkKind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LinkKind -> c LinkKind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LinkKind
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LinkKind -> u
forall u. (forall d. Data d => d -> u) -> LinkKind -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LinkKind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LinkKind -> c LinkKind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LinkKind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LinkKind)
$cThmLink :: Constr
$cDefLink :: Constr
$tLinkKind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
gmapMp :: (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
gmapM :: (forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LinkKind -> m LinkKind
gmapQi :: Int -> (forall d. Data d => d -> u) -> LinkKind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LinkKind -> u
gmapQ :: (forall d. Data d => d -> u) -> LinkKind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LinkKind -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LinkKind -> r
gmapT :: (forall b. Data b => b -> b) -> LinkKind -> LinkKind
$cgmapT :: (forall b. Data b => b -> b) -> LinkKind -> LinkKind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LinkKind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LinkKind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LinkKind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LinkKind)
dataTypeOf :: LinkKind -> DataType
$cdataTypeOf :: LinkKind -> DataType
toConstr :: LinkKind -> Constr
$ctoConstr :: LinkKind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LinkKind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LinkKind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LinkKind -> c LinkKind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LinkKind -> c LinkKind
$cp1Data :: Typeable LinkKind
Data)

data FreeOrCofree = Free | Cofree | NPFree | Minimize
  deriving (Int -> FreeOrCofree -> ShowS
[FreeOrCofree] -> ShowS
FreeOrCofree -> String
(Int -> FreeOrCofree -> ShowS)
-> (FreeOrCofree -> String)
-> ([FreeOrCofree] -> ShowS)
-> Show FreeOrCofree
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreeOrCofree] -> ShowS
$cshowList :: [FreeOrCofree] -> ShowS
show :: FreeOrCofree -> String
$cshow :: FreeOrCofree -> String
showsPrec :: Int -> FreeOrCofree -> ShowS
$cshowsPrec :: Int -> FreeOrCofree -> ShowS
Show, FreeOrCofree -> FreeOrCofree -> Bool
(FreeOrCofree -> FreeOrCofree -> Bool)
-> (FreeOrCofree -> FreeOrCofree -> Bool) -> Eq FreeOrCofree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FreeOrCofree -> FreeOrCofree -> Bool
$c/= :: FreeOrCofree -> FreeOrCofree -> Bool
== :: FreeOrCofree -> FreeOrCofree -> Bool
$c== :: FreeOrCofree -> FreeOrCofree -> Bool
Eq, Eq FreeOrCofree
Eq FreeOrCofree =>
(FreeOrCofree -> FreeOrCofree -> Ordering)
-> (FreeOrCofree -> FreeOrCofree -> Bool)
-> (FreeOrCofree -> FreeOrCofree -> Bool)
-> (FreeOrCofree -> FreeOrCofree -> Bool)
-> (FreeOrCofree -> FreeOrCofree -> Bool)
-> (FreeOrCofree -> FreeOrCofree -> FreeOrCofree)
-> (FreeOrCofree -> FreeOrCofree -> FreeOrCofree)
-> Ord FreeOrCofree
FreeOrCofree -> FreeOrCofree -> Bool
FreeOrCofree -> FreeOrCofree -> Ordering
FreeOrCofree -> FreeOrCofree -> FreeOrCofree
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree
$cmin :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree
max :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree
$cmax :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree
>= :: FreeOrCofree -> FreeOrCofree -> Bool
$c>= :: FreeOrCofree -> FreeOrCofree -> Bool
> :: FreeOrCofree -> FreeOrCofree -> Bool
$c> :: FreeOrCofree -> FreeOrCofree -> Bool
<= :: FreeOrCofree -> FreeOrCofree -> Bool
$c<= :: FreeOrCofree -> FreeOrCofree -> Bool
< :: FreeOrCofree -> FreeOrCofree -> Bool
$c< :: FreeOrCofree -> FreeOrCofree -> Bool
compare :: FreeOrCofree -> FreeOrCofree -> Ordering
$ccompare :: FreeOrCofree -> FreeOrCofree -> Ordering
$cp1Ord :: Eq FreeOrCofree
Ord, Int -> FreeOrCofree
FreeOrCofree -> Int
FreeOrCofree -> [FreeOrCofree]
FreeOrCofree -> FreeOrCofree
FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
FreeOrCofree -> FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
(FreeOrCofree -> FreeOrCofree)
-> (FreeOrCofree -> FreeOrCofree)
-> (Int -> FreeOrCofree)
-> (FreeOrCofree -> Int)
-> (FreeOrCofree -> [FreeOrCofree])
-> (FreeOrCofree -> FreeOrCofree -> [FreeOrCofree])
-> (FreeOrCofree -> FreeOrCofree -> [FreeOrCofree])
-> (FreeOrCofree -> FreeOrCofree -> FreeOrCofree -> [FreeOrCofree])
-> Enum FreeOrCofree
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
$cenumFromThenTo :: FreeOrCofree -> FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
enumFromTo :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
$cenumFromTo :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
enumFromThen :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
$cenumFromThen :: FreeOrCofree -> FreeOrCofree -> [FreeOrCofree]
enumFrom :: FreeOrCofree -> [FreeOrCofree]
$cenumFrom :: FreeOrCofree -> [FreeOrCofree]
fromEnum :: FreeOrCofree -> Int
$cfromEnum :: FreeOrCofree -> Int
toEnum :: Int -> FreeOrCofree
$ctoEnum :: Int -> FreeOrCofree
pred :: FreeOrCofree -> FreeOrCofree
$cpred :: FreeOrCofree -> FreeOrCofree
succ :: FreeOrCofree -> FreeOrCofree
$csucc :: FreeOrCofree -> FreeOrCofree
Enum, FreeOrCofree
FreeOrCofree -> FreeOrCofree -> Bounded FreeOrCofree
forall a. a -> a -> Bounded a
maxBound :: FreeOrCofree
$cmaxBound :: FreeOrCofree
minBound :: FreeOrCofree
$cminBound :: FreeOrCofree
Bounded, ReadPrec [FreeOrCofree]
ReadPrec FreeOrCofree
Int -> ReadS FreeOrCofree
ReadS [FreeOrCofree]
(Int -> ReadS FreeOrCofree)
-> ReadS [FreeOrCofree]
-> ReadPrec FreeOrCofree
-> ReadPrec [FreeOrCofree]
-> Read FreeOrCofree
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [FreeOrCofree]
$creadListPrec :: ReadPrec [FreeOrCofree]
readPrec :: ReadPrec FreeOrCofree
$creadPrec :: ReadPrec FreeOrCofree
readList :: ReadS [FreeOrCofree]
$creadList :: ReadS [FreeOrCofree]
readsPrec :: Int -> ReadS FreeOrCofree
$creadsPrec :: Int -> ReadS FreeOrCofree
Read, Typeable, Typeable FreeOrCofree
Constr
DataType
Typeable FreeOrCofree =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FreeOrCofree)
-> (FreeOrCofree -> Constr)
-> (FreeOrCofree -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FreeOrCofree))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c FreeOrCofree))
-> ((forall b. Data b => b -> b) -> FreeOrCofree -> FreeOrCofree)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r)
-> (forall u. (forall d. Data d => d -> u) -> FreeOrCofree -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FreeOrCofree -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree)
-> Data FreeOrCofree
FreeOrCofree -> Constr
FreeOrCofree -> DataType
(forall b. Data b => b -> b) -> FreeOrCofree -> FreeOrCofree
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FreeOrCofree
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FreeOrCofree -> u
forall u. (forall d. Data d => d -> u) -> FreeOrCofree -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FreeOrCofree
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FreeOrCofree)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FreeOrCofree)
$cMinimize :: Constr
$cNPFree :: Constr
$cCofree :: Constr
$cFree :: Constr
$tFreeOrCofree :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
gmapMp :: (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
gmapM :: (forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FreeOrCofree -> m FreeOrCofree
gmapQi :: Int -> (forall d. Data d => d -> u) -> FreeOrCofree -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FreeOrCofree -> u
gmapQ :: (forall d. Data d => d -> u) -> FreeOrCofree -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FreeOrCofree -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FreeOrCofree -> r
gmapT :: (forall b. Data b => b -> b) -> FreeOrCofree -> FreeOrCofree
$cgmapT :: (forall b. Data b => b -> b) -> FreeOrCofree -> FreeOrCofree
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FreeOrCofree)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FreeOrCofree)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FreeOrCofree)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FreeOrCofree)
dataTypeOf :: FreeOrCofree -> DataType
$cdataTypeOf :: FreeOrCofree -> DataType
toConstr :: FreeOrCofree -> Constr
$ctoConstr :: FreeOrCofree -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FreeOrCofree
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FreeOrCofree
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FreeOrCofree -> c FreeOrCofree
$cp1Data :: Typeable FreeOrCofree
Data)

fcList :: [FreeOrCofree]
fcList :: [FreeOrCofree]
fcList = [FreeOrCofree
forall a. Bounded a => a
minBound .. FreeOrCofree
forall a. Bounded a => a
maxBound]

-- | required and proven conservativity (with a proof)
data ConsStatus = ConsStatus
  { ConsStatus -> Conservativity
requiredConservativity :: Conservativity,
    ConsStatus -> Conservativity
provenConservativity :: Conservativity,
    ConsStatus -> ThmLinkStatus
linkStatus :: ThmLinkStatus
  }
  deriving (Int -> ConsStatus -> ShowS
[ConsStatus] -> ShowS
ConsStatus -> String
(Int -> ConsStatus -> ShowS)
-> (ConsStatus -> String)
-> ([ConsStatus] -> ShowS)
-> Show ConsStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConsStatus] -> ShowS
$cshowList :: [ConsStatus] -> ShowS
show :: ConsStatus -> String
$cshow :: ConsStatus -> String
showsPrec :: Int -> ConsStatus -> ShowS
$cshowsPrec :: Int -> ConsStatus -> ShowS
Show, ConsStatus -> ConsStatus -> Bool
(ConsStatus -> ConsStatus -> Bool)
-> (ConsStatus -> ConsStatus -> Bool) -> Eq ConsStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConsStatus -> ConsStatus -> Bool
$c/= :: ConsStatus -> ConsStatus -> Bool
== :: ConsStatus -> ConsStatus -> Bool
$c== :: ConsStatus -> ConsStatus -> Bool
Eq, Eq ConsStatus
Eq ConsStatus =>
(ConsStatus -> ConsStatus -> Ordering)
-> (ConsStatus -> ConsStatus -> Bool)
-> (ConsStatus -> ConsStatus -> Bool)
-> (ConsStatus -> ConsStatus -> Bool)
-> (ConsStatus -> ConsStatus -> Bool)
-> (ConsStatus -> ConsStatus -> ConsStatus)
-> (ConsStatus -> ConsStatus -> ConsStatus)
-> Ord ConsStatus
ConsStatus -> ConsStatus -> Bool
ConsStatus -> ConsStatus -> Ordering
ConsStatus -> ConsStatus -> ConsStatus
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ConsStatus -> ConsStatus -> ConsStatus
$cmin :: ConsStatus -> ConsStatus -> ConsStatus
max :: ConsStatus -> ConsStatus -> ConsStatus
$cmax :: ConsStatus -> ConsStatus -> ConsStatus
>= :: ConsStatus -> ConsStatus -> Bool
$c>= :: ConsStatus -> ConsStatus -> Bool
> :: ConsStatus -> ConsStatus -> Bool
$c> :: ConsStatus -> ConsStatus -> Bool
<= :: ConsStatus -> ConsStatus -> Bool
$c<= :: ConsStatus -> ConsStatus -> Bool
< :: ConsStatus -> ConsStatus -> Bool
$c< :: ConsStatus -> ConsStatus -> Bool
compare :: ConsStatus -> ConsStatus -> Ordering
$ccompare :: ConsStatus -> ConsStatus -> Ordering
$cp1Ord :: Eq ConsStatus
Ord, Typeable, Typeable ConsStatus
Constr
DataType
Typeable ConsStatus =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ConsStatus -> c ConsStatus)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ConsStatus)
-> (ConsStatus -> Constr)
-> (ConsStatus -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ConsStatus))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ConsStatus))
-> ((forall b. Data b => b -> b) -> ConsStatus -> ConsStatus)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ConsStatus -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ConsStatus -> r)
-> (forall u. (forall d. Data d => d -> u) -> ConsStatus -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ConsStatus -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus)
-> Data ConsStatus
ConsStatus -> Constr
ConsStatus -> DataType
(forall b. Data b => b -> b) -> ConsStatus -> ConsStatus
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConsStatus -> c ConsStatus
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConsStatus
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ConsStatus -> u
forall u. (forall d. Data d => d -> u) -> ConsStatus -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConsStatus
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConsStatus -> c ConsStatus
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConsStatus)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConsStatus)
$cConsStatus :: Constr
$tConsStatus :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
gmapMp :: (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
gmapM :: (forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ConsStatus -> m ConsStatus
gmapQi :: Int -> (forall d. Data d => d -> u) -> ConsStatus -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ConsStatus -> u
gmapQ :: (forall d. Data d => d -> u) -> ConsStatus -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ConsStatus -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ConsStatus -> r
gmapT :: (forall b. Data b => b -> b) -> ConsStatus -> ConsStatus
$cgmapT :: (forall b. Data b => b -> b) -> ConsStatus -> ConsStatus
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConsStatus)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConsStatus)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ConsStatus)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ConsStatus)
dataTypeOf :: ConsStatus -> DataType
$cdataTypeOf :: ConsStatus -> DataType
toConstr :: ConsStatus -> Constr
$ctoConstr :: ConsStatus -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConsStatus
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ConsStatus
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConsStatus -> c ConsStatus
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ConsStatus -> c ConsStatus
$cp1Data :: Typeable ConsStatus
Data)

isProvenConsStatusLink :: ConsStatus -> Bool
isProvenConsStatusLink :: ConsStatus -> Bool
isProvenConsStatusLink = Bool -> Bool
not (Bool -> Bool) -> (ConsStatus -> Bool) -> ConsStatus -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ConsStatus -> Bool
hasOpenConsStatus Bool
False

mkConsStatus :: Conservativity -> ConsStatus
mkConsStatus :: Conservativity -> ConsStatus
mkConsStatus c :: Conservativity
c = Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
c Conservativity
None ThmLinkStatus
LeftOpen

getConsOfStatus :: ConsStatus -> Conservativity
getConsOfStatus :: ConsStatus -> Conservativity
getConsOfStatus (ConsStatus c :: Conservativity
c _ _) = Conservativity
c

-- | to be displayed as edge label
showConsStatus :: ConsStatus -> String
showConsStatus :: ConsStatus -> String
showConsStatus cs :: ConsStatus
cs = case ConsStatus
cs of
  ConsStatus None None _ -> ""
  ConsStatus None _ LeftOpen -> ""
  ConsStatus c :: Conservativity
c _ LeftOpen -> Conservativity -> String
forall a. Show a => a -> String
show Conservativity
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ "?"
  ConsStatus _ cp :: Conservativity
cp _ -> Conservativity -> String
forall a. Show a => a -> String
show Conservativity
cp

-- | converts a DGEdgeType to a String
getDGEdgeTypeName :: DGEdgeType -> String
getDGEdgeTypeName :: DGEdgeType -> String
getDGEdgeTypeName e :: DGEdgeType
e =
  (if DGEdgeType -> Bool
isInc DGEdgeType
e then (String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Inc") else ShowS
forall a. a -> a
id)
  ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ DGEdgeTypeModInc -> String
getDGEdgeTypeModIncName (DGEdgeTypeModInc -> String) -> DGEdgeTypeModInc -> String
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e

revertDGEdgeTypeName :: String -> DGEdgeType
revertDGEdgeTypeName :: String -> DGEdgeType
revertDGEdgeTypeName tp :: String
tp = DGEdgeType -> Maybe DGEdgeType -> DGEdgeType
forall a. a -> Maybe a -> a
fromMaybe (String -> DGEdgeType
forall a. HasCallStack => String -> a
error "DevGraph.revertDGEdgeTypeName")
  (Maybe DGEdgeType -> DGEdgeType) -> Maybe DGEdgeType -> DGEdgeType
forall a b. (a -> b) -> a -> b
$ (DGEdgeType -> Bool) -> [DGEdgeType] -> Maybe DGEdgeType
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
tp) (String -> Bool) -> (DGEdgeType -> String) -> DGEdgeType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGEdgeType -> String
getDGEdgeTypeName) [DGEdgeType]
listDGEdgeTypes

getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
getDGEdgeTypeModIncName et :: DGEdgeTypeModInc
et = case DGEdgeTypeModInc
et of
  ThmType thm :: ThmTypes
thm isPrvn :: Bool
isPrvn _ _ ->
    let prvn :: String
prvn = (if Bool
isPrvn then "P" else "Unp") String -> ShowS
forall a. [a] -> [a] -> [a]
++ "roven" in
    case ThmTypes
thm of
      HidingThm -> String
prvn String -> ShowS
forall a. [a] -> [a] -> [a]
++ "HidingThm"
      FreeOrCofreeThm fc :: FreeOrCofree
fc -> String
prvn String -> ShowS
forall a. [a] -> [a] -> [a]
++ FreeOrCofree -> ShowS
forall a. Show a => a -> ShowS
shows FreeOrCofree
fc "Thm"
      GlobalOrLocalThm scope :: Scope
scope isHom :: Bool
isHom ->
          let het :: ShowS
het = if Bool
isHom then ShowS
forall a. a -> a
id else ("Het" String -> ShowS
forall a. [a] -> [a] -> [a]
++) in
          ShowS
het (case Scope
scope of
                 Local -> "Local"
                 Global -> if Bool
isHom then "Global" else "") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
prvn String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Thm"
  FreeOrCofreeDef fc :: FreeOrCofree
fc -> FreeOrCofree -> ShowS
forall a. Show a => a -> ShowS
shows FreeOrCofree
fc "Def"
  _ -> DGEdgeTypeModInc -> String
forall a. Show a => a -> String
show DGEdgeTypeModInc
et

data DGEdgeType = DGEdgeType
  { DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc :: DGEdgeTypeModInc
  , DGEdgeType -> Bool
isInc :: Bool }
  deriving (Int -> DGEdgeType -> ShowS
[DGEdgeType] -> ShowS
DGEdgeType -> String
(Int -> DGEdgeType -> ShowS)
-> (DGEdgeType -> String)
-> ([DGEdgeType] -> ShowS)
-> Show DGEdgeType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGEdgeType] -> ShowS
$cshowList :: [DGEdgeType] -> ShowS
show :: DGEdgeType -> String
$cshow :: DGEdgeType -> String
showsPrec :: Int -> DGEdgeType -> ShowS
$cshowsPrec :: Int -> DGEdgeType -> ShowS
Show, DGEdgeType -> DGEdgeType -> Bool
(DGEdgeType -> DGEdgeType -> Bool)
-> (DGEdgeType -> DGEdgeType -> Bool) -> Eq DGEdgeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGEdgeType -> DGEdgeType -> Bool
$c/= :: DGEdgeType -> DGEdgeType -> Bool
== :: DGEdgeType -> DGEdgeType -> Bool
$c== :: DGEdgeType -> DGEdgeType -> Bool
Eq, Eq DGEdgeType
Eq DGEdgeType =>
(DGEdgeType -> DGEdgeType -> Ordering)
-> (DGEdgeType -> DGEdgeType -> Bool)
-> (DGEdgeType -> DGEdgeType -> Bool)
-> (DGEdgeType -> DGEdgeType -> Bool)
-> (DGEdgeType -> DGEdgeType -> Bool)
-> (DGEdgeType -> DGEdgeType -> DGEdgeType)
-> (DGEdgeType -> DGEdgeType -> DGEdgeType)
-> Ord DGEdgeType
DGEdgeType -> DGEdgeType -> Bool
DGEdgeType -> DGEdgeType -> Ordering
DGEdgeType -> DGEdgeType -> DGEdgeType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DGEdgeType -> DGEdgeType -> DGEdgeType
$cmin :: DGEdgeType -> DGEdgeType -> DGEdgeType
max :: DGEdgeType -> DGEdgeType -> DGEdgeType
$cmax :: DGEdgeType -> DGEdgeType -> DGEdgeType
>= :: DGEdgeType -> DGEdgeType -> Bool
$c>= :: DGEdgeType -> DGEdgeType -> Bool
> :: DGEdgeType -> DGEdgeType -> Bool
$c> :: DGEdgeType -> DGEdgeType -> Bool
<= :: DGEdgeType -> DGEdgeType -> Bool
$c<= :: DGEdgeType -> DGEdgeType -> Bool
< :: DGEdgeType -> DGEdgeType -> Bool
$c< :: DGEdgeType -> DGEdgeType -> Bool
compare :: DGEdgeType -> DGEdgeType -> Ordering
$ccompare :: DGEdgeType -> DGEdgeType -> Ordering
$cp1Ord :: Eq DGEdgeType
Ord, Typeable, Typeable DGEdgeType
Constr
DataType
Typeable DGEdgeType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DGEdgeType)
-> (DGEdgeType -> Constr)
-> (DGEdgeType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DGEdgeType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DGEdgeType))
-> ((forall b. Data b => b -> b) -> DGEdgeType -> DGEdgeType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r)
-> (forall u. (forall d. Data d => d -> u) -> DGEdgeType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DGEdgeType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType)
-> Data DGEdgeType
DGEdgeType -> Constr
DGEdgeType -> DataType
(forall b. Data b => b -> b) -> DGEdgeType -> DGEdgeType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeType
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DGEdgeType -> u
forall u. (forall d. Data d => d -> u) -> DGEdgeType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGEdgeType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGEdgeType)
$cDGEdgeType :: Constr
$tDGEdgeType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
gmapMp :: (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
gmapM :: (forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DGEdgeType -> m DGEdgeType
gmapQi :: Int -> (forall d. Data d => d -> u) -> DGEdgeType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DGEdgeType -> u
gmapQ :: (forall d. Data d => d -> u) -> DGEdgeType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DGEdgeType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeType -> r
gmapT :: (forall b. Data b => b -> b) -> DGEdgeType -> DGEdgeType
$cgmapT :: (forall b. Data b => b -> b) -> DGEdgeType -> DGEdgeType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGEdgeType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DGEdgeType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DGEdgeType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGEdgeType)
dataTypeOf :: DGEdgeType -> DataType
$cdataTypeOf :: DGEdgeType -> DataType
toConstr :: DGEdgeType -> Constr
$ctoConstr :: DGEdgeType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeType -> c DGEdgeType
$cp1Data :: Typeable DGEdgeType
Data)

data DGEdgeTypeModInc =
    GlobalDef
  | HetDef
  | HidingDef
  | LocalDef
  | FreeOrCofreeDef FreeOrCofree
  | ThmType { DGEdgeTypeModInc -> ThmTypes
thmEdgeType :: ThmTypes
            , DGEdgeTypeModInc -> Bool
isProvenEdge :: Bool
            , DGEdgeTypeModInc -> Bool
isConservativ :: Bool
            , DGEdgeTypeModInc -> Bool
isPending :: Bool }
  deriving (Int -> DGEdgeTypeModInc -> ShowS
[DGEdgeTypeModInc] -> ShowS
DGEdgeTypeModInc -> String
(Int -> DGEdgeTypeModInc -> ShowS)
-> (DGEdgeTypeModInc -> String)
-> ([DGEdgeTypeModInc] -> ShowS)
-> Show DGEdgeTypeModInc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DGEdgeTypeModInc] -> ShowS
$cshowList :: [DGEdgeTypeModInc] -> ShowS
show :: DGEdgeTypeModInc -> String
$cshow :: DGEdgeTypeModInc -> String
showsPrec :: Int -> DGEdgeTypeModInc -> ShowS
$cshowsPrec :: Int -> DGEdgeTypeModInc -> ShowS
Show, DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
(DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> Eq DGEdgeTypeModInc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c/= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
== :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c== :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
Eq, Eq DGEdgeTypeModInc
Eq DGEdgeTypeModInc =>
(DGEdgeTypeModInc -> DGEdgeTypeModInc -> Ordering)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc)
-> (DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc)
-> Ord DGEdgeTypeModInc
DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
DGEdgeTypeModInc -> DGEdgeTypeModInc -> Ordering
DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
$cmin :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
max :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
$cmax :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> DGEdgeTypeModInc
>= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c>= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
> :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c> :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
<= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c<= :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
< :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
$c< :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Bool
compare :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Ordering
$ccompare :: DGEdgeTypeModInc -> DGEdgeTypeModInc -> Ordering
$cp1Ord :: Eq DGEdgeTypeModInc
Ord, Typeable, Typeable DGEdgeTypeModInc
Constr
DataType
Typeable DGEdgeTypeModInc =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc)
-> (DGEdgeTypeModInc -> Constr)
-> (DGEdgeTypeModInc -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DGEdgeTypeModInc))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DGEdgeTypeModInc))
-> ((forall b. Data b => b -> b)
    -> DGEdgeTypeModInc -> DGEdgeTypeModInc)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DGEdgeTypeModInc -> m DGEdgeTypeModInc)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DGEdgeTypeModInc -> m DGEdgeTypeModInc)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DGEdgeTypeModInc -> m DGEdgeTypeModInc)
-> Data DGEdgeTypeModInc
DGEdgeTypeModInc -> Constr
DGEdgeTypeModInc -> DataType
(forall b. Data b => b -> b)
-> DGEdgeTypeModInc -> DGEdgeTypeModInc
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> u
forall u. (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGEdgeTypeModInc)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DGEdgeTypeModInc)
$cThmType :: Constr
$cFreeOrCofreeDef :: Constr
$cLocalDef :: Constr
$cHidingDef :: Constr
$cHetDef :: Constr
$cGlobalDef :: Constr
$tDGEdgeTypeModInc :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
gmapMp :: (forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
gmapM :: (forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DGEdgeTypeModInc -> m DGEdgeTypeModInc
gmapQi :: Int -> (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> u
gmapQ :: (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DGEdgeTypeModInc -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DGEdgeTypeModInc -> r
gmapT :: (forall b. Data b => b -> b)
-> DGEdgeTypeModInc -> DGEdgeTypeModInc
$cgmapT :: (forall b. Data b => b -> b)
-> DGEdgeTypeModInc -> DGEdgeTypeModInc
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DGEdgeTypeModInc)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DGEdgeTypeModInc)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DGEdgeTypeModInc)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DGEdgeTypeModInc)
dataTypeOf :: DGEdgeTypeModInc -> DataType
$cdataTypeOf :: DGEdgeTypeModInc -> DataType
toConstr :: DGEdgeTypeModInc -> Constr
$ctoConstr :: DGEdgeTypeModInc -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DGEdgeTypeModInc
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DGEdgeTypeModInc -> c DGEdgeTypeModInc
$cp1Data :: Typeable DGEdgeTypeModInc
Data)

data ThmTypes =
    HidingThm
  | FreeOrCofreeThm FreeOrCofree
  | GlobalOrLocalThm { ThmTypes -> Scope
thmScope :: Scope
                     , ThmTypes -> Bool
isHomThm :: Bool }
  deriving (Int -> ThmTypes -> ShowS
[ThmTypes] -> ShowS
ThmTypes -> String
(Int -> ThmTypes -> ShowS)
-> (ThmTypes -> String) -> ([ThmTypes] -> ShowS) -> Show ThmTypes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThmTypes] -> ShowS
$cshowList :: [ThmTypes] -> ShowS
show :: ThmTypes -> String
$cshow :: ThmTypes -> String
showsPrec :: Int -> ThmTypes -> ShowS
$cshowsPrec :: Int -> ThmTypes -> ShowS
Show, ThmTypes -> ThmTypes -> Bool
(ThmTypes -> ThmTypes -> Bool)
-> (ThmTypes -> ThmTypes -> Bool) -> Eq ThmTypes
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThmTypes -> ThmTypes -> Bool
$c/= :: ThmTypes -> ThmTypes -> Bool
== :: ThmTypes -> ThmTypes -> Bool
$c== :: ThmTypes -> ThmTypes -> Bool
Eq, Eq ThmTypes
Eq ThmTypes =>
(ThmTypes -> ThmTypes -> Ordering)
-> (ThmTypes -> ThmTypes -> Bool)
-> (ThmTypes -> ThmTypes -> Bool)
-> (ThmTypes -> ThmTypes -> Bool)
-> (ThmTypes -> ThmTypes -> Bool)
-> (ThmTypes -> ThmTypes -> ThmTypes)
-> (ThmTypes -> ThmTypes -> ThmTypes)
-> Ord ThmTypes
ThmTypes -> ThmTypes -> Bool
ThmTypes -> ThmTypes -> Ordering
ThmTypes -> ThmTypes -> ThmTypes
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ThmTypes -> ThmTypes -> ThmTypes
$cmin :: ThmTypes -> ThmTypes -> ThmTypes
max :: ThmTypes -> ThmTypes -> ThmTypes
$cmax :: ThmTypes -> ThmTypes -> ThmTypes
>= :: ThmTypes -> ThmTypes -> Bool
$c>= :: ThmTypes -> ThmTypes -> Bool
> :: ThmTypes -> ThmTypes -> Bool
$c> :: ThmTypes -> ThmTypes -> Bool
<= :: ThmTypes -> ThmTypes -> Bool
$c<= :: ThmTypes -> ThmTypes -> Bool
< :: ThmTypes -> ThmTypes -> Bool
$c< :: ThmTypes -> ThmTypes -> Bool
compare :: ThmTypes -> ThmTypes -> Ordering
$ccompare :: ThmTypes -> ThmTypes -> Ordering
$cp1Ord :: Eq ThmTypes
Ord, Typeable, Typeable ThmTypes
Constr
DataType
Typeable ThmTypes =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ThmTypes -> c ThmTypes)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ThmTypes)
-> (ThmTypes -> Constr)
-> (ThmTypes -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ThmTypes))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmTypes))
-> ((forall b. Data b => b -> b) -> ThmTypes -> ThmTypes)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ThmTypes -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ThmTypes -> r)
-> (forall u. (forall d. Data d => d -> u) -> ThmTypes -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ThmTypes -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes)
-> Data ThmTypes
ThmTypes -> Constr
ThmTypes -> DataType
(forall b. Data b => b -> b) -> ThmTypes -> ThmTypes
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmTypes -> c ThmTypes
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmTypes
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ThmTypes -> u
forall u. (forall d. Data d => d -> u) -> ThmTypes -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmTypes
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmTypes -> c ThmTypes
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ThmTypes)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmTypes)
$cGlobalOrLocalThm :: Constr
$cFreeOrCofreeThm :: Constr
$cHidingThm :: Constr
$tThmTypes :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
gmapMp :: (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
gmapM :: (forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ThmTypes -> m ThmTypes
gmapQi :: Int -> (forall d. Data d => d -> u) -> ThmTypes -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ThmTypes -> u
gmapQ :: (forall d. Data d => d -> u) -> ThmTypes -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ThmTypes -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ThmTypes -> r
gmapT :: (forall b. Data b => b -> b) -> ThmTypes -> ThmTypes
$cgmapT :: (forall b. Data b => b -> b) -> ThmTypes -> ThmTypes
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmTypes)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ThmTypes)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ThmTypes)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ThmTypes)
dataTypeOf :: ThmTypes -> DataType
$cdataTypeOf :: ThmTypes -> DataType
toConstr :: ThmTypes -> Constr
$ctoConstr :: ThmTypes -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmTypes
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ThmTypes
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmTypes -> c ThmTypes
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ThmTypes -> c ThmTypes
$cp1Data :: Typeable ThmTypes
Data)

-- | Creates a list with all DGEdgeType types
listDGEdgeTypes :: [DGEdgeType]
listDGEdgeTypes :: [DGEdgeType]
listDGEdgeTypes =
  [ DGEdgeType :: DGEdgeTypeModInc -> Bool -> DGEdgeType
DGEdgeType { edgeTypeModInc :: DGEdgeTypeModInc
edgeTypeModInc = DGEdgeTypeModInc
modinc
               , isInc :: Bool
isInc = Bool
isInclusion' }
  | DGEdgeTypeModInc
modinc <-
    [ DGEdgeTypeModInc
GlobalDef
    , DGEdgeTypeModInc
HetDef
    , DGEdgeTypeModInc
HidingDef
    , DGEdgeTypeModInc
LocalDef
    ] [DGEdgeTypeModInc] -> [DGEdgeTypeModInc] -> [DGEdgeTypeModInc]
forall a. [a] -> [a] -> [a]
++ [ FreeOrCofree -> DGEdgeTypeModInc
FreeOrCofreeDef FreeOrCofree
fc | FreeOrCofree
fc <- [FreeOrCofree]
fcList ] [DGEdgeTypeModInc] -> [DGEdgeTypeModInc] -> [DGEdgeTypeModInc]
forall a. [a] -> [a] -> [a]
++
      [ ThmType :: ThmTypes -> Bool -> Bool -> Bool -> DGEdgeTypeModInc
ThmType { thmEdgeType :: ThmTypes
thmEdgeType = ThmTypes
thmType
                , isProvenEdge :: Bool
isProvenEdge = Bool
proven
                , isConservativ :: Bool
isConservativ = Bool
cons
                , isPending :: Bool
isPending = Bool
pending }
      | ThmTypes
thmType <- ThmTypes
HidingThm
        ThmTypes -> [ThmTypes] -> [ThmTypes]
forall a. a -> [a] -> [a]
: [ FreeOrCofree -> ThmTypes
FreeOrCofreeThm FreeOrCofree
fc | FreeOrCofree
fc <- [FreeOrCofree]
fcList ] [ThmTypes] -> [ThmTypes] -> [ThmTypes]
forall a. [a] -> [a] -> [a]
++
          [ GlobalOrLocalThm :: Scope -> Bool -> ThmTypes
GlobalOrLocalThm { thmScope :: Scope
thmScope = Scope
scope
                             , isHomThm :: Bool
isHomThm = Bool
hom }
          | Scope
scope <- [Scope
Local, Scope
Global]
          , Bool
hom <- [Bool
True, Bool
False]
          ]
      , Bool
proven <- [Bool
True, Bool
False]
      , Bool
cons <- [Bool
True, Bool
False]
      , Bool
pending <- [Bool
True, Bool
False]
      ]
  , Bool
isInclusion' <- [Bool
True, Bool
False]
  ]

-- | check an EdgeType and see if its a definition link
isDefEdgeType :: DGEdgeType -> Bool
isDefEdgeType :: DGEdgeType -> Bool
isDefEdgeType edgeTp :: DGEdgeType
edgeTp = case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
edgeTp of
    ThmType {} -> Bool
False
    _ -> Bool
True


-- * datatypes for storing the nodes of the ref tree in the global env

data RTPointer =
   RTNone
 | NPUnit Int
 | NPBranch Int (Map.Map IRI RTPointer)
        -- here the leaves can be either NPUnit or NPComp
 | NPRef Int Int
 | NPComp (Map.Map IRI RTPointer)
         {- here the leaves can be NPUnit or NPComp
         and roots are needed for inserting edges -}
 deriving (Int -> RTPointer -> ShowS
[RTPointer] -> ShowS
RTPointer -> String
(Int -> RTPointer -> ShowS)
-> (RTPointer -> String)
-> ([RTPointer] -> ShowS)
-> Show RTPointer
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTPointer] -> ShowS
$cshowList :: [RTPointer] -> ShowS
show :: RTPointer -> String
$cshow :: RTPointer -> String
showsPrec :: Int -> RTPointer -> ShowS
$cshowsPrec :: Int -> RTPointer -> ShowS
Show, RTPointer -> RTPointer -> Bool
(RTPointer -> RTPointer -> Bool)
-> (RTPointer -> RTPointer -> Bool) -> Eq RTPointer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RTPointer -> RTPointer -> Bool
$c/= :: RTPointer -> RTPointer -> Bool
== :: RTPointer -> RTPointer -> Bool
$c== :: RTPointer -> RTPointer -> Bool
Eq, Eq RTPointer
Eq RTPointer =>
(RTPointer -> RTPointer -> Ordering)
-> (RTPointer -> RTPointer -> Bool)
-> (RTPointer -> RTPointer -> Bool)
-> (RTPointer -> RTPointer -> Bool)
-> (RTPointer -> RTPointer -> Bool)
-> (RTPointer -> RTPointer -> RTPointer)
-> (RTPointer -> RTPointer -> RTPointer)
-> Ord RTPointer
RTPointer -> RTPointer -> Bool
RTPointer -> RTPointer -> Ordering
RTPointer -> RTPointer -> RTPointer
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RTPointer -> RTPointer -> RTPointer
$cmin :: RTPointer -> RTPointer -> RTPointer
max :: RTPointer -> RTPointer -> RTPointer
$cmax :: RTPointer -> RTPointer -> RTPointer
>= :: RTPointer -> RTPointer -> Bool
$c>= :: RTPointer -> RTPointer -> Bool
> :: RTPointer -> RTPointer -> Bool
$c> :: RTPointer -> RTPointer -> Bool
<= :: RTPointer -> RTPointer -> Bool
$c<= :: RTPointer -> RTPointer -> Bool
< :: RTPointer -> RTPointer -> Bool
$c< :: RTPointer -> RTPointer -> Bool
compare :: RTPointer -> RTPointer -> Ordering
$ccompare :: RTPointer -> RTPointer -> Ordering
$cp1Ord :: Eq RTPointer
Ord, Typeable, Typeable RTPointer
Constr
DataType
Typeable RTPointer =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RTPointer -> c RTPointer)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RTPointer)
-> (RTPointer -> Constr)
-> (RTPointer -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RTPointer))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTPointer))
-> ((forall b. Data b => b -> b) -> RTPointer -> RTPointer)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RTPointer -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RTPointer -> r)
-> (forall u. (forall d. Data d => d -> u) -> RTPointer -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RTPointer -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer)
-> Data RTPointer
RTPointer -> Constr
RTPointer -> DataType
(forall b. Data b => b -> b) -> RTPointer -> RTPointer
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTPointer -> c RTPointer
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTPointer
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RTPointer -> u
forall u. (forall d. Data d => d -> u) -> RTPointer -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTPointer
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTPointer -> c RTPointer
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RTPointer)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTPointer)
$cNPComp :: Constr
$cNPRef :: Constr
$cNPBranch :: Constr
$cNPUnit :: Constr
$cRTNone :: Constr
$tRTPointer :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
gmapMp :: (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
gmapM :: (forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RTPointer -> m RTPointer
gmapQi :: Int -> (forall d. Data d => d -> u) -> RTPointer -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RTPointer -> u
gmapQ :: (forall d. Data d => d -> u) -> RTPointer -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RTPointer -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTPointer -> r
gmapT :: (forall b. Data b => b -> b) -> RTPointer -> RTPointer
$cgmapT :: (forall b. Data b => b -> b) -> RTPointer -> RTPointer
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTPointer)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTPointer)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RTPointer)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RTPointer)
dataTypeOf :: RTPointer -> DataType
$cdataTypeOf :: RTPointer -> DataType
toConstr :: RTPointer -> Constr
$ctoConstr :: RTPointer -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTPointer
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTPointer
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTPointer -> c RTPointer
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTPointer -> c RTPointer
$cp1Data :: Typeable RTPointer
Data)

-- map nodes

mapRTNodes :: Map.Map Int Int -> RTPointer -> RTPointer
mapRTNodes :: Map Int Int -> RTPointer -> RTPointer
mapRTNodes f :: Map Int Int
f rtp :: RTPointer
rtp = let app :: Map Int c -> Int -> c
app = (Int -> Map Int c -> c) -> Map Int c -> Int -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Int -> Map Int c -> c) -> Map Int c -> Int -> c)
-> (Int -> Map Int c -> c) -> Map Int c -> Int -> c
forall a b. (a -> b) -> a -> b
$ c -> Int -> Map Int c -> c
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> c
forall a. HasCallStack => String -> a
error "mapRTNodes")
  in case RTPointer
rtp of
  RTNone -> RTPointer
RTNone
  NPUnit x :: Int
x -> Int -> RTPointer
NPUnit (Map Int Int -> Int -> Int
forall c. Map Int c -> Int -> c
app Map Int Int
f Int
x)
  NPRef x :: Int
x y :: Int
y -> Int -> Int -> RTPointer
NPRef (Map Int Int -> Int -> Int
forall c. Map Int c -> Int -> c
app Map Int Int
f Int
x) (Map Int Int -> Int -> Int
forall c. Map Int c -> Int -> c
app Map Int Int
f Int
y)
  NPBranch x :: Int
x g :: Map IRI RTPointer
g -> Int -> Map IRI RTPointer -> RTPointer
NPBranch (Map Int Int -> Int -> Int
forall c. Map Int c -> Int -> c
app Map Int Int
f Int
x) ((RTPointer -> RTPointer) -> Map IRI RTPointer -> Map IRI RTPointer
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Int Int -> RTPointer -> RTPointer
mapRTNodes Map Int Int
f) Map IRI RTPointer
g)
  NPComp g :: Map IRI RTPointer
g -> Map IRI RTPointer -> RTPointer
NPComp ((RTPointer -> RTPointer) -> Map IRI RTPointer -> Map IRI RTPointer
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Int Int -> RTPointer -> RTPointer
mapRTNodes Map Int Int
f) Map IRI RTPointer
g)

-- compositions

compPointer :: RTPointer -> RTPointer -> RTPointer
compPointer :: RTPointer -> RTPointer -> RTPointer
compPointer (NPUnit n1 :: Int
n1) (NPUnit n2 :: Int
n2) = Int -> Int -> RTPointer
NPRef Int
n1 Int
n2
compPointer (NPUnit n1 :: Int
n1) (NPBranch _ f :: Map IRI RTPointer
f) = Int -> Map IRI RTPointer -> RTPointer
NPBranch Int
n1 Map IRI RTPointer
f
compPointer (NPUnit n1 :: Int
n1) (NPRef _ n2 :: Int
n2) = Int -> Int -> RTPointer
NPRef Int
n1 Int
n2
compPointer (NPRef n1 :: Int
n1 _) (NPRef _ n2 :: Int
n2) = Int -> Int -> RTPointer
NPRef Int
n1 Int
n2
compPointer (NPRef n1 :: Int
n1 _) (NPBranch _ f :: Map IRI RTPointer
f) = Int -> Map IRI RTPointer -> RTPointer
NPBranch Int
n1 Map IRI RTPointer
f
compPointer (NPBranch n1 :: Int
n1 f1 :: Map IRI RTPointer
f1) (NPComp f2 :: Map IRI RTPointer
f2) =
       Int -> Map IRI RTPointer -> RTPointer
NPBranch Int
n1 ((RTPointer -> RTPointer -> RTPointer)
-> Map IRI RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (\ _ y :: RTPointer
y -> RTPointer
y) Map IRI RTPointer
f1 Map IRI RTPointer
f2 )
compPointer (NPComp f1 :: Map IRI RTPointer
f1) (NPComp f2 :: Map IRI RTPointer
f2) =
       Map IRI RTPointer -> RTPointer
NPComp ((RTPointer -> RTPointer -> RTPointer)
-> Map IRI RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (\ _ y :: RTPointer
y -> RTPointer
y) Map IRI RTPointer
f1 Map IRI RTPointer
f2)
compPointer x :: RTPointer
x y :: RTPointer
y = String -> RTPointer
forall a. HasCallStack => String -> a
error (String -> RTPointer) -> String -> RTPointer
forall a b. (a -> b) -> a -> b
$ "compPointer:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RTPointer -> String
forall a. Show a => a -> String
show RTPointer
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ " composed with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RTPointer -> String
forall a. Show a => a -> String
show RTPointer
y

-- sources

refSource :: RTPointer -> Int
refSource :: RTPointer -> Int
refSource (NPUnit n :: Int
n) = Int
n
refSource (NPBranch n :: Int
n _) = Int
n
refSource (NPRef n :: Int
n _) = Int
n
refSource x :: RTPointer
x = String -> Int
forall a. HasCallStack => String -> a
error ("refSource:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RTPointer -> String
forall a. Show a => a -> String
show RTPointer
x)

data RTLeaves = RTLeaf Int | RTLeaves (Map.Map IRI RTLeaves)
 deriving (Int -> RTLeaves -> ShowS
[RTLeaves] -> ShowS
RTLeaves -> String
(Int -> RTLeaves -> ShowS)
-> (RTLeaves -> String) -> ([RTLeaves] -> ShowS) -> Show RTLeaves
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTLeaves] -> ShowS
$cshowList :: [RTLeaves] -> ShowS
show :: RTLeaves -> String
$cshow :: RTLeaves -> String
showsPrec :: Int -> RTLeaves -> ShowS
$cshowsPrec :: Int -> RTLeaves -> ShowS
Show, Typeable, Typeable RTLeaves
Constr
DataType
Typeable RTLeaves =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RTLeaves -> c RTLeaves)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RTLeaves)
-> (RTLeaves -> Constr)
-> (RTLeaves -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RTLeaves))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTLeaves))
-> ((forall b. Data b => b -> b) -> RTLeaves -> RTLeaves)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RTLeaves -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RTLeaves -> r)
-> (forall u. (forall d. Data d => d -> u) -> RTLeaves -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> RTLeaves -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves)
-> Data RTLeaves
RTLeaves -> Constr
RTLeaves -> DataType
(forall b. Data b => b -> b) -> RTLeaves -> RTLeaves
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTLeaves -> c RTLeaves
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTLeaves
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RTLeaves -> u
forall u. (forall d. Data d => d -> u) -> RTLeaves -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTLeaves
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTLeaves -> c RTLeaves
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RTLeaves)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTLeaves)
$cRTLeaves :: Constr
$cRTLeaf :: Constr
$tRTLeaves :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
gmapMp :: (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
gmapM :: (forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RTLeaves -> m RTLeaves
gmapQi :: Int -> (forall d. Data d => d -> u) -> RTLeaves -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RTLeaves -> u
gmapQ :: (forall d. Data d => d -> u) -> RTLeaves -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RTLeaves -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RTLeaves -> r
gmapT :: (forall b. Data b => b -> b) -> RTLeaves -> RTLeaves
$cgmapT :: (forall b. Data b => b -> b) -> RTLeaves -> RTLeaves
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTLeaves)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RTLeaves)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RTLeaves)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RTLeaves)
dataTypeOf :: RTLeaves -> DataType
$cdataTypeOf :: RTLeaves -> DataType
toConstr :: RTLeaves -> Constr
$ctoConstr :: RTLeaves -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTLeaves
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RTLeaves
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTLeaves -> c RTLeaves
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RTLeaves -> c RTLeaves
$cp1Data :: Typeable RTLeaves
Data)

refTarget :: RTPointer -> RTLeaves
refTarget :: RTPointer -> RTLeaves
refTarget (NPUnit n :: Int
n) = Int -> RTLeaves
RTLeaf Int
n
refTarget (NPRef _ n :: Int
n) = Int -> RTLeaves
RTLeaf Int
n
refTarget (NPComp f :: Map IRI RTPointer
f) = Map IRI RTLeaves -> RTLeaves
RTLeaves (Map IRI RTLeaves -> RTLeaves) -> Map IRI RTLeaves -> RTLeaves
forall a b. (a -> b) -> a -> b
$ (RTPointer -> RTLeaves) -> Map IRI RTPointer -> Map IRI RTLeaves
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map RTPointer -> RTLeaves
refTarget Map IRI RTPointer
f
refTarget (NPBranch _ f :: Map IRI RTPointer
f) = Map IRI RTLeaves -> RTLeaves
RTLeaves (Map IRI RTLeaves -> RTLeaves) -> Map IRI RTLeaves -> RTLeaves
forall a b. (a -> b) -> a -> b
$ (RTPointer -> RTLeaves) -> Map IRI RTPointer -> Map IRI RTLeaves
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map RTPointer -> RTLeaves
refTarget Map IRI RTPointer
f
refTarget x :: RTPointer
x = String -> RTLeaves
forall a. HasCallStack => String -> a
error ("refTarget:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RTPointer -> String
forall a. Show a => a -> String
show RTPointer
x)

-- ** for node names

emptyNodeName :: NodeName
emptyNodeName :: NodeName
emptyNodeName = IRI -> String -> Int -> [XPathPart] -> Range -> NodeName
NodeName IRI
nullIRI "" 0 [] Range
nullRange

showExt :: NodeName -> String
showExt :: NodeName -> String
showExt n :: NodeName
n = let i :: Int
i = NodeName -> Int
extIndex NodeName
n in NodeName -> String
extString NodeName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then "" else Int -> String
forall a. Show a => a -> String
show Int
i

showName :: NodeName -> String
showName :: NodeName -> String
showName n :: NodeName
n = let ext :: String
ext = NodeName -> String
showExt NodeName
n in
    IRI -> String
iriToStringShortUnsecure (Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ NodeName -> IRI
getName NodeName
n)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
ext then String
ext else "__" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ext

makeRgName :: IRI -> Range -> NodeName
makeRgName :: IRI -> Range -> NodeName
makeRgName n :: IRI
n = IRI -> String -> Int -> [XPathPart] -> Range -> NodeName
NodeName IRI
n "" 0 [String -> XPathPart
ElemName (String -> XPathPart) -> String -> XPathPart
forall a b. (a -> b) -> a -> b
$ IRI -> String
iriToStringShortUnsecure IRI
n]

makeName :: IRI -> NodeName
makeName :: IRI -> NodeName
makeName n :: IRI
n = IRI -> Range -> NodeName
makeRgName IRI
n (Range -> NodeName) -> Range -> NodeName
forall a b. (a -> b) -> a -> b
$ IRI -> Range
iriPos IRI
n

setSrcRange :: Range -> NodeName -> NodeName
setSrcRange :: Range -> NodeName -> NodeName
setSrcRange r :: Range
r n :: NodeName
n = NodeName
n { srcRange :: Range
srcRange = Range
r }

parseNodeName :: String -> NodeName
parseNodeName :: String -> NodeName
parseNodeName s :: String
s =
  let err :: String -> a
err msg :: String
msg = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "parseNodeName: malformed NodeName" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
      mkName :: String -> NodeName
mkName = IRI -> NodeName
makeName (IRI -> NodeName) -> (String -> IRI) -> String -> NodeName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe (String -> IRI
forall a. String -> a
err ": ") (Maybe IRI -> IRI) -> (String -> Maybe IRI) -> String -> IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe IRI
parseCurie
  in case String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitByList "__" String
s of
    [i :: String
i] -> String -> NodeName
mkName String
i
    [i :: String
i, e :: String
e] ->
        let n :: NodeName
n = String -> NodeName
mkName String
i
            mSf :: Maybe (String, Int)
mSf = String -> Maybe (String, Int)
numberSuffix String
e
            (es :: String
es, sf :: Int
sf) = (String, Int) -> Maybe (String, Int) -> (String, Int)
forall a. a -> Maybe a -> a
fromMaybe (String
e, 0) Maybe (String, Int)
mSf
        in NodeName
n { extString :: String
extString = String
es
             , extIndex :: Int
extIndex = Int
sf }
    _ -> String -> NodeName
forall a. String -> a
err ", too many __: "

incBy :: Int -> NodeName -> NodeName
incBy :: Int -> NodeName -> NodeName
incBy i :: Int
i n :: NodeName
n = NodeName
n
  { extIndex :: Int
extIndex = NodeName -> Int
extIndex NodeName
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
  , xpath :: [XPathPart]
xpath = case NodeName -> [XPathPart]
xpath NodeName
n of
              ChildIndex j :: Int
j : r :: [XPathPart]
r -> Int -> XPathPart
ChildIndex (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) XPathPart -> [XPathPart] -> [XPathPart]
forall a. a -> [a] -> [a]
: [XPathPart]
r
              l :: [XPathPart]
l -> Int -> XPathPart
ChildIndex Int
i XPathPart -> [XPathPart] -> [XPathPart]
forall a. a -> [a] -> [a]
: [XPathPart]
l }

inc :: NodeName -> NodeName
inc :: NodeName -> NodeName
inc = Int -> NodeName -> NodeName
incBy 1

extName :: String -> NodeName -> NodeName
extName :: String -> NodeName -> NodeName
extName s :: String
s n :: NodeName
n = NodeName
n
  { extString :: String
extString = NodeName -> String
showExt NodeName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take 1 String
s
  , extIndex :: Int
extIndex = 0
  , xpath :: [XPathPart]
xpath = String -> XPathPart
ElemName String
s XPathPart -> [XPathPart] -> [XPathPart]
forall a. a -> [a] -> [a]
: NodeName -> [XPathPart]
xpath NodeName
n }

-- ** handle edge numbers and proof bases

-- | create a default ID which has to be changed when inserting a certain edge.
defaultEdgeId :: EdgeId
defaultEdgeId :: EdgeId
defaultEdgeId = Int -> EdgeId
EdgeId (Int -> EdgeId) -> Int -> EdgeId
forall a b. (a -> b) -> a -> b
$ -1

emptyProofBasis :: ProofBasis
emptyProofBasis :: ProofBasis
emptyProofBasis = Set EdgeId -> ProofBasis
ProofBasis Set EdgeId
forall a. Set a
Set.empty

nullProofBasis :: ProofBasis -> Bool
nullProofBasis :: ProofBasis -> Bool
nullProofBasis = Set EdgeId -> Bool
forall a. Set a -> Bool
Set.null (Set EdgeId -> Bool)
-> (ProofBasis -> Set EdgeId) -> ProofBasis -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofBasis -> Set EdgeId
proofBasis

addEdgeId :: ProofBasis -> EdgeId -> ProofBasis
addEdgeId :: ProofBasis -> EdgeId -> ProofBasis
addEdgeId (ProofBasis s :: Set EdgeId
s) e :: EdgeId
e = Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis) -> Set EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert EdgeId
e Set EdgeId
s

delEdgeId :: ProofBasis -> EdgeId -> ProofBasis
delEdgeId :: ProofBasis -> EdgeId -> ProofBasis
delEdgeId (ProofBasis s :: Set EdgeId
s) e :: EdgeId
e = Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis) -> Set EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.delete EdgeId
e Set EdgeId
s

updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
updEdgeId pb :: ProofBasis
pb = ProofBasis -> EdgeId -> ProofBasis
addEdgeId (ProofBasis -> EdgeId -> ProofBasis)
-> (EdgeId -> ProofBasis) -> EdgeId -> EdgeId -> ProofBasis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofBasis -> EdgeId -> ProofBasis
delEdgeId ProofBasis
pb

-- | checks if the given edge is contained in the given proof basis..
edgeInProofBasis :: EdgeId -> ProofBasis -> Bool
edgeInProofBasis :: EdgeId -> ProofBasis -> Bool
edgeInProofBasis e :: EdgeId
e = EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
e (Set EdgeId -> Bool)
-> (ProofBasis -> Set EdgeId) -> ProofBasis -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofBasis -> Set EdgeId
proofBasis

-- * utilities

topsortedLibsWithImports :: Rel.Rel LibName -> [LibName]
topsortedLibsWithImports :: Rel LibName -> [LibName]
topsortedLibsWithImports = (Set LibName -> [LibName]) -> [Set LibName] -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Set LibName -> [LibName]
forall a. Set a -> [a]
Set.toList ([Set LibName] -> [LibName])
-> (Rel LibName -> [Set LibName]) -> Rel LibName -> [LibName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel LibName -> [Set LibName]
forall a. Ord a => Rel a -> [Set a]
Rel.topSort

getMapAndMaxIndex :: Ord k => k -> (b -> Map.Map k a) -> b -> (Map.Map k a, k)
getMapAndMaxIndex :: k -> (b -> Map k a) -> b -> (Map k a, k)
getMapAndMaxIndex c :: k
c f :: b -> Map k a
f gctx :: b
gctx =
    let m :: Map k a
m = b -> Map k a
f b
gctx in (Map k a
m, if Map k a -> Bool
forall k a. Map k a -> Bool
Map.null Map k a
m then k
c else (k, a) -> k
forall a b. (a, b) -> a
fst ((k, a) -> k) -> (k, a) -> k
forall a b. (a -> b) -> a -> b
$ Map k a -> (k, a)
forall k a. Map k a -> (k, a)
Map.findMax Map k a
m)

-- | or two predicates
liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr f :: a -> Bool
f g :: a -> Bool
g x :: a
x = a -> Bool
f a
x Bool -> Bool -> Bool
|| a -> Bool
g a
x