content: {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE ViewPatterns #-}
  
  module Lang.Crucible.Syntax.Monad
    ( MonadSyntax(..)
  
    -- * Describing syntax
    , describe
    , atom
    , cons
    , depCons
    , depConsCond
    , followedBy
    , rep
    , list
    , backwards
    , emptyList
    , atomic
    , anyList
    , sideCondition
    , sideCondition'
    , satisfy
  
    -- * Eliminating location information
    , syntaxToDatum
    , datum
  
    -- * Parsing context
    , position
    , withProgressStep
  
    -- * Control structures
    , commit
    , parse
  
    -- * Progress through a parsing problem
    , ProgressStep(..)
    , Progress
    , emptyProgress
    , pushProgress
  
    -- * Errors
    , later
    , Reason(..)
    ) where
  
  import Control.Applicative
  import Control.Monad (MonadPlus(..), ap)
  import Control.Monad.Reader (MonadReader(..), ReaderT(..))
  import qualified Control.Monad.State.Strict as Strict
  import qualified Control.Monad.State.Lazy as Lazy
  import Control.Monad.State.Class
  import Control.Monad.Trans.Class (MonadTrans(..))
  import qualified Control.Monad.Writer.Strict as Strict
  import qualified Control.Monad.Writer.Lazy as Lazy
  import Control.Monad.Writer.Class
  
  import Data.Foldable as Foldable
  import Data.List.NonEmpty (NonEmpty(..))
  import Data.Text (Text)
  import qualified Data.Text as T
  
  import Lang.Crucible.Syntax.SExpr
  
  import What4.ProgramLoc (Posd(..), Position)
  
  data Search a = Try a (Search a) | Fail | Cut
    deriving Functor
  
  instance Applicative Search where
    pure x = Try x Fail
    (<*>) = ap
  
  instance Alternative Search where
    empty = Fail
    x <|> y =
      case x of
        Try first rest -> Try first (rest <|> y)
        Fail -> y
        Cut -> Cut
  
  instance Monad Search where
    m >>= f =
      case m of
        Try x more -> f x <|> (more >>= f)
        Fail -> Fail
        Cut -> Fail
  
  instance MonadPlus Search where
    mzero = empty
    mplus = (<|>)
  
  instance Semigroup (Search a) where
    (<>) = (<|>)
  
  instance Monoid (Search a) where
    mempty  = empty
  
  instance Foldable Search where
    foldMap f (Try x xs) = f x `mappend` foldMap f xs
    foldMap _ _ = mempty
  
    toList (Try x xs) = x : toList xs
    toList _          = []
  
  instance Traversable Search where
    traverse f (Try x xs) = Try <$> f x <*> traverse f xs
    traverse _ Fail = pure Fail
    traverse _ Cut = pure Cut
  
  -- | Components of a path taken through a syntax object to reach the
  -- current focus.
  data ProgressStep =
      First -- ^ The head of a list was followed
    | Rest -- ^ The tail of a list was followed
    | Late -- ^ The path was annotated as 'later'
    deriving (Eq, Show)
  
  instance Ord ProgressStep where
    compare First First = EQ
    compare First _ = LT
    compare Rest First = GT
    compare Rest Rest = EQ
    compare Rest _ = LT
    compare Late Late = EQ
    compare Late _ = GT
  
  -- | The path taken through a syntax object to reach the current
  -- focus.
  newtype Progress = Progress [ProgressStep]
    deriving (Eq, Show)
  
  -- | An empty path, used to initialize parsers
  emptyProgress :: Progress
  emptyProgress = Progress []
  
  -- | Add a step to a progress path
  pushProgress :: ProgressStep -> Progress -> Progress
  pushProgress p (Progress ps) = Progress (p : ps)
  
  instance Ord Progress where
    compare (Progress xs) (Progress ys) =
      case (xs, ys) of
        ([], []) -> EQ
        ([], _:_) -> LT
        (_:_, []) -> GT
        (x:xs', y:ys') ->
          case compare (Progress xs') (Progress ys') of
            LT -> LT
            GT -> GT
            EQ -> compare x y
  
  
  -- | The reason why a failure has occurred, consisting of description
  -- 'message' combined with the focus that was described.
  data Reason atom = Reason { expr :: Syntax atom
                            , message :: Text
                            }
    deriving (Functor, Show, Eq)
  
  data Failure atom = Ok | Oops Progress (NonEmpty (Reason atom))
    deriving (Functor, Show)
  
  instance Semigroup (Failure atom) where
    Ok              <> e2 = e2
    e1@(Oops _ _)   <> Ok = e1
    e1@(Oops p1 r1) <> e2@(Oops p2 r2) =
      case compare p1 p2 of
        LT -> e2
        GT -> e1
        EQ -> Oops p1 (r1 <> r2)
  
  instance Monoid (Failure atom) where
    mempty = Ok
  
  data P atom a = P { _success :: Search a
                    , _failure :: Failure atom
                    }
    deriving Functor
  
  -- | Monads that can parse syntax need a few fundamental operations.
  -- A parsing monad maintains an implicit "focus", which is the syntax
  -- currently being matched, as well as the progress, which is the path
  -- taken through the surrounding syntactic context to reach the
  -- current focus. Additionally, the reason for a failure will always
  -- be reported with respect to explicit descriptions - these are
  -- inserted through 'withReason'.
  class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where
    -- | Succeed with the current focus.
    anything :: m (Syntax atom)
    -- | Succeed with the current progress.
    progress :: m Progress
    -- | Run a new parser with a different focus.
    withFocus :: Syntax atom -> m a -> m a
    -- | Run a parser in a modified notion of progress.
    withProgress :: (Progress -> Progress) -> m a -> m a
    -- | Run a parser with a new reason for failure.
    withReason :: Reason atom -> m a -> m a
    -- | Fail, and additionally prohibit backtracking across the failure.
    cut :: m a
    -- | Delimit the dynamic extent of a 'cut'.
    delimit :: m a -> m a
    -- | Make the first solution reported by a computation into the only
    -- solution reported, eliminating further backtracking and previous
    -- errors. This allows syntax to be matched in exclusive "layers",
    -- reminiscent of the effect of trampolining through a macro
    -- expander. Use when solutions are expected to be unique.
    call :: m a -> m a
  
  instance MonadSyntax atom m => MonadSyntax atom (ReaderT r m) where
    anything = lift anything
    cut = lift cut
    progress = lift progress
    delimit m =
      do r <- ask
         lift $ delimit (runReaderT m r)
    call m =
      do r <- ask
         lift $ call (runReaderT m r)
    withFocus stx m =
      do r <- ask
         lift $ withFocus stx (runReaderT m r)
    withProgress p m =
      do r <- ask
         lift $ withProgress p (runReaderT m r)
    withReason why m =
      do r <- ask
         lift $ withReason why (runReaderT m r)
  
  instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Strict.StateT s m) where
    anything = lift anything
    cut = lift cut
    progress = lift progress
    delimit m =
      do st <- get
         (s, st') <- lift $ delimit (Strict.runStateT m st)
         put st'
         return s
    call m =
      do st <- get
         (s, st') <- lift $ call (Strict.runStateT m st)
         put st'
         return s
    withFocus stx m =
      do st <- get
         (s, st') <- lift $ withFocus stx (Strict.runStateT m st)
         put st'
         return s
    withProgress p m =
      do st <- get
         (s, st') <- lift $ withProgress p (Strict.runStateT m st)
         put st'
         return s
    withReason why m =
      do st <- get
         (s, st') <- lift $ withReason why (Strict.runStateT m st)
         put st'
         return s
  
  instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Lazy.StateT s m) where
    anything = lift anything
    cut = lift cut
    progress = lift progress
    delimit m =
      do st <- get
         (s, st') <- lift $ delimit (Lazy.runStateT m st)
         put st'
         return s
    call m =
      do st <- get
         (s, st') <- lift $ call (Lazy.runStateT m st)
         put st'
         return s
    withFocus stx m =
      do st <- get
         (s, st') <- lift $ withFocus stx (Lazy.runStateT m st)
         put st'
         return s
    withProgress p m =
      do st <- get
         (s, st') <- lift $ withProgress p (Lazy.runStateT m st)
         put st'
         return s
    withReason why m =
      do st <- get
         (s, st') <- lift $ withReason why (Lazy.runStateT m st)
         put st'
         return s
  
  instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Strict.WriterT w m) where
    anything = lift anything
    cut = lift cut
    progress = lift progress
    delimit m =
      do (x, w) <- lift $ delimit $ Strict.runWriterT m
         tell w
         return x
    call m =
      do (x, w) <- lift $ call $ Strict.runWriterT m
         tell w
         return x
    withFocus stx m =
      do (x, w) <- lift $ withFocus stx $ Strict.runWriterT m
         tell w
         return x
    withProgress p m =
      do (x, w) <- lift $ withProgress p $ Strict.runWriterT m
         tell w
         return x
    withReason why m =
      do (x, w) <- lift $ withReason why $ Strict.runWriterT m
         tell w
         return x
  
  instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Lazy.WriterT w m) where
    anything = lift anything
    cut = lift cut
    progress = lift progress
    delimit m =
      do (x, w) <- lift $ delimit $ Lazy.runWriterT m
         tell w
         return x
    call m =
      do (x, w) <- lift $ call $ Lazy.runWriterT m
         tell w
         return x
    withFocus stx m =
      do (x, w) <- lift $ withFocus stx $ Lazy.runWriterT m
         tell w
         return x
    withProgress p m =
      do (x, w) <- lift $ withProgress p $ Lazy.runWriterT m
         tell w
         return x
    withReason why m =
      do (x, w) <- lift $ withReason why $ Lazy.runWriterT m
         tell w
         return x
  
  -- | Strip location information from a syntax object
  syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
  syntaxToDatum (A x) = Datum $ Atom x
  syntaxToDatum (L ls) = Datum $ List $ map syntaxToDatum ls
  syntaxToDatum _ = error "syntaxToDatum: impossible case - bad Syntactic instance"
  
  -- | Succeed if and only if the focus satisfies a Boolean predicate.
  satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom)
  satisfy p =
    do foc <- anything
       if p foc
         then pure foc
         else empty
  
  -- | Succeed only if the focus, having been stripped of position
  -- information, is structurally equal to some datum.
  datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m ()
  datum dat =
    describe (datumToText mempty dat) $
      satisfy (\stx -> dat == syntaxToDatum stx) *> pure ()
  
  -- | Succeed if and only if the focus is some particular given atom.
  atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m ()
  atom a = datum (Datum (Atom a))
  
  -- | Succeed if and only if the focus is any atom, returning the atom.
  atomic :: MonadSyntax atom m => m atom
  atomic = sideCondition "an atom" perhapsAtom (syntaxToDatum <$> anything)
    where perhapsAtom (Datum (Atom a)) = Just a
          perhapsAtom _ = Nothing
  
  -- | Annotate a parser with a description, documenting its role in the
  -- grammar. These descriptions are used to construct error messages.
  describe :: MonadSyntax atom m => Text -> m a -> m a
  describe !d p =
    do foc <- anything
       withReason (Reason foc d) p
  
  -- | Succeed if and only if the focus is the empty list.
  emptyList :: MonadSyntax atom m => m ()
  emptyList = describe (T.pack "empty expression ()") (satisfy (isNil . syntaxToDatum) *> pure ())
    where isNil (Datum (List [])) = True
          isNil _ = False
  
  -- | Succeed if and only if the focus is a list, returning its contents.
  anyList :: MonadSyntax atom m => m [Syntax atom]
  anyList = sideCondition "zero or more expressions, in parentheses" isList anything
    where isList (Syntax (pos_val -> List xs)) = Just xs
          isList _ = Nothing
  
  -- | If the current focus is a list, apply one parser to its head and
  -- another to its tail.
  cons :: MonadSyntax atom m => m a -> m b -> m (a, b)
  cons a d = depCons a (\x -> d >>= \y -> pure (x, y))
  
  -- | If the current focus is a list, apply one parser to its head and
  -- another to its tail, ignoring the result of the head.
  followedBy :: MonadSyntax atom m => m a -> m b -> m b
  followedBy a d = depCons a (const d)
  
  -- | Return the source position of the focus.
  position :: MonadSyntax atom m => m Position
  position = syntaxPos <$> anything
  
  -- | Manually add a progress step to the current path through the
  -- context. Use this to appropriately guard calls to 'parse'.
  withProgressStep :: (MonadSyntax atom m) => ProgressStep -> m a -> m a
  withProgressStep s = withProgress (pushProgress s)
  
  -- | A dependent cons (see 'depcons') that can impose a validation
  -- step on the head of a list focus. If the head fails the validation
  -- (that is, the second action returns 'Left'), the error is reported
  -- in the head position.
  depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b
  depConsCond a d =
    do focus <- anything
       case focus of
         L (e:es) ->
           do x <- withFocus e $ withProgressStep First $ a
              let cdr = Syntax (Posd (syntaxPos focus) (List es))
              res <- withFocus cdr $ withProgressStep Rest $ d x
              case res of
                Right answer -> return answer
                Left what -> withFocus e $ withProgressStep First $ later $ describe what empty
         _ -> empty
  
  -- | Use the result of parsing the head of the current-focused list to
  -- compute a parsing action to use for the tail of the list.
  depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b
  depCons a d =
    do focus <- anything
       case focus of
         L (e:es) ->
           do x <- withFocus e $ withProgressStep First $ a
              let cdr = Syntax (Posd (syntaxPos focus) (List es))
              withFocus cdr $ withProgressStep Rest $ d x
         _ -> empty
  
  -- | Produce a parser that matches a list of things matched by another
  -- parser.
  rep :: MonadSyntax atom m => m a -> m [a]
  rep p =
    do focus <- anything
       case focus of
         L [] ->
           pure []
         L (e:es) ->
           do x <- withFocus e $ withProgressStep First p
              let cdr = Syntax (Posd (syntaxPos focus) (List es))
              xs <- withFocus cdr $ withProgressStep Rest $ rep p
              pure (x : xs)
         _ -> empty
  
  -- | Manually override the focus. Use this with care - it can lead to
  -- bogus error selection unless 'withProgress' is used to provide an
  -- appropriate path.
  parse :: MonadSyntax atom m => Syntax atom -> m a -> m a
  parse = withFocus
  
  -- | Match a list focus elementwise.
  list :: MonadSyntax atom m => [m a] -> m [a]
  list parsers = describe desc $ list' parsers
    where desc =
            mappend (T.pack (show (length parsers))) (T.pack " expressions")
          list' ps =
            do focus <- anything
               case focus of
                 L es -> go (syntaxPos focus) ps es
                 _ -> empty
  
          go _ [] [] = pure []
          go _ (_:_) [] = empty
          go _ [] (_:_) = empty
          go loc (p:ps) (e:es) =
            do x <- withFocus e $ withProgressStep First p
               xs <- withFocus (Syntax (Posd loc (List es))) $
                     withProgressStep Rest $
                     list' ps
               pure (x : xs)
  
  -- | Transform a parser such that its errors are considered to occur
  -- after others, and thus be reported with a higher priority.
  later :: MonadSyntax atom m => m a -> m a
  later = withProgressStep Late
  
  -- | Impose a side condition on a parser, failing with the given
  -- description if the side condition is 'Nothing'.
  sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b
  sideCondition !msg ok p =
    do x <- p
       case ok x of
         Just y -> pure y
         Nothing ->
           later $ describe msg empty
  
  -- | Impose a Boolean side condition on a parser, failing with the
  -- given description if the side condition is 'False'.
  sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a
  sideCondition' !msg ok p = sideCondition msg (\x -> if ok x then Just x else Nothing) p
  
  -- | When the current focus is a list, reverse its contents while
  -- invoking another parser. If it is not a list, fail.
  backwards :: MonadSyntax atom m => m a -> m a
  backwards p =
    do foc <- anything
       case foc of
        l@(L xs) -> withFocus (Syntax (Posd (syntaxPos l) (List (reverse xs)))) p
        _ -> empty
  
  -- | Trivially succeed, but prevent backtracking.
  commit :: MonadSyntax atom m => m ()
  commit = pure () <|> cut
  