[isabelle-dev] Constructors and the predicate compiler

[Andreas Lochbihler]

Dear Florian,

I myself have never looked in detail through the implementation of the predicate compiler, 
but I have been a major user. I previously noticed that it does not go well together with 
code_datatype. Here are my 50 cents.

On the one hand, the predicate compiler generates code equations, so it should work 
together with the code generator. On the other hand, it operates inside Isabelle/HOL, so 
it does not have access to the extra-logical features of the code generator such as data 
refinement. This is probably the source of the confusion. To me, it seems more sensible to 
do everything as in the logic and ignore the code generator setup as much as possible.

The compilation requires that the constructors are invertible inside the logic 
(code_datatype's pseudo-constructors are invertible in the generated code, but not 
necessarily in the logic). Therefore, IMHO, mode inference has to use Ctr_Sugar, not 
Code.is_constr. Otherwise, the compiler will later try to construct a case expression for 
a code_datatype pseudo-constructur and raise an "Error in case expression: Not a datatype 
constructor".

In predicate_compile_proof.ML, the generated equations are proven. The is_constructor 
function is used to check whether the constructor should be inverted (using a case 
expression). Since this happens inside the logic and has to be coupled with the mode 
inference, it should use the same criterion as the mode inference, namely Ctr_Sugar.

I am not familiar with the flatten function in predicate_compile_fun and what exactly it 
is good for. My educated guess is that this determines which of the function constants in 
an (inductive) definition should be replaced with predicates and which not. If this is 
right, then it should also be Ctr_Sugar there.

In summary, I'd say that code_pred should only use Ctr_Sugar and ignore code_datatype 
declarations. If a user does use code_datatype, then he is responsible for providing 
appropriate code equations for the existing functions, i.e., the constructors and the case 
operator, or set up the code preprocessor to eliminate them (cf. the Suc eliminiation in 
Code_Target_Nat and friends). Otherwise, users will have a hard time to follow what is 
actually going on in code_pred.

Andreas


On 14/02/15 11:25, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>