{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./CASL/ToItem.hs
Description :  extracted annotated items as strings from BASIC_SPEC
Copyright   :  (c) Christian Maeder and Ewaryst Schulz  and DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Ewaryst.Schulz@dfki.de
Stability   :  experimental
Portability :  non-portable

get item representation of 'BASIC_SPEC'
-}

module CASL.ToItem (bsToItem) where

import Control.Monad.Reader

import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Item

import CASL.AS_Basic_CASL
import CASL.ToDoc

-- ------------------- TS = TransState
data TS b s f = TS { TS b s f -> b -> Doc
fB :: b -> Doc
                   , TS b s f -> s -> Doc
fS :: s -> Doc }

{- LITC = LocalITContext
This datastructure is used to pass an additional ItemType argument to
the toitem method when one needs an instance for which this method
should behave differently in different contexts depending on this argument.
Typically the ItemType is used as ItemType of the Item to be created. -}

data LITC a = LITC ItemType a

-- ------------------- lifting to Local Contexts
withLIT :: ItemTypeable a => a -> b -> LITC b
withLIT :: a -> b -> LITC b
withLIT = ItemType -> b -> LITC b
forall a. ItemType -> a -> LITC a
LITC (ItemType -> b -> LITC b) -> (a -> ItemType) -> a -> b -> LITC b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ItemType
forall a. ItemTypeable a => a -> ItemType
toIT

listWithLIT :: ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT :: a -> [b] -> [LITC b]
listWithLIT = (b -> LITC b) -> [b] -> [LITC b]
forall a b. (a -> b) -> [a] -> [b]
map ((b -> LITC b) -> [b] -> [LITC b])
-> (a -> b -> LITC b) -> a -> [b] -> [LITC b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> LITC b
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT

{- analogous for annotated objects, don't needed yet
annWithLIT :: ItemTypeable a => a -> Annoted b -> Annoted (LITC b)
annWithLIT it = fmap (withLIT it) -}

{- annlistWithLIT :: ItemTypeable a => a -> [Annoted b] -> [Annoted (LITC b)]
annlistWithLIT it = map (annWithLIT it) -}


{- this function is only to unify the types of the state and the basic spec
in the call of toitem and runState in bsToItem -}
getTransState :: (Pretty b, Pretty s)
    => BASIC_SPEC b s f -> TS b s f
getTransState :: BASIC_SPEC b s f -> TS b s f
getTransState _ = (b -> Doc) -> (s -> Doc) -> TS b s f
forall b s f. (b -> Doc) -> (s -> Doc) -> TS b s f
TS b -> Doc
forall a. Pretty a => a -> Doc
pretty s -> Doc
forall a. Pretty a => a -> Doc
pretty

-- ------------------- The Main function of this module
bsToItem :: (Pretty b, Pretty s, GetRange b, GetRange s, FormExtension f)
    => BASIC_SPEC b s f -> Item
bsToItem :: BASIC_SPEC b s f -> Item
bsToItem bs :: BASIC_SPEC b s f
bs = Reader (TS b s f) Item -> TS b s f -> Item
forall r a. Reader r a -> r -> a
runReader (BASIC_SPEC b s f -> Reader (TS b s f) Item
forall a (m :: * -> *). ItemConvertible a m => a -> m Item
toitem BASIC_SPEC b s f
bs) (TS b s f -> Item) -> TS b s f -> Item
forall a b. (a -> b) -> a -> b
$ BASIC_SPEC b s f -> TS b s f
forall b s f. (Pretty b, Pretty s) => BASIC_SPEC b s f -> TS b s f
getTransState BASIC_SPEC b s f
bs

instance (GetRange b, GetRange s, FormExtension f)
    => ItemConvertible (BASIC_SPEC b s f) (Reader (TS b s f)) where
    toitem :: BASIC_SPEC b s f -> Reader (TS b s f) Item
toitem (Basic_spec l :: [Annoted (BASIC_ITEMS b s f)]
l) = do
        [Annoted Item]
l' <- [Annoted (BASIC_ITEMS b s f)]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (BASIC_ITEMS b s f)]
l
        Item -> Reader (TS b s f) Item
forall (m :: * -> *) a. Monad m => a -> m a
return Item
rootItem { items :: [Annoted Item]
items = [Annoted Item]
l' }

instance (GetRange b, GetRange s, FormExtension f)
    => ItemConvertible (BASIC_ITEMS b s f) (Reader (TS b s f)) where
    toitem :: BASIC_ITEMS b s f -> Reader (TS b s f) Item
toitem bi :: BASIC_ITEMS b s f
bi = let rg :: Range
rg = BASIC_ITEMS b s f -> Range
forall a. GetRange a => a -> Range
getRangeSpan BASIC_ITEMS b s f
bi in
        case BASIC_ITEMS b s f
bi of
          Sig_items s :: SIG_ITEMS s f
s -> SIG_ITEMS s f -> Reader (TS b s f) Item
forall a (m :: * -> *). ItemConvertible a m => a -> m Item
toitem SIG_ITEMS s f
s
          Var_items l :: [VAR_DECL]
l _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Var_items" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[a] -> m [Annoted Item]
listFromL [VAR_DECL]
l
          Axiom_items al :: [Annoted (FORMULA f)]
al _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Axiom_items" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted (FORMULA f)] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (FORMULA f)]
al
          Local_var_axioms vl :: [VAR_DECL]
vl fl :: [Annoted (FORMULA f)]
fl _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Local_var_axioms" Range
rg
                           [[Char] -> [VAR_DECL] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [a] -> m (Annoted Item)
fromL "VAR_DECLS" [VAR_DECL]
vl, [Char]
-> [Annoted (FORMULA f)]
-> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [Annoted a] -> m (Annoted Item)
fromAL "FORMULAS" [Annoted (FORMULA f)]
fl]
          Sort_gen asis :: [Annoted (SIG_ITEMS s f)]
asis _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Sort_gen" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted (SIG_ITEMS s f)]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (SIG_ITEMS s f)]
asis
          Free_datatype sk :: SortsKind
sk adtds :: [Annoted DATATYPE_DECL]
adtds _ ->
              ([Char], [Char], [Char])
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM ("Free_datatype", "SortsKind", SortsKind -> [Char]
forall a. Show a => a -> [Char]
show SortsKind
sk) Range
rg
                          (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted DATATYPE_DECL]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted DATATYPE_DECL]
adtds
          Ext_BASIC_ITEMS b :: b
b -> do
              TS b s f
st <- ReaderT (TS b s f) Identity (TS b s f)
forall r (m :: * -> *). MonadReader r m => m r
ask
              (b -> Doc) -> [Char] -> b -> Reader (TS b s f) Item
forall (m :: * -> *) a.
Monad m =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinter (TS b s f -> b -> Doc
forall b s f. TS b s f -> b -> Doc
fB TS b s f
st) "Ext_BASIC_ITEMS" b
b

instance (GetRange s, FormExtension f)
    => ItemConvertible (SIG_ITEMS s f) (Reader (TS b s f)) where
    toitem :: SIG_ITEMS s f -> Reader (TS b s f) Item
toitem si :: SIG_ITEMS s f
si = let rg :: Range
rg = SIG_ITEMS s f -> Range
forall a. GetRange a => a -> Range
getRangeSpan SIG_ITEMS s f
si in
        case SIG_ITEMS s f
si of
          Sort_items sk :: SortsKind
sk sis :: [Annoted (SORT_ITEM f)]
sis _ ->
              ([Char], [Char], [Char])
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM ("Sort_items", "SortsKind", SortsKind -> [Char]
forall a. Show a => a -> [Char]
show SortsKind
sk) Range
rg
                (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted (SORT_ITEM f)]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (SORT_ITEM f)]
sis
          Op_items aois :: [Annoted (OP_ITEM f)]
aois _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Op_items" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted (OP_ITEM f)] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (OP_ITEM f)]
aois
          Pred_items apis :: [Annoted (PRED_ITEM f)]
apis _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Pred_items" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted (PRED_ITEM f)]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted (PRED_ITEM f)]
apis
          Datatype_items sk :: SortsKind
sk adds :: [Annoted DATATYPE_DECL]
adds _ ->
              ([Char], [Char], [Char])
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM ("Datatype_items", "SortsKind", SortsKind -> [Char]
forall a. Show a => a -> [Char]
show SortsKind
sk) Range
rg
                (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [Annoted DATATYPE_DECL]
-> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[Annoted a] -> m [Annoted Item]
listFromAL [Annoted DATATYPE_DECL]
adds
          Ext_SIG_ITEMS s :: s
s -> do
              TS b s f
st <- ReaderT (TS b s f) Identity (TS b s f)
forall r (m :: * -> *). MonadReader r m => m r
ask
              (s -> Doc) -> [Char] -> s -> Reader (TS b s f) Item
forall (m :: * -> *) a.
Monad m =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinter (TS b s f -> s -> Doc
forall b s f. TS b s f -> s -> Doc
fS TS b s f
st) "Ext_SIG_ITEMS" s
s


instance FormExtension f
    => ItemConvertible (SORT_ITEM f) (Reader (TS b s f)) where
    toitem :: SORT_ITEM f -> Reader (TS b s f) Item
toitem si :: SORT_ITEM f
si = let rg :: Range
rg = SORT_ITEM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan SORT_ITEM f
si in
        case SORT_ITEM f
si of
          Sort_decl l :: [SORT]
l _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Sort_decl" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[a] -> m [Annoted Item]
listFromL
                            ([LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item])
-> [LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a b. (a -> b) -> a -> b
$ [Char] -> [SORT] -> [LITC SORT]
forall a b. ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT "SORT" [SORT]
l
          Subsort_decl sl :: [SORT]
sl s :: SORT
s _ -> [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Subsort_decl" Range
rg
                                  [ [Char] -> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [a] -> m (Annoted Item)
fromL "SORTS" ([LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item))
-> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> [SORT] -> [LITC SORT]
forall a b. ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT "SORT" [SORT]
sl
                                  , LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT -> LITC SORT
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "SORT" SORT
s]
          Subsort_defn s :: SORT
s v :: VAR
v s' :: SORT
s' f :: Annoted (FORMULA f)
f _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Subsort_defn" Range
rg
                [ LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT -> LITC SORT
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "SORT" SORT
s, LITC VAR -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC VAR -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC VAR -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> VAR -> LITC VAR
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "VAR" VAR
v
                , LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT -> LITC SORT
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "SORT" SORT
s', Annoted (FORMULA f) -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
Annoted a -> m (Annoted Item)
fromAC Annoted (FORMULA f)
f]
          Iso_decl l :: [SORT]
l _ -> [Char]
-> Range
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> m [Annoted Item] -> m Item
mkItemM "Iso_decl" Range
rg (ReaderT (TS b s f) Identity [Annoted Item]
 -> Reader (TS b s f) Item)
-> ReaderT (TS b s f) Identity [Annoted Item]
-> Reader (TS b s f) Item
forall a b. (a -> b) -> a -> b
$ [LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a (m :: * -> *).
ItemConvertible a m =>
[a] -> m [Annoted Item]
listFromL
                           ([LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item])
-> [LITC SORT] -> ReaderT (TS b s f) Identity [Annoted Item]
forall a b. (a -> b) -> a -> b
$ [Char] -> [SORT] -> [LITC SORT]
forall a b. ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT "SORT" [SORT]
l


instance FormExtension f
    => ItemConvertible (OP_ITEM f) (Reader (TS b s f)) where
    toitem :: OP_ITEM f -> Reader (TS b s f) Item
toitem oi :: OP_ITEM f
oi = let rg :: Range
rg = OP_ITEM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan OP_ITEM f
oi in
        case OP_ITEM f
oi of
          Op_decl onl :: [SORT]
onl ot :: OP_TYPE
ot oal :: [OP_ATTR f]
oal _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Op_decl" Range
rg
                [ [Char] -> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [a] -> m (Annoted Item)
fromL "OP_NAMES" ([LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item))
-> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> [SORT] -> [LITC SORT]
forall a b. ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT "OP_NAME" [SORT]
onl, OP_TYPE -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC OP_TYPE
ot
                , [Char] -> [OP_ATTR f] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [a] -> m (Annoted Item)
fromL "OP_ATTRIBS" [OP_ATTR f]
oal]
          Op_defn on :: SORT
on oh :: OP_HEAD
oh at :: Annoted (TERM f)
at _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Op_defn" Range
rg [ LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT -> LITC SORT
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "OP_NAME" SORT
on, OP_HEAD -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC OP_HEAD
oh
                                    , Annoted (TERM f) -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
Annoted a -> m (Annoted Item)
fromAC Annoted (TERM f)
at]


instance FormExtension f
    => ItemConvertible (PRED_ITEM f) (Reader (TS b s f)) where
    toitem :: PRED_ITEM f -> Reader (TS b s f) Item
toitem p :: PRED_ITEM f
p = let rg :: Range
rg = PRED_ITEM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan PRED_ITEM f
p in
        case PRED_ITEM f
p of
          Pred_decl pnl :: [SORT]
pnl pt :: PRED_TYPE
pt _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Pred_decl" Range
rg
                [[Char] -> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *) b.
(ItemConvertible a m, ItemTypeable b) =>
b -> [a] -> m (Annoted Item)
fromL "PRED_NAMES" ([LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item))
-> [LITC SORT] -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> [SORT] -> [LITC SORT]
forall a b. ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT "PRED_NAME" [SORT]
pnl, PRED_TYPE -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC PRED_TYPE
pt]
          Pred_defn pn :: SORT
pn ph :: PRED_HEAD
ph af :: Annoted (FORMULA f)
af _ ->
              [Char]
-> Range
-> [ReaderT (TS b s f) Identity (Annoted Item)]
-> Reader (TS b s f) Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM "Pred_defn" Range
rg [ LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC (LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item))
-> LITC SORT -> ReaderT (TS b s f) Identity (Annoted Item)
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT -> LITC SORT
forall a b. ItemTypeable a => a -> b -> LITC b
withLIT "PRED_NAME" SORT
pn, PRED_HEAD -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
a -> m (Annoted Item)
fromC PRED_HEAD
ph
                                      , Annoted (FORMULA f) -> ReaderT (TS b s f) Identity (Annoted Item)
forall a (m :: * -> *).
ItemConvertible a m =>
Annoted a -> m (Annoted Item)
fromAC Annoted (FORMULA f)
af]

-- ------------------ not further expanded --------------------

fromPrinterWithRg :: (Monad m, GetRange a) =>
                     (a -> Doc) -> String -> a -> m Item
fromPrinterWithRg :: (a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg = (a -> Range) -> (a -> Doc) -> [Char] -> a -> m Item
forall (m :: * -> *) a.
Monad m =>
(a -> Range) -> (a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRange a -> Range
forall a. GetRange a => a -> Range
getRangeSpan

fromPrinterWithRange
    :: Monad m => (a -> Range) -> (a -> Doc) -> String -> a -> m Item
fromPrinterWithRange :: (a -> Range) -> (a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRange r :: a -> Range
r p :: a -> Doc
p n :: [Char]
n o :: a
o = ([Char], Doc) -> Range -> [m (Annoted Item)] -> m Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM ([Char]
n, a -> Doc
p a
o) (a -> Range
r a
o) []

fromPrinter :: Monad m => (a -> Doc) -> String -> a -> m Item
fromPrinter :: (a -> Doc) -> [Char] -> a -> m Item
fromPrinter p :: a -> Doc
p n :: [Char]
n o :: a
o = ([Char], Doc) -> Range -> [m (Annoted Item)] -> m Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM ([Char]
n, a -> Doc
p a
o) Range
nullRange []

litFromPrinterWithRg :: (Monad m, GetRange a) =>
                        (a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg :: (a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg p :: a -> Doc
p (LITC (IT l :: [Char]
l attrs :: [([Char], [Char])]
attrs _) o :: a
o) =
    ItemType -> Range -> [m (Annoted Item)] -> m Item
forall a (m :: * -> *).
(ItemTypeable a, Monad m) =>
a -> Range -> [m (Annoted Item)] -> m Item
mkItemMM ([Char] -> [([Char], [Char])] -> Maybe Doc -> ItemType
IT [Char]
l [([Char], [Char])]
attrs (Maybe Doc -> ItemType) -> Maybe Doc -> ItemType
forall a b. (a -> b) -> a -> b
$ Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
p a
o) (a -> Range
forall a. GetRange a => a -> Range
getRangeSpan a
o) []


instance ItemConvertible OP_TYPE (Reader (TS b s f)) where
    toitem :: OP_TYPE -> Reader (TS b s f) Item
toitem = (OP_TYPE -> Doc) -> [Char] -> OP_TYPE -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg OP_TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty "OP_TYPE"

instance ItemConvertible OP_HEAD (Reader (TS b s f)) where
    toitem :: OP_HEAD -> Reader (TS b s f) Item
toitem = (OP_HEAD -> Doc) -> [Char] -> OP_HEAD -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg OP_HEAD -> Doc
forall a. Pretty a => a -> Doc
pretty "OP_HEAD"

instance FormExtension f
    => ItemConvertible (OP_ATTR f) (Reader (TS b s f)) where
    toitem :: OP_ATTR f -> Reader (TS b s f) Item
toitem = (OP_ATTR f -> Doc) -> [Char] -> OP_ATTR f -> Reader (TS b s f) Item
forall (m :: * -> *) a.
Monad m =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinter OP_ATTR f -> Doc
forall f. FormExtension f => OP_ATTR f -> Doc
printAttr "OP_ATTR"

instance ItemConvertible PRED_TYPE (Reader (TS b s f)) where
    toitem :: PRED_TYPE -> Reader (TS b s f) Item
toitem = (PRED_TYPE -> Doc) -> [Char] -> PRED_TYPE -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg PRED_TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty "PRED_TYPE"

instance ItemConvertible PRED_HEAD (Reader (TS b s f)) where
    toitem :: PRED_HEAD -> Reader (TS b s f) Item
toitem = (PRED_HEAD -> Doc) -> [Char] -> PRED_HEAD -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg PRED_HEAD -> Doc
printPredHead "PRED_HEAD"

instance ItemConvertible DATATYPE_DECL (Reader (TS b s f)) where
    toitem :: DATATYPE_DECL -> Reader (TS b s f) Item
toitem = (DATATYPE_DECL -> Doc)
-> [Char] -> DATATYPE_DECL -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg DATATYPE_DECL -> Doc
forall a. Pretty a => a -> Doc
pretty "DATATYPE_DECL"

instance ItemConvertible VAR_DECL (Reader (TS b s f)) where
    toitem :: VAR_DECL -> Reader (TS b s f) Item
toitem = (VAR_DECL -> Doc) -> [Char] -> VAR_DECL -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRg VAR_DECL -> Doc
forall a. Pretty a => a -> Doc
pretty "VAR_DECL"

instance FormExtension f
    => ItemConvertible (FORMULA f) (Reader (TS b s f)) where
    toitem :: FORMULA f -> Reader (TS b s f) Item
toitem = (FORMULA f -> Range)
-> (FORMULA f -> Doc)
-> [Char]
-> FORMULA f
-> Reader (TS b s f) Item
forall (m :: * -> *) a.
Monad m =>
(a -> Range) -> (a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRange FORMULA f -> Range
forall a. GetRange a => a -> Range
getRangeSpan FORMULA f -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula "FORMULA"

instance FormExtension f => ItemConvertible (TERM f) (Reader (TS b s f)) where
    toitem :: TERM f -> Reader (TS b s f) Item
toitem = (TERM f -> Range)
-> (TERM f -> Doc) -> [Char] -> TERM f -> Reader (TS b s f) Item
forall (m :: * -> *) a.
Monad m =>
(a -> Range) -> (a -> Doc) -> [Char] -> a -> m Item
fromPrinterWithRange TERM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan TERM f -> Doc
forall f. FormExtension f => TERM f -> Doc
printTerm "TERM"

instance ItemConvertible (LITC Id) (Reader (TS b s f)) where
    toitem :: LITC SORT -> Reader (TS b s f) Item
toitem = (SORT -> Doc) -> LITC SORT -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg SORT -> Doc
forall a. Pretty a => a -> Doc
pretty

instance ItemConvertible (LITC Token) (Reader (TS b s f)) where
    toitem :: LITC VAR -> Reader (TS b s f) Item
toitem = (VAR -> Doc) -> LITC VAR -> Reader (TS b s f) Item
forall (m :: * -> *) a.
(Monad m, GetRange a) =>
(a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg VAR -> Doc
forall a. Pretty a => a -> Doc
pretty