maple2ssr := module() option package; export # Exported but lower level. pp_integer, pp_pure_power, pp_monomial, pp_polynomial, pp_rational_function, pp_name_of_monomial, pp_coeffs_def, # High-level calls. pp_skew_poly, pp_in_terms_of, write; local string_of_index, string_of_coeffs; local possibly_add_parentheses := proc(s, b, $) `if`(b, sprintf("(%s)", s), s) end proc; pp_integer := proc(expr, $) sprintf(`if`(expr < 0, "- %s %d", "%s %d"), "rat_of_Z", abs(expr)) end proc; pp_pure_power := proc(expr, v, $) local dg := degree(expr, v); if dg < 0 then error "Negative exponents not allowed, but found %1", dg end if; `if`(dg = 1, sprintf("%s", v), sprintf("%s^%d", v, dg)) end proc; pp_monomial := proc(expr, vars, is_a_factor, $) local v, i, res, cf, dg; local actual_vars := indets(expr, name); local nb := nops(actual_vars); local excess := actual_vars minus convert(vars, set); if excess <> {} then error "unexpected variables: %1", excess end if; if is_a_factor then if nb = 0 then pp_integer(expr) else if nops(actual_vars) <> 1 then error "bug in pp_monomial (%1, %2, %3)", expr, vars, actual_vars end if; res[i] := pp_pure_power(expr, op(1, actual_vars)) end if else cf := eval(expr, {seq(op(i, actual_vars) = 1, i = 1 .. nb)}); if nb > 0 then if cf = 1 then res[0] := "" elif cf = -1 then res[0] := "- " else res[0] := sprintf("%s * ", pp_integer(cf)) end if; for i to nb do res[i] := pp_pure_power(expr, op(i, actual_vars)) end do; cat(res[0], res[1], seq(cat(" * ", res[i]), i = 2 .. nb)) else pp_integer(cf) end if end if end proc; # The boolean is_a_factor impacts if parentheses are added around # the output string: if set to true and if the polynomial is not a # single monomial, then parentheses are added. pp_polynomial := proc(expr, vars, is_a_factor, $) local i, res, nb; if type(expr, `^`) and hastype(expr, `+`) then sprintf("(%s)^%d", pp_polynomial(op(1, expr), vars, false), op(2, expr)) elif type(expr, `*`) and hastype(expr, `+`) then nb := nops(expr); for i to nb do res[i] := pp_polynomial(op(i, expr), vars, true) end do; possibly_add_parentheses( cat(res[1], seq(cat(" * ", res[i]), i = 2 .. nb)), is_a_factor) elif type(expr, `+`) then nb := nops(expr); for i to nb do res[i] := pp_monomial(op(i, expr), vars, false) end do; possibly_add_parentheses( cat(res[1], seq(cat(" + ", res[i]), i = 2 .. nb)), is_a_factor) else pp_monomial(expr, vars, true) end if end proc; pp_rational_function := proc(expr, vars, $) if hastype(expr, name) and not type(expr, polynom) then sprintf("(%s) / (%s)", pp_polynomial(numer(expr), vars, false), pp_polynomial(denom(expr), vars, true)) else pp_polynomial(expr, vars, true) end if end proc; # Take a monomial lm that is a power product of the variables in Sxs, # and output a name like Sn2Sk3. pp_name_of_monomial := proc(lm, Sxs, $) local degs, Sx, res; degs := table(); for Sx in Sxs do degs[Sx] := degree(lm, Sx) end do; res := cat(seq( `if`(degs[Sx] > 1, sprintf("%s%d", Sx, degs[Sx]), `if`(degs[Sx] = 1, sprintf("%s", Sx), "" )), Sx = Sxs)); if res = "" then res := "id_op" end if; res end proc; # Pretty print a list of integers [i1, ..., ir] into the form # "_..._". string_of_index := proc(idx, $) local i; local s := sprintf("%d", idx[1]); for i from 2 to nops(idx) do s := sprintf("%s_%d", s, idx[i]) end do; s end proc; # Given a list of coefficients, variables xs, and a string rr_name, # pretty print the definition of Coq constants _cf_..._. # The list of coefficients is really a list of pairs [idx, c], in which # the index idx is a list [i1, ..., ir] used to generate a name # of the form ..._cf_..._. pp_coeffs_def := proc(cf, xs, rr_name, $) local x, c; local def_prefix := sprintf( "Definition %s_cf%%s (%s: int) : rat :=\n%s%%s.\n\n", rr_name, cat(seq("" || x || "_ ", x = xs)), cat(seq("let " || x || " : rat := " || x || "_%%:~R in\n", x = xs)) ); cat(seq(sprintf( def_prefix, string_of_index(c:-idx), pp_rational_function(c:-val, xs)), c = cf)) end proc; # Makes a representation as a Coq seq (or seq seq) for a Maple # list (or list list). string_of_coeffs := proc(rr_name, cf_, $) local n, cf_sort, aux, cf, s, i, m; n := nops(cf_[1]:-idx); cf_sort := proc(key, $) (a, b) -> evalb(a:-idx[key] <= b:-idx[key]) end proc; aux := proc(rr_name, cf, $) local i; local s := StringTools:-SubString(cat(seq( sprintf(" %s_cf%s;", rr_name, string_of_index(cf[i]:-idx)), i = 1..nops(cf))), 1..-2); sprintf("[::%s]", s) end proc; # Caution: if n > 2, sorting has no meaning. if n <> 2 then cf := sort(cf_, cf_sort(1)); s := aux(rr_name, cf) else m := max(op(map(a -> a:-idx[2], cf_))); cf := [seq(select((a, j) -> evalb(a:-idx[2] = j), cf_, i), i = 0..m)]; # map(op, cf) is sorted w.r.t. cf_sort(2) by the construction above. # There remains to sort w.r.t. cf_sort(1). cf := map(sort, cf, cf_sort(1)); s := "[::"; for i to nops(cf) do s := sprintf("%s %s;", s, aux(rr_name, cf[i])) end do; s := StringTools:-SubString(s, 1..-2); s := sprintf("%s]", s) end if; s end proc; # Two modes of operation are available: # * If mode is a monomial order, outputs rewriting rule of the # form leading_monomial = queue, whose name is obtained by # encoding the leading monomial. # * If mode is a string, plainly output the operator, whose name # is given by the string. pp_skew_poly := proc(p, xs, Sxs, f, {mode := "foo"}, $) local MOrd, lm, lc, q, mo, i, x, deg, cf, rr_name, xs_, def_prefix, coeffs_def, aux, ints, lin_comb, nxs, coeffs_seq, whole_def; if type(mode, string) then q := p elif type(mode, ShortMonomialOrder) then MOrd := mode; lm := Groebner:-LeadingMonomial(p, MOrd); lc := Groebner:-LeadingCoefficient(p, MOrd); q := (lc * lm - p) / lc else error "bad mode argument" end if; q := collect(q, Sxs, distributed, factor); # Ensure little-endian numbering of coefficients in the # univariate case. # Caveat: This makes it a dense representation. if nops(Sxs) = 1 then deg := degree(q, Sxs[1]); cf := [seq(Record(idx = [i], val = coeff(q, Sxs[1], i)), i = 0..deg)]; mo := [seq(Sxs[1]^i, i = 0..deg)] else cf := [coeffs(q, Sxs, 'mo')]; mo := [mo]; cf := [seq(Record( idx = map2(degree, mo[i], Sxs), val = cf[i]), i = 1..nops(cf))] end if; rr_name := `if`(type(mode, string), mode, pp_name_of_monomial(lm, Sxs)); xs_ := cat(seq("" || x || "_ ", x = xs)); coeffs_def := pp_coeffs_def(cf, xs, rr_name); aux := proc(m, $) local s := f; local d; for i to nops(Sxs) do d := degree(m, Sxs[i]); if d = 0 then s := sprintf("%s %s_", s, xs[i]) else s := sprintf("%s (int.shift %d %s_)", s, d, xs[i]) end if end do; s end proc; ints := cat("int -> " $ nops(xs)); lin_comb := StringTools:-SubString(cat(seq( sprintf(" + %s_cf%s %s* %s", rr_name, string_of_index(cf[i]:-idx), xs_, aux(mo[i])), i = 1..nops(cf))), 4..-1); if type(mode, string) then coeffs_seq := string_of_coeffs(rr_name, cf); whole_def := sprintf( "%sDefinition %s_flat (%s : %srat) (%s: int) : rat :=\n%s.\n", coeffs_def, rr_name, f, ints, xs_, lin_comb ); nxs := nops(xs); if nxs = 1 or nxs = 2 then whole_def := sprintf( "%s\nDefinition %s_seq := %s.\n\nDefinition %s_horner := %s %s_seq.\n", whole_def, rr_name, coeffs_seq, rr_name, `if`(nxs = 1, "punk.horner_seqop", "punk.biv_horner_seqop2"), rr_name ) else whole_def := sprintf( "%s\n(* No definition of constants %s_seq and %s_horner: %s_flat is multivariate. *)\n", whole_def, rr_name, rr_name, rr_name ) end if else whole_def := sprintf( "%sDefinition %s (%s : %srat) := forall (%s: int), precond.%s %s->\n%s = %s.\n", coeffs_def, rr_name, f, ints, xs_, rr_name, xs_, aux(lm), lin_comb ) end if; whole_def end proc; # Allows the reuse of a definition of a module (whose name is given # by the string old_module) into the current Coq module. Slightly # extended to be able to reuse as a new constant in the present Coq # module a linear combination of constants from a module old_module # with names are given in the list old_consts. pp_in_terms_of := proc(cf, xs, f, old_module, old_consts, new_const, $) local x, i; local xs_ := cat(seq("" || x || "_ ", x = xs)); local coeffs_def := pp_coeffs_def([seq(Record(idx = [i], val = cf[i]), i = 1..nops(cf))], xs, new_const || "_lcomb"); local ints := cat("int -> " $ nops(xs)); local lin_comb := StringTools:-SubString(cat(seq(sprintf("+ %s_lcomb_cf%s %s* %s %s %s", new_const, string_of_index([i]), xs_, old_module || "." || (old_consts[i]), f, xs_), i = 1..nops(cf))), 3..-1); sprintf( "Require %s.\n\n%sDefinition %s_lcomb (%s : %srat) (%s: int) : rat :=\n%s.\n", old_module, coeffs_def, new_const, f, ints, xs_, lin_comb ) end proc; # The string s is output to the terminal or a file according to the # optional parameters: # * append: By default, data are appended to the file. Set to # false to overwrite a file or create a new file. # * skip_line: By default, a blank line is added at the end of the # given string. Set to false if not wanted, like at the end # of a file. # * file: The default "" writes to the terminal. Set to some path # to a file if writing to a file is wanted. The first # parameter append has no impact when writing to the terminal. write := proc(s, {append::boolean := true, skip_line::boolean := true, file::string := ""}, $) if file <> "" then `if`(append, appendto, writeto)(file) end if; if not append then printf("(* Generated by Maple. *)\n\n") end if; printf(`if`(skip_line, "%s\n", "%s"), s); if file <> "" then writeto(terminal) end if; end proc; end module: