docs/proof/Maps.html


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

<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<title>Maps.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" />
<script type="text/javascript" src="alectryon.js"></script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
</head>
<body>
<div class="alectryon-root alectryon-floating"><div class="document">


<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require Import</span> Vericertlib.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Export</span> Maps.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Errors.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Import</span> PTree.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Set Implicit Arguments</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Local Open Scope</span> error_monad_scope.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
<span class="sd">(** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised</span>
<span class="sd">    in the future. *)</span>

</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">PTree</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">xtraverse</span> (<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>) (<span class="nv">f</span> : positive -&gt; A -&gt; res B) (<span class="nv">m</span> : PTree.t A) (<span class="nv">i</span> : positive)
         {<span class="nv">struct</span> <span class="nv">m</span>} : res (PTree.t B) :=
  <span class="kr">match</span> m <span class="kr">with</span>
  | Leaf =&gt; OK Leaf
  | Node l o r =&gt;
    <span class="kr">let</span> <span class="nv">newo</span> :=
        <span class="kr">match</span> o <span class="kr">with</span>
        | None =&gt; OK None
        | Some x =&gt;
          <span class="kr">match</span> f (prev i) x <span class="kr">with</span>
          | Error err =&gt; Error err
          | OK val =&gt; OK (Some val)
          <span class="kr">end</span>
        <span class="kr">end</span> <span class="kr">in</span>
    <span class="kr">match</span> newo <span class="kr">with</span>
    | OK no =&gt;
      <span class="kp">do</span> nl &lt;- xtraverse f l (xO i);
      <span class="kp">do</span> nr &lt;- xtraverse f r (xI i);
      OK (Node nl no nr)
    | Error msg =&gt; Error msg
    <span class="kr">end</span>
  <span class="kr">end</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">traverse</span> (<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>) (<span class="nv">f</span> : positive -&gt; A -&gt; res B) <span class="nv">m</span> := xtraverse f m xH.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">traverse1</span> (<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>) (<span class="nv">f</span> : A -&gt; res B) := traverse (<span class="kr">fun</span> <span class="nv">_</span> =&gt; f).</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">PTree</span>.</span></span></span></pre>
</div>
</div></body>
</html>