author | wenzelm |
Sun, 19 Sep 2021 21:14:14 +0200 | |
changeset 74317 | 0a4e93250e44 |
parent 74291 | b83fa8f3a271 |
child 74331 | b9a3d2fb53e0 |
permissions | -rw-r--r-- |
73613 | 1 |
(* Title: Pure/ML/ml_antiquotations1.ML |
56205 | 2 |
Author: Makarius |
3 |
||
73613 | 4 |
Miscellaneous ML antiquotations: part 1. |
56205 | 5 |
*) |
6 |
||
73613 | 7 |
structure ML_Antiquotations1: sig end = |
56205 | 8 |
struct |
9 |
||
58632 | 10 |
(* ML support *) |
11 |
||
12 |
val _ = Theory.setup |
|
67147 | 13 |
(ML_Antiquotation.inline \<^binding>\<open>undefined\<close> |
61597
53e32a9b66b8
added @{undefined} with somewhat undefined symbol;
wenzelm
parents:
61596
diff
changeset
|
14 |
(Scan.succeed "(raise General.Match)") #> |
53e32a9b66b8
added @{undefined} with somewhat undefined symbol;
wenzelm
parents:
61596
diff
changeset
|
15 |
|
67147 | 16 |
ML_Antiquotation.inline \<^binding>\<open>assert\<close> |
58632 | 17 |
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
18 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
19 |
ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close> |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62900
diff
changeset
|
20 |
(Scan.lift (Scan.optional Args.embedded "Output.writeln")) |
58632 | 21 |
(fn src => fn output => fn ctxt => |
22 |
let |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
23 |
val struct_name = ML_Context.struct_name ctxt; |
58632 | 24 |
val (_, pos) = Token.name_of_src src; |
59112 | 25 |
val (a, ctxt') = ML_Context.variant "output" ctxt; |
58632 | 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 = |
|
62900
c641bf9402fd
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
wenzelm
parents:
62899
diff
changeset
|
31 |
"(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; |
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
63120
diff
changeset
|
32 |
in (K (env, body), ctxt') end) #> |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
63120
diff
changeset
|
33 |
|
67147 | 34 |
ML_Antiquotation.value \<^binding>\<open>rat\<close> |
63204
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
63120
diff
changeset
|
35 |
(Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- |
921a5be54132
support rat numerals via special antiquotation syntax;
wenzelm
parents:
63120
diff
changeset
|
36 |
Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => |
73586 | 37 |
"Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> |
38 |
||
39 |
ML_Antiquotation.conditional \<^binding>\<open>if_linux\<close> (fn _ => ML_System.platform_is_linux) #> |
|
40 |
ML_Antiquotation.conditional \<^binding>\<open>if_macos\<close> (fn _ => ML_System.platform_is_macos) #> |
|
41 |
ML_Antiquotation.conditional \<^binding>\<open>if_windows\<close> (fn _ => ML_System.platform_is_windows) #> |
|
42 |
ML_Antiquotation.conditional \<^binding>\<open>if_unix\<close> (fn _ => ML_System.platform_is_unix)); |
|
58632 | 43 |
|
44 |
||
45 |
(* formal entities *) |
|
46 |
||
56205 | 47 |
val _ = Theory.setup |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
48 |
(ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
49 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => |
67208 | 50 |
(Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> |
56205 | 51 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
52 |
ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
53 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => |
68482 | 54 |
(Theory.check {long = false} ctxt (name, pos); |
55 |
"Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ |
|
56 |
ML_Syntax.print_string name)) |
|
56205 | 57 |
|| Scan.succeed "Proof_Context.theory_of ML_context") #> |
58 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
59 |
ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
60 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => |
68482 | 61 |
(Theory.check {long = false} ctxt (name, pos); |
56205 | 62 |
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ |
63 |
ML_Syntax.print_string name))) #> |
|
64 |
||
67147 | 65 |
ML_Antiquotation.inline \<^binding>\<open>context\<close> |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59112
diff
changeset
|
66 |
(Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> |
56205 | 67 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
68 |
ML_Antiquotation.inline_embedded \<^binding>\<open>typ\<close> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
69 |
(Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> |
56205 | 70 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
71 |
ML_Antiquotation.inline_embedded \<^binding>\<open>term\<close> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
72 |
(Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
73 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
74 |
ML_Antiquotation.inline_embedded \<^binding>\<open>prop\<close> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
75 |
(Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
76 |
|
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
77 |
ML_Antiquotation.value_embedded \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T => |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59573
diff
changeset
|
78 |
"Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
56205 | 79 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
80 |
ML_Antiquotation.value_embedded \<^binding>\<open>cterm\<close> (Args.term >> (fn t => |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59573
diff
changeset
|
81 |
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
56205 | 82 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
83 |
ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t => |
62075 | 84 |
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
85 |
||
70565 | 86 |
ML_Antiquotation.inline_embedded \<^binding>\<open>oracle_name\<close> |
87 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => |
|
73613 | 88 |
ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); |
63553
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63204
diff
changeset
|
89 |
|
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63204
diff
changeset
|
90 |
|
74290 | 91 |
(* schematic variables *) |
92 |
||
93 |
val schematic_input = |
|
94 |
Args.context -- Scan.lift Args.embedded_input >> (fn (ctxt, src) => |
|
95 |
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt, |
|
96 |
(Syntax.implode_input src, Input.pos_of src))); |
|
97 |
||
98 |
val _ = Theory.setup |
|
99 |
(ML_Antiquotation.inline_embedded \<^binding>\<open>tvar\<close> |
|
100 |
(schematic_input >> (fn (ctxt, (s, pos)) => |
|
101 |
(case Syntax.read_typ ctxt s of |
|
102 |
TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v |
|
103 |
| _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> |
|
104 |
ML_Antiquotation.inline_embedded \<^binding>\<open>var\<close> |
|
105 |
(schematic_input >> (fn (ctxt, (s, pos)) => |
|
106 |
(case Syntax.read_term ctxt s of |
|
107 |
Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v |
|
108 |
| _ => error ("Schematic variable expected" ^ Position.here pos))))); |
|
109 |
||
110 |
||
56205 | 111 |
(* type classes *) |
112 |
||
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62900
diff
changeset
|
113 |
fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => |
56205 | 114 |
Proof_Context.read_class ctxt s |
115 |
|> syn ? Lexicon.mark_class |
|
116 |
|> ML_Syntax.print_string); |
|
117 |
||
118 |
val _ = Theory.setup |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
119 |
(ML_Antiquotation.inline_embedded \<^binding>\<open>class\<close> (class false) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
120 |
ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #> |
56205 | 121 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
122 |
ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close> |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62900
diff
changeset
|
123 |
(Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => |
56205 | 124 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); |
125 |
||
126 |
||
127 |
(* type constructors *) |
|
128 |
||
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
129 |
fun type_name kind check = Args.context -- Scan.lift Args.embedded_token |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
130 |
>> (fn (ctxt, tok) => |
56205 | 131 |
let |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
132 |
val s = Token.inner_syntax_of tok; |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
133 |
val (_, pos) = Input.source_content (Token.input_of tok); |
56205 | 134 |
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; |
135 |
val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); |
|
136 |
val res = |
|
137 |
(case try check (c, decl) of |
|
138 |
SOME res => res |
|
139 |
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); |
|
140 |
in ML_Syntax.print_string res end); |
|
141 |
||
142 |
val _ = Theory.setup |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
143 |
(ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close> |
56205 | 144 |
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
145 |
ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close> |
56205 | 146 |
(type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
147 |
ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close> |
56205 | 148 |
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
149 |
ML_Antiquotation.inline_embedded \<^binding>\<open>type_syntax\<close> |
56205 | 150 |
(type_name "type" (fn (c, _) => Lexicon.mark_type c))); |
151 |
||
152 |
||
153 |
(* constants *) |
|
154 |
||
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
155 |
fun const_name check = Args.context -- Scan.lift Args.embedded_token |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
156 |
>> (fn (ctxt, tok) => |
56205 | 157 |
let |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
158 |
val s = Token.inner_syntax_of tok; |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
159 |
val (_, pos) = Input.source_content (Token.input_of tok); |
56205 | 160 |
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; |
161 |
val res = check (Proof_Context.consts_of ctxt, c) |
|
162 |
handle TYPE (msg, _, _) => error (msg ^ Position.here pos); |
|
163 |
in ML_Syntax.print_string res end); |
|
164 |
||
165 |
val _ = Theory.setup |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
166 |
(ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close> |
56205 | 167 |
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
168 |
ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close> |
56205 | 169 |
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
170 |
ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close> |
56205 | 171 |
(const_name (fn (_, c) => Lexicon.mark_const c)) #> |
172 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
173 |
ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
174 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) => |
56205 | 175 |
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) |
176 |
then ML_Syntax.print_string c |
|
177 |
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> |
|
178 |
||
69595 | 179 |
ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close> |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62900
diff
changeset
|
180 |
(Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional |
56205 | 181 |
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
56251 | 182 |
>> (fn ((ctxt, (raw_c, pos)), Ts) => |
56205 | 183 |
let |
184 |
val Const (c, _) = |
|
185 |
Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; |
|
186 |
val consts = Proof_Context.consts_of ctxt; |
|
187 |
val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); |
|
188 |
val _ = length Ts <> n andalso |
|
189 |
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ |
|
56251 | 190 |
quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); |
56205 | 191 |
val const = Const (c, Consts.instance consts (c, Ts)); |
192 |
in ML_Syntax.atomic (ML_Syntax.print_term const) end))); |
|
193 |
||
194 |
||
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
195 |
(* type/term constructors *) |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
196 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
197 |
local |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
198 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
199 |
fun read_embedded ctxt src parse = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
200 |
let |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
201 |
val keywords = Thy_Header.get_keywords' ctxt; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
202 |
val input = #1 (Token.syntax (Scan.lift Args.embedded_input) src ctxt); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
203 |
val syms = Input.source_explode input; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
204 |
in |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
205 |
(case Token.read_body keywords parse syms of |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
206 |
SOME res => res |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
207 |
| NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
208 |
end; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
209 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
210 |
fun ml_sources ctxt srcs = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
211 |
let |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
212 |
val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes o ML_Lex.read_source) srcs ctxt; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
213 |
fun decl' ctxt'' = map (fn decl => decl ctxt'') decls; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
214 |
in (decl', ctxt') end |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
215 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
216 |
val parse_name = Parse.input Parse.name; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
217 |
val parse_args = Scan.repeat (Parse.input Parse.underscore || Parse.embedded_input); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
218 |
val parse_for_args = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
219 |
Scan.optional ((Parse.position (Parse.$$$ "for") >> #2) -- Parse.!!! parse_args) |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
220 |
(Position.none, []); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
221 |
|
74317 | 222 |
fun parse_body b = |
223 |
if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> single |
|
224 |
else Scan.succeed []; |
|
225 |
||
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
226 |
fun is_dummy s = Input.string_of s = "_"; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
227 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
228 |
val ml = ML_Lex.tokenize_no_range; |
74317 | 229 |
val ml_range = ML_Lex.tokenize_range; |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
230 |
val ml_dummy = ml "_"; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
231 |
fun ml_parens x = ml "(" @ x @ ml ")"; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
232 |
fun ml_bracks x = ml "[" @ x @ ml "]"; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
233 |
fun ml_commas xs = flat (separate (ml ", ") xs); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
234 |
val ml_list = ml_bracks o ml_commas; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
235 |
val ml_string = ml o ML_Syntax.print_string; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
236 |
fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
237 |
|
74317 | 238 |
fun type_antiquotation binding {function} = |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
239 |
ML_Context.add_antiquotation binding true |
74317 | 240 |
(fn range => fn src => fn ctxt => |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
241 |
let |
74317 | 242 |
val ((s, type_args), fn_body) = |
243 |
read_embedded ctxt src (parse_name -- parse_args -- parse_body function); |
|
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
244 |
val pos = Input.pos_of s; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
245 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
246 |
val Type (c, Ts) = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
247 |
Proof_Context.read_type_name {proper = true, strict = true} ctxt |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
248 |
(Syntax.implode_input s); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
249 |
val n = length Ts; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
250 |
val _ = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
251 |
length type_args = n orelse |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
252 |
error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
253 |
" takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
254 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
255 |
val (decls1, ctxt1) = ml_sources ctxt type_args; |
74317 | 256 |
val (decls2, ctxt2) = (ml_sources ctxt1) fn_body; |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
257 |
fun decl' ctxt' = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
258 |
let |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
259 |
val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); |
74317 | 260 |
val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); |
261 |
val ml1 = ml_parens (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); |
|
262 |
val ml2 = |
|
263 |
if function then |
|
264 |
ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ |
|
265 |
ml "| T => " @ ml_range range "raise" @ |
|
266 |
ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], []))" |
|
267 |
else ml1; |
|
268 |
in (flat (ml_args_env @ ml_fn_env), ml2) end; |
|
269 |
in (decl', ctxt2) end); |
|
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
270 |
|
74317 | 271 |
fun const_antiquotation binding {pattern, function} = |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
272 |
ML_Context.add_antiquotation binding true |
74317 | 273 |
(fn range => fn src => fn ctxt => |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
274 |
let |
74317 | 275 |
val (((s, type_args), (for_pos, term_args)), fn_body) = |
276 |
read_embedded ctxt src (parse_name -- parse_args -- parse_for_args -- parse_body function); |
|
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
277 |
val _ = Context_Position.report ctxt for_pos (Markup.keyword_properties Markup.keyword1); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
278 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
279 |
val Const (c, T) = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
280 |
Proof_Context.read_const {proper = true, strict = true} ctxt |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
281 |
(Syntax.implode_input s); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
282 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
283 |
val consts = Proof_Context.consts_of ctxt; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
284 |
val type_paths = Consts.type_arguments consts c; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
285 |
val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
286 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
287 |
val n = length type_params; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
288 |
val m = length (Term.binder_types T); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
289 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
290 |
fun err msg = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
291 |
error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
292 |
Position.here (Input.pos_of s)); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
293 |
val _ = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
294 |
length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
295 |
val _ = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
296 |
length term_args > m andalso Term.is_Type (Term.body_type T) andalso |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
297 |
err (" cannot have more than " ^ string_of_int m ^ " type argument(s)"); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
298 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
299 |
val (decls1, ctxt1) = ml_sources ctxt type_args; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
300 |
val (decls2, ctxt2) = ml_sources ctxt1 term_args; |
74317 | 301 |
val (decls3, ctxt3) = ml_sources ctxt2 fn_body; |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
302 |
fun decl' ctxt' = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
303 |
let |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
304 |
val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
305 |
val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); |
74317 | 306 |
val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); |
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
307 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
308 |
val relevant = map is_dummy type_args ~~ type_paths; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
309 |
fun relevant_path is = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
310 |
not pattern orelse |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
311 |
let val p = rev is |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
312 |
in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
313 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
314 |
val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
315 |
fun ml_typ is (Type (d, Us)) = |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
316 |
if relevant_path is then |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
317 |
ml "Term.Type " @ |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
318 |
ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
319 |
else ml_dummy |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
320 |
| ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
321 |
| ml_typ _ (TFree _) = raise Match; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
322 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
323 |
fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
324 |
| ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
325 |
|
74317 | 326 |
val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); |
327 |
val ml1 = ml_parens (ml_app (rev ml_args_body2)); |
|
328 |
val ml2 = |
|
329 |
if function then |
|
330 |
ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ |
|
331 |
ml "| t => " @ ml_range range "raise" @ |
|
332 |
ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t]))" |
|
333 |
else ml1; |
|
334 |
in (ml_env, ml2) end; |
|
335 |
in (decl', ctxt3) end); |
|
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
336 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
337 |
val _ = Theory.setup |
74317 | 338 |
(type_antiquotation \<^binding>\<open>Type\<close> {function = false} #> |
339 |
type_antiquotation \<^binding>\<open>Type_fn\<close> {function = true} #> |
|
340 |
const_antiquotation \<^binding>\<open>Const\<close> {pattern = false, function = false} #> |
|
341 |
const_antiquotation \<^binding>\<open>Const_\<close> {pattern = true, function = false} #> |
|
342 |
const_antiquotation \<^binding>\<open>Const_fn\<close> {pattern = true, function = true}); |
|
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
343 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
344 |
in end; |
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
345 |
|
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset
|
346 |
|
73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
347 |
(* special forms *) |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
348 |
|
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
349 |
val _ = Theory.setup |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
350 |
(ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #> |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
351 |
ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can"); |
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
352 |
|
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
70565
diff
changeset
|
353 |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
354 |
(* basic combinators *) |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
355 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
356 |
local |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
357 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
358 |
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
|
359 |
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
|
360 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
361 |
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
|
362 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
363 |
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
|
364 |
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
|
365 |
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
|
366 |
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
|
367 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
368 |
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
|
369 |
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
|
370 |
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
|
371 |
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
|
372 |
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
|
373 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
374 |
in |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
375 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
376 |
val _ = Theory.setup |
67147 | 377 |
(ML_Antiquotation.value \<^binding>\<open>map\<close> |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
378 |
(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
|
379 |
"fn f =>\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
380 |
\ let\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
381 |
\ 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
|
382 |
\ | 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
|
383 |
\ | 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
|
384 |
" in map f end")) #> |
67147 | 385 |
ML_Antiquotation.value \<^binding>\<open>fold\<close> |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
386 |
(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
|
387 |
"fn f =>\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
388 |
\ let\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
389 |
\ 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
|
390 |
\ | 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
|
391 |
\ | 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
|
392 |
" in fold f end")) #> |
67147 | 393 |
ML_Antiquotation.value \<^binding>\<open>fold_map\<close> |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
394 |
(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
|
395 |
"fn f =>\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
396 |
\ let\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
397 |
\ 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
|
398 |
\ | 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
|
399 |
\ let\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
400 |
\ 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
|
401 |
\ 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
|
402 |
\ 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
|
403 |
\ | 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
|
404 |
" in fold_map f end")) #> |
67147 | 405 |
ML_Antiquotation.value \<^binding>\<open>split_list\<close> |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
406 |
(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
|
407 |
"fn list =>\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
408 |
\ let\n\ |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
409 |
\ 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
|
410 |
\ | 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
|
411 |
\ 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
|
412 |
\ in " ^ cons_tuple n ^ "end\n\ |
59057
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
413 |
\ in split_list list end")) #> |
67147 | 414 |
ML_Antiquotation.value \<^binding>\<open>apply\<close> |
59057
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
415 |
(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
|
416 |
(fn (n, opt_index) => |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
417 |
let |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
418 |
val cond = |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
419 |
(case opt_index of |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
420 |
NONE => K true |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
421 |
| SOME (index, index_pos) => |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
422 |
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
|
423 |
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
|
424 |
in |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
425 |
"fn f => fn " ^ tuple_vars "x" n ^ " => " ^ |
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
58978
diff
changeset
|
426 |
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
|
427 |
end))); |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
428 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
429 |
end; |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
430 |
|
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58632
diff
changeset
|
431 |
|
56205 | 432 |
(* outer syntax *) |
433 |
||
434 |
val _ = Theory.setup |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
435 |
(ML_Antiquotation.value_embedded \<^binding>\<open>keyword\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
436 |
(Args.context -- |
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
437 |
Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) |
64594 | 438 |
>> (fn (ctxt, (name, pos)) => |
439 |
if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then |
|
440 |
(Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); |
|
441 |
"Parse.$$$ " ^ ML_Syntax.print_string name) |
|
442 |
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
443 |
ML_Antiquotation.value_embedded \<^binding>\<open>command_keyword\<close> |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68482
diff
changeset
|
444 |
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => |
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59878
diff
changeset
|
445 |
(case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59878
diff
changeset
|
446 |
SOME markup => |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59878
diff
changeset
|
447 |
(Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59878
diff
changeset
|
448 |
ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59878
diff
changeset
|
449 |
| NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); |
56205 | 450 |
|
451 |
end; |