method names in instance declarations are always unqualified
authorhaftmann
Sun, 09 Feb 2014 21:37:27 +0100
changeset 55373 2b4204cb7904
parent 55372 3662c44d018c
child 55374 636a8523876f
method names in instance declarations are always unqualified
src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Feb 09 21:37:27 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sun Feb 09 21:37:27 2014 +0100
@@ -227,37 +227,38 @@
       | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun requires_args classparam = case const_syntax classparam
-             of NONE => NONE
-              | SOME (_, Code_Printer.Plain_printer _) => SOME 0
-              | SOME (k, Code_Printer.Complex_printer _) => SOME k;
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
-              case requires_args classparam
-               of NONE => semicolon [
-                      (str o Long_Name.base_name o deresolve_const) classparam,
+              case const_syntax classparam of
+                NONE => semicolon [
+                    (str o Long_Name.base_name o deresolve_const) classparam,
+                    str "=",
+                    print_app tyvars (SOME thm) reserved NOBR (const, [])
+                  ]
+              | SOME (_, Code_Printer.Plain_printer s) => semicolon [
+                    (str o Long_Name.base_name) s,
+                    str "=",
+                    print_app tyvars (SOME thm) reserved NOBR (const, [])
+                  ]
+              | SOME (k, Code_Printer.Complex_printer _) =>
+                  let
+                    val { sym = Constant c, dom, range, ... } = const;
+                    val (vs, rhs) = (apfst o map) fst
+                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                    val s = if (is_some o const_syntax) c
+                      then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
+                    val vars = reserved
+                      |> intro_vars (map_filter I (s :: vs));
+                    val lhs = IConst { sym = Constant classparam, typargs = [],
+                      dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
+                      (*dictionaries are not relevant at this late stage,
+                        and these consts never need type annotations for disambiguation *)
+                  in
+                    semicolon [
+                      print_term tyvars (SOME thm) vars NOBR lhs,
                       str "=",
-                      print_app tyvars (SOME thm) reserved NOBR (const, [])
+                      print_term tyvars (SOME thm) vars NOBR rhs
                     ]
-                | SOME k =>
-                    let
-                      val { sym = Constant c, dom, range, ... } = const;
-                      val (vs, rhs) = (apfst o map) fst
-                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
-                      val s = if (is_some o const_syntax) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
-                      val vars = reserved
-                        |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst { sym = Constant classparam, typargs = [],
-                        dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
-                        (*dictionaries are not relevant at this late stage,
-                          and these consts never need type annotations for disambiguation *)
-                    in
-                      semicolon [
-                        print_term tyvars (SOME thm) vars NOBR lhs,
-                        str "=",
-                        print_term tyvars (SOME thm) vars NOBR rhs
-                      ]
-                    end;
+                  end;
           in
             Pretty.block_enclose (
               Pretty.block [