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