Or.lhs

% Or Simplification

== Header

\begin{code}
{-|
Module      : Kore.Step.Simplification.Or
Description : Tools for Or pattern simplification.
Copyright   : (c) Runtime Verification, 2018
License     : NCSA
Maintainer  : virgil.serbanuta@runtimeverification.com
Stability   : experimental
Portability : portable
-}
module Kore.Step.Simplification.Or
    ( simplifyEvaluated
    , simplify
    ) where

import           Control.Applicative
                 ( Alternative (..) )
import qualified Data.Functor.Foldable as Recursive

import           Kore.AST.Pure
import           Kore.Predicate.Predicate
                 ( makeOrPredicate )
import           Kore.Step.ExpandedPattern
                 ( ExpandedPattern, Predicated (..) )
import           Kore.Step.OrOfExpandedPattern
                 ( OrOfExpandedPattern )
import qualified Kore.Step.OrOfExpandedPattern as OrOfExpandedPattern
                 ( extractPatterns, make, merge )
import           Kore.Step.Simplification.Data
                 ( SimplificationProof (..) )
import           Kore.Unparser
\end{code}

== Driver

\begin{code}
{-|'simplify' simplifies an 'Or' pattern with 'OrOfExpandedPattern'
children by merging the two children.
-}
simplify
    ::  ( MetaOrObject level
        , SortedVariable variable
        , Ord (variable level)
        , Show (variable level)
        , Unparse (variable level)
        )
    => Or level (OrOfExpandedPattern level variable)
    ->  ( OrOfExpandedPattern level variable
        , SimplificationProof level
        )
\end{code}

`simplify` is a driver responsible for breaking down an `\or` pattern and
simplifying its children.

\begin{code}
simplify
    Or
        { orFirst = first
        , orSecond = second
        }
  =
    simplifyEvaluated first second

{-| simplifies an 'Or' given its two 'OrOfExpandedPattern' children.

See 'simplify' for detailed documentation.
-}
simplifyEvaluated
    ::  ( MetaOrObject level
        , SortedVariable variable
        , Ord (variable level)
        , Show (variable level)
        , Unparse (variable level)
        )
    => OrOfExpandedPattern level variable
    -> OrOfExpandedPattern level variable
    ->  ( OrOfExpandedPattern level variable
        , SimplificationProof level
        )
\end{code}

**TODO** (virgil): Preserve pattern sorts under simplification.
One way to preserve the required sort annotations is to make `simplifyEvaluated`
take an argument of type
``` haskell
CofreeF (Or level) (Valid level) (OrOfExpandedPattern level variable)
```
instead of two `OrOfExpandedPattern` arguments. The type of `makeEvaluate` may
be changed analogously. The `Valid` annotation will eventually cache
information besides the pattern sort, which will make it even more useful to
carry around.

**TODO** (virgil): This should do all possible mergings, not just the first term
with the second.

\begin{code}
simplifyEvaluated first second

  | (head1 : tail1) <- OrOfExpandedPattern.extractPatterns first
  , (head2 : tail2) <- OrOfExpandedPattern.extractPatterns second
  , Just (result, proof) <- simplifySinglePatterns head1 head2
  = (OrOfExpandedPattern.make $ result : (tail1 ++ tail2), proof)

  | otherwise =
    ( OrOfExpandedPattern.merge first second
    , SimplificationProof
    )

  where
    simplifySinglePatterns first' second' =
        disjoinPredicates first' second' <|> topAnnihilates first' second'
\end{code}

== Disjoin predicates

\begin{code}
{- | Merge two configurations by the disjunction of their predicates.

This simplification case is only applied if the configurations have the same
'term'.

 -}
disjoinPredicates
    ::  ( MetaOrObject level
        , SortedVariable variable
        , Ord (variable level)
        , Show (variable level)
        , Unparse (variable level)
        )
    => ExpandedPattern level variable
    -- ^ Configuration
    -> ExpandedPattern level variable
    -- ^ Disjunction
    -> Maybe (ExpandedPattern level variable, SimplificationProof level)
\end{code}

When two configurations have the same substitution, it may be possible to
simplify the pair by disjunction of their predicates.
```
(             t₁, p₁, s) ∨ (             t₂, p₂, s)
([t₂ ∨ ¬t₂] ∧ t₁, p₁, s) ∨ ([t₁ ∨ ¬t₁] ∧ t₂, p₂, s)

(t₁ ∧ t₂, p₁ ∨ p₂, s) ∨ (¬t₂ ∧ t₁, p₁, s) ∨ (¬t₁ ∧ t₂, p₂, s)
```
It is useful to apply the above equality when
```
¬t₂ ∧ t₁ = ¬t₁ ∧ t₂ = ⊥
```
so that
```
(t₁, p₁, s) ∨ (t₂, p₂, s) = (t₁ ∧ t₂, p₁ ∨ p₂, s)
  where
    ¬t₂ ∧ t₁ = ¬t₁ ∧ t₂ = ⊥.
```
Checking the side condition may be expensive, so in practice we only apply this
simplification when `t₁=t₂`.

**Note**: It is not clear that we should *ever* apply this simplification.  We
attempt to refute the conditions on configurations using an external solver to
reduce the configuration space for execution.  The solver operates best when it
has the most information, and the predicate `p₁ ∨ p₂` is strictly weaker than
either `p₁` or `p₂`.

\begin{code}
disjoinPredicates
    predicated1@Predicated
        { term = term1
        , predicate = predicate1
        , substitution = substitution1
        }
    Predicated
        { term = term2
        , predicate = predicate2
        , substitution = substitution2
        }

  | term1         == term2
  , substitution1 == substitution2
  = Just (result, SimplificationProof)

  | otherwise =
    Nothing

  where
    result = predicated1 { predicate = makeOrPredicate predicate1 predicate2 }
\end{code}

== `\top` annihilates `\or`

\begin{code}
{- | 'Top' patterns are the annihilator of 'Or'.
 -}
topAnnihilates
    ::  ( MetaOrObject level
        , SortedVariable variable
        , Ord (variable level)
        , Show (variable level)
        , Unparse (variable level)
        )
    => ExpandedPattern level variable
    -- ^ Configuration
    -> ExpandedPattern level variable
    -- ^ Disjunction
    -> Maybe (ExpandedPattern level variable, SimplificationProof level)
\end{code}

`⊤` is the annihilator of `∨`; when two configurations have the same
substitution, it may be possible to use this property to simplify the pair by
annihilating the lesser term.
```
(⊤,              p₁, s) ∨ (t₂,              p₂, s)
(⊤, [p₂ ∨ ¬p₂] ∧ p₁, s) ∨ (t₂, [p₁ ∨ ¬p₁] ∧ p₂, s)

(⊤, p₁ ∧ p₂, s) ∨ (⊤, p₁ ∧ ¬p₂, s) ∨ (t₂, ¬p₁ ∧ p₂, s)
```
It is useful to apply the above equality when
```
¬p₂ ∧ p₁ = ¬p₁ ∧ p₂ = ⊥
```
so that
```
(⊤, p₁, s) ∨ (t₂, p₂, s) = (⊤, p₁ ∧ p₂, s)
  where
    ¬p₂ ∧ p₁ = ¬p₁ ∧ p₂ = ⊥.
```
Checking the side condition may be expensive, so in practice we only apply this
simplification when `p₁ = p₂`.

\begin{code}
topAnnihilates
    predicated1@Predicated
        { term = term1
        , predicate = predicate1
        , substitution = substitution1
        }
    predicated2@Predicated
        { term = term2
        , predicate = predicate2
        , substitution = substitution2
        }

  -- The 'term's are checked first because checking the equality of predicates
  -- and substitutions could be expensive.

  | _ :< TopPattern _ <- Recursive.project term1
  , predicate1    == predicate2
  , substitution1 == substitution2
  = Just (predicated1, SimplificationProof)

  | _ :< TopPattern _ <- Recursive.project term2
  , predicate1    == predicate2
  , substitution1 == substitution2
  = Just (predicated2, SimplificationProof)

  | otherwise =
    Nothing
\end{code}

Simplification-Or.html

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang xml:lang>
<head>
  <meta charset="utf-8" />
  <meta name="generator" content="pandoc" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
  <title>Or Simplification</title>
  <style type="text/css">
      code{white-space: pre-wrap;}
      span.smallcaps{font-variant: small-caps;}
      span.underline{text-decoration: underline;}
      div.column{display: inline-block; vertical-align: top; width: 50%;}
  </style>
  <style type="text/css">
a.sourceLine { display: inline-block; line-height: 1.25; }
a.sourceLine { pointer-events: none; color: inherit; text-decoration: inherit; }
a.sourceLine:empty { height: 1.2em; }
.sourceCode { overflow: visible; }
code.sourceCode { white-space: pre; position: relative; }
div.sourceCode { margin: 1em 0; }
pre.sourceCode { margin: 0; }
@media screen {
div.sourceCode { overflow: auto; }
}
@media print {
code.sourceCode { white-space: pre-wrap; }
a.sourceLine { text-indent: -1em; padding-left: 1em; }
}
pre.numberSource a.sourceLine
  { position: relative; left: -4em; }
pre.numberSource a.sourceLine::before
  { content: attr(title);
    position: relative; left: -1em; text-align: right; vertical-align: baseline;
    border: none; pointer-events: all; display: inline-block;
    -webkit-touch-callout: none; -webkit-user-select: none;
    -khtml-user-select: none; -moz-user-select: none;
    -ms-user-select: none; user-select: none;
    padding: 0 4px; width: 4em;
    color: #aaaaaa;
  }
pre.numberSource { margin-left: 3em; border-left: 1px solid #aaaaaa;  padding-left: 4px; }
div.sourceCode
  {  }
@media screen {
a.sourceLine::before { text-decoration: underline; }
}
code span.al { color: #ff0000; font-weight: bold; } /* Alert */
code span.an { color: #60a0b0; font-weight: bold; font-style: italic; } /* Annotation */
code span.at { color: #7d9029; } /* Attribute */
code span.bn { color: #40a070; } /* BaseN */
code span.bu { } /* BuiltIn */
code span.cf { color: #007020; font-weight: bold; } /* ControlFlow */
code span.ch { color: #4070a0; } /* Char */
code span.cn { color: #880000; } /* Constant */
code span.co { color: #60a0b0; font-style: italic; } /* Comment */
code span.cv { color: #60a0b0; font-weight: bold; font-style: italic; } /* CommentVar */
code span.do { color: #ba2121; font-style: italic; } /* Documentation */
code span.dt { color: #902000; } /* DataType */
code span.dv { color: #40a070; } /* DecVal */
code span.er { color: #ff0000; font-weight: bold; } /* Error */
code span.ex { } /* Extension */
code span.fl { color: #40a070; } /* Float */
code span.fu { color: #06287e; } /* Function */
code span.im { } /* Import */
code span.in { color: #60a0b0; font-weight: bold; font-style: italic; } /* Information */
code span.kw { color: #007020; font-weight: bold; } /* Keyword */
code span.op { color: #666666; } /* Operator */
code span.ot { color: #007020; } /* Other */
code span.pp { color: #bc7a00; } /* Preprocessor */
code span.sc { color: #4070a0; } /* SpecialChar */
code span.ss { color: #bb6688; } /* SpecialString */
code span.st { color: #4070a0; } /* String */
code span.va { color: #19177c; } /* Variable */
code span.vs { color: #4070a0; } /* VerbatimString */
code span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */
  </style>
  <!--[if lt IE 9]>
    <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
  <![endif]-->
</head>
<body>
<header id="title-block-header">
<h1 class="title">Or Simplification</h1>
</header>
<h2 id="header">Header</h2>
<div class="sourceCode" id="cb1"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb1-1" title="1"><span class="co">{-|</span></a>
<a class="sourceLine" id="cb1-2" title="2"><span class="co">Module      : Kore.Step.Simplification.Or</span></a>
<a class="sourceLine" id="cb1-3" title="3"><span class="co">Description : Tools for Or pattern simplification.</span></a>
<a class="sourceLine" id="cb1-4" title="4"><span class="co">Copyright   : (c) Runtime Verification, 2018</span></a>
<a class="sourceLine" id="cb1-5" title="5"><span class="co">License     : NCSA</span></a>
<a class="sourceLine" id="cb1-6" title="6"><span class="co">Maintainer  : virgil.serbanuta@runtimeverification.com</span></a>
<a class="sourceLine" id="cb1-7" title="7"><span class="co">Stability   : experimental</span></a>
<a class="sourceLine" id="cb1-8" title="8"><span class="co">Portability : portable</span></a>
<a class="sourceLine" id="cb1-9" title="9"><span class="co">-}</span></a>
<a class="sourceLine" id="cb1-10" title="10"><span class="kw">module</span> <span class="dt">Kore.Step.Simplification.Or</span></a>
<a class="sourceLine" id="cb1-11" title="11">    ( simplifyEvaluated</a>
<a class="sourceLine" id="cb1-12" title="12">    , simplify</a>
<a class="sourceLine" id="cb1-13" title="13">    ) <span class="kw">where</span></a>
<a class="sourceLine" id="cb1-14" title="14"></a>
<a class="sourceLine" id="cb1-15" title="15"><span class="kw">import</span>           <span class="dt">Control.Applicative</span></a>
<a class="sourceLine" id="cb1-16" title="16">                 ( <span class="dt">Alternative</span> (<span class="fu">..</span>) )</a>
<a class="sourceLine" id="cb1-17" title="17"><span class="kw">import</span> <span class="kw">qualified</span> <span class="dt">Data.Functor.Foldable</span> <span class="kw">as</span> <span class="dt">Recursive</span></a>
<a class="sourceLine" id="cb1-18" title="18"></a>
<a class="sourceLine" id="cb1-19" title="19"><span class="kw">import</span>           <span class="dt">Kore.AST.Pure</span></a>
<a class="sourceLine" id="cb1-20" title="20"><span class="kw">import</span>           <span class="dt">Kore.Predicate.Predicate</span></a>
<a class="sourceLine" id="cb1-21" title="21">                 ( makeOrPredicate )</a>
<a class="sourceLine" id="cb1-22" title="22"><span class="kw">import</span>           <span class="dt">Kore.Step.ExpandedPattern</span></a>
<a class="sourceLine" id="cb1-23" title="23">                 ( <span class="dt">ExpandedPattern</span>, <span class="dt">Predicated</span> (<span class="fu">..</span>) )</a>
<a class="sourceLine" id="cb1-24" title="24"><span class="kw">import</span>           <span class="dt">Kore.Step.OrOfExpandedPattern</span></a>
<a class="sourceLine" id="cb1-25" title="25">                 ( <span class="dt">OrOfExpandedPattern</span> )</a>
<a class="sourceLine" id="cb1-26" title="26"><span class="kw">import</span> <span class="kw">qualified</span> <span class="dt">Kore.Step.OrOfExpandedPattern</span> <span class="kw">as</span> <span class="dt">OrOfExpandedPattern</span></a>
<a class="sourceLine" id="cb1-27" title="27">                 ( extractPatterns, make, merge )</a>
<a class="sourceLine" id="cb1-28" title="28"><span class="kw">import</span>           <span class="dt">Kore.Step.Simplification.Data</span></a>
<a class="sourceLine" id="cb1-29" title="29">                 ( <span class="dt">SimplificationProof</span> (<span class="fu">..</span>) )</a>
<a class="sourceLine" id="cb1-30" title="30"><span class="kw">import</span>           <span class="dt">Kore.Unparser</span></a></code></pre></div>
<h2 id="driver">Driver</h2>
<div class="sourceCode" id="cb2"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb2-1" title="1"><span class="co">{-|&#39;simplify&#39; simplifies an &#39;Or&#39; pattern with &#39;OrOfExpandedPattern&#39;</span></a>
<a class="sourceLine" id="cb2-2" title="2"><span class="co">children by merging the two children.</span></a>
<a class="sourceLine" id="cb2-3" title="3"><span class="co">-}</span></a>
<a class="sourceLine" id="cb2-4" title="4">simplify</a>
<a class="sourceLine" id="cb2-5" title="5"><span class="ot">    ::</span>  ( <span class="dt">MetaOrObject</span> level</a>
<a class="sourceLine" id="cb2-6" title="6">        , <span class="dt">SortedVariable</span> variable</a>
<a class="sourceLine" id="cb2-7" title="7">        , <span class="dt">Ord</span> (variable level)</a>
<a class="sourceLine" id="cb2-8" title="8">        , <span class="dt">Show</span> (variable level)</a>
<a class="sourceLine" id="cb2-9" title="9">        , <span class="dt">Unparse</span> (variable level)</a>
<a class="sourceLine" id="cb2-10" title="10">        )</a>
<a class="sourceLine" id="cb2-11" title="11">    <span class="ot">=&gt;</span> <span class="dt">Or</span> level (<span class="dt">OrOfExpandedPattern</span> level variable)</a>
<a class="sourceLine" id="cb2-12" title="12">    <span class="ot">-&gt;</span>  ( <span class="dt">OrOfExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb2-13" title="13">        , <span class="dt">SimplificationProof</span> level</a>
<a class="sourceLine" id="cb2-14" title="14">        )</a></code></pre></div>
<p><code>simplify</code> is a driver responsible for breaking down an <code>\or</code> pattern and simplifying its children.</p>
<div class="sourceCode" id="cb3"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb3-1" title="1">simplify</a>
<a class="sourceLine" id="cb3-2" title="2">    <span class="dt">Or</span></a>
<a class="sourceLine" id="cb3-3" title="3">        { orFirst <span class="fu">=</span> first</a>
<a class="sourceLine" id="cb3-4" title="4">        , orSecond <span class="fu">=</span> second</a>
<a class="sourceLine" id="cb3-5" title="5">        }</a>
<a class="sourceLine" id="cb3-6" title="6">  <span class="fu">=</span></a>
<a class="sourceLine" id="cb3-7" title="7">    simplifyEvaluated first second</a>
<a class="sourceLine" id="cb3-8" title="8"></a>
<a class="sourceLine" id="cb3-9" title="9"><span class="co">{-| simplifies an &#39;Or&#39; given its two &#39;OrOfExpandedPattern&#39; children.</span></a>
<a class="sourceLine" id="cb3-10" title="10"></a>
<a class="sourceLine" id="cb3-11" title="11"><span class="co">See &#39;simplify&#39; for detailed documentation.</span></a>
<a class="sourceLine" id="cb3-12" title="12"><span class="co">-}</span></a>
<a class="sourceLine" id="cb3-13" title="13">simplifyEvaluated</a>
<a class="sourceLine" id="cb3-14" title="14"><span class="ot">    ::</span>  ( <span class="dt">MetaOrObject</span> level</a>
<a class="sourceLine" id="cb3-15" title="15">        , <span class="dt">SortedVariable</span> variable</a>
<a class="sourceLine" id="cb3-16" title="16">        , <span class="dt">Ord</span> (variable level)</a>
<a class="sourceLine" id="cb3-17" title="17">        , <span class="dt">Show</span> (variable level)</a>
<a class="sourceLine" id="cb3-18" title="18">        , <span class="dt">Unparse</span> (variable level)</a>
<a class="sourceLine" id="cb3-19" title="19">        )</a>
<a class="sourceLine" id="cb3-20" title="20">    <span class="ot">=&gt;</span> <span class="dt">OrOfExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb3-21" title="21">    <span class="ot">-&gt;</span> <span class="dt">OrOfExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb3-22" title="22">    <span class="ot">-&gt;</span>  ( <span class="dt">OrOfExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb3-23" title="23">        , <span class="dt">SimplificationProof</span> level</a>
<a class="sourceLine" id="cb3-24" title="24">        )</a></code></pre></div>
<p><strong>TODO</strong> (virgil): Preserve pattern sorts under simplification. One way to preserve the required sort annotations is to make <code>simplifyEvaluated</code> take an argument of type</p>
<div class="sourceCode" id="cb4"><pre class="sourceCode haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb4-1" title="1"><span class="dt">CofreeF</span> (<span class="dt">Or</span> level) (<span class="dt">Valid</span> level) (<span class="dt">OrOfExpandedPattern</span> level variable)</a></code></pre></div>
<p>instead of two <code>OrOfExpandedPattern</code> arguments. The type of <code>makeEvaluate</code> may be changed analogously. The <code>Valid</code> annotation will eventually cache information besides the pattern sort, which will make it even more useful to carry around.</p>
<p><strong>TODO</strong> (virgil): This should do all possible mergings, not just the first term with the second.</p>
<div class="sourceCode" id="cb5"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb5-1" title="1">simplifyEvaluated first second</a>
<a class="sourceLine" id="cb5-2" title="2"></a>
<a class="sourceLine" id="cb5-3" title="3">  <span class="fu">|</span> (head1 <span class="fu">:</span> tail1) <span class="ot">&lt;-</span> OrOfExpandedPattern.extractPatterns first</a>
<a class="sourceLine" id="cb5-4" title="4">  , (head2 <span class="fu">:</span> tail2) <span class="ot">&lt;-</span> OrOfExpandedPattern.extractPatterns second</a>
<a class="sourceLine" id="cb5-5" title="5">  , <span class="dt">Just</span> (result, proof) <span class="ot">&lt;-</span> simplifySinglePatterns head1 head2</a>
<a class="sourceLine" id="cb5-6" title="6">  <span class="fu">=</span> (OrOfExpandedPattern.make <span class="fu">$</span> result <span class="fu">:</span> (tail1 <span class="fu">++</span> tail2), proof)</a>
<a class="sourceLine" id="cb5-7" title="7"></a>
<a class="sourceLine" id="cb5-8" title="8">  <span class="fu">|</span> <span class="fu">otherwise</span> <span class="fu">=</span></a>
<a class="sourceLine" id="cb5-9" title="9">    ( OrOfExpandedPattern.merge first second</a>
<a class="sourceLine" id="cb5-10" title="10">    , <span class="dt">SimplificationProof</span></a>
<a class="sourceLine" id="cb5-11" title="11">    )</a>
<a class="sourceLine" id="cb5-12" title="12"></a>
<a class="sourceLine" id="cb5-13" title="13">  <span class="kw">where</span></a>
<a class="sourceLine" id="cb5-14" title="14">    simplifySinglePatterns first&#39; second&#39; <span class="fu">=</span></a>
<a class="sourceLine" id="cb5-15" title="15">        disjoinPredicates first&#39; second&#39; <span class="fu">&lt;|&gt;</span> topAnnihilates first&#39; second&#39;</a></code></pre></div>
<h2 id="disjoin-predicates">Disjoin predicates</h2>
<div class="sourceCode" id="cb6"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb6-1" title="1"><span class="co">{- | Merge two configurations by the disjunction of their predicates.</span></a>
<a class="sourceLine" id="cb6-2" title="2"></a>
<a class="sourceLine" id="cb6-3" title="3"><span class="co">This simplification case is only applied if the configurations have the same</span></a>
<a class="sourceLine" id="cb6-4" title="4"><span class="co">&#39;term&#39;.</span></a>
<a class="sourceLine" id="cb6-5" title="5"></a>
<a class="sourceLine" id="cb6-6" title="6"><span class="co"> -}</span></a>
<a class="sourceLine" id="cb6-7" title="7">disjoinPredicates</a>
<a class="sourceLine" id="cb6-8" title="8"><span class="ot">    ::</span>  ( <span class="dt">MetaOrObject</span> level</a>
<a class="sourceLine" id="cb6-9" title="9">        , <span class="dt">SortedVariable</span> variable</a>
<a class="sourceLine" id="cb6-10" title="10">        , <span class="dt">Ord</span> (variable level)</a>
<a class="sourceLine" id="cb6-11" title="11">        , <span class="dt">Show</span> (variable level)</a>
<a class="sourceLine" id="cb6-12" title="12">        , <span class="dt">Unparse</span> (variable level)</a>
<a class="sourceLine" id="cb6-13" title="13">        )</a>
<a class="sourceLine" id="cb6-14" title="14">    <span class="ot">=&gt;</span> <span class="dt">ExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb6-15" title="15">    <span class="co">-- ^ Configuration</span></a>
<a class="sourceLine" id="cb6-16" title="16">    <span class="ot">-&gt;</span> <span class="dt">ExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb6-17" title="17">    <span class="co">-- ^ Disjunction</span></a>
<a class="sourceLine" id="cb6-18" title="18">    <span class="ot">-&gt;</span> <span class="dt">Maybe</span> (<span class="dt">ExpandedPattern</span> level variable, <span class="dt">SimplificationProof</span> level)</a></code></pre></div>
<p>When two configurations have the same substitution, it may be possible to simplify the pair by disjunction of their predicates.</p>
<pre><code>(             t₁, p₁, s) ∨ (             t₂, p₂, s)
([t₂ ∨ ¬t₂] ∧ t₁, p₁, s) ∨ ([t₁ ∨ ¬t₁] ∧ t₂, p₂, s)

(t₁ ∧ t₂, p₁ ∨ p₂, s) ∨ (¬t₂ ∧ t₁, p₁, s) ∨ (¬t₁ ∧ t₂, p₂, s)</code></pre>
<p>It is useful to apply the above equality when</p>
<pre><code>¬t₂ ∧ t₁ = ¬t₁ ∧ t₂ = ⊥</code></pre>
<p>so that</p>
<pre><code>(t₁, p₁, s) ∨ (t₂, p₂, s) = (t₁ ∧ t₂, p₁ ∨ p₂, s)
  where
    ¬t₂ ∧ t₁ = ¬t₁ ∧ t₂ = ⊥.</code></pre>
<p>Checking the side condition may be expensive, so in practice we only apply this simplification when <code>t₁=t₂</code>.</p>
<p><strong>Note</strong>: It is not clear that we should <em>ever</em> apply this simplification. We attempt to refute the conditions on configurations using an external solver to reduce the configuration space for execution. The solver operates best when it has the most information, and the predicate <code>p₁ ∨ p₂</code> is strictly weaker than either <code>p₁</code> or <code>p₂</code>.</p>
<div class="sourceCode" id="cb10"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb10-1" title="1">disjoinPredicates</a>
<a class="sourceLine" id="cb10-2" title="2">    predicated1<span class="fu">@</span><span class="dt">Predicated</span></a>
<a class="sourceLine" id="cb10-3" title="3">        { term <span class="fu">=</span> term1</a>
<a class="sourceLine" id="cb10-4" title="4">        , predicate <span class="fu">=</span> predicate1</a>
<a class="sourceLine" id="cb10-5" title="5">        , substitution <span class="fu">=</span> substitution1</a>
<a class="sourceLine" id="cb10-6" title="6">        }</a>
<a class="sourceLine" id="cb10-7" title="7">    <span class="dt">Predicated</span></a>
<a class="sourceLine" id="cb10-8" title="8">        { term <span class="fu">=</span> term2</a>
<a class="sourceLine" id="cb10-9" title="9">        , predicate <span class="fu">=</span> predicate2</a>
<a class="sourceLine" id="cb10-10" title="10">        , substitution <span class="fu">=</span> substitution2</a>
<a class="sourceLine" id="cb10-11" title="11">        }</a>
<a class="sourceLine" id="cb10-12" title="12"></a>
<a class="sourceLine" id="cb10-13" title="13">  <span class="fu">|</span> term1         <span class="fu">==</span> term2</a>
<a class="sourceLine" id="cb10-14" title="14">  , substitution1 <span class="fu">==</span> substitution2</a>
<a class="sourceLine" id="cb10-15" title="15">  <span class="fu">=</span> <span class="dt">Just</span> (result, <span class="dt">SimplificationProof</span>)</a>
<a class="sourceLine" id="cb10-16" title="16"></a>
<a class="sourceLine" id="cb10-17" title="17">  <span class="fu">|</span> <span class="fu">otherwise</span> <span class="fu">=</span></a>
<a class="sourceLine" id="cb10-18" title="18">    <span class="dt">Nothing</span></a>
<a class="sourceLine" id="cb10-19" title="19"></a>
<a class="sourceLine" id="cb10-20" title="20">  <span class="kw">where</span></a>
<a class="sourceLine" id="cb10-21" title="21">    result <span class="fu">=</span> predicated1 { predicate <span class="fu">=</span> makeOrPredicate predicate1 predicate2 }</a></code></pre></div>
<p>## <code>\top</code> annihilates <code>\or</code></p>
<div class="sourceCode" id="cb11"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb11-1" title="1"><span class="co">{- | &#39;Top&#39; patterns are the annihilator of &#39;Or&#39;.</span></a>
<a class="sourceLine" id="cb11-2" title="2"><span class="co"> -}</span></a>
<a class="sourceLine" id="cb11-3" title="3">topAnnihilates</a>
<a class="sourceLine" id="cb11-4" title="4"><span class="ot">    ::</span>  ( <span class="dt">MetaOrObject</span> level</a>
<a class="sourceLine" id="cb11-5" title="5">        , <span class="dt">SortedVariable</span> variable</a>
<a class="sourceLine" id="cb11-6" title="6">        , <span class="dt">Ord</span> (variable level)</a>
<a class="sourceLine" id="cb11-7" title="7">        , <span class="dt">Show</span> (variable level)</a>
<a class="sourceLine" id="cb11-8" title="8">        , <span class="dt">Unparse</span> (variable level)</a>
<a class="sourceLine" id="cb11-9" title="9">        )</a>
<a class="sourceLine" id="cb11-10" title="10">    <span class="ot">=&gt;</span> <span class="dt">ExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb11-11" title="11">    <span class="co">-- ^ Configuration</span></a>
<a class="sourceLine" id="cb11-12" title="12">    <span class="ot">-&gt;</span> <span class="dt">ExpandedPattern</span> level variable</a>
<a class="sourceLine" id="cb11-13" title="13">    <span class="co">-- ^ Disjunction</span></a>
<a class="sourceLine" id="cb11-14" title="14">    <span class="ot">-&gt;</span> <span class="dt">Maybe</span> (<span class="dt">ExpandedPattern</span> level variable, <span class="dt">SimplificationProof</span> level)</a></code></pre></div>
<p><code>⊤</code> is the annihilator of <code>∨</code>; when two configurations have the same substitution, it may be possible to use this property to simplify the pair by annihilating the lesser term.</p>
<pre><code>(⊤,              p₁, s) ∨ (t₂,              p₂, s)
(⊤, [p₂ ∨ ¬p₂] ∧ p₁, s) ∨ (t₂, [p₁ ∨ ¬p₁] ∧ p₂, s)

(⊤, p₁ ∧ p₂, s) ∨ (⊤, p₁ ∧ ¬p₂, s) ∨ (t₂, ¬p₁ ∧ p₂, s)</code></pre>
<p>It is useful to apply the above equality when</p>
<pre><code>¬p₂ ∧ p₁ = ¬p₁ ∧ p₂ = ⊥</code></pre>
<p>so that</p>
<pre><code>(⊤, p₁, s) ∨ (t₂, p₂, s) = (⊤, p₁ ∧ p₂, s)
  where
    ¬p₂ ∧ p₁ = ¬p₁ ∧ p₂ = ⊥.</code></pre>
<p>Checking the side condition may be expensive, so in practice we only apply this simplification when <code>p₁ = p₂</code>.</p>
<div class="sourceCode" id="cb15"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb15-1" title="1">topAnnihilates</a>
<a class="sourceLine" id="cb15-2" title="2">    predicated1<span class="fu">@</span><span class="dt">Predicated</span></a>
<a class="sourceLine" id="cb15-3" title="3">        { term <span class="fu">=</span> term1</a>
<a class="sourceLine" id="cb15-4" title="4">        , predicate <span class="fu">=</span> predicate1</a>
<a class="sourceLine" id="cb15-5" title="5">        , substitution <span class="fu">=</span> substitution1</a>
<a class="sourceLine" id="cb15-6" title="6">        }</a>
<a class="sourceLine" id="cb15-7" title="7">    predicated2<span class="fu">@</span><span class="dt">Predicated</span></a>
<a class="sourceLine" id="cb15-8" title="8">        { term <span class="fu">=</span> term2</a>
<a class="sourceLine" id="cb15-9" title="9">        , predicate <span class="fu">=</span> predicate2</a>
<a class="sourceLine" id="cb15-10" title="10">        , substitution <span class="fu">=</span> substitution2</a>
<a class="sourceLine" id="cb15-11" title="11">        }</a>
<a class="sourceLine" id="cb15-12" title="12"></a>
<a class="sourceLine" id="cb15-13" title="13">  <span class="co">-- The &#39;term&#39;s are checked first because checking the equality of predicates</span></a>
<a class="sourceLine" id="cb15-14" title="14">  <span class="co">-- and substitutions could be expensive.</span></a>
<a class="sourceLine" id="cb15-15" title="15"></a>
<a class="sourceLine" id="cb15-16" title="16">  <span class="fu">|</span> _ <span class="fu">:&lt;</span> <span class="dt">TopPattern</span> _ <span class="ot">&lt;-</span> Recursive.project term1</a>
<a class="sourceLine" id="cb15-17" title="17">  , predicate1    <span class="fu">==</span> predicate2</a>
<a class="sourceLine" id="cb15-18" title="18">  , substitution1 <span class="fu">==</span> substitution2</a>
<a class="sourceLine" id="cb15-19" title="19">  <span class="fu">=</span> <span class="dt">Just</span> (predicated1, <span class="dt">SimplificationProof</span>)</a>
<a class="sourceLine" id="cb15-20" title="20"></a>
<a class="sourceLine" id="cb15-21" title="21">  <span class="fu">|</span> _ <span class="fu">:&lt;</span> <span class="dt">TopPattern</span> _ <span class="ot">&lt;-</span> Recursive.project term2</a>
<a class="sourceLine" id="cb15-22" title="22">  , predicate1    <span class="fu">==</span> predicate2</a>
<a class="sourceLine" id="cb15-23" title="23">  , substitution1 <span class="fu">==</span> substitution2</a>
<a class="sourceLine" id="cb15-24" title="24">  <span class="fu">=</span> <span class="dt">Just</span> (predicated2, <span class="dt">SimplificationProof</span>)</a>
<a class="sourceLine" id="cb15-25" title="25"></a>
<a class="sourceLine" id="cb15-26" title="26">  <span class="fu">|</span> <span class="fu">otherwise</span> <span class="fu">=</span></a>
<a class="sourceLine" id="cb15-27" title="27">    <span class="dt">Nothing</span></a></code></pre></div>
</body>
</html>