0 | module Text.ILex.Debug
  1 |
  2 | import Control.Monad.State
  3 | import Data.ByteString
  4 | import Data.Linear.Traverse1
  5 | import Data.SortedMap
  6 | import Data.String
  7 | import Derive.Pretty
  8 | import Language.Reflection.Pretty
  9 |
 10 | import Text.ILex.Char.UTF8
 11 | import Text.ILex.Stack
 12 | import Text.ILex.Internal.DFA
 13 | import Text.ILex.Internal.ENFA
 14 | import Text.ILex.Internal.NFA
 15 | import Text.ILex.Internal.Types
 16 | import Text.ILex.Parser
 17 | import Text.ILex.RExp
 18 |
 19 | %default total
 20 |
 21 | export
 22 | appLst : {d : _} -> Doc d -> List (Doc d) -> Doc d
 23 | appLst nm [] = nm
 24 | appLst nm ds = nm `vappend` (indent 2 $ vsep ds)
 25 |
 26 | export
 27 | strLst : {d : _} -> String -> List (Doc d) -> Doc d
 28 | strLst = appLst . line
 29 |
 30 | export
 31 | prettyNats : {d : _} -> List Nat -> Doc d
 32 | prettyNats []      = line ""
 33 | prettyNats [n]     = line (show n)
 34 | prettyNats (n::ns) = line (show n) <+> comma <+> prettyNats ns
 35 |
 36 | export
 37 | Pretty Range8 where
 38 |   prettyPrec p r =
 39 |     let l := lowerBound r
 40 |         u := upperBound r
 41 |
 42 |      in if l > u then line "<empty>"
 43 |         else if l == u then line (show l)
 44 |         else line "\{show l}-\{show u}"
 45 |
 46 | export
 47 | prettyEdge : {d : _} -> Edge -> Doc d
 48 | prettyEdge (E r tgt) = pretty r <+> colon <++> line (show tgt)
 49 |
 50 | export
 51 | prettyENode : {d : _} -> (Nat,ENode) -> Doc d
 52 | prettyENode (n, EN accs eps ds) =
 53 |   appLst (line "Node" <++> pretty n)
 54 |     [ line   "acc:      " <+> prettyNats accs
 55 |     , line   "eps:      " <+> prettyNats eps
 56 |     , strLst "deltas:   " (map prettyEdge ds)
 57 |     ]
 58 |
 59 | export
 60 | prettyNEdge : {d : _} -> NEdge -> Doc d
 61 | prettyNEdge (NE r tgts) = pretty r <+> colon <++> line (show tgts)
 62 |
 63 | export
 64 | prettyNNode : {d : _} -> (Nat,NNode) -> Doc d
 65 | prettyNNode (n, NN _ accs ds) =
 66 |   appLst (line "Node" <++> pretty n)
 67 |     [ line   "acc:      " <+> prettyNats accs
 68 |     , strLst "deltas:   " (map prettyNEdge ds)
 69 |     ]
 70 |
 71 | export
 72 | prettyNode : {d : _} -> (Nat,Node) -> Doc d
 73 | prettyNode (n, N _ acc ds) =
 74 |   appLst (line "Node" <++> pretty n)
 75 |     [ line   "acc:      " <+> prettyNats acc
 76 |     , strLst "deltas:   " (map prettyEdge ds)
 77 |     ]
 78 |
 79 | export
 80 | Pretty (List (Nat,ENode)) where
 81 |   prettyPrec p g = strLst "graph:" (map prettyENode g)
 82 |
 83 | export
 84 | Pretty (List (Nat,NNode)) where
 85 |   prettyPrec p g = strLst "graph:" (map prettyNNode g)
 86 |
 87 | export
 88 | Pretty (List (Nat,Node)) where
 89 |   prettyPrec p g = strLst "graph:" (map prettyNode g)
 90 |
 91 | terminal : Pretty a => {d : _} -> (Nat, a) -> Doc d
 92 | terminal (n,c) = line (show n) <+> colon <++> pretty c
 93 |
 94 | export
 95 | Pretty a => Pretty b => Pretty (Machine a b) where
 96 |   prettyPrec p (M sm g) =
 97 |     vsep
 98 |       [ appLst (line "Terminals") (map terminal $ SortedMap.toList sm)
 99 |       , pretty g
100 |       ]
101 |
102 | export covering
103 | prettyENFA : Pretty a => TokenMap8 a -> IO ()
104 | prettyENFA tm = putPretty $ machine $ toENFA tm
105 |
106 | export covering
107 | prettyNFA : Pretty a => TokenMap8 a -> IO ()
108 | prettyNFA tm = putPretty $ machine $ toNFA tm
109 |
110 | export covering
111 | prettyDFA : Pretty a => TokenMap8 a -> IO ()
112 | prettyDFA tm = putPretty $ machine $ toDFA tm
113 |
114 | --------------------------------------------------------------------------------
115 | -- Lexer Pretty Printing
116 | --------------------------------------------------------------------------------
117 |
118 | prettyByte : {d : _} -> Nat -> Doc d
119 | prettyByte n = line "\{pre} 0x\{toHex $ cast n}"
120 |   where
121 |     pre : String
122 |     pre =
123 |      case n >= 128 || Prelude.isControl (cast n) of
124 |        True  => "   "
125 |        False => "'\{String.singleton $ cast n}'"
126 |
127 | export
128 | Pretty a => Pretty (Tok e a) where
129 |   prettyPrec _ Ignore    = line "<ignore>"
130 |   prettyPrec _ (Const x) = pretty x
131 |   prettyPrec _ (Txt   f) = line "<Txt>"
132 |   prettyPrec _ (Bytes f) = line "<Bytes>"
133 |
134 | prettyByteStep : {d : _} -> (Nat, ByteStep n q r s) -> Doc d
135 | prettyByteStep (x,bs) =
136 |   vsep
137 |     [ line (show x)
138 |     , indent 2 $ vsep (mapMaybe trans $ zipWithIndex $ toList bs)
139 |     ]
140 |
141 |   where
142 |     trans : (Nat, Transition n q r s) -> Maybe (Doc d)
143 |     trans (byte,t) =
144 |       case t of
145 |         Keep       => Just (prettyByte byte <+> colon <++> line "stay")
146 |         Done y     => Just (prettyByte byte <+> colon <++> line "done")
147 |         DoneBS y   => Just (prettyByte byte <+> colon <++> line "done with bytes")
148 |         Move y z   => Just (prettyByte byte <+> colon <++> line "move (\{show y})")
149 |         MoveE y    => Just (prettyByte byte <+> colon <++> line "move non-terminal (\{show y})")
150 |         Bottom     => Nothing
151 |
152 | export
153 | Pretty (DFA q r s) where
154 |   prettyPrec p (L _ next) =
155 |     vsep $ prettyByteStep <$> zipWithIndex (toList next)
156 |
157 | export
158 | prettyLexer : DFA q r s -> IO ()
159 | prettyLexer dfa = putPretty dfa
160 |
161 | export
162 | prettyParser :
163 |      {default False details : Bool}
164 |   -> (p : P1 World e a)
165 |   -> (PIx p -> String)
166 |   -> IO ()
167 | prettyParser p shw = go 0 0
168 |   where
169 |     go : Nat -> Bits32 -> IO ()
170 |     go tot v =
171 |       case lt v p.states of
172 |         Just0 prf =>
173 |           let lx := p.lex `at` I v
174 |            in case details of
175 |                 False => Prelude.do
176 |                   putStrLn "\{shw $ I v} (\{show $ S lx.states} states)"
177 |                   go (tot + lx.states) (assert_smaller v $ v+1)
178 |                 True  => Prelude.do
179 |                   putStrLn "\{shw $ I v} (\{show $ S lx.states} states): "
180 |                   prettyLexer lx
181 |                   putStrLn ""
182 |                   go (tot + lx.states) (assert_smaller v $ v+1)
183 |         Nothing0  => putStrLn "Total: \{show tot} state transitions"
184 |