mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-17 01:41:09 +03:00
Add the basic Cryptol classes
This commit is contained in:
parent
c03a590c34
commit
6bb573eef3
@ -701,6 +701,119 @@ Functions
|
|||||||
f p1 p2 = e // Function definition
|
f p1 p2 = e // Function definition
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
********************************************************************************
|
||||||
|
Overloaded Operations
|
||||||
|
********************************************************************************
|
||||||
|
|
||||||
|
Equality
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Eq
|
||||||
|
(==) : {a} (Eq a) => a -> a -> Bit
|
||||||
|
(!=) : {a} (Eq a) => a -> a -> Bit
|
||||||
|
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||||
|
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||||
|
|
||||||
|
Comparisons
|
||||||
|
===========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Cmp
|
||||||
|
(<) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(>) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(<=) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(>=) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
min : {a} (Cmp a) => a -> a -> a
|
||||||
|
max : {a} (Cmp a) => a -> a -> a
|
||||||
|
abs : {a} (Cmp a, Ring a) => a -> a
|
||||||
|
|
||||||
|
|
||||||
|
Signed Comparisons
|
||||||
|
==================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
SignedCmp
|
||||||
|
(<$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
|
||||||
|
|
||||||
|
Zero
|
||||||
|
====
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Zero
|
||||||
|
zero : {a} (Zero a) => a
|
||||||
|
|
||||||
|
Logical Operations
|
||||||
|
==================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Logic
|
||||||
|
(&&) : {a} (Logic a) => a -> a -> a
|
||||||
|
(||) : {a} (Logic a) => a -> a -> a
|
||||||
|
(^) : {a} (Logic a) => a -> a -> a
|
||||||
|
complement : {a} (Logic a) => a -> a
|
||||||
|
|
||||||
|
Basic Arithmetic
|
||||||
|
================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Ring
|
||||||
|
fromInteger : {a} (Ring a) => Integer -> a
|
||||||
|
(+) : {a} (Ring a) => a -> a -> a
|
||||||
|
(-) : {a} (Ring a) => a -> a -> a
|
||||||
|
(*) : {a} (Ring a) => a -> a -> a
|
||||||
|
negate : {a} (Ring a) => a -> a
|
||||||
|
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
|
||||||
|
|
||||||
|
Integral Operations
|
||||||
|
===================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Integral
|
||||||
|
(/) : {a} (Integral a) => a -> a -> a
|
||||||
|
(%) : {a} (Integral a) => a -> a -> a
|
||||||
|
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
|
||||||
|
toInteger : {a} (Integral a) => a -> Integer
|
||||||
|
infFrom : {a} (Integral a) => a -> [inf]a
|
||||||
|
infFromThen : {a} (Integral a) => a -> a -> [inf]a
|
||||||
|
|
||||||
|
|
||||||
|
Division
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Field
|
||||||
|
recip : {a} (Field a) => a -> a
|
||||||
|
(/.) : {a} (Field a) => a -> a -> a
|
||||||
|
|
||||||
|
Rounding
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Round
|
||||||
|
ceiling : {a} (Round a) => a -> Integer
|
||||||
|
floor : {a} (Round a) => a -> Integer
|
||||||
|
trunc : {a} (Round a) => a -> Integer
|
||||||
|
roundAway : {a} (Round a) => a -> Integer
|
||||||
|
roundToEven : {a} (Round a) => a -> Integer
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
********************************************************************************
|
********************************************************************************
|
||||||
Type Declarations
|
Type Declarations
|
||||||
********************************************************************************
|
********************************************************************************
|
||||||
|
Binary file not shown.
Binary file not shown.
@ -124,6 +124,18 @@
|
|||||||
<li><a class="reference internal" href="#functions">Functions</a></li>
|
<li><a class="reference internal" href="#functions">Functions</a></li>
|
||||||
</ul>
|
</ul>
|
||||||
</li>
|
</li>
|
||||||
|
<li><a class="reference internal" href="#overloaded-operations">Overloaded Operations</a><ul>
|
||||||
|
<li><a class="reference internal" href="#equality">Equality</a></li>
|
||||||
|
<li><a class="reference internal" href="#comparisons">Comparisons</a></li>
|
||||||
|
<li><a class="reference internal" href="#signed-comparisons">Signed Comparisons</a></li>
|
||||||
|
<li><a class="reference internal" href="#zero">Zero</a></li>
|
||||||
|
<li><a class="reference internal" href="#logical-operations">Logical Operations</a></li>
|
||||||
|
<li><a class="reference internal" href="#basic-arithmetic">Basic Arithmetic</a></li>
|
||||||
|
<li><a class="reference internal" href="#integral-operations">Integral Operations</a></li>
|
||||||
|
<li><a class="reference internal" href="#division">Division</a></li>
|
||||||
|
<li><a class="reference internal" href="#rounding">Rounding</a></li>
|
||||||
|
</ul>
|
||||||
|
</li>
|
||||||
<li><a class="reference internal" href="#type-declarations">Type Declarations</a><ul>
|
<li><a class="reference internal" href="#type-declarations">Type Declarations</a><ul>
|
||||||
<li><a class="reference internal" href="#type-synonyms">Type Synonyms</a></li>
|
<li><a class="reference internal" href="#type-synonyms">Type Synonyms</a></li>
|
||||||
<li><a class="reference internal" href="#newtypes">Newtypes</a></li>
|
<li><a class="reference internal" href="#newtypes">Newtypes</a></li>
|
||||||
@ -873,6 +885,102 @@ a location
|
|||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
|
<div class="section" id="overloaded-operations">
|
||||||
|
<h2>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this headline">¶</a></h2>
|
||||||
|
<div class="section" id="equality">
|
||||||
|
<h3>Equality<a class="headerlink" href="#equality" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Eq</span>
|
||||||
|
<span class="p">(</span><span class="o">==</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">!=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">===</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">b</span><span class="p">)</span> <span class="ow">=></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="n">b</span><span class="p">)</span> <span class="ow">-></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="n">b</span><span class="p">)</span> <span class="ow">-></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span><span class="p">)</span>
|
||||||
|
<span class="p">(</span><span class="o">!==</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">}</span> <span class="p">(</span><span class="kt">Eq</span> <span class="n">b</span><span class="p">)</span> <span class="ow">=></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="n">b</span><span class="p">)</span> <span class="ow">-></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="n">b</span><span class="p">)</span> <span class="ow">-></span> <span class="p">(</span><span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span><span class="p">)</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="comparisons">
|
||||||
|
<h3>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">Cmp</span>
|
||||||
|
<span class="p">(</span><span class="o"><</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">></span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o"><=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">>=</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="kr">min</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="kr">max</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="n">abs</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kr">Cmp</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="signed-comparisons">
|
||||||
|
<h3>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">SignedCmp</span>
|
||||||
|
<span class="p">(</span><span class="o"><$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">>$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o"><=$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
<span class="p">(</span><span class="o">>=$</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">SignedCmp</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="kr">Bit</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="zero">
|
||||||
|
<h3>Zero<a class="headerlink" href="#zero" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Zero</span>
|
||||||
|
<span class="n">zero</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Zero</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="logical-operations">
|
||||||
|
<h3>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Logic</span>
|
||||||
|
<span class="p">(</span><span class="o">&&</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">||</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="n">complement</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Logic</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="basic-arithmetic">
|
||||||
|
<h3>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Ring</span>
|
||||||
|
<span class="n">fromInteger</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="kt">Integer</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">+</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">-</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">*</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="n">negate</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">^^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">e</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Integral</span> <span class="n">e</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">e</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="integral-operations">
|
||||||
|
<h3>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Integral</span>
|
||||||
|
<span class="p">(</span><span class="o">/</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">%</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">^^</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">,</span> <span class="n">e</span><span class="p">}</span> <span class="p">(</span><span class="kt">Ring</span> <span class="n">a</span><span class="p">,</span> <span class="kt">Integral</span> <span class="n">e</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">e</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="n">toInteger</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
<span class="n">infFrom</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="p">[</span><span class="kr">inf</span><span class="p">]</span><span class="n">a</span>
|
||||||
|
<span class="n">infFromThen</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Integral</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="p">[</span><span class="kr">inf</span><span class="p">]</span><span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="division">
|
||||||
|
<h3>Division<a class="headerlink" href="#division" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Field</span>
|
||||||
|
<span class="n">recip</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Field</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
<span class="p">(</span><span class="o">/.</span><span class="p">)</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Field</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span> <span class="ow">-></span> <span class="n">a</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
<div class="section" id="rounding">
|
||||||
|
<h3>Rounding<a class="headerlink" href="#rounding" title="Permalink to this headline">¶</a></h3>
|
||||||
|
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Round</span>
|
||||||
|
<span class="n">ceiling</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
<span class="n">floor</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
<span class="n">trunc</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
<span class="n">roundAway</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
<span class="n">roundToEven</span> <span class="kt">:</span> <span class="p">{</span><span class="n">a</span><span class="p">}</span> <span class="p">(</span><span class="kt">Round</span> <span class="n">a</span><span class="p">)</span> <span class="ow">=></span> <span class="n">a</span> <span class="ow">-></span> <span class="kt">Integer</span>
|
||||||
|
</pre></div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
|
</div>
|
||||||
<div class="section" id="type-declarations">
|
<div class="section" id="type-declarations">
|
||||||
<h2>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this headline">¶</a></h2>
|
<h2>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this headline">¶</a></h2>
|
||||||
<div class="section" id="type-synonyms">
|
<div class="section" id="type-synonyms">
|
||||||
|
@ -701,6 +701,119 @@ Functions
|
|||||||
f p1 p2 = e // Function definition
|
f p1 p2 = e // Function definition
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
********************************************************************************
|
||||||
|
Overloaded Operations
|
||||||
|
********************************************************************************
|
||||||
|
|
||||||
|
Equality
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Eq
|
||||||
|
(==) : {a} (Eq a) => a -> a -> Bit
|
||||||
|
(!=) : {a} (Eq a) => a -> a -> Bit
|
||||||
|
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||||
|
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||||
|
|
||||||
|
Comparisons
|
||||||
|
===========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Cmp
|
||||||
|
(<) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(>) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(<=) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
(>=) : {a} (Cmp a) => a -> a -> Bit
|
||||||
|
min : {a} (Cmp a) => a -> a -> a
|
||||||
|
max : {a} (Cmp a) => a -> a -> a
|
||||||
|
abs : {a} (Cmp a, Ring a) => a -> a
|
||||||
|
|
||||||
|
|
||||||
|
Signed Comparisons
|
||||||
|
==================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
SignedCmp
|
||||||
|
(<$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
||||||
|
|
||||||
|
|
||||||
|
Zero
|
||||||
|
====
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Zero
|
||||||
|
zero : {a} (Zero a) => a
|
||||||
|
|
||||||
|
Logical Operations
|
||||||
|
==================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Logic
|
||||||
|
(&&) : {a} (Logic a) => a -> a -> a
|
||||||
|
(||) : {a} (Logic a) => a -> a -> a
|
||||||
|
(^) : {a} (Logic a) => a -> a -> a
|
||||||
|
complement : {a} (Logic a) => a -> a
|
||||||
|
|
||||||
|
Basic Arithmetic
|
||||||
|
================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Ring
|
||||||
|
fromInteger : {a} (Ring a) => Integer -> a
|
||||||
|
(+) : {a} (Ring a) => a -> a -> a
|
||||||
|
(-) : {a} (Ring a) => a -> a -> a
|
||||||
|
(*) : {a} (Ring a) => a -> a -> a
|
||||||
|
negate : {a} (Ring a) => a -> a
|
||||||
|
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
|
||||||
|
|
||||||
|
Integral Operations
|
||||||
|
===================
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Integral
|
||||||
|
(/) : {a} (Integral a) => a -> a -> a
|
||||||
|
(%) : {a} (Integral a) => a -> a -> a
|
||||||
|
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
|
||||||
|
toInteger : {a} (Integral a) => a -> Integer
|
||||||
|
infFrom : {a} (Integral a) => a -> [inf]a
|
||||||
|
infFromThen : {a} (Integral a) => a -> a -> [inf]a
|
||||||
|
|
||||||
|
|
||||||
|
Division
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Field
|
||||||
|
recip : {a} (Field a) => a -> a
|
||||||
|
(/.) : {a} (Field a) => a -> a -> a
|
||||||
|
|
||||||
|
Rounding
|
||||||
|
========
|
||||||
|
|
||||||
|
.. code-block:: cryptol
|
||||||
|
|
||||||
|
Round
|
||||||
|
ceiling : {a} (Round a) => a -> Integer
|
||||||
|
floor : {a} (Round a) => a -> Integer
|
||||||
|
trunc : {a} (Round a) => a -> Integer
|
||||||
|
roundAway : {a} (Round a) => a -> Integer
|
||||||
|
roundToEven : {a} (Round a) => a -> Integer
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
********************************************************************************
|
********************************************************************************
|
||||||
Type Declarations
|
Type Declarations
|
||||||
********************************************************************************
|
********************************************************************************
|
||||||
|
File diff suppressed because one or more lines are too long
Loading…
Reference in New Issue
Block a user