Effective parse tree support for the working semanticist

If, like me, you spend large amounts of time designing, discussing, and proving things about programming languages and formal calculi, chances are you have used Ott (and if you do, but you haven’t, you are really missing out). You write down a formal system once, in a special format that Ott understands, and Ott typechecks it and can automatically generate nice LaTeX as well as code for proof assistants like Coq or Isabelle.

However, anyone who has worked with Ott is familiar with is the dreaded ambiguous parse error. Quite often Ott grammars end up being ambiguous, and Ott needs some guidance to know which parse you want. However, the error messages are horrendous: Ott spews forth several massive parse trees in a format requiring formidable patience to read. Finding the slight differences between two such parse trees is an exercise in seizure-inducing tedium.

I got sick of this so I wrote a little tool to help, which is now available on Hackage: ottparse-pretty. You paste in an Ott parse tree and it shows it to you in a nicely formatted tree view with a bunch of useless cruft removed. For example, it turns this:

(St_node :formula:formula_judgement: (Ste_st (St_node :judgement:judgement_Jtype: (Ste_st
(St_node :Jtype:coerce: (Ste_st (St_nonterm G)) (Ste_st (St_nonterm g)) (Ste_st (St_node
:s:T_MultiTypeApp: (Ste_st (St_node :s:T_EqTy: (Ste_st (St_node :s:T_MultiTypeApp: (Ste_st
(St_node :s:T_MultiKindApp: (Ste_st (St_node :s:T_Cons: (Ste_st (St_nonterm H)))) (Ste_st
(St_nonterm k)))) (Ste_st (St_nonterm t)))) (Ste_st (St_node :s:T_MultiKindApp: (Ste_st
(St_node :s:T_Cons: (Ste_st (St_nonterm H)))) (Ste_st (St_nonterm k)))))) (Ste_st (St_nonterm

into this:

`- judgement_Jtype
   `- coerce
      +- G
      +- g
      `- T_MultiTypeApp
         +- T_EqTy
         |  |
         |  +- T_MultiTypeApp
         |  |  |
         |  |  +- T_MultiKindApp
         |  |  |  |
         |  |  |  +- T_Cons
         |  |  |  |  |
         |  |  |  |  `- H
         |  |  |  |
         |  |  |  `- k
         |  |  |
         |  |  `- t
         |  |
         |  `- T_MultiKindApp
         |     |
         |     +- T_Cons
         |     |  |
         |     |  `- H
         |     |
         |     `- k
         `- t'

It’s pretty simplistic at the moment—I may add more features depending on feedback. But it’s been useful for me so it seemed worth packaging it up in case it’s useful to anyone else.

About Brent

Assistant Professor of Computer Science at Hendrix College. Functional programmer, mathematician, teacher, pianist, follower of Jesus.
This entry was posted in haskell, projects and tagged , , , , , . Bookmark the permalink.

2 Responses to Effective parse tree support for the working semanticist

  1. Harley says:

    I have been using Ott everyday for about a year now. This will come in handy! Great work!


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.