7 *) |
7 *) |
8 |
8 |
9 signature CODEGEN_SERIALIZER = |
9 signature CODEGEN_SERIALIZER = |
10 sig |
10 sig |
11 include BASIC_CODEGEN_THINGOL; |
11 include BASIC_CODEGEN_THINGOL; |
12 val get_serializer: theory -> string * Args.T list |
12 |
13 -> string list option -> CodegenThingol.code -> unit; |
|
14 val eval_verbose: bool ref; |
|
15 val eval_term: theory -> |
|
16 (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code |
|
17 -> 'a; |
|
18 val const_has_serialization: theory -> string list -> string -> bool; |
|
19 val tyco_has_serialization: theory -> string list -> string -> bool; |
|
20 val add_syntax_class: |
|
21 string -> string -> string * (string * string) list -> theory -> theory; |
|
22 val add_syntax_inst: string -> (string * string) -> theory -> theory; |
|
23 val parse_syntax_tyco: (theory |
|
24 -> CodegenConsts.const list * (string * typ) list |
|
25 -> string |
|
26 -> CodegenNames.tyco |
|
27 -> typ list -> CodegenThingol.itype list) |
|
28 -> Symtab.key |
|
29 -> xstring |
|
30 -> OuterParse.token list |
|
31 -> (theory -> theory) * OuterParse.token list; |
|
32 val parse_syntax_const: (theory |
|
33 -> CodegenConsts.const list * (string * typ) list |
|
34 -> string |
|
35 -> CodegenNames.const |
|
36 -> term list -> CodegenThingol.iterm list) |
|
37 -> Symtab.key |
|
38 -> string |
|
39 -> OuterParse.token list |
|
40 -> (theory -> theory) * OuterParse.token list; |
|
41 val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T) |
13 val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T) |
42 -> ((string -> string) * (string -> string)) option -> int * string |
14 -> ((string -> string) * (string -> string)) option -> int * string |
43 -> theory -> theory; |
15 -> theory -> theory; |
44 val add_pretty_ml_string: string -> string -> string -> string |
16 val add_pretty_ml_string: string -> string -> string -> string |
45 -> (string -> string) -> (string -> string) -> string -> theory -> theory; |
17 -> (string -> string) -> (string -> string) -> string -> theory -> theory; |
46 val add_undefined: string -> string -> string -> theory -> theory; |
18 val add_undefined: string -> string -> string -> theory -> theory; |
47 |
19 |
48 type fixity; |
|
49 type serializer; |
20 type serializer; |
50 val add_serializer : string * serializer -> theory -> theory; |
21 val add_serializer : string * serializer -> theory -> theory; |
51 val ml_from_thingol: serializer; |
22 val ml_from_thingol: serializer; |
52 val hs_from_thingol: serializer; |
23 val hs_from_thingol: serializer; |
|
24 val get_serializer: theory -> string * Args.T list |
|
25 -> string list option -> CodegenThingol.code -> unit; |
|
26 |
|
27 val const_has_serialization: theory -> string list -> string -> bool; |
|
28 val tyco_has_serialization: theory -> string list -> string -> bool; |
|
29 |
|
30 val eval_verbose: bool ref; |
|
31 val eval_term: theory -> |
|
32 (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code |
|
33 -> 'a; |
53 end; |
34 end; |
54 |
35 |
55 structure CodegenSerializer: CODEGEN_SERIALIZER = |
36 structure CodegenSerializer: CODEGEN_SERIALIZER = |
56 struct |
37 struct |
57 |
38 |
118 ("target_atom", "infix", "infixl", "infixr"); |
99 ("target_atom", "infix", "infixl", "infixr"); |
119 val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK]; |
100 val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK]; |
120 |
101 |
121 datatype 'a mixfix = |
102 datatype 'a mixfix = |
122 Arg of fixity |
103 Arg of fixity |
123 | Pretty of Pretty.T |
104 | Pretty of Pretty.T; |
124 | Quote of 'a; |
|
125 |
105 |
126 fun fillin_mixfix fxy_this ms fxy_ctxt pr args = |
106 fun fillin_mixfix fxy_this ms fxy_ctxt pr args = |
127 let |
107 let |
128 fun fillin [] [] = |
108 fun fillin [] [] = |
129 [] |
109 [] |
130 | fillin (Arg fxy :: ms) (a :: args) = |
110 | fillin (Arg fxy :: ms) (a :: args) = |
131 pr fxy a :: fillin ms args |
111 pr fxy a :: fillin ms args |
132 | fillin (Pretty p :: ms) args = |
112 | fillin (Pretty p :: ms) args = |
133 p :: fillin ms args |
113 p :: fillin ms args |
134 | fillin (Quote q :: ms) args = |
|
135 pr BR q :: fillin ms args |
|
136 | fillin [] _ = |
114 | fillin [] _ = |
137 error ("Inconsistent mixfix: too many arguments") |
115 error ("Inconsistent mixfix: too many arguments") |
138 | fillin _ [] = |
116 | fillin _ [] = |
139 error ("Inconsistent mixfix: too less arguments"); |
117 error ("Inconsistent mixfix: too less arguments"); |
140 in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end; |
118 in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end; |
144 val l = case x of L => fixity |
122 val l = case x of L => fixity |
145 | _ => INFX (i, X); |
123 | _ => INFX (i, X); |
146 val r = case x of R => fixity |
124 val r = case x of R => fixity |
147 | _ => INFX (i, X); |
125 | _ => INFX (i, X); |
148 in |
126 in |
149 pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r] |
127 [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r] |
150 end; |
128 end; |
151 |
129 |
152 fun parse_mixfix reader s ctxt = |
130 fun parse_mixfix s = |
153 let |
131 let |
154 fun sym s = Scan.lift ($$ s); |
132 val sym_any = Scan.one Symbol.not_eof; |
155 fun lift_reader ctxt s = |
|
156 ctxt |
|
157 |> reader s |
|
158 |-> (fn x => pair (Quote x)); |
|
159 val sym_any = Scan.lift (Scan.one Symbol.not_eof); |
|
160 val parse = Scan.repeat ( |
133 val parse = Scan.repeat ( |
161 (sym "_" -- sym "_" >> K (Arg NOBR)) |
134 ($$ "_" -- $$ "_" >> K (Arg NOBR)) |
162 || (sym "_" >> K (Arg BR)) |
135 || ($$ "_" >> K (Arg BR)) |
163 || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length)) |
136 || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)) |
164 || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1 |
|
165 ( $$ "'" |-- Scan.one Symbol.not_eof |
|
166 || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --| |
|
167 $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap)) |
|
168 || (Scan.repeat1 |
137 || (Scan.repeat1 |
169 ( sym "'" |-- sym_any |
138 ( $$ "'" |-- sym_any |
170 || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*") |
139 || Scan.unless ($$ "_" || $$ "/") |
171 sym_any) >> (Pretty o str o implode))); |
140 sym_any) >> (Pretty o str o implode))); |
172 in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s) |
141 in case Scan.finite Symbol.stopper parse (Symbol.explode s) |
173 of (p, (ctxt, [])) => (p, ctxt) |
142 of (p, []) => p |
174 | _ => error ("Malformed mixfix annotation: " ^ quote s) |
143 | _ => error ("Malformed mixfix annotation: " ^ quote s) |
175 end; |
144 end; |
176 |
145 |
177 fun parse_syntax num_args reader = |
146 fun parse_syntax num_args = |
178 let |
147 let |
179 fun is_arg (Arg _) = true |
148 fun is_arg (Arg _) = true |
180 | is_arg _ = false; |
149 | is_arg _ = false; |
181 fun parse_nonatomic s ctxt = |
150 fun parse_nonatomic s = |
182 case parse_mixfix reader s ctxt |
151 case parse_mixfix s |
183 of ([Pretty _], _) => |
152 of [Pretty _] => |
184 error ("Mixfix contains just one pretty element; either declare as " |
153 error ("Mixfix contains just one pretty element; either declare as " |
185 ^ quote atomK ^ " or consider adding a break") |
154 ^ quote atomK ^ " or consider adding a break") |
186 | x => x; |
155 | x => x; |
|
156 fun mk fixity mfx ctxt = |
|
157 let |
|
158 val i = (length o List.filter is_arg) mfx; |
|
159 val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else (); |
|
160 in (i, fillin_mixfix fixity mfx) end; |
187 val parse = ( |
161 val parse = ( |
188 OuterParse.$$$ infixK |-- OuterParse.nat |
162 OuterParse.$$$ infixK |-- OuterParse.nat |
189 >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) |
163 >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) |
190 || OuterParse.$$$ infixlK |-- OuterParse.nat |
164 || OuterParse.$$$ infixlK |-- OuterParse.nat |
191 >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) |
165 >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) |
192 || OuterParse.$$$ infixrK |-- OuterParse.nat |
166 || OuterParse.$$$ infixrK |-- OuterParse.nat |
193 >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) |
167 >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) |
194 || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR) |
168 || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR) |
195 || pair (parse_nonatomic, BR) |
169 || pair (parse_nonatomic, BR) |
196 ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy)); |
170 ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy)); |
197 fun mk fixity mfx ctxt = |
171 in |
198 let |
172 parse #-> (fn (mfx, fixity) => pair (mk fixity mfx)) |
199 val i = (length o List.filter is_arg) mfx; |
|
200 val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else (); |
|
201 in ((i, fillin_mixfix fixity mfx), ctxt) end; |
|
202 in |
|
203 parse |
|
204 #-> (fn (mfx_reader, fixity) => |
|
205 pair (mfx_reader #-> (fn mfx => (mk fixity mfx))) |
|
206 ) |
|
207 end; |
173 end; |
208 |
174 |
209 |
175 |
210 (* list and string serializer *) |
176 (* list and string serializer *) |
211 |
177 |
1318 in |
1284 in |
1319 (parse_multi_file ((K o K) NONE) "hs" serializer) args |
1285 (parse_multi_file ((K o K) NONE) "hs" serializer) args |
1320 end; |
1286 end; |
1321 |
1287 |
1322 |
1288 |
1323 (** LEGACY DIAGNOSIS **) |
|
1324 |
|
1325 local |
|
1326 |
|
1327 open CodegenThingol; |
|
1328 |
|
1329 in |
|
1330 |
|
1331 val pretty_typparms = |
|
1332 Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks) |
|
1333 [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]); |
|
1334 |
|
1335 fun pretty_itype (tyco `%% tys) = |
|
1336 Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys) |
|
1337 | pretty_itype (ty1 `-> ty2) = |
|
1338 Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2] |
|
1339 | pretty_itype (ITyVar v) = |
|
1340 Pretty.str v; |
|
1341 |
|
1342 fun pretty_iterm (IConst (c, _)) = |
|
1343 Pretty.str c |
|
1344 | pretty_iterm (IVar v) = |
|
1345 Pretty.str ("?" ^ v) |
|
1346 | pretty_iterm (t1 `$ t2) = |
|
1347 (Pretty.enclose "(" ")" o Pretty.breaks) |
|
1348 [pretty_iterm t1, pretty_iterm t2] |
|
1349 | pretty_iterm ((v, ty) `|-> t) = |
|
1350 (Pretty.enclose "(" ")" o Pretty.breaks) |
|
1351 [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t] |
|
1352 | pretty_iterm (INum (n, _)) = |
|
1353 (Pretty.str o IntInf.toString) n |
|
1354 | pretty_iterm (IChar (h, _)) = |
|
1355 (Pretty.str o quote) h |
|
1356 | pretty_iterm (ICase (((t, _), bs), _)) = |
|
1357 (Pretty.enclose "(" ")" o Pretty.breaks) [ |
|
1358 Pretty.str "case", |
|
1359 pretty_iterm t, |
|
1360 Pretty.enclose "(" ")" (map (fn (p, t) => |
|
1361 (Pretty.block o Pretty.breaks) [ |
|
1362 pretty_iterm p, |
|
1363 Pretty.str "=>", |
|
1364 pretty_iterm t |
|
1365 ] |
|
1366 ) bs) |
|
1367 ]; |
|
1368 |
|
1369 fun pretty_def Bot = |
|
1370 Pretty.str "<Bot>" |
|
1371 | pretty_def (Fun (eqs, (vs, ty))) = |
|
1372 Pretty.enum " |" "" "" ( |
|
1373 map (fn (ps, body) => |
|
1374 Pretty.block [ |
|
1375 Pretty.enum "," "[" "]" (map pretty_iterm ps), |
|
1376 Pretty.str " |->", |
|
1377 Pretty.brk 1, |
|
1378 pretty_iterm body, |
|
1379 Pretty.str "::", |
|
1380 pretty_typparms vs, |
|
1381 Pretty.str "/", |
|
1382 pretty_itype ty |
|
1383 ]) eqs |
|
1384 ) |
|
1385 | pretty_def (Datatype (vs, cs)) = |
|
1386 Pretty.block [ |
|
1387 pretty_typparms vs, |
|
1388 Pretty.str " |=> ", |
|
1389 Pretty.enum " |" "" "" |
|
1390 (map (fn (c, tys) => (Pretty.block o Pretty.breaks) |
|
1391 (Pretty.str c :: map pretty_itype tys)) cs) |
|
1392 ] |
|
1393 | pretty_def (Datatypecons dtname) = |
|
1394 Pretty.str ("cons " ^ dtname) |
|
1395 | pretty_def (Class (supcls, (v, mems))) = |
|
1396 Pretty.block [ |
|
1397 Pretty.str ("class var " ^ v ^ " extending "), |
|
1398 Pretty.enum "," "[" "]" (map Pretty.str supcls), |
|
1399 Pretty.str " with ", |
|
1400 Pretty.enum "," "[" "]" |
|
1401 (map (fn (m, ty) => Pretty.block |
|
1402 [Pretty.str (m ^ "::"), pretty_itype ty]) mems) |
|
1403 ] |
|
1404 | pretty_def (Classmember clsname) = |
|
1405 Pretty.block [ |
|
1406 Pretty.str "class member belonging to ", |
|
1407 Pretty.str clsname |
|
1408 ] |
|
1409 | pretty_def (Classinst ((clsname, (tyco, arity)), _)) = |
|
1410 Pretty.block [ |
|
1411 Pretty.str "class instance (", |
|
1412 Pretty.str clsname, |
|
1413 Pretty.str ", (", |
|
1414 Pretty.str tyco, |
|
1415 Pretty.str ", ", |
|
1416 Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o |
|
1417 map Pretty.str o snd) arity), |
|
1418 Pretty.str "))" |
|
1419 ]; |
|
1420 |
|
1421 fun pretty_module code = |
|
1422 Pretty.chunks (map (fn (name, def) => Pretty.block |
|
1423 [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def]) |
|
1424 (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev))); |
|
1425 |
|
1426 fun pretty_deps code = |
|
1427 let |
|
1428 fun one_node key = |
|
1429 let |
|
1430 val preds_ = Graph.imm_preds code key; |
|
1431 val succs_ = Graph.imm_succs code key; |
|
1432 val mutbs = gen_inter (op =) (preds_, succs_); |
|
1433 val preds = subtract (op =) mutbs preds_; |
|
1434 val succs = subtract (op =) mutbs succs_; |
|
1435 in |
|
1436 (Pretty.block o Pretty.fbreaks) ( |
|
1437 Pretty.str key |
|
1438 :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs |
|
1439 @ map (fn s => Pretty.str ("<-- " ^ s)) preds |
|
1440 @ map (fn s => Pretty.str ("--> " ^ s)) succs |
|
1441 ) |
|
1442 end |
|
1443 in |
|
1444 code |
|
1445 |> Graph.strong_conn |
|
1446 |> flat |
|
1447 |> rev |
|
1448 |> map one_node |
|
1449 |> Pretty.chunks |
|
1450 end; |
|
1451 |
|
1452 end; (*local*) |
|
1453 |
|
1454 |
|
1455 |
1289 |
1456 (** theory data **) |
1290 (** theory data **) |
1457 |
1291 |
1458 datatype syntax_expr = SyntaxExpr of { |
1292 datatype syntax_expr = SyntaxExpr of { |
1459 class: ((string * (string -> string option)) * serial) Symtab.table, |
1293 class: ((string * (string -> string option)) * serial) Symtab.table, |
1673 let |
1507 let |
1674 val cs' = AList.make (fn c => Sign.the_const_type thy c) cs; |
1508 val cs' = AList.make (fn c => Sign.the_const_type thy c) cs; |
1675 val cs'' = map (CodegenConsts.norm_of_typ thy) cs'; |
1509 val cs'' = map (CodegenConsts.norm_of_typ thy) cs'; |
1676 in AList.make (CodegenNames.const thy) cs'' end; |
1510 in AList.make (CodegenNames.const thy) cs'' end; |
1677 |
1511 |
1678 fun read_quote reader consts_of target get_init gen raw_it thy = |
1512 fun parse_quote num_of consts_of target get_init adder = |
1679 let |
1513 parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy)); |
1680 val it = reader thy raw_it; |
1514 |
1681 val cs = consts_of thy it; |
1515 fun zip_list (x::xs) f g = |
1682 in |
1516 f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs |
1683 gen thy cs target (get_init thy) [it] |
1517 #-> (fn xys => pair ((x, y) :: xys))); |
1684 |> (fn [it'] => (it', thy)) |
1518 |
1685 end; |
1519 structure P = OuterParse |
1686 |
1520 and K = OuterKeyword |
1687 fun parse_quote num_of reader consts_of target get_init gen adder = |
1521 |
1688 parse_syntax num_of |
1522 fun parse_multi_syntax parse_thing parse_syntax = |
1689 (read_quote reader consts_of target get_init gen) |
1523 P.and_list1 parse_thing |
1690 #-> (fn modifier => pair (modifier #-> adder target)); |
1524 #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :-- |
1691 |
1525 (fn target => zip_list things (parse_syntax target) |
1692 in |
1526 (P.$$$ "and")) --| P.$$$ ")")) |
1693 |
1527 |
1694 val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const; |
1528 val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const; |
1695 val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type; |
1529 val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type; |
1696 |
1530 |
1697 fun parse_syntax_tyco generate target raw_tyco = |
1531 fun parse_syntax_tyco target raw_tyco = |
1698 let |
1532 let |
1699 fun intern thy = read_type thy raw_tyco; |
1533 fun intern thy = read_type thy raw_tyco; |
1700 fun num_of thy = Sign.arity_number thy (intern thy); |
1534 fun num_of thy = Sign.arity_number thy (intern thy); |
1701 fun idf_of thy = CodegenNames.tyco thy (intern thy); |
1535 fun idf_of thy = CodegenNames.tyco thy (intern thy); |
1702 fun read_typ thy = |
1536 fun read_typ thy = |
1703 Sign.read_typ (thy, K NONE); |
1537 Sign.read_typ (thy, K NONE); |
1704 in |
1538 in |
1705 parse_quote num_of read_typ ((K o K) ([], [])) target idf_of generate |
1539 parse_quote num_of ((K o K) ([], [])) target idf_of |
1706 (gen_add_syntax_tyco read_type raw_tyco) |
1540 (gen_add_syntax_tyco read_type raw_tyco) |
1707 end; |
1541 end; |
1708 |
1542 |
1709 fun parse_syntax_const generate target raw_const = |
1543 fun parse_syntax_const target raw_const = |
1710 let |
1544 let |
1711 fun intern thy = CodegenConsts.read_const thy raw_const; |
1545 fun intern thy = CodegenConsts.read_const thy raw_const; |
1712 fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy; |
1546 fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy; |
1713 fun idf_of thy = (CodegenNames.const thy o intern) thy; |
1547 fun idf_of thy = (CodegenNames.const thy o intern) thy; |
1714 in |
1548 in |
1715 parse_quote num_of Sign.read_term CodegenConsts.consts_of target idf_of generate |
1549 parse_quote num_of CodegenConsts.consts_of target idf_of |
1716 (gen_add_syntax_const CodegenConsts.read_const raw_const) |
1550 (gen_add_syntax_const CodegenConsts.read_const raw_const) |
1717 end; |
1551 end; |
|
1552 |
|
1553 val (code_classK, code_instanceK, code_typeK, code_constK) = |
|
1554 ("code_class", "code_instance", "code_type", "code_const"); |
|
1555 |
|
1556 in |
|
1557 |
|
1558 val code_classP = |
|
1559 OuterSyntax.command code_classK "define code syntax for class" K.thy_decl ( |
|
1560 parse_multi_syntax P.xname |
|
1561 (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 |
|
1562 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []) |
|
1563 >> (Toplevel.theory oo fold) (fn (target, syns) => |
|
1564 fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns) |
|
1565 ); |
|
1566 |
|
1567 val code_instanceP = |
|
1568 OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl ( |
|
1569 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) |
|
1570 (fn _ => fn _ => P.name #-> |
|
1571 (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ())) |
|
1572 >> (Toplevel.theory oo fold) (fn (target, syns) => |
|
1573 fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns) |
|
1574 ); |
|
1575 |
|
1576 val code_typeP = |
|
1577 OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl ( |
|
1578 Scan.repeat1 ( |
|
1579 parse_multi_syntax P.xname parse_syntax_tyco |
|
1580 ) |
|
1581 >> (Toplevel.theory o (fold o fold) (fold snd o snd)) |
|
1582 ); |
|
1583 |
|
1584 val code_constP = |
|
1585 OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl ( |
|
1586 Scan.repeat1 ( |
|
1587 parse_multi_syntax P.term parse_syntax_const |
|
1588 ) |
|
1589 >> (Toplevel.theory o (fold o fold) (fold snd o snd)) |
|
1590 ); |
|
1591 |
|
1592 val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP]; |
1718 |
1593 |
1719 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = |
1594 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = |
1720 let |
1595 let |
1721 val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons]; |
1596 val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons]; |
1722 val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons; |
1597 val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons; |