{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./QBF/AS_BASIC_QBF.der.hs
Description :  Abstract syntax for propositional logic extended with QBFs
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <jonathan.von_schroeder@dfki.de>
Stability   :  experimental
Portability :  portable

Definition of abstract syntax for propositional logic extended with QBFs

  Ref.
  <http://en.wikipedia.org/wiki/Propositional_logic>
  <http://www.voronkov.com/lics.cgi>
-}

module QBF.AS_BASIC_QBF
    ( FORMULA (..)             -- datatype for Propositional Formulas
    , BASICITEMS (..)          -- Items of a Basic Spec
    , BASICSPEC (..)           -- Basic Spec
    , SYMBITEMS (..)           -- List of symbols
    , SYMB (..)                -- Symbols
    , SYMBMAPITEMS (..)        -- Symbol map
    , SYMBORMAP (..)           -- Symbol or symbol map
    , PREDITEM (..)            -- Predicates
    , isPrimForm
    , ID (..)
    ) where

import Common.Id as Id
import Common.Doc
import Common.DocUtils
import Common.Keywords
import Common.AS_Annotation as AS_Anno

import Data.Data
import Data.Maybe (isJust)
import qualified Data.List as List

-- DrIFT command
{-! global: GetRange !-}

-- | predicates = propositions
data PREDITEM = PredItem [Id.Token] Id.Range
               deriving (Int -> PREDITEM -> ShowS
[PREDITEM] -> ShowS
PREDITEM -> String
(Int -> PREDITEM -> ShowS)
-> (PREDITEM -> String) -> ([PREDITEM] -> ShowS) -> Show PREDITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PREDITEM] -> ShowS
$cshowList :: [PREDITEM] -> ShowS
show :: PREDITEM -> String
$cshow :: PREDITEM -> String
showsPrec :: Int -> PREDITEM -> ShowS
$cshowsPrec :: Int -> PREDITEM -> ShowS
Show, Typeable, Typeable PREDITEM
Constr
DataType
Typeable PREDITEM =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PREDITEM -> c PREDITEM)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PREDITEM)
-> (PREDITEM -> Constr)
-> (PREDITEM -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PREDITEM))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM))
-> ((forall b. Data b => b -> b) -> PREDITEM -> PREDITEM)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r)
-> (forall u. (forall d. Data d => d -> u) -> PREDITEM -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PREDITEM -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM)
-> Data PREDITEM
PREDITEM -> Constr
PREDITEM -> DataType
(forall b. Data b => b -> b) -> PREDITEM -> PREDITEM
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PREDITEM -> c PREDITEM
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PREDITEM
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) -> PREDITEM -> u
forall u. (forall d. Data d => d -> u) -> PREDITEM -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PREDITEM
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PREDITEM -> c PREDITEM
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PREDITEM)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM)
$cPredItem :: Constr
$tPREDITEM :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
gmapMp :: (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
gmapM :: (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
gmapQi :: Int -> (forall d. Data d => d -> u) -> PREDITEM -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PREDITEM -> u
gmapQ :: (forall d. Data d => d -> u) -> PREDITEM -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PREDITEM -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PREDITEM -> r
gmapT :: (forall b. Data b => b -> b) -> PREDITEM -> PREDITEM
$cgmapT :: (forall b. Data b => b -> b) -> PREDITEM -> PREDITEM
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PREDITEM)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PREDITEM)
dataTypeOf :: PREDITEM -> DataType
$cdataTypeOf :: PREDITEM -> DataType
toConstr :: PREDITEM -> Constr
$ctoConstr :: PREDITEM -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PREDITEM
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PREDITEM
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PREDITEM -> c PREDITEM
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PREDITEM -> c PREDITEM
$cp1Data :: Typeable PREDITEM
Data)

newtype BASICSPEC = BasicSpec [AS_Anno.Annoted BASICITEMS]
                  deriving (Int -> BASICSPEC -> ShowS
[BASICSPEC] -> ShowS
BASICSPEC -> String
(Int -> BASICSPEC -> ShowS)
-> (BASICSPEC -> String)
-> ([BASICSPEC] -> ShowS)
-> Show BASICSPEC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASICSPEC] -> ShowS
$cshowList :: [BASICSPEC] -> ShowS
show :: BASICSPEC -> String
$cshow :: BASICSPEC -> String
showsPrec :: Int -> BASICSPEC -> ShowS
$cshowsPrec :: Int -> BASICSPEC -> ShowS
Show, Typeable, Typeable BASICSPEC
Constr
DataType
Typeable BASICSPEC =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BASICSPEC)
-> (BASICSPEC -> Constr)
-> (BASICSPEC -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BASICSPEC))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC))
-> ((forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r)
-> (forall u. (forall d. Data d => d -> u) -> BASICSPEC -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BASICSPEC -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC)
-> Data BASICSPEC
BASICSPEC -> Constr
BASICSPEC -> DataType
(forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICSPEC
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) -> BASICSPEC -> u
forall u. (forall d. Data d => d -> u) -> BASICSPEC -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICSPEC
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BASICSPEC)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC)
$cBasicSpec :: Constr
$tBASICSPEC :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
gmapMp :: (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
gmapM :: (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICSPEC -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BASICSPEC -> u
gmapQ :: (forall d. Data d => d -> u) -> BASICSPEC -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BASICSPEC -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r
gmapT :: (forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC
$cgmapT :: (forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BASICSPEC)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BASICSPEC)
dataTypeOf :: BASICSPEC -> DataType
$cdataTypeOf :: BASICSPEC -> DataType
toConstr :: BASICSPEC -> Constr
$ctoConstr :: BASICSPEC -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICSPEC
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICSPEC
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC
$cp1Data :: Typeable BASICSPEC
Data)

data BASICITEMS =
    PredDecl PREDITEM
    | AxiomItems [AS_Anno.Annoted FORMULA]
    -- pos: dots
    deriving (Int -> BASICITEMS -> ShowS
[BASICITEMS] -> ShowS
BASICITEMS -> String
(Int -> BASICITEMS -> ShowS)
-> (BASICITEMS -> String)
-> ([BASICITEMS] -> ShowS)
-> Show BASICITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASICITEMS] -> ShowS
$cshowList :: [BASICITEMS] -> ShowS
show :: BASICITEMS -> String
$cshow :: BASICITEMS -> String
showsPrec :: Int -> BASICITEMS -> ShowS
$cshowsPrec :: Int -> BASICITEMS -> ShowS
Show, Typeable, Typeable BASICITEMS
Constr
DataType
Typeable BASICITEMS =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BASICITEMS)
-> (BASICITEMS -> Constr)
-> (BASICITEMS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BASICITEMS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c BASICITEMS))
-> ((forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r)
-> (forall u. (forall d. Data d => d -> u) -> BASICITEMS -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS)
-> Data BASICITEMS
BASICITEMS -> Constr
BASICITEMS -> DataType
(forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICITEMS
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) -> BASICITEMS -> u
forall u. (forall d. Data d => d -> u) -> BASICITEMS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICITEMS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BASICITEMS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS)
$cAxiomItems :: Constr
$cPredDecl :: Constr
$tBASICITEMS :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
gmapMp :: (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
gmapM :: (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u
gmapQ :: (forall d. Data d => d -> u) -> BASICITEMS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BASICITEMS -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r
gmapT :: (forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS
$cgmapT :: (forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BASICITEMS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BASICITEMS)
dataTypeOf :: BASICITEMS -> DataType
$cdataTypeOf :: BASICITEMS -> DataType
toConstr :: BASICITEMS -> Constr
$ctoConstr :: BASICITEMS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICITEMS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BASICITEMS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS
$cp1Data :: Typeable BASICITEMS
Data)

-- | Datatype for QBF formulas
data FORMULA =
    FalseAtom Id.Range
    -- pos: "False
  | TrueAtom Id.Range
    -- pos: "True"
  | Predication Id.Token
    -- pos: Propositional Identifiers
  | Negation FORMULA Id.Range
    -- pos: not
  | Conjunction [FORMULA] Id.Range
    -- pos: "/\"s
  | Disjunction [FORMULA] Id.Range
    -- pos: "\/"s
  | Implication FORMULA FORMULA Id.Range
    -- pos: "=>"
  | Equivalence FORMULA FORMULA Id.Range
    -- pos: "<=>"
  | ForAll [Id.Token] FORMULA Id.Range
  | Exists [Id.Token] FORMULA Id.Range
    deriving (Int -> FORMULA -> ShowS
[FORMULA] -> ShowS
FORMULA -> String
(Int -> FORMULA -> ShowS)
-> (FORMULA -> String) -> ([FORMULA] -> ShowS) -> Show FORMULA
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FORMULA] -> ShowS
$cshowList :: [FORMULA] -> ShowS
show :: FORMULA -> String
$cshow :: FORMULA -> String
showsPrec :: Int -> FORMULA -> ShowS
$cshowsPrec :: Int -> FORMULA -> ShowS
Show, Eq FORMULA
Eq FORMULA =>
(FORMULA -> FORMULA -> Ordering)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> FORMULA)
-> (FORMULA -> FORMULA -> FORMULA)
-> Ord FORMULA
FORMULA -> FORMULA -> Bool
FORMULA -> FORMULA -> Ordering
FORMULA -> FORMULA -> FORMULA
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 :: FORMULA -> FORMULA -> FORMULA
$cmin :: FORMULA -> FORMULA -> FORMULA
max :: FORMULA -> FORMULA -> FORMULA
$cmax :: FORMULA -> FORMULA -> FORMULA
>= :: FORMULA -> FORMULA -> Bool
$c>= :: FORMULA -> FORMULA -> Bool
> :: FORMULA -> FORMULA -> Bool
$c> :: FORMULA -> FORMULA -> Bool
<= :: FORMULA -> FORMULA -> Bool
$c<= :: FORMULA -> FORMULA -> Bool
< :: FORMULA -> FORMULA -> Bool
$c< :: FORMULA -> FORMULA -> Bool
compare :: FORMULA -> FORMULA -> Ordering
$ccompare :: FORMULA -> FORMULA -> Ordering
$cp1Ord :: Eq FORMULA
Ord, Typeable, Typeable FORMULA
Constr
DataType
Typeable FORMULA =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FORMULA -> c FORMULA)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FORMULA)
-> (FORMULA -> Constr)
-> (FORMULA -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FORMULA))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA))
-> ((forall b. Data b => b -> b) -> FORMULA -> FORMULA)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FORMULA -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FORMULA -> r)
-> (forall u. (forall d. Data d => d -> u) -> FORMULA -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FORMULA -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA)
-> Data FORMULA
FORMULA -> Constr
FORMULA -> DataType
(forall b. Data b => b -> b) -> FORMULA -> FORMULA
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
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) -> FORMULA -> u
forall u. (forall d. Data d => d -> u) -> FORMULA -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FORMULA)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
$cExists :: Constr
$cForAll :: Constr
$cEquivalence :: Constr
$cImplication :: Constr
$cDisjunction :: Constr
$cConjunction :: Constr
$cNegation :: Constr
$cPredication :: Constr
$cTrueAtom :: Constr
$cFalseAtom :: Constr
$tFORMULA :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapMp :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapM :: (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
gmapQi :: Int -> (forall d. Data d => d -> u) -> FORMULA -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FORMULA -> u
gmapQ :: (forall d. Data d => d -> u) -> FORMULA -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FORMULA -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FORMULA -> r
gmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULA
$cgmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULA
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FORMULA)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FORMULA)
dataTypeOf :: FORMULA -> DataType
$cdataTypeOf :: FORMULA -> DataType
toConstr :: FORMULA -> Constr
$ctoConstr :: FORMULA -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FORMULA
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FORMULA -> c FORMULA
$cp1Data :: Typeable FORMULA
Data)

data ID = ID Id.Token (Maybe Id.Token) deriving (Typeable, Typeable ID
Constr
DataType
Typeable ID =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ID -> c ID)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ID)
-> (ID -> Constr)
-> (ID -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ID))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID))
-> ((forall b. Data b => b -> b) -> ID -> ID)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r)
-> (forall u. (forall d. Data d => d -> u) -> ID -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ID -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ID -> m ID)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ID -> m ID)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ID -> m ID)
-> Data ID
ID -> Constr
ID -> DataType
(forall b. Data b => b -> b) -> ID -> ID
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ID -> c ID
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ID
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) -> ID -> u
forall u. (forall d. Data d => d -> u) -> ID -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ID -> m ID
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ID -> m ID
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ID
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ID -> c ID
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ID)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID)
$cID :: Constr
$tID :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ID -> m ID
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ID -> m ID
gmapMp :: (forall d. Data d => d -> m d) -> ID -> m ID
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ID -> m ID
gmapM :: (forall d. Data d => d -> m d) -> ID -> m ID
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ID -> m ID
gmapQi :: Int -> (forall d. Data d => d -> u) -> ID -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ID -> u
gmapQ :: (forall d. Data d => d -> u) -> ID -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ID -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r
gmapT :: (forall b. Data b => b -> b) -> ID -> ID
$cgmapT :: (forall b. Data b => b -> b) -> ID -> ID
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ID)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ID)
dataTypeOf :: ID -> DataType
$cdataTypeOf :: ID -> DataType
toConstr :: ID -> Constr
$ctoConstr :: ID -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ID
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ID
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ID -> c ID
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ID -> c ID
$cp1Data :: Typeable ID
Data)

instance Eq ID where
    ID t1 :: Token
t1 (Just t2 :: Token
t2) == :: ID -> ID -> Bool
== ID t3 :: Token
t3 (Just t4 :: Token
t4) =
                             ((Token
t1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t3) Bool -> Bool -> Bool
&& (Token
t2 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t4))
                          Bool -> Bool -> Bool
|| ((Token
t2 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t3) Bool -> Bool -> Bool
&& (Token
t1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t4))
    ID t1 :: Token
t1 Nothing == ID t2 :: Token
t2 t3 :: Maybe Token
t3 = (Token
t1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t2) Bool -> Bool -> Bool
|| (Token -> Maybe Token
forall a. a -> Maybe a
Just Token
t1 Maybe Token -> Maybe Token -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Token
t3)
    ID _ (Just _) == ID _ Nothing = Bool
False

{- two QBFs are equivalent if bound variables
can be renamed such that the QBFs are equal -}
qbfMakeEqual :: Maybe [ID] -> FORMULA -> [Id.Token]
             -> FORMULA -> [Id.Token] -> Maybe [ID]
qbfMakeEqual :: Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual (Just ids :: [ID]
ids) f :: FORMULA
f ts :: [Token]
ts f1 :: FORMULA
f1 ts1 :: [Token]
ts1 = if [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
ts1 then
                                          Maybe [ID]
forall a. Maybe a
Nothing
                                      else case (FORMULA
f, FORMULA
f1) of
  (Predication t :: Token
t, Predication t1 :: Token
t1)
    | Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t1 -> [ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids
    | Token
t Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Token]
ts Bool -> Bool -> Bool
&& Token
t1 Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Token]
ts1 -> let tt1 :: ID
tt1 = Token -> Maybe Token -> ID
ID Token
t (Token -> Maybe Token
forall a. a -> Maybe a
Just Token
t1) in
      if ID
tt1 ID -> [ID] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ID]
ids then
        [ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids
      else
        if Token -> Maybe Token -> ID
ID Token
t Maybe Token
forall a. Maybe a
Nothing ID -> [ID] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ID]
ids Bool -> Bool -> Bool
&& Token -> Maybe Token -> ID
ID Token
t1 Maybe Token
forall a. Maybe a
Nothing ID -> [ID] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ID]
ids then
          [ID] -> Maybe [ID]
forall a. a -> Maybe a
Just (ID
tt1 ID -> [ID] -> [ID]
forall a. a -> [a] -> [a]
: [ID]
ids)
        else
          Maybe [ID]
forall a. Maybe a
Nothing
    | Bool
otherwise -> Maybe [ID]
forall a. Maybe a
Nothing
  (Negation f_ :: FORMULA
f_ _, Negation f1_ :: FORMULA
f1_ _) -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids) FORMULA
f_ [Token]
ts FORMULA
f1_ [Token]
ts1
  (Conjunction (f_ :: FORMULA
f_ : fs :: [FORMULA]
fs) _, Conjunction (f1_ :: FORMULA
f1_ : fs1 :: [FORMULA]
fs1) _) ->
    if [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FORMULA]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FORMULA]
fs1 then Maybe [ID]
forall a. Maybe a
Nothing else
        case Maybe [ID]
r of
            Nothing -> Maybe [ID]
forall a. Maybe a
Nothing
            _ -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual Maybe [ID]
r
                   ([FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
fs Range
nullRange) [Token]
ts
                   ([FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
fs1 Range
nullRange) [Token]
ts1
    where
      r :: Maybe [ID]
r = Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids) FORMULA
f_ [Token]
ts FORMULA
f1_ [Token]
ts1
  (Disjunction fs :: [FORMULA]
fs r :: Range
r, Disjunction fs1 :: [FORMULA]
fs1 r1 :: Range
r1) -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids)
    ([FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
fs Range
r) [Token]
ts ([FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
fs1 Range
r1) [Token]
ts1
  (Implication f_ :: FORMULA
f_ f1_ :: FORMULA
f1_ _, Implication f2 :: FORMULA
f2 f3 :: FORMULA
f3 _) -> case Maybe [ID]
r of
    Nothing -> Maybe [ID]
forall a. Maybe a
Nothing
    _ -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual Maybe [ID]
r FORMULA
f1_ [Token]
ts FORMULA
f3 [Token]
ts1
   where
     r :: Maybe [ID]
r = Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids) FORMULA
f_ [Token]
ts FORMULA
f2 [Token]
ts1
  (Equivalence f_ :: FORMULA
f_ f1_ :: FORMULA
f1_ r1 :: Range
r1, Equivalence f2 :: FORMULA
f2 f3 :: FORMULA
f3 _) -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids)
    (FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
f_ FORMULA
f1_ Range
r1) [Token]
ts
    (FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
f2 FORMULA
f3 Range
r1) [Token]
ts1
  (ForAll ts_ :: [Token]
ts_ f_ :: FORMULA
f_ _, ForAll ts1_ :: [Token]
ts1_ f1_ :: FORMULA
f1_ _) -> case Maybe [ID]
r of
    Nothing -> Maybe [ID]
forall a. Maybe a
Nothing
    (Just ids_ :: [ID]
ids_) -> [ID] -> Maybe [ID]
forall a. a -> Maybe a
Just ([ID]
ids [ID] -> [ID] -> [ID]
forall a. [a] -> [a] -> [a]
++ (ID -> Bool) -> [ID] -> [ID]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (ID x :: Token
x my :: Maybe Token
my) ->
      let Just y :: Token
y = Maybe Token
my in
      (Token
x Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Token]
ts_ Bool -> Bool -> Bool
&& Token
y Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Token]
ts1_) Bool -> Bool -> Bool
||
      (Token
x Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Token]
ts1_ Bool -> Bool -> Bool
&& Token
y Token -> [Token] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Token]
ts_)) [ID]
d)
     where
       d :: [ID]
d = [ID]
ids_ [ID] -> [ID] -> [ID]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [ID]
ids
   where
     r :: Maybe [ID]
r = Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids) FORMULA
f_ ([Token]
ts [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ts_) FORMULA
f1_ ([Token]
ts1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ts1_)
  (Exists ts_ :: [Token]
ts_ f_ :: FORMULA
f_ r :: Range
r, Exists ts1_ :: [Token]
ts1_ f1_ :: FORMULA
f1_ r1 :: Range
r1) -> Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just [ID]
ids)
    ([Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts_ FORMULA
f_ Range
r) [Token]
ts
    ([Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts1_ FORMULA
f1_ Range
r1) [Token]
ts1
  (_1 :: FORMULA
_1, _2 :: FORMULA
_2) -> Maybe [ID]
forall a. Maybe a
Nothing

qbfMakeEqual Nothing _ _ _ _ = Maybe [ID]
forall a. Maybe a
Nothing

-- ranges are always equal (see Common/Id.hs) - thus they can be ignored
instance Eq FORMULA where
  FalseAtom _ == :: FORMULA -> FORMULA -> Bool
== FalseAtom _ = Bool
True
  TrueAtom _ == TrueAtom _ = Bool
True
  Predication t :: Token
t == Predication t1 :: Token
t1 = Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t1
  Negation f :: FORMULA
f _ == Negation f1 :: FORMULA
f1 _ = FORMULA
f FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
f1
  Conjunction xs :: [FORMULA]
xs _ == Conjunction xs1 :: [FORMULA]
xs1 _ = [FORMULA]
xs [FORMULA] -> [FORMULA] -> Bool
forall a. Eq a => a -> a -> Bool
== [FORMULA]
xs1
  Disjunction xs :: [FORMULA]
xs _ == Disjunction xs1 :: [FORMULA]
xs1 _ = [FORMULA]
xs [FORMULA] -> [FORMULA] -> Bool
forall a. Eq a => a -> a -> Bool
== [FORMULA]
xs1
  Implication f :: FORMULA
f f1 :: FORMULA
f1 _ == Implication f2 :: FORMULA
f2 f3 :: FORMULA
f3 _ = (FORMULA
f FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
f2) Bool -> Bool -> Bool
&& (FORMULA
f1 FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
f3)
  Equivalence f :: FORMULA
f f1 :: FORMULA
f1 _ == Equivalence f2 :: FORMULA
f2 f3 :: FORMULA
f3 _ = (FORMULA
f FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
f2) Bool -> Bool -> Bool
&& (FORMULA
f1 FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
f3)
  ForAll ts :: [Token]
ts f :: FORMULA
f _ == ForAll ts1 :: [Token]
ts1 f1 :: FORMULA
f1 _ = Maybe [ID] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just []) FORMULA
f [Token]
ts FORMULA
f1 [Token]
ts1)
  Exists ts :: [Token]
ts f :: FORMULA
f _ == Exists ts1 :: [Token]
ts1 f1 :: FORMULA
f1 _ = Maybe [ID] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [ID]
-> FORMULA -> [Token] -> FORMULA -> [Token] -> Maybe [ID]
qbfMakeEqual ([ID] -> Maybe [ID]
forall a. a -> Maybe a
Just []) FORMULA
f [Token]
ts FORMULA
f1 [Token]
ts1)
  _ == _ = Bool
False

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

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

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

data SYMBORMAP = Symb SYMB
                 | SymbMap SYMB SYMB Id.Range
                   -- pos: "|->"
                   deriving (Int -> SYMBORMAP -> ShowS
[SYMBORMAP] -> ShowS
SYMBORMAP -> String
(Int -> SYMBORMAP -> ShowS)
-> (SYMBORMAP -> String)
-> ([SYMBORMAP] -> ShowS)
-> Show SYMBORMAP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMBORMAP] -> ShowS
$cshowList :: [SYMBORMAP] -> ShowS
show :: SYMBORMAP -> String
$cshow :: SYMBORMAP -> String
showsPrec :: Int -> SYMBORMAP -> ShowS
$cshowsPrec :: Int -> SYMBORMAP -> ShowS
Show, SYMBORMAP -> SYMBORMAP -> Bool
(SYMBORMAP -> SYMBORMAP -> Bool)
-> (SYMBORMAP -> SYMBORMAP -> Bool) -> Eq SYMBORMAP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMBORMAP -> SYMBORMAP -> Bool
$c/= :: SYMBORMAP -> SYMBORMAP -> Bool
== :: SYMBORMAP -> SYMBORMAP -> Bool
$c== :: SYMBORMAP -> SYMBORMAP -> Bool
Eq, Eq SYMBORMAP
Eq SYMBORMAP =>
(SYMBORMAP -> SYMBORMAP -> Ordering)
-> (SYMBORMAP -> SYMBORMAP -> Bool)
-> (SYMBORMAP -> SYMBORMAP -> Bool)
-> (SYMBORMAP -> SYMBORMAP -> Bool)
-> (SYMBORMAP -> SYMBORMAP -> Bool)
-> (SYMBORMAP -> SYMBORMAP -> SYMBORMAP)
-> (SYMBORMAP -> SYMBORMAP -> SYMBORMAP)
-> Ord SYMBORMAP
SYMBORMAP -> SYMBORMAP -> Bool
SYMBORMAP -> SYMBORMAP -> Ordering
SYMBORMAP -> SYMBORMAP -> SYMBORMAP
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 :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
$cmin :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
max :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
$cmax :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
>= :: SYMBORMAP -> SYMBORMAP -> Bool
$c>= :: SYMBORMAP -> SYMBORMAP -> Bool
> :: SYMBORMAP -> SYMBORMAP -> Bool
$c> :: SYMBORMAP -> SYMBORMAP -> Bool
<= :: SYMBORMAP -> SYMBORMAP -> Bool
$c<= :: SYMBORMAP -> SYMBORMAP -> Bool
< :: SYMBORMAP -> SYMBORMAP -> Bool
$c< :: SYMBORMAP -> SYMBORMAP -> Bool
compare :: SYMBORMAP -> SYMBORMAP -> Ordering
$ccompare :: SYMBORMAP -> SYMBORMAP -> Ordering
$cp1Ord :: Eq SYMBORMAP
Ord, Typeable, Typeable SYMBORMAP
Constr
DataType
Typeable SYMBORMAP =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SYMBORMAP)
-> (SYMBORMAP -> Constr)
-> (SYMBORMAP -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP))
-> ((forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r)
-> (forall u. (forall d. Data d => d -> u) -> SYMBORMAP -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP)
-> Data SYMBORMAP
SYMBORMAP -> Constr
SYMBORMAP -> DataType
(forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMBORMAP
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) -> SYMBORMAP -> u
forall u. (forall d. Data d => d -> u) -> SYMBORMAP -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMBORMAP
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP)
$cSymbMap :: Constr
$cSymb :: Constr
$tSYMBORMAP :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
gmapMp :: (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
gmapM :: (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u
gmapQ :: (forall d. Data d => d -> u) -> SYMBORMAP -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SYMBORMAP -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r
gmapT :: (forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP
$cgmapT :: (forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP)
dataTypeOf :: SYMBORMAP -> DataType
$cdataTypeOf :: SYMBORMAP -> DataType
toConstr :: SYMBORMAP -> Constr
$ctoConstr :: SYMBORMAP -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMBORMAP
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMBORMAP
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP
$cp1Data :: Typeable SYMBORMAP
Data)

-- All about pretty printing we chose the easy way here :)
instance Pretty FORMULA where
    pretty :: FORMULA -> Doc
pretty = FORMULA -> Doc
printFormula
instance Pretty BASICSPEC where
    pretty :: BASICSPEC -> Doc
pretty = BASICSPEC -> Doc
printBasicSpec
instance Pretty SYMB where
    pretty :: SYMB -> Doc
pretty = SYMB -> Doc
printSymbol
instance Pretty SYMBITEMS where
    pretty :: SYMBITEMS -> Doc
pretty = SYMBITEMS -> Doc
printSymbItems
instance Pretty SYMBMAPITEMS where
    pretty :: SYMBMAPITEMS -> Doc
pretty = SYMBMAPITEMS -> Doc
printSymbMapItems
instance Pretty BASICITEMS where
    pretty :: BASICITEMS -> Doc
pretty = BASICITEMS -> Doc
printBasicItems
instance Pretty SYMBORMAP where
    pretty :: SYMBORMAP -> Doc
pretty = SYMBORMAP -> Doc
printSymbOrMap
instance Pretty PREDITEM where
    pretty :: PREDITEM -> Doc
pretty = PREDITEM -> Doc
printPredItem

isPrimForm :: FORMULA -> Bool
isPrimForm :: FORMULA -> Bool
isPrimForm f :: FORMULA
f = case FORMULA
f of
        TrueAtom _ -> Bool
True
        FalseAtom _ -> Bool
True
        Predication _ -> Bool
True
        Negation _ _ -> Bool
True
        _ -> Bool
False

-- Pretty printing for formulas
printFormula :: FORMULA -> Doc
printFormula :: FORMULA -> Doc
printFormula frm :: FORMULA
frm =
  let ppf :: (FORMULA -> Bool) -> FORMULA -> Doc
ppf p :: FORMULA -> Bool
p f :: FORMULA
f = (if FORMULA -> Bool
p FORMULA
f then Doc -> Doc
forall a. a -> a
id else Doc -> Doc
parens) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FORMULA -> Doc
printFormula FORMULA
f
      isJunctForm :: FORMULA -> Bool
isJunctForm f :: FORMULA
f = case FORMULA
f of
        Implication {} -> Bool
False
        Equivalence {} -> Bool
False
        ForAll {} -> Bool
False
        Exists {} -> Bool
False
        _ -> Bool
True
  in case FORMULA
frm of
  FalseAtom _ -> String -> Doc
text String
falseS
  TrueAtom _ -> String -> Doc
text String
trueS
  Predication x :: Token
x -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
x
  Negation f :: FORMULA
f _ -> Doc
notDoc Doc -> Doc -> Doc
<+> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isPrimForm FORMULA
f
  Conjunction xs :: [FORMULA]
xs _ -> Doc -> [Doc] -> Doc
sepByArbitrary Doc
andDoc ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (FORMULA -> Doc) -> [FORMULA] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isPrimForm) [FORMULA]
xs
  Disjunction xs :: [FORMULA]
xs _ -> Doc -> [Doc] -> Doc
sepByArbitrary Doc
orDoc ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (FORMULA -> Doc) -> [FORMULA] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isPrimForm) [FORMULA]
xs
  Implication x :: FORMULA
x y :: FORMULA
y _ -> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
x Doc -> Doc -> Doc
<+> Doc
implies Doc -> Doc -> Doc
<+> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
y
  Equivalence x :: FORMULA
x y :: FORMULA
y _ -> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
x Doc -> Doc -> Doc
<+> Doc
equiv Doc -> Doc -> Doc
<+> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
y
  ForAll xs :: [Token]
xs y :: FORMULA
y _ -> Doc
forallDoc Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
sepByArbitrary Doc
comma ((Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty [Token]
xs)
                     Doc -> Doc -> Doc
<+> Doc
space
                     Doc -> Doc -> Doc
<+> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
y
  Exists xs :: [Token]
xs y :: FORMULA
y _ -> Doc
exists Doc -> Doc -> Doc
<+> Doc -> [Doc] -> Doc
sepByArbitrary Doc
comma ((Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty [Token]
xs)
                     Doc -> Doc -> Doc
<+> Doc
space
                     Doc -> Doc -> Doc
<+> (FORMULA -> Bool) -> FORMULA -> Doc
ppf FORMULA -> Bool
isJunctForm FORMULA
y

sepByArbitrary :: Doc -> [Doc] -> Doc
sepByArbitrary :: Doc -> [Doc] -> Doc
sepByArbitrary d :: Doc
d = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
prepPunctuate (Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)

printPredItem :: PREDITEM -> Doc
printPredItem :: PREDITEM -> Doc
printPredItem (PredItem xs :: [Token]
xs _) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty [Token]
xs

printBasicSpec :: BASICSPEC -> Doc
printBasicSpec :: BASICSPEC -> Doc
printBasicSpec (BasicSpec xs :: [Annoted BASICITEMS]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted BASICITEMS -> Doc) -> [Annoted BASICITEMS] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASICITEMS -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted BASICITEMS]
xs

printBasicItems :: BASICITEMS -> Doc
printBasicItems :: BASICITEMS -> Doc
printBasicItems (AxiomItems xs :: [Annoted FORMULA]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted FORMULA -> Doc) -> [Annoted FORMULA] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted FORMULA]
xs
printBasicItems (PredDecl x :: PREDITEM
x) = PREDITEM -> Doc
forall a. Pretty a => a -> Doc
pretty PREDITEM
x

printSymbol :: SYMB -> Doc
printSymbol :: SYMB -> Doc
printSymbol (SymbId sym :: Token
sym) = Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
sym

printSymbItems :: SYMBITEMS -> Doc
printSymbItems :: SYMBITEMS -> Doc
printSymbItems (SymbItems xs :: [SYMB]
xs _) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SYMB -> Doc) -> [SYMB] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty [SYMB]
xs

printSymbOrMap :: SYMBORMAP -> Doc
printSymbOrMap :: SYMBORMAP -> Doc
printSymbOrMap (Symb sym :: SYMB
sym) = SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty SYMB
sym
printSymbOrMap (SymbMap source :: SYMB
source dest :: SYMB
dest _) =
  SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty SYMB
source Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+> SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty SYMB
dest

printSymbMapItems :: SYMBMAPITEMS -> Doc
printSymbMapItems :: SYMBMAPITEMS -> Doc
printSymbMapItems (SymbMapItems xs :: [SYMBORMAP]
xs _) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SYMBORMAP -> Doc) -> [SYMBORMAP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SYMBORMAP -> Doc
forall a. Pretty a => a -> Doc
pretty [SYMBORMAP]
xs

-- Generated by DrIFT, look but don't touch!

instance GetRange PREDITEM where
  getRange :: PREDITEM -> Range
getRange = Range -> PREDITEM -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: PREDITEM -> [Pos]
rangeSpan x :: PREDITEM
x = case PREDITEM
x of
    PredItem a :: [Token]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[Token] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Token]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange BASICSPEC where
  getRange :: BASICSPEC -> Range
getRange = Range -> BASICSPEC -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: BASICSPEC -> [Pos]
rangeSpan x :: BASICSPEC
x = case BASICSPEC
x of
    BasicSpec a :: [Annoted BASICITEMS]
a -> [[Pos]] -> [Pos]
joinRanges [[Annoted BASICITEMS] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted BASICITEMS]
a]

instance GetRange BASICITEMS where
  getRange :: BASICITEMS -> Range
getRange = Range -> BASICITEMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: BASICITEMS -> [Pos]
rangeSpan x :: BASICITEMS
x = case BASICITEMS
x of
    PredDecl a :: PREDITEM
a -> [[Pos]] -> [Pos]
joinRanges [PREDITEM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PREDITEM
a]
    AxiomItems a :: [Annoted FORMULA]
a -> [[Pos]] -> [Pos]
joinRanges [[Annoted FORMULA] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted FORMULA]
a]

instance GetRange FORMULA where
  getRange :: FORMULA -> Range
getRange = Range -> FORMULA -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: FORMULA -> [Pos]
rangeSpan x :: FORMULA
x = case FORMULA
x of
    FalseAtom a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    TrueAtom a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    Predication a :: Token
a -> [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
a]
    Negation a :: FORMULA
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Conjunction a :: [FORMULA]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[FORMULA] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [FORMULA]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Disjunction a :: [FORMULA]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[FORMULA] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [FORMULA]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Implication a :: FORMULA
a b :: FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
a, FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
b,
                                     Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Equivalence a :: FORMULA
a b :: FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
a, FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
b,
                                     Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    ForAll a :: [Token]
a b :: FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Token] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Token]
a, FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Exists a :: [Token]
a b :: FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Token] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Token]
a, FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange ID where
  getRange :: ID -> Range
getRange = Range -> ID -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: ID -> [Pos]
rangeSpan x :: ID
x = case ID
x of
    ID a :: Token
a b :: Maybe Token
b -> [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
a, Maybe Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Maybe Token
b]

instance GetRange SYMBITEMS where
  getRange :: SYMBITEMS -> Range
getRange = Range -> SYMBITEMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMBITEMS -> [Pos]
rangeSpan x :: SYMBITEMS
x = case SYMBITEMS
x of
    SymbItems a :: [SYMB]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[SYMB] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [SYMB]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange SYMB where
  getRange :: SYMB -> Range
getRange = Range -> SYMB -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMB -> [Pos]
rangeSpan x :: SYMB
x = case SYMB
x of
    SymbId a :: Token
a -> [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
a]

instance GetRange SYMBMAPITEMS where
  getRange :: SYMBMAPITEMS -> Range
getRange = Range -> SYMBMAPITEMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMBMAPITEMS -> [Pos]
rangeSpan x :: SYMBMAPITEMS
x = case SYMBMAPITEMS
x of
    SymbMapItems a :: [SYMBORMAP]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[SYMBORMAP] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [SYMBORMAP]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange SYMBORMAP where
  getRange :: SYMBORMAP -> Range
getRange = Range -> SYMBORMAP -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMBORMAP -> [Pos]
rangeSpan x :: SYMBORMAP
x = case SYMBORMAP
x of
    Symb a :: SYMB
a -> [[Pos]] -> [Pos]
joinRanges [SYMB -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SYMB
a]
    SymbMap a :: SYMB
a b :: SYMB
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [SYMB -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SYMB
a, SYMB -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SYMB
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]