# HG changeset patch
# User ballarin
# Date 1294344378 -3600
# Node ID 12585dfb86fef51f18493607049666ed32599b40
# Parent  710cdb9e0d17024a78019b3f252f7b64366ae185
Diagnostic command to show locale dependencies.

diff -r 710cdb9e0d17 -r 12585dfb86fe NEWS
--- a/NEWS	Thu Jan 06 21:06:17 2011 +0100
+++ b/NEWS	Thu Jan 06 21:06:18 2011 +0100
@@ -103,8 +103,15 @@
 
 * Support for real valued preferences (with approximative PGIP type).
 
-* Interpretation command 'interpret' accepts a list of equations like
-'interpretation' does.
+* Locale interpretation commands 'interpret' and 'sublocale' accept
+lists of equations to map definitions in a locale to appropriate
+entities in the context of the interpretation.  The 'interpretation'
+command already provided this functionality.
+
+* New diagnostic command 'print_dependencies' prints the locale
+instances that would be activated if the specified expression was
+interpreted in the current context.  Variant 'print_dependencies!'
+assumes a context without interpretations.
 
 * Diagnostic command 'print_interps' prints interpretations in proofs
 in addition to interpretations in theories.
@@ -123,11 +130,6 @@
 * Document antiquotation @{file} checks file/directory entries within
 the local file system.
 
-* Locale interpretation commands 'interpret' and 'sublocale' accept
-equations to map definitions in a locale to appropriate entities in
-the context of the interpretation.  The 'interpretation' command
-already provided this functionality.
-
 
 *** HOL ***
 
diff -r 710cdb9e0d17 -r 12585dfb86fe doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:17 2011 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:18 2011 +0100
@@ -497,6 +497,7 @@
     @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
     @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+    @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
@@ -508,10 +509,12 @@
     ;
     'sublocale' nameref ('<' | subseteq) localeexpr equations?
     ;
-    equations: 'where' (thmdecl? prop + 'and')
+    'print_dependencies' '!'? localeexpr
     ;
     'print_interps' nameref
     ;
+    equations: 'where' (thmdecl? prop + 'and')
+    ;
   \end{rail}
 
   \begin{description}
@@ -580,6 +583,14 @@
   from the interpreted locales to entities of @{text name}.  This
   feature is experimental.
 
+  \item @{command "print_dependencies"}~@{text "expr"} is useful for
+  understanding the effect of an interpretation of @{text "expr"}.  It
+  lists all locale instances for which interpretations would be added
+  to the current context.  Variant @{command
+  "print_dependencies"}@{text "!"} prints all locale instances that
+  would be considered for interpretation, and would be interpreted in
+  an empty context (that is, without interpretations).
+
   \item @{command "print_interps"}~@{text "locale"} lists all
   interpretations of @{text "locale"} in the current theory or proof
   context, including those due to a combination of a @{command
diff -r 710cdb9e0d17 -r 12585dfb86fe doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jan 06 21:06:17 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jan 06 21:06:18 2011 +0100
@@ -518,6 +518,7 @@
     \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}}} \\
     \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}}} \\
     \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}}} \\
+    \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}}} \\
     \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}}} \\
   \end{matharray}
 
@@ -529,10 +530,12 @@
     ;
     'sublocale' nameref ('<' | subseteq) localeexpr equations?
     ;
-    equations: 'where' (thmdecl? prop + 'and')
+    'print_dependencies' '!'? localeexpr
     ;
     'print_interps' nameref
     ;
+    equations: 'where' (thmdecl? prop + 'and')
+    ;
   \end{rail}
 
   \begin{description}
@@ -600,6 +603,13 @@
   from the interpreted locales to entities of \isa{name}.  This
   feature is experimental.
 
+  \item \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}} is useful for
+  understanding the effect of an interpretation of \isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}}.  It
+  lists all locale instances for which interpretations would be added
+  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
+  would be considered for interpretation, and would be interpreted in
+  an empty context (that is, without interpretations).
+
   \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all
   interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof
   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
diff -r 710cdb9e0d17 -r 12585dfb86fe etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Jan 06 21:06:17 2011 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Jan 06 21:06:18 2011 +0100
@@ -131,6 +131,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_dependencies"
     "print_drafts"
     "print_facts"
     "print_induct_rules"
@@ -300,6 +301,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_dependencies"
     "print_drafts"
     "print_facts"
     "print_induct_rules"
diff -r 710cdb9e0d17 -r 12585dfb86fe etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Jan 06 21:06:17 2011 +0100
+++ b/etc/isar-keywords.el	Thu Jan 06 21:06:18 2011 +0100
@@ -171,6 +171,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_dependencies"
     "print_drafts"
     "print_facts"
     "print_induct_rules"
@@ -372,6 +373,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_dependencies"
     "print_drafts"
     "print_facts"
     "print_induct_rules"
diff -r 710cdb9e0d17 -r 12585dfb86fe src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jan 06 21:06:18 2011 +0100
@@ -771,6 +771,7 @@
     then interpret local_fixed: lgrp "op +" zero "minus"
       by unfold_locales
     thm local_fixed.lone
+    print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
   }
   assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
   then interpret local_free: lgrp "op +" zero "minus" for zero
diff -r 710cdb9e0d17 -r 12585dfb86fe src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Jan 06 21:06:18 2011 +0100
@@ -51,6 +51,9 @@
     bool -> Proof.state -> Proof.state
   val interpret_cmd: expression -> (Attrib.binding * string) list ->
     bool -> Proof.state -> Proof.state
+
+  (* Diagnostic *)
+  val print_dependencies: Proof.context -> bool -> expression -> unit
 end;
 
 structure Expression : EXPRESSION =
@@ -913,12 +916,6 @@
       note_eqns_dependency target deps witss attrss eqns export export';
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
-(*
-    fun after_qed witss = ProofContext.background_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) (K I) (K I) x;
@@ -927,5 +924,17 @@
 
 end;
 
+
+(** Print the instances that would be activated by an interpretation
+  of the expression in the current context (clean = false) or in an
+  empty context (clean = true). **)
+
+fun print_dependencies ctxt clean expression =
+  let
+    val ((_, deps, export), expr_ctxt) = read_goal_expression expression ctxt;
+  in
+    Locale.print_dependencies expr_ctxt clean export deps
+  end;
+
 end;
 
diff -r 710cdb9e0d17 -r 12585dfb86fe src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jan 06 21:06:18 2011 +0100
@@ -50,6 +50,8 @@
   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_dependencies: bool * Expression.expression -> 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
@@ -342,6 +344,10 @@
   Toplevel.keep (fn state =>
     Locale.print_registrations (Toplevel.context_of state) name);
 
+fun print_dependencies (clean, expression) = Toplevel.unknown_context o
+  Toplevel.keep (fn state =>
+    Expression.print_dependencies (Toplevel.context_of state) clean expression);
+
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 
diff -r 710cdb9e0d17 -r 12585dfb86fe src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:18 2011 +0100
@@ -836,10 +836,16 @@
 
 val _ =
   Outer_Syntax.improper_command "print_interps"
-    "print interpretations of locale for this theory" Keyword.diag
+    "print interpretations of locale for this theory or proof context" Keyword.diag
     (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
 
 val _ =
+  Outer_Syntax.improper_command "print_dependencies"
+    "print dependencies of locale expression" Keyword.diag
+    (opt_bang -- Parse_Spec.locale_expression true >>
+      (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
+
+val _ =
   Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
 
diff -r 710cdb9e0d17 -r 12585dfb86fe src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Jan 06 21:06:18 2011 +0100
@@ -79,6 +79,7 @@
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
   val print_registrations: Proof.context -> string -> unit
+  val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
   val locale_deps: theory ->
     {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
       * term list list Symtab.table Symtab.table
@@ -212,10 +213,10 @@
 
 (* Print instance and qualifiers *)
 
-fun pretty_reg thy (name, morph) =
+fun pretty_reg ctxt (name, morph) =
   let
+    val thy = ProofContext.theory_of ctxt;
     val name' = extern thy name;
-    val ctxt = ProofContext.init_global 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;
@@ -649,10 +650,22 @@
 fun print_registrations ctxt raw_name =
   let
     val thy = ProofContext.theory_of ctxt;
+    val name = intern thy raw_name;
+    val _ = the_locale thy name;  (* error if locale unknown *)
   in
-    (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+    (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
       [] => Pretty.str ("no interpretations")
-    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+    | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
+  end |> Pretty.writeln;
+
+fun print_dependencies ctxt clean export insts =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val idents = if clean then [] else get_idents (Context.Proof ctxt);
+  in
+    (case fold (roundup thy cons export) insts (idents, []) |> snd of
+      [] => Pretty.str ("no dependencies")
+    | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
   end |> Pretty.writeln;
 
 fun locale_deps thy =