copilot-theorem-4.3: src/Copilot/Theorem/Misc/SExpr.hs
{-# 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 = Atom ""
-- | Atomic expression constructor.
atom = Atom -- s
-- | Empty expression (empty list).
unit = List [] -- ()
-- | Single expression.
singleton a = List [Atom a] -- (s)
-- | Sequence of expressions.
list = List -- (ss)
-- | Sequence of expressions with a root or main note, and a series of
-- additional expressions or arguments.
node a l = List (Atom a : l) -- (s ss)
-- A straightforward string representation for 'SExpr's of Strings that
-- parenthesizes lists of expressions.
instance Show (SExpr String) where
show = PP.render . show'
where
show' (Atom s) = text s
show' (List ts) = parens . hsep . map show' $ ts
-- More advanced printing with some basic indentation
-- | Indent by a given number.
indent = nest 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 shouldIndent printAtom expr =
PP.render (toDoc shouldIndent printAtom 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 shouldIndent printAtom expr = case expr of
Atom a -> text (printAtom a)
List l -> parens (foldl renderItem empty l)
where
renderItem doc s
| shouldIndent s =
doc $$ indent (toDoc shouldIndent printAtom s)
| otherwise =
doc <+> toDoc shouldIndent printAtom 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 =
choice [try unitP, nodeP, leafP]
where
symbol = oneOf "!#$%&|*+-/:<=>?@^_~."
lonelyStr = many1 (alphaNum <|> symbol)
unitP = string "()" >> return unit
leafP = atom <$> lonelyStr
nodeP = do void $ char '('
spaces
st <- sepBy parser spaces
spaces
void $ char ')'
return $ List 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 str = case parse parser "" str of
Left s -> error (show s) -- Nothing
Right t -> Just t