28060
|
1 |
(* Title: Tools/code/code_printer.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Generic operations for pretty printing of target language code.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature CODE_PRINTER =
|
|
9 |
sig
|
|
10 |
val first_upper: string -> string
|
|
11 |
val first_lower: string -> string
|
|
12 |
val dest_name: string -> string * string
|
|
13 |
val mk_name_module: Name.context -> string option -> (string -> string option)
|
|
14 |
-> 'a Graph.T -> string -> string
|
|
15 |
type var_ctxt;
|
|
16 |
val make_vars: string list -> var_ctxt;
|
|
17 |
val intro_vars: string list -> var_ctxt -> var_ctxt;
|
|
18 |
val lookup_var: var_ctxt -> string -> string;
|
|
19 |
|
|
20 |
val @@ : 'a * 'a -> 'a list
|
|
21 |
val @| : 'a list * 'a -> 'a list
|
|
22 |
val str: string -> Pretty.T
|
|
23 |
val concat: Pretty.T list -> Pretty.T
|
|
24 |
val brackets: Pretty.T list -> Pretty.T
|
|
25 |
val semicolon: Pretty.T list -> Pretty.T
|
|
26 |
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
|
|
27 |
|
|
28 |
type lrx
|
|
29 |
val L: lrx
|
|
30 |
val R: lrx
|
|
31 |
val X: lrx
|
|
32 |
type fixity
|
|
33 |
val BR: fixity
|
|
34 |
val NOBR: fixity
|
|
35 |
val INFX: int * lrx -> fixity
|
|
36 |
val APP: fixity
|
|
37 |
val brackify: fixity -> Pretty.T list -> Pretty.T
|
|
38 |
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
|
|
39 |
|
|
40 |
type itype = Code_Thingol.itype
|
|
41 |
type iterm = Code_Thingol.iterm
|
|
42 |
type const = Code_Thingol.const
|
|
43 |
type dict = Code_Thingol.dict
|
|
44 |
type class_syntax
|
|
45 |
type tyco_syntax
|
|
46 |
type const_syntax
|
|
47 |
val parse_infix: ('a -> 'b) -> lrx * int -> string
|
|
48 |
-> int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)
|
|
49 |
val parse_syntax: ('a -> 'b) -> OuterParse.token list
|
|
50 |
-> (int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)) option
|
|
51 |
* OuterParse.token list
|
|
52 |
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) -> fixity
|
|
53 |
-> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
|
|
54 |
val gen_pr_app: (thm -> bool -> var_ctxt -> const * iterm list -> Pretty.T list)
|
|
55 |
-> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
|
|
56 |
-> (string -> const_syntax option) -> (string -> bool)
|
|
57 |
-> thm -> bool -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
|
|
58 |
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
|
|
59 |
-> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
|
|
60 |
-> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
|
|
61 |
|
28064
|
62 |
type literals
|
|
63 |
val Literals: { literal_char: string -> string, literal_string: string -> string,
|
|
64 |
literal_numeral: bool -> int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
|
|
65 |
-> literals
|
|
66 |
val literal_char: literals -> string -> string
|
|
67 |
val literal_string: literals -> string -> string
|
|
68 |
val literal_numeral: literals -> bool -> int -> string
|
|
69 |
val literal_list: literals -> Pretty.T list -> Pretty.T
|
|
70 |
val infix_cons: literals -> int * string
|
|
71 |
|
28060
|
72 |
val nerror: thm -> string -> 'a
|
|
73 |
end;
|
|
74 |
|
|
75 |
structure Code_Printer : CODE_PRINTER =
|
|
76 |
struct
|
|
77 |
|
|
78 |
open Code_Thingol;
|
|
79 |
|
|
80 |
fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
|
|
81 |
|
|
82 |
(** names and naming **)
|
|
83 |
|
|
84 |
(* auxiliary *)
|
|
85 |
|
|
86 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
|
|
87 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
|
|
88 |
|
|
89 |
val dest_name =
|
|
90 |
apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
|
|
91 |
|
|
92 |
fun mk_name_module reserved_names module_prefix module_alias program =
|
|
93 |
let
|
|
94 |
fun mk_alias name = case module_alias name
|
|
95 |
of SOME name' => name'
|
|
96 |
| NONE => name
|
|
97 |
|> NameSpace.explode
|
|
98 |
|> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
|
|
99 |
|> NameSpace.implode;
|
|
100 |
fun mk_prefix name = case module_prefix
|
|
101 |
of SOME module_prefix => NameSpace.append module_prefix name
|
|
102 |
| NONE => name;
|
|
103 |
val tab =
|
|
104 |
Symtab.empty
|
|
105 |
|> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
|
|
106 |
o fst o dest_name o fst)
|
|
107 |
program
|
|
108 |
in the o Symtab.lookup tab end;
|
|
109 |
|
|
110 |
(* variable name contexts *)
|
|
111 |
|
|
112 |
type var_ctxt = string Symtab.table * Name.context;
|
|
113 |
|
|
114 |
fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
|
|
115 |
Name.make_context names);
|
|
116 |
|
|
117 |
fun intro_vars names (namemap, namectxt) =
|
|
118 |
let
|
|
119 |
val (names', namectxt') = Name.variants names namectxt;
|
|
120 |
val namemap' = fold2 (curry Symtab.update) names names' namemap;
|
|
121 |
in (namemap', namectxt') end;
|
|
122 |
|
|
123 |
fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
|
|
124 |
of SOME name' => name'
|
|
125 |
| NONE => error ("Invalid name in context: " ^ quote name);
|
|
126 |
|
|
127 |
|
|
128 |
(** assembling text pieces **)
|
|
129 |
|
|
130 |
infixr 5 @@;
|
|
131 |
infixr 5 @|;
|
|
132 |
fun x @@ y = [x, y];
|
|
133 |
fun xs @| y = xs @ [y];
|
|
134 |
val str = PrintMode.setmp [] Pretty.str;
|
|
135 |
val concat = Pretty.block o Pretty.breaks;
|
|
136 |
val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
|
|
137 |
fun semicolon ps = Pretty.block [concat ps, str ";"];
|
|
138 |
fun enum_default default sep opn cls [] = str default
|
|
139 |
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
|
|
140 |
|
|
141 |
|
|
142 |
(** syntax printer **)
|
|
143 |
|
|
144 |
(* binding priorities *)
|
|
145 |
|
|
146 |
datatype lrx = L | R | X;
|
|
147 |
|
|
148 |
datatype fixity =
|
|
149 |
BR
|
|
150 |
| NOBR
|
|
151 |
| INFX of (int * lrx);
|
|
152 |
|
|
153 |
val APP = INFX (~1, L);
|
|
154 |
|
|
155 |
fun fixity_lrx L L = false
|
|
156 |
| fixity_lrx R R = false
|
|
157 |
| fixity_lrx _ _ = true;
|
|
158 |
|
|
159 |
fun fixity NOBR _ = false
|
|
160 |
| fixity _ NOBR = false
|
|
161 |
| fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
|
|
162 |
pr < pr_ctxt
|
|
163 |
orelse pr = pr_ctxt
|
|
164 |
andalso fixity_lrx lr lr_ctxt
|
|
165 |
orelse pr_ctxt = ~1
|
|
166 |
| fixity BR (INFX _) = false
|
|
167 |
| fixity _ _ = true;
|
|
168 |
|
|
169 |
fun gen_brackify _ [p] = p
|
|
170 |
| gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
|
|
171 |
| gen_brackify false (ps as _::_) = Pretty.block ps;
|
|
172 |
|
|
173 |
fun brackify fxy_ctxt =
|
|
174 |
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
|
|
175 |
|
|
176 |
fun brackify_infix infx fxy_ctxt =
|
|
177 |
gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
|
|
178 |
|
|
179 |
|
|
180 |
(* generic syntax *)
|
|
181 |
|
|
182 |
type class_syntax = string * (string -> string option);
|
|
183 |
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
|
|
184 |
-> fixity -> itype list -> Pretty.T);
|
|
185 |
type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
|
|
186 |
-> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
|
|
187 |
|
|
188 |
fun simple_const_syntax x = (Option.map o apsnd)
|
|
189 |
(fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
|
|
190 |
|
|
191 |
(*int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
|
|
192 |
-> )
|
|
193 |
|
|
194 |
('a * ('b -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)) option
|
|
195 |
*** -> ('a * (('d -> 'b) -> 'e -> 'f -> 'd -> 'c)) option*)
|
|
196 |
|
|
197 |
fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
|
|
198 |
vars fxy (app as ((c, (_, tys)), ts)) =
|
|
199 |
case syntax_const c
|
|
200 |
of NONE => if pat andalso not (is_cons c) then
|
|
201 |
nerror thm "Non-constructor in pattern"
|
|
202 |
else brackify fxy (pr_app thm pat vars app)
|
|
203 |
| SOME (k, pr) =>
|
|
204 |
let
|
|
205 |
fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
|
|
206 |
in if k = length ts
|
|
207 |
then pr' fxy ts
|
|
208 |
else if k < length ts
|
|
209 |
then case chop k ts of (ts1, ts2) =>
|
|
210 |
brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
|
|
211 |
else pr_term thm pat vars fxy (Code_Thingol.eta_expand k app)
|
|
212 |
end;
|
|
213 |
|
|
214 |
fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
|
|
215 |
let
|
|
216 |
val vs = case pat
|
|
217 |
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
|
|
218 |
| NONE => [];
|
|
219 |
val vars' = intro_vars (the_list v) vars;
|
|
220 |
val vars'' = intro_vars vs vars';
|
|
221 |
val v' = Option.map (lookup_var vars') v;
|
|
222 |
val pat' = Option.map (pr_term thm true vars'' fxy) pat;
|
|
223 |
in (pr_bind ((v', pat'), ty), vars'') end;
|
|
224 |
|
|
225 |
|
|
226 |
(* mixfix syntax *)
|
|
227 |
|
|
228 |
datatype 'a mixfix =
|
|
229 |
Arg of fixity
|
|
230 |
| Pretty of Pretty.T;
|
|
231 |
|
|
232 |
fun mk_mixfix prep_arg (fixity_this, mfx) =
|
|
233 |
let
|
|
234 |
fun is_arg (Arg _) = true
|
|
235 |
| is_arg _ = false;
|
|
236 |
val i = (length o filter is_arg) mfx;
|
|
237 |
fun fillin _ [] [] =
|
|
238 |
[]
|
|
239 |
| fillin pr (Arg fxy :: mfx) (a :: args) =
|
|
240 |
(pr fxy o prep_arg) a :: fillin pr mfx args
|
|
241 |
| fillin pr (Pretty p :: mfx) args =
|
|
242 |
p :: fillin pr mfx args;
|
|
243 |
in
|
|
244 |
(i, fn pr => fn fixity_ctxt => fn args =>
|
|
245 |
gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
|
|
246 |
end;
|
|
247 |
|
|
248 |
fun parse_infix prep_arg (x, i) s =
|
|
249 |
let
|
|
250 |
val l = case x of L => INFX (i, L) | _ => INFX (i, X);
|
|
251 |
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
|
|
252 |
in
|
|
253 |
mk_mixfix prep_arg (INFX (i, x),
|
|
254 |
[Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
|
|
255 |
end;
|
|
256 |
|
|
257 |
fun parse_mixfix prep_arg s =
|
|
258 |
let
|
|
259 |
val sym_any = Scan.one Symbol.is_regular;
|
|
260 |
val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
|
|
261 |
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|
|
262 |
|| ($$ "_" >> K (Arg BR))
|
|
263 |
|| ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
|
|
264 |
|| (Scan.repeat1
|
|
265 |
( $$ "'" |-- sym_any
|
|
266 |
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
|
|
267 |
sym_any) >> (Pretty o str o implode)));
|
|
268 |
in case Scan.finite Symbol.stopper parse (Symbol.explode s)
|
|
269 |
of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
|
|
270 |
| ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
|
|
271 |
| _ => Scan.!!
|
|
272 |
(the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
|
|
273 |
end;
|
|
274 |
|
|
275 |
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
|
|
276 |
|
|
277 |
fun parse_syntax prep_arg xs =
|
|
278 |
Scan.option ((
|
|
279 |
((OuterParse.$$$ infixK >> K X)
|
|
280 |
|| (OuterParse.$$$ infixlK >> K L)
|
|
281 |
|| (OuterParse.$$$ infixrK >> K R))
|
|
282 |
-- OuterParse.nat >> parse_infix prep_arg
|
|
283 |
|| Scan.succeed (parse_mixfix prep_arg))
|
|
284 |
-- OuterParse.string
|
|
285 |
>> (fn (parse, s) => parse s)) xs;
|
|
286 |
|
|
287 |
val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
|
|
288 |
|
28064
|
289 |
|
|
290 |
(** pretty literals **)
|
|
291 |
|
|
292 |
datatype literals = Literals of {
|
|
293 |
literal_char: string -> string,
|
|
294 |
literal_string: string -> string,
|
|
295 |
literal_numeral: bool -> int -> string,
|
|
296 |
literal_list: Pretty.T list -> Pretty.T,
|
|
297 |
infix_cons: int * string
|
|
298 |
};
|
|
299 |
|
|
300 |
fun dest_Literals (Literals lits) = lits;
|
|
301 |
|
|
302 |
val literal_char = #literal_char o dest_Literals;
|
|
303 |
val literal_string = #literal_string o dest_Literals;
|
|
304 |
val literal_numeral = #literal_numeral o dest_Literals;
|
|
305 |
val literal_list = #literal_list o dest_Literals;
|
|
306 |
val infix_cons = #infix_cons o dest_Literals;
|
|
307 |
|
28060
|
308 |
end; (*struct*)
|