1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./LF/AS.hs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaDescription : Abstract syntax for the Edinburgh Logical Framework

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2010

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaStability : experimental

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaPortability : portable

99c3239092cab05eaca2f021e5edef2eab00ba01Christian Maeder

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-}

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovamodule LF.AS

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova ( BASIC_SPEC (..)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , BASIC_ITEM (..)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , SYMB_ITEMS (..)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , SYMB_MAP_ITEMS (..)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , SYMB_OR_MAP (..)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova ) where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.AS_Annotation

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Id

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.DocUtils

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Data.Data

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- grammar for basic specs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovadata BASIC_SPEC = Basic_spec [Annoted BASIC_ITEM]

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance GetRange BASIC_SPEC

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovadata BASIC_ITEM = Decl String

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova | Form String

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- grammar for symbols and symbol maps

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovadata SYMB_ITEMS = Symb_items [String]

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Typeable)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovadata SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP]

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Typeable)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovadata SYMB_OR_MAP = Symb String

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova | Symb_map String String

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Typeable)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- pretty printing

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty BASIC_SPEC where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty = printBasicSpec

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty BASIC_ITEM where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty = printBasicItem

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty SYMB_ITEMS where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty = printSymbItems

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty SYMB_MAP_ITEMS where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty = printSymbMapItems

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovainstance Pretty SYMB_OR_MAP where

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova pretty = printSymbOrMap

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintBasicSpec :: BASIC_SPEC -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintBasicSpec (Basic_spec xs) = vcat $ map pretty xs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintBasicItem :: BASIC_ITEM -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintBasicItem (Decl d) = pretty d <> dot

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintBasicItem (Form f) = dot <+> pretty f

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbItems :: SYMB_ITEMS -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbItems (Symb_items xs) = ppWithCommas xs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbMapItems (Symb_map_items xs) = ppWithCommas xs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbOrMap :: SYMB_OR_MAP -> Doc

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbOrMap (Symb s) = pretty s

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaprintSymbOrMap (Symb_map s t) = pretty s <+> mapsto <+> pretty t