Created
February 5, 2019 16:05
-
-
Save ttuegel/c6fa7fd2bfbba6229d11c41324e717bc to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % Or Simplification | |
| == Header | |
| \begin{code} | |
| {-| | |
| Module : Kore.Step.Simplification.Or | |
| Description : Tools for Or pattern simplification. | |
| Copyright : (c) Runtime Verification, 2018 | |
| License : NCSA | |
| Maintainer : [email protected] | |
| 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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!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 : [email protected]</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">{-|'simplify' simplifies an 'Or' pattern with 'OrOfExpandedPattern'</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">=></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">-></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 'Or' given its two 'OrOfExpandedPattern' children.</span></a> | |
| <a class="sourceLine" id="cb3-10" title="10"></a> | |
| <a class="sourceLine" id="cb3-11" title="11"><span class="co">See 'simplify' 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">=></span> <span class="dt">OrOfExpandedPattern</span> level variable</a> | |
| <a class="sourceLine" id="cb3-21" title="21"> <span class="ot">-></span> <span class="dt">OrOfExpandedPattern</span> level variable</a> | |
| <a class="sourceLine" id="cb3-22" title="22"> <span class="ot">-></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"><-</span> OrOfExpandedPattern.extractPatterns first</a> | |
| <a class="sourceLine" id="cb5-4" title="4"> , (head2 <span class="fu">:</span> tail2) <span class="ot"><-</span> OrOfExpandedPattern.extractPatterns second</a> | |
| <a class="sourceLine" id="cb5-5" title="5"> , <span class="dt">Just</span> (result, proof) <span class="ot"><-</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' second' <span class="fu">=</span></a> | |
| <a class="sourceLine" id="cb5-15" title="15"> disjoinPredicates first' second' <span class="fu"><|></span> topAnnihilates first' second'</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">'term'.</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">=></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">-></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">-></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">{- | 'Top' patterns are the annihilator of 'Or'.</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">=></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">-></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">-></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 'term'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">:<</span> <span class="dt">TopPattern</span> _ <span class="ot"><-</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">:<</span> <span class="dt">TopPattern</span> _ <span class="ot"><-</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> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment