[isabelle-dev] sets and code generation

[Lukas Bulwahn]

On 03/21/2012 09:08 AM, Christian Sternagel wrote:
> On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
>> On 03/21/2012 08:36 AM, Christian Sternagel wrote:
>>> Hi there,
>>>
>>> since set is a proper type some code equations that used to work, no
>>> longer do, e.g.,
>>>
>>> "op |> = {(x, y). supt_impl x y}"
>>>
>>> as a code equation leads to an error stating that terms (x and y are
>>> first-order terms) do not support the enum class. Since the possible
>>> terms (using strings as function symbols and variables) cannot be
>>> enumerated in a (finite) list, I can also not introduce an enum 
>>> instance.
>>
>> Introducing 'a set as a type constructor now allows us to refine the set
>> operations to operations on lists (by Florian's way of data refinement
>> for code generation).
>> However, this now disallows the execution of "op |>" on the type "...
>> set". To execute this, you have to move this specification to predicates
>> ('a => bool):
>>
>> Define "op |> = (%(x, y). supt_impl x y)"
>>
>>
>> Lukas
> Sorry I don't quite get it. op |>  is already defined to be of type 
> "('f, 'v) term rel" (and used heavily as a set). So the above equation 
> would not be well-typed. Is your suggestion to change op |> into a 
> predicate?
>
> cheers
>
> chris
Yes.

If you have an infinite set during the execution in the generated code, 
which you hinted at before, you cannot use the type 'a set for code 
generation, but you must use 'a => bool.

I cannot estimate how much work that is in your case.
If it is unfeasible in your formalisation to change this, there might 
also be other means to obtain an executable specification by creating an 
alternative data refinement for sets, but I only had this in the back of 
my mind, and we have not done this (yet).


Lukas