{- |
Module      :  ./Common/SExpr.hs
Description :  S-Expressions as intermediate output format
Copyright   :  (c) E. Schulz, D. Dietrich, C. Maeder, DFKI 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

S-Expressions for the translation from HasCASL, CASL and VSE to OMDoc
-}

module Common.SExpr
  ( SExpr (..)
  , prettySExpr
  , idToSSymbol
  , transToken
  , transString
  ) where

import Common.Doc
import Common.Id
import Common.LibName
import Common.ProofUtils
import qualified Data.Map as Map
import Data.Char

data SExpr = SSymbol String | SList [SExpr] deriving (SExpr -> SExpr -> Bool
(SExpr -> SExpr -> Bool) -> (SExpr -> SExpr -> Bool) -> Eq SExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SExpr -> SExpr -> Bool
$c/= :: SExpr -> SExpr -> Bool
== :: SExpr -> SExpr -> Bool
$c== :: SExpr -> SExpr -> Bool
Eq, Eq SExpr
Eq SExpr =>
(SExpr -> SExpr -> Ordering)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> Bool)
-> (SExpr -> SExpr -> SExpr)
-> (SExpr -> SExpr -> SExpr)
-> Ord SExpr
SExpr -> SExpr -> Bool
SExpr -> SExpr -> Ordering
SExpr -> SExpr -> SExpr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SExpr -> SExpr -> SExpr
$cmin :: SExpr -> SExpr -> SExpr
max :: SExpr -> SExpr -> SExpr
$cmax :: SExpr -> SExpr -> SExpr
>= :: SExpr -> SExpr -> Bool
$c>= :: SExpr -> SExpr -> Bool
> :: SExpr -> SExpr -> Bool
$c> :: SExpr -> SExpr -> Bool
<= :: SExpr -> SExpr -> Bool
$c<= :: SExpr -> SExpr -> Bool
< :: SExpr -> SExpr -> Bool
$c< :: SExpr -> SExpr -> Bool
compare :: SExpr -> SExpr -> Ordering
$ccompare :: SExpr -> SExpr -> Ordering
$cp1Ord :: Eq SExpr
Ord, Int -> SExpr -> ShowS
[SExpr] -> ShowS
SExpr -> String
(Int -> SExpr -> ShowS)
-> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SExpr] -> ShowS
$cshowList :: [SExpr] -> ShowS
show :: SExpr -> String
$cshow :: SExpr -> String
showsPrec :: Int -> SExpr -> ShowS
$cshowsPrec :: Int -> SExpr -> ShowS
Show)

prettySExpr :: SExpr -> Doc
prettySExpr :: SExpr -> Doc
prettySExpr sexpr :: SExpr
sexpr = case SExpr
sexpr of
  SSymbol s :: String
s -> String -> Doc
text String
s
  SList l :: [SExpr]
l -> Doc -> Doc
parens (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SExpr -> Doc) -> [SExpr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> Doc
prettySExpr [SExpr]
l

-- | transform an overloaded identifier
idToSSymbol :: Int -> Id -> SExpr
idToSSymbol :: Int -> Id -> SExpr
idToSSymbol n :: Int
n i :: Id
i = String -> SExpr
SSymbol
  (String -> SExpr) -> String -> SExpr
forall a b. (a -> b) -> a -> b
$ Id -> ShowS
transQualId Id
i ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then ShowS
forall a. a -> a
id else String -> ShowS
showString "_O" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
n) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ""

transQualId :: Id -> ShowS
transQualId :: Id -> ShowS
transQualId = Id -> ShowS
transId (Id -> ShowS) -> (Id -> Id) -> Id -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Id
unQualName

transId :: Id -> ShowS
transId :: Id -> ShowS
transId (Id ts :: [Token]
ts cs :: [Id]
cs _) =
    ShowS -> (Token -> ShowS) -> [Token] -> ShowS
forall a. ShowS -> (a -> ShowS) -> [a] -> ShowS
showSepList ShowS
forall a. a -> a
id (String -> ShowS
showString (String -> ShowS) -> (Token -> String) -> Token -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
transToken) [Token]
ts ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
cs then ShowS
forall a. a -> a
id else
    String -> ShowS
showString "{" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> (Id -> ShowS) -> [Id] -> ShowS
forall a. ShowS -> (a -> ShowS) -> [a] -> ShowS
showSepList (String -> ShowS
showString "-") Id -> ShowS
transId [Id]
cs
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString "}"

transToken :: Token -> String
transToken :: Token -> String
transToken t :: Token
t = if Token -> Bool
isPlace Token
t then "_2" else ShowS
transString ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Token -> String
tokStr Token
t

transStringAux :: String -> String
transStringAux :: ShowS
transStringAux = (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: Char
c -> String -> Char -> Map Char String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [Char
c] Char
c Map Char String
cMap)

transString :: String -> String
transString :: ShowS
transString s :: String
s = case String
s of
  c :: Char
c : r :: String
r | Char -> Bool
isDigit Char
c -> "_D" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
transStringAux String
r
  _ -> ShowS
transStringAux String
s

cMap :: Map.Map Char String
cMap :: Map Char String
cMap = ShowS -> Map Char String -> Map Char String
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ('_' Char -> ShowS
forall a. a -> [a] -> [a]
:) (Map Char String -> Map Char String)
-> Map Char String -> Map Char String
forall a b. (a -> b) -> a -> b
$ Char -> String -> Map Char String -> Map Char String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert '_' "1" Map Char String
charMap