src/Tools/code/code_haskell.ML
changeset 28687 150a8a1eae1a
parent 28663 bd8438543bf2
child 28708 a1a436f09ec6
     1.1 --- a/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:39 2008 +0200
     1.2 +++ b/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:40 2008 +0200
     1.3 @@ -38,12 +38,7 @@
     1.4      val deresolve_base = NameSpace.base o deresolve;
     1.5      fun class_name class = case syntax_class class
     1.6       of NONE => deresolve class
     1.7 -      | SOME (class, _) => class;
     1.8 -    fun classparam_name class classparam = case syntax_class class
     1.9 -     of NONE => deresolve_base classparam
    1.10 -      | SOME (_, classparam_syntax) => case classparam_syntax classparam
    1.11 -         of NONE => (snd o Code_Name.dest_name) classparam
    1.12 -          | SOME classparam => classparam;
    1.13 +      | SOME class => class;
    1.14      fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    1.15       of [] => []
    1.16        | classbinds => Pretty.enum "," "(" ")" (
    1.17 @@ -231,7 +226,7 @@
    1.18              val tyvars = Code_Name.intro_vars [v] init_syms;
    1.19              fun pr_classparam (classparam, ty) =
    1.20                semicolon [
    1.21 -                (str o classparam_name name) classparam,
    1.22 +                (str o deresolve_base) classparam,
    1.23                  str "::",
    1.24                  pr_typ tyvars NOBR ty
    1.25                ]
    1.26 @@ -248,13 +243,34 @@
    1.27            end
    1.28        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
    1.29            let
    1.30 +            val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
    1.31 +            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
    1.32              val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
    1.33 -            fun pr_instdef ((classparam, c_inst), (thm, _)) =
    1.34 -              semicolon [
    1.35 -                (str o classparam_name class) classparam,
    1.36 -                str "=",
    1.37 -                pr_app tyvars thm false init_syms NOBR (c_inst, [])
    1.38 -              ];
    1.39 +            fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
    1.40 +             of NONE => semicolon [
    1.41 +                    (str o deresolve_base) classparam,
    1.42 +                    str "=",
    1.43 +                    pr_app tyvars thm false init_syms NOBR (c_inst, [])
    1.44 +                  ]
    1.45 +              | SOME (k, pr) =>
    1.46 +                  let
    1.47 +                    val (c_inst_name, (_, tys)) = c_inst;
    1.48 +                    val const = if (is_some o syntax_const) c_inst_name
    1.49 +                      then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
    1.50 +                    val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
    1.51 +                    val (vs, rhs) = unfold_abs_pure proto_rhs;
    1.52 +                    val vars = init_syms
    1.53 +                      |> Code_Name.intro_vars (the_list const)
    1.54 +                      |> Code_Name.intro_vars vs;
    1.55 +                    val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
    1.56 +                      (*dictionaries are not relevant at this late stage*)
    1.57 +                  in
    1.58 +                    semicolon [
    1.59 +                      pr_term tyvars thm false vars NOBR lhs,
    1.60 +                      str "=",
    1.61 +                      pr_term tyvars thm false vars NOBR rhs
    1.62 +                    ]
    1.63 +                  end;
    1.64            in
    1.65              Pretty.block_enclose (
    1.66                Pretty.block [