[request] c_call like c_func / fmt_c_decl

[JasonGross]

In usage in fiat-crypto, I find myself needing to recreate some of the logic from

bedrock2/bedrock2/src/bedrock2/ToCString.v

Lines 149 to 156 in 13365e8

	match rets with
	| nil => (fmt_c_decl "void" args name nil, None, nil)
	| cons r0 _ =>
	let r0 := List.last rets r0 in
	let rets' := List.removelast rets in
	let retrenames := fst (rename_outs rets' (cmd.vars body)) in
	(fmt_c_decl "uintptr_t" args name (List.map snd retrenames), Some r0, retrenames)
	end in

I would like a function like

c_arrange_arguments {A R} (args : list A) (rets : list R) : option R * list (A + R)

which factors out the logic about which return gets returned and which returns get added to the argument list, and the logic about which order things get added. (I can make a PR for this if you'd like.) See also mit-plv/fiat-crypto#895

[andres-erbsen]

So do you actually want c_arrange_arguments or just c_call?

[JasonGross]

I think c_arrange_arguments would be better; I need access to things that operate not just on strings (I need to bundle the type info with names).