# HG changeset patch # User krauss # Date 1306768068 -7200 # Node ID 0318781be05586708378d20837fbf744b016ba8e # Parent 88e45168272c473e37be48f2b09f5683f29e2910 explicit type for search queries diff -r 88e45168272c -r 0318781be055 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon May 30 17:07:48 2011 +0200 +++ b/src/Pure/Tools/find_theorems.ML Mon May 30 17:07:48 2011 +0200 @@ -13,6 +13,13 @@ datatype theorem = Internal of Facts.ref * thm | External of Facts.ref * term + type 'term query = { + goal: thm option, + limit: int option, + rem_dups: bool, + criteria: (bool * 'term criterion) list + } + val tac_limit: int Unsynchronized.ref val limit: int Unsynchronized.ref @@ -23,11 +30,10 @@ (bool * term criterion) list -> int option * (Facts.ref * thm) list val find_theorems_cmd: Proof.context -> thm option -> int option -> bool -> (bool * string criterion) list -> int option * (Facts.ref * thm) list - val filter_theorems: Proof.context -> theorem list -> thm option -> - int option -> bool -> (bool * term criterion) list -> + + val filter_theorems: Proof.context -> theorem list -> term query -> int option * theorem list - val filter_theorems_cmd: Proof.context -> theorem list -> thm option -> - int option -> bool -> (bool * string criterion) list -> + val filter_theorems_cmd: Proof.context -> theorem list -> string query -> int option * theorem list val pretty_theorem: Proof.context -> theorem -> Pretty.T @@ -90,6 +96,19 @@ end; +(** queries **) + +type 'term query = { + goal: thm option, + limit: int option, + rem_dups: bool, + criteria: (bool * 'term criterion) list +}; + +fun map_criteria f {goal, limit, rem_dups, criteria} = + {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria}; + + (** theorems, either internal or external (without proof) **) datatype theorem = @@ -429,8 +448,9 @@ val limit = Unsynchronized.ref 40; -fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria = +fun filter_theorems ctxt theorems query = let + val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query val filters = map (filter_criterion ctxt opt_goal) criteria; fun find_all theorems = @@ -453,9 +473,9 @@ in find theorems end; -fun filter_theorems_cmd ctxt theorems opt_goal opt_limit rem_dups raw_criteria = - filter_theorems ctxt theorems opt_goal opt_limit rem_dups - (map (apsnd (read_criterion ctxt)) raw_criteria); +fun filter_theorems_cmd ctxt theorems raw_query = + filter_theorems ctxt theorems (map_criteria + (map (apsnd (read_criterion ctxt))) raw_query); fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria = let @@ -465,8 +485,8 @@ val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); val opt_goal' = Option.map add_prems opt_goal; in - filter ctxt (map Internal (all_facts_of ctxt)) opt_goal' opt_limit - rem_dups raw_criteria + filter ctxt (map Internal (all_facts_of ctxt)) + {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria} |> apsnd (map (fn Internal f => f)) end; @@ -488,7 +508,7 @@ val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt)) - opt_goal opt_limit rem_dups criteria; + {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria}; val returned = length theorems; val tally_msg =