author | haftmann |
Fri, 04 Dec 2009 18:51:15 +0100 | |
changeset 33994 | fc8af744f63c |
parent 33957 | e9afca2118d4 |
parent 33989 | cb136b5f6050 |
child 34071 | 93bfbb557e2e |
permissions | -rw-r--r-- |
28060 | 1 |
(* Title: Tools/code/code_printer.ML |
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 |
||
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
14 |
val eqn_error: thm -> 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 |
|
21 |
val semicolon: Pretty.T list -> Pretty.T |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
22 |
val doublesemicolon: Pretty.T list -> Pretty.T |
28060 | 23 |
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T |
24 |
||
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
25 |
val first_upper: string -> string |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
26 |
val first_lower: string -> string |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
27 |
type var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
28 |
val make_vars: string list -> var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
29 |
val intro_vars: string list -> var_ctxt -> var_ctxt |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
30 |
val lookup_var: var_ctxt -> string -> string |
32913 | 31 |
val intro_base_names: (string -> bool) -> (string -> string) |
32 |
-> string list -> var_ctxt -> var_ctxt |
|
32908 | 33 |
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
|
34 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
35 |
type literals |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
36 |
val Literals: { literal_char: string -> string, literal_string: string -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
37 |
literal_numeral: bool -> int -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
38 |
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
|
39 |
-> literals |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
40 |
val literal_char: literals -> string -> string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
41 |
val literal_string: literals -> string -> string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
42 |
val literal_numeral: literals -> bool -> int -> string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
43 |
val literal_list: literals -> Pretty.T list -> Pretty.T |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
44 |
val infix_cons: literals -> int * string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
45 |
|
28060 | 46 |
type lrx |
47 |
val L: lrx |
|
48 |
val R: lrx |
|
49 |
val X: lrx |
|
50 |
type fixity |
|
51 |
val BR: fixity |
|
52 |
val NOBR: fixity |
|
53 |
val INFX: int * lrx -> fixity |
|
54 |
val APP: fixity |
|
55 |
val brackify: fixity -> Pretty.T list -> Pretty.T |
|
56 |
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T |
|
31665 | 57 |
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T |
28060 | 58 |
|
59 |
type tyco_syntax |
|
60 |
type const_syntax |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
61 |
type proto_const_syntax |
28060 | 62 |
val parse_infix: ('a -> 'b) -> lrx * int -> string |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
63 |
-> int * ((fixity -> 'b -> Pretty.T) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
64 |
-> fixity -> 'a list -> Pretty.T) |
28060 | 65 |
val parse_syntax: ('a -> 'b) -> OuterParse.token list |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
66 |
-> (int * ((fixity -> 'b -> Pretty.T) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
67 |
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
68 |
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
69 |
-> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
70 |
val activate_const_syntax: theory -> literals |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
71 |
-> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
72 |
val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list) |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
73 |
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
74 |
-> (string -> const_syntax option) |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
75 |
-> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
76 |
val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28064
diff
changeset
|
77 |
-> thm -> fixity |
31889 | 78 |
-> iterm -> var_ctxt -> Pretty.T * var_ctxt |
28060 | 79 |
|
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
80 |
val mk_name_module: Name.context -> string option -> (string -> string option) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
81 |
-> 'a Graph.T -> string -> string |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
82 |
val dest_name: string -> string * string |
28060 | 83 |
end; |
84 |
||
85 |
structure Code_Printer : CODE_PRINTER = |
|
86 |
struct |
|
87 |
||
88 |
open Code_Thingol; |
|
89 |
||
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
90 |
fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm); |
28060 | 91 |
|
92 |
(** assembling text pieces **) |
|
93 |
||
94 |
infixr 5 @@; |
|
95 |
infixr 5 @|; |
|
96 |
fun x @@ y = [x, y]; |
|
97 |
fun xs @| y = xs @ [y]; |
|
98 |
val str = PrintMode.setmp [] Pretty.str; |
|
99 |
val concat = Pretty.block o Pretty.breaks; |
|
100 |
val brackets = Pretty.enclose "(" ")" o Pretty.breaks; |
|
101 |
fun semicolon ps = Pretty.block [concat ps, str ";"]; |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
102 |
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; |
28060 | 103 |
fun enum_default default sep opn cls [] = str default |
104 |
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; |
|
105 |
||
106 |
||
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
107 |
(** names and variable name contexts **) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
108 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
109 |
type var_ctxt = string Symtab.table * Name.context; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
110 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
111 |
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
|
112 |
Name.make_context names); |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
113 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
114 |
fun intro_vars names (namemap, namectxt) = |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
115 |
let |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
116 |
val (names', namectxt') = Name.variants names namectxt; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
117 |
val namemap' = fold2 (curry Symtab.update) names names' namemap; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
118 |
in (namemap', namectxt') end; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
119 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
120 |
fun lookup_var (namemap, _) name = case Symtab.lookup namemap name |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
121 |
of SOME name' => name' |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
122 |
| NONE => error ("Invalid name in context: " ^ quote name); |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
123 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
124 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
125 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
126 |
|
32908 | 127 |
fun aux_params vars lhss = |
128 |
let |
|
129 |
fun fish_param _ (w as SOME _) = w |
|
130 |
| fish_param (IVar (SOME v)) NONE = SOME v |
|
131 |
| fish_param _ NONE = NONE; |
|
132 |
fun fillup_param _ (_, SOME v) = v |
|
133 |
| fillup_param x (i, NONE) = x ^ string_of_int i; |
|
134 |
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); |
|
135 |
val x = Name.variant (map_filter I fished1) "x"; |
|
136 |
val fished2 = map_index (fillup_param x) fished1; |
|
137 |
val (fished3, _) = Name.variants fished2 Name.context; |
|
138 |
val vars' = intro_vars fished3 vars; |
|
139 |
in map (lookup_var vars') fished3 end; |
|
140 |
||
32913 | 141 |
fun intro_base_names no_syntax deresolve names = names |
142 |
|> map_filter (fn name => if no_syntax name then |
|
143 |
let val name' = deresolve name in |
|
144 |
if Long_Name.is_qualified name' then NONE else SOME name' |
|
145 |
end else NONE) |
|
146 |
|> intro_vars; |
|
147 |
||
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
148 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
149 |
(** pretty literals **) |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
150 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
151 |
datatype literals = Literals of { |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
152 |
literal_char: string -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
153 |
literal_string: string -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
154 |
literal_numeral: bool -> int -> string, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
155 |
literal_list: Pretty.T list -> Pretty.T, |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
156 |
infix_cons: int * string |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
157 |
}; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
158 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
159 |
fun dest_Literals (Literals lits) = lits; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
160 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
161 |
val literal_char = #literal_char o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
162 |
val literal_string = #literal_string o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
163 |
val literal_numeral = #literal_numeral o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
164 |
val literal_list = #literal_list o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
165 |
val infix_cons = #infix_cons o dest_Literals; |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
166 |
|
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
167 |
|
28060 | 168 |
(** syntax printer **) |
169 |
||
170 |
(* binding priorities *) |
|
171 |
||
172 |
datatype lrx = L | R | X; |
|
173 |
||
174 |
datatype fixity = |
|
175 |
BR |
|
176 |
| NOBR |
|
177 |
| INFX of (int * lrx); |
|
178 |
||
179 |
val APP = INFX (~1, L); |
|
180 |
||
181 |
fun fixity_lrx L L = false |
|
182 |
| fixity_lrx R R = false |
|
183 |
| fixity_lrx _ _ = true; |
|
184 |
||
185 |
fun fixity NOBR _ = false |
|
186 |
| fixity _ NOBR = false |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
187 |
| fixity (INFX (pr, lr)) (INFX (print_ctxt, lr_ctxt)) = |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
188 |
pr < print_ctxt |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
189 |
orelse pr = print_ctxt |
28060 | 190 |
andalso fixity_lrx lr lr_ctxt |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
191 |
orelse print_ctxt = ~1 |
28060 | 192 |
| fixity BR (INFX _) = false |
193 |
| fixity _ _ = true; |
|
194 |
||
195 |
fun gen_brackify _ [p] = p |
|
196 |
| gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps |
|
197 |
| gen_brackify false (ps as _::_) = Pretty.block ps; |
|
198 |
||
199 |
fun brackify fxy_ctxt = |
|
200 |
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks; |
|
201 |
||
202 |
fun brackify_infix infx fxy_ctxt = |
|
203 |
gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks; |
|
204 |
||
31665 | 205 |
fun brackify_block fxy_ctxt p1 ps p2 = |
206 |
let val p = Pretty.block_enclose (p1, p2) ps |
|
207 |
in if fixity BR fxy_ctxt |
|
208 |
then Pretty.enclose "(" ")" [p] |
|
209 |
else p |
|
210 |
end; |
|
211 |
||
28060 | 212 |
|
213 |
(* generic syntax *) |
|
214 |
||
215 |
type tyco_syntax = int * ((fixity -> itype -> Pretty.T) |
|
216 |
-> fixity -> itype list -> Pretty.T); |
|
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
217 |
type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
218 |
-> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
219 |
type proto_const_syntax = int * (string list * (literals -> string list |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
220 |
-> (var_ctxt -> fixity -> iterm -> Pretty.T) |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
221 |
-> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)); |
28060 | 222 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
223 |
fun simple_const_syntax (SOME (n, f)) = SOME (n, |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
224 |
([], (fn _ => fn _ => fn print => fn thm => fn vars => f (print vars)))) |
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
225 |
| simple_const_syntax NONE = NONE; |
28060 | 226 |
|
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
227 |
fun activate_const_syntax thy literals (n, (cs, f)) naming = |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
228 |
fold_map (Code_Thingol.ensure_declared_const thy) cs naming |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
229 |
|-> (fn cs' => pair (n, f literals cs')); |
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
30648
diff
changeset
|
230 |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
231 |
fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) = |
28060 | 232 |
case syntax_const c |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
233 |
of NONE => brackify fxy (print_app_expr thm vars app) |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
234 |
| SOME (k, print) => |
28060 | 235 |
let |
33994 | 236 |
fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys); |
28060 | 237 |
in if k = length ts |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
238 |
then print' fxy ts |
28060 | 239 |
else if k < length ts |
240 |
then case chop k ts of (ts1, ts2) => |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
241 |
brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2) |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
242 |
else print_term thm vars fxy (Code_Thingol.eta_expand k app) |
28060 | 243 |
end; |
244 |
||
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
245 |
fun gen_print_bind print_term thm (fxy : fixity) pat vars = |
28060 | 246 |
let |
31889 | 247 |
val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; |
31874 | 248 |
val vars' = intro_vars vs vars; |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
249 |
in (print_term thm vars' fxy pat, vars') end; |
28060 | 250 |
|
251 |
||
252 |
(* mixfix syntax *) |
|
253 |
||
254 |
datatype 'a mixfix = |
|
255 |
Arg of fixity |
|
256 |
| Pretty of Pretty.T; |
|
257 |
||
258 |
fun mk_mixfix prep_arg (fixity_this, mfx) = |
|
259 |
let |
|
260 |
fun is_arg (Arg _) = true |
|
261 |
| is_arg _ = false; |
|
262 |
val i = (length o filter is_arg) mfx; |
|
263 |
fun fillin _ [] [] = |
|
264 |
[] |
|
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
265 |
| fillin print (Arg fxy :: mfx) (a :: args) = |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
266 |
(print fxy o prep_arg) a :: fillin print mfx args |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
267 |
| fillin print (Pretty p :: mfx) args = |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
268 |
p :: fillin print mfx args; |
28060 | 269 |
in |
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
270 |
(i, fn print => fn fixity_ctxt => fn args => |
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32924
diff
changeset
|
271 |
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) |
28060 | 272 |
end; |
273 |
||
274 |
fun parse_infix prep_arg (x, i) s = |
|
275 |
let |
|
276 |
val l = case x of L => INFX (i, L) | _ => INFX (i, X); |
|
277 |
val r = case x of R => INFX (i, R) | _ => INFX (i, X); |
|
278 |
in |
|
279 |
mk_mixfix prep_arg (INFX (i, x), |
|
280 |
[Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]) |
|
281 |
end; |
|
282 |
||
283 |
fun parse_mixfix prep_arg s = |
|
284 |
let |
|
285 |
val sym_any = Scan.one Symbol.is_regular; |
|
286 |
val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat ( |
|
287 |
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) |
|
288 |
|| ($$ "_" >> K (Arg BR)) |
|
289 |
|| ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)) |
|
290 |
|| (Scan.repeat1 |
|
291 |
( $$ "'" |-- sym_any |
|
292 |
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") |
|
293 |
sym_any) >> (Pretty o str o implode))); |
|
294 |
in case Scan.finite Symbol.stopper parse (Symbol.explode s) |
|
295 |
of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p) |
|
296 |
| ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p) |
|
297 |
| _ => Scan.!! |
|
298 |
(the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail () |
|
299 |
end; |
|
300 |
||
301 |
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); |
|
302 |
||
303 |
fun parse_syntax prep_arg xs = |
|
304 |
Scan.option (( |
|
305 |
((OuterParse.$$$ infixK >> K X) |
|
306 |
|| (OuterParse.$$$ infixlK >> K L) |
|
307 |
|| (OuterParse.$$$ infixrK >> K R)) |
|
308 |
-- OuterParse.nat >> parse_infix prep_arg |
|
309 |
|| Scan.succeed (parse_mixfix prep_arg)) |
|
310 |
-- OuterParse.string |
|
311 |
>> (fn (parse, s) => parse s)) xs; |
|
312 |
||
313 |
val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK]; |
|
314 |
||
28064 | 315 |
|
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
316 |
(** module name spaces **) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
317 |
|
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
318 |
val dest_name = |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
319 |
apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
320 |
|
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset
|
321 |
fun mk_name_module reserved module_prefix module_alias program = |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
322 |
let |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
323 |
fun mk_alias name = case module_alias name |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
324 |
of SOME name' => name' |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
325 |
| NONE => name |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
326 |
|> Long_Name.explode |
32924
d2e9b2dab760
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
haftmann
parents:
32913
diff
changeset
|
327 |
|> map (fn name => (the_single o fst) (Name.variants [name] reserved)) |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
328 |
|> Long_Name.implode; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
329 |
fun mk_prefix name = case module_prefix |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
330 |
of SOME module_prefix => Long_Name.append module_prefix name |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
331 |
| NONE => name; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
332 |
val tab = |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
333 |
Symtab.empty |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
334 |
|> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
335 |
o fst o dest_name o fst) |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
336 |
program |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
337 |
in the o Symtab.lookup tab end; |
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30161
diff
changeset
|
338 |
|
28060 | 339 |
end; (*struct*) |