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



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.