32 infixr 5 @|; |
32 infixr 5 @|; |
33 |
33 |
34 |
34 |
35 (** Haskell serializer **) |
35 (** Haskell serializer **) |
36 |
36 |
37 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax |
37 fun print_haskell_stmt class_syntax tyco_syntax const_syntax |
38 reserved deresolve deriving_show = |
38 reserved deresolve deriving_show = |
39 let |
39 let |
40 fun class_name class = case class_syntax class |
40 fun class_name class = case class_syntax class |
41 of NONE => deresolve class |
41 of NONE => deresolve class |
42 | SOME class => class; |
42 | SOME class => class; |
50 of [] => [] |
50 of [] => [] |
51 | vnames => str "forall " :: Pretty.breaks |
51 | vnames => str "forall " :: Pretty.breaks |
52 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
52 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
53 fun print_tyco_expr tyvars fxy (tyco, tys) = |
53 fun print_tyco_expr tyvars fxy (tyco, tys) = |
54 brackify fxy (str tyco :: map (print_typ tyvars BR) tys) |
54 brackify fxy (str tyco :: map (print_typ tyvars BR) tys) |
55 and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco |
55 and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco |
56 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) |
56 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) |
57 | SOME (i, print) => print (print_typ tyvars) fxy tys) |
57 | SOME (_, print) => print (print_typ tyvars) fxy tys) |
58 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; |
58 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; |
59 fun print_typdecl tyvars (vs, tycoexpr) = |
59 fun print_typdecl tyvars (vs, tycoexpr) = |
60 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); |
60 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); |
61 fun print_typscheme tyvars (vs, ty) = |
61 fun print_typscheme tyvars (vs, ty) = |
62 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); |
62 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); |
99 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 |
100 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 |
101 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
101 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
102 let |
102 let |
103 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
103 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
104 fun print_match ((pat, ty), t) vars = |
104 fun print_match ((pat, _), t) vars = |
105 vars |
105 vars |
106 |> print_bind tyvars some_thm BR pat |
106 |> print_bind tyvars some_thm BR pat |
107 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) |
107 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) |
108 val (ps, vars') = fold_map print_match binds vars; |
108 val (ps, vars') = fold_map print_match binds vars; |
109 in brackify_block fxy (str "let {") |
109 in brackify_block fxy (str "let {") |
323 | NONE => true) |
323 | NONE => true) |
324 and deriv' tycos (tyco `%% tys) = deriv tycos tyco |
324 and deriv' tycos (tyco `%% tys) = deriv tycos tyco |
325 andalso forall (deriv' tycos) tys |
325 andalso forall (deriv' tycos) tys |
326 | deriv' _ (ITyVar _) = true |
326 | deriv' _ (ITyVar _) = true |
327 in deriv [] tyco end; |
327 in deriv [] tyco end; |
328 fun print_stmt deresolve = print_haskell_stmt labelled_name |
328 fun print_stmt deresolve = print_haskell_stmt |
329 class_syntax tyco_syntax const_syntax (make_vars reserved) |
329 class_syntax tyco_syntax const_syntax (make_vars reserved) |
330 deresolve (if string_classes then deriving_show else K false); |
330 deresolve (if string_classes then deriving_show else K false); |
331 |
331 |
332 (* print modules *) |
332 (* print modules *) |
333 val import_includes_ps = |
333 val import_includes_ps = |