Re: [isabelle] Uncaught exception in function package



Hi Florian,

Ok, that makes sense.

Thanks,
-john

On Jul 22, 2010, at 2:21 AM, Florian Haftmann wrote:

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"
where
 "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,
	Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


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



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