<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html>
<head>
<!-- Generated by HsColour, http://www.cs.york.ac.uk/fp/darcs/hscolour/ -->
<title>src/Darcs/Patch/Properties.lhs</title>
<link type='text/css' rel='stylesheet' href='hscolour.css' />
</head>
<body>
% Copyright (C) 2007 David Roundy
%
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
%
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU General Public License
% along with this program; see the file COPYING. If not, write to
% the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
% Boston, MA 02110-1301, USA.
\documentclass{article}
%\usepackage{color}
\usepackage{verbatim}
\usepackage{html}
\usepackage{fancyvrb}
\newenvironment{code}{\comment}{\endcomment}
% \newenvironment{code}{\color{blue}\verbatim}{\endverbatim}
\newcommand{\commutes}{\longleftrightarrow}
\begin{document}
\begin{code}
<pre><a name="line-1"></a><span class='hs-comment'>{-# LANGUAGE CPP #-}</span>
<a name="line-2"></a><span class='hs-comment'>{-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts #-}</span>
<a name="line-3"></a>
<a name="line-4"></a><span class='hs-cpp'>#include "gadts.h"</span>
<a name="line-5"></a>
<a name="line-6"></a><span class='hs-keyword'>module</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Patch</span><span class='hs-varop'>.</span><span class='hs-conid'>Properties</span> <span class='hs-layout'>(</span> <span class='hs-varid'>recommute</span><span class='hs-layout'>,</span> <span class='hs-varid'>commute_inverses</span><span class='hs-layout'>,</span> <span class='hs-varid'>permutivity</span><span class='hs-layout'>,</span> <span class='hs-varid'>partial_permutivity</span><span class='hs-layout'>,</span>
<a name="line-7"></a> <span class='hs-varid'>identity_commutes</span><span class='hs-layout'>,</span> <span class='hs-varid'>inverse_doesnt_commute</span><span class='hs-layout'>,</span>
<a name="line-8"></a> <span class='hs-varid'>patch_and_inverse_commute</span><span class='hs-layout'>,</span> <span class='hs-varid'>merge_either_way</span><span class='hs-layout'>,</span>
<a name="line-9"></a> <span class='hs-varid'>show_read</span><span class='hs-layout'>,</span>
<a name="line-10"></a> <span class='hs-varid'>merge_commute</span><span class='hs-layout'>,</span> <span class='hs-varid'>merge_consistent</span><span class='hs-layout'>,</span> <span class='hs-varid'>merge_arguments_consistent</span><span class='hs-layout'>,</span>
<a name="line-11"></a> <span class='hs-varid'>join_inverses</span><span class='hs-layout'>,</span> <span class='hs-varid'>join_commute</span> <span class='hs-layout'>)</span> <span class='hs-keyword'>where</span>
<a name="line-12"></a>
<a name="line-13"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Control</span><span class='hs-varop'>.</span><span class='hs-conid'>Monad</span> <span class='hs-layout'>(</span> <span class='hs-varid'>msum</span><span class='hs-layout'>,</span> <span class='hs-varid'>mplus</span> <span class='hs-layout'>)</span>
<a name="line-14"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Witnesses</span><span class='hs-varop'>.</span><span class='hs-conid'>Show</span> <span class='hs-layout'>(</span> <span class='hs-conid'>Show2</span><span class='hs-layout'>(</span><span class='hs-keyglyph'>..</span><span class='hs-layout'>)</span> <span class='hs-layout'>)</span>
<a name="line-15"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Patch</span><span class='hs-varop'>.</span><span class='hs-conid'>Patchy</span>
<a name="line-16"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Patch</span><span class='hs-varop'>.</span><span class='hs-conid'>Prim</span>
<a name="line-17"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Patch</span> <span class='hs-conid'>()</span>
<a name="line-18"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Patch</span><span class='hs-varop'>.</span><span class='hs-conid'>Read</span> <span class='hs-layout'>(</span> <span class='hs-varid'>readPatch</span> <span class='hs-layout'>)</span>
<a name="line-19"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Witnesses</span><span class='hs-varop'>.</span><span class='hs-conid'>Ordered</span>
<a name="line-20"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Darcs</span><span class='hs-varop'>.</span><span class='hs-conid'>Witnesses</span><span class='hs-varop'>.</span><span class='hs-conid'>Sealed</span> <span class='hs-layout'>(</span> <span class='hs-conid'>Sealed</span><span class='hs-layout'>(</span><span class='hs-conid'>Sealed</span><span class='hs-layout'>)</span> <span class='hs-layout'>)</span>
<a name="line-21"></a><span class='hs-keyword'>import</span> <span class='hs-conid'>Printer</span> <span class='hs-layout'>(</span> <span class='hs-conid'>Doc</span><span class='hs-layout'>,</span> <span class='hs-varid'>renderPS</span><span class='hs-layout'>,</span> <span class='hs-varid'>redText</span><span class='hs-layout'>,</span> <span class='hs-varid'>greenText</span><span class='hs-layout'>,</span> <span class='hs-layout'>(</span><span class='hs-varop'>$$</span><span class='hs-layout'>)</span> <span class='hs-layout'>)</span>
<a name="line-22"></a><span class='hs-comment'>--import Darcs.ColorPrinter ( traceDoc )</span>
</pre>\end{code}
\section{Patch properties}
Darcs is built on a hierarchy of patch types. At the lowest level are
``primitive'' patches, and from these building blocks, a whole hierarchy of
patch types are built. Each of these patch types must support a number of
functions, which must obey a number of laws.
\subsection{Properties of identity}
\newtheorem{prp}{Property}
\begin{prp}[Identity commutes trivially]
The identity patch must commute with any patch without modifying said patch.
\end{prp}
\begin{code}
<pre><a name="line-1"></a><a name="identity_commutes"></a><span class='hs-definition'>identity_commutes</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-varop'>.</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-2"></a><span class='hs-definition'>identity_commutes</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>case</span> <span class='hs-varid'>commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>identity</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-3"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"identity_commutes failed:"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p</span>
<a name="line-4"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>i</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>identity</span><span class='hs-layout'>,</span>
<a name="line-5"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>p'</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>-></span>
<a name="line-6"></a> <span class='hs-varid'>checkRightIdentity</span> <span class='hs-varop'>$</span> <span class='hs-varid'>commute</span> <span class='hs-varop'>$</span> <span class='hs-varid'>identity</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span>
<a name="line-7"></a> <span class='hs-conid'>Just</span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"identity_commutes"</span>
<a name="line-8"></a> <span class='hs-keyword'>where</span> <span class='hs-varid'>checkRightIdentity</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-9"></a> <span class='hs-varid'>checkRightIdentity</span> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"identity_commutes failed 2:"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p</span>
<a name="line-10"></a> <span class='hs-varid'>checkRightIdentity</span> <span class='hs-layout'>(</span><span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>p2</span> <span class='hs-conop'>:></span> <span class='hs-varid'>i2</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>i2</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>identity</span><span class='hs-layout'>,</span>
<a name="line-11"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>p2</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Nothing</span>
<a name="line-12"></a> <span class='hs-varid'>checkRightIdentity</span> <span class='hs-layout'>(</span><span class='hs-conid'>Just</span> <span class='hs-keyword'>_</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"identity_commutes 2"</span>
</pre>\end{code}
\begin{prp}[Inverse doesn't commute]
A patch and its inverse will always commute, unless that patch is an
identity patch (or an identity-like patch that has no effect).
\end{prp}
\begin{code}
<pre><a name="line-1"></a><a name="inverse_doesnt_commute"></a><span class='hs-definition'>inverse_doesnt_commute</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-2"></a><span class='hs-definition'>inverse_doesnt_commute</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>sloppyIdentity</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Nothing</span>
<a name="line-3"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>do</span> <span class='hs-varid'>p'</span> <span class='hs-conop'>:></span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span>
<a name="line-4"></a> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"inverse_doesnt_commute"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p'</span>
</pre>\end{code}
\subsection{Commute properties}
\begin{prp}[Recommute]
$AB \commutes B'A'$ if and only if $B'A' \commutes AB$
\end{prp}
\begin{code}
<pre><a name="line-1"></a><a name="recommute"></a><span class='hs-definition'>recommute</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-2"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-3"></a><span class='hs-definition'>recommute</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-4"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-5"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-6"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>y'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-7"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>y'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-8"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"failed"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>":>"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span>
<a name="line-9"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>x''</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y''</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-10"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>y''</span> <span class='hs-varop'>=/\=</span> <span class='hs-varid'>y</span> <span class='hs-keyword'>of</span>
<a name="line-11"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"y'' =/\\= y failed, where x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-12"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-13"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-14"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-15"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x''"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x''</span> <span class='hs-varop'>$$</span>
<a name="line-16"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> y''"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y''</span><span class='hs-layout'>)</span>
<a name="line-17"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>x''</span> <span class='hs-varop'>=/\=</span> <span class='hs-varid'>x</span> <span class='hs-keyword'>of</span>
<a name="line-18"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"x'' /= x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x''</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>":>"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y''</span><span class='hs-layout'>)</span>
<a name="line-19"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
</pre>\end{code}
\begin{prp}[Commute inverses]
$AB \commutes B'A'$ if and only if $B^{-1}A^{-1} \commutes A'^{-1}B'^{-1}$
\end{prp}
\begin{code}
<pre><a name="line-1"></a><a name="commute_inverses"></a><span class='hs-definition'>commute_inverses</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-2"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-3"></a><span class='hs-definition'>commute_inverses</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-4"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-5"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-6"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>y'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-7"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>y</span> <span class='hs-conop'>:></span> <span class='hs-varid'>invert</span> <span class='hs-varid'>x</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-8"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"second commute failed"</span> <span class='hs-varop'>$$</span>
<a name="line-9"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-10"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span>
<a name="line-11"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>ix'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>iy'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-12"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>invert</span> <span class='hs-varid'>ix'</span> <span class='hs-varop'>=/\=</span> <span class='hs-varid'>x'</span> <span class='hs-keyword'>of</span>
<a name="line-13"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"invert ix' /= x'"</span> <span class='hs-varop'>$$</span>
<a name="line-14"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-15"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-16"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-17"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-18"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"ix'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>ix'</span> <span class='hs-varop'>$$</span>
<a name="line-19"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"iy'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>iy'</span> <span class='hs-varop'>$$</span>
<a name="line-20"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"invert ix'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>ix'</span><span class='hs-layout'>)</span> <span class='hs-varop'>$$</span>
<a name="line-21"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"invert iy'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>iy'</span><span class='hs-layout'>)</span>
<a name="line-22"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>invert</span> <span class='hs-varid'>iy'</span> <span class='hs-keyword'>of</span>
<a name="line-23"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"y' /= invert iy'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>iy'</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span>
<a name="line-24"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
</pre>\end{code}
\begin{prp}[Patch and inverse]
If $AB \commutes B'A'$ then $A^{-1}B' \commutes BA'^{-1}$
\end{prp}
This property is only true of primitive patches.
\begin{code}
<pre><a name="line-1"></a><a name="patch_and_inverse_commute"></a><span class='hs-definition'>patch_and_inverse_commute</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span>
<a name="line-2"></a> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-3"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-4"></a><span class='hs-definition'>patch_and_inverse_commute</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-5"></a> <span class='hs-keyword'>do</span> <span class='hs-varid'>y'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span>
<a name="line-6"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y'</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-7"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"failure in patch_and_inverse_commute"</span><span class='hs-layout'>)</span>
<a name="line-8"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>y''</span> <span class='hs-conop'>:></span> <span class='hs-varid'>ix'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-9"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>y''</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>y</span> <span class='hs-keyword'>of</span>
<a name="line-10"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"y'' /= y"</span> <span class='hs-varop'>$$</span>
<a name="line-11"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-12"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-13"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-14"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-15"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y''"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y''</span> <span class='hs-varop'>$$</span>
<a name="line-16"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span>
<a name="line-17"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>invert</span> <span class='hs-varid'>ix'</span> <span class='hs-keyword'>of</span>
<a name="line-18"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"x' /= invert ix'"</span> <span class='hs-varop'>$$</span>
<a name="line-19"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y''"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y''</span> <span class='hs-varop'>$$</span>
<a name="line-20"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-21"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"invert x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>x</span><span class='hs-layout'>)</span> <span class='hs-varop'>$$</span>
<a name="line-22"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>":> y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-23"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-24"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"ix'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>ix'</span><span class='hs-layout'>)</span>
<a name="line-25"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
</pre>\end{code}
\begin{prp}[Permutivity]
(to be added...)
\end{prp}
\begin{code}
<pre><a name="line-1"></a><a name="permutivity"></a><span class='hs-definition'>permutivity</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-2"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-3"></a><span class='hs-definition'>permutivity</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:></span><span class='hs-varid'>y</span><span class='hs-conop'>:></span><span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-4"></a> <span class='hs-keyword'>do</span> <span class='hs-varid'>y1</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x1</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span>
<a name="line-5"></a> <span class='hs-varid'>z2</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y2</span> <span class='hs-keyglyph'><-</span> <span class='hs-comment'>--traceDoc (greenText "first commuted") $</span>
<a name="line-6"></a> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>y</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span>
<a name="line-7"></a> <span class='hs-varid'>z3</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x3</span> <span class='hs-keyglyph'><-</span> <span class='hs-comment'>--traceDoc (greenText "second commuted") $</span>
<a name="line-8"></a> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z2</span><span class='hs-layout'>)</span>
<a name="line-9"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x1</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-10"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity1"</span>
<a name="line-11"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>z4</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x4</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-12"></a> <span class='hs-comment'>--traceDoc (greenText "third commuted" $$</span>
<a name="line-13"></a> <span class='hs-comment'>-- greenText "about to commute" $$</span>
<a name="line-14"></a> <span class='hs-comment'>-- greenText "y1" $$ showPatch y1 $$</span>
<a name="line-15"></a> <span class='hs-comment'>-- greenText "z4" $$ showPatch z4) $</span>
<a name="line-16"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>y1</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z4</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-17"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity2"</span>
<a name="line-18"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>z3_</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y4</span><span class='hs-layout'>)</span>
<a name="line-19"></a> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>z3_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>z3</span> <span class='hs-keyglyph'>-></span>
<a name="line-20"></a> <span class='hs-comment'>--traceDoc (greenText "passed z3") $ error "foobar test" $</span>
<a name="line-21"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>y4</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x4</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-22"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity5: input was"</span> <span class='hs-varop'>$$</span>
<a name="line-23"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-24"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-25"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"z"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>z</span> <span class='hs-varop'>$$</span>
<a name="line-26"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"z3"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>z3</span> <span class='hs-varop'>$$</span>
<a name="line-27"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"failed commute of"</span> <span class='hs-varop'>$$</span>
<a name="line-28"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y4"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y4</span> <span class='hs-varop'>$$</span>
<a name="line-29"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x4"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x4</span> <span class='hs-varop'>$$</span>
<a name="line-30"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"whereas commute of x and y give"</span> <span class='hs-varop'>$$</span>
<a name="line-31"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y1"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y1</span> <span class='hs-varop'>$$</span>
<a name="line-32"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x1"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x1</span>
<a name="line-33"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>x3_</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y2_</span><span class='hs-layout'>)</span>
<a name="line-34"></a> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>x3_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>x3</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity6"</span>
<a name="line-35"></a> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>y2_</span> <span class='hs-varop'>=/\=</span> <span class='hs-varid'>y2</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity7"</span>
<a name="line-36"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-37"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span>
<a name="line-38"></a> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"permutivity failed"</span> <span class='hs-varop'>$$</span>
<a name="line-39"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"z3"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>z3</span> <span class='hs-varop'>$$</span>
<a name="line-40"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"z3_"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>z3_</span>
<a name="line-41"></a>
<a name="line-42"></a><a name="partial_permutivity"></a><span class='hs-definition'>partial_permutivity</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-43"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-44"></a><span class='hs-definition'>partial_permutivity</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>xx</span><span class='hs-conop'>:></span><span class='hs-varid'>yy</span><span class='hs-conop'>:></span><span class='hs-varid'>zz</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>pp</span> <span class='hs-layout'>(</span><span class='hs-varid'>xx</span><span class='hs-conop'>:></span><span class='hs-varid'>yy</span><span class='hs-conop'>:></span><span class='hs-varid'>zz</span><span class='hs-layout'>)</span> <span class='hs-varop'>`mplus`</span> <span class='hs-varid'>pp</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>zz</span><span class='hs-conop'>:></span><span class='hs-varid'>invert</span> <span class='hs-varid'>yy</span><span class='hs-conop'>:></span><span class='hs-varid'>invert</span> <span class='hs-varid'>xx</span><span class='hs-layout'>)</span>
<a name="line-45"></a> <span class='hs-keyword'>where</span> <span class='hs-varid'>pp</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:></span><span class='hs-varid'>y</span><span class='hs-conop'>:></span><span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>do</span> <span class='hs-varid'>z1</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y1</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>y</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span>
<a name="line-46"></a> <span class='hs-keyword'>_</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x1</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>z1</span><span class='hs-layout'>)</span>
<a name="line-47"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-48"></a> <span class='hs-conid'>Just</span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span> <span class='hs-comment'>-- this is covered by full permutivity test above</span>
<a name="line-49"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span>
<a name="line-50"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>c</span> <span class='hs-layout'>(</span><span class='hs-varid'>x1</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y1</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-51"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-52"></a> <span class='hs-conid'>Just</span> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"partial_permutivity error"</span> <span class='hs-varop'>$$</span>
<a name="line-53"></a> <span class='hs-varid'>greenText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-54"></a> <span class='hs-varid'>greenText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-55"></a> <span class='hs-varid'>greenText</span> <span class='hs-str'>"z"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>z</span>
<a name="line-56"></a>
<a name="line-57"></a><a name="merge_arguments_consistent"></a><span class='hs-definition'>merge_arguments_consistent</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span>
<a name="line-58"></a> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span><span class='hs-layout'>)</span>
<a name="line-59"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-60"></a><span class='hs-definition'>merge_arguments_consistent</span> <span class='hs-varid'>is_consistent</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-61"></a> <span class='hs-varid'>msum</span> <span class='hs-keyglyph'>[</span><span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_arguments_consistent x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>x</span><span class='hs-layout'>,</span>
<a name="line-62"></a> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_arguments_consistent y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>y</span><span class='hs-keyglyph'>]</span>
<a name="line-63"></a>
<a name="line-64"></a><a name="merge_consistent"></a><span class='hs-definition'>merge_consistent</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span>
<a name="line-65"></a> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span><span class='hs-layout'>)</span>
<a name="line-66"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-67"></a><span class='hs-definition'>merge_consistent</span> <span class='hs-varid'>is_consistent</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-68"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>merge</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-69"></a> <span class='hs-varid'>y'</span> <span class='hs-conop'>:/\:</span> <span class='hs-varid'>x'</span> <span class='hs-keyglyph'>-></span>
<a name="line-70"></a> <span class='hs-varid'>msum</span> <span class='hs-keyglyph'>[</span><span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_consistent x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>x</span><span class='hs-layout'>,</span>
<a name="line-71"></a> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_consistent y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>y</span><span class='hs-layout'>,</span>
<a name="line-72"></a> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_consistent x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span> <span class='hs-varop'>$$</span>
<a name="line-73"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"where x' comes from x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-74"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"and y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>x'</span><span class='hs-layout'>,</span>
<a name="line-75"></a> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_consistent y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> <span class='hs-varop'>`fmap`</span> <span class='hs-varid'>is_consistent</span> <span class='hs-varid'>y'</span><span class='hs-keyglyph'>]</span>
<a name="line-76"></a>
<a name="line-77"></a><a name="merge_either_way"></a><span class='hs-definition'>merge_either_way</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-78"></a><span class='hs-definition'>merge_either_way</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-79"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>merge</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-80"></a> <span class='hs-varid'>y'</span> <span class='hs-conop'>:/\:</span> <span class='hs-varid'>x'</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>merge</span> <span class='hs-layout'>(</span><span class='hs-varid'>y</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>x</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-81"></a> <span class='hs-varid'>x''</span> <span class='hs-conop'>:/\:</span> <span class='hs-varid'>y''</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>x''</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>x'</span><span class='hs-layout'>,</span>
<a name="line-82"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>y''</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>y'</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-83"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_either_way bug"</span>
<a name="line-84"></a>
<a name="line-85"></a><a name="merge_commute"></a><span class='hs-definition'>merge_commute</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=></span> <span class='hs-layout'>(</span><span class='hs-varid'>p</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-86"></a><span class='hs-definition'>merge_commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-87"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>merge</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:\/:</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-88"></a> <span class='hs-varid'>y'</span> <span class='hs-conop'>:/\:</span> <span class='hs-varid'>x'</span> <span class='hs-keyglyph'>-></span>
<a name="line-89"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y'</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-90"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_commute 1"</span> <span class='hs-varop'>$$</span>
<a name="line-91"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-92"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-93"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-94"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span>
<a name="line-95"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>y_</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'_</span><span class='hs-layout'>)</span>
<a name="line-96"></a> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>y_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>y</span><span class='hs-layout'>,</span>
<a name="line-97"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>x'_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>x'</span> <span class='hs-keyglyph'>-></span>
<a name="line-98"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>y</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x'</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-99"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_commute 2 failed"</span> <span class='hs-varop'>$$</span>
<a name="line-100"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-101"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-102"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-103"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span>
<a name="line-104"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>x_</span> <span class='hs-conop'>:></span> <span class='hs-varid'>y'_</span><span class='hs-layout'>)</span>
<a name="line-105"></a> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>x_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>x</span><span class='hs-layout'>,</span>
<a name="line-106"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>y'_</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>y'</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-107"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_commute 3"</span> <span class='hs-varop'>$$</span>
<a name="line-108"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-109"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-110"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-111"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-112"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x_"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x_</span> <span class='hs-varop'>$$</span>
<a name="line-113"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'_"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'_</span>
<a name="line-114"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"merge_commute 4"</span> <span class='hs-varop'>$$</span>
<a name="line-115"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x</span> <span class='hs-varop'>$$</span>
<a name="line-116"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y</span> <span class='hs-varop'>$$</span>
<a name="line-117"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>$$</span>
<a name="line-118"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y'"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y'</span> <span class='hs-varop'>$$</span>
<a name="line-119"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"x'_"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>x'_</span> <span class='hs-varop'>$$</span>
<a name="line-120"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"y_"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>y_</span>
<a name="line-121"></a>
<a name="line-122"></a><a name="join_inverses"></a><span class='hs-definition'>join_inverses</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Prim</span> <span class='hs-conop'>:></span> <span class='hs-conid'>Prim</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-conid'>Prim</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-123"></a> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prim</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-124"></a><span class='hs-definition'>join_inverses</span> <span class='hs-varid'>j</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>case</span> <span class='hs-varid'>j</span> <span class='hs-layout'>(</span><span class='hs-varid'>invert</span> <span class='hs-varid'>p</span> <span class='hs-conop'>:></span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-125"></a> <span class='hs-conid'>Just</span> <span class='hs-conid'>Identity</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-126"></a> <span class='hs-conid'>Just</span> <span class='hs-varid'>p'</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"join_inverses gave just"</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p'</span>
<a name="line-127"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"join_inverses failed"</span>
<a name="line-128"></a>
<a name="line-129"></a><a name="join_commute"></a><span class='hs-definition'>join_commute</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>FORALL</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Prim</span> <span class='hs-conop'>:></span> <span class='hs-conid'>Prim</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-layout'>(</span><span class='hs-conid'>Prim</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varid'>y</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
<a name="line-130"></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Prim</span> <span class='hs-conop'>:></span> <span class='hs-conid'>Prim</span> <span class='hs-conop'>:></span> <span class='hs-conid'>Prim</span><span class='hs-layout'>)</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-131"></a><span class='hs-definition'>join_commute</span> <span class='hs-varid'>j</span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-conop'>:></span> <span class='hs-varid'>b</span> <span class='hs-conop'>:></span> <span class='hs-varid'>c</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span>
<a name="line-132"></a> <span class='hs-keyword'>do</span> <span class='hs-varid'>x</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>j</span> <span class='hs-layout'>(</span><span class='hs-varid'>b</span> <span class='hs-conop'>:></span> <span class='hs-varid'>c</span><span class='hs-layout'>)</span>
<a name="line-133"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>commuteFL</span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-conop'>:></span> <span class='hs-varid'>b</span> <span class='hs-conop'>:>:</span> <span class='hs-varid'>c</span> <span class='hs-conop'>:>:</span> <span class='hs-conid'>NilFL</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-134"></a> <span class='hs-conid'>Right</span> <span class='hs-layout'>(</span><span class='hs-varid'>b'</span> <span class='hs-conop'>:>:</span> <span class='hs-varid'>c'</span> <span class='hs-conop'>:>:</span> <span class='hs-conid'>NilFL</span> <span class='hs-conop'>:></span> <span class='hs-varid'>a'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-135"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>commute</span> <span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-conop'>:></span> <span class='hs-varid'>x</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-136"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"join_commute 1"</span>
<a name="line-137"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>x'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>a''</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span>
<a name="line-138"></a> <span class='hs-keyword'>case</span> <span class='hs-varid'>a''</span> <span class='hs-varop'>=/\=</span> <span class='hs-varid'>a'</span> <span class='hs-keyword'>of</span>
<a name="line-139"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"join_commute 3"</span>
<a name="line-140"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>j</span> <span class='hs-layout'>(</span><span class='hs-varid'>b'</span> <span class='hs-conop'>:></span> <span class='hs-varid'>c'</span><span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<a name="line-141"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"join_commute 4"</span>
<a name="line-142"></a> <span class='hs-conid'>Just</span> <span class='hs-varid'>x''</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <span class='hs-varid'>x'</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>x''</span> <span class='hs-keyword'>of</span>
<a name="line-143"></a> <span class='hs-conid'>NotEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>greenText</span> <span class='hs-str'>"join_commute 5"</span>
<a name="line-144"></a> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-145"></a> <span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-146"></a>
<a name="line-147"></a><a name="show_read"></a><span class='hs-definition'>show_read</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>Show2</span> <span class='hs-varid'>p</span><span class='hs-layout'>,</span> <span class='hs-conid'>Patchy</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=></span> <span class='hs-varid'>p</span> <span class='hs-conid'>C</span><span class='hs-layout'>(</span><span class='hs-varid'>a</span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Maybe</span> <span class='hs-conid'>Doc</span>
<a name="line-148"></a><span class='hs-definition'>show_read</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>let</span> <span class='hs-varid'>ps</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>renderPS</span> <span class='hs-layout'>(</span><span class='hs-varid'>showPatch</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span>
<a name="line-149"></a> <span class='hs-keyword'>in</span> <span class='hs-keyword'>case</span> <span class='hs-varid'>readPatch</span> <span class='hs-varid'>ps</span> <span class='hs-keyword'>of</span>
<a name="line-150"></a> <span class='hs-conid'>Nothing</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-varid'>redText</span> <span class='hs-str'>"unable to read "</span> <span class='hs-varop'>$$</span> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span>
<a name="line-151"></a> <span class='hs-conid'>Just</span> <span class='hs-layout'>(</span><span class='hs-conid'>Sealed</span> <span class='hs-varid'>p'</span><span class='hs-layout'>,</span><span class='hs-keyword'>_</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>IsEq</span> <span class='hs-keyglyph'><-</span> <span class='hs-varid'>p'</span> <span class='hs-varop'>=\/=</span> <span class='hs-varid'>p</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nothing</span>
<a name="line-152"></a> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Just</span> <span class='hs-varop'>$</span> <span class='hs-varid'>redText</span> <span class='hs-str'>"trouble reading patch p"</span> <span class='hs-varop'>$$</span>
<a name="line-153"></a> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p</span> <span class='hs-varop'>$$</span>
<a name="line-154"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"reads as p'"</span> <span class='hs-varop'>$$</span>
<a name="line-155"></a> <span class='hs-varid'>showPatch</span> <span class='hs-varid'>p'</span> <span class='hs-varop'>$$</span>
<a name="line-156"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"aka"</span> <span class='hs-varop'>$$</span>
<a name="line-157"></a> <span class='hs-varid'>greenText</span> <span class='hs-layout'>(</span><span class='hs-varid'>show2</span> <span class='hs-varid'>p</span><span class='hs-layout'>)</span> <span class='hs-varop'>$$</span>
<a name="line-158"></a> <span class='hs-varid'>redText</span> <span class='hs-str'>"and"</span> <span class='hs-varop'>$$</span>
<a name="line-159"></a> <span class='hs-varid'>greenText</span> <span class='hs-layout'>(</span><span class='hs-varid'>show2</span> <span class='hs-varid'>p'</span><span class='hs-layout'>)</span>
</pre>\end{code}
\end{document}
</body>
</html>
