tuned locale interface
authorhaftmann
Fri Jul 10 07:59:29 2009 +0200 (2009-07-10)
changeset 31988801aabf9f376
parent 31987 f4c7be4d684f
child 31989 a290c36e94d6
tuned locale interface
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:28 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:29 2009 +0200
     1.3 @@ -242,16 +242,15 @@
     1.4      val diff_sort = Sign.complete_sort thy [sup]
     1.5        |> subtract (op =) (Sign.complete_sort thy [sub])
     1.6        |> filter (is_class thy);
     1.7 +    val deps_witss = case some_dep_morph
     1.8 +     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
     1.9 +      | NONE => []
    1.10    in
    1.11      thy
    1.12      |> AxClass.add_classrel classrel
    1.13      |> ClassData.map (Graph.add_edge (sub, sup))
    1.14      |> activate_defs sub (these_defs thy diff_sort)
    1.15 -    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
    1.16 -        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
    1.17 -          (the_list some_dep_morph)
    1.18 -    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    1.19 -        (Locale.get_registrations thy) thy)
    1.20 +    |> Locale.add_dependencies sub deps_witss export
    1.21    end;
    1.22  
    1.23  
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:28 2009 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:29 2009 +0200
     2.3 @@ -796,14 +796,9 @@
     2.4    let
     2.5      val target = intern thy raw_target;
     2.6      val target_ctxt = Locale.init target thy;
     2.7 -
     2.8      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     2.9 -
    2.10      fun after_qed witss = ProofContext.theory
    2.11 -      (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
    2.12 -        (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
    2.13 -      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    2.14 -        (Locale.get_registrations thy) thy));
    2.15 +      (Locale.add_dependencies target (deps ~~ witss) export);
    2.16    in Element.witness_proof after_qed propss goal_ctxt end;
    2.17  
    2.18  in
    2.19 @@ -860,7 +855,7 @@
    2.20            end;
    2.21  
    2.22      fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
    2.23 -        #-> (fn regs => store_eqns_activate regs eqs));
    2.24 +      #-> (fn regs => store_eqns_activate regs eqs));
    2.25  
    2.26    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    2.27  
     3.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:28 2009 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:29 2009 +0200
     3.3 @@ -45,7 +45,6 @@
     3.4    val instance_of: theory -> string -> morphism -> term list
     3.5    val specification_of: theory -> string -> term option * term list
     3.6    val declarations_of: theory -> string -> declaration list * declaration list
     3.7 -  val dependencies_of: theory -> string -> (string * morphism) list
     3.8  
     3.9    (* Storing results *)
    3.10    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    3.11 @@ -53,7 +52,6 @@
    3.12    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    3.13    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    3.14    val add_declaration: string -> declaration -> Proof.context -> Proof.context
    3.15 -  val add_dependency: string -> string * morphism -> theory -> theory
    3.16  
    3.17    (* Activation *)
    3.18    val activate_declarations: string * morphism -> Proof.context -> Proof.context
    3.19 @@ -69,10 +67,11 @@
    3.20    val unfold_add: attribute
    3.21    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    3.22  
    3.23 -  (* Registrations *)
    3.24 +  (* Registrations and dependencies *)
    3.25    val add_registration: string * (morphism * morphism) -> theory -> theory
    3.26    val amend_registration: morphism -> string * morphism -> theory -> theory
    3.27 -  val get_registrations: theory -> (string * morphism) list
    3.28 +  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
    3.29 +    morphism  -> theory -> theory
    3.30  
    3.31    (* Diagnostic *)
    3.32    val print_locales: theory -> unit
    3.33 @@ -338,13 +337,19 @@
    3.34      (* FIXME consolidate with dependencies, consider one data slot only *)
    3.35  );
    3.36  
    3.37 -val get_registrations =
    3.38 -  Registrations.get #> map (#1 #> apsnd op $>);
    3.39 +fun reg_morph ((name, (base, export)), _) = (name, base $> export);
    3.40 +
    3.41 +fun these_registrations thy name = Registrations.get thy
    3.42 +  |> filter (curry (op =) name o fst o fst)
    3.43 +  |> map reg_morph;
    3.44 +
    3.45 +fun all_registrations thy = Registrations.get thy
    3.46 +  |> map reg_morph;
    3.47  
    3.48  fun add_registration (name, (base_morph, export)) thy =
    3.49    roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
    3.50 -    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
    3.51 -    (* FIXME |-> put_global_idents ?*)
    3.52 +    (name, base_morph) (get_idents (Context.Theory thy), thy)
    3.53 +  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
    3.54  
    3.55  fun amend_registration morph (name, base_morph) thy =
    3.56    let
    3.57 @@ -364,6 +369,17 @@
    3.58    end;
    3.59  
    3.60  
    3.61 +(*** Dependencies ***)
    3.62 +
    3.63 +fun add_dependencies loc deps_witss export thy =
    3.64 +  thy
    3.65 +  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
    3.66 +      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
    3.67 +        deps_witss
    3.68 +  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
    3.69 +      (all_registrations thy) thy);
    3.70 +
    3.71 +
    3.72  (*** Storing results ***)
    3.73  
    3.74  (* Theorems *)
    3.75 @@ -375,12 +391,12 @@
    3.76        (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
    3.77          #>
    3.78        (* Registrations *)
    3.79 -      (fn thy => fold_rev (fn (name, morph) =>
    3.80 +      (fn thy => fold_rev (fn (_, morph) =>
    3.81              let
    3.82                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    3.83                  Attrib.map_facts (Attrib.attribute_i thy)
    3.84              in PureThy.note_thmss kind args'' #> snd end)
    3.85 -        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
    3.86 +        (these_registrations thy loc) thy))
    3.87    in ctxt'' end;
    3.88  
    3.89  
    3.90 @@ -404,11 +420,6 @@
    3.91  end;
    3.92  
    3.93  
    3.94 -(* Dependencies *)
    3.95 -
    3.96 -fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
    3.97 -
    3.98 -
    3.99  (*** Reasoning about locales ***)
   3.100  
   3.101  (* Storage for witnesses, intro and unfold rules *)