reduce-equations

Last updated: 2017-06-15 17:47:37 +0100

Upstream URL: git clone http://chriswarbo.net/git/reduce-equations.git

Repo

View repository

View issue tracker

Contents of follows


Reduce Equations

This package provides a command reduce-equations which reads in a list of equations from stdin, performs some simplification, and writes the results to stdout.

For example, given the equations a = b, b = c and a = c, one of these will be removed as it can be inferred from the other two. Similarly, given equations f a = g, f b = g and a = b, one of the first equations will be removed as it can be recovered by subtitution.

All of the real work is done by QuickSpec This package just provides stdio and machine-friendly formatting.

Formats

All IO is encoded in JSON. Both stdin and stdout should contain a single array of equations. The following example gives a single equation, which if written in a more human-friendly form, would be plus x x = times x 2:

[
 {"relation": "~=",
  "lhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int ->gt; Int ->gt; Int",
                                 "symbol": "plus"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role": "variable",
                        "type": "Int",
                        "id":   0}},
  "rhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int ->gt; Int ->gt; Int",
                                 "symbol": "times"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role":   "constant",
                        "type":   "Int",
                        "symbol": "two"}}}
]

Equations

An equation is an object with the following values:

Example:

{"relation": "~=",
  "lhs":     {"role": "application",
              "lhs":  {"role":   "constant",
                       "type":   "Bool ->gt; Bool",
                       "symbol": "not"},
              "rhs":  {"role": "application",
                       "lhs": {"role":   "constant",
                               "type":   "Bool ->gt; Bool",
                               "symbol": "not"},
                       "rhs": {"role": "variable",
                               "type": "Bool",
                               "id": 0}}},
  "rhs":     {"role": "variable",
              "type": "Bool",
              "id":   0}}

Terms

A term is an object containing a role, which is one of "constant", "variable" or "application". The other fields depend on what the term's role is:

Implementation Notes

We co-opt the equation-reducing machinery of the QuickSpec library to do the actual reduction. This relies heavily on existential types and Haskell's Typeable mechanism.

Since the incoming equations may have arbitrary types, and GHC doesn't let us define custom Typeable instances, we perform a conversion step: