Re: [isabelle] less_eq_set generated by Haskell and SML code generation raising runtime exceptions



Hi Andreas,

Oops, yes, thanks for pointing that out.  The card_UNIV approach you
mentioned fixed my issue.

Thanks,
Dominic

On 27 July 2017 at 12:09, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
> Dear Dominic,
>
> This is a well-known problem. You cannot decide whether the complement of a
> set is a subset of an explicitly given set unless you know something more
> about the type, e.g., how many elements there are. The theory Cardinality in
> HOL/Library provides an implementation in that direction, but it requires
> that every element type in use must instantiate the type class card_UNIV.
>
> In general, the code generator does not check for missing patterns and it
> provides only partial correctness: If the generated code successfully
> evaluates to a result, then this result is correct.
>
> Hope this helps,
> Andreas
>
>
> On 27/07/17 09:44, Dominic Mulligan via Cl-isabelle-users wrote:
>>
>> Hi,
>>
>> The SML and Haskell backends of the Isabelle2016-1 code generator are
>> introducing partial pattern matches which cause runtime failures.  I
>> think I have narrowed down the cause to the generated functions
>> less_eq_set in both backends:
>>
>>      less_eq_set :: forall a. (Eq a) => Set a -> Set a -> Bool;
>>      less_eq_set (Coset []) (Set []) = False;
>>      less_eq_set a (Coset ys) = all (\ y -> not (member y a)) ys;
>>      less_eq_set (Set xs) b = all (\ x -> member x b) xs;
>>
>> for Haskell, and
>>
>>      fun less_eq_set A_ (Coset []) (Set []) = false
>>        | less_eq_set A_ a (Coset ys) = List.list_all (fn y => not
>> (member A_ y a)) ys
>>        | less_eq_set A_ (Set xs) b = List.list_all (fn x => member A_ x b)
>> xs;
>>
>> in SML.  In particular, calling
>>
>>      less_eq_set (Coset [1,2,3]) (Set [])
>>
>> will produce a runtime exception.
>>
>> The following small theory is sufficient to show the problem in both
>> generator backends:
>>
>>      theory Test imports Main begin
>>
>>      definition foo :: "bool" where
>>        "foo â (UNIV - {1::nat}) â {}"
>>
>>      export_code foo in Haskell
>>        module_name Test
>>      export_code foo in SML
>>
>>      MLâ
>>        val it = @{code foo}
>>      â
>>
>>      end
>>
>> Thanks,
>> Dominic
>>
>




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