Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
Local_Theory.target refers to bottom;
tuned signature;
--- a/src/Pure/Isar/class.ML Sun Apr 01 09:12:03 2012 +0200
+++ b/src/Pure/Isar/class.ML Sun Apr 01 14:29:22 2012 +0200
@@ -320,7 +320,7 @@
lthy
|> Local_Theory.raw_theory f
|> Local_Theory.map_contexts
- (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
+ (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class)));
fun target_const class ((c, mx), (type_params, dict)) thy =
let
@@ -484,7 +484,7 @@
Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.map_contexts synchronize_inst_syntax;
+ ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
(case instantiation_param lthy b of
--- a/src/Pure/Isar/generic_target.ML Sun Apr 01 09:12:03 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Apr 01 14:29:22 2012 +0200
@@ -191,7 +191,7 @@
fun standard_declaration decl =
background_declaration decl #>
- (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+ (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
--- a/src/Pure/Isar/local_theory.ML Sun Apr 01 09:12:03 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun Apr 01 14:29:22 2012 +0200
@@ -10,12 +10,12 @@
signature LOCAL_THEORY =
sig
type operations
- val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
val assert: local_theory -> local_theory
val level: Proof.context -> int
val assert_bottom: bool -> local_theory -> local_theory
val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
val close_target: local_theory -> local_theory
+ val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val naming_of: local_theory -> Name_Space.naming
val full_name: local_theory -> binding -> string
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
@@ -23,17 +23,16 @@
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
val restore_naming: local_theory -> local_theory -> local_theory
- val target_of: local_theory -> Proof.context
+ val standard_morphism: local_theory -> Proof.context -> morphism
+ val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val background_theory: (theory -> theory) -> local_theory -> local_theory
- val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
+ val target_of: local_theory -> Proof.context
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
+ val target_morphism: local_theory -> morphism
val propagate_ml_env: generic_theory -> generic_theory
- val standard_morphism: local_theory -> Proof.context -> morphism
- val target_morphism: local_theory -> morphism
- val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val operations_of: local_theory -> operations
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
@@ -98,21 +97,13 @@
fun init _ = [];
);
-fun map_contexts f =
- (Data.map o map) (fn {naming, operations, target} =>
- make_lthy (naming, operations,
- target
- |> Context_Position.set_visible false
- |> f
- |> Context_Position.restore_visible target))
- #> f;
-
fun assert lthy =
if null (Data.get lthy) then error "Missing local theory context" else lthy;
-val get_lthy = hd o Data.get o assert;
+val get_last_lthy = List.last o Data.get o assert;
+val get_first_lthy = hd o Data.get o assert;
-fun map_lthy f = assert #>
+fun map_first_lthy f = assert #>
Data.map (fn {naming, operations, target} :: parents =>
make_lthy (f (naming, operations, target)) :: parents);
@@ -137,13 +128,25 @@
fun close_target lthy =
assert_bottom false lthy |> Data.map tl;
+fun map_contexts f lthy =
+ let val n = level lthy in
+ lthy |> (Data.map o map_index) (fn (i, {naming, operations, target}) =>
+ make_lthy (naming, operations,
+ target
+ |> Context_Position.set_visible false
+ |> f (n - i - 1)
+ |> Context_Position.restore_visible target))
+ |> f n
+ end;
+
(* naming *)
-val naming_of = #naming o get_lthy;
+val naming_of = #naming o get_first_lthy;
val full_name = Name_Space.full_name o naming_of;
-fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
+fun map_naming f =
+ map_first_lthy (fn (naming, operations, target) => (f naming, operations, target));
val conceal = map_naming Name_Space.conceal;
val new_group = map_naming Name_Space.new_group;
@@ -152,19 +155,22 @@
val restore_naming = map_naming o K o naming_of;
-(* target *)
+(* standard morphisms *)
-val target_of = #target o get_lthy;
+fun standard_morphism lthy ctxt =
+ Proof_Context.norm_export_morphism lthy ctxt $>
+ Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
-fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
+fun standard_form lthy ctxt x =
+ Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
-(* substructure mappings *)
+(* background theory *)
fun raw_theory_result f lthy =
let
val (res, thy') = f (Proof_Context.theory_of lthy);
- val lthy' = map_contexts (Proof_Context.transfer thy') lthy;
+ val lthy' = map_contexts (K (Proof_Context.transfer thy')) lthy;
in (res, lthy') end;
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -181,47 +187,37 @@
fun background_theory f = #2 o background_theory_result (f #> pair ());
-fun target_result f lthy =
+
+(* target contexts *)
+
+val target_of = #target o get_last_lthy;
+
+fun target f lthy =
let
- val target = target_of lthy;
- val (res, ctxt') = target
+ val ctxt = target_of lthy;
+ val ctxt' = ctxt
|> Context_Position.set_visible false
|> f
- ||> Context_Position.restore_visible target;
+ |> Context_Position.restore_visible ctxt;
val thy' = Proof_Context.theory_of ctxt';
- val lthy' = lthy
- |> map_target (K ctxt')
- |> map_contexts (Proof_Context.transfer thy');
- in (res, lthy') end;
+ in map_contexts (fn 0 => K ctxt' | _ => Proof_Context.transfer thy') lthy end;
-fun target f = #2 o target_result (f #> pair ());
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
fun propagate_ml_env (context as Context.Proof lthy) =
let val inherit = ML_Env.inherit context in
lthy
|> background_theory (Context.theory_map inherit)
- |> map_contexts (Context.proof_map inherit)
+ |> map_contexts (K (Context.proof_map inherit))
|> Context.Proof
end
| propagate_ml_env context = context;
-(* morphisms *)
-
-fun standard_morphism lthy ctxt =
- Proof_Context.norm_export_morphism lthy ctxt $>
- Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
-
-fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-
-fun standard_form lthy ctxt x =
- Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
-
-
(** operations **)
-val operations_of = #operations o get_lthy;
+val operations_of = #operations o get_first_lthy;
(* primitives *)
@@ -286,7 +282,7 @@
|> checkpoint;
fun restore lthy =
- let val {naming, operations, target} = get_lthy lthy
+ let val {naming, operations, target} = get_first_lthy lthy
in init naming operations target end;
--- a/src/Pure/Isar/overloading.ML Sun Apr 01 09:12:03 2012 +0200
+++ b/src/Pure/Isar/overloading.ML Sun Apr 01 14:29:22 2012 +0200
@@ -155,7 +155,7 @@
(Thm.def_binding_optional (Binding.name v) b_def,
Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.map_contexts synchronize_syntax
+ ##> Local_Theory.map_contexts (K synchronize_syntax)
#-> (fn (_, def) => pair (Const (c, U), def));
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =