aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/ideal.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-24 12:23:43 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-04-09 22:00:20 +0200
commitba636891121821b4943a0464b49e14de54de8253 (patch)
treed70caf013b7e428f376d48ea018d880b9d36a505 /plugins/nsatz/ideal.mli
parent2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff)
Academic prescriptivism strikes back: down with baroque programming in Nsatz.
Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging.
Diffstat (limited to 'plugins/nsatz/ideal.mli')
-rw-r--r--plugins/nsatz/ideal.mli21
1 files changed, 13 insertions, 8 deletions
diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli
index d1a2a0a7d..b7ec901af 100644
--- a/plugins/nsatz/ideal.mli
+++ b/plugins/nsatz/ideal.mli
@@ -6,6 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+type metadata = {
+ name_var : string list;
+}
+
+module Monomial :
+sig
+type t
+val repr : t -> int array
+val make : int array -> t
+end
+
module Make (P : Polynom.S) :
sig
(* Polynomials *)
@@ -14,32 +25,26 @@ type deg = int
type coef = P.t
type poly
-val repr : poly -> (coef * int array) list
+val repr : poly -> (coef * Monomial.t) list
val polconst : int -> coef -> poly
val zeroP : poly
val gen : int -> int -> poly
val equal : poly -> poly -> bool
-val name_var : string list ref
val plusP : poly -> poly -> poly
val oppP : poly -> poly
val multP : poly -> poly -> poly
val puisP : poly -> int -> poly
-val poldepcontent : coef list ref
-
type certificate =
{ coef : coef; power : int;
gb_comb : poly list list; last_comb : poly list }
-val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
+val in_ideal : metadata -> deg -> poly list -> poly -> certificate
module Hashpol : Hashtbl.S with type key = poly
-val sugar_flag : bool ref
-val divide_rem_with_critical_pair : bool ref
-
end
exception NotInIdeal