# HG changeset patch # User wenzelm # Date 1235747140 -3600 # Node ID 98a986b02022f92d5e6cebab5d31a0976723f73b # Parent 8d6145694bb5b2bc5c87ee2f55bce9f682a384b0 observe basic Isabelle/ML coding conventions; diff -r 8d6145694bb5 -r 98a986b02022 src/Pure/Tools/find_consts.ML --- 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 => diff -r 8d6145694bb5 -r 98a986b02022 src/Pure/Tools/find_theorems.ML --- 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;