# HG changeset patch # User wenzelm # Date 1116773479 -7200 # Node ID fbf3471214d66bb17fc15d14c5e1b213c051e258 # Parent bbfb2f1378b3506215e21fd10ff75b37634caea2 moved everything related to thms_containing to find_theorems.ML; export is_known; added fact_index_of, valid_thms; gen_read': removed unused dummies option; declare_term(_syntax): canonical argument order; removed declare_terms(_syntax); diff -r bbfb2f1378b3 -r fbf3471214d6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun May 22 16:51:18 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun May 22 16:51:19 2005 +0200 @@ -6,7 +6,6 @@ *) val show_structs = ref false; -val thms_containing_limit = ref 40; signature PROOF_CONTEXT = sig @@ -16,9 +15,11 @@ val theory_of: context -> theory val sign_of: context -> Sign.sg val is_fixed: context -> string -> bool + val is_known: context -> string -> bool val fixed_names_of: context -> string list val assumptions_of: context -> (cterm list * exporter) list val prems_of: context -> thm list + val fact_index_of: context -> FactIndex.T val print_proof_data: theory -> unit val init: theory -> context val pretty_term: context -> term -> Pretty.T @@ -55,7 +56,6 @@ val cert_term_pats: typ -> context -> term list -> term list val cert_prop_pats: context -> term list -> term list val declare_term: term -> context -> context - val declare_terms: term list -> context -> context val read_tyname: context -> string -> typ val read_const: context -> string -> term val warn_extra_tfrees: context -> context -> context @@ -91,6 +91,8 @@ val get_thm_closure: context -> thmref -> thm val get_thms: context -> thmref -> thm list val get_thms_closure: context -> thmref -> thm list + val valid_thms: context -> string * thm list -> bool + val lthms_containing: context -> FactIndex.spec -> (string * thm list) list val cond_extern: context -> string -> xstring val qualified: bool -> context -> context val restore_qualified: context -> context -> context @@ -154,9 +156,6 @@ val prems_limit: int ref val pretty_asms: context -> Pretty.T list val pretty_context: context -> Pretty.T list - datatype search_criterion = Intro | Elim | Dest | Rewrite | - Pattern of string | Name of string; - val print_thms_containing: context -> term option -> int option -> (bool * search_criterion) list -> unit end; signature PRIVATE_PROOF_CONTEXT = @@ -172,8 +171,6 @@ structure ProofContext: PRIVATE_PROOF_CONTEXT = struct -datatype search_criterion = Intro | Elim | Dest | Rewrite | - Pattern of string | Name of string; (** datatype context **) @@ -189,15 +186,9 @@ (string * thm list) list) * (*prems: A |- A *) (string * string) list, (*fixes: !!x. _*) binds: (term * typ) Vartab.table, (*term bindings*) - thms: bool * NameSpace.T * thm list Symtab.table - * FactIndex.T, (*local thms*) - (*thms is of the form (q, n, t, i) where - q: indicates whether theorems with qualified names may be stored; - this is initially forbidden (false); flag may be changed with - qualified and restore_qualified; - n: theorem namespace; - t: table of theorems; - i: index for theorem lookup (cf. thms_containing) *) + thms: bool * NameSpace.T * thm list Symtab.table * FactIndex.T, (*local thms*) + (*the bool indicates whether theorems with qualified names may be stored, + cf. 'qualified' and 'restore_qualified'*) cases: (string * RuleCases.T) list, (*local contexts*) defs: typ Vartab.table * (*type constraints*) @@ -228,6 +219,7 @@ fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms; fun prems_of (Context {asms = ((_, prems), _), ...}) = List.concat (map #2 prems); +fun fact_index_of (Context {thms = (_, _, _, idx), ...}) = idx; @@ -596,7 +588,7 @@ fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some); -fun gen_read' read app pattern dummies schematic +fun gen_read' read app pattern schematic ctxt internal more_types more_sorts more_used s = let val types = append_env (def_type ctxt pattern) more_types; @@ -608,30 +600,29 @@ | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) |> app (intern_skolem ctxt internal) |> app (if pattern then I else norm_term ctxt schematic) - |> app (if pattern then prepare_dummies else if dummies then I else reject_dummies ctxt) + |> app (if pattern then prepare_dummies else reject_dummies ctxt) end; -fun gen_read read app pattern dummies schematic ctxt = - gen_read' read app pattern dummies schematic ctxt (K false) (K NONE) (K NONE) []; +fun gen_read read app pattern schematic ctxt = + gen_read' read app pattern schematic ctxt (K false) (K NONE) (K NONE) []; in -val read_termTs = gen_read' (read_def_termTs false) (apfst o map) false false false; -val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true; +val read_termTs = gen_read' (read_def_termTs false) (apfst o map) false false; +val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false true; fun read_term_pats T ctxt = - #1 o gen_read (read_def_termTs false) (apfst o map) true false false ctxt o map (rpair T); + #1 o gen_read (read_def_termTs false) (apfst o map) true false ctxt o map (rpair T); val read_prop_pats = read_term_pats propT; fun read_term_liberal ctxt = - gen_read' (read_term_sg true) I false false false ctxt (K true) (K NONE) (K NONE) []; + gen_read' (read_term_sg true) I false false ctxt (K true) (K NONE) (K NONE) []; -val read_term = gen_read (read_term_sg true) I false false false; -val read_term_dummies = gen_read (read_term_sg true) I false true false; -val read_prop = gen_read (read_prop_sg true) I false false false; -val read_prop_schematic = gen_read (read_prop_sg true) I false false true; -val read_terms = gen_read (read_terms_sg true) map false false false; -fun read_props schematic = gen_read (read_props_sg true) map false false schematic; +val read_term = gen_read (read_term_sg true) I false false; +val read_prop = gen_read (read_prop_sg true) I false false; +val read_prop_schematic = gen_read (read_prop_sg true) I false true; +val read_terms = gen_read (read_terms_sg true) map false false; +fun read_props schematic = gen_read (read_props_sg true) map false schematic; end; @@ -687,24 +678,21 @@ fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => (thy, syntax, data, asms, binds, thms, cases, f defs)); -fun declare_syn (ctxt, t) = +in + +fun declare_term_syntax t ctxt = ctxt |> map_defaults (fn (types, sorts, used, occ) => (ins_types (types, t), sorts, used, occ)) |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ)) |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ)); -fun declare_occ (ctxt as Context {asms = (_, fixes), ...}, t) = - declare_syn (ctxt, t) +fun declare_term t (ctxt as Context {asms = (_, fixes), ...}) = + ctxt + |> declare_term_syntax t |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t))) |> map_defaults (fn (types, sorts, used, occ) => (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ)); -in - -fun declare_term t ctxt = declare_occ (ctxt, t); -fun declare_terms ts ctxt = Library.foldl declare_occ (ctxt, ts); -fun declare_terms_syntax ts ctxt = Library.foldl declare_syn (ctxt, ts); - end; @@ -736,7 +724,8 @@ val extras = Library.gen_rems Library.eq_fst (Symtab.dest occ2, Symtab.dest occ1) - |> map (fn (a, ts) => map (pair a) (List.mapPartial (try (#1 o Term.dest_Free)) ts)) |> List.concat + |> map (fn (a, ts) => map (pair a) (List.mapPartial (try (#1 o Term.dest_Free)) ts)) + |> List.concat |> List.mapPartial (fn (a, x) => (case def_type ctxt1 false (x, ~1) of NONE => SOME (a, x) | SOME T => if known_tfree a T then NONE else SOME (a, x))); @@ -759,11 +748,11 @@ | still_fixed _ = false; val occs_inner = type_occs inner; val occs_outer = type_occs outer; - fun add (gen, a) = + fun add a gen = if is_some (Symtab.lookup (occs_outer, a)) orelse exists still_fixed (Symtab.lookup_multi (occs_inner, a)) then gen else a :: gen; - in fn tfrees => Library.foldl add ([], tfrees) end; + in fn tfrees => fold add tfrees [] end; fun generalize inner outer ts = let @@ -868,8 +857,8 @@ let fun fail () = raise CONTEXT ("Pattern match failed!", ctxt); - val maxidx = Library.foldl (fn (i, (t1, t2)) => - Int.max (i, Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2))) (~1, pairs); + val maxidx = fold (fn (t1, t2) => fn i => + Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1; val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx, map swap pairs); (*prefer assignment of variables from patterns*) val env = @@ -889,18 +878,16 @@ local -fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) = +fun gen_bind prep (xi as (x, _), raw_t) ctxt = ctxt |> delete_update_binds [(xi, Option.map (prep ctxt) raw_t)]; -fun gen_binds prep binds ctxt = Library.foldl (gen_bind prep) (ctxt, binds); - in fun drop_schematic (b as (xi, SOME t)) = if null (Term.term_vars t) then b else (xi, NONE) | drop_schematic b = b; -val add_binds = gen_binds read_term; -val add_binds_i = gen_binds cert_term; +val add_binds = fold (gen_bind read_term); +val add_binds_i = fold (gen_bind cert_term); fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (sign_of ctxt) ts)); val auto_bind_goal = auto_bind AutoBind.goal; @@ -931,7 +918,8 @@ val binds'' = map (apsnd SOME) binds'; in warn_extra_tfrees ctxt - (if gen then ctxt (*sic!*) |> declare_terms (map #2 binds') |> add_binds_i binds'' + (if gen then + ctxt (*sic!*) |> fold declare_term (map #2 binds') |> add_binds_i binds'' else ctxt' |> add_binds_i binds'') end; @@ -1011,6 +999,22 @@ val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I); +(* valid_thms *) + +fun valid_thms ctxt (name, ths) = + (case try (transform_error (fn () => get_thms ctxt (name, NONE))) () of + NONE => false + | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths')); + + +(* lthms_containing *) + +fun lthms_containing ctxt spec = + FactIndex.find (fact_index_of ctxt) spec + |> List.filter (valid_thms ctxt) + |> gen_distinct eq_fst; + + (* name space operations *) fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space; @@ -1035,8 +1039,8 @@ if not override_q andalso not q andalso NameSpace.is_qualified name then raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt) else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]), - Symtab.update ((name, ths), tab), - FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs)); + Symtab.update ((name, ths), tab), FactIndex.add (is_known ctxt) (name, ths) index), + cases, defs)); fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]); fun gen_put_thmss q acc = fold (gen_put_thms q acc); @@ -1057,7 +1061,7 @@ (* note_thmss *) local - +(* FIXME foldl_map (!?) *) fun gen_note_thss get acc (ctxt, ((name, more_attrs), ths_attrs)) = let fun app ((ct, ths), (th, attrs)) = @@ -1184,7 +1188,7 @@ val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; val T = if_none opt_T TypeInfer.logicT; - val ctxt' = ctxt |> declare_terms_syntax (map (fn x => Free (x, T)) xs); + val ctxt' = ctxt |> fold declare_term_syntax (map (fn x => Free (x, T)) xs); in (ctxt', (xs, opt_T)) end; in @@ -1208,7 +1212,8 @@ fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); val declare = - declare_terms_syntax o List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T))); + fold declare_term_syntax o + List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T))); fun add_vars xs Ts ctxt = let val xs' = Term.variantlist (map Syntax.skolem xs, map #2 (fixes_of ctxt)) in @@ -1456,186 +1461,4 @@ verb_single (fn () => Pretty.strs ("used type variable names:" :: used)) end; - -(* print_thms_containing *) - -fun lthms_containing (ctxt as Context {thms = (_, _, _, index), ...}) idx = - let - fun valid (name, ths) = - (case try (transform_error (fn () => get_thms ctxt (name, NONE))) () of - NONE => false - | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths')); - in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end; - -(* facts which are local to the current context, with their names - examples are "prems" and "x" in "assumes x:" during a proof *) -fun local_facts (ctxt as Context {thms = (_, _, _, index), ...}) = - (* things like "prems" can occur twice under some circumstances *) - gen_distinct eq_fst (FactIndex.find ([],[]) index); - -fun isSubstring pat str = - if String.size pat = 0 then true - else if String.size pat > String.size str then false - else if String.substring (str, 0, String.size pat) = pat then true - else isSubstring pat (String.extract (str, 1, NONE)); - -(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into - a term with all free variables made schematic *) -fun str_pattern_to_term sg str_pattern = - let - (* pattern as term with dummies as Consts *) - val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) - |> Thm.term_of; - (* with dummies as Vars *) - val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern)); - in - (* with schematic vars *) - #1 (Type.varify (v_pattern, [])) - end; - -(* alternate rem_top which checks for a Trueprop, unlike that in PureThy *) -fun rem_top_c (Term.Const ("Trueprop", _) $ t) = t - | rem_top_c _ = Bound 0; - -(* ---------- search filter contructions go here *) - -(* terms supplied in string form as patterns *) -fun str_term_pat_to_filter sg str_pat = - let - val tsig = Sign.tsig_of sg; - val pat = str_pattern_to_term sg str_pat; - - (* must qualify type so ML doesn't go and replace it with a concrete one *) - fun name_thm_matches_pattern tsig pat (_:string, thm) = - Pattern.matches_subterm tsig (pat, Thm.prop_of thm); - in - name_thm_matches_pattern (Sign.tsig_of sg) pat - end; - -(* create filter that just looks for a string in the name, - substring match only (no regexps are performed) *) -fun str_name_pat_to_filter str_pat (name, _:Thm.thm) = isSubstring str_pat name; - -(* for elimination and destruction rules, we must check if the major premise - matches with one of the assumptions in the top subgoal, but we must - additionally make sure that we tell elim/dest apart, using thm_check_fun *) -fun elim_dest_filter thm_check_fun sg goal = - let - val elims_extract = (fn thm => if Thm.no_prems thm then [] else [thm], - rem_top_c o hd o Logic.strip_imp_prems); - - (* assumptions of the top subgoal *) - val prems = map rem_top_c (Logic.prems_of_goal goal 1); - - fun prem_matches_name_thm prems (name_thm as (name,thm)) = - List.exists - (fn p => PureThy.is_matching_thm elims_extract sg p name_thm - andalso (thm_check_fun thm)) prems; - in - prem_matches_name_thm prems - end; - -(* ------------ *) - -(* elimination rule: conclusion is a Var and - no Var in the conclusion appears in the major premise - Note: only makes sense if the major premise already matched the assumption - of some goal! *) -fun is_elim_rule thm = - let - val {prop, ...} = rep_thm thm; - val concl = rem_top_c (Logic.strip_imp_concl prop); - val major_prem = hd (Logic.strip_imp_prems prop); - val prem_vars = distinct (Drule.vars_of_terms [major_prem]); - val concl_vars = distinct (Drule.vars_of_terms [concl]); - in - Term.is_Var concl andalso (prem_vars inter concl_vars) = [] - end; - -fun crit2str (Name name) = "name:" ^ name - | crit2str Elim = "elim" - | crit2str Intro = "intro" - | crit2str Rewrite = "rewrite" - | crit2str Dest = "dest" - | crit2str (Pattern x) = x; - -val criteria_to_str = - let - fun criterion_to_str ( true, ct) = "+ : " ^ crit2str ct - | criterion_to_str (false, ct) = "- : " ^ crit2str ct - in - map criterion_to_str - end; - -fun make_filter _ _ (Name name) = str_name_pat_to_filter name - | make_filter sg _ (Pattern p) = str_term_pat_to_filter sg p - (* beyond this point, only criteria requiring a goal! *) - | make_filter _ NONE c = - error ("Need to have a current goal to use " ^ (crit2str c)) - | make_filter sg (SOME goal) Elim = - elim_dest_filter is_elim_rule sg goal - | make_filter sg (SOME goal) Dest = - (* in this case all that is not elim rule is dest *) - elim_dest_filter (not o is_elim_rule) sg goal - | make_filter sg (SOME goal) Intro = - let - (* filter by checking conclusion of theorem against conclusion of goal *) - fun intros_extract () = (single, rem_top_c o Logic.strip_imp_concl); - val concl = rem_top_c (Logic.concl_of_goal goal 1); - in - (fn name_thm => - PureThy.is_matching_thm (intros_extract ()) sg concl name_thm) - end - | make_filter _ _ c = - error (crit2str c ^ " unimplemented"); - (* XXX: searching for rewrites currently impossible since we'd need - a simplifier, which is included *after* Pure *) - -(* create filters ... convert negative ones to positive ones *) -fun make_filters sg opt_goal = - map (fn (b,sc) => (if b then I else not) o (make_filter sg opt_goal sc)); - -fun print_thms_containing ctxt opt_goal opt_limit criteria = - let - val prt_term = pretty_term ctxt; - val prt_fact = pretty_fact ctxt; - val ss = criteria_to_str criteria; - - (* facts from the theory and its ancestors *) - val thy = theory_of ctxt; - val sg1 = Theory.sign_of thy; - val all_thys = thy :: (Theory.ancestors_of thy) - val facts1 = List.concat (map PureThy.thms_with_names_of all_thys); - val filters1 = make_filters sg1 opt_goal criteria; - val matches1 = PureThy.find_theorems facts1 filters1; - - (* facts from the local context *) - val sg2 = sign_of ctxt; - val facts2 = local_facts ctxt; - val filters2 = make_filters sg2 opt_goal criteria; - val matches2 = PureThy.find_theorems facts2 filters2; - - (* combine them, use a limit, then print *) - val matches = matches1 @ matches2; - val len = length matches; - val limit = if_none opt_limit (! thms_containing_limit); - val count = Int.min (limit, len); - - val header = Pretty.blk (0, [Pretty.str "Searched for:", Pretty.fbrk, - Pretty.indent 4 ( - Pretty.blk (0, separate Pretty.fbrk (map Pretty.str ss))), - Pretty.fbrk, Pretty.fbrk, - Pretty.str ("Found " ^ (Int.toString len) ^ - " theorems (" ^ (Int.toString count) ^ " displayed):"), - Pretty.fbrk]); - in - if null matches then - warning "find_theorems: nothing found" - else - Pretty.writeln header; - ((if len <= limit then [] else [Pretty.str "..."]) @ - map (prt_fact) (Library.drop (len - limit, matches))) |> - Pretty.chunks |> Pretty.writeln - end; - end;