src/Pure/Isar/find_consts.ML
author kleing
Fri Feb 13 08:00:46 2009 +1100 (2009-02-13)
changeset 29884 74c183927054
child 29895 0e70a29d3e02
permissions -rw-r--r--
added ML file for the find_consts command
kleing@29884
     1
(*  Title:      find_consts.ML
kleing@29884
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
kleing@29884
     3
kleing@29884
     4
  Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
kleing@29884
     5
  over constants, but matching is not fuzzy
kleing@29884
     6
*)
kleing@29884
     7
kleing@29884
     8
signature FIND_CONSTS =
kleing@29884
     9
sig
kleing@29884
    10
  datatype criterion = Strict of string
kleing@29884
    11
                     | Loose of string
kleing@29884
    12
                     | Name of string
kleing@29884
    13
kleing@29884
    14
  val default_criteria : (bool * criterion) list ref
kleing@29884
    15
kleing@29884
    16
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    17
end;
kleing@29884
    18
kleing@29884
    19
structure FindConsts : FIND_CONSTS =
kleing@29884
    20
struct
kleing@29884
    21
kleing@29884
    22
datatype criterion = Strict of string
kleing@29884
    23
                   | Loose of string
kleing@29884
    24
                   | Name of string;
kleing@29884
    25
kleing@29884
    26
val default_criteria = ref [(false, Name ".sko_")];
kleing@29884
    27
kleing@29884
    28
fun add_tye (_, (_, t)) n = size_of_typ t + n;
kleing@29884
    29
kleing@29884
    30
fun matches_subtype thy typat = let
kleing@29884
    31
    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
kleing@29884
    32
kleing@29884
    33
    fun fs [] = false
kleing@29884
    34
      | fs (t::ts) = f t orelse fs ts
kleing@29884
    35
kleing@29884
    36
    and f (t as Type (_, ars)) = p t orelse fs ars
kleing@29884
    37
      | f t = p t;
kleing@29884
    38
  in f end;
kleing@29884
    39
kleing@29884
    40
fun check_const p (nm, (ty, _)) = if p (nm, ty)
kleing@29884
    41
                                  then SOME (size_of_typ ty)
kleing@29884
    42
                                  else NONE;
kleing@29884
    43
kleing@29884
    44
fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
kleing@29884
    45
                                    then NONE else SOME (size_of_typ ty);
kleing@29884
    46
kleing@29884
    47
fun find_consts ctxt raw_criteria = let
kleing@29884
    48
    val thy = ProofContext.theory_of ctxt;
kleing@29884
    49
    val low_ranking = 10000;
kleing@29884
    50
kleing@29884
    51
    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
kleing@29884
    52
                            |> type_of;
kleing@29884
    53
kleing@29884
    54
    fun make_match (Strict arg) =
kleing@29884
    55
          let val qty = make_pattern arg; in
kleing@29884
    56
            fn (_, (ty, _)) => let
kleing@29884
    57
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
kleing@29884
    58
                val sub_size = Vartab.fold add_tye tye 0;
kleing@29884
    59
              in SOME sub_size end handle MATCH => NONE
kleing@29884
    60
          end
kleing@29884
    61
kleing@29884
    62
      | make_match (Loose arg) =
kleing@29884
    63
          check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884
    64
      
kleing@29884
    65
      | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884
    66
kleing@29884
    67
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
kleing@29884
    68
    val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
kleing@29884
    69
kleing@29884
    70
    val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
kleing@29884
    71
kleing@29884
    72
    fun filter_const (_, NONE) = NONE
kleing@29884
    73
      | filter_const (f, (SOME (c, r))) = Option.map
kleing@29884
    74
                                            (pair c o ((curry Int.min) r))
kleing@29884
    75
                                            (f c);
kleing@29884
    76
kleing@29884
    77
    fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
kleing@29884
    78
kleing@29884
    79
    fun show (nm, ty) = let
kleing@29884
    80
        val ty' = Logic.unvarifyT ty;
kleing@29884
    81
      in
kleing@29884
    82
        (Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
kleing@29884
    83
                       Pretty.str "::", Pretty.brk 1,
kleing@29884
    84
                       Pretty.quote (Syntax.pretty_typ ctxt ty')])
kleing@29884
    85
      end;
kleing@29884
    86
  in
kleing@29884
    87
    Symtab.fold (cons o eval_entry) consts []
kleing@29884
    88
    |> map_filter I
kleing@29884
    89
    |> sort (rev_order o int_ord o pairself snd)
kleing@29884
    90
    |> map ((apsnd fst) o fst)
kleing@29884
    91
    |> map show
kleing@29884
    92
    |> Pretty.big_list "results:"
kleing@29884
    93
    |> Pretty.writeln
kleing@29884
    94
  end handle ERROR s => Output.error_msg s
kleing@29884
    95
kleing@29884
    96
end;
kleing@29884
    97