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