--------------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Safe #-}

-- | A representation for structured expression trees, with support for pretty
-- printing and for parsing.
module Copilot.Theorem.Misc.SExpr where

import Text.ParserCombinators.Parsec
import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)

import Control.Monad

--------------------------------------------------------------------------------

-- | A structured expression is either an atom, or a sequence of expressions,
-- where the first in the sequence denotes the tag or label of the tree.
data SExpr a = Atom a
             | List [SExpr a]

-- | Empty string expression.
blank :: SExpr [Char]
blank = [Char] -> SExpr [Char]
forall a. a -> SExpr a
Atom [Char]
""

-- | Atomic expression constructor.
atom :: a -> SExpr a
atom = a -> SExpr a
forall a. a -> SExpr a
Atom                 -- s

-- | Empty expression (empty list).
unit :: SExpr a
unit = [SExpr a] -> SExpr a
forall a. [SExpr a] -> SExpr a
List []              -- ()

-- | Single expression.
singleton :: a -> SExpr a
singleton a
a  = [SExpr a] -> SExpr a
forall a. [SExpr a] -> SExpr a
List [a -> SExpr a
forall a. a -> SExpr a
Atom a
a]        -- (s)

-- | Sequence of expressions.
list :: [SExpr a] -> SExpr a
list = [SExpr a] -> SExpr a
forall a. [SExpr a] -> SExpr a
List                 -- (ss)

-- | Sequence of expressions with a root or main note, and a series of
-- additional expressions or arguments..
node :: a -> [SExpr a] -> SExpr a
node a
a [SExpr a]
l = [SExpr a] -> SExpr a
forall a. [SExpr a] -> SExpr a
List (a -> SExpr a
forall a. a -> SExpr a
Atom a
a SExpr a -> [SExpr a] -> [SExpr a]
forall a. a -> [a] -> [a]
: [SExpr a]
l)    -- (s ss)

--------------------------------------------------------------------------------

-- A straightforward string representation for 'SExpr's of Strings that
-- parenthesizes lists of expressions.
instance Show (SExpr String) where
  show :: SExpr [Char] -> [Char]
show = Doc -> [Char]
PP.render (Doc -> [Char]) -> (SExpr [Char] -> Doc) -> SExpr [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr [Char] -> Doc
show'
    where
      show' :: SExpr [Char] -> Doc
show' (Atom [Char]
s) = [Char] -> Doc
text [Char]
s
      show' (List [SExpr [Char]]
ts) = Doc -> Doc
parens (Doc -> Doc) -> ([SExpr [Char]] -> Doc) -> [SExpr [Char]] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> Doc)
-> ([SExpr [Char]] -> [Doc]) -> [SExpr [Char]] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SExpr [Char] -> Doc) -> [SExpr [Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SExpr [Char] -> Doc
show' ([SExpr [Char]] -> Doc) -> [SExpr [Char]] -> Doc
forall a b. (a -> b) -> a -> b
$ [SExpr [Char]]
ts


-- More advanced printing with some basic indentation

-- | Indent by a given number.
indent :: Doc -> Doc
indent = Int -> Doc -> Doc
nest Int
1

-- | Pretty print a structured expression as a String.
toString :: (SExpr a -> Bool)  -- ^ True if an expression should be indented.
         -> (a -> String)      -- ^ Pretty print the value inside as 'SExpr'.
         -> SExpr a            -- ^ Root of 'SExpr' tree.
         -> String
toString :: (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> [Char]
toString SExpr a -> Bool
shouldIndent a -> [Char]
printAtom SExpr a
expr =
  Doc -> [Char]
PP.render ((SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
forall a. (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> [Char]
printAtom SExpr a
expr)

-- | Pretty print a structured expression as a 'Doc', or set of layouts.
toDoc :: (SExpr a -> Bool)  -- ^ True if an expression should be indented.
      -> (a -> String)      -- ^ Pretty print the value inside as 'SExpr'.
      -> SExpr a            -- ^ Root of 'SExpr' tree.
      -> Doc
toDoc :: (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> [Char]
printAtom SExpr a
expr = case SExpr a
expr of
  Atom a
a  -> [Char] -> Doc
text (a -> [Char]
printAtom a
a)
  List [SExpr a]
l  -> Doc -> Doc
parens ((Doc -> SExpr a -> Doc) -> Doc -> [SExpr a] -> Doc
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Doc -> SExpr a -> Doc
renderItem Doc
empty [SExpr a]
l)

  where renderItem :: Doc -> SExpr a -> Doc
renderItem Doc
doc SExpr a
s
          | SExpr a -> Bool
shouldIndent SExpr a
s =
            Doc
doc Doc -> Doc -> Doc
$$ Doc -> Doc
indent ((SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
forall a. (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> [Char]
printAtom SExpr a
s)
          | Bool
otherwise =
            Doc
doc Doc -> Doc -> Doc
<+> (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
forall a. (SExpr a -> Bool) -> (a -> [Char]) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> [Char]
printAtom SExpr a
s

--------------------------------------------------------------------------------

-- | Parser for strings of characters separated by spaces into a structured
-- tree.
--
-- Parentheses are interpreted as grouping elements, that is, defining a
-- 'List', which may be empty.
parser :: GenParser Char st (SExpr String)
parser :: GenParser Char st (SExpr [Char])
parser =
  [GenParser Char st (SExpr [Char])]
-> GenParser Char st (SExpr [Char])
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice [GenParser Char st (SExpr [Char])
-> GenParser Char st (SExpr [Char])
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st (SExpr [Char])
forall u a. ParsecT [Char] u Identity (SExpr a)
unitP, GenParser Char st (SExpr [Char])
forall u. ParsecT [Char] u Identity (SExpr [Char])
nodeP, GenParser Char st (SExpr [Char])
forall u. ParsecT [Char] u Identity (SExpr [Char])
leafP]

  where symbol :: ParsecT [Char] u Identity Char
symbol     = [Char] -> ParsecT [Char] u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf [Char]
"!#$%&|*+-/:<=>?@^_~."
        lonelyStr :: ParsecT [Char] u Identity [Char]
lonelyStr  = ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT [Char] u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT [Char] u Identity Char
-> ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] u Identity Char
forall u. ParsecT [Char] u Identity Char
symbol)

        unitP :: ParsecT [Char] u Identity (SExpr a)
unitP      = [Char] -> ParsecT [Char] u Identity [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string [Char]
"()" ParsecT [Char] u Identity [Char]
-> ParsecT [Char] u Identity (SExpr a)
-> ParsecT [Char] u Identity (SExpr a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SExpr a -> ParsecT [Char] u Identity (SExpr a)
forall (m :: * -> *) a. Monad m => a -> m a
return SExpr a
forall a. SExpr a
unit

        leafP :: ParsecT [Char] u Identity (SExpr [Char])
leafP      = [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom ([Char] -> SExpr [Char])
-> ParsecT [Char] u Identity [Char]
-> ParsecT [Char] u Identity (SExpr [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT [Char] u Identity [Char]
forall u. ParsecT [Char] u Identity [Char]
lonelyStr

        nodeP :: ParsecT [Char] u Identity (SExpr [Char])
nodeP      = do ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ())
-> ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT [Char] u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'('
                        ParsecT [Char] u Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
                        [SExpr [Char]]
st <- ParsecT [Char] u Identity (SExpr [Char])
-> ParsecT [Char] u Identity ()
-> ParsecT [Char] u Identity [SExpr [Char]]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT [Char] u Identity (SExpr [Char])
forall u. ParsecT [Char] u Identity (SExpr [Char])
parser ParsecT [Char] u Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
                        ParsecT [Char] u Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
                        ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ())
-> ParsecT [Char] u Identity Char -> ParsecT [Char] u Identity ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT [Char] u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
                        SExpr [Char] -> ParsecT [Char] u Identity (SExpr [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr [Char] -> ParsecT [Char] u Identity (SExpr [Char]))
-> SExpr [Char] -> ParsecT [Char] u Identity (SExpr [Char])
forall a b. (a -> b) -> a -> b
$ [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
List [SExpr [Char]]
st

-- | Parser for strings of characters separated by spaces into a structured
-- tree.
--
-- Parentheses are interpreted as grouping elements, that is, defining a
-- 'List', which may be empty.
parseSExpr :: String -> Maybe (SExpr String)
parseSExpr :: [Char] -> Maybe (SExpr [Char])
parseSExpr [Char]
str = case Parsec [Char] () (SExpr [Char])
-> [Char] -> [Char] -> Either ParseError (SExpr [Char])
forall s t a.
Stream s Identity t =>
Parsec s () a -> [Char] -> s -> Either ParseError a
parse Parsec [Char] () (SExpr [Char])
forall u. ParsecT [Char] u Identity (SExpr [Char])
parser [Char]
"" [Char]
str of
  Left ParseError
s -> [Char] -> Maybe (SExpr [Char])
forall a. HasCallStack => [Char] -> a
error (ParseError -> [Char]
forall a. Show a => a -> [Char]
show ParseError
s) -- Nothing
  Right SExpr [Char]
t -> SExpr [Char] -> Maybe (SExpr [Char])
forall a. a -> Maybe a
Just SExpr [Char]
t

--------------------------------------------------------------------------------