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
