# HG changeset patch # User ballarin # Date 1226927019 -3600 # Node ID 249e394e5b8e758a3f7de3d95eddd265c46bf18d # Parent c8cc94a470d437004175310dd2a399dc28d2d24a Generic activation of locales. diff -r c8cc94a470d4 -r 249e394e5b8e src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Sun Nov 16 22:12:44 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Mon Nov 17 14:03:39 2008 +0100 @@ -25,7 +25,18 @@ val params_of: theory -> string -> (Name.binding * typ option * mixfix) list val declarations_of: theory -> string -> declaration list * declaration list; - (* Evaluate locales *) + (* Storing results *) +(* +val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> + Proof.context -> Proof.context +*) + val add_type_syntax: string -> declaration -> Proof.context -> Proof.context + val add_term_syntax: string -> declaration -> Proof.context -> Proof.context + val add_declaration: string -> declaration -> Proof.context -> Proof.context + + (* Activate locales *) + val activate_declarations: string -> theory -> Proof.context -> Proof.context + val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a val init: string -> theory -> Proof.context (* Diagnostic *) @@ -136,9 +147,9 @@ end; -(*** Target context ***) +(*** Activate context elements of locale ***) -(* round up locale dependencies in a depth-first fashion *) +(* Resolve locale dependencies in a depth-first fashion *) local @@ -172,63 +183,122 @@ end; -(* full context *) - -fun make_asms NONE = [] - | make_asms (SOME asm) = [((Name.no_binding, []), [(asm, [])])]; +fun activate_decls thy (name, morph) ctxt = + let + val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name; + in + ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |> + fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls + end; -fun make_defs [] = [] - | make_defs defs = [((Name.no_binding, []), map (fn def => (def, [])) defs)]; - -fun note_notes (name, morph) ctxt = +fun activate_declarations name thy ctxt = let - val thy = ProofContext.theory_of ctxt; - val Loc {notes, ...} = the_locale (ProofContext.theory_of ctxt) name; - fun activate ((kind, facts), _) ctxt = + val name' = intern thy name; + val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name'; + val dependencies' = + (name', Morphism.identity) :: roundup thy (map fst dependencies); + in + ctxt |> + not (null params) ? (ProofContext.add_fixes_i params #> snd) |> + (* FIXME type parameters *) + fold_rev (activate_decls thy) dependencies' + end; + +fun activate_notes activ_elem thy (name, morph) input = + let + val Loc {notes, ...} = the_locale thy name; + fun activate ((kind, facts), _) input = let - val facts' = facts |> Element.facts_map (Element.morph_ctxt morph) |> - Attrib.map_facts (Attrib.attribute_i thy); - in fold (fn args => Locale.local_note_prefix kind args #> snd) facts' ctxt end; + val facts' = facts |> Element.facts_map (Element.morph_ctxt morph) + in activ_elem (Notes (kind, facts')) input end; in - fold_rev activate notes ctxt + fold_rev activate notes input end; -fun init name thy = +fun activate name thy activ_elem input = let + val name' = intern thy name; val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} = - the_locale thy name; + the_locale thy name'; val dependencies' = - (intern thy name, Morphism.identity) :: roundup thy (map fst dependencies); + (name', Morphism.identity) :: roundup thy (map fst dependencies); in - thy |> ProofContext.init |> - ProofContext.add_fixes_i params |> snd |> + input |> + not (null params) ? activ_elem (Fixes params) |> (* FIXME type parameters *) - fold Variable.auto_fixes (the_list asm) |> - ProofContext.add_assms_i Assumption.assume_export (make_asms asm) |> snd |> - fold Variable.auto_fixes defs |> - ProofContext.add_assms_i LocalDefs.def_export (make_defs defs) |> snd |> - fold_rev note_notes dependencies' + is_some asm ? activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) |> + not (null defs) ? + activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs)) |> + fold_rev (activate_notes activ_elem thy) dependencies' end; +local + +fun init_elem (Fixes fixes) ctxt = ctxt |> + ProofContext.add_fixes_i fixes |> snd + | init_elem (Assumes assms) ctxt = + let + val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms + in + ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |> + ProofContext.add_assms_i Assumption.assume_export assms' |> snd + end + | init_elem (Defines defs) ctxt = + let + val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs + in + 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 + end + | init_elem (Notes (kind, facts)) ctxt = + let + val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts + in fold (fn args => Locale.local_note_prefix kind args #> snd) facts' ctxt end + +fun cons_elem false (Notes notes) elems = elems + | cons_elem _ elem elems = elem :: elems + +in + +fun init name thy = activate name thy init_elem (ProofContext.init thy); + fun print_locale thy show_facts name = - let - val Loc {parameters = (tparams, params), spec = (asm, defs), notes, ...} = - the_locale thy (intern thy name); - - val fixes = [Fixes params]; - val assumes = case asm of NONE => [] | - SOME spec => [Assumes [(Attrib.no_binding, [(spec, [])])]]; - val defines = case defs of [] => [] | - defs => [Defines (map (fn def => (Attrib.no_binding, (def, []))) defs)]; - val notes = if show_facts then map (Notes o fst) notes else []; - val ctxt = ProofContext.init thy; + let val ctxt = init name thy in Pretty.big_list "locale elements:" - (fixes @ assumes @ defines @ notes |> map (Element.pretty_ctxt ctxt) |> - map Pretty.chunks) |> Pretty.writeln - end; - + (activate name thy (cons_elem show_facts) [] |> rev |> + map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln + end end; +(*** Storing results ***) + +(* Declarations *) + +local + +fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi)); + +fun add_decls add loc decl = + ProofContext.theory (change_locale loc + (fn (parameters, spec, decls, notes, dependencies) => + (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) +(* + #> + add_thmss loc Thm.internalK + [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])]; +*) + +in + +val add_type_syntax = add_decls (apfst o cons); +val add_term_syntax = add_decls (apsnd o cons); +val add_declaration = add_decls (K I); + +end; + +end; +