diff -r 059c3568fdc8 -r abc6a2ea4b88 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Apr 02 13:33:48 2010 +0200 +++ b/src/Pure/Isar/locale.ML Wed Apr 07 19:17:10 2010 +0200 @@ -33,7 +33,7 @@ (string * sort) list * ((string * typ) * mixfix) list -> term option * term list -> thm option * thm option -> thm list -> - declaration list * declaration list -> + declaration list -> (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list -> (string * morphism) list -> theory -> theory val intern: theory -> xstring -> string @@ -44,14 +44,12 @@ val axioms_of: theory -> string -> thm list val instance_of: theory -> string -> morphism -> term list val specification_of: theory -> string -> term option * term list - val declarations_of: theory -> string -> declaration list * declaration list (* 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 + val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context (* Activation *) val activate_declarations: string * morphism -> Proof.context -> Proof.context @@ -97,26 +95,33 @@ intros: thm option * thm option, axioms: thm list, (** dynamic part **) +(* <<<<<<< local decls: (declaration * serial) list * (declaration * serial) list, (* type and term syntax declarations *) notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list, +======= *) + syntax_decls: (declaration * serial) list, + (* syntax declarations *) + notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list, +(* >>>>>>> other *) (* theorem declarations *) dependencies: ((string * morphism) * serial) list (* locale dependencies (sublocale relation) *) }; -fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) = +fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) = Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec, - decls = decls, notes = notes, dependencies = dependencies}; + syntax_decls = syntax_decls, notes = notes, dependencies = dependencies}; + +fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) = + mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies))); -fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) = - mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies))); - -fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2), - notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes', - dependencies = dependencies', ...}) = mk_locale +fun merge_locale + (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}, + Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) = + mk_locale ((parameters, spec, intros, axioms), - (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')), + ((merge (eq_snd op =) (syntax_decls, syntax_decls'), merge (eq_snd op =) (notes, notes')), merge (eq_snd op =) (dependencies, dependencies'))); @@ -139,12 +144,17 @@ SOME (Loc loc) => loc | NONE => error ("Unknown locale " ^ quote name)); -fun register_locale binding parameters spec intros axioms decls notes dependencies thy = +fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy = thy |> Locales.map (Name_Space.define true (Sign.naming_of thy) (binding, mk_locale ((parameters, spec, intros, axioms), +(* <<<<<<< local ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes), map (fn d => (d, serial ())) dependencies))) #> snd); +======= *) + ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes), + map (fn d => (d, serial ())) dependencies))) #> snd); +(* >>>>>>> other *) fun change_locale name = Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd; @@ -167,9 +177,6 @@ fun specification_of thy = #spec o the_locale thy; -fun declarations_of thy name = the_locale thy name |> - #decls |> pairself (map fst); - fun dependencies_of thy name = the_locale thy name |> #dependencies |> map fst; @@ -257,14 +264,13 @@ (* Declarations, facts and entire locale content *) -fun activate_decls (name, morph) context = +fun activate_syntax_decls (name, morph) context = let val thy = Context.theory_of context; - val {decls = (typ_decls, term_decls), ...} = the_locale thy name; + val {syntax_decls, ...} = the_locale thy name; in context - |> fold_rev (fn (decl, _) => decl morph) typ_decls - |> fold_rev (fn (decl, _) => decl morph) term_decls + |> fold_rev (fn (decl, _) => decl morph) syntax_decls end; fun activate_notes activ_elem transfer thy (name, morph) input = @@ -300,7 +306,10 @@ fun activate_declarations dep = Context.proof_map (fn context => let val thy = Context.theory_of context; - in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end); + in + roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context) + |-> put_idents + end); fun activate_facts dep context = let @@ -518,23 +527,24 @@ (* Declarations *) +(* <<<<<<< local local fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi)); fun add_decls add loc decl = ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #> +======= *) +fun add_declaration loc decl = +(* >>>>>>> other *) add_thmss loc "" - [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]), + [((Binding.conceal Binding.empty, + [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]), [([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; +fun add_syntax_declaration loc decl = + ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ()))) + #> add_declaration loc decl; (*** Reasoning about locales ***)