Numeric Constraint Guards

.gitignore

@@ -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

CHANGES.md

@@ -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.

ConditionalConstraints.md

@@ -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.

cryptol-remote-api/src/CryptolServer/Exceptions.hs

@@ -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)

cryptol.cabal

@@ -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,

docs/RefMan/BasicSyntax.rst

@@ -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
 ------

docs/RefMan/_build/html/.buildinfo

@@ -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

docs/RefMan/_build/html/BasicSyntax.html

@@ -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">=&gt;</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">=&gt;</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">-&gt;</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">=&gt;</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">&gt;</span><span class="w">  </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</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&#39;</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">=&gt;</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">-&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
+<span class="nf">len&#39;</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">=&gt;</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">&gt;</span><span class="w">  </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</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">&gt;=</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">&gt;</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">&gt;=</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">&lt;=</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 @@ <h2>Layout<a class="headerlink" href="#layout" title="Permalink to this heading"
 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 @@ <h2>Comments<a class="headerlink" href="#comments" title="Permalink to this head
 </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 @@ <h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to thi
 </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 @@ <h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-bui
 </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 @@ <h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-leve
 </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