# HG changeset patch # User wenzelm # Date 1281543473 -7200 # Node ID ea1ee55aa41f49e163e2d51b3dcc83b8152d7614 # Parent 480b2de9927c76c8f45833bbbdb5cda650f37748# Parent f6c1e169f51b36c1aded9594834ba7fb90acab2a merged diff -r 480b2de9927c -r ea1ee55aa41f src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 18:17:53 2010 +0200 @@ -830,10 +830,10 @@ str "case Seq.pull (testf p) of", Pretty.brk 1, str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"], str " =>", Pretty.brk 1, str "SOME ", - Pretty.block (str "[" :: - Pretty.commas (map (fn (s, T) => Pretty.block - [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @ - [str "]"]), Pretty.brk 1, + Pretty.enum "," "[" "]" + (map (fn (s, T) => Pretty.block + [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'), + Pretty.brk 1, str "| NONE => NONE);"]) ^ "\n\nend;\n"; val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Aug 11 18:17:53 2010 +0200 @@ -16,7 +16,6 @@ val defined: theory -> string -> bool val attribute: theory -> src -> attribute val attribute_i: theory -> src -> attribute - val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list val map_specs: ('a -> 'att) -> (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list val map_facts: ('a -> 'att) -> @@ -25,6 +24,7 @@ val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) -> (('c * 'a list) * ('b * 'a list) list) list -> (('c * 'att list) * ('fact * 'att list) list) list + val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list val crude_closure: Proof.context -> src -> src val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> @@ -94,8 +94,7 @@ fun pretty_attribs _ [] = [] | pretty_attribs ctxt srcs = - [Pretty.enclose "[" "]" - (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))]; + [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)]; (* get attributes *) @@ -115,11 +114,6 @@ fun attribute thy = attribute_i thy o intern_src thy; -fun eval_thms ctxt args = ProofContext.note_thmss "" - [(Thm.empty_binding, args |> map (fn (a, atts) => - (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt - |> fst |> maps snd; - (* attributed declarations *) @@ -129,6 +123,15 @@ fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g))); +(* fact expressions *) + +fun eval_thms ctxt srcs = ctxt + |> ProofContext.note_thmss "" + (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt) + [((Binding.empty, []), srcs)]) + |> fst |> maps snd; + + (* crude_closure *) (*Produce closure without knowing facts in advance! The following diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/calculation.ML Wed Aug 11 18:17:53 2010 +0200 @@ -37,8 +37,10 @@ ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); ); +val get_rules = #1 o Data.get o Context.Proof; + fun print_rules ctxt = - let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in + let val (trans, sym) = get_rules ctxt in [Pretty.big_list "transitivity rules:" (map (Display.pretty_thm ctxt) (Item_Net.content trans)), Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)] @@ -122,21 +124,21 @@ (* also and finally *) -val get_rules = #1 o Data.get o Context.Proof o Proof.context_of; - fun calculate prep_rules final raw_rules int state = let + val ctxt = Proof.context_of state; + val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); fun projection ths th = exists (curry eq_prop th) ths; - val opt_rules = Option.map (prep_rules state) raw_rules; + val opt_rules = Option.map (prep_rules ctxt) raw_rules; fun combine ths = (case opt_rules of SOME rules => rules | NONE => (case ths of - [] => Item_Net.content (#1 (get_rules state)) - | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th))) + [] => Item_Net.content (#1 (get_rules ctxt)) + | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th))) |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |> Seq.filter (not o projection ths); @@ -154,9 +156,9 @@ end; val also = calculate (K I) false; -val also_cmd = calculate Proof.get_thmss_cmd false; +val also_cmd = calculate Attrib.eval_thms false; val finally = calculate (K I) true; -val finally_cmd = calculate Proof.get_thmss_cmd true; +val finally_cmd = calculate Attrib.eval_thms true; (* moreover and ultimately *) diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Wed Aug 11 18:17:53 2010 +0200 @@ -416,7 +416,7 @@ fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => Thm_Deps.thm_deps (Toplevel.theory_of state) - (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args)); + (Attrib.eval_thms (Toplevel.context_of state) args)); (* find unused theorems *) @@ -450,20 +450,20 @@ local -fun string_of_stmts state args = - Proof.get_thmss_cmd state args - |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK) +fun string_of_stmts ctxt args = + Attrib.eval_thms ctxt args + |> map (Element.pretty_statement ctxt Thm.theoremK) |> Pretty.chunks2 |> Pretty.string_of; -fun string_of_thms state args = - Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args)); +fun string_of_thms ctxt args = + Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args)); fun string_of_prfs full state arg = Pretty.string_of (case arg of NONE => let - val {context = ctxt, goal = thm} = Proof.simple_goal state; + val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); val thy = ProofContext.theory_of ctxt; val prf = Thm.proof_of thm; val prop = Thm.full_prop_of thm; @@ -472,20 +472,19 @@ Proof_Syntax.pretty_proof ctxt (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') end - | SOME args => Pretty.chunks - (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full) - (Proof.get_thmss_cmd state args))); + | SOME srcs => + let val ctxt = Toplevel.context_of state + in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end + |> Pretty.chunks); -fun string_of_prop state s = +fun string_of_prop ctxt s = let - val ctxt = Proof.context_of state; val prop = Syntax.read_prop ctxt s; val ctxt' = Variable.auto_fixes prop ctxt; in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; -fun string_of_term state s = +fun string_of_term ctxt s = let - val ctxt = Proof.context_of state; val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Variable.auto_fixes t ctxt; @@ -495,24 +494,21 @@ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) end; -fun string_of_type state s = - let - val ctxt = Proof.context_of state; - val T = Syntax.read_typ ctxt s; +fun string_of_type ctxt s = + let val T = Syntax.read_typ ctxt s in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end; fun print_item string_of (modes, arg) = Toplevel.keep (fn state => - Print_Mode.with_modes modes (fn () => - writeln (string_of (Toplevel.enter_proof_body state) arg)) ()); + Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); in -val print_stmts = print_item string_of_stmts; -val print_thms = print_item string_of_thms; +val print_stmts = print_item (string_of_stmts o Toplevel.context_of); +val print_thms = print_item (string_of_thms o Toplevel.context_of); val print_prfs = print_item o string_of_prfs; -val print_prop = print_item string_of_prop; -val print_term = print_item string_of_term; -val print_type = print_item string_of_type; +val print_prop = print_item (string_of_prop o Toplevel.context_of); +val print_term = print_item (string_of_term o Toplevel.context_of); +val print_type = print_item (string_of_type o Toplevel.context_of); end; diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/proof.ML Wed Aug 11 18:17:53 2010 +0200 @@ -60,7 +60,6 @@ val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state val chain: state -> state val chain_facts: thm list -> state -> state - val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state val from_thmss: ((thm list * attribute list) list) list -> state -> state @@ -679,8 +678,6 @@ val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact); -fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state); - end; diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Aug 11 18:17:53 2010 +0200 @@ -1123,7 +1123,7 @@ val type_notation = gen_notation (K type_syntax); val notation = gen_notation const_syntax; -fun target_type_notation add mode args phi = +fun target_type_notation add mode args phi = let val args' = args |> map_filter (fn (T, mx) => let diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 18:17:53 2010 +0200 @@ -20,7 +20,6 @@ val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int - val enter_proof_body: state -> Proof.state val end_theory: Position.T -> state -> theory val print_state_context: state -> unit val print_state: bool -> state -> unit @@ -186,8 +185,6 @@ Proof (prf, _) => Proof_Node.position prf | _ => raise UNDEF); -val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward; - fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos); diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Syntax/ast.ML Wed Aug 11 18:17:53 2010 +0200 @@ -75,8 +75,7 @@ fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a) | pretty_ast (Variable x) = Pretty.str x - | pretty_ast (Appl asts) = - Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); + | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); fun pretty_rule (lhs, rhs) = Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 18:17:53 2010 +0200 @@ -28,24 +28,13 @@ (* matching types/consts *) 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 + Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat)); - 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 (Term.size_of_typ ty) - else NONE; +fun check_const pred (nm, (ty, _)) = + if pred (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 (Term.size_of_typ 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)) = @@ -71,8 +60,7 @@ val ty' = Logic.unvarifyT_global ty; in Pretty.block - [Pretty.quote (Pretty.str nm), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, + [Pretty.str nm, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')] end; @@ -128,35 +116,35 @@ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; in - Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) - :: Pretty.str "" - :: (Pretty.str o implode) - (if null matches - then ["nothing found", end_msg] - else ["found ", (string_of_int o length) matches, - " constants", end_msg, ":"]) - :: Pretty.str "" - :: map (pretty_const ctxt) matches - |> Pretty.chunks - |> Pretty.writeln - end; + Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: + Pretty.str "" :: + Pretty.str + (if null matches + then "nothing found" ^ end_msg + else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") :: + Pretty.str "" :: + map (pretty_const ctxt) matches + end |> Pretty.chunks |> Pretty.writeln; (* command syntax *) -fun find_consts_cmd spec = - Toplevel.unknown_theory o Toplevel.keep (fn state => - find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec); +local val criterion = Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict || Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || Parse.xname >> Loose; +in + val _ = Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion) - >> (Toplevel.no_timing oo find_consts_cmd)); + >> (fn spec => Toplevel.no_timing o + Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec))); end; +end; + diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 18:17:53 2010 +0200 @@ -433,36 +433,27 @@ val tally_msg = (case foundo of - NONE => "displaying " ^ string_of_int returned ^ " theorems" + NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" | SOME found => - "found " ^ string_of_int found ^ " theorems" ^ + "found " ^ string_of_int found ^ " theorem(s)" ^ (if returned < found then " (" ^ string_of_int returned ^ " displayed)" else "")); val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; in - Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) - :: Pretty.str "" :: - (if null thms then [Pretty.str ("nothing found" ^ end_msg)] - else - [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ + Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: + Pretty.str "" :: + (if null thms then [Pretty.str ("nothing found" ^ end_msg)] + else + [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ map (pretty_thm ctxt) thms) - |> Pretty.chunks |> Pretty.writeln - end; + end |> Pretty.chunks |> Pretty.writeln; (** command syntax **) -fun find_theorems_cmd ((opt_lim, rem_dups), spec) = - Toplevel.unknown_theory o Toplevel.keep (fn state => - let - val proof_state = Toplevel.enter_proof_body state; - val ctxt = Proof.context_of proof_state; - val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal; - in print_theorems ctxt opt_goal opt_lim rem_dups spec end); - local val criterion = @@ -486,7 +477,13 @@ Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" Keyword.diag (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)) - >> (Toplevel.no_timing oo find_theorems_cmd)); + >> (fn ((opt_lim, rem_dups), spec) => + Toplevel.no_timing o + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; + in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); end; diff -r 480b2de9927c -r ea1ee55aa41f src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Aug 11 14:45:38 2010 +0200 +++ b/src/Pure/codegen.ML Wed Aug 11 18:17:53 2010 +0200 @@ -889,9 +889,8 @@ mk_app false (str "testf") (map (str o fst) args), Pretty.brk 1, str "then NONE", Pretty.brk 1, str "else ", - Pretty.block [str "SOME ", Pretty.block (str "[" :: - Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @ - [str "]"])]]), + Pretty.block [str "SOME ", + Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]), str ");"]) ^ "\n\nend;\n"; val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;