1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE OverloadedStrings #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE ViewPatterns #-}
7 {-# OPTIONS_GHC -fno-warn-orphans #-}
8 -- | Read DTC from TCT.
9 module Language.DTC.Read.TCT where
11 import Control.Applicative (Applicative(..))
12 import Control.Monad (Monad(..))
14 import Data.Default.Class (Default(..))
15 import Data.Either (Either(..))
16 import Data.Eq (Eq(..))
17 import Data.Foldable (Foldable(..))
18 import Data.Function (($), (.), const, id)
19 import Data.Functor ((<$>), (<$))
21 import Data.List.NonEmpty (NonEmpty(..))
22 import Data.Maybe (Maybe(..), fromMaybe, maybe)
23 import Data.Monoid (Monoid(..), First(..))
24 import Data.Ord (Ord(..))
25 import Data.Proxy (Proxy(..))
26 import Data.Semigroup (Semigroup(..))
27 import Data.Sequence (ViewL(..), (|>))
28 import Data.String (String)
29 import Data.Tuple (snd)
30 import Prelude (Num(..))
31 import Text.Read (readMaybe)
32 import Text.Show (Show(..))
33 import qualified Control.Monad.Trans.State as S
34 import qualified Data.List as List
35 import qualified Data.Map.Strict as Map
36 import qualified Data.Sequence as Seq
37 import qualified Data.Set as Set
38 import qualified Data.Text.Lazy as TL
39 import qualified Text.Megaparsec as P
40 import qualified Text.Megaparsec.Perm as P
42 import Language.TCT hiding (Parser, ErrorRead)
44 import qualified Language.DTC.Document as DTC
45 import qualified Language.DTC.Sym as DTC
46 import qualified Language.RNC.Sym as RNC
52 -- type Parser = P.Parsec ErrorRead XMLs
53 type Parser = S.StateT State (P.Parsec ErrorRead XMLs)
55 instance RNC.Sym_Rule Parser where
56 -- rule n p = P.dbg s p {-(p P.<?> s)-} where s = Text.unpack n
58 instance RNC.Sym_RNC Parser where
59 none = P.label "none" $ P.eof
60 any = P.label "any" $ p_satisfyMaybe $ const $ Just ()
61 anyElem p = P.label "anyElem" $ do
62 (n,ts) <- P.token check $ Just expected
65 expected = Tree (cell0 $ XmlElem "") mempty
66 check (Tree (unCell -> XmlElem n) ts) = Right (n,ts)
68 ( Just $ P.Tokens $ pure t
69 , Set.singleton $ P.Tokens $ pure expected )
71 ts <- P.token check $ Just expected
75 -- NOTE: special case renaming the current DTC.Pos
76 -- using the @type attribute to have positions like this:
84 , Just ty <- getFirst $ (`foldMap` ts) $ \case
85 Tree0 (unCell -> XmlAttr "type" ty) -> First $ Just ty
89 let anc name = maybe 1 (+1) $ Map.lookup name $ DTC.posPrecedingsSiblings xp
91 { DTC.posAncestors = DTC.posAncestors xp |> (n,anc n)
92 , DTC.posAncestorsWithFigureNames =
93 DTC.posAncestorsWithFigureNames xp |>
94 (nameOrFigureName,anc nameOrFigureName)
95 , DTC.posPrecedingsSiblings = mempty
97 parserXMLs p ts <* S.put xp
98 { DTC.posPrecedingsSiblings=
99 (if n /= nameOrFigureName
100 then Map.insertWith (\_new old -> old + 1) nameOrFigureName 1
102 Map.insertWith (\_new old -> old + 1) n 1 $
103 DTC.posPrecedingsSiblings xp
106 expected = Tree (cell0 $ XmlElem n) mempty
107 check (Tree (unCell -> XmlElem e) ts) | e == n = Right ts
109 ( Just $ P.Tokens $ pure t
110 , Set.singleton $ P.Tokens $ pure expected )
112 v <- P.token check $ Just expected
115 expected = Tree0 (cell0 $ XmlAttr n "")
116 check (Tree0 (Cell bp ep (XmlAttr k v))) | k == n =
117 Right $ Seq.singleton $ Tree0 $ Cell bp ep $ XmlText v
119 ( Just $ P.Tokens $ pure t
120 , Set.singleton $ P.Tokens $ pure expected )
124 Tree0 (unCell -> XmlComment c) :< ts -> do
127 t :< _ts -> P.failure (Just $ P.Tokens $ pure t) ex
128 EmptyL -> P.failure Nothing ex
130 ex = Set.singleton $ P.Tokens $ pure expected
131 expected = Tree0 (cell0 $ XmlComment "")
133 P.token check (Just expected)
136 expected = Tree0 (cell0 $ XmlText "")
137 check (Tree0 (unCell -> XmlText t)) = Right t
139 ( Just $ P.Tokens $ pure t
140 , Set.singleton $ P.Tokens $ pure expected )
141 int = RNC.rule "int" $ RNC.text >>= \t ->
142 case readMaybe (TL.unpack t) of
144 Nothing -> P.fancyFailure $
145 Set.singleton $ P.ErrorCustom $ ErrorRead_Not_Int t
146 nat = RNC.rule "nat" $ RNC.int >>= \i ->
149 else P.fancyFailure $ Set.singleton $
150 P.ErrorCustom $ ErrorRead_Not_Nat i
151 nat1 = RNC.rule "nat1" $ RNC.int >>= \i ->
154 else P.fancyFailure $ Set.singleton $
155 P.ErrorCustom $ ErrorRead_Not_Nat1 i
159 optional = P.optional
163 type instance RNC.Perm Parser = P.PermParser XMLs Parser
164 instance RNC.Sym_Interleaved Parser where
165 interleaved = P.makePermParser
170 f <$*> a = f P.<$?> ([],P.some a)
171 f <|*> a = f P.<|?> ([],P.some a)
172 instance DTC.Sym_DTC Parser where
176 DTC.Sym_DTC Parser =>
178 Either (P.ParseError (P.Token XMLs) ErrorRead) DTC.Document
179 readDTC = parseXMLs def (P.initialPos "") DTC.document
182 DTC.Sym_DTC Parser =>
184 P.SourcePos -> Parser a -> XMLs ->
185 Either (P.ParseError (P.Token XMLs) ErrorRead) a
186 parseXMLs st pos p i =
188 P.runParser' ((`S.evalStateT` st) $ p <* RNC.none)
191 , P.statePos = pure $
193 Tree c _ :< _ -> sourcePosCell c
195 , P.stateTabWidth = P.pos1
196 , P.stateTokensProcessed = 0
199 -- | @parserXMLs st pos p xs@ returns a 'Parser' parsing @xs@ with @p@ from state @st@.
201 DTC.Sym_DTC Parser =>
202 Parser a -> XMLs -> Parser a
206 case parseXMLs st pos p xs of
207 Left (P.TrivialError (posErr:|_) un ex) -> do
210 Left (P.FancyError (posErr:|_) errs) -> do
213 Right a -> a <$ fixPos
215 -- | Adjust the current 'P.SourcePos'
216 -- to be the begining of the following-sibling 'XML' node
217 -- so that on error 'P.toHints' keeps expected 'P.Token's in the list,
218 -- and thus makes useful error messages.
220 -- This is needed because the end of a 'Cell'
221 -- is not necessarily the begin of the next 'Cell'.
226 , P.statePos = pos :| _
227 } <- P.getParserState
228 case Seq.viewl inp of
230 t :< _ -> P.setPosition $
231 P.positionAt1 (Proxy::Proxy XMLs) pos t
233 sourcePosCell :: Cell a -> P.SourcePos
234 sourcePosCell (cell_begin -> bp) =
236 (P.mkPos $ pos_line bp)
237 (P.mkPos $ pos_column bp)
239 sourcePos :: Pos -> Maybe P.SourcePos
240 sourcePos (Pos l c) | l>0 && c>0 = Just $ P.SourcePos "" (P.mkPos l) (P.mkPos c)
241 sourcePos _ = Nothing
243 instance P.Stream XMLs where
244 type Token XMLs = XML
245 type Tokens XMLs = XMLs
248 Tree0 (unCell -> XmlComment{}) :< ts -> P.take1_ ts
252 fromMaybe pos . sourcePos .
254 positionAtN s pos ts =
256 t :< _ -> P.positionAt1 s pos t
258 advance1 _s _indent pos =
259 -- WARNING: the end of a 'Cell' is not necessarily
260 -- the beginning of the next 'Cell'.
261 fromMaybe pos . sourcePos .
263 advanceN s = foldl' . P.advance1 s
265 | n <= 0 = Just (mempty, s)
267 | otherwise = Just (Seq.splitAt n s) -- FIXME: handle XmlComment
268 tokensToChunk _s = Seq.fromList
269 chunkToTokens _s = toList
270 chunkLength _s = Seq.length
271 takeWhile_ = Seq.spanl
272 instance P.ShowToken XML where
273 showTokens toks = List.intercalate ", " $ toList $ showTree <$> toks
275 showTree :: XML -> String
276 showTree (Tree a _ts) =
278 XmlElem n -> "<"<>show n<>">"
279 XmlAttr n _v -> show n<>"="
281 XmlComment _c -> "comment"
283 showCell (Cell (Pos 0 0) (Pos 0 0) a) f = f a
284 showCell (Cell bp ep a) f = f a<>" at "<>show bp<>"-"<>show ep
286 -- ** Type 'ErrorRead'
288 = ErrorRead_EndOfInput
289 | ErrorRead_Not_Int TL.Text
290 | ErrorRead_Not_Nat Int
291 | ErrorRead_Not_Nat1 Int
292 -- | ErrorRead_Unexpected P.sourcePos XML
293 deriving (Eq,Ord,Show)
294 instance P.ShowErrorComponent ErrorRead where
295 showErrorComponent = show