--- 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 ***)