src/Pure/Isar/term_style.ML
author schirmer
Wed Sep 14 23:04:59 2005 +0200 (2005-09-14 ago)
changeset 17392 a639d580b34b
parent 17221 6cd180204582
child 17412 e26cb20ef0cc
permissions -rw-r--r--
added prem10 - prem19
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@17221
     5
Styles for terms, to use with the "term_style" and "thm_style"
wenzelm@17221
     6
antiquotations.
haftmann@15918
     7
*)
haftmann@15918
     8
haftmann@15960
     9
signature TERM_STYLE =
haftmann@15918
    10
sig
wenzelm@15990
    11
  val the_style: theory -> string -> (Proof.context -> term -> term)
wenzelm@15990
    12
  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
wenzelm@15990
    13
  val print_styles: theory -> unit
haftmann@15918
    14
end;
haftmann@15918
    15
haftmann@15960
    16
structure TermStyle: TERM_STYLE =
haftmann@15918
    17
struct
haftmann@15918
    18
wenzelm@15990
    19
(* style data *)
wenzelm@15990
    20
wenzelm@15990
    21
fun err_dup_styles names =
wenzelm@15990
    22
  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
wenzelm@15990
    23
wenzelm@16424
    24
structure StyleData = TheoryDataFun
wenzelm@16424
    25
(struct
wenzelm@16541
    26
  val name = "Isar/antiquote_style";
wenzelm@15990
    27
  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
haftmann@15960
    28
  val empty = Symtab.empty;
haftmann@15918
    29
  val copy = I;
wenzelm@16424
    30
  val extend = I;
wenzelm@16424
    31
  fun merge _ tabs = Symtab.merge eq_snd tabs
wenzelm@15990
    32
    handle Symtab.DUPS dups => err_dup_styles dups;
wenzelm@15990
    33
  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
wenzelm@16424
    34
end);
haftmann@15918
    35
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@17221
    43
  (case Symtab.curried_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@17221
    48
  StyleData.map (Symtab.curried_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 =
wenzelm@16424
    55
  let
wenzelm@16424
    56
    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
wenzelm@16424
    57
      (Logic.strip_imp_concl t)
wenzelm@16424
    58
  in
haftmann@15960
    59
    case concl of (_ $ l $ r) => (l, r)
wenzelm@15990
    60
    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
haftmann@15960
    61
  end;
haftmann@15918
    62
haftmann@16167
    63
fun style_parm_premise i ctxt t =
wenzelm@16424
    64
  let val prems = Logic.strip_imp_prems t in
wenzelm@16424
    65
    if i <= length prems then List.nth (prems, i - 1)
wenzelm@16424
    66
    else error ("Not enough premises for prem" ^ string_of_int i ^
wenzelm@16424
    67
      " in propositon: " ^ ProofContext.string_of_term ctxt t)
nipkow@16160
    68
  end;
haftmann@16167
    69
wenzelm@15990
    70
val _ = Context.add_setup
wenzelm@15990
    71
 [add_style "lhs" (fst oo style_binargs),
wenzelm@15990
    72
  add_style "rhs" (snd oo style_binargs),
haftmann@16167
    73
  add_style "prem1" (style_parm_premise 1),
haftmann@16167
    74
  add_style "prem2" (style_parm_premise 2),
haftmann@16167
    75
  add_style "prem3" (style_parm_premise 3),
haftmann@16167
    76
  add_style "prem4" (style_parm_premise 4),
haftmann@16167
    77
  add_style "prem5" (style_parm_premise 5),
haftmann@16167
    78
  add_style "prem6" (style_parm_premise 6),
haftmann@16167
    79
  add_style "prem7" (style_parm_premise 7),
haftmann@16167
    80
  add_style "prem8" (style_parm_premise 8),
haftmann@16167
    81
  add_style "prem9" (style_parm_premise 9),
schirmer@17392
    82
  add_style "prem10" (style_parm_premise 10),
schirmer@17392
    83
  add_style "prem11" (style_parm_premise 11),
schirmer@17392
    84
  add_style "prem12" (style_parm_premise 12),
schirmer@17392
    85
  add_style "prem13" (style_parm_premise 13),
schirmer@17392
    86
  add_style "prem14" (style_parm_premise 14),
schirmer@17392
    87
  add_style "prem15" (style_parm_premise 15),
schirmer@17392
    88
  add_style "prem16" (style_parm_premise 16),
schirmer@17392
    89
  add_style "prem17" (style_parm_premise 17),
schirmer@17392
    90
  add_style "prem18" (style_parm_premise 18),
schirmer@17392
    91
  add_style "prem19" (style_parm_premise 19),
haftmann@16165
    92
  add_style "concl" (K Logic.strip_imp_concl)];
haftmann@15918
    93
end;