1.1 --- a/src/Tools/Code/code_haskell.ML Mon Jun 04 12:55:54 2012 +0200
1.2 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 05 07:05:56 2012 +0200
1.3 @@ -60,8 +60,8 @@
1.4 print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
1.5 fun print_typscheme tyvars (vs, ty) =
1.6 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
1.7 - fun print_term tyvars some_thm vars fxy (IConst c) =
1.8 - print_app tyvars some_thm vars fxy (c, [])
1.9 + fun print_term tyvars some_thm vars fxy (IConst const) =
1.10 + print_app tyvars some_thm vars fxy (const, [])
1.11 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
1.12 (case Code_Thingol.unfold_const_app t
1.13 of SOME app => print_app tyvars some_thm vars fxy app
1.14 @@ -79,15 +79,15 @@
1.15 val (binds, t') = Code_Thingol.unfold_pat_abs t;
1.16 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
1.17 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
1.18 - | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
1.19 - (case Code_Thingol.unfold_const_app t0
1.20 - of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
1.21 - then print_case tyvars some_thm vars fxy cases
1.22 - else print_app tyvars some_thm vars fxy c_ts
1.23 - | NONE => print_case tyvars some_thm vars fxy cases)
1.24 - and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
1.25 + | print_term tyvars some_thm vars fxy (ICase case_expr) =
1.26 + (case Code_Thingol.unfold_const_app (#primitive case_expr)
1.27 + of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
1.28 + then print_case tyvars some_thm vars fxy case_expr
1.29 + else print_app tyvars some_thm vars fxy app
1.30 + | NONE => print_case tyvars some_thm vars fxy case_expr)
1.31 + and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
1.32 let
1.33 - val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
1.34 + val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
1.35 val printed_const =
1.36 if annotate then
1.37 brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
1.38 @@ -98,9 +98,11 @@
1.39 end
1.40 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
1.41 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
1.42 - and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
1.43 + and print_case tyvars some_thm vars fxy { clauses = [], ... } =
1.44 + (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
1.45 + | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
1.46 let
1.47 - val (binds, body) = Code_Thingol.unfold_let (ICase cases);
1.48 + val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
1.49 fun print_match ((pat, _), t) vars =
1.50 vars
1.51 |> print_bind tyvars some_thm BR pat
1.52 @@ -110,7 +112,7 @@
1.53 ps
1.54 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
1.55 end
1.56 - | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
1.57 + | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
1.58 let
1.59 fun print_select (pat, body) =
1.60 let
1.61 @@ -119,9 +121,7 @@
1.62 in Pretty.block_enclose
1.63 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
1.64 (map print_select clauses)
1.65 - end
1.66 - | print_case tyvars some_thm vars fxy ((_, []), _) =
1.67 - (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
1.68 + end;
1.69 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
1.70 let
1.71 val tyvars = intro_vars (map fst vs) reserved;
1.72 @@ -221,7 +221,7 @@
1.73 str "};"
1.74 ) (map print_classparam classparams)
1.75 end
1.76 - | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
1.77 + | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
1.78 let
1.79 val tyvars = intro_vars (map fst vs) reserved;
1.80 fun requires_args classparam = case const_syntax classparam
1.81 @@ -237,14 +237,15 @@
1.82 ]
1.83 | SOME k =>
1.84 let
1.85 - val (c, ((_, tys), _)) = const;
1.86 + val { name = c, dom, range, ... } = const;
1.87 val (vs, rhs) = (apfst o map) fst
1.88 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
1.89 val s = if (is_some o const_syntax) c
1.90 then NONE else (SOME o Long_Name.base_name o deresolve) c;
1.91 val vars = reserved
1.92 |> intro_vars (map_filter I (s :: vs));
1.93 - val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
1.94 + val lhs = IConst { name = classparam, typargs = [],
1.95 + dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
1.96 (*dictionaries are not relevant at this late stage,
1.97 and these consts never need type annotations for disambiguation *)
1.98 in
1.99 @@ -264,7 +265,7 @@
1.100 str " where {"
1.101 ],
1.102 str "};"
1.103 - ) (map print_classparam_instance classparam_instances)
1.104 + ) (map print_classparam_instance inst_params)
1.105 end;
1.106 in print_stmt end;
1.107
1.108 @@ -407,7 +408,7 @@
1.109 of SOME ((pat, ty), t') =>
1.110 SOME ((SOME ((pat, ty), true), t1), t')
1.111 | NONE => NONE;
1.112 - fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
1.113 + fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
1.114 if c = c_bind_name then dest_bind t1 t2
1.115 else NONE
1.116 | dest_monad _ t = case Code_Thingol.split_let t