Nicer names in FindTheorems.
authorTimothy Bourke
Mon Feb 09 17:25:07 2009 +1100 (2009-02-09)
changeset 29848a7c164e228e1
parent 29847 af32126ee729
child 29851 55ddff2ed906
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.
src/Pure/General/name_space.ML
src/Pure/Isar/find_theorems.ML
src/Pure/facts.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Feb 09 17:21:46 2009 +0000
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Feb 09 17:25:07 2009 +1100
     1.3 @@ -133,10 +133,19 @@
     1.4    | SOME ((name :: _, _), _) => (name, false)
     1.5    | SOME (([], name' :: _), _) => (hidden name', true));
     1.6  
     1.7 -fun get_accesses (NameSpace (_, tab)) name =
     1.8 +fun ex_mapsto_in (NameSpace (tab, _)) name xname =
     1.9 +    (case Symtab.lookup tab xname of
    1.10 +      SOME ((name'::_, _), _) => name' = name
    1.11 +    | _ => false);
    1.12 +
    1.13 +fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
    1.14    (case Symtab.lookup tab name of
    1.15      NONE => [name]
    1.16 -  | SOME (xnames, _) => xnames);
    1.17 +  | SOME (xnames, _) => if valid_only
    1.18 +                        then filter (ex_mapsto_in ns name) xnames
    1.19 +                        else xnames);
    1.20 +
    1.21 +val get_accesses = get_accesses' true;
    1.22  
    1.23  fun put_accesses name xnames (NameSpace (tab, xtab)) =
    1.24    NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
    1.25 @@ -160,7 +169,7 @@
    1.26    in
    1.27      if ! long_names then name
    1.28      else if ! short_names then base name
    1.29 -    else ext (get_accesses space name)
    1.30 +    else ext (get_accesses' false space name)
    1.31    end;
    1.32  
    1.33  
    1.34 @@ -194,7 +203,7 @@
    1.35        space
    1.36        |> add_name' name name
    1.37        |> fold (del_name name) (if fully then names else names inter_string [base name])
    1.38 -      |> fold (del_name_extra name) (get_accesses space name)
    1.39 +      |> fold (del_name_extra name) (get_accesses' false space name)
    1.40      end;
    1.41  
    1.42  
     2.1 --- a/src/Pure/Isar/find_theorems.ML	Mon Feb 09 17:21:46 2009 +0000
     2.2 +++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 09 17:25:07 2009 +1100
     2.3 @@ -267,12 +267,7 @@
     2.4      | ord => ord)
     2.5    | ord => ord) <> GREATER;
     2.6  
     2.7 -fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
     2.8 -      nicer_name (x, i) (y, j)
     2.9 -  | nicer (Facts.Fact _) (Facts.Named _) = true
    2.10 -  | nicer (Facts.Named _) (Facts.Fact _) = false;
    2.11 -
    2.12 -fun rem_cdups xs =
    2.13 +fun rem_cdups nicer xs =
    2.14    let
    2.15      fun rem_c rev_seen [] = rev rev_seen
    2.16        | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
    2.17 @@ -284,10 +279,26 @@
    2.18  
    2.19  in
    2.20  
    2.21 -fun rem_thm_dups xs =
    2.22 +fun nicer_shortest ctxt = let
    2.23 +    val ns = ProofContext.theory_of ctxt
    2.24 +             |> PureThy.facts_of
    2.25 +             |> Facts.space_of;
    2.26 +
    2.27 +    val len_sort = sort (int_ord o (pairself size));
    2.28 +    fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
    2.29 +                       [] => s
    2.30 +                     | s'::_ => s');
    2.31 +
    2.32 +    fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
    2.33 +          nicer_name (shorten x, i) (shorten y, j)
    2.34 +      | nicer (Facts.Fact _) (Facts.Named _) = true
    2.35 +      | nicer (Facts.Named _) (Facts.Fact _) = false;
    2.36 +  in nicer end;
    2.37 +
    2.38 +fun rem_thm_dups nicer xs =
    2.39    xs ~~ (1 upto length xs)
    2.40    |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
    2.41 -  |> rem_cdups
    2.42 +  |> rem_cdups nicer
    2.43    |> sort (int_ord o pairself #2)
    2.44    |> map #1;
    2.45  
    2.46 @@ -313,7 +324,7 @@
    2.47  
    2.48      val matches =
    2.49        if rem_dups
    2.50 -      then rem_thm_dups raw_matches
    2.51 +      then rem_thm_dups (nicer_shortest ctxt) raw_matches
    2.52        else raw_matches;
    2.53  
    2.54      val len = length matches;
     3.1 --- a/src/Pure/facts.ML	Mon Feb 09 17:21:46 2009 +0000
     3.2 +++ b/src/Pure/facts.ML	Mon Feb 09 17:25:07 2009 +1100
     3.3 @@ -20,6 +20,7 @@
     3.4    val selections: string * thm list -> (ref * thm) list
     3.5    type T
     3.6    val empty: T
     3.7 +  val space_of: T -> NameSpace.T
     3.8    val intern: T -> xstring -> string
     3.9    val extern: T -> string -> xstring
    3.10    val lookup: Context.generic -> T -> string -> (bool * thm list) option