{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./LF/AS.hs
Description : Abstract syntax for the Edinburgh Logical Framework
Copyright : (c) Kristina Sojakova, DFKI Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : k.sojakova@jacobs-university.de
Stability : experimental
Portability : portable
-}
module LF.AS
( BASIC_SPEC (..)
, BASIC_ITEM (..)
, SYMB_ITEMS (..)
, SYMB_MAP_ITEMS (..)
, SYMB_OR_MAP (..)
) where
import Common.AS_Annotation
import Common.Id
import Common.Doc
import Common.DocUtils
import Data.Data
-- grammar for basic specs
data BASIC_SPEC = Basic_spec [Annoted BASIC_ITEM]
deriving (Show, Typeable)
instance GetRange BASIC_SPEC
data BASIC_ITEM = Decl String
| Form String
deriving (Show, Typeable)
-- grammar for symbols and symbol maps
data SYMB_ITEMS = Symb_items [String]
deriving (Show, Eq, Typeable)
data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP]
deriving (Show, Eq, Typeable)
data SYMB_OR_MAP = Symb String
| Symb_map String String
deriving (Show, Eq, Typeable)
-- pretty printing
instance Pretty BASIC_SPEC where
pretty = printBasicSpec
instance Pretty BASIC_ITEM where
pretty = printBasicItem
instance Pretty SYMB_ITEMS where
pretty = printSymbItems
instance Pretty SYMB_MAP_ITEMS where
pretty = printSymbMapItems
instance Pretty SYMB_OR_MAP where
pretty = printSymbOrMap
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (Basic_spec xs) = vcat $ map pretty xs
printBasicItem :: BASIC_ITEM -> Doc
printBasicItem (Decl d) = pretty d <> dot
printBasicItem (Form f) = dot <+> pretty f
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items xs) = ppWithCommas xs
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items xs) = ppWithCommas xs
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap (Symb s) = pretty s
printSymbOrMap (Symb_map s t) = pretty s <+> mapsto <+> pretty t