--- a/src/Pure/Tools/class_package.ML Mon Mar 13 10:41:04 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Tue Mar 14 14:25:09 2006 +0100
@@ -24,6 +24,8 @@
val instance_sort_i: class * sort -> theory -> Proof.state
val prove_instance_sort: tactic -> class * sort -> theory -> theory
+ val use_cp_instance: bool ref;
+
val intern_class: theory -> xstring -> class
val intern_sort: theory -> sort -> sort
val extern_class: theory -> class -> xstring
@@ -45,10 +47,11 @@
type sortcontext = (string * sort) list
datatype classlookup = Instance of (class * string) * classlookup list list
- | Lookup of class list * (string * int)
+ | Lookup of class list * (string * (int * int))
val extract_sortctxt: theory -> typ -> sortcontext
val extract_classlookup: theory -> string * typ -> classlookup list list
val extract_classlookup_inst: theory -> class * string -> class -> classlookup list list
+ val extract_classlookup_member: theory -> typ * typ -> classlookup list list
end;
structure ClassPackage: CLASS_PACKAGE =
@@ -176,7 +179,7 @@
let
val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
val arity =
- (fst o the o AList.lookup (op =) (the_instances thy class)) tyco
+ Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class];
val clsvar = (#var o the_class_data thy) class;
val const_sign = (snd o the_consts_sign thy) class;
fun add_var sort used =
@@ -497,11 +500,10 @@
|> Sign.add_const_constraint_i (c, NONE)
|> pair (c, Type.unvarifyT ty)
end;
- fun check_defs raw_defs c_req thy =
+ fun check_defs0 thy raw_defs c_req =
let
- val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy;
fun get_c raw_def =
- (fst o Sign.cert_def pp o tap_def thy' o snd) raw_def;
+ (fst o Sign.cert_def pp o tap_def thy o snd) raw_def;
val c_given = map get_c raw_defs;
fun eq_c ((c1, ty1), (c2, ty2)) =
let
@@ -509,18 +511,22 @@
val ty2' = Type.varifyT ty2;
in
c1 = c2
- andalso Sign.typ_instance thy' (ty1', ty2')
- andalso Sign.typ_instance thy' (ty2', ty1')
+ andalso Sign.typ_instance thy (ty1', ty2')
+ andalso Sign.typ_instance thy (ty2', ty1')
end;
val _ = case fold (remove eq_c) c_req c_given
of [] => ()
| cs => error ("superfluous definition(s) given for "
- ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy' ty))) cs);
+ ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
val _ = case fold (remove eq_c) c_given c_req
of [] => ()
| cs => error ("no definition(s) given for "
- ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy' ty))) cs);
- in thy end;
+ ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
+ in () end;
+ fun check_defs1 raw_defs c_req thy =
+ let
+ val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy
+ in (check_defs0 thy' raw_defs c_req; thy) end;
fun mangle_alldef_name tyco sort =
Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);
fun note_all tyco sort thms thy =
@@ -530,10 +536,12 @@
fun after_qed cs thy =
thy
|> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
- |> fold (fn class => add_inst_data (class, (tyco, (asorts, Context.theory_name thy)))) sort;
+ |> fold (fn class =>
+ add_inst_data (class, (tyco,
+ (map (operational_sort_of thy) asorts, Context.theory_name thy)))) sort;
in
theory
- |> check_defs raw_defs cs
+ |> check_defs1 raw_defs cs
|> fold_map get_remove_contraint (map fst cs)
||>> add_defs tyco (map (pair NONE) raw_defs)
|-> (fn (cs, defnames) => note_all tyco sort defnames #> pair cs)
@@ -629,15 +637,15 @@
|> filter (not o null o snd);
datatype classlookup = Instance of (class * string) * classlookup list list
- | Lookup of class list * (string * int)
+ | Lookup of class list * (string * (int * int))
fun pretty_lookup' (Instance ((class, tyco), lss)) =
(Pretty.block o Pretty.breaks) (
Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco]
:: map pretty_lookup lss
)
- | pretty_lookup' (Lookup (classes, (v, i))) =
- Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i)])
+ | pretty_lookup' (Lookup (classes, (v, (i, j)))) =
+ Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)])
and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls;
fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
@@ -651,8 +659,7 @@
val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
get_superclass_derivation thy (subclass, superclass)
) subclasses;
- val i' = if length subclasses = 1 then ~1 else i;
- in (rev deriv, i') end;
+ in (rev deriv, (i, length subclasses)) end;
fun mk_lookup (sort_def, (Type (tyco, tys))) =
map (fn class => Instance ((class, tyco),
map2 (curry mk_lookup)
@@ -705,6 +712,8 @@
extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
end;
+fun extract_classlookup_member thy (ty_decl, ty_use) =
+ extract_lookup thy (extract_sortctxt thy ty_decl) ty_decl ty_use;
(* toplevel interface *)
@@ -717,10 +726,13 @@
val (classK, instanceK) = ("class", "instance")
+val use_cp_instance = ref false;
+
fun wrap_add_instance_subclass (class, sort) thy =
case Sign.read_sort thy sort
of [class'] =>
- if (is_some o lookup_class_data thy o Sign.intern_class thy) class
+ if ! use_cp_instance
+ andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class'
then
instance_sort (class, sort) thy
--- a/src/Pure/Tools/codegen_package.ML Mon Mar 13 10:41:04 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Mar 14 14:25:09 2006 +0100
@@ -691,10 +691,10 @@
|> ensure_def_inst thy tabs inst
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls
|-> (fn (inst, ls) => pair (Instance (inst, ls)))
- | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns =
+ | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns =
trns
|> fold_map (ensure_def_class thy tabs) clss
- |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", i))))
+ |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
and mk_fun thy tabs restrict (c, ty1) trns =
case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs)
of SOME ((eq_thms, default), ty2) =>
@@ -734,7 +734,7 @@
||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default
||>> exprsgen_type thy tabs [ty3]
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
- |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) (eqs @ eq_default, (sortctxt, ty)))
+ |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) ((eqs @ eq_default, (sortctxt, ty)), ty3))
end
| NONE => (NONE, trns)
and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
@@ -754,8 +754,12 @@
fun gen_membr (m, ty) trns =
trns
|> mk_fun thy tabs true (m, ty)
- |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_instmem m, funn))
- | NONE => error ("could not derive definition for member " ^ quote m));
+ |-> (fn NONE => error ("could not derive definition for member " ^ quote m)
+ | SOME (funn, ty_use) =>
+ (fold_map o fold_map) (exprgen_classlookup thy tabs)
+ (ClassPackage.extract_classlookup_member thy (ty, ty_use))
+ #-> (fn lss =>
+ pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
in
trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls
@@ -786,7 +790,7 @@
of SOME (c, ty) =>
trns
|> mk_fun thy tabs false (c, ty)
- |-> (fn (SOME funn) => succeed (Fun funn)
+ |-> (fn SOME (funn, _) => succeed (Fun funn)
| NONE => fail ("no defining equations found for " ^ quote c))
| NONE =>
trns
@@ -908,7 +912,8 @@
(* function extractors *)
fun eqextr_defs thy (deftab, _) (c, ty) =
- Option.mapPartial (get_first (fn (ty', (thm, _)) => if eq_typ thy (ty, ty')
+ Option.mapPartial (get_first (fn (ty', (thm, _)) =>
+ if eq_typ thy (ty, ty')
then SOME ([thm], ty')
else NONE
)) (Symtab.lookup deftab c);
--- a/src/Pure/Tools/codegen_serializer.ML Mon Mar 13 10:41:04 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Mar 14 14:25:09 2006 +0100
@@ -407,7 +407,8 @@
str v,
str ":",
case sort
- of [class] => mk_class v class
+ of [] => str "unit"
+ | [class] => mk_class v class
| _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
str ")"
]
@@ -437,7 +438,8 @@
| from_classlookup fxy (Lookup (classes, (v, i))) =
from_lookup BR (string_of_int (i+1) :: classes) (str v)
in case ls
- of [l] => from_classlookup fxy l
+ of [] => str "()"
+ | [l] => from_classlookup fxy l
| ls => (Pretty.list "(" ")" o map (from_classlookup NOBR)) ls
end;
fun ml_from_tycoexpr fxy (tyco, tys) =
@@ -738,43 +740,46 @@
:: (str o resolv) supinst
:: map (ml_from_sortlookup NOBR) lss
);
- fun from_memdef (m, (m', def)) =
+ fun from_memdef (m, ((m', def), lss)) =
(ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
ml_from_label m
:: str "="
:: (str o resolv) m'
- :: map (str o fst) arity
+ :: map (ml_from_sortlookup NOBR) lss
));
+ fun mk_corp rhs =
+ (Pretty.block o Pretty.breaks) (
+ str definer
+ :: (str o resolv) name
+ :: map ml_from_tyvar arity
+ @ [str "=", rhs]
+ );
fun mk_memdefs supclassexprs [] =
Pretty.enum "," "{" "};" (
supclassexprs
- )
+ ) |> mk_corp
| mk_memdefs supclassexprs memdefs =
let
val (defs, assigns) = (split_list o map from_memdef) memdefs;
in
Pretty.chunks [
- [str ("let"), Pretty.fbrk, defs |> Pretty.chunks]
- |> Pretty.block,
- [str ("in "), Pretty.enum "," "{" "} : "
- (supclassexprs @ assigns),
- ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]),
- str " end;"]
- |> Pretty.block
- ]
+ Pretty.block [
+ str "local",
+ Pretty.fbrk,
+ Pretty.chunks defs
+ ],
+ Pretty.block [str "in", Pretty.brk 1,
+ (mk_corp o Pretty.block o Pretty.breaks) [
+ Pretty.enum "," "{" "}" (supclassexprs @ assigns),
+ str ":",
+ ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ]
+ ],
+ str "end; (* instance *)"
+ ]
end;
in
- Pretty.block [
- (Pretty.block o Pretty.breaks) (
- str definer
- :: (str o resolv) name
- :: map ml_from_tyvar arity
- ),
- Pretty.brk 1,
- str "=",
- Pretty.brk 1,
- mk_memdefs (map from_supclass suparities) memdefs
- ] |> SOME
+ mk_memdefs (map from_supclass suparities) memdefs |> SOME
end
| ml_from_def (name, CodegenThingol.Classinstmember) = NONE;
in case defs
@@ -1071,7 +1076,7 @@
hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
str " where",
Pretty.fbrk,
- Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs)
+ Pretty.chunks (map (fn (m, ((_, (eqs, ty)), _)) => hs_from_funeqs (m, (eqs, ty))) memdefs)
] |> SOME
| hs_from_def (_, CodegenThingol.Classinstmember) =
NONE
--- a/src/Pure/Tools/codegen_thingol.ML Mon Mar 13 10:41:04 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Mar 14 14:25:09 2006 +0100
@@ -75,7 +75,7 @@
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * (string * iclasslookup list list)) list)
- * (string * (string * funn)) list
+ * (string * ((string * funn) * iclasslookup list list)) list
| Classinstmember;
type module;
type transact;
@@ -419,7 +419,7 @@
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * (string * iclasslookup list list)) list)
- * (string * (string * funn)) list
+ * (string * ((string * funn) * iclasslookup list list)) list
| Classinstmember;
datatype node = Def of def | Module of node Graph.T;
@@ -799,12 +799,12 @@
fun mk_memdef (m, (sortctxt, ty)) =
case AList.lookup (op =) memdefs m
of NONE => error ("missing definition for member " ^ quote m)
- | SOME (m', (eqs, (sortctxt', ty'))) =>
+ | SOME ((m', (eqs, (sortctxt', ty'))), lss) =>
let
val sortctxt'' = sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity;
val ty'' = instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty;
in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
- then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
+ then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
else
error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
^ (Pretty.output o Pretty.block o Pretty.breaks) [
@@ -839,8 +839,8 @@
) membrs
)
| postprocess_def (name, Classinst (_, memdefs)) =
- (check_samemodule (name :: map (fst o snd) memdefs);
- fold (fn (_, (m', _)) =>
+ (check_samemodule (name :: map (fst o fst o snd) memdefs);
+ fold (fn (_, ((m', _), _)) =>
add_def_incr (m', Classinstmember)
) memdefs
)