diff options
Diffstat (limited to 'plugins/groebner/ideal.mli')
-rw-r--r-- | plugins/groebner/ideal.mli | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/plugins/groebner/ideal.mli b/plugins/groebner/ideal.mli new file mode 100644 index 000000000..48b81102e --- /dev/null +++ b/plugins/groebner/ideal.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type coef = Polynom.poly +val coef_of_int : int -> coef +val eq_coef : coef -> coef -> bool +val plus_coef : coef -> coef -> coef +val mult_coef : coef -> coef -> coef +val sub_coef : coef -> coef -> coef +val opp_coef : coef -> coef +val div_coef : coef -> coef -> coef +val coef0 : coef +val coef1 : coef +val string_of_coef : coef -> string +val pgcd : coef -> coef -> coef + +type mon = int array +type poly = (coef * mon) list + +val eq_poly : poly -> poly -> bool +val mult_mon : int -> mon -> mon -> mon +val deg : mon -> int +val compare_mon : int -> mon -> mon -> int +val div_mon : int -> mon -> mon -> mon +val div_pol_coef : poly -> coef -> poly +val div_mon_test : int -> mon -> mon -> bool +val set_deg : int -> mon -> mon +val ppcm_mon : int -> mon -> mon -> mon + +val name_var : string list ref +val getvar : string list -> int -> string +val stringP : poly -> string +val stringPcut : poly -> string +val lstringP : poly list -> string +val printP : poly -> unit +val lprintP : poly list -> unit + +val polconst : int -> coef -> poly +val zeroP : poly +val plusP : int -> poly -> poly -> poly +val mult_t_pol : int -> coef -> mon -> poly -> poly +val selectdiv : int -> mon -> poly list -> poly +val gen : int -> int -> poly +val oppP : poly -> poly +val emultP : coef -> poly -> poly +val multP : int -> poly -> poly -> poly +val puisP : int -> poly -> int -> poly +val contentP : poly -> coef +val contentPlist : poly list -> coef +val pgcdpos : coef -> coef -> coef +val div_pol : int -> poly -> poly -> coef -> coef -> mon -> poly +val reduce2 : int -> poly -> poly list -> coef * poly + +val poldepcontent : coef list ref +val coefpoldep_find : poly -> poly -> poly +val coefpoldep_set : poly -> poly -> poly -> unit +val initcoefpoldep : int -> poly list -> unit +val reduce2_trace : + int -> poly -> poly list -> poly list -> poly list * poly +val homogeneous : bool ref +val spol : int -> poly -> poly -> poly +val etrangers : int -> ('a * mon) list -> ('b * mon) list -> bool +val div_ppcm : int -> poly -> poly -> poly -> bool + +type 'a cpRes = Keep of 'a list | DontKeep of 'a list +val list_rec : 'a -> ('b -> 'b list -> 'a -> 'a) -> 'b list -> 'a +val addRes : 'a -> 'a cpRes -> 'a cpRes +val slice : int -> poly -> poly -> poly list -> poly cpRes +val addS : 'a -> 'a list -> 'a list +val genPcPf : int -> poly -> poly list -> poly list -> poly list +val genOCPf : int -> poly list -> poly list + +val is_homogeneous : poly -> bool + +val in_ideal : + int -> poly list -> poly -> + coef * poly list * poly * poly list list * poly list |