Skip to content

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.

License

Notifications You must be signed in to change notification settings

omelkonian/rewrite-inspector

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

18 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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 Hackage

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 examples folder.

Features

The features depicted below have been recorded on the optimizing phase of the Cλash compiler.

  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:

About

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.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published