# HG changeset patch # User haftmann # Date 1247674808 -7200 # Node ID 76d6ba08a05f7cff95191b1aac5be092f3863167 # Parent 0a83608e21f11435d29da98e3bbe9d5205383daa simplification of locale interfaces diff -r 0a83608e21f1 -r 76d6ba08a05f src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Wed Jul 15 10:11:13 2009 +0200 +++ b/src/Pure/Isar/class_target.ML Wed Jul 15 18:20:08 2009 +0200 @@ -242,15 +242,16 @@ val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]) |> filter (is_class thy); - val deps_witss = case some_dep_morph - of SOME dep_morph => [((sup, dep_morph), the_list some_wit)] - | NONE => [] + val add_dependency = case some_dep_morph + of SOME dep_morph => Locale.add_dependency sub + (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export + | NONE => I in thy |> AxClass.add_classrel classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) - |> Locale.add_dependencies sub deps_witss export + |> add_dependency end; diff -r 0a83608e21f1 -r 76d6ba08a05f src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Jul 15 10:11:13 2009 +0200 +++ b/src/Pure/Isar/expression.ML Wed Jul 15 18:20:08 2009 +0200 @@ -788,27 +788,6 @@ (*** Interpretation ***) -(** Interpretation between locales: declaring sublocale relationships **) - -local - -fun gen_sublocale prep_expr intern raw_target expression thy = - let - val target = intern thy raw_target; - val target_ctxt = Locale.init target thy; - val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; - fun after_qed witss = ProofContext.theory - (Locale.add_dependencies target (deps ~~ witss) export); - in Element.witness_proof after_qed propss goal_ctxt end; - -in - -fun sublocale x = gen_sublocale cert_goal_expression (K I) x; -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x; - -end; - - (** Interpretation in theories **) local @@ -816,46 +795,31 @@ fun gen_interpretation prep_expr parse_prop prep_attr expression equations theory = let - val ((propss, regs, export), expr_ctxt) = ProofContext.init theory + val ((propss, deps, export), expr_ctxt) = ProofContext.init theory |> prep_expr expression; val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; - val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations; + val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - fun store_reg ((name, morph), wits) thy = + fun note_eqns raw_eqns thy = let - val wits' = map (Element.morph_witness export') wits; - val morph' = morph $> Element.satisfy_morphism wits'; + val eqns = map (Morphism.thm (export' $> export)) raw_eqns; + val eqn_attrss = map2 (fn attrs => fn eqn => + ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns; + fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> + Drule.abs_def) o maps snd; in thy - |> Locale.add_registration (name, (morph', export)) - |> pair (name, morph') + |> PureThy.note_thmss Thm.lemmaK eqn_attrss + |-> (fn facts => `(fn thy => meta_rewrite thy facts)) end; - fun store_eqns_activate regs [] thy = - thy - |> fold (fn (name, morph) => - Context.theory_map (Locale.activate_facts (name, morph $> export))) regs - | store_eqns_activate regs eqs thy = - let - val eqs' = eqs |> map (Morphism.thm (export' $> export)); - val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> - Drule.abs_def); - val eq_morph = Element.eq_morphism thy morph_eqs; - val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns; - in - thy - |> fold (fn (name, morph) => - Locale.amend_registration eq_morph (name, morph) #> - Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs - |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs') - |> snd - end; - - fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits) - #-> (fn regs => store_eqns_activate regs eqs)); + fun after_qed witss eqns = ProofContext.theory (note_eqns eqns + #-> (fn eqns => fold (fn ((dep, morph), wits) => + Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism + (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss))); in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; @@ -868,12 +832,33 @@ end; +(** Interpretation between locales: declaring sublocale relationships **) + +local + +fun gen_sublocale prep_expr intern raw_target expression thy = + let + val target = intern thy raw_target; + val target_ctxt = Locale.init target thy; + val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; + fun after_qed witss = ProofContext.theory + (fold (fn ((dep, morph), wits) => Locale.add_dependency + target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss)); + in Element.witness_proof after_qed propss goal_ctxt end; + +in + +fun sublocale x = gen_sublocale cert_goal_expression (K I) x; +fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x; + +end; + + (** Interpretation in proof contexts **) local -fun gen_interpret prep_expr - expression int state = +fun gen_interpret prep_expr expression int state = let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; diff -r 0a83608e21f1 -r 76d6ba08a05f src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Jul 15 10:11:13 2009 +0200 +++ b/src/Pure/Isar/locale.ML Wed Jul 15 18:20:08 2009 +0200 @@ -70,8 +70,8 @@ (* Registrations and dependencies *) val add_registration: string * (morphism * morphism) -> theory -> theory val amend_registration: morphism -> string * morphism -> theory -> theory - val add_dependencies: string -> ((string * morphism) * Element.witness list) list -> - morphism -> theory -> theory + val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory + val add_dependency: string -> string * morphism -> morphism -> theory -> theory (* Diagnostic *) val print_locales: theory -> unit @@ -368,14 +368,22 @@ (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy end; +fun add_registration_eqs (dep, proto_morph) eqns export thy = + let + val morph = if null eqns then proto_morph + else proto_morph $> Element.eq_morphism thy eqns; + in + thy + |> add_registration (dep, (morph, export)) + |> Context.theory_map (activate_facts (dep, morph $> export)) + end; + (*** Dependencies ***) -fun add_dependencies loc deps_witss export thy = +fun add_dependency loc (dep, morph) export thy = thy - |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd) - (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ()))) - deps_witss + |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ())) |> (fn thy => fold_rev (Context.theory_map o activate_facts) (all_registrations thy) thy);