/usr/share/doc/libaac-tactics-ocaml-dev/html/api/Coq.Rewrite.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 158 159 160 161 162 163 164 165 166 167 168 | <!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="Coq.Equivalence.html">
<link rel="Up" href="Coq.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="Datatypes" rel="Section" href="#2_Datatypes">
<link title="Rewriting with bindings" rel="Section" href="#2_Rewritingwithbindings">
<title>Coq.Rewrite</title>
</head>
<body>
<div class="navbar"><a class="pre" href="Coq.Equivalence.html" title="Coq.Equivalence">Previous</a>
<a class="up" href="Coq.html" title="Coq">Up</a>
</div>
<h1>Module <a href="type_Coq.Rewrite.html">Coq.Rewrite</a></h1>
<pre><span class="keyword">module</span> Rewrite: <code class="code">sig</code> <a href="Coq.Rewrite.html">..</a> <code class="code">end</code></pre><hr width="100%">
<br>
The rewriting tactics used in aac_rewrite, build as handlers of the usual <code class="code">setoid_rewrite</code><br>
<br>
The rewriting tactics used in aac_rewrite, build as handlers of the usual <code class="code">setoid_rewrite</code><br>
<br>
<h2 id="2_Datatypes">Datatypes</h2><br>
<pre><code><span id="TYPEhypinfo"><span class="keyword">type</span> <code class="type"></code>hypinfo</span> = {</code></pre><table class="typetable">
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.hyp">hyp</span> : <code class="type">Term.constr</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
the actual constr corresponding to the hypothese<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.hyptype">hyptype</span> : <code class="type">Term.constr</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
the type of the hypothesis<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.context">context</span> : <code class="type">Context.Rel.t</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
the quantifications of the hypothese<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.body">body</span> : <code class="type">Term.constr</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
the body of the hypothese<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.rel">rel</span> : <code class="type"><a href="Coq.Relation.html#TYPEt">Coq.Relation.t</a></code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
the relation<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.left">left</span> : <code class="type">Term.constr</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
left hand side<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.right">right</span> : <code class="type">Term.constr</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
right hand side<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr>
<tr>
<td align="left" valign="top" >
<code> </code></td>
<td align="left" valign="top" >
<code><span id="TYPEELThypinfo.l2r">l2r</span> : <code class="type">bool</code>;</code></td>
<td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><div class="info ">
rewriting from left to right<br>
</div>
</td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td>
</tr></table>
}
<div class="info ">
We keep some informations about the hypothesis, with an (informal)
invariant:<ul>
<li><code class="code">typeof hyp = typ</code></li>
<li><code class="code">typ = forall context, body</code></li>
<li><code class="code">body = rel left right</code></li>
</ul>
<br>
</div>
<pre><span id="VALget_hypinfo"><span class="keyword">val</span> get_hypinfo</span> : <code class="type">Term.constr -><br> l2r:bool -><br> ?check_type:(Term.types -> bool) -><br> (<a href="Coq.Rewrite.html#TYPEhypinfo">hypinfo</a> -> Proof_type.tactic) -> Proof_type.tactic</code></pre><div class="info ">
<code class="code">get_hypinfo H l2r ?check_type k</code> analyse the hypothesis H, and
build the related hypinfo, in CPS style. Moreover, an optionnal
function can be provided to check the type of every free
variable of the body of the hypothesis.<br>
</div>
<br>
<h2 id="2_Rewritingwithbindings">Rewriting with bindings</h2>
<p>
The problem : Given a term to rewrite of type <code class="code">H :forall xn ... x1,
t</code>, we have to instanciate the subset of <code class="code">xi</code> of type
<code class="code">carrier</code>. <code class="code">subst : (int * constr)</code> is the mapping the De Bruijn
indices in <code class="code">t</code> to the <code class="code">constrs</code>. We need to handle the rest of the
indexes. Two ways :
<p>
<ul>
<li>either using fresh evars and rewriting <code class="code">H tn ?1 tn-2 ?2 </code></li>
<li>either building a term like <code class="code">fun 1 2 => H tn 1 tn-2 2</code></li>
</ul>
Both these terms have the same type.<br>
<pre><span id="VALbuild"><span class="keyword">val</span> build</span> : <code class="type"><a href="Coq.Rewrite.html#TYPEhypinfo">hypinfo</a> -><br> (int * Term.constr) list -><br> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic</code></pre><div class="info ">
build the constr to rewrite, in CPS style, with lambda abstractions<br>
</div>
<pre><span id="VALbuild_with_evar"><span class="keyword">val</span> build_with_evar</span> : <code class="type"><a href="Coq.Rewrite.html#TYPEhypinfo">hypinfo</a> -><br> (int * Term.constr) list -><br> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic</code></pre><div class="info ">
build the constr to rewrite, in CPS style, with evars<br>
</div>
<pre><span id="VALrewrite"><span class="keyword">val</span> rewrite</span> : <code class="type">?abort:bool -><br> <a href="Coq.Rewrite.html#TYPEhypinfo">hypinfo</a> -><br> (int * Term.constr) list -><br> (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic</code></pre><div class="info ">
<code class="code">rewrite ?abort hypinfo subst</code> builds the rewriting tactic
associated with the given <code class="code">subst</code> and <code class="code">hypinfo</code>, and feeds it to
the given continuation. If <code class="code">abort</code> is set to <code class="code">true</code>, we build
<code class="code">tclIDTAC</code> instead.<br>
</div>
</body></html>
|