[inferbo] no polymorphic max in [degree_with_term]

Summary:
Polymorphic compare is bad, 'mkay? I also tried changing this to do what
the comment says the function does (keep the first term instead of the
"largest" term) but that resulted in test changes so I kept the original
behaviour instead.

Reviewed By: jberdine

Differential Revision: D19861587

fbshipit-source-id: d57fd4a02
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent b7f42759cf
commit bc50a8e724

@ -208,7 +208,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
- contents of terms are not zero
- symbols in terms are only symbolic values
*)
type t = {const: NonNegativeInt.t; terms: t M.t}
type t = {const: NonNegativeInt.t; terms: t M.t} [@@deriving compare]
let of_non_negative_int : NonNegativeInt.t -> t = fun const -> {const; terms= M.empty}
@ -376,12 +376,14 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
match subst p eval_sym with p -> Below p | exception ReturnTop s_trace -> Above s_trace
(** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such degree *)
(** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such
degree *)
let rec degree_with_term {terms} =
M.fold
(fun t p acc ->
(fun t p cur_max ->
let d, p' = degree_with_term p in
max acc (Degree.succ (S.degree_kind t) d, mult_symb p' t) )
let degree_term = (Degree.succ (S.degree_kind t) d, mult_symb p' t) in
if [%compare: Degree.t * t] degree_term cur_max > 0 then degree_term else cur_max )
terms (Degree.zero, one)

Loading…
Cancel
Save