--- a/src/Doc/Implementation/Proof.thy Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Doc/Implementation/Proof.thy Tue Sep 07 10:17:03 2021 +0200
@@ -101,7 +101,7 @@
@{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{define_ML Variable.import: "bool -> thm list -> Proof.context ->
- ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
+ ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
* Proof.context"} \\
@{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
((string * (string * typ)) list * term) * Proof.context"} \\
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Tue Sep 07 10:17:03 2021 +0200
@@ -6,7 +6,7 @@
ML_file \<open>../more_antiquote.ML\<close>
attribute_setup all =
- \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (K Thm.forall_intr_vars))\<close>
"quantified schematic vars"
setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
--- a/src/HOL/Analysis/metric_arith.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Analysis/metric_arith.ML Tue Sep 07 10:17:03 2021 +0200
@@ -24,8 +24,7 @@
fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
fun REPEAT' tac i = REPEAT (tac i)
-fun frees ct = Drule.cterm_add_frees ct []
-fun free_in v ct = member (op aconvc) (frees ct) v
+fun free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v
(* build a cterm set with elements cts of type ty *)
fun mk_ct_set ctxt ty =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Sep 07 10:17:03 2021 +0200
@@ -206,7 +206,7 @@
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
val nnf = K (nnf_conv ctxt then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
+ val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Misc_Legacy.cterm_frees tm)
(isolate_conv ctxt) nnf
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
whatis = whatis, simpset = ss}) vs
--- a/src/HOL/Decision_Procs/langford.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Tue Sep 07 10:17:03 2021 +0200
@@ -188,7 +188,7 @@
in
fn p =>
Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
- (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+ (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive)
(K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
end;
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -26,10 +26,10 @@
fun add_thm_insts ctxt thm =
let
- val tyvars = Thm.fold_terms Term.add_tvars thm [];
+ val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
- val tvars = Thm.fold_terms Term.add_vars thm [];
+ val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
val tvars' = tvars |> map (Logic.mk_term o Var);
val conj =
@@ -56,8 +56,8 @@
fun instantiate_xis ctxt insts thm =
let
- val tyvars = Thm.fold_terms Term.add_tvars thm [];
- val tvars = Thm.fold_terms Term.add_vars thm [];
+ val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
+ val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
fun add_inst (xi, t) (Ts, ts) =
(case AList.lookup (op =) tyvars xi of
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Sep 07 10:17:03 2021 +0200
@@ -868,9 +868,11 @@
then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
else raise Failure "substitutable_monomial"
| \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
- (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+ (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
+ (Thm.dest_arg1 tm)
handle Failure _ =>
- substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+ substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
+ (Thm.dest_arg tm))
| _ => raise Failure "substitutable_monomial")
fun isolate_variable v th =
--- a/src/HOL/Tools/Argo/argo_tactic.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Sep 07 10:17:03 2021 +0200
@@ -692,7 +692,7 @@
thm
|> instantiate_elim_rule
|> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
- |> Drule.forall_intr_vars
+ |> Thm.forall_intr_vars
|> Conv.fconv_rule (atomize_conv ctxt)
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 07 10:17:03 2021 +0200
@@ -830,7 +830,7 @@
(Variable.gen_all lthy
(Drule.rename_bvars'
(map (SOME o fst) xs')
- (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+ (Thm.forall_intr_vars (case_thm RS (sel_def RS trans)))));
val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
--- a/src/HOL/Tools/Function/function_core.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Tue Sep 07 10:17:03 2021 +0200
@@ -466,7 +466,7 @@
forall_intr_rename (n, Thm.cterm_of lthy (Var (varmap (n, T), T)))) qs thm
end
in
- ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
+ ((Rdef, map2 requantify intrs intrs_gen, Thm.forall_intr_vars elim_gen, induct), lthy)
end
fun define_graph (G_binding, G_type) fvar clauses RCss lthy =
@@ -809,7 +809,7 @@
|> Thm.forall_intr (Thm.cterm_of ctxt' x)
|> (fn it => Drule.compose (it, 2, wf_induct_rule))
|> curry op RS (Thm.assume wfR')
- |> forall_intr_vars
+ |> Thm.forall_intr_vars
|> (fn it => it COMP allI)
|> fold Thm.implies_intr hyps
|> Thm.implies_intr wfR'
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Sep 07 10:17:03 2021 +0200
@@ -300,7 +300,7 @@
val th =
th |> transform_elim_theorem
|> zero_var_indexes
- |> new_skolem ? forall_intr_vars
+ |> new_skolem ? Thm.forall_intr_vars
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
|> Meson.cong_extensionalize_thm ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Sep 07 10:17:03 2021 +0200
@@ -870,8 +870,8 @@
val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
fun rewrite_pat (ct1, ct2) =
(ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
- val t_insts' = map rewrite_pat t_insts
- val intro'' = Thm.instantiate (T_insts, t_insts') intro
+ val t_insts' = map rewrite_pat (Term_Subst.Vars.dest t_insts)
+ val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
val [intro'''] = Variable.export ctxt3 ctxt [intro'']
val intro'''' =
Simplifier.full_simplify
@@ -1162,7 +1162,9 @@
let
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
- let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
+ let
+ val t' = map_types (Logic.incr_tvar (i + 1))
+ (#2 (Type.varify_global Term_Subst.TFrees.empty t))
in (maxidx_of_term t', t' :: ts) end
val (i, cs') = List.foldr varify (~1, []) cs
val (i', intr_ts') = List.foldr varify (i, []) intr_ts
--- a/src/HOL/Tools/Qelim/qelim.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Tue Sep 07 10:17:03 2021 +0200
@@ -66,7 +66,7 @@
fun standard_qelim_conv ctxt atcv ncv qcv p =
let val pcv = pcv ctxt
- in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
+ in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end
end;
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Sep 07 10:17:03 2021 +0200
@@ -42,7 +42,7 @@
fun atomize_thm ctxt thm =
let
- val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
+ val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
--- a/src/HOL/Tools/SMT/smt_normalize.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Sep 07 10:17:03 2021 +0200
@@ -255,7 +255,7 @@
instantiate_elim #>
norm_def #>
Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
- Drule.forall_intr_vars #>
+ Thm.forall_intr_vars #>
Conv.fconv_rule (gen_normalize1_conv ctxt) #>
(* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
--- a/src/HOL/Tools/Transfer/transfer.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Sep 07 10:17:03 2021 +0200
@@ -696,7 +696,7 @@
val rules = extra_rules @ get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
- val thm1 = Drule.forall_intr_vars thm
+ val thm1 = Thm.forall_intr_vars thm
val instT =
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
@@ -731,7 +731,7 @@
val rules = extra_rules @ get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
- val thm1 = Drule.forall_intr_vars thm
+ val thm1 = Thm.forall_intr_vars thm
val instT =
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
--- a/src/HOL/Tools/choice_specification.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/choice_specification.ML Tue Sep 07 10:17:03 2021 +0200
@@ -99,7 +99,7 @@
val frees = map snd props''
val prop = myfoldr HOLogic.mk_conj (map fst props'')
- val (vmap, prop_thawed) = Type.varify_global [] prop
+ val (vmap, prop_thawed) = Type.varify_global Term_Subst.TFrees.empty prop
val thawed_prop_consts = collect_consts (prop_thawed, [])
val (altcos, overloaded) = split_list cos
val (names, sconsts) = split_list altcos
@@ -109,7 +109,7 @@
fun proc_const c =
let
- val (_, c') = Type.varify_global [] c
+ val (_, c') = Type.varify_global Term_Subst.TFrees.empty c
val (cname,ctyp) = dest_Const c'
in
(case filter (fn t =>
--- a/src/HOL/Tools/datatype_realizer.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 07 10:17:03 2021 +0200
@@ -131,7 +131,7 @@
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
- val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
+ val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []);
val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\<open>bool\<close> = tname_of (body_type T)) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
--- a/src/HOL/Tools/groebner.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/groebner.ML Tue Sep 07 10:17:03 2021 +0200
@@ -528,8 +528,7 @@
fun simp_ex_conv ctxt =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
-fun frees t = Drule.cterm_add_frees t [];
-fun free_in v t = member op aconvc (frees t) v;
+fun free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v;
val vsubst = let
fun vsubst (t,v) tm =
@@ -737,7 +736,7 @@
val T = Thm.typ_of_cterm x;
val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
in Thm.apply all (Thm.lambda x p) end
- val avs = Drule.cterm_add_frees tm []
+ val avs = Misc_Legacy.cterm_frees tm
val P' = fold mk_forall avs tm
val th1 = initial_conv ctxt (mk_neg P')
val (evs,bod) = strip_exists(concl th1) in
@@ -796,7 +795,7 @@
val mons = striplist(dest_binary ring_add_tm) t
in member (op aconvc) mons v andalso
forall (fn m => v aconvc m
- orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
+ orelse not(member (op aconvc) (Misc_Legacy.cterm_frees m) v)) mons
end
fun isolate_variable vars tm =
@@ -851,7 +850,7 @@
fun isolate_monomials vars tm =
let
val (cmons,vmons) =
- List.partition (fn m => null (inter (op aconvc) vars (frees m)))
+ List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m)))
(striplist ring_dest_add tm)
val cofactors = map (fn v => find_multipliers v vmons) vars
val cnc = if null cmons then zero_tm
--- a/src/Pure/General/buffer.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/buffer.ML Tue Sep 07 10:17:03 2021 +0200
@@ -9,8 +9,10 @@
type T
val empty: T
val is_empty: T -> bool
+ val add: string -> T -> T
val content: T -> string
- val add: string -> T -> T
+ val build: (T -> T) -> T
+ val build_content: (T -> T) -> string
val output: T -> (string -> unit) -> unit
val markup: Markup.T -> (T -> T) -> T -> T
end;
@@ -30,6 +32,9 @@
fun content (Buffer xs) = implode (rev xs);
+fun build (f: T -> T) = f empty;
+fun build_content f = build f |> content;
+
fun output (Buffer xs) out = List.app out (rev xs);
end;
--- a/src/Pure/General/graph_display.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/graph_display.ML Tue Sep 07 10:17:03 2021 +0200
@@ -65,8 +65,9 @@
fun build_graph entries =
let
val ident_names =
- fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
- entries Symtab.empty;
+ Symtab.build
+ (entries |> fold (fn ((ident, Node {name, ...}), _) =>
+ Symtab.update_new (ident, (name, ident))));
val the_key = the o Symtab.lookup ident_names;
in
Graph.empty
--- a/src/Pure/General/pretty.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/pretty.ML Tue Sep 07 10:17:03 2021 +0200
@@ -321,7 +321,7 @@
(* special output *)
(*symbolic markup -- no formatting*)
-fun symbolic prt =
+val symbolic =
let
fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
| out (Block ((bg, en), consistent, indent, prts, _)) =
@@ -332,15 +332,15 @@
Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
| out (Break (true, _, _)) = Buffer.add (Output.output "\n")
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(*unformatted output*)
-fun unformatted prt =
+val unformatted =
let
fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
| out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(* output interfaces *)
--- a/src/Pure/General/table.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/table.ML Tue Sep 07 10:17:03 2021 +0200
@@ -19,18 +19,20 @@
exception SAME
exception UNDEF of key
val empty: 'a table
+ val build: ('a table -> 'a table) -> 'a table
val is_empty: 'a table -> bool
val is_single: '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 size: 'a table -> int
val dest: 'a table -> (key * 'a) list
val keys: 'a table -> key list
val min: 'a table -> (key * 'a) option
val max: 'a table -> (key * 'a) option
- val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
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_key: 'a table -> key -> (key * 'a) option
val lookup: 'a table -> key -> 'a option
val defined: 'a table -> key -> bool
@@ -60,6 +62,8 @@
val insert_set: key -> set -> set
val remove_set: key -> set -> set
val make_set: key list -> set
+ val subset: set * set -> bool
+ val eq_set: set * set -> bool
end;
functor Table(Key: KEY): TABLE =
@@ -82,6 +86,8 @@
val empty = Empty;
+fun build (f: 'a table -> 'a table) = f empty;
+
fun is_empty Empty = true
| is_empty _ = false;
@@ -118,6 +124,7 @@
fold left (f p1 (fold mid (f p2 (fold right x))));
in fold end;
+fun size tab = fold_table (fn _ => fn n => n + 1) tab 0;
fun dest tab = fold_rev_table cons tab [];
fun keys tab = fold_rev_table (cons o #1) tab [];
@@ -137,6 +144,20 @@
| max (Branch3 (_, _, _, _, right)) = max right;
+(* exists and forall *)
+
+fun exists pred =
+ let
+ fun ex Empty = false
+ | ex (Branch2 (left, (k, x), right)) =
+ ex left orelse pred (k, x) orelse ex right
+ | ex (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+ ex left orelse pred (k1, x1) orelse ex mid orelse pred (k2, x2) orelse ex right;
+ in ex end;
+
+fun forall pred = not o exists (not o pred);
+
+
(* get_first *)
fun get_first f =
@@ -164,9 +185,6 @@
| some => some);
in get end;
-fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE);
-fun forall pred = not o exists (not o pred);
-
(* lookup *)
@@ -424,7 +442,7 @@
fun merge_list eq = join (fn _ => Library.merge eq);
-(* unit tables *)
+(* set operations *)
type set = unit table;
@@ -432,6 +450,9 @@
fun remove_set x : set -> set = delete_safe x;
fun make_set entries = fold insert_set entries empty;
+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);
+
(* ML pretty-printing *)
--- a/src/Pure/Isar/class.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/class.ML Tue Sep 07 10:17:03 2021 +0200
@@ -179,10 +179,8 @@
val type_space = Proof_Context.type_space ctxt;
val arities =
- Symtab.empty
- |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
- Symtab.map_default (class, []) (insert (op =) tyco)) arities)
- (Sorts.arities_of algebra);
+ Symtab.build (Sorts.arities_of algebra |> Symtab.fold (fn (tyco, arities) =>
+ fold (fn (class, _) => Symtab.map_default (class, []) (insert (op =) tyco)) arities));
fun prt_supersort class =
Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class));
@@ -610,7 +608,7 @@
| SOME sorts =>
fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
| matchings _ = I;
- val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
+ val tvartab = Vartab.build ((fold o fold_aterms) matchings ts)
handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
--- a/src/Pure/Isar/code.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/code.ML Tue Sep 07 10:17:03 2021 +0200
@@ -960,7 +960,7 @@
val _ = map (fn thm => if c = const_eqn thy thm then ()
else error ("Wrong head of code equation,\nexpected constant "
^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
- fun tvars_of T = rev (Term.add_tvarsT T []);
+ val tvars_of = build_rev o Term.add_tvarsT;
val vss = map (tvars_of o snd o head_eqn) thms;
fun inter_sorts vs =
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
--- a/src/Pure/Isar/generic_target.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/generic_target.ML Tue Sep 07 10:17:03 2021 +0200
@@ -95,8 +95,10 @@
val u = fold_rev lambda term_params rhs';
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
+ val type_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfreesT (Term.fastype_of u));
val extra_tfrees =
- subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+ build_rev (u |> (Term.fold_types o Term.fold_atyps)
+ (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
@@ -259,8 +261,11 @@
val xs = Variable.add_fixed lthy rhs' [];
val T = Term.fastype_of rhs;
- val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
- val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
+ val type_tfrees =
+ Term_Subst.TFrees.build (Term_Subst.add_tfreesT T #> fold (Term_Subst.add_tfreesT o #2) xs);
+ val extra_tfrees =
+ build_rev (rhs |> (Term.fold_types o Term.fold_atyps)
+ (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
@@ -302,8 +307,8 @@
val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
(*export fixes*)
- val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
- val frees = map Free (Thm.fold_terms Term.add_frees th' []);
+ val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []);
+ val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []);
val (th'' :: vs) =
(th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
|> Variable.export ctxt thy_ctxt
@@ -318,8 +323,8 @@
|>> map Logic.dest_type;
val instT =
- fold2 (fn a => fn b => (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I))
- tvars tfrees Term_Subst.TVars.empty;
+ Term_Subst.TVars.build (fold2 (fn a => fn b =>
+ (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I)) tvars tfrees);
val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
val cinst =
map_filter
--- a/src/Pure/Isar/method.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/method.ML Tue Sep 07 10:17:03 2021 +0200
@@ -118,7 +118,7 @@
fun insert_tac _ [] _ = all_tac
| insert_tac ctxt facts i =
- EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
+ EVERY (map (fn r => resolve_tac ctxt [Thm.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
fun insert thms =
CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
--- a/src/Pure/Isar/obtain.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/obtain.ML Tue Sep 07 10:17:03 2021 +0200
@@ -103,8 +103,11 @@
fun mk_all_internal ctxt (y, z) t =
let
+ val frees =
+ Term_Subst.Frees.build (t |> Term.fold_aterms
+ (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I));
val T =
- (case AList.lookup (op =) (Term.add_frees t []) z of
+ (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
SOME T => T
| NONE => the_default dummyT (Variable.default_type ctxt z));
in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
@@ -325,11 +328,16 @@
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
val instT =
- fold (Term.add_tvarsT o #2) params []
- |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
+ Term_Subst.TVars.build
+ (params |> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
+ (case T of
+ TVar v =>
+ if Term_Subst.TVars.defined instT v then instT
+ else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
+ | _ => instT))));
val closed_rule = rule
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
- |> Thm.instantiate (instT, []);
+ |> Thm.instantiate (Term_Subst.TVars.dest instT, []);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =
--- a/src/Pure/Isar/overloading.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/overloading.ML Tue Sep 07 10:17:03 2021 +0200
@@ -76,7 +76,7 @@
then SOME (ty', apply_subst t') else NONE
| NONE => NONE)
| _ => NONE) t;
- val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
+ val improvements = Vartab.build ((fold o fold_aterms) accumulate_improvements ts);
val ts' =
ts
|> (map o map_types) (Envir.subst_type improvements)
--- a/src/Pure/Isar/proof_context.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 07 10:17:03 2021 +0200
@@ -724,10 +724,10 @@
end;
val env =
- (fold o fold_atyps)
+ Vartab.build (tys |> (fold o fold_atyps)
(fn TFree (x, S) => constraint ((x, ~1), S)
| TVar v => constraint v
- | _ => I) tys Vartab.empty;
+ | _ => I));
fun get_sort xi raw_S =
if xi = dummy_var then
@@ -1269,8 +1269,8 @@
NONE => Inttab.empty
| SOME ctxt0 =>
let val cases0 = cases_of ctxt0 in
- Name_Space.fold_table (fn (a, _) => Inttab.insert_set (serial_of cases0 a))
- cases0 Inttab.empty
+ Inttab.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
+ Inttab.insert_set (serial_of cases0 a)))
end);
val cases = cases_of ctxt;
in
--- a/src/Pure/Isar/specification.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/specification.ML Tue Sep 07 10:17:03 2021 +0200
@@ -281,7 +281,7 @@
val _ =
Proof_Display.print_consts int (Position.thread_data ()) lthy5
- (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+ (Term_Subst.Frees.defined (Term_Subst.Frees.build (Term_Subst.add_frees lhs'))) [(x, T)];
in ((lhs, (def_name, th')), lthy5) end;
val definition' = gen_def check_spec_open (K I);
--- a/src/Pure/Isar/subgoal.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/subgoal.ML Tue Sep 07 10:17:03 2021 +0200
@@ -58,7 +58,7 @@
val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
- val schematics = (schematic_types, schematic_terms);
+ val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
val concl' = Thm.instantiate_cterm schematics concl;
val (prems, context) = Assumption.add_assumes asms' ctxt3;
@@ -88,15 +88,15 @@
val ts = map Thm.term_of params;
val prop = Thm.full_prop_of th';
- val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
- val vars = rev (Term.add_vars prop []);
+ val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
+ val vars = build_rev (Term.add_vars prop);
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
fun var_inst v y =
let
val ((x, i), T) = v;
val (U, args) =
- if member (op =) concl_vars v then (T, [])
+ if Term_Subst.Vars.defined concl_vars v then (T, [])
else (Ts ---> T, ts);
val u = Free (y, U);
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
--- a/src/Pure/PIDE/document.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/document.ML Tue Sep 07 10:17:03 2021 +0200
@@ -490,15 +490,15 @@
val versions' = fold delete_version version_ids versions;
val commands' =
- (versions', Inttab.empty) |->
+ Inttab.build (versions' |>
Inttab.fold (fn (_, version) => nodes_of version |>
String_Graph.fold (fn (_, (node, _)) => node |>
iterate_entries (fn ((_, command_id), _) =>
- SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
+ SOME o Inttab.insert (K true) (command_id, the_command state command_id)))));
val blobs' =
- (commands', Symtab.empty) |->
+ Symtab.build (commands' |>
Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
- fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I));
+ fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I)));
in (versions', blobs', commands', execution) end);
@@ -815,7 +815,7 @@
val nodes = nodes_of new_version;
val required = make_required nodes;
val required0 = make_required (nodes_of old_version);
- val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
+ val edited = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ())));
val updated = timeit "Document.update" (fn () =>
nodes |> String_Graph.schedule
--- a/src/Pure/PIDE/resources.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Sep 07 10:17:03 2021 +0200
@@ -118,8 +118,8 @@
(fn _ =>
({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
session_directories =
- fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
- session_directories Symtab.empty,
+ Symtab.build (session_directories |> fold_rev (fn (dir, name) =>
+ Symtab.cons_list (name, Path.explode dir))),
session_chapters = Symtab.make session_chapters,
bibtex_entries = Symtab.make bibtex_entries,
timings = make_timings command_timings,
--- a/src/Pure/PIDE/xml.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/xml.ML Tue Sep 07 10:17:03 2021 +0200
@@ -110,7 +110,7 @@
Elem (_, ts) => fold add_content ts
| Text s => Buffer.add s));
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+val content_of = Buffer.build_content o fold add_content;
(* trim blanks *)
@@ -164,9 +164,9 @@
else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
-(* output *)
+(* output content *)
-fun buffer_of depth tree =
+fun content_depth depth =
let
fun traverse _ (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
@@ -177,12 +177,11 @@
| traverse _ (Text s) = Buffer.add (text s)
and traverse_body 0 _ = Buffer.add "..."
| traverse_body d ts = fold (traverse (d - 1)) ts;
- in Buffer.empty |> traverse depth tree end;
+ in Buffer.build_content o traverse depth end;
-val string_of = Buffer.content o buffer_of ~1;
+val string_of = content_depth ~1;
-fun pretty depth tree =
- Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
--- a/src/Pure/PIDE/yxml.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/yxml.ML Tue Sep 07 10:17:03 2021 +0200
@@ -85,7 +85,7 @@
(* output *)
-fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
val string_of = string_of_body o single;
fun write_body path body =
--- a/src/Pure/Proof/extraction.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/extraction.ML Tue Sep 07 10:17:03 2021 +0200
@@ -123,8 +123,8 @@
fun msg d s = writeln (Symbol.spaces d ^ s);
-fun vars_of t = map Var (rev (Term.add_vars t []));
-fun frees_of t = map Free (rev (Term.add_frees t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
+fun frees_of t = map Free (build_rev (Term.add_frees t));
fun vfs_of t = vars_of t @ frees_of t;
val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
@@ -385,7 +385,7 @@
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
SOME (TVar (("'" ^ v, i), [])) else NONE)
- (rev (Term.add_vars prop' []));
+ (build_rev (Term.add_vars prop'));
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
fun typ_map T = Type.strip_sorts
--- a/src/Pure/Proof/proof_checker.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/proof_checker.ML Tue Sep 07 10:17:03 2021 +0200
@@ -16,7 +16,7 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
+ let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in
fn s =>
(case Symtab.lookup tab s of
NONE => error ("Unknown theorem " ^ quote s)
@@ -76,12 +76,12 @@
fun thm_of_atom thm Ts =
let
- val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
- val (fmap, thm') = Thm.varifyT_global' [] thm;
+ val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
+ val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
val ctye =
(tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
in
- Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+ Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Sep 07 10:17:03 2021 +0200
@@ -249,7 +249,7 @@
if member (op =) defs s then
let
val vs = vars_of prop;
- val tvars = Term.add_tvars prop [] |> rev;
+ val tvars = build_rev (Term.add_tvars prop);
val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
@@ -291,11 +291,11 @@
fun elim_vars mk_default prf =
let
val prop = Proofterm.prop_of prf;
- val tv = Term.add_vars prop [];
- val tf = Term.add_frees prop [];
+ val tv = Term_Subst.Vars.build (Term_Subst.add_vars prop);
+ val tf = Term_Subst.Frees.build (Term_Subst.add_frees prop);
- fun hidden_variable (Var v) = not (member (op =) tv v)
- | hidden_variable (Free f) = not (member (op =) tf f)
+ fun hidden_variable (Var v) = not (Term_Subst.Vars.defined tv v)
+ | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
| hidden_variable _ = false;
fun mk_default' T =
@@ -303,8 +303,8 @@
fun elim_varst (t $ u) = elim_varst t $ elim_varst u
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
- | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
- | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
+ | elim_varst (t as Free (x, T)) = if Term_Subst.Frees.defined tf (x, T) then t else mk_default' T
+ | elim_varst (t as Var (xi, T)) = if Term_Subst.Vars.defined tv (xi, T) then t else mk_default' T
| elim_varst t = t;
in
Proofterm.map_proof_terms (fn t =>
--- a/src/Pure/Syntax/ast.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Syntax/ast.ML Tue Sep 07 10:17:03 2021 +0200
@@ -158,7 +158,7 @@
end
| _ => (ast, []));
in
- SOME (mtch head pat Symtab.empty, args) handle NO_MATCH => NONE
+ SOME (Symtab.build (mtch head pat), args) handle NO_MATCH => NONE
end;
--- a/src/Pure/System/options.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/System/options.ML Tue Sep 07 10:17:03 2021 +0200
@@ -156,8 +156,8 @@
fun encode (Options tab) =
let
val opts =
- (tab, []) |-> Symtab.fold (fn (name, {pos, typ, value}) =>
- cons (Position.properties_of pos, (name, (typ, value))));
+ build (tab |> Symtab.fold (fn (name, {pos, typ, value}) =>
+ cons (Position.properties_of pos, (name, (typ, value)))));
open XML.Encode;
in list (pair properties (pair string (pair string string))) opts end;
--- a/src/Pure/Thy/export_theory.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Thy/export_theory.ML Tue Sep 07 10:17:03 2021 +0200
@@ -78,7 +78,7 @@
SOME goal => Thm.prems_of goal
| NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
end;
- val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
+ val typargs = build_rev (fold Term.add_tfrees (map (Free o #1) args @ axioms));
in {typargs = typargs, args = args, axioms = axioms} end;
fun get_locales thy =
@@ -148,8 +148,8 @@
{props = pos_properties pos,
name = name,
rough_classification = rough_classification,
- typargs = rev (fold Term.add_tfrees spec []),
- args = rev (fold Term.add_frees spec []),
+ typargs = build_rev (fold Term.add_tfrees spec),
+ args = build_rev (fold Term.add_frees spec),
terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
rules = drop (length terms) spec}
end;
@@ -172,7 +172,7 @@
val parent_spaces = map get_space parents;
val space = get_space thy;
in
- (decls, []) |-> fold (fn (name, decl) =>
+ build (decls |> fold (fn (name, decl) =>
if exists (fn space => Name_Space.declared space name) parent_spaces then I
else
(case export name decl of
@@ -181,7 +181,7 @@
let
val i = #serial (Name_Space.the_entry space name);
val body = if enabled then make_body () else [];
- in cons (i, XML.Elem (entity_markup space name, body)) end))
+ in cons (i, XML.Elem (entity_markup space name, body)) end)))
|> sort (int_ord o apply2 #1) |> map #2
|> export_body thy export_name
end;
--- a/src/Pure/Tools/find_consts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Tools/find_consts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -90,7 +90,7 @@
let val qty = make_pattern arg; in
fn (_, (ty, _)) =>
let
- val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
+ val tye = Vartab.build (Sign.typ_match thy (qty, ty));
val sub_size =
Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
in SOME sub_size end handle Type.TYPE_MATCH => NONE
--- a/src/Pure/Tools/rule_insts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Tools/rule_insts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -52,13 +52,13 @@
fun error_var msg (xi, pos) =
error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
-fun the_sort tvars (xi, pos) : sort =
- (case AList.lookup (op =) tvars xi of
+fun the_sort tvars (ai, pos) : sort =
+ (case Term_Subst.TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
SOME S => S
- | NONE => error_var "No such type variable in theorem: " (xi, pos));
+ | NONE => error_var "No such type variable in theorem: " (ai, pos));
fun the_type vars (xi, pos) : typ =
- (case AList.lookup (op =) vars xi of
+ (case Vartab.lookup vars xi of
SOME T => T
| NONE => error_var "No such variable in theorem: " (xi, pos));
@@ -71,17 +71,23 @@
else error_var "Bad sort for instantiation of type variable: " (xi, pos)
end;
-fun make_instT f v =
+fun make_instT f (tvars: Term_Subst.TVars.set) =
let
- val T = TVar v;
- val T' = f T;
- in if T = T' then NONE else SOME (v, T') end;
+ fun add v =
+ let
+ val T = TVar v;
+ val T' = f T;
+ in if T = T' then I else cons (v, T') end;
+ in Term_Subst.TVars.fold (add o #1) tvars [] end;
-fun make_inst f v =
+fun make_inst f vars =
let
- val t = Var v;
- val t' = f t;
- in if t aconv t' then NONE else SOME (v, t') end;
+ fun add v =
+ let
+ val t = Var v;
+ val t' = f t;
+ in if t aconv t' then I else cons (v, t') end;
+ in fold add vars [] end;
fun read_terms ss Ts ctxt =
let
@@ -92,7 +98,7 @@
|> Syntax.check_terms ctxt'
|> Variable.polymorphic ctxt';
val Ts' = map Term.fastype_of ts';
- val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
+ val tyenv = Vartab.build (fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts'));
val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
in ((ts', tyenv'), ctxt') end;
@@ -109,19 +115,21 @@
val (type_insts, term_insts) =
List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
- val tvars = Thm.fold_terms Term.add_tvars thm [];
- val vars = Thm.fold_terms Term.add_vars thm [];
+ val tvars = Term_Subst.TVars.build (Thm.fold_terms {hyps = false} Term_Subst.add_tvars thm);
+ val vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars thm);
(*eigen-context*)
val (_, ctxt1) = ctxt
- |> fold (Variable.declare_internal o Logic.mk_type o TVar) tvars
- |> fold (Variable.declare_internal o Var) vars
+ |> Term_Subst.TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars
+ |> Term_Subst.Vars.fold (Variable.declare_internal o Var o #1) vars
|> Proof_Context.add_fixes_cmd raw_fixes;
(*explicit type instantiations*)
val instT1 =
Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
- val vars1 = map (apsnd instT1) vars;
+ val vars1 =
+ Vartab.build (vars |> Term_Subst.Vars.fold (fn ((v, T), ()) =>
+ Vartab.insert (K true) (v, instT1 T)));
(*term instantiations*)
val (xs, ss) = split_list term_insts;
@@ -130,15 +138,15 @@
(*implicit type instantiations*)
val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
- val vars2 = map (apsnd instT2) vars1;
+ val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 [];
val inst2 =
Term_Subst.instantiate (Term_Subst.TVars.empty,
- fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t))
- xs ts Term_Subst.Vars.empty)
+ Term_Subst.Vars.build
+ (fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t)) xs ts))
#> Envir.beta_norm;
- val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
- val inst_vars = map_filter (make_inst inst2) vars2;
+ val inst_tvars = make_instT (instT2 o instT1) tvars;
+ val inst_vars = make_inst inst2 vars2;
in ((inst_tvars, inst_vars), ctxt2) end;
end;
@@ -166,8 +174,8 @@
| zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
| zip_vars [] _ = error "More instantiations than variables in theorem";
val insts =
- zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
- zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
+ zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @
+ zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args;
in where_rule ctxt insts fixes thm end;
fun read_instantiate ctxt insts xs =
--- a/src/Pure/consts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/consts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -227,8 +227,8 @@
val declT = type_scheme consts c;
val args = typargs consts (c, declT);
val inst =
- fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T))
- args Ts Term_Subst.TVars.empty
+ Term_Subst.TVars.build
+ (fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T)) args Ts)
handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
in declT |> Term_Subst.instantiateT inst end;
--- a/src/Pure/context.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/context.ML Tue Sep 07 10:17:03 2021 +0200
@@ -466,10 +466,10 @@
end;
fun theory_data_size thy =
- (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
+ build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
(case Theory_Data.obj_size k thy of
NONE => I
- | SOME n => (cons (invoke_pos k, n))));
+ | SOME n => (cons (invoke_pos k, n)))));
--- a/src/Pure/defs.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/defs.ML Tue Sep 07 10:17:03 2021 +0200
@@ -85,13 +85,13 @@
fun disjoint_args (Ts, Us) =
not (Type.could_unifys (Ts, Us)) orelse
- ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
+ ((Vartab.build (Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us)); false)
handle Type.TUNIFY => true);
fun match_args (Ts, Us) =
if Type.could_matches (Ts, Us) then
Option.map Envir.subst_type
- (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+ (SOME (Vartab.build (Type.raw_matches (Ts, Us))) handle Type.TYPE_MATCH => NONE)
else NONE;
@@ -148,10 +148,10 @@
NONE => false
| SOME {specs, ...} => Inttab.defined specs i));
in
- (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) =>
+ build (defs |> Itemtab.fold (fn (c, {specs, ...}) =>
specs |> Inttab.fold (fn (i, spec) =>
if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i)
- then cons (#2 c, the (#def spec)) else I))
+ then cons (#2 c, the (#def spec)) else I)))
end;
val empty = Defs Itemtab.empty;
--- a/src/Pure/drule.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/drule.ML Tue Sep 07 10:17:03 2021 +0200
@@ -14,7 +14,6 @@
val strip_imp_concl: cterm -> cterm
val cprems_of: thm -> cterm list
val forall_intr_list: cterm list -> thm -> thm
- val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
@@ -89,8 +88,6 @@
val mk_term: cterm -> thm
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
- val cterm_add_frees: cterm -> cterm list -> cterm list
- val cterm_add_vars: cterm -> cterm list -> cterm list
val dummy_thm: thm
val free_dummy_thm: thm
val is_sort_constraint: term -> bool
@@ -165,9 +162,6 @@
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev Thm.forall_intr;
-(*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
-
fun outer_params t =
let val vs = Term.strip_all_vars t
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
@@ -185,11 +179,18 @@
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
val Ts = map Term.fastype_of ps;
val inst =
- Thm.fold_terms Term.add_vars th []
- |> map (fn (xi, T) => ((xi, T), Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))));
+ Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+ (fn t => fn inst =>
+ (case t of
+ Var (xi, T) =>
+ if Term_Subst.Vars.defined inst (xi, T) then inst
+ else
+ let val ct = Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))
+ in Term_Subst.Vars.update ((xi, T), ct) inst end
+ | _ => inst)));
in
th
- |> Thm.instantiate ([], inst)
+ |> Thm.instantiate ([], Term_Subst.Vars.dest inst)
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
@@ -212,17 +213,17 @@
val (instT, inst) =
Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
- val tvars = fold Thm.add_tvars ths [];
- fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
+ val tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty;
+ val the_tvar = the o Term_Subst.TVars.lookup tvars;
val instT' =
- (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
- cons (v, Thm.rename_tvar b (the_tvar v)));
+ build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+ cons (v, Thm.rename_tvar b (the_tvar v))));
- val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
- fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
+ val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths Term_Subst.Vars.empty;
+ val the_var = the o Term_Subst.Vars.lookup vars;
val inst' =
- (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
- cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
+ build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+ cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))));
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -610,9 +611,6 @@
fun cterm_rule f = dest_term o f o mk_term;
-val cterm_add_frees = Thm.add_frees o mk_term;
-val cterm_add_vars = Thm.add_vars o mk_term;
-
val dummy_thm = mk_term (certify Term.dummy_prop);
val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
@@ -788,7 +786,7 @@
fun infer_instantiate' ctxt args th =
let
- val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
+ val vars = build_rev (Term.add_vars (Thm.full_prop_of th));
val args' = zip_options vars args
handle ListPair.UnequalLengths =>
raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]);
--- a/src/Pure/envir.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/envir.ML Tue Sep 07 10:17:03 2021 +0200
@@ -395,7 +395,7 @@
(** expand defined atoms -- with local beta reduction **)
fun expand_atom T (U, u) =
- subst_term_types (Type.raw_match (U, T) Vartab.empty) u
+ subst_term_types (Vartab.build (Type.raw_match (U, T))) u
handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
fun expand_term get =
--- a/src/Pure/facts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/facts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -217,7 +217,8 @@
fun consolidate facts =
let
val unfinished =
- (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
+ build (facts |> fold_static_lazy (fn (_, ths) =>
+ if Lazy.is_finished ths then I else cons ths));
val _ = Lazy.consolidate unfinished;
in facts end;
--- a/src/Pure/global_theory.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/global_theory.ML Tue Sep 07 10:17:03 2021 +0200
@@ -124,8 +124,8 @@
fun lookup_thm_id thy =
let
val theories =
- fold (fn thy' => Symtab.update (Context.theory_long_name thy', lazy_thm_names thy'))
- (Theory.nodes_of thy) Symtab.empty;
+ Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
+ Symtab.update (Context.theory_long_name thy', lazy_thm_names thy')));
fun lookup (thm_id: Proofterm.thm_id) =
(case Symtab.lookup theories (#theory_name thm_id) of
NONE => NONE
@@ -170,8 +170,8 @@
fun transfer_theories thy =
let
val theories =
- fold (fn thy' => Symtab.update (Context.theory_name thy', thy'))
- (Theory.nodes_of thy) Symtab.empty;
+ Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
+ Symtab.update (Context.theory_name thy', thy')));
fun transfer th =
Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
in transfer end;
--- a/src/Pure/goal.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/goal.ML Tue Sep 07 10:17:03 2021 +0200
@@ -116,30 +116,34 @@
val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
- val xs = map Free (fold Term.add_frees (prop :: As) []);
- val fixes = map (Thm.cterm_of ctxt) xs;
+ val frees = Term_Subst.Frees.build (fold Term_Subst.add_frees (prop :: As));
+ val xs = Term_Subst.Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
- val tfrees = fold Term.add_tfrees (prop :: As) [];
- val tfrees_set = fold (Symtab.insert_set o #1) tfrees Symtab.empty;
- val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
+ val tfrees = Term_Subst.TFrees.build (fold Term_Subst.add_tfrees (prop :: As));
+ val Ts = Symtab.build (Term_Subst.TFrees.fold (Symtab.insert_set o #1 o #1) tfrees);
+ val instT =
+ build (tfrees |> Term_Subst.TFrees.fold (fn ((a, S), ()) =>
+ cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
val global_prop =
- Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
+ Logic.list_implies (As, prop)
+ |> Term_Subst.Frees.fold_rev (Logic.all o Free o #1) frees
+ |> Logic.varify_types_global
|> Thm.cterm_of ctxt
|> Thm.weaken_sorts' ctxt;
val global_result = result |> Future.map
(Drule.flexflex_unique (SOME ctxt) #>
Drule.implies_intr_list assms #>
- Drule.forall_intr_list fixes #>
+ Drule.forall_intr_list xs #>
Thm.adjust_maxidx_thm ~1 #>
- Thm.generalize (tfrees_set, Symtab.empty) 0 #>
+ Thm.generalize (Ts, Symtab.empty) 0 #>
Thm.strip_shyps #>
Thm.solve_constraints);
val local_result =
Thm.future global_result global_prop
|> Thm.close_derivation \<^here>
|> Thm.instantiate (instT, [])
- |> Drule.forall_elim_list fixes
+ |> Drule.forall_elim_list xs
|> fold (Thm.elim_implies o Thm.assume) assms
|> Thm.solve_constraints;
in local_result end;
--- a/src/Pure/library.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/library.ML Tue Sep 07 10:17:03 2021 +0200
@@ -51,6 +51,8 @@
val forall: ('a -> bool) -> 'a list -> bool
(*lists*)
+ val build: ('a list -> 'a list) -> 'a list
+ val build_rev: ('a list -> 'a list) -> 'a list
val single: 'a -> 'a list
val the_single: 'a list -> 'a
val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -301,6 +303,9 @@
(** lists **)
+fun build (f: 'a list -> 'a list) = f [];
+fun build_rev f = build f |> rev;
+
fun single x = [x];
fun the_single [x] = x
--- a/src/Pure/more_thm.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/more_thm.ML Tue Sep 07 10:17:03 2021 +0200
@@ -25,9 +25,8 @@
structure Thmtab: TABLE
val eq_ctyp: ctyp * ctyp -> bool
val aconvc: cterm * cterm -> bool
- val add_tvars: thm -> ctyp list -> ctyp list
- val add_frees: thm -> cterm list -> cterm list
- val add_vars: thm -> cterm list -> cterm list
+ val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
+ val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -76,6 +75,7 @@
val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
+ val forall_intr_vars: thm -> thm
val unvarify_global: theory -> thm -> thm
val unvarify_axiom: theory -> string -> thm
val rename_params_rule: string list * int -> thm -> thm
@@ -137,9 +137,15 @@
val eq_ctyp = op = o apply2 Thm.typ_of;
val op aconvc = op aconv o apply2 Thm.term_of;
-val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
-val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
-val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+val add_tvars =
+ Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
+ let val v = Term.dest_TVar (Thm.typ_of cT)
+ in tab |> not (Term_Subst.TVars.defined tab v) ? Term_Subst.TVars.update (v, cT) end);
+
+val add_vars =
+ Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
+ let val v = Term.dest_Var (Thm.term_of ct)
+ in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
(* ctyp operations *)
@@ -378,7 +384,7 @@
fun forall_elim_vars_list vars i th =
let
val used =
- (Thm.fold_terms o Term.fold_aterms)
+ (Thm.fold_terms {hyps = false} o Term.fold_aterms)
(fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
val vars' = (Name.variant_list used (map #1 vars), vars)
|> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
@@ -408,8 +414,8 @@
val idx = Thm.maxidx_of th + 1;
fun index ((a, A), b) = (((a, idx), A), b);
val insts = (map index instT, map index inst);
- val tfrees = fold (Symtab.insert_set o #1 o #1) instT Symtab.empty;
- val frees = fold (Symtab.insert_set o #1 o #1) inst Symtab.empty;
+ val tfrees = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT);
+ val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) inst);
val hyps = Thm.chyps_of th;
val inst_cterm =
@@ -437,24 +443,40 @@
zip_options xs ys handle ListPair.UnequalLengths =>
err "more instantiations than variables in thm";
- val thm' =
- Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
- val thm'' =
- Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
- in thm'' end;
+ val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs;
+ val thm' = Thm.instantiate (instT, []) thm;
+ val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts;
+ in Thm.instantiate ([], inst) thm' end;
-(* forall_intr_frees: generalization over all suitable Free variables *)
+(* implicit generalization over variables -- canonical order *)
+
+fun forall_intr_vars th =
+ let
+ val (_, vars) =
+ (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+ (fn ct => fn (seen, vars) =>
+ let val v = Term.dest_Var (Thm.term_of ct) in
+ if not (Term_Subst.Vars.defined seen v)
+ then (Term_Subst.Vars.add (v, ()) seen, ct :: vars)
+ else (seen, vars)
+ end);
+ in fold Thm.forall_intr vars th end;
fun forall_intr_frees th =
let
val fixed =
- fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) [];
- val frees =
- Thm.fold_atomic_cterms (fn a =>
- (case Thm.term_of a of
- Free v => not (member (op =) fixed v) ? insert (op aconvc) a
- | _ => I)) th [];
+ Term_Subst.Frees.build
+ (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
+ fold Term_Subst.add_frees (Thm.hyps_of th));
+ val (_, frees) =
+ (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
+ (fn ct => fn (seen, frees) =>
+ let val v = Term.dest_Free (Thm.term_of ct) in
+ if not (Term_Subst.Frees.defined seen v)
+ then (Term_Subst.Frees.add (v, ()) seen, ct :: frees)
+ else (seen, frees)
+ end);
in fold Thm.forall_intr frees th end;
@@ -466,12 +488,27 @@
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
- val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
- val instantiateT = Term_Subst.instantiateT (Term_Subst.TVars.table instT);
- val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
- let val T' = instantiateT T
- in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
- in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
+ val cert = Thm.global_cterm_of thy;
+ val certT = Thm.global_ctyp_of thy;
+
+ val instT =
+ Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
+ (fn T => fn instT =>
+ (case T of
+ TVar (v as ((a, _), S)) =>
+ if Term_Subst.TVars.defined instT v then instT
+ else Term_Subst.TVars.update (v, TFree (a, S)) instT
+ | _ => instT)));
+ val cinstT = Term_Subst.TVars.map (K certT) instT;
+ val cinst =
+ Term_Subst.Vars.build (prop |> Term.fold_aterms
+ (fn t => fn inst =>
+ (case t of
+ Var ((x, i), T) =>
+ let val T' = Term_Subst.instantiateT instT T
+ in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end
+ | _ => inst)));
+ in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end;
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
@@ -515,7 +552,7 @@
fun stripped_sorts thy t =
let
- val tfrees = rev (Term.add_tfrees t []);
+ val tfrees = build_rev (Term.add_tfrees t);
val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees));
val recover =
map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
--- a/src/Pure/morphism.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/morphism.ML Tue Sep 07 10:17:03 2021 +0200
@@ -138,11 +138,11 @@
| instantiate_frees_morphism (cinstT, cinst) =
let
val instT =
- fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT))
- cinstT Term_Subst.TFrees.empty;
+ Term_Subst.TFrees.build
+ (cinstT |> fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT)));
val inst =
- fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct))
- cinst Term_Subst.Frees.empty;
+ Term_Subst.Frees.build
+ (cinst |> fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct)));
in
morphism "instantiate_frees"
{binding = [],
@@ -157,11 +157,11 @@
| instantiate_morphism (cinstT, cinst) =
let
val instT =
- fold (fn (v, cT) => Term_Subst.TVars.add (v, Thm.typ_of cT))
- cinstT Term_Subst.TVars.empty;
+ Term_Subst.TVars.build (cinstT |> fold (fn (v, cT) =>
+ Term_Subst.TVars.add (v, Thm.typ_of cT)));
val inst =
- fold (fn (v, ct) => Term_Subst.Vars.add (v, Thm.term_of ct))
- cinst Term_Subst.Vars.empty;
+ Term_Subst.Vars.build (cinst |> fold (fn (v, ct) =>
+ Term_Subst.Vars.add (v, Thm.term_of ct)));
in
morphism "instantiate"
{binding = [],
--- a/src/Pure/primitive_defs.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/primitive_defs.ML Tue Sep 07 10:17:03 2021 +0200
@@ -37,7 +37,7 @@
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
val lhs = Envir.beta_eta_contract raw_lhs;
val (head, args) = Term.strip_comb lhs;
- val head_tfrees = Term.add_tfrees head [];
+ val head_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfrees head);
fun check_arg (Bound _) = true
| check_arg (Free (x, _)) = check_free_lhs x
@@ -52,7 +52,7 @@
if check_free_rhs x orelse member (op aconv) args v then I
else insert (op aconv) v | _ => I) rhs [];
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
- if check_tfree a orelse member (op =) head_tfrees (a, S) then I
+ if check_tfree a orelse Term_Subst.TFrees.defined head_tfrees (a, S) then I
else insert (op =) v | _ => I)) rhs [];
in
if not (check_head head) then
--- a/src/Pure/proofterm.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/proofterm.ML Tue Sep 07 10:17:03 2021 +0200
@@ -109,7 +109,7 @@
val implies_intr_proof': term -> proof -> proof
val forall_intr_proof: string * term -> typ option -> proof -> proof
val forall_intr_proof': term -> proof -> proof
- val varify_proof: term -> (string * sort) list -> proof -> proof
+ val varify_proof: term -> Term_Subst.TFrees.set -> proof -> proof
val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
val permute_prems_proof: term list -> int -> int -> proof -> proof
@@ -671,25 +671,37 @@
(* substitutions *)
-fun del_conflicting_tvars envT T =
+local
+
+fun conflicting_tvarsT envT =
+ Term.fold_atyps
+ (fn T => fn instT =>
+ (case T of
+ TVar (v as (_, S)) =>
+ if Term_Subst.TVars.defined instT v orelse can (Type.lookup envT) v then instT
+ else Term_Subst.TVars.update (v, Logic.dummy_tfree S) instT
+ | _ => instT));
+
+fun conflicting_tvars env =
+ Term.fold_aterms
+ (fn t => fn inst =>
+ (case t of
+ Var (v as (_, T)) =>
+ if Term_Subst.Vars.defined inst v orelse can (Envir.lookup env) v then inst
+ else Term_Subst.Vars.update (v, Free ("dummy", T)) inst
+ | _ => inst));
+
+fun del_conflicting_tvars envT ty =
+ Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty;
+
+fun del_conflicting_vars env tm =
let
val instT =
- map_filter (fn ixnS as (_, S) =>
- (Type.lookup envT ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])
- in Term_Subst.instantiateT (Term_Subst.TVars.table instT) T end;
+ Term_Subst.TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
+ val inst = Term_Subst.Vars.build (tm |> conflicting_tvars env);
+ in Term_Subst.instantiate (instT, inst) tm end;
-fun del_conflicting_vars env t =
- let
- val instT =
- map_filter (fn ixnS as (_, S) =>
- (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []);
- val inst =
- map_filter (fn (ixnT as (_, T)) =>
- (Envir.lookup env ixnT; NONE) handle TYPE _ =>
- SOME (ixnT, Free ("dummy", T))) (Term.add_vars t []);
- in Term_Subst.instantiate (Term_Subst.TVars.make instT, Term_Subst.Vars.table inst) t end;
+in
fun norm_proof env =
let
@@ -726,6 +738,8 @@
| norm _ = raise Same.SAME;
in Same.commit norm end;
+end;
+
(* remove some types in proof term (to save space) *)
@@ -887,8 +901,9 @@
fun varify_proof t fixed prf =
let
- val fs = Term.fold_types (Term.fold_atyps
- (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+ val fs =
+ build (t |> (Term.fold_types o Term.fold_atyps)
+ (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
@@ -1110,7 +1125,7 @@
| is_fun (TVar _) = true
| is_fun _ = false;
-fun vars_of t = map Var (rev (Term.add_vars t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
fun add_funvars Ts (vs, t) =
if is_fun (fastype_of1 (Ts, t)) then
@@ -2131,7 +2146,7 @@
fun export_body (PBody {thms, ...}) = fold export_thm thms;
- val exports = (bodies, Inttab.empty) |-> fold export_body |> Inttab.dest;
+ val exports = Inttab.build (fold export_body bodies) |> Inttab.dest;
in List.app (Lazy.force o #2) exports end;
local
@@ -2312,7 +2327,7 @@
end)
| boxes_of MinProof = raise MIN_PROOF ()
| boxes_of _ = I;
- in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end;
+ in Inttab.fold_rev (cons o #2) (Inttab.build (fold boxes_of proofs)) [] end;
end;
--- a/src/Pure/raw_simplifier.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Sep 07 10:17:03 2021 +0200
@@ -161,13 +161,13 @@
fun rewrite_rule_extra_vars prems elhs erhs =
let
val elhss = elhs :: prems;
- val tvars = fold Term.add_tvars elhss [];
- val vars = fold Term.add_vars elhss [];
+ val tvars = Term_Subst.TVars.build (fold Term_Subst.add_tvars elhss);
+ val vars = Term_Subst.Vars.build (fold Term_Subst.add_vars elhss);
in
erhs |> Term.exists_type (Term.exists_subtype
- (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
+ (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
erhs |> Term.exists_subterm
- (fn Var v => not (member (op =) vars v) | _ => false)
+ (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
end;
fun rrule_extra_vars elhs thm =
@@ -474,6 +474,8 @@
(cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
ctxt));
+val vars_set = Term_Subst.Vars.build o Term_Subst.add_vars;
+
local
fun vperm (Var _, Var _) = true
@@ -481,8 +483,7 @@
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
| vperm (t, u) = (t = u);
-fun var_perm (t, u) =
- vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
+fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
in
@@ -945,7 +946,7 @@
while the premises are solved.*)
fun cond_skel (args as (_, (lhs, rhs))) =
- if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
+ if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
else skel0;
(*
--- a/src/Pure/sorts.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/sorts.ML Tue Sep 07 10:17:03 2021 +0200
@@ -257,9 +257,8 @@
(* classrel *)
-fun rebuild_arities context algebra = algebra |> map_arities (fn arities =>
- Symtab.empty
- |> add_arities_table context algebra arities);
+fun rebuild_arities context algebra = algebra
+ |> map_arities (Symtab.build o add_arities_table context algebra);
fun add_classrel context rel = rebuild_arities context o map_classes (fn classes =>
classes |> Graph.add_edge_trans_acyclic rel
@@ -286,12 +285,11 @@
if pointer_eq (ars1, ars2) then raise Symtab.SAME
else insert_ars context algebra0 t ars2 ars1)
| (false, true) => (*unary completion*)
- Symtab.empty
- |> add_arities_table context algebra0 arities1
+ Symtab.build (add_arities_table context algebra0 arities1)
| (false, false) => (*binary completion*)
- Symtab.empty
- |> add_arities_table context algebra0 arities1
- |> add_arities_table context algebra0 arities2);
+ Symtab.build
+ (add_arities_table context algebra0 arities1 #>
+ add_arities_table context algebra0 arities2));
in make_algebra (classes', arities') end;
@@ -301,16 +299,16 @@
let
fun new_classrel rel = not (exists (fn algebra => class_less algebra rel) parents);
val classrel =
- (classes, []) |-> Graph.fold (fn (c, (_, (_, ds))) =>
+ build (classes |> Graph.fold (fn (c, (_, (_, ds))) =>
(case filter (fn d => new_classrel (c, d)) (Graph.Keys.dest ds) of
[] => I
- | ds' => cons (c, sort_strings ds')))
+ | ds' => cons (c, sort_strings ds'))))
|> sort_by #1;
fun is_arity t ar algebra = member (op =) (Symtab.lookup_list (arities_of algebra) t) ar;
fun add_arity t (c, Ss) = not (exists (is_arity t (c, Ss)) parents) ? cons (t, Ss, c);
val arities =
- (arities, []) |-> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars))
+ build (arities |> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars)))
|> sort_by #1;
in {classrel = classrel, arities = arities} end;
@@ -390,7 +388,7 @@
in uncurry meet end;
fun meet_sort_typ algebra (T, S) =
- let val tab = meet_sort algebra (T, S) Vartab.empty;
+ let val tab = Vartab.build (meet_sort algebra (T, S));
in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
--- a/src/Pure/term_subst.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/term_subst.ML Tue Sep 07 10:17:03 2021 +0200
@@ -17,7 +17,7 @@
structure Tab = Table(Key);
fun add entry = Tab.insert (K true) entry;
-fun table entries = fold add entries Tab.empty;
+fun table entries = Tab.build (fold add entries);
open Tab;
@@ -29,6 +29,15 @@
structure TVars: INST_TABLE
structure Frees: INST_TABLE
structure Vars: INST_TABLE
+ val add_tfreesT: typ -> TFrees.set -> TFrees.set
+ val add_tfrees: term -> TFrees.set -> TFrees.set
+ val add_tvarsT: typ -> TVars.set -> TVars.set
+ val add_tvars: term -> TVars.set -> TVars.set
+ val add_frees: term -> Frees.set -> Frees.set
+ val add_vars: term -> Vars.set -> Vars.set
+ val add_tfree_namesT: typ -> Symtab.set -> Symtab.set
+ val add_tfree_names: term -> Symtab.set -> Symtab.set
+ val add_free_names: term -> Symtab.set -> Symtab.set
val map_atypsT_same: typ Same.operation -> typ Same.operation
val map_types_same: typ Same.operation -> term Same.operation
val map_aterms_same: term Same.operation -> term Same.operation
@@ -77,6 +86,16 @@
val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
);
+val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I);
+val add_tvars = fold_types add_tvarsT;
+val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I);
+val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I);
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I);
+
(* generic mapping *)
@@ -256,12 +275,12 @@
let
val (instT, _) =
(TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1)
- ((fold o fold_types o fold_atyps) (fn TVar v =>
- TVars.add (v, ()) | _ => I) ts TVars.empty);
+ (TVars.build (ts |> (fold o fold_types o fold_atyps)
+ (fn TVar v => TVars.add (v, ()) | _ => I)));
val (inst, _) =
(Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1)
- ((fold o fold_aterms) (fn Var (xi, T) =>
- Vars.add ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty);
+ (Vars.build (ts |> (fold o fold_aterms)
+ (fn Var (xi, T) => Vars.add ((xi, instantiateT instT T), ()) | _ => I)));
in (instT, inst) end;
fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
--- a/src/Pure/theory.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/theory.ML Tue Sep 07 10:17:03 2021 +0200
@@ -244,10 +244,10 @@
[] => (item, map Logic.varifyT_global args)
| vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
- val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
+ val lhs_vars = Term_Subst.TFrees.build (snd lhs |> fold Term_Subst.add_tfreesT);
val rhs_extras =
- fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
- if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
+ build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
+ (fn TFree v => not (Term_Subst.TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
val _ =
if null rhs_extras then ()
else error ("Specification depends on extra type variables: " ^
--- a/src/Pure/thm.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/thm.ML Tue Sep 07 10:17:03 2021 +0200
@@ -59,9 +59,9 @@
val first_order_match: cterm * cterm ->
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
(*theorems*)
- val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
- val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
- val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_atomic_cterms: {hyps: bool} -> (term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_id: thm -> Context.theory_id
@@ -161,7 +161,7 @@
val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val unconstrainT: thm -> thm
- val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm
val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
val plain_prop_of: thm -> term
@@ -434,19 +434,22 @@
fun rep_thm (Thm (_, args)) = args;
-fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
- fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
+fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) =
+ fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;
-fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
- in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end;
+ in (fold_terms h o fold_types o fold_atyps) (fn T => if g T then f (ctyp T) else I) th end;
-fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) =
- let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in
- (fold_terms o fold_aterms)
- (fn t as Const (_, T) => f (cterm t T)
- | t as Free (_, T) => f (cterm t T)
- | t as Var (_, T) => f (cterm t T)
+fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+ let
+ fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps};
+ fun apply t T = if g t then f (cterm t T) else I;
+ in
+ (fold_terms h o fold_aterms)
+ (fn t as Const (_, T) => apply t T
+ | t as Free (_, T) => apply t T
+ | t as Var (_, T) => apply t T
| _ => I) th
end;
@@ -985,7 +988,7 @@
(*Dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
- Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
+ Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;
(*Remove extra sorts that are witnessed by type signature information*)
fun strip_shyps thm =
@@ -1001,7 +1004,8 @@
fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
- val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+ val present =
+ (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
val extra = fold (Sorts.remove_sort o #2) present shyps;
val witnessed = Sign.witness_sorts thy present extra;
val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
@@ -1641,8 +1645,8 @@
|> fold add_instT_sorts instT
|> fold add_inst_sorts inst;
- val instT' = fold (add_instT thy') instT Term_Subst.TVars.empty;
- val inst' = fold (add_inst thy') inst Term_Subst.Vars.empty;
+ val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT);
+ val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst);
in ((instT', inst'), (cert', sorts')) end;
in
@@ -1752,7 +1756,7 @@
fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
val _ = null hyps orelse err "bad hyps";
val _ = null tpairs orelse err "bad flex-flex constraints";
- val tfrees = rev (Term.add_tfree_names prop []);
+ val tfrees = build_rev (Term.add_tfree_names prop);
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
@@ -1776,7 +1780,7 @@
(*Replace all TFrees not fixed or in the hyps by new TVars*)
fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
let
- val tfrees = fold Term.add_tfrees hyps fixed;
+ val tfrees = fold Term_Subst.add_tfrees hyps fixed;
val prop1 = attach_tpairs tpairs prop;
val (al, prop2) = Type.varify_global tfrees prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
@@ -1792,7 +1796,7 @@
prop = prop3}))
end;
-val varifyT_global = #2 o varifyT_global' [];
+val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty;
(*Replace all TVars by TFrees that are often new*)
fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
@@ -2093,7 +2097,7 @@
val add_vars =
full_prop_of #>
fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I);
- val vars = Vartab.empty |> add_vars th1 |> add_vars th2;
+ val vars = Vartab.build (add_vars th1 #> add_vars th2);
in SOME (Vartab.fold (unify_vars o #2) vars env) end
handle Pattern.Unif => NONE;
@@ -2257,7 +2261,7 @@
fun standard_tvars thm =
let
val thy = theory_of_thm thm;
- val tvars = rev (Term.add_tvars (prop_of thm) []);
+ val tvars = build_rev (Term.add_tvars (prop_of thm));
val names = Name.invent Name.context Name.aT (length tvars);
val tinst =
map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
@@ -2300,8 +2304,8 @@
(* type arities *)
fun thynames_of_arity thy (a, c) =
- (get_arities thy, []) |-> Aritytab.fold
- (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser))
+ build (get_arities thy |> Aritytab.fold
+ (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
|> sort (int_ord o apply2 #2) |> map #1;
fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
--- a/src/Pure/thm_deps.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/thm_deps.ML Tue Sep 07 10:17:03 2021 +0200
@@ -67,7 +67,7 @@
end;
in
fn thms =>
- (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, [])
+ (Inttab.build (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
|-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
end;
@@ -119,12 +119,13 @@
fun is_unused a = not (Symtab.defined used a);
(*groups containing at least one used theorem*)
- val used_groups = fold (fn (a, (_, _, group)) =>
- if is_unused a then I
- else
- (case group of
- NONE => I
- | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
+ val used_groups =
+ Inttab.build (new_thms |> fold (fn (a, (_, _, group)) =>
+ if is_unused a then I
+ else
+ (case group of
+ NONE => I
+ | SOME grp => Inttab.update (grp, ()))));
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
if not concealed andalso
--- a/src/Pure/type.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/type.ML Tue Sep 07 10:17:03 2021 +0200
@@ -61,7 +61,7 @@
val strip_sorts: typ -> typ
val strip_sorts_dummy: typ -> typ
val no_tvars: typ -> typ
- val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
+ val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
val legacy_freeze_type: typ -> typ
val legacy_freeze_thaw: term -> term * (term -> term)
@@ -355,8 +355,9 @@
fun varify_global fixed t =
let
- val fs = Term.fold_types (Term.fold_atyps
- (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+ val fs =
+ build (t |> (Term.fold_types o Term.fold_atyps)
+ (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
@@ -446,7 +447,7 @@
in match end;
fun typ_instance tsig (T, U) =
- (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+ (Vartab.build (typ_match tsig (U, T)); true) handle TYPE_MATCH => false;
(*purely structural matching*)
fun raw_match (TVar (v, S), T) subs =
@@ -474,7 +475,7 @@
fun raw_instance (T, U) =
if could_match (U, T) then
- (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+ (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false
else false;
--- a/src/Pure/variable.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/variable.ML Tue Sep 07 10:17:03 2021 +0200
@@ -74,11 +74,10 @@
(typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
val importT_terms: term list -> Proof.context -> term list * Proof.context
val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
- val importT: thm list -> Proof.context ->
- (((indexname * sort) * ctyp) list * thm list) * Proof.context
+ val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
val import: bool -> thm list -> Proof.context ->
- ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
+ ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
val import_vars: Proof.context -> thm -> thm
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -268,7 +267,7 @@
val declare_prf =
Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
-val declare_thm = Thm.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
(* renaming term/type frees *)
@@ -516,14 +515,14 @@
val still_fixed = not o is_newly_fixed inner outer;
val gen_fixes =
- Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y)
- (fixes_of inner) Symtab.empty;
+ Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
+ not (is_fixed outer y) ? Symtab.insert_set y));
val type_occs_inner = type_occs_of inner;
fun gen_fixesT ts =
- Symtab.fold (fn (a, xs) =>
+ Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
if declared_outer a orelse exists still_fixed xs
- then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty;
+ then I else Symtab.insert_set a));
in (gen_fixesT, gen_fixes) end;
fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -591,22 +590,22 @@
fun importT_inst ts ctxt =
let
- val tvars = rev (fold Term.add_tvars ts []);
+ val tvars = build_rev (fold Term.add_tvars ts);
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
val instT =
- fold2 (fn a => fn b => Term_Subst.TVars.add (a, TFree b))
- tvars tfrees Term_Subst.TVars.empty;
+ Term_Subst.TVars.build (fold2 (fn a => fn b =>
+ Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
in (instT, ctxt') end;
fun import_inst is_open ts ctxt =
let
val ren = Name.clean #> (if is_open then I else Name.internal);
val (instT, ctxt') = importT_inst ts ctxt;
- val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
+ val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
val inst =
- fold2 (fn (x, T) => fn y => Term_Subst.Vars.add ((x, T), Free (y, T)))
- vars ys Term_Subst.Vars.empty;
+ Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
+ Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
in ((instT, inst), ctxt'') end;
fun importT_terms ts ctxt =
@@ -620,8 +619,8 @@
fun importT ths ctxt =
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
- val ths' = map (Thm.instantiate (instT', [])) ths;
+ val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+ val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
@@ -633,9 +632,9 @@
fun import is_open ths ctxt =
let
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
- val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
- val ths' = map (Thm.instantiate (instT', inst')) ths;
+ val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+ val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
+ val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
in (((instT', inst'), ths'), ctxt') end;
fun import_vars ctxt th =
@@ -691,10 +690,10 @@
fun focus_subgoal bindings i st =
let
- val all_vars = Thm.fold_terms Term.add_vars st [];
+ val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
in
- fold (unbind_term o #1) all_vars #>
- fold (declare_constraints o Var) all_vars #>
+ Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
+ Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
focus_cterm bindings (Thm.cprem_of st i)
end;
@@ -733,8 +732,8 @@
val occs = type_occs_of ctxt;
val occs' = type_occs_of ctxt';
val types =
- Symtab.fold (fn (a, _) =>
- if Symtab.defined occs a then I else Symtab.insert_set a) occs' Symtab.empty;
+ Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
+ if Symtab.defined occs a then I else Symtab.insert_set a));
val idx = maxidx_of ctxt' + 1;
val Ts' = (fold o fold_types o fold_atyps)
(fn T as TFree _ =>
--- a/src/Tools/Code/code_printer.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/Code/code_printer.ML Tue Sep 07 10:17:03 2021 +0200
@@ -142,10 +142,9 @@
fun markup_stmt sym = with_presentation_marker
(Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
-fun filter_presentation [] tree =
- Buffer.empty
- |> fold XML.add_content tree
- | filter_presentation presentation_syms tree =
+fun filter_presentation [] xml =
+ Buffer.build (fold XML.add_content xml)
+ | filter_presentation presentation_syms xml =
let
val presentation_idents = map Code_Symbol.marker presentation_syms
fun is_selected (name, attrs) =
@@ -159,7 +158,7 @@
fun filter (XML.Elem (name_attrs, xs)) =
fold (if is_selected name_attrs then add_content_with_space else filter) xs
| filter (XML.Text _) = I;
- in snd (fold filter tree (true, Buffer.empty)) end;
+ in snd (fold filter xml (true, Buffer.empty)) end;
fun format presentation_names width =
with_presentation_marker (Pretty.string_of_margin width)
--- a/src/Tools/Haskell/Haskell.thy Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/Haskell/Haskell.thy Tue Sep 07 10:17:03 2021 +0200
@@ -572,11 +572,12 @@
See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
-}
-module Isabelle.Buffer (T, empty, add, content)
+module Isabelle.Buffer (T, empty, add, content, build, build_content)
where
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
+import Isabelle.Library
newtype T = Buffer [Bytes]
@@ -589,6 +590,12 @@
content :: T -> Bytes
content (Buffer bs) = Bytes.concat (reverse bs)
+
+build :: (T -> T) -> T
+build f = f empty
+
+build_content :: (T -> T) -> Bytes
+build_content f = build f |> content
\<close>
generate_file "Isabelle/Value.hs" = \<open>
@@ -1522,7 +1529,7 @@
Text s -> Buffer.add s
content_of :: Body -> Bytes
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
+content_of = Buffer.build_content . fold add_content
{- string representation -}
@@ -1540,7 +1547,7 @@
instance Show Tree where
show tree =
- Buffer.empty |> show_tree tree |> Buffer.content |> make_string
+ make_string $ Buffer.build_content (show_tree tree)
where
show_tree (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
@@ -1831,7 +1838,7 @@
buffer (XML.Text s) = Buffer.add s
string_of_body :: XML.Body -> Bytes
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
+string_of_body = Buffer.build_content . buffer_body
string_of :: XML.Tree -> Bytes
string_of = string_of_body . single
@@ -2049,7 +2056,7 @@
formatted = YXML.string_of_body . symbolic
unformatted :: T -> Bytes
-unformatted prt = Buffer.empty |> out prt |> Buffer.content
+unformatted = Buffer.build_content . out
where
out (Block markup _ _ prts) =
let (bg, en) = YXML.output_markup markup
--- a/src/Tools/IsaPlanner/rw_inst.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML Tue Sep 07 10:17:03 2021 +0200
@@ -236,7 +236,7 @@
|> Drule.implies_intr_list cprems
|> Drule.forall_intr_list frees_of_fixed_vars
|> Drule.forall_elim_list vars
- |> Thm.varifyT_global' othertfrees
+ |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
|-> K Drule.zero_var_indexes
end;
--- a/src/Tools/misc_legacy.ML Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/misc_legacy.ML Tue Sep 07 10:17:03 2021 +0200
@@ -5,6 +5,8 @@
signature MISC_LEGACY =
sig
+ val thm_frees: thm -> cterm list
+ val cterm_frees: cterm -> cterm list
val add_term_names: term * string list -> string list
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -24,6 +26,18 @@
structure Misc_Legacy: MISC_LEGACY =
struct
+fun thm_frees th =
+ (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+ (fn ct => fn (set, list) =>
+ let val v = Term.dest_Free (Thm.term_of ct) in
+ if not (Term_Subst.Frees.defined set v)
+ then (Term_Subst.Frees.add (v, ()) set, ct :: list)
+ else (set, list)
+ end)
+ |> #2;
+
+val cterm_frees = thm_frees o Drule.mk_term;
+
(*iterate a function over all types in a term*)
fun it_term_types f =
let fun iter(Const(_,T), a) = f(T,a)
@@ -235,7 +249,7 @@
fun freeze_thaw_robust ctxt th =
let val fth = Thm.legacy_freezeT th
in
- case Thm.fold_terms Term.add_vars fth [] of
+ case Thm.fold_terms {hyps = false} Term.add_vars fth [] of
[] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*)
| vars =>
let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))