[isabelle] Uncaught exception in function package


I'm trying out the Haskabelle tool on a simple example program:

  module HB1 where

  newtype Arr a = A [a]

  alist :: Arr a -> [a]
  alist (A xs) = xs

  {-# HASKABELLE permissive mk_array #-}
  mk_array :: Integer -> a -> Arr a
  mk_array 0 x = A []
  mk_array n x
      = A (x:xs)
        where xs = alist $ mk_array (n - 1) x

Haskabelle is able to translate the file, but then Isabelle's function package gives this error on mk_array:

  *** exception Option raised (line 80 of "General/basics.ML")
  *** At command "function".

I'm using Isabelle2009-2. I suspect it's due to the numeric pattern match on an "int" type. However, this pattern is pretty common in Haskell programs. Is it possible to have the function package accept these kinds of patterns, at least for the "int" type?


Attachment: smime.p7s
Description: S/MIME cryptographic signature

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