ada: Build invariant procedure while freezing in GNATprove mode

ada: Build invariant procedure while freezing in GNATprove mode

Invariant procedure bodies are created either by expansion of freezing
nodes (but only in ordinary compilation mode) or at the end of package
private declarations (but not for with private types in the type
derivation chain).

In GNATprove mode we didn't create invariant procedure bodies in
lightweight expansion, so we didn't create them at all when there were
private types in the type derivation chain.

This patch copies the relevant freezing part from ordinary to
lightweight expansion. This obviously involves code duplication,
but it seems better to duplicate whole sections that work properly
instead of small pieces that are incomplete. There are other pieces
of freezing that are similarly duplicated, so this patch doesn't make
the code substantially worse.

gcc/ada/

	* exp_spark.adb (SPARK_Freeze_Type): Copy whole handling of DIC
	and Type_Invariant from Freeze_Type.