Re: [isabelle] Uncaught exception in function package

Hi John,

>   {-# 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

function (sequential) mk_array :: "int ⇒ 'a ⇒ 'a Arr"
  "mk_array 0 x = A Nil"
| "mk_array n x = (let xs = alist $ mk_array (n - 1) x
                   in A (x # xs))"
sorry termination sorry

The fundamental problem is that while in Haskell overlapping pattern are
disambiguated by order, in Isabelle every equations must be
disambiguated "on its own" to be logically consistent and
self-contained.  I.e. disambiguation must be encoded syntactically.  For
datatypes this can be done using pattern disambiguation.  For
non-datatypes the story is not that clear (how would you encode "any
number different from 0"?).  Here it is perhaps best to rewrite that
pattern match into an explicit if-then-else.

Note that if you remove (sequential), their will be no attempt for
disambiguation, but then the specification is inconsistent anyway.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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