Re: [isabelle] rep_datatype and Datatype exception



On Thu, Dec 16, 2010 at 2:28 AM, Mathieu Giorgino
<mathieu.giorgino at irit.fr> wrote:
> I'm trying to use rep_datatype command, however I'm getting an exception
> "Datatype" and I'm not sure why.

> typedef 'a list2 = "UNIV:: 'a list set" ..
>
> definition Nil2 :: "'a list2" where "Nil2 = Abs_list2 []"

> fun Cons2' :: "('a * 'a list2) \<Rightarrow> 'a list2" where
>  "Cons2' (a, as) = Abs_list2 (a # Rep_list2 as)"
>
> rep_datatype Nil2 Cons2' (* exception Datatype raised
>        (line 218 of "~~/src/HOL/Tools/Datatype/datatype_aux.ML") *)
> ------
>
> What does this exception mean ?

Hi Mathieu,

This is a bug. "Datatype" is an exception used internally in the
implementation of "rep_datatype"; users are never supposed to see it.

It appears that while "rep_datatype" supports mutual recursion, it has
problems with indirect-recursive datatypes like your "list2" type.
(Indirect recursion means that a recursive type appears as a parameter
of another datatype. In your case, type "'a list2" appears inside a
product type.)

To the Isabelle developers: I was able to get a little further on this
example by modifying HOL/Tools/Datatype/datatype_data.ML like this:

     val descr = map_index mk_spec cs;
     val injs = Datatype_Prop.make_injs [descr] vs;
     val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
-    val ind = Datatype_Prop.make_ind [descr] vs;
+    val dt_info = get_all thy;
+    val (descrs, _) = unfold_datatypes thy descr vs dt_info descr (length cs);
+    val ind = Datatype_Prop.make_ind descrs vs;
     val rules = (map o map o map) Logic.close_form [[[ind]], injs,
half_distincts];

Now the rep_datatype command produces the right goals for me to prove,
but it raises another Datatype exception after I finish the proof.
Maybe whoever is currently maintaining the datatype package (Stefan or
Florian?) can follow up on this.

- Brian





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