9 val show_brackets: bool Unsynchronized.ref |
9 val show_brackets: bool Unsynchronized.ref |
10 val show_sorts: bool Unsynchronized.ref |
10 val show_sorts: bool Unsynchronized.ref |
11 val show_types: bool Unsynchronized.ref |
11 val show_types: bool Unsynchronized.ref |
12 val show_no_free_types: bool Unsynchronized.ref |
12 val show_no_free_types: bool Unsynchronized.ref |
13 val show_all_types: bool Unsynchronized.ref |
13 val show_all_types: bool Unsynchronized.ref |
|
14 val show_structs: bool Unsynchronized.ref |
14 val pp_show_brackets: Pretty.pp -> Pretty.pp |
15 val pp_show_brackets: Pretty.pp -> Pretty.pp |
15 end; |
16 end; |
16 |
17 |
17 signature PRINTER = |
18 signature PRINTER = |
18 sig |
19 sig |
19 include PRINTER0 |
20 include PRINTER0 |
20 val term_to_ast: Proof.context -> |
21 val sort_to_ast: Proof.context -> |
21 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast |
22 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast |
22 val typ_to_ast: Proof.context -> |
23 val typ_to_ast: Proof.context -> |
23 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast |
24 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast |
24 val sort_to_ast: Proof.context -> |
25 val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context -> |
25 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast |
26 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast |
26 type prtabs |
27 type prtabs |
27 val empty_prtabs: prtabs |
28 val empty_prtabs: prtabs |
28 val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
29 val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
29 val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
30 val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
30 val merge_prtabs: prtabs -> prtabs -> prtabs |
31 val merge_prtabs: prtabs -> prtabs -> prtabs |
31 val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs |
32 val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring, |
32 -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) |
33 extern_const: string -> xstring} -> Proof.context -> bool -> prtabs -> |
33 -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list |
34 (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) -> |
34 val pretty_typ_ast: Proof.context -> bool -> prtabs |
35 (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list |
35 -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) |
36 val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} -> |
36 -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list |
37 Proof.context -> bool -> prtabs -> |
|
38 (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) -> |
|
39 (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list |
37 end; |
40 end; |
38 |
41 |
39 structure Printer: PRINTER = |
42 structure Printer: PRINTER = |
40 struct |
43 struct |
41 |
44 |
45 val show_types = Unsynchronized.ref false; |
48 val show_types = Unsynchronized.ref false; |
46 val show_sorts = Unsynchronized.ref false; |
49 val show_sorts = Unsynchronized.ref false; |
47 val show_brackets = Unsynchronized.ref false; |
50 val show_brackets = Unsynchronized.ref false; |
48 val show_no_free_types = Unsynchronized.ref false; |
51 val show_no_free_types = Unsynchronized.ref false; |
49 val show_all_types = Unsynchronized.ref false; |
52 val show_all_types = Unsynchronized.ref false; |
|
53 val show_structs = Unsynchronized.ref false; |
50 |
54 |
51 fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp), |
55 fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp), |
52 Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp); |
56 Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp); |
53 |
57 |
54 |
58 |
82 |
86 |
83 (** sort_to_ast, typ_to_ast **) |
87 (** sort_to_ast, typ_to_ast **) |
84 |
88 |
85 fun ast_of_termT ctxt trf tm = |
89 fun ast_of_termT ctxt trf tm = |
86 let |
90 let |
87 fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t |
91 fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t |
88 | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t |
|
89 | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t |
92 | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t |
90 | ast_of (Const (a, _)) = trans a [] |
93 | ast_of (Const (a, _)) = trans a [] |
91 | ast_of (t as _ $ _) = |
94 | ast_of (t as _ $ _) = |
92 (case strip_comb t of |
95 (case strip_comb t of |
93 (Const (a, _), args) => trans a args |
96 (Const (a, _), args) => trans a args |
103 |
106 |
104 |
107 |
105 |
108 |
106 (** term_to_ast **) |
109 (** term_to_ast **) |
107 |
110 |
108 fun mark_freevars ((t as Const (c, _)) $ u) = |
111 fun ast_of_term idents consts ctxt trf |
109 if member (op =) SynExt.standard_token_markers c then (t $ u) |
112 show_all_types no_freeTs show_types show_sorts show_structs tm = |
110 else t $ mark_freevars u |
113 let |
111 | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u |
114 val {structs, fixes} = idents; |
112 | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t) |
115 |
113 | mark_freevars (t as Free _) = Lexicon.const "_free" $ t |
116 fun mark_atoms ((t as Const (c, T)) $ u) = |
114 | mark_freevars (t as Var (xi, T)) = |
117 if member (op =) consts c then (t $ u) |
115 if xi = SynExt.dddot_indexname then Const ("_DDDOT", T) |
118 else Const (Lexicon.mark_const c, T) $ mark_atoms u |
116 else Lexicon.const "_var" $ t |
119 | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u |
117 | mark_freevars a = a; |
120 | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) |
118 |
121 | mark_atoms (Const (c, T)) = Const (Lexicon.mark_const c, T) |
119 fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm = |
122 | mark_atoms (t as Free (x, T)) = |
120 let |
123 let val i = find_index (fn s => s = x) structs + 1 in |
|
124 if i = 0 andalso member (op =) fixes x then |
|
125 Term.Const (Lexicon.mark_fixed x, T) |
|
126 else if i = 1 andalso not show_structs then |
|
127 Lexicon.const "_struct" $ Lexicon.const "_indexdefault" |
|
128 else Lexicon.const "_free" $ t |
|
129 end |
|
130 | mark_atoms (t as Var (xi, T)) = |
|
131 if xi = SynExt.dddot_indexname then Const ("_DDDOT", T) |
|
132 else Lexicon.const "_var" $ t |
|
133 | mark_atoms a = a; |
|
134 |
121 fun prune_typs (t_seen as (Const _, _)) = t_seen |
135 fun prune_typs (t_seen as (Const _, _)) = t_seen |
122 | prune_typs (t as Free (x, ty), seen) = |
136 | prune_typs (t as Free (x, ty), seen) = |
123 if ty = dummyT then (t, seen) |
137 if ty = dummyT then (t, seen) |
124 else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen) |
138 else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen) |
125 else (t, t :: seen) |
139 else (t, t :: seen) |
146 Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts) |
160 Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts) |
147 | ((c as Const ("_bound", _)), Free (x, T) :: ts) => |
161 | ((c as Const ("_bound", _)), Free (x, T) :: ts) => |
148 Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) |
162 Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) |
149 | (Const ("_idtdummy", T), ts) => |
163 | (Const ("_idtdummy", T), ts) => |
150 Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts) |
164 Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts) |
151 | (c' as Const (c, T), ts) => |
165 | (const as Const (c, T), ts) => |
152 if show_all_types |
166 if show_all_types |
153 then Ast.mk_appl (constrain c' T) (map ast_of ts) |
167 then Ast.mk_appl (constrain const T) (map ast_of ts) |
154 else trans c T ts |
168 else trans c T ts |
155 | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts)) |
169 | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts)) |
156 |
170 |
157 and trans a T args = |
171 and trans a T args = |
158 ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args) |
172 ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args) |
289 | synT markup (TypArg p :: symbs, t :: args) = |
305 | synT markup (TypArg p :: symbs, t :: args) = |
290 let |
306 let |
291 val (Ts, args') = synT markup (symbs, args); |
307 val (Ts, args') = synT markup (symbs, args); |
292 in |
308 in |
293 if type_mode then (astT (t, p) @ Ts, args') |
309 if type_mode then (astT (t, p) @ Ts, args') |
294 else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args') |
310 else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args') |
295 end |
311 end |
296 | synT markup (String s :: symbs, args) = |
312 | synT markup (String s :: symbs, args) = |
297 let val (Ts, args') = synT markup (symbs, args); |
313 let val (Ts, args') = synT markup (symbs, args); |
298 in (markup (Pretty.str s) :: Ts, args') end |
314 in (markup (Pretty.str s) :: Ts, args') end |
299 | synT markup (Space s :: symbs, args) = |
315 | synT markup (Space s :: symbs, args) = |
310 | synT markup (Break i :: symbs, args) = |
326 | synT markup (Break i :: symbs, args) = |
311 let |
327 let |
312 val (Ts, args') = synT markup (symbs, args); |
328 val (Ts, args') = synT markup (symbs, args); |
313 val T = if i < 0 then Pretty.fbrk else Pretty.brk i; |
329 val T = if i < 0 then Pretty.fbrk else Pretty.brk i; |
314 in (T :: Ts, args') end |
330 in (T :: Ts, args') end |
315 | synT _ (_ :: _, []) = sys_error "synT" |
|
316 |
331 |
317 and parT markup (pr, args, p, p': int) = #1 (synT markup |
332 and parT markup (pr, args, p, p': int) = #1 (synT markup |
318 (if p > p' orelse |
333 (if p > p' orelse |
319 (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr)) |
334 (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr)) |
320 then [Block (1, Space "(" :: pr @ [Space ")"])] |
335 then [Block (1, Space "(" :: pr @ [Space ")"])] |
321 else pr, args)) |
336 else pr, args)) |
322 |
337 |
323 and atomT a = |
338 and atomT a = a |> Lexicon.unmark |
324 (case try Lexicon.unmark_const a of |
339 {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)), |
325 SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)) |
340 case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)), |
326 | NONE => |
341 case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)), |
327 (case try Lexicon.unmark_fixed a of |
342 case_fixed = fn x => the (token_trans "_free" x), |
328 SOME x => the (token_trans "_free" x) |
343 case_default = Pretty.str} |
329 | NONE => Pretty.str a)) |
|
330 |
344 |
331 and prefixT (_, a, [], _) = [atomT a] |
345 and prefixT (_, a, [], _) = [atomT a] |
332 | prefixT (c, _, args, p) = astT (appT (c, args), p) |
346 | prefixT (c, _, args, p) = astT (appT (c, args), p) |
333 |
347 |
334 and splitT 0 ([x], ys) = (x, ys) |
348 and splitT 0 ([x], ys) = (x, ys) |
335 | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) |
349 | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) |
336 | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) |
350 | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) |
337 | splitT _ _ = sys_error "splitT" |
|
338 |
351 |
339 and combT (tup as (c, a, args, p)) = |
352 and combT (tup as (c, a, args, p)) = |
340 let |
353 let |
341 val nargs = length args; |
354 val nargs = length args; |
342 val markup = Pretty.mark |
355 val markup = a |> Lexicon.unmark |
343 (Markup.const (Lexicon.unmark_const a) handle Fail _ => |
356 {case_class = Pretty.mark o Markup.tclass, |
344 (Markup.fixed (Lexicon.unmark_fixed a))) |
357 case_type = Pretty.mark o Markup.tycon, |
345 handle Fail _ => I; |
358 case_const = Pretty.mark o Markup.const, |
|
359 case_fixed = Pretty.mark o Markup.fixed, |
|
360 case_default = K I}; |
346 |
361 |
347 (*find matching table entry, or print as prefix / postfix*) |
362 (*find matching table entry, or print as prefix / postfix*) |
348 fun prnt ([], []) = prefixT tup |
363 fun prnt ([], []) = prefixT tup |
349 | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs) |
364 | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs) |
350 | prnt ((pr, n, p') :: prnps, tbs) = |
365 | prnt ((pr, n, p') :: prnps, tbs) = |
369 in astT (ast0, p0) end; |
384 in astT (ast0, p0) end; |
370 |
385 |
371 |
386 |
372 (* pretty_term_ast *) |
387 (* pretty_term_ast *) |
373 |
388 |
374 fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast = |
389 fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast = |
375 pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ())) |
390 pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) |
376 trf tokentrf false curried ast 0; |
391 trf tokentrf false curried ast 0; |
377 |
392 |
378 |
393 |
379 (* pretty_typ_ast *) |
394 (* pretty_typ_ast *) |
380 |
395 |
381 fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast = |
396 fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast = |
382 pretty I ctxt (mode_tabs prtabs (print_mode_value ())) |
397 pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I} |
|
398 ctxt (mode_tabs prtabs (print_mode_value ())) |
383 trf tokentrf true false ast 0; |
399 trf tokentrf true false ast 0; |
384 |
400 |
385 end; |
401 end; |