--- a/src/Pure/Tools/class_package.ML Mon Jan 23 14:06:11 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Mon Jan 23 14:06:28 2006 +0100
@@ -2,14 +2,14 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Haskell98-like operational view on type classes.
+Type classes, simulated by locales.
*)
signature CLASS_PACKAGE =
sig
- val add_class: bstring -> Locale.expr -> Element.context list -> theory
+ val add_class: bstring -> class list -> Element.context list -> theory
-> ProofContext.context * theory
- val add_class_i: bstring -> Locale.expr -> Element.context_i list -> theory
+ val add_class_i: bstring -> class list -> Element.context_i list -> theory
-> ProofContext.context * theory
val add_instance_arity: (xstring * string list) * string
-> ((bstring * string) * Attrib.src list) list
@@ -19,6 +19,9 @@
-> theory -> Proof.state
val add_classentry: class -> xstring list -> xstring list -> theory -> theory
+ val intern_class: theory -> xstring -> string
+ val extern_class: theory -> string -> xstring
+ val certify_class: theory -> class -> class
val syntactic_sort_of: theory -> sort -> sort
val the_superclasses: theory -> class -> class list
val the_consts_sign: theory -> class -> string * (string * typ) list
@@ -95,7 +98,7 @@
fun get_class_data thy class =
case lookup_class_data thy class
- of NONE => error ("undeclared class " ^ quote class)
+ of NONE => error ("undeclared operational class " ^ quote class)
| SOME data => data;
fun add_class_data (class, (superclasses, name_locale, name_axclass, classvar, consts)) =
@@ -126,6 +129,18 @@
});
+(* name handling *)
+
+fun certify_class thy class =
+ (get_class_data thy class; class);
+
+fun intern_class thy raw_class =
+ certify_class thy (Sign.intern_class thy raw_class);
+
+fun extern_class thy class =
+ Sign.extern_class thy (certify_class thy class);
+
+
(* classes and instances *)
fun subst_clsvar v ty_subst =
@@ -134,10 +149,16 @@
local
-open Element
-
-fun gen_add_class add_locale bname raw_import raw_body thy =
+fun gen_add_class add_locale prep_class bname raw_supclasses raw_body thy =
let
+ val supclasses = map (prep_class thy) raw_supclasses;
+ val supsort = case map (#name_axclass o get_class_data thy) supclasses
+ of [] => Sign.defaultS thy
+ | sort => Sorts.certify_sort (Sign.classes_of thy) sort;
+ val locexpr = case supclasses
+ of [] => Locale.empty
+ | _ => (Locale.Merge o map (Locale.Locale o #name_locale o get_class_data thy))
+ supclasses;
fun extract_assumes c_adds elems =
let
fun subst_free ts =
@@ -149,7 +170,7 @@
in
elems
|> (map o List.mapPartial)
- (fn (Assumes asms) => (SOME o map (map fst o snd)) asms
+ (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms
| _ => NONE)
|> Library.flat o Library.flat o Library.flat
|> subst_free
@@ -157,23 +178,30 @@
fun extract_tyvar_name thy tys =
fold (curry add_typ_tfrees) tys []
|> (fn [(v, sort)] =>
- if Sorts.sort_eq (Sign.classes_of thy) (Sign.defaultS thy, sort)
+ if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
then v
else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
| [] => error ("no class type variable")
| vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
- fun extract_tyvar_consts thy elems =
- elems
- |> Library.flat
- |> List.mapPartial
- (fn (Fixes consts) => SOME consts
- | _ => NONE)
- |> Library.flat
- |> map (fn (c, ty, syn) =>
- ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c) syn))
- |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts))
- |-> (fn v => map ((apfst o apsnd) (subst_clsvar v (TFree (v, []))))
- #> pair v);
+ fun extract_tyvar_consts thy (import_elems, body_elems) =
+ let
+ fun get_elems elems =
+ elems
+ |> Library.flat
+ |> List.mapPartial
+ (fn (Element.Fixes consts) => SOME consts
+ | _ => NONE)
+ |> Library.flat
+ |> map (fn (c, ty, syn) =>
+ ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c) syn))
+ val import_consts = get_elems import_elems;
+ val body_consts = get_elems body_elems;
+ val v = extract_tyvar_name thy (map (snd o fst) (import_consts @ body_consts));
+ fun subst_ty cs =
+ map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
+ val import_cs = subst_ty import_consts;
+ val body_cs = subst_ty body_consts;
+ in (v, (import_cs, body_cs)) end;
fun add_global_const v ((c, ty), syn) thy =
thy
|> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
@@ -181,35 +209,42 @@
fun add_global_constraint v class (_, (c, ty)) thy =
thy
|> Sign.add_const_constraint_i (c, subst_clsvar v (TVar ((v, 0), [class])) ty);
+ fun interpret name_locale cs ax_axioms thy =
+ thy
+ |> Locale.interpretation (NameSpace.base name_locale, [])
+ (Locale.Locale name_locale)
+ (map (fn ((c, _), _) => SOME (Sign.intern_const thy c)) cs)
+ |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE)
+ |> swap;
fun print_ctxt ctxt elem =
map Pretty.writeln (Element.pretty_ctxt ctxt elem)
in
thy
- |> add_locale bname raw_import raw_body
+ |> add_locale bname locexpr raw_body
|-> (fn ((import_elems, body_elems), ctxt) =>
`(fn thy => Locale.intern thy bname)
#-> (fn name_locale =>
- `(fn thy => extract_tyvar_consts thy body_elems)
- #-> (fn (v, c_defs) =>
+ `(fn thy => extract_tyvar_consts thy (import_elems, body_elems))
+ #-> (fn (v, (c_global, c_defs)) =>
fold_map (add_global_const v) c_defs
#-> (fn c_adds =>
- AxClass.add_axclass_i (bname, Sign.defaultS thy)
+ AxClass.add_axclass_i (bname, supsort)
(map (Thm.no_attributes o pair "") (extract_assumes c_adds (import_elems @ body_elems)))
- #-> (fn _ =>
+ #-> (fn { axioms = ax_axioms : thm list, ...} =>
`(fn thy => Sign.intern_class thy bname)
#-> (fn name_axclass =>
fold (add_global_constraint v name_axclass) c_adds
- #> add_class_data (name_locale, ([], name_locale, name_axclass, v, map snd c_adds))
+ #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
#> tap (fn _ => (map o map) (print_ctxt ctxt) import_elems)
#> tap (fn _ => (map o map) (print_ctxt ctxt) body_elems)
- #> pair ctxt
+ #> interpret name_locale (c_global @ c_defs) ax_axioms
))))))
end;
in
-val add_class = gen_add_class (Locale.add_locale_context true);
-val add_class_i = gen_add_class (Locale.add_locale_context_i true);
+val add_class = gen_add_class (Locale.add_locale_context true) intern_class;
+val add_class_i = gen_add_class (Locale.add_locale_context_i true) certify_class;
end; (* local *)
@@ -239,23 +274,25 @@
let
fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2
andalso Sign.typ_instance thy (ty1, ty2)
- andalso Sign.typ_instance thy (ty2, ty1)
+ andalso Sign.typ_instance thy (ty2, ty1);
+ 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);
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);
- val _ = case fold (remove eq_c) c_req c_given
- of [] => ()
- | cs => error ("superfluous definition(s) given for"
+ | 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;
+ fun after_qed cs =
+ fold Sign.add_const_constraint_i cs
+ #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
in
thy
|> fold_map get_remove_contraint (map fst c_req)
- ||> tap (fn thy => check_defs (get_c_given thy) c_req)
+ ||> tap (fn thy => check_defs (get_c_given thy) c_req thy)
||> add_defs (true, raw_defs)
- |-> (fn cs => fold Sign.add_const_constraint_i cs)
- |> AxClass.instance_arity_i arity
+ |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
end;
val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
@@ -430,22 +467,19 @@
val (classK, instanceK) = ("class", "class_instance")
-val locale_val =
- (P.locale_expr --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
- Scan.repeat1 P.context_element >> pair Locale.empty);
-
val classP =
OuterSyntax.command classK "operational type classes" K.thy_decl
- (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
+ (P.name --| P.$$$ "="
+ -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
+ -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
>> (Toplevel.theory_context
- o (fn f => swap o f) o (fn (bname, (expr, elems)) => add_class bname expr elems)));
+ o (fn f => swap o f) o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
val instanceP =
- OuterSyntax.command instanceK "" K.thy_goal
+ OuterSyntax.command instanceK "declare instance for operational type class" K.thy_goal
(P.xname -- (P.$$$ "::" |-- P.!!! P.arity)
-- Scan.repeat1 P.spec_name
- >> (Toplevel.theory_to_proof
+ >> (Toplevel.print oo Toplevel.theory_to_proof
o (fn ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs)));
val _ = OuterSyntax.add_parsers [classP, instanceP];