author | wenzelm |
Fri, 01 Apr 2016 16:15:31 +0200 | |
changeset 62789 | ce15dd971965 |
parent 62787 | f90a9fe3329f |
child 62795 | 063d2f23cdf6 |
permissions | -rw-r--r-- |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
1 |
(* Title: Pure/Syntax/syntax_ext.ML |
911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset
|
2 |
Author: Markus Wenzel and Carsten Clasohm, TU Muenchen |
240 | 3 |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
4 |
Syntax extension. |
240 | 5 |
*) |
6 |
||
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
7 |
signature SYNTAX_EXT = |
4050 | 8 |
sig |
62753 | 9 |
datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T |
1510 | 10 |
val typ_to_nonterm: typ -> string |
62789 | 11 |
type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int} |
62783 | 12 |
val block_indent: int -> block_info |
1510 | 13 |
datatype xsymb = |
14 |
Delim of string | |
|
15 |
Argument of string * int | |
|
16 |
Space of string | |
|
62783 | 17 |
Bg of block_info | |
18 |
Brk of int | |
|
19 |
En |
|
1510 | 20 |
datatype xprod = XProd of string * xsymb list * string * int |
21 |
val chain_pri: int |
|
4701 | 22 |
val delims_of: xprod list -> string list list |
1510 | 23 |
datatype syn_ext = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35429
diff
changeset
|
24 |
Syn_Ext of { |
1510 | 25 |
xprods: xprod list, |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42297
diff
changeset
|
26 |
consts: (string * string) list, |
21772 | 27 |
parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, |
1510 | 28 |
parse_rules: (Ast.ast * Ast.ast) list, |
21772 | 29 |
parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
30 |
print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, |
1510 | 31 |
print_rules: (Ast.ast * Ast.ast) list, |
42268 | 32 |
print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} |
62752 | 33 |
val mfix_args: Symbol_Pos.T list -> int |
34 |
val mixfix_args: Input.source -> int |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
35 |
val escape: string -> string |
59841 | 36 |
val syn_ext': string list -> mfix list -> |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42297
diff
changeset
|
37 |
(string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * |
21772 | 38 |
(string * ((Proof.context -> term list -> term) * stamp)) list * |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
39 |
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list * |
42268 | 40 |
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> |
41 |
(Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext |
|
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42297
diff
changeset
|
42 |
val syn_ext: mfix list -> (string * string) list -> |
21772 | 43 |
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * |
44 |
(string * ((Proof.context -> term list -> term) * stamp)) list * |
|
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
45 |
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list * |
42268 | 46 |
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> |
47 |
(Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext |
|
14903 | 48 |
val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext |
49 |
val syn_ext_trfuns: |
|
21772 | 50 |
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * |
51 |
(string * ((Proof.context -> term list -> term) * stamp)) list * |
|
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
52 |
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list * |
21772 | 53 |
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
54 |
val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp) |
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
55 |
val mk_trfun: string * 'a -> string * ('a * stamp) |
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
56 |
val eq_trfun: ('a * stamp) * ('a * stamp) -> bool |
4050 | 57 |
end; |
240 | 58 |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42268
diff
changeset
|
59 |
structure Syntax_Ext: SYNTAX_EXT = |
240 | 60 |
struct |
61 |
||
62 |
(** datatype xprod **) |
|
63 |
||
64 |
(*Delim s: delimiter s |
|
65 |
Argument (s, p): nonterminal s requiring priority >= p, or valued token |
|
66 |
Space s: some white space for printing |
|
67 |
Bg, Brk, En: blocks and breaks for pretty printing*) |
|
68 |
||
62789 | 69 |
type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}; |
70 |
||
71 |
fun block_indent indent : block_info = |
|
72 |
{markup = Markup.empty, consistent = false, unbreakable = false, indent = indent}; |
|
62783 | 73 |
|
240 | 74 |
datatype xsymb = |
75 |
Delim of string | |
|
76 |
Argument of string * int | |
|
77 |
Space of string | |
|
62783 | 78 |
Bg of block_info | |
79 |
Brk of int | |
|
80 |
En; |
|
240 | 81 |
|
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
82 |
fun is_delim (Delim _) = true |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
83 |
| is_delim _ = false; |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
84 |
|
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
85 |
fun is_terminal (Delim _) = true |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
86 |
| is_terminal (Argument (s, _)) = Lexicon.is_terminal s |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
87 |
| is_terminal _ = false; |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
88 |
|
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
89 |
fun is_argument (Argument _) = true |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
90 |
| is_argument _ = false; |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
91 |
|
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
92 |
fun is_index (Argument ("index", _)) = true |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
93 |
| is_index _ = false; |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
94 |
|
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
95 |
val index = Argument ("index", 1000); |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
96 |
|
240 | 97 |
|
98 |
(*XProd (lhs, syms, c, p): |
|
99 |
lhs: name of nonterminal on the lhs of the production |
|
100 |
syms: list of symbols on the rhs of the production |
|
101 |
c: head of parse tree |
|
102 |
p: priority of this production*) |
|
103 |
||
104 |
datatype xprod = XProd of string * xsymb list * string * int; |
|
105 |
||
106 |
val chain_pri = ~1; (*dummy for chain productions*) |
|
107 |
||
108 |
fun delims_of xprods = |
|
19004 | 109 |
fold (fn XProd (_, xsymbs, _, _) => |
110 |
fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods [] |
|
111 |
|> map Symbol.explode; |
|
240 | 112 |
|
62764 | 113 |
fun reports_of (xsym, pos: Position.T) = |
62787 | 114 |
(pos, Markup.expression) :: |
115 |
(case xsym of |
|
116 |
Delim _ => [(pos, Markup.literal)] |
|
117 |
| Bg _ => [(pos, Markup.keyword3)] |
|
118 |
| Brk _ => [(pos, Markup.keyword3)] |
|
119 |
| En => [(pos, Markup.keyword3)] |
|
120 |
| _ => []); |
|
62764 | 121 |
|
240 | 122 |
|
123 |
||
124 |
(** datatype mfix **) |
|
125 |
||
62753 | 126 |
(*Mfix (sy, ty, c, ps, p, pos): |
62752 | 127 |
sy: rhs of production as symbolic text |
240 | 128 |
ty: type description of production |
129 |
c: head of parse tree |
|
130 |
ps: priorities of arguments in sy |
|
62753 | 131 |
p: priority of production |
132 |
pos: source position*) |
|
240 | 133 |
|
62753 | 134 |
datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
135 |
|
240 | 136 |
|
137 |
(* typ_to_nonterm *) |
|
138 |
||
865 | 139 |
fun typ_to_nt _ (Type (c, _)) = c |
140 |
| typ_to_nt default _ = default; |
|
141 |
||
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset
|
142 |
(*get nonterminal for rhs*) |
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
143 |
val typ_to_nonterm = typ_to_nt "any"; |
240 | 144 |
|
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset
|
145 |
(*get nonterminal for lhs*) |
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
146 |
val typ_to_nonterm1 = typ_to_nt "logic"; |
240 | 147 |
|
148 |
||
62786 | 149 |
(* properties *) |
150 |
||
151 |
local |
|
152 |
||
153 |
open Basic_Symbol_Pos; |
|
154 |
||
155 |
val err_prefix = "Error in mixfix block properties: "; |
|
156 |
val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "expected identifier or numeral or cartouche"); |
|
157 |
||
158 |
val scan_atom = |
|
159 |
Symbol_Pos.scan_ident || |
|
160 |
($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) || |
|
161 |
Symbol_Pos.scan_float || Symbol_Pos.scan_nat || |
|
162 |
Symbol_Pos.scan_cartouche_content err_prefix; |
|
163 |
||
164 |
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol); |
|
165 |
val scan_item = |
|
166 |
scan_blanks |-- scan_atom --| scan_blanks |
|
167 |
>> (fn ss => (Symbol_Pos.content ss, #1 (Symbol_Pos.range ss))); |
|
168 |
||
169 |
val scan_prop = |
|
170 |
scan_item -- Scan.optional ($$ "=" |-- !!! scan_item >> #1) "true" |
|
171 |
>> (fn ((x, pos), y) => (x, (y, pos))); |
|
172 |
||
173 |
val scan_end = Scan.ahead (Scan.one Symbol_Pos.is_eof) >> K ("", Position.none) || !!! Scan.fail; |
|
174 |
||
175 |
fun get_property default parse name props = |
|
176 |
(case AList.lookup (op =) props name of |
|
177 |
NONE => default |
|
178 |
| SOME (s, pos) => |
|
179 |
(parse s handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here pos))); |
|
180 |
||
181 |
in |
|
182 |
||
183 |
fun show_props props = |
|
184 |
commas_quote (map #1 props) ^ Position.here_list (map (#2 o #2) props); |
|
185 |
||
186 |
fun read_properties ss = |
|
187 |
let |
|
188 |
val props = the (Scan.read Symbol_Pos.stopper (Scan.repeat1 scan_prop --| scan_end) ss); |
|
189 |
val _ = |
|
190 |
(case duplicates (eq_fst op =) props of |
|
191 |
[] => () |
|
192 |
| dups => error ("Duplicate properties: " ^ show_props dups)); |
|
193 |
in props end; |
|
194 |
||
195 |
val get_string = get_property "" I; |
|
196 |
val get_bool = get_property false Markup.parse_bool; |
|
197 |
val get_nat = get_property 0 Markup.parse_nat; |
|
198 |
||
199 |
end; |
|
200 |
||
201 |
||
19004 | 202 |
(* read mixfix annotations *) |
4050 | 203 |
|
204 |
local |
|
19004 | 205 |
|
62752 | 206 |
open Basic_Symbol_Pos; |
207 |
||
208 |
fun scan_one pred = Scan.one (pred o Symbol_Pos.symbol); |
|
209 |
fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol); |
|
210 |
fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); |
|
211 |
||
62786 | 212 |
fun read_block_properties ss = |
213 |
let |
|
214 |
val props = read_properties ss; |
|
62783 | 215 |
|
62786 | 216 |
val markup_name = get_string Markup.markupN props; |
217 |
val markup_props = fold (AList.delete (op =)) Markup.block_properties props; |
|
218 |
val markup = (markup_name, map (apsnd #1) markup_props); |
|
219 |
val _ = |
|
220 |
if markup_name = "" andalso not (null markup_props) then |
|
221 |
error ("Markup name required for block properties: " ^ show_props markup_props) |
|
222 |
else (); |
|
62783 | 223 |
|
62786 | 224 |
val consistent = get_bool Markup.consistentN props; |
62789 | 225 |
val unbreakable = get_bool Markup.unbreakableN props; |
62786 | 226 |
val indent = get_nat Markup.indentN props; |
62789 | 227 |
in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end |
62787 | 228 |
handle ERROR msg => error (msg ^ |
229 |
Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 "")); |
|
62783 | 230 |
|
231 |
val read_block_indent = |
|
62789 | 232 |
Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol; |
62783 | 233 |
|
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
59841
diff
changeset
|
234 |
val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"]; |
19004 | 235 |
|
236 |
val scan_delim_char = |
|
62752 | 237 |
$$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) || |
238 |
scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); |
|
19004 | 239 |
|
240 |
val scan_sym = |
|
241 |
$$ "_" >> K (Argument ("", 0)) || |
|
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
59841
diff
changeset
|
242 |
$$ "\<index>" >> K index || |
62783 | 243 |
$$ "(" |-- |
244 |
(Symbol_Pos.scan_cartouche_content "Error in mixfix annotation: " >> read_block_properties || |
|
245 |
scan_many Symbol.is_digit >> read_block_indent) || |
|
19004 | 246 |
$$ ")" >> K En || |
247 |
$$ "/" -- $$ "/" >> K (Brk ~1) || |
|
62752 | 248 |
$$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) || |
249 |
scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) || |
|
250 |
Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content); |
|
14819 | 251 |
|
19004 | 252 |
val scan_symb = |
62764 | 253 |
Scan.trace scan_sym >> |
254 |
(fn (syms, trace) => SOME (syms, Position.set_range (Symbol_Pos.range trace))) || |
|
62752 | 255 |
$$ "'" -- scan_one Symbol.is_blank >> K NONE; |
19004 | 256 |
|
19305 | 257 |
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); |
4050 | 258 |
|
19004 | 259 |
in |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
260 |
|
62764 | 261 |
fun read_mfix ss = |
262 |
let |
|
263 |
val xsymbs = map_filter I (the (Scan.read Symbol_Pos.stopper scan_symbs ss)); |
|
264 |
val _ = Position.reports (maps reports_of xsymbs); |
|
265 |
in xsymbs end; |
|
19004 | 266 |
|
62764 | 267 |
val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none)); |
62752 | 268 |
val mixfix_args = mfix_args o Input.source_explode; |
19004 | 269 |
|
35390 | 270 |
val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; |
19004 | 271 |
|
4050 | 272 |
end; |
273 |
||
274 |
||
240 | 275 |
(* mfix_to_xprod *) |
276 |
||
62753 | 277 |
fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) = |
240 | 278 |
let |
62772 | 279 |
val _ = Position.report pos Markup.language_mixfix; |
62764 | 280 |
val symbs0 = read_mfix sy; |
281 |
||
62762 | 282 |
fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos); |
240 | 283 |
|
62762 | 284 |
fun check_blocks [] pending bad = pending @ bad |
285 |
| check_blocks ((Bg _, pos) :: rest) pending bad = check_blocks rest (pos :: pending) bad |
|
286 |
| check_blocks ((En, pos) :: rest) [] bad = check_blocks rest [] (pos :: bad) |
|
287 |
| check_blocks ((En, _) :: rest) (_ :: pending) bad = check_blocks rest pending bad |
|
288 |
| check_blocks (_ :: rest) pending bad = check_blocks rest pending bad; |
|
240 | 289 |
|
290 |
fun add_args [] ty [] = ([], typ_to_nonterm1 ty) |
|
62762 | 291 |
| add_args [] _ _ = err_in_mixfix "Too many precedences" |
292 |
| add_args ((sym as (Argument ("index", _), _)) :: syms) ty ps = |
|
293 |
add_args syms ty ps |>> cons sym |
|
294 |
| add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) [] = |
|
295 |
add_args syms tys [] |>> cons (Argument (typ_to_nonterm ty, 0), pos) |
|
296 |
| add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) (p :: ps) = |
|
297 |
add_args syms tys ps |>> cons (Argument (typ_to_nonterm ty, p), pos) |
|
298 |
| add_args ((Argument _, _) :: _) _ _ = |
|
299 |
err_in_mixfix "More arguments than in corresponding type" |
|
300 |
| add_args (sym :: syms) ty ps = add_args syms ty ps |>> cons sym; |
|
301 |
||
302 |
fun logical_args (a as (Argument (s, p))) = |
|
303 |
if s <> "prop" andalso member (op =) logical_types s then Argument ("logic", p) else a |
|
304 |
| logical_args a = a; |
|
240 | 305 |
|
306 |
fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) |
|
307 |
| rem_pri sym = sym; |
|
308 |
||
62764 | 309 |
val indexes = filter (is_index o #1) symbs0; |
62762 | 310 |
val _ = |
311 |
if length indexes <= 1 then () |
|
312 |
else error ("More than one index argument" ^ Position.here_list (map #2 indexes)); |
|
2364 | 313 |
|
62764 | 314 |
val args = map_filter (fn (arg as Argument _, _) => SOME arg | _ => NONE) symbs0; |
44470
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
315 |
val (const', typ', syntax_consts, parse_rules) = |
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
316 |
if not (exists is_index args) then (const, typ, NONE, NONE) |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
317 |
else |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
318 |
let |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35390
diff
changeset
|
319 |
val indexed_const = |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35390
diff
changeset
|
320 |
if const <> "" then const ^ "_indexed" |
62762 | 321 |
else err_in_mixfix "Missing constant name for indexed syntax"; |
14697 | 322 |
val rangeT = Term.range_type typ handle Match => |
62762 | 323 |
err_in_mixfix "Missing structure argument for indexed syntax"; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
324 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43323
diff
changeset
|
325 |
val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1)); |
19012 | 326 |
val (xs1, xs2) = chop (find_index is_index args) xs; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
327 |
val i = Ast.Variable "i"; |
62762 | 328 |
val lhs = |
329 |
Ast.mk_appl (Ast.Constant indexed_const) |
|
330 |
(xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); |
|
14697 | 331 |
val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs); |
44470
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
332 |
in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
333 |
|
62764 | 334 |
val (symbs1, lhs) = add_args symbs0 typ' pris; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
335 |
|
2364 | 336 |
val copy_prod = |
20675 | 337 |
(lhs = "prop" orelse lhs = "logic") |
2364 | 338 |
andalso const <> "" |
62764 | 339 |
andalso not (null symbs1) |
340 |
andalso not (exists (is_delim o #1) symbs1); |
|
2364 | 341 |
val lhs' = |
62764 | 342 |
if copy_prod orelse lhs = "prop" andalso map #1 symbs1 = [Argument ("prop'", 0)] then lhs |
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
343 |
else if lhs = "prop" then "prop'" |
62762 | 344 |
else if member (op =) logical_types lhs then "logic" |
2364 | 345 |
else lhs; |
62764 | 346 |
val symbs2 = map (apfst logical_args) symbs1; |
240 | 347 |
|
62762 | 348 |
val _ = |
349 |
(pri :: pris) |> List.app (fn p => |
|
350 |
if p >= 0 andalso p <= 1000 then () |
|
351 |
else err_in_mixfix ("Precedence " ^ string_of_int p ^ " out of range")); |
|
352 |
val _ = |
|
62764 | 353 |
(case check_blocks symbs2 [] [] of |
62762 | 354 |
[] => () |
355 |
| bad => error ("Unbalanced block parentheses" ^ Position.here_list bad)); |
|
356 |
||
62764 | 357 |
val xprod = XProd (lhs', map #1 symbs2, const', pri); |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
358 |
val xprod' = |
62762 | 359 |
if Lexicon.is_terminal lhs' then |
360 |
err_in_mixfix ("Illegal use of terminal " ^ quote lhs' ^ " as nonterminal") |
|
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
361 |
else if const <> "" then xprod |
62764 | 362 |
else if length (filter (is_argument o #1) symbs2) <> 1 then |
62762 | 363 |
err_in_mixfix "Copy production must have exactly one argument" |
62764 | 364 |
else if exists (is_terminal o #1) symbs2 then xprod |
365 |
else XProd (lhs', map (rem_pri o #1) symbs2, "", chain_pri); |
|
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
366 |
|
44470
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
367 |
in (xprod', syntax_consts, parse_rules) end; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
368 |
|
240 | 369 |
|
370 |
||
371 |
(** datatype syn_ext **) |
|
372 |
||
373 |
datatype syn_ext = |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35429
diff
changeset
|
374 |
Syn_Ext of { |
240 | 375 |
xprods: xprod list, |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42297
diff
changeset
|
376 |
consts: (string * string) list, |
21772 | 377 |
parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, |
1510 | 378 |
parse_rules: (Ast.ast * Ast.ast) list, |
21772 | 379 |
parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
380 |
print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, |
1510 | 381 |
print_rules: (Ast.ast * Ast.ast) list, |
42268 | 382 |
print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}; |
240 | 383 |
|
384 |
||
385 |
(* syn_ext *) |
|
386 |
||
59841 | 387 |
fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) = |
240 | 388 |
let |
389 |
val (parse_ast_translation, parse_translation, print_translation, |
|
390 |
print_ast_translation) = trfuns; |
|
391 |
||
59841 | 392 |
val xprod_results = map (mfix_to_xprod logical_types) mfixes; |
44470
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
393 |
val xprods = map #1 xprod_results; |
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
394 |
val consts' = map_filter #2 xprod_results; |
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
395 |
val parse_rules' = rev (map_filter #3 xprod_results); |
42298
d622145603ee
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
wenzelm
parents:
42297
diff
changeset
|
396 |
val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods; |
240 | 397 |
in |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35429
diff
changeset
|
398 |
Syn_Ext { |
624 | 399 |
xprods = xprods, |
44470
6c6c31ef6bb2
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
wenzelm
parents:
43329
diff
changeset
|
400 |
consts = mfix_consts @ consts' @ consts, |
240 | 401 |
parse_ast_translation = parse_ast_translation, |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
402 |
parse_rules = parse_rules' @ parse_rules, |
240 | 403 |
parse_translation = parse_translation, |
404 |
print_translation = print_translation, |
|
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
405 |
print_rules = map swap parse_rules' @ print_rules, |
42268 | 406 |
print_ast_translation = print_ast_translation} |
240 | 407 |
end; |
408 |
||
2382 | 409 |
|
59841 | 410 |
val syn_ext = syn_ext' []; |
555
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset
|
411 |
|
42268 | 412 |
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; |
52143 | 413 |
fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []); |
16610 | 414 |
|
15754 | 415 |
fun stamp_trfun s (c, f) = (c, (f, s)); |
416 |
fun mk_trfun tr = stamp_trfun (stamp ()) tr; |
|
29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset
|
417 |
fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; |
15754 | 418 |
|
240 | 419 |
end; |