added ML file for the find_consts command
authorkleing
Fri Feb 13 08:00:46 2009 +1100 (2009-02-13)
changeset 2988474c183927054
parent 29883 14841d4c808e
child 29885 379e43e513c2
added ML file for the find_consts command
src/Pure/Isar/find_consts.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/find_consts.ML	Fri Feb 13 08:00:46 2009 +1100
     1.3 @@ -0,0 +1,97 @@
     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 find_consts ctxt raw_criteria = let
    1.51 +    val thy = ProofContext.theory_of ctxt;
    1.52 +    val low_ranking = 10000;
    1.53 +
    1.54 +    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
    1.55 +                            |> type_of;
    1.56 +
    1.57 +    fun make_match (Strict arg) =
    1.58 +          let val qty = make_pattern arg; in
    1.59 +            fn (_, (ty, _)) => let
    1.60 +                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    1.61 +                val sub_size = Vartab.fold add_tye tye 0;
    1.62 +              in SOME sub_size end handle MATCH => NONE
    1.63 +          end
    1.64 +
    1.65 +      | make_match (Loose arg) =
    1.66 +          check_const (matches_subtype thy (make_pattern arg) o snd)
    1.67 +      
    1.68 +      | make_match (Name arg) = check_const (match_string arg o fst);
    1.69 +
    1.70 +    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
    1.71 +    val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
    1.72 +
    1.73 +    val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    1.74 +
    1.75 +    fun filter_const (_, NONE) = NONE
    1.76 +      | filter_const (f, (SOME (c, r))) = Option.map
    1.77 +                                            (pair c o ((curry Int.min) r))
    1.78 +                                            (f c);
    1.79 +
    1.80 +    fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
    1.81 +
    1.82 +    fun show (nm, ty) = let
    1.83 +        val ty' = Logic.unvarifyT ty;
    1.84 +      in
    1.85 +        (Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    1.86 +                       Pretty.str "::", Pretty.brk 1,
    1.87 +                       Pretty.quote (Syntax.pretty_typ ctxt ty')])
    1.88 +      end;
    1.89 +  in
    1.90 +    Symtab.fold (cons o eval_entry) consts []
    1.91 +    |> map_filter I
    1.92 +    |> sort (rev_order o int_ord o pairself snd)
    1.93 +    |> map ((apsnd fst) o fst)
    1.94 +    |> map show
    1.95 +    |> Pretty.big_list "results:"
    1.96 +    |> Pretty.writeln
    1.97 +  end handle ERROR s => Output.error_msg s
    1.98 +
    1.99 +end;
   1.100 +