--- a/src/Tools/Code/code_haskell.ML Mon Dec 14 10:59:46 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML Mon Dec 14 11:01:04 2009 +0100
@@ -330,11 +330,12 @@
fun deriving_show tyco =
let
fun deriv _ "fun" = false
- | deriv tycos tyco = member (op =) tycos tyco orelse
- case try (Graph.get_node program) tyco
+ | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
+ andalso (member (op =) tycos tyco
+ orelse case try (Graph.get_node program) tyco
of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
(maps snd cs)
- | NONE => true
+ | NONE => true)
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
--- a/src/Tools/Code/code_thingol.ML Mon Dec 14 10:59:46 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Dec 14 11:01:04 2009 +0100
@@ -36,6 +36,7 @@
signature CODE_THINGOL =
sig
include BASIC_CODE_THINGOL
+ val fun_tyco: string
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
val unfold_fun: itype -> itype list * itype
@@ -388,8 +389,10 @@
of SOME const' => (const', naming)
| NONE => declare_const thy const naming;
+val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
+
val unfold_fun = unfoldr
- (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
+ (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
| _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
end; (* local *)