{-# 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 (Int -> BASIC_SPEC -> ShowS
[BASIC_SPEC] -> ShowS
BASIC_SPEC -> String
(Int -> BASIC_SPEC -> ShowS)
-> (BASIC_SPEC -> String)
-> ([BASIC_SPEC] -> ShowS)
-> Show BASIC_SPEC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASIC_SPEC] -> ShowS
$cshowList :: [BASIC_SPEC] -> ShowS
show :: BASIC_SPEC -> String
$cshow :: BASIC_SPEC -> String
showsPrec :: Int -> BASIC_SPEC -> ShowS
$cshowsPrec :: Int -> BASIC_SPEC -> ShowS
Show, Typeable)

instance GetRange BASIC_SPEC

data BASIC_ITEM = Decl String
                | Form String
                  deriving (Int -> BASIC_ITEM -> ShowS
[BASIC_ITEM] -> ShowS
BASIC_ITEM -> String
(Int -> BASIC_ITEM -> ShowS)
-> (BASIC_ITEM -> String)
-> ([BASIC_ITEM] -> ShowS)
-> Show BASIC_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BASIC_ITEM] -> ShowS
$cshowList :: [BASIC_ITEM] -> ShowS
show :: BASIC_ITEM -> String
$cshow :: BASIC_ITEM -> String
showsPrec :: Int -> BASIC_ITEM -> ShowS
$cshowsPrec :: Int -> BASIC_ITEM -> ShowS
Show, Typeable)

-- grammar for symbols and symbol maps
data SYMB_ITEMS = Symb_items [String]
                  deriving (Int -> SYMB_ITEMS -> ShowS
[SYMB_ITEMS] -> ShowS
SYMB_ITEMS -> String
(Int -> SYMB_ITEMS -> ShowS)
-> (SYMB_ITEMS -> String)
-> ([SYMB_ITEMS] -> ShowS)
-> Show SYMB_ITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_ITEMS] -> ShowS
$cshowList :: [SYMB_ITEMS] -> ShowS
show :: SYMB_ITEMS -> String
$cshow :: SYMB_ITEMS -> String
showsPrec :: Int -> SYMB_ITEMS -> ShowS
$cshowsPrec :: Int -> SYMB_ITEMS -> ShowS
Show, SYMB_ITEMS -> SYMB_ITEMS -> Bool
(SYMB_ITEMS -> SYMB_ITEMS -> Bool)
-> (SYMB_ITEMS -> SYMB_ITEMS -> Bool) -> Eq SYMB_ITEMS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c/= :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
$c== :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
Eq, Typeable)

data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP]
                      deriving (Int -> SYMB_MAP_ITEMS -> ShowS
[SYMB_MAP_ITEMS] -> ShowS
SYMB_MAP_ITEMS -> String
(Int -> SYMB_MAP_ITEMS -> ShowS)
-> (SYMB_MAP_ITEMS -> String)
-> ([SYMB_MAP_ITEMS] -> ShowS)
-> Show SYMB_MAP_ITEMS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_MAP_ITEMS] -> ShowS
$cshowList :: [SYMB_MAP_ITEMS] -> ShowS
show :: SYMB_MAP_ITEMS -> String
$cshow :: SYMB_MAP_ITEMS -> String
showsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS
$cshowsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS
Show, SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
(SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool)
-> (SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool) -> Eq SYMB_MAP_ITEMS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
$c/= :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
== :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
$c== :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
Eq, Typeable)

data SYMB_OR_MAP = Symb String
                 | Symb_map String String
                   deriving (Int -> SYMB_OR_MAP -> ShowS
[SYMB_OR_MAP] -> ShowS
SYMB_OR_MAP -> String
(Int -> SYMB_OR_MAP -> ShowS)
-> (SYMB_OR_MAP -> String)
-> ([SYMB_OR_MAP] -> ShowS)
-> Show SYMB_OR_MAP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SYMB_OR_MAP] -> ShowS
$cshowList :: [SYMB_OR_MAP] -> ShowS
show :: SYMB_OR_MAP -> String
$cshow :: SYMB_OR_MAP -> String
showsPrec :: Int -> SYMB_OR_MAP -> ShowS
$cshowsPrec :: Int -> SYMB_OR_MAP -> ShowS
Show, SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
(SYMB_OR_MAP -> SYMB_OR_MAP -> Bool)
-> (SYMB_OR_MAP -> SYMB_OR_MAP -> Bool) -> Eq SYMB_OR_MAP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
$c/= :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
== :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
$c== :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool
Eq, Typeable)

-- pretty printing
instance Pretty BASIC_SPEC where
    pretty :: BASIC_SPEC -> Doc
pretty = BASIC_SPEC -> Doc
printBasicSpec
instance Pretty BASIC_ITEM where
    pretty :: BASIC_ITEM -> Doc
pretty = BASIC_ITEM -> Doc
printBasicItem
instance Pretty SYMB_ITEMS where
    pretty :: SYMB_ITEMS -> Doc
pretty = SYMB_ITEMS -> Doc
printSymbItems
instance Pretty SYMB_MAP_ITEMS where
    pretty :: SYMB_MAP_ITEMS -> Doc
pretty = SYMB_MAP_ITEMS -> Doc
printSymbMapItems
instance Pretty SYMB_OR_MAP where
    pretty :: SYMB_OR_MAP -> Doc
pretty = SYMB_OR_MAP -> Doc
printSymbOrMap

printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (Basic_spec xs :: [Annoted BASIC_ITEM]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEM -> Doc) -> [Annoted BASIC_ITEM] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASIC_ITEM -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted BASIC_ITEM]
xs

printBasicItem :: BASIC_ITEM -> Doc
printBasicItem :: BASIC_ITEM -> Doc
printBasicItem (Decl d :: String
d) = String -> Doc
forall a. Pretty a => a -> Doc
pretty String
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
printBasicItem (Form f :: String
f) = Doc
dot Doc -> Doc -> Doc
<+> String -> Doc
forall a. Pretty a => a -> Doc
pretty String
f

printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items xs :: [String]
xs) = [String] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [String]
xs

printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items xs :: [SYMB_OR_MAP]
xs) = [SYMB_OR_MAP] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [SYMB_OR_MAP]
xs

printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap (Symb s :: String
s) = String -> Doc
forall a. Pretty a => a -> Doc
pretty String
s
printSymbOrMap (Symb_map s :: String
s t :: String
t) = String -> Doc
forall a. Pretty a => a -> Doc
pretty String
s Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+> String -> Doc
forall a. Pretty a => a -> Doc
pretty String
t