{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Propositional/AS_BASIC_Propositional.der.hs
Description :  Abstract syntax for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Definition of abstract syntax for propositional logic
-}

{-
  Ref.
  http://en.wikipedia.org/wiki/Propositional_logic
-}

module Propositional.AS_BASIC_Propositional
    ( FORMULA (..)             -- datatype for Propositional Formulas
    , BASIC_ITEMS (..)         -- Items of a Basic Spec
    , BASIC_SPEC (..)          -- Basic Spec
    , SYMB_ITEMS (..)          -- List of symbols
    , SYMB (..)                -- Symbols
    , SYMB_MAP_ITEMS (..)      -- Symbol map
    , SYMB_OR_MAP (..)         -- Symbol or symbol map
    , PRED_ITEM (..)           -- Predicates
    , isPrimForm
    ) 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

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

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

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

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

-- | Datatype for propositional formulas
data FORMULA =
    False_atom Id.Range
    -- pos: "False
  | True_atom 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: "<=>"
    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, FORMULA -> FORMULA -> Bool
(FORMULA -> FORMULA -> Bool)
-> (FORMULA -> FORMULA -> Bool) -> Eq FORMULA
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FORMULA -> FORMULA -> Bool
$c/= :: FORMULA -> FORMULA -> Bool
== :: FORMULA -> FORMULA -> Bool
$c== :: FORMULA -> FORMULA -> Bool
Eq, 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)
$cEquivalence :: Constr
$cImplication :: Constr
$cDisjunction :: Constr
$cConjunction :: Constr
$cNegation :: Constr
$cPredication :: Constr
$cTrue_atom :: Constr
$cFalse_atom :: 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 SYMB_ITEMS = Symb_items [SYMB] Id.Range
                  -- pos: SYMB_KIND, commas
                  deriving (Int -> SYMB_ITEMS -> ShowS
[SYMB_ITEMS] -> ShowS
SYMB_ITEMS -> String
(Int -> SYMB_ITEMS -> ShowS)
-> (SYMB_ITEMS -> String)
-> ([SYMB_ITEMS] -> ShowS)
-> Show SYMB_ITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_ITEMS] -> ShowS
$cshowList :: [SYMB_ITEMS] -> ShowS
show :: SYMB_ITEMS -> String
$cshow :: SYMB_ITEMS -> String
showsPrec :: Int -> SYMB_ITEMS -> ShowS
$cshowsPrec :: Int -> SYMB_ITEMS -> ShowS
Show, SYMB_ITEMS -> SYMB_ITEMS -> Bool
(SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool) -> Eq SYMB_ITEMS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
Eq, Eq SYMB_ITEMS
Eq SYMB_ITEMS =>
(SYMB_ITEMS -> SYMB_ITEMS -> Ordering)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS)
-> (SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS)
-> Ord SYMB_ITEMS
SYMB_ITEMS -> SYMB_ITEMS -> Bool
SYMB_ITEMS -> SYMB_ITEMS -> Ordering
SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS
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_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS
$cmin :: SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS
max :: SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS
$cmax :: SYMB_ITEMS -> SYMB_ITEMS -> SYMB_ITEMS
>= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c>= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
> :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c> :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
<= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c<= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
< :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c< :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
compare :: SYMB_ITEMS -> SYMB_ITEMS -> Ordering
$ccompare :: SYMB_ITEMS -> SYMB_ITEMS -> Ordering
$cp1Ord :: Eq SYMB_ITEMS
Ord, Typeable, Typeable SYMB_ITEMS
Constr
DataType
Typeable SYMB_ITEMS =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS)
-> (SYMB_ITEMS -> Constr)
-> (SYMB_ITEMS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SYMB_ITEMS))
-> ((forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r)
-> (forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS)
-> Data SYMB_ITEMS
SYMB_ITEMS -> Constr
SYMB_ITEMS -> DataType
(forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
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_ITEMS -> u
forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
$cSymb_items :: Constr
$tSYMB_ITEMS :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapMp :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapM :: (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u
gmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r
gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
$cgmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)
dataTypeOf :: SYMB_ITEMS -> DataType
$cdataTypeOf :: SYMB_ITEMS -> DataType
toConstr :: SYMB_ITEMS -> Constr
$ctoConstr :: SYMB_ITEMS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS
$cp1Data :: Typeable SYMB_ITEMS
Data)

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

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

{- All about pretty printing
we chose the easy way here :) -}
instance Pretty FORMULA where
    pretty :: FORMULA -> Doc
pretty = FORMULA -> Doc
printFormula
instance Pretty BASIC_SPEC where
    pretty :: BASIC_SPEC -> Doc
pretty = BASIC_SPEC -> Doc
printBasicSpec
instance Pretty SYMB where
    pretty :: SYMB -> Doc
pretty = SYMB -> Doc
printSymbol
instance Pretty SYMB_ITEMS where
    pretty :: SYMB_ITEMS -> Doc
pretty = SYMB_ITEMS -> Doc
printSymbItems
instance Pretty SYMB_MAP_ITEMS where
    pretty :: SYMB_MAP_ITEMS -> Doc
pretty = SYMB_MAP_ITEMS -> Doc
printSymbMapItems
instance Pretty BASIC_ITEMS where
    pretty :: BASIC_ITEMS -> Doc
pretty = BASIC_ITEMS -> Doc
printBasicItems
instance Pretty SYMB_OR_MAP where
    pretty :: SYMB_OR_MAP -> Doc
pretty = SYMB_OR_MAP -> Doc
printSymbOrMap
instance Pretty PRED_ITEM where
    pretty :: PRED_ITEM -> Doc
pretty = PRED_ITEM -> Doc
printPredItem

isPrimForm :: FORMULA -> Bool
isPrimForm :: FORMULA -> Bool
isPrimForm f :: FORMULA
f = case FORMULA
f of
        True_atom _ -> Bool
True
        False_atom _ -> 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
        _ -> Bool
True
  in case FORMULA
frm of
  False_atom _ -> String -> Doc
text String
falseS
  True_atom _ -> 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

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 :: PRED_ITEM -> Doc
printPredItem :: PRED_ITEM -> Doc
printPredItem (Pred_item xs :: [Token]
xs _) =
  String -> Doc
keyword (String
propS String -> ShowS
forall a. [a] -> [a] -> [a]
++ case [Token]
xs of
     [_] -> ""
     _ -> "s") Doc -> Doc -> Doc
<+> [Token] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [Token]
xs

printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (Basic_spec xs :: [Annoted BASIC_ITEMS]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> Doc) -> [Annoted BASIC_ITEMS] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASIC_ITEMS -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted BASIC_ITEMS]
xs

printBasicItems :: BASIC_ITEMS -> Doc
printBasicItems :: BASIC_ITEMS -> Doc
printBasicItems (Axiom_items 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 (Doc -> Doc
addBullet (Doc -> Doc) -> (Annoted FORMULA -> Doc) -> Annoted FORMULA -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty) [Annoted FORMULA]
xs
printBasicItems (Pred_decl x :: PRED_ITEM
x) = PRED_ITEM -> Doc
forall a. Pretty a => a -> Doc
pretty PRED_ITEM
x

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

printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items 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 :: SYMB_OR_MAP -> Doc
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap (Symb sym :: SYMB
sym) = SYMB -> Doc
forall a. Pretty a => a -> Doc
pretty SYMB
sym
printSymbOrMap (Symb_map 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 :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items xs :: [SYMB_OR_MAP]
xs _) = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SYMB_OR_MAP -> Doc) -> [SYMB_OR_MAP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SYMB_OR_MAP -> Doc
forall a. Pretty a => a -> Doc
pretty [SYMB_OR_MAP]
xs

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

instance GetRange PRED_ITEM where
  getRange :: PRED_ITEM -> Range
getRange = Range -> PRED_ITEM -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: PRED_ITEM -> [Pos]
rangeSpan x :: PRED_ITEM
x = case PRED_ITEM
x of
    Pred_item 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 BASIC_SPEC where
  getRange :: BASIC_SPEC -> Range
getRange = Range -> BASIC_SPEC -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: BASIC_SPEC -> [Pos]
rangeSpan x :: BASIC_SPEC
x = case BASIC_SPEC
x of
    Basic_spec a :: [Annoted BASIC_ITEMS]
a -> [[Pos]] -> [Pos]
joinRanges [[Annoted BASIC_ITEMS] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted BASIC_ITEMS]
a]

instance GetRange BASIC_ITEMS where
  getRange :: BASIC_ITEMS -> Range
getRange = Range -> BASIC_ITEMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: BASIC_ITEMS -> [Pos]
rangeSpan x :: BASIC_ITEMS
x = case BASIC_ITEMS
x of
    Pred_decl a :: PRED_ITEM
a -> [[Pos]] -> [Pos]
joinRanges [PRED_ITEM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan PRED_ITEM
a]
    Axiom_items 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
    False_atom a :: Range
a -> [[Pos]] -> [Pos]
joinRanges [Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
a]
    True_atom 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]

instance GetRange SYMB_ITEMS where
  getRange :: SYMB_ITEMS -> Range
getRange = Range -> SYMB_ITEMS -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMB_ITEMS -> [Pos]
rangeSpan x :: SYMB_ITEMS
x = case SYMB_ITEMS
x of
    Symb_items 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
    Symb_id a :: Token
a -> [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
a]

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

instance GetRange SYMB_OR_MAP where
  getRange :: SYMB_OR_MAP -> Range
getRange = Range -> SYMB_OR_MAP -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: SYMB_OR_MAP -> [Pos]
rangeSpan x :: SYMB_OR_MAP
x = case SYMB_OR_MAP
x of
    Symb a :: SYMB
a -> [[Pos]] -> [Pos]
joinRanges [SYMB -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SYMB
a]
    Symb_map 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]