src/Pure/Thy/term_style.ML
author wenzelm
Tue Mar 18 11:27:09 2014 +0100 (2014-03-18)
changeset 56201 dd2df97b379b
parent 56032 b034b9f0fa2a
child 56203 76c72f4d0667
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Thy/term_style.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Styles for term printing.
     5 *)
     6 
     7 signature TERM_STYLE =
     8 sig
     9   val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory
    10   val parse: (term -> term) context_parser
    11 end;
    12 
    13 structure Term_Style: TERM_STYLE =
    14 struct
    15 
    16 (* theory data *)
    17 
    18 structure Data = Theory_Data
    19 (
    20   type T = (Proof.context -> term -> term) parser Name_Space.table;
    21   val empty : T = Name_Space.empty_table "antiquotation_style";
    22   val extend = I;
    23   fun merge data : T = Name_Space.merge_tables data;
    24 );
    25 
    26 val get_data = Data.get o Proof_Context.theory_of;
    27 val get_style = Name_Space.get o get_data;
    28 
    29 fun setup binding style thy =
    30   Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;
    31 
    32 
    33 (* style parsing *)
    34 
    35 fun parse_single ctxt =
    36   Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
    37     let
    38       val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
    39       val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
    40     in f ctxt end);
    41 
    42 val parse = Args.context :|-- (fn ctxt => Scan.lift
    43   (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    44       >> fold I
    45   || Scan.succeed I));
    46 
    47 
    48 (* predefined styles *)
    49 
    50 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
    51   let
    52     val concl =
    53       Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
    54   in
    55     (case concl of
    56       _ $ l $ r => proj (l, r)
    57     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
    58   end);
    59 
    60 val style_prem = Parse.nat >> (fn i => fn ctxt => fn t =>
    61   let
    62     val prems = Logic.strip_imp_prems t;
    63   in
    64     if i <= length prems then nth prems (i - 1)
    65     else
    66       error ("Not enough premises for prem " ^ string_of_int i ^
    67         " in propositon: " ^ Syntax.string_of_term ctxt t)
    68   end);
    69 
    70 fun sub_symbols (d :: s :: ss) =
    71       if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
    72       then d :: "\\<^sub>" :: sub_symbols (s :: ss)
    73       else d :: s :: ss
    74   | sub_symbols cs = cs;
    75 
    76 val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
    77 
    78 fun sub_term (Free (n, T)) = Free (sub_name n, T)
    79   | sub_term (Var ((n, idx), T)) =
    80       if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
    81       else Var ((sub_name n, 0), T)
    82   | sub_term (t $ u) = sub_term t $ sub_term u
    83   | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
    84   | sub_term t = t;
    85 
    86 val _ = Theory.setup
    87  (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
    88   setup (Binding.name "rhs") (style_lhs_rhs snd) #>
    89   setup (Binding.name "prem") style_prem #>
    90   setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
    91   setup (Binding.name "sub") (Scan.succeed (K sub_term)));
    92 
    93 end;