--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sat Feb 17 11:11:28 2018 +0100
@@ -99,7 +99,7 @@
where "star_of x \<equiv> star_n (\<lambda>n. x)"
text \<open>Initialize transfer tactic.\<close>
-ML_file "transfer.ML"
+ML_file "transfer_principle.ML"
method_setup transfer =
\<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close>
--- a/src/HOL/Nonstandard_Analysis/transfer.ML Sat Feb 03 09:11:21 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-(* Title: HOL/Nonstandard_Analysis/transfer.ML
- Author: Brian Huffman
-
-Transfer principle tactic for nonstandard analysis.
-*)
-
-signature TRANSFER_PRINCIPLE =
-sig
- val transfer_tac: Proof.context -> thm list -> int -> tactic
- val add_const: string -> theory -> theory
-end;
-
-structure Transfer_Principle: TRANSFER_PRINCIPLE =
-struct
-
-structure Data = Generic_Data
-(
- type T = {
- intros: thm list,
- unfolds: thm list,
- refolds: thm list,
- consts: string list
- };
- val empty = {intros = [], unfolds = [], refolds = [], consts = []};
- val extend = I;
- fun merge
- ({intros = intros1, unfolds = unfolds1,
- refolds = refolds1, consts = consts1},
- {intros = intros2, unfolds = unfolds2,
- refolds = refolds2, consts = consts2}) : T =
- {intros = Thm.merge_thms (intros1, intros2),
- unfolds = Thm.merge_thms (unfolds1, unfolds2),
- refolds = Thm.merge_thms (refolds1, refolds2),
- consts = Library.merge (op =) (consts1, consts2)};
-);
-
-fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
- | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
- | unstar_typ T = T
-
-fun unstar_term consts term =
- let
- fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t)
- else (Const(a,unstar_typ T) $ unstar t)
- | unstar (f $ t) = unstar f $ unstar t
- | unstar (Const(a,T)) = Const(a,unstar_typ T)
- | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
- | unstar t = t
- in
- unstar term
- end
-
-local exception MATCH
-in
-fun transfer_star_tac ctxt =
- let
- fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
- | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
- | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
- | thm_of _ = raise MATCH;
-
- fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
- thm_of t
- | thm_of_goal _ = raise MATCH;
- in
- SUBGOAL (fn (t, i) =>
- resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
- handle MATCH => no_tac)
- end;
-end;
-
-fun transfer_thm_of ctxt ths t =
- let
- val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt);
- val meta = Local_Defs.meta_rewrite_rule ctxt;
- val ths' = map meta ths;
- val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
- val u = unstar_term consts t'
- val tac =
- rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
- ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
- match_tac ctxt [transitive_thm] 1 THEN
- resolve_tac ctxt [@{thm transfer_start}] 1 THEN
- REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
- match_tac ctxt [reflexive_thm] 1
- in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end;
-
-fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th =>
- let
- val tr = transfer_thm_of ctxt ths t
- val (_$ l $ r) = Thm.concl_of tr;
- val trs = if l aconv r then [] else [tr];
- in rewrite_goals_tac ctxt trs th end));
-
-local
-
-fun map_intros f = Data.map
- (fn {intros,unfolds,refolds,consts} =>
- {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
-
-fun map_unfolds f = Data.map
- (fn {intros,unfolds,refolds,consts} =>
- {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
-
-fun map_refolds f = Data.map
- (fn {intros,unfolds,refolds,consts} =>
- {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
-in
-
-val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
-val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
-
-val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
-val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
-
-val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
-val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
-
-end
-
-fun add_const c = Context.theory_map (Data.map
- (fn {intros,unfolds,refolds,consts} =>
- {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
-
-val _ =
- Theory.setup
- (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
- "declaration of transfer introduction rule" #>
- Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
- "declaration of transfer unfolding rule" #>
- Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
- "declaration of transfer refolding rule")
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML Sat Feb 17 11:11:28 2018 +0100
@@ -0,0 +1,135 @@
+(* Title: HOL/Nonstandard_Analysis/transfer_principle.ML
+ Author: Brian Huffman
+
+Transfer principle tactic for nonstandard analysis.
+*)
+
+signature TRANSFER_PRINCIPLE =
+sig
+ val transfer_tac: Proof.context -> thm list -> int -> tactic
+ val add_const: string -> theory -> theory
+end;
+
+structure Transfer_Principle: TRANSFER_PRINCIPLE =
+struct
+
+structure Data = Generic_Data
+(
+ type T = {
+ intros: thm list,
+ unfolds: thm list,
+ refolds: thm list,
+ consts: string list
+ };
+ val empty = {intros = [], unfolds = [], refolds = [], consts = []};
+ val extend = I;
+ fun merge
+ ({intros = intros1, unfolds = unfolds1,
+ refolds = refolds1, consts = consts1},
+ {intros = intros2, unfolds = unfolds2,
+ refolds = refolds2, consts = consts2}) : T =
+ {intros = Thm.merge_thms (intros1, intros2),
+ unfolds = Thm.merge_thms (unfolds1, unfolds2),
+ refolds = Thm.merge_thms (refolds1, refolds2),
+ consts = Library.merge (op =) (consts1, consts2)};
+);
+
+fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
+ | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
+ | unstar_typ T = T
+
+fun unstar_term consts term =
+ let
+ fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t)
+ else (Const(a,unstar_typ T) $ unstar t)
+ | unstar (f $ t) = unstar f $ unstar t
+ | unstar (Const(a,T)) = Const(a,unstar_typ T)
+ | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
+ | unstar t = t
+ in
+ unstar term
+ end
+
+local exception MATCH
+in
+fun transfer_star_tac ctxt =
+ let
+ fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
+ | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
+ | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
+ | thm_of _ = raise MATCH;
+
+ fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
+ thm_of t
+ | thm_of_goal _ = raise MATCH;
+ in
+ SUBGOAL (fn (t, i) =>
+ resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
+ handle MATCH => no_tac)
+ end;
+end;
+
+fun transfer_thm_of ctxt ths t =
+ let
+ val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt);
+ val meta = Local_Defs.meta_rewrite_rule ctxt;
+ val ths' = map meta ths;
+ val unfolds' = map meta unfolds and refolds' = map meta refolds;
+ val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
+ val u = unstar_term consts t'
+ val tac =
+ rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
+ ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
+ match_tac ctxt [transitive_thm] 1 THEN
+ resolve_tac ctxt [@{thm transfer_start}] 1 THEN
+ REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
+ match_tac ctxt [reflexive_thm] 1
+ in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end;
+
+fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th =>
+ let
+ val tr = transfer_thm_of ctxt ths t
+ val (_$ l $ r) = Thm.concl_of tr;
+ val trs = if l aconv r then [] else [tr];
+ in rewrite_goals_tac ctxt trs th end));
+
+local
+
+fun map_intros f = Data.map
+ (fn {intros,unfolds,refolds,consts} =>
+ {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
+
+fun map_unfolds f = Data.map
+ (fn {intros,unfolds,refolds,consts} =>
+ {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
+
+fun map_refolds f = Data.map
+ (fn {intros,unfolds,refolds,consts} =>
+ {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
+in
+
+val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm o Thm.trim_context);
+val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
+
+val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm o Thm.trim_context);
+val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
+
+val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm o Thm.trim_context);
+val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
+
+end
+
+fun add_const c = Context.theory_map (Data.map
+ (fn {intros,unfolds,refolds,consts} =>
+ {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
+
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+ "declaration of transfer introduction rule" #>
+ Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+ "declaration of transfer unfolding rule" #>
+ Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+ "declaration of transfer refolding rule")
+
+end;
--- a/src/HOL/Tools/Function/function.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Function/function.ML Sat Feb 17 11:11:28 2018 +0100
@@ -6,7 +6,7 @@
signature FUNCTION =
sig
- include FUNCTION_DATA
+ type info = Function_Common.info
val add_function: (binding * typ option * mixfix) list ->
Specification.multi_specs -> Function_Common.function_config ->
@@ -266,7 +266,7 @@
val get_congs = Function_Context_Tree.get_function_congs
-fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t
+fun get_info ctxt t = Function_Common.retrieve_function_data ctxt t
|> the_single |> snd
--- a/src/HOL/Tools/Function/function_common.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Function/function_common.ML Sat Feb 17 11:11:28 2018 +0100
@@ -4,7 +4,7 @@
Common definitions and other infrastructure for the function package.
*)
-signature FUNCTION_DATA =
+signature FUNCTION_COMMON =
sig
type info =
{is_partial : bool,
@@ -26,37 +26,6 @@
cases : thm list,
pelims: thm list list,
elims: thm list list option}
-end
-
-structure Function_Data : FUNCTION_DATA =
-struct
-
-type info =
- {is_partial : bool,
- defname : binding,
- (*contains no logical entities: invariant under morphisms:*)
- add_simps : (binding -> binding) -> string -> (binding -> binding) ->
- Token.src list -> thm list -> local_theory -> thm list * local_theory,
- fnames : binding list,
- case_names : string list,
- fs : term list,
- R : term,
- dom: term,
- psimps: thm list,
- pinducts: thm list,
- simps : thm list option,
- inducts : thm list option,
- termination : thm,
- totality : thm option,
- cases : thm list,
- pelims : thm list list,
- elims : thm list list option}
-
-end
-
-signature FUNCTION_COMMON =
-sig
- include FUNCTION_DATA
val profile : bool Unsynchronized.ref
val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
val mk_acc : typ -> term -> term
@@ -78,7 +47,7 @@
preproc
val termination_rule_tac : Proof.context -> int -> tactic
val store_termination_rule : thm -> Context.generic -> Context.generic
- val get_functions : Proof.context -> (term * info) Item_Net.T
+ val retrieve_function_data : Proof.context -> term -> (term * info) list
val add_function_data : info -> Context.generic -> Context.generic
val termination_prover_tac : bool -> Proof.context -> tactic
val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
@@ -107,9 +76,46 @@
structure Function_Common : FUNCTION_COMMON =
struct
-open Function_Data
+local open Function_Lib in
+
+(* info *)
-local open Function_Lib in
+type info =
+ {is_partial : bool,
+ defname : binding,
+ (*contains no logical entities: invariant under morphisms:*)
+ add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+ Token.src list -> thm list -> local_theory -> thm list * local_theory,
+ fnames : binding list,
+ case_names : string list,
+ fs : term list,
+ R : term,
+ dom: term,
+ psimps: thm list,
+ pinducts: thm list,
+ simps : thm list option,
+ inducts : thm list option,
+ termination : thm,
+ totality : thm option,
+ cases : thm list,
+ pelims : thm list list,
+ elims : thm list list option}
+
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+ simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
+ let
+ val term = Morphism.term phi
+ val thm = Morphism.thm phi
+ val fact = Morphism.fact phi
+ in
+ { add_simps = add_simps, case_names = case_names, fnames = fnames,
+ fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
+ pinducts = fact pinducts, simps = Option.map fact simps,
+ inducts = Option.map fact inducts, termination = thm termination,
+ totality = Option.map thm totality, defname = Morphism.binding phi defname,
+ is_partial = is_partial, cases = fact cases,
+ elims = Option.map (map fact) elims, pelims = map fact pelims }
+ end
(* profiling *)
@@ -267,9 +273,17 @@
val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
val get_functions = #2 o Data.get o Context.Proof
-fun add_function_data (info : info as {fs, termination, ...}) =
- (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
- #> store_termination_rule termination
+
+fun retrieve_function_data ctxt t =
+ Item_Net.retrieve (get_functions ctxt) t
+ |> (map o apsnd)
+ (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+
+val add_function_data =
+ transform_function_data Morphism.trim_context_morphism #>
+ (fn info as {fs, termination, ...} =>
+ (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
+ #> store_termination_rule termination)
fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
val set_termination_prover = Data.map o @{apply 4(3)} o K
@@ -292,22 +306,6 @@
termination : thm,
domintros : thm list option}
-fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
- let
- val term = Morphism.term phi
- val thm = Morphism.thm phi
- val fact = Morphism.fact phi
- in
- { add_simps = add_simps, case_names = case_names, fnames = fnames,
- fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
- pinducts = fact pinducts, simps = Option.map fact simps,
- inducts = Option.map fact inducts, termination = thm termination,
- totality = Option.map thm totality, defname = Morphism.binding phi defname,
- is_partial = is_partial, cases = fact cases,
- elims = Option.map (map fact) elims, pelims = map fact pelims }
- end
-
fun lift_morphism ctxt f =
let
fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
@@ -328,7 +326,7 @@
SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
handle Pattern.MATCH => NONE
in
- get_first match (Item_Net.retrieve (get_functions ctxt) t)
+ get_first match (retrieve_function_data ctxt t)
end
fun import_last_function ctxt =
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Feb 17 11:11:28 2018 +0100
@@ -61,11 +61,11 @@
val (_, prop') = Local_Defs.cert_def lthy (K []) prop
val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , def_thm)), lthy') =
+ val ((qconst, (_ , def)), lthy') =
Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
- (* data storage *)
- val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
+ fun qconst_data phi =
+ Quotient_Info.transform_quotconsts phi {qconst = qconst, rconst = rhs, def = def}
fun qualify defname suffix = Binding.name suffix
|> Binding.qualify true defname
@@ -76,14 +76,14 @@
val lthy'' = lthy'
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi =>
- (case Quotient_Info.transform_quotconsts phi qconst_data of
+ (case qconst_data phi of
qcinfo as {qconst = Const (c, _), ...} =>
Quotient_Info.update_quotconsts (c, qcinfo)
| _ => I))
|> (snd oo Local_Theory.note)
((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
- (qconst_data, lthy'')
+ (qconst_data Morphism.identity, lthy'')
end
fun mk_readable_rsp_thm_eq tm lthy =
--- a/src/HOL/Tools/Quotient/quotient_info.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Feb 17 11:11:28 2018 +0100
@@ -9,6 +9,7 @@
type quotmaps = {relmap: string, quot_thm: thm}
val lookup_quotmaps: Proof.context -> string -> quotmaps option
val lookup_quotmaps_global: theory -> string -> quotmaps option
+ val update_quotmaps: string * quotmaps -> Context.generic -> Context.generic
val print_quotmaps: Proof.context -> unit
type abs_rep = {abs : term, rep : term}
@@ -30,10 +31,10 @@
val transform_quotconsts: morphism -> quotconsts -> quotconsts
val lookup_quotconsts_global: theory -> term -> quotconsts option
val update_quotconsts: string * quotconsts -> Context.generic -> Context.generic
+ val dest_quotconsts: Proof.context -> quotconsts list
val dest_quotconsts_global: theory -> quotconsts list
- val dest_quotconsts: Proof.context -> quotconsts list
val print_quotconsts: Proof.context -> unit
-end;
+end
structure Quotient_Info: QUOTIENT_INFO =
struct
@@ -42,20 +43,23 @@
(*info about map- and rel-functions for a type*)
type quotmaps = {relmap: string, quot_thm: thm}
+fun transform_quotmaps phi : quotmaps -> quotmaps =
+ fn {relmap, quot_thm} => {relmap = relmap, quot_thm = Morphism.thm phi quot_thm}
(*info about abs/rep terms*)
type abs_rep = {abs : term, rep : term}
-fun transform_abs_rep phi {abs, rep} : abs_rep =
- {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+fun transform_abs_rep phi : abs_rep -> abs_rep =
+ fn {abs, rep} => {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
(*info about quotient types*)
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} : quotients =
- {qtyp = Morphism.typ phi qtyp,
- rtyp = Morphism.typ phi rtyp,
- equiv_rel = Morphism.term phi equiv_rel,
- equiv_thm = Morphism.thm phi equiv_thm,
- quot_thm = Morphism.thm phi quot_thm}
+fun transform_quotients phi : quotients -> quotients =
+ fn {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =>
+ {qtyp = Morphism.typ phi qtyp,
+ rtyp = Morphism.typ phi rtyp,
+ equiv_rel = Morphism.term phi equiv_rel,
+ equiv_thm = Morphism.thm phi equiv_thm,
+ quot_thm = Morphism.thm phi quot_thm}
(*info about quotient constants*)
(*We need to be able to lookup instances of lifted constants,
@@ -63,10 +67,11 @@
but overloaded constants share the same name.*)
type quotconsts = {qconst: term, rconst: term, def: thm}
fun eq_quotconsts (x: quotconsts, y: quotconsts) = #qconst x = #qconst y
-fun transform_quotconsts phi {qconst, rconst, def} : quotconsts =
- {qconst = Morphism.term phi qconst,
- rconst = Morphism.term phi rconst,
- def = Morphism.thm phi def}
+fun transform_quotconsts phi : quotconsts -> quotconsts =
+ fn {qconst, rconst, def} =>
+ {qconst = Morphism.term phi qconst,
+ rconst = Morphism.term phi rconst,
+ def = Morphism.thm phi def}
structure Data = Generic_Data
(
@@ -99,10 +104,15 @@
(* quotmaps *)
-val lookup_quotmaps = Symtab.lookup o get_quotmaps o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o get_quotmaps o Context.Theory
+fun lookup_quotmaps_generic context name =
+ Symtab.lookup (get_quotmaps context) name
+ |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
-(* FIXME export proper internal update operation!? *)
+val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
+val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
+
+val update_quotmaps =
+ map_quotmaps o Symtab.update o apsnd (transform_quotmaps Morphism.trim_context_morphism)
val _ =
Theory.setup
@@ -111,9 +121,9 @@
(Scan.lift @{keyword "("} |--
Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
Attrib.thm --| Scan.lift @{keyword ")"}) >>
- (fn (tyname, (relname, qthm)) =>
- let val minfo = {relmap = relname, quot_thm = qthm}
- in Thm.declaration_attribute (fn _ => map_quotmaps (Symtab.update (tyname, minfo))) end))
+ (fn (tyname, (relmap, quot_thm)) =>
+ Thm.declaration_attribute
+ (K (update_quotmaps (tyname, {relmap = relmap, quot_thm = quot_thm})))))
"declaration of map information")
fun print_quotmaps ctxt =
@@ -138,7 +148,8 @@
val lookup_abs_rep = Symtab.lookup o get_abs_rep o Context.Proof
val lookup_abs_rep_global = Symtab.lookup o get_abs_rep o Context.Theory
-val update_abs_rep = map_abs_rep o Symtab.update
+val update_abs_rep =
+ map_abs_rep o Symtab.update o apsnd (transform_abs_rep Morphism.trim_context_morphism)
fun print_abs_rep ctxt =
let
@@ -159,10 +170,15 @@
(* quotients *)
-val lookup_quotients = Symtab.lookup o get_quotients o Context.Proof
-val lookup_quotients_global = Symtab.lookup o get_quotients o Context.Theory
+fun lookup_quotients_generic context name =
+ Symtab.lookup (get_quotients context) name
+ |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
-val update_quotients = map_quotients o Symtab.update
+val lookup_quotients = lookup_quotients_generic o Context.Proof
+val lookup_quotients_global = lookup_quotients_generic o Context.Theory
+
+val update_quotients =
+ map_quotients o Symtab.update o apsnd (transform_quotients Morphism.trim_context_morphism)
fun dest_quotients ctxt =
map snd (Symtab.dest (get_quotients (Context.Proof ctxt)))
@@ -190,24 +206,25 @@
(* quotconsts *)
-val update_quotconsts = map_quotconsts o Symtab.cons_list
+val update_quotconsts =
+ map_quotconsts o Symtab.cons_list o apsnd (transform_quotconsts Morphism.trim_context_morphism)
-fun dest_quotconsts ctxt =
- maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt)))
+fun dest_quotconsts_generic context =
+ maps #2 (Symtab.dest (get_quotconsts context))
+ |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
-fun dest_quotconsts_global thy =
- maps snd (Symtab.dest (get_quotconsts (Context.Theory thy)))
+val dest_quotconsts = dest_quotconsts_generic o Context.Proof
+val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
fun lookup_quotconsts_global thy t =
let
val (name, qty) = dest_Const t
- fun matches (x: quotconsts) =
- let val (name', qty') = dest_Const (#qconst x);
- in name = name' andalso Sign.typ_instance thy (qty, qty') end
in
- (case Symtab.lookup (get_quotconsts (Context.Theory thy)) name of
- NONE => NONE
- | SOME l => find_first matches l)
+ Symtab.lookup_list (get_quotconsts (Context.Theory thy)) name
+ |> find_first (fn {qconst, ...} =>
+ let val (name', qty') = dest_Const qconst
+ in name = name' andalso Sign.typ_instance thy (qty, qty') end)
+ |> Option.map (transform_quotconsts (Morphism.transfer_morphism thy))
end
fun print_quotconsts ctxt =
@@ -220,7 +237,7 @@
Pretty.str "as",
Syntax.pretty_term ctxt (Thm.prop_of def)])
in
- map prt_qconst (maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt))))
+ map prt_qconst (dest_quotconsts ctxt)
|> Pretty.big_list "quotient constants:"
|> Pretty.writeln
end
@@ -240,4 +257,4 @@
Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
-end;
+end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Feb 17 11:11:28 2018 +0100
@@ -154,7 +154,6 @@
fun regularize_tac ctxt =
let
- val thy = Proof_Context.theory_of ctxt
val simpset =
mk_minimal_simpset ctxt
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Feb 17 11:11:28 2018 +0100
@@ -83,7 +83,7 @@
val thy = Proof_Context.theory_of ctxt
in
(case Quotient_Info.lookup_quotients_global thy s of
- SOME qdata => (#rtyp qdata, #qtyp qdata)
+ SOME {rtyp, qtyp, ...} => (rtyp, qtyp)
| NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
end
@@ -104,12 +104,9 @@
| mk_dummyT (Free (c, _)) = Free (c, dummyT)
| mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"
in
- case Quotient_Info.lookup_abs_rep ctxt qty_str of
- SOME abs_rep =>
- mk_dummyT (case flag of
- AbsF => #abs abs_rep
- | RepF => #rep abs_rep)
- | NONE => error ("No abs/rep terms for " ^ quote qty_str)
+ (case Quotient_Info.lookup_abs_rep ctxt qty_str of
+ SOME {abs, rep} => mk_dummyT (case flag of AbsF => abs | RepF => rep)
+ | NONE => error ("No abs/rep terms for " ^ quote qty_str))
end
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
@@ -273,14 +270,14 @@
fun mk_rel_compose (trm1, trm2) =
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
-fun get_relmap thy s =
- (case Quotient_Info.lookup_quotmaps thy s of
- SOME map_data => Const (#relmap map_data, dummyT)
+fun get_relmap ctxt s =
+ (case Quotient_Info.lookup_quotmaps ctxt s of
+ SOME {relmap, ...} => Const (relmap, dummyT)
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-fun get_equiv_rel thy s =
- (case Quotient_Info.lookup_quotients thy s of
- SOME qdata => #equiv_rel qdata
+fun get_equiv_rel ctxt s =
+ (case Quotient_Info.lookup_quotients ctxt s of
+ SOME {equiv_rel, ...} => equiv_rel
| NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
fun equiv_match_err ctxt ty_pat ty =
@@ -338,22 +335,14 @@
exception CODE_GEN of string
fun get_quot_thm ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- in
- (case Quotient_Info.lookup_quotients ctxt s of
- SOME qdata => Thm.transfer thy (#quot_thm qdata)
- | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
- end
+ (case Quotient_Info.lookup_quotients ctxt s of
+ SOME {quot_thm, ...} => quot_thm
+ | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."));
fun get_rel_quot_thm ctxt s =
- let
- val thy = Proof_Context.theory_of ctxt
- in
- (case Quotient_Info.lookup_quotmaps ctxt s of
- SOME map_data => Thm.transfer thy (#quot_thm map_data)
- | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
- end
+ (case Quotient_Info.lookup_quotmaps ctxt s of
+ SOME {quot_thm, ...} => quot_thm
+ | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"));
fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient3})
@@ -497,7 +486,7 @@
else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
else
(case Quotient_Info.lookup_quotients_global thy qs of
- SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+ SOME {rtyp, ...} => Sign.typ_instance thy (rT, rtyp)
| NONE => false)
| _ => false)
end
@@ -626,7 +615,7 @@
let
val rtrm' =
(case Quotient_Info.lookup_quotconsts_global thy qtrm of
- SOME qconst_info => #rconst qconst_info
+ SOME {rconst, ...} => rconst
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
in
if Pattern.matches thy (rtrm', rtrm)
@@ -858,5 +847,4 @@
fun derive_rtrm ctxt qtys qtrm =
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
-
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Feb 17 11:11:28 2018 +0100
@@ -141,17 +141,18 @@
val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm
val (qtyp, rtyp) = (dest_funT o fastype_of) rep
val qty_full_name = (fst o dest_Type) qtyp
- val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
- quot_thm = quot_thm }
- fun quot_info phi = Quotient_Info.transform_quotients phi quotients
- val abs_rep = {abs = abs, rep = rep}
- fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+ fun quotients phi =
+ Quotient_Info.transform_quotients phi
+ {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
+ quot_thm = quot_thm}
+ fun abs_rep phi =
+ Quotient_Info.transform_abs_rep phi {abs = abs, rep = rep}
in
lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi)
- #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi))
- |> setup_lifting_package quot_thm equiv_thm opt_par_thm
+ |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ Quotient_Info.update_quotients (qty_full_name, quotients phi) #>
+ Quotient_Info.update_abs_rep (qty_full_name, abs_rep phi))
+ |> setup_lifting_package quot_thm equiv_thm opt_par_thm
end
(* main function for constructing a quotient type *)
--- a/src/HOL/Tools/inductive.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/inductive.ML Sat Feb 17 11:11:28 2018 +0100
@@ -257,21 +257,26 @@
fun the_inductive ctxt term =
Item_Net.retrieve (#infos (rep_data ctxt)) term
|> the_single
+ |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
fun the_inductive_global ctxt name =
#infos (rep_data ctxt)
|> Item_Net.content
|> filter (fn ({names, ...}, _) => member op = names name)
|> the_single
+ |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
fun put_inductives info =
map_data (fn (infos, monos, equations) =>
- (Item_Net.update info infos, monos, equations));
+ (Item_Net.update (apsnd (transform_result Morphism.trim_context_morphism) info) infos,
+ monos, equations));
(* monotonicity rules *)
-val get_monos = #monos o rep_data;
+fun get_monos ctxt =
+ #monos (rep_data ctxt)
+ |> map (Thm.transfer (Proof_Context.theory_of ctxt));
fun mk_mono ctxt thm =
let
@@ -291,7 +296,8 @@
val mono_add =
Thm.declaration_attribute (fn thm => fn context =>
map_data (fn (infos, monos, equations) =>
- (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
+ (infos, Thm.add_thm (Thm.trim_context (mk_mono (Context.proof_of context) thm)) monos,
+ equations)) context);
val mono_del =
Thm.declaration_attribute (fn thm => fn context =>
@@ -306,12 +312,14 @@
(* equations *)
-val get_equations = #equations o rep_data;
+fun retrieve_equations ctxt =
+ Item_Net.retrieve (#equations (rep_data ctxt))
+ #> map (Thm.transfer (Proof_Context.theory_of ctxt));
val equation_add_permissive =
Thm.declaration_attribute (fn thm =>
map_data (fn (infos, monos, equations) =>
- (infos, monos, perhaps (try (Item_Net.update thm)) equations)));
+ (infos, monos, perhaps (try (Item_Net.update (Thm.trim_context thm))) equations)));
@@ -645,7 +653,7 @@
val ctxt' = Variable.auto_fixes prop ctxt;
val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
val substs =
- Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop)
+ retrieve_equations ctxt (HOLogic.dest_Trueprop prop)
|> map_filter
(fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
(Vartab.empty, Vartab.empty), eq)
--- a/src/HOL/Tools/inductive_set.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/inductive_set.ML Sat Feb 17 11:11:28 2018 +0100
@@ -285,9 +285,9 @@
warning ("Ignoring conversion rule for operator " ^ s')
else (); tab)
else
- {to_set_simps = thm :: to_set_simps,
+ {to_set_simps = Thm.trim_context thm :: to_set_simps,
to_pred_simps =
- mk_to_pred_eq ctxt h fs fs' T' thm :: to_pred_simps,
+ Thm.trim_context (mk_to_pred_eq ctxt h fs fs' T' thm) :: to_pred_simps,
set_arities = Symtab.insert_list op = (s',
(T', (map (AList.lookup op = fs) ts', fs'))) set_arities,
pred_arities = Symtab.insert_list op = (s,
@@ -347,7 +347,8 @@
thm |>
Thm.instantiate ([], insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
- [to_pred_simproc (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: to_pred_simps)]) |>
+ [to_pred_simproc
+ (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |>
eta_contract_thm ctxt (is_pred pred_arities) |>
Rule_Cases.save thm
end;
--- a/src/HOL/Tools/lin_arith.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/lin_arith.ML Sat Feb 17 11:11:28 2018 +0100
@@ -85,8 +85,12 @@
val get_arith_data = Lin_Arith_Data.get o Context.Proof;
+fun get_splits ctxt =
+ #splits (get_arith_data ctxt)
+ |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
- {splits = update Thm.eq_thm_prop thm splits,
+ {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,
inj_consts = inj_consts, discrete = discrete});
fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
@@ -418,7 +422,7 @@
(* where ti' = HOLogic.dest_Trueprop ti *)
fun REPEAT_DETERM_etac_rev_mp tms =
fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms) \<^term>\<open>False\<close>
- val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+ val split_thms = filter (is_split_thm ctxt) (get_splits ctxt)
val cmap = Splitter.cmap_of_split_thms split_thms
val goal_tm = REPEAT_DETERM_etac_rev_mp terms
val splits = Splitter.split_posns cmap thy Ts goal_tm
@@ -819,7 +823,7 @@
fun pre_tac ctxt i =
let
- val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+ val split_thms = filter (is_split_thm ctxt) (get_splits ctxt)
fun is_relevant t = is_some (decomp ctxt t)
in
DETERM (
@@ -940,7 +944,7 @@
(* split_limit may trigger. *)
(* Therefore splitting outside of simple_tac may allow us to prove *)
(* some goals that simple_tac alone would fail on. *)
- (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
+ (REPEAT_DETERM o split_tac ctxt (get_splits ctxt))
(Fast_Arith.lin_arith_tac ctxt);
in
--- a/src/Pure/Isar/attrib.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/attrib.ML Sat Feb 17 11:11:28 2018 +0100
@@ -29,6 +29,7 @@
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
type thms = (thm list * Token.src list) list
+ val trim_context: thms -> thms
val global_notes: string -> (Attrib.binding * thms) list ->
theory -> (string * thm list) list * theory
val local_notes: string -> (Attrib.binding * thms) list ->
@@ -181,6 +182,8 @@
type thms = (thm list * Token.src list) list;
+val trim_context: thms -> thms = (map o apfst o map) Thm.trim_context;
+
fun global_notes kind facts thy = thy |>
Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
--- a/src/Pure/Isar/bundle.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/bundle.ML Sat Feb 17 11:11:28 2018 +0100
@@ -55,9 +55,10 @@
val get_bundle = get_bundle_generic o Context.Proof;
fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
-fun define_bundle def context =
+fun define_bundle (b, bundle) context =
let
- val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+ val bundle' = Attrib.trim_context bundle;
+ val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context);
val context' = (Data.map o apfst o K) bundles' context;
in (name, context') end;
@@ -70,7 +71,7 @@
| NONE => error "Missing bundle target");
val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
-val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context;
fun augment_target thms =
Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
--- a/src/Pure/Isar/calculation.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/calculation.ML Sat Feb 17 11:11:28 2018 +0100
@@ -98,8 +98,11 @@
(* add/del rules *)
-val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
-val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
+val trans_add =
+ Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update o Thm.trim_context);
+
+val trans_del =
+ Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
val sym_add =
Thm.declaration_attribute (fn th =>
@@ -108,7 +111,7 @@
val sym_del =
Thm.declaration_attribute (fn th =>
- (Data.map o apfst o apsnd) (Thm.del_thm (Thm.trim_context th)) #>
+ (Data.map o apfst o apsnd) (Thm.del_thm th) #>
Thm.attribute_declaration Context_Rules.rule_del th);
--- a/src/Pure/Isar/class.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/class.ML Sat Feb 17 11:11:28 2018 +0100
@@ -87,10 +87,12 @@
Class_Data {consts = consts, base_sort = base_sort,
base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+
fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
of_class, axiom, defs, operations}) =
make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
(defs, operations)));
+
fun merge_class_data _ (Class_Data {consts = consts,
base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},
--- a/src/Pure/Isar/context_rules.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/context_rules.ML Sat Feb 17 11:11:28 2018 +0100
@@ -193,7 +193,7 @@
(* add and del rules *)
-val rule_del = Thm.declaration_attribute (fn th => Rules.map (del_rule th));
+val rule_del = Thm.declaration_attribute (Rules.map o del_rule);
fun rule_add k view opt_w =
Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th));
--- a/src/Pure/Isar/local_defs.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/local_defs.ML Sat Feb 17 11:11:28 2018 +0100
@@ -189,7 +189,7 @@
(map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
-val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
(* meta rewrite rules *)
--- a/src/Pure/ML/ml_heap.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/ML/ml_heap.ML Sat Feb 17 11:11:28 2018 +0100
@@ -7,6 +7,7 @@
signature ML_HEAP =
sig
val obj_size: 'a -> int
+ val full_gc: unit -> unit
val share_common_data: unit -> unit
val save_child: string -> unit
end;
@@ -16,6 +17,8 @@
val obj_size = PolyML.objSize;
+val full_gc = PolyML.fullGC;
+
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
fun save_child name =
--- a/src/Pure/axclass.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/axclass.ML Sat Feb 17 11:11:28 2018 +0100
@@ -152,7 +152,11 @@
fun get_info thy c =
(case Symtab.lookup (axclasses_of thy) c of
- SOME info => info
+ SOME {def, intro, axioms, params} =>
+ {def = Thm.transfer thy def,
+ intro = Thm.transfer thy intro,
+ axioms = map (Thm.transfer thy) axioms,
+ params = params}
| NONE => error ("No such axclass: " ^ quote c));
fun all_params_of thy S =
@@ -170,8 +174,6 @@
fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
-val update_classrel = map_proven_classrels o Symreltab.update;
-
val is_classrel = Symreltab.defined o proven_classrels_of;
fun the_classrel thy (c1, c2) =
@@ -189,10 +191,11 @@
else
(false,
thy2
- |> update_classrel ((c1, c2),
+ |> (map_proven_classrels o Symreltab.update) ((c1, c2),
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
|> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
- |> Thm.close_derivation));
+ |> Thm.close_derivation
+ |> Thm.trim_context));
val proven = is_classrel thy1;
val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
@@ -235,7 +238,8 @@
val th1 =
(th RS the_classrel thy (c, c1))
|> Thm.instantiate' std_vars []
- |> Thm.close_derivation;
+ |> Thm.close_derivation
+ |> Thm.trim_context;
in ((th1, thy_name), c1) end);
val finished' = finished andalso null completions;
@@ -243,7 +247,7 @@
in (finished', arities') end;
fun put_arity_completion ((t, Ss, c), th) thy =
- let val ar = ((c, Ss), (th, Context.theory_name thy)) in
+ let val ar = ((c, Ss), (Thm.trim_context th, Context.theory_name thy)) in
thy
|> map_proven_arities
(Symtab.insert_list (eq_fst op =) (t, ar) #>
@@ -274,12 +278,13 @@
fun get_inst_param thy (c, tyco) =
(case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
- SOME c' => c'
+ SOME (a, th) => (a, Thm.transfer thy th)
| NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
-fun add_inst_param (c, tyco) inst =
- (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
- #> (map_inst_params o apsnd) (Symtab.update_new (#1 inst, (c, tyco)));
+fun add_inst_param (c, tyco) (a, th) =
+ (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty))
+ (Symtab.update_new (tyco, (a, Thm.trim_context th)))
+ #> (map_inst_params o apsnd) (Symtab.update_new (a, (c, tyco)));
val inst_of_param = Symtab.lookup o #2 o inst_params_of;
val param_of_inst = #1 oo get_inst_param;
@@ -392,7 +397,8 @@
val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val th'' = th'
|> Thm.unconstrainT
- |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] []
+ |> Thm.trim_context;
in
thy'
|> Sign.primitive_classrel (c1, c2)
@@ -414,7 +420,7 @@
val args = Name.invent_names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
- val std_vars = map (fn (a, S) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
+ val std_vars = map (fn (a, _) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
val missing_params = Sign.complete_sort thy' [c]
|> maps (these o Option.map #params o try (get_info thy'))
@@ -450,7 +456,6 @@
let
val ctxt = Proof_Context.init_global thy;
val arity = Proof_Context.cert_arity ctxt raw_arity;
- val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
val ths =
Goal.prove_common ctxt NONE [] [] props
@@ -556,11 +561,14 @@
(* result *)
- val axclass = make_axclass (def, intro, axioms, params);
+ val axclass =
+ make_axclass
+ (Thm.trim_context def, Thm.trim_context intro, map Thm.trim_context axioms, params);
val result_thy =
facts_thy
|> map_proven_classrels
- (fold2 (fn c => fn th => Symreltab.update ((class, c), th)) super classrel)
+ (fold2 (fn c => fn th => Symreltab.update ((class, c), Thm.trim_context th))
+ super classrel)
|> perhaps complete_classrels
|> Sign.qualified_path false bconst
|> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
@@ -589,9 +597,6 @@
|-> fold (add o Drule.export_without_context o snd)
end;
-fun class_const c =
- (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
-
fun class_const_dep c =
((Defs.Const, Logic.const_of_class c), [Term.aT []]);
--- a/src/Pure/context.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/context.ML Sat Feb 17 11:11:28 2018 +0100
@@ -48,8 +48,11 @@
val proper_subthy: theory * theory -> bool
val subthy_id: theory_id * theory_id -> bool
val subthy: theory * theory -> bool
+ val trace_theories: bool Unsynchronized.ref
+ val theories_trace: unit -> {active: int, all: int}
+ val begin_thy: string -> theory list -> theory
val finish_thy: theory -> theory
- val begin_thy: string -> theory list -> theory
+ val theory_data_size: theory -> (Position.T * int) list
(*proof context*)
val raw_transfer: theory -> Proof.context -> Proof.context
(*certificate*)
@@ -125,7 +128,9 @@
datatype theory =
Theory of
- theory_id *
+ (*identity*)
+ {theory_id: theory_id,
+ token: unit Unsynchronized.ref} *
(*ancestry*)
{parents: theory list, (*immediate predecessors*)
ancestors: theory list} * (*all predecessors -- canonical reverse order*)
@@ -137,7 +142,8 @@
fun rep_theory_id (Theory_Id args) = args;
fun rep_theory (Theory args) = args;
-val theory_id = #1 o rep_theory;
+val theory_identity = #1 o rep_theory;
+val theory_id = #theory_id o theory_identity;
val identity_of_id = #1 o rep_theory_id;
val identity_of = identity_of_id o theory_id;
@@ -202,12 +208,12 @@
fun insert_id id ids = Inttab.update (id, ()) ids;
-fun merge_ids
- (Theory (Theory_Id ({id = id1, ids = ids1, ...}, _), _, _))
- (Theory (Theory_Id ({id = id2, ids = ids2, ...}, _), _, _)) =
- Inttab.merge (K true) (ids1, ids2)
- |> insert_id id1
- |> insert_id id2;
+val merge_ids =
+ apply2 theory_id #>
+ (fn (Theory_Id ({id = id1, ids = ids1, ...}, _), Theory_Id ({id = id2, ids = ids2, ...}, _)) =>
+ Inttab.merge (K true) (ids1, ids2)
+ |> insert_id id1
+ |> insert_id id2);
(* equality and inclusion *)
@@ -265,6 +271,7 @@
in
+fun invoke_pos k = invoke "" (K o #pos) k ();
fun invoke_empty k = invoke "" (K o #empty) k ();
val invoke_extend = invoke "extend" #extend;
fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
@@ -285,10 +292,44 @@
(** build theories **)
-(* primitives *)
+(* create theory *)
+
+val trace_theories = Unsynchronized.ref false;
+
+local
+
+val theories =
+ Synchronized.var "theory_tokens" ([]: unit Unsynchronized.ref option Unsynchronized.ref list);
+
+val dummy_token = Unsynchronized.ref ();
+
+fun make_token () =
+ if ! trace_theories then
+ let
+ val token = Unsynchronized.ref ();
+ val _ = Synchronized.change theories (cons (Weak.weak (SOME token)));
+ in token end
+ else dummy_token;
+
+in
+
+fun theories_trace () =
+ let
+ val trace = Synchronized.value theories;
+ val _ = ML_Heap.full_gc ();
+ val active = fold (fn Unsynchronized.ref NONE => I | _ => Integer.add 1) trace 0;
+ in {all = length trace, active = active} end;
fun create_thy ids history ancestry data =
- Theory (Theory_Id (make_identity (serial ()) ids, history), ancestry, data);
+ let
+ val theory_id = Theory_Id (make_identity (serial ()) ids, history);
+ val token = make_token ();
+ in Theory ({theory_id = theory_id, token = token}, ancestry, data) end;
+
+end;
+
+
+(* primitives *)
val pre_pure_thy =
create_thy Inttab.empty (make_history PureN 0) (make_ancestry [] []) Datatab.empty;
@@ -297,7 +338,8 @@
fun change_thy finish f thy =
let
- val Theory (Theory_Id ({id, ids}, {name, stage}), ancestry, data) = thy;
+ val Theory_Id ({id, ids}, {name, stage}) = theory_id thy;
+ val Theory (_, ancestry, data) = thy;
val (ancestry', data') =
if stage = finished then
(make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data)
@@ -320,12 +362,12 @@
local
-fun merge_thys (thy1, thy2) =
+fun merge_thys thys =
let
- val ids = merge_ids thy1 thy2;
+ val ids = merge_ids thys;
val history = make_history "" 0;
val ancestry = make_ancestry [] [];
- val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
+ val data = merge_data thys (apply2 data_of thys);
in create_thy ids history ancestry data end;
fun maximal_thys thys =
@@ -342,15 +384,16 @@
Library.foldl merge_ancestors ([], map ancestors_of parents)
|> fold extend_ancestors parents;
- val Theory (Theory_Id ({ids, ...}, _), _, data) =
+ val thy0 =
(case parents of
[] => error "Missing theory imports"
| [thy] => extend_thy thy
| thy :: thys => Library.foldl merge_thys (thy, thys));
+ val Theory_Id ({ids, ...}, _) = theory_id thy0;
val history = make_history name 0;
val ancestry = make_ancestry parents ancestors;
- in create_thy ids history ancestry data end;
+ in create_thy ids history ancestry (data_of thy0) end;
end;
@@ -369,8 +412,17 @@
fun put k mk x = update_thy (Datatab.update (k, mk x));
+fun obj_size k thy =
+ Datatab.lookup (data_of thy) k |> Option.map ML_Heap.obj_size;
+
end;
+fun theory_data_size thy =
+ (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))));
+
(*** proof context ***)
--- a/src/Tools/Code/code_runtime.ML Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Tools/Code/code_runtime.ML Sat Feb 17 11:11:28 2018 +0100
@@ -349,10 +349,12 @@
val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
in
thy
- |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms)
+ |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms)
end;
-fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt);
+fun get ctxt =
+ Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
+ |> map (Thm.transfer (Proof_Context.theory_of ctxt))
in