blob: 926ab3ca597926fe6919cc9b82553393b0edf6df (
plain)
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
|
<?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>Show.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-wsp"><span class="highlight"><span class="c">(* </span>
<span class="c"> * Vericert: Verified high-level synthesis.</span>
<span class="c"> * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com></span>
<span class="c"> *</span>
<span class="c"> * This program is free software: you can redistribute it and/or modify</span>
<span class="c"> * it under the terms of the GNU General Public License as published by</span>
<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span>
<span class="c"> * (at your option) any later version.</span>
<span class="c"> *</span>
<span class="c"> * This program is distributed in the hope that it will be useful,</span>
<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span>
<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span>
<span class="c"> * GNU General Public License for more details.</span>
<span class="c"> *</span>
<span class="c"> * You should have received a copy of the GNU General Public License</span>
<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span>
<span class="c"> *)</span>
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> Coq <span class="kn">Require Import</span>
Strings.String
Bool.Bool
Arith.Arith
ZArith.ZArith.</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> string.</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">Class</span> <span class="nf">Show</span> <span class="nv">A</span> : <span class="kt">Type</span> :=
{
show : A -> string
}.</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">Instance</span> <span class="nf">showBool</span> : <span class="kn">Show</span> bool :=
{
show := <span class="kr">fun</span> <span class="nv">b</span>:bool => <span class="kr">if</span> b <span class="kr">then</span> <span class="s2">"true"</span> <span class="kr">else</span> <span class="s2">"false"</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">string_of_nat_aux</span> (<span class="nv">time</span> <span class="nv">n</span> : nat) (<span class="nv">acc</span> : string) : string :=
<span class="kr">let</span> <span class="nv">d</span> := <span class="kr">match</span> n mod <span class="mi">10</span> <span class="kr">with</span>
| <span class="mi">0</span> => <span class="s2">"0"</span> | <span class="mi">1</span> => <span class="s2">"1"</span> | <span class="mi">2</span> => <span class="s2">"2"</span> | <span class="mi">3</span> => <span class="s2">"3"</span> | <span class="mi">4</span> => <span class="s2">"4"</span> | <span class="mi">5</span> => <span class="s2">"5"</span>
| <span class="mi">6</span> => <span class="s2">"6"</span> | <span class="mi">7</span> => <span class="s2">"7"</span> | <span class="mi">8</span> => <span class="s2">"8"</span> | _ => <span class="s2">"9"</span>
<span class="kr">end</span> <span class="kr">in</span>
<span class="kr">let</span> <span class="nv">acc'</span> := d ++ acc <span class="kr">in</span>
<span class="kr">match</span> <span class="kp">time</span> <span class="kr">with</span>
| <span class="mi">0</span> => acc'
| S time' =>
<span class="kr">match</span> n / <span class="mi">10</span> <span class="kr">with</span>
| <span class="mi">0</span> => acc'
| n' => string_of_nat_aux time' n' acc'
<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">string_of_nat</span> (<span class="nv">n</span> : nat) : string :=
string_of_nat_aux n n <span class="s2">""</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">Instance</span> <span class="nf">showNat</span> : <span class="kn">Show</span> nat :=
{
show := string_of_nat
}.</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">Instance</span> <span class="nf">showZ</span> : <span class="kn">Show</span> Z :=
{
show a := show (Z.to_nat a)
}.</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">Instance</span> <span class="nf">showPositive</span> : <span class="kn">Show</span> positive :=
{
show a := show (Zpos a)
}.</span></span></span></pre>
</div>
</div></body>
</html>
|
