115 ], vars') |
115 ], vars') |
116 end |
116 end |
117 and print_app tyvars is_pat some_thm vars fxy |
117 and print_app tyvars is_pat some_thm vars fxy |
118 (app as ({ sym, typargs, dom, dicts, ... }, ts)) = |
118 (app as ({ sym, typargs, dom, dicts, ... }, ts)) = |
119 let |
119 let |
120 val k = length ts; |
|
121 val typargs' = if is_pat then [] else typargs; |
120 val typargs' = if is_pat then [] else typargs; |
122 val syntax = case sym of |
121 val syntax = case sym of |
123 Constant const => const_syntax const |
122 Constant const => const_syntax const |
124 | _ => NONE; |
123 | _ => NONE; |
125 val applify_dicts = |
124 val applify_dicts = |
126 if is_pat orelse is_some syntax orelse is_constr sym |
125 if is_pat orelse is_some syntax orelse is_constr sym |
127 orelse Code_Thingol.unambiguous_dictss dicts |
126 orelse Code_Thingol.unambiguous_dictss dicts |
128 then fn p => K p |
127 then fn p => K p |
129 else applify_dictss tyvars; |
128 else applify_dictss tyvars; |
130 val (l, print') = case syntax of |
129 val (wanted, print') = case syntax of |
131 NONE => (args_num sym, fn fxy => fn ts => applify_dicts |
130 NONE => (args_num sym, fn fxy => fn ts => applify_dicts |
132 (gen_applify (is_constr sym) "(" ")" |
131 (gen_applify (is_constr sym) "(" ")" |
133 (print_term tyvars is_pat some_thm vars NOBR) fxy |
132 (print_term tyvars is_pat some_thm vars NOBR) fxy |
134 (applify "[" "]" (print_typ tyvars NOBR) |
133 (applify "[" "]" (print_typ tyvars NOBR) |
135 NOBR ((str o deresolve) sym) typargs') ts) dicts) |
134 NOBR ((str o deresolve) sym) typargs') ts) dicts) |
139 (applify "[" "]" (print_typ tyvars NOBR) |
138 (applify "[" "]" (print_typ tyvars NOBR) |
140 NOBR (str s) typargs') ts) dicts) |
139 NOBR (str s) typargs') ts) dicts) |
141 | SOME (k, Complex_printer print) => |
140 | SOME (k, Complex_printer print) => |
142 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy |
141 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy |
143 (ts ~~ take k dom)) |
142 (ts ~~ take k dom)) |
144 in if k = l then print' fxy ts |
143 in if length ts = wanted then print' fxy ts |
145 else if k < l then |
144 else if length ts < wanted then |
146 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) |
145 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.satisfied_application wanted app) |
147 else let |
146 else let |
148 val (ts1, ts23) = chop l ts; |
147 val (ts1, ts23) = chop wanted ts; |
149 in |
148 in |
150 Pretty.block (print' BR ts1 :: map (fn t => Pretty.block |
149 Pretty.block (print' BR ts1 :: map (fn t => Pretty.block |
151 [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) |
150 [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) |
152 end end |
151 end end |
153 and print_bind tyvars some_thm fxy p = |
152 and print_bind tyvars some_thm fxy p = |