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