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