docs/proof/Monad.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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

<?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>Monad.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" />
<link rel="stylesheet" href="../docs/css/org.css" type="text/css" />
</head>
<body>
<div id="left-bar">
<header id="ymhg-header">
<div class="logo"><a href="/vericert">Vericert</a></div>
<nav id="navbar">
<span><a href="/vericert/documentation.html">Documentation</a></span>
<span><a href="/vericert/proof/toc.html">Proof</a></span>
</nav>
<p>Vericert is the first formally verified high-level synthesis tool.</p>
</header>
<div id="toc"></div>
</div>
<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> Coq <span class="kn">Require Import</span> Lists.List.</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">Module Type</span> <span class="nf">Monad</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Parameter</span> <span class="nv">mon</span> : <span class="kt">Type</span> -&gt; <span class="kt">Type</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Parameter</span> <span class="nv">ret</span> : <span class="kr">forall</span> (<span class="nv">A</span> : <span class="kt">Type</span>) (<span class="nv">x</span> : A), mon A.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Arguments</span> ret [A].</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Parameter</span> <span class="nv">bind</span> : <span class="kr">forall</span> (<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>) (<span class="nv">f</span> : mon A) (<span class="nv">g</span> : A -&gt; mon B), mon B.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Arguments</span> bind [A B].</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Parameter</span> <span class="nv">bind2</span> : <span class="kr">forall</span> (<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span>: <span class="kt">Type</span>) (<span class="nv">f</span>: mon (A * B)) (<span class="nv">g</span>: A -&gt; B -&gt; mon C), mon C.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Arguments</span> bind2 [A B C].</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">Monad</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">Module</span> <span class="nf">MonadExtra</span>(M : Monad).</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Import</span> M.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Module</span> <span class="nf">MonadNotation</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">    </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Notation</span> <span class="s2">&quot;&#39;do&#39; X &lt;- A ; B&quot;</span> :=
      (bind A (<span class="kr">fun</span> <span class="nv">X</span> =&gt; B))
        (<span class="kn">at level</span> <span class="mi">200</span>, X <span class="kn">ident</span>, A <span class="kn">at level</span> <span class="mi">100</span>, B <span class="kn">at level</span> <span class="mi">200</span>).</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">    </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Notation</span> <span class="s2">&quot;&#39;do&#39; ( X , Y ) &lt;- A ; B&quot;</span> :=
      (bind2 A (<span class="kr">fun</span> <span class="nv">X</span> <span class="nv">Y</span> =&gt; B))
        (<span class="kn">at level</span> <span class="mi">200</span>, X <span class="kn">ident</span>, Y <span class="kn">ident</span>, A <span class="kn">at level</span> <span class="mi">100</span>, B <span class="kn">at level</span> <span class="mi">200</span>).</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">MonadNotation</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Import</span> MonadNotation.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">traverselist</span> {<span class="nv">A</span> <span class="nv">B</span>: <span class="kt">Type</span>} (<span class="nv">f</span>: A -&gt; mon B) (<span class="nv">l</span>: list A) {<span class="nv">struct</span> <span class="nv">l</span>}: mon (list B) :=
    <span class="kr">match</span> l <span class="kr">with</span>
    | nil =&gt; ret nil
    | x::xs =&gt;
      <span class="kp">do</span> r &lt;- f x;
      <span class="kp">do</span> rs &lt;- traverselist f xs;
      ret (r::rs)
    <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-wsp">  </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">collectlist</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : A -&gt; mon unit) (<span class="nv">l</span> : list A) {<span class="nv">struct</span> <span class="nv">l</span>} : mon unit :=
    <span class="kr">match</span> l <span class="kr">with</span>
    | nil =&gt; ret tt
    | x::xs =&gt; <span class="kp">do</span> _ &lt;- f x; collectlist f xs
    <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">End</span> <span class="nf">MonadExtra</span>.</span></span></span></pre>
</div>
</div></body>
</html>