src/Pure/Thy/term_style.ML
author wenzelm
Fri Jan 19 22:08:15 2007 +0100 (2007-01-19)
changeset 22107 926afa3361e1
child 22846 fb79144af9a3
permissions -rw-r--r--
renamed Isar/term_style.ML to Thy/term_style.ML;
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@22107
    21
fun err_dup_styles names =
wenzelm@22107
    22
  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
wenzelm@22107
    23
wenzelm@22107
    24
structure StyleData = TheoryDataFun
wenzelm@22107
    25
(struct
wenzelm@22107
    26
  val name = "Isar/antiquote_style";
wenzelm@22107
    27
  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
wenzelm@22107
    28
  val empty = Symtab.empty;
wenzelm@22107
    29
  val copy = I;
wenzelm@22107
    30
  val extend = I;
wenzelm@22107
    31
  fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
wenzelm@22107
    32
    handle Symtab.DUPS dups => err_dup_styles dups;
wenzelm@22107
    33
  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
wenzelm@22107
    34
end);
wenzelm@22107
    35
wenzelm@22107
    36
val _ = Context.add_setup StyleData.init;
wenzelm@22107
    37
val print_styles = StyleData.print;
wenzelm@22107
    38
wenzelm@22107
    39
wenzelm@22107
    40
(* accessors *)
wenzelm@22107
    41
wenzelm@22107
    42
fun the_style thy name =
wenzelm@22107
    43
  (case Symtab.lookup (StyleData.get thy) name of
wenzelm@22107
    44
    NONE => error ("Unknown antiquote style: " ^ quote name)
wenzelm@22107
    45
  | SOME (style, _) => style);
wenzelm@22107
    46
wenzelm@22107
    47
fun add_style name style thy =
wenzelm@22107
    48
  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
wenzelm@22107
    49
    handle Symtab.DUP _ => err_dup_styles [name];
wenzelm@22107
    50
wenzelm@22107
    51
wenzelm@22107
    52
(* predefined styles *)
wenzelm@22107
    53
wenzelm@22107
    54
fun style_binargs ctxt t =
wenzelm@22107
    55
  let
wenzelm@22107
    56
    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
wenzelm@22107
    57
      (Logic.strip_imp_concl t)
wenzelm@22107
    58
  in
wenzelm@22107
    59
    case concl of (_ $ l $ r) => (l, r)
wenzelm@22107
    60
    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
wenzelm@22107
    61
  end;
wenzelm@22107
    62
wenzelm@22107
    63
fun style_parm_premise i ctxt t =
wenzelm@22107
    64
  let val prems = Logic.strip_imp_prems t in
wenzelm@22107
    65
    if i <= length prems then nth prems (i - 1)
wenzelm@22107
    66
    else error ("Not enough premises for prem" ^ string_of_int i ^
wenzelm@22107
    67
      " in propositon: " ^ ProofContext.string_of_term ctxt t)
wenzelm@22107
    68
  end;
wenzelm@22107
    69
wenzelm@22107
    70
val _ = Context.add_setup
wenzelm@22107
    71
 (add_style "lhs" (fst oo style_binargs) #>
wenzelm@22107
    72
  add_style "rhs" (snd oo style_binargs) #>
wenzelm@22107
    73
  add_style "prem1" (style_parm_premise 1) #>
wenzelm@22107
    74
  add_style "prem2" (style_parm_premise 2) #>
wenzelm@22107
    75
  add_style "prem3" (style_parm_premise 3) #>
wenzelm@22107
    76
  add_style "prem4" (style_parm_premise 4) #>
wenzelm@22107
    77
  add_style "prem5" (style_parm_premise 5) #>
wenzelm@22107
    78
  add_style "prem6" (style_parm_premise 6) #>
wenzelm@22107
    79
  add_style "prem7" (style_parm_premise 7) #>
wenzelm@22107
    80
  add_style "prem8" (style_parm_premise 8) #>
wenzelm@22107
    81
  add_style "prem9" (style_parm_premise 9) #>
wenzelm@22107
    82
  add_style "prem10" (style_parm_premise 10) #>
wenzelm@22107
    83
  add_style "prem11" (style_parm_premise 11) #>
wenzelm@22107
    84
  add_style "prem12" (style_parm_premise 12) #>
wenzelm@22107
    85
  add_style "prem13" (style_parm_premise 13) #>
wenzelm@22107
    86
  add_style "prem14" (style_parm_premise 14) #>
wenzelm@22107
    87
  add_style "prem15" (style_parm_premise 15) #>
wenzelm@22107
    88
  add_style "prem16" (style_parm_premise 16) #>
wenzelm@22107
    89
  add_style "prem17" (style_parm_premise 17) #>
wenzelm@22107
    90
  add_style "prem18" (style_parm_premise 18) #>
wenzelm@22107
    91
  add_style "prem19" (style_parm_premise 19) #>
wenzelm@22107
    92
  add_style "concl" (K Logic.strip_imp_concl));
wenzelm@22107
    93
wenzelm@22107
    94
end;