diff -r 3b9ca8d2c5fb -r 096c8397c989 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon Jul 19 11:55:44 2010 +0200 @@ -218,30 +218,35 @@ | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = let val tyvars = intro_vars (map fst vs) reserved; - fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam - of NONE => semicolon [ - (str o deresolve_base) classparam, - str "=", - print_app tyvars (SOME thm) reserved NOBR (const, []) - ] - | SOME (k, pr) => - let - val (c, (_, tys)) = const; - val (vs, rhs) = (apfst o map) fst - (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); - val s = if (is_some o syntax_const) c - then NONE else (SOME o Long_Name.base_name o deresolve) c; - val vars = reserved - |> intro_vars (map_filter I (s :: vs)); - val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; - (*dictionaries are not relevant at this late stage*) - in - semicolon [ - print_term tyvars (SOME thm) vars NOBR lhs, + fun requires_args classparam = case syntax_const classparam + of NONE => 0 + | SOME (Code_Printer.Plain_const_syntax _) => 0 + | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k; + fun print_classparam_instance ((classparam, const), (thm, _)) = + case requires_args classparam + of 0 => semicolon [ + (str o deresolve_base) classparam, str "=", - print_term tyvars (SOME thm) vars NOBR rhs + print_app tyvars (SOME thm) reserved NOBR (const, []) ] - end; + | k => + let + val (c, (_, tys)) = const; + val (vs, rhs) = (apfst o map) fst + (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); + val s = if (is_some o syntax_const) c + then NONE else (SOME o Long_Name.base_name o deresolve) c; + val vars = reserved + |> intro_vars (map_filter I (s :: vs)); + val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; + (*dictionaries are not relevant at this late stage*) + in + semicolon [ + print_term tyvars (SOME thm) vars NOBR lhs, + str "=", + print_term tyvars (SOME thm) vars NOBR rhs + ] + end; in Pretty.block_enclose ( Pretty.block [ @@ -459,7 +464,7 @@ in if target = target' then thy |> Code_Target.add_syntax_const target c_bind - (SOME (pretty_haskell_monad c_bind)) + (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) else error "Only Haskell target allows for monad syntax" end;