added Proof.context to antiquotation
authorhaftmann
Sat May 14 21:31:13 2005 +0200 (2005-05-14)
changeset 159609bd6550dc004
parent 15959 366d39e95d3c
child 15961 24c6b96b4a2f
added Proof.context to antiquotation
doc-src/IsarRef/syntax.tex
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
src/Pure/Isar/isar_output.ML
src/Pure/Isar/term_style.ML
     1.1 --- a/doc-src/IsarRef/syntax.tex	Fri May 13 20:21:41 2005 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Sat May 14 21:31:13 2005 +0200
     1.3 @@ -412,11 +412,13 @@
     1.4  
     1.5  \begin{matharray}{rcl@{\hspace*{2cm}}rcl}
     1.6    thm & : & \isarantiq & text & : & \isarantiq \\
     1.7 -  lhs & : & \isarantiq & goals & : & \isarantiq \\
     1.8 -  rhs & : & \isarantiq & subgoals & : & \isarantiq \\
     1.9 -  prop & : & \isarantiq & prf & : & \isarantiq \\
    1.10 -  term & : & \isarantiq & full_prf & : & \isarantiq \\
    1.11 +  prop & : & \isarantiq & goals & : & \isarantiq \\
    1.12 +  term & : & \isarantiq & subgoals & : & \isarantiq \\
    1.13 +  const & : & \isarantiq & prf & : & \isarantiq \\
    1.14 +  typeof & : & \isarantiq & full_prf & : & \isarantiq \\
    1.15    typ & : & \isarantiq \\  
    1.16 +  thm_style & : & \isarantiq \\  
    1.17 +  term_style & : & \isarantiq \\  
    1.18  \end{matharray}
    1.19  
    1.20  The text body of formal comments (see also \S\ref{sec:comments}) may contain
    1.21 @@ -442,11 +444,13 @@
    1.22  
    1.23    antiquotation:
    1.24      'thm' options thmrefs |
    1.25 -    'lhs' options thmrefs |
    1.26 -    'rhs' options thmrefs |
    1.27      'prop' options prop |
    1.28      'term' options term |
    1.29 +    'const' options term |
    1.30 +    'typeof' options term |
    1.31      'typ' options type |
    1.32 +    'thm\_style' options style thmref |
    1.33 +    'term\_style' options style term |
    1.34      'text' options name |
    1.35      'goals' options |
    1.36      'subgoals' options |
    1.37 @@ -469,21 +473,23 @@
    1.38    $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
    1.39    useful to suppress printing of schematic variables.
    1.40  
    1.41 -\item [$\at\{lhs~\vec a\}$] prints the left hand sides of theorems $\vec a$.
    1.42 -  The antiquotation only works for $\vec a$ that are definitions,
    1.43 -  equations or other binary operators.  It understands the same
    1.44 -  options and attributes as $\at\{thm~\vec a\}$.
    1.45 -
    1.46 -\item [$\at\{rhs~\vec a\}$] prints the right hand sides of theorems $\vec a$.
    1.47 -  As for $\at\{lhs~\vec a\}$, $\vec a$ must be definitions, equations or
    1.48 -  other binary operators.
    1.49 -
    1.50  \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
    1.51  
    1.52  \item [$\at\{term~t\}$] prints a well-typed term $t$.
    1.53  
    1.54 +\item [$\at\{const~c\}$] prints a well-defined constant $c$.
    1.55 +
    1.56 +\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
    1.57 +
    1.58  \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
    1.59  
    1.60 +\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously
    1.61 +  applying a style $s$ to it; otherwise behaves the same as $\at\{thm~a\}$
    1.62 +  with just one theorem.
    1.63 +
    1.64 +\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$, previously
    1.65 +  applying a style $s$ to it; otherwise behaves the same as $\at\{term~t\}$.
    1.66 +
    1.67  \item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
    1.68    particularly useful to print portions of text according to the Isabelle
    1.69    {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
    1.70 @@ -510,6 +516,24 @@
    1.71  
    1.72  \end{descr}
    1.73  
    1.74 +Per default, each theory contains three default styles for use with
    1.75 +$\at\{thm_style~s~a\}$ and $\at\{term_style~s~t\}$:
    1.76 +
    1.77 +\begin{descr}
    1.78 +
    1.79 +\item [$lhs$] extracts the left hand sides of terms; this style only works
    1.80 +    for terms that are definitions, equations or other binary operators.
    1.81 +
    1.82 +\item [$rhs$] extracts the right hand sides of terms; likewise,
    1.83 +    this style only works
    1.84 +    for terms that are definitions, equations or other binary operators.
    1.85 +
    1.86 +\item [$conlusion$] extracts the conclusion from propositions.
    1.87 +
    1.88 +\end{descr}
    1.89 +
    1.90 +Further styles may be defined at ML level.
    1.91 +
    1.92  \medskip
    1.93  
    1.94  The following options are available to tune the output.  Note that most of
     2.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri May 13 20:21:41 2005 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sat May 14 21:31:13 2005 +0200
     2.3 @@ -327,29 +327,41 @@
     2.4    \end{quote}
     2.5  
     2.6    If you are not afraid of ML, you may also define your own styles.
     2.7 -  A style is simply implemented by an ML function of type \verb!term -> term!.
     2.8 -  Have a look at the following example (which indeed shows just the way the
     2.9 -  \verb!lhs! style is implemented):
    2.10 +  A style is implemented by an ML function of type
    2.11 +  \verb!Proof.context -> term -> term!.
    2.12 +  Have a look at the following example:
    2.13 +
    2.14    \begin{quote}
    2.15      \verb!setup {!\verb!*!\\
    2.16      \verb!let!\\
    2.17 -    \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
    2.18 -    \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
    2.19 -    \verb!    | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\
    2.20 -    \verb!    | my_lhs (_ $ t $ _) = t!\\
    2.21 -    \verb!    | my_lhs _ = error ("Binary operator expected")!\\
    2.22 -    \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
    2.23 +    \verb!  fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\
    2.24 +    \verb!    | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\
    2.25 +    \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\
    2.26 +    \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
    2.27 +    \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
    2.28 +    \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
    2.29      \verb!end;!\\
    2.30      \verb!*!\verb!}!\\
    2.31    \end{quote}
    2.32 +
    2.33 +  This example indeed shows a way the \verb!lhs! style could be implemented;
    2.34 +  note that the real implementation is more sophisticated.
    2.35 +
    2.36    This code must go into your theory file, not as part of your
    2.37    \LaTeX\ text but as a separate command in front of it.
    2.38    Like in this example, it is recommended to put the definition of the style
    2.39    function into a \verb!let! expression, in order not to pollute the
    2.40 -  ML global namespace. The mapping from identifier name to the style function
    2.41 -  is done by the \verb!Style.put_style! expression which expects the desired
    2.42 -  style name and the style function as arguments. After this \verb!setup!,
    2.43 -  there will be a new style available named \verb!new_lhs! allowing
    2.44 +  ML global namespace. Each style receives the current proof context
    2.45 +  as first argument; this is necessary in situations where the current proof
    2.46 +  context has an impact on the style (which is the case e.~g.~when the
    2.47 +  style has some object-logic specific behaviour).
    2.48 +
    2.49 +  The mapping from identifier name to the style function
    2.50 +  is done by the \verb!Style.update_style! expression which expects the desired
    2.51 +  style name and the style function as arguments.
    2.52 +  
    2.53 +  After this \verb!setup!,
    2.54 +  there will be a new style available named \verb!new_lhs!, thus allowing
    2.55    antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
    2.56    yielding @{thm_style lhs rev_map}.
    2.57  
    2.58 @@ -357,6 +369,7 @@
    2.59    your own styles; for a description of the constructs used, please refer
    2.60    to the Isabelle reference manual.
    2.61  
    2.62 +
    2.63  *}
    2.64  
    2.65  (*<*)
     3.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri May 13 20:21:41 2005 +0200
     3.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat May 14 21:31:13 2005 +0200
     3.3 @@ -371,29 +371,41 @@
     3.4    \end{quote}
     3.5  
     3.6    If you are not afraid of ML, you may also define your own styles.
     3.7 -  A style is simply implemented by an ML function of type \verb!term -> term!.
     3.8 -  Have a look at the following example (which indeed shows just the way the
     3.9 -  \verb!lhs! style is implemented):
    3.10 +  A style is implemented by an ML function of type
    3.11 +  \verb!Proof.context -> term -> term!.
    3.12 +  Have a look at the following example:
    3.13 +
    3.14    \begin{quote}
    3.15      \verb!setup {!\verb!*!\\
    3.16      \verb!let!\\
    3.17 -    \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
    3.18 -    \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
    3.19 -    \verb!    | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\
    3.20 -    \verb!    | my_lhs (_ $ t $ _) = t!\\
    3.21 -    \verb!    | my_lhs _ = error ("Binary operator expected")!\\
    3.22 -    \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
    3.23 +    \verb!  fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\
    3.24 +    \verb!    | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs t!\\
    3.25 +    \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs t!\\
    3.26 +    \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
    3.27 +    \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
    3.28 +    \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
    3.29      \verb!end;!\\
    3.30      \verb!*!\verb!}!\\
    3.31    \end{quote}
    3.32 +
    3.33 +  This example indeed shows a way the \verb!lhs! style could be implemented;
    3.34 +  note that the real implementation is more sophisticated.
    3.35 +
    3.36    This code must go into your theory file, not as part of your
    3.37    \LaTeX\ text but as a separate command in front of it.
    3.38    Like in this example, it is recommended to put the definition of the style
    3.39    function into a \verb!let! expression, in order not to pollute the
    3.40 -  ML global namespace. The mapping from identifier name to the style function
    3.41 -  is done by the \verb!Style.put_style! expression which expects the desired
    3.42 -  style name and the style function as arguments. After this \verb!setup!,
    3.43 -  there will be a new style available named \verb!new_lhs! allowing
    3.44 +  ML global namespace. Each style receives the current proof context
    3.45 +  as first argument; this is necessary in situations where the current proof
    3.46 +  context has an impact on the style (which is the case e.~g.~when the
    3.47 +  style has some object-logic specific behaviour).
    3.48 +
    3.49 +  The mapping from identifier name to the style function
    3.50 +  is done by the \verb!Style.update_style! expression which expects the desired
    3.51 +  style name and the style function as arguments.
    3.52 +  
    3.53 +  After this \verb!setup!,
    3.54 +  there will be a new style available named \verb!new_lhs!, thus allowing
    3.55    antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
    3.56    yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}.
    3.57  
     4.1 --- a/src/Pure/Isar/isar_output.ML	Fri May 13 20:21:41 2005 +0200
     4.2 +++ b/src/Pure/Isar/isar_output.ML	Sat May 14 21:31:13 2005 +0200
     4.3 @@ -360,11 +360,15 @@
     4.4  fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt;
     4.5  
     4.6  fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c)
     4.7 -  | pretty_term_const ctxt term = raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
     4.8 +  | pretty_term_const ctxt term =
     4.9 +      raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
    4.10  
    4.11  fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    4.12  
    4.13 -fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((Style.get_style (ProofContext.theory_of ctxt) name) term);
    4.14 +fun pretty_term_style ctxt (name, term) =
    4.15 +  let
    4.16 +    val thy = ProofContext.theory_of ctxt
    4.17 +  in pretty_term ctxt (TermStyle.lookup_style thy name ctxt term) end;
    4.18  
    4.19  fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm);
    4.20  
     5.1 --- a/src/Pure/Isar/term_style.ML	Fri May 13 20:21:41 2005 +0200
     5.2 +++ b/src/Pure/Isar/term_style.ML	Sat May 14 21:31:13 2005 +0200
     5.3 @@ -5,60 +5,53 @@
     5.4  Styles for terms, to use with the "term_style" and "thm_style" antiquotations
     5.5  *)
     5.6  
     5.7 -signature STYLE =
     5.8 +(* style data *)
     5.9 +signature TERM_STYLE =
    5.10  sig
    5.11 -  val get_style: theory -> string -> (Term.term -> Term.term)
    5.12 -  val put_style: string -> (Term.term -> Term.term) -> theory -> theory
    5.13 +  val lookup_style: theory -> string -> (Proof.context -> term -> term)
    5.14 +  val update_style: string -> (Proof.context -> term -> term) -> theory -> theory
    5.15  end;
    5.16  
    5.17 -structure Style: STYLE =
    5.18 +structure TermStyle: TERM_STYLE =
    5.19  struct
    5.20  
    5.21 -(* exception *)
    5.22 -exception STYLE of string;
    5.23 -
    5.24 -(* style data *)
    5.25  structure StyleArgs =
    5.26  struct
    5.27    val name = "Isar/style";
    5.28 -  type T = (string * (Term.term -> Term.term)) list;
    5.29 -  val empty = [];
    5.30 +  type T = (Proof.context -> term -> term) Symtab.table;
    5.31 +  val empty = Symtab.empty;
    5.32    val copy = I;
    5.33    val prep_ext = I;
    5.34 -  fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2);
    5.35 -    (* piecewise update of a1 by a2 *)
    5.36 -  fun print _ _ = raise (STYLE "cannot print style (not implemented)");
    5.37 +  val merge = Symtab.merge (K true);
    5.38 +  fun print _ table =
    5.39 +    Pretty.strs ("defined styles:" :: (Symtab.keys table))
    5.40 +    |> Pretty.writeln;
    5.41  end;
    5.42  
    5.43  structure StyleData = TheoryDataFun(StyleArgs);
    5.44  
    5.45  (* accessors *)
    5.46 -fun get_style thy name =
    5.47 -  case Library.assoc_string ((StyleData.get thy), name)
    5.48 -    of NONE => raise (STYLE ("no style named " ^ name))
    5.49 +fun lookup_style thy name =
    5.50 +  case Symtab.lookup ((StyleData.get thy), name)
    5.51 +    of NONE => raise (ERROR_MESSAGE ("no style named " ^ name))
    5.52       | SOME style => style
    5.53  
    5.54 -fun put_style name style thy =
    5.55 -  StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy;
    5.56 +fun update_style name style thy =
    5.57 +  thy
    5.58 +  |> StyleData.put (Symtab.update ((name, style), StyleData.get thy));
    5.59  
    5.60  (* predefined styles *)
    5.61 -fun style_lhs (Const ("==", _) $ t $ _) = t
    5.62 -  | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t
    5.63 -  | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t
    5.64 -  | style_lhs (_ $ t $ _) = t
    5.65 -  | style_lhs _ = error ("Binary operator expected")
    5.66 -
    5.67 -fun style_rhs (Const ("==", _) $ _ $ t) = t
    5.68 -  | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t
    5.69 -  | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t
    5.70 -  | style_rhs (_ $ _ $ t) = t
    5.71 -  | style_rhs _ = error ("Binary operator expected")
    5.72 +fun style_binargs ctxt t =
    5.73 +  let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
    5.74 +    case concl of (_ $ l $ r) => (l, r)
    5.75 +        | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
    5.76 +  end;
    5.77  
    5.78  (* initialization *)
    5.79  val _ = Context.add_setup [StyleData.init,
    5.80 -  put_style "lhs" style_lhs,
    5.81 -  put_style "rhs" style_rhs,
    5.82 -  put_style "conclusion" Logic.strip_imp_concl
    5.83 +  update_style "lhs" (fst oo style_binargs),
    5.84 +  update_style "rhs" (snd oo style_binargs),
    5.85 +  update_style "conclusion" (K Logic.strip_imp_concl)
    5.86  ];
    5.87  
    5.88  end;