Re: [isabelle] Fwd: Code generation for typedefs with an invariant



Small addition: another application of this is to make a "safe" constructor for types with invariants that returns "None" if the given value does not fulfil the invariant, e.g.:

mk_pos_nat :: nat ⇒ good_nat option
mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None)

One can do this with an auxiliary function that returns a default value instead of None, but then you have to check the condition twice.

The best possible solution I see here is if "code abstype" could handle not only equations of the form "projection (fun_with_invariant x y z) = …" but relations involving "canonical" relators on types. In the above case, one would then not have a code equation but a code relation:

rel_fun (=) (rel_option pcr_good_nat)
     (λn. if good n then Some n else None) mk_good_nat

Similarly, the function in my last email have the following relations:

rel_fun (=) (list_all2 pcr_good_nat)
     my_complicated_computation my_complicated_computation'

The actual generated code should of course be:

mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None

my_complicated_computation' xs = map Abs_good_nat (my_complicated_computation xs)

Which is exactly the m_complicated_computation' that comes out of the lift_definition anyway (and I imagine there's a one-to-one correspondence between the map operations in the def lemma and the relators in the transfer lemma).


So, not sure – is there some fundamental problem with implementation something like this in the code generator?

Manuel



On 14/10/2021 21:31, Manuel Eberl wrote:
Hello,

I have a typedef of the form

typedef good_nat = "{n::nat. good n}"

and I have an executable function that produces a "nat list" where I have proven that all entries are good.

How can I lift that to an *executable* function that produces a "good_nat list" instead?

The way I see it, the usual approach of doing a "code abstype" and specifying the code equation in terms of some projection out of the "type with invariant" to "type without invariant" doesn't work here because I have lists of these things.

I do have a workaround involving a second typedef for intermediate results, but it is very boilerplatey and I'd be happy to know if there is something easier.

See attachment for all the details.

Thanks,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.