ToItem.hs revision ccd28c25c1aee73a195053e677eca17e20917d84
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module : $Header$
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 { fB :: b -> 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 = LITC . toIT
listWithLIT :: ItemTypeable a => a -> [b] -> [LITC b]
listWithLIT = map . 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 _ = TS pretty 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 bs = runReader (toitem bs) $ getTransState bs
instance (GetRange b, GetRange s, FormExtension f)
=> ItemConvertible (BASIC_SPEC b s f) (Reader (TS b s f)) where
toitem (Basic_spec l) = do
l' <- listFromAL l
return rootItem { items = l' }
instance (GetRange b, GetRange s, FormExtension f)
=> ItemConvertible (BASIC_ITEMS b s f) (Reader (TS b s f)) where
toitem bi = let rg = getRangeSpan bi in
case bi of
Sig_items s -> toitem s
Var_items l _ -> mkItemM "Var_items" rg $ listFromL l
Axiom_items al _ -> mkItemM "Axiom_items" rg $ listFromAL al
Local_var_axioms vl fl _ ->
mkItemMM "Local_var_axioms" rg
[fromL "VAR_DECLS" vl, fromAL "FORMULAS" fl]
Sort_gen asis _ -> mkItemM "Sort_gen" rg $ listFromAL asis
Free_datatype sk adtds _ ->
mkItemM ("Free_datatype", "SortsKind", show sk) rg
$ listFromAL adtds
Ext_BASIC_ITEMS b -> do
st <- ask
fromPrinter (fB st) "Ext_BASIC_ITEMS" b
instance (GetRange s, FormExtension f)
=> ItemConvertible (SIG_ITEMS s f) (Reader (TS b s f)) where
toitem si = let rg = getRangeSpan si in
case si of
Sort_items sk sis _ ->
mkItemM ("Sort_items", "SortsKind", show sk) rg
$ listFromAL sis
Op_items aois _ -> mkItemM "Op_items" rg $ listFromAL aois
Pred_items apis _ -> mkItemM "Pred_items" rg $ listFromAL apis
Datatype_items sk adds _ ->
mkItemM ("Datatype_items", "SortsKind", show sk) rg
$ listFromAL adds
Ext_SIG_ITEMS s -> do
st <- ask
fromPrinter (fS st) "Ext_SIG_ITEMS" s
instance FormExtension f
=> ItemConvertible (SORT_ITEM f) (Reader (TS b s f)) where
toitem si = let rg = getRangeSpan si in
case si of
Sort_decl l _ -> mkItemM "Sort_decl" rg $ listFromL
$ listWithLIT "SORT" l
Subsort_decl sl s _ -> mkItemMM "Subsort_decl" rg
[ fromL "SORTS" $ listWithLIT "SORT" sl
, fromC $ withLIT "SORT" s]
Subsort_defn s v s' f _ ->
mkItemMM "Subsort_defn" rg
[ fromC $ withLIT "SORT" s, fromC $ withLIT "VAR" v
, fromC $ withLIT "SORT" s', fromAC f]
Iso_decl l _ -> mkItemM "Iso_decl" rg $ listFromL
$ listWithLIT "SORT" l
instance FormExtension f
=> ItemConvertible (OP_ITEM f) (Reader (TS b s f)) where
toitem oi = let rg = getRangeSpan oi in
case oi of
Op_decl onl ot oal _ ->
mkItemMM "Op_decl" rg
[ fromL "OP_NAMES" $ listWithLIT "OP_NAME" onl, fromC ot
, fromL "OP_ATTRIBS" oal]
Op_defn on oh at _ ->
mkItemMM "Op_defn" rg [ fromC $ withLIT "OP_NAME" on, fromC oh
, fromAC at]
instance FormExtension f
=> ItemConvertible (PRED_ITEM f) (Reader (TS b s f)) where
toitem p = let rg = getRangeSpan p in
case p of
Pred_decl pnl pt _ ->
mkItemMM "Pred_decl" rg
[fromL "PRED_NAMES" $ listWithLIT "PRED_NAME" pnl, fromC pt]
Pred_defn pn ph af _ ->
mkItemMM "Pred_defn" rg [ fromC $ withLIT "PRED_NAME" pn, fromC ph
, fromAC af]
-------------------- not further expanded --------------------
fromPrinterWithRg :: (Monad m, GetRange a) =>
(a -> Doc) -> String -> a -> m Item
fromPrinterWithRg = fromPrinterWithRange getRangeSpan
fromPrinterWithRange
:: Monad m => (a -> Range) -> (a -> Doc) -> String -> a -> m Item
fromPrinterWithRange r p n o = mkItemMM (n, p o) (r o) []
fromPrinter :: Monad m => (a -> Doc) -> String -> a -> m Item
fromPrinter p n o = mkItemMM (n, p o) nullRange []
litFromPrinterWithRg :: (Monad m, GetRange a) =>
(a -> Doc) -> LITC a -> m Item
litFromPrinterWithRg p (LITC (IT l attrs _) o) =
mkItemMM (IT l attrs $ Just $ p o) (getRangeSpan o) []
instance ItemConvertible OP_TYPE (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "OP_TYPE"
instance ItemConvertible OP_HEAD (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "OP_HEAD"
instance FormExtension f
=> ItemConvertible (OP_ATTR f) (Reader (TS b s f)) where
toitem = fromPrinter printAttr "OP_ATTR"
instance ItemConvertible PRED_TYPE (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "PRED_TYPE"
instance ItemConvertible PRED_HEAD (Reader (TS b s f)) where
toitem = fromPrinterWithRg printPredHead "PRED_HEAD"
instance ItemConvertible DATATYPE_DECL (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "DATATYPE_DECL"
instance ItemConvertible VAR_DECL (Reader (TS b s f)) where
toitem = fromPrinterWithRg pretty "VAR_DECL"
instance FormExtension f
=> ItemConvertible (FORMULA f) (Reader (TS b s f)) where
toitem = fromPrinterWithRange getRangeSpan printFormula "FORMULA"
instance FormExtension f => ItemConvertible (TERM f) (Reader (TS b s f)) where
toitem = fromPrinterWithRange getRangeSpan printTerm "TERM"
instance ItemConvertible (LITC Id) (Reader (TS b s f)) where
toitem = litFromPrinterWithRg pretty
instance ItemConvertible (LITC Token) (Reader (TS b s f)) where
toitem = litFromPrinterWithRg pretty