1.1 --- a/NEWS Thu Jan 06 21:06:17 2011 +0100
1.2 +++ b/NEWS Thu Jan 06 21:06:18 2011 +0100
1.3 @@ -103,8 +103,15 @@
1.4
1.5 * Support for real valued preferences (with approximative PGIP type).
1.6
1.7 -* Interpretation command 'interpret' accepts a list of equations like
1.8 -'interpretation' does.
1.9 +* Locale interpretation commands 'interpret' and 'sublocale' accept
1.10 +lists of equations to map definitions in a locale to appropriate
1.11 +entities in the context of the interpretation. The 'interpretation'
1.12 +command already provided this functionality.
1.13 +
1.14 +* New diagnostic command 'print_dependencies' prints the locale
1.15 +instances that would be activated if the specified expression was
1.16 +interpreted in the current context. Variant 'print_dependencies!'
1.17 +assumes a context without interpretations.
1.18
1.19 * Diagnostic command 'print_interps' prints interpretations in proofs
1.20 in addition to interpretations in theories.
1.21 @@ -123,11 +130,6 @@
1.22 * Document antiquotation @{file} checks file/directory entries within
1.23 the local file system.
1.24
1.25 -* Locale interpretation commands 'interpret' and 'sublocale' accept
1.26 -equations to map definitions in a locale to appropriate entities in
1.27 -the context of the interpretation. The 'interpretation' command
1.28 -already provided this functionality.
1.29 -
1.30
1.31 *** HOL ***
1.32
2.1 --- a/doc-src/IsarRef/Thy/Spec.thy Thu Jan 06 21:06:17 2011 +0100
2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jan 06 21:06:18 2011 +0100
2.3 @@ -497,6 +497,7 @@
2.4 @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2.5 @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
2.6 @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
2.7 + @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
2.8 @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
2.9 \end{matharray}
2.10
2.11 @@ -508,10 +509,12 @@
2.12 ;
2.13 'sublocale' nameref ('<' | subseteq) localeexpr equations?
2.14 ;
2.15 - equations: 'where' (thmdecl? prop + 'and')
2.16 + 'print_dependencies' '!'? localeexpr
2.17 ;
2.18 'print_interps' nameref
2.19 ;
2.20 + equations: 'where' (thmdecl? prop + 'and')
2.21 + ;
2.22 \end{rail}
2.23
2.24 \begin{description}
2.25 @@ -580,6 +583,14 @@
2.26 from the interpreted locales to entities of @{text name}. This
2.27 feature is experimental.
2.28
2.29 + \item @{command "print_dependencies"}~@{text "expr"} is useful for
2.30 + understanding the effect of an interpretation of @{text "expr"}. It
2.31 + lists all locale instances for which interpretations would be added
2.32 + to the current context. Variant @{command
2.33 + "print_dependencies"}@{text "!"} prints all locale instances that
2.34 + would be considered for interpretation, and would be interpreted in
2.35 + an empty context (that is, without interpretations).
2.36 +
2.37 \item @{command "print_interps"}~@{text "locale"} lists all
2.38 interpretations of @{text "locale"} in the current theory or proof
2.39 context, including those due to a combination of a @{command
3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 06 21:06:17 2011 +0100
3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 06 21:06:18 2011 +0100
3.3 @@ -518,6 +518,7 @@
3.4 \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
3.5 \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
3.6 \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
3.7 + \indexdef{}{command}{print\_dependencies}\hypertarget{command.print-dependencies}{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
3.8 \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
3.9 \end{matharray}
3.10
3.11 @@ -529,10 +530,12 @@
3.12 ;
3.13 'sublocale' nameref ('<' | subseteq) localeexpr equations?
3.14 ;
3.15 - equations: 'where' (thmdecl? prop + 'and')
3.16 + 'print_dependencies' '!'? localeexpr
3.17 ;
3.18 'print_interps' nameref
3.19 ;
3.20 + equations: 'where' (thmdecl? prop + 'and')
3.21 + ;
3.22 \end{rail}
3.23
3.24 \begin{description}
3.25 @@ -600,6 +603,13 @@
3.26 from the interpreted locales to entities of \isa{name}. This
3.27 feature is experimental.
3.28
3.29 + \item \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}} is useful for
3.30 + understanding the effect of an interpretation of \isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}}. It
3.31 + lists all locale instances for which interpretations would be added
3.32 + to the current context. Variant \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}} prints all locale instances that
3.33 + would be considered for interpretation, and would be interpreted in
3.34 + an empty context (that is, without interpretations).
3.35 +
3.36 \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all
3.37 interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof
3.38 context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several
4.1 --- a/etc/isar-keywords-ZF.el Thu Jan 06 21:06:17 2011 +0100
4.2 +++ b/etc/isar-keywords-ZF.el Thu Jan 06 21:06:18 2011 +0100
4.3 @@ -131,6 +131,7 @@
4.4 "print_commands"
4.5 "print_configs"
4.6 "print_context"
4.7 + "print_dependencies"
4.8 "print_drafts"
4.9 "print_facts"
4.10 "print_induct_rules"
4.11 @@ -300,6 +301,7 @@
4.12 "print_commands"
4.13 "print_configs"
4.14 "print_context"
4.15 + "print_dependencies"
4.16 "print_drafts"
4.17 "print_facts"
4.18 "print_induct_rules"
5.1 --- a/etc/isar-keywords.el Thu Jan 06 21:06:17 2011 +0100
5.2 +++ b/etc/isar-keywords.el Thu Jan 06 21:06:18 2011 +0100
5.3 @@ -171,6 +171,7 @@
5.4 "print_commands"
5.5 "print_configs"
5.6 "print_context"
5.7 + "print_dependencies"
5.8 "print_drafts"
5.9 "print_facts"
5.10 "print_induct_rules"
5.11 @@ -372,6 +373,7 @@
5.12 "print_commands"
5.13 "print_configs"
5.14 "print_context"
5.15 + "print_dependencies"
5.16 "print_drafts"
5.17 "print_facts"
5.18 "print_induct_rules"
6.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 06 21:06:17 2011 +0100
6.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 06 21:06:18 2011 +0100
6.3 @@ -771,6 +771,7 @@
6.4 then interpret local_fixed: lgrp "op +" zero "minus"
6.5 by unfold_locales
6.6 thm local_fixed.lone
6.7 + print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
6.8 }
6.9 assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
6.10 then interpret local_free: lgrp "op +" zero "minus" for zero
7.1 --- a/src/Pure/Isar/expression.ML Thu Jan 06 21:06:17 2011 +0100
7.2 +++ b/src/Pure/Isar/expression.ML Thu Jan 06 21:06:18 2011 +0100
7.3 @@ -51,6 +51,9 @@
7.4 bool -> Proof.state -> Proof.state
7.5 val interpret_cmd: expression -> (Attrib.binding * string) list ->
7.6 bool -> Proof.state -> Proof.state
7.7 +
7.8 + (* Diagnostic *)
7.9 + val print_dependencies: Proof.context -> bool -> expression -> unit
7.10 end;
7.11
7.12 structure Expression : EXPRESSION =
7.13 @@ -913,12 +916,6 @@
7.14 note_eqns_dependency target deps witss attrss eqns export export';
7.15
7.16 in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
7.17 -(*
7.18 - fun after_qed witss = ProofContext.background_theory
7.19 - (fold (fn ((dep, morph), wits) => Locale.add_dependency
7.20 - target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
7.21 - in Element.witness_proof after_qed propss goal_ctxt end;
7.22 -*)
7.23 in
7.24
7.25 fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
7.26 @@ -927,5 +924,17 @@
7.27
7.28 end;
7.29
7.30 +
7.31 +(** Print the instances that would be activated by an interpretation
7.32 + of the expression in the current context (clean = false) or in an
7.33 + empty context (clean = true). **)
7.34 +
7.35 +fun print_dependencies ctxt clean expression =
7.36 + let
7.37 + val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt;
7.38 + in
7.39 + Locale.print_dependencies expr_ctxt clean export deps
7.40 + end;
7.41 +
7.42 end;
7.43
8.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Jan 06 21:06:17 2011 +0100
8.2 +++ b/src/Pure/Isar/isar_cmd.ML Thu Jan 06 21:06:18 2011 +0100
8.3 @@ -50,6 +50,8 @@
8.4 val print_locales: Toplevel.transition -> Toplevel.transition
8.5 val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
8.6 val print_registrations: string -> Toplevel.transition -> Toplevel.transition
8.7 + val print_dependencies: bool * Expression.expression -> Toplevel.transition
8.8 + -> Toplevel.transition
8.9 val print_attributes: Toplevel.transition -> Toplevel.transition
8.10 val print_simpset: Toplevel.transition -> Toplevel.transition
8.11 val print_rules: Toplevel.transition -> Toplevel.transition
8.12 @@ -342,6 +344,10 @@
8.13 Toplevel.keep (fn state =>
8.14 Locale.print_registrations (Toplevel.context_of state) name);
8.15
8.16 +fun print_dependencies (clean, expression) = Toplevel.unknown_context o
8.17 + Toplevel.keep (fn state =>
8.18 + Expression.print_dependencies (Toplevel.context_of state) clean expression);
8.19 +
8.20 val print_attributes = Toplevel.unknown_theory o
8.21 Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
8.22
9.1 --- a/src/Pure/Isar/isar_syn.ML Thu Jan 06 21:06:17 2011 +0100
9.2 +++ b/src/Pure/Isar/isar_syn.ML Thu Jan 06 21:06:18 2011 +0100
9.3 @@ -836,10 +836,16 @@
9.4
9.5 val _ =
9.6 Outer_Syntax.improper_command "print_interps"
9.7 - "print interpretations of locale for this theory" Keyword.diag
9.8 + "print interpretations of locale for this theory or proof context" Keyword.diag
9.9 (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
9.10
9.11 val _ =
9.12 + Outer_Syntax.improper_command "print_dependencies"
9.13 + "print dependencies of locale expression" Keyword.diag
9.14 + (opt_bang -- Parse_Spec.locale_expression true >>
9.15 + (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
9.16 +
9.17 +val _ =
9.18 Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
9.19 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
9.20
10.1 --- a/src/Pure/Isar/locale.ML Thu Jan 06 21:06:17 2011 +0100
10.2 +++ b/src/Pure/Isar/locale.ML Thu Jan 06 21:06:18 2011 +0100
10.3 @@ -79,6 +79,7 @@
10.4 val print_locales: theory -> unit
10.5 val print_locale: theory -> bool -> xstring -> unit
10.6 val print_registrations: Proof.context -> string -> unit
10.7 + val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
10.8 val locale_deps: theory ->
10.9 {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
10.10 * term list list Symtab.table Symtab.table
10.11 @@ -212,10 +213,10 @@
10.12
10.13 (* Print instance and qualifiers *)
10.14
10.15 -fun pretty_reg thy (name, morph) =
10.16 +fun pretty_reg ctxt (name, morph) =
10.17 let
10.18 + val thy = ProofContext.theory_of ctxt;
10.19 val name' = extern thy name;
10.20 - val ctxt = ProofContext.init_global thy;
10.21 fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
10.22 fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
10.23 val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
10.24 @@ -649,10 +650,22 @@
10.25 fun print_registrations ctxt raw_name =
10.26 let
10.27 val thy = ProofContext.theory_of ctxt;
10.28 + val name = intern thy raw_name;
10.29 + val _ = the_locale thy name; (* error if locale unknown *)
10.30 in
10.31 - (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
10.32 + (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
10.33 [] => Pretty.str ("no interpretations")
10.34 - | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
10.35 + | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
10.36 + end |> Pretty.writeln;
10.37 +
10.38 +fun print_dependencies ctxt clean export insts =
10.39 + let
10.40 + val thy = ProofContext.theory_of ctxt;
10.41 + val idents = if clean then [] else get_idents (Context.Proof ctxt);
10.42 + in
10.43 + (case fold (roundup thy cons export) insts (idents, []) |> snd of
10.44 + [] => Pretty.str ("no dependencies")
10.45 + | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
10.46 end |> Pretty.writeln;
10.47
10.48 fun locale_deps thy =