--- a/src/Pure/ROOT.ML Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/ROOT.ML Thu Sep 09 15:45:27 2021 +0200
@@ -150,6 +150,7 @@
subsection "Core of tactical proof system";
ML_file "term_ord.ML";
+ML_file "term_items.ML";
ML_file "term_subst.ML";
ML_file "General/completion.ML";
ML_file "General/name_space.ML";
@@ -171,6 +172,7 @@
ML_file "theory.ML";
ML_file "proofterm.ML";
ML_file "thm.ML";
+ML_file "cterm_items.ML";
ML_file "more_pattern.ML";
ML_file "more_unify.ML";
ML_file "more_thm.ML";
--- a/src/Pure/conv.ML Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/conv.ML Thu Sep 09 15:45:27 2021 +0200
@@ -81,7 +81,7 @@
fun try_conv cv = cv else_conv all_conv;
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
-fun cache_conv (cv: conv) = Thm.cterm_cache cv;
+fun cache_conv (cv: conv) = Ctermtab.cterm_cache cv;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/cterm_items.ML Thu Sep 09 15:45:27 2021 +0200
@@ -0,0 +1,38 @@
+(* Title: Pure/cterm_items.ML
+ Author: Makarius
+
+Scalable collections of term items: for type thm and cterm.
+See als Pure/term_items.ML.
+*)
+
+structure Ctermtab:
+sig
+ include TABLE
+ val cterm_cache: (cterm -> 'a) -> cterm -> 'a
+end =
+struct
+
+structure Table = Table(type key = cterm val ord = Thm.fast_term_ord);
+open Table;
+
+fun cterm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Thmtab:
+sig
+ include TABLE
+ val thm_cache: (thm -> 'a) -> thm -> 'a
+end =
+struct
+
+structure Table = Table(type key = thm val ord = Thm.thm_ord);
+open Table;
+
+fun thm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Cterms: TERM_ITEMS = Term_Items(type key = cterm val ord = Thm.fast_term_ord);
--- a/src/Pure/more_thm.ML Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/more_thm.ML Thu Sep 09 15:45:27 2021 +0200
@@ -12,9 +12,6 @@
val show_consts: bool Config.T
val show_hyps: bool Config.T
val show_tags: bool Config.T
- structure Cterms: ITEMS
- structure Ctermtab: TABLE
- structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
type attribute = Context.generic * thm -> Context.generic option * thm option
end;
@@ -22,9 +19,6 @@
signature THM =
sig
include THM
- structure Ctermtab: TABLE
- structure Thmtab: TABLE
- structure Cterms: ITEMS
val eq_ctyp: ctyp * ctyp -> bool
val aconvc: cterm * cterm -> bool
val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
@@ -41,11 +35,6 @@
val dest_equals_rhs: cterm -> cterm
val lhs_of: thm -> cterm
val rhs_of: thm -> cterm
- 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
val eq_thm: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
@@ -205,37 +194,12 @@
val rhs_of = dest_equals_rhs o Thm.cprop_of;
-(* certified term order *)
-
-val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of;
-val term_ord = Term_Ord.term_ord o apply2 Thm.term_of;
-
-
-(* thm order: ignores theory context! *)
-
-val thm_ord =
- Term_Ord.fast_term_ord o apply2 Thm.prop_of
- ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of
- ||| list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of
- ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of;
-
-
-(* scalable collections *)
-
-structure Cterms = Items(type key = cterm val ord = fast_term_ord);
-structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
-structure Thmtab = Table(type key = thm val ord = thm_ord);
-
-fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
-fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f;
-
-
(* equality *)
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
handle TERM _ => false;
-val eq_thm = is_equal o thm_ord;
+val eq_thm = is_equal o Thm.thm_ord;
val eq_thm_prop = op aconv o apply2 Thm.full_prop_of;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_items.ML Thu Sep 09 15:45:27 2021 +0200
@@ -0,0 +1,193 @@
+(* Title: Pure/term_items.ML
+ Author: Makarius
+
+Scalable collections of term items:
+ - table: e.g. for instantiation
+ - set with order of addition, e.g. occurrences within term
+*)
+
+signature TERM_ITEMS =
+sig
+ type key
+ type 'a table
+ val empty: 'a table
+ val build: ('a table -> 'a table) -> 'a table
+ val size: 'a table -> int
+ val is_empty: 'a table -> bool
+ val map: (key -> 'a -> 'b) -> 'a table -> 'b table
+ val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+ val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+ val dest: 'a table -> (key * 'a) list
+ val keys: 'a table -> key list
+ val exists: (key * 'a -> bool) -> 'a table -> bool
+ val forall: (key * 'a -> bool) -> 'a table -> bool
+ val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
+ val lookup: 'a table -> key -> 'a option
+ val defined: 'a table -> key -> bool
+ val add: key * 'a -> 'a table -> 'a table
+ val make: (key * 'a) list -> 'a table
+ type set = int table
+ val add_set: key -> set -> set
+ val make_set: key list -> set
+ val list_set: set -> key list
+ val list_set_rev: set -> key list
+ val subset: set * set -> bool
+ val eq_set: set * set -> bool
+end;
+
+functor Term_Items(Key: KEY): TERM_ITEMS =
+struct
+
+(* table with length *)
+
+structure Table = Table(Key);
+
+type key = Table.key;
+datatype 'a table = Items of int * 'a Table.table;
+
+fun size (Items (n, _)) = n;
+fun table (Items (_, tab)) = tab;
+
+val empty = Items (0, Table.empty);
+fun build (f: 'a table -> 'a table) = f empty;
+fun is_empty items = size items = 0;
+
+fun dest items = Table.dest (table items);
+fun keys items = Table.keys (table items);
+fun exists pred = Table.exists pred o table;
+fun forall pred = Table.forall pred o table;
+fun get_first get = Table.get_first get o table;
+fun lookup items = Table.lookup (table items);
+fun defined items = Table.defined (table items);
+
+fun add (key, x) (items as Items (n, tab)) =
+ if Table.defined tab key then items
+ else Items (n + 1, Table.update_new (key, x) tab);
+
+fun make entries = build (fold add entries);
+
+
+(* set with order of addition *)
+
+type set = int table;
+
+fun add_set x (items as Items (n, tab)) =
+ if Table.defined tab x then items
+ else Items (n + 1, Table.update_new (x, n) tab);
+
+fun make_set xs = build (fold add_set xs);
+
+fun subset (A: set, B: set) = forall (defined B o #1) A;
+fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+
+fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1
+val list_set = list_set_ord int_ord;
+val list_set_rev = list_set_ord (rev_order o int_ord);
+
+fun map f (Items (n, tab)) = Items (n, Table.map f tab);
+fun fold f = Table.fold f o table;
+fun fold_rev f = Table.fold_rev f o table;
+
+end;
+
+
+structure TFrees:
+sig
+ include TERM_ITEMS
+ val add_tfreesT: typ -> set -> set
+ val add_tfrees: term -> set -> set
+end =
+struct
+
+structure Items = Term_Items
+(
+ type key = string * sort;
+ val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord);
+);
+open Items;
+
+val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+
+end;
+
+
+structure TVars:
+sig
+ include TERM_ITEMS
+ val add_tvarsT: typ -> set -> set
+ val add_tvars: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items(
+ type key = indexname * sort;
+ val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord);
+);
+open Term_Items;
+
+val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
+val add_tvars = fold_types add_tvarsT;
+
+end;
+
+
+structure Frees:
+sig
+ include TERM_ITEMS
+ val add_frees: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+ type key = string * typ;
+ val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord);
+);
+open Term_Items;
+
+val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
+
+end;
+
+
+structure Vars:
+sig
+ include TERM_ITEMS
+ val add_vars: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+ type key = indexname * typ;
+ val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
+);
+open Term_Items;
+
+val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
+
+end;
+
+
+structure Names:
+sig
+ include TERM_ITEMS
+ val add_tfree_namesT: typ -> set -> set
+ val add_tfree_names: term -> set -> set
+ val add_free_names: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+ type key = string;
+ val ord = fast_string_ord
+);
+open Term_Items;
+
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
+
+end;
--- a/src/Pure/term_ord.ML Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/term_ord.ML Thu Sep 09 15:45:27 2021 +0200
@@ -2,137 +2,11 @@
Author: Tobias Nipkow, TU Muenchen
Author: Makarius
-Term orderings and scalable collections.
+Term orderings.
*)
-signature ITEMS =
-sig
- type key
- type 'a table
- val empty: 'a table
- val build: ('a table -> 'a table) -> 'a table
- val size: 'a table -> int
- val is_empty: 'a table -> bool
- val map: (key -> 'a -> 'b) -> 'a table -> 'b table
- val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
- val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
- val dest: 'a table -> (key * 'a) list
- val keys: 'a table -> key list
- val exists: (key * 'a -> bool) -> 'a table -> bool
- val forall: (key * 'a -> bool) -> 'a table -> bool
- val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
- val lookup: 'a table -> key -> 'a option
- val defined: 'a table -> key -> bool
- val add: key * 'a -> 'a table -> 'a table
- val make: (key * 'a) list -> 'a table
- type set = int table
- val add_set: key -> set -> set
- val make_set: key list -> set
- val list_set: set -> key list
- val list_set_rev: set -> key list
- val subset: set * set -> bool
- val eq_set: set * set -> bool
-end;
-
-functor Items(Key: KEY): ITEMS =
-struct
-
-(* table with length *)
-
-structure Table = Table(Key);
-
-type key = Table.key;
-datatype 'a table = Items of int * 'a Table.table;
-
-fun size (Items (n, _)) = n;
-fun table (Items (_, tab)) = tab;
-
-val empty = Items (0, Table.empty);
-fun build (f: 'a table -> 'a table) = f empty;
-fun is_empty items = size items = 0;
-
-fun dest items = Table.dest (table items);
-fun keys items = Table.keys (table items);
-fun exists pred = Table.exists pred o table;
-fun forall pred = Table.forall pred o table;
-fun get_first get = Table.get_first get o table;
-fun lookup items = Table.lookup (table items);
-fun defined items = Table.defined (table items);
-
-fun add (key, x) (items as Items (n, tab)) =
- if Table.defined tab key then items
- else Items (n + 1, Table.update_new (key, x) tab);
-
-fun make entries = build (fold add entries);
-
-
-(* set with order of addition *)
-
-type set = int table;
-
-fun add_set x (items as Items (n, tab)) =
- if Table.defined tab x then items
- else Items (n + 1, Table.update_new (x, n) tab);
-
-fun make_set xs = build (fold add_set xs);
-
-fun subset (A: set, B: set) = forall (defined B o #1) A;
-fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
-
-fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1
-val list_set = list_set_ord int_ord;
-val list_set_rev = list_set_ord (rev_order o int_ord);
-
-fun map f (Items (n, tab)) = Items (n, Table.map f tab);
-fun fold f = Table.fold f o table;
-fun fold_rev f = Table.fold_rev f o table;
-
-end;
-
-signature BASIC_TERM_ORD =
-sig
- structure Vartab: TABLE
- structure Sorttab: TABLE
- structure Typtab: TABLE
- structure Termtab: TABLE
- structure Var_Graph: GRAPH
- structure Sort_Graph: GRAPH
- structure Typ_Graph: GRAPH
- structure Term_Graph: GRAPH
- structure TFrees:
- sig
- include ITEMS
- val add_tfreesT: typ -> set -> set
- val add_tfrees: term -> set -> set
- end
- structure TVars:
- sig
- include ITEMS
- val add_tvarsT: typ -> set -> set
- val add_tvars: term -> set -> set
- end
- structure Frees:
- sig
- include ITEMS
- val add_frees: term -> set -> set
- end
- structure Vars:
- sig
- include ITEMS
- val add_vars: term -> set -> set
- end
- structure Names:
- sig
- include ITEMS
- val add_tfree_namesT: typ -> set -> set
- val add_tfree_names: term -> set -> set
- val add_free_names: term -> set -> set
- end
-end;
-
signature TERM_ORD =
sig
- include BASIC_TERM_ORD
val fast_indexname_ord: indexname ord
val sort_ord: sort ord
val typ_ord: typ ord
@@ -144,7 +18,6 @@
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;
structure Term_Ord: TERM_ORD =
@@ -326,65 +199,27 @@
val term_lpo = term_lpo
end;
+end;
+
(* scalable collections *)
-structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
-structure Sorttab = Table(type key = sort val ord = sort_ord);
-structure Typtab = Table(type key = typ val ord = typ_ord);
-structure Termtab = Table(type key = term val ord = fast_term_ord);
-
-fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+structure Vartab = Table(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sorttab = Table(type key = sort val ord = Term_Ord.sort_ord);
+structure Typtab = Table(type key = typ val ord = Term_Ord.typ_ord);
-structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord);
-structure Sort_Graph = Graph(type key = sort val ord = sort_ord);
-structure Typ_Graph = Graph(type key = typ val ord = typ_ord);
-structure Term_Graph = Graph(type key = term val ord = fast_term_ord);
-
-structure TFrees =
+structure Termtab:
+sig
+ include TABLE;
+ val term_cache: (term -> 'a) -> term -> 'a
+end =
struct
- structure Items =
- Items(type key = string * sort val ord = pointer_eq_ord (prod_ord fast_string_ord sort_ord));
- open Items;
- val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
- val add_tfrees = fold_types add_tfreesT;
-end;
-
-structure TVars =
-struct
- structure Items =
- Items(type key = indexname * sort val ord = pointer_eq_ord (prod_ord fast_indexname_ord sort_ord));
- open Items;
- val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
- val add_tvars = fold_types add_tvarsT;
+ structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord);
+ open Table;
+ fun term_cache f = Cache.create empty lookup update f;
end;
-structure Frees =
-struct
- structure Items =
- Items(type key = string * typ val ord = pointer_eq_ord (prod_ord fast_string_ord typ_ord));
- open Items;
- val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
-end;
-
-structure Vars =
-struct
- structure Items =
- Items(type key = indexname * typ val ord = pointer_eq_ord (prod_ord fast_indexname_ord typ_ord));
- open Items;
- val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
-end;
-
-structure Names =
-struct
- structure Items = Items(type key = string val ord = fast_string_ord);
- open Items;
- val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
- val add_tfree_names = fold_types add_tfree_namesT;
- val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
-end;
-
-end;
-
-structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
-open Basic_Term_Ord;
+structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
+structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
--- a/src/Pure/thm.ML Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/thm.ML Thu Sep 09 15:45:27 2021 +0200
@@ -41,6 +41,8 @@
val global_cterm_of: theory -> term -> cterm
val cterm_of: Proof.context -> term -> cterm
val renamed_term: term -> cterm -> cterm
+ val fast_term_ord: cterm ord
+ val term_ord: cterm ord
val dest_comb: cterm -> cterm * cterm
val dest_fun: cterm -> cterm
val dest_arg: cterm -> cterm
@@ -82,6 +84,7 @@
val cconcl_of: thm -> cterm
val cprems_of: thm -> cterm list
val chyps_of: thm -> cterm list
+ val thm_ord: thm ord
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
val theory_of_cterm: cterm -> theory
val theory_of_thm: thm -> theory
@@ -269,6 +272,9 @@
if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts}
else raise TERM ("renamed_term: terms disagree", [t, t']);
+val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of;
+val term_ord = Term_Ord.term_ord o apply2 term_of;
+
(* destructors *)
@@ -518,6 +524,15 @@
map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
+(* thm order: ignores theory context! *)
+
+val thm_ord =
+ Term_Ord.fast_term_ord o apply2 prop_of
+ ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
+ ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
+ ||| list_ord Term_Ord.sort_ord o apply2 shyps_of;
+
+
(* implicit theory context *)
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option;