blob: b78049c2cd9ab595047eb5949bc21a924920f6b1 (
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
|
<?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>Statemonad.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> compcert <span class="kn">Require</span> Errors.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> vericert <span class="kn">Require Import</span> Monad.</span></span><span class="coq-wsp">
</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> 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">State</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">Parameter</span> <span class="nv">st</span> : <span class="kt">Type</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">Parameter</span> <span class="nv">st_prop</span> : st -> st -> <span class="kt">Prop</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">Axiom</span> <span class="nv">st_refl</span> : <span class="kr">forall</span> <span class="nv">s</span>, st_prop s s.</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">Axiom</span> <span class="nv">st_trans</span> : <span class="kr">forall</span> <span class="nv">s1</span> <span class="nv">s2</span> <span class="nv">s3</span>, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">End</span> <span class="nf">State</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">Statemonad</span>(S : State) <: Monad.</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">Inductive</span> <span class="nf">res</span> (<span class="nv">A</span>: <span class="kt">Type</span>) (<span class="nv">s</span>: S.st): <span class="kt">Type</span> :=
| Error : Errors.errmsg -> res A s
| OK : A -> <span class="kr">forall</span> (<span class="nv">s'</span> : S.st), S.st_prop s s' -> res A s.</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">Arguments</span> OK [A s].</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> Error [A s].</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">Definition</span> <span class="nf">mon</span> (<span class="nv">A</span>: <span class="kt">Type</span>) : <span class="kt">Type</span> := <span class="kr">forall</span> (<span class="nv">s</span>: S.st), res A s.</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">Definition</span> <span class="nf">ret</span> {<span class="nv">A</span>: <span class="kt">Type</span>} (<span class="nv">x</span>: A) : mon A :=
<span class="kr">fun</span> (<span class="nv">s</span> : S.st) => OK x s (S.st_refl s).</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">Definition</span> <span class="nf">bind</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 -> mon B) : mon B :=
<span class="kr">fun</span> (<span class="nv">s</span> : S.st) =>
<span class="kr">match</span> f s <span class="kr">with</span>
| Error msg => Error msg
| OK a s' i =>
<span class="kr">match</span> g a s' <span class="kr">with</span>
| Error msg => Error msg
| OK b s'' i' => OK b s'' (S.st_trans s s' s'' i i')
<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-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">bind2</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 -> B -> mon C) : mon C :=
bind f (<span class="kr">fun</span> <span class="nv">xy</span> => g (fst xy) (snd xy)).</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">Definition</span> <span class="nf">handle_error</span> {<span class="nv">A</span>: <span class="kt">Type</span>} (<span class="nv">f</span> <span class="nv">g</span>: mon A) : mon A :=
<span class="kr">fun</span> (<span class="nv">s</span> : S.st) =>
<span class="kr">match</span> f s <span class="kr">with</span>
| OK a s' i => OK a s' i
| Error _ => g s
<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">Definition</span> <span class="nf">error</span> {<span class="nv">A</span>: <span class="kt">Type</span>} (<span class="nv">err</span>: Errors.errmsg) : mon A := <span class="kr">fun</span> (<span class="nv">s</span>: S.st) => Error err.</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">Definition</span> <span class="nf">get</span> : mon S.st := <span class="kr">fun</span> <span class="nv">s</span> => OK s s (S.st_refl s).</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">Definition</span> <span class="nf">set</span> (<span class="nv">s</span>: S.st) (<span class="nv">i</span>: <span class="kr">forall</span> <span class="nv">s'</span>, S.st_prop s' s) : mon unit :=
<span class="kr">fun</span> <span class="nv">s'</span> => OK tt s (i s').</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">Definition</span> <span class="nf">run_mon</span> {<span class="nv">A</span>: <span class="kt">Type</span>} (<span class="nv">s</span>: S.st) (<span class="nv">m</span>: mon A): Errors.res A :=
<span class="kr">match</span> m s <span class="kr">with</span>
| OK a s' i => Errors.OK a
| Error err => Errors.Error err
<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">Statemonad</span>.</span></span></span></pre>
</div>
</div></body>
</html>
|
