1(* Title: HOL/ex/Cartouche_Examples.thy 2 Author: Makarius 3*) 4 5section \<open>Some examples with text cartouches\<close> 6 7theory Cartouche_Examples 8imports Main 9keywords 10 "cartouche" :: diag and 11 "text_cartouche" :: thy_decl 12begin 13 14subsection \<open>Regular outer syntax\<close> 15 16text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>, 17 as alternative to the traditional \<open>verbatim\<close> tokens. An example is 18 this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close> 19 20notepad 21begin 22 txt \<open>Cartouches work as additional syntax for embedded language tokens 23 (types, terms, props) and as a replacement for the \<open>altstring\<close> category 24 (for literal fact references). For example:\<close> 25 26 fix x y :: 'a 27 assume \<open>x = y\<close> 28 note \<open>x = y\<close> 29 have \<open>x = y\<close> by (rule \<open>x = y\<close>) 30 from \<open>x = y\<close> have \<open>x = y\<close> . 31 32 txt \<open>Of course, this can be nested inside formal comments and 33 antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym 34 [OF \<open>x = y\<close>]}.\<close> 35 36 have \<open>x = y\<close> 37 by (tactic \<open>resolve_tac \<^context> @{thms \<open>x = y\<close>} 1\<close>) 38 \<comment> \<open>more cartouches involving ML\<close> 39end 40 41 42subsection \<open>Outer syntax: cartouche within command syntax\<close> 43 44ML \<open> 45 Outer_Syntax.command \<^command_keyword>\<open>cartouche\<close> "" 46 (Parse.cartouche >> (fn s => 47 Toplevel.keep (fn _ => writeln s))) 48\<close> 49 50cartouche \<open>abc\<close> 51cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close> 52 53 54subsection \<open>Inner syntax: string literals via cartouche\<close> 55 56ML \<open> 57 local 58 fun mk_char (s, pos) = 59 let 60 val c = 61 if Symbol.is_ascii s then ord s 62 else if s = "\<newline>" then 10 63 else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos); 64 in list_comb (Syntax.const \<^const_syntax>\<open>Char\<close>, String_Syntax.mk_bits_syntax 8 c) end; 65 66 fun mk_string [] = Const (\<^const_syntax>\<open>Nil\<close>, \<^typ>\<open>string\<close>) 67 | mk_string (s :: ss) = 68 Syntax.const \<^const_syntax>\<open>Cons\<close> $ mk_char s $ mk_string ss; 69 70 in 71 fun string_tr content args = 72 let fun err () = raise TERM ("string_tr", args) in 73 (case args of 74 [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] => 75 (case Term_Position.decode_position p of 76 SOME (pos, _) => c $ mk_string (content (s, pos)) $ p 77 | NONE => err ()) 78 | _ => err ()) 79 end; 80 end; 81\<close> 82 83syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close> ("_") 84 85parse_translation \<open> 86 [(\<^syntax_const>\<open>_cartouche_string\<close>, 87 K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] 88\<close> 89 90term \<open>\<open>\<close>\<close> 91term \<open>\<open>abc\<close>\<close> 92term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close> 93term \<open>\<open>\<newline>\<close>\<close> 94 95 96subsection \<open>Alternate outer and inner syntax: string literals\<close> 97 98subsubsection \<open>Nested quotes\<close> 99 100syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close> ("_") 101 102parse_translation \<open> 103 [(\<^syntax_const>\<open>_string_string\<close>, K (string_tr Lexicon.explode_string))] 104\<close> 105 106term \<open>""\<close> 107term \<open>"abc"\<close> 108term \<open>"abc" @ "xyz"\<close> 109term \<open>"\<newline>"\<close> 110term \<open>"\001\010\100"\<close> 111 112 113subsubsection \<open>Further nesting: antiquotations\<close> 114 115ML \<open> 116 \<^term>\<open>""\<close>; 117 \<^term>\<open>"abc"\<close>; 118 \<^term>\<open>"abc" @ "xyz"\<close>; 119 \<^term>\<open>"\<newline>"\<close>; 120 \<^term>\<open>"\001\010\100"\<close>; 121\<close> 122 123text \<open> 124 \<^ML>\<open> 125 ( 126 \<^term>\<open>""\<close>; 127 \<^term>\<open>"abc"\<close>; 128 \<^term>\<open>"abc" @ "xyz"\<close>; 129 \<^term>\<open>"\<newline>"\<close>; 130 \<^term>\<open>"\001\010\100"\<close> 131 ) 132 \<close> 133\<close> 134 135 136subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close> 137 138ML \<open> 139 Outer_Syntax.command 140 \<^command_keyword>\<open>text_cartouche\<close> "" 141 (Parse.opt_target -- Parse.input Parse.cartouche 142 >> Pure_Syn.document_command {markdown = true}) 143\<close> 144 145text_cartouche 146\<open> 147 \<^ML>\<open> 148 ( 149 \<^term>\<open>""\<close>; 150 \<^term>\<open>"abc"\<close>; 151 \<^term>\<open>"abc" @ "xyz"\<close>; 152 \<^term>\<open>"\<newline>"\<close>; 153 \<^term>\<open>"\001\010\100"\<close> 154 ) 155 \<close> 156\<close> 157 158 159subsection \<open>Proof method syntax: ML tactic expression\<close> 160 161ML \<open> 162structure ML_Tactic: 163sig 164 val set: (Proof.context -> tactic) -> Proof.context -> Proof.context 165 val ml_tactic: Input.source -> Proof.context -> tactic 166end = 167struct 168 structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); 169 170 val set = Data.put; 171 172 fun ml_tactic source ctxt = 173 let 174 val ctxt' = ctxt 175 |> Context.proof_map (ML_Context.expression (Input.pos_of source) 176 (ML_Lex.read "Theory.local_setup (ML_Tactic.set (fn ctxt: Proof.context => (" @ 177 ML_Lex.read_source source @ ML_Lex.read ")))")); 178 in Data.get ctxt' ctxt end; 179end 180\<close> 181 182 183subsubsection \<open>Explicit version: method with cartouche argument\<close> 184 185method_setup ml_tactic = \<open> 186 Scan.lift Args.cartouche_input 187 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) 188\<close> 189 190lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> 191 apply (ml_tactic \<open>resolve_tac \<^context> @{thms impI} 1\<close>) 192 apply (ml_tactic \<open>eresolve_tac \<^context> @{thms conjE} 1\<close>) 193 apply (ml_tactic \<open>resolve_tac \<^context> @{thms conjI} 1\<close>) 194 apply (ml_tactic \<open>ALLGOALS (assume_tac \<^context>)\<close>) 195 done 196 197lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>) 198 199ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close> 200 201text \<open>\<^ML>\<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>\<close> 202 203 204subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close> 205 206method_setup "cartouche" = \<open> 207 Scan.lift Args.cartouche_input 208 >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt)) 209\<close> 210 211lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> 212 apply \<open>resolve_tac \<^context> @{thms impI} 1\<close> 213 apply \<open>eresolve_tac \<^context> @{thms conjE} 1\<close> 214 apply \<open>resolve_tac \<^context> @{thms conjI} 1\<close> 215 apply \<open>ALLGOALS (assume_tac \<^context>)\<close> 216 done 217 218lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> 219 by (\<open>resolve_tac \<^context> @{thms impI} 1\<close>, 220 \<open>eresolve_tac \<^context> @{thms conjE} 1\<close>, 221 \<open>resolve_tac \<^context> @{thms conjI} 1\<close>, 222 \<open>assume_tac \<^context> 1\<close>+) 223 224 225subsection \<open>ML syntax\<close> 226 227text \<open>Input source with position information:\<close> 228ML \<open> 229 val s: Input.source = \<open>abc123def456\<close>; 230 Output.information ("Look here!" ^ Position.here (Input.pos_of s)); 231 232 \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) => 233 if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); 234\<close> 235 236end 237