Inspection of rewriting steps.

A terminal UI for inspecting steps taken by a rewriting process. Useful for the optimization phase of a compiler, or even evaluators of small languages.

Rewrite Inspector

A terminal user-interface (TUI) for inspecting steps taken by a rewriting process. Useful for the optimization phase of a compiler, or even evaluators of small languages.

Available on

Usage Instructions

To use the library, the user's type of language expressions must be an instance of the Diff typeclass.

Let's see an example for a simple language for arithmetic expressions.

data Expr = N Int | Expr :+: Expr deriving (Eq, Show)

We first need to give the type of contexts, which navigate to a certain sub-term:

data ExprContext = L | R deriving (Eq, Show)

We can then give the instance for the Diff typeclass, by providing the following:

1. readHistory: A way to read the rewrite history from file (for this example, always return a constant history).
2. ppr': A pretty-printing for (for this example, the type of annotations is just the type of contexts)
3. patch: A way to patch a given expression at some context.

Below is the complete definition of our instance:

instance Diff Expr where
  type Ann     Expr = ExprContext
  type Options Expr = ()
  type Ctx     Expr = ExprContext

  readHistory _ = return [ HStep { _ctx    = [L]
                                 , _bndrS  = "top"
                                 , _name   = "adhocI"
                                 , _before = N 1
                                 , _after  = N 11 :+: N 12
                                 }
                         , HStep { _ctx    = [L, L]
                                 , _bndrS  = "top"
                                 , _name   = "adhocII"
                                 , _before = N 11
                                 , _after  = N 111 :+: N 112
                                 }
                         , HStep { _ctx    = []
                                 , _bndrS  = "top"
                                 , _name   = "normalization"
                                 , _before = N 1 :+: (N 2 :+: N 3)
                                 , _after  = ((N 111 :+: N 112) :+: N 12)
                                         :+: (N 2 :+: N 3)
                                 }
                         ]

  ppr' _    (N n)      = pretty n
  ppr' opts (e :+: e') = hsep [ annotate L (ppr' opts e)
                              , "+"
                              , annotate R (ppr' opts e')
                              ]

  patch _ []     e' = e'
  patch curE (c:cs) e' = let go e = patch e cs e' in
    case (curE, c) of
      (l :+: r, L) -> go l :+: r
      (l :+: r, R) -> l :+: go r
      _            -> error "patch"

Finally, we are ready to run our TUI to inspect the rewriting steps with proper highlighting (.ini files are used to provide styling directives):

main :: IO ()
main = runTerminal @Expr "examples/expr/theme.ini"

For more examples, check the folder.

Features

The features depicted below have been recorded on the optimizing phase of the .

1. Use Ctrl-p to show/hide keyboard controls:

2. Syntax highlighting:

3. Navigate through the rewriting steps with highlighted diffs:

4. Also navigate through all top-level binders:

5. Hide extraneous code output, suc as uniques/types/qualifiers:

6. Individual and grouped scrolling for code panes, both vertically and horizontally:

7. Move to next transformation with the given step number:

8. Move to next transformation with the given name:

9. Search for string occurrences within source code:

10. Inside code panes, the line width is dynamically adjusted depending on available space:

11. User-configurable colour theme: