--- a/src/Pure/Tools/find_consts.ML Fri Feb 27 15:46:22 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML Fri Feb 27 16:05:40 2009 +0100
@@ -1,15 +1,16 @@
-(* Title: find_consts.ML
+(* Title: Pure/Tools/find_consts.ML
Author: Timothy Bourke and Gerwin Klein, NICTA
- Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
- over constants, but matching is not fuzzy
+Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
+type over constants, but matching is not fuzzy.
*)
signature FIND_CONSTS =
sig
- datatype criterion = Strict of string
- | Loose of string
- | Name of string
+ datatype criterion =
+ Strict of string
+ | Loose of string
+ | Name of string
val default_criteria : (bool * criterion) list ref
@@ -19,34 +20,46 @@
structure FindConsts : FIND_CONSTS =
struct
-datatype criterion = Strict of string
- | Loose of string
- | Name of string;
+(* search criteria *)
+
+datatype criterion =
+ Strict of string
+ | Loose of string
+ | Name of string;
val default_criteria = ref [(false, Name ".sko_")];
-fun add_tye (_, (_, t)) n = size_of_typ t + n;
+
+(* matching types/consts *)
-fun matches_subtype thy typat = let
+fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
+
+fun matches_subtype thy typat =
+ let
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
fun fs [] = false
- | fs (t::ts) = f t orelse fs ts
+ | fs (t :: ts) = f t orelse fs ts
and f (t as Type (_, ars)) = p t orelse fs ars
| f t = p t;
in f end;
-fun check_const p (nm, (ty, _)) = if p (nm, ty)
- then SOME (size_of_typ ty)
- else NONE;
+fun check_const p (nm, (ty, _)) =
+ if p (nm, ty)
+ then SOME (Term.size_of_typ ty)
+ else NONE;
-fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
- then NONE else SOME (size_of_typ ty);
+fun opt_not f (c as (_, (ty, _))) =
+ if is_some (f c)
+ then NONE else SOME (Term.size_of_typ ty);
fun filter_const (_, NONE) = NONE
- | filter_const (f, (SOME (c, r))) = Option.map
- (pair c o ((curry Int.min) r)) (f c);
+ | filter_const (f, (SOME (c, r))) =
+ Option.map (pair c o (curry Int.min r)) (f c);
+
+
+(* pretty results *)
fun pretty_criterion (b, c) =
let
@@ -58,26 +71,32 @@
| Name name => Pretty.str (prfx "name: " ^ quote name))
end;
-fun pretty_const ctxt (nm, ty) = let
+fun pretty_const ctxt (nm, ty) =
+ let
val ty' = Logic.unvarifyT ty;
in
- Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1,
- Pretty.quote (Syntax.pretty_typ ctxt ty')]
+ Pretty.block
+ [Pretty.quote (Pretty.str nm), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
-fun find_consts ctxt raw_criteria = let
+
+(* find_consts *)
+
+fun find_consts ctxt raw_criteria =
+ let
val start = start_timing ();
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
- fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
- |> type_of;
+ fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> Term.type_of;
fun make_match (Strict arg) =
let val qty = make_pattern arg; in
- fn (_, (ty, _)) => let
+ fn (_, (ty, _)) =>
+ let
val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
val sub_size = Vartab.fold add_tye tye 0;
in SOME sub_size end handle MATCH => NONE
@@ -89,15 +108,16 @@
| make_match (Name arg) = check_const (match_string arg o fst);
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
- val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
+ val criteria = map make_criterion (! default_criteria @ raw_criteria);
val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
- val matches = Symtab.fold (cons o eval_entry) consts []
- |> map_filter I
- |> sort (rev_order o int_ord o pairself snd)
- |> map ((apsnd fst) o fst);
+ val matches =
+ Symtab.fold (cons o eval_entry) consts []
+ |> map_filter I
+ |> sort (rev_order o int_ord o pairself snd)
+ |> map ((apsnd fst) o fst);
val end_msg = " in " ^
(List.nth (String.tokens Char.isSpace (end_timing start), 3))
@@ -114,11 +134,10 @@
:: map (pretty_const ctxt) matches
|> Pretty.chunks
|> Pretty.writeln
- end handle ERROR s => Output.error_msg s
+ end handle ERROR s => Output.error_msg s;
-
-(** command syntax **)
+(* command syntax *)
fun find_consts_cmd spec =
Toplevel.unknown_theory o Toplevel.keep (fn state =>
--- a/src/Pure/Tools/find_theorems.ML Fri Feb 27 15:46:22 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Fri Feb 27 16:05:40 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: Pure/Isar/find_theorems.ML
+(* Title: Pure/Tools/find_theorems.ML
Author: Rafal Kolanski and Gerwin Klein, NICTA
Retrieve theorems from proof context.
@@ -163,17 +163,20 @@
val tac_limit = ref 5;
-fun filter_solves ctxt goal = let
- val baregoal = Logic.get_goal (prop_of goal) 1;
+fun filter_solves ctxt goal =
+ let
+ val baregoal = Logic.get_goal (Thm.prop_of goal) 1;
- fun etacn thm i = Seq.take (!tac_limit) o etac thm i;
- fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal
- else (etacn thm THEN_ALL_NEW
- (Goal.norm_hhf_tac THEN'
- Method.assumption_tac ctxt)) 1 goal;
+ fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
+ fun try_thm thm =
+ if Thm.no_prems thm then rtac thm 1 goal
+ else (etacn thm THEN_ALL_NEW
+ (Goal.norm_hhf_tac THEN'
+ Method.assumption_tac ctxt)) 1 goal;
in
- fn (_, thm) => if (is_some o Seq.pull o try_thm) thm
- then SOME (Thm.nprems_of thm, 0) else NONE
+ fn (_, thm) =>
+ if (is_some o Seq.pull o try_thm) thm
+ then SOME (Thm.nprems_of thm, 0) else NONE
end;
@@ -195,18 +198,20 @@
fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
- (* Including all constants and frees is only sound because
- matching uses higher-order patterns. If full matching
- were used, then constants that may be subject to
- beta-reduction after substitution of frees should
- not be included for LHS set because they could be
- thrown away by the substituted function.
- e.g. for (?F 1 2) do not include 1 or 2, if it were
- possible for ?F to be (% x y. 3)
- The largest possible set should always be included on
- the RHS. *)
-fun filter_pattern ctxt pat = let
+(*Including all constants and frees is only sound because
+ matching uses higher-order patterns. If full matching
+ were used, then constants that may be subject to
+ beta-reduction after substitution of frees should
+ not be included for LHS set because they could be
+ thrown away by the substituted function.
+ e.g. for (?F 1 2) do not include 1 or 2, if it were
+ possible for ?F to be (% x y. 3)
+ The largest possible set should always be included on
+ the RHS.*)
+
+fun filter_pattern ctxt pat =
+ let
val pat_consts = get_names pat;
fun check (t, NONE) = check (t, SOME (get_thm_names t))
@@ -233,12 +238,9 @@
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
| filter_crit _ NONE Solves = err_no_goal "solves"
- | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt
- (fix_goal goal))
- | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt
- (fix_goal goal))
- | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt
- (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
@@ -248,11 +250,13 @@
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
| opt_add _ _ = NONE;
-fun app_filters thm = let
+fun app_filters thm =
+ let
fun app (NONE, _, _) = NONE
| app (SOME v, consts, []) = SOME (v, thm)
- | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts)
- in app (opt_add r r', consts', fs) end;
+ | app (r, consts, f :: fs) =
+ let val (r', consts') = f (thm, consts)
+ in app (opt_add r r', consts', fs) end;
in app end;
in
@@ -302,7 +306,8 @@
in
-fun nicer_shortest ctxt = let
+fun nicer_shortest ctxt =
+ let
val ns = ProofContext.theory_of ctxt
|> PureThy.facts_of
|> Facts.space_of;
@@ -354,7 +359,8 @@
else raw_matches;
in matches end;
-fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let
+fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+ let
val start = start_timing ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;