Merge revs 8491, 8495-7 and 8510 (Hol_datatype bugs) into K6 release.

doc/kananaskis-6.release.html

@@ -211,6 +211,16 @@ <h2 id="bugs-fixed">Bugs fixed:</h2>
 types where the new type was also polymorphic failed.  Thanks to Ramana
 Kumar for the report of this bug. </p>
 
+<li><p>In <code>Hol_datatype</code>, nested recursion involving
+the <code>itself</code> type constructor could fail.  Thanks to Ramana
+Kumar for the report of and fix for this bug. </p>
+
+<li><p>The <code>TypeNet</code> data structure for indexing
+information by types could get confused if the “same” type was
+redefined (in the one interactive session) with different arities.
+Thanks to Ramana Kumar for the bug report that led to the isolation of
+this problem.</p>
+
 </ul>
 
 

src/bool/Prim_rec.sml

@@ -370,33 +370,34 @@ fun type_constructors ax name =
   map (#1 o strip_comb) (type_constructors_with_args ax name)
 
 
-(* return all of the types defined by an axiom, formerly "new_types". *)
-fun doms_of_tyaxiom ax =
- let val (evs, _) = strip_exists (#2 (strip_forall (concl ax)))
-     val candidate_types = map (#1 o dom_rng o type_of) evs
-     fun isop_applied_to_other ty = List.exists
-           (fn ty' => Lib.mem ty' candidate_types) (snd (dest_type ty))
- in
-    List.filter (not o isop_applied_to_other) candidate_types
- end
+local
+  fun only_variable_args ty = List.all (not o is_type) (snd (dest_type ty))
+  fun only_new types = List.filter only_variable_args types
+in
+  (* return all of the types defined by an axiom, formerly "new_types". *)
+  fun doms_of_tyaxiom ax =
+   let val (evs, _) = strip_exists (#2 (strip_forall (concl ax)))
+       val candidate_types = map (#1 o dom_rng o type_of) evs
+   in
+      only_new candidate_types
+   end
 
-(*---------------------------------------------------------------------------
-    similarly for an induction theorem, which will be of the form
+  (*---------------------------------------------------------------------------
+      similarly for an induction theorem, which will be of the form
 
-      !P1 .. PN.
-         c1 /\ ... /\ cn ==> (!x. P1 x) /\ (!x. P2 x) ... /\ (!x. PN x)
+        !P1 .. PN.
+           c1 /\ ... /\ cn ==> (!x. P1 x) /\ (!x. P2 x) ... /\ (!x. PN x)
 
-   Formerly "new_types_from_ind"
- ---------------------------------------------------------------------------*)
+     Formerly "new_types_from_ind"
+   ---------------------------------------------------------------------------*)
 
-fun doms_of_ind_thm ind =
- let val conclusions = strip_conj(#2(strip_imp(#2(strip_forall(concl ind)))))
-     val candidate_types = map (type_of o fst o dest_forall) conclusions
-     fun isop_applied_to_other ty = List.exists
-            (fn ty' => Lib.mem ty' candidate_types) (snd (dest_type ty))
- in
-   List.filter (not o isop_applied_to_other) candidate_types
- end
+  fun doms_of_ind_thm ind =
+   let val conclusions = strip_conj(#2(strip_imp(#2(strip_forall(concl ind)))))
+       val candidate_types = map (type_of o fst o dest_forall) conclusions
+   in
+     only_new candidate_types
+   end
+end
 
 (*---------------------------------------------------------------------------*
  * Define a case constant for a datatype. This is used by TFL's              *

src/bool/selftest.sml

@@ -246,6 +246,14 @@ val _ = set_trace "Unicode" 0
 val _ = set_trace "Unicode" 1
 val _ = checkparse ()
 
+(* test for type abbreviation bug caused by stale types in a TypeNet.*)
+val _ = tprint "Testing stale type abbreviations bug"
+val _ = new_type ("foo", 1)
+val _ = type_abbrev("bar", ``:bool foo``)
+val _ = new_type ("foo", 0)
+val _ = type_abbrev("baz", ``:foo``) handle _ => die "FAILED!"
+val _ = print "OK\n"
+
 
 (* pretty-printing tests - turn Unicode off *)
 val _ = set_trace "Unicode" 0

src/datatype/selftest.sml

@@ -159,6 +159,18 @@ val result = ind_types.define_type spec' handle e => Raise e;
 val _ = Hol_datatype`pointer = pnil | pref of 'a`
 val _ = Hol_datatype`failure = <| head : 'a pointer; tail : failure pointer |>`
 
+(* Ramana Kumar's examples from 2010/08/25 *)
+val _ = Hol_datatype `t1 = c1 of 'a => t1 itself `;
+val _ = Hol_datatype `t2 = c2 of t2 t1 itself ` ;
+
+val _ = Hol_datatype `u1 = d1 of 'a itself`;
+val _ = Hol_datatype `u2 = d2 of 'a u1 `;
+val _ = Hol_datatype `u3 = d3 of u4 u2 u1 ;
+                      u4 = d4 of u3 u1 `;
+
+(* Ramana Kumar's TypeNet bug from 2010/08/25 *)
+val _ = Hol_datatype `foo = fooC of 'a`
+val _ = Hol_datatype `foo = fooC' of num`
 
 fun tprint s = print (StringCvt.padRight #" " 70 s)
 

src/parse/TypeNet.sml

@@ -3,14 +3,37 @@ struct
 
 open HolKernel
 
-datatype label = TV | TOP of {Thy : string, Tyop : string}
+datatype label = TV
+               | TOP of {Thy : string, Tyop : string} * int
+  (* The integer records arity of operator - this is necessary when
+     types are redefined.  If the old and new versions have the
+     same arity, all is well, but if they are different then the data
+     structure expects the wrong thing.
+
+     For example, if scratch$foo is of arity 1, then there will be a
+     ND node beneath it (where the argument gets treated).  But if
+     the user dumps that foo, and replaces it with one of arity 0, an
+     attempt to follow the tree will find the node that was right before
+     when it should be a leaf.
+
+     If the user does a lot of this, the data structure will slowly fill
+     up with garbage.  If a type gets replaced with a new one of the same
+     arity, the data for the old type will be returned as part of a
+     Binarymap.listItems when "match" is called, but the user will eliminate
+     the junk with the usual sort of call to match_type.  With "peek", the
+     old data won't be called because the lookup at the leaf's Binarymap
+     will just find whatever's supposed to be associated with the new type.
+  *)
+
+fun reccmp ({Thy=th1,Tyop=op1}, {Thy=th2,Tyop=op2}) =
+    pair_compare(String.compare, String.compare) ((op1,th1),(op2,th2))
 
 fun labcmp p =
     case p of
       (TV, TV) => EQUAL
     | (TV, TOP _) => LESS
-    | (TOP{Thy = thy1, Tyop = op1}, TOP{Thy = thy2, Tyop = op2}) =>
-      pair_compare(String.compare, String.compare) ((op1,thy1),(op2,thy2))
+    | (TOP opdata1, TOP opdata2) =>
+         pair_compare(reccmp, Int.compare) (opdata1, opdata2)
     | (TOP _, TV) => GREATER
 
 datatype 'a N = LF of (hol_type,'a) Binarymap.dict
@@ -30,7 +53,7 @@ fun ndest_type ty =
     else let
         val  {Thy,Tyop,Args} = dest_thy_type ty
       in
-        (TOP{Thy=Thy,Tyop=Tyop}, Args)
+        (TOP({Thy=Thy,Tyop=Tyop},length Args), Args)
       end
 
 fun insert ((net,sz), ty, item) = let
@@ -188,4 +211,4 @@ end
 fun transform f = map (fn (k,v) => f v)
 
 
-end (* struct *)
+end (* struct *)