83 (case Code_Thingol.unfold_const_app t0 |
83 (case Code_Thingol.unfold_const_app t0 |
84 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
84 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
85 then print_case tyvars some_thm vars fxy cases |
85 then print_case tyvars some_thm vars fxy cases |
86 else print_app tyvars some_thm vars fxy c_ts |
86 else print_app tyvars some_thm vars fxy c_ts |
87 | NONE => print_case tyvars some_thm vars fxy cases) |
87 | NONE => print_case tyvars some_thm vars fxy cases) |
88 and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) = |
88 and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) = |
89 let |
89 let |
90 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ) |
90 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty) |
91 fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty] |
91 val printed_const = |
|
92 if annotate then |
|
93 brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty] |
|
94 else |
|
95 (str o deresolve) c |
92 in |
96 in |
93 ((if annotate then put_annotation else I) |
97 printed_const :: map (print_term tyvars some_thm vars BR) ts |
94 ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts |
|
95 end |
98 end |
96 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax |
99 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax |
97 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p |
100 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p |
98 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
101 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
99 let |
102 let |
232 str "=", |
235 str "=", |
233 print_app tyvars (SOME thm) reserved NOBR (const, []) |
236 print_app tyvars (SOME thm) reserved NOBR (const, []) |
234 ] |
237 ] |
235 | SOME k => |
238 | SOME k => |
236 let |
239 let |
237 val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *) |
240 val (c, ((_, tys), _)) = const; |
238 val (vs, rhs) = (apfst o map) fst |
241 val (vs, rhs) = (apfst o map) fst |
239 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); |
242 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); |
240 val s = if (is_some o const_syntax) c |
243 val s = if (is_some o const_syntax) c |
241 then NONE else (SOME o Long_Name.base_name o deresolve) c; |
244 then NONE else (SOME o Long_Name.base_name o deresolve) c; |
242 val vars = reserved |
245 val vars = reserved |
243 |> intro_vars (map_filter I (s :: vs)); |
246 |> intro_vars (map_filter I (s :: vs)); |
244 val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs; |
247 val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs; |
245 (*dictionaries are not relevant at this late stage*) |
248 (*dictionaries are not relevant at this late stage, |
|
249 and these consts never need type annotations for disambiguation *) |
246 in |
250 in |
247 semicolon [ |
251 semicolon [ |
248 print_term tyvars (SOME thm) vars NOBR lhs, |
252 print_term tyvars (SOME thm) vars NOBR lhs, |
249 str "=", |
253 str "=", |
250 print_term tyvars (SOME thm) vars NOBR rhs |
254 print_term tyvars (SOME thm) vars NOBR rhs |
321 andalso forall (deriv' tycos) tys |
325 andalso forall (deriv' tycos) tys |
322 | deriv' _ (ITyVar _) = true |
326 | deriv' _ (ITyVar _) = true |
323 in deriv [] tyco end; |
327 in deriv [] tyco end; |
324 fun print_stmt deresolve = print_haskell_stmt labelled_name |
328 fun print_stmt deresolve = print_haskell_stmt labelled_name |
325 class_syntax tyco_syntax const_syntax (make_vars reserved) |
329 class_syntax tyco_syntax const_syntax (make_vars reserved) |
326 deresolve |
330 deresolve (if string_classes then deriving_show else K false); |
327 (if string_classes then deriving_show else K false); |
|
328 |
331 |
329 (* print modules *) |
332 (* print modules *) |
330 val import_includes_ps = |
333 val import_includes_ps = |
331 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes; |
334 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes; |
332 fun print_module_frame module_name ps = |
335 fun print_module_frame module_name ps = |