/usr/share/doc/libaac-tactics-ocaml-dev/html/api/Matcher.html is in libaac-tactics-ocaml-dev 8.6.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link rel="previous" href="Helper.html">
<link rel="next" href="Print.html">
<link rel="Up" href="index.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Index of module types" rel=Appendix href="index_module_types.html">
<link title="Aac_rewrite" rel="Chapter" href="Aac_rewrite.html">
<link title="Coq" rel="Chapter" href="Coq.html">
<link title="Helper" rel="Chapter" href="Helper.html">
<link title="Matcher" rel="Chapter" href="Matcher.html">
<link title="Print" rel="Chapter" href="Print.html">
<link title="Search_monad" rel="Chapter" href="Search_monad.html">
<link title="Theory" rel="Chapter" href="Theory.html"><link title="Utility functions" rel="Section" href="#2_Utilityfunctions">
<link title="Main functions exported by this module" rel="Section" href="#2_Mainfunctionsexportedbythismodule">
<title>Matcher</title>
</head>
<body>
<div class="navbar"><a class="pre" href="Helper.html" title="Helper">Previous</a>
<a class="up" href="index.html" title="Index">Up</a>
<a class="post" href="Print.html" title="Print">Next</a>
</div>
<h1>Module <a href="type_Matcher.html">Matcher</a></h1>
<pre><span class="keyword">module</span> Matcher: <code class="code">sig</code> <a href="Matcher.html">..</a> <code class="code">end</code></pre><div class="info module top">
Standalone module containing the algorithm for matching modulo
associativity and associativity and commutativity
(AAC). Additionnaly, some A or AC operators can have units (U).
<p>
This module could be reused outside of the Coq plugin.
<p>
Matching a pattern <code class="code">p</code> against a term <code class="code">t</code> modulo AACU boils down
to finding a substitution <code class="code">env</code> such that the pattern <code class="code">p</code>
instantiated with <code class="code">env</code> is equal to <code class="code">t</code> modulo AACU.
<p>
We proceed by structural decomposition of the pattern, trying all
possible non-deterministic splittings of the subject, when needed. The
function <a href="Matcher.html#VALmatcher"><code class="code">Matcher.matcher</code></a> is limited to top-level matching, that is, the
subject must make a perfect match against the pattern (<code class="code">x+x</code> does
not match <code class="code">a+a+b</code> ).
<p>
We use a search monad <a href="Search_monad.html"><code class="code">Search_monad</code></a> to perform non-deterministic
choices in an almost transparent way.
<p>
We also provide a function <a href="Matcher.html#VALsubterm"><code class="code">Matcher.subterm</code></a> for finding a match that is
a subterm of the subject modulo AACU. In particular, this function
gives a solution to the aforementioned case (<code class="code">x+x</code> against
<code class="code">a+b+a</code>).
<p>
On a slightly more involved level :<ul>
<li>it must be noted that we allow several AC/A operators to share
the same units, but that a given AC/A operator can have at most
one unit.</li>
</ul>
<ul>
<li>if the pattern does not contain "hard" symbols (like constants,
function symbols, AC or A symbols without units), there can be
infinitely many subterms such that the pattern matches: it is
possible to build "subterms" modulo AAC and U that make the size
of the term increase (by making neutral elements appear in a
layered fashion). Hence, in this case, a warning is issued, and
some solutions are omitted.</li>
</ul>
<br>
</div>
<hr width="100%">
<br>
<h2 id="2_Utilityfunctions">Utility functions</h2><br>
<pre><span id="TYPEsymbol"><span class="keyword">type</span> <code class="type"></code>symbol</span> = <code class="type">int</code> </pre>
<pre><span id="TYPEvar"><span class="keyword">type</span> <code class="type"></code>var</span> = <code class="type">int</code> </pre>
<br>
Relationship between units and operators. This is a sparse
representation of a matrix of couples <code class="code">(op,unit)</code> where <code class="code">op</code> is
the index of the operation, and <code class="code">unit</code> the index of the relevant
unit. We make the assumption that any operation has 0 or 1 unit,
and that operations can share a unit).<br>
<pre><span id="TYPEunits"><span class="keyword">type</span> <code class="type"></code>units</span> = <code class="type">(<a href="Matcher.html#TYPEsymbol">symbol</a> * <a href="Matcher.html#TYPEsymbol">symbol</a>) list</code> </pre>
<pre><code><span id="TYPEext_units"><span class="keyword">type</span> <code class="type"></code>ext_units</span> = {</code></pre><table class="typetable">
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELText_units.unit_for">unit_for</span> : <code class="type"><a href="Matcher.html#TYPEunits">units</a></code>;</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELText_units.is_ac">is_ac</span> : <code class="type">(<a href="Matcher.html#TYPEsymbol">symbol</a> * bool) list</code>;</code></td>
</tr></table>
}
<pre><span id="TYPEmset"><span class="keyword">type</span> <code class="type">'a</code> mset</span> = <code class="type">('a * int) list</code> </pre>
<div class="info ">
The arguments of sums (or AC operators) are represented using finite multisets.
(Typically, <code class="code">a+b+a</code> corresponds to <code class="code">2.a+b</code>, i.e. <code class="code">Sum[a,2;b,1]</code>)<br>
</div>
<pre><span id="VALlinear"><span class="keyword">val</span> linear</span> : <code class="type">'a <a href="Matcher.html#TYPEmset">mset</a> -> 'a list</code></pre><div class="info ">
<code class="code">linear</code> expands a multiset into a simple list<br>
</div>
<pre><span class="keyword">module</span> <a href="Matcher.Terms.html">Terms</a>: <code class="code">sig</code> <a href="Matcher.Terms.html">..</a> <code class="code">end</code></pre><div class="info">
Representations of expressions
</div>
<pre><span class="keyword">module</span> <a href="Matcher.Subst.html">Subst</a>: <code class="code">sig</code> <a href="Matcher.Subst.html">..</a> <code class="code">end</code></pre><div class="info">
Substitutions (or environments)
</div>
<br>
<h2 id="2_Mainfunctionsexportedbythismodule">Main functions exported by this module</h2><br>
<pre><span id="VALmatcher"><span class="keyword">val</span> matcher</span> : <code class="type">?strict:bool -><br> <a href="Matcher.html#TYPEext_units">ext_units</a> -><br> <a href="Matcher.Terms.html#TYPEt">Terms.t</a> -> <a href="Matcher.Terms.html#TYPEt">Terms.t</a> -> <a href="Matcher.Subst.html#TYPEt">Subst.t</a> <a href="Search_monad.html#TYPEm">Search_monad.m</a></code></pre><div class="info ">
<code class="code">matcher p t</code> computes the set of solutions to the given top-level
matching problem (<code class="code">p</code> is the pattern, <code class="code">t</code> is the term). If the
<code class="code">strict</code> flag is set, solutions where units are used to
instantiate some variables are excluded, unless this unit appears
directly under a function symbol (e.g., f(x) still matches f(1),
while x+x+y does not match a+b+c, since this would require to
assign 1 to x).<br>
</div>
<pre><span id="VALsubterm"><span class="keyword">val</span> subterm</span> : <code class="type">?strict:bool -><br> <a href="Matcher.html#TYPEext_units">ext_units</a> -><br> <a href="Matcher.Terms.html#TYPEt">Terms.t</a> -><br> <a href="Matcher.Terms.html#TYPEt">Terms.t</a> -><br> (int * <a href="Matcher.Terms.html#TYPEt">Terms.t</a> * <a href="Matcher.Subst.html#TYPEt">Subst.t</a> <a href="Search_monad.html#TYPEm">Search_monad.m</a>) <a href="Search_monad.html#TYPEm">Search_monad.m</a></code></pre><div class="info ">
<code class="code">subterm p t</code> computes a set of solutions to the given
subterm-matching problem.
<p>
Return a collection of possible solutions (each with the
associated depth, the context, and the solutions of the matching
problem). The context is actually a <a href="Matcher.Terms.html#TYPEt"><code class="code">Matcher.Terms.t</code></a> where the variables
are yet to be instantiated by one of the associated substitutions<br>
</div>
</body></html>
|