src/Pure/Isar/locale.ML
changeset 31988 801aabf9f376
parent 30777 9960ff945c52
child 32074 76d6ba08a05f
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:28 2009 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:29 2009 +0200
     1.3 @@ -45,7 +45,6 @@
     1.4    val instance_of: theory -> string -> morphism -> term list
     1.5    val specification_of: theory -> string -> term option * term list
     1.6    val declarations_of: theory -> string -> declaration list * declaration list
     1.7 -  val dependencies_of: theory -> string -> (string * morphism) list
     1.8  
     1.9    (* Storing results *)
    1.10    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.11 @@ -53,7 +52,6 @@
    1.12    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.13    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.14    val add_declaration: string -> declaration -> Proof.context -> Proof.context
    1.15 -  val add_dependency: string -> string * morphism -> theory -> theory
    1.16  
    1.17    (* Activation *)
    1.18    val activate_declarations: string * morphism -> Proof.context -> Proof.context
    1.19 @@ -69,10 +67,11 @@
    1.20    val unfold_add: attribute
    1.21    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    1.22  
    1.23 -  (* Registrations *)
    1.24 +  (* Registrations and dependencies *)
    1.25    val add_registration: string * (morphism * morphism) -> theory -> theory
    1.26    val amend_registration: morphism -> string * morphism -> theory -> theory
    1.27 -  val get_registrations: theory -> (string * morphism) list
    1.28 +  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
    1.29 +    morphism  -> theory -> theory
    1.30  
    1.31    (* Diagnostic *)
    1.32    val print_locales: theory -> unit
    1.33 @@ -338,13 +337,19 @@
    1.34      (* FIXME consolidate with dependencies, consider one data slot only *)
    1.35  );
    1.36  
    1.37 -val get_registrations =
    1.38 -  Registrations.get #> map (#1 #> apsnd op $>);
    1.39 +fun reg_morph ((name, (base, export)), _) = (name, base $> export);
    1.40 +
    1.41 +fun these_registrations thy name = Registrations.get thy
    1.42 +  |> filter (curry (op =) name o fst o fst)
    1.43 +  |> map reg_morph;
    1.44 +
    1.45 +fun all_registrations thy = Registrations.get thy
    1.46 +  |> map reg_morph;
    1.47  
    1.48  fun add_registration (name, (base_morph, export)) thy =
    1.49    roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
    1.50 -    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
    1.51 -    (* FIXME |-> put_global_idents ?*)
    1.52 +    (name, base_morph) (get_idents (Context.Theory thy), thy)
    1.53 +  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
    1.54  
    1.55  fun amend_registration morph (name, base_morph) thy =
    1.56    let
    1.57 @@ -364,6 +369,17 @@
    1.58    end;
    1.59  
    1.60  
    1.61 +(*** Dependencies ***)
    1.62 +
    1.63 +fun add_dependencies loc deps_witss export thy =
    1.64 +  thy
    1.65 +  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
    1.66 +      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
    1.67 +        deps_witss
    1.68 +  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
    1.69 +      (all_registrations thy) thy);
    1.70 +
    1.71 +
    1.72  (*** Storing results ***)
    1.73  
    1.74  (* Theorems *)
    1.75 @@ -375,12 +391,12 @@
    1.76        (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
    1.77          #>
    1.78        (* Registrations *)
    1.79 -      (fn thy => fold_rev (fn (name, morph) =>
    1.80 +      (fn thy => fold_rev (fn (_, morph) =>
    1.81              let
    1.82                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    1.83                  Attrib.map_facts (Attrib.attribute_i thy)
    1.84              in PureThy.note_thmss kind args'' #> snd end)
    1.85 -        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
    1.86 +        (these_registrations thy loc) thy))
    1.87    in ctxt'' end;
    1.88  
    1.89  
    1.90 @@ -404,11 +420,6 @@
    1.91  end;
    1.92  
    1.93  
    1.94 -(* Dependencies *)
    1.95 -
    1.96 -fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
    1.97 -
    1.98 -
    1.99  (*** Reasoning about locales ***)
   1.100  
   1.101  (* Storage for witnesses, intro and unfold rules *)