render-eqs

Last updated: 2019-08-10 14:05:48 +0100

Upstream URL: git clone http://chriswarbo.net/git/render-eqs.git

Repo

View repository

View issue tracker

Contents of README follows


render-eqs

This is a simple Python script for converting equations from a JSON format into a more human-friendly format.

This output format loosely follows ML-style syntax (e.g. juxtaposition for function calls). but it is <em>not</em> designed to be parsed! All data processing should be done using the JSON format; this renderer is just to aid in debugging or pretty-printing for UIs.

Input Syntax

Input is an array of 'equations', where the terms in each equation are made from nested JSON objects. Terms can have the following "roles":

Constants

A constant, like <code>plus</code>, is written as follows:

<div class="sourceCode"><pre class="sourceCode json"><code class="sourceCode json"><span class="fu">{</span> <span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="st">"plus"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int -> Int -> Int"</span> <span class="fu">}</span></code></pre></div>

The <code>role</code> must be <code>constant</code>.

The <code>symbol</code> is the text that we will show when rendering this constant (in principle this could be anything you like, but if you are going to do something dodgy like writing a compound expression or nested JSON, I'd at least advise wrapping it in delimiters like parentheses).

The <code>type</code> should be a string, ideally of this constant's type in some ML/Haskell form. It isn't currently used by any tooling that I know of, but is often worth including if known. In the future this <em>might</em> be extended into a more meaningful format (e.g. a JSON object to indicate the structure), but I don't have any concrete plans to do that at the moment.

Variables

A variable, like <code>x</code>, is written as follows:

<div class="sourceCode"><pre class="sourceCode json"><code class="sourceCode json"><span class="fu">{</span> <span class="dt">"role"</span><span class="fu">:</span> <span class="st">"variable"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int"</span><span class="fu">,</span> <span class="dt">"id"</span><span class="fu">:</span> <span class="dv">0</span> <span class="fu">}</span></code></pre></div>

The <code>role</code> must be <code>variable</code>.

The <code>id</code> is a number, used to distinguish different variables within the same equation. For example, given an equation like <code>plus x y = plus y x</code> we must make <code>x</code> distinct from <code>y</code>, but <em>not</em> distinct from the other occurrence of <code>x</code>. We could do this by using an <code>id</code> of <code>0</code> for every occurrence of <code>x</code> and an <code>id</code> of <code>1</code> for every occurrence of <code>y</code>. Variables in separate equations are unrelated, so we can re-use the same <code>id</code> values without implying any sort of relationship between the variables of different equations. It is recommended to start with an <code>id</code> of <code>0</code> for the "left-most" variable and increment the <code>id</code> for each distinct variable when read from left to right.

Application

Function application, like <code>square 42</code>, is written as follows:

<div class="sourceCode"><pre class="sourceCode json"><code class="sourceCode json"><span class="fu">{</span> <span class="dt">"role"</span><span class="fu">:</span> <span class="st">"application"</span><span class="fu">,</span> <span class="dt">"lhs"</span><span class="fu">:</span> <span class="fu">{</span><span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int -> Int"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="st">"square"</span><span class="fu">},</span> <span class="dt">"rhs"</span><span class="fu">:</span> <span class="fu">{</span><span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="st">"42"</span><span class="fu">}</span> <span class="fu">}</span></code></pre></div>

The <code>role</code> must be <code>application</code>.

The <code>lhs</code> is the "left-hand-side", i.e. the thing we're calling. This can be any term.

The `<code>rhs</code> is the "right-hand-side", i.e. the argument we're passing. This can be any term.

Function application only accepts one argument, like in lambda calculus. Multiple arguments can be simulated using currying (nested applications).

It is recommended that the <code>lhs</code> be something of function type (either directly, in the case of a <code>constant</code> or <code>variable</code>; or as a result, in the case of another <code>application</code>). It is also recommended that the <code>rhs</code> be of a type compatible with the input of the <code>lhs</code>. I don't know of any tooling that uses the <code>type</code> fields, so it's up to you if you're going to bother, and what "compatible" means (e.g. w.r.t polymorphism, etc.).

Equations

An equation, stating that two terms are equal. These terms are referred to (arbitrarily) as the "left-hand-side" and the "right-hand-side". Any variables occurring in these terms are (implicitly) universally quantified. For example, to state that <code>25 = square 5</code> we write:

<div class="sourceCode"><pre class="sourceCode json"><code class="sourceCode json"><span class="fu">{</span> <span class="dt">"relation"</span><span class="fu">:</span> <span class="st">"~="</span><span class="fu">,</span> <span class="dt">"lhs"</span><span class="fu">:</span> <span class="fu">{</span><span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="dv">25</span><span class="fu">},</span> <span class="dt">"rhs"</span><span class="fu">:</span> <span class="fu">{</span> <span class="dt">"role"</span><span class="fu">:</span> <span class="st">"application"</span><span class="fu">,</span> <span class="dt">"lhs"</span><span class="fu">:</span> <span class="fu">{</span><span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int -> Int"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="st">"square"</span><span class="fu">},</span> <span class="dt">"rhs"</span><span class="fu">:</span> <span class="fu">{</span><span class="dt">"role"</span><span class="fu">:</span> <span class="st">"constant"</span><span class="fu">,</span> <span class="dt">"type"</span><span class="fu">:</span> <span class="st">"Int"</span><span class="fu">,</span> <span class="dt">"symbol"</span><span class="fu">:</span> <span class="st">"5"</span><span class="fu">}</span> <span class="fu">}</span> <span class="fu">}</span></code></pre></div>

The <code>relation</code> must be <code>~=</code>. This was chosen to indicate that we don't actually carry any proof or evidence of the stated equation; the tooling it comes from may be unreliable, or using different definitions to what we expect, or different rules of logic (e.g. classical versus constructive), etc.

The <code>lhs</code> is one of the equal terms. It will be rendered first.

The <code>rhs</code> is the other term. It will be rendered second.