content: {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE ViewPatterns #-}
  module Lang.Crucible.Syntax.SExpr
    ( pattern A
    , pattern L
    , pattern (:::)
    , Syntax(..)
    , Datum(..)
    , Syntactic(..)
    ,  Parser
    , syntaxPos
    , withPosFrom
    , sexp
    , identifier
    , toText
    , datumToText
    , skipWhitespace
    , PrintRules(..)
    , PrintStyle(..)
    , Layer(..)
    , IsAtom(..)
    ) where
  
  import Data.Char (isDigit, isLetter)
  import Data.Text (Text)
  import qualified Data.Text as T
  import Data.Void
  import What4.ProgramLoc as C
  
  import Text.Megaparsec as MP
  import Text.Megaparsec.Char
  import qualified Text.Megaparsec.Char.Lexer as L
  import qualified Prettyprinter as PP
  import qualified Prettyprinter.Render.Text as PP (renderStrict)
  
  
  -- | Syntax objects, in which each layer is annotated with a source position.
  newtype Syntax a = Syntax { unSyntax :: Posd (Layer Syntax a) }
    deriving (Show, Functor, Eq)
  
  -- | Syntax objects divorced of their source-code context, without source positions.
  newtype Datum a = Datum { unDatum :: Layer Datum a}
    deriving (Show, Functor, Eq)
  
  -- | Extract the source position from a 'Syntax' object.
  syntaxPos :: Syntax a -> Position
  syntaxPos (Syntax (Posd p _)) = p
  
  -- | Use the position from a syntax object around something else.
  withPosFrom :: Syntax a -> b -> Posd b
  withPosFrom stx x = Posd (syntaxPos stx) x
  
  -- | Instances of 'Syntactic' support observations using the 'L' and 'A' patterns.
  class Syntactic a b | a -> b where
    syntaxE :: a -> Layer Syntax b
  
  instance Syntactic (Layer Syntax a) a where
    syntaxE = id
  
  
  instance Syntactic (Syntax a) a where
    syntaxE (Syntax (Posd _ e)) = e
  
  -- | Match an atom from a syntactic structure
  pattern A :: Syntactic a b => b -> a
  pattern A x <- (syntaxE -> Atom x)
  
  -- | Match a list from a syntactic structure
  pattern L :: Syntactic a b => [Syntax b] -> a
  pattern L xs <- (syntaxE -> List xs)
  
  -- | Match the head and tail of a list-like structure
  pattern (:::) :: Syntactic a b => Syntax b -> [Syntax b] -> a
  pattern x ::: xs <- (syntaxE -> List (x : xs))
  
  -- | The pattern functor for syntax, used both for 'Syntax' and
  -- 'Datum'. In 'Syntax', it is composed with another structure that
  -- adds source positions.
  data Layer f a = List [f a] | Atom a
    deriving (Show, Functor, Eq)
  
  -- | Convert any syntactic structure to its simplest description.
  syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
  syntaxToDatum (A x) = Datum (Atom x)
  syntaxToDatum (L xs) = Datum (List (map syntaxToDatum xs))
  syntaxToDatum _ = error "impossible - bad Syntactic instance"
  
  -- | A parser for s-expressions.
  type Parser = Parsec Void Text
  
  -- | Skip whitespace.
  skipWhitespace :: Parser ()
  skipWhitespace = L.space space1 lineComment blockComment
    where lineComment = L.skipLineComment ";"
          blockComment = L.skipBlockComment "#|" "|#"
  
  -- | Skip the whitespace after a token.
  lexeme :: Parser a -> Parser a
  lexeme = L.lexeme skipWhitespace
  
  -- | Parse something with its location.
  withPos :: Parser a -> Parser (Posd a)
  withPos p =
    do MP.SourcePos file line col <- getSourcePos
       let loc = C.SourcePos (T.pack file) (unPos line) (unPos col)
       res <- p
       return $ Posd loc res
  
  -- | Parse a particular string.
  symbol :: Text -> Parser Text
  symbol = L.symbol skipWhitespace
  
  -- | Parse a parenthesized list.
  list :: Parser (Syntax a) -> Parser (Syntax a)
  list p =
    do Posd loc _ <- withPos (symbol "(")
       xs <- many p
       _ <- lexeme $ symbol ")"
       return $ Syntax (Posd loc (List xs))
  
  -- | Given a parser for atoms, parse an s-expression that contains them.
  sexp :: Parser a -> Parser (Syntax a)
  sexp atom =
    (Syntax . fmap Atom <$> lexeme (withPos atom)) <|>
    list (sexp atom)
  
  -- | Parse an identifier.
  identifier :: Parser Text
  identifier = T.pack <$> identString
    where letterLike x = isLetter x || elem x ("<>=+-*/!_\\?" :: [Char])
          nameChar x = letterLike x || isDigit x || elem x ("$" :: [Char])
          identString = (:) <$> satisfy letterLike <*> many (satisfy nameChar)
  
  -- | Styles of printing
  data PrintStyle =
    -- | Special forms should treat the first n subforms as special, and
    -- the remaining as a body. For instance, for a Lisp-like
    -- let-expression, use 'Special 1' for indentation.
    Special Int
  
  -- | Printing rules describe how to specially format expressions that
  -- begin with particular atoms.
  newtype PrintRules a = PrintRules (a -> Maybe PrintStyle)
  
  instance Semigroup (PrintRules a) where
    PrintRules f <> PrintRules g = PrintRules $ \z -> f z <|> g z
  
  instance Monoid (PrintRules a) where
    mempty = PrintRules $ const Nothing
  
  
  class IsAtom a where
    showAtom :: a -> Text
  
  pprint :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> PP.Doc ann
  pprint rules expr = pprintDatum rules (syntaxToDatum expr)
  
  pprintDatum :: IsAtom a => PrintRules a -> Datum a -> PP.Doc ann
  pprintDatum rules@(PrintRules getLayout) stx =
    case unDatum stx of
      Atom at -> ppAtom at
      List lst ->
        PP.parens . PP.group $
        case lst of
          [] -> mempty
          [x] -> pprintDatum rules x
          ((unDatum -> Atom car) : xs) ->
            case getLayout car of
              Nothing -> ppAtom car <> PP.space <> PP.align (PP.vsep $ pprintDatum rules <$> xs)
              Just (Special i) ->
                let (special, rest) = splitAt i xs
                in PP.hang 2 $ PP.vsep $
                   PP.group (PP.hang 2 $ PP.vsep $ ppAtom car : (map (pprintDatum rules) special)) :
                   map (pprintDatum rules) rest
          xs -> PP.vsep $ pprintDatum rules <$> xs
  
    where ppAtom = PP.pretty . showAtom
  
  -- | Render a syntactic structure to text, according to rules.
  toText :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> Text
  toText rules stx = PP.renderStrict (PP.layoutSmart opts $ pprint rules stx)
    where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)
  
  -- | Render a datum to text according to rules.
  datumToText :: IsAtom a => PrintRules a -> Datum a -> Text
  datumToText rules dat = PP.renderStrict (PP.layoutSmart opts $ pprintDatum rules dat)
    where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)
  