--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 20 20:23:21 2019 +0200
@@ -104,7 +104,7 @@
* string * (string * 'd list) list) list * string list
val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
- val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
+ val vampire_step_name_ord : (string * 'a) ord
val core_of_agsyhol_proof : string -> string list option
end;
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Tue Aug 20 20:23:21 2019 +0200
@@ -7,7 +7,7 @@
signature ATP_ATOM =
sig
type key
- val ord : key * key -> order
+ val ord : key ord
val string_of : key -> string
end;
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Aug 20 20:23:21 2019 +0200
@@ -92,7 +92,7 @@
val untuple : (nut -> 'a) -> nut -> 'a list
val add_free_and_const_names :
nut -> nut list * nut list -> nut list * nut list
- val name_ord : (nut * nut) -> order
+ val name_ord : nut ord
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
val nut_from_term : hol_context -> op2 -> term -> nut
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
val eq_mode : mode * mode -> bool
- val mode_ord: mode * mode -> order
+ val mode_ord: mode ord
val list_fun_mode : mode list -> mode
val strip_fun_mode : mode -> mode list
val dest_fun_mode : mode -> mode list
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Aug 20 20:23:21 2019 +0200
@@ -24,7 +24,7 @@
val no_label : label
- val label_ord : label * label -> order
+ val label_ord : label ord
val string_of_label : label -> string
val sort_facts : facts -> facts
@@ -39,7 +39,7 @@
structure Canonical_Label_Tab : TABLE
- val canonical_label_ord : (label * label) -> order
+ val canonical_label_ord : label ord
val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
val chain_isar_proof : isar_proof -> isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Aug 20 20:23:21 2019 +0200
@@ -48,7 +48,7 @@
(real * (('a * real) list * 'a list)) list -> 'a list
val nickname_of_thm : thm -> string
val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
- val crude_thm_ord : Proof.context -> thm * thm -> order
+ val crude_thm_ord : Proof.context -> thm ord
val thm_less : thm * thm -> bool
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Aug 20 20:23:21 2019 +0200
@@ -38,7 +38,7 @@
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
- val play_outcome_ord : play_outcome * play_outcome -> order
+ val play_outcome_ord : play_outcome ord
val one_line_proof_text : Proof.context -> int -> one_line_params -> string
end;
--- a/src/HOL/Tools/groebner.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/groebner.ML Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
(cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
conv -> conv ->
{ring_conv: Proof.context -> conv,
- simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
+ simple_ideal: cterm list -> cterm -> cterm ord -> cterm list,
multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
poly_eq_ss: simpset, unwind_conv: Proof.context -> conv}
val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
--- a/src/HOL/Tools/semiring_normalizer.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Tue Aug 20 20:23:21 2019 +0200
@@ -18,21 +18,19 @@
local_theory -> local_theory
val semiring_normalize_conv: Proof.context -> conv
- val semiring_normalize_ord_conv: Proof.context -> (cterm * cterm -> order) -> conv
+ val semiring_normalize_ord_conv: Proof.context -> cterm ord -> conv
val semiring_normalize_wrapper: Proof.context -> entry -> conv
- val semiring_normalize_ord_wrapper: Proof.context -> entry
- -> (cterm * cterm -> order) -> conv
+ val semiring_normalize_ord_wrapper: Proof.context -> entry -> cterm ord -> conv
val semiring_normalizers_conv: cterm list -> cterm list * thm list
-> cterm list * thm list -> cterm list * thm list ->
- (cterm -> bool) * conv * conv * conv -> (cterm * cterm -> order) ->
+ (cterm -> bool) * conv * conv * conv -> cterm ord ->
{add: Proof.context -> conv,
mul: Proof.context -> conv,
neg: Proof.context -> conv,
main: Proof.context -> conv,
pow: Proof.context -> conv,
sub: Proof.context -> conv}
- val semiring_normalizers_ord_wrapper: Proof.context -> entry ->
- (cterm * cterm -> order) ->
+ val semiring_normalizers_ord_wrapper: Proof.context -> entry -> cterm ord ->
{add: Proof.context -> conv,
mul: Proof.context -> conv,
neg: Proof.context -> conv,
--- a/src/Pure/General/heap.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/heap.ML Tue Aug 20 20:23:21 2019 +0200
@@ -20,7 +20,7 @@
val upto: elem -> T -> elem list * T
end;
-functor Heap(type elem val ord: elem * elem -> order): HEAP =
+functor Heap(type elem val ord: elem ord): HEAP =
struct
--- a/src/Pure/General/name_space.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/name_space.ML Tue Aug 20 20:23:21 2019 +0200
@@ -16,14 +16,14 @@
val markup_def: T -> string -> Markup.T
val the_entry: T -> string ->
{concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
- val entry_ord: T -> string * string -> order
+ val entry_ord: T -> string ord
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val names_long: bool Config.T
val names_short: bool Config.T
val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
- val extern_ord: Proof.context -> T -> string * string -> order
+ val extern_ord: Proof.context -> T -> string ord
val extern_shortest: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val pretty: Proof.context -> T -> string -> Pretty.T
--- a/src/Pure/General/rat.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/rat.ML Tue Aug 20 20:23:21 2019 +0200
@@ -13,7 +13,7 @@
val dest: rat -> int * int
val string_of_rat: rat -> string
val signed_string_of_rat: rat -> string
- val ord: rat * rat -> order
+ val ord: rat ord
val le: rat -> rat -> bool
val lt: rat -> rat -> bool
val sign: rat -> order
--- a/src/Pure/General/table.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/table.ML Tue Aug 20 20:23:21 2019 +0200
@@ -8,7 +8,7 @@
signature KEY =
sig
type key
- val ord: key * key -> order
+ val ord: key ord
end;
signature TABLE =
--- a/src/Pure/Isar/spec_rules.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Isar/spec_rules.ML Tue Aug 20 20:23:21 2019 +0200
@@ -10,9 +10,9 @@
sig
datatype recursion =
Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
- val recursion_ord: recursion * recursion -> order
+ val recursion_ord: recursion ord
datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
- val rough_classification_ord: rough_classification * rough_classification -> order
+ val rough_classification_ord: rough_classification ord
val equational_primrec: string list -> rough_classification
val equational_recdef: rough_classification
val equational_primcorec: string list -> rough_classification
--- a/src/Pure/Proof/extraction.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Aug 20 20:23:21 2019 +0200
@@ -173,6 +173,21 @@
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
+fun make_proof_body prf =
+ let
+ val (oracles, thms) =
+ ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
+ (fn Oracle (name, prop, _) => apfst (cons (name, prop))
+ | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
+ | _ => I);
+ val body =
+ PBody
+ {oracles = Ord_List.make Proofterm.oracle_ord oracles,
+ thms = Ord_List.make Proofterm.thm_ord thms,
+ proof = prf};
+ in Proofterm.thm_body body end;
+
+
(**** theory data ****)
@@ -625,11 +640,10 @@
Proofterm.thm_header (serial ()) pos theory_name
(corr_name name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
- val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
val corr_prf' =
Proofterm.proof_combP
(Proofterm.proof_combt
- (PThm (corr_header, corr_body), vfs_of corr_prop),
+ (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
fold_rev Proofterm.forall_intr_proof'
(map (get_var_type corr_prop) (vfs_of prop)) |>
@@ -746,10 +760,9 @@
Proofterm.thm_header (serial ()) pos theory_name
(corr_name s vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
- val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
- (PThm (corr_header, corr_body), vfs_of corr_prop),
+ (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
map PBound (length shyps - 1 downto 0)) |>
fold_rev Proofterm.forall_intr_proof'
(map (get_var_type corr_prop) (vfs_of prop)) |>
--- a/src/Pure/Syntax/lexicon.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Syntax/lexicon.ML Tue Aug 20 20:23:21 2019 +0200
@@ -32,7 +32,7 @@
val dummy: token
val literal: string -> token
val is_literal: token -> bool
- val tokens_match_ord: token * token -> order
+ val tokens_match_ord: token ord
val mk_eof: Position.T -> token
val eof: token
val is_eof: token -> bool
--- a/src/Pure/Thy/export_theory.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML Tue Aug 20 20:23:21 2019 +0200
@@ -255,13 +255,20 @@
val {pos, ...} = Name_Space.the_entry space name;
in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
- val encode_thm = clean_thm #> (fn thm =>
- standard_prop Name.context
- (Thm.extra_shyps thm)
- (Thm.full_prop_of thm)
- (try Thm.reconstruct_proof_of thm) |>
- let open XML.Encode Term_XML.Encode
- in pair encode_prop (option Proofterm.encode_full) end);
+ fun encode_thm raw_thm =
+ let
+ val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
+ val thm = clean_thm raw_thm;
+ val (prop, proof) =
+ standard_prop Name.context
+ (Thm.extra_shyps thm)
+ (Thm.full_prop_of thm)
+ (try Thm.reconstruct_proof_of thm);
+ in
+ (prop, (deps, proof)) |>
+ let open XML.Encode Term_XML.Encode
+ in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end
+ end;
fun export_thms thms =
let val elems =
--- a/src/Pure/Thy/export_theory.scala Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala Tue Aug 20 20:23:21 2019 +0200
@@ -327,23 +327,23 @@
/* theorems */
- sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+ sealed case class Thm(entity: Entity, prop: Prop, deps: List[String], proof: Option[Term.Proof])
{
def cache(cache: Term.Cache): Thm =
- Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+ Thm(entity.cache(cache), prop.cache(cache), deps.map(cache.string _), proof.map(cache.proof _))
}
def read_thms(provider: Export.Provider): List[Thm] =
provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.THM, tree)
- val (prop, prf) =
+ val (prop, (deps, prf)) =
{
import XML.Decode._
import Term_XML.Decode._
- pair(decode_prop _, option(proof))(body)
+ pair(decode_prop _, pair(list(string), option(proof)))(body)
}
- Thm(entity, prop, prf)
+ Thm(entity, prop, deps, prf)
})
def read_proof(
--- a/src/Pure/Thy/thm_deps.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML Tue Aug 20 20:23:21 2019 +0200
@@ -10,6 +10,7 @@
val all_oracles: thm list -> Proofterm.oracle list
val has_skip_proof: thm list -> bool
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
+ val thm_deps: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) list
val thm_deps_cmd: theory -> thm list -> unit
val unused_thms_cmd: theory list * theory list -> (string * thm) list
end;
@@ -20,7 +21,16 @@
(* oracles *)
fun all_oracles thms =
- Proofterm.all_oracles_of (map Thm.proof_body_of thms);
+ let
+ fun collect (PBody {oracles, thms, ...}) =
+ (if null oracles then I else apfst (cons oracles)) #>
+ (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
+ if Inttab.defined seen i then (res, seen)
+ else
+ let val body = Future.join (Proofterm.thm_node_body thm_node)
+ in collect body (res, Inttab.update (i, ()) seen) end));
+ val bodies = map Thm.proof_body_of thms;
+ 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>\<open>skip_proof\<close>);
@@ -35,6 +45,26 @@
in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
+(* thm_deps *)
+
+fun thm_deps thy =
+ let
+ val lookup = Global_Theory.lookup_thm_id thy;
+ fun deps (i, thm_node) res =
+ if Inttab.defined res i then res
+ else
+ let val thm_id = Proofterm.thm_id (i, thm_node) in
+ (case lookup thm_id of
+ SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res
+ | NONE => fold deps (Proofterm.thm_node_thms thm_node) res)
+ end;
+ in
+ fn thm =>
+ fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty
+ |> Inttab.dest |> map #2
+ end;
+
+
(* thm_deps_cmd *)
fun thm_deps_cmd thy thms =
--- a/src/Pure/context.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/context.ML Tue Aug 20 20:23:21 2019 +0200
@@ -33,7 +33,7 @@
val timing: bool Unsynchronized.ref
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
- val theory_id_ord: theory_id * theory_id -> order
+ val theory_id_ord: theory_id ord
val theory_id_long_name: theory_id -> string
val theory_id_name: theory_id -> string
val theory_long_name: theory -> string
--- a/src/Pure/defs.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/defs.ML Tue Aug 20 20:23:21 2019 +0200
@@ -11,7 +11,7 @@
datatype item_kind = Const | Type
type item = item_kind * string
type entry = item * typ list
- val item_kind_ord: item_kind * item_kind -> order
+ val item_kind_ord: item_kind ord
val plain_args: typ list -> bool
type context = Proof.context * (Name_Space.T * Name_Space.T)
val global_context: theory -> context
--- a/src/Pure/global_theory.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/global_theory.ML Tue Aug 20 20:23:21 2019 +0200
@@ -15,7 +15,7 @@
val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
val dest_thm_names: theory -> (serial * Thm_Name.T) list
val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
- val lookup_thm: theory -> thm -> Thm_Name.T option
+ val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
val transfer_theories: theory -> thm -> thm
@@ -126,8 +126,15 @@
in lookup end;
fun lookup_thm thy =
- let val lookup = lookup_thm_id thy
- in fn thm => (case Thm.derivation_id thm of NONE => NONE | SOME thm_id => lookup thm_id) end;
+ let val lookup = lookup_thm_id thy in
+ fn thm =>
+ (case Thm.derivation_id thm of
+ NONE => NONE
+ | SOME thm_id =>
+ (case lookup thm_id of
+ NONE => NONE
+ | SOME thm_name => SOME (thm_id, thm_name)))
+ end;
val _ =
Theory.setup (Theory.at_end (fn thy =>
--- a/src/Pure/library.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/library.ML Tue Aug 20 20:23:21 2019 +0200
@@ -185,24 +185,25 @@
val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
(*orders*)
+ type 'a ord = 'a * 'a -> order
val is_equal: order -> bool
val is_less: order -> bool
val is_less_equal: order -> bool
val is_greater: order -> bool
val is_greater_equal: order -> bool
val rev_order: order -> order
- val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
- val bool_ord: bool * bool -> order
- val int_ord: int * int -> order
- val string_ord: string * string -> order
- val fast_string_ord: string * string -> order
+ val make_ord: ('a * 'a -> bool) -> 'a ord
+ val bool_ord: bool ord
+ val int_ord: int ord
+ val string_ord: string ord
+ val fast_string_ord: string ord
val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
val <<< : ('a -> order) * ('a -> order) -> 'a -> order
val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
- val sort: ('a * 'a -> order) -> 'a list -> 'a list
- val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
+ val sort: 'a ord -> 'a list -> 'a list
+ val sort_distinct: 'a ord -> 'a list -> 'a list
val sort_strings: string list -> string list
val sort_by: ('a -> string) -> 'a list -> 'a list
val tag_list: int -> 'a list -> (int * 'a) list
@@ -896,6 +897,8 @@
(** orders **)
+type 'a ord = 'a * 'a -> order;
+
fun is_equal ord = ord = EQUAL;
fun is_less ord = ord = LESS;
fun is_less_equal ord = ord = LESS orelse ord = EQUAL;
--- a/src/Pure/more_thm.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/more_thm.ML Tue Aug 20 20:23:21 2019 +0200
@@ -40,9 +40,9 @@
val dest_equals_rhs: cterm -> cterm
val lhs_of: thm -> cterm
val rhs_of: thm -> cterm
- val fast_term_ord: cterm * cterm -> order
- val term_ord: cterm * cterm -> order
- val thm_ord: thm * thm -> order
+ val fast_term_ord: cterm ord
+ val term_ord: cterm ord
+ val thm_ord: thm ord
val cterm_cache: (cterm -> 'a) -> cterm -> 'a
val thm_cache: (thm -> 'a) -> thm -> 'a
val is_reflexive: thm -> bool
--- a/src/Pure/proofterm.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/proofterm.ML Tue Aug 20 20:23:21 2019 +0200
@@ -8,11 +8,11 @@
signature PROOFTERM =
sig
- type thm_node
type thm_header =
{serial: serial, pos: Position.T list, theory_name: string, name: string,
prop: term, types: typ list option}
type thm_body
+ type thm_node
datatype proof =
MinProof
| PBound of int
@@ -29,34 +29,33 @@
{oracles: (string * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
proof: proof}
- val %> : proof * term -> proof
- val proofs: int Unsynchronized.ref
+ type oracle = string * term option
+ type thm = serial * thm_node
exception MIN_PROOF
- type pthm = serial * thm_node
- type oracle = string * term option
val proof_of: proof_body -> proof
+ val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
val thm_body_proof_open: thm_body -> proof
+ val thm_node_theory_name: thm_node -> string
val thm_node_name: thm_node -> string
val thm_node_prop: thm_node -> term
val thm_node_body: thm_node -> proof_body future
- val join_proof: proof_body future -> proof
+ val thm_node_thms: thm_node -> thm list
+ val join_thms: thm list -> proof_body list
+ val consolidate: proof_body list -> unit
+ val make_thm: thm_header -> thm_body -> thm
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
- val consolidate: proof_body list -> unit
-
- val oracle_ord: oracle * oracle -> order
- val thm_ord: pthm * pthm -> order
+ val oracle_ord: oracle ord
+ val thm_ord: thm ord
val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
- val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
- val all_oracles_of: proof_body list -> oracle Ord_List.T
- val approximate_proof_body: proof -> proof_body
+ val unions_thms: thm Ord_List.T list -> thm Ord_List.T
val no_proof_body: proof -> proof_body
val no_thm_proofs: proof -> proof
val no_body_proofs: proof -> proof
@@ -67,7 +66,10 @@
val decode: proof XML.Decode.T
val decode_body: proof_body XML.Decode.T
+ val %> : proof * term -> proof
+
(*primitive operations*)
+ val proofs: int Unsynchronized.ref
val proofs_enabled: unit -> bool
val atomic_proof: proof -> bool
val compact_proof: proof -> bool
@@ -165,12 +167,13 @@
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> string * Position.T -> sort list ->
- term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof
+ term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
val unconstrain_thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> sort list -> term ->
- (serial * proof_body future) list -> proof_body -> pthm * proof
+ (serial * proof_body future) list -> proof_body -> thm * proof
val get_approximative_name: sort list -> term list -> term -> proof -> string
type thm_id = {serial: serial, theory_name: string}
+ val thm_id: thm -> thm_id
val get_id: sort list -> term list -> term -> proof -> thm_id option
end
@@ -202,14 +205,18 @@
and thm_body =
Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
and thm_node =
- Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
+ Thm_Node of {theory_name: string, name: string, prop: term,
+ body: proof_body future, consolidate: unit lazy};
+
+type oracle = string * term option;
+val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
+val oracle_prop = the_default Term.dummy;
+
+type thm = serial * thm_node;
+val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
exception MIN_PROOF;
-type oracle = string * term option;
-val oracle_prop = the_default Term.dummy;
-
-type pthm = serial * thm_node;
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -229,25 +236,30 @@
fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
fun rep_thm_node (Thm_Node args) = args;
+val thm_node_theory_name = #theory_name o rep_thm_node;
val thm_node_name = #name o rep_thm_node;
val thm_node_prop = #prop o rep_thm_node;
val thm_node_body = #body o rep_thm_node;
+val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
val thm_node_consolidate = #consolidate o rep_thm_node;
-fun join_thms (thms: pthm list) =
+fun join_thms (thms: thm list) =
Future.joins (map (thm_node_body o #2) thms);
val consolidate =
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
-fun make_thm_node name prop body =
- Thm_Node {name = name, prop = prop, body = body,
+fun make_thm_node theory_name name prop body =
+ Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
consolidate =
Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
in consolidate (join_thms thms) end)};
+fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+ (serial, make_thm_node theory_name name prop body);
+
(* proof atoms *)
@@ -283,37 +295,9 @@
(* proof body *)
-val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
-fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
-
val unions_oracles = Ord_List.unions oracle_ord;
val unions_thms = Ord_List.unions thm_ord;
-fun all_oracles_of bodies =
- let
- fun collect (PBody {oracles, thms, ...}) =
- (if null oracles then I else apfst (cons oracles)) #>
- (tap join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
- if Inttab.defined seen i then (res, seen)
- else
- let val body = Future.join (thm_node_body thm_node)
- in collect body (res, Inttab.update (i, ()) seen) end));
- in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
-
-fun approximate_proof_body prf =
- let
- val (oracles, thms) = fold_proof_atoms false
- (fn Oracle (s, prop, _) => apfst (cons (s, prop))
- | PThm ({serial = i, name, prop, ...}, Thm_Body {body, ...}) =>
- apsnd (cons (i, make_thm_node name prop body))
- | _ => I) [prf] ([], []);
- in
- PBody
- {oracles = Ord_List.make oracle_ord oracles,
- thms = Ord_List.make thm_ord thms,
- proof = prf}
- end;
-
fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
val no_thm_body = thm_body (no_proof_body MinProof);
@@ -361,10 +345,11 @@
pair (list properties) (pair term (pair (option (list typ)) proof_body))
(map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
and proof_body (PBody {oracles, thms, proof = prf}) =
- triple (list (pair string (option term))) (list pthm) proof (oracles, thms, prf)
-and pthm (a, thm_node) =
- pair int (triple string term proof_body)
- (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
+ triple (list (pair string (option term))) (list thm) proof (oracles, thms, prf)
+and thm (a, thm_node) =
+ pair int (pair string (pair string (pair term proof_body)))
+ (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
+ (Future.join (thm_node_body thm_node))))));
fun full_proof prf = prf |> variant
[fn MinProof => ([], []),
@@ -413,11 +398,11 @@
val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
in PThm (header, thm_body h) end]
and proof_body x =
- let val (a, b, c) = triple (list (pair string (option term))) (list pthm) proof x
+ let val (a, b, c) = triple (list (pair string (option term))) (list thm) proof x
in PBody {oracles = a, thms = b, proof = c} end
-and pthm x =
- let val (a, (b, c, d)) = pair int (triple string term proof_body) x
- in (a, make_thm_node b c (Future.value d)) end;
+and thm x =
+ let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair term proof_body))) x
+ in (a, make_thm_node b c d (Future.value e)) end;
in
@@ -429,6 +414,9 @@
(** proof objects with different levels of detail **)
+val proofs = Unsynchronized.ref 2;
+fun proofs_enabled () = ! proofs >= 2;
+
fun atomic_proof prf =
(case prf of
Abst _ => false
@@ -1086,9 +1074,6 @@
(** axioms and theorems **)
-val proofs = Unsynchronized.ref 2;
-fun proofs_enabled () = ! proofs >= 2;
-
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
@@ -2167,10 +2152,10 @@
if named orelse not (export_enabled ()) then no_export_proof
else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
- val pthm = (i, make_thm_node name prop1 body');
+ val theory_name = Context.theory_long_name thy;
+ val thm = (i, make_thm_node theory_name name prop1 body');
- val header =
- thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
+ val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
val head = PThm (header, thm_body);
val proof =
@@ -2179,7 +2164,7 @@
else
proof_combP (proof_combt' (head, args),
map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
- in (pthm, proof) end;
+ in (thm, proof) end;
in
@@ -2209,6 +2194,9 @@
type thm_id = {serial: serial, theory_name: string};
+fun thm_id (serial, thm_node) : thm_id =
+ {serial = serial, theory_name = thm_node_theory_name thm_node};
+
fun get_id shyps hyps prop prf : thm_id option =
(case get_identity shyps hyps prop prf of
NONE => NONE
--- a/src/Pure/raw_simplifier.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Aug 20 20:23:21 2019 +0200
@@ -82,7 +82,7 @@
mk_sym: Proof.context -> thm -> thm option,
mk_eq_True: Proof.context -> thm -> thm option,
reorient: Proof.context -> term list -> term -> term -> bool},
- term_ord: term * term -> order,
+ term_ord: term ord,
subgoal_tac: Proof.context -> int -> tactic,
loop_tacs: (string * (Proof.context -> int -> tactic)) list,
solvers: solver list * solver list}
@@ -101,7 +101,7 @@
val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
- val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
+ val set_term_ord: term ord -> Proof.context -> Proof.context
val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
val solver: Proof.context -> solver -> int -> tactic
val default_mk_sym: Proof.context -> thm -> thm option
@@ -268,7 +268,7 @@
mk_sym: Proof.context -> thm -> thm option,
mk_eq_True: Proof.context -> thm -> thm option,
reorient: Proof.context -> term list -> term -> term -> bool},
- term_ord: term * term -> order,
+ term_ord: term ord,
subgoal_tac: Proof.context -> int -> tactic,
loop_tacs: (string * (Proof.context -> int -> tactic)) list,
solvers: solver list * solver list};
--- a/src/Pure/simplifier.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/simplifier.ML Tue Aug 20 20:23:21 2019 +0200
@@ -57,7 +57,7 @@
val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
- val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
+ val set_term_ord: term ord -> Proof.context -> Proof.context
val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
type trace_ops
val set_trace_ops: trace_ops -> theory -> theory
--- a/src/Pure/term_ord.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/term_ord.ML Tue Aug 20 20:23:21 2019 +0200
@@ -15,17 +15,17 @@
signature TERM_ORD =
sig
include BASIC_TERM_ORD
- val fast_indexname_ord: indexname * indexname -> order
- val sort_ord: sort * sort -> order
- val typ_ord: typ * typ -> order
- val fast_term_ord: term * term -> order
- val syntax_term_ord: term * term -> order
- val indexname_ord: indexname * indexname -> order
- val tvar_ord: (indexname * sort) * (indexname * sort) -> order
- val var_ord: (indexname * typ) * (indexname * typ) -> order
- val term_ord: term * term -> order
- val hd_ord: term * term -> order
- val term_lpo: (term -> int) -> term * term -> order
+ val fast_indexname_ord: indexname ord
+ val sort_ord: sort ord
+ val typ_ord: typ ord
+ val fast_term_ord: term ord
+ val syntax_term_ord: term ord
+ val indexname_ord: indexname ord
+ val tvar_ord: (indexname * sort) ord
+ val var_ord: (indexname * typ) ord
+ val term_ord: term ord
+ val hd_ord: term ord
+ val term_lpo: (term -> int) -> term ord
val term_cache: (term -> 'a) -> term -> 'a
end;
--- a/src/Pure/thm.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/thm.ML Tue Aug 20 20:23:21 2019 +0200
@@ -103,6 +103,7 @@
val proof_of: thm -> proof
val consolidate: thm list -> unit
val future: thm future -> cterm -> thm
+ val thm_deps: thm -> Proofterm.thm Ord_List.T
val derivation_closed: thm -> bool
val derivation_name: thm -> string
val derivation_id: thm -> Proofterm.thm_id option
@@ -371,7 +372,7 @@
local
-val constraint_ord : constraint * constraint -> order =
+val constraint_ord : constraint ord =
Context.theory_id_ord o apply2 (Context.theory_id o #theory)
<<< Term_Ord.typ_ord o apply2 #typ
<<< Term_Ord.sort_ord o apply2 #sort;
@@ -710,7 +711,7 @@
(* inference rules *)
-fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
+val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
fun deriv_rule2 f
(Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
@@ -736,7 +737,6 @@
(* fulfilled proofs *)
-fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
fun join_promises [] = ()
@@ -933,7 +933,7 @@
fun union_digest (oracles1, thms1) (oracles2, thms2) =
(Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
-fun thm_digest (Thm (Deriv {body = Proofterm.PBody {oracles, thms, ...}, ...}, _)) =
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
(oracles, thms);
fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
@@ -963,10 +963,10 @@
raise THEORY ("solve_constraints: bad theories for theorem\n" ^
Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
- val Deriv {promises, body = Proofterm.PBody {oracles, thms, proof}} = der;
+ val Deriv {promises, body = PBody {oracles, thms, proof}} = der;
val (oracles', thms') = (oracles, thms)
|> fold (fold union_digest o constraint_digest) constraints;
- val body' = Proofterm.PBody {oracles = oracles', thms = thms', proof = proof};
+ val body' = PBody {oracles = oracles', thms = thms', proof = proof};
in
Thm (Deriv {promises = promises, body = body'},
{constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -991,10 +991,19 @@
fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
+(*identified PThm node*)
fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
Proofterm.get_id shyps hyps prop (proof_of thm)
handle Proofterm.MIN_PROOF => NONE;
+(*dependencies of PThm node*)
+fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =
+ (case (derivation_id thm, thms) of
+ (SOME {serial = i, ...}, [(j, thm_node)]) =>
+ if i = j then Proofterm.thm_node_thms thm_node else thms
+ | _ => thms)
+ | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
+
fun name_derivation name_pos =
solve_constraints #> (fn thm as Thm (der, args) =>
let
--- a/src/Pure/thm_name.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/thm_name.ML Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
signature THM_NAME =
sig
type T = string * int
- val ord: T * T -> order
+ val ord: T ord
val print: T -> string
val flatten: T -> string
val make_list: string -> thm list -> (T * thm) list
--- a/src/Pure/variable.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/variable.ML Tue Aug 20 20:23:21 2019 +0200
@@ -41,7 +41,7 @@
val is_improper: Proof.context -> string -> bool
val is_fixed: Proof.context -> string -> bool
val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
- val fixed_ord: Proof.context -> string * string -> order
+ val fixed_ord: Proof.context -> string ord
val intern_fixed: Proof.context -> string -> string
val lookup_fixed: Proof.context -> string -> string option
val revert_fixed: Proof.context -> string -> string
--- a/src/Tools/Argo/argo_expr.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_expr.ML Tue Aug 20 20:23:21 2019 +0200
@@ -15,11 +15,11 @@
(* indices, equalities, orders *)
val int_of_kind: kind -> int
- val con_ord: (string * typ) * (string * typ) -> order
+ val con_ord: (string * typ) ord
val eq_kind: kind * kind -> bool
- val kind_ord: kind * kind -> order
+ val kind_ord: kind ord
val eq_expr: expr * expr -> bool
- val expr_ord: expr * expr -> order
+ val expr_ord: expr ord
val dual_expr: expr -> expr -> bool
(* constructors *)
--- a/src/Tools/Argo/argo_proof.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_proof.ML Tue Aug 20 20:23:21 2019 +0200
@@ -52,7 +52,7 @@
(* equalities and orders *)
val eq_proof_id: proof_id * proof_id -> bool
- val proof_id_ord: proof_id * proof_id -> order
+ val proof_id_ord: proof_id ord
(* conversion constructors *)
val keep_conv: conv
--- a/src/Tools/Argo/argo_term.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_term.ML Tue Aug 20 20:23:21 2019 +0200
@@ -17,7 +17,7 @@
val expr_of: term -> Argo_Expr.expr
val type_of: term -> Argo_Expr.typ
val eq_term: term * term -> bool
- val term_ord: term * term -> order
+ val term_ord: term ord
(* context *)
type context
--- a/src/Tools/float.ML Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/float.ML Tue Aug 20 20:23:21 2019 +0200
@@ -9,7 +9,7 @@
type float = int * int
val zero: float
val eq: float * float -> bool
- val ord: float * float -> order
+ val ord: float ord
val sign: float -> order
val min: float -> float -> float
val max: float -> float -> float