# HG changeset patch
# User Timothy Bourke
# Date 1234160707 -39600
# Node ID a7c164e228e1d808bbbeb8ac86e99e2c3e3f5dc2
# Parent  af32126ee7294399606f59382ef21ca547403a2f
Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:

  NameSpace.get_accesses has been patched to fix the following
  bug:
      theory OverHOL imports Main begin
        lemma conjI: "a & b --> b"
          by blast

        ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
  	    val x1 = NameSpace.get_accesses ns "HOL.conjI";
  	    val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
      end

  where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
  but x1 should be just ["HOL.conjI"].

  NameSpace.get_accesses is only used within the NameSpace
  structure itself. The two uses have been modified to retain
  their original behaviour.

  Note that NameSpace.valid_accesses gives different results:
      get_accesses ns "HOL.eq_class.eq"
      gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
      but,
      valid_accesses ns "HOL.eq_class.eq"
      gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]

* Patch FindTheorems:
  Prefer names that are shorter to type in the current context.

* Re-export space_of.

diff -r af32126ee729 -r a7c164e228e1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Feb 09 17:21:46 2009 +0000
+++ b/src/Pure/General/name_space.ML	Mon Feb 09 17:25:07 2009 +1100
@@ -133,10 +133,19 @@
   | SOME ((name :: _, _), _) => (name, false)
   | SOME (([], name' :: _), _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, tab)) name =
+fun ex_mapsto_in (NameSpace (tab, _)) name xname =
+    (case Symtab.lookup tab xname of
+      SOME ((name'::_, _), _) => name' = name
+    | _ => false);
+
+fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
   (case Symtab.lookup tab name of
     NONE => [name]
-  | SOME (xnames, _) => xnames);
+  | SOME (xnames, _) => if valid_only
+                        then filter (ex_mapsto_in ns name) xnames
+                        else xnames);
+
+val get_accesses = get_accesses' true;
 
 fun put_accesses name xnames (NameSpace (tab, xtab)) =
   NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
@@ -160,7 +169,7 @@
   in
     if ! long_names then name
     else if ! short_names then base name
-    else ext (get_accesses space name)
+    else ext (get_accesses' false space name)
   end;
 
 
@@ -194,7 +203,7 @@
       space
       |> add_name' name name
       |> fold (del_name name) (if fully then names else names inter_string [base name])
-      |> fold (del_name_extra name) (get_accesses space name)
+      |> fold (del_name_extra name) (get_accesses' false space name)
     end;
 
 
diff -r af32126ee729 -r a7c164e228e1 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Mon Feb 09 17:21:46 2009 +0000
+++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 09 17:25:07 2009 +1100
@@ -267,12 +267,7 @@
     | ord => ord)
   | ord => ord) <> GREATER;
 
-fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
-      nicer_name (x, i) (y, j)
-  | nicer (Facts.Fact _) (Facts.Named _) = true
-  | nicer (Facts.Named _) (Facts.Fact _) = false;
-
-fun rem_cdups xs =
+fun rem_cdups nicer xs =
   let
     fun rem_c rev_seen [] = rev rev_seen
       | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
@@ -284,10 +279,26 @@
 
 in
 
-fun rem_thm_dups xs =
+fun nicer_shortest ctxt = let
+    val ns = ProofContext.theory_of ctxt
+             |> PureThy.facts_of
+             |> Facts.space_of;
+
+    val len_sort = sort (int_ord o (pairself size));
+    fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
+                       [] => s
+                     | s'::_ => s');
+
+    fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
+          nicer_name (shorten x, i) (shorten y, j)
+      | nicer (Facts.Fact _) (Facts.Named _) = true
+      | nicer (Facts.Named _) (Facts.Fact _) = false;
+  in nicer end;
+
+fun rem_thm_dups nicer xs =
   xs ~~ (1 upto length xs)
   |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
-  |> rem_cdups
+  |> rem_cdups nicer
   |> sort (int_ord o pairself #2)
   |> map #1;
 
@@ -313,7 +324,7 @@
 
     val matches =
       if rem_dups
-      then rem_thm_dups raw_matches
+      then rem_thm_dups (nicer_shortest ctxt) raw_matches
       else raw_matches;
 
     val len = length matches;
diff -r af32126ee729 -r a7c164e228e1 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Feb 09 17:21:46 2009 +0000
+++ b/src/Pure/facts.ML	Mon Feb 09 17:25:07 2009 +1100
@@ -20,6 +20,7 @@
   val selections: string * thm list -> (ref * thm) list
   type T
   val empty: T
+  val space_of: T -> NameSpace.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option