#####################################################################
#
# FactorsPolyZVerified
#
# Factors a univariate polynomial over Z using verified code.
# It calls an external binary called factor_poly_verified that has been generated
# from a verified functional implementation of the Berlekamp and Zassenhaus algorithm.
# Verification and code generation were done in the Isabelle proof assistant
# by Divasón, Joosten, Thiemann and Yamada.
# For details see this article in the Archive of Formal Proofs:
# https://www.isa-afp.org/entries/Berlekamp_Zassenhaus.html
#
# The polynomial is passed to factor_polynomial_verified as a string of the form
# "[a0,a1,...]" representing a list of coefficients (in increasing order of degree)
# of the polynomial over Z. The factorization is returned as a string of the form
# "[c, [[a00, a01, ...], e0], [[a10, a11, ...], e1], ...]"
# with a leading coefficient c and a list of pairs [factor, exponent],
# where each factor is represented by its list of coefficients.
#
# AUTHORS
# Tobias Nipkow and Olexandr Konovalov
# Initial version (2023-10) prepared at Dagstuhl seminar 23401:
#  "Automated mathematics: integrating proofs, algorithms and data"
#
# EXAMPLES
#
# Read("FactorsPolyZVerified.g");
# x := Indeterminate(Integers,"x");
# f := 6 * (x^2 + 2*x + 1);
# FactorsPolyZVerified(f);
# -> [ 6*x+6, x+1 ]
# g := x^16 + 4*x^12 - 16*x^11 + 80*x^9 + 2*x^8 + 160*x^7 + 128*x^6 - 160*x^5 + 28*x^4 - 48*x^3 + 128*x^2 - 16*x + 1;
# h := x^16 + 4*x^12 + 16*x^11 - 80*x^9 + 2*x^8 - 160*x^7 + 128*x^6 + 160*x^5 + 28*x^4 + 48*x^3 + 128*x^2 + 16*x + 1;
# FactorsPolyZVerified(g * h);
#


FactorsPolyZVerified := function( poly )
local xi, poly_string, factors_string, factors_obj, lead_coeff, fam, res;

xi := IndeterminateNumberOfUnivariateRationalFunction(poly);
poly_string := String(CoefficientsOfUnivariatePolynomial(poly));
factors_string := IO_PipeThrough("factor_polynomial_verified",[], poly_string);
factors_obj := EvalString(factors_string);
lead_coeff := factors_obj[1];
fam := FamilyObj(lead_coeff);
res := Concatenation(List(factors_obj[2], t -> ListWithIdenticalEntries(t[2],UnivariatePolynomialByCoefficients(fam,t[1],xi))));
res[1] := res[1]*lead_coeff;
return res;

end;