# HG changeset patch # User ballarin # Date 1254255354 -7200 # Node ID ca430e6aee1c51378df7c0ca80d705bd4692f7f4 # Parent fc02b4b9eccc04bcdef29735d64d064214078c17# Parent 6f97a67e8da8bae97510c7e33127f980a3ed634f Propagation of mixins for interpretation; reactivated diagnostic command print_interps. diff -r fc02b4b9eccc -r ca430e6aee1c doc-src/Locales/Locales/Examples3.thy --- a/doc-src/Locales/Locales/Examples3.thy Sun Sep 27 11:50:27 2009 +0200 +++ b/doc-src/Locales/Locales/Examples3.thy Tue Sep 29 22:15:54 2009 +0200 @@ -14,7 +14,7 @@ interpretation. The third revision of the example illustrates this. *} interpretation %visible nat: partial_order "op \ :: nat \ nat \ bool" - where nat_less_eq: "partial_order.less op \ (x::nat) y = (x < y)" + where "partial_order.less op \ (x::nat) y = (x < y)" proof - show "partial_order (op \ :: nat \ nat \ bool)" by unfold_locales auto @@ -44,11 +44,10 @@ elaborate interpretation proof. *} interpretation %visible nat: lattice "op \ :: nat \ nat \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" - and nat_meet_eq: "lattice.meet op \ (x::nat) y = min x y" - and nat_join_eq: "lattice.join op \ (x::nat) y = max x y" + where "lattice.meet op \ (x::nat) y = min x y" + and "lattice.join op \ (x::nat) y = max x y" proof - - show lattice: "lattice (op \ :: nat \ nat \ bool)" + show "lattice (op \ :: nat \ nat \ bool)" txt {* We have already shown that this is a partial order, *} apply unfold_locales txt {* hence only the lattice axioms remain to be shown: @{subgoals @@ -57,13 +56,9 @@ txt {* the goals become @{subgoals [display]} which can be solved by Presburger arithmetic. *} by arith+ - txt {* For the first of the equations, we refer to the theorem - shown in the previous interpretation. *} - show "partial_order.less op \ (x::nat) y = (x < y)" - by (rule nat_less_eq) - txt {* In order to show the remaining equations, we put ourselves in a + txt {* In order to show the equations, we put ourselves in a situation where the lattice theorems can be used in a convenient way. *} - from lattice interpret nat: lattice "op \ :: nat \ nat \ bool" . + then interpret nat: lattice "op \ :: nat \ nat \ bool" . show "lattice.meet op \ (x::nat) y = min x y" by (bestsimp simp: nat.meet_def nat.is_inf_def) show "lattice.join op \ (x::nat) y = max x y" @@ -73,25 +68,7 @@ text {* Next follows that @{text \} is a total order. *} interpretation %visible nat: total_order "op \ :: nat \ nat \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" - and "lattice.meet op \ (x::nat) y = min x y" - and "lattice.join op \ (x::nat) y = max x y" -proof - - show "total_order (op \ :: nat \ nat \ bool)" - by unfold_locales arith -qed (rule nat_less_eq nat_meet_eq nat_join_eq)+ - -text {* Since the locale hierarchy reflects that total - orders are distributive lattices, an explicit interpretation of - distributive lattices for the order relation on natural numbers is - only necessary for mapping the definitions to the right operators on - @{typ nat}. *} - -interpretation %visible nat: distrib_lattice "op \ :: nat \ nat \ bool" - where "partial_order.less op \ (x::nat) y = (x < y)" - and "lattice.meet op \ (x::nat) y = min x y" - and "lattice.join op \ (x::nat) y = max x y" - by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+ + by unfold_locales arith text {* Theorems that are available in the theory at this point are shown in Table~\ref{tab:nat-lattice}. @@ -115,6 +92,29 @@ \caption{Interpreted theorems for @{text \} on the natural numbers.} \label{tab:nat-lattice} \end{table} + + Note that since the locale hierarchy reflects that total orders are + distributive lattices, an explicit interpretation of distributive + lattices for the order relation on natural numbers is not neccessary. + + Why not push this idea further and just give the last interpretation + as a single interpretation instead of the sequence of three? The + reasons for this are twofold: +\begin{itemize} +\item + Often it is easier to work in an incremental fashion, because later + interpretations require theorems provided by earlier + interpretations. +\item + Assume that a definition is made in some locale $l_1$, and that $l_2$ + imports $l_1$. Let an equation for the definition be + proved in an interpretation of $l_2$. The equation will be unfolded + in interpretations of theorems added to $l_2$ or below in the import + hierarchy, but not for theorems added above $l_2$. + Hence, an equation interpreting a definition should always be given in + an interpretation of the locale where the definition is made, not in + an interpretation of a locale further down the hierarchy. +\end{itemize} *} @@ -125,8 +125,7 @@ incrementally. *} interpretation nat_dvd: partial_order "op dvd :: nat \ nat \ bool" - where nat_dvd_less_eq: - "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" + where "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" proof - show "partial_order (op dvd :: nat \ nat \ bool)" by unfold_locales (auto simp: dvd_def) @@ -142,8 +141,7 @@ x \ y"}. *} interpretation nat_dvd: lattice "op dvd :: nat \ nat \ bool" - where "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" - and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" + where nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" and nat_dvd_join_eq: "lattice.join (op dvd :: nat \ nat \ bool) = lcm" proof - show "lattice (op dvd :: nat \ nat \ bool)" @@ -155,8 +153,6 @@ apply (auto intro: lcm_least_nat) done then interpret nat_dvd: lattice "op dvd :: nat \ nat \ bool" . - show "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" - by (rule nat_dvd_less_eq) show "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" apply (auto simp add: expand_fun_eq) apply (unfold nat_dvd.meet_def) @@ -198,18 +194,11 @@ interpretation %visible nat_dvd: distrib_lattice "op dvd :: nat \ nat \ bool" - where "partial_order.less op dvd (x::nat) y = (x dvd y \ x \ y)" - and "lattice.meet (op dvd :: nat \ nat \ bool) = gcd" - and "lattice.join (op dvd :: nat \ nat \ bool) = lcm" -proof - - show "distrib_lattice (op dvd :: nat \ nat \ bool)" - apply unfold_locales - txt {* @{subgoals [display]} *} - apply (unfold nat_dvd_meet_eq nat_dvd_join_eq) - txt {* @{subgoals [display]} *} - apply (rule gcd_lcm_distr) - done -qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+ + apply unfold_locales + txt {* @{subgoals [display]} *} + apply (unfold nat_dvd_meet_eq nat_dvd_join_eq) + txt {* @{subgoals [display]} *} + apply (rule gcd_lcm_distr) done text {* Theorems that are available in the theory after these diff -r fc02b4b9eccc -r ca430e6aee1c etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Sun Sep 27 11:50:27 2009 +0200 +++ b/etc/isar-keywords-ZF.el Tue Sep 29 22:15:54 2009 +0200 @@ -139,6 +139,7 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_locale" "print_locales" "print_methods" @@ -304,6 +305,7 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_locale" "print_locales" "print_methods" diff -r fc02b4b9eccc -r ca430e6aee1c etc/isar-keywords.el --- a/etc/isar-keywords.el Sun Sep 27 11:50:27 2009 +0200 +++ b/etc/isar-keywords.el Tue Sep 29 22:15:54 2009 +0200 @@ -176,6 +176,7 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_locale" "print_locales" "print_methods" @@ -379,6 +380,7 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_locale" "print_locales" "print_methods" diff -r fc02b4b9eccc -r ca430e6aee1c src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun Sep 27 11:50:27 2009 +0200 +++ b/src/Pure/Isar/expression.ML Tue Sep 29 22:15:54 2009 +0200 @@ -818,8 +818,9 @@ 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))); + fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism + (map (Element.morph_witness export') wits)) + (Element.eq_morphism thy eqns, true) export thy) (deps ~~ witss))); in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; diff -r fc02b4b9eccc -r ca430e6aee1c src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Sep 27 11:50:27 2009 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Sep 29 22:15:54 2009 +0200 @@ -53,6 +53,7 @@ val print_theorems: Toplevel.transition -> Toplevel.transition val print_locales: Toplevel.transition -> Toplevel.transition val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition + val print_registrations: string -> Toplevel.transition -> Toplevel.transition val print_attributes: Toplevel.transition -> Toplevel.transition val print_simpset: Toplevel.transition -> Toplevel.transition val print_rules: Toplevel.transition -> Toplevel.transition @@ -357,6 +358,10 @@ Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) show_facts name); +fun print_registrations name = Toplevel.unknown_context o + Toplevel.keep (fn state => + Locale.print_registrations (Toplevel.theory_of state) name); + val print_attributes = Toplevel.unknown_theory o Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); diff -r fc02b4b9eccc -r ca430e6aee1c src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Sep 27 11:50:27 2009 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 29 22:15:54 2009 +0200 @@ -800,10 +800,15 @@ o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); val _ = - OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag + OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); val _ = + OuterSyntax.improper_command "print_interps" + "print interpretations of locale for this theory" K.diag + (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); + +val _ = OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); diff -r fc02b4b9eccc -r ca430e6aee1c src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Sep 27 11:50:27 2009 +0200 +++ b/src/Pure/Isar/locale.ML Tue Sep 29 22:15:54 2009 +0200 @@ -68,6 +68,8 @@ val intro_locales_tac: bool -> Proof.context -> thm list -> tactic (* Registrations and dependencies *) + val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory + val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory val amend_registration_legacy: morphism -> string * morphism -> theory -> theory val add_dependency: string -> string * morphism -> morphism -> theory -> theory @@ -75,6 +77,7 @@ (* Diagnostic *) val print_locales: theory -> unit val print_locale: theory -> bool -> xstring -> unit + val print_registrations: theory -> string -> unit end; structure Locale: LOCALE = @@ -177,6 +180,7 @@ (** Identifiers: activated locales in theory or proof context **) fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts); +(* FIXME: this is ident_le, smaller term is more general *) local @@ -234,7 +238,7 @@ in -(* Note that while identifiers always have the exported view, activate_dep is +(* Note that while identifiers always have the external (exported) view, activate_dep is is presented with the internal view. *) fun roundup thy activate_dep export (name, morph) (marked, input) = @@ -328,29 +332,158 @@ structure Registrations = TheoryDataFun ( - type T = ((string * (morphism * morphism)) * stamp) list; - (* FIXME mixins need to be stamped *) + type T = ((string * (morphism * morphism)) * stamp) list * (* registrations, in reverse order of declaration *) - val empty = []; + (stamp * ((morphism * bool) * stamp) list) list; + (* alist of mixin lists, per list mixins in reverse order of declaration *) + val empty = ([], []); val extend = I; val copy = I; - fun merge _ data : T = Library.merge (eq_snd op =) data; + fun merge _ ((r1, m1), (r2, m2)) : T = + (Library.merge (eq_snd op =) (r1, r2), + AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2)); (* FIXME consolidate with dependencies, consider one data slot only *) ); -fun reg_morph ((name, (base, export)), _) = (name, base $> export); + +(* Primitive operations *) + +fun compose_mixins mixins = + fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; + +fun reg_morph mixins ((name, (base, export)), stamp) = + let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins; + in (name, base $> mix $> export) end; fun these_registrations thy name = Registrations.get thy - |> filter (curry (op =) name o fst o fst) - |> map reg_morph; + |>> filter (curry (op =) name o fst o fst) + |-> (fn regs => fn mixins => map (reg_morph mixins) regs); fun all_registrations thy = Registrations.get thy - |> map reg_morph; + |-> (fn regs => fn mixins => map (reg_morph mixins) regs); + +fun get_mixins thy (name, morph) = + let + val (regs, mixins) = Registrations.get thy; + in + case find_first (fn ((name', (morph', export')), _) => ident_eq thy + ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of + NONE => [] + | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp) + end; + +fun collect_mixins thy (name, morph) = + roundup thy (fn dep => fn mixins => + merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], []) + |> snd |> filter (snd o fst); (* only inheritable mixins *) + +fun activate_notes' activ_elem transfer thy export (name, morph) input = + let + val {notes, ...} = the_locale thy name; + fun activate ((kind, facts), _) input = + let + val mixin = collect_mixins thy (name, morph $> export) |> compose_mixins; + val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export)) + in activ_elem (Notes (kind, facts')) input end; + in + fold_rev activate notes input + end; + +fun activate_facts' export dep context = + let + val thy = Context.theory_of context; + val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export; + in roundup thy activate export dep (get_idents context, context) |-> put_idents end; + + +(* Diagnostic *) + +fun print_registrations thy raw_name = + let + val name = intern thy raw_name; + val name' = extern thy name; + val ctxt = ProofContext.init thy; + fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?")); + fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block; + val prt_term = Pretty.quote o Syntax.pretty_term ctxt; + fun prt_term' t = if !show_types + then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", + Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] + else prt_term t; + fun prt_inst ts = + Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts)); + fun prt_reg (name, morph) = + let + val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of; + val ts = instance_of thy name morph; + in + case qs of + [] => prt_inst ts + | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", + Pretty.brk 1, prt_inst ts] + end; + in + (case these_registrations thy name of + [] => Pretty.str ("no interpretations") + | regs => Pretty.big_list "interpretations:" (map prt_reg regs)) + |> Pretty.writeln + end; + + +(* Add and extend registrations *) + +fun amend_registration (name, morph) mixin export thy = + let + val regs = Registrations.get thy |> fst; + val base = instance_of thy name (morph $> export); + fun match ((name', (morph', export')), _) = + name = name' andalso eq_list (op aconv) (base, instance_of thy name' (morph' $> export')); + in + case find_first match (rev regs) of + NONE => error ("No interpretation of locale " ^ + quote (extern thy name) ^ " and\nparameter instantiation " ^ + space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ + " available") + | SOME (_, stamp') => Registrations.map + (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy + (* FIXME deal with inheritance: propagate to existing children *) + end; + +(* Note that a registration that would be subsumed by an existing one will not be + generated, and it will not be possible to amend it. *) + +fun add_registration (name, base_morph) mixin export thy = + let + val base = instance_of thy name base_morph; + in + if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base) + then thy + else + let + fun add_reg (dep', morph') = + let + val mixins = collect_mixins thy (dep', morph' $> export); + val stamp = stamp (); + in + Registrations.map (apfst (cons ((dep', (morph', export)), stamp)) + #> apsnd (cons (stamp, mixins))) + end + in + (get_idents (Context.Theory thy), thy) + (* add new registrations with inherited mixins *) + |> roundup thy add_reg export (name, base_morph) + |> snd + (* add mixin *) + |> amend_registration (name, base_morph) mixin export + (* activate import hierarchy as far as not already active *) + |> Context.theory_map (activate_facts' export (name, base_morph)) + end + end; fun amend_registration_legacy morph (name, base_morph) thy = (* legacy, never modify base morphism *) let - val regs = map #1 (Registrations.get thy); + val regs = Registrations.get thy |> fst |> map fst; val base = instance_of thy name base_morph; fun match (name', (morph', _)) = name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph'); @@ -361,7 +494,7 @@ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available") else (); in - Registrations.map (nth_map (length regs - 1 - i) + Registrations.map ((apfst o nth_map (length regs - 1 - i)) (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy end; @@ -372,7 +505,7 @@ in (get_idents (Context.Theory thy), thy) |> roundup thy (fn (dep', morph') => - Registrations.map (cons ((dep', (morph', export)), stamp ()))) export (dep, morph) + Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph) |> snd |> Context.theory_map (activate_facts (dep, morph $> export)) end; @@ -383,8 +516,9 @@ fun add_dependency loc (dep, morph) export thy = thy |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ())) - |> (fn thy => fold_rev (Context.theory_map o activate_facts) + |> (fn thy => fold_rev (Context.theory_map o activate_facts' export) (all_registrations thy) thy); + (* FIXME deal with inheritance: propagate mixins to new children *) (*** Storing results ***)