diff options
| author | Emilio Jesus Gallego Arias | 2016-03-03 18:26:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-10-20 15:18:28 +0200 |
| commit | 2dfe032fd42f2489320936fe1e60c9cf7dafe8cf (patch) | |
| tree | 20b0c583febeda8d96a0fb4c8ba6ffb6fa4763ec /test-suite/output/SearchPattern.out | |
| parent | df1de9fa318f1924d92fb39c4bc67c16f3d31db4 (diff) | |
[search] Don't build intermediate lists in search.
This patch converts the `search_*` functions to use an iter-style API.
Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.
It also allows different printers to be used.
I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).
As a minor tweak, we make search with "Output Name Only" more efficient.
Motivation:
-----------
Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:
```ocaml
val generic_search : int option -> display_function -> unit
```
This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.
The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.
However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.
Diffstat (limited to 'test-suite/output/SearchPattern.out')
| -rw-r--r-- | test-suite/output/SearchPattern.out | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 1eb7eca8f1..f3c12effca 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat Nat.lor: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat Nat.lxor: nat -> nat -> nat - S: nat -> nat Nat.succ: nat -> nat Nat.pred: nat -> nat @@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat - h: n <> newdef n h: n <> newdef n h: P n |