added antiquotation abbrev;
authorwenzelm
Sat Dec 09 18:05:36 2006 +0100 (2006-12-09)
changeset 21717410ca6910f6f
parent 21716 8fcacb0e3b15
child 21718 43b935d6fb5a
added antiquotation abbrev;
NEWS
doc-src/IsarRef/syntax.tex
src/Pure/Isar/isar_output.ML
     1.1 --- a/NEWS	Sat Dec 09 18:05:34 2006 +0100
     1.2 +++ b/NEWS	Sat Dec 09 18:05:36 2006 +0100
     1.3 @@ -45,13 +45,18 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Added antiquotation @{theory name} which prints the name $A$, after
     1.8 -checking that it refers to a valid ancestor theory in the current
     1.9 -context.
    1.10 +* Added antiquotation @{theory name} which prints the given name,
    1.11 +after checking that it refers to a valid ancestor theory in the
    1.12 +current context.
    1.13  
    1.14  * Added antiquotations @{ML_type text} and @{ML_struct text} which
    1.15  check the given source text as ML type/structure, printing verbatim.
    1.16  
    1.17 +* Added antiquotation @{abbrev "c args"} which prints the abbreviation
    1.18 +"c args == rhs" given in the current context.  (Any number of
    1.19 +arguments on the LHS may be given.)
    1.20 +
    1.21 +
    1.22  
    1.23  *** Pure ***
    1.24  
     2.1 --- a/doc-src/IsarRef/syntax.tex	Sat Dec 09 18:05:34 2006 +0100
     2.2 +++ b/doc-src/IsarRef/syntax.tex	Sat Dec 09 18:05:36 2006 +0100
     2.3 @@ -435,6 +435,7 @@
     2.4    prop & : & \isarantiq \\
     2.5    term & : & \isarantiq \\
     2.6    const & : & \isarantiq \\
     2.7 +  abbrev & : & \isarantiq \\
     2.8    typeof & : & \isarantiq \\
     2.9    typ & : & \isarantiq \\
    2.10    thm_style & : & \isarantiq \\
    2.11 @@ -465,7 +466,7 @@
    2.12  which are easier to read.
    2.13  
    2.14  \indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
    2.15 -\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
    2.16 +\indexisarant{abbrev}\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
    2.17  \indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
    2.18  \indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
    2.19  \indexisarant{ML-type}\indexisarant{ML-struct}
    2.20 @@ -480,6 +481,7 @@
    2.21      'prop' options prop |
    2.22      'term' options term |
    2.23      'const' options term |
    2.24 +    'abbrev' options term |
    2.25      'typeof' options term |
    2.26      'typ' options type |
    2.27      'thm\_style' options name thmref |
    2.28 @@ -517,6 +519,9 @@
    2.29  \item [$\at\{term~t\}$] prints a well-typed term $t$.
    2.30  
    2.31  \item [$\at\{const~c\}$] prints a well-defined constant $c$.
    2.32 +  
    2.33 +\item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
    2.34 +  $c\,\vec x \equiv rhs$ as defined in the current context.
    2.35  
    2.36  \item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
    2.37  
     3.1 --- a/src/Pure/Isar/isar_output.ML	Sat Dec 09 18:05:34 2006 +0100
     3.2 +++ b/src/Pure/Isar/isar_output.ML	Sat Dec 09 18:05:36 2006 +0100
     3.3 @@ -441,6 +441,8 @@
     3.4  val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
     3.5  
     3.6  fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     3.7 +fun pretty_term_abbrev ctxt =
     3.8 +  ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
     3.9  
    3.10  fun pretty_term_typ ctxt t =
    3.11    ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
    3.12 @@ -451,6 +453,16 @@
    3.13    if Term.is_Const t then pretty_term ctxt t
    3.14    else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
    3.15  
    3.16 +fun pretty_abbrev ctxt t =
    3.17 +  let
    3.18 +    fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
    3.19 +    val (head, args) = Term.strip_comb t;
    3.20 +    val (c, T) = Term.dest_Const head handle TERM _ => err ();
    3.21 +    val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
    3.22 +      handle TYPE _ => err ();
    3.23 +    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
    3.24 +  in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
    3.25 +
    3.26  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    3.27  
    3.28  fun pretty_term_style ctxt (name, t) =
    3.29 @@ -517,6 +529,7 @@
    3.30    ("term_type", args Args.term (output pretty_term_typ)),
    3.31    ("typeof", args Args.term (output pretty_term_typeof)),
    3.32    ("const", args Args.term (output pretty_term_const)),
    3.33 +  ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
    3.34    ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
    3.35    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    3.36    ("goals", output_goals true),