src/Pure/Tools/find_consts.ML
changeset 30142 8d6145694bb5
parent 29895 0e70a29d3e02
child 30143 98a986b02022
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Fri Feb 27 15:46:22 2009 +0100
     1.3 @@ -0,0 +1,146 @@
     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 +
   1.123 +
   1.124 +(** command syntax **)
   1.125 +
   1.126 +fun find_consts_cmd spec =
   1.127 +  Toplevel.unknown_theory o Toplevel.keep (fn state =>
   1.128 +    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
   1.129 +
   1.130 +local
   1.131 +
   1.132 +structure P = OuterParse and K = OuterKeyword;
   1.133 +
   1.134 +val criterion =
   1.135 +  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   1.136 +  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   1.137 +  P.xname >> Loose;
   1.138 +
   1.139 +in
   1.140 +
   1.141 +val _ =
   1.142 +  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   1.143 +    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   1.144 +      >> (Toplevel.no_timing oo find_consts_cmd));
   1.145 +
   1.146 +end;
   1.147 +
   1.148 +end;
   1.149 +