[isabelle-dev] Constructors and the predicate compiler

[Florian Haftmann]

Hi all,

while reviewing some technical details of code generation, I stumbled
over a confusion in the predicate compiler regarding what a
»constructor« is supposed to be.

The presumably fundamental notions are given in predicate_compile_aux.ML
(c3ca292c1484) as:

	(* check if a term contains only constructor functions *)
	(* TODO: another copy in the core! *)
	(* FIXME: constructor terms are supposed to be seen in the way the code
generator
	  sees constructors.*)
 	fun is_constrt thy = … (* relying on Ctr_Sugar *)
	
	val is_constr = Code.is_constr o Proof_Context.theory_of (* relying on
Code *)

is_constrt is actually only used in predicate_compile_fun.ML:

	… Predicate_Compile_Aux.is_constrt …

guarding whether a given term is supposed to stay »as it is«, suggesting
that the postulating comment for is_constrt reflects actually the
intended behaviour, leaving open the question why it has not ever been
implemented like this.

On the other hand is_constr is used in mode_inference.ML:

	fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
	  | is_invertible_function ctxt _ = false

and this seems odd, since a constructor in the sense of the code
generator is by now means invertible, suggesting that here a fundamental
misconception occurs.

From such a superficial analysis it seems to follow that the two
implementations should be actually swapped: is_constrt relying on
Code.is_constr, is_constr relying ont Ctr_Sugar.

To make the confusion perfect, in predicate_compile_proof.ML there is a
third variant:

	(* returns true if t is an application of a datatype constructor *)
	(* which then consequently would be splitted *)
	fun is_constructor ctxt t =
	  (case fastype_of t of
	    Type (s, _) => s <> @{type_name fun} andalso can
(Ctr_Sugar.dest_ctr ctxt s) t
	  | _ => false)

Can anybody acquainted with the predicate compiler shed some light on this?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150214/5beabdf3/attachment.sig>