mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-29 10:53:31 +03:00
Merge pull request #1380 from GaloisInc/conditional-constraints
Numeric Constraint Guards
This commit is contained in:
Iavor S. Diatchki
GitHub
commit
f8b5543946
4
.gitignore
vendored
4
.gitignore
vendored
@ -10,6 +10,7 @@ dist-newstyle
|
||||
.ghc.environment.*
|
||||
cabal.project.freeze
|
||||
cabal.project.local*
|
||||
.vscode/
|
||||
|
||||
# don't check in generated documentation
|
||||
#docs/CryptolPrims.pdf
|
||||
@ -38,3 +39,6 @@ allfiles.wxs
|
||||
cryptol.msi
|
||||
cryptol.wixobj
|
||||
cryptol.wixpdb
|
||||
|
||||
# happy-generated files
|
||||
src/Cryptol/Parser.hs
|
||||
@ -2,6 +2,11 @@
|
||||
|
||||
## Language changes
|
||||
|
||||
* Declarations may now use *numeric constraint guards*. This is a feature
|
||||
that allows a function to behave differently depending on its numeric
|
||||
type parameters. See the [manual section](https://galoisinc.github.io/cryptol/RefMan/_build/html/BasicSyntax.html#numeric-constraint-guards))
|
||||
for more information.
|
||||
|
||||
* The foreign function interface (FFI) has been added, which allows Cryptol to
|
||||
call functions written in C. See the [manual section](https://galoisinc.github.io/cryptol/RefMan/_build/html/FFI.html)
|
||||
for more information.
|
||||
|
||||
55
ConditionalConstraints.md
Normal file
55
ConditionalConstraints.md
Normal file
@ -0,0 +1,55 @@
|
||||
# Conditional Constraints
|
||||
|
||||
## Syntax
|
||||
|
||||
The front-end AST has a new constructor:
|
||||
|
||||
```hs
|
||||
data BindDef name = DPropGuards [([Prop name], Expr name)] | ...
|
||||
```
|
||||
|
||||
which is parsed from the following syntax:
|
||||
|
||||
```
|
||||
<name> : <signature>
|
||||
<name> <pats>
|
||||
[ | <props> => <expr> ]
|
||||
```
|
||||
|
||||
## Expanding PropGuards
|
||||
|
||||
- Before renaming, a `Bind` with a `bDef = DPropGuards ...` will be expanded into several `Bind`s, one for each guard case.
|
||||
- The generated `Bind`s will have fresh names, but the names will have the same location as the original function's name.
|
||||
- These generated `Bind`'s will have the same type as the original function, except that the list of type constraints will also include the `Prop name`s that appeared on the LHS of the originating ase of `DPropGuards`.
|
||||
- The original function will have the `Expr name` in each of the `DPropGuards` cases replaced with a function call the appropriate, generated function.
|
||||
|
||||
## Renaming
|
||||
|
||||
The new constructor of `BindDef` is traversed as normal during renaming. This ensures that a function with `DPropGuards` ends up in the same mutual-recursion group as the generated functions that it calls.
|
||||
|
||||
## Typechecking
|
||||
|
||||
The back-end AST has a new constructor:
|
||||
|
||||
```hs
|
||||
data Expr = EPropGuards [([Prop], Expr)] | ...
|
||||
```
|
||||
|
||||
During typechecking, a `BindDef` of the form
|
||||
|
||||
```
|
||||
DPropGuards [(props1, f1 x y), (prop2, f2 x y)]
|
||||
```
|
||||
|
||||
is processed into a `Decl` of the form
|
||||
|
||||
```
|
||||
Decl
|
||||
{ dDefinition =
|
||||
DExpr (EPropGuards
|
||||
[ (props1, f1 x y)
|
||||
, (props2, f2 x y) ])
|
||||
}
|
||||
```
|
||||
|
||||
Each case of an `EPropGuards` is typechecked by first asssuming the `props` and then typechecking the expression. However, this typechecking isn't really that important because by construction the expression is just a simple application that is ensured to be well-typed. But we can use this structure for more general purposes.
|
||||
@ -79,6 +79,11 @@ cryptolError modErr warns =
|
||||
(20710, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonList (map jsonPretty errs))
|
||||
])
|
||||
ExpandPropGuardsError src err ->
|
||||
(20711, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonPretty err)
|
||||
])
|
||||
|
||||
NoIncludeErrors src errs ->
|
||||
-- TODO: structured error here
|
||||
(20720, [ ("source", jsonPretty src)
|
||||
|
||||
@ -104,6 +104,7 @@ library
|
||||
Cryptol.Parser.Names,
|
||||
Cryptol.Parser.Name,
|
||||
Cryptol.Parser.NoPat,
|
||||
Cryptol.Parser.ExpandPropGuards,
|
||||
Cryptol.Parser.NoInclude,
|
||||
Cryptol.Parser.Selector,
|
||||
Cryptol.Parser.Utils,
|
||||
|
||||
@ -19,6 +19,54 @@ Type Signatures
|
||||
f,g : {a,b} (fin a) => [a] b
|
||||
|
||||
|
||||
Numeric Constraint Guards
|
||||
-------------------------
|
||||
|
||||
A declaration with a signature can use *numeric constraint guards*,
|
||||
which are used to change the behavior of a functoin depending on its
|
||||
numeric type parameters. For example:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
len : {n} (fin n) => [n]a -> Integer
|
||||
len xs | n == 0 => 0
|
||||
| n > 0 => 1 + len (drop `{1} xs)
|
||||
|
||||
Each behavior starts with ``|`` and lists some constraints on the numeric
|
||||
parameters to a declaration. When applied, the function will use the first
|
||||
definition that satisfies the provided numeric parameters.
|
||||
|
||||
Numeric constraint guards are quite similar to an ``if`` expression,
|
||||
except that decisions are based on *types* rather than values. There
|
||||
is also an important difference to simply using demotion and an
|
||||
actual ``if`` statement:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
len' : {n} (fin n) => [n]a -> Integer
|
||||
len' xs = if `n == 0 => 0
|
||||
| `n > 0 => 1 + len (drop `{1} xs)
|
||||
|
||||
The definition of ``len'`` is rejected, because the *value based* ``if``
|
||||
expression does provide the *type based* fact ``n >= 1`` which is
|
||||
required by ``drop `{1} xs``, while in ``len``, the type-checker
|
||||
locally-assumes the constraint ``n > 0`` in that constraint-guarded branch
|
||||
and so it can in fact determine that ``n >= 1``.
|
||||
|
||||
Requirements:
|
||||
- Numeric constraint guards only support constraints over numeric literals,
|
||||
such as ``fin``, ``<=``, ``==``, etc.
|
||||
Type constraint aliases can also be used as long as they only constrain
|
||||
numeric literals.
|
||||
- The numeric constraint guards of a declaration should be exhaustive. The
|
||||
type-checker will attempt to prove that the set of constraint guards is
|
||||
exhaustive, but if it can't then it will issue a non-exhaustive constraint
|
||||
guards warning. This warning is controlled by the environmental option
|
||||
``warnNonExhaustiveConstraintGuards``.
|
||||
- Each constraint guard is checked *independently* of the others, and there
|
||||
are no implict assumptions that the previous behaviors do not match---
|
||||
instead the programmer needs to specify all constraints explicitly
|
||||
in the guard.
|
||||
|
||||
Layout
|
||||
------
|
||||
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -1,4 +1,4 @@
|
||||
# Sphinx build info version 1
|
||||
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
|
||||
config: 12febdda05646d6655d93ce350355f10
|
||||
config: 41758cdb8fafe65367e2aa727ac7d826
|
||||
tags: 645f666f9bcd5a90fca523b33c5a78b7
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -43,6 +42,7 @@
|
||||
<li class="toctree-l1 current"><a class="current reference internal" href="#">Basic Syntax</a><ul>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#declarations">Declarations</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#type-signatures">Type Signatures</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#numeric-constraint-guards">Numeric Constraint Guards</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#layout">Layout</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#comments">Comments</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#identifiers">Identifiers</a></li>
|
||||
@ -84,21 +84,67 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="basic-syntax">
|
||||
<h1>Basic Syntax<a class="headerlink" href="#basic-syntax" title="Permalink to this heading"></a></h1>
|
||||
<h1>Basic Syntax<a class="headerlink" href="#basic-syntax" title="Permalink to this headline"></a></h1>
|
||||
<section id="declarations">
|
||||
<h2>Declarations<a class="headerlink" href="#declarations" title="Permalink to this heading"></a></h2>
|
||||
<h2>Declarations<a class="headerlink" href="#declarations" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">z</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</section>
|
||||
<section id="type-signatures">
|
||||
<h2>Type Signatures<a class="headerlink" href="#type-signatures" title="Permalink to this heading"></a></h2>
|
||||
<h2>Type Signatures<a class="headerlink" href="#type-signatures" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="p">,</span><span class="n">g</span><span class="w"> </span><span class="kt">:</span><span class="w"> </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="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="w"> </span><span class="n">b</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</section>
|
||||
<section id="numeric-constraint-guards">
|
||||
<h2>Numeric Constraint Guards<a class="headerlink" href="#numeric-constraint-guards" title="Permalink to this headline"></a></h2>
|
||||
<p>A declaration with a signature can use <em>numeric constraint guards</em>,
|
||||
which are used to change the behavior of a functoin depending on its
|
||||
numeric type parameters. For example:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
<span class="nf">len</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>Each behavior starts with <code class="docutils literal notranslate"><span class="pre">|</span></code> and lists some constraints on the numeric
|
||||
parameters to a declaration. When applied, the function will use the first
|
||||
definition that satisfies the provided numeric parameters.</p>
|
||||
<p>Numeric constraint guards are quite similar to an <code class="docutils literal notranslate"><span class="pre">if</span></code> expression,
|
||||
except that decisions are based on <em>types</em> rather than values. There
|
||||
is also an important difference to simply using demotion and an
|
||||
actual <code class="docutils literal notranslate"><span class="pre">if</span></code> statement:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len'</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
<span class="nf">len'</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kr">if</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>The definition of <code class="docutils literal notranslate"><span class="pre">len'</span></code> is rejected, because the <em>value based</em> <code class="docutils literal notranslate"><span class="pre">if</span></code>
|
||||
expression does provide the <em>type based</em> fact <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">>=</span> <span class="pre">1</span></code> which is
|
||||
required by <code class="docutils literal notranslate"><span class="pre">drop</span> <span class="pre">`{1}</span> <span class="pre">xs</span></code>, while in <code class="docutils literal notranslate"><span class="pre">len</span></code>, the type-checker
|
||||
locally-assumes the constraint <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">></span> <span class="pre">0</span></code> in that constraint-guarded branch
|
||||
and so it can in fact determine that <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">>=</span> <span class="pre">1</span></code>.</p>
|
||||
<dl class="simple">
|
||||
<dt>Requirements:</dt><dd><ul class="simple">
|
||||
<li><p>Numeric constraint guards only support constraints over numeric literals,
|
||||
such as <code class="docutils literal notranslate"><span class="pre">fin</span></code>, <code class="docutils literal notranslate"><span class="pre"><=</span></code>, <code class="docutils literal notranslate"><span class="pre">==</span></code>, etc.
|
||||
Type constraint aliases can also be used as long as they only constrain
|
||||
numeric literals.</p></li>
|
||||
<li><p>The numeric constraint guards of a declaration should be exhaustive. The
|
||||
type-checker will attempt to prove that the set of constraint guards is
|
||||
exhaustive, but if it can’t then it will issue a non-exhaustive constraint
|
||||
guards warning. This warning is controlled by the environmental option
|
||||
<code class="docutils literal notranslate"><span class="pre">warnNonExhaustiveConstraintGuards</span></code>.</p></li>
|
||||
<li><p>Each constraint guard is checked <em>independently</em> of the others, and there
|
||||
are no implict assumptions that the previous behaviors do not match—
|
||||
instead the programmer needs to specify all constraints explicitly
|
||||
in the guard.</p></li>
|
||||
</ul>
|
||||
</dd>
|
||||
</dl>
|
||||
</section>
|
||||
<section id="layout">
|
||||
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this heading"></a></h2>
|
||||
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this headline"></a></h2>
|
||||
<p>Groups of declarations are organized based on indentation.
|
||||
Declarations with the same indentation belong to the same group.
|
||||
Lines of text that are indented more than the beginning of a
|
||||
@ -119,7 +165,7 @@ lines between <cite>f</cite> and <cite>g</cite> that are indented more than <cit
|
||||
of <cite>f</cite>, which defines two more local names, <cite>y</cite> and <cite>z</cite>.</p>
|
||||
</section>
|
||||
<section id="comments">
|
||||
<h2>Comments<a class="headerlink" href="#comments" title="Permalink to this heading"></a></h2>
|
||||
<h2>Comments<a class="headerlink" href="#comments" title="Permalink to this headline"></a></h2>
|
||||
<p>Cryptol supports block comments, which start with <code class="docutils literal notranslate"><span class="pre">/*</span></code> and end with
|
||||
<code class="docutils literal notranslate"><span class="pre">*/</span></code>, and line comments, which start with <code class="docutils literal notranslate"><span class="pre">//</span></code> and terminate at the
|
||||
end of the line. Block comments may be nested arbitrarily.</p>
|
||||
@ -134,7 +180,7 @@ end of the line. Block comments may be nested arbitrarily.</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="identifiers">
|
||||
<h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to this heading"></a></h2>
|
||||
<h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to this headline"></a></h2>
|
||||
<p>Cryptol identifiers consist of one or more characters. The first
|
||||
character must be either an English letter or underscore (<code class="docutils literal notranslate"><span class="pre">_</span></code>). The
|
||||
following characters may be an English letter, a decimal digit,
|
||||
@ -150,7 +196,7 @@ names (see <a class="reference internal" href="#keywords-and-built-in-operators"
|
||||
</div>
|
||||
</section>
|
||||
<section id="keywords-and-built-in-operators">
|
||||
<h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-built-in-operators" title="Permalink to this heading"></a></h2>
|
||||
<h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-built-in-operators" title="Permalink to this headline"></a></h2>
|
||||
<p>The following identifiers have special meanings in Cryptol, and may
|
||||
not be used for programmer defined names:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id3">
|
||||
@ -227,7 +273,7 @@ precedence last.</p>
|
||||
</table>
|
||||
</section>
|
||||
<section id="built-in-type-level-operators">
|
||||
<h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-level-operators" title="Permalink to this heading"></a></h2>
|
||||
<h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-level-operators" title="Permalink to this headline"></a></h2>
|
||||
<p>Cryptol includes a variety of operators that allow computations on
|
||||
the numeric types used to specify the sizes of sequences.</p>
|
||||
<table class="docutils align-default" id="id5">
|
||||
@ -282,7 +328,7 @@ the numeric types used to specify the sizes of sequences.</p>
|
||||
</table>
|
||||
</section>
|
||||
<section id="numeric-literals">
|
||||
<h2>Numeric Literals<a class="headerlink" href="#numeric-literals" title="Permalink to this heading"></a></h2>
|
||||
<h2>Numeric Literals<a class="headerlink" href="#numeric-literals" title="Permalink to this headline"></a></h2>
|
||||
<p>Numeric literals may be written in binary, octal, decimal, or
|
||||
hexadecimal notation. The base of a literal is determined by its prefix:
|
||||
<code class="docutils literal notranslate"><span class="pre">0b</span></code> for binary, <code class="docutils literal notranslate"><span class="pre">0o</span></code> for octal, no special prefix for
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -83,9 +82,9 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="basic-types">
|
||||
<h1>Basic Types<a class="headerlink" href="#basic-types" title="Permalink to this heading"></a></h1>
|
||||
<h1>Basic Types<a class="headerlink" href="#basic-types" title="Permalink to this headline"></a></h1>
|
||||
<section id="tuples-and-records">
|
||||
<h2>Tuples and Records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h2>
|
||||
<h2>Tuples and Records<a class="headerlink" href="#tuples-and-records" title="Permalink to this headline"></a></h2>
|
||||
<p>Tuples and records are used for packaging multiple values together.
|
||||
Tuples are enclosed in parentheses, while records are enclosed in
|
||||
curly braces. The components of both tuples and records are separated by
|
||||
@ -114,7 +113,7 @@ Examples:</p>
|
||||
components are compared in the order they appear, whereas record
|
||||
fields are compared in alphabetical order of field names.</p>
|
||||
<section id="accessing-fields">
|
||||
<h3>Accessing Fields<a class="headerlink" href="#accessing-fields" title="Permalink to this heading"></a></h3>
|
||||
<h3>Accessing Fields<a class="headerlink" href="#accessing-fields" title="Permalink to this headline"></a></h3>
|
||||
<p>The components of a record or a tuple may be accessed in two ways: via
|
||||
pattern matching or by using explicit component selectors. Explicit
|
||||
component selectors are written as follows:</p>
|
||||
@ -165,7 +164,7 @@ entry in the tuple.</p>
|
||||
<p>This behavior is quite handy when examining complex data at the REPL.</p>
|
||||
</section>
|
||||
<section id="updating-fields">
|
||||
<h3>Updating Fields<a class="headerlink" href="#updating-fields" title="Permalink to this heading"></a></h3>
|
||||
<h3>Updating Fields<a class="headerlink" href="#updating-fields" title="Permalink to this headline"></a></h3>
|
||||
<p>The components of a record or a tuple may be updated using the following
|
||||
notation:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// Example values</span><span class="w"></span>
|
||||
@ -188,7 +187,7 @@ notation:</p>
|
||||
</section>
|
||||
</section>
|
||||
<section id="sequences">
|
||||
<h2>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h2>
|
||||
<h2>Sequences<a class="headerlink" href="#sequences" title="Permalink to this headline"></a></h2>
|
||||
<p>A sequence is a fixed-length collection of elements of the same type.
|
||||
The type of a finite sequence of length <cite>n</cite>, with elements of type <cite>a</cite>
|
||||
is <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">a</span></code>. Often, a finite sequence of bits, <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">Bit</span></code>, is called a
|
||||
@ -267,7 +266,7 @@ a location
|
||||
</div>
|
||||
</section>
|
||||
<section id="functions">
|
||||
<h2>Functions<a class="headerlink" href="#functions" title="Permalink to this heading"></a></h2>
|
||||
<h2>Functions<a class="headerlink" href="#functions" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">\</span><span class="n">p1</span><span class="w"> </span><span class="n">p2</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="c1">// Lambda expression</span><span class="w"></span>
|
||||
<span class="nf">f</span><span class="w"> </span><span class="n">p1</span><span class="w"> </span><span class="n">p2</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="c1">// Function definition</span><span class="w"></span>
|
||||
</pre></div>
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -85,10 +84,10 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="expressions">
|
||||
<h1>Expressions<a class="headerlink" href="#expressions" title="Permalink to this heading"></a></h1>
|
||||
<h1>Expressions<a class="headerlink" href="#expressions" title="Permalink to this headline"></a></h1>
|
||||
<p>This section provides an overview of the Cryptol’s expression syntax.</p>
|
||||
<section id="calling-functions">
|
||||
<h2>Calling Functions<a class="headerlink" href="#calling-functions" title="Permalink to this heading"></a></h2>
|
||||
<h2>Calling Functions<a class="headerlink" href="#calling-functions" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="c1">// call `f` with parameter `2`</span><span class="w"></span>
|
||||
<span class="nf">g</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="c1">// call `g` with two parameters: `x` and `y`</span><span class="w"></span>
|
||||
<span class="nf">h</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">y</span><span class="p">)</span><span class="w"> </span><span class="c1">// call `h` with one parameter, the pair `(x,y)`</span><span class="w"></span>
|
||||
@ -96,7 +95,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="prefix-operators">
|
||||
<h2>Prefix Operators<a class="headerlink" href="#prefix-operators" title="Permalink to this heading"></a></h2>
|
||||
<h2>Prefix Operators<a class="headerlink" href="#prefix-operators" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="o">-</span><span class="mi">2</span><span class="w"> </span><span class="c1">// call unary `-` with parameter `2`</span><span class="w"></span>
|
||||
<span class="o">-</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="c1">// call unary `-` with parameter `2`</span><span class="w"></span>
|
||||
<span class="nf">f</span><span class="w"> </span><span class="p">(</span><span class="o">-</span><span class="mi">2</span><span class="p">)</span><span class="w"> </span><span class="c1">// call `f` with one argument: `-2`, parens are important</span><span class="w"></span>
|
||||
@ -106,7 +105,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="infix-functions">
|
||||
<h2>Infix Functions<a class="headerlink" href="#infix-functions" title="Permalink to this heading"></a></h2>
|
||||
<h2>Infix Functions<a class="headerlink" href="#infix-functions" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3`</span><span class="w"></span>
|
||||
<span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">*</span><span class="w"> </span><span class="mi">5</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3 * 5`</span><span class="w"></span>
|
||||
<span class="p">(</span><span class="o">+</span><span class="p">)</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3`</span><span class="w"></span>
|
||||
@ -117,7 +116,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="type-annotations">
|
||||
<h2>Type Annotations<a class="headerlink" href="#type-annotations" title="Permalink to this heading"></a></h2>
|
||||
<h2>Type Annotations<a class="headerlink" href="#type-annotations" title="Permalink to this headline"></a></h2>
|
||||
<p>Explicit type annotations may be added on expressions, patterns, and
|
||||
in argument definitions.</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kr">Bit</span><span class="w"> </span><span class="c1">// specify that `x` has type `Bit`</span><span class="w"></span>
|
||||
@ -139,7 +138,7 @@ in argument definitions.</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="explicit-type-instantiation">
|
||||
<h2>Explicit Type Instantiation<a class="headerlink" href="#explicit-type-instantiation" title="Permalink to this heading"></a></h2>
|
||||
<h2>Explicit Type Instantiation<a class="headerlink" href="#explicit-type-instantiation" title="Permalink to this headline"></a></h2>
|
||||
<p>If <code class="docutils literal notranslate"><span class="pre">f</span></code> is a polymorphic value with type:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">tyParam</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="n">tyParam</span><span class="w"></span>
|
||||
<span class="nf">f</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">zero</span><span class="w"></span>
|
||||
@ -151,7 +150,7 @@ in argument definitions.</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="local-declarations">
|
||||
<h2>Local Declarations<a class="headerlink" href="#local-declarations" title="Permalink to this heading"></a></h2>
|
||||
<h2>Local Declarations<a class="headerlink" href="#local-declarations" title="Permalink to this headline"></a></h2>
|
||||
<p>Local declarations have the weakest precedence of all expressions.</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="kt">T</span><span class="p">]</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="kr">where</span><span class="w"></span>
|
||||
@ -167,7 +166,7 @@ in argument definitions.</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="block-arguments">
|
||||
<h2>Block Arguments<a class="headerlink" href="#block-arguments" title="Permalink to this heading"></a></h2>
|
||||
<h2>Block Arguments<a class="headerlink" href="#block-arguments" title="Permalink to this headline"></a></h2>
|
||||
<p>When used as the last argument to a function call,
|
||||
<code class="docutils literal notranslate"><span class="pre">if</span></code> and lambda expressions do not need parens:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="nf">\</span><span class="n">x</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="c1">// call `f` with one argument `x -> x`</span><span class="w"></span>
|
||||
@ -178,7 +177,7 @@ in argument definitions.</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="conditionals">
|
||||
<h2>Conditionals<a class="headerlink" href="#conditionals" title="Permalink to this heading"></a></h2>
|
||||
<h2>Conditionals<a class="headerlink" href="#conditionals" title="Permalink to this headline"></a></h2>
|
||||
<p>The <code class="docutils literal notranslate"><span class="pre">if</span> <span class="pre">...</span> <span class="pre">then</span> <span class="pre">...</span> <span class="pre">else</span></code> construct can be used with
|
||||
multiple branches. For example:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kr">if</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="kr">then</span><span class="w"> </span><span class="mi">22</span><span class="w"> </span><span class="kr">else</span><span class="w"> </span><span class="mi">33</span><span class="w"></span>
|
||||
@ -191,7 +190,7 @@ multiple branches. For example:</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="demoting-numeric-types-to-values">
|
||||
<h2>Demoting Numeric Types to Values<a class="headerlink" href="#demoting-numeric-types-to-values" title="Permalink to this heading"></a></h2>
|
||||
<h2>Demoting Numeric Types to Values<a class="headerlink" href="#demoting-numeric-types-to-values" title="Permalink to this headline"></a></h2>
|
||||
<p>The value corresponding to a numeric type may be accessed using the
|
||||
following notation:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">`</span><span class="n">t</span><span class="w"></span>
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -94,16 +93,16 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="foreign-function-interface">
|
||||
<h1>Foreign Function Interface<a class="headerlink" href="#foreign-function-interface" title="Permalink to this heading"></a></h1>
|
||||
<h1>Foreign Function Interface<a class="headerlink" href="#foreign-function-interface" title="Permalink to this headline"></a></h1>
|
||||
<p>The foreign function interface (FFI) allows Cryptol to call functions written in
|
||||
C (or other languages that use the C calling convention).</p>
|
||||
<section id="platform-support">
|
||||
<h2>Platform support<a class="headerlink" href="#platform-support" title="Permalink to this heading"></a></h2>
|
||||
<h2>Platform support<a class="headerlink" href="#platform-support" title="Permalink to this headline"></a></h2>
|
||||
<p>The FFI is currently <strong>not supported on Windows</strong>, and only works on Unix-like
|
||||
systems (macOS and Linux).</p>
|
||||
</section>
|
||||
<section id="basic-usage">
|
||||
<h2>Basic usage<a class="headerlink" href="#basic-usage" title="Permalink to this heading"></a></h2>
|
||||
<h2>Basic usage<a class="headerlink" href="#basic-usage" title="Permalink to this headline"></a></h2>
|
||||
<p>Suppose we want to call the following C function:</p>
|
||||
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">uint32_t</span><span class="w"> </span><span class="nf">add</span><span class="p">(</span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">y</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="k">return</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="p">;</span><span class="w"></span>
|
||||
@ -149,7 +148,7 @@ responsibility to make sure the types match up</strong>. If they do not then the
|
||||
be undefined behavior.</p>
|
||||
</section>
|
||||
<section id="compiling-c-code">
|
||||
<h2>Compiling C code<a class="headerlink" href="#compiling-c-code" title="Permalink to this heading"></a></h2>
|
||||
<h2>Compiling C code<a class="headerlink" href="#compiling-c-code" title="Permalink to this headline"></a></h2>
|
||||
<p>Cryptol currently does not handle compilation of C code to shared libraries. For
|
||||
simple usages, you can do this manually with the following commands:</p>
|
||||
<ul class="simple">
|
||||
@ -158,12 +157,12 @@ simple usages, you can do this manually with the following commands:</p>
|
||||
</ul>
|
||||
</section>
|
||||
<section id="converting-between-cryptol-and-c-types">
|
||||
<h2>Converting between Cryptol and C types<a class="headerlink" href="#converting-between-cryptol-and-c-types" title="Permalink to this heading"></a></h2>
|
||||
<h2>Converting between Cryptol and C types<a class="headerlink" href="#converting-between-cryptol-and-c-types" title="Permalink to this headline"></a></h2>
|
||||
<p>This section describes how a given Cryptol function signature maps to a C
|
||||
function prototype. The FFI only supports a limited set of Cryptol types which
|
||||
have a clear translation into C.</p>
|
||||
<section id="overall-structure">
|
||||
<h3>Overall structure<a class="headerlink" href="#overall-structure" title="Permalink to this heading"></a></h3>
|
||||
<h3>Overall structure<a class="headerlink" href="#overall-structure" title="Permalink to this headline"></a></h3>
|
||||
<p>Cryptol <code class="docutils literal notranslate"><span class="pre">foreign</span></code> bindings must be functions. These functions may have
|
||||
multiple (curried) arguments; they may also be polymorphic, with certain
|
||||
limitations. That is, the general structure of a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration would
|
||||
@ -190,7 +189,7 @@ Cryptol arguments.</p>
|
||||
corresponds to.</p>
|
||||
</section>
|
||||
<section id="type-parameters">
|
||||
<h3>Type parameters<a class="headerlink" href="#type-parameters" title="Permalink to this heading"></a></h3>
|
||||
<h3>Type parameters<a class="headerlink" href="#type-parameters" title="Permalink to this headline"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 55%" />
|
||||
@ -217,7 +216,7 @@ satisfy <code class="docutils literal notranslate"><span class="pre"><</span>
|
||||
cumbersome.)</p>
|
||||
</section>
|
||||
<section id="bit">
|
||||
<h3>Bit<a class="headerlink" href="#bit" title="Permalink to this heading"></a></h3>
|
||||
<h3>Bit<a class="headerlink" href="#bit" title="Permalink to this headline"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 52%" />
|
||||
@ -239,7 +238,7 @@ When converting to Cryptol, any nonzero number is converted to <code class="docu
|
||||
<code class="docutils literal notranslate"><span class="pre">0</span></code> is converted to <code class="docutils literal notranslate"><span class="pre">False</span></code>.</p>
|
||||
</section>
|
||||
<section id="integral-types">
|
||||
<h3>Integral types<a class="headerlink" href="#integral-types" title="Permalink to this heading"></a></h3>
|
||||
<h3>Integral types<a class="headerlink" href="#integral-types" title="Permalink to this headline"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type. Note <code class="docutils literal notranslate"><span class="pre">K</span></code> must be an actual fixed numeric type
|
||||
and not a type variable.</p>
|
||||
<table class="docutils align-default">
|
||||
@ -278,7 +277,7 @@ words first in Cryptol, then use the FFI conversion for sequences of words to
|
||||
handle it in C as an array.</p>
|
||||
</section>
|
||||
<section id="floating-point-types">
|
||||
<h3>Floating point types<a class="headerlink" href="#floating-point-types" title="Permalink to this heading"></a></h3>
|
||||
<h3>Floating point types<a class="headerlink" href="#floating-point-types" title="Permalink to this headline"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 55%" />
|
||||
@ -302,7 +301,7 @@ handle it in C as an array.</p>
|
||||
Other sizes of floating points are not supported.</p>
|
||||
</section>
|
||||
<section id="sequences">
|
||||
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h3>
|
||||
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this headline"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">n1,</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">nk</span> <span class="pre">:</span> <span class="pre">#</span></code> be Cryptol types (with <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">>=</span> <span class="pre">1</span></code>), possibly
|
||||
containing type variables, that satisfy <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n1,</span> <span class="pre">fin</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">fin</span> <span class="pre">nk</span></code>, and
|
||||
<code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or <em>floating point types</em>.
|
||||
@ -331,7 +330,7 @@ along with the pointer, any type arguments contained in the size are passed as C
|
||||
<code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s earlier, so the C code can always know the dimensions of the array.</p>
|
||||
</section>
|
||||
<section id="tuples-and-records">
|
||||
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h3>
|
||||
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this headline"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> be Cryptol types supported by the FFI (which may be any
|
||||
of the types mentioned above, or tuples and records themselves). Let
|
||||
<code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code> be the C types that <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> respectively
|
||||
@ -361,12 +360,12 @@ flattening is applied recursively for nested tuples and records. Note that this
|
||||
means empty tuples don’t map to any C values at all.</p>
|
||||
</section>
|
||||
<section id="type-synonyms">
|
||||
<h3>Type synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this heading"></a></h3>
|
||||
<h3>Type synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this headline"></a></h3>
|
||||
<p>All type synonyms are expanded before applying the above rules, so you can use
|
||||
type synonyms in <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declarations to improve readability.</p>
|
||||
</section>
|
||||
<section id="return-values">
|
||||
<h3>Return values<a class="headerlink" href="#return-values" title="Permalink to this heading"></a></h3>
|
||||
<h3>Return values<a class="headerlink" href="#return-values" title="Permalink to this headline"></a></h3>
|
||||
<p>If the Cryptol return type is <code class="docutils literal notranslate"><span class="pre">Bit</span></code> or one of the above <em>integral types</em> or
|
||||
<em>floating point types</em>, the value is returned directly from the C function. In
|
||||
that case, the return type of the C function will be the C type corresponding to
|
||||
@ -379,7 +378,7 @@ a pointer <code class="docutils literal notranslate"><span class="pre">U*</span>
|
||||
input versions are the same type, because it is already a pointer.</p>
|
||||
</section>
|
||||
<section id="quick-reference">
|
||||
<h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalink to this heading"></a></h3>
|
||||
<h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalink to this headline"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 37%" />
|
||||
@ -457,7 +456,7 @@ input versions are the same type, because it is already a pointer.</p>
|
||||
</section>
|
||||
</section>
|
||||
<section id="memory">
|
||||
<h2>Memory<a class="headerlink" href="#memory" title="Permalink to this heading"></a></h2>
|
||||
<h2>Memory<a class="headerlink" href="#memory" title="Permalink to this headline"></a></h2>
|
||||
<p>When pointers are involved, namely in the cases of sequences and output
|
||||
arguments, they point to memory. This memory is always allocated and deallocated
|
||||
by Cryptol; the C code does not need to manage this memory.</p>
|
||||
@ -471,11 +470,11 @@ memory may be uninitialized when passed to C, and the C code should not read
|
||||
from it. It must write to the memory the value it is returning.</p>
|
||||
</section>
|
||||
<section id="evaluation">
|
||||
<h2>Evaluation<a class="headerlink" href="#evaluation" title="Permalink to this heading"></a></h2>
|
||||
<h2>Evaluation<a class="headerlink" href="#evaluation" title="Permalink to this headline"></a></h2>
|
||||
<p>All Cryptol arguments are fully evaluated when a foreign function is called.</p>
|
||||
</section>
|
||||
<section id="example">
|
||||
<h2>Example<a class="headerlink" href="#example" title="Permalink to this heading"></a></h2>
|
||||
<h2>Example<a class="headerlink" href="#example" title="Permalink to this headline"></a></h2>
|
||||
<p>The Cryptol signature</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">][</span><span class="mi">10</span><span class="p">]</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kr">Bit</span><span class="p">,</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">64</span><span class="p">]}</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">(</span><span class="kt">Float64</span><span class="p">,</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">1</span><span class="p">][</span><span class="mi">20</span><span class="p">])</span><span class="w"></span>
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -100,7 +99,7 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="modules">
|
||||
<h1>Modules<a class="headerlink" href="#modules" title="Permalink to this heading"></a></h1>
|
||||
<h1>Modules<a class="headerlink" href="#modules" title="Permalink to this headline"></a></h1>
|
||||
<p>A <em>module</em> is used to group some related definitions. Each file may
|
||||
contain at most one top-level module.</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span><span class="w"> </span><span class="nn">M</span><span class="w"> </span><span class="kr">where</span><span class="w"></span>
|
||||
@ -112,7 +111,7 @@ contain at most one top-level module.</p>
|
||||
</pre></div>
|
||||
</div>
|
||||
<section id="hierarchical-module-names">
|
||||
<h2>Hierarchical Module Names<a class="headerlink" href="#hierarchical-module-names" title="Permalink to this heading"></a></h2>
|
||||
<h2>Hierarchical Module Names<a class="headerlink" href="#hierarchical-module-names" title="Permalink to this headline"></a></h2>
|
||||
<p>Module may have either simple or <em>hierarchical</em> names.
|
||||
Hierarchical names are constructed by gluing together ordinary
|
||||
identifiers using the symbol <code class="docutils literal notranslate"><span class="pre">::</span></code>.</p>
|
||||
@ -129,7 +128,7 @@ will look for a file named <code class="docutils literal notranslate"><span clas
|
||||
<code class="docutils literal notranslate"><span class="pre">Hash</span></code>, contained in one of the directories specified by <code class="docutils literal notranslate"><span class="pre">CRYPTOLPATH</span></code>.</p>
|
||||
</section>
|
||||
<section id="module-imports">
|
||||
<h2>Module Imports<a class="headerlink" href="#module-imports" title="Permalink to this heading"></a></h2>
|
||||
<h2>Module Imports<a class="headerlink" href="#module-imports" title="Permalink to this headline"></a></h2>
|
||||
<p>To use the definitions from one module in another module, we use
|
||||
<code class="docutils literal notranslate"><span class="pre">import</span></code> declarations:</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id1">
|
||||
@ -154,7 +153,7 @@ will look for a file named <code class="docutils literal notranslate"><span clas
|
||||
</div>
|
||||
</div>
|
||||
<section id="import-lists">
|
||||
<h3>Import Lists<a class="headerlink" href="#import-lists" title="Permalink to this heading"></a></h3>
|
||||
<h3>Import Lists<a class="headerlink" href="#import-lists" title="Permalink to this headline"></a></h3>
|
||||
<p>Sometimes, we may want to import only some of the definitions
|
||||
from a module. To do so, we use an import declaration with
|
||||
an <em>import list</em>.</p>
|
||||
@ -177,7 +176,7 @@ It also tends to make code easier to understand, because
|
||||
it makes it easy to see the source of definitions.</p>
|
||||
</section>
|
||||
<section id="hiding-imports">
|
||||
<h3>Hiding Imports<a class="headerlink" href="#hiding-imports" title="Permalink to this heading"></a></h3>
|
||||
<h3>Hiding Imports<a class="headerlink" href="#hiding-imports" title="Permalink to this headline"></a></h3>
|
||||
<p>Sometimes a module may provide many definitions, and we want to use
|
||||
most of them but with a few exceptions (e.g., because those would
|
||||
result to a name clash). In such situations it is convenient
|
||||
@ -204,7 +203,7 @@ to use a <em>hiding</em> import:</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="qualified-module-imports">
|
||||
<h3>Qualified Module Imports<a class="headerlink" href="#qualified-module-imports" title="Permalink to this heading"></a></h3>
|
||||
<h3>Qualified Module Imports<a class="headerlink" href="#qualified-module-imports" title="Permalink to this headline"></a></h3>
|
||||
<p>Another way to avoid name collisions is by using a
|
||||
<em>qualified</em> import.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id5">
|
||||
@ -253,7 +252,7 @@ but to use them, you would have to qualify using the prefix <code class="docutil
|
||||
</section>
|
||||
</section>
|
||||
<section id="private-blocks">
|
||||
<h2>Private Blocks<a class="headerlink" href="#private-blocks" title="Permalink to this heading"></a></h2>
|
||||
<h2>Private Blocks<a class="headerlink" href="#private-blocks" title="Permalink to this headline"></a></h2>
|
||||
<p>In some cases, definitions in a module might use helper
|
||||
functions that are not intended to be used outside the module.
|
||||
It is good practice to place such declarations in <em>private blocks</em>:</p>
|
||||
@ -318,7 +317,7 @@ is equivalent to the previous one:</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="nested-modules">
|
||||
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this heading"></a></h2>
|
||||
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this headline"></a></h2>
|
||||
<p>Module may be declared withing other modules, using the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keword.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id12">
|
||||
<div class="code-block-caption"><span class="caption-text">Declaring a nested module called N</span><a class="headerlink" href="#id12" title="Permalink to this code"></a></div>
|
||||
@ -355,7 +354,7 @@ to the name of a submodule.</p>
|
||||
So, in the previous example, it would be an error if <code class="docutils literal notranslate"><span class="pre">y</span></code> was
|
||||
to try to use <code class="docutils literal notranslate"><span class="pre">z</span></code> in its definition.</p>
|
||||
<section id="implicit-imports">
|
||||
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this heading"></a></h3>
|
||||
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this headline"></a></h3>
|
||||
<p>For convenience, we add an implicit qualified submodule import for
|
||||
each locally defined submodules.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id14">
|
||||
@ -375,7 +374,7 @@ each locally defined submodules.</p>
|
||||
an implicit import <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submoulde</span> <span class="pre">N</span> <span class="pre">as</span> <span class="pre">N</span></code>.</p>
|
||||
</section>
|
||||
<section id="managing-module-names">
|
||||
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this heading"></a></h3>
|
||||
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this headline"></a></h3>
|
||||
<p>The names of nested modules are managed by the module system just
|
||||
like the name of any other declaration in Cryptol. Thus, nested
|
||||
modules may declared in the public or private sections of their
|
||||
@ -407,14 +406,14 @@ another top-level module <code class="docutils literal notranslate"><span class=
|
||||
</section>
|
||||
</section>
|
||||
<section id="parameterized-modules">
|
||||
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this heading"></a></h2>
|
||||
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this headline"></a></h2>
|
||||
<div class="admonition warning">
|
||||
<p class="admonition-title">Warning</p>
|
||||
<p>The documentation in this section is for the upcoming variant of
|
||||
the feature, which is not yet part of main line Cryptol.</p>
|
||||
</div>
|
||||
<section id="interface-modules">
|
||||
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this heading"></a></h3>
|
||||
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this headline"></a></h3>
|
||||
<p>An <em>interface module</em> describes the content of a module
|
||||
without providing a concrete implementation.</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id16">
|
||||
@ -449,7 +448,7 @@ other modules:</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="importing-an-interface-module">
|
||||
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this heading"></a></h3>
|
||||
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this headline"></a></h3>
|
||||
<p>A module may be parameterized by importing an interface,
|
||||
instead of a concrete module</p>
|
||||
<div class="literal-block-wrapper docutils container" id="id18">
|
||||
@ -498,7 +497,7 @@ module, as described in <a class="reference internal" href="#instantiating-modul
|
||||
</div>
|
||||
</section>
|
||||
<section id="interface-constraints">
|
||||
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this heading"></a></h3>
|
||||
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this headline"></a></h3>
|
||||
<p>When working with multiple interfaces, it is to useful
|
||||
to be able to impose additional constraints on the
|
||||
types imported from the interface.</p>
|
||||
@ -527,7 +526,7 @@ same. Note that, of course, the two instantiations
|
||||
may provide different values for <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
|
||||
</section>
|
||||
<section id="instantiating-a-parameterized-module">
|
||||
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this heading"></a></h3>
|
||||
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this headline"></a></h3>
|
||||
<p>To use a parameterized module we need to provide concrete
|
||||
implementations for the interfaces that it uses, and provide
|
||||
a name for the resulting module. This is done as follows:</p>
|
||||
@ -622,7 +621,7 @@ use <code class="docutils literal notranslate"><span class="pre">submodule</span
|
||||
</div>
|
||||
</section>
|
||||
<section id="anonymous-interface-modules">
|
||||
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this heading"></a></h3>
|
||||
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this headline"></a></h3>
|
||||
<p>If we need to just parameterize a module by a couple of types/values,
|
||||
it is quite cumbersome to have to define a whole separate interface module.
|
||||
To make this more convenient we provide the following notation for defining
|
||||
@ -646,7 +645,7 @@ Note that the parameters may not use things defined in <code class="docutils lit
|
||||
the interface is declared outside of <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
|
||||
</section>
|
||||
<section id="anonymous-instantiation-arguments">
|
||||
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this heading"></a></h3>
|
||||
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this headline"></a></h3>
|
||||
<p>Sometimes it is also a bit cumbersome to have to define a whole
|
||||
separate module just to pass it as an argument to some parameterized
|
||||
module. To make this more convenient we support the following notion
|
||||
@ -678,7 +677,7 @@ definition of an anonymous module which is passed as the argument
|
||||
to parameterized module <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
|
||||
</section>
|
||||
<section id="anonymous-import-instantiations">
|
||||
<h3>Anonymous Import Instantiations<a class="headerlink" href="#anonymous-import-instantiations" title="Permalink to this heading"></a></h3>
|
||||
<h3>Anonymous Import Instantiations<a class="headerlink" href="#anonymous-import-instantiations" title="Permalink to this headline"></a></h3>
|
||||
<p>We provide syntactic sugar for importing and instantiating a functor
|
||||
at the same time:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">submodule</span><span class="w"> </span><span class="kt">F</span><span class="w"> </span><span class="kr">where</span><span class="w"></span>
|
||||
@ -729,7 +728,7 @@ to the following declarations:</p>
|
||||
</div>
|
||||
</section>
|
||||
<section id="passing-through-module-parameters">
|
||||
<h3>Passing Through Module Parameters<a class="headerlink" href="#passing-through-module-parameters" title="Permalink to this heading"></a></h3>
|
||||
<h3>Passing Through Module Parameters<a class="headerlink" href="#passing-through-module-parameters" title="Permalink to this headline"></a></h3>
|
||||
<p>Occasionally it is useful to define a functor that instantiates <em>another</em>
|
||||
functor using the same parameters as the functor being defined
|
||||
(i.e., a functor parameter is passed on to another functor). This can
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -85,9 +84,9 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="overloaded-operations">
|
||||
<h1>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this heading"></a></h1>
|
||||
<h1>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this headline"></a></h1>
|
||||
<section id="equality">
|
||||
<h2>Equality<a class="headerlink" href="#equality" title="Permalink to this heading"></a></h2>
|
||||
<h2>Equality<a class="headerlink" href="#equality" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Eq</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">==</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Eq</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">!=</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Eq</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
@ -97,7 +96,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="comparisons">
|
||||
<h2>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this heading"></a></h2>
|
||||
<h2>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">Cmp</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o"><</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">Cmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">></span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">Cmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
@ -110,7 +109,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="signed-comparisons">
|
||||
<h2>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this heading"></a></h2>
|
||||
<h2>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">SignedCmp</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o"><$</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">SignedCmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">>$</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">SignedCmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
|
||||
@ -120,14 +119,14 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="zero">
|
||||
<h2>Zero<a class="headerlink" href="#zero" title="Permalink to this heading"></a></h2>
|
||||
<h2>Zero<a class="headerlink" href="#zero" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Zero</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Zero</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</section>
|
||||
<section id="logical-operations">
|
||||
<h2>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this heading"></a></h2>
|
||||
<h2>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Logic</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">&&</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Logic</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">||</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Logic</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
@ -137,7 +136,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="basic-arithmetic">
|
||||
<h2>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this heading"></a></h2>
|
||||
<h2>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Ring</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="n">fromInteger</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Ring</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="kt">Integer</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">+</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Ring</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
@ -149,7 +148,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="integral-operations">
|
||||
<h2>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this heading"></a></h2>
|
||||
<h2>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Integral</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">/</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Integral</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">%</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Integral</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
@ -161,7 +160,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="division">
|
||||
<h2>Division<a class="headerlink" href="#division" title="Permalink to this heading"></a></h2>
|
||||
<h2>Division<a class="headerlink" href="#division" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Field</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="n">recip</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Field</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="p">(</span><span class="o">/.</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Field</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="n">a</span><span class="w"></span>
|
||||
@ -169,7 +168,7 @@
|
||||
</div>
|
||||
</section>
|
||||
<section id="rounding">
|
||||
<h2>Rounding<a class="headerlink" href="#rounding" title="Permalink to this heading"></a></h2>
|
||||
<h2>Rounding<a class="headerlink" href="#rounding" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Round</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="n">ceiling</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Round</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="n">floor</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Round</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -73,13 +72,14 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="cryptol-reference-manual">
|
||||
<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this heading"></a></h1>
|
||||
<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this headline"></a></h1>
|
||||
<div class="toctree-wrapper compound">
|
||||
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
|
||||
<ul>
|
||||
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a><ul>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#declarations">Declarations</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#type-signatures">Type Signatures</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#numeric-constraint-guards">Numeric Constraint Guards</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#layout">Layout</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#comments">Comments</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#identifiers">Identifiers</a></li>
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
@ -78,9 +77,9 @@
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="type-declarations">
|
||||
<h1>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this heading"></a></h1>
|
||||
<h1>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this headline"></a></h1>
|
||||
<section id="type-synonyms">
|
||||
<h2>Type Synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this heading"></a></h2>
|
||||
<h2>Type Synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">type</span><span class="w"> </span><span class="kt">T</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="w"> </span><span class="n">b</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
@ -93,7 +92,7 @@ Type synonyms may mention other synonyms, but it is not
|
||||
allowed to create a recursive collection of type synonyms.</p>
|
||||
</section>
|
||||
<section id="newtypes">
|
||||
<h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this heading"></a></h2>
|
||||
<h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this headline"></a></h2>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">newtype</span><span class="w"> </span><span class="kt">NewT</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="nb">seq</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="n">b</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
|
||||
@ -19,6 +19,54 @@ Type Signatures
|
||||
f,g : {a,b} (fin a) => [a] b
|
||||
|
||||
|
||||
Numeric Constraint Guards
|
||||
-------------------------
|
||||
|
||||
A declaration with a signature can use *numeric constraint guards*,
|
||||
which are used to change the behavior of a functoin depending on its
|
||||
numeric type parameters. For example:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
len : {n} (fin n) => [n]a -> Integer
|
||||
len xs | n == 0 => 0
|
||||
| n > 0 => 1 + len (drop `{1} xs)
|
||||
|
||||
Each behavior starts with ``|`` and lists some constraints on the numeric
|
||||
parameters to a declaration. When applied, the function will use the first
|
||||
definition that satisfies the provided numeric parameters.
|
||||
|
||||
Numeric constraint guards are quite similar to an ``if`` expression,
|
||||
except that decisions are based on *types* rather than values. There
|
||||
is also an important difference to simply using demotion and an
|
||||
actual ``if`` statement:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
len' : {n} (fin n) => [n]a -> Integer
|
||||
len' xs = if `n == 0 => 0
|
||||
| `n > 0 => 1 + len (drop `{1} xs)
|
||||
|
||||
The definition of ``len'`` is rejected, because the *value based* ``if``
|
||||
expression does provide the *type based* fact ``n >= 1`` which is
|
||||
required by ``drop `{1} xs``, while in ``len``, the type-checker
|
||||
locally-assumes the constraint ``n > 0`` in that constraint-guarded branch
|
||||
and so it can in fact determine that ``n >= 1``.
|
||||
|
||||
Requirements:
|
||||
- Numeric constraint guards only support constraints over numeric literals,
|
||||
such as ``fin``, ``<=``, ``==``, etc.
|
||||
Type constraint aliases can also be used as long as they only constrain
|
||||
numeric literals.
|
||||
- The numeric constraint guards of a declaration should be exhaustive. The
|
||||
type-checker will attempt to prove that the set of constraint guards is
|
||||
exhaustive, but if it can't then it will issue a non-exhaustive constraint
|
||||
guards warning. This warning is controlled by the environmental option
|
||||
``warnNonExhaustiveConstraintGuards``.
|
||||
- Each constraint guard is checked *independently* of the others, and there
|
||||
are no implict assumptions that the previous behaviors do not match---
|
||||
instead the programmer needs to specify all constraints explicitly
|
||||
in the guard.
|
||||
|
||||
Layout
|
||||
------
|
||||
|
||||
@ -4,7 +4,7 @@
|
||||
*
|
||||
* Sphinx stylesheet -- basic theme.
|
||||
*
|
||||
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
|
||||
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
|
||||
* :license: BSD, see LICENSE for details.
|
||||
*
|
||||
*/
|
||||
@ -222,7 +222,7 @@ table.modindextable td {
|
||||
/* -- general body styles --------------------------------------------------- */
|
||||
|
||||
div.body {
|
||||
min-width: 360px;
|
||||
min-width: 450px;
|
||||
max-width: 800px;
|
||||
}
|
||||
|
||||
@ -236,6 +236,7 @@ div.body p, div.body dd, div.body li, div.body blockquote {
|
||||
a.headerlink {
|
||||
visibility: hidden;
|
||||
}
|
||||
|
||||
a.brackets:before,
|
||||
span.brackets > a:before{
|
||||
content: "[";
|
||||
@ -246,7 +247,6 @@ span.brackets > a:after {
|
||||
content: "]";
|
||||
}
|
||||
|
||||
|
||||
h1:hover > a.headerlink,
|
||||
h2:hover > a.headerlink,
|
||||
h3:hover > a.headerlink,
|
||||
@ -334,11 +334,13 @@ aside.sidebar {
|
||||
p.sidebar-title {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
div.admonition, div.topic, blockquote {
|
||||
clear: left;
|
||||
}
|
||||
|
||||
/* -- topics ---------------------------------------------------------------- */
|
||||
|
||||
div.topic {
|
||||
border: 1px solid #ccc;
|
||||
padding: 7px;
|
||||
@ -426,6 +428,10 @@ table.docutils td, table.docutils th {
|
||||
border-bottom: 1px solid #aaa;
|
||||
}
|
||||
|
||||
table.footnote td, table.footnote th {
|
||||
border: 0 !important;
|
||||
}
|
||||
|
||||
th {
|
||||
text-align: left;
|
||||
padding-right: 5px;
|
||||
@ -608,6 +614,7 @@ ol.simple p,
|
||||
ul.simple p {
|
||||
margin-bottom: 0;
|
||||
}
|
||||
|
||||
dl.footnote > dt,
|
||||
dl.citation > dt {
|
||||
float: left;
|
||||
@ -636,11 +643,11 @@ dl.field-list > dt {
|
||||
padding-left: 0.5em;
|
||||
padding-right: 5px;
|
||||
}
|
||||
|
||||
dl.field-list > dt:after {
|
||||
content: ":";
|
||||
}
|
||||
|
||||
|
||||
dl.field-list > dd {
|
||||
padding-left: 0.5em;
|
||||
margin-top: 0em;
|
||||
@ -750,7 +757,6 @@ span.pre {
|
||||
-ms-hyphens: none;
|
||||
-webkit-hyphens: none;
|
||||
hyphens: none;
|
||||
white-space: nowrap;
|
||||
}
|
||||
|
||||
div[class*="highlight-"] {
|
||||
|
||||
@ -2,263 +2,322 @@
|
||||
* doctools.js
|
||||
* ~~~~~~~~~~~
|
||||
*
|
||||
* Base JavaScript utilities for all Sphinx HTML documentation.
|
||||
* Sphinx JavaScript utilities for all documentation.
|
||||
*
|
||||
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
|
||||
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
|
||||
* :license: BSD, see LICENSE for details.
|
||||
*
|
||||
*/
|
||||
"use strict";
|
||||
|
||||
const _ready = (callback) => {
|
||||
if (document.readyState !== "loading") {
|
||||
callback();
|
||||
} else {
|
||||
document.addEventListener("DOMContentLoaded", callback);
|
||||
/**
|
||||
* select a different prefix for underscore
|
||||
*/
|
||||
$u = _.noConflict();
|
||||
|
||||
/**
|
||||
* make the code below compatible with browsers without
|
||||
* an installed firebug like debugger
|
||||
if (!window.console || !console.firebug) {
|
||||
var names = ["log", "debug", "info", "warn", "error", "assert", "dir",
|
||||
"dirxml", "group", "groupEnd", "time", "timeEnd", "count", "trace",
|
||||
"profile", "profileEnd"];
|
||||
window.console = {};
|
||||
for (var i = 0; i < names.length; ++i)
|
||||
window.console[names[i]] = function() {};
|
||||
}
|
||||
*/
|
||||
|
||||
/**
|
||||
* small helper function to urldecode strings
|
||||
*
|
||||
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
|
||||
*/
|
||||
jQuery.urldecode = function(x) {
|
||||
if (!x) {
|
||||
return x
|
||||
}
|
||||
return decodeURIComponent(x.replace(/\+/g, ' '));
|
||||
};
|
||||
|
||||
/**
|
||||
* highlight a given string on a node by wrapping it in
|
||||
* small helper function to urlencode strings
|
||||
*/
|
||||
jQuery.urlencode = encodeURIComponent;
|
||||
|
||||
/**
|
||||
* This function returns the parsed url parameters of the
|
||||
* current request. Multiple values per key are supported,
|
||||
* it will always return arrays of strings for the value parts.
|
||||
*/
|
||||
jQuery.getQueryParameters = function(s) {
|
||||
if (typeof s === 'undefined')
|
||||
s = document.location.search;
|
||||
var parts = s.substr(s.indexOf('?') + 1).split('&');
|
||||
var result = {};
|
||||
for (var i = 0; i < parts.length; i++) {
|
||||
var tmp = parts[i].split('=', 2);
|
||||
var key = jQuery.urldecode(tmp[0]);
|
||||
var value = jQuery.urldecode(tmp[1]);
|
||||
if (key in result)
|
||||
result[key].push(value);
|
||||
else
|
||||
result[key] = [value];
|
||||
}
|
||||
return result;
|
||||
};
|
||||
|
||||
/**
|
||||
* highlight a given string on a jquery object by wrapping it in
|
||||
* span elements with the given class name.
|
||||
*/
|
||||
const _highlight = (node, addItems, text, className) => {
|
||||
if (node.nodeType === Node.TEXT_NODE) {
|
||||
const val = node.nodeValue;
|
||||
const parent = node.parentNode;
|
||||
const pos = val.toLowerCase().indexOf(text);
|
||||
if (
|
||||
pos >= 0 &&
|
||||
!parent.classList.contains(className) &&
|
||||
!parent.classList.contains("nohighlight")
|
||||
) {
|
||||
let span;
|
||||
|
||||
const closestNode = parent.closest("body, svg, foreignObject");
|
||||
const isInSVG = closestNode && closestNode.matches("svg");
|
||||
if (isInSVG) {
|
||||
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
|
||||
} else {
|
||||
span = document.createElement("span");
|
||||
span.classList.add(className);
|
||||
}
|
||||
|
||||
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
|
||||
parent.insertBefore(
|
||||
span,
|
||||
parent.insertBefore(
|
||||
jQuery.fn.highlightText = function(text, className) {
|
||||
function highlight(node, addItems) {
|
||||
if (node.nodeType === 3) {
|
||||
var val = node.nodeValue;
|
||||
var pos = val.toLowerCase().indexOf(text);
|
||||
if (pos >= 0 &&
|
||||
!jQuery(node.parentNode).hasClass(className) &&
|
||||
!jQuery(node.parentNode).hasClass("nohighlight")) {
|
||||
var span;
|
||||
var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
|
||||
if (isInSVG) {
|
||||
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
|
||||
} else {
|
||||
span = document.createElement("span");
|
||||
span.className = className;
|
||||
}
|
||||
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
|
||||
node.parentNode.insertBefore(span, node.parentNode.insertBefore(
|
||||
document.createTextNode(val.substr(pos + text.length)),
|
||||
node.nextSibling
|
||||
)
|
||||
);
|
||||
node.nodeValue = val.substr(0, pos);
|
||||
|
||||
if (isInSVG) {
|
||||
const rect = document.createElementNS(
|
||||
"http://www.w3.org/2000/svg",
|
||||
"rect"
|
||||
);
|
||||
const bbox = parent.getBBox();
|
||||
rect.x.baseVal.value = bbox.x;
|
||||
rect.y.baseVal.value = bbox.y;
|
||||
rect.width.baseVal.value = bbox.width;
|
||||
rect.height.baseVal.value = bbox.height;
|
||||
rect.setAttribute("class", className);
|
||||
addItems.push({ parent: parent, target: rect });
|
||||
node.nextSibling));
|
||||
node.nodeValue = val.substr(0, pos);
|
||||
if (isInSVG) {
|
||||
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
|
||||
var bbox = node.parentElement.getBBox();
|
||||
rect.x.baseVal.value = bbox.x;
|
||||
rect.y.baseVal.value = bbox.y;
|
||||
rect.width.baseVal.value = bbox.width;
|
||||
rect.height.baseVal.value = bbox.height;
|
||||
rect.setAttribute('class', className);
|
||||
addItems.push({
|
||||
"parent": node.parentNode,
|
||||
"target": rect});
|
||||
}
|
||||
}
|
||||
}
|
||||
} else if (node.matches && !node.matches("button, select, textarea")) {
|
||||
node.childNodes.forEach((el) => _highlight(el, addItems, text, className));
|
||||
else if (!jQuery(node).is("button, select, textarea")) {
|
||||
jQuery.each(node.childNodes, function() {
|
||||
highlight(this, addItems);
|
||||
});
|
||||
}
|
||||
}
|
||||
var addItems = [];
|
||||
var result = this.each(function() {
|
||||
highlight(this, addItems);
|
||||
});
|
||||
for (var i = 0; i < addItems.length; ++i) {
|
||||
jQuery(addItems[i].parent).before(addItems[i].target);
|
||||
}
|
||||
return result;
|
||||
};
|
||||
const _highlightText = (thisNode, text, className) => {
|
||||
let addItems = [];
|
||||
_highlight(thisNode, addItems, text, className);
|
||||
addItems.forEach((obj) =>
|
||||
obj.parent.insertAdjacentElement("beforebegin", obj.target)
|
||||
);
|
||||
};
|
||||
|
||||
/*
|
||||
* backward compatibility for jQuery.browser
|
||||
* This will be supported until firefox bug is fixed.
|
||||
*/
|
||||
if (!jQuery.browser) {
|
||||
jQuery.uaMatch = function(ua) {
|
||||
ua = ua.toLowerCase();
|
||||
|
||||
var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
|
||||
/(webkit)[ \/]([\w.]+)/.exec(ua) ||
|
||||
/(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
|
||||
/(msie) ([\w.]+)/.exec(ua) ||
|
||||
ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
|
||||
[];
|
||||
|
||||
return {
|
||||
browser: match[ 1 ] || "",
|
||||
version: match[ 2 ] || "0"
|
||||
};
|
||||
};
|
||||
jQuery.browser = {};
|
||||
jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
|
||||
}
|
||||
|
||||
/**
|
||||
* Small JavaScript module for the documentation.
|
||||
*/
|
||||
const Documentation = {
|
||||
init: () => {
|
||||
Documentation.highlightSearchWords();
|
||||
Documentation.initDomainIndexTable();
|
||||
Documentation.initOnKeyListeners();
|
||||
var Documentation = {
|
||||
|
||||
init : function() {
|
||||
this.fixFirefoxAnchorBug();
|
||||
this.highlightSearchWords();
|
||||
this.initIndexTable();
|
||||
if (DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) {
|
||||
this.initOnKeyListeners();
|
||||
}
|
||||
},
|
||||
|
||||
/**
|
||||
* i18n support
|
||||
*/
|
||||
TRANSLATIONS: {},
|
||||
PLURAL_EXPR: (n) => (n === 1 ? 0 : 1),
|
||||
LOCALE: "unknown",
|
||||
TRANSLATIONS : {},
|
||||
PLURAL_EXPR : function(n) { return n === 1 ? 0 : 1; },
|
||||
LOCALE : 'unknown',
|
||||
|
||||
// gettext and ngettext don't access this so that the functions
|
||||
// can safely bound to a different name (_ = Documentation.gettext)
|
||||
gettext: (string) => {
|
||||
const translated = Documentation.TRANSLATIONS[string];
|
||||
switch (typeof translated) {
|
||||
case "undefined":
|
||||
return string; // no translation
|
||||
case "string":
|
||||
return translated; // translation exists
|
||||
default:
|
||||
return translated[0]; // (singular, plural) translation tuple exists
|
||||
}
|
||||
gettext : function(string) {
|
||||
var translated = Documentation.TRANSLATIONS[string];
|
||||
if (typeof translated === 'undefined')
|
||||
return string;
|
||||
return (typeof translated === 'string') ? translated : translated[0];
|
||||
},
|
||||
|
||||
ngettext: (singular, plural, n) => {
|
||||
const translated = Documentation.TRANSLATIONS[singular];
|
||||
if (typeof translated !== "undefined")
|
||||
return translated[Documentation.PLURAL_EXPR(n)];
|
||||
return n === 1 ? singular : plural;
|
||||
ngettext : function(singular, plural, n) {
|
||||
var translated = Documentation.TRANSLATIONS[singular];
|
||||
if (typeof translated === 'undefined')
|
||||
return (n == 1) ? singular : plural;
|
||||
return translated[Documentation.PLURALEXPR(n)];
|
||||
},
|
||||
|
||||
addTranslations: (catalog) => {
|
||||
Object.assign(Documentation.TRANSLATIONS, catalog.messages);
|
||||
Documentation.PLURAL_EXPR = new Function(
|
||||
"n",
|
||||
`return (${catalog.plural_expr})`
|
||||
);
|
||||
Documentation.LOCALE = catalog.locale;
|
||||
addTranslations : function(catalog) {
|
||||
for (var key in catalog.messages)
|
||||
this.TRANSLATIONS[key] = catalog.messages[key];
|
||||
this.PLURAL_EXPR = new Function('n', 'return +(' + catalog.plural_expr + ')');
|
||||
this.LOCALE = catalog.locale;
|
||||
},
|
||||
|
||||
/**
|
||||
* add context elements like header anchor links
|
||||
*/
|
||||
addContextElements : function() {
|
||||
$('div[id] > :header:first').each(function() {
|
||||
$('<a class="headerlink">\u00B6</a>').
|
||||
attr('href', '#' + this.id).
|
||||
attr('title', _('Permalink to this headline')).
|
||||
appendTo(this);
|
||||
});
|
||||
$('dt[id]').each(function() {
|
||||
$('<a class="headerlink">\u00B6</a>').
|
||||
attr('href', '#' + this.id).
|
||||
attr('title', _('Permalink to this definition')).
|
||||
appendTo(this);
|
||||
});
|
||||
},
|
||||
|
||||
/**
|
||||
* workaround a firefox stupidity
|
||||
* see: https://bugzilla.mozilla.org/show_bug.cgi?id=645075
|
||||
*/
|
||||
fixFirefoxAnchorBug : function() {
|
||||
if (document.location.hash && $.browser.mozilla)
|
||||
window.setTimeout(function() {
|
||||
document.location.href += '';
|
||||
}, 10);
|
||||
},
|
||||
|
||||
/**
|
||||
* highlight the search words provided in the url in the text
|
||||
*/
|
||||
highlightSearchWords: () => {
|
||||
const highlight =
|
||||
new URLSearchParams(window.location.search).get("highlight") || "";
|
||||
const terms = highlight.toLowerCase().split(/\s+/).filter(x => x);
|
||||
if (terms.length === 0) return; // nothing to do
|
||||
highlightSearchWords : function() {
|
||||
var params = $.getQueryParameters();
|
||||
var terms = (params.highlight) ? params.highlight[0].split(/\s+/) : [];
|
||||
if (terms.length) {
|
||||
var body = $('div.body');
|
||||
if (!body.length) {
|
||||
body = $('body');
|
||||
}
|
||||
window.setTimeout(function() {
|
||||
$.each(terms, function() {
|
||||
body.highlightText(this.toLowerCase(), 'highlighted');
|
||||
});
|
||||
}, 10);
|
||||
$('<p class="highlight-link"><a href="javascript:Documentation.' +
|
||||
'hideSearchWords()">' + _('Hide Search Matches') + '</a></p>')
|
||||
.appendTo($('#searchbox'));
|
||||
}
|
||||
},
|
||||
|
||||
// There should never be more than one element matching "div.body"
|
||||
const divBody = document.querySelectorAll("div.body");
|
||||
const body = divBody.length ? divBody[0] : document.querySelector("body");
|
||||
window.setTimeout(() => {
|
||||
terms.forEach((term) => _highlightText(body, term, "highlighted"));
|
||||
}, 10);
|
||||
|
||||
const searchBox = document.getElementById("searchbox");
|
||||
if (searchBox === null) return;
|
||||
searchBox.appendChild(
|
||||
document
|
||||
.createRange()
|
||||
.createContextualFragment(
|
||||
'<p class="highlight-link">' +
|
||||
'<a href="javascript:Documentation.hideSearchWords()">' +
|
||||
Documentation.gettext("Hide Search Matches") +
|
||||
"</a></p>"
|
||||
)
|
||||
);
|
||||
/**
|
||||
* init the domain index toggle buttons
|
||||
*/
|
||||
initIndexTable : function() {
|
||||
var togglers = $('img.toggler').click(function() {
|
||||
var src = $(this).attr('src');
|
||||
var idnum = $(this).attr('id').substr(7);
|
||||
$('tr.cg-' + idnum).toggle();
|
||||
if (src.substr(-9) === 'minus.png')
|
||||
$(this).attr('src', src.substr(0, src.length-9) + 'plus.png');
|
||||
else
|
||||
$(this).attr('src', src.substr(0, src.length-8) + 'minus.png');
|
||||
}).css('display', '');
|
||||
if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) {
|
||||
togglers.click();
|
||||
}
|
||||
},
|
||||
|
||||
/**
|
||||
* helper function to hide the search marks again
|
||||
*/
|
||||
hideSearchWords: () => {
|
||||
document
|
||||
.querySelectorAll("#searchbox .highlight-link")
|
||||
.forEach((el) => el.remove());
|
||||
document
|
||||
.querySelectorAll("span.highlighted")
|
||||
.forEach((el) => el.classList.remove("highlighted"));
|
||||
const url = new URL(window.location);
|
||||
url.searchParams.delete("highlight");
|
||||
window.history.replaceState({}, "", url);
|
||||
hideSearchWords : function() {
|
||||
$('#searchbox .highlight-link').fadeOut(300);
|
||||
$('span.highlighted').removeClass('highlighted');
|
||||
},
|
||||
|
||||
/**
|
||||
* helper function to focus on search bar
|
||||
* make the url absolute
|
||||
*/
|
||||
focusSearchBar: () => {
|
||||
document.querySelectorAll("input[name=q]")[0]?.focus();
|
||||
makeURL : function(relativeURL) {
|
||||
return DOCUMENTATION_OPTIONS.URL_ROOT + '/' + relativeURL;
|
||||
},
|
||||
|
||||
/**
|
||||
* Initialise the domain index toggle buttons
|
||||
* get the current relative url
|
||||
*/
|
||||
initDomainIndexTable: () => {
|
||||
const toggler = (el) => {
|
||||
const idNumber = el.id.substr(7);
|
||||
const toggledRows = document.querySelectorAll(`tr.cg-${idNumber}`);
|
||||
if (el.src.substr(-9) === "minus.png") {
|
||||
el.src = `${el.src.substr(0, el.src.length - 9)}plus.png`;
|
||||
toggledRows.forEach((el) => (el.style.display = "none"));
|
||||
} else {
|
||||
el.src = `${el.src.substr(0, el.src.length - 8)}minus.png`;
|
||||
toggledRows.forEach((el) => (el.style.display = ""));
|
||||
}
|
||||
};
|
||||
|
||||
const togglerElements = document.querySelectorAll("img.toggler");
|
||||
togglerElements.forEach((el) =>
|
||||
el.addEventListener("click", (event) => toggler(event.currentTarget))
|
||||
);
|
||||
togglerElements.forEach((el) => (el.style.display = ""));
|
||||
if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) togglerElements.forEach(toggler);
|
||||
getCurrentURL : function() {
|
||||
var path = document.location.pathname;
|
||||
var parts = path.split(/\//);
|
||||
$.each(DOCUMENTATION_OPTIONS.URL_ROOT.split(/\//), function() {
|
||||
if (this === '..')
|
||||
parts.pop();
|
||||
});
|
||||
var url = parts.join('/');
|
||||
return path.substring(url.lastIndexOf('/') + 1, path.length - 1);
|
||||
},
|
||||
|
||||
initOnKeyListeners: () => {
|
||||
// only install a listener if it is really needed
|
||||
if (
|
||||
!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS &&
|
||||
!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS
|
||||
)
|
||||
return;
|
||||
|
||||
const blacklistedElements = new Set([
|
||||
"TEXTAREA",
|
||||
"INPUT",
|
||||
"SELECT",
|
||||
"BUTTON",
|
||||
]);
|
||||
document.addEventListener("keydown", (event) => {
|
||||
if (blacklistedElements.has(document.activeElement.tagName)) return; // bail for input elements
|
||||
if (event.altKey || event.ctrlKey || event.metaKey) return; // bail with special keys
|
||||
|
||||
if (!event.shiftKey) {
|
||||
switch (event.key) {
|
||||
case "ArrowLeft":
|
||||
if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break;
|
||||
|
||||
const prevLink = document.querySelector('link[rel="prev"]');
|
||||
if (prevLink && prevLink.href) {
|
||||
window.location.href = prevLink.href;
|
||||
event.preventDefault();
|
||||
initOnKeyListeners: function() {
|
||||
$(document).keydown(function(event) {
|
||||
var activeElementType = document.activeElement.tagName;
|
||||
// don't navigate when in search box, textarea, dropdown or button
|
||||
if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT'
|
||||
&& activeElementType !== 'BUTTON' && !event.altKey && !event.ctrlKey && !event.metaKey
|
||||
&& !event.shiftKey) {
|
||||
switch (event.keyCode) {
|
||||
case 37: // left
|
||||
var prevHref = $('link[rel="prev"]').prop('href');
|
||||
if (prevHref) {
|
||||
window.location.href = prevHref;
|
||||
return false;
|
||||
}
|
||||
break;
|
||||
case "ArrowRight":
|
||||
if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break;
|
||||
|
||||
const nextLink = document.querySelector('link[rel="next"]');
|
||||
if (nextLink && nextLink.href) {
|
||||
window.location.href = nextLink.href;
|
||||
event.preventDefault();
|
||||
case 39: // right
|
||||
var nextHref = $('link[rel="next"]').prop('href');
|
||||
if (nextHref) {
|
||||
window.location.href = nextHref;
|
||||
return false;
|
||||
}
|
||||
break;
|
||||
case "Escape":
|
||||
if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break;
|
||||
Documentation.hideSearchWords();
|
||||
event.preventDefault();
|
||||
}
|
||||
}
|
||||
|
||||
// some keyboard layouts may need Shift to get /
|
||||
switch (event.key) {
|
||||
case "/":
|
||||
if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break;
|
||||
Documentation.focusSearchBar();
|
||||
event.preventDefault();
|
||||
}
|
||||
});
|
||||
},
|
||||
}
|
||||
};
|
||||
|
||||
// quick alias for translations
|
||||
const _ = Documentation.gettext;
|
||||
_ = Documentation.gettext;
|
||||
|
||||
_ready(Documentation.init);
|
||||
$(document).ready(function() {
|
||||
Documentation.init();
|
||||
});
|
||||
|
||||
@ -1,14 +1,12 @@
|
||||
var DOCUMENTATION_OPTIONS = {
|
||||
URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'),
|
||||
VERSION: '2.11.0',
|
||||
LANGUAGE: 'en',
|
||||
LANGUAGE: 'None',
|
||||
COLLAPSE_INDEX: false,
|
||||
BUILDER: 'html',
|
||||
FILE_SUFFIX: '.html',
|
||||
LINK_SUFFIX: '.html',
|
||||
HAS_SOURCE: true,
|
||||
SOURCELINK_SUFFIX: '.txt',
|
||||
NAVIGATION_WITH_KEYS: false,
|
||||
SHOW_SEARCH_SUMMARY: true,
|
||||
ENABLE_SEARCH_SHORTCUTS: true,
|
||||
NAVIGATION_WITH_KEYS: false
|
||||
};
|
||||
10881
docs/RefMan/_build/html/_static/jquery.js
vendored
10881
docs/RefMan/_build/html/_static/jquery.js
vendored
File diff suppressed because one or more lines are too long
@ -5,12 +5,12 @@
|
||||
* This script contains the language-specific data used by searchtools.js,
|
||||
* namely the list of stopwords, stemmer, scorer and splitter.
|
||||
*
|
||||
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
|
||||
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
|
||||
* :license: BSD, see LICENSE for details.
|
||||
*
|
||||
*/
|
||||
|
||||
var stopwords = ["a", "and", "are", "as", "at", "be", "but", "by", "for", "if", "in", "into", "is", "it", "near", "no", "not", "of", "on", "or", "such", "that", "the", "their", "then", "there", "these", "they", "this", "to", "was", "will", "with"];
|
||||
var stopwords = ["a","and","are","as","at","be","but","by","for","if","in","into","is","it","near","no","not","of","on","or","such","that","the","their","then","there","these","they","this","to","was","will","with"];
|
||||
|
||||
|
||||
/* Non-minified version is copied as a separate JS file, is available */
|
||||
@ -197,3 +197,101 @@ var Stemmer = function() {
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
var splitChars = (function() {
|
||||
var result = {};
|
||||
var singles = [96, 180, 187, 191, 215, 247, 749, 885, 903, 907, 909, 930, 1014, 1648,
|
||||
1748, 1809, 2416, 2473, 2481, 2526, 2601, 2609, 2612, 2615, 2653, 2702,
|
||||
2706, 2729, 2737, 2740, 2857, 2865, 2868, 2910, 2928, 2948, 2961, 2971,
|
||||
2973, 3085, 3089, 3113, 3124, 3213, 3217, 3241, 3252, 3295, 3341, 3345,
|
||||
3369, 3506, 3516, 3633, 3715, 3721, 3736, 3744, 3748, 3750, 3756, 3761,
|
||||
3781, 3912, 4239, 4347, 4681, 4695, 4697, 4745, 4785, 4799, 4801, 4823,
|
||||
4881, 5760, 5901, 5997, 6313, 7405, 8024, 8026, 8028, 8030, 8117, 8125,
|
||||
8133, 8181, 8468, 8485, 8487, 8489, 8494, 8527, 11311, 11359, 11687, 11695,
|
||||
11703, 11711, 11719, 11727, 11735, 12448, 12539, 43010, 43014, 43019, 43587,
|
||||
43696, 43713, 64286, 64297, 64311, 64317, 64319, 64322, 64325, 65141];
|
||||
var i, j, start, end;
|
||||
for (i = 0; i < singles.length; i++) {
|
||||
result[singles[i]] = true;
|
||||
}
|
||||
var ranges = [[0, 47], [58, 64], [91, 94], [123, 169], [171, 177], [182, 184], [706, 709],
|
||||
[722, 735], [741, 747], [751, 879], [888, 889], [894, 901], [1154, 1161],
|
||||
[1318, 1328], [1367, 1368], [1370, 1376], [1416, 1487], [1515, 1519], [1523, 1568],
|
||||
[1611, 1631], [1642, 1645], [1750, 1764], [1767, 1773], [1789, 1790], [1792, 1807],
|
||||
[1840, 1868], [1958, 1968], [1970, 1983], [2027, 2035], [2038, 2041], [2043, 2047],
|
||||
[2070, 2073], [2075, 2083], [2085, 2087], [2089, 2307], [2362, 2364], [2366, 2383],
|
||||
[2385, 2391], [2402, 2405], [2419, 2424], [2432, 2436], [2445, 2446], [2449, 2450],
|
||||
[2483, 2485], [2490, 2492], [2494, 2509], [2511, 2523], [2530, 2533], [2546, 2547],
|
||||
[2554, 2564], [2571, 2574], [2577, 2578], [2618, 2648], [2655, 2661], [2672, 2673],
|
||||
[2677, 2692], [2746, 2748], [2750, 2767], [2769, 2783], [2786, 2789], [2800, 2820],
|
||||
[2829, 2830], [2833, 2834], [2874, 2876], [2878, 2907], [2914, 2917], [2930, 2946],
|
||||
[2955, 2957], [2966, 2968], [2976, 2978], [2981, 2983], [2987, 2989], [3002, 3023],
|
||||
[3025, 3045], [3059, 3076], [3130, 3132], [3134, 3159], [3162, 3167], [3170, 3173],
|
||||
[3184, 3191], [3199, 3204], [3258, 3260], [3262, 3293], [3298, 3301], [3312, 3332],
|
||||
[3386, 3388], [3390, 3423], [3426, 3429], [3446, 3449], [3456, 3460], [3479, 3481],
|
||||
[3518, 3519], [3527, 3584], [3636, 3647], [3655, 3663], [3674, 3712], [3717, 3718],
|
||||
[3723, 3724], [3726, 3731], [3752, 3753], [3764, 3772], [3774, 3775], [3783, 3791],
|
||||
[3802, 3803], [3806, 3839], [3841, 3871], [3892, 3903], [3949, 3975], [3980, 4095],
|
||||
[4139, 4158], [4170, 4175], [4182, 4185], [4190, 4192], [4194, 4196], [4199, 4205],
|
||||
[4209, 4212], [4226, 4237], [4250, 4255], [4294, 4303], [4349, 4351], [4686, 4687],
|
||||
[4702, 4703], [4750, 4751], [4790, 4791], [4806, 4807], [4886, 4887], [4955, 4968],
|
||||
[4989, 4991], [5008, 5023], [5109, 5120], [5741, 5742], [5787, 5791], [5867, 5869],
|
||||
[5873, 5887], [5906, 5919], [5938, 5951], [5970, 5983], [6001, 6015], [6068, 6102],
|
||||
[6104, 6107], [6109, 6111], [6122, 6127], [6138, 6159], [6170, 6175], [6264, 6271],
|
||||
[6315, 6319], [6390, 6399], [6429, 6469], [6510, 6511], [6517, 6527], [6572, 6592],
|
||||
[6600, 6607], [6619, 6655], [6679, 6687], [6741, 6783], [6794, 6799], [6810, 6822],
|
||||
[6824, 6916], [6964, 6980], [6988, 6991], [7002, 7042], [7073, 7085], [7098, 7167],
|
||||
[7204, 7231], [7242, 7244], [7294, 7400], [7410, 7423], [7616, 7679], [7958, 7959],
|
||||
[7966, 7967], [8006, 8007], [8014, 8015], [8062, 8063], [8127, 8129], [8141, 8143],
|
||||
[8148, 8149], [8156, 8159], [8173, 8177], [8189, 8303], [8306, 8307], [8314, 8318],
|
||||
[8330, 8335], [8341, 8449], [8451, 8454], [8456, 8457], [8470, 8472], [8478, 8483],
|
||||
[8506, 8507], [8512, 8516], [8522, 8525], [8586, 9311], [9372, 9449], [9472, 10101],
|
||||
[10132, 11263], [11493, 11498], [11503, 11516], [11518, 11519], [11558, 11567],
|
||||
[11622, 11630], [11632, 11647], [11671, 11679], [11743, 11822], [11824, 12292],
|
||||
[12296, 12320], [12330, 12336], [12342, 12343], [12349, 12352], [12439, 12444],
|
||||
[12544, 12548], [12590, 12592], [12687, 12689], [12694, 12703], [12728, 12783],
|
||||
[12800, 12831], [12842, 12880], [12896, 12927], [12938, 12976], [12992, 13311],
|
||||
[19894, 19967], [40908, 40959], [42125, 42191], [42238, 42239], [42509, 42511],
|
||||
[42540, 42559], [42592, 42593], [42607, 42622], [42648, 42655], [42736, 42774],
|
||||
[42784, 42785], [42889, 42890], [42893, 43002], [43043, 43055], [43062, 43071],
|
||||
[43124, 43137], [43188, 43215], [43226, 43249], [43256, 43258], [43260, 43263],
|
||||
[43302, 43311], [43335, 43359], [43389, 43395], [43443, 43470], [43482, 43519],
|
||||
[43561, 43583], [43596, 43599], [43610, 43615], [43639, 43641], [43643, 43647],
|
||||
[43698, 43700], [43703, 43704], [43710, 43711], [43715, 43738], [43742, 43967],
|
||||
[44003, 44015], [44026, 44031], [55204, 55215], [55239, 55242], [55292, 55295],
|
||||
[57344, 63743], [64046, 64047], [64110, 64111], [64218, 64255], [64263, 64274],
|
||||
[64280, 64284], [64434, 64466], [64830, 64847], [64912, 64913], [64968, 65007],
|
||||
[65020, 65135], [65277, 65295], [65306, 65312], [65339, 65344], [65371, 65381],
|
||||
[65471, 65473], [65480, 65481], [65488, 65489], [65496, 65497]];
|
||||
for (i = 0; i < ranges.length; i++) {
|
||||
start = ranges[i][0];
|
||||
end = ranges[i][1];
|
||||
for (j = start; j <= end; j++) {
|
||||
result[j] = true;
|
||||
}
|
||||
}
|
||||
return result;
|
||||
})();
|
||||
|
||||
function splitQuery(query) {
|
||||
var result = [];
|
||||
var start = -1;
|
||||
for (var i = 0; i < query.length; i++) {
|
||||
if (splitChars[query.charCodeAt(i)]) {
|
||||
if (start !== -1) {
|
||||
result.push(query.slice(start, i));
|
||||
start = -1;
|
||||
}
|
||||
} else if (start === -1) {
|
||||
start = i;
|
||||
}
|
||||
}
|
||||
if (start !== -1) {
|
||||
result.push(query.slice(start));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -4,24 +4,22 @@
|
||||
*
|
||||
* Sphinx JavaScript utilities for the full-text search.
|
||||
*
|
||||
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
|
||||
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
|
||||
* :license: BSD, see LICENSE for details.
|
||||
*
|
||||
*/
|
||||
"use strict";
|
||||
|
||||
/**
|
||||
* Simple result scoring code.
|
||||
*/
|
||||
if (typeof Scorer === "undefined") {
|
||||
if (!Scorer) {
|
||||
/**
|
||||
* Simple result scoring code.
|
||||
*/
|
||||
var Scorer = {
|
||||
// Implement the following function to further tweak the score for each result
|
||||
// The function takes a result array [docname, title, anchor, descr, score, filename]
|
||||
// The function takes a result array [filename, title, anchor, descr, score]
|
||||
// and returns the new score.
|
||||
/*
|
||||
score: result => {
|
||||
const [docname, title, anchor, descr, score, filename] = result
|
||||
return score
|
||||
score: function(result) {
|
||||
return result[4];
|
||||
},
|
||||
*/
|
||||
|
||||
@ -30,11 +28,9 @@ if (typeof Scorer === "undefined") {
|
||||
// or matches in the last dotted part of the object name
|
||||
objPartialMatch: 6,
|
||||
// Additive scores depending on the priority of the object
|
||||
objPrio: {
|
||||
0: 15, // used to be importantResults
|
||||
1: 5, // used to be objectResults
|
||||
2: -5, // used to be unimportantResults
|
||||
},
|
||||
objPrio: {0: 15, // used to be importantResults
|
||||
1: 5, // used to be objectResults
|
||||
2: -5}, // used to be unimportantResults
|
||||
// Used when the priority is not in the mapping.
|
||||
objPrioDefault: 0,
|
||||
|
||||
@ -43,453 +39,459 @@ if (typeof Scorer === "undefined") {
|
||||
partialTitle: 7,
|
||||
// query found in terms
|
||||
term: 5,
|
||||
partialTerm: 2,
|
||||
partialTerm: 2
|
||||
};
|
||||
}
|
||||
|
||||
const _removeChildren = (element) => {
|
||||
while (element && element.lastChild) element.removeChild(element.lastChild);
|
||||
};
|
||||
|
||||
/**
|
||||
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions#escaping
|
||||
*/
|
||||
const _escapeRegExp = (string) =>
|
||||
string.replace(/[.*+\-?^${}()|[\]\\]/g, "\\$&"); // $& means the whole matched string
|
||||
|
||||
const _displayItem = (item, highlightTerms, searchTerms) => {
|
||||
const docBuilder = DOCUMENTATION_OPTIONS.BUILDER;
|
||||
const docUrlRoot = DOCUMENTATION_OPTIONS.URL_ROOT;
|
||||
const docFileSuffix = DOCUMENTATION_OPTIONS.FILE_SUFFIX;
|
||||
const docLinkSuffix = DOCUMENTATION_OPTIONS.LINK_SUFFIX;
|
||||
const showSearchSummary = DOCUMENTATION_OPTIONS.SHOW_SEARCH_SUMMARY;
|
||||
|
||||
const [docName, title, anchor, descr] = item;
|
||||
|
||||
let listItem = document.createElement("li");
|
||||
let requestUrl;
|
||||
let linkUrl;
|
||||
if (docBuilder === "dirhtml") {
|
||||
// dirhtml builder
|
||||
let dirname = docName + "/";
|
||||
if (dirname.match(/\/index\/$/))
|
||||
dirname = dirname.substring(0, dirname.length - 6);
|
||||
else if (dirname === "index/") dirname = "";
|
||||
requestUrl = docUrlRoot + dirname;
|
||||
linkUrl = requestUrl;
|
||||
} else {
|
||||
// normal html builders
|
||||
requestUrl = docUrlRoot + docName + docFileSuffix;
|
||||
linkUrl = docName + docLinkSuffix;
|
||||
if (!splitQuery) {
|
||||
function splitQuery(query) {
|
||||
return query.split(/\s+/);
|
||||
}
|
||||
const params = new URLSearchParams();
|
||||
params.set("highlight", [...highlightTerms].join(" "));
|
||||
let linkEl = listItem.appendChild(document.createElement("a"));
|
||||
linkEl.href = linkUrl + "?" + params.toString() + anchor;
|
||||
linkEl.innerHTML = title;
|
||||
if (descr)
|
||||
listItem.appendChild(document.createElement("span")).innerHTML =
|
||||
" (" + descr + ")";
|
||||
else if (showSearchSummary)
|
||||
fetch(requestUrl)
|
||||
.then((responseData) => responseData.text())
|
||||
.then((data) => {
|
||||
if (data)
|
||||
listItem.appendChild(
|
||||
Search.makeSearchSummary(data, searchTerms, highlightTerms)
|
||||
);
|
||||
});
|
||||
Search.output.appendChild(listItem);
|
||||
};
|
||||
const _finishSearch = (resultCount) => {
|
||||
Search.stopPulse();
|
||||
Search.title.innerText = _("Search Results");
|
||||
if (!resultCount)
|
||||
Search.status.innerText = Documentation.gettext(
|
||||
"Your search did not match any documents. Please make sure that all words are spelled correctly and that you've selected enough categories."
|
||||
);
|
||||
else
|
||||
Search.status.innerText = _(
|
||||
`Search finished, found ${resultCount} page(s) matching the search query.`
|
||||
);
|
||||
};
|
||||
const _displayNextItem = (
|
||||
results,
|
||||
resultCount,
|
||||
highlightTerms,
|
||||
searchTerms
|
||||
) => {
|
||||
// results left, load the summary and display it
|
||||
// this is intended to be dynamic (don't sub resultsCount)
|
||||
if (results.length) {
|
||||
_displayItem(results.pop(), highlightTerms, searchTerms);
|
||||
setTimeout(
|
||||
() => _displayNextItem(results, resultCount, highlightTerms, searchTerms),
|
||||
5
|
||||
);
|
||||
}
|
||||
// search finished, update title and status message
|
||||
else _finishSearch(resultCount);
|
||||
};
|
||||
|
||||
/**
|
||||
* Default splitQuery function. Can be overridden in ``sphinx.search`` with a
|
||||
* custom function per language.
|
||||
*
|
||||
* The regular expression works by splitting the string on consecutive characters
|
||||
* that are not Unicode letters, numbers, underscores, or emoji characters.
|
||||
* This is the same as ``\W+`` in Python, preserving the surrogate pair area.
|
||||
*/
|
||||
if (typeof splitQuery === "undefined") {
|
||||
var splitQuery = (query) => query
|
||||
.split(/[^\p{Letter}\p{Number}_\p{Emoji_Presentation}]+/gu)
|
||||
.filter(term => term) // remove remaining empty strings
|
||||
}
|
||||
|
||||
/**
|
||||
* Search Module
|
||||
*/
|
||||
const Search = {
|
||||
_index: null,
|
||||
_queued_query: null,
|
||||
_pulse_status: -1,
|
||||
var Search = {
|
||||
|
||||
htmlToText: (htmlString) => {
|
||||
const htmlElement = new DOMParser().parseFromString(htmlString, 'text/html');
|
||||
htmlElement.querySelectorAll(".headerlink").forEach((el) => { el.remove() });
|
||||
const docContent = htmlElement.querySelector('[role="main"]');
|
||||
if (docContent !== undefined) return docContent.textContent;
|
||||
console.warn(
|
||||
"Content block not found. Sphinx search tries to obtain it via '[role=main]'. Could you check your theme or template."
|
||||
);
|
||||
return "";
|
||||
_index : null,
|
||||
_queued_query : null,
|
||||
_pulse_status : -1,
|
||||
|
||||
htmlToText : function(htmlString) {
|
||||
var virtualDocument = document.implementation.createHTMLDocument('virtual');
|
||||
var htmlElement = $(htmlString, virtualDocument);
|
||||
htmlElement.find('.headerlink').remove();
|
||||
docContent = htmlElement.find('[role=main]')[0];
|
||||
if(docContent === undefined) {
|
||||
console.warn("Content block not found. Sphinx search tries to obtain it " +
|
||||
"via '[role=main]'. Could you check your theme or template.");
|
||||
return "";
|
||||
}
|
||||
return docContent.textContent || docContent.innerText;
|
||||
},
|
||||
|
||||
init: () => {
|
||||
const query = new URLSearchParams(window.location.search).get("q");
|
||||
document
|
||||
.querySelectorAll('input[name="q"]')
|
||||
.forEach((el) => (el.value = query));
|
||||
if (query) Search.performSearch(query);
|
||||
init : function() {
|
||||
var params = $.getQueryParameters();
|
||||
if (params.q) {
|
||||
var query = params.q[0];
|
||||
$('input[name="q"]')[0].value = query;
|
||||
this.performSearch(query);
|
||||
}
|
||||
},
|
||||
|
||||
loadIndex: (url) =>
|
||||
(document.body.appendChild(document.createElement("script")).src = url),
|
||||
loadIndex : function(url) {
|
||||
$.ajax({type: "GET", url: url, data: null,
|
||||
dataType: "script", cache: true,
|
||||
complete: function(jqxhr, textstatus) {
|
||||
if (textstatus != "success") {
|
||||
document.getElementById("searchindexloader").src = url;
|
||||
}
|
||||
}});
|
||||
},
|
||||
|
||||
setIndex: (index) => {
|
||||
Search._index = index;
|
||||
if (Search._queued_query !== null) {
|
||||
const query = Search._queued_query;
|
||||
Search._queued_query = null;
|
||||
Search.query(query);
|
||||
setIndex : function(index) {
|
||||
var q;
|
||||
this._index = index;
|
||||
if ((q = this._queued_query) !== null) {
|
||||
this._queued_query = null;
|
||||
Search.query(q);
|
||||
}
|
||||
},
|
||||
|
||||
hasIndex: () => Search._index !== null,
|
||||
hasIndex : function() {
|
||||
return this._index !== null;
|
||||
},
|
||||
|
||||
deferQuery: (query) => (Search._queued_query = query),
|
||||
deferQuery : function(query) {
|
||||
this._queued_query = query;
|
||||
},
|
||||
|
||||
stopPulse: () => (Search._pulse_status = -1),
|
||||
stopPulse : function() {
|
||||
this._pulse_status = 0;
|
||||
},
|
||||
|
||||
startPulse: () => {
|
||||
if (Search._pulse_status >= 0) return;
|
||||
|
||||
const pulse = () => {
|
||||
startPulse : function() {
|
||||
if (this._pulse_status >= 0)
|
||||
return;
|
||||
function pulse() {
|
||||
var i;
|
||||
Search._pulse_status = (Search._pulse_status + 1) % 4;
|
||||
Search.dots.innerText = ".".repeat(Search._pulse_status);
|
||||
if (Search._pulse_status >= 0) window.setTimeout(pulse, 500);
|
||||
};
|
||||
var dotString = '';
|
||||
for (i = 0; i < Search._pulse_status; i++)
|
||||
dotString += '.';
|
||||
Search.dots.text(dotString);
|
||||
if (Search._pulse_status > -1)
|
||||
window.setTimeout(pulse, 500);
|
||||
}
|
||||
pulse();
|
||||
},
|
||||
|
||||
/**
|
||||
* perform a search for something (or wait until index is loaded)
|
||||
*/
|
||||
performSearch: (query) => {
|
||||
performSearch : function(query) {
|
||||
// create the required interface elements
|
||||
const searchText = document.createElement("h2");
|
||||
searchText.textContent = _("Searching");
|
||||
const searchSummary = document.createElement("p");
|
||||
searchSummary.classList.add("search-summary");
|
||||
searchSummary.innerText = "";
|
||||
const searchList = document.createElement("ul");
|
||||
searchList.classList.add("search");
|
||||
this.out = $('#search-results');
|
||||
this.title = $('<h2>' + _('Searching') + '</h2>').appendTo(this.out);
|
||||
this.dots = $('<span></span>').appendTo(this.title);
|
||||
this.status = $('<p class="search-summary"> </p>').appendTo(this.out);
|
||||
this.output = $('<ul class="search"/>').appendTo(this.out);
|
||||
|
||||
const out = document.getElementById("search-results");
|
||||
Search.title = out.appendChild(searchText);
|
||||
Search.dots = Search.title.appendChild(document.createElement("span"));
|
||||
Search.status = out.appendChild(searchSummary);
|
||||
Search.output = out.appendChild(searchList);
|
||||
|
||||
const searchProgress = document.getElementById("search-progress");
|
||||
// Some themes don't use the search progress node
|
||||
if (searchProgress) {
|
||||
searchProgress.innerText = _("Preparing search...");
|
||||
}
|
||||
Search.startPulse();
|
||||
$('#search-progress').text(_('Preparing search...'));
|
||||
this.startPulse();
|
||||
|
||||
// index already loaded, the browser was quick!
|
||||
if (Search.hasIndex()) Search.query(query);
|
||||
else Search.deferQuery(query);
|
||||
if (this.hasIndex())
|
||||
this.query(query);
|
||||
else
|
||||
this.deferQuery(query);
|
||||
},
|
||||
|
||||
/**
|
||||
* execute search (requires search index to be loaded)
|
||||
*/
|
||||
query: (query) => {
|
||||
// stem the search terms and add them to the correct list
|
||||
const stemmer = new Stemmer();
|
||||
const searchTerms = new Set();
|
||||
const excludedTerms = new Set();
|
||||
const highlightTerms = new Set();
|
||||
const objectTerms = new Set(splitQuery(query.toLowerCase().trim()));
|
||||
splitQuery(query.trim()).forEach((queryTerm) => {
|
||||
const queryTermLower = queryTerm.toLowerCase();
|
||||
query : function(query) {
|
||||
var i;
|
||||
|
||||
// maybe skip this "word"
|
||||
// stopwords array is from language_data.js
|
||||
if (
|
||||
stopwords.indexOf(queryTermLower) !== -1 ||
|
||||
queryTerm.match(/^\d+$/)
|
||||
)
|
||||
return;
|
||||
|
||||
// stem the word
|
||||
let word = stemmer.stemWord(queryTermLower);
|
||||
// select the correct list
|
||||
if (word[0] === "-") excludedTerms.add(word.substr(1));
|
||||
else {
|
||||
searchTerms.add(word);
|
||||
highlightTerms.add(queryTermLower);
|
||||
// stem the searchterms and add them to the correct list
|
||||
var stemmer = new Stemmer();
|
||||
var searchterms = [];
|
||||
var excluded = [];
|
||||
var hlterms = [];
|
||||
var tmp = splitQuery(query);
|
||||
var objectterms = [];
|
||||
for (i = 0; i < tmp.length; i++) {
|
||||
if (tmp[i] !== "") {
|
||||
objectterms.push(tmp[i].toLowerCase());
|
||||
}
|
||||
});
|
||||
|
||||
// console.debug("SEARCH: searching for:");
|
||||
// console.info("required: ", [...searchTerms]);
|
||||
// console.info("excluded: ", [...excludedTerms]);
|
||||
if ($u.indexOf(stopwords, tmp[i].toLowerCase()) != -1 || tmp[i] === "") {
|
||||
// skip this "word"
|
||||
continue;
|
||||
}
|
||||
// stem the word
|
||||
var word = stemmer.stemWord(tmp[i].toLowerCase());
|
||||
// prevent stemmer from cutting word smaller than two chars
|
||||
if(word.length < 3 && tmp[i].length >= 3) {
|
||||
word = tmp[i];
|
||||
}
|
||||
var toAppend;
|
||||
// select the correct list
|
||||
if (word[0] == '-') {
|
||||
toAppend = excluded;
|
||||
word = word.substr(1);
|
||||
}
|
||||
else {
|
||||
toAppend = searchterms;
|
||||
hlterms.push(tmp[i].toLowerCase());
|
||||
}
|
||||
// only add if not already in the list
|
||||
if (!$u.contains(toAppend, word))
|
||||
toAppend.push(word);
|
||||
}
|
||||
var highlightstring = '?highlight=' + $.urlencode(hlterms.join(" "));
|
||||
|
||||
// array of [docname, title, anchor, descr, score, filename]
|
||||
let results = [];
|
||||
_removeChildren(document.getElementById("search-progress"));
|
||||
// console.debug('SEARCH: searching for:');
|
||||
// console.info('required: ', searchterms);
|
||||
// console.info('excluded: ', excluded);
|
||||
|
||||
// prepare search
|
||||
var terms = this._index.terms;
|
||||
var titleterms = this._index.titleterms;
|
||||
|
||||
// array of [filename, title, anchor, descr, score]
|
||||
var results = [];
|
||||
$('#search-progress').empty();
|
||||
|
||||
// lookup as object
|
||||
objectTerms.forEach((term) =>
|
||||
results.push(...Search.performObjectSearch(term, objectTerms))
|
||||
);
|
||||
for (i = 0; i < objectterms.length; i++) {
|
||||
var others = [].concat(objectterms.slice(0, i),
|
||||
objectterms.slice(i+1, objectterms.length));
|
||||
results = results.concat(this.performObjectSearch(objectterms[i], others));
|
||||
}
|
||||
|
||||
// lookup as search terms in fulltext
|
||||
results.push(...Search.performTermsSearch(searchTerms, excludedTerms));
|
||||
results = results.concat(this.performTermsSearch(searchterms, excluded, terms, titleterms));
|
||||
|
||||
// let the scorer override scores with a custom scoring function
|
||||
if (Scorer.score) results.forEach((item) => (item[4] = Scorer.score(item)));
|
||||
if (Scorer.score) {
|
||||
for (i = 0; i < results.length; i++)
|
||||
results[i][4] = Scorer.score(results[i]);
|
||||
}
|
||||
|
||||
// now sort the results by score (in opposite order of appearance, since the
|
||||
// display function below uses pop() to retrieve items) and then
|
||||
// alphabetically
|
||||
results.sort((a, b) => {
|
||||
const leftScore = a[4];
|
||||
const rightScore = b[4];
|
||||
if (leftScore === rightScore) {
|
||||
results.sort(function(a, b) {
|
||||
var left = a[4];
|
||||
var right = b[4];
|
||||
if (left > right) {
|
||||
return 1;
|
||||
} else if (left < right) {
|
||||
return -1;
|
||||
} else {
|
||||
// same score: sort alphabetically
|
||||
const leftTitle = a[1].toLowerCase();
|
||||
const rightTitle = b[1].toLowerCase();
|
||||
if (leftTitle === rightTitle) return 0;
|
||||
return leftTitle > rightTitle ? -1 : 1; // inverted is intentional
|
||||
left = a[1].toLowerCase();
|
||||
right = b[1].toLowerCase();
|
||||
return (left > right) ? -1 : ((left < right) ? 1 : 0);
|
||||
}
|
||||
return leftScore > rightScore ? 1 : -1;
|
||||
});
|
||||
|
||||
// remove duplicate search results
|
||||
// note the reversing of results, so that in the case of duplicates, the highest-scoring entry is kept
|
||||
let seen = new Set();
|
||||
results = results.reverse().reduce((acc, result) => {
|
||||
let resultStr = result.slice(0, 4).concat([result[5]]).map(v => String(v)).join(',');
|
||||
if (!seen.has(resultStr)) {
|
||||
acc.push(result);
|
||||
seen.add(resultStr);
|
||||
}
|
||||
return acc;
|
||||
}, []);
|
||||
|
||||
results = results.reverse();
|
||||
|
||||
// for debugging
|
||||
//Search.lastresults = results.slice(); // a copy
|
||||
// console.info("search results:", Search.lastresults);
|
||||
//console.info('search results:', Search.lastresults);
|
||||
|
||||
// print the results
|
||||
_displayNextItem(results, results.length, highlightTerms, searchTerms);
|
||||
var resultCount = results.length;
|
||||
function displayNextItem() {
|
||||
// results left, load the summary and display it
|
||||
if (results.length) {
|
||||
var item = results.pop();
|
||||
var listItem = $('<li></li>');
|
||||
var requestUrl = "";
|
||||
var linkUrl = "";
|
||||
if (DOCUMENTATION_OPTIONS.BUILDER === 'dirhtml') {
|
||||
// dirhtml builder
|
||||
var dirname = item[0] + '/';
|
||||
if (dirname.match(/\/index\/$/)) {
|
||||
dirname = dirname.substring(0, dirname.length-6);
|
||||
} else if (dirname == 'index/') {
|
||||
dirname = '';
|
||||
}
|
||||
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + dirname;
|
||||
linkUrl = requestUrl;
|
||||
|
||||
} else {
|
||||
// normal html builders
|
||||
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + item[0] + DOCUMENTATION_OPTIONS.FILE_SUFFIX;
|
||||
linkUrl = item[0] + DOCUMENTATION_OPTIONS.LINK_SUFFIX;
|
||||
}
|
||||
listItem.append($('<a/>').attr('href',
|
||||
linkUrl +
|
||||
highlightstring + item[2]).html(item[1]));
|
||||
if (item[3]) {
|
||||
listItem.append($('<span> (' + item[3] + ')</span>'));
|
||||
Search.output.append(listItem);
|
||||
setTimeout(function() {
|
||||
displayNextItem();
|
||||
}, 5);
|
||||
} else if (DOCUMENTATION_OPTIONS.HAS_SOURCE) {
|
||||
$.ajax({url: requestUrl,
|
||||
dataType: "text",
|
||||
complete: function(jqxhr, textstatus) {
|
||||
var data = jqxhr.responseText;
|
||||
if (data !== '' && data !== undefined) {
|
||||
var summary = Search.makeSearchSummary(data, searchterms, hlterms);
|
||||
if (summary) {
|
||||
listItem.append(summary);
|
||||
}
|
||||
}
|
||||
Search.output.append(listItem);
|
||||
setTimeout(function() {
|
||||
displayNextItem();
|
||||
}, 5);
|
||||
}});
|
||||
} else {
|
||||
// no source available, just display title
|
||||
Search.output.append(listItem);
|
||||
setTimeout(function() {
|
||||
displayNextItem();
|
||||
}, 5);
|
||||
}
|
||||
}
|
||||
// search finished, update title and status message
|
||||
else {
|
||||
Search.stopPulse();
|
||||
Search.title.text(_('Search Results'));
|
||||
if (!resultCount)
|
||||
Search.status.text(_('Your search did not match any documents. Please make sure that all words are spelled correctly and that you\'ve selected enough categories.'));
|
||||
else
|
||||
Search.status.text(_('Search finished, found %s page(s) matching the search query.').replace('%s', resultCount));
|
||||
Search.status.fadeIn(500);
|
||||
}
|
||||
}
|
||||
displayNextItem();
|
||||
},
|
||||
|
||||
/**
|
||||
* search for object names
|
||||
*/
|
||||
performObjectSearch: (object, objectTerms) => {
|
||||
const filenames = Search._index.filenames;
|
||||
const docNames = Search._index.docnames;
|
||||
const objects = Search._index.objects;
|
||||
const objNames = Search._index.objnames;
|
||||
const titles = Search._index.titles;
|
||||
performObjectSearch : function(object, otherterms) {
|
||||
var filenames = this._index.filenames;
|
||||
var docnames = this._index.docnames;
|
||||
var objects = this._index.objects;
|
||||
var objnames = this._index.objnames;
|
||||
var titles = this._index.titles;
|
||||
|
||||
const results = [];
|
||||
var i;
|
||||
var results = [];
|
||||
|
||||
const objectSearchCallback = (prefix, match) => {
|
||||
const name = match[4]
|
||||
const fullname = (prefix ? prefix + "." : "") + name;
|
||||
const fullnameLower = fullname.toLowerCase();
|
||||
if (fullnameLower.indexOf(object) < 0) return;
|
||||
|
||||
let score = 0;
|
||||
const parts = fullnameLower.split(".");
|
||||
|
||||
// check for different match types: exact matches of full name or
|
||||
// "last name" (i.e. last dotted part)
|
||||
if (fullnameLower === object || parts.slice(-1)[0] === object)
|
||||
score += Scorer.objNameMatch;
|
||||
else if (parts.slice(-1)[0].indexOf(object) > -1)
|
||||
score += Scorer.objPartialMatch; // matches in last name
|
||||
|
||||
const objName = objNames[match[1]][2];
|
||||
const title = titles[match[0]];
|
||||
|
||||
// If more than one term searched for, we require other words to be
|
||||
// found in the name/title/description
|
||||
const otherTerms = new Set(objectTerms);
|
||||
otherTerms.delete(object);
|
||||
if (otherTerms.size > 0) {
|
||||
const haystack = `${prefix} ${name} ${objName} ${title}`.toLowerCase();
|
||||
if (
|
||||
[...otherTerms].some((otherTerm) => haystack.indexOf(otherTerm) < 0)
|
||||
)
|
||||
return;
|
||||
for (var prefix in objects) {
|
||||
if (!(objects[prefix] instanceof Array)) {
|
||||
objects[prefix] = Object.entries(objects[prefix]).map(([name, match]) => [...match, name]);
|
||||
}
|
||||
for (var iMatch = 0; iMatch != objects[prefix].length; ++iMatch) {
|
||||
var match = objects[prefix][iMatch];
|
||||
var name = match[4];
|
||||
var fullname = (prefix ? prefix + '.' : '') + name;
|
||||
var fullnameLower = fullname.toLowerCase()
|
||||
if (fullnameLower.indexOf(object) > -1) {
|
||||
var score = 0;
|
||||
var parts = fullnameLower.split('.');
|
||||
// check for different match types: exact matches of full name or
|
||||
// "last name" (i.e. last dotted part)
|
||||
if (fullnameLower == object || parts[parts.length - 1] == object) {
|
||||
score += Scorer.objNameMatch;
|
||||
// matches in last name
|
||||
} else if (parts[parts.length - 1].indexOf(object) > -1) {
|
||||
score += Scorer.objPartialMatch;
|
||||
}
|
||||
var objname = objnames[match[1]][2];
|
||||
var title = titles[match[0]];
|
||||
// If more than one term searched for, we require other words to be
|
||||
// found in the name/title/description
|
||||
if (otherterms.length > 0) {
|
||||
var haystack = (prefix + ' ' + name + ' ' +
|
||||
objname + ' ' + title).toLowerCase();
|
||||
var allfound = true;
|
||||
for (i = 0; i < otherterms.length; i++) {
|
||||
if (haystack.indexOf(otherterms[i]) == -1) {
|
||||
allfound = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!allfound) {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
var descr = objname + _(', in ') + title;
|
||||
|
||||
let anchor = match[3];
|
||||
if (anchor === "") anchor = fullname;
|
||||
else if (anchor === "-") anchor = objNames[match[1]][1] + "-" + fullname;
|
||||
var anchor = match[3];
|
||||
if (anchor === '')
|
||||
anchor = fullname;
|
||||
else if (anchor == '-')
|
||||
anchor = objnames[match[1]][1] + '-' + fullname;
|
||||
// add custom score for some objects according to scorer
|
||||
if (Scorer.objPrio.hasOwnProperty(match[2])) {
|
||||
score += Scorer.objPrio[match[2]];
|
||||
} else {
|
||||
score += Scorer.objPrioDefault;
|
||||
}
|
||||
results.push([docnames[match[0]], fullname, '#'+anchor, descr, score, filenames[match[0]]]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
const descr = objName + _(", in ") + title;
|
||||
|
||||
// add custom score for some objects according to scorer
|
||||
if (Scorer.objPrio.hasOwnProperty(match[2]))
|
||||
score += Scorer.objPrio[match[2]];
|
||||
else score += Scorer.objPrioDefault;
|
||||
|
||||
results.push([
|
||||
docNames[match[0]],
|
||||
fullname,
|
||||
"#" + anchor,
|
||||
descr,
|
||||
score,
|
||||
filenames[match[0]],
|
||||
]);
|
||||
};
|
||||
Object.keys(objects).forEach((prefix) =>
|
||||
objects[prefix].forEach((array) =>
|
||||
objectSearchCallback(prefix, array)
|
||||
)
|
||||
);
|
||||
return results;
|
||||
},
|
||||
|
||||
/**
|
||||
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions
|
||||
*/
|
||||
escapeRegExp : function(string) {
|
||||
return string.replace(/[.*+\-?^${}()|[\]\\]/g, '\\$&'); // $& means the whole matched string
|
||||
},
|
||||
|
||||
/**
|
||||
* search for full-text terms in the index
|
||||
*/
|
||||
performTermsSearch: (searchTerms, excludedTerms) => {
|
||||
// prepare search
|
||||
const terms = Search._index.terms;
|
||||
const titleTerms = Search._index.titleterms;
|
||||
const docNames = Search._index.docnames;
|
||||
const filenames = Search._index.filenames;
|
||||
const titles = Search._index.titles;
|
||||
performTermsSearch : function(searchterms, excluded, terms, titleterms) {
|
||||
var docnames = this._index.docnames;
|
||||
var filenames = this._index.filenames;
|
||||
var titles = this._index.titles;
|
||||
|
||||
const scoreMap = new Map();
|
||||
const fileMap = new Map();
|
||||
var i, j, file;
|
||||
var fileMap = {};
|
||||
var scoreMap = {};
|
||||
var results = [];
|
||||
|
||||
// perform the search on the required terms
|
||||
searchTerms.forEach((word) => {
|
||||
const files = [];
|
||||
const arr = [
|
||||
{ files: terms[word], score: Scorer.term },
|
||||
{ files: titleTerms[word], score: Scorer.title },
|
||||
for (i = 0; i < searchterms.length; i++) {
|
||||
var word = searchterms[i];
|
||||
var files = [];
|
||||
var _o = [
|
||||
{files: terms[word], score: Scorer.term},
|
||||
{files: titleterms[word], score: Scorer.title}
|
||||
];
|
||||
// add support for partial matches
|
||||
if (word.length > 2) {
|
||||
const escapedWord = _escapeRegExp(word);
|
||||
Object.keys(terms).forEach((term) => {
|
||||
if (term.match(escapedWord) && !terms[word])
|
||||
arr.push({ files: terms[term], score: Scorer.partialTerm });
|
||||
});
|
||||
Object.keys(titleTerms).forEach((term) => {
|
||||
if (term.match(escapedWord) && !titleTerms[word])
|
||||
arr.push({ files: titleTerms[word], score: Scorer.partialTitle });
|
||||
});
|
||||
var word_regex = this.escapeRegExp(word);
|
||||
for (var w in terms) {
|
||||
if (w.match(word_regex) && !terms[word]) {
|
||||
_o.push({files: terms[w], score: Scorer.partialTerm})
|
||||
}
|
||||
}
|
||||
for (var w in titleterms) {
|
||||
if (w.match(word_regex) && !titleterms[word]) {
|
||||
_o.push({files: titleterms[w], score: Scorer.partialTitle})
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// no match but word was a required one
|
||||
if (arr.every((record) => record.files === undefined)) return;
|
||||
|
||||
if ($u.every(_o, function(o){return o.files === undefined;})) {
|
||||
break;
|
||||
}
|
||||
// found search word in contents
|
||||
arr.forEach((record) => {
|
||||
if (record.files === undefined) return;
|
||||
$u.each(_o, function(o) {
|
||||
var _files = o.files;
|
||||
if (_files === undefined)
|
||||
return
|
||||
|
||||
let recordFiles = record.files;
|
||||
if (recordFiles.length === undefined) recordFiles = [recordFiles];
|
||||
files.push(...recordFiles);
|
||||
if (_files.length === undefined)
|
||||
_files = [_files];
|
||||
files = files.concat(_files);
|
||||
|
||||
// set score for the word in each file
|
||||
recordFiles.forEach((file) => {
|
||||
if (!scoreMap.has(file)) scoreMap.set(file, {});
|
||||
scoreMap.get(file)[word] = record.score;
|
||||
});
|
||||
// set score for the word in each file to Scorer.term
|
||||
for (j = 0; j < _files.length; j++) {
|
||||
file = _files[j];
|
||||
if (!(file in scoreMap))
|
||||
scoreMap[file] = {};
|
||||
scoreMap[file][word] = o.score;
|
||||
}
|
||||
});
|
||||
|
||||
// create the mapping
|
||||
files.forEach((file) => {
|
||||
if (fileMap.has(file) && fileMap.get(file).indexOf(word) === -1)
|
||||
fileMap.get(file).push(word);
|
||||
else fileMap.set(file, [word]);
|
||||
});
|
||||
});
|
||||
for (j = 0; j < files.length; j++) {
|
||||
file = files[j];
|
||||
if (file in fileMap && fileMap[file].indexOf(word) === -1)
|
||||
fileMap[file].push(word);
|
||||
else
|
||||
fileMap[file] = [word];
|
||||
}
|
||||
}
|
||||
|
||||
// now check if the files don't contain excluded terms
|
||||
const results = [];
|
||||
for (const [file, wordList] of fileMap) {
|
||||
// check if all requirements are matched
|
||||
for (file in fileMap) {
|
||||
var valid = true;
|
||||
|
||||
// as search terms with length < 3 are discarded
|
||||
const filteredTermCount = [...searchTerms].filter(
|
||||
(term) => term.length > 2
|
||||
).length;
|
||||
// check if all requirements are matched
|
||||
var filteredTermCount = // as search terms with length < 3 are discarded: ignore
|
||||
searchterms.filter(function(term){return term.length > 2}).length
|
||||
if (
|
||||
wordList.length !== searchTerms.size &&
|
||||
wordList.length !== filteredTermCount
|
||||
)
|
||||
continue;
|
||||
fileMap[file].length != searchterms.length &&
|
||||
fileMap[file].length != filteredTermCount
|
||||
) continue;
|
||||
|
||||
// ensure that none of the excluded terms is in the search result
|
||||
if (
|
||||
[...excludedTerms].some(
|
||||
(term) =>
|
||||
terms[term] === file ||
|
||||
titleTerms[term] === file ||
|
||||
(terms[term] || []).includes(file) ||
|
||||
(titleTerms[term] || []).includes(file)
|
||||
)
|
||||
)
|
||||
break;
|
||||
for (i = 0; i < excluded.length; i++) {
|
||||
if (terms[excluded[i]] == file ||
|
||||
titleterms[excluded[i]] == file ||
|
||||
$u.contains(terms[excluded[i]] || [], file) ||
|
||||
$u.contains(titleterms[excluded[i]] || [], file)) {
|
||||
valid = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
// select one (max) score for the file.
|
||||
const score = Math.max(...wordList.map((w) => scoreMap.get(file)[w]));
|
||||
// add result to the result list
|
||||
results.push([
|
||||
docNames[file],
|
||||
titles[file],
|
||||
"",
|
||||
null,
|
||||
score,
|
||||
filenames[file],
|
||||
]);
|
||||
// if we have still a valid result we can add it to the result list
|
||||
if (valid) {
|
||||
// select one (max) score for the file.
|
||||
// for better ranking, we should calculate ranking by using words statistics like basic tf-idf...
|
||||
var score = $u.max($u.map(fileMap[file], function(w){return scoreMap[file][w]}));
|
||||
results.push([docnames[file], titles[file], '', null, score, filenames[file]]);
|
||||
}
|
||||
}
|
||||
return results;
|
||||
},
|
||||
@ -497,34 +499,34 @@ const Search = {
|
||||
/**
|
||||
* helper function to return a node containing the
|
||||
* search summary for a given text. keywords is a list
|
||||
* of stemmed words, highlightWords is the list of normal, unstemmed
|
||||
* of stemmed words, hlwords is the list of normal, unstemmed
|
||||
* words. the first one is used to find the occurrence, the
|
||||
* latter for highlighting it.
|
||||
*/
|
||||
makeSearchSummary: (htmlText, keywords, highlightWords) => {
|
||||
const text = Search.htmlToText(htmlText);
|
||||
if (text === "") return null;
|
||||
|
||||
const textLower = text.toLowerCase();
|
||||
const actualStartPosition = [...keywords]
|
||||
.map((k) => textLower.indexOf(k.toLowerCase()))
|
||||
.filter((i) => i > -1)
|
||||
.slice(-1)[0];
|
||||
const startWithContext = Math.max(actualStartPosition - 120, 0);
|
||||
|
||||
const top = startWithContext === 0 ? "" : "...";
|
||||
const tail = startWithContext + 240 < text.length ? "..." : "";
|
||||
|
||||
let summary = document.createElement("p");
|
||||
summary.classList.add("context");
|
||||
summary.textContent = top + text.substr(startWithContext, 240).trim() + tail;
|
||||
|
||||
highlightWords.forEach((highlightWord) =>
|
||||
_highlightText(summary, highlightWord, "highlighted")
|
||||
);
|
||||
|
||||
return summary;
|
||||
},
|
||||
makeSearchSummary : function(htmlText, keywords, hlwords) {
|
||||
var text = Search.htmlToText(htmlText);
|
||||
if (text == "") {
|
||||
return null;
|
||||
}
|
||||
var textLower = text.toLowerCase();
|
||||
var start = 0;
|
||||
$.each(keywords, function() {
|
||||
var i = textLower.indexOf(this.toLowerCase());
|
||||
if (i > -1)
|
||||
start = i;
|
||||
});
|
||||
start = Math.max(start - 120, 0);
|
||||
var excerpt = ((start > 0) ? '...' : '') +
|
||||
$.trim(text.substr(start, 240)) +
|
||||
((start + 240 - text.length) ? '...' : '');
|
||||
var rv = $('<p class="context"></p>').text(excerpt);
|
||||
$.each(hlwords, function() {
|
||||
rv = rv.highlightText(this, 'highlighted');
|
||||
});
|
||||
return rv;
|
||||
}
|
||||
};
|
||||
|
||||
_ready(Search.init);
|
||||
$(document).ready(function() {
|
||||
Search.init();
|
||||
});
|
||||
|
||||
File diff suppressed because one or more lines are too long
@ -13,7 +13,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="#" />
|
||||
|
||||
@ -14,7 +14,6 @@
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<script src="_static/searchtools.js"></script>
|
||||
|
||||
File diff suppressed because one or more lines are too long
@ -1,5 +1,6 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
-- | Errors from dynamic loading of shared libraries for FFI.
|
||||
module Cryptol.Backend.FFI.Error where
|
||||
|
||||
@ -421,10 +421,11 @@ data EvalError
|
||||
| NoPrim Name -- ^ Primitive with no implementation
|
||||
| BadRoundingMode Integer -- ^ Invalid rounding mode
|
||||
| BadValue String -- ^ Value outside the domain of a partial function.
|
||||
| NoMatchingPropGuardCase String -- ^ No prop guard holds for the given type variables.
|
||||
| FFINotSupported Name -- ^ Foreign function cannot be called
|
||||
| FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
|
||||
-- as a type argument is too large
|
||||
deriving Typeable
|
||||
deriving Typeable
|
||||
|
||||
instance PP EvalError where
|
||||
ppPrec _ e = case e of
|
||||
@ -443,6 +444,7 @@ instance PP EvalError where
|
||||
BadRoundingMode r -> "invalid rounding mode" <+> integer r
|
||||
BadValue x -> "invalid input for" <+> backticks (text x)
|
||||
NoPrim x -> text "unimplemented primitive:" <+> pp x
|
||||
NoMatchingPropGuardCase msg -> text $ "No matching constraint guard; " ++ msg
|
||||
FFINotSupported x -> vcat
|
||||
[ text "cannot call foreign function" <+> pp x
|
||||
, text "FFI calls are not supported in this context"
|
||||
|
||||
@ -15,6 +15,7 @@
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
|
||||
module Cryptol.Eval (
|
||||
moduleEnv
|
||||
@ -35,6 +36,7 @@ module Cryptol.Eval (
|
||||
, Unsupported(..)
|
||||
, WordTooWide(..)
|
||||
, forceValue
|
||||
, checkProp
|
||||
) where
|
||||
|
||||
import Cryptol.Backend
|
||||
@ -63,6 +65,7 @@ import Data.Maybe
|
||||
import qualified Data.IntMap.Strict as IntMap
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Semigroup
|
||||
import Control.Applicative
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
@ -215,12 +218,52 @@ evalExpr sym env expr = case expr of
|
||||
env' <- evalDecls sym ds env
|
||||
evalExpr sym env' e
|
||||
|
||||
EPropGuards guards _ -> {-# SCC "evalExpr->EPropGuards" #-} do
|
||||
let checkedGuards = [ e | (ps,e) <- guards, all (checkProp . evalProp env) ps ]
|
||||
case checkedGuards of
|
||||
(e:_) -> eval e
|
||||
[] -> raiseError sym (NoMatchingPropGuardCase $ "Among constraint guards: " ++ show (fmap pp . fst <$> guards))
|
||||
|
||||
where
|
||||
|
||||
{-# INLINE eval #-}
|
||||
eval = evalExpr sym env
|
||||
ppV = ppValue sym defaultPPOpts
|
||||
|
||||
-- | Checks whether an evaluated `Prop` holds
|
||||
checkProp :: Prop -> Bool
|
||||
checkProp = \case
|
||||
TCon tcon ts ->
|
||||
let ns = toNat' <$> ts in
|
||||
case tcon of
|
||||
PC PEqual | [n1, n2] <- ns -> n1 == n2
|
||||
PC PNeq | [n1, n2] <- ns -> n1 /= n2
|
||||
PC PGeq | [n1, n2] <- ns -> n1 >= n2
|
||||
PC PFin | [n] <- ns -> n /= Inf
|
||||
-- TODO: instantiate UniqueFactorization for Nat'?
|
||||
-- PC PPrime | [n] <- ns -> isJust (isPrime n)
|
||||
PC PTrue -> True
|
||||
_ -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ TCon tcon ts ]
|
||||
prop -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ prop ]
|
||||
where
|
||||
toNat' :: Type -> Nat'
|
||||
toNat' = \case
|
||||
TCon (TC (TCNum n)) [] -> Nat n
|
||||
TCon (TC TCInf) [] -> Inf
|
||||
prop -> panic "checkProp" ["Expected `" ++ pretty prop ++ "` to be an evaluated numeric type"]
|
||||
|
||||
|
||||
-- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables according
|
||||
-- to `envTypes` and expanding all type synonyms via `tNoUser`.
|
||||
evalProp :: GenEvalEnv sym -> Prop -> Prop
|
||||
evalProp env@EvalEnv { envTypes } = \case
|
||||
TCon tc tys -> TCon tc (toType . evalType envTypes <$> tys)
|
||||
TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty
|
||||
prop@TUser {} -> evalProp env (tNoUser prop)
|
||||
TVar tv | Nothing <- lookupTypeVar tv envTypes -> panic "evalProp" ["Could not find type variable `" ++ pretty tv ++ "` in the type evaluation environment"]
|
||||
prop -> panic "evalProp" ["Cannot use the following as a type constraint: `" ++ pretty prop ++ "`"]
|
||||
where
|
||||
toType = either tNumTy tValTy
|
||||
|
||||
-- | Capure the current call stack from the evaluation monad and
|
||||
-- annotate function values. When arguments are later applied
|
||||
@ -409,8 +452,10 @@ evalDecl ::
|
||||
GenEvalEnv sym {- ^ An evaluation environment to extend with the given declaration -} ->
|
||||
Decl {- ^ The declaration to evaluate -} ->
|
||||
SEval sym (GenEvalEnv sym)
|
||||
evalDecl sym renv env d =
|
||||
let ?range = nameLoc (dName d) in
|
||||
-- evalDecl sym renv env d =
|
||||
-- let ?range = nameLoc (dName d) in
|
||||
evalDecl sym renv env d = do
|
||||
let ?range = nameLoc (dName d)
|
||||
case dDefinition d of
|
||||
DPrim ->
|
||||
case ?evalPrim =<< asPrim (dName d) of
|
||||
|
||||
@ -10,6 +10,8 @@
|
||||
> {-# LANGUAGE BlockArguments #-}
|
||||
> {-# LANGUAGE PatternGuards #-}
|
||||
> {-# LANGUAGE LambdaCase #-}
|
||||
> {-# LANGUAGE NamedFieldPuns #-}
|
||||
> {-# LANGUAGE ViewPatterns #-}
|
||||
>
|
||||
> module Cryptol.Eval.Reference
|
||||
> ( Value(..)
|
||||
@ -32,6 +34,7 @@
|
||||
> import LibBF (BigFloat)
|
||||
> import qualified LibBF as FP
|
||||
> import qualified GHC.Num.Compat as Integer
|
||||
> import qualified Data.List as List
|
||||
>
|
||||
> import Cryptol.ModuleSystem.Name (asPrim)
|
||||
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
|
||||
@ -46,6 +49,8 @@
|
||||
> import Cryptol.Utils.Panic (panic)
|
||||
> import Cryptol.Utils.PP
|
||||
> import Cryptol.Utils.RecordMap
|
||||
> import Cryptol.Eval (checkProp)
|
||||
> import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy)
|
||||
>
|
||||
> import qualified Cryptol.ModuleSystem as M
|
||||
> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)
|
||||
@ -332,11 +337,27 @@ assigns values to those variables.
|
||||
> EProofAbs _ e -> evalExpr env e
|
||||
> EProofApp e -> evalExpr env e
|
||||
> EWhere e dgs -> evalExpr (foldl evalDeclGroup env dgs) e
|
||||
|
||||
>
|
||||
> EPropGuards guards _ty ->
|
||||
> case List.find (all (checkProp . evalProp env) . fst) guards of
|
||||
> Just (_, e) -> evalExpr env e
|
||||
> Nothing -> evalPanic "fromVBit" ["No guard constraint was satisfied"]
|
||||
|
||||
> appFun :: E Value -> E Value -> E Value
|
||||
> appFun f v = f >>= \f' -> fromVFun f' v
|
||||
|
||||
> -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables
|
||||
> -- according to `envTypes` and expanding all type synonyms via `tNoUser`.
|
||||
> evalProp :: Env -> Prop -> Prop
|
||||
> evalProp env@Env { envTypes } = \case
|
||||
> TCon tc tys -> TCon tc (toType . evalType envTypes <$> tys)
|
||||
> TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty
|
||||
> prop@TUser {} -> evalProp env (tNoUser prop)
|
||||
> TVar tv | Nothing <- lookupTypeVar tv envTypes -> panic "evalProp" ["Could not find type variable `" ++ pretty tv ++ "` in the type evaluation environment"]
|
||||
> prop -> panic "evalProp" ["Cannot use the following as a type constraint: `" ++ pretty prop ++ "`"]
|
||||
> where
|
||||
> toType = either tNumTy tValTy
|
||||
|
||||
|
||||
Selectors
|
||||
---------
|
||||
|
||||
@ -28,7 +28,7 @@ import Control.DeepSeq
|
||||
-- | An evaluated type of kind *.
|
||||
-- These types do not contain type variables, type synonyms, or type functions.
|
||||
data TValue
|
||||
= TVBit -- ^ @ Bit @
|
||||
= TVBit -- ^ @ Bit @
|
||||
| TVInteger -- ^ @ Integer @
|
||||
| TVFloat Integer Integer -- ^ @ Float e p @
|
||||
| TVIntMod Integer -- ^ @ Z n @
|
||||
@ -105,6 +105,7 @@ finNat' n' =
|
||||
newtype TypeEnv =
|
||||
TypeEnv
|
||||
{ envTypeMap :: IntMap.IntMap (Either Nat' TValue) }
|
||||
deriving (Show)
|
||||
|
||||
instance Monoid TypeEnv where
|
||||
mempty = TypeEnv mempty
|
||||
|
||||
@ -117,6 +117,7 @@ instance FreeVars Expr where
|
||||
EProofAbs p e -> freeVars p <> freeVars e
|
||||
EProofApp e -> freeVars e
|
||||
EWhere e ds -> foldFree ds <> rmVals (defs ds) (freeVars e)
|
||||
EPropGuards guards _ -> mconcat [ freeVars e | (_, e) <- guards ]
|
||||
where
|
||||
foldFree :: (FreeVars a, Defs a) => [a] -> Deps
|
||||
foldFree = foldr updateFree mempty
|
||||
|
||||
@ -61,6 +61,8 @@ import qualified Cryptol.Parser as P
|
||||
import qualified Cryptol.Parser.Unlit as P
|
||||
import Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))
|
||||
import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards
|
||||
( expandPropGuards, runExpandPropGuardsM )
|
||||
import Cryptol.Parser.NoInclude (removeIncludesModule)
|
||||
import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
@ -118,6 +120,14 @@ noPat a = do
|
||||
unless (null errs) (noPatErrors errs)
|
||||
return a'
|
||||
|
||||
-- ExpandPropGuards ------------------------------------------------------------
|
||||
|
||||
-- | Run the expandPropGuards pass.
|
||||
expandPropGuards :: Module PName -> ModuleM (Module PName)
|
||||
expandPropGuards a =
|
||||
case ExpandPropGuards.runExpandPropGuardsM $ ExpandPropGuards.expandPropGuards a of
|
||||
Left err -> expandPropGuardsError err
|
||||
Right a' -> pure a'
|
||||
|
||||
-- Parsing ---------------------------------------------------------------------
|
||||
|
||||
@ -468,8 +478,11 @@ checkSingleModule how isrc m = do
|
||||
-- remove pattern bindings
|
||||
npm <- noPat m
|
||||
|
||||
-- run expandPropGuards
|
||||
epgm <- expandPropGuards npm
|
||||
|
||||
-- rename everything
|
||||
renMod <- renameModule npm
|
||||
renMod <- renameModule epgm
|
||||
|
||||
-- when generating the prim map for the typechecker, if we're checking the
|
||||
-- prelude, we have to generate the map from the renaming environment, as we
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.ModuleSystem.Exports where
|
||||
|
||||
import Data.Set(Set)
|
||||
|
||||
@ -217,6 +217,10 @@ instance Inst Expr where
|
||||
EProofApp e -> EProofApp (go e)
|
||||
EWhere e ds -> EWhere (go e) (inst env ds)
|
||||
|
||||
-- TODO: this doesn't exist in the new module system, so it will have to
|
||||
-- be implemented differently there anyway
|
||||
EPropGuards _guards _ty -> panic "inst" ["This is not implemented for EPropGuards yet."]
|
||||
|
||||
|
||||
instance Inst DeclGroup where
|
||||
inst env dg =
|
||||
|
||||
@ -11,6 +11,7 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.ModuleSystem.Interface (
|
||||
Iface
|
||||
, IfaceG(..)
|
||||
|
||||
@ -29,6 +29,7 @@ import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Position (Located)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import qualified Cryptol.Parser.NoPat as NoPat
|
||||
import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards
|
||||
import qualified Cryptol.Parser.NoInclude as NoInc
|
||||
import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
@ -102,6 +103,8 @@ data ModuleError
|
||||
-- ^ Problems during the renaming phase
|
||||
| NoPatErrors ImportSource [NoPat.Error]
|
||||
-- ^ Problems during the NoPat phase
|
||||
| ExpandPropGuardsError ImportSource ExpandPropGuards.Error
|
||||
-- ^ Problems during the ExpandPropGuards phase
|
||||
| NoIncludeErrors ImportSource [NoInc.IncludeError]
|
||||
-- ^ Problems during the NoInclude phase
|
||||
| TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)]
|
||||
@ -137,6 +140,7 @@ instance NFData ModuleError where
|
||||
RecursiveModules mods -> mods `deepseq` ()
|
||||
RenamerErrors src errs -> src `deepseq` errs `deepseq` ()
|
||||
NoPatErrors src errs -> src `deepseq` errs `deepseq` ()
|
||||
ExpandPropGuardsError src err -> src `deepseq` err `deepseq` ()
|
||||
NoIncludeErrors src errs -> src `deepseq` errs `deepseq` ()
|
||||
TypeCheckingFailed nm src errs -> nm `deepseq` src `deepseq` errs `deepseq` ()
|
||||
ModuleNameMismatch expected found ->
|
||||
@ -185,6 +189,8 @@ instance PP ModuleError where
|
||||
|
||||
NoPatErrors _src errs -> vcat (map pp errs)
|
||||
|
||||
ExpandPropGuardsError _src err -> pp err
|
||||
|
||||
NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs)
|
||||
|
||||
TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs)
|
||||
@ -250,6 +256,11 @@ noPatErrors errs = do
|
||||
src <- getImportSource
|
||||
ModuleT (raise (NoPatErrors src errs))
|
||||
|
||||
expandPropGuardsError :: ExpandPropGuards.Error -> ModuleM a
|
||||
expandPropGuardsError err = do
|
||||
src <- getImportSource
|
||||
ModuleT (raise (ExpandPropGuardsError src err))
|
||||
|
||||
noIncludeErrors :: [NoInc.IncludeError] -> ModuleM a
|
||||
noIncludeErrors errs = do
|
||||
src <- getImportSource
|
||||
|
||||
@ -685,6 +685,11 @@ instance Rename BindDef where
|
||||
rename DPrim = return DPrim
|
||||
rename DForeign = return DForeign
|
||||
rename (DExpr e) = DExpr <$> rename e
|
||||
rename (DPropGuards cases) = DPropGuards <$> traverse rename cases
|
||||
|
||||
instance Rename PropGuardCase where
|
||||
rename g = PropGuardCase <$> traverse (rnLocated rename) (pgcProps g)
|
||||
<*> rename (pgcExpr g)
|
||||
|
||||
-- NOTE: this only renames types within the pattern.
|
||||
instance Rename Pattern where
|
||||
|
||||
@ -302,11 +302,14 @@ mbDoc :: { Maybe (Located Text) }
|
||||
: doc { Just $1 }
|
||||
| {- empty -} { Nothing }
|
||||
|
||||
|
||||
decl :: { Decl PName }
|
||||
: vars_comma ':' schema { at (head $1,$3) $ DSignature (reverse $1) $3 }
|
||||
| ipat '=' expr { at ($1,$3) $ DPatBind $1 $3 }
|
||||
| '(' op ')' '=' expr { at ($1,$5) $ DPatBind (PVar $2) $5 }
|
||||
| var apats_indices propguards_cases
|
||||
{% mkPropGuardsDecl $1 $2 $3 }
|
||||
| var propguards_cases
|
||||
{% mkConstantPropGuardsDecl $1 $2 }
|
||||
| var apats_indices '=' expr
|
||||
{ at ($1,$4) $ mkIndexedDecl $1 $2 $4 }
|
||||
|
||||
@ -385,6 +388,19 @@ let_decl :: { Decl PName }
|
||||
| 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) }
|
||||
|
||||
|
||||
|
||||
|
||||
propguards_cases :: { [PropGuardCase PName] }
|
||||
: propguards_cases propguards_case { $2 : $1 }
|
||||
| propguards_case { [$1] }
|
||||
|
||||
propguards_case :: { PropGuardCase PName }
|
||||
: '|' propguards_quals '=>' expr { PropGuardCase $2 $4 }
|
||||
|
||||
propguards_quals :: { [Located (Prop PName)] }
|
||||
: type {% mkPropGuards $1 }
|
||||
|
||||
|
||||
newtype :: { Newtype PName }
|
||||
: 'newtype' qname '=' newtype_body
|
||||
{ Newtype $2 [] (thing $4) }
|
||||
|
||||
@ -16,6 +16,7 @@
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
module Cryptol.Parser.AST
|
||||
( -- * Names
|
||||
Ident, mkIdent, mkInfix, isInfixIdent, nullIdent, identText
|
||||
@ -59,6 +60,7 @@ module Cryptol.Parser.AST
|
||||
, ParameterType(..)
|
||||
, ParameterFun(..)
|
||||
, NestedModule(..)
|
||||
, PropGuardCase(..)
|
||||
|
||||
-- * Interactive
|
||||
, ReplInput(..)
|
||||
@ -76,6 +78,7 @@ module Cryptol.Parser.AST
|
||||
, emptyFunDesc
|
||||
, PrefixOp(..)
|
||||
, prefixFixity
|
||||
, asEApps
|
||||
|
||||
-- * Positions
|
||||
, Located(..)
|
||||
@ -280,8 +283,15 @@ type LBindDef = Located (BindDef PName)
|
||||
data BindDef name = DPrim
|
||||
| DForeign
|
||||
| DExpr (Expr name)
|
||||
| DPropGuards [PropGuardCase name]
|
||||
deriving (Eq, Show, Generic, NFData, Functor)
|
||||
|
||||
data PropGuardCase name = PropGuardCase
|
||||
{ pgcProps :: [Located (Prop name)]
|
||||
, pgcExpr :: Expr name
|
||||
}
|
||||
deriving (Eq,Generic,NFData,Functor,Show)
|
||||
|
||||
data Pragma = PragmaNote String
|
||||
| PragmaProperty
|
||||
deriving (Eq, Show, Generic, NFData)
|
||||
@ -728,6 +738,7 @@ instance (Show name, PPName name) => PP (BindDef name) where
|
||||
ppPrec _ DPrim = text "<primitive>"
|
||||
ppPrec _ DForeign = text "<foreign>"
|
||||
ppPrec p (DExpr e) = ppPrec p e
|
||||
ppPrec _p (DPropGuards _guards) = text "propguards"
|
||||
|
||||
|
||||
instance PPName name => PP (TySyn name) where
|
||||
@ -991,6 +1002,8 @@ instance PPName name => PP (Type name) where
|
||||
instance PPName name => PP (Prop name) where
|
||||
ppPrec n (CType t) = ppPrec n t
|
||||
|
||||
instance PPName name => PP [Prop name] where
|
||||
ppPrec n props = parens . commaSep . fmap (ppPrec n) $ props
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Drop all position information, so equality reflects program structure
|
||||
|
||||
130
src/Cryptol/Parser/ExpandPropGuards.hs
Normal file
130
src/Cryptol/Parser/ExpandPropGuards.hs
Normal file
@ -0,0 +1,130 @@
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
|
||||
-- |
|
||||
-- Module : Cryptol.Parser.PropGuards
|
||||
-- Copyright : (c) 2022 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Expands PropGuards into a top-level definition for each case, and rewrites
|
||||
-- the body of each case to be an appropriate call to the respectively generated
|
||||
-- function.
|
||||
module Cryptol.Parser.ExpandPropGuards where
|
||||
|
||||
import Control.DeepSeq
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Data.Text (pack)
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
-- | Monad
|
||||
type ExpandPropGuardsM a = Either Error a
|
||||
|
||||
runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a
|
||||
runExpandPropGuardsM m = m
|
||||
|
||||
-- | Error
|
||||
data Error = NoSignature (Located PName)
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
instance PP Error where
|
||||
ppPrec _ err = case err of
|
||||
NoSignature x ->
|
||||
text "At" <+> pp (srcRange x) <.> colon
|
||||
<+> text "Declarations using constraint guards require an explicit type signature."
|
||||
|
||||
expandPropGuards :: ModuleG m PName -> ExpandPropGuardsM (ModuleG m PName)
|
||||
expandPropGuards m =
|
||||
do mDecls' <- mapM expandTopDecl (mDecls m)
|
||||
pure m {mDecls = concat mDecls' }
|
||||
|
||||
expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
|
||||
expandTopDecl topDecl =
|
||||
case topDecl of
|
||||
Decl topLevelDecl ->
|
||||
do ds <- expandDecl (tlValue topLevelDecl)
|
||||
pure [ Decl topLevelDecl { tlValue = d } | d <- ds ]
|
||||
|
||||
DModule tl | NestedModule m <- tlValue tl ->
|
||||
do m1 <- expandPropGuards m
|
||||
pure [DModule tl { tlValue = NestedModule m1 }]
|
||||
|
||||
_ -> pure [topDecl]
|
||||
|
||||
expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
|
||||
expandDecl decl =
|
||||
case decl of
|
||||
DBind bind -> do bs <- expandBind bind
|
||||
pure (map DBind bs)
|
||||
_ -> pure [decl]
|
||||
|
||||
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
|
||||
expandBind bind =
|
||||
case thing (bDef bind) of
|
||||
DPropGuards guards -> do
|
||||
Forall params props t rng <-
|
||||
case bSignature bind of
|
||||
Just schema -> pure schema
|
||||
Nothing -> Left . NoSignature $ bName bind
|
||||
let goGuard ::
|
||||
PropGuardCase PName ->
|
||||
ExpandPropGuardsM (PropGuardCase PName, Bind PName)
|
||||
goGuard (PropGuardCase props' e) = do
|
||||
bName' <- newName (bName bind) (thing <$> props')
|
||||
-- call to generated function
|
||||
tParams <- case bSignature bind of
|
||||
Just (Forall tps _ _ _) -> pure tps
|
||||
Nothing -> Left $ NoSignature (bName bind)
|
||||
typeInsts <-
|
||||
(\(TParam n _ _) -> Right . PosInst $ TUser n [])
|
||||
`traverse` tParams
|
||||
let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bParams bind)
|
||||
pure
|
||||
( PropGuardCase props' e',
|
||||
bind
|
||||
{ bName = bName',
|
||||
-- include guarded props in signature
|
||||
bSignature = Just (Forall params
|
||||
(props <> map thing props')
|
||||
t rng),
|
||||
-- keeps same location at original bind
|
||||
-- i.e. "on top of" original bind
|
||||
bDef = (bDef bind) {thing = DExpr e}
|
||||
}
|
||||
)
|
||||
(guards', binds') <- unzip <$> mapM goGuard guards
|
||||
pure $
|
||||
bind {bDef = DPropGuards guards' <$ bDef bind} :
|
||||
binds'
|
||||
_ -> pure [bind]
|
||||
|
||||
patternToExpr :: Pattern PName -> Expr PName
|
||||
patternToExpr (PVar locName) = EVar (thing locName)
|
||||
patternToExpr _ =
|
||||
panic "patternToExpr"
|
||||
["Unimplemented: patternToExpr of anything other than PVar"]
|
||||
|
||||
newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)
|
||||
newName locName props =
|
||||
pure case thing locName of
|
||||
Qual modName ident ->
|
||||
let txt = identText ident
|
||||
txt' = pack $ show $ pp props
|
||||
in Qual modName (mkIdent $ txt <> txt') <$ locName
|
||||
UnQual ident ->
|
||||
let txt = identText ident
|
||||
txt' = pack $ show $ pp props
|
||||
in UnQual (mkIdent $ txt <> txt') <$ locName
|
||||
NewName _ _ ->
|
||||
panic "mkName"
|
||||
[ "During expanding prop guards"
|
||||
, "tried to make new name from NewName case of PName"
|
||||
]
|
||||
@ -7,6 +7,7 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Parser.Name where
|
||||
|
||||
@ -33,6 +34,7 @@ data PName = UnQual !Ident
|
||||
-- | Passes that can generate fresh names.
|
||||
data Pass = NoPat
|
||||
| MonoValues
|
||||
| ExpandPropGuards String
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
|
||||
instance NFData PName
|
||||
@ -54,8 +56,9 @@ getIdent (Qual _ n) = n
|
||||
getIdent (NewName p i) = packIdent ("__" ++ pass ++ show i)
|
||||
where
|
||||
pass = case p of
|
||||
NoPat -> "p"
|
||||
MonoValues -> "mv"
|
||||
NoPat -> "p"
|
||||
MonoValues -> "mv"
|
||||
ExpandPropGuards _ -> "epg"
|
||||
|
||||
isGeneratedName :: PName -> Bool
|
||||
isGeneratedName x =
|
||||
|
||||
@ -9,6 +9,8 @@
|
||||
-- This module defines the scoping rules for value- and type-level
|
||||
-- names in Cryptol.
|
||||
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Parser.Names
|
||||
( tnamesNT
|
||||
, tnamesT
|
||||
@ -65,6 +67,7 @@ namesDef :: Ord name => BindDef name -> Set name
|
||||
namesDef DPrim = Set.empty
|
||||
namesDef DForeign = Set.empty
|
||||
namesDef (DExpr e) = namesE e
|
||||
namesDef (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards)
|
||||
|
||||
|
||||
-- | The names used by an expression.
|
||||
@ -186,6 +189,11 @@ tnamesDef :: Ord name => BindDef name -> Set name
|
||||
tnamesDef DPrim = Set.empty
|
||||
tnamesDef DForeign = Set.empty
|
||||
tnamesDef (DExpr e) = tnamesE e
|
||||
tnamesDef (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)
|
||||
|
||||
tnamesPropGuardCase :: Ord name => PropGuardCase name -> Set name
|
||||
tnamesPropGuardCase c =
|
||||
Set.unions (tnamesE (pgcExpr c) : map (tnamesC . thing) (pgcProps c))
|
||||
|
||||
-- | The type names used by an expression.
|
||||
tnamesE :: Ord name => Expr name -> Set name
|
||||
|
||||
@ -228,6 +228,20 @@ noMatchB b =
|
||||
do e' <- noPatFun (Just (thing (bName b))) 0 (bParams b) e
|
||||
return b { bParams = [], bDef = DExpr e' <$ bDef b }
|
||||
|
||||
DPropGuards guards ->
|
||||
do let nm = thing (bName b)
|
||||
ps = bParams b
|
||||
gs <- mapM (noPatPropGuardCase nm ps) guards
|
||||
pure b { bParams = [], bDef = DPropGuards gs <$ bDef b }
|
||||
|
||||
noPatPropGuardCase ::
|
||||
PName ->
|
||||
[Pattern PName] ->
|
||||
PropGuardCase PName -> NoPatM (PropGuardCase PName)
|
||||
noPatPropGuardCase f xs pc =
|
||||
do e <- noPatFun (Just f) 0 xs (pgcExpr pc)
|
||||
pure pc { pgcExpr = e }
|
||||
|
||||
noMatchD :: Decl PName -> NoPatM [Decl PName]
|
||||
noMatchD decl =
|
||||
case decl of
|
||||
|
||||
@ -609,6 +609,35 @@ mkIndexedDecl f (ps, ixs) e =
|
||||
rhs :: Expr PName
|
||||
rhs = mkGenerate (reverse ixs) e
|
||||
|
||||
-- NOTE: The lists of patterns are reversed!
|
||||
mkPropGuardsDecl ::
|
||||
LPName ->
|
||||
([Pattern PName], [Pattern PName]) ->
|
||||
[PropGuardCase PName] ->
|
||||
ParseM (Decl PName)
|
||||
mkPropGuardsDecl f (ps, ixs) guards =
|
||||
do unless (null ixs) $
|
||||
errorMessage (srcRange f)
|
||||
["Indexed sequence definitions may not use constraint guards"]
|
||||
let gs = reverse guards
|
||||
pure $
|
||||
DBind Bind { bName = f
|
||||
, bParams = reverse ps
|
||||
, bDef = Located (srcRange f) (DPropGuards gs)
|
||||
, bSignature = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = False
|
||||
, bInfix = False
|
||||
, bFixity = Nothing
|
||||
, bDoc = Nothing
|
||||
, bExport = Public
|
||||
}
|
||||
|
||||
mkConstantPropGuardsDecl ::
|
||||
LPName -> [PropGuardCase PName] -> ParseM (Decl PName)
|
||||
mkConstantPropGuardsDecl f guards =
|
||||
mkPropGuardsDecl f ([],[]) guards
|
||||
|
||||
-- NOTE: The lists of patterns are reversed!
|
||||
mkIndexedExpr :: ([Pattern PName], [Pattern PName]) -> Expr PName -> Expr PName
|
||||
mkIndexedExpr (ps, ixs) body
|
||||
@ -768,6 +797,10 @@ distrLoc :: Located [a] -> [Located a]
|
||||
distrLoc x = [ Located { srcRange = r, thing = a } | a <- thing x ]
|
||||
where r = srcRange x
|
||||
|
||||
mkPropGuards :: Type PName -> ParseM [Located (Prop PName)]
|
||||
mkPropGuards ty =
|
||||
do lp <- mkProp ty
|
||||
pure [ lp { thing = p } | p <- thing lp ]
|
||||
|
||||
mkProp :: Type PName -> ParseM (Located [Prop PName])
|
||||
mkProp ty =
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.Parser.Token where
|
||||
|
||||
import Data.Text(Text)
|
||||
|
||||
@ -10,6 +10,7 @@
|
||||
-- from previous Cryptol versions.
|
||||
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Parser.Utils
|
||||
( translateExprToNumT
|
||||
|
||||
@ -1536,23 +1536,16 @@ liftModuleCmd cmd =
|
||||
}
|
||||
moduleCmdResult =<< io (cmd minp)
|
||||
|
||||
-- TODO: add filter for my exhaustie prop guards warning here
|
||||
|
||||
moduleCmdResult :: M.ModuleRes a -> REPL a
|
||||
moduleCmdResult (res,ws0) = do
|
||||
warnDefaulting <- getKnownUser "warnDefaulting"
|
||||
warnShadowing <- getKnownUser "warnShadowing"
|
||||
warnPrefixAssoc <- getKnownUser "warnPrefixAssoc"
|
||||
warnNonExhConGrds <- getKnownUser "warnNonExhaustiveConstraintGuards"
|
||||
-- XXX: let's generalize this pattern
|
||||
let isDefaultWarn (T.DefaultingTo _ _) = True
|
||||
isDefaultWarn _ = False
|
||||
|
||||
filterDefaults w | warnDefaulting = Just w
|
||||
filterDefaults (M.TypeCheckWarnings nameMap xs) =
|
||||
case filter (not . isDefaultWarn . snd) xs of
|
||||
[] -> Nothing
|
||||
ys -> Just (M.TypeCheckWarnings nameMap ys)
|
||||
filterDefaults w = Just w
|
||||
|
||||
isShadowWarn (M.SymbolShadowed {}) = True
|
||||
let isShadowWarn (M.SymbolShadowed {}) = True
|
||||
isShadowWarn _ = False
|
||||
|
||||
isPrefixAssocWarn (M.PrefixAssocChanged {}) = True
|
||||
@ -1565,9 +1558,23 @@ moduleCmdResult (res,ws0) = do
|
||||
ys -> Just (M.RenamerWarnings ys)
|
||||
filterRenamer _ _ w = Just w
|
||||
|
||||
let ws = mapMaybe filterDefaults
|
||||
. mapMaybe (filterRenamer warnShadowing isShadowWarn)
|
||||
-- ignore certain warnings during typechecking
|
||||
filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning
|
||||
filterTypecheck (M.TypeCheckWarnings nameMap xs) =
|
||||
case filter (allow . snd) xs of
|
||||
[] -> Nothing
|
||||
ys -> Just (M.TypeCheckWarnings nameMap ys)
|
||||
where
|
||||
allow :: T.Warning -> Bool
|
||||
allow = \case
|
||||
T.DefaultingTo _ _ | not warnDefaulting -> False
|
||||
T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False
|
||||
_ -> True
|
||||
filterTypecheck w = Just w
|
||||
|
||||
let ws = mapMaybe (filterRenamer warnShadowing isShadowWarn)
|
||||
. mapMaybe (filterRenamer warnPrefixAssoc isPrefixAssocWarn)
|
||||
. mapMaybe filterTypecheck
|
||||
$ ws0
|
||||
names <- M.mctxNameDisp <$> getFocusedEnv
|
||||
mapM_ (rPrint . runDoc names . pp) ws
|
||||
|
||||
@ -902,6 +902,8 @@ userOptions = mkOptionMap
|
||||
"Choose whether to display warnings when expression association has changed due to new prefix operator fixities."
|
||||
, simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck
|
||||
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
|
||||
, simpleOpt "warnNonExhaustiveConstraintGuards" ["warn-nonexhaustive-constraintguards"] (EnvBool True) noCheck
|
||||
"Choose whether to issue a warning when a use of constraint guards is not determined to be exhaustive."
|
||||
, simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
|
||||
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
|
||||
, OptionDescr "path" [] (EnvString "") noCheck
|
||||
|
||||
@ -17,6 +17,7 @@ import Cryptol.ModuleSystem.Name(toParamInstName,asParamName,nameIdent
|
||||
,paramModRecParam)
|
||||
import Cryptol.Utils.Ident(paramInstModName)
|
||||
import Cryptol.Utils.RecordMap(recordFromFields)
|
||||
import Data.Bifunctor (Bifunctor(second))
|
||||
|
||||
{-
|
||||
Note that we have to be careful when doing this transformation on
|
||||
@ -258,6 +259,7 @@ instance Inst Expr where
|
||||
_ -> EProofApp (inst ps e1)
|
||||
|
||||
EWhere e dgs -> EWhere (inst ps e) (inst ps dgs)
|
||||
EPropGuards guards ty -> EPropGuards (second (inst ps) <$> guards) ty
|
||||
|
||||
|
||||
instance Inst Match where
|
||||
|
||||
@ -201,6 +201,8 @@ rewE rews = go
|
||||
EWhere e dgs -> EWhere <$> go e <*> inLocal
|
||||
(mapM (rewDeclGroup rews) dgs)
|
||||
|
||||
EPropGuards guards ty -> EPropGuards <$> (\(props, e) -> (,) <$> pure props <*> go e) `traverse` guards <*> pure ty
|
||||
|
||||
|
||||
rewM :: RewMap -> Match -> M Match
|
||||
rewM rews ma =
|
||||
|
||||
@ -19,12 +19,16 @@ import qualified Cryptol.ModuleSystem as M
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
import qualified Cryptol.ModuleSystem.Monad as M
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Eval (checkProp)
|
||||
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe (catMaybes)
|
||||
import qualified Data.List as List
|
||||
|
||||
import MonadLib hiding (mapM)
|
||||
import Cryptol.ModuleSystem.Base (getPrimMap)
|
||||
|
||||
|
||||
-- Specializer Monad -----------------------------------------------------------
|
||||
|
||||
@ -102,6 +106,16 @@ specializeExpr expr =
|
||||
EProofAbs p e -> EProofAbs p <$> specializeExpr e
|
||||
EProofApp {} -> specializeConst expr
|
||||
EWhere e dgs -> specializeEWhere e dgs
|
||||
-- The type should be monomorphic, and the guarded expressions should
|
||||
-- already be normalized, so we just need to choose the first expression
|
||||
-- that's true.
|
||||
EPropGuards guards ty ->
|
||||
case List.find (all checkProp . fst) guards of
|
||||
Just (_, e) -> specializeExpr e
|
||||
Nothing -> do
|
||||
pm <- liftSpecT getPrimMap
|
||||
pure $ eError pm ty "no constraint guard was satisfied"
|
||||
|
||||
|
||||
specializeMatch :: Match -> SpecM Match
|
||||
specializeMatch (From qn l t e) = From qn l t <$> specializeExpr e
|
||||
|
||||
@ -150,6 +150,8 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements)
|
||||
|
||||
| EWhere Expr [DeclGroup]
|
||||
|
||||
| EPropGuards [([Prop], Expr)] Type
|
||||
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
|
||||
@ -268,6 +270,12 @@ instance PP (WithNames Expr) where
|
||||
, hang "where" 2 (vcat (map ppW ds))
|
||||
]
|
||||
|
||||
EPropGuards guards _ ->
|
||||
parens (text "propguards" <+> vsep (ppGuard <$> guards))
|
||||
where ppGuard (props, e) = indent 1
|
||||
$ pipe <+> commaSep (ppW <$> props)
|
||||
<+> text "=>" <+> ppW e
|
||||
|
||||
where
|
||||
ppW x = ppWithNames nm x
|
||||
ppWP x = ppWithNamesPrec nm x
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.TypeCheck.Default where
|
||||
|
||||
import qualified Data.Set as Set
|
||||
|
||||
@ -68,6 +68,7 @@ subsumes _ _ = False
|
||||
data Warning = DefaultingKind (P.TParam Name) P.Kind
|
||||
| DefaultingWildType P.Kind
|
||||
| DefaultingTo !TVarInfo Type
|
||||
| NonExhaustivePropGuards Name
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Various errors that might happen during type checking/inference
|
||||
@ -151,6 +152,16 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
|
||||
| UnsupportedFFIType TypeSource FFITypeError
|
||||
-- ^ Type is not supported for FFI
|
||||
|
||||
| NestedConstraintGuard Ident
|
||||
-- ^ Constraint guards may only apper at the top-level
|
||||
|
||||
| DeclarationRequiresSignatureCtrGrd Ident
|
||||
-- ^ All declarataions in a recursive group involving
|
||||
-- constraint guards should have signatures
|
||||
|
||||
| InvalidConstraintGuard Prop
|
||||
-- ^ The given constraint may not be used as a constraint guard
|
||||
|
||||
| TemporaryError Doc
|
||||
-- ^ This is for errors that don't fit other cateogories.
|
||||
-- We should not use it much, and is generally to be used
|
||||
@ -211,6 +222,10 @@ errorImportance err =
|
||||
UnsupportedFFIType {} -> 7
|
||||
-- less than UnexpectedTypeWildCard
|
||||
|
||||
NestedConstraintGuard {} -> 10
|
||||
DeclarationRequiresSignatureCtrGrd {} -> 9
|
||||
InvalidConstraintGuard {} -> 5
|
||||
|
||||
|
||||
instance TVars Warning where
|
||||
apSubst su warn =
|
||||
@ -218,6 +233,7 @@ instance TVars Warning where
|
||||
DefaultingKind {} -> warn
|
||||
DefaultingWildType {} -> warn
|
||||
DefaultingTo d ty -> DefaultingTo d $! (apSubst su ty)
|
||||
NonExhaustivePropGuards {} -> warn
|
||||
|
||||
instance FVS Warning where
|
||||
fvs warn =
|
||||
@ -225,6 +241,7 @@ instance FVS Warning where
|
||||
DefaultingKind {} -> Set.empty
|
||||
DefaultingWildType {} -> Set.empty
|
||||
DefaultingTo _ ty -> fvs ty
|
||||
NonExhaustivePropGuards {} -> Set.empty
|
||||
|
||||
instance TVars Error where
|
||||
apSubst su err =
|
||||
@ -262,6 +279,10 @@ instance TVars Error where
|
||||
UnsupportedFFIKind {} -> err
|
||||
UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
|
||||
|
||||
NestedConstraintGuard {} -> err
|
||||
DeclarationRequiresSignatureCtrGrd {} -> err
|
||||
InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p
|
||||
|
||||
TemporaryError {} -> err
|
||||
|
||||
|
||||
@ -300,6 +321,10 @@ instance FVS Error where
|
||||
UnsupportedFFIKind {} -> Set.empty
|
||||
UnsupportedFFIType _ t -> fvs t
|
||||
|
||||
NestedConstraintGuard {} -> Set.empty
|
||||
DeclarationRequiresSignatureCtrGrd {} -> Set.empty
|
||||
InvalidConstraintGuard p -> fvs p
|
||||
|
||||
TemporaryError {} -> Set.empty
|
||||
|
||||
instance PP Warning where
|
||||
@ -323,6 +348,10 @@ instance PP (WithNames Warning) where
|
||||
text "Defaulting" <+> pp (tvarDesc d) <+> text "to"
|
||||
<+> ppWithNames names ty
|
||||
|
||||
NonExhaustivePropGuards n ->
|
||||
text "Could not prove that the constraint guards used in defining" <+>
|
||||
pp n <+> text "were exhaustive."
|
||||
|
||||
instance PP (WithNames Error) where
|
||||
ppPrec _ (WithNames err names) =
|
||||
case err of
|
||||
@ -337,8 +366,13 @@ instance PP (WithNames Error) where
|
||||
|
||||
UnexpectedTypeWildCard ->
|
||||
addTVarsDescsAfter names err $
|
||||
nested "Wild card types are not allowed in this context"
|
||||
"(e.g., they cannot be used in type synonyms or FFI declarations)."
|
||||
nested "Wild card types are not allowed in this context" $
|
||||
vcat [ "They cannot be used in:"
|
||||
, bullets [ "type synonyms"
|
||||
, "FFI declarations"
|
||||
, "declarations with constraint guards"
|
||||
]
|
||||
]
|
||||
|
||||
KindMismatch mbsrc k1 k2 ->
|
||||
addTVarsDescsAfter names err $
|
||||
@ -484,6 +518,27 @@ instance PP (WithNames Error) where
|
||||
[ ppWithNames names t
|
||||
, "When checking" <+> pp src ]
|
||||
|
||||
NestedConstraintGuard d ->
|
||||
vcat [ "Local declaration" <+> backticks (pp d)
|
||||
<+> "may not use constraint guards."
|
||||
, "Constraint guards may only appear at the top-level of a module."
|
||||
]
|
||||
|
||||
DeclarationRequiresSignatureCtrGrd d ->
|
||||
vcat [ "The declaration of" <+> backticks (pp d) <+>
|
||||
"requires a full type signature,"
|
||||
, "because it is part of a recursive group with constraint guards."
|
||||
]
|
||||
|
||||
InvalidConstraintGuard p ->
|
||||
let d = case tNoUser p of
|
||||
TCon tc _ -> pp tc
|
||||
_ -> ppWithNames names p
|
||||
in
|
||||
vcat [ backticks d <+> "may not be used in a constraint guard."
|
||||
, "Constraint guards support only numeric comparisons and `fin`."
|
||||
]
|
||||
|
||||
TemporaryError doc -> doc
|
||||
where
|
||||
bullets xs = vcat [ "•" <+> d | d <- xs ]
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
-- | Checking and conversion of 'Type's to 'FFIType's.
|
||||
module Cryptol.TypeCheck.FFI
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
-- | Errors from typechecking foreign functions.
|
||||
module Cryptol.TypeCheck.FFI.Error where
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
-- | This module defines a nicer intermediate representation of Cryptol types
|
||||
-- allowed for the FFI, which the typechecker generates then stores in the AST.
|
||||
|
||||
@ -15,8 +15,13 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
-- {-# LANGUAGE Trustworthy #-}
|
||||
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
|
||||
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
|
||||
{-# HLINT ignore "Redundant <$>" #-}
|
||||
{-# HLINT ignore "Redundant <&>" #-}
|
||||
module Cryptol.TypeCheck.Infer
|
||||
( checkE
|
||||
, checkSigB
|
||||
@ -30,7 +35,7 @@ import Data.Text(Text)
|
||||
import qualified Data.Text as Text
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc)
|
||||
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc, nameIdent)
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import qualified Cryptol.ModuleSystem.Exports as P
|
||||
@ -43,7 +48,8 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
|
||||
checkPropSyn,checkNewtype,
|
||||
checkParameterType,
|
||||
checkPrimType,
|
||||
checkParameterConstraints)
|
||||
checkParameterConstraints,
|
||||
checkPropGuards)
|
||||
import Cryptol.TypeCheck.Instantiate
|
||||
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
|
||||
import Cryptol.TypeCheck.Unify(rootPath)
|
||||
@ -52,20 +58,22 @@ import Cryptol.TypeCheck.FFI.FFIType
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.RecordMap
|
||||
import Cryptol.Utils.PP (pp)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Set as Set
|
||||
import Data.List(foldl',sortBy,groupBy)
|
||||
import Data.List(foldl', sortBy, groupBy, partition)
|
||||
import Data.Either(partitionEithers)
|
||||
import Data.Maybe(isJust, fromMaybe, mapMaybe)
|
||||
import Data.List(partition)
|
||||
import Data.Ratio(numerator,denominator)
|
||||
import Data.Traversable(forM)
|
||||
import Data.Function(on)
|
||||
import Control.Monad(zipWithM,unless,foldM,forM_,mplus,when)
|
||||
|
||||
import Control.Monad(zipWithM, unless, foldM, forM_, mplus, zipWithM,
|
||||
unless, foldM, forM_, mplus, when)
|
||||
|
||||
-- import Debug.Trace
|
||||
-- import Cryptol.TypeCheck.PP
|
||||
|
||||
inferModule :: P.Module Name -> InferM Module
|
||||
inferModule m =
|
||||
@ -733,15 +741,18 @@ inferCArm armNum (m : ms) =
|
||||
newGoals CtComprehension [ pFin n' ]
|
||||
return (m1 : ms', Map.insertWith (\_ old -> old) x t ds, tMul n n')
|
||||
|
||||
-- | @inferBinds isTopLevel isRec binds@ performs inference for a
|
||||
-- strongly-connected component of 'P.Bind's.
|
||||
-- If any of the members of the recursive group are already marked
|
||||
-- as monomorphic, then we don't do generalization.
|
||||
-- If @isTopLevel@ is true,
|
||||
-- any bindings without type signatures will be generalized. If it is
|
||||
-- false, and the mono-binds flag is enabled, no bindings without type
|
||||
-- signatures will be generalized, but bindings with signatures will
|
||||
-- be unaffected.
|
||||
{- | @inferBinds isTopLevel isRec binds@ performs inference for a
|
||||
strongly-connected component of 'P.Bind's.
|
||||
If any of the members of the recursive group are already marked
|
||||
as monomorphic, then we don't do generalization.
|
||||
If @isTopLevel@ is true,
|
||||
any bindings without type signatures will be generalized. If it is
|
||||
false, and the mono-binds flag is enabled, no bindings without type
|
||||
signatures will be generalized, but bindings with signatures will
|
||||
be unaffected.
|
||||
|
||||
-}
|
||||
|
||||
inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
|
||||
inferBinds isTopLevel isRec binds =
|
||||
do -- when mono-binds is enabled, and we're not checking top-level
|
||||
@ -789,6 +800,8 @@ inferBinds isTopLevel isRec binds =
|
||||
genCs <- generalize bs1 cs
|
||||
return (done,genCs)
|
||||
|
||||
checkNumericConstraintGuardsOK isTopLevel sigs noSigs
|
||||
|
||||
rec
|
||||
let exprMap = Map.fromList (map monoUse genBs)
|
||||
(doneBs, genBs) <- check exprMap
|
||||
@ -816,6 +829,37 @@ inferBinds isTopLevel isRec binds =
|
||||
withQs = foldl' appP withTys qs
|
||||
|
||||
|
||||
{-
|
||||
Here we also check that:
|
||||
* Numeric constraint guards appear only at the top level
|
||||
* All definitions in a recursive groups with numberic constraint guards
|
||||
have signatures
|
||||
|
||||
The reason is to avoid interference between local constraints coming
|
||||
from the guards and type inference. It might be possible to
|
||||
relex these requirements, but this requires some more careful thought on
|
||||
the interaction between the two, and the effects on pricniple types.
|
||||
-}
|
||||
checkNumericConstraintGuardsOK ::
|
||||
Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()
|
||||
checkNumericConstraintGuardsOK isTopLevel haveSig noSig =
|
||||
do unless isTopLevel
|
||||
(mapM_ (mkErr NestedConstraintGuard) withGuards)
|
||||
unless (null withGuards)
|
||||
(mapM_ (mkErr DeclarationRequiresSignatureCtrGrd) noSig)
|
||||
where
|
||||
mkErr f b =
|
||||
do let nm = P.bName b
|
||||
inRange (srcRange nm) (recordError (f (nameIdent (thing nm))))
|
||||
|
||||
withGuards = filter hasConstraintGuards haveSig
|
||||
-- When desugaring constraint guards we check that they have signatures,
|
||||
-- so no need to look at noSig
|
||||
|
||||
hasConstraintGuards b =
|
||||
case thing (P.bDef b) of
|
||||
P.DPropGuards {} -> True
|
||||
_ -> False
|
||||
|
||||
|
||||
|
||||
@ -836,9 +880,10 @@ guessType exprMap b@(P.Bind { .. }) =
|
||||
|
||||
Just s ->
|
||||
do let wildOk = case thing bDef of
|
||||
P.DForeign {} -> NoWildCards
|
||||
P.DPrim -> NoWildCards
|
||||
P.DExpr {} -> AllowWildCards
|
||||
P.DForeign {} -> NoWildCards
|
||||
P.DPrim -> NoWildCards
|
||||
P.DExpr {} -> AllowWildCards
|
||||
P.DPropGuards {} -> NoWildCards
|
||||
s1 <- checkSchema wildOk s
|
||||
return ((name, ExtVar (fst s1)), Left (checkSigB b s1))
|
||||
|
||||
@ -973,25 +1018,33 @@ checkMonoB b t =
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
P.DPropGuards _ ->
|
||||
tcPanic "checkMonoB"
|
||||
[ "Used constraint guards without a signature at "
|
||||
, show . pp $ P.bName b ]
|
||||
|
||||
-- XXX: Do we really need to do the defaulting business in two different places?
|
||||
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
|
||||
checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
let name = thing (P.bName b) in
|
||||
case thing (P.bDef b) of
|
||||
|
||||
-- XXX what should we do with validSchema in this case?
|
||||
P.DPrim ->
|
||||
do return Decl { dName = thing (P.bName b)
|
||||
, dSignature = Forall as asmps0 t0
|
||||
, dDefinition = DPrim
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
-- XXX what should we do with validSchema in this case?
|
||||
P.DPrim ->
|
||||
return Decl
|
||||
{ dName = name
|
||||
, dSignature = Forall as asmps0 t0
|
||||
, dDefinition = DPrim
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
P.DForeign ->
|
||||
do let loc = getLoc b
|
||||
name = thing $ P.bName b
|
||||
src = DefinitionOf name
|
||||
P.DForeign -> do
|
||||
let loc = getLoc b
|
||||
name' = thing $ P.bName b
|
||||
src = DefinitionOf name'
|
||||
inRangeMb loc do
|
||||
-- Ensure all type params are of kind #
|
||||
forM_ as \a ->
|
||||
@ -1001,8 +1054,8 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
ffiFunType <-
|
||||
case toFFIFunType (Forall as asmps0 t0) of
|
||||
Right (props, ffiFunType) -> ffiFunType <$ do
|
||||
ffiGoals <- traverse (newGoal (CtFFI name)) props
|
||||
proveImplication True (Just name) as asmps0 $
|
||||
ffiGoals <- traverse (newGoal (CtFFI name')) props
|
||||
proveImplication True (Just name') as asmps0 $
|
||||
validSchema ++ ffiGoals
|
||||
Left err -> do
|
||||
recordErrorLoc loc $ UnsupportedFFIType src err
|
||||
@ -1019,54 +1072,198 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
P.DExpr e0 ->
|
||||
inRangeMb (getLoc b) $
|
||||
withTParams as $
|
||||
do (e1,cs0) <- collectGoals $
|
||||
do let nm = thing (P.bName b)
|
||||
tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
|
||||
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
|
||||
addGoals validSchema
|
||||
() <- simplifyAllConstraints -- XXX: using `asmps` also?
|
||||
return e1
|
||||
P.DExpr e0 ->
|
||||
inRangeMb (getLoc b) $
|
||||
withTParams as $ do
|
||||
(t, asmps, e2) <- checkBindDefExpr [] asmps0 e0
|
||||
|
||||
asmps1 <- applySubstPreds asmps0
|
||||
cs <- applySubstGoals cs0
|
||||
return Decl
|
||||
{ dName = name
|
||||
, dSignature = Forall as asmps t
|
||||
, dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
let findKeep vs keep todo =
|
||||
let stays (_,cvs) = not $ Set.null $ Set.intersection vs cvs
|
||||
(yes,perhaps) = partition stays todo
|
||||
(stayPs,newVars) = unzip yes
|
||||
in case stayPs of
|
||||
[] -> (keep,map fst todo)
|
||||
_ -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
|
||||
P.DPropGuards cases0 ->
|
||||
inRangeMb (getLoc b) $
|
||||
withTParams as $ do
|
||||
asmps1 <- applySubstPreds asmps0
|
||||
t1 <- applySubst t0
|
||||
cases1 <- mapM checkPropGuardCase cases0
|
||||
|
||||
let -- if a goal mentions any of these variables, we'll commit to
|
||||
-- solving it now.
|
||||
stickyVars = Set.fromList (map tpVar as) `Set.union` fvs asmps1
|
||||
(stay,leave) = findKeep stickyVars []
|
||||
[ (c, fvs c) | c <- cs ]
|
||||
exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)
|
||||
unless exh $
|
||||
-- didn't prove exhaustive i.e. none of the guarding props
|
||||
-- necessarily hold
|
||||
recordWarning (NonExhaustivePropGuards name)
|
||||
|
||||
addGoals leave
|
||||
let schema = Forall as asmps1 t1
|
||||
|
||||
return Decl
|
||||
{ dName = name
|
||||
, dSignature = schema
|
||||
, dDefinition = DExpr
|
||||
(foldr ETAbs
|
||||
(foldr EProofAbs
|
||||
(EPropGuards cases1 t1)
|
||||
asmps1)
|
||||
as)
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
|
||||
su <- proveImplication False (Just (thing (P.bName b))) as asmps1 stay
|
||||
extendSubst su
|
||||
where
|
||||
|
||||
let asmps = concatMap pSplitAnd (apSubst su asmps1)
|
||||
t <- applySubst t0
|
||||
e2 <- applySubst e1
|
||||
checkBindDefExpr ::
|
||||
[Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)
|
||||
checkBindDefExpr asmpsSign asmps1 e0 = do
|
||||
|
||||
return Decl
|
||||
{ dName = thing (P.bName b)
|
||||
, dSignature = Forall as asmps t
|
||||
, dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
(e1,cs0) <- collectGoals $ do
|
||||
let nm = thing (P.bName b)
|
||||
tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
|
||||
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
|
||||
addGoals validSchema
|
||||
() <- simplifyAllConstraints -- XXX: using `asmps` also?
|
||||
return e1
|
||||
asmps2 <- applySubstPreds asmps1
|
||||
cs <- applySubstGoals cs0
|
||||
|
||||
let findKeep vs keep todo =
|
||||
let stays (_,cvs) = not $ Set.null $ Set.intersection vs cvs
|
||||
(yes,perhaps) = partition stays todo
|
||||
(stayPs,newVars) = unzip yes
|
||||
in case stayPs of
|
||||
[] -> (keep,map fst todo)
|
||||
_ -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
|
||||
|
||||
let -- if a goal mentions any of these variables, we'll commit to
|
||||
-- solving it now.
|
||||
stickyVars = Set.fromList (map tpVar as) `Set.union` fvs asmps2
|
||||
(stay,leave) = findKeep stickyVars []
|
||||
[ (c, fvs c) | c <- cs ]
|
||||
|
||||
addGoals leave
|
||||
|
||||
-- includes asmpsSign for the sake of implication, but doesn't actually
|
||||
-- include them in the resulting asmps
|
||||
su <- proveImplication True (Just (thing (P.bName b))) as (asmpsSign <> asmps2) stay
|
||||
extendSubst su
|
||||
|
||||
let asmps = concatMap pSplitAnd (apSubst su asmps2)
|
||||
t <- applySubst t0
|
||||
e2 <- applySubst e1
|
||||
|
||||
pure (t, asmps, e2)
|
||||
|
||||
|
||||
|
||||
{- |
|
||||
Given a DPropGuards of the form
|
||||
|
||||
@
|
||||
f : {...} A
|
||||
f | (B1, B2) => ...
|
||||
| (C1, C2, C2) => ...
|
||||
@
|
||||
|
||||
we check that it is exhaustive by trying to prove the following
|
||||
implications:
|
||||
|
||||
@
|
||||
A /\ ~B1 => C1 /\ C2 /\ C3
|
||||
A /\ ~B2 => C1 /\ C2 /\ C3
|
||||
@
|
||||
|
||||
The implications were derive by the following general algorithm:
|
||||
- Find that @(C1, C2, C3)@ is the guard that has the most conjuncts, so we
|
||||
will keep it on the RHS of the generated implications in order to minimize
|
||||
the number of implications we need to check.
|
||||
- Negate @(B1, B2)@ which yields @(~B1) \/ (~B2)@. This is a disjunction, so
|
||||
we need to consider a branch for each disjunct --- one branch gets the
|
||||
assumption @~B1@ and another branch gets the assumption @~B2@. Each
|
||||
branch's implications need to be proven independently.
|
||||
|
||||
-}
|
||||
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
|
||||
checkExhaustive name as asmps guards =
|
||||
case sortBy cmpByLonger guards of
|
||||
[] -> pure False -- XXX: we should check the asmps are unsatisfiable
|
||||
longest : rest -> doGoals (theAlts rest) (map toGoal longest)
|
||||
|
||||
where
|
||||
cmpByLonger props1 props2 = compare (length props2) (length props1)
|
||||
-- reversed, so that longets is first
|
||||
|
||||
theAlts :: [[Prop]] -> [[Prop]]
|
||||
theAlts = map concat . sequence . map chooseNeg
|
||||
|
||||
-- Choose one of the things to negate
|
||||
chooseNeg ps =
|
||||
case ps of
|
||||
[] -> []
|
||||
p : qs -> (pNegNumeric p ++ qs) : [ p : alts | alts <- chooseNeg qs ]
|
||||
|
||||
|
||||
|
||||
-- Try to validate all cases
|
||||
doGoals todo gs =
|
||||
case todo of
|
||||
[] -> pure True
|
||||
alt : more ->
|
||||
do ok <- canProve (asmps ++ alt) gs
|
||||
if ok then doGoals more gs
|
||||
else pure False
|
||||
|
||||
toGoal :: Prop -> Goal
|
||||
toGoal prop =
|
||||
Goal
|
||||
{ goalSource = CtPropGuardsExhaustive (thing name)
|
||||
, goalRange = srcRange name
|
||||
, goal = prop
|
||||
}
|
||||
|
||||
canProve :: [Prop] -> [Goal] -> InferM Bool
|
||||
canProve asmps' goals =
|
||||
tryProveImplication (Just (thing name)) as asmps' goals
|
||||
|
||||
{- | This function does not validate anything---it just translates into
|
||||
the type-checkd syntax. The actual validation of the guard will happen
|
||||
when the (automatically generated) function corresponding to the guard is
|
||||
checked, assuming 'ExpandpropGuards' did its job correctly.
|
||||
|
||||
-}
|
||||
checkPropGuardCase :: P.PropGuardCase Name -> InferM ([Prop],Expr)
|
||||
checkPropGuardCase (P.PropGuardCase guards e0) =
|
||||
do ps <- checkPropGuards guards
|
||||
tys <- mapM (`checkType` Nothing) ts
|
||||
let rhsTs = foldl ETApp (getV eV) tys
|
||||
rhsPs = foldl (\e _p -> EProofApp e) rhsTs ps
|
||||
rhs = foldl EApp rhsPs (map getV es)
|
||||
pure (ps,rhs)
|
||||
|
||||
where
|
||||
(e1,es) = P.asEApps e0
|
||||
(eV,ts) = case e1 of
|
||||
P.EAppT ex1 tis -> (ex1, map getT tis)
|
||||
_ -> (e1, [])
|
||||
|
||||
getV ex =
|
||||
case ex of
|
||||
P.EVar x -> EVar x
|
||||
_ -> bad "Expression is not a variable."
|
||||
|
||||
getT ti =
|
||||
case ti of
|
||||
P.PosInst t -> t
|
||||
P.NamedInst {} -> bad "Unexpeceted NamedInst"
|
||||
|
||||
bad msg = panic "checkPropGuardCase" [msg]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -220,6 +220,7 @@ data ConstraintSource
|
||||
| CtImprovement
|
||||
| CtPattern TypeSource -- ^ Constraints arising from type-checking patterns
|
||||
| CtModuleInstance ModName -- ^ Instantiating a parametrized module
|
||||
| CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
|
||||
| CtFFI Name -- ^ Constraints on a foreign declaration required
|
||||
-- by the FFI (e.g. sequences must be finite)
|
||||
deriving (Show, Generic, NFData)
|
||||
@ -249,6 +250,7 @@ instance TVars ConstraintSource where
|
||||
CtImprovement -> src
|
||||
CtPattern _ -> src
|
||||
CtModuleInstance _ -> src
|
||||
CtPropGuardsExhaustive _ -> src
|
||||
CtFFI _ -> src
|
||||
|
||||
|
||||
@ -356,6 +358,7 @@ instance PP ConstraintSource where
|
||||
CtImprovement -> "examination of collected goals"
|
||||
CtPattern ad -> "checking a pattern:" <+> pp ad
|
||||
CtModuleInstance n -> "module instantiation" <+> pp n
|
||||
CtPropGuardsExhaustive n -> "exhaustion check for prop guards used in defining" <+> pp n
|
||||
CtFFI f -> "declaration of foreign function" <+> pp f
|
||||
|
||||
ppUse :: Expr -> Doc
|
||||
|
||||
@ -6,6 +6,7 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
{-# Language OverloadedStrings #-}
|
||||
{-# Language Safe #-}
|
||||
module Cryptol.TypeCheck.Instantiate
|
||||
( instantiateWith
|
||||
, TypeArg(..)
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.TypeCheck.Interface where
|
||||
|
||||
import qualified Data.Map as Map
|
||||
|
||||
@ -7,6 +7,7 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE RecursiveDo #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
|
||||
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
|
||||
@ -19,6 +20,7 @@ module Cryptol.TypeCheck.Kind
|
||||
, checkPropSyn
|
||||
, checkParameterType
|
||||
, checkParameterConstraints
|
||||
, checkPropGuards
|
||||
) where
|
||||
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
@ -40,8 +42,6 @@ import Data.Function(on)
|
||||
import Data.Text (Text)
|
||||
import Control.Monad(unless,when)
|
||||
|
||||
|
||||
|
||||
-- | Check a type signature. Returns validated schema, and any implicit
|
||||
-- constraints that we inferred.
|
||||
checkSchema :: AllowWildCards -> P.Schema Name -> InferM (Schema, [Goal])
|
||||
@ -66,6 +66,30 @@ checkSchema withWild (P.Forall xs ps t mb) =
|
||||
Nothing -> id
|
||||
Just r -> inRange r
|
||||
|
||||
{- | Validate parsed propositions that appear in the guard of a PropGuard.
|
||||
|
||||
* Note that we don't validate the well-formedness constraints here---instead,
|
||||
they'd be validated when the signature for the auto generated
|
||||
function corresponding guard is checked.
|
||||
|
||||
* We also check that there are no wild-cards in the constraints.
|
||||
-}
|
||||
checkPropGuards :: [Located (P.Prop Name)] -> InferM [Prop]
|
||||
checkPropGuards props =
|
||||
do (newPs,_gs) <- collectGoals (mapM check props)
|
||||
pure newPs
|
||||
where
|
||||
check lp =
|
||||
inRange (srcRange lp)
|
||||
do let p = thing lp
|
||||
(_,ps) <- withTParams NoWildCards schemaParam [] (checkProp p)
|
||||
case tNoUser ps of
|
||||
TCon (PC x) _ | x `elem` [PEqual,PNeq,PGeq,PFin,PTrue] -> pure ()
|
||||
_ -> recordError (InvalidConstraintGuard ps)
|
||||
pure ps
|
||||
|
||||
|
||||
|
||||
-- | Check a module parameter declarations. Nothing much to check,
|
||||
-- we just translate from one syntax to another.
|
||||
checkParameterType :: P.ParameterType Name -> Maybe Text -> InferM ModTParam
|
||||
@ -398,7 +422,7 @@ doCheckType ty k =
|
||||
|
||||
-- | Validate a parsed proposition.
|
||||
checkProp :: P.Prop Name -- ^ Proposition that need to be checked
|
||||
-> KindM Type -- ^ Checked representation
|
||||
-> KindM Prop -- ^ Checked representation
|
||||
checkProp (P.CType t) = doCheckType t (Just KProp)
|
||||
|
||||
|
||||
@ -411,5 +435,3 @@ checkKind _ (Just k1) k2
|
||||
| k1 /= k2 = do kRecordError (KindMismatch Nothing k1 k2)
|
||||
kNewType TypeErrorPlaceHolder k1
|
||||
checkKind t _ _ = return t
|
||||
|
||||
|
||||
|
||||
@ -63,6 +63,8 @@ instance ShowParseable Expr where
|
||||
--NOTE: erase all "proofs" for now (change the following two lines to change that)
|
||||
showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
|
||||
showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")"
|
||||
|
||||
showParseable (EPropGuards guards _) = parens (text "EPropGuards" $$ showParseable guards)
|
||||
|
||||
instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
|
||||
showParseable (x,y) = parens (showParseable x <> comma <> showParseable y)
|
||||
|
||||
@ -270,6 +270,9 @@ exprSchema expr =
|
||||
in go dgs
|
||||
|
||||
|
||||
EPropGuards _guards typ ->
|
||||
pure Forall {sVars = [], sProps = [], sType = typ}
|
||||
|
||||
checkHas :: Type -> Selector -> TcM Type
|
||||
checkHas t sel =
|
||||
case sel of
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
|
||||
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
|
||||
module Cryptol.TypeCheck.SimpType where
|
||||
|
||||
@ -11,6 +11,7 @@
|
||||
module Cryptol.TypeCheck.Solve
|
||||
( simplifyAllConstraints
|
||||
, proveImplication
|
||||
, tryProveImplication
|
||||
, proveModuleTopLevel
|
||||
, defaultAndSimplify
|
||||
, defaultReplExpr
|
||||
@ -287,6 +288,25 @@ proveImplication dedupErrs lnam as ps gs =
|
||||
Left errs -> mapM_ recordError errs
|
||||
return su
|
||||
|
||||
-- | Tries to prove an implication. If proved, then returns `Right (m_su ::
|
||||
-- InferM Subst)` where `m_su` is an `InferM` computation that results in the
|
||||
-- solution substitution, and records any warning invoked during proving. If not
|
||||
-- proved, then returns `Left (m_err :: InferM ())`, which records all errors
|
||||
-- invoked during proving.
|
||||
tryProveImplication ::
|
||||
Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
|
||||
tryProveImplication lnam as ps gs =
|
||||
do evars <- varsWithAsmps
|
||||
solver <- getSolver
|
||||
|
||||
extraAs <- (map mtpParam . Map.elems) <$> getParamTypes
|
||||
extra <- map thing <$> getParamConstraints
|
||||
|
||||
(mbErr,_su) <- io (proveImplicationIO solver False lnam evars
|
||||
(extraAs ++ as) (extra ++ ps) gs)
|
||||
case mbErr of
|
||||
Left {} -> pure False
|
||||
Right {} -> pure True
|
||||
|
||||
proveImplicationIO :: Solver
|
||||
-> Bool -- ^ Whether to remove duplicate goals in errors
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
-- | Look for opportunity to solve goals by instantiating variables.
|
||||
module Cryptol.TypeCheck.Solver.Improve where
|
||||
|
||||
|
||||
@ -10,6 +10,7 @@
|
||||
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.TypeCheck.Solver.Numeric.Interval where
|
||||
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.TypeCheck.Solver.Types where
|
||||
|
||||
import Data.Map(Map)
|
||||
|
||||
@ -391,6 +391,8 @@ instance TVars Expr where
|
||||
|
||||
EWhere e ds -> EWhere !$ (go e) !$ (apSubst su ds)
|
||||
|
||||
EPropGuards guards ty -> EPropGuards !$ (\(props, e) -> (apSubst su `fmap'` props, apSubst su e)) `fmap'` guards .$ ty
|
||||
|
||||
instance TVars Match where
|
||||
apSubst su (From x len t e) = From x !$ (apSubst su len) !$ (apSubst su t) !$ (apSubst su e)
|
||||
apSubst su (Let b) = Let !$ (apSubst su b)
|
||||
|
||||
@ -696,7 +696,7 @@ tFun :: Type -> Type -> Type
|
||||
tFun a b = TCon (TC TCFun) [a,b]
|
||||
|
||||
-- | Eliminate outermost type synonyms.
|
||||
tNoUser :: Type -> Type
|
||||
tNoUser :: Type -> Type
|
||||
tNoUser t = case t of
|
||||
TUser _ _ a -> tNoUser a
|
||||
_ -> t
|
||||
@ -847,6 +847,49 @@ pPrime ty =
|
||||
where
|
||||
prop = TCon (PC PPrime) [ty]
|
||||
|
||||
-- Negation --------------------------------------------------------------------
|
||||
|
||||
{-| `pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop
|
||||
over numeric type vars. The result is a conjunction of properties. -}
|
||||
pNegNumeric :: Prop -> [Prop]
|
||||
pNegNumeric prop =
|
||||
case tNoUser prop of
|
||||
TCon tcon tys ->
|
||||
case tcon of
|
||||
PC pc ->
|
||||
case pc of
|
||||
|
||||
-- not (x == y) <=> x /= y
|
||||
PEqual -> [TCon (PC PNeq) tys]
|
||||
|
||||
-- not (x /= y) <=> x == y
|
||||
PNeq -> [TCon (PC PEqual) tys]
|
||||
|
||||
-- not (x >= y) <=> x /= y and y >= x
|
||||
PGeq -> [TCon (PC PNeq) tys, TCon (PC PGeq) (reverse tys)]
|
||||
|
||||
-- not (fin x) <=> x == Inf
|
||||
PFin | [ty] <- tys -> [ty =#= tInf]
|
||||
| otherwise -> bad
|
||||
|
||||
-- not True <=> 0 == 1
|
||||
PTrue -> [TCon (PC PEqual) [tZero, tOne]]
|
||||
|
||||
_ -> bad
|
||||
|
||||
TError _ki -> [prop] -- propogates `TError`
|
||||
|
||||
TC _tc -> bad
|
||||
TF _tf -> bad
|
||||
|
||||
_ -> bad
|
||||
|
||||
where
|
||||
bad = panic "pNegNumeric"
|
||||
[ "Unexpeceted numeric constraint:"
|
||||
, pretty prop
|
||||
]
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -888,10 +931,6 @@ instance FVS Schema where
|
||||
Set.difference (Set.union (fvs ps) (fvs t)) bound
|
||||
where bound = Set.fromList (map tpVar as)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- Pretty Printing -------------------------------------------------------------
|
||||
|
||||
instance PP TParam where
|
||||
|
||||
@ -9,6 +9,7 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
module Cryptol.TypeCheck.TypeOf
|
||||
( fastTypeOf
|
||||
, fastSchemaOf
|
||||
@ -43,6 +44,7 @@ fastTypeOf tyenv expr =
|
||||
Just (_, t) -> t
|
||||
Nothing -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
|
||||
[ "EApp with non-function operator" ]
|
||||
EPropGuards _guards sType -> sType
|
||||
-- Polymorphic fragment
|
||||
EVar {} -> polymorphic
|
||||
ETAbs {} -> polymorphic
|
||||
@ -111,8 +113,11 @@ fastSchemaOf tyenv expr =
|
||||
EComp {} -> monomorphic
|
||||
EApp {} -> monomorphic
|
||||
EAbs {} -> monomorphic
|
||||
|
||||
-- PropGuards
|
||||
EPropGuards _ t -> Forall {sVars = [], sProps = [], sType = t}
|
||||
where
|
||||
monomorphic = Forall [] [] (fastTypeOf tyenv expr)
|
||||
monomorphic = Forall {sVars = [], sProps = [], sType = fastTypeOf tyenv expr}
|
||||
|
||||
-- | Apply a substitution to a type *without* simplifying
|
||||
-- constraints like @Arith [n]a@ to @Arith a@. (This is in contrast to
|
||||
|
||||
@ -1,5 +1,6 @@
|
||||
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns]
|
||||
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
module Cryptol.TypeCheck.TypePat
|
||||
( aInf, aNat, aNat'
|
||||
|
||||
|
||||
@ -8,6 +8,7 @@
|
||||
|
||||
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Utils.Ident
|
||||
( -- * Module names
|
||||
|
||||
@ -337,6 +337,8 @@ comma = liftPP PP.comma
|
||||
colon :: Doc
|
||||
colon = liftPP PP.colon
|
||||
|
||||
pipe :: Doc
|
||||
pipe = liftPP PP.pipe
|
||||
instance PP T.Text where
|
||||
ppPrec _ str = text (T.unpack str)
|
||||
|
||||
|
||||
@ -14,6 +14,7 @@
|
||||
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Utils.RecordMap
|
||||
( RecordMap
|
||||
|
||||
@ -7,7 +7,6 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Version (
|
||||
commitHash
|
||||
|
||||
36
tests/constraint-guards/constant.cry
Normal file
36
tests/constraint-guards/constant.cry
Normal file
@ -0,0 +1,36 @@
|
||||
isZero : {n : #} Bit
|
||||
isZero | n == 0 => True
|
||||
| () => False
|
||||
|
||||
property isZero_correct =
|
||||
~isZero `{inf} &&
|
||||
isZero `{ 0} &&
|
||||
~isZero `{ 1} &&
|
||||
~isZero `{ 2} &&
|
||||
~isZero `{ 4} &&
|
||||
~isZero `{ 8} &&
|
||||
~isZero `{ 16}
|
||||
|
||||
isFin : {n : #} Bit
|
||||
isFin | fin n => True
|
||||
| () => False
|
||||
|
||||
property isFin_correct =
|
||||
~isFin `{inf} &&
|
||||
isFin `{ 0} &&
|
||||
isFin `{ 1} &&
|
||||
isFin `{ 2} &&
|
||||
isFin `{ 4} &&
|
||||
isFin `{ 8} &&
|
||||
isFin `{ 16}
|
||||
|
||||
idTypeNum : {n : #} Integer
|
||||
idTypeNum | fin n => `n
|
||||
|
||||
property idTypeNum_correct =
|
||||
(idTypeNum `{ 0} == 0) &&
|
||||
(idTypeNum `{ 1} == 1) &&
|
||||
(idTypeNum `{ 2} == 2) &&
|
||||
(idTypeNum `{ 4} == 4) &&
|
||||
(idTypeNum `{ 8} == 8) &&
|
||||
(idTypeNum `{16} == 16)
|
||||
3
tests/constraint-guards/constant.icry
Normal file
3
tests/constraint-guards/constant.icry
Normal file
@ -0,0 +1,3 @@
|
||||
:l constant.cry
|
||||
|
||||
:check
|
||||
18
tests/constraint-guards/constant.icry.stdout
Normal file
18
tests/constraint-guards/constant.icry.stdout
Normal file
@ -0,0 +1,18 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at constant.cry:1:11--1:16
|
||||
Unused name: n
|
||||
[warning] at constant.cry:14:10--14:15
|
||||
Unused name: n
|
||||
[warning] at constant.cry:28:1--28:10:
|
||||
Could not prove that the constraint guards used in defining Main::idTypeNum were exhaustive.
|
||||
property isZero_correct Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
property isFin_correct Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
property idTypeNum_correct Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
31
tests/constraint-guards/inits.cry
Normal file
31
tests/constraint-guards/inits.cry
Normal file
@ -0,0 +1,31 @@
|
||||
// ys | zs | acc
|
||||
// ––––––––+–-–––––––+–––––––––––
|
||||
// [1,2,3] | [] | []
|
||||
// [2,3] | [1] | [1]
|
||||
// [3] | [1,2] | [1,1,2]
|
||||
// [] | [1,2,3] | [1,1,2,1,2,3]
|
||||
|
||||
inits : {n, a} (fin n) => [n]a -> [(n * (n+1))/2]a
|
||||
inits xs
|
||||
| n == 0 => []
|
||||
| n > 0 => initsLoop xs' x []
|
||||
where
|
||||
(x : [1]_) # xs' = xs
|
||||
|
||||
initsLoop : {n, l, m, a} (fin l, fin m, l + m == n, m >= 1) =>
|
||||
[l]a -> [m]a ->
|
||||
[((m-1) * ((m-1)+1))/2]a ->
|
||||
[(n * (n+1))/2]a
|
||||
initsLoop ys zs acc
|
||||
| l == 0 => acc # zs
|
||||
| l > 0 => initsLoop ys' (zs # y) (acc # zs)
|
||||
where (y : [1]_) # ys' = ys
|
||||
|
||||
|
||||
property inits_correct =
|
||||
(inits [] == []) &&
|
||||
(inits [1] == [1]) &&
|
||||
(inits [1,2] == [1,1,2]) &&
|
||||
(inits [1,2,3] == [1,1,2,1,2,3]) &&
|
||||
(inits [1,2,3,4] == [1,1,2,1,2,3,1,2,3,4]) &&
|
||||
(inits [1,2,3,4,5] == [1,1,2,1,2,3,1,2,3,4,1,2,3,4,5])
|
||||
2
tests/constraint-guards/inits.icry
Normal file
2
tests/constraint-guards/inits.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:l inits.cry
|
||||
:check inits_correct
|
||||
8
tests/constraint-guards/inits.icry.stdout
Normal file
8
tests/constraint-guards/inits.icry.stdout
Normal file
@ -0,0 +1,8 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Showing a specific instance of polymorphic result:
|
||||
* Using 'Integer' for type of sequence member
|
||||
Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
28
tests/constraint-guards/insert.cry
Normal file
28
tests/constraint-guards/insert.cry
Normal file
@ -0,0 +1,28 @@
|
||||
// assumes that `xs` is sorted
|
||||
insert : {n, a} (fin n, Cmp a) => a -> [n]a -> [n+1]a
|
||||
insert x' xs
|
||||
| n == 0 => [x']
|
||||
| n == 1 => if x' <= x then [x', x] else [x, x']
|
||||
where [x] = xs
|
||||
| ( n % 2 == 0
|
||||
, n > 1 ) => if x' <= x
|
||||
then insert x' (xs1 # [x]) # xs2
|
||||
else xs1 # [x] # insert x' xs2
|
||||
where (xs1 : [n/2 - 1]_) # [x] # (xs2 : [n/2]_) = xs
|
||||
| ( n % 2 == 1
|
||||
, n > 1 ) => if x' <= x
|
||||
then insert x' (xs1 # [x]) # xs2
|
||||
else xs1 # [x] # insert x' xs2
|
||||
where (xs1 : [n/2]_) # [x] # (xs2 : [n/2]_) = xs
|
||||
|
||||
property insert_correct =
|
||||
(insert 0 [ 1,2,3,4,5,6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 1 [0, 2,3,4,5,6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 2 [0,1, 3,4,5,6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 3 [0,1,2, 4,5,6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 4 [0,1,2,3, 5,6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 5 [0,1,2,3,4, 6,7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 6 [0,1,2,3,4,5, 7,8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 7 [0,1,2,3,4,5,6, 8,9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 8 [0,1,2,3,4,5,6,7, 9] == [0,1,2,3,4,5,6,7,8,9]) &&
|
||||
(insert 9 [0,1,2,3,4,5,6,7,8 ] == [0,1,2,3,4,5,6,7,8,9])
|
||||
2
tests/constraint-guards/insert.icry
Normal file
2
tests/constraint-guards/insert.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:l insert.cry
|
||||
:check insert_correct
|
||||
6
tests/constraint-guards/insert.icry.stdout
Normal file
6
tests/constraint-guards/insert.icry.stdout
Normal file
@ -0,0 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
17
tests/constraint-guards/len.cry
Normal file
17
tests/constraint-guards/len.cry
Normal file
@ -0,0 +1,17 @@
|
||||
len : {n,a} (fin n) => [n] a -> Integer
|
||||
len x
|
||||
| (n == 0) => 0
|
||||
| (n > 0) => 1 + len (drop`{1} x)
|
||||
|
||||
|
||||
property
|
||||
len_correct = and
|
||||
[ len l == length l where l = []
|
||||
, len l == length l where l = [1]
|
||||
, len l == length l where l = [1,2]
|
||||
, len l == length l where l = [1,2,3]
|
||||
, len l == length l where l = [1,2,3,4,5]
|
||||
, len l == length l where l = [1,2,3,4,5,6]
|
||||
, len l == length l where l = [1,2,3,4,5,6,7]
|
||||
, len l == length l where l = [1,2,3,4,5,6,7,8]
|
||||
]
|
||||
2
tests/constraint-guards/len.icry
Normal file
2
tests/constraint-guards/len.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:l len.cry
|
||||
:check len_correct
|
||||
6
tests/constraint-guards/len.icry.stdout
Normal file
6
tests/constraint-guards/len.icry.stdout
Normal file
@ -0,0 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Using exhaustive testing.
|
||||
Testing... Passed 1 tests.
|
||||
Q.E.D.
|
||||
28
tests/constraint-guards/mergesort.cry
Normal file
28
tests/constraint-guards/mergesort.cry
Normal file
@ -0,0 +1,28 @@
|
||||
sort : {n,a} Cmp a => (fin n) => [n]a -> [n]a
|
||||
sort xs
|
||||
| n <= 1 => xs
|
||||
| () => merge (sort left) (sort right)
|
||||
where (left : [n/2] _) # right = xs
|
||||
|
||||
merge : {m,n,a} Cmp a => [m]a -> [n]a -> [m+n]a
|
||||
merge xs ys
|
||||
| m == 0 => ys
|
||||
| n == 0 => xs
|
||||
| (m > 0, n > 0) => if x <= y
|
||||
then [x] # merge restX ys
|
||||
else [y] # merge xs restY
|
||||
where
|
||||
[x] # restX = xs
|
||||
[y] # restY = ys
|
||||
|
||||
|
||||
property sort_correct =
|
||||
(sort [] == []) &&
|
||||
(sort [0] == [0]) &&
|
||||
(sort [-6, 1, 9, -3, -9, 2, 4] == [-9, -6, -3, 1, 2, 4, 9]) &&
|
||||
(sort [4, -8, -1, -7, -5, 9, 8, 8] == [-8, -7, -5, -1, 4, 8, 8, 9]) &&
|
||||
(sort [1, -1, -2, -3, -2, 7, 5] == [-3, -2, -2, -1, 1, 5, 7]) &&
|
||||
(sort [9, 9, 8, -3, 1, 1, -6, -6, -8] == [-8, -6, -6, -3, 1, 1, 8, 9, 9]) &&
|
||||
(sort [9, 1, 5, 0] == [0, 1, 5, 9]) &&
|
||||
(sort [8, 3, 3] == [3, 3, 8]) &&
|
||||
(sort [-7, 8] == [-7, 8])
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user