51 | print_tupled_typ tyvars (tys, ty) = |
51 | print_tupled_typ tyvars (tys, ty) = |
52 concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), |
52 concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), |
53 str "=>", print_typ tyvars NOBR ty]; |
53 str "=>", print_typ tyvars NOBR ty]; |
54 fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; |
54 fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; |
55 fun print_var vars NONE = str "_" |
55 fun print_var vars NONE = str "_" |
56 | print_var vars (SOME v) = (str o lookup_var vars) v |
56 | print_var vars (SOME v) = (str o lookup_var vars) v; |
|
57 fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d |
|
58 and applify_plain_dict tyvars (Dict_Const (inst, dss)) = |
|
59 applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss |
|
60 | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = |
|
61 Pretty.block [str "implicitly", |
|
62 enclose "[" "]" [Pretty.block [(str o deresolve_class) class, |
|
63 enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] |
|
64 and applify_dictss tyvars p dss = |
|
65 applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) |
57 fun print_term tyvars is_pat some_thm vars fxy (IConst const) = |
66 fun print_term tyvars is_pat some_thm vars fxy (IConst const) = |
58 print_app tyvars is_pat some_thm vars fxy (const, []) |
67 print_app tyvars is_pat some_thm vars fxy (const, []) |
59 | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = |
68 | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = |
60 (case Code_Thingol.unfold_const_app t |
69 (case Code_Thingol.unfold_const_app t |
61 of SOME app => print_app tyvars is_pat some_thm vars fxy app |
70 of SOME app => print_app tyvars is_pat some_thm vars fxy app |
86 enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], |
95 enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], |
87 str "=>" |
96 str "=>" |
88 ], vars') |
97 ], vars') |
89 end |
98 end |
90 and print_app tyvars is_pat some_thm vars fxy |
99 and print_app tyvars is_pat some_thm vars fxy |
91 (app as ({ sym, typargs, dom, ... }, ts)) = |
100 (app as ({ sym, typargs, dom, dicts, ... }, ts)) = |
92 let |
101 let |
93 val k = length ts; |
102 val k = length ts; |
94 val typargs' = if is_pat then [] else typargs; |
103 val typargs' = if is_pat then [] else typargs; |
95 val syntax = case sym of |
104 val syntax = case sym of |
96 Constant const => const_syntax const |
105 Constant const => const_syntax const |
97 | _ => NONE; |
106 | _ => NONE; |
|
107 val applify_dicts = |
|
108 if is_pat orelse is_some syntax orelse is_constr sym |
|
109 orelse Code_Thingol.unambiguous_dictss dicts |
|
110 then fn p => K p |
|
111 else applify_dictss tyvars; |
98 val (l, print') = case syntax of |
112 val (l, print') = case syntax of |
99 NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")" |
113 NONE => (args_num sym, fn fxy => fn ts => applify_dicts |
|
114 (gen_applify (is_constr sym) "(" ")" |
100 (print_term tyvars is_pat some_thm vars NOBR) fxy |
115 (print_term tyvars is_pat some_thm vars NOBR) fxy |
101 (applify "[" "]" (print_typ tyvars NOBR) |
116 (applify "[" "]" (print_typ tyvars NOBR) |
102 NOBR ((str o deresolve) sym) typargs') ts) |
117 NOBR ((str o deresolve) sym) typargs') ts) dicts) |
103 | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")" |
118 | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts |
|
119 (applify "(" ")" |
104 (print_term tyvars is_pat some_thm vars NOBR) fxy |
120 (print_term tyvars is_pat some_thm vars NOBR) fxy |
105 (applify "[" "]" (print_typ tyvars NOBR) |
121 (applify "[" "]" (print_typ tyvars NOBR) |
106 NOBR (str s) typargs') ts) |
122 NOBR (str s) typargs') ts) dicts) |
107 | SOME (k, Complex_printer print) => |
123 | SOME (k, Complex_printer print) => |
108 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy |
124 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy |
109 (ts ~~ take k dom)) |
125 (ts ~~ take k dom)) |
110 in if k = l then print' fxy ts |
126 in if k = l then print' fxy ts |
111 else if k < l then |
127 else if k < l then |