src/Pure/Isar/locale.ML
changeset 35798 fd1bb29f8170
parent 33643 b275f26a638b
child 36096 abc6a2ea4b88
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Mar 15 15:13:22 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Mar 15 18:59:16 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4      (string * sort) list * ((string * typ) * mixfix) list ->
     1.5      term option * term list ->
     1.6      thm option * thm option -> thm list ->
     1.7 -    declaration list * declaration list ->
     1.8 +    declaration list ->
     1.9      (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
    1.10      (string * morphism) list -> theory -> theory
    1.11    val intern: theory -> xstring -> string
    1.12 @@ -44,14 +44,12 @@
    1.13    val axioms_of: theory -> string -> thm list
    1.14    val instance_of: theory -> string -> morphism -> term list
    1.15    val specification_of: theory -> string -> term option * term list
    1.16 -  val declarations_of: theory -> string -> declaration list * declaration list
    1.17  
    1.18    (* Storing results *)
    1.19    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.20      Proof.context -> Proof.context
    1.21 -  val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.22 -  val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.23    val add_declaration: string -> declaration -> Proof.context -> Proof.context
    1.24 +  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
    1.25  
    1.26    (* Activation *)
    1.27    val activate_declarations: string * morphism -> Proof.context -> Proof.context
    1.28 @@ -97,26 +95,27 @@
    1.29    intros: thm option * thm option,
    1.30    axioms: thm list,
    1.31    (** dynamic part **)
    1.32 -  decls: (declaration * stamp) list * (declaration * stamp) list,
    1.33 -    (* type and term syntax declarations *)
    1.34 +  syntax_decls: (declaration * stamp) list,
    1.35 +    (* syntax declarations *)
    1.36    notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
    1.37      (* theorem declarations *)
    1.38    dependencies: ((string * morphism) * stamp) list
    1.39      (* locale dependencies (sublocale relation) *)
    1.40  };
    1.41  
    1.42 -fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
    1.43 +fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
    1.44    Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
    1.45 -    decls = decls, notes = notes, dependencies = dependencies};
    1.46 +    syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
    1.47 +
    1.48 +fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
    1.49 +  mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
    1.50  
    1.51 -fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
    1.52 -  mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
    1.53 -
    1.54 -fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
    1.55 -  notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
    1.56 -    dependencies = dependencies', ...}) = mk_locale
    1.57 +fun merge_locale
    1.58 + (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
    1.59 +  Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
    1.60 +    mk_locale
    1.61        ((parameters, spec, intros, axioms),
    1.62 -        (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
    1.63 +        ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
    1.64            merge (eq_snd op =) (notes, notes')),
    1.65              merge (eq_snd op =) (dependencies, dependencies')));
    1.66  
    1.67 @@ -139,11 +138,11 @@
    1.68      SOME (Loc loc) => loc
    1.69    | NONE => error ("Unknown locale " ^ quote name));
    1.70  
    1.71 -fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
    1.72 +fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
    1.73    thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
    1.74      (binding,
    1.75        mk_locale ((parameters, spec, intros, axioms),
    1.76 -        ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
    1.77 +        ((map (fn decl => (decl, stamp ())) syntax_decls, map (fn n => (n, stamp ())) notes),
    1.78            map (fn d => (d, stamp ())) dependencies))) #> snd);
    1.79  
    1.80  fun change_locale name =
    1.81 @@ -167,9 +166,6 @@
    1.82  
    1.83  fun specification_of thy = #spec o the_locale thy;
    1.84  
    1.85 -fun declarations_of thy name = the_locale thy name |>
    1.86 -  #decls |> pairself (map fst);
    1.87 -
    1.88  fun dependencies_of thy name = the_locale thy name |>
    1.89    #dependencies |> map fst;
    1.90  
    1.91 @@ -257,14 +253,13 @@
    1.92  
    1.93  (* Declarations, facts and entire locale content *)
    1.94  
    1.95 -fun activate_decls (name, morph) context =
    1.96 +fun activate_syntax_decls (name, morph) context =
    1.97    let
    1.98      val thy = Context.theory_of context;
    1.99 -    val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   1.100 +    val {syntax_decls, ...} = the_locale thy name;
   1.101    in
   1.102      context
   1.103 -    |> fold_rev (fn (decl, _) => decl morph) typ_decls
   1.104 -    |> fold_rev (fn (decl, _) => decl morph) term_decls
   1.105 +    |> fold_rev (fn (decl, _) => decl morph) syntax_decls
   1.106    end;
   1.107  
   1.108  fun activate_notes activ_elem transfer thy (name, morph) input =
   1.109 @@ -300,7 +295,10 @@
   1.110  fun activate_declarations dep = Context.proof_map (fn context =>
   1.111    let
   1.112      val thy = Context.theory_of context;
   1.113 -  in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
   1.114 +  in
   1.115 +    roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
   1.116 +    |-> put_idents
   1.117 +  end);
   1.118  
   1.119  fun activate_facts dep context =
   1.120    let
   1.121 @@ -512,23 +510,15 @@
   1.122  
   1.123  (* Declarations *)
   1.124  
   1.125 -local
   1.126 -
   1.127 -fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   1.128 -
   1.129 -fun add_decls add loc decl =
   1.130 -  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   1.131 +fun add_declaration loc decl =
   1.132    add_thmss loc ""
   1.133 -    [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
   1.134 +    [((Binding.conceal Binding.empty,
   1.135 +        [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   1.136        [([Drule.dummy_thm], [])])];
   1.137  
   1.138 -in
   1.139 -
   1.140 -val add_type_syntax = add_decls (apfst o cons);
   1.141 -val add_term_syntax = add_decls (apsnd o cons);
   1.142 -val add_declaration = add_decls (K I);
   1.143 -
   1.144 -end;
   1.145 +fun add_syntax_declaration loc decl =
   1.146 +  ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, stamp ())))
   1.147 +  #> add_declaration loc decl;
   1.148  
   1.149  
   1.150  (*** Reasoning about locales ***)