author | wenzelm |
Fri, 26 Apr 2024 13:25:44 +0200 | |
changeset 80150 | 96f60533ec1d |
parent 78811 | d3328c562307 |
permissions | -rw-r--r-- |
24582 | 1 |
(* Title: Pure/ML/ml_syntax.ML |
24574 | 2 |
Author: Makarius |
3 |
||
62528 | 4 |
Concrete ML syntax for basic values. |
24574 | 5 |
*) |
6 |
||
7 |
signature ML_SYNTAX = |
|
8 |
sig |
|
9 |
val reserved_names: string list |
|
10 |
val reserved: Name.context |
|
11 |
val is_reserved: string -> bool |
|
12 |
val is_identifier: string -> bool |
|
13 |
val atomic: string -> string |
|
14 |
val print_int: int -> string |
|
15 |
val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string |
|
16 |
val print_list: ('a -> string) -> 'a list -> string |
|
17 |
val print_option: ('a -> string) -> 'a option -> string |
|
69207 | 18 |
val print_symbol_char: Symbol.symbol -> string |
19 |
val print_symbol: Symbol.symbol -> string |
|
24574 | 20 |
val print_string: string -> string |
21 |
val print_strings: string list -> string |
|
69281 | 22 |
val print_path: Path.T -> string |
72288 | 23 |
val print_platform_path: Path.T -> string |
30230 | 24 |
val print_properties: Properties.T -> string |
25 |
val print_position: Position.T -> string |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
26 |
val print_range: Position.range -> string |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69281
diff
changeset
|
27 |
val print_path_binding: Path.binding -> string |
30523 | 28 |
val make_binding: string * Position.T -> string |
24574 | 29 |
val print_indexname: indexname -> string |
30 |
val print_class: class -> string |
|
31 |
val print_sort: sort -> string |
|
32 |
val print_typ: typ -> string |
|
33 |
val print_term: term -> string |
|
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
34 |
val pretty_string: int -> string -> Pretty.T |
24574 | 35 |
end; |
36 |
||
37 |
structure ML_Syntax: ML_SYNTAX = |
|
38 |
struct |
|
39 |
||
40 |
(* reserved words *) |
|
41 |
||
50238
98d35a7368bd
more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents:
43845
diff
changeset
|
42 |
val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords; |
24574 | 43 |
val reserved = Name.make_context reserved_names; |
44 |
val is_reserved = Name.is_declared reserved; |
|
45 |
||
46 |
||
47 |
(* identifiers *) |
|
48 |
||
49 |
fun is_identifier name = |
|
50238
98d35a7368bd
more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents:
43845
diff
changeset
|
50 |
not (is_reserved name) andalso Symbol.is_ascii_identifier name; |
24574 | 51 |
|
52 |
||
53 |
(* literal output -- unformatted *) |
|
54 |
||
55 |
val atomic = enclose "(" ")"; |
|
56 |
||
41491 | 57 |
val print_int = string_of_int; |
24574 | 58 |
|
59 |
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; |
|
60 |
||
61 |
fun print_list f = enclose "[" "]" o commas o map f; |
|
62 |
||
63 |
fun print_option f NONE = "NONE" |
|
64 |
| print_option f (SOME x) = "SOME (" ^ f x ^ ")"; |
|
65 |
||
69207 | 66 |
fun print_symbol_char s = |
62528 | 67 |
if Symbol.is_char s then |
68 |
(case ord s of |
|
69 |
34 => "\\\"" |
|
70 |
| 92 => "\\\\" |
|
65933
f3e4f9e6c485
more correct and complete output of control characters;
wenzelm
parents:
62819
diff
changeset
|
71 |
| 7 => "\\a" |
f3e4f9e6c485
more correct and complete output of control characters;
wenzelm
parents:
62819
diff
changeset
|
72 |
| 8 => "\\b" |
62528 | 73 |
| 9 => "\\t" |
74 |
| 10 => "\\n" |
|
65933
f3e4f9e6c485
more correct and complete output of control characters;
wenzelm
parents:
62819
diff
changeset
|
75 |
| 11 => "\\v" |
f3e4f9e6c485
more correct and complete output of control characters;
wenzelm
parents:
62819
diff
changeset
|
76 |
| 12 => "\\f" |
62528 | 77 |
| 13 => "\\r" |
78 |
| c => |
|
79 |
if c < 32 then "\\^" ^ chr (c + 64) |
|
80 |
else if c < 127 then s |
|
81 |
else "\\" ^ string_of_int c) |
|
82 |
else error ("Bad character: " ^ quote s); |
|
83 |
||
69207 | 84 |
fun print_symbol s = |
85 |
if Symbol.is_char s then print_symbol_char s |
|
86 |
else if Symbol.is_utf8 s then translate_string print_symbol_char s |
|
62528 | 87 |
else s; |
24574 | 88 |
|
69207 | 89 |
val print_string = quote o implode o map print_symbol o Symbol.explode; |
24574 | 90 |
val print_strings = print_list print_string; |
91 |
||
69281 | 92 |
fun print_path path = |
93 |
"Path.explode " ^ print_string (Path.implode path); |
|
94 |
||
72288 | 95 |
val print_platform_path = print_string o File.platform_path; |
96 |
||
30230 | 97 |
val print_properties = print_list (print_pair print_string print_string); |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
98 |
|
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
99 |
fun print_position pos = |
78811 | 100 |
let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in |
101 |
space_implode " " |
|
102 |
["Position.make0", print_int line, print_int offset, print_int end_offset, |
|
103 |
print_string label, print_string file, print_string id] |
|
104 |
end; |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
105 |
|
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
106 |
fun print_range range = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
107 |
"Position.range_of_properties " ^ print_properties (Position.properties_of_range range); |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
108 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69281
diff
changeset
|
109 |
fun print_path_binding binding = |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69281
diff
changeset
|
110 |
"Path.binding " ^ print_pair print_path print_position (Path.dest_binding binding); |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69281
diff
changeset
|
111 |
|
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
112 |
fun make_binding (name, pos) = |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
56184
diff
changeset
|
113 |
"Binding.make " ^ print_pair print_string print_position (name, pos); |
30230 | 114 |
|
24574 | 115 |
val print_indexname = print_pair print_string print_int; |
116 |
||
117 |
val print_class = print_string; |
|
118 |
val print_sort = print_list print_class; |
|
119 |
||
56184
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
120 |
fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
121 |
| print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
122 |
| print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg; |
24574 | 123 |
|
56184
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
124 |
fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
125 |
| print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
126 |
| print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
127 |
| print_term (Bound i) = "Term.Bound " ^ print_int i |
24574 | 128 |
| print_term (Abs (s, T, t)) = |
56184
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
129 |
"Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" |
a2bd40830593
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents:
50238
diff
changeset
|
130 |
| print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2); |
24574 | 131 |
|
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
132 |
|
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
133 |
(* toplevel pretty printing *) |
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
134 |
|
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
135 |
fun pretty_string max_len str = |
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
136 |
let |
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
137 |
val body = |
71456
09c850e82258
more robust pretty printing of broken YXML, e.g. single "\^E";
wenzelm
parents:
70015
diff
changeset
|
138 |
if YXML.is_wellformed str then |
09c850e82258
more robust pretty printing of broken YXML, e.g. single "\^E";
wenzelm
parents:
70015
diff
changeset
|
139 |
maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str) |
09c850e82258
more robust pretty printing of broken YXML, e.g. single "\^E";
wenzelm
parents:
70015
diff
changeset
|
140 |
else Symbol.explode str; |
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
141 |
val body' = |
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
40626
diff
changeset
|
142 |
if length body <= max_len then body |
42047
a7a4e04b5386
pretty_string: proper handling of negative max_len;
wenzelm
parents:
41491
diff
changeset
|
143 |
else take (Int.max (max_len, 0)) body @ ["..."]; |
69207 | 144 |
in Pretty.str (quote (implode (map print_symbol body'))) end; |
37535
75de61a479e3
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents:
31543
diff
changeset
|
145 |
|
77842
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
146 |
fun pretty_string' depth = pretty_string (FixedInt.toInt (depth * 100)); |
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
147 |
|
62663 | 148 |
val _ = |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset
|
149 |
ML_system_pp (fn depth => fn _ => fn str => |
77842
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
150 |
Pretty.to_polyml (pretty_string' depth str)); |
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
151 |
|
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
152 |
val _ = |
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
153 |
ML_system_pp (fn depth => fn _ => fn chunks => |
0eb54e7004eb
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
wenzelm
parents:
72288
diff
changeset
|
154 |
Pretty.to_polyml (pretty_string' depth (Long_Name.implode_chunks chunks))); |
62663 | 155 |
|
24574 | 156 |
end; |