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://www.haftmann-online.de/florian/florian_at_haftmann_online_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev