Language/DTC/Read/TCT.hs

   1 {-# LANGUAGE BangPatterns #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE OverloadedStrings #-}
   5 {-# LANGUAGE RecordWildCards #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE ViewPatterns #-}
   9 {-# OPTIONS_GHC -fno-warn-orphans #-}
  10 -- | Read DTC from TCT.
  11 module Language.DTC.Read.TCT where
  12
  13 -- import Control.Monad.Trans.Class (MonadTrans(..))
  14 -- import qualified Control.Monad.Trans.Reader as R
  15 import Control.Applicative (Applicative(..))
  16 import Control.Monad (Monad(..))
  17 import Data.Bool
  18 import Data.Either (Either(..))
  19 import Data.Eq (Eq(..))
  20 import Data.Foldable (null, foldl')
  21 import Data.Function (($), (.), const, id)
  22 import Data.Functor ((<$>), (<$))
  23 import Data.Int (Int)
  24 import Data.List.NonEmpty (NonEmpty(..))
  25 import Data.Maybe (Maybe(..), fromMaybe, maybe)
  26 import Data.Monoid (Monoid(..))
  27 import Data.Ord (Ord(..))
  28 import Data.Proxy (Proxy(..))
  29 import Data.Semigroup (Semigroup(..))
  30 import Data.Sequence (ViewL(..))
  31 import Data.String (String)
  32 import Data.Text (Text)
  33 import Data.Tuple (snd)
  34 import GHC.Exts (toList)
  35 import Prelude (Num(..))
  36 import Text.Read (readMaybe)
  37 import Text.Show (Show(..))
  38 import qualified Control.Monad.Trans.State as S
  39 import qualified Data.List as List
  40 import qualified Data.Map.Strict as Map
  41 import qualified Data.Sequence as Seq
  42 import qualified Data.Set as Set
  43 import qualified Data.Text as Text
  44 import qualified Text.Megaparsec as P
  45 import qualified Text.Megaparsec.Perm as P
  46
  47 import Language.DTC.Document (Nat(..), Nat1(..))
  48 import Language.TCT hiding (Parser)
  49 import Language.TCT.Write.XML (XML,XMLs,XmlLeaf(..),XmlPos(..))
  50 import qualified Language.DTC.Document as DTC
  51 import qualified Language.DTC.Sym as DTC
  52 import qualified Language.RNC.Sym as RNC
  53 import qualified Language.TCT.Write.XML as XML
  54
  55 -- * Type 'Parser'
  56 -- type Parser = P.Parsec Error XMLs
  57 type Parser = S.StateT XmlPos (P.Parsec Error XMLs)
  58
  59 instance RNC.Sym_Rule Parser where
  60         -- rule n p = P.dbg s p {-(p P.<?> s)-} where s = Text.unpack n
  61         rule _n = id
  62 instance RNC.Sym_RNC Parser where
  63         none = P.label "none" $ P.eof
  64         any  = P.label "any" $ p_satisfyMaybe $ const $ Just ()
  65         anyElem p = P.label "anyElem" $ do
  66                 (n,ts) <- P.token check $ Just expected
  67                 parserXMLs (p n) ts
  68                 where
  69                 expected = TreeN (cell0 "") mempty
  70                 check (TreeN (unCell -> n) ts) = Right (n,ts)
  71                 check t = Left
  72                  ( Just $ P.Tokens $ pure t
  73                  , Set.singleton $ P.Tokens $ pure expected )
  74         position p = do
  75                 st <- S.get
  76                 ($ st) <$> p
  77         element n p = do
  78                 ts <- P.token check $ Just expected
  79                 xp <- S.get
  80                 S.put xp
  81                  { xmlPosAncestors          = (n,maybe 1 (+1) $ Map.lookup n $ xmlPosPrecedingsSiblings xp):xmlPosAncestors xp
  82                  , xmlPosPrecedingsSiblings = mempty
  83                  }
  84                 parserXMLs p ts <* S.put xp
  85                  { xmlPosPrecedingsSiblings =
  86                         Map.insertWith (\_new old -> old + 1) n 1 $
  87                                 xmlPosPrecedingsSiblings xp
  88                  }
  89                 where
  90                 expected = TreeN (cell0 n) mempty
  91                 check (TreeN (unCell -> e) ts) | e == n = Right ts
  92                 check t = Left
  93                  ( Just $ P.Tokens $ pure t
  94                  , Set.singleton $ P.Tokens $ pure expected )
  95         attribute n p = do
  96                 v <- P.token check $ Just expected
  97                 parserXMLs p v
  98                 where
  99                 expected = Tree0 (cell0 $ XML.XmlAttr n "")
 100                 check (TreeN (unCell -> e) ts) | e == n = Right ts
 101                 check (Tree0 (Cell bp ep (XML.XmlAttr k v))) | k == n =
 102                         Right $ Seq.singleton $ Tree0 $ Cell bp ep $ XML.XmlText v
 103                 check t = Left
 104                  ( Just $ P.Tokens $ pure t
 105                  , Set.singleton $ P.Tokens $ pure expected )
 106         comment = do
 107                 s <- P.getInput
 108                 case Seq.viewl s of
 109                  Tree0 (unCell -> XmlComment c) :< ts -> do
 110                         P.setInput ts
 111                         c <$ fixPos
 112                  t :< _ts -> P.failure (Just $ P.Tokens $ pure t) ex
 113                  EmptyL -> P.failure Nothing ex
 114                 where
 115                 ex = Set.singleton $ P.Tokens $ pure expected
 116                 expected = Tree0 (cell0 $ XML.XmlComment "")
 117         text = do
 118                 P.token check (Just expected)
 119                  <* fixPos
 120                 where
 121                 expected = Tree0 (cell0 $ XML.XmlText "")
 122                 check (Tree0 (unCell -> XML.XmlText t)) = Right t
 123                 check t = Left
 124                  ( Just $ P.Tokens $ pure t
 125                  , Set.singleton $ P.Tokens $ pure expected )
 126         int = RNC.rule "int" $ RNC.text >>= \t ->
 127                 case readMaybe (Text.unpack t) of
 128                  Just i -> return i
 129                  Nothing -> P.fancyFailure $
 130                         Set.singleton $ P.ErrorCustom $ Error_Not_Int t
 131         nat = RNC.rule "nat" $ RNC.int >>= \i ->
 132                 if i >= 0
 133                 then return $ Nat i
 134                 else P.fancyFailure $ Set.singleton $
 135                         P.ErrorCustom $ Error_Not_Nat i
 136         nat1 = RNC.rule "nat1" $ RNC.int >>= \i ->
 137                 if i > 0
 138                 then return $ Nat1 i
 139                 else P.fancyFailure $ Set.singleton $
 140                         P.ErrorCustom $ Error_Not_Nat1 i
 141         (<|>)    = (P.<|>)
 142         many     = P.many
 143         some     = P.some
 144         optional = P.optional
 145         option   = P.option
 146         choice   = P.choice
 147         try      = P.try
 148 type instance RNC.Perm Parser = P.PermParser XMLs Parser
 149 instance RNC.Sym_Interleaved Parser where
 150         interleaved = P.makePermParser
 151         (<$$>) = (P.<$$>)
 152         (<||>) = (P.<||>)
 153         (<$?>) = (P.<$?>)
 154         (<|?>) = (P.<|?>)
 155         f <$*> a = f P.<$?> ([],P.some a)
 156         f <|*> a = f P.<|?> ([],P.some a)
 157 instance DTC.Sym_DTC Parser
 158
 159 readDTC ::
 160  DTC.Sym_DTC Parser =>
 161  XMLs ->
 162  Either (P.ParseError (P.Token XMLs) Error) DTC.Document
 163 readDTC =
 164         parseXMLs
 165          XmlPos { xmlPosAncestors = []
 166                 , xmlPosPrecedingsSiblings = mempty
 167                 }
 168          (P.initialPos "")
 169          DTC.document
 170
 171 parseXMLs ::
 172  DTC.Sym_DTC Parser =>
 173  XmlPos ->
 174  P.SourcePos -> Parser a -> XMLs ->
 175  Either (P.ParseError (P.Token XMLs) Error) a
 176 parseXMLs xp pos p i =
 177         snd $
 178         P.runParser' ((`S.evalStateT` xp) $ p <* RNC.none)
 179          P.State
 180                  { P.stateInput = i
 181                  , P.statePos = pure $
 182                         case Seq.viewl i of
 183                          Tree0 c   :< _ -> sourcePosCell c
 184                          TreeN c _ :< _ -> sourcePosCell c
 185                          _ -> pos
 186                  , P.stateTabWidth = P.pos1
 187                  , P.stateTokensProcessed = 0
 188                  }
 189
 190 -- | @parserXMLs xp pos p xs@ returns a 'Parser' parsing @xs@ with @p@ from position @xp@.
 191 parserXMLs ::
 192  DTC.Sym_DTC Parser =>
 193  Parser a -> XMLs -> Parser a
 194 parserXMLs p xs = do
 195         pos <- P.getPosition
 196         xp <- S.get
 197         case parseXMLs xp pos p xs of
 198          Left (P.TrivialError (posErr:|_) un ex) -> do
 199                 P.setPosition posErr
 200                 P.failure un ex
 201          Left (P.FancyError (posErr:|_) errs) -> do
 202                 P.setPosition posErr
 203                 P.fancyFailure errs
 204          Right a -> a <$ fixPos
 205
 206 -- | Adjust the current 'P.SourcePos'
 207 -- to be the begining of the following-sibling 'XML' node
 208 -- so that on error 'P.toHints' keeps expected 'P.Token's in the list,
 209 -- and thus makes useful error messages.
 210 --
 211 -- This is needed because the end of a 'Cell'
 212 -- is not necessarily the begin of the next 'Cell'.
 213 fixPos :: Parser ()
 214 fixPos = do
 215         P.State
 216          { P.stateInput = inp
 217          , P.statePos   = pos :| _
 218          } <- P.getParserState
 219         case Seq.viewl inp of
 220          EmptyL -> return ()
 221          t :< _ -> P.setPosition $
 222                 P.positionAt1 (Proxy::Proxy XMLs) pos t
 223
 224 sourcePosCell :: Cell a -> P.SourcePos
 225 sourcePosCell c =
 226         P.SourcePos ""
 227          (P.mkPos $ lineCell c)
 228          (P.mkPos $ columnCell c)
 229
 230 sourcePos :: Pos -> Maybe P.SourcePos
 231 sourcePos (Pos l c) | l>0 && c>0 = Just $ P.SourcePos "" (P.mkPos l) (P.mkPos c)
 232 sourcePos _ = Nothing
 233
 234 instance P.Stream XMLs where
 235         type Token  XMLs = XML
 236         type Tokens XMLs = XMLs
 237         take1_ s =
 238                 case Seq.viewl s of
 239                  Tree0 (unCell -> XmlComment{}) :< ts -> P.take1_ ts
 240                  t:<ts  -> Just (t,ts)
 241                  EmptyL -> Nothing
 242         positionAt1 _s pos t =
 243                 fromMaybe pos $ sourcePos $
 244                 case t of
 245                  TreeN c _ -> posCell c
 246                  Tree0 c   -> posCell c
 247         positionAtN s pos ts =
 248                 case Seq.viewl ts of
 249                  t :< _ -> P.positionAt1 s pos t
 250                  _ -> pos
 251         advance1 _s _indent pos t =
 252                 -- WARNING: the end of a 'Cell' is not necessarily
 253                 -- the beginning of the next 'Cell'.
 254                 fromMaybe pos $ sourcePos $
 255                 case t of
 256                  TreeN c _ -> posEndCell c
 257                  Tree0 c   -> posEndCell c
 258         advanceN s = foldl' . P.advance1 s
 259         takeN_ n s
 260          | n <= 0    = Just (mempty, s)
 261          | null s    = Nothing
 262          | otherwise = Just (Seq.splitAt n s) -- FIXME: handle XmlComment
 263         tokensToChunk _s = Seq.fromList
 264         chunkToTokens _s = toList
 265         chunkLength _s   = Seq.length
 266         takeWhile_       = Seq.spanl
 267 instance P.ShowToken XML where
 268         showTokens toks = List.intercalate ", " $ toList $ showTree <$> toks
 269                 where
 270                 showTree :: XML -> String
 271                 showTree = \case
 272                  Tree0 c     -> showCell c showXmlLeaf
 273                  TreeN c _ts -> showCell c showXmlName
 274
 275                 showCell (Cell (Pos 0 0) (Pos 0 0) a) f = f a
 276                 showCell (Cell bp ep a) f = f a<>" at "<>show bp<>"-"<>show ep
 277
 278                 showXmlLeaf = \case
 279                  XmlAttr n _v  -> show n<>"="
 280                  XmlText _t    -> "text"
 281                  XmlComment _c -> "comment"
 282                 showXmlName n = "<"<>show n<>">"
 283
 284 -- ** Type 'Error'
 285 data Error
 286  =   Error_EndOfInput
 287  |   Error_Not_Int Text
 288  |   Error_Not_Nat Int
 289  |   Error_Not_Nat1 Int
 290  -- |   Error_Unexpected P.sourcePos XML
 291  deriving (Eq,Ord,Show)
 292 instance P.ShowErrorComponent Error where
 293         showErrorComponent = show