author | wenzelm |
Wed, 26 Sep 2018 17:04:50 +0200 | |
changeset 69071 | 3ef82592dc22 |
parent 69003 | a015f1d3ba0c |
child 69584 | a91e32843310 |
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 |
|
113 |
||
114 |
||
115 |
(** datatype mfix **) |
|
116 |
||
62753 | 117 |
(*Mfix (sy, ty, c, ps, p, pos): |
62752 | 118 |
sy: rhs of production as symbolic text |
240 | 119 |
ty: type description of production |
120 |
c: head of parse tree |
|
121 |
ps: priorities of arguments in sy |
|
62753 | 122 |
p: priority of production |
123 |
pos: source position*) |
|
240 | 124 |
|
62753 | 125 |
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
|
126 |
|
240 | 127 |
|
128 |
(* typ_to_nonterm *) |
|
129 |
||
865 | 130 |
fun typ_to_nt _ (Type (c, _)) = c |
131 |
| typ_to_nt default _ = default; |
|
132 |
||
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset
|
133 |
(*get nonterminal for rhs*) |
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
134 |
val typ_to_nonterm = typ_to_nt "any"; |
240 | 135 |
|
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset
|
136 |
(*get nonterminal for lhs*) |
42293
6cca0343ea48
renamed sprop "prop#" to "prop'" -- proper identifier;
wenzelm
parents:
42288
diff
changeset
|
137 |
val typ_to_nonterm1 = typ_to_nt "logic"; |
240 | 138 |
|
139 |
||
62786 | 140 |
(* properties *) |
141 |
||
142 |
local |
|
143 |
||
144 |
open Basic_Symbol_Pos; |
|
145 |
||
146 |
val err_prefix = "Error in mixfix block properties: "; |
|
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
147 |
val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "atom expected (identifier, numeral, cartouche)"); |
62786 | 148 |
|
149 |
val scan_atom = |
|
150 |
Symbol_Pos.scan_ident || |
|
151 |
($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) || |
|
152 |
Symbol_Pos.scan_float || Symbol_Pos.scan_nat || |
|
153 |
Symbol_Pos.scan_cartouche_content err_prefix; |
|
154 |
||
155 |
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol); |
|
156 |
val scan_item = |
|
157 |
scan_blanks |-- scan_atom --| scan_blanks |
|
158 |
>> (fn ss => (Symbol_Pos.content ss, #1 (Symbol_Pos.range ss))); |
|
159 |
||
160 |
val scan_prop = |
|
161 |
scan_item -- Scan.optional ($$ "=" |-- !!! scan_item >> #1) "true" |
|
162 |
>> (fn ((x, pos), y) => (x, (y, pos))); |
|
163 |
||
164 |
fun get_property default parse name props = |
|
165 |
(case AList.lookup (op =) props name of |
|
166 |
NONE => default |
|
167 |
| SOME (s, pos) => |
|
168 |
(parse s handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here pos))); |
|
169 |
||
170 |
in |
|
171 |
||
172 |
fun read_properties ss = |
|
173 |
let |
|
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
174 |
val props = |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
175 |
(case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_prop)) ss of |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
176 |
(props, []) => props |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
177 |
| (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); |
62786 | 178 |
val _ = |
62802 | 179 |
(case AList.group (op =) props |> filter (fn (_, [_]) => false | _ => true) of |
62786 | 180 |
[] => () |
62802 | 181 |
| dups => error ("Duplicate properties: " ^ commas_quote (map #1 dups) ^ |
182 |
Position.here_list (map #2 (maps #2 dups)))); |
|
62786 | 183 |
in props end; |
184 |
||
185 |
val get_string = get_property "" I; |
|
63806 | 186 |
val get_bool = get_property false Value.parse_bool; |
187 |
val get_nat = get_property 0 Value.parse_nat; |
|
62786 | 188 |
|
189 |
end; |
|
190 |
||
191 |
||
19004 | 192 |
(* read mixfix annotations *) |
4050 | 193 |
|
194 |
local |
|
19004 | 195 |
|
62752 | 196 |
open Basic_Symbol_Pos; |
197 |
||
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
198 |
val err_prefix = "Error in mixfix annotation: "; |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
199 |
|
62752 | 200 |
fun scan_one pred = Scan.one (pred o Symbol_Pos.symbol); |
201 |
fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol); |
|
202 |
fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); |
|
203 |
||
62806 | 204 |
fun reports_of_block pos = |
205 |
[(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)]; |
|
206 |
||
62808 | 207 |
fun reports_of (xsym, pos) = |
62806 | 208 |
(case xsym of |
209 |
Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)] |
|
210 |
| Argument _ => [(pos, Markup.expression "mixfix argument")] |
|
211 |
| Space _ => [(pos, Markup.expression "mixfix space")] |
|
212 |
| Bg _ => reports_of_block pos |
|
213 |
| Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)] |
|
214 |
| En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]); |
|
215 |
||
62808 | 216 |
fun reports_text_of (xsym, pos) = |
217 |
(case xsym of |
|
218 |
Delim s => |
|
219 |
if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then |
|
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
63933
diff
changeset
|
220 |
[((pos, Markup.bad ()), |
62808 | 221 |
"Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")] |
222 |
else [] |
|
223 |
| _ => []); |
|
224 |
||
62786 | 225 |
fun read_block_properties ss = |
226 |
let |
|
227 |
val props = read_properties ss; |
|
62783 | 228 |
|
62786 | 229 |
val markup_name = get_string Markup.markupN props; |
230 |
val markup_props = fold (AList.delete (op =)) Markup.block_properties props; |
|
231 |
val markup = (markup_name, map (apsnd #1) markup_props); |
|
232 |
val _ = |
|
233 |
if markup_name = "" andalso not (null markup_props) then |
|
62802 | 234 |
error ("Markup name required for block properties: " ^ |
235 |
commas_quote (map #1 markup_props) ^ Position.here_list (map (#2 o #2) markup_props)) |
|
62786 | 236 |
else (); |
62783 | 237 |
|
62786 | 238 |
val consistent = get_bool Markup.consistentN props; |
62789 | 239 |
val unbreakable = get_bool Markup.unbreakableN props; |
62786 | 240 |
val indent = get_nat Markup.indentN props; |
62789 | 241 |
in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end |
62806 | 242 |
handle ERROR msg => |
243 |
let |
|
244 |
val reported_texts = |
|
245 |
reports_of_block (#1 (Symbol_Pos.range ss)) |
|
246 |
|> map (fn (p, m) => Markup.markup_report (Position.reported_text p m "")) |
|
247 |
in error (msg ^ implode reported_texts) end; |
|
62783 | 248 |
|
249 |
val read_block_indent = |
|
62789 | 250 |
Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol; |
62783 | 251 |
|
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
252 |
val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close]; |
19004 | 253 |
|
63933 | 254 |
val scan_delim = |
255 |
scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " || |
|
256 |
$$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single || |
|
257 |
scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single; |
|
19004 | 258 |
|
259 |
val scan_sym = |
|
260 |
$$ "_" >> K (Argument ("", 0)) || |
|
62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
59841
diff
changeset
|
261 |
$$ "\<index>" >> K index || |
62783 | 262 |
$$ "(" |-- |
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
263 |
(Symbol_Pos.scan_cartouche_content err_prefix >> read_block_properties || |
62783 | 264 |
scan_many Symbol.is_digit >> read_block_indent) || |
19004 | 265 |
$$ ")" >> K En || |
266 |
$$ "/" -- $$ "/" >> K (Brk ~1) || |
|
62805 | 267 |
$$ "/" |-- scan_many Symbol.is_space >> (Brk o length) || |
268 |
scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) || |
|
63933 | 269 |
Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat); |
14819 | 270 |
|
19004 | 271 |
val scan_symb = |
62795
063d2f23cdf6
removed redundant Position.set_range -- already done in Position.range;
wenzelm
parents:
62789
diff
changeset
|
272 |
Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) || |
62805 | 273 |
$$ "'" -- scan_one Symbol.is_space >> K NONE; |
19004 | 274 |
|
19305 | 275 |
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); |
4050 | 276 |
|
19004 | 277 |
in |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
278 |
|
62764 | 279 |
fun read_mfix ss = |
280 |
let |
|
62801
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
281 |
val xsymbs = |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
282 |
(case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
283 |
(res, []) => map_filter I res |
f9d102ef13f1
clarified errors -- disallow cartouche fragments as delimiter;
wenzelm
parents:
62795
diff
changeset
|
284 |
| (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); |
62764 | 285 |
val _ = Position.reports (maps reports_of xsymbs); |
62808 | 286 |
val _ = Position.reports_text (maps reports_text_of xsymbs); |
62764 | 287 |
in xsymbs end; |
19004 | 288 |
|
62764 | 289 |
val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none)); |
62752 | 290 |
val mixfix_args = mfix_args o Input.source_explode; |
19004 | 291 |
|
35390 | 292 |
val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; |
19004 | 293 |
|
4050 | 294 |
end; |
295 |
||
296 |
||
240 | 297 |
(* mfix_to_xprod *) |
298 |
||
62753 | 299 |
fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) = |
240 | 300 |
let |
62772 | 301 |
val _ = Position.report pos Markup.language_mixfix; |
62764 | 302 |
val symbs0 = read_mfix sy; |
303 |
||
62762 | 304 |
fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos); |
240 | 305 |
|
62762 | 306 |
fun check_blocks [] pending bad = pending @ bad |
307 |
| check_blocks ((Bg _, pos) :: rest) pending bad = check_blocks rest (pos :: pending) bad |
|
308 |
| check_blocks ((En, pos) :: rest) [] bad = check_blocks rest [] (pos :: bad) |
|
309 |
| check_blocks ((En, _) :: rest) (_ :: pending) bad = check_blocks rest pending bad |
|
310 |
| check_blocks (_ :: rest) pending bad = check_blocks rest pending bad; |
|
240 | 311 |
|
312 |
fun add_args [] ty [] = ([], typ_to_nonterm1 ty) |
|
62762 | 313 |
| add_args [] _ _ = err_in_mixfix "Too many precedences" |
314 |
| add_args ((sym as (Argument ("index", _), _)) :: syms) ty ps = |
|
315 |
add_args syms ty ps |>> cons sym |
|
316 |
| add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) [] = |
|
317 |
add_args syms tys [] |>> cons (Argument (typ_to_nonterm ty, 0), pos) |
|
318 |
| add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) (p :: ps) = |
|
319 |
add_args syms tys ps |>> cons (Argument (typ_to_nonterm ty, p), pos) |
|
320 |
| add_args ((Argument _, _) :: _) _ _ = |
|
321 |
err_in_mixfix "More arguments than in corresponding type" |
|
322 |
| add_args (sym :: syms) ty ps = add_args syms ty ps |>> cons sym; |
|
323 |
||
324 |
fun logical_args (a as (Argument (s, p))) = |
|
325 |
if s <> "prop" andalso member (op =) logical_types s then Argument ("logic", p) else a |
|
326 |
| logical_args a = a; |
|
240 | 327 |
|
328 |
fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) |
|
329 |
| rem_pri sym = sym; |
|
330 |
||
62764 | 331 |
val indexes = filter (is_index o #1) symbs0; |
62762 | 332 |
val _ = |
333 |
if length indexes <= 1 then () |
|
334 |
else error ("More than one index argument" ^ Position.here_list (map #2 indexes)); |
|
2364 | 335 |
|
62764 | 336 |
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
|
337 |
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
|
338 |
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
|
339 |
else |
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
340 |
let |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35390
diff
changeset
|
341 |
val indexed_const = |
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35390
diff
changeset
|
342 |
if const <> "" then const ^ "_indexed" |
62762 | 343 |
else err_in_mixfix "Missing constant name for indexed syntax"; |
14697 | 344 |
val rangeT = Term.range_type typ handle Match => |
62762 | 345 |
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
|
346 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43323
diff
changeset
|
347 |
val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1)); |
19012 | 348 |
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
|
349 |
val i = Ast.Variable "i"; |
62762 | 350 |
val lhs = |
351 |
Ast.mk_appl (Ast.Constant indexed_const) |
|
352 |
(xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); |
|
14697 | 353 |
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
|
354 |
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
|
355 |
|
62764 | 356 |
val (symbs1, lhs) = add_args symbs0 typ' pris; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
357 |
|
2364 | 358 |
val copy_prod = |
20675 | 359 |
(lhs = "prop" orelse lhs = "logic") |
2364 | 360 |
andalso const <> "" |
62764 | 361 |
andalso not (null symbs1) |
362 |
andalso not (exists (is_delim o #1) symbs1); |
|
2364 | 363 |
val lhs' = |
62764 | 364 |
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
|
365 |
else if lhs = "prop" then "prop'" |
62762 | 366 |
else if member (op =) logical_types lhs then "logic" |
2364 | 367 |
else lhs; |
62764 | 368 |
val symbs2 = map (apfst logical_args) symbs1; |
240 | 369 |
|
62762 | 370 |
val _ = |
371 |
(pri :: pris) |> List.app (fn p => |
|
372 |
if p >= 0 andalso p <= 1000 then () |
|
373 |
else err_in_mixfix ("Precedence " ^ string_of_int p ^ " out of range")); |
|
374 |
val _ = |
|
62764 | 375 |
(case check_blocks symbs2 [] [] of |
62762 | 376 |
[] => () |
377 |
| bad => error ("Unbalanced block parentheses" ^ Position.here_list bad)); |
|
378 |
||
62764 | 379 |
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
|
380 |
val xprod' = |
62762 | 381 |
if Lexicon.is_terminal lhs' then |
382 |
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
|
383 |
else if const <> "" then xprod |
62764 | 384 |
else if length (filter (is_argument o #1) symbs2) <> 1 then |
62762 | 385 |
err_in_mixfix "Copy production must have exactly one argument" |
62764 | 386 |
else if exists (is_terminal o #1) symbs2 then xprod |
387 |
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
|
388 |
|
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
|
389 |
in (xprod', syntax_consts, parse_rules) end; |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
390 |
|
240 | 391 |
|
392 |
||
393 |
(** datatype syn_ext **) |
|
394 |
||
395 |
datatype syn_ext = |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35429
diff
changeset
|
396 |
Syn_Ext of { |
240 | 397 |
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
|
398 |
consts: (string * string) list, |
21772 | 399 |
parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, |
1510 | 400 |
parse_rules: (Ast.ast * Ast.ast) list, |
21772 | 401 |
parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, |
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset
|
402 |
print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, |
1510 | 403 |
print_rules: (Ast.ast * Ast.ast) list, |
42268 | 404 |
print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}; |
240 | 405 |
|
406 |
||
407 |
(* syn_ext *) |
|
408 |
||
59841 | 409 |
fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) = |
240 | 410 |
let |
411 |
val (parse_ast_translation, parse_translation, print_translation, |
|
412 |
print_ast_translation) = trfuns; |
|
413 |
||
59841 | 414 |
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
|
415 |
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
|
416 |
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
|
417 |
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
|
418 |
val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods; |
240 | 419 |
in |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35429
diff
changeset
|
420 |
Syn_Ext { |
624 | 421 |
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
|
422 |
consts = mfix_consts @ consts' @ consts, |
240 | 423 |
parse_ast_translation = parse_ast_translation, |
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
424 |
parse_rules = parse_rules' @ parse_rules, |
240 | 425 |
parse_translation = parse_translation, |
426 |
print_translation = print_translation, |
|
12513
0ffb824dc95c
support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents:
11546
diff
changeset
|
427 |
print_rules = map swap parse_rules' @ print_rules, |
42268 | 428 |
print_ast_translation = print_ast_translation} |
240 | 429 |
end; |
430 |
||
2382 | 431 |
|
59841 | 432 |
val syn_ext = syn_ext' []; |
555
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset
|
433 |
|
42268 | 434 |
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; |
52143 | 435 |
fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []); |
16610 | 436 |
|
15754 | 437 |
fun stamp_trfun s (c, f) = (c, (f, s)); |
438 |
fun mk_trfun tr = stamp_trfun (stamp ()) tr; |
|
29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset
|
439 |
fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; |
15754 | 440 |
|
240 | 441 |
end; |