Re-implementation of zify

The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress.  If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.

This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.

The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.)  efficiency impact.

There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite

1 files changed, 21 insertions, 9 deletions

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 5829292a0c..14a1bc9712 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -16,25 +16,19 @@
 
 module type PHashtable =
   sig
+    (* see documentation in [persistent_cache.mli] *)
     type 'a t
     type key
 
     val open_in : string -> 'a t
-    (** [open_in f] rebuilds a table from the records stored in file [f].
-        As marshaling is not type-safe, it might segfault.
-    *)
 
     val find : 'a t -> key -> 'a
-    (** find has the specification of Hashtable.find *)
 
     val add  : 'a t -> key -> 'a -> unit
-    (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl].
-	(and writes the binding to the file associated with [tbl].)
-	If [key] is already bound, raises KeyAlreadyBound *)
 
     val memo : string -> (key -> 'a) -> (key -> 'a)
-      (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
-	  Note that the cache will only be loaded when the function is used for the first time *)
+
+    val memo_cond : string -> (key -> bool) -> (key -> 'a) -> (key -> 'a)
 
   end
 
@@ -200,6 +194,24 @@ let memo cache f =
 		add tbl x res ;
 		res
 
+let memo_cond cache cond f =
+  let tbl = lazy (try Some (open_in cache) with _ -> None) in
+  fun x ->
+  match Lazy.force tbl with
+  | None -> f x
+  | Some tbl ->
+     if cond x
+     then
+       begin
+       try find tbl x
+       with  Not_found ->
+         let res = f x in
+         add tbl x res ;
+         res
+       end
+     else f x
+
+
 end