{- |
Module      :  $Header$
Description :  read and write ATerms to and from strings
Copyright   :  (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports ATerm.AbstractSyntax)

convert 'ATermTable's (created by 'ATerm.Conversion.toATermTable') from
  'String's and to 'SDoc's as shared (TAF format) or unshared (AT format).
  Indices (following hash marks) are base64 encoded.
-}

module ATerm.ReadWrite(
    -- * read shared or unshared ATerms
      readATerm
    , readATermFile
    -- * writing out shared ATerms (use these functions for serialization)
    , writeSharedATerm
    , writeSharedATermFile
    -- * writing out unshared ATerms (just for compatibility purposes)
    , writeATerm
    , writeATermFile
    -- * support different renderings via 'ATerm.SimpPretty.SDoc'
    , writeSharedATermSDoc
    , writeATermSDoc
    ) where

{-
        Author: Joost Visser, CWI, 2002
        Changed by: Klaus Luettich & Felix Reckers, 2002-2003, C. Maeder 2005

        This module contains functions for reading and writing ATerms
        from and to Strings. Two ATerm formats are supported:

                AT:     plain (non-shared) textual ATerms
                TAF:    shared textual ATerms

        The binary ATerm format (BAF) is not supported.

        Current limitations:

                BLOBS and place-holders are not supported.

        accidental support for the empty aterm: ShAAppl "" [] []
-}

import ATerm.AbstractSyntax
import ATerm.SimpPretty
import ATerm.Base64
import Data.Char
import qualified Data.IntMap as IntMap

readATermFile :: FilePath -> IO ATermTable
readATermFile fp = do
  str <- readFile fp
  if null str then error $ "ATerm.readATermFile: empty input file: " ++ fp
     else return $ readATerm str

--- From String to ATerm ------------------------------------------------------

data ReadTAFStruct = RTS
    ATermTable
    String -- remaing string
    (AbbrevTable Int)
    Int -- string length of last ATerm read

{- | create an ATerm table from an input string. Shared or unshared ATerms can
be read. A string for shared ATerms usually starts with an exclamation mark
and contains many hash marks indicating references. Unshared ATerms are plain
constructor terms.  -}
readATerm :: String -> ATermTable
readATerm = readATerm' . dropWhile ( \ c -> case c of
    '!' -> True
    _ -> isSpace c)

readATerm' :: String -> ATermTable
readATerm' str =
    case readTAF emptyATermTable str emptyATab of
    (RTS at rt _ _, _) -> case dropSpaces rt of
       [] -> toReadonlyATT at
       s -> error $ "garbage following aterm: " ++ take 10 s

-- non-shared is a special case of shared (but could be made more fool proof)

readTAF :: ATermTable -> String -> AbbrevTable Int -> (ReadTAFStruct, Int)
readTAF at str tbl = case readTAF' at str tbl of
    (rs@(RTS at' str' tbl' l'), eith) -> case eith of
        Left i -> (rs, i)
        Right a -> case addATerm a at' of
            (at'', i) ->
                (RTS at'' str' (insertATab l' (sizeATab tbl') i tbl') l', i)

readTAF' :: ATermTable -> String -> AbbrevTable Int
         -> (ReadTAFStruct, Either Int ShATerm)
readTAF' at str tbl = case str of
  '#' : xs -> case spanAbbrevChar xs of
      (i, str') -> case lookupATab (deAbbrev i) tbl of
          Nothing -> error $ "unknown aterm index " ++ '#' : i
          Just a -> (RTS at str' tbl $ length i + 1, Left a)
  '[' : _ -> case readParTAFs '[' ']' at str tbl 0 of
      (RTS at' str'  tbl'  l', kids) ->
          case readAnnTAF at' (dropSpaces str') tbl' l' of
            (rs, ann) -> (rs, Right $ ShAList kids ann)
  x : xs | isIntHead x -> case span isDigit xs of
      (i, str') -> let (intl, l') = readInteger $ x : i in
          case readAnnTAF at (dropSpaces str') tbl l' of
            (rs, ann) -> (rs, Right $ ShAInt intl ann)
  _ -> case readAFun str of
      (c, str') -> case readParenTAFs at (dropSpaces str') tbl $ length c of
          (RTS at' str'' tbl' l', kids) ->
              case readAnnTAF at' (dropSpaces str'') tbl' l' of
                (rs, ann) -> (rs, Right $ ShAAppl c kids ann)

readParenTAFs :: ATermTable -> String -> AbbrevTable Int -> Int
              -> (ReadTAFStruct, [Int])
readParenTAFs = readParTAFs '(' ')'

readParTAFs :: Char -> Char -> ATermTable -> String -> AbbrevTable Int -> Int
              -> (ReadTAFStruct, [Int])
readParTAFs op cp at str tbl l = case str of
    p : r | op == p -> readTAFs0 at cp (dropSpaces r) tbl $ l + 1
    _ -> (RTS at str tbl l, [])

readTAFs0 :: ATermTable -> Char -> String -> AbbrevTable Int -> Int
         -> (ReadTAFStruct, [Int])
readTAFs0 at par str tbl l = case str of
    p : r | par == p -> (RTS at r tbl $ l + 1, [])
    _ -> readTAFs1 at par str tbl l

readTAFs1 :: ATermTable -> Char -> String -> AbbrevTable Int -> Int
          -> (ReadTAFStruct, [Int])
readTAFs1 at par str tbl l =
    case readTAF at (dropSpaces str) tbl of
      (RTS at' str'  tbl'  l', t) ->
          case readTAFs2 at' par (dropSpaces str') tbl' $ l + l' of
            (RTS at'' str'' tbl'' l'', ts) ->
                (RTS at'' str'' tbl'' l'', t : ts)

readTAFs2 :: ATermTable -> Char -> String -> AbbrevTable Int -> Int
          -> (ReadTAFStruct, [Int])
readTAFs2 at par str tbl l = case str of
    ',' : r -> readTAFs1 at par (dropSpaces r) tbl $ l + 1
    p : r | par == p -> (RTS at r tbl $ l + 1, [])
    _ -> error $ "expecting ',' or '" ++ [par] ++ "' in aterm but found: "
         ++ take 10 str

readAnnTAF :: ATermTable -> String -> AbbrevTable Int -> Int
           -> (ReadTAFStruct, [Int])
readAnnTAF = readParTAFs '{' '}'

-- helpers --

dropSpaces :: String -> String
dropSpaces = dropWhile isSpace

readAFun :: String -> (String, String)
readAFun str = case str of
  q : r | q == '"' -> let (c, s) = spanNotQuote' r in (q : c, s)
  _ -> span isAFunChar str

spanNotQuote' :: String -> (String, String)
spanNotQuote' str = case str of
     q : r | q == '"'  -> ([q], r)
     c : r@(d : s) -> let
         (e, l) = if c == '\\' then ([c, d], s) else ([c], r)
         (f, t) = spanNotQuote' l
         in (e ++ f, t)
     _ -> error $ "wrongly terminated aterm string: " ++ take 10 str

isAFunChar :: Char -> Bool
isAFunChar c = isAlphaNum c || c `elem` "_*+-."

spanAbbrevChar :: String -> (String, String)
spanAbbrevChar = span isBase64Char

isIntHead :: Char -> Bool
isIntHead c = isDigit c || c == '-'

--- From (shared) ATerms to strings via simple documents with associated length

data DocLen = DocLen SDoc Int

data WriteStruct = WS (AbbrevTable DocLen) DocLen

writeATermSDoc :: ATermTable -> SDoc
writeATermSDoc = writeSharedATermSDoc' False

writeATerm :: ATermTable -> String
writeATerm = render . writeATermSDoc

writeATermFile :: FilePath -> ATermTable -> IO ()
writeATermFile fp = writeFileSDoc fp . writeATermSDoc

writeSharedATermSDoc :: ATermTable -> SDoc
writeSharedATermSDoc = writeSharedATermSDoc' True

writeSharedATerm :: ATermTable -> String
writeSharedATerm = render . writeSharedATermSDoc

writeSharedATermFile :: FilePath -> ATermTable -> IO ()
writeSharedATermFile fp = writeFileSDoc fp . writeSharedATermSDoc

writeSharedATermSDoc' :: Bool -> ATermTable -> SDoc
writeSharedATermSDoc' b at =
    case writeTAF b (toReadonlyATT at) emptyATab of
    WS _ (DocLen doc _) -> (if b then text "!" else empty) <> doc

--shared (if input is True)

writeTAF :: Bool -> ATermTable -> AbbrevTable DocLen -> WriteStruct
writeTAF b at tbl = let i = getTopIndex at in
    case lookupATab i tbl of
    Just s -> if b then WS tbl s else writeTAF' b at tbl
    Nothing  -> case writeTAF' b at tbl of
        WS tbl' d_len@(DocLen _ len) ->
            WS (insertATab len i (abbrevD $ sizeATab tbl') tbl') d_len

writeTAF' :: Bool -> ATermTable -> AbbrevTable DocLen -> WriteStruct
writeTAF' b at tbl = case getATerm at of
    ShAAppl c ts anns -> case writeTAFs b at ts tbl of
        WS tbl' kids -> case writeTAFs b at anns tbl' of
            WS tbl'' kidsAnn -> WS tbl'' $ dlConcat (writeATermAuxS c kids)
                                $ parenthesiseAnnS kidsAnn
    ShAList ts anns -> case writeTAFs b at ts tbl of
        WS tbl' kids -> case writeTAFs b at anns tbl' of
            WS tbl'' kidsAnn -> WS tbl'' $ dlConcat (bracketS kids)
                                $ parenthesiseAnnS kidsAnn
    ShAInt i anns -> case writeTAFs b at anns tbl of
        WS tbl' kidsAnn -> WS tbl' $ dlConcat (integerDoc i)
                           $ parenthesiseAnnS kidsAnn

dlConcat :: DocLen -> DocLen -> DocLen
dlConcat s1@(DocLen sf1 sl1) s2@(DocLen sf2 sl2)
    | sl1 == 0 = s2
    | sl2 == 0 = s1
    | otherwise = DocLen (sf1 <> sf2) $ sl1 + sl2

dlConcatComma :: DocLen -> DocLen -> DocLen
dlConcatComma (DocLen sf1 sl1) (DocLen sf2 sl2) =
    DocLen (sf1 <> comma <> sf2) $ sl1 + sl2 + 1

-- produce comma seperated output from aterm indices
writeTAFs :: Bool -> ATermTable -> [Int] -> AbbrevTable DocLen -> WriteStruct
writeTAFs b at inds tbl = case inds of
    [] -> WS tbl $ DocLen empty 0
    i : is -> case writeTAF b (getATermByIndex1 i at) tbl of
              ws@(WS t1 s1) -> if null is then ws
                else case writeTAFs b at is t1 of
                       WS t2 s2 -> WS t2 $ dlConcatComma s1 s2

docLen :: String -> DocLen
docLen s = DocLen (text s) $ length s

integerDoc :: Integer -> DocLen
integerDoc = docLen . show

writeATermAuxS :: String -> DocLen -> DocLen
writeATermAuxS s = dlConcat (docLen s) . parenthesiseS

-- list brackets must not be omitted
bracketS :: DocLen -> DocLen
bracketS         (DocLen d dl)
    | dl == 0 = docLen "[]"
    | otherwise = DocLen (brackets d) $ dl + 2

parenthesiseS :: DocLen -> DocLen
parenthesiseS    s@(DocLen d dl)
    | dl == 0 = s
    | otherwise = DocLen (parens d) $ dl + 2

parenthesiseAnnS :: DocLen -> DocLen
parenthesiseAnnS s@(DocLen d dl)
    | dl == 0 = s
    | otherwise = DocLen (braces d) $ dl + 2

{- | This abbreviation table maps abbreviation ints to aterm indices for
     reading and aterm indices to abbreviation docs during writing. -}
data AbbrevTable a = ATab !(IntMap.IntMap a) !(Int, Int) !Int

{- The last component is the current maximal abbreviation int that
serves as a key when reading and as a value when writing. The pair
stores the size of this component and the maximal power of 64
that is less than it, in order to simplify the computation of the size
of the next abbreviation int. -}

-- | initial table
emptyATab :: AbbrevTable a
emptyATab = ATab IntMap.empty (2, 64) 0

-- | only insert if the first argument is greater than the abbreviation size
insertATab :: Int -> Int -> a -> AbbrevTable a -> AbbrevTable a
insertATab dl i a t@(ATab m p@(sl, b) s) =
    if dl > sl then let n = s + 1 in
        ATab (IntMap.insert i a m)
           (if rem n b == 0 then (sl + 1, 64 * b) else p) n
    else t

-- | get current abbreviation size
sizeATab :: AbbrevTable a -> Int
sizeATab (ATab _ _ s) = s

-- | lookup map value
lookupATab :: Int -> AbbrevTable a -> Maybe a
lookupATab i (ATab m _ _) = IntMap.lookup i m

--- Intger Read ---------------------------------------------------------------

readInteger :: String -> (Integer, Int)
readInteger s = case s of
                  (hd:str) -> if hd == '-' then case conv str of
                         (m, l) -> (negate m, l + 1)
                         else conv s
                  _ -> error "readInteger"
    where f (m, l) x = (toInteger (ord x - ord0) + 10 * m, l + 1)
          conv = foldl f (0, 0)

--- Base 64 encoding ----------------------------------------------------------

abbrevD :: Int -> DocLen
abbrevD = docLen . abbrev

abbrev :: Int -> String
abbrev i = '#' : mkAbbrev i

mkAbbrev :: Int -> String
mkAbbrev x = if x > 0 then mkAbbrevAux x "" else "A"

mkAbbrevAux :: Int -> String -> String
mkAbbrevAux x str =
  if x > 0 then case quotRem x 64 of
         (d, m) -> mkAbbrevAux d $ toBase64Char m : str
  else str

deAbbrev :: String -> Int
deAbbrev = let f m c = 64 * m + toBase64Int c in foldl f 0