register_locale: produce stamps at the spot where elements are registered;
authorwenzelm
Thu Mar 26 17:00:59 2009 +0100 (2009-03-26)
changeset 30725c23a5b3cd1b9
parent 30724 2e54e89bcce7
child 30726 67388cc4ccb4
register_locale: produce stamps at the spot where elements are registered;
tuned signature;
misc internal tuning and simplification;
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 26 15:20:50 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 26 17:00:59 2009 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4  
     1.5  fun parse_concl prep_term ctxt concl =
     1.6    (map o map) (fn (t, ps) =>
     1.7 -    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *)
     1.8 +    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t,
     1.9        map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
    1.10  
    1.11  
    1.12 @@ -288,13 +288,13 @@
    1.13  fun closeup _ _ false elem = elem
    1.14    | closeup ctxt parms true elem =
    1.15        let
    1.16 +        (* FIXME consider closing in syntactic phase -- before type checking *)
    1.17          fun close_frees t =
    1.18            let
    1.19              val rev_frees =
    1.20                Term.fold_aterms (fn Free (x, T) =>
    1.21                  if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
    1.22 -          in Term.list_all_free (rev rev_frees, t) end; (* FIXME use fold Logic.all *)
    1.23 -  (* FIXME consider closing in syntactic phase *)
    1.24 +          in fold (Logic.all o Free) rev_frees t end;
    1.25  
    1.26          fun no_binds [] = []
    1.27            | no_binds _ = error "Illegal term bindings in context element";
    1.28 @@ -325,9 +325,7 @@
    1.29    in (loc, morph) end;
    1.30  
    1.31  fun finish_elem ctxt parms do_close elem =
    1.32 -  let
    1.33 -    val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
    1.34 -  in elem' end
    1.35 +  finish_primitive parms (closeup ctxt parms do_close) elem;
    1.36  
    1.37  fun finish ctxt parms do_close insts elems =
    1.38    let
    1.39 @@ -363,7 +361,7 @@
    1.40          val inst''' = insts'' |> List.last |> snd |> snd;
    1.41          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
    1.42          val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
    1.43 -      in (i+1, insts', ctxt'') end;
    1.44 +      in (i + 1, insts', ctxt'') end;
    1.45  
    1.46      fun prep_elem insts raw_elem (elems, ctxt) =
    1.47        let
    1.48 @@ -564,9 +562,7 @@
    1.49    in text' end;
    1.50  
    1.51  fun eval_elem ctxt elem text =
    1.52 -  let
    1.53 -    val text' = eval_text ctxt true elem text;
    1.54 -  in text' end;
    1.55 +  eval_text ctxt true elem text;
    1.56  
    1.57  fun eval ctxt deps elems =
    1.58    let
    1.59 @@ -676,7 +672,7 @@
    1.60              thy'
    1.61              |> Sign.mandatory_path (Binding.name_of aname)
    1.62              |> PureThy.note_thmss Thm.internalK
    1.63 -              [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
    1.64 +              [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
    1.65              ||> Sign.restore_naming thy';
    1.66            in (SOME statement, SOME intro, axioms, thy'') end;
    1.67      val (b_pred, b_intro, b_axioms, thy'''') =
    1.68 @@ -690,7 +686,7 @@
    1.69              thy'''
    1.70              |> Sign.mandatory_path (Binding.name_of pname)
    1.71              |> PureThy.note_thmss Thm.internalK
    1.72 -                 [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
    1.73 +                 [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
    1.74                    ((Binding.name axiomsN, []),
    1.75                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
    1.76              ||> Sign.restore_naming thy''';
    1.77 @@ -712,7 +708,7 @@
    1.78  fun defines_to_notes thy (Defines defs) =
    1.79        Notes (Thm.definitionK, map (fn (a, (def, _)) =>
    1.80          (a, [([Assumption.assume (cterm_of thy def)],
    1.81 -          [(Attrib.internal o K) Locale.witness_attrib])])) defs)
    1.82 +          [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.83    | defines_to_notes _ e = e;
    1.84  
    1.85  fun gen_add_locale prep_decl
    1.86 @@ -745,11 +741,11 @@
    1.87      val asm = if is_some b_statement then b_statement else a_statement;
    1.88  
    1.89      val notes =
    1.90 -        if is_some asm
    1.91 -        then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
    1.92 -          [([Assumption.assume (cterm_of thy' (the asm))],
    1.93 -            [(Attrib.internal o K) Locale.witness_attrib])])])]
    1.94 -        else [];
    1.95 +      if is_some asm
    1.96 +      then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
    1.97 +        [([Assumption.assume (cterm_of thy' (the asm))],
    1.98 +          [(Attrib.internal o K) Locale.witness_add])])])]
    1.99 +      else [];
   1.100  
   1.101      val notes' = body_elems |>
   1.102        map (defines_to_notes thy') |>
   1.103 @@ -764,8 +760,7 @@
   1.104  
   1.105      val loc_ctxt = thy'
   1.106        |> Locale.register_locale bname (extraTs, params)
   1.107 -          (asm, rev defs) (a_intro, b_intro) axioms ([], [])
   1.108 -          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
   1.109 +          (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
   1.110        |> TheoryTarget.init (SOME name)
   1.111        |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
   1.112  
   1.113 @@ -792,11 +787,11 @@
   1.114  
   1.115      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
   1.116  
   1.117 -    fun after_qed witss = ProofContext.theory (
   1.118 -      fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
   1.119 +    fun after_qed witss = ProofContext.theory
   1.120 +      (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
   1.121          (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
   1.122        (fn thy => fold_rev Locale.activate_global_facts
   1.123 -          (Locale.get_registrations thy) thy));
   1.124 +        (Locale.get_registrations thy) thy));
   1.125    in Element.witness_proof after_qed propss goal_ctxt end;
   1.126  
   1.127  in
     2.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 26 15:20:50 2009 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 26 17:00:59 2009 +0100
     2.3 @@ -1,8 +1,7 @@
     2.4  (*  Title:      Pure/Isar/locale.ML
     2.5      Author:     Clemens Ballarin, TU Muenchen
     2.6  
     2.7 -Locales -- Isar proof contexts as meta-level predicates, with local
     2.8 -syntax and implicit structures.
     2.9 +Locales -- managed Isar proof contexts, based on Pure predicates.
    2.10  
    2.11  Draws basic ideas from Florian Kammueller's original version of
    2.12  locales, but uses the richer infrastructure of Isar instead of the raw
    2.13 @@ -34,9 +33,9 @@
    2.14      (string * sort) list * (binding * typ option * mixfix) list ->
    2.15      term option * term list ->
    2.16      thm option * thm option -> thm list ->
    2.17 -    (declaration * stamp) list * (declaration * stamp) list ->
    2.18 -    ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    2.19 -    ((string * morphism) * stamp) list -> theory -> theory
    2.20 +    declaration list * declaration list ->
    2.21 +    (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
    2.22 +    (string * morphism) list -> theory -> theory
    2.23    val intern: theory -> xstring -> string
    2.24    val extern: theory -> string -> xstring
    2.25    val defined: theory -> string -> bool
    2.26 @@ -64,16 +63,17 @@
    2.27    val init: string -> theory -> Proof.context
    2.28  
    2.29    (* Reasoning about locales *)
    2.30 -  val witness_attrib: attribute
    2.31 -  val intro_attrib: attribute
    2.32 -  val unfold_attrib: attribute
    2.33 +  val get_witnesses: Proof.context -> thm list
    2.34 +  val get_intros: Proof.context -> thm list
    2.35 +  val get_unfolds: Proof.context -> thm list
    2.36 +  val witness_add: attribute
    2.37 +  val intro_add: attribute
    2.38 +  val unfold_add: attribute
    2.39    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    2.40  
    2.41    (* Registrations *)
    2.42 -  val add_registration: string * (morphism * morphism) ->
    2.43 -    theory -> theory
    2.44 -  val amend_registration: morphism -> string * morphism ->
    2.45 -    theory -> theory
    2.46 +  val add_registration: string * (morphism * morphism) -> theory -> theory
    2.47 +  val amend_registration: morphism -> string * morphism -> theory -> theory
    2.48    val get_registrations: theory -> (string * morphism) list
    2.49  
    2.50    (* Diagnostic *)
    2.51 @@ -81,27 +81,6 @@
    2.52    val print_locale: theory -> bool -> xstring -> unit
    2.53  end;
    2.54  
    2.55 -
    2.56 -(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
    2.57 -
    2.58 -(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
    2.59 -functor ThmsFun() =
    2.60 -struct
    2.61 -
    2.62 -structure Data = GenericDataFun
    2.63 -(
    2.64 -  type T = thm list;
    2.65 -  val empty = [];
    2.66 -  val extend = I;
    2.67 -  fun merge _ = Thm.merge_thms;
    2.68 -);
    2.69 -
    2.70 -val get = Data.get o Context.Proof;
    2.71 -val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
    2.72 -
    2.73 -end;
    2.74 -
    2.75 -
    2.76  structure Locale: LOCALE =
    2.77  struct
    2.78  
    2.79 @@ -140,7 +119,7 @@
    2.80            merge (eq_snd op =) (notes, notes')),
    2.81              merge (eq_snd op =) (dependencies, dependencies')));
    2.82  
    2.83 -structure LocalesData = TheoryDataFun
    2.84 +structure Locales = TheoryDataFun
    2.85  (
    2.86    type T = locale NameSpace.table;
    2.87    val empty = NameSpace.empty_table;
    2.88 @@ -149,26 +128,29 @@
    2.89    fun merge _ = NameSpace.join_tables (K merge_locale);
    2.90  );
    2.91  
    2.92 -val intern = NameSpace.intern o #1 o LocalesData.get;
    2.93 -val extern = NameSpace.extern o #1 o LocalesData.get;
    2.94 -
    2.95 -fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
    2.96 +val intern = NameSpace.intern o #1 o Locales.get;
    2.97 +val extern = NameSpace.extern o #1 o Locales.get;
    2.98  
    2.99 -fun defined thy = is_some o get_locale thy;
   2.100 +val get_locale = Symtab.lookup o #2 o Locales.get;
   2.101 +val defined = Symtab.defined o #2 o Locales.get;
   2.102  
   2.103 -fun the_locale thy name = case get_locale thy name
   2.104 - of SOME (Loc loc) => loc
   2.105 -  | NONE => error ("Unknown locale " ^ quote name);
   2.106 +fun the_locale thy name =
   2.107 +  (case get_locale thy name of
   2.108 +    SOME (Loc loc) => loc
   2.109 +  | NONE => error ("Unknown locale " ^ quote name));
   2.110  
   2.111  fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
   2.112 -  thy |> LocalesData.map (NameSpace.define (Sign.naming_of thy) (binding,
   2.113 -    mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
   2.114 +  thy |> Locales.map (NameSpace.define (Sign.naming_of thy)
   2.115 +    (binding,
   2.116 +      mk_locale ((parameters, spec, intros, axioms),
   2.117 +        ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
   2.118 +          map (fn d => (d, stamp ())) dependencies))) #> snd);
   2.119  
   2.120  fun change_locale name =
   2.121 -  LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   2.122 +  Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
   2.123  
   2.124  fun print_locales thy =
   2.125 -  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
   2.126 +  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
   2.127    |> Pretty.writeln;
   2.128  
   2.129  
   2.130 @@ -181,12 +163,12 @@
   2.131  fun axioms_of thy = #axioms o the_locale thy;
   2.132  
   2.133  fun instance_of thy name morph = params_of thy name |>
   2.134 -  map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
   2.135 +  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
   2.136  
   2.137  fun specification_of thy = #spec o the_locale thy;
   2.138  
   2.139  fun declarations_of thy name = the_locale thy name |>
   2.140 -  #decls |> apfst (map fst) |> apsnd (map fst);
   2.141 +  #decls |> pairself (map fst);
   2.142  
   2.143  fun dependencies_of thy name = the_locale thy name |>
   2.144    #dependencies |> map fst;
   2.145 @@ -206,7 +188,7 @@
   2.146  
   2.147  datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
   2.148  
   2.149 -structure IdentifiersData = GenericDataFun
   2.150 +structure Identifiers = GenericDataFun
   2.151  (
   2.152    type T = identifiers delayed;
   2.153    val empty = Ready empty;
   2.154 @@ -220,18 +202,17 @@
   2.155    | finish _ (Ready ids) = ids;
   2.156  
   2.157  val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
   2.158 -  (case IdentifiersData.get (Context.Theory thy) of
   2.159 -    Ready _ => NONE |
   2.160 -    ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
   2.161 -  )));
   2.162 +  (case Identifiers.get (Context.Theory thy) of
   2.163 +    Ready _ => NONE
   2.164 +  | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
   2.165  
   2.166  fun get_global_idents thy =
   2.167 -  let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
   2.168 -val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
   2.169 +  let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
   2.170 +val put_global_idents = Context.theory_map o Identifiers.put o Ready;
   2.171  
   2.172  fun get_local_idents ctxt =
   2.173 -  let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
   2.174 -val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
   2.175 +  let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
   2.176 +val put_local_idents = Context.proof_map o Identifiers.put o Ready;
   2.177  
   2.178  end;
   2.179  
   2.180 @@ -385,7 +366,7 @@
   2.181  
   2.182  (*** Registrations: interpretations in theories ***)
   2.183  
   2.184 -structure RegistrationsData = TheoryDataFun
   2.185 +structure Registrations = TheoryDataFun
   2.186  (
   2.187    type T = ((string * (morphism * morphism)) * stamp) list;
   2.188      (* FIXME mixins need to be stamped *)
   2.189 @@ -398,17 +379,17 @@
   2.190  );
   2.191  
   2.192  val get_registrations =
   2.193 -  RegistrationsData.get #> map fst #> map (apsnd op $>);
   2.194 +  Registrations.get #> map fst #> map (apsnd op $>);
   2.195  
   2.196  fun add_registration (name, (base_morph, export)) thy =
   2.197    roundup thy (fn _ => fn (name', morph') =>
   2.198 -    (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
   2.199 +    (Registrations.map o cons) ((name', (morph', export)), stamp ()))
   2.200      (name, base_morph) (get_global_idents thy, thy) |> snd
   2.201      (* FIXME |-> put_global_idents ?*);
   2.202  
   2.203  fun amend_registration morph (name, base_morph) thy =
   2.204    let
   2.205 -    val regs = (RegistrationsData.get #> map fst) thy;
   2.206 +    val regs = (Registrations.get #> map fst) thy;
   2.207      val base = instance_of thy name base_morph;
   2.208      fun match (name', (morph', _)) =
   2.209        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   2.210 @@ -418,7 +399,7 @@
   2.211          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   2.212        else ();
   2.213    in
   2.214 -    RegistrationsData.map (nth_map (length regs - 1 - i)
   2.215 +    Registrations.map (nth_map (length regs - 1 - i)
   2.216        (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   2.217    end;
   2.218  
   2.219 @@ -463,6 +444,7 @@
   2.220  
   2.221  end;
   2.222  
   2.223 +
   2.224  (* Dependencies *)
   2.225  
   2.226  fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   2.227 @@ -470,21 +452,36 @@
   2.228  
   2.229  (*** Reasoning about locales ***)
   2.230  
   2.231 -(** Storage for witnesses, intro and unfold rules **)
   2.232 +(* Storage for witnesses, intro and unfold rules *)
   2.233  
   2.234 -structure Witnesses = ThmsFun();
   2.235 -structure Intros = ThmsFun();
   2.236 -structure Unfolds = ThmsFun();
   2.237 +structure Thms = GenericDataFun
   2.238 +(
   2.239 +  type T = thm list * thm list * thm list;
   2.240 +  val empty = ([], [], []);
   2.241 +  val extend = I;
   2.242 +  fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   2.243 +   (Thm.merge_thms (witnesses1, witnesses2),
   2.244 +    Thm.merge_thms (intros1, intros2),
   2.245 +    Thm.merge_thms (unfolds1, unfolds2));
   2.246 +);
   2.247  
   2.248 -val witness_attrib = Witnesses.add;
   2.249 -val intro_attrib = Intros.add;
   2.250 -val unfold_attrib = Unfolds.add;
   2.251 +val get_witnesses = #1 o Thms.get o Context.Proof;
   2.252 +val get_intros = #2 o Thms.get o Context.Proof;
   2.253 +val get_unfolds = #3 o Thms.get o Context.Proof;
   2.254  
   2.255 -(** Tactic **)
   2.256 +val witness_add =
   2.257 +  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
   2.258 +val intro_add =
   2.259 +  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
   2.260 +val unfold_add =
   2.261 +  Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   2.262  
   2.263 -fun intro_locales_tac eager ctxt facts st =
   2.264 +
   2.265 +(* Tactic *)
   2.266 +
   2.267 +fun intro_locales_tac eager ctxt =
   2.268    Method.intros_tac
   2.269 -    (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
   2.270 +    (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
   2.271  
   2.272  val _ = Context.>> (Context.map_theory
   2.273   (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))