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.
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:
readHistory
: A way to read the rewrite history from file (for this example, always return a constant history).ppr'
: A pretty-printing for (for this example, the type of annotations is just the type of contexts)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.
The features depicted below have been recorded on the optimizing phase of the .