Email Gateway (Aug 18 2022 at 15:41): Email Gateway (Aug 18 2022 at 15:41):From: John Matthews <matthews@galois.com>
Hello,
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?
Thanks,
-john
smime.p7s
Email Gateway (Aug 18 2022 at 15:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
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
signature.asc
Email Gateway (Aug 18 2022 at 15:43):From: John Matthews <matthews@galois.com>
Hi Florian,
Ok, that makes sense.
Thanks,
-john
smime.p7s
Last updated: Apr 25 2024 at 16:19 UTC