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