Theory Cartouche_Examples

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

section ‹Some examples with text cartouches›

theory Cartouche_Examples
imports Main
keywords
  "cartouche" :: diag and
  "text_cartouche" :: thy_decl
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 Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral 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›

ML ‹
  Outer_Syntax.command
    @{command_keyword text_cartouche} ""
    (Parse.opt_target -- Parse.input Parse.cartouche
      >> Thy_Output.document_command {markdown = true})
›

text_cartouche
‹
  @{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.range_of source) "tactic" "Proof.context -> tactic"
          "Context.map_proof (ML_Tactic.set tactic)"
          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
    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