src/Pure/Thy/term_style.ML
author wenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655 d2d1138e0ddc
parent 23577 c5b93c69afd3
child 24920 2a45e400fdad
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm@22107
     1
(*  Title:      Pure/Thy/term_style.ML
wenzelm@22107
     2
    ID:         $Id$
wenzelm@22107
     3
    Author:     Florian Haftmann, TU Muenchen
wenzelm@22107
     4
wenzelm@22107
     5
Styles for terms, to use with the "term_style" and "thm_style"
wenzelm@22107
     6
antiquotations.
wenzelm@22107
     7
*)
wenzelm@22107
     8
wenzelm@22107
     9
signature TERM_STYLE =
wenzelm@22107
    10
sig
wenzelm@22107
    11
  val the_style: theory -> string -> (Proof.context -> term -> term)
wenzelm@22107
    12
  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
wenzelm@22107
    13
  val print_styles: theory -> unit
wenzelm@22107
    14
end;
wenzelm@22107
    15
wenzelm@22107
    16
structure TermStyle: TERM_STYLE =
wenzelm@22107
    17
struct
wenzelm@22107
    18
wenzelm@22107
    19
(* style data *)
wenzelm@22107
    20
wenzelm@23655
    21
fun err_dup_style name =
wenzelm@23655
    22
  error ("Duplicate declaration of antiquote style: " ^ quote name);
wenzelm@22107
    23
wenzelm@22107
    24
structure StyleData = TheoryDataFun
wenzelm@22846
    25
(
wenzelm@22107
    26
  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
wenzelm@22107
    27
  val empty = Symtab.empty;
wenzelm@22107
    28
  val copy = I;
wenzelm@22107
    29
  val extend = I;
wenzelm@23577
    30
  fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
wenzelm@23655
    31
    handle Symtab.DUP dup => err_dup_style dup;
wenzelm@22846
    32
);
wenzelm@22107
    33
wenzelm@22846
    34
fun print_styles thy =
wenzelm@22846
    35
  Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
wenzelm@22107
    36
wenzelm@22107
    37
wenzelm@22107
    38
(* accessors *)
wenzelm@22107
    39
wenzelm@22107
    40
fun the_style thy name =
wenzelm@22107
    41
  (case Symtab.lookup (StyleData.get thy) name of
wenzelm@22107
    42
    NONE => error ("Unknown antiquote style: " ^ quote name)
wenzelm@22107
    43
  | SOME (style, _) => style);
wenzelm@22107
    44
wenzelm@22107
    45
fun add_style name style thy =
wenzelm@22107
    46
  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
wenzelm@23655
    47
    handle Symtab.DUP _ => err_dup_style name;
wenzelm@22107
    48
wenzelm@22107
    49
wenzelm@22107
    50
(* predefined styles *)
wenzelm@22107
    51
wenzelm@22107
    52
fun style_binargs ctxt t =
wenzelm@22107
    53
  let
wenzelm@22107
    54
    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
wenzelm@22107
    55
      (Logic.strip_imp_concl t)
wenzelm@22107
    56
  in
wenzelm@22107
    57
    case concl of (_ $ l $ r) => (l, r)
wenzelm@22107
    58
    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
wenzelm@22107
    59
  end;
wenzelm@22107
    60
wenzelm@22107
    61
fun style_parm_premise i ctxt t =
wenzelm@22107
    62
  let val prems = Logic.strip_imp_prems t in
wenzelm@22107
    63
    if i <= length prems then nth prems (i - 1)
wenzelm@22107
    64
    else error ("Not enough premises for prem" ^ string_of_int i ^
wenzelm@22107
    65
      " in propositon: " ^ ProofContext.string_of_term ctxt t)
wenzelm@22107
    66
  end;
wenzelm@22107
    67
wenzelm@22107
    68
val _ = Context.add_setup
wenzelm@22107
    69
 (add_style "lhs" (fst oo style_binargs) #>
wenzelm@22107
    70
  add_style "rhs" (snd oo style_binargs) #>
wenzelm@22107
    71
  add_style "prem1" (style_parm_premise 1) #>
wenzelm@22107
    72
  add_style "prem2" (style_parm_premise 2) #>
wenzelm@22107
    73
  add_style "prem3" (style_parm_premise 3) #>
wenzelm@22107
    74
  add_style "prem4" (style_parm_premise 4) #>
wenzelm@22107
    75
  add_style "prem5" (style_parm_premise 5) #>
wenzelm@22107
    76
  add_style "prem6" (style_parm_premise 6) #>
wenzelm@22107
    77
  add_style "prem7" (style_parm_premise 7) #>
wenzelm@22107
    78
  add_style "prem8" (style_parm_premise 8) #>
wenzelm@22107
    79
  add_style "prem9" (style_parm_premise 9) #>
wenzelm@22107
    80
  add_style "prem10" (style_parm_premise 10) #>
wenzelm@22107
    81
  add_style "prem11" (style_parm_premise 11) #>
wenzelm@22107
    82
  add_style "prem12" (style_parm_premise 12) #>
wenzelm@22107
    83
  add_style "prem13" (style_parm_premise 13) #>
wenzelm@22107
    84
  add_style "prem14" (style_parm_premise 14) #>
wenzelm@22107
    85
  add_style "prem15" (style_parm_premise 15) #>
wenzelm@22107
    86
  add_style "prem16" (style_parm_premise 16) #>
wenzelm@22107
    87
  add_style "prem17" (style_parm_premise 17) #>
wenzelm@22107
    88
  add_style "prem18" (style_parm_premise 18) #>
wenzelm@22107
    89
  add_style "prem19" (style_parm_premise 19) #>
wenzelm@22107
    90
  add_style "concl" (K Logic.strip_imp_concl));
wenzelm@22107
    91
wenzelm@22107
    92
end;