removing previous crude approximation to add type annotations to disambiguate types
--- a/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:35 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:36 2011 +0200
@@ -25,7 +25,7 @@
(** Haskell serializer **)
fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
- reserved deresolve contr_classparam_typs deriving_show =
+ reserved deresolve deriving_show =
let
fun class_name class = case class_syntax class
of NONE => deresolve class
@@ -298,7 +298,6 @@
labelled_name module_alias module_prefix (Name.make_context reserved) program;
(* print statements *)
- val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
fun deriv _ "fun" = false
@@ -314,7 +313,7 @@
in deriv [] tyco end;
fun print_stmt deresolve = print_haskell_stmt labelled_name
class_syntax tyco_syntax const_syntax (make_vars reserved)
- deresolve contr_classparam_typs
+ deresolve
(if string_classes then deriving_show else K false);
(* print modules *)
--- a/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:35 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:36 2011 +0200
@@ -88,7 +88,6 @@
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
val is_cons: program -> string -> bool
val is_case: stmt -> bool
- val contr_classparam_typs: program -> string -> itype option list
val labelled_name: theory -> program -> string -> string
val group_stmts: theory -> program
-> ((string * stmt) list * (string * stmt) list
@@ -481,28 +480,6 @@
(fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
Option.map (fn ((const, _), _) => (class, const))
(find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
-
-fun contr_classparam_typs program name =
- let
- fun contr_classparam_typs' (class, name) =
- let
- val Class (_, (_, (_, params))) = Graph.get_node program class;
- val SOME ty = AList.lookup (op =) params name;
- val (tys, res_ty) = unfold_fun ty;
- fun no_tyvar (_ `%% tys) = forall no_tyvar tys
- | no_tyvar (ITyVar _) = false;
- in if no_tyvar res_ty
- then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
- else []
- end
- in
- case Graph.get_node program name
- of Classparam (_, class) => contr_classparam_typs' (class, name)
- | Fun (c, _) => (case lookup_classparam_instance program name
- of NONE => []
- | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
- | _ => []
- end;
fun labelled_name thy program name =
let val ctxt = Proof_Context.init_global thy in