# HG changeset patch # User haftmann # Date 1138963677 -3600 # Node ID 77e18862990fee531276e6d0886757a5c8d7b9e3 # Parent fda5b8dbbef6b4bbe65a0d8e331b2fd1efb0ce7b refined signature of locale module diff -r fda5b8dbbef6 -r 77e18862990f src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Feb 03 08:48:33 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 03 11:47:57 2006 +0100 @@ -321,8 +321,8 @@ OuterSyntax.command "locale" "define named proof context" K.thy_decl ((P.opt_keyword "open" >> not) -- P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) - >> (Toplevel.theory_context o (fn ((x, y), (z, w)) => - Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (ctxt, thy))))); + >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) => + Locale.add_locale is_open name expr elems))); val opt_inst = Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []; diff -r fda5b8dbbef6 -r 77e18862990f src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Feb 03 08:48:33 2006 +0100 +++ b/src/Pure/Isar/locale.ML Fri Feb 03 11:47:57 2006 +0100 @@ -46,7 +46,7 @@ (* The specification of a locale *) val parameters_of: theory -> string -> - (string * typ option * mixfix) list + ((string * typ) * mixfix) list val local_asms_of: theory -> string -> ((string * Attrib.src list) * term list) list val global_asms_of: theory -> string -> @@ -70,14 +70,10 @@ val print_local_registrations: bool -> string -> Proof.context -> unit (* FIXME avoid duplicates *) - val add_locale_context: bool -> bstring -> expr -> Element.context list -> theory - -> ((Element.context_i list list * Element.context_i list list) - * Proof.context) * theory - val add_locale_context_i: bool -> bstring -> expr -> Element.context_i list -> theory - -> ((Element.context_i list list * Element.context_i list list) - * Proof.context) * theory - val add_locale: bool -> bstring -> expr -> Element.context list -> theory -> theory - val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory -> theory + val add_locale: bool -> bstring -> expr -> Element.context list -> theory + -> Proof.context * theory + val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory + -> Proof.context * theory (* Storing results *) val note_thmss: string -> xstring -> @@ -1273,8 +1269,7 @@ in fun parameters_of thy name = - the_locale thy name |> #params |> #1 - |> map (fn ((p, T), mix) => (p, SOME T, mix)); + the_locale thy name |> #params |> fst; fun local_asms_of thy name = gen_asms_of (single o Library.last_elem) thy name; @@ -1602,7 +1597,7 @@ (* CB: changes only "new" elems, these have identifier ("", _). *) -fun change_elemss axioms (import_elemss, body_elemss) = +fun change_elemss axioms elemss = let fun change (id as ("", _), es)= fold_map assumes_to_notes @@ -1610,11 +1605,7 @@ #-> (fn es' => pair (id, es')) | change e = pair e; in - axioms - |> map (conclude_protected o #2) - |> fold_map change import_elemss - ||>> fold_map change body_elemss - |> fst + fst (fold_map change elemss (map (conclude_protected o snd) axioms)) end; in @@ -1631,10 +1622,8 @@ val ((statement, intro, axioms), def_thy) = thy |> def_pred aname parms defs exts exts'; val elemss' = - elemss - |> change_elemss axioms - |> apsnd (fn elems => elems @ - [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])]); + change_elemss axioms elemss + @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])]; in def_thy |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])] @@ -1676,7 +1665,7 @@ val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text as (parms, ((_, exts'), _), _)) = prep_ctxt raw_import raw_body thy_ctxt; - val elemss = (import_elemss, body_elemss); + val elemss = import_elemss @ body_elemss; val import = prep_expr thy raw_import; val extraTs = foldr Term.add_term_tfrees [] exts' \\ @@ -1697,34 +1686,35 @@ |> snd; val pred_ctxt = ProofContext.init pred_thy; val (ctxt, (_, facts)) = activate_facts (K I) - (pred_ctxt, axiomify predicate_axioms ((op @) elemss')); + (pred_ctxt, axiomify predicate_axioms elemss'); val export = ProofContext.export_view predicate_statement ctxt thy_ctxt; val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); - val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) ((op @) elemss'))) + val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss')) in pred_thy |> PureThy.note_thmss_qualified "" bname facts' |> snd |> declare_locale name |> put_locale name {predicate = predicate, import = import, elems = map (fn e => (e, stamp ())) elems', - params = (params_of ((op @) elemss') |> + params = (params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)), regs = []} - |> pair ((fn (e1, e2) => (map snd e1, map snd e2)) elemss', body_ctxt) + |> pair (body_ctxt) end; in -val add_locale_context = gen_add_locale read_context intern_expr; -val add_locale_context_i = gen_add_locale cert_context (K I); -fun add_locale b = #2 oooo add_locale_context b; -fun add_locale_i b = #2 oooo add_locale_context_i b; +val add_locale = gen_add_locale read_context intern_expr; +val add_locale_i = gen_add_locale cert_context (K I); end; -val _ = Context.add_setup - (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> - add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]); +val _ = Context.add_setup ( + add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] + #> snd + #> add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] + #> snd +)