explicit type for search queries
authorkrauss
Mon May 30 17:07:48 2011 +0200 (2011-05-30)
changeset 430700318781be055
parent 43069 88e45168272c
child 43071 c9859f634cef
explicit type for search queries
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -13,6 +13,13 @@
     1.4    datatype theorem =
     1.5      Internal of Facts.ref * thm | External of Facts.ref * term
     1.6  
     1.7 +  type 'term query = {
     1.8 +    goal: thm option,
     1.9 +    limit: int option,
    1.10 +    rem_dups: bool,
    1.11 +    criteria: (bool * 'term criterion) list
    1.12 +  }
    1.13 +
    1.14    val tac_limit: int Unsynchronized.ref
    1.15    val limit: int Unsynchronized.ref
    1.16  
    1.17 @@ -23,11 +30,10 @@
    1.18      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.19    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    1.20      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    1.21 -  val filter_theorems: Proof.context -> theorem list -> thm option ->
    1.22 -    int option -> bool -> (bool * term criterion) list ->
    1.23 +
    1.24 +  val filter_theorems: Proof.context -> theorem list -> term query ->
    1.25      int option * theorem list
    1.26 -  val filter_theorems_cmd: Proof.context -> theorem list -> thm option ->
    1.27 -    int option -> bool -> (bool * string criterion) list ->
    1.28 +  val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
    1.29      int option * theorem list
    1.30  
    1.31    val pretty_theorem: Proof.context -> theorem -> Pretty.T
    1.32 @@ -90,6 +96,19 @@
    1.33    end;
    1.34  
    1.35  
    1.36 +(** queries **)
    1.37 +
    1.38 +type 'term query = {
    1.39 +  goal: thm option,
    1.40 +  limit: int option,
    1.41 +  rem_dups: bool,
    1.42 +  criteria: (bool * 'term criterion) list
    1.43 +};
    1.44 +
    1.45 +fun map_criteria f {goal, limit, rem_dups, criteria} =
    1.46 +  {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
    1.47 +
    1.48 +
    1.49  (** theorems, either internal or external (without proof) **)
    1.50  
    1.51  datatype theorem =
    1.52 @@ -429,8 +448,9 @@
    1.53  
    1.54  val limit = Unsynchronized.ref 40;
    1.55  
    1.56 -fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria =
    1.57 +fun filter_theorems ctxt theorems query =
    1.58    let
    1.59 +    val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query
    1.60      val filters = map (filter_criterion ctxt opt_goal) criteria;
    1.61  
    1.62      fun find_all theorems =
    1.63 @@ -453,9 +473,9 @@
    1.64  
    1.65    in find theorems end;
    1.66  
    1.67 -fun filter_theorems_cmd ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
    1.68 -  filter_theorems ctxt theorems opt_goal opt_limit rem_dups
    1.69 -    (map (apsnd (read_criterion ctxt)) raw_criteria);
    1.70 +fun filter_theorems_cmd ctxt theorems raw_query = 
    1.71 +  filter_theorems ctxt theorems (map_criteria 
    1.72 +    (map (apsnd (read_criterion ctxt))) raw_query);
    1.73  
    1.74  fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.75    let
    1.76 @@ -465,8 +485,8 @@
    1.77      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
    1.78      val opt_goal' = Option.map add_prems opt_goal;
    1.79    in
    1.80 -    filter ctxt (map Internal (all_facts_of ctxt)) opt_goal' opt_limit
    1.81 -       rem_dups raw_criteria
    1.82 +    filter ctxt (map Internal (all_facts_of ctxt)) 
    1.83 +      {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria}
    1.84      |> apsnd (map (fn Internal f => f))
    1.85    end;
    1.86  
    1.87 @@ -488,7 +508,7 @@
    1.88  
    1.89      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.90      val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
    1.91 -      opt_goal opt_limit rem_dups criteria;
    1.92 +      {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
    1.93      val returned = length theorems;
    1.94  
    1.95      val tally_msg =