# HG changeset patch # User wenzelm # Date 1582574249 -3600 # Node ID 910a081cca741bb1463105da78e5f18e3235d75d # Parent 4a04b6bd628bfe17cd974a4d95cbcb0171f6a07c more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1; diff -r 4a04b6bd628b -r 910a081cca74 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Doc/Implementation/Logic.thy Mon Feb 24 20:57:29 2020 +0100 @@ -598,7 +598,7 @@ \begin{mldecls} @{index_ML Theory.add_deps: "Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory"} \\ - @{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\ + @{index_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\ \end{mldecls} \<^descr> \<^ML>\Logic.all\~\a B\ produces a Pure quantification \\a. B\, where @@ -676,9 +676,10 @@ \<^descr> \<^ML>\Thm_Deps.all_oracles\~\thms\ returns all oracles used in the internal derivation of the given theorems; this covers the full graph of - transitive dependencies. The result contains a name, plus the original - proposition, if @{ML Proofterm.proofs} was at least @{ML 1} during the - oracle inference. See also the command @{command_ref "thm_oracles"}. + transitive dependencies. The result contains an authentic oracle name; if + @{ML Proofterm.proofs} was at least @{ML 1} during the oracle inference, it + also contains the position of the oracle invocation and its proposition. See + also the command @{command_ref "thm_oracles"}. \ text %mlantiq \ diff -r 4a04b6bd628b -r 910a081cca74 src/HOL/ex/Iff_Oracle.thy --- a/src/HOL/ex/Iff_Oracle.thy Mon Feb 24 12:14:13 2020 +0000 +++ b/src/HOL/ex/Iff_Oracle.thy Mon Feb 24 20:57:29 2020 +0100 @@ -36,7 +36,7 @@ ML \iff_oracle (\<^theory>, 10)\ ML \ - \<^assert> (map #1 (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\iff_oracle\]); + \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\iff_oracle\]); \ text \These oracle calls had better fail.\ diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/General/position.ML Mon Feb 24 20:57:29 2020 +0100 @@ -7,6 +7,7 @@ signature POSITION = sig eqtype T + val ord: T ord val make: Thread_Position.T -> T val dest: T -> Thread_Position.T val line_of: T -> int option @@ -52,6 +53,7 @@ val store_reports: report_text list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit val append_reports: report_text list Unsynchronized.ref -> report list -> unit + val here_strs: T -> string * string val here: T -> string val here_list: T list -> string type range = T * T @@ -73,6 +75,19 @@ datatype T = Pos of (int * int * int) * Properties.T; +fun ord (pos1 as Pos ((i, j, k), props), pos2 as Pos ((i', j', k'), props')) = + if pointer_eq (pos1, pos2) then EQUAL + else + (case int_ord (i, i') of + EQUAL => + (case int_ord (j, j') of + EQUAL => + (case int_ord (k, k') of + EQUAL => Properties.ord (props, props') + | ord => ord) + | ord => ord) + | ord => ord); + fun norm_props (props: Properties.T) = maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties'; @@ -228,15 +243,17 @@ (* here: user output *) +fun here_strs pos = + (case (line_of pos, file_of pos) of + (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") + | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") + | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") + | _ => if is_reported pos then ("", "\092<^here>") else ("", "")); + fun here pos = let val props = properties_of pos; - val (s1, s2) = - (case (line_of pos, file_of pos) of - (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") - | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") - | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") - | _ => if is_reported pos then ("", "\092<^here>") else ("", "")); + val (s1, s2) = here_strs pos; in if s2 = "" then "" else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/General/pretty.ML Mon Feb 24 20:57:29 2020 +0100 @@ -53,6 +53,7 @@ val enclose: string -> string -> T list -> T val enum: string -> string -> string -> T list -> T val position: Position.T -> T + val here: Position.T -> T list val list: string -> string -> T list -> T val str_list: string -> string -> string list -> T val big_list: string -> T list -> T @@ -191,6 +192,15 @@ val position = enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of; +fun here pos = + let + val props = Position.properties_of pos; + val (s1, s2) = Position.here_strs pos; + in + if s2 = "" then [] + else [str s1, mark_str (Markup.properties props Markup.position, s2)] + end; + val list = enum ","; fun str_list lpar rpar strs = list lpar rpar (map str strs); diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/General/properties.ML --- a/src/Pure/General/properties.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/General/properties.ML Mon Feb 24 20:57:29 2020 +0100 @@ -8,6 +8,8 @@ sig type entry = string * string type T = entry list + val entry_ord: entry ord + val ord: T ord val defined: T -> string -> bool val get: T -> string -> string option val put: entry -> T -> T @@ -21,6 +23,9 @@ type entry = string * string; type T = entry list; +val entry_ord = prod_ord string_ord string_ord; +val ord = list_ord entry_ord; + fun defined (props: T) name = AList.defined (op =) props name; fun get (props: T) name = AList.lookup (op =) props name; fun put entry (props: T) = AList.update (op =) entry props; diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/Proof/extraction.ML Mon Feb 24 20:57:29 2020 +0100 @@ -177,7 +177,7 @@ let val (oracles, thms) = ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false - (fn Oracle (name, prop, _) => apfst (cons (name, SOME prop)) + (fn Oracle (name, prop, _) => apfst (cons ((name, Position.none), SOME prop)) | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body)) | _ => I); val body = diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/proofterm.ML Mon Feb 24 20:57:29 2020 +0100 @@ -26,10 +26,10 @@ | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of - {oracles: (string * term option) Ord_List.T, + {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} - type oracle = string * term option + type oracle = (string * Position.T) * term option type thm = serial * thm_node exception MIN_PROOF of unit val proof_of: proof_body -> proof @@ -218,7 +218,7 @@ | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of - {oracles: (string * term option) Ord_List.T, + {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = @@ -227,8 +227,9 @@ Thm_Node of {theory_name: string, name: string, prop: term, body: proof_body future, export: unit lazy, consolidate: unit lazy}; -type oracle = string * term option; -val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); +type oracle = (string * Position.T) * term option; +val oracle_ord: oracle ord = + prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord); type thm = serial * thm_node; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); @@ -374,8 +375,8 @@ pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] and proof_body consts (PBody {oracles, thms, proof = prf}) = - triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) - (oracles, thms, prf) + triple (list (pair (pair string (properties o Position.properties_of)) + (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) and thm consts (a, thm_node) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, @@ -439,7 +440,8 @@ and proof_body consts x = let val (a, b, c) = - triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x; + triple (list (pair (pair string (Position.of_properties o properties)) + (option (term consts)))) (list (thm consts)) (proof consts) x; in PBody {oracles = a, thms = b, proof = c} end and thm consts x = let diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/thm.ML Mon Feb 24 20:57:29 2020 +0100 @@ -1065,9 +1065,9 @@ let val (oracle, prf) = (case ! Proofterm.proofs of - 2 => ((name, SOME prop), Proofterm.oracle_proof name prop) - | 1 => ((name, SOME prop), MinProof) - | 0 => ((name, NONE), MinProof) + 2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop) + | 1 => (((name, Position.thread_data ()), SOME prop), MinProof) + | 0 => (((name, Position.none), NONE), MinProof) | i => bad_proofs i); in Thm (make_deriv [] [oracle] [] prf, diff -r 4a04b6bd628b -r 910a081cca74 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Mon Feb 24 12:14:13 2020 +0000 +++ b/src/Pure/thm_deps.ML Mon Feb 24 20:57:29 2020 +0100 @@ -33,15 +33,15 @@ in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; fun has_skip_proof thms = - all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\skip_proof\); + all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\skip_proof\); fun pretty_thm_oracles ctxt thms = let val thy = Proof_Context.theory_of ctxt; - fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] - | prt_oracle (name, SOME prop) = - [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, - Syntax.pretty_term_global thy prop]; + fun prt_ora (name, pos) = Thm.pretty_oracle ctxt name :: Pretty.here pos; + fun prt_oracle (ora, NONE) = prt_ora ora + | prt_oracle (ora, SOME prop) = + prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop]; in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;