src/Pure/Isar/term_style.ML
author haftmann
Wed Jun 01 10:52:17 2005 +0200 (2005-06-01 ago)
changeset 16167 b2e4c4058b71
parent 16165 dbe9ee8ffcdd
child 16424 18a07ad8fea8
permissions -rw-r--r--
renamed premise* to prem
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
haftmann@16167
    60
fun style_parm_premise i ctxt t =
nipkow@16160
    61
  let val prems = Logic.strip_imp_prems t
haftmann@16165
    62
  in if i <= length prems then List.nth(prems, i-1)
haftmann@16167
    63
     else error ("Not enough premises for prem" ^ string_of_int i ^
haftmann@16167
    64
                 " in propositon: " ^ ProofContext.string_of_term ctxt t)
nipkow@16160
    65
  end;
haftmann@16167
    66
wenzelm@15990
    67
val _ = Context.add_setup
wenzelm@15990
    68
 [add_style "lhs" (fst oo style_binargs),
wenzelm@15990
    69
  add_style "rhs" (snd oo style_binargs),
haftmann@16167
    70
  add_style "prem1" (style_parm_premise 1),
haftmann@16167
    71
  add_style "prem2" (style_parm_premise 2),
haftmann@16167
    72
  add_style "prem3" (style_parm_premise 3),
haftmann@16167
    73
  add_style "prem4" (style_parm_premise 4),
haftmann@16167
    74
  add_style "prem5" (style_parm_premise 5),
haftmann@16167
    75
  add_style "prem6" (style_parm_premise 6),
haftmann@16167
    76
  add_style "prem7" (style_parm_premise 7),
haftmann@16167
    77
  add_style "prem8" (style_parm_premise 8),
haftmann@16167
    78
  add_style "prem9" (style_parm_premise 9),
haftmann@16165
    79
  add_style "concl" (K Logic.strip_imp_concl)];
haftmann@15918
    80
haftmann@15918
    81
end;