src/Pure/Isar/find_consts.ML
changeset 30242 aea5d7fa7ef5
parent 30241 3a1aef73b2b2
parent 30236 e70dae49dc57
child 30244 48543b307e99
child 30251 7aec011818e0
child 30257 06b2d7f9f64b
     1.1 --- a/src/Pure/Isar/find_consts.ML	Wed Mar 04 11:05:02 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,120 +0,0 @@
     1.4 -(*  Title:      find_consts.ML
     1.5 -    Author:     Timothy Bourke and Gerwin Klein, NICTA
     1.6 -
     1.7 -  Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
     1.8 -  over constants, but matching is not fuzzy
     1.9 -*)
    1.10 -
    1.11 -signature FIND_CONSTS =
    1.12 -sig
    1.13 -  datatype criterion = Strict of string
    1.14 -                     | Loose of string
    1.15 -                     | Name of string
    1.16 -
    1.17 -  val default_criteria : (bool * criterion) list ref
    1.18 -
    1.19 -  val find_consts : Proof.context -> (bool * criterion) list -> unit
    1.20 -end;
    1.21 -
    1.22 -structure FindConsts : FIND_CONSTS =
    1.23 -struct
    1.24 -
    1.25 -datatype criterion = Strict of string
    1.26 -                   | Loose of string
    1.27 -                   | Name of string;
    1.28 -
    1.29 -val default_criteria = ref [(false, Name ".sko_")];
    1.30 -
    1.31 -fun add_tye (_, (_, t)) n = size_of_typ t + n;
    1.32 -
    1.33 -fun matches_subtype thy typat = let
    1.34 -    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    1.35 -
    1.36 -    fun fs [] = false
    1.37 -      | fs (t::ts) = f t orelse fs ts
    1.38 -
    1.39 -    and f (t as Type (_, ars)) = p t orelse fs ars
    1.40 -      | f t = p t;
    1.41 -  in f end;
    1.42 -
    1.43 -fun check_const p (nm, (ty, _)) = if p (nm, ty)
    1.44 -                                  then SOME (size_of_typ ty)
    1.45 -                                  else NONE;
    1.46 -
    1.47 -fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
    1.48 -                                    then NONE else SOME (size_of_typ ty);
    1.49 -
    1.50 -fun filter_const (_, NONE) = NONE
    1.51 -  | filter_const (f, (SOME (c, r))) = Option.map
    1.52 -                                        (pair c o ((curry Int.min) r)) (f c);
    1.53 -
    1.54 -fun pretty_criterion (b, c) =
    1.55 -  let
    1.56 -    fun prfx s = if b then s else "-" ^ s;
    1.57 -  in
    1.58 -    (case c of
    1.59 -      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    1.60 -    | Loose pat => Pretty.str (prfx (quote pat))
    1.61 -    | Name name => Pretty.str (prfx "name: " ^ quote name))
    1.62 -  end;
    1.63 -
    1.64 -fun pretty_const ctxt (nm, ty) = let
    1.65 -    val ty' = Logic.unvarifyT ty;
    1.66 -  in
    1.67 -    Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    1.68 -                  Pretty.str "::", Pretty.brk 1,
    1.69 -                  Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.70 -  end;
    1.71 -
    1.72 -fun find_consts ctxt raw_criteria = let
    1.73 -    val start = start_timing ();
    1.74 -
    1.75 -    val thy = ProofContext.theory_of ctxt;
    1.76 -    val low_ranking = 10000;
    1.77 -
    1.78 -    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
    1.79 -                            |> type_of;
    1.80 -
    1.81 -    fun make_match (Strict arg) =
    1.82 -          let val qty = make_pattern arg; in
    1.83 -            fn (_, (ty, _)) => let
    1.84 -                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    1.85 -                val sub_size = Vartab.fold add_tye tye 0;
    1.86 -              in SOME sub_size end handle MATCH => NONE
    1.87 -          end
    1.88 -
    1.89 -      | make_match (Loose arg) =
    1.90 -          check_const (matches_subtype thy (make_pattern arg) o snd)
    1.91 -      
    1.92 -      | make_match (Name arg) = check_const (match_string arg o fst);
    1.93 -
    1.94 -    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
    1.95 -    val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
    1.96 -
    1.97 -    val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    1.98 -    fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
    1.99 -
   1.100 -    val matches = Symtab.fold (cons o eval_entry) consts []
   1.101 -                  |> map_filter I
   1.102 -                  |> sort (rev_order o int_ord o pairself snd)
   1.103 -                  |> map ((apsnd fst) o fst);
   1.104 -
   1.105 -    val end_msg = " in " ^
   1.106 -                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
   1.107 -                  ^ " secs"
   1.108 -  in
   1.109 -    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   1.110 -      :: Pretty.str ""
   1.111 -      :: (Pretty.str o concat)
   1.112 -           (if null matches
   1.113 -            then ["nothing found", end_msg]
   1.114 -            else ["found ", (string_of_int o length) matches,
   1.115 -                  " constants", end_msg, ":"])
   1.116 -      :: Pretty.str ""
   1.117 -      :: map (pretty_const ctxt) matches
   1.118 -    |> Pretty.chunks
   1.119 -    |> Pretty.writeln
   1.120 -  end handle ERROR s => Output.error_msg s
   1.121 -
   1.122 -end;
   1.123 -