src/Pure/Isar/term_style.ML
author wenzelm
Wed Jun 22 19:41:29 2005 +0200 (2005-06-22 ago)
changeset 16541 d539d47cce69
parent 16424 18a07ad8fea8
child 17221 6cd180204582
permissions -rw-r--r--
renamed data kind;
haftmann@15918
     1
(*  Title:      Pure/Isar/term_style.ML
haftmann@15918
     2
    ID:         $Id$
haftmann@15918
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@15918
     4
wenzelm@15990
     5
Styles for terms, to use with the "term_style" and "thm_style" antiquotations.
haftmann@15918
     6
*)
haftmann@15918
     7
haftmann@15960
     8
signature TERM_STYLE =
haftmann@15918
     9
sig
wenzelm@15990
    10
  val the_style: theory -> string -> (Proof.context -> term -> term)
wenzelm@15990
    11
  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
wenzelm@15990
    12
  val print_styles: theory -> unit
haftmann@15918
    13
end;
haftmann@15918
    14
haftmann@15960
    15
structure TermStyle: TERM_STYLE =
haftmann@15918
    16
struct
haftmann@15918
    17
wenzelm@15990
    18
(* style data *)
wenzelm@15990
    19
wenzelm@15990
    20
fun err_dup_styles names =
wenzelm@15990
    21
  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
wenzelm@15990
    22
wenzelm@16424
    23
structure StyleData = TheoryDataFun
wenzelm@16424
    24
(struct
wenzelm@16541
    25
  val name = "Isar/antiquote_style";
wenzelm@15990
    26
  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
haftmann@15960
    27
  val empty = Symtab.empty;
haftmann@15918
    28
  val copy = I;
wenzelm@16424
    29
  val extend = I;
wenzelm@16424
    30
  fun merge _ tabs = Symtab.merge eq_snd tabs
wenzelm@15990
    31
    handle Symtab.DUPS dups => err_dup_styles dups;
wenzelm@15990
    32
  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
wenzelm@16424
    33
end);
haftmann@15918
    34
wenzelm@15990
    35
val _ = Context.add_setup [StyleData.init];
wenzelm@15990
    36
val print_styles = StyleData.print;
wenzelm@15990
    37
haftmann@15918
    38
haftmann@15918
    39
(* accessors *)
haftmann@15918
    40
wenzelm@15990
    41
fun the_style thy name =
wenzelm@15990
    42
  (case Symtab.lookup (StyleData.get thy, name) of
wenzelm@15990
    43
    NONE => error ("Unknown antiquote style: " ^ quote name)
wenzelm@15990
    44
  | SOME (style, _) => style);
wenzelm@15990
    45
wenzelm@15990
    46
fun add_style name style thy =
wenzelm@15990
    47
  StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
wenzelm@15990
    48
    handle Symtab.DUP _ => err_dup_styles [name];
wenzelm@15990
    49
haftmann@15918
    50
haftmann@15918
    51
(* predefined styles *)
wenzelm@15990
    52
haftmann@15960
    53
fun style_binargs ctxt t =
wenzelm@16424
    54
  let
wenzelm@16424
    55
    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
wenzelm@16424
    56
      (Logic.strip_imp_concl t)
wenzelm@16424
    57
  in
haftmann@15960
    58
    case concl of (_ $ l $ r) => (l, r)
wenzelm@15990
    59
    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
haftmann@15960
    60
  end;
haftmann@15918
    61
haftmann@16167
    62
fun style_parm_premise i ctxt t =
wenzelm@16424
    63
  let val prems = Logic.strip_imp_prems t in
wenzelm@16424
    64
    if i <= length prems then List.nth (prems, i - 1)
wenzelm@16424
    65
    else error ("Not enough premises for prem" ^ string_of_int i ^
wenzelm@16424
    66
      " in propositon: " ^ ProofContext.string_of_term ctxt t)
nipkow@16160
    67
  end;
haftmann@16167
    68
wenzelm@15990
    69
val _ = Context.add_setup
wenzelm@15990
    70
 [add_style "lhs" (fst oo style_binargs),
wenzelm@15990
    71
  add_style "rhs" (snd oo style_binargs),
haftmann@16167
    72
  add_style "prem1" (style_parm_premise 1),
haftmann@16167
    73
  add_style "prem2" (style_parm_premise 2),
haftmann@16167
    74
  add_style "prem3" (style_parm_premise 3),
haftmann@16167
    75
  add_style "prem4" (style_parm_premise 4),
haftmann@16167
    76
  add_style "prem5" (style_parm_premise 5),
haftmann@16167
    77
  add_style "prem6" (style_parm_premise 6),
haftmann@16167
    78
  add_style "prem7" (style_parm_premise 7),
haftmann@16167
    79
  add_style "prem8" (style_parm_premise 8),
haftmann@16167
    80
  add_style "prem9" (style_parm_premise 9),
haftmann@16165
    81
  add_style "concl" (K Logic.strip_imp_concl)];
haftmann@15918
    82
haftmann@15918
    83
end;