Improve rewriter speed

Andres and I met yesterday, and discovered that there's a source of
non-linear complexity in the rewriter which is not type casts.

In adding side-conditions to the rewrite rules (which are not discussed
in the pattern-matching compilation paper), I represented them by
allowing rewrite rules to fail.  So, for example,

    # + x ~~> x (when # == 0)

is represented as

    # + x ~~> if (# =? 0) then Some x else None

In the case that a rewrite rule fails, we need to try all other rewrite
rules that might still apply.  However, doing this in the naive-CPS way
leads to non-linear blowup, because wildcard rewrite rules get
duplicated in the failure branches.  (This is similar to the issue that
`match x with "some string" => true | _ => false end%string` will
generate a large number of "false" branches, and duplicate "false"
across all of them, rather than having a single default case.)
For example, if we had the rewrite rules

    # + # ~~> literal sum
    x + (-y) ~~> x - y
    (-x) + y ~~> y - x

then the compiled code would look like

    fun x y
      => if x is a literal
         then if y is a literal
              then literal sum
              else if y is an opp
                   then x - y
                   else x + y
         else if y is an opp
         then x - y
         else if x is an opp
              then y - x
              else x + y

where we actually want the code

    fun x y
      => if x is a literal
         then if y is a literal
              then return (literal sum);
         if y is an opp
         then return (x - y);
         if x is an opp
         then return (y - x);
         return (x + y)

in the sequence+return monad.  i.e., we want to not duplicate the "if y
is an opp" code multiple times.

I think the solution to this is to have the discrimination tree
evaluator return an option, and to have the function that computes the
discrimination tree not duplicate rewrite rules among different cases.

Note that this leads to slightly inefficient matching sometimes: when
two rules with the same structure are separated by a rule with a
wildcard instead of structure, we will now try to match on the structure
twice.  It might be useful to be able to denote that some rewrite rules
can be commuted.

Also, we remove `Module pident := pattern.ident.` to work around
https://github.com/coq/coq/issues/8152, now that we're no longer
unfolding all of the `pattern.ident` stuff (because not unfolding it
gives slightly nicer output code).

After     | File Name                                                            | Before    || Change     | % Change
---------------------------------------------------------------------------------------------------------------------
17m41.82s | Total                                                                | 29m58.10s || -12m16.27s | -40.94%
---------------------------------------------------------------------------------------------------------------------
1m08.84s  | Experiments/NewPipeline/Rewriter                                     | 5m16.96s  || -4m08.11s  | -78.28%
0m37.50s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 2m03.59s  || -1m26.09s  | -69.65%
0m17.35s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 1m41.56s  || -1m24.21s  | -82.91%
0m24.10s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 1m43.33s  || -1m19.22s  | -76.67%
0m38.44s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 1m28.64s  || -0m50.20s  | -56.63%
0m20.86s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 1m06.91s  || -0m46.04s  | -68.82%
0m11.46s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m55.64s  || -0m44.17s  | -79.40%
0m04.17s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m22.22s  || -0m18.04s  | -81.23%
1m31.73s  | Experiments/NewPipeline/Toplevel2                                    | 1m49.50s  || -0m17.76s  | -16.22%
0m06.12s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m23.22s  || -0m17.09s  | -73.64%
0m08.69s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m22.12s  || -0m13.43s  | -60.71%
0m05.80s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m15.32s  || -0m09.51s  | -62.14%
0m04.10s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m13.20s  || -0m09.09s  | -68.93%
0m03.30s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m13.02s  || -0m09.71s  | -74.65%
5m47.58s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m52.86s  || -0m05.28s  | -1.49%
4m02.15s  | Experiments/NewPipeline/Toplevel1                                    | 4m04.75s  || -0m02.59s  | -1.06%
0m11.40s  | p384_64.c                                                            | 0m09.04s  || +0m02.36s  | +26.10%
0m34.20s  | p521_64.c                                                            | 0m32.80s  || +0m01.40s  | +4.26%
0m23.40s  | p384_32.c                                                            | 0m21.95s  || +0m01.44s  | +6.60%
0m38.90s  | p521_32.c                                                            | 0m39.34s  || -0m00.44s  | -1.11%
0m03.40s  | p256_32.c                                                            | 0m03.63s  || -0m00.23s  | -6.33%
0m03.24s  | secp256k1_32.c                                                       | 0m03.37s  || -0m00.12s  | -3.85%
0m02.14s  | curve25519_32.c                                                      | 0m02.00s  || +0m00.14s  | +7.00%
0m02.13s  | p256_64.c                                                            | 0m01.72s  || +0m00.40s  | +23.83%
0m01.82s  | p224_32.c                                                            | 0m01.82s  || +0m00.00s  | +0.00%
0m01.44s  | p224_64.c                                                            | 0m01.48s  || -0m00.04s  | -2.70%
0m01.40s  | secp256k1_64.c                                                       | 0m01.97s  || -0m00.57s  | -28.93%
0m01.35s  | curve25519_64.c                                                      | 0m01.34s  || +0m00.01s  | +0.74%
0m01.34s  | Experiments/NewPipeline/CLI                                          | 0m01.32s  || +0m00.02s  | +1.51%
0m01.20s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.16s  || +0m00.04s  | +3.44%
0m01.20s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.25s  || -0m00.05s  | -4.00%
0m01.08s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.07s  || +0m00.01s  | +0.93%

0 files changed, 0 insertions, 0 deletions