1(* Title: Pure/ML/ml_antiquotations.ML 2 Author: Makarius 3 4Miscellaneous ML antiquotations. 5*) 6 7structure ML_Antiquotations: sig end = 8struct 9 10(* ML support *) 11 12val _ = Theory.setup 13 (ML_Antiquotation.inline \<^binding>\<open>undefined\<close> 14 (Scan.succeed "(raise General.Match)") #> 15 16 ML_Antiquotation.inline \<^binding>\<open>assert\<close> 17 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> 18 19 ML_Antiquotation.declaration \<^binding>\<open>print\<close> 20 (Scan.lift (Scan.optional Args.embedded "Output.writeln")) 21 (fn src => fn output => fn ctxt => 22 let 23 val struct_name = ML_Context.struct_name ctxt; 24 val (_, pos) = Token.name_of_src src; 25 val (a, ctxt') = ML_Context.variant "output" ctxt; 26 val env = 27 "val " ^ a ^ ": string -> unit =\n\ 28 \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ 29 ML_Syntax.print_position pos ^ "));\n"; 30 val body = 31 "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; 32 in (K (env, body), ctxt') end) #> 33 34 ML_Antiquotation.value \<^binding>\<open>rat\<close> 35 (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- 36 Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => 37 "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b)))) 38 39 40(* formal entities *) 41 42val _ = Theory.setup 43 (ML_Antiquotation.value \<^binding>\<open>system_option\<close> 44 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => 45 (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> 46 47 ML_Antiquotation.value \<^binding>\<open>theory\<close> 48 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => 49 (Theory.check {long = false} ctxt (name, pos); 50 "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ 51 ML_Syntax.print_string name)) 52 || Scan.succeed "Proof_Context.theory_of ML_context") #> 53 54 ML_Antiquotation.value \<^binding>\<open>theory_context\<close> 55 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => 56 (Theory.check {long = false} ctxt (name, pos); 57 "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ 58 ML_Syntax.print_string name))) #> 59 60 ML_Antiquotation.inline \<^binding>\<open>context\<close> 61 (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> 62 63 ML_Antiquotation.inline \<^binding>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> 64 ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> 65 ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> 66 67 ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T => 68 "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> 69 70 ML_Antiquotation.value \<^binding>\<open>cterm\<close> (Args.term >> (fn t => 71 "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> 72 73 ML_Antiquotation.value \<^binding>\<open>cprop\<close> (Args.prop >> (fn t => 74 "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> 75 76 ML_Antiquotation.inline \<^binding>\<open>method\<close> 77 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => 78 ML_Syntax.print_string (Method.check_name ctxt (name, pos))))); 79 80 81(* locales *) 82 83val _ = Theory.setup 84 (ML_Antiquotation.inline \<^binding>\<open>locale\<close> 85 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => 86 Locale.check (Proof_Context.theory_of ctxt) (name, pos) 87 |> ML_Syntax.print_string))); 88 89 90(* type classes *) 91 92fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => 93 Proof_Context.read_class ctxt s 94 |> syn ? Lexicon.mark_class 95 |> ML_Syntax.print_string); 96 97val _ = Theory.setup 98 (ML_Antiquotation.inline \<^binding>\<open>class\<close> (class false) #> 99 ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #> 100 101 ML_Antiquotation.inline \<^binding>\<open>sort\<close> 102 (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => 103 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); 104 105 106(* type constructors *) 107 108fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) 109 >> (fn (ctxt, (s, pos)) => 110 let 111 val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; 112 val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); 113 val res = 114 (case try check (c, decl) of 115 SOME res => res 116 | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); 117 in ML_Syntax.print_string res end); 118 119val _ = Theory.setup 120 (ML_Antiquotation.inline \<^binding>\<open>type_name\<close> 121 (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> 122 ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close> 123 (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> 124 ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close> 125 (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> 126 ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close> 127 (type_name "type" (fn (c, _) => Lexicon.mark_type c))); 128 129 130(* constants *) 131 132fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) 133 >> (fn (ctxt, (s, pos)) => 134 let 135 val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; 136 val res = check (Proof_Context.consts_of ctxt, c) 137 handle TYPE (msg, _, _) => error (msg ^ Position.here pos); 138 in ML_Syntax.print_string res end); 139 140val _ = Theory.setup 141 (ML_Antiquotation.inline \<^binding>\<open>const_name\<close> 142 (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> 143 ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close> 144 (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> 145 ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close> 146 (const_name (fn (_, c) => Lexicon.mark_const c)) #> 147 148 ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close> 149 (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) => 150 if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) 151 then ML_Syntax.print_string c 152 else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> 153 154 ML_Antiquotation.inline \<^binding>\<open>const\<close> 155 (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional 156 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] 157 >> (fn ((ctxt, (raw_c, pos)), Ts) => 158 let 159 val Const (c, _) = 160 Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; 161 val consts = Proof_Context.consts_of ctxt; 162 val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); 163 val _ = length Ts <> n andalso 164 error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ 165 quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); 166 val const = Const (c, Consts.instance consts (c, Ts)); 167 in ML_Syntax.atomic (ML_Syntax.print_term const) end))); 168 169 170(* basic combinators *) 171 172local 173 174val parameter = Parse.position Parse.nat >> (fn (n, pos) => 175 if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); 176 177fun indices n = map string_of_int (1 upto n); 178 179fun empty n = replicate_string n " []"; 180fun dummy n = replicate_string n " _"; 181fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); 182fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); 183 184val tuple = enclose "(" ")" o commas; 185fun tuple_empty n = tuple (replicate n "[]"); 186fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); 187fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" 188fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); 189 190in 191 192val _ = Theory.setup 193 (ML_Antiquotation.value \<^binding>\<open>map\<close> 194 (Scan.lift parameter >> (fn n => 195 "fn f =>\n\ 196 \ let\n\ 197 \ fun map _" ^ empty n ^ " = []\n\ 198 \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ 199 \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ 200 " in map f end")) #> 201 ML_Antiquotation.value \<^binding>\<open>fold\<close> 202 (Scan.lift parameter >> (fn n => 203 "fn f =>\n\ 204 \ let\n\ 205 \ fun fold _" ^ empty n ^ " a = a\n\ 206 \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ 207 \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ 208 " in fold f end")) #> 209 ML_Antiquotation.value \<^binding>\<open>fold_map\<close> 210 (Scan.lift parameter >> (fn n => 211 "fn f =>\n\ 212 \ let\n\ 213 \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ 214 \ | fold_map f" ^ cons n ^ " a =\n\ 215 \ let\n\ 216 \ val (x, a') = f" ^ vars "x" n ^ " a\n\ 217 \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ 218 \ in (x :: xs, a'') end\n\ 219 \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ 220 " in fold_map f end")) #> 221 ML_Antiquotation.value \<^binding>\<open>split_list\<close> 222 (Scan.lift parameter >> (fn n => 223 "fn list =>\n\ 224 \ let\n\ 225 \ fun split_list [] =" ^ tuple_empty n ^ "\n\ 226 \ | split_list" ^ tuple_cons n ^ " =\n\ 227 \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ 228 \ in " ^ cons_tuple n ^ "end\n\ 229 \ in split_list list end")) #> 230 ML_Antiquotation.value \<^binding>\<open>apply\<close> 231 (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> 232 (fn (n, opt_index) => 233 let 234 val cond = 235 (case opt_index of 236 NONE => K true 237 | SOME (index, index_pos) => 238 if 1 <= index andalso index <= n then equal (string_of_int index) 239 else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); 240 in 241 "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ 242 tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) 243 end))); 244 245end; 246 247 248(* outer syntax *) 249 250val _ = Theory.setup 251 (ML_Antiquotation.value \<^binding>\<open>keyword\<close> 252 (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true))) 253 >> (fn (ctxt, (name, pos)) => 254 if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then 255 (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); 256 "Parse.$$$ " ^ ML_Syntax.print_string name) 257 else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> 258 ML_Antiquotation.value \<^binding>\<open>command_keyword\<close> 259 (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) => 260 (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of 261 SOME markup => 262 (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; 263 ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) 264 | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); 265 266end; 267