Diagnostic command to show locale dependencies.
authorballarin
Thu Jan 06 21:06:18 2011 +0100 (2011-01-06 ago)
changeset 4143512585dfb86fe
parent 41434 710cdb9e0d17
child 41436 480978f80eae
Diagnostic command to show locale dependencies.
NEWS
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
     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 =