{-# 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