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_keyword>‹cartouche› ""
    (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_syntax>‹Char›, String_Syntax.mk_bits_syntax 8 c) end;

    fun mk_string [] = Const (\<^const_syntax>‹Nil›, \<^typ>‹string›)
      | mk_string (s :: ss) =
          Syntax.const \<^const_syntax>‹Cons› $ 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