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



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.