0 | module Text.PrettyPrint.Prettyprinter.SimpleDocTree
2 | import Text.PrettyPrint.Prettyprinter.Doc
9 | data SimpleDocTree : Type -> Type where
10 | STEmpty : SimpleDocTree ann
11 | STChar : (c : Char) -> SimpleDocTree ann
12 | STText : (len : Int) -> (text : String) -> SimpleDocTree ann
13 | STLine : (i : Int) -> SimpleDocTree ann
14 | STAnn : ann -> (rest : SimpleDocTree ann) -> SimpleDocTree ann
15 | STConcat : List (SimpleDocTree ann) -> SimpleDocTree ann
19 | alterAnnotationsST : (ann -> List ann') -> SimpleDocTree ann -> SimpleDocTree ann'
20 | alterAnnotationsST re STEmpty = STEmpty
21 | alterAnnotationsST re (STChar c) = STChar c
22 | alterAnnotationsST re (STText len text) = STText len text
23 | alterAnnotationsST re (STLine i) = STLine i
24 | alterAnnotationsST re (STAnn ann rest) = foldr STAnn (alterAnnotationsST re rest) (re ann)
25 | alterAnnotationsST re (STConcat xs) = assert_total $
STConcat (map (alterAnnotationsST re) xs)
29 | reAnnotateST : (ann -> ann') -> SimpleDocTree ann -> SimpleDocTree ann'
30 | reAnnotateST f = alterAnnotationsST (pure . f)
34 | unAnnotateST : SimpleDocTree ann -> SimpleDocTree xxx
35 | unAnnotateST = alterAnnotationsST (const [])
39 | collectAnnotations : Monoid m => (ann -> m) -> SimpleDocTree ann -> m
40 | collectAnnotations f STEmpty = neutral
41 | collectAnnotations f (STChar c) = neutral
42 | collectAnnotations f (STText len text) = neutral
43 | collectAnnotations f (STLine i) = neutral
44 | collectAnnotations f (STAnn ann rest) = f ann <+> collectAnnotations f rest
45 | collectAnnotations f (STConcat xs) = assert_total $
concat $
map (collectAnnotations f) xs
49 | traverse : Applicative f => (ann -> f ann') -> SimpleDocTree ann -> f (SimpleDocTree ann')
50 | traverse f STEmpty = pure STEmpty
51 | traverse f (STChar c) = pure $
STChar c
52 | traverse f (STText len text) = pure $
STText len text
53 | traverse f (STLine i) = pure $
STLine i
54 | traverse f (STAnn ann rest) = STAnn <$> f ann <*> traverse f rest
55 | traverse f (STConcat xs) = assert_total $
STConcat <$> Prelude.traverse (traverse f) xs
57 | sdocToTreeParser : SimpleDocStream ann -> (Maybe (SimpleDocTree ann), Maybe (SimpleDocStream ann))
58 | sdocToTreeParser SEmpty = (Just STEmpty, Nothing)
59 | sdocToTreeParser (SChar c rest) = case sdocToTreeParser rest of
60 | (Just tree, rest') => (Just $
STConcat [STChar c, tree], rest')
61 | (Nothing, rest') => (Just $
STChar c, rest')
62 | sdocToTreeParser (SText len text rest) = case sdocToTreeParser rest of
63 | (Just tree, rest') => (Just $
STConcat [STText len text, tree], rest')
64 | (Nothing, rest') => (Just $
STText len text, rest')
65 | sdocToTreeParser (SLine i rest) = case sdocToTreeParser rest of
66 | (Just tree, rest') => (Just $
STConcat [STLine i, tree], rest')
67 | (Nothing, rest') => (Just $
STLine i, rest')
68 | sdocToTreeParser (SAnnPush ann rest) = case sdocToTreeParser rest of
69 | (tree, Nothing) => (Nothing, Nothing)
70 | (Just tree, Nothing) => (Just $
STAnn ann tree, Nothing)
71 | (Just tree, Just rest') => case sdocToTreeParser (assert_smaller rest rest') of
72 | (Just tree', rest'') => (Just $
STConcat [STAnn ann tree, tree'], rest'')
73 | (Nothing, rest'') => (Just $
STAnn ann tree, rest'')
74 | (Nothing, Just rest') => sdocToTreeParser (assert_smaller rest rest')
75 | (Nothing, Nothing) => (Nothing, Nothing)
76 | sdocToTreeParser (SAnnPop rest) = (Nothing, Just rest)
79 | fromStream : SimpleDocStream ann -> SimpleDocTree ann
80 | fromStream sdoc = case sdocToTreeParser sdoc of
81 | (Just tree, Nothing) => flatten tree
84 | flatten : SimpleDocTree ann -> SimpleDocTree ann
85 | flatten (STConcat [x, STEmpty]) = flatten x
86 | flatten (STConcat [x, STConcat xs]) = case flatten (STConcat xs) of
87 | (STConcat xs') => STConcat (x :: xs')
88 | y => STConcat [x, y]
91 | internalError : SimpleDocTree ann
92 | internalError = let msg = "<internal pretty printing error>" in
93 | STText (cast $
length msg) msg