{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.Misc.SExpr where
import Text.ParserCombinators.Parsec
import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)
import Control.Monad
data SExpr a = Atom a
| List [SExpr a]
blank :: SExpr String
blank = forall a. a -> SExpr a
Atom String
""
atom :: a -> SExpr a
atom = forall a. a -> SExpr a
Atom
unit :: SExpr a
unit = forall a. [SExpr a] -> SExpr a
List []
singleton :: a -> SExpr a
singleton a
a = forall a. [SExpr a] -> SExpr a
List [forall a. a -> SExpr a
Atom a
a]
list :: [SExpr a] -> SExpr a
list = forall a. [SExpr a] -> SExpr a
List
node :: a -> [SExpr a] -> SExpr a
node a
a [SExpr a]
l = forall a. [SExpr a] -> SExpr a
List (forall a. a -> SExpr a
Atom a
a forall a. a -> [a] -> [a]
: [SExpr a]
l)
instance Show (SExpr String) where
show :: SExpr String -> String
show = Doc -> String
PP.render forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr String -> Doc
show'
where
show' :: SExpr String -> Doc
show' (Atom String
s) = String -> Doc
text String
s
show' (List [SExpr String]
ts) = Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map SExpr String -> Doc
show' forall a b. (a -> b) -> a -> b
$ [SExpr String]
ts
indent :: Doc -> Doc
indent = Int -> Doc -> Doc
nest Int
1
toString :: (SExpr a -> Bool)
-> (a -> String)
-> SExpr a
-> String
toString :: forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String
toString SExpr a -> Bool
shouldIndent a -> String
printAtom SExpr a
expr =
Doc -> String
PP.render (forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> String
printAtom SExpr a
expr)
toDoc :: (SExpr a -> Bool)
-> (a -> String)
-> SExpr a
-> Doc
toDoc :: forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> String
printAtom SExpr a
expr = case SExpr a
expr of
Atom a
a -> String -> Doc
text (a -> String
printAtom a
a)
List [SExpr a]
l -> Doc -> Doc
parens (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 (forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> String
printAtom SExpr a
s)
| Bool
otherwise =
Doc
doc Doc -> Doc -> Doc
<+> forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc
toDoc SExpr a -> Bool
shouldIndent a -> String
printAtom SExpr a
s
parser :: GenParser Char st (SExpr String)
parser :: forall st. GenParser Char st (SExpr String)
parser =
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice [forall tok st a. GenParser tok st a -> GenParser tok st a
try forall {u} {a}. ParsecT String u Identity (SExpr a)
unitP, forall st. GenParser Char st (SExpr String)
nodeP, forall st. GenParser Char st (SExpr String)
leafP]
where
symbol :: ParsecT String u Identity Char
symbol = forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
"!#$%&|*+-/:<=>?@^_~."
lonelyStr :: ParsecT String u Identity String
lonelyStr = forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall {u}. ParsecT String u Identity Char
symbol)
unitP :: ParsecT String u Identity (SExpr a)
unitP = forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"()" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall {a}. SExpr a
unit
leafP :: ParsecT String u Identity (SExpr String)
leafP = forall a. a -> SExpr a
atom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {u}. ParsecT String u Identity String
lonelyStr
nodeP :: ParsecT String u Identity (SExpr String)
nodeP = do forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'('
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
[SExpr String]
st <- 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 forall st. GenParser Char st (SExpr String)
parser forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [SExpr a] -> SExpr a
List [SExpr String]
st
parseSExpr :: String -> Maybe (SExpr String)
parseSExpr :: String -> Maybe (SExpr String)
parseSExpr String
str = case forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse forall st. GenParser Char st (SExpr String)
parser String
"" String
str of
Left ParseError
s -> forall a. HasCallStack => String -> a
error (forall a. Show a => a -> String
show ParseError
s)
Right SExpr String
t -> forall a. a -> Maybe a
Just SExpr String
t