# HG changeset patch # User wenzelm # Date 1238341670 -7200 # Node ID 71f777103225e938207b0bb96fc2a63c59424df6 # Parent 5daee9354a9c6743ba1860938cc12d9416d27120 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned; diff -r 5daee9354a9c -r 71f777103225 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Mar 29 16:13:44 2009 +0200 +++ b/src/Pure/Isar/element.ML Sun Mar 29 17:47:50 2009 +0200 @@ -60,6 +60,7 @@ (Attrib.binding * (thm list * Attrib.src list) list) list val eq_morphism: theory -> thm list -> morphism val transfer_morphism: theory -> morphism + val init: context_i -> Context.generic -> Context.generic val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context val activate_i: context_i list -> Proof.context -> context_i list * Proof.context end; @@ -481,62 +482,62 @@ -(** activate in context, return elements and facts **) +(** activate in context **) -local +(* init *) -fun activate_elem (Fixes fixes) ctxt = - ctxt |> ProofContext.add_fixes fixes |> snd - | activate_elem (Constrains _) ctxt = - ctxt - | activate_elem (Assumes asms) ctxt = +fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2) + | init (Constrains _) = I + | init (Assumes asms) = Context.map_proof (fn ctxt => let val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; - val ts = maps (map #1 o #2) asms'; - val (_, ctxt') = - ctxt |> fold Variable.auto_fixes ts - |> ProofContext.add_assms_i Assumption.presume_export asms'; - in ctxt' end - | activate_elem (Defines defs) ctxt = + val (_, ctxt') = ctxt + |> fold Variable.auto_fixes (maps (map #1 o #2) asms') + |> ProofContext.add_assms_i Assumption.assume_export asms'; + in ctxt' end) + | init (Defines defs) = Context.map_proof (fn ctxt => let val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; val asms = defs' |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = LocalDefs.cert_def ctxt t + let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *) in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); - val (_, ctxt') = - ctxt |> fold (Variable.auto_fixes o #1) asms + val (_, ctxt') = ctxt + |> fold Variable.auto_fixes (map #1 asms) |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); - in ctxt' end - | activate_elem (Notes (kind, facts)) ctxt = + in ctxt' end) + | init (Notes (kind, facts)) = (fn context => let - val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; - val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts'; - in ctxt' end; + val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; + val context' = context |> Context.mapping + (PureThy.note_thmss kind facts' #> #2) + (ProofContext.note_thmss kind facts' #> #2); + in context' end); + + +(* activate *) + +local fun gen_activate prep_facts raw_elems ctxt = let - fun activate elem ctxt = - let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem - in (elem', activate_elem elem' ctxt) end + fun activate elem ctxt' = + let val elem' = map_ctxt_attrib Args.assignable (prep_facts ctxt' elem) + in (elem', Context.proof_map (init elem') ctxt') end; val (elems, ctxt') = fold_map activate raw_elems ctxt; in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end; -fun check_name name = - if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name) - else name; - -fun prep_facts prep_name get intern ctxt = +fun prep_facts ctxt = map_ctxt - {binding = Binding.map_name prep_name, + {binding = tap Name.of_binding, typ = I, term = I, pattern = I, - fact = get ctxt, - attrib = intern (ProofContext.theory_of ctxt)}; + fact = ProofContext.get_fact ctxt, + attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}; in -fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x; +fun activate x = gen_activate prep_facts x; fun activate_i x = gen_activate (K I) x; end; diff -r 5daee9354a9c -r 71f777103225 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Mar 29 16:13:44 2009 +0200 +++ b/src/Pure/Isar/locale.ML Sun Mar 29 17:47:50 2009 +0200 @@ -293,52 +293,20 @@ (** Public activation functions **) -local - -fun init_elem (Fixes fixes) (Context.Proof ctxt) = - Context.Proof (ProofContext.add_fixes fixes ctxt |> snd) - | init_elem (Assumes assms) (Context.Proof ctxt) = - let - val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms; - val ctxt' = ctxt - |> fold Variable.auto_fixes (maps (map fst o snd) assms') - |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd; - in Context.Proof ctxt' end - | init_elem (Defines defs) (Context.Proof ctxt) = - let - val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; - val ctxt' = ctxt - |> fold Variable.auto_fixes (map (fst o snd) defs') - |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') - |> snd; - in Context.Proof ctxt' end - | init_elem (Notes (kind, facts)) (Context.Proof ctxt) = - let - val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts - in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end - | init_elem (Notes (kind, facts)) (Context.Theory thy) = - let - val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts - in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end - | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory"; - -in - -fun activate_declarations dep ctxt = +fun activate_declarations dep = Context.proof_map (fn context => let - val context = Context.Proof ctxt; val thy = Context.theory_of context; val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents; - in Context.the_proof context' end; + in context' end); fun activate_facts dep context = let val thy = Context.theory_of context; - val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy; + val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy; in roundup thy activate dep (get_idents context, context) |-> put_idents end; fun init name thy = - activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of) + activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of; fun print_locale thy show_facts raw_name = @@ -355,8 +323,6 @@ |> Pretty.writeln end; -end; - (*** Registrations: interpretations in theories ***) @@ -398,7 +364,6 @@ end; - (*** Storing results ***) (* Theorems *)