Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: term_style.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Thy/term_style.ML
    Author:     Florian Haftmann, TU Muenchen

Styles for term printing.
*)

signature TERM_STYLE =
sig
  val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory
  val parse: (term -> term) context_parser
end;

structure Term_Style: TERM_STYLE =
struct

(* theory data *)

structure Data = Theory_Data
(
  type T = (Proof.context -> term -> term) parser Name_Space.table;
  val empty : T = Name_Space.empty_table "antiquotation_style";
  val extend = I;
  fun merge data : T = Name_Space.merge_tables data;
);

val get_data = Data.get o Proof_Context.theory_of;

fun setup binding style thy =
  Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;

(* style parsing *)

fun parse_single ctxt =
  Parse.token Parse.name ::: Parse.args >> (fn src0 =>
    let
      val (src, parse) = Token.check_src ctxt get_data src0;
      val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
    in f ctxt end);

val parse = Args.context :|-- (fn ctxt => Scan.lift
  (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
      >> fold I
  || Scan.succeed I));

(* predefined styles *)

fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
  let
    val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t);
  in
    (case concl of
      _ $ l $ r => proj (l, r)
    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
  end);

val style_prem = Parse.nat >> (fn i => fn ctxt => fn t =>
  let
    val prems = Logic.strip_imp_prems t;
  in
    if i <= length prems then nth prems (i - 1)
    else
      error ("Not enough premises for prem " ^ string_of_int i ^
        " in propositon: " ^ Syntax.string_of_term ctxt t)
  end);

fun sub_symbols (d :: s :: ss) =
      if Symbol.is_ascii_digit d andalso not (Symbol.is_control s)
      then d :: "\<^sub>" :: sub_symbols (s :: ss)
      else d :: s :: ss
  | sub_symbols cs = cs;

val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;

fun sub_term (Free (n, T)) = Free (sub_name n, T)
  | sub_term (Var ((n, idx), T)) =
      if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
      else Var ((sub_name n, 0), T)
  | sub_term (t $ u) = sub_term t $ sub_term u
  | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
  | sub_term t = t;

val _ = Theory.setup
(setup \<^binding>\<open>lhs\<close> (style_lhs_rhs fst) #>
  setup \<^binding>\<open>rhs\<close> (style_lhs_rhs snd) #>
  setup \<^binding>\<open>prem\<close> style_prem #>
  setup \<^binding>\<open>concl\<close> (Scan.succeed (K Logic.strip_imp_concl)) #>
  setup \<^binding>\<open>sub\<close> (Scan.succeed (K sub_term)));

end;

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.