author | wenzelm |
Mon, 20 May 2013 13:29:45 +0200 | |
changeset 52079 | 291bb1f4af29 |
parent 52070 | fd497099f5f5 |
child 52099 | 6225d5b308f9 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: Tools/Code/code_printer.ML |
28060 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
4 |
Generic operations for pretty printing of target language code. |
|
5 |
*) |
|
6 |
||
7 |
signature CODE_PRINTER = |
|
8 |
sig |
|
32908 | 9 |
type itype = Code_Thingol.itype |
10 |
type iterm = Code_Thingol.iterm |
|
11 |
type const = Code_Thingol.const |
|
12 |
type dict = Code_Thingol.dict |
|
13 |
||
35228 | 14 |
val eqn_error: thm option -> string -> 'a |
28060 | 15 |
|
16 |
val @@ : 'a * 'a -> 'a list |
|
17 |
val @| : 'a list * 'a -> 'a list |
|
18 |
val str: string -> Pretty.T |
|
19 |
val concat: Pretty.T list -> Pretty.T |
|
20 |
val brackets: Pretty.T list -> Pretty.T |
|
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
21 |
val enclose: string -> string -> Pretty.T list -> Pretty.T |
38778 | 22 |
val commas: Pretty.T list -> Pretty.T list |
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
23 |
val enum: string -> string -> string -> Pretty.T list -> Pretty.T |
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
24 |
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T |
28060 | 25 |
val semicolon: Pretty.T list -> Pretty.T |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
26 |
val doublesemicolon: Pretty.T list -> Pretty.T |
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
27 |
val indent: int -> Pretty.T -> Pretty.T |
39056 | 28 |
val markup_stmt: string -> Pretty.T -> Pretty.T |
29 |
val format: string list -> int -> Pretty.T -> string |
|
28060 | 30 |
|
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
31 |
val first_upper: string -> string |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
32 |
val first_lower: string -> string |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
33 |
type var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
34 |
val make_vars: string list -> var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
35 |
val intro_vars: string list -> var_ctxt -> var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
36 |
val lookup_var: var_ctxt -> string -> string |
32913 | 37 |
val intro_base_names: (string -> bool) -> (string -> string) |
38 |
-> string list -> var_ctxt -> var_ctxt |
|
32908 | 39 |
val aux_params: var_ctxt -> iterm list list -> string list |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
40 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
41 |
type literals |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
42 |
val Literals: { literal_char: string -> string, literal_string: string -> string, |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37899
diff
changeset
|
43 |
literal_numeral: int -> string, |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
44 |
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string } |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
45 |
-> literals |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
46 |
val literal_char: literals -> string -> string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
47 |
val literal_string: literals -> string -> string |
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34247
diff
changeset
|
48 |
val literal_numeral: literals -> int -> string |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
49 |
val literal_list: literals -> Pretty.T list -> Pretty.T |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
50 |
val infix_cons: literals -> int * string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
51 |
|
28060 | 52 |
type lrx |
53 |
val L: lrx |
|
54 |
val R: lrx |
|
55 |
val X: lrx |
|
56 |
type fixity |
|
57 |
val BR: fixity |
|
58 |
val NOBR: fixity |
|
59 |
val INFX: int * lrx -> fixity |
|
60 |
val APP: fixity |
|
61 |
val brackify: fixity -> Pretty.T list -> Pretty.T |
|
37242
97097e589715
brackify_infix etc.: no break before infix operator -- eases survival in Scala
haftmann
parents:
37146
diff
changeset
|
62 |
val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T |
31665 | 63 |
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T |
50626
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
64 |
val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T |
37638 | 65 |
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T |
38922 | 66 |
val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option |
67 |
||
52070
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
68 |
datatype ('a, 'b, 'c, 'd, 'e) symbol_attr = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
69 |
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Instance of 'd | Module of 'e |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
70 |
val map_symbol_attr: ('a -> 'f) -> ('b -> 'g) -> ('c -> 'h) -> ('d -> 'i) -> ('e -> 'j) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
71 |
-> ('a, 'b, 'c, 'd, 'e) symbol_attr -> ('f, 'g, 'h, 'i, 'j) symbol_attr |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
72 |
val maps_symbol_attr: ('a -> 'f list) -> ('b -> 'g list) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
73 |
-> ('c -> 'h list) -> ('d -> 'i list) -> ('e -> 'j list) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
74 |
-> ('a, 'b, 'c, 'd, 'e) symbol_attr -> ('f, 'g, 'h, 'i, 'j) symbol_attr list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
75 |
val maps_symbol_attr': ('a -> ('k * 'f) list) -> ('b -> ('k * 'g) list) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
76 |
-> ('c -> ('k * 'h) list) -> ('d -> ('k * 'i) list) -> ('e -> ('k * 'j) list) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
77 |
-> ('a, 'b, 'c, 'd, 'e) symbol_attr -> ('k * ('f, 'g, 'h, 'i, 'j) symbol_attr) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
78 |
type ('a, 'b, 'c, 'd, 'e) symbol_data |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
79 |
val empty_symbol_data: ('a, 'b, 'c, 'd, 'e) symbol_data |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
80 |
val merge_symbol_data: ('a, 'b, 'c, 'd, 'e) symbol_data * ('a, 'b, 'c, 'd, 'e) symbol_data |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
81 |
-> ('a, 'b, 'c, 'd, 'e) symbol_data |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
82 |
val lookup_constant_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> string -> 'a option |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
83 |
val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> string -> 'b option |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
84 |
val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> string -> 'c option |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
85 |
val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> string * string -> 'd option |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
86 |
val lookup_module_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> string -> 'e option |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
87 |
val dest_constant_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> (string * 'a) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
88 |
val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> (string * 'b) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
89 |
val dest_type_class_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> (string * 'c) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
90 |
val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> ((string * string) * 'd) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
91 |
val dest_module_data: ('a, 'b, 'c, 'd, 'e) symbol_data -> (string * 'e) list |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
92 |
val set_symbol_data: (string * 'a option, string * 'b option, string * 'c option, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
93 |
(string * string) * 'd option, string * 'e option) symbol_attr |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
94 |
-> ('a, 'b, 'c, 'd, 'e) symbol_data -> ('a, 'b, 'c, 'd, 'e) symbol_data |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
95 |
|
34152 | 96 |
type simple_const_syntax |
37881 | 97 |
type complex_const_syntax |
28060 | 98 |
type const_syntax |
37881 | 99 |
type activated_complex_const_syntax |
100 |
datatype activated_const_syntax = Plain_const_syntax of int * string |
|
101 |
| Complex_const_syntax of activated_complex_const_syntax |
|
52070
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
102 |
type tyco_syntax |
37881 | 103 |
val requires_args: const_syntax -> int |
52079 | 104 |
val parse_const_syntax: const_syntax parser |
105 |
val parse_tyco_syntax: tyco_syntax parser |
|
37881 | 106 |
val plain_const_syntax: string -> const_syntax |
37876 | 107 |
val simple_const_syntax: simple_const_syntax -> const_syntax |
37881 | 108 |
val complex_const_syntax: complex_const_syntax -> const_syntax |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
109 |
val activate_const_syntax: theory -> literals |
37881 | 110 |
-> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming |
35228 | 111 |
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) |
112 |
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) |
|
37876 | 113 |
-> (string -> activated_const_syntax option) |
35228 | 114 |
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T |
115 |
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) |
|
116 |
-> thm option -> fixity |
|
31889 | 117 |
-> iterm -> var_ctxt -> Pretty.T * var_ctxt |
28060 | 118 |
end; |
119 |
||
120 |
structure Code_Printer : CODE_PRINTER = |
|
121 |
struct |
|
122 |
||
123 |
open Code_Thingol; |
|
124 |
||
39034
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
125 |
(** generic nonsense *) |
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
126 |
|
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
127 |
fun eqn_error (SOME thm) s = |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
128 |
error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm) |
35228 | 129 |
| eqn_error NONE s = error s; |
28060 | 130 |
|
39034
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
131 |
val code_presentationN = "code_presentation"; |
39057
c6d146ed07ae
manage statement selection for presentation wholly through markup
haftmann
parents:
39056
diff
changeset
|
132 |
val stmt_nameN = "stmt_name"; |
39034
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
133 |
val _ = Markup.add_mode code_presentationN YXML.output_markup; |
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
134 |
|
ebeb48fd653b
formal framework for presentation of selected statements
haftmann
parents:
38923
diff
changeset
|
135 |
|
34071 | 136 |
(** assembling and printing text pieces **) |
28060 | 137 |
|
138 |
infixr 5 @@; |
|
139 |
infixr 5 @|; |
|
140 |
fun x @@ y = [x, y]; |
|
141 |
fun xs @| y = xs @ [y]; |
|
39660 | 142 |
val str = Print_Mode.setmp [] Pretty.str; |
28060 | 143 |
val concat = Pretty.block o Pretty.breaks; |
39660 | 144 |
val commas = Print_Mode.setmp [] Pretty.commas; |
145 |
fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r); |
|
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
146 |
val brackets = enclose "(" ")" o Pretty.breaks; |
39660 | 147 |
fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r); |
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
148 |
fun enum_default default sep l r [] = str default |
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
149 |
| enum_default default sep l r xs = enum sep l r xs; |
28060 | 150 |
fun semicolon ps = Pretty.block [concat ps, str ";"]; |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
151 |
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; |
39660 | 152 |
fun indent i = Print_Mode.setmp [] (Pretty.indent i); |
28060 | 153 |
|
39660 | 154 |
fun markup_stmt name = Print_Mode.setmp [code_presentationN] |
39069 | 155 |
(Pretty.mark (code_presentationN, [(stmt_nameN, name)])); |
39062 | 156 |
|
39558 | 157 |
fun filter_presentation [] tree = |
158 |
Buffer.empty |
|
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
159 |
|> fold XML.add_content tree |
39558 | 160 |
| filter_presentation presentation_names tree = |
39057
c6d146ed07ae
manage statement selection for presentation wholly through markup
haftmann
parents:
39056
diff
changeset
|
161 |
let |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
162 |
fun is_selected (name, attrs) = |
39558 | 163 |
name = code_presentationN |
164 |
andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN)); |
|
165 |
fun add_content_with_space tree (is_first, buf) = |
|
166 |
buf |
|
167 |
|> not is_first ? Buffer.add "\n\n" |
|
168 |
|> XML.add_content tree |
|
169 |
|> pair false; |
|
170 |
fun filter (XML.Elem (name_attrs, xs)) = |
|
171 |
fold (if is_selected name_attrs then add_content_with_space else filter) xs |
|
47576 | 172 |
| filter (XML.Text _) = I; |
39558 | 173 |
in snd (fold filter tree (true, Buffer.empty)) end; |
39062 | 174 |
|
175 |
fun format presentation_names width = |
|
39660 | 176 |
Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) |
39062 | 177 |
#> YXML.parse_body |
39558 | 178 |
#> filter_presentation presentation_names |
39678 | 179 |
#> Buffer.add "\n" |
39558 | 180 |
#> Buffer.content; |
34071 | 181 |
|
28060 | 182 |
|
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
183 |
(** names and variable name contexts **) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
184 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
185 |
type var_ctxt = string Symtab.table * Name.context; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
186 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
187 |
fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
188 |
Name.make_context names); |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
189 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
190 |
fun intro_vars names (namemap, namectxt) = |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
191 |
let |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
192 |
val (names', namectxt') = fold_map Name.variant names namectxt; |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
193 |
val namemap' = fold2 (curry Symtab.update) names names' namemap; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
194 |
in (namemap', namectxt') end; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
195 |
|
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
196 |
fun lookup_var (namemap, _) name = |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
197 |
case Symtab.lookup namemap name of |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
198 |
SOME name' => name' |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
199 |
| NONE => error ("Invalid name in context: " ^ quote name); |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
200 |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
39678
diff
changeset
|
201 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode; |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
39678
diff
changeset
|
202 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode; |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
203 |
|
32908 | 204 |
fun aux_params vars lhss = |
205 |
let |
|
206 |
fun fish_param _ (w as SOME _) = w |
|
207 |
| fish_param (IVar (SOME v)) NONE = SOME v |
|
208 |
| fish_param _ NONE = NONE; |
|
209 |
fun fillup_param _ (_, SOME v) = v |
|
210 |
| fillup_param x (i, NONE) = x ^ string_of_int i; |
|
211 |
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
40627
diff
changeset
|
212 |
val x = singleton (Name.variant_list (map_filter I fished1)) "x"; |
32908 | 213 |
val fished2 = map_index (fillup_param x) fished1; |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
214 |
val (fished3, _) = fold_map Name.variant fished2 Name.context; |
32908 | 215 |
val vars' = intro_vars fished3 vars; |
216 |
in map (lookup_var vars') fished3 end; |
|
217 |
||
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
218 |
fun intro_base_names no_syntax deresolve names = names |
32913 | 219 |
|> map_filter (fn name => if no_syntax name then |
220 |
let val name' = deresolve name in |
|
221 |
if Long_Name.is_qualified name' then NONE else SOME name' |
|
222 |
end else NONE) |
|
223 |
|> intro_vars; |
|
224 |
||
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
225 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
226 |
(** pretty literals **) |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
227 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
228 |
datatype literals = Literals of { |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
229 |
literal_char: string -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
230 |
literal_string: string -> string, |
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34247
diff
changeset
|
231 |
literal_numeral: int -> string, |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
232 |
literal_list: Pretty.T list -> Pretty.T, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
233 |
infix_cons: int * string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
234 |
}; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
235 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
236 |
fun dest_Literals (Literals lits) = lits; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
237 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
238 |
val literal_char = #literal_char o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
239 |
val literal_string = #literal_string o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
240 |
val literal_numeral = #literal_numeral o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
241 |
val literal_list = #literal_list o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
242 |
val infix_cons = #infix_cons o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
243 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
244 |
|
28060 | 245 |
(** syntax printer **) |
246 |
||
247 |
(* binding priorities *) |
|
248 |
||
249 |
datatype lrx = L | R | X; |
|
250 |
||
251 |
datatype fixity = |
|
252 |
BR |
|
253 |
| NOBR |
|
254 |
| INFX of (int * lrx); |
|
255 |
||
256 |
val APP = INFX (~1, L); |
|
257 |
||
258 |
fun fixity_lrx L L = false |
|
259 |
| fixity_lrx R R = false |
|
260 |
| fixity_lrx _ _ = true; |
|
261 |
||
262 |
fun fixity NOBR _ = false |
|
263 |
| fixity _ NOBR = false |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
264 |
| fixity (INFX (pr, lr)) (INFX (print_ctxt, lr_ctxt)) = |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
265 |
pr < print_ctxt |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
266 |
orelse pr = print_ctxt |
28060 | 267 |
andalso fixity_lrx lr lr_ctxt |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
268 |
orelse print_ctxt = ~1 |
28060 | 269 |
| fixity BR (INFX _) = false |
270 |
| fixity _ _ = true; |
|
271 |
||
272 |
fun gen_brackify _ [p] = p |
|
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
273 |
| gen_brackify true (ps as _::_) = enclose "(" ")" ps |
28060 | 274 |
| gen_brackify false (ps as _::_) = Pretty.block ps; |
275 |
||
276 |
fun brackify fxy_ctxt = |
|
277 |
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks; |
|
278 |
||
37242
97097e589715
brackify_infix etc.: no break before infix operator -- eases survival in Scala
haftmann
parents:
37146
diff
changeset
|
279 |
fun brackify_infix infx fxy_ctxt (l, m, r) = |
50627 | 280 |
gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r]; |
28060 | 281 |
|
31665 | 282 |
fun brackify_block fxy_ctxt p1 ps p2 = |
283 |
let val p = Pretty.block_enclose (p1, p2) ps |
|
284 |
in if fixity BR fxy_ctxt |
|
34178
a78b8d5b91cb
take care for destructive print mode properly using dedicated pretty builders
haftmann
parents:
34176
diff
changeset
|
285 |
then enclose "(" ")" [p] |
31665 | 286 |
else p |
287 |
end; |
|
288 |
||
50626
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
289 |
fun gen_applify strict opn cls f fxy_ctxt p [] = |
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
290 |
if strict |
50628 | 291 |
then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)] |
50626
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
292 |
else p |
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
293 |
| gen_applify strict opn cls f fxy_ctxt p ps = |
50627 | 294 |
gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps)); |
34247 | 295 |
|
50626
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
296 |
fun applify opn = gen_applify false opn; |
e21485358c56
uniform parentheses for constructor -- necessary to accomodate scala 10
haftmann
parents:
50618
diff
changeset
|
297 |
|
38922 | 298 |
fun tuplify _ _ [] = NONE |
299 |
| tuplify print fxy [x] = SOME (print fxy x) |
|
300 |
| tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); |
|
301 |
||
28060 | 302 |
|
52070
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
303 |
(* data for symbols *) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
304 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
305 |
datatype ('a, 'b, 'c, 'd, 'e) symbol_attr = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
306 |
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Instance of 'd | Module of 'e; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
307 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
308 |
fun map_symbol_attr const tyco class inst module (Constant x) = Constant (const x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
309 |
| map_symbol_attr const tyco class inst module (Type_Constructor x) = Type_Constructor (tyco x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
310 |
| map_symbol_attr const tyco class inst module (Type_Class x) = Type_Class (class x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
311 |
| map_symbol_attr const tyco class inst module (Class_Instance x) = Class_Instance (inst x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
312 |
| map_symbol_attr const tyco class inst module (Module x) = Module (module x); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
313 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
314 |
fun maps_symbol_attr const tyco class inst module (Constant x) = map Constant (const x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
315 |
| maps_symbol_attr const tyco class inst module (Type_Constructor x) = map Type_Constructor (tyco x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
316 |
| maps_symbol_attr const tyco class inst module (Type_Class x) = map Type_Class (class x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
317 |
| maps_symbol_attr const tyco class inst module (Class_Instance x) = map Class_Instance (inst x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
318 |
| maps_symbol_attr const tyco class inst module (Module x) = map Module (module x); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
319 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
320 |
fun maps_symbol_attr' const tyco class inst module (Constant x) = (map o apsnd) Constant (const x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
321 |
| maps_symbol_attr' const tyco class inst module (Type_Constructor x) = (map o apsnd) Type_Constructor (tyco x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
322 |
| maps_symbol_attr' const tyco class inst module (Type_Class x) = (map o apsnd) Type_Class (class x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
323 |
| maps_symbol_attr' const tyco class inst module (Class_Instance x) = (map o apsnd) Class_Instance (inst x) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
324 |
| maps_symbol_attr' const tyco class inst module (Module x) = (map o apsnd) Module (module x); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
325 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
326 |
datatype ('a, 'b, 'c, 'd, 'e) symbol_data = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
327 |
Symbol_Data of { constant: 'a Symtab.table, type_constructor: 'b Symtab.table, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
328 |
type_class: 'c Symtab.table, class_instance: 'd Symreltab.table, module: 'e Symtab.table }; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
329 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
330 |
fun make_symbol_data constant type_constructor type_class class_instance module = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
331 |
Symbol_Data { constant = constant, type_constructor = type_constructor, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
332 |
type_class = type_class, class_instance = class_instance, module = module }; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
333 |
fun dest_symbol_data (Symbol_Data x) = x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
334 |
fun map_symbol_data map_constant map_type_constructor map_type_class map_class_instance map_module |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
335 |
(Symbol_Data { constant, type_constructor, type_class, class_instance, module }) = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
336 |
Symbol_Data { constant = map_constant constant, type_constructor = map_type_constructor type_constructor, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
337 |
type_class = map_type_class type_class, class_instance = map_class_instance class_instance, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
338 |
module = map_module module }; |
28060 | 339 |
|
52070
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
340 |
val empty_symbol_data = Symbol_Data { constant = Symtab.empty, type_constructor = Symtab.empty, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
341 |
type_class = Symtab.empty, class_instance = Symreltab.empty, module = Symtab.empty }; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
342 |
fun merge_symbol_data (Symbol_Data { constant = constant1, type_constructor = type_constructor1, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
343 |
type_class = type_class1, class_instance = class_instance1, module = module1 }, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
344 |
Symbol_Data { constant = constant2, type_constructor = type_constructor2, |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
345 |
type_class = type_class2, class_instance = class_instance2, module = module2 }) = |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
346 |
make_symbol_data (Symtab.join (K snd) (constant1, constant2)) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
347 |
(Symtab.join (K snd) (type_constructor1, type_constructor2)) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
348 |
(Symtab.join (K snd) (type_class1, type_class2)) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
349 |
(Symreltab.join (K snd) (class_instance1, class_instance2)) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
350 |
(Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
351 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
352 |
fun lookup_constant_data x = (Symtab.lookup o #constant o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
353 |
fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
354 |
fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
355 |
fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
356 |
fun lookup_module_data x = (Symtab.lookup o #module o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
357 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
358 |
fun dest_constant_data x = (Symtab.dest o #constant o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
359 |
fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
360 |
fun dest_type_class_data x = (Symtab.dest o #type_class o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
361 |
fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
362 |
fun dest_module_data x = (Symtab.dest o #module o dest_symbol_data) x; |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
363 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
364 |
fun set_sym (sym, NONE) = Symtab.delete_safe sym |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
365 |
| set_sym (sym, SOME y) = Symtab.update (sym, y); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
366 |
fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
367 |
| set_symrel (symrel, SOME y) = Symreltab.update (symrel, y); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
368 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
369 |
fun set_symbol_data (Constant x) = map_symbol_data (set_sym x) I I I I |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
370 |
| set_symbol_data (Type_Constructor x) = map_symbol_data I (set_sym x) I I I |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
371 |
| set_symbol_data (Type_Class x) = map_symbol_data I I (set_sym x) I I |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
372 |
| set_symbol_data (Class_Instance x) = map_symbol_data I I I (set_symrel x) I |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
373 |
| set_symbol_data (Module x) = map_symbol_data I I I I (set_sym x); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
374 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
375 |
|
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
376 |
(* generic syntax *) |
34152 | 377 |
|
378 |
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T) |
|
379 |
-> fixity -> (iterm * itype) list -> Pretty.T); |
|
37881 | 380 |
|
381 |
type complex_const_syntax = int * (string list * (literals -> string list |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
382 |
-> (var_ctxt -> fixity -> iterm -> Pretty.T) |
35228 | 383 |
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)); |
37881 | 384 |
|
385 |
datatype const_syntax = plain_const_syntax of string |
|
386 |
| complex_const_syntax of complex_const_syntax; |
|
387 |
||
388 |
fun requires_args (plain_const_syntax _) = 0 |
|
389 |
| requires_args (complex_const_syntax (k, _)) = k; |
|
28060 | 390 |
|
34176 | 391 |
fun simple_const_syntax syn = |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
392 |
complex_const_syntax |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
393 |
(apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn); |
28060 | 394 |
|
37881 | 395 |
type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) |
396 |
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T) |
|
397 |
||
398 |
datatype activated_const_syntax = Plain_const_syntax of int * string |
|
399 |
| Complex_const_syntax of activated_complex_const_syntax; |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
400 |
|
37881 | 401 |
fun activate_const_syntax thy literals c (plain_const_syntax s) naming = |
402 |
(Plain_const_syntax (Code.args_number thy c, s), naming) |
|
403 |
| activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming = |
|
404 |
fold_map (Code_Thingol.ensure_declared_const thy) cs naming |
|
405 |
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); |
|
406 |
||
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
407 |
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy |
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
47576
diff
changeset
|
408 |
(app as ({ name = c, dom, ... }, ts)) = |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
409 |
case const_syntax c of |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
410 |
NONE => brackify fxy (print_app_expr some_thm vars app) |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
411 |
| SOME (Plain_const_syntax (_, s)) => |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
412 |
brackify fxy (str s :: map (print_term some_thm vars BR) ts) |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
413 |
| SOME (Complex_const_syntax (k, print)) => |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
414 |
let |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
415 |
fun print' fxy ts = |
48072
ace701efe203
prefer records with speaking labels over deeply nested tuples
haftmann
parents:
47576
diff
changeset
|
416 |
print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
417 |
in |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
418 |
if k = length ts |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
419 |
then print' fxy ts |
28060 | 420 |
else if k < length ts |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
421 |
then case chop k ts of (ts1, ts2) => |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
422 |
brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
423 |
else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
424 |
end; |
28060 | 425 |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
426 |
fun gen_print_bind print_term thm (fxy : fixity) pat vars = |
28060 | 427 |
let |
31889 | 428 |
val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; |
31874 | 429 |
val vars' = intro_vars vs vars; |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
430 |
in (print_term thm vars' fxy pat, vars') end; |
28060 | 431 |
|
52070
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
432 |
type tyco_syntax = int * ((fixity -> itype -> Pretty.T) |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
433 |
-> fixity -> itype list -> Pretty.T); |
fd497099f5f5
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
haftmann
parents:
52069
diff
changeset
|
434 |
|
28060 | 435 |
|
436 |
(* mixfix syntax *) |
|
437 |
||
438 |
datatype 'a mixfix = |
|
439 |
Arg of fixity |
|
37881 | 440 |
| String of string |
441 |
| Break; |
|
28060 | 442 |
|
52069 | 443 |
fun printer_of_mixfix prep_arg (fixity_this, mfx) = |
28060 | 444 |
let |
445 |
fun is_arg (Arg _) = true |
|
446 |
| is_arg _ = false; |
|
447 |
val i = (length o filter is_arg) mfx; |
|
448 |
fun fillin _ [] [] = |
|
449 |
[] |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
450 |
| fillin print (Arg fxy :: mfx) (a :: args) = |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
451 |
(print fxy o prep_arg) a :: fillin print mfx args |
37881 | 452 |
| fillin print (String s :: mfx) args = |
453 |
str s :: fillin print mfx args |
|
454 |
| fillin print (Break :: mfx) args = |
|
455 |
Pretty.brk 1 :: fillin print mfx args; |
|
28060 | 456 |
in |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
457 |
(i, fn print => fn fixity_ctxt => fn args => |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
458 |
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) |
28060 | 459 |
end; |
460 |
||
52069 | 461 |
fun read_infix (fixity_this, i) s = |
28060 | 462 |
let |
52069 | 463 |
val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X); |
464 |
val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X); |
|
28060 | 465 |
in |
52069 | 466 |
(INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r]) |
28060 | 467 |
end; |
468 |
||
52069 | 469 |
fun read_mixfix s = |
28060 | 470 |
let |
471 |
val sym_any = Scan.one Symbol.is_regular; |
|
52069 | 472 |
val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat ( |
28060 | 473 |
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) |
474 |
|| ($$ "_" >> K (Arg BR)) |
|
37881 | 475 |
|| ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) |
28060 | 476 |
|| (Scan.repeat1 |
477 |
( $$ "'" |-- sym_any |
|
478 |
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") |
|
37881 | 479 |
sym_any) >> (String o implode))); |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
480 |
fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s) |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
481 |
| err _ (_, SOME msg) = msg; |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
482 |
in |
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
43326
diff
changeset
|
483 |
case Scan.finite Symbol.stopper parse (Symbol.explode s) of |
52069 | 484 |
(fixity_mixfix, []) => fixity_mixfix |
485 |
| _ => Scan.!! (err s) Scan.fail () |
|
28060 | 486 |
end; |
487 |
||
52069 | 488 |
val parse_fixity = |
489 |
(@{keyword "infix"} >> K X) || (@{keyword "infixl"} >> K L) || (@{keyword "infixr"} >> K R) |
|
490 |
||
491 |
val parse_mixfix = |
|
492 |
Parse.string >> read_mixfix |
|
493 |
|| parse_fixity -- Parse.nat -- Parse.string |
|
494 |
>> (fn ((fixity, i), s) => read_infix (fixity, i) s); |
|
28060 | 495 |
|
52069 | 496 |
fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s |
497 |
| syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) = |
|
498 |
of_printer (printer_of_mixfix prep_arg (fixity, mfx)); |
|
37881 | 499 |
|
52069 | 500 |
val parse_tyco_syntax = |
501 |
parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I; |
|
502 |
||
503 |
val parse_const_syntax = |
|
504 |
parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst; |
|
37881 | 505 |
|
28060 | 506 |
end; (*struct*) |