hets/CASL/ToItem.hs

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