blob: 9c8f43d7d4c241ef5b03a7e3f46445182f181ea0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
(************************************************************************)
(* 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 *)
(************************************************************************)
exception NotInIdeal
val lexico : bool ref
val use_hmon : bool ref
module type S = sig
(* Monomials *)
type mon = int array
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_mon_test : int -> mon -> mon -> bool
val ppcm_mon : int -> mon -> mon -> mon
(* Polynomials *)
type deg = int
type coef
type poly
val repr : poly -> (coef * mon) list
val polconst : deg -> coef -> poly
val zeroP : poly
val gen : deg -> int -> poly
val equal : poly -> poly -> bool
val name_var : string list ref
val getvar : string list -> int -> string
val lstringP : poly list -> string
val printP : poly -> unit
val lprintP : poly list -> unit
val div_pol_coef : poly -> coef -> poly
val plusP : deg -> poly -> poly -> poly
val mult_t_pol : deg -> coef -> mon -> poly -> poly
val selectdiv : deg -> mon -> poly list -> poly
val oppP : poly -> poly
val emultP : coef -> poly -> poly
val multP : deg -> poly -> poly -> poly
val puisP : deg -> poly -> int -> poly
val contentP : poly -> coef
val contentPlist : poly list -> coef
val pgcdpos : coef -> coef -> coef
val div_pol : deg -> poly -> poly -> coef -> coef -> mon -> poly
val reduce2 : deg -> 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 : deg -> poly list -> unit
val reduce2_trace : deg -> poly -> poly list -> poly list -> poly list * poly
val spol : deg -> poly -> poly -> poly
val etrangers : deg -> poly -> poly -> bool
val div_ppcm : deg -> poly -> poly -> poly -> bool
val genPcPf : deg -> poly -> poly list -> poly list -> poly list
val genOCPf : deg -> poly list -> poly list
val is_homogeneous : poly -> bool
type certificate =
{ coef : coef; power : int;
gb_comb : poly list list; last_comb : poly list }
val test_dans_ideal : deg -> poly -> poly list -> poly list ->
poly list * poly * certificate
val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
end
module Make (P:Polynom.S) : S with type coef = P.t
|
