Theory HOL-ex.Cartouche_Examples

(*  Title:      HOL/ex/Cartouche_Examples.thy
    Author:     Makarius
*)

section ‹Some examples with text cartouches›

theory Cartouche_Examples
  imports Main
  keywords "cartouche" :: diag
begin

subsection ‹Regular outer syntax›

text ‹Text cartouches may be used in the outer syntax category text›,
  as alternative to the traditional verbatim› tokens.  An example is
  this text block.›  ― ‹The same works for small side-comments.›

notepad
begin
  txt ‹Cartouches work as additional syntax for embedded language tokens
    (types, terms, props) and as a replacement for the altstring› category
    (for literal fact references). For example:›

  fix x y :: 'a
  assume x = y
  note x = y
  have x = y by (rule x = y)
  from x = y have x = y .

  txt ‹Of course, this can be nested inside formal comments and
    antiquotations, e.g. like this @{thm x = y} or this @{thm sym
    [OF x = y]}.›

  have x = y
    by (tactic resolve_tac context @{thms x = y} 1)
      ― ‹more cartouches involving ML›
end


subsection ‹Outer syntax: cartouche within command syntax›

ML Outer_Syntax.command command_keywordcartouche ""
    (Parse.cartouche >> (fn s =>
      Toplevel.keep (fn _ => writeln s)))

cartouche ‹abc›
cartouche ‹abc ‹αβγ› xzy›


subsection ‹Inner syntax: string literals via cartouche›

ML local
    fun mk_char (s, pos) =
      let
        val c =
          if Symbol.is_ascii s then ord s
          else if s = "⏎" then 10
          else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
      in list_comb (Syntax.const const_syntaxChar, String_Syntax.mk_bits_syntax 8 c) end;

    fun mk_string [] = Const (const_syntaxNil, typstring)
      | mk_string (s :: ss) =
          Syntax.const const_syntaxCons $ mk_char s $ mk_string ss;

  in
    fun string_tr content args =
      let fun err () = raise TERM ("string_tr", args) in
        (case args of
          [(c as Const (syntax_const‹_constrain›, _)) $ Free (s, _) $ p] =>
            (case Term_Position.decode_position p of
              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
            | NONE => err ())
        | _ => err ())
      end;
  end;

syntax "_cartouche_string" :: cartouche_position  string  ("_")

parse_translation [(syntax_const‹_cartouche_string›,
    K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]

term ‹›
term ‹abc›
term ‹abc› @ ‹xyz›
term ‹⏎›


subsection ‹Alternate outer and inner syntax: string literals›

subsubsection ‹Nested quotes›

syntax "_string_string" :: string_position  string  ("_")

parse_translation [(syntax_const‹_string_string›, K (string_tr Lexicon.explode_string))]

term ""
term "abc"
term "abc" @ "xyz"
term "⏎"
term "\001\010\100"


subsubsection ‹Further nesting: antiquotations›

ML term"";
  term"abc";
  term"abc" @ "xyz";
  term"⏎";
  term"\001\010\100";

text ML(
        term"";
        term"abc";
        term"abc" @ "xyz";
        term"⏎";
        term"\001\010\100"
      )


subsubsection ‹Uniform nesting of sub-languages: document source, ML, term, string literals›

text
ML(
        term"";
        term"abc";
        term"abc" @ "xyz";
        term"⏎";
        term"\001\010\100"
      )


subsection ‹Proof method syntax: ML tactic expression›

ML structure ML_Tactic:
sig
  val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
  val ml_tactic: Input.source -> Proof.context -> tactic
end =
struct
  structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);

  val set = Data.put;

  fun ml_tactic source ctxt =
    let
      val ctxt' = ctxt
        |> Context.proof_map (ML_Context.expression (Input.pos_of source)
          (ML_Lex.read "Theory.local_setup (ML_Tactic.set (fn ctxt: Proof.context => (" @
           ML_Lex.read_source source @ ML_Lex.read ")))"));
    in Data.get ctxt' ctxt end;
end


subsubsection ‹Explicit version: method with cartouche argument›

method_setup ml_tactic = Scan.lift Args.cartouche_input
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))

lemma A  B  B  A
  apply (ml_tactic resolve_tac context @{thms impI} 1)
  apply (ml_tactic eresolve_tac context @{thms conjE} 1)
  apply (ml_tactic resolve_tac context @{thms conjI} 1)
  apply (ml_tactic ALLGOALS (assume_tac context))
  done

lemma A  B  B  A by (ml_tactic blast_tac ctxt 1)

ML @{lemma A  B  B  A by (ml_tactic blast_tac ctxt 1)}

text ML@{lemma A  B  B  A by (ml_tactic blast_tac ctxt 1)}


subsubsection ‹Implicit version: method with special name "cartouche" (dynamic!)›

method_setup "cartouche" = Scan.lift Args.cartouche_input
    >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))

lemma A  B  B  A
  apply resolve_tac context @{thms impI} 1
  apply eresolve_tac context @{thms conjE} 1
  apply resolve_tac context @{thms conjI} 1
  apply ALLGOALS (assume_tac context)
  done

lemma A  B  B  A
  by (resolve_tac context @{thms impI} 1,
    eresolve_tac context @{thms conjE} 1,
    resolve_tac context @{thms conjI} 1,
    assume_tac context 1+)


subsection ‹ML syntax›

text ‹Input source with position information:›
ML val s: Input.source = abc123def456›;
  Output.information ("Look here!" ^ Position.here (Input.pos_of s));

  abc123def456 |> Input.source_explode |> List.app (fn (s, pos) =>
    if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());

end