Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] less_eq_set generated by Haskell and SML code ...

Email Gateway (Aug 22 2022 at 15:48):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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

Email Gateway (Aug 22 2022 at 15:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 15:49):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Andreas,

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

Thanks,
Dominic

Last updated: Nov 21 2024 at 12:39 UTC