Re: [isabelle] exception using "case ... of ..." with HOLCF



Am 05.12.2013 17:28, schrieb Florian Haftmann:
when I tried to adapt Isabelle/HOLCF Prelude (e.g.,

   hg clone http://hg.code.sf.net/p/holcf-prelude/code holcf-prelude

) to Isabelle2013-2-RC3 I got an exception in the definition of

   fixrec scanr :: "('a → 'b → 'b) → 'b → ['a] → ['b]" where
   "scanr⋅f⋅q0⋅[] = [q0]" |
   "scanr⋅f⋅q0⋅(x : xs) = (
     let qs = scanr⋅f⋅q0⋅xs in
     (case qs of
       [] ⇒ ⊥
     | q : _ ⇒ f⋅x⋅q : qs))"

(and similar definitions). The error message is

   exception TERM raised (line 142 of "Syntax/syntax_trans.ML"):
   binder_tr: _cabs
   \<^const>dummy_pattern
   \<^const>Cfun.Rep_cfun (\<^const>Cfun.Rep_cfun
\<^const>Data_List.list.Cons (\<^const>Cfun.Rep_cfun
(\<^const>Cfun.Rep_cfun f x) q)) qs

What is this supposed to tell me? ;)
Good question.  Maybe it is related to recent renovations in the case
syntax!?  Any experts in this and/or HOLCF?

	Florian
The recent renovations of the case syntax are not used in HOLCF. There was a thread on this earlier (which didn't lead to any reasonable code changes AFAIK):

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-April/004067.html

Dmitriy




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