src/Pure/Isar/term_style.ML
author nipkow
Wed Jun 01 08:44:25 2005 +0200 (2005-06-01 ago)
changeset 16160 833f4160130e
parent 15990 4ef32dcbb44f
child 16165 dbe9ee8ffcdd
permissions -rw-r--r--
added premise<i>
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
haftmann@15918
    23
structure StyleArgs =
haftmann@15918
    24
struct
haftmann@15918
    25
  val name = "Isar/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;
haftmann@15918
    29
  val prep_ext = I;
wenzelm@15990
    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));
haftmann@15918
    33
end;
haftmann@15918
    34
haftmann@15918
    35
structure StyleData = TheoryDataFun(StyleArgs);
wenzelm@15990
    36
val _ = Context.add_setup [StyleData.init];
wenzelm@15990
    37
val print_styles = StyleData.print;
wenzelm@15990
    38
haftmann@15918
    39
haftmann@15918
    40
(* accessors *)
haftmann@15918
    41
wenzelm@15990
    42
fun the_style thy name =
wenzelm@15990
    43
  (case Symtab.lookup (StyleData.get thy, name) of
wenzelm@15990
    44
    NONE => error ("Unknown antiquote style: " ^ quote name)
wenzelm@15990
    45
  | SOME (style, _) => style);
wenzelm@15990
    46
wenzelm@15990
    47
fun add_style name style thy =
wenzelm@15990
    48
  StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
wenzelm@15990
    49
    handle Symtab.DUP _ => err_dup_styles [name];
wenzelm@15990
    50
haftmann@15918
    51
haftmann@15918
    52
(* predefined styles *)
wenzelm@15990
    53
haftmann@15960
    54
fun style_binargs ctxt t =
haftmann@15960
    55
  let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
haftmann@15960
    56
    case concl of (_ $ l $ r) => (l, r)
wenzelm@15990
    57
    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
haftmann@15960
    58
  end;
haftmann@15918
    59
nipkow@16160
    60
fun premise i _ t =
nipkow@16160
    61
  let val prems = Logic.strip_imp_prems t
nipkow@16160
    62
  in if i <= length prems then List.nth(prems,i-1)
nipkow@16160
    63
     else error ("Not enough premises: premise" ^ string_of_int i)
nipkow@16160
    64
  end;
nipkow@16160
    65
 
wenzelm@15990
    66
val _ = Context.add_setup
wenzelm@15990
    67
 [add_style "lhs" (fst oo style_binargs),
wenzelm@15990
    68
  add_style "rhs" (snd oo style_binargs),
nipkow@16160
    69
  add_style "premise1" (premise 1),
nipkow@16160
    70
  add_style "premise2" (premise 2),
nipkow@16160
    71
  add_style "premise3" (premise 3),
nipkow@16160
    72
  add_style "premise4" (premise 4),
nipkow@16160
    73
  add_style "premise5" (premise 5),
nipkow@16160
    74
  add_style "premise6" (premise 6),
nipkow@16160
    75
  add_style "premise7" (premise 7),
nipkow@16160
    76
  add_style "premise8" (premise 8),
nipkow@16160
    77
  add_style "premise9" (premise 9),
wenzelm@15990
    78
  add_style "conclusion" (K Logic.strip_imp_concl)];
haftmann@15918
    79
haftmann@15918
    80
end;