module Agda.Interaction.Emacs.Lisp
( Lisp(..)
, response
, putResponse
) where
import Agda.Syntax.Common.Pretty
data Lisp a
= A a
| Cons (Lisp a) (Lisp a)
| L [Lisp a]
| Q (Lisp a)
deriving Lisp a -> Lisp a -> Bool
(Lisp a -> Lisp a -> Bool)
-> (Lisp a -> Lisp a -> Bool) -> Eq (Lisp a)
forall a. Eq a => Lisp a -> Lisp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Lisp a -> Lisp a -> Bool
== :: Lisp a -> Lisp a -> Bool
$c/= :: forall a. Eq a => Lisp a -> Lisp a -> Bool
/= :: Lisp a -> Lisp a -> Bool
Eq
instance Pretty a => Pretty (Lisp a) where
pretty :: Lisp a -> Doc
pretty (A a
a ) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
pretty (Cons Lisp a
a Lisp a
b) = Doc -> Doc
parens (Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"." Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
b)
pretty (L [Lisp a]
xs) = Doc -> Doc
parens ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ((Lisp a -> Doc) -> [Lisp a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty [Lisp a]
xs))
pretty (Q Lisp a
x) = Doc
"'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Lisp a -> Doc
forall a. Pretty a => a -> Doc
pretty Lisp a
x
response :: Lisp String -> String
response :: Lisp [Char] -> [Char]
response = ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n") ([Char] -> [Char])
-> (Lisp [Char] -> [Char]) -> Lisp [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
replaceNewLines ([Char] -> [Char])
-> (Lisp [Char] -> [Char]) -> Lisp [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp [Char] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow
where
replaceNewLines :: Char -> Char
replaceNewLines Char
'\n' = Char
' '
replaceNewLines Char
c = Char
c
putResponse :: Lisp String -> IO ()
putResponse :: Lisp [Char] -> IO ()
putResponse = [Char] -> IO ()
putStr ([Char] -> IO ())
-> (Lisp [Char] -> [Char]) -> Lisp [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp [Char] -> [Char]
response