diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 15:46:26 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-07 18:04:04 +0200 |
commit | 19f49cb0088868cfb6c91d04924c44ffbf8d9fc7 (patch) | |
tree | bfcda8be1555d70c8f7eea085de81075fcaf1d97 /plugins/micromega/mfourier.mli | |
parent | af902fa028f8ceb152d9add198e7dd490a4394ca (diff) |
Micromega clean-up
We add .mli files, removed dead code and use standard combinators
instead of redefined ad-hoc ones in a few places.
A lot of cleaning still has to be done on this code: documenting the
interfaces, resolving the many abstraction leaks. I suspect there is
still a lot of code duplication.
Diffstat (limited to 'plugins/micromega/mfourier.mli')
-rw-r--r-- | plugins/micromega/mfourier.mli | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/plugins/micromega/mfourier.mli b/plugins/micromega/mfourier.mli new file mode 100644 index 000000000..f1d8edeab --- /dev/null +++ b/plugins/micromega/mfourier.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module Itv : sig + + type interval = Num.num option * Num.num option + val range : interval -> Num.num option + val smaller_itv : interval -> interval -> bool + +end + +module IMap : CSig.MapS with type key = int + +type proof + +module Fourier : sig + + val find_point : Polynomial.cstr_compat list -> + ((IMap.key * Num.num) list, proof) Util.union + + val optimise : Polynomial.Vect.t -> + Polynomial.cstr_compat list -> + Itv.interval option + +end + +val pp_proof : out_channel -> proof -> unit + +module Proof : sig + + val mk_proof : Polynomial.cstr_compat list -> + proof -> (Polynomial.Vect.t * Polynomial.cstr_compat) list + + val add_op : Polynomial.op -> Polynomial.op -> Polynomial.op + +end + +val max_nb_cstr : int ref + +val eval_op : Polynomial.op -> Num.num -> Num.num -> bool + +exception TimeOut |