--- a/src/Tools/Code/code_haskell.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Jun 07 13:42:38 2010 +0200
@@ -32,9 +32,9 @@
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
- | classbinds => enum "," "(" ")" (
+ | constraints => enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
@@ str " => ";
fun print_typforall tyvars vs = case map fst vs
of [] => []
@@ -194,7 +194,7 @@
@ (if deriving_show name then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
+ | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
@@ -207,32 +207,31 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- Pretty.block (print_typcontext tyvars [(v, map fst superclasses)]),
+ Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
str (deresolve_base name ^ " " ^ lookup_var tyvars v),
str " where {"
],
str "};"
) (map print_classparam classparams)
end
- | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
+ | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
+ 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 (c_inst, [])
+ print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME (k, pr) =>
let
- val (c_inst_name, (_, tys)) = c_inst;
- val const = if (is_some o syntax_const) c_inst_name
- then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
- val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
- val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
+ 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 (the_list const)
- |> intro_vars (map_filter I vs);
+ |> intro_vars (map_filter I (s :: vs));
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -252,7 +251,7 @@
str " where {"
],
str "};"
- ) (map print_instdef classparam_insts)
+ ) (map print_classparam_instance classparam_instances)
end;
in print_stmt end;
--- a/src/Tools/Code/code_ml.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Mon Jun 07 13:42:38 2010 +0200
@@ -32,7 +32,7 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * ((class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
+ * (((class * (string * (string * dict list list))) list * (class * class) list list)
* ((string * const) * (thm * bool)) list));
datatype ml_stmt =
@@ -219,19 +219,19 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
+ (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
let
- fun print_superinst (_, (classrel, dss)) =
+ fun print_super_instance (_, (classrel, dss)) =
concat [
(str o Long_Name.base_name o deresolve) classrel,
str "=",
print_dict is_pseudo_fun NOBR (DictConst dss)
];
- fun print_classparam ((classparam, c_inst), (thm, _)) =
+ fun print_classparam_instance ((classparam, const), (thm, _)) =
concat [
(str o Long_Name.base_name o deresolve) classparam,
str "=",
- print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
+ print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
@@ -243,7 +243,8 @@
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
- (map print_superinst superinsts @ map print_classparam classparams)
+ (map print_super_instance super_instances
+ @ map print_classparam_instance classparam_instances)
:: str ":"
@@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
))
@@ -300,19 +301,19 @@
sig_ps
(Pretty.chunks (ps @| semicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_proj s p = semicolon
(map str ["val", s, "=", "#" ^ s, ":"] @| p);
- fun print_superclass_decl (superclass, classrel) =
+ fun print_super_class_decl (super_class, classrel) =
print_val_decl print_dicttypscheme
- (classrel, ([(v, [class])], (superclass, ITyVar v)));
- fun print_superclass_field (superclass, classrel) =
- print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
- fun print_superclass_proj (superclass, classrel) =
+ (classrel, ([(v, [class])], (super_class, ITyVar v)));
+ fun print_super_class_field (super_class, classrel) =
+ print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
+ fun print_super_class_proj (super_class, classrel) =
print_proj (deresolve classrel)
- (print_dicttypscheme ([(v, [class])], (superclass, ITyVar v)));
+ (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
(classparam, ([(v, [class])], ty));
@@ -323,7 +324,7 @@
(print_typscheme ([(v, [class])], ty));
in pair
(concat [str "type", print_dicttyp (class, ITyVar v)]
- :: map print_superclass_decl superclasses
+ :: map print_super_class_decl super_classes
@ map print_classparam_decl classparams)
(Pretty.chunks (
concat [
@@ -331,11 +332,11 @@
(str o deresolve) class,
str "=",
enum "," "{" "};" (
- map print_superclass_field superclasses
+ map print_super_class_field super_classes
@ map print_classparam_field classparams
)
]
- :: map print_superclass_proj superclasses
+ :: map print_super_class_proj super_classes
@ map print_classparam_proj classparams
))
end;
@@ -552,19 +553,20 @@
@| print_eqns (is_pseudo_fun name) eqs
))
end
- | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
+ | print_def is_pseudo_fun _ definer
+ (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
let
- fun print_superinst (_, (classrel, dss)) =
+ fun print_super_instance (_, (classrel, dss)) =
concat [
(str o deresolve) classrel,
str "=",
print_dict is_pseudo_fun NOBR (DictConst dss)
];
- fun print_classparam ((classparam, c_inst), (thm, _)) =
+ fun print_classparam_instance ((classparam, const), (thm, _)) =
concat [
(str o deresolve) classparam,
str "=",
- print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
+ print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
@@ -575,8 +577,8 @@
:: print_dict_args vs
@ str "="
@@ brackets [
- enum_default "()" ";" "{" "}" (map print_superinst superinsts
- @ map print_classparam classparams),
+ enum_default "()" ";" "{" "}" (map print_super_instance super_instances
+ @ map print_classparam_instance classparam_instances),
str ":",
print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
]
@@ -633,11 +635,11 @@
sig_ps
(Pretty.chunks (ps @| doublesemicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
- fun print_superclass_field (superclass, classrel) =
- print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
+ fun print_super_class_field (super_class, classrel) =
+ print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
(classparam, ([(v, [class])], ty));
@@ -652,7 +654,7 @@
(str o deresolve) class,
str "=",
enum_default "unit" ";" "{" "}" (
- map print_superclass_field superclasses
+ map print_super_class_field super_classes
@ map print_classparam_field classparams
)
];
--- a/src/Tools/Code/code_preproc.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Jun 07 13:42:38 2010 +0200
@@ -262,11 +262,11 @@
of SOME classess => (classess, ([], []))
| NONE => let
val all_classes = complete_proper_sort thy [class];
- val superclasses = remove (op =) class all_classes;
+ val super_classes = remove (op =) class all_classes;
val classess = map (complete_proper_sort thy)
(Sign.arity_sorts thy tyco [class]);
val inst_params = inst_params thy tyco all_classes;
- in (classess, (superclasses, inst_params)) end;
+ in (classess, (super_classes, inst_params)) end;
(* computing instantiations *)
@@ -284,14 +284,14 @@
|> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
|> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
end end
-and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
+and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
let
- val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
- in if member (op =) old_styps tyco_styps then vardeps_data
+ val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
+ in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
else
vardeps_data
- |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
- |> fold (ensure_typmatch_inst thy arities eqngr tyco_styps) classes
+ |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
+ |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
end
and add_dep thy arities eqngr c_k c_k' vardeps_data =
let
@@ -311,20 +311,20 @@
and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
if member (op =) insts inst then vardeps_data
else let
- val (classess, (superclasses, inst_params)) =
+ val (classess, (super_classes, inst_params)) =
obtain_instance thy arities inst;
in
vardeps_data
|> (apsnd o apsnd) (insert (op =) inst)
|> fold_index (fn (k, _) =>
apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
- |> fold (fn superclass => ensure_inst thy arities eqngr (superclass, tyco)) superclasses
+ |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
|> fold (ensure_fun thy arities eqngr) inst_params
|> fold_index (fn (k, classes) =>
add_classes thy arities eqngr (Inst (class, tyco), k) classes
- #> fold (fn superclass =>
- add_dep thy arities eqngr (Inst (superclass, tyco), k)
- (Inst (class, tyco), k)) superclasses
+ #> fold (fn super_class =>
+ add_dep thy arities eqngr (Inst (super_class, tyco), k)
+ (Inst (class, tyco), k)) super_classes
#> fold (fn inst_param =>
add_dep thy arities eqngr (Fun inst_param, k)
(Inst (class, tyco), k)
--- a/src/Tools/Code/code_scala.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Mon Jun 07 13:42:38 2010 +0200
@@ -212,13 +212,13 @@
:: map print_co cos
)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
+ | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
val tyvars = intro_vars [v] reserved;
val vs = [(v, [name])];
fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
- fun print_superclasses [] = NONE
- | print_superclasses classes = SOME (concat (str "extends"
+ fun print_super_classes [] = NONE
+ | print_super_classes classes = SOME (concat (str "extends"
:: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
fun print_tupled_typ ([], ty) =
print_typ tyvars NOBR ty
@@ -246,13 +246,13 @@
Pretty.chunks (
(Pretty.block_enclose
(concat ([str "trait", add_typarg ((str o deresolve_base) name)]
- @ the_list (print_superclasses superclasses) @ [str "{"]), str "}")
+ @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
)
end
| print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
- (super_instances, classparam_insts))) =
+ ((super_instances, _), classparam_instances))) =
let
val tyvars = intro_vars (map fst vs) reserved;
val insttyp = tyco `%% map (ITyVar o fst) vs;
@@ -260,7 +260,7 @@
fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
- fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
+ fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
let
val auxs = Name.invents (snd reserved) "a" (length tys);
val vars = intro_vars auxs reserved;
@@ -278,10 +278,10 @@
add_typ_params ((str o deresolve_base) name),
str "extends",
Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
- @ map (fn (_, (_, (superinst, _))) => add_typ_params (str ("with " ^ deresolve superinst)))
+ @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance)))
super_instances @| str "{"), str "}")
(map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
- @ map print_classparam_inst classparam_insts),
+ @ map print_classparam_instance classparam_instances),
concat [str "implicit", str (if null vs then "val" else "def"),
applify "(implicit " ")" NOBR (applify "[" "]" NOBR
((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
--- a/src/Tools/Code/code_thingol.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Jun 07 13:42:38 2010 +0200
@@ -72,9 +72,10 @@
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
| Classparam of string * class
- | Classinst of (class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
- * ((string * const) * (thm * bool)) list)
+ | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
+ * (((class * (string * (string * dict list list))) list (*super instances*)
+ * (class * class) list list (*type argument weakening mapping*))
+ * ((string * const) * (thm * bool)) list (*class parameter instances*))
type program = stmt Graph.T
val empty_funs: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -276,8 +277,8 @@
in
fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
-fun namify_classrel thy = namify thy (fn (class1, class2) =>
- Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
+fun namify_classrel thy = namify thy (fn (sub_class, super_class) =>
+ Long_Name.base_name sub_class ^ "_" ^ Long_Name.base_name super_class)
(fn thy => thyname_of_class thy o fst);
(*order fits nicely with composed projections*)
fun namify_tyco thy "fun" = "Pure.fun"
@@ -386,11 +387,12 @@
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 fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
+ (*depends on add_suffix*);
val unfold_fun = unfoldr
(fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
- | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
+ | _ => NONE);
end; (* local *)
@@ -407,8 +409,9 @@
| Classrel of class * class
| Classparam of string * class
| Classinst of (class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
- * ((string * const) * (thm * bool)) list);
+ * (((class * (string * (string * dict list list))) list
+ * (class * class) list list)
+ * ((string * const) * (thm * bool)) list) (*see also signature*);
type program = stmt Graph.T;
@@ -434,8 +437,8 @@
| map_terms_stmt f (stmt as Class _) = stmt
| map_terms_stmt f (stmt as Classrel _) = stmt
| map_terms_stmt f (stmt as Classparam _) = stmt
- | map_terms_stmt f (Classinst (arity, (superinsts, classparams))) =
- Classinst (arity, (superinsts, (map o apfst o apsnd) (fn const =>
+ | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
+ Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
case f (IConst const) of IConst const' => const') classparams));
fun is_cons program name = case Graph.get_node program name
@@ -580,25 +583,25 @@
in ensure_stmt lookup_const (declare_const thy) stmt_const c end
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
let
- val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
+ val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (AxClass.get_info thy class);
val stmt_class =
- fold_map (fn superclass => ensure_class thy algbr eqngr permissive superclass
- ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)) superclasses
+ fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
+ ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
##>> translate_typ thy algbr eqngr permissive ty) cs
#>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
in ensure_stmt lookup_class (declare_class thy) stmt_class class end
-and ensure_classrel thy algbr eqngr permissive (subclass, superclass) =
+and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
let
val stmt_classrel =
- ensure_class thy algbr eqngr permissive subclass
- ##>> ensure_class thy algbr eqngr permissive superclass
+ ensure_class thy algbr eqngr permissive sub_class
+ ##>> ensure_class thy algbr eqngr permissive super_class
#>> Classrel;
- in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
+ in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
let
- val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
+ val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
val classparams = these (try (#params o AxClass.get_info thy) class);
val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -606,31 +609,31 @@
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
val arity_typ = Type (tyco, map TFree vs);
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
- fun translate_superarity superclass =
- ensure_class thy algbr eqngr permissive superclass
- ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)
- ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [superclass])
- #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
- (superclass, (classrel, (inst, dss))));
- fun translate_classparam_inst (c, ty) =
+ fun translate_super_instance super_class =
+ ensure_class thy algbr eqngr permissive super_class
+ ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
+ ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
+ #>> (fn ((super_class, classrel), [DictConst (inst, dss)]) =>
+ (super_class, (classrel, (inst, dss))));
+ fun translate_classparam_instance (c, ty) =
let
- val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
- val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
- val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
+ val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
+ val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
+ val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in
ensure_const thy algbr eqngr permissive c
- ##>> translate_const thy algbr eqngr permissive (SOME thm) (c_ty, NONE)
- #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
+ ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
+ #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
end;
val stmt_inst =
ensure_class thy algbr eqngr permissive class
##>> ensure_tyco thy algbr eqngr permissive tyco
##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
- ##>> fold_map translate_superarity superclasses
- ##>> fold_map translate_classparam_inst classparams
- #>> (fn ((((class, tyco), arity), superinsts), classparams) =>
- Classinst ((class, (tyco, arity)), (superinsts, classparams)));
+ ##>> fold_map translate_super_instance super_classes
+ ##>> fold_map translate_classparam_instance classparams
+ #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
+ Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
@@ -772,8 +775,8 @@
| Local of (class * class) list * (string * (int * sort));
fun class_relation (Global ((_, tyco), yss), _) class =
Global ((class, tyco), yss)
- | class_relation (Local (classrels, v), subclass) superclass =
- Local ((subclass, superclass) :: classrels, v);
+ | class_relation (Local (classrels, v), sub_class) super_class =
+ Local ((sub_class, super_class) :: classrels, v);
fun type_constructor (tyco, _) yss class =
Global ((class, tyco), (map o map) fst yss);
fun type_variable (TFree (v, sort)) =
--- a/src/Tools/nbe.ML Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/nbe.ML Mon Jun 07 13:42:38 2010 +0200
@@ -404,9 +404,9 @@
[]
| eqns_of_stmt (_, Code_Thingol.Datatype _) =
[]
- | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) =
+ | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
- val names = map snd superclasses @ map fst classops;
+ val names = map snd super_classes @ map fst classparams;
val params = Name.invent_list [] "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
@@ -417,10 +417,10 @@
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
- [(inst, (arities, [([], IConst (class, (([], []), [])) `$$
- map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts
- @ map (IConst o snd o fst) instops)]))];
+ | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), ((super_instances, _), classparam_instances))) =
+ [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
+ map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+ @ map (IConst o snd o fst) classparam_instances)]))];
fun compile_stmts ctxt stmts_deps =
let