https://github.com/AU-COBRA/ConCert
Tip revision: 932cb97084707cbac70c60db5d249bee24626750 authored by github-actions[bot] on 22 August 2022, 09:00:22 UTC
Deploy to GitHub pages
Deploy to GitHub pages
Tip revision: 932cb97
ConCert.Examples.Counter.embedding.CounterEmbed.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<link href="toc.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
<span id="toggle-toc">Contents</span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="https://github.com/AU-COBRA/ConCert" target="_balnk">Project Page</a>
<a href="index.html">Index</a>
<a href="toc.html">Table of contents</a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="js-toc" class="toc" data-toc="h1,h2,h3,h4" data-toc-container="doc" data-toc-offset="-40">
<div id="js-toc-header" class="toc-header">Contents:</div>
</div>
<div id="main">
<h1 class="libtitle">Library ConCert.Examples.Counter.embedding.CounterEmbed</h1>
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.ZArith.ZArith.html#"><span class="id" title="library">ZArith</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Utils.html#"><span class="id" title="library">Utils</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Notations.html#"><span class="id" title="library">Notations</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Ast.html#"><span class="id" title="library">Ast</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#"><span class="id" title="library">PCUICTranslate</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.TranslationUtils.html#"><span class="id" title="library">TranslationUtils</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#"><span class="id" title="library">SimpleBlockchain</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Prelude.html#"><span class="id" title="library">Prelude</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding.Extraction</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#"><span class="id" title="library">Liquidity</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Embedding.Extraction</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#"><span class="id" title="library">PreludeExt</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Utils</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Utils.Env.html#"><span class="id" title="library">Env</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">MetaCoq.Template</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.All.html#"><span class="id" title="library">All</span></a>.<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ListNotations"><span class="id" title="module">ListNotations</span></a>.<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#MCMonadNotation"><span class="id" title="module">MCMonadNotation</span></a>.<br/>
<br/>
<span class="id" title="keyword">Module</span> <a id="Counter" class="idref" href="#Counter"><span class="id" title="module">Counter</span></a>.<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain"><span class="id" title="module">AcornBlockchain</span></a>.<br/>
<br/>
<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">list</span>.<br/>
<br/>
</div>
<div class="doc">
Generating names for the data structures
</div>
<div class="code">
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span><br/>
(<a id="mp_:1" class="idref" href="#mp_:1"><span class="id" title="binder">mp_</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#6bec7af38cdf877f357faf8f1699c8f9"><span class="id" title="notation"><-</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmCurrentModPath"><span class="id" title="constructor">tmCurrentModPath</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#6bec7af38cdf877f357faf8f1699c8f9"><span class="id" title="notation">;;</span></a><br/>
<span class="id" title="keyword">let</span> <a id="mp:2" class="idref" href="#mp:2"><span class="id" title="binder">mp</span></a> := (<a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#string_of_modpath"><span class="id" title="definition">PCUICTranslate.string_of_modpath</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#mp_:1"><span class="id" title="variable">mp_</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "@")%<span class="id" title="var">string</span> <span class="id" title="tactic">in</span><br/>
<a class="idref" href="ConCert.Embedding.Utils.html#mkNames"><span class="id" title="definition">mkNames</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#mp:2"><span class="id" title="variable">mp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>"state" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "MkState" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "owner" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "msg" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a> "_coq").<br/>
<br/>
</div>
<div class="doc">
Variable names and constructor names
</div>
<div class="code">
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Embedding.Utils.html#mkNames"><span class="id" title="definition">mkNames</span></a> "" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>"m" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>"n"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "own"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "st" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "new_st" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "addr" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "new_balance"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "Inc" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "Dec"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a> "_coq").<br/>
<br/>
</div>
<div class="doc">
<a id="lab244"></a><h2 class="section">Definitions of data structures for the contract</h2>
<div class="paragraph"> </div>
The contract's state. We use the product type directly, because records are not yet supported by extraction
</div>
<div class="code">
<span class="comment">(* TODO: make address a separate data type (say, a wrapper around nat) to be able to recognise it in the extraction *)</span><br/>
<span class="id" title="keyword">Notation</span> <a id="Counter.:type::'CounterState'" class="idref" href="#Counter.:type::'CounterState'"><span class="id" title="notation">"</span></a>'CounterState'" := <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">[!</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">!]</span></a> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="keyword">type</span>).<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="Counter.:expr::'balance'_x" class="idref" href="#Counter.:expr::'balance'_x"><span class="id" title="notation">"</span></a>'balance' a" :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'first'_x_x_x"><span class="id" title="notation">first</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">{</span></a><span class="id" title="var">a</span><a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">}</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a><br/>
(<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">expr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="Counter.:expr::'owner'_x" class="idref" href="#Counter.:expr::'owner'_x"><span class="id" title="notation">"</span></a>'owner' a" :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'second'_x_x_x"><span class="id" title="notation">second</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">{</span></a><span class="id" title="var">a</span><a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">}</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a><br/>
(<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">expr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<br/>
</div>
<div class="doc">
Messages
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Counter.msg_syn" class="idref" href="#Counter.msg_syn"><span class="id" title="definition">msg_syn</span></a> :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#fe8473dd9402cdf9a6648d9eb80cf296"><span class="id" title="notation">[\</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#18c7f55b52af015fa0e74bfb243086c1"><span class="id" title="notation">data</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg"><span class="id" title="definition">msg</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#18c7f55b52af015fa0e74bfb243086c1"><span class="id" title="notation">=</span></a><br/>
<a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.Inc"><span class="id" title="definition">Inc</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#ebb8c269f26fdf46621f04e85ed4d72b"><span class="id" title="notation">[</span></a><a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a><a class="idref" href="ConCert.Embedding.Notations.html#8a1a1396a6fb40da8f616b6c388ba74a"><span class="id" title="notation">,</span></a><a class="idref" href="ConCert.Embedding.Notations.html#:ctor_args::'''_'''"><span class="id" title="notation">_</span></a><a class="idref" href="ConCert.Embedding.Notations.html#ebb8c269f26fdf46621f04e85ed4d72b"><span class="id" title="notation">]</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#18c7f55b52af015fa0e74bfb243086c1"><span class="id" title="notation">|</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.Dec"><span class="id" title="definition">Dec</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#ebb8c269f26fdf46621f04e85ed4d72b"><span class="id" title="notation">[</span></a><a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a><a class="idref" href="ConCert.Embedding.Notations.html#8a1a1396a6fb40da8f616b6c388ba74a"><span class="id" title="notation">,</span></a><a class="idref" href="ConCert.Embedding.Notations.html#:ctor_args::'''_'''"><span class="id" title="notation">_</span></a><a class="idref" href="ConCert.Embedding.Notations.html#ebb8c269f26fdf46621f04e85ed4d72b"><span class="id" title="notation">]</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#fe8473dd9402cdf9a6648d9eb80cf296"><span class="id" title="notation">\]</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="6eb8fcdc381668614d47d37b3c51dcaf" class="idref" href="#6eb8fcdc381668614d47d37b3c51dcaf"><span class="id" title="definition">Σ'</span></a> :=<br/>
(<a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#47d0d78d4d530216364af042577b7f7e"><span class="id" title="definition">StdLib.Σ</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c6"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#AcornMaybe"><span class="id" title="definition">Prelude.AcornMaybe</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg_syn"><span class="id" title="definition">msg_syn</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>)%<span class="id" title="var">list</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Counter.update_balance_syn" class="idref" href="#Counter.update_balance_syn"><span class="id" title="definition">update_balance_syn</span></a> :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.st"><span class="id" title="definition">st</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.new_balance"><span class="id" title="definition">new_balance</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a><br/>
<a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'Pair'_x_x_x_x"><span class="id" title="notation">Pair</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:expr::'balance'_x"><span class="id" title="notation">balance</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.st"><span class="id" title="definition">st</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#4e7f3c18e37c71881015cf8eb5da4608"><span class="id" title="notation">+</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.new_balance"><span class="id" title="definition">new_balance</span></a><a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">)</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:expr::'owner'_x"><span class="id" title="notation">owner</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.st"><span class="id" title="definition">st</span></a><a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">)</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a>.<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Unquote</span> <span class="id" title="keyword">Definition</span> <span class="id" title="var">_update_balance</span> :=<br/>
(<a class="idref" href="ConCert.Embedding.TranslationUtils.html#expr_to_tc"><span class="id" title="definition">expr_to_tc</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#6eb8fcdc381668614d47d37b3c51dcaf"><span class="id" title="definition">Σ'</span></a> (<a class="idref" href="ConCert.Embedding.Ast.html#indexify"><span class="id" title="definition">indexify</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.update_balance_syn"><span class="id" title="definition">update_balance_syn</span></a>)).<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="Counter.:expr::'update_balance'_x_x" class="idref" href="#Counter.:expr::'update_balance'_x_x"><span class="id" title="notation">"</span></a>'update_balance' a b" :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">{</span></a><a class="idref" href="ConCert.Embedding.Ast.html#eConst"><span class="id" title="constructor">eConst</span></a> (<a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter._update_balance"><span class="id" title="definition">_update_balance</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a>)<a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">}</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">{</span></a><span class="id" title="var">a</span><a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">}</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">{</span></a><span class="id" title="var">b</span><a class="idref" href="ConCert.Embedding.Notations.html#9bb18901484762033c8f1fa6120fb5d4"><span class="id" title="notation">}</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a><br/>
(<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">expr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
<span class="id" title="var">a</span> <span class="id" title="var">custom</span> <span class="id" title="var">expr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1,<br/>
<span class="id" title="var">b</span> <span class="id" title="var">custom</span> <span class="id" title="var">expr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1).<br/>
<br/>
</div>
<div class="doc">
The main functionality
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Counter.counter_syn" class="idref" href="#Counter.counter_syn"><span class="id" title="definition">counter_syn</span></a> :=<br/>
<a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.m"><span class="id" title="definition">m</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg"><span class="id" title="definition">msg</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.st"><span class="id" title="definition">st</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">case</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.m"><span class="id" title="definition">m</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg"><span class="id" title="definition">msg</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">return</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#Maybe"><span class="id" title="definition">Maybe</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#85ad000a5f24386f70f03588f3994b98"><span class="id" title="notation">((</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#List"><span class="id" title="definition">List</span></a> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain.SimpleActionBody"><span class="id" title="definition">SimpleActionBody</span></a><a class="idref" href="ConCert.Embedding.Notations.html#85ad000a5f24386f70f03588f3994b98"><span class="id" title="notation">)</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a><a class="idref" href="ConCert.Embedding.Notations.html#85ad000a5f24386f70f03588f3994b98"><span class="id" title="notation">)</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">of</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">|</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.Inc"><span class="id" title="definition">Inc</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.n"><span class="id" title="definition">n</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">-></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Just"><span class="id" title="definition">Just</span></a><a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Maybe"><span class="id" title="definition">Maybe</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">[:</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#List"><span class="id" title="definition">List</span></a> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain.SimpleActionBody"><span class="id" title="definition">SimpleActionBody</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a><a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">]</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'Pair'_x_x_x_x"><span class="id" title="notation">Pair</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#85ad000a5f24386f70f03588f3994b98"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#List"><span class="id" title="definition">List</span></a> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain.SimpleActionBody"><span class="id" title="definition">SimpleActionBody</span></a><a class="idref" href="ConCert.Embedding.Notations.html#85ad000a5f24386f70f03588f3994b98"><span class="id" title="notation">)</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'Nil'_x"><span class="id" title="notation">Nil</span></a> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain.SimpleActionBody"><span class="id" title="definition">SimpleActionBody</span></a><a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">)</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:expr::'update_balance'_x_x"><span class="id" title="notation">update_balance</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.st"><span class="id" title="definition">st</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.n"><span class="id" title="definition">n</span></a><a class="idref" href="ConCert.Embedding.Notations.html#d8c7a17158b575954bc29fcd16b46d59"><span class="id" title="notation">))</span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">|</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.Dec"><span class="id" title="definition">Dec</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.n"><span class="id" title="definition">n</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#decaa3b9884dd31ec0b158d946c8e148"><span class="id" title="notation">-></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Nothing"><span class="id" title="definition">Nothing</span></a><a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Maybe"><span class="id" title="definition">Maybe</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">[:</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#List"><span class="id" title="definition">List</span></a> <a class="idref" href="ConCert.Embedding.SimpleBlockchain.html#AcornBlockchain.SimpleActionBody"><span class="id" title="definition">SimpleActionBody</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a><a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">]</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a>.<br/>
<br/>
</div>
<div class="doc">
Packing together the data type definitions and functions
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="Counter.CounterModule" class="idref" href="#Counter.CounterModule"><span class="id" title="definition">CounterModule</span></a> : <a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#LiquidityModule"><span class="id" title="record">LiquidityModule</span></a> :=<br/>
{| <a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#datatypes"><span class="id" title="projection">datatypes</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg_syn"><span class="id" title="definition">msg_syn</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a>;<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#storage"><span class="id" title="projection">storage</span></a> := <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">[!</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.:type::'CounterState'"><span class="id" title="notation">CounterState</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">!]</span></a>;<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#init"><span class="id" title="projection">init</span></a> := <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">[|</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.n"><span class="id" title="definition">n</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a><a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.addr"><span class="id" title="definition">addr</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">\</span></a>"c" <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#:type::'CallCtx'"><span class="id" title="notation">CallCtx</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#5a67c20fae665de9355aa131b6b33c35"><span class="id" title="notation">=></span></a><br/>
<a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Just"><span class="id" title="definition">Just</span></a><a class="idref" href="ConCert.Embedding.Notations.html#4f86eaf1000e9ca2937549c277fa0fee"><span class="id" title="notation">$</span></a><a class="idref" href="ConCert.Embedding.Prelude.html#Maybe"><span class="id" title="definition">Maybe</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">[:</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#13c5a29999dbbe18ed94bdd5721d5919"><span class="id" title="notation">×</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a><a class="idref" href="ConCert.Embedding.Notations.html#e975a5db232bcbae17131a9ff8da5ecd"><span class="id" title="notation">]</span></a> <a class="idref" href="ConCert.Embedding.Prelude.html#:expr::'Pair'_x_x_x_x"><span class="id" title="notation">Pair</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#money"><span class="id" title="definition">money</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address"><span class="id" title="definition">address</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.n"><span class="id" title="definition">n</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.addr"><span class="id" title="definition">addr</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#143c2b826a30d37e0d680ea16616e805"><span class="id" title="notation">|]</span></a>;<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#message"><span class="id" title="projection">message</span></a> := <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">[!</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg"><span class="id" title="definition">msg</span></a> <a class="idref" href="ConCert.Embedding.Notations.html#8fd011f97194c1e6feedf544bfd179b4"><span class="id" title="notation">!]</span></a>;<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#functions"><span class="id" title="projection">functions</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>"_update_balance"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.update_balance_syn"><span class="id" title="definition">update_balance_syn</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>"counter"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.counter_syn"><span class="id" title="definition">counter_syn</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>;<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#main"><span class="id" title="projection">main</span></a> := "counter";<br/>
<a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#main_extra_args"><span class="id" title="projection">main_extra_args</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>|}.<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Unquote</span> <span class="id" title="keyword">Inductive</span> (<a class="idref" href="ConCert.Embedding.TranslationUtils.html#global_to_tc"><span class="id" title="definition">global_to_tc</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.msg_syn"><span class="id" title="definition">msg_syn</span></a>).<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Unquote</span> <span class="id" title="keyword">Definition</span> <span class="id" title="var">counter</span> :=<br/>
(<a class="idref" href="ConCert.Embedding.TranslationUtils.html#expr_to_tc"><span class="id" title="definition">expr_to_tc</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#6eb8fcdc381668614d47d37b3c51dcaf"><span class="id" title="definition">Σ'</span></a> (<a class="idref" href="ConCert.Embedding.Ast.html#indexify"><span class="id" title="definition">indexify</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter.counter_syn"><span class="id" title="definition">counter_syn</span></a>)).<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#Counter"><span class="id" title="module">Counter</span></a>.<br/>
<br/>
</div>
<div class="doc">
A translation table for types
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="TTty" class="idref" href="#TTty"><span class="id" title="definition">TTty</span></a> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#address_coq"><span class="id" title="inductive">address_coq</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "address"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="ConCert.Embedding.Extraction.PreludeExt.html#time_coq"><span class="id" title="inductive">time_coq</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "timestamp"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "tez"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "nat"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>.<br/>
<br/>
</div>
<div class="doc">
A translation table for primitive binary operations
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="TT" class="idref" href="#TT"><span class="id" title="definition">TT</span></a> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Embedding.pcuic.PCUICTranslate.html#to_string_name"><span class="id" title="definition">to_string_name</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation"><%</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.ZArith.BinInt.html#Z.add"><span class="id" title="definition">Z.add</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Loader.html#718bcc50d47fdc3f494b25555b8a784b"><span class="id" title="notation">%></span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "addTez"<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a>.<br/>
<br/>
</div>
<div class="doc">
The output has been tested in the online Liquidity editor: https://www.liquidity-lang.org/edit/
</div>
<div class="code">
<span class="id" title="keyword">Compute</span> <a class="idref" href="ConCert.Embedding.Extraction.Liquidity.html#liquidifyModule"><span class="id" title="definition">liquidifyModule</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#TT"><span class="id" title="definition">TT</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#TTty"><span class="id" title="definition">TTty</span></a> <a class="idref" href="ConCert.Examples.Counter.embedding.CounterEmbed.html#CounterModule"><span class="id" title="definition">Counter.CounterModule</span></a>.<br/>
<br/>
</div>
<div class="doc">
An attempt of extraction from the shallow embedding using the "native" Coq extraction mechanism
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Extraction</span> <span class="id" title="var">Language</span> <span class="id" title="var">OCaml</span>.<br/>
<br/>
<span class="id" title="keyword">Extract</span> <span class="id" title="keyword">Inductive</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> => "list" [ "[]" "(::)" ].<br/>
<span class="id" title="keyword">Extract</span> <span class="id" title="keyword">Inductive</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#prod"><span class="id" title="inductive">prod</span></a> => "(*)" [ "(,)" ].<br/>
<span class="id" title="keyword">Extract</span> <span class="id" title="keyword">Inductive</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> => "tez" ["0DUN" "id" "negate"].<br/>
<span class="id" title="keyword">Extract</span> <span class="id" title="var">Inlined</span> <span class="id" title="var">Constant</span> <span class="id" title="var">Z.add</span> => "addTez".<br/>
<br/>
</div>
<div class="doc">
In Liquidify, <span class="inlinecode">+</span> is overloaded and thus requires type annotations. We can overcome this issue by un-overloading the operations and providing specialised versions (not infix anymore).
<div class="paragraph"> </div>
Essentially, we need to prepend the follwing "prelude" before our contracts: let<span class="inlinecode">@<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a></span> fst (p : 'a * 'b) : 'a = p.(0)
let<span class="inlinecode">@<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a></span> snd (p : 'a * 'b) : 'b = p.(1)
let<span class="inlinecode">@<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a></span> addN (n : nat) (m : nat) = n + m
let<span class="inlinecode">@<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a></span> addTez (n : tez) (m : tez) = n + m
<div class="paragraph"> </div>
It seems there are some syntactic and semantic differences from OCaml. E.g. it's not possible to pattern-match on tuples in Liquidity, a special form of <span class="inlinecode"><span class="id" title="keyword">let</span></span> or projections must be used instead. That's why our "prelude" features the <span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#fst"><span class="id" title="definition">fst</span></a></span> and <span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#snd"><span class="id" title="definition">snd</span></a></span> functions. We use them explicitly instead of destructing pairs.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Extraction</span> <span class="id" title="var">Counter._update_balance</span>.<br/>
<span class="id" title="keyword">Extraction</span> <span class="id" title="var">Counter.counter</span>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="https://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a> and <a href="https://github.com/jgallen23/toc">TOC</a>
</div>
</div>
<script>
const elements = document.getElementsByClassName("libtitle");
while(elements.length > 0){
elements[0].parentNode.removeChild(elements[0]);
}
if (window.location.pathname.endsWith("/toc.html")) {
const jstocDiv = document.getElementById("js-toc");
jstocDiv.classList.remove("toc");
jstocDiv.classList.add("jstoc-hidden");
const jstocHeaderDiv = document.getElementById("js-toc-header");
jstocHeaderDiv.classList.add("jstoc-hidden");
const mainDiv = document.getElementById("main");
mainDiv.classList.add("jstoc-hidden-main");
const toggleDiv = document.getElementById("toggle-toc");
toggleDiv.classList.add("jstoc-hidden");
}
console.log(window.location.pathname);
</script>
<script type="text/javascript" src="toc.js"></script>
</body>
</html>
