{-# LANGUAGE CPP #-}
module ATerm.ReadWrite (
readATerm
, readATermFile
, writeSharedATerm
, writeSharedATermFile
, writeATerm
, writeATermFile
, writeSharedATermSDoc
, writeATermSDoc
) where
#if __GLASGOW_HASKELL__ >= 803
import Prelude hiding ((<>))
#endif
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
data ReadTAFStruct = RTS
ATermTable
String
(AbbrevTable Int)
Int
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
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 '{' '}'
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 == '-'
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
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
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
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
data AbbrevTable a = ATab !(IntMap.IntMap a) !(Int, Int) !Int
emptyATab :: AbbrevTable a
emptyATab = ATab IntMap.empty (2, 64) 0
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
sizeATab :: AbbrevTable a -> Int
sizeATab (ATab _ _ s) = s
lookupATab :: Int -> AbbrevTable a -> Maybe a
lookupATab i (ATab m _ _) = IntMap.lookup i m
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)
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