--- a/src/Pure/Tools/class_package.ML Fri Sep 01 08:36:53 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Fri Sep 01 08:36:54 2006 +0200
@@ -29,9 +29,7 @@
val certify_sort: theory -> sort -> sort
val read_class: theory -> xstring -> class
val read_sort: theory -> string -> sort
- val operational_sort_of: theory -> sort -> sort
- val operational_algebra: theory -> Sorts.algebra
- val the_superclasses: theory -> class -> class list
+ val operational_algebra: theory -> Sorts.algebra * (sort -> sort)
val the_consts_sign: theory -> class -> string * (string * typ) list
val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
@@ -41,19 +39,13 @@
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
val default_intro_classes_tac: thm list -> tactic
-
- type sortcontext = (string * sort) list
- datatype classlookup = Instance of (class * string) * classlookup list list
- | Lookup of class list * (string * (int * int))
- val sortcontext_of_typ: theory -> typ -> sortcontext
- val sortlookup: theory -> typ * sort -> classlookup list
end;
structure ClassPackage : CLASS_PACKAGE =
struct
-(* theory data *)
+(** theory data **)
datatype class_data = ClassData of {
name_locale: string,
@@ -104,75 +96,34 @@
fun the_class_data thy class =
case lookup_class_data thy class
- of NONE => error ("undeclared operational class " ^ quote class)
+ of NONE => error ("undeclared constructive class " ^ quote class)
| SOME data => data;
-val is_class = is_some oo lookup_class_data;
-
fun is_operational_class thy cls =
lookup_class_data thy cls
|> Option.map (not o null o #consts o fst)
|> the_default false;
-fun operational_algebra thy =
- Sorts.project_algebra (Sign.pp thy)
- (is_operational_class thy) (Sign.classes_of thy);
-
-fun operational_sort_of thy =
+fun the_ancestry thy classes =
let
- fun get_sort class =
+ fun proj_class class =
if is_operational_class thy class
then [class]
- else operational_sort_of thy (Sign.super_classes thy class);
- in Sign.certify_sort thy o maps get_sort end;
-
-fun the_superclasses thy class =
- if is_class thy class
- then
- Sign.super_classes thy class
- |> operational_sort_of thy
- else
- error ("no operational class: " ^ class);
-
-fun the_ancestry thy classes =
- let
+ else (Sign.certify_sort thy o maps proj_class o Sign.super_classes thy) class;
fun ancestry class anc =
anc
|> insert (op =) class
- |> fold ancestry (the_superclasses thy class);
+ |> fold ancestry ((maps proj_class o Sign.super_classes thy) class);
in fold ancestry classes [] end;
+val the_parm_map = #consts o fst oo the_class_data;
+
+val the_propnames = #propnames o fst oo the_class_data;
+
fun subst_clsvar v ty_subst =
map_type_tfree (fn u as (w, _) =>
if w = v then ty_subst else TFree u);
-val the_parm_map = #consts o fst oo the_class_data;
-
-fun the_consts_sign thy class =
- let
- val data = (fst o the_class_data thy) class
- in (#var data, (map snd o #consts) data) end;
-
-fun the_inst_sign thy (class, tyco) =
- let
- val _ = if is_operational_class thy class then () else error ("no operational class: " ^ class);
- val asorts = Sign.arity_sorts thy tyco [class];
- val (clsvar, const_sign) = the_consts_sign thy class;
- fun add_var sort used =
- let val v = hd (Name.invents used "'a" 1);
- in ((v, sort), Name.declare v used) end;
- val (vsorts, _) =
- Name.context
- |> Name.declare clsvar
- |> fold (fn (_, ty) => fold Name.declare
- ((map (fst o fst) o typ_tvars) ty @ map fst (Term.add_tfreesT ty []))) const_sign
- |> fold_map add_var asorts;
- val ty_inst = Type (tyco, map TFree vsorts);
- val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
- in (vsorts, inst_signs) end;
-
-val the_propnames = #propnames o fst oo the_class_data;
-
(* updaters *)
@@ -208,7 +159,8 @@
certify_sort thy o Sign.read_sort thy;
-(* contexts with arity assumptions *)
+
+(** contexts with arity assumptions **)
fun assume_arities_of_sort thy arities ty_sort =
let
@@ -224,7 +176,9 @@
=> Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy
in f thy_read end;
-(* tactics and methods *)
+
+
+(** tactics and methods **)
fun intro_classes_tac facts st =
(ALLGOALS (Method.insert_tac facts THEN'
@@ -245,7 +199,8 @@
"apply some intro/elim rule")]);
-(* axclass instances *)
+
+(** axclass instances **)
local
@@ -272,7 +227,8 @@
end;
-(* classes and instances *)
+
+(** classes and instances **)
local
@@ -388,7 +344,7 @@
val class = gen_class (Locale.add_locale false) read_class;
val class_i = gen_class (Locale.add_locale_i false) certify_class;
-end; (* local *)
+end; (*local*)
local
@@ -517,7 +473,7 @@
val instance_arity_i = instance_arity_i' (K axclass_instance_arity_i);
val prove_instance_arity = instance_arity_i' o tactic_proof;
-end; (* local *)
+end; (*local*)
local
@@ -572,51 +528,40 @@
end; (* local *)
-(* extracting dictionary obligations from types *)
-type sortcontext = (string * sort) list;
+(** code generation view **)
-fun sortcontext_of_typ thy ty = (rev ooo fold_atyps)
- (fn TFree (v, S) =>
- (case operational_sort_of thy S of
- [] => I
- | S' => insert (op =) (v, S'))) (Type.no_tvars ty) [];
+fun operational_algebra thy =
+ Sorts.project_algebra (Sign.pp thy)
+ (is_operational_class thy) (Sign.classes_of thy);
-datatype classlookup = Instance of (class * string) * classlookup list list
- | Lookup of class list * (string * (int * int));
+fun the_consts_sign thy class =
+ let
+ val _ = if is_operational_class thy class then () else error ("no operational class: " ^ quote class);
+ val data = (fst o the_class_data thy) class
+ in (#var data, (map snd o #consts) data) end;
-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, 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 sortlookup thy (typ_ctxt, sort_decl) =
+fun the_inst_sign thy (class, tyco) =
let
- val pp = Sign.pp thy;
- val algebra = Sorts.project_algebra pp (is_operational_class thy)
- (Sign.classes_of thy);
- fun classrel (l as Lookup (classes, p), _) class =
- Lookup (class :: classes, p)
- | classrel (Instance ((_, tyco), lss), _) class =
- Instance ((class, tyco), lss);
- fun constructor tyco lss class =
- Instance ((class, tyco), (map o map) fst lss);
- fun variable (TFree (v, sort)) =
- let val op_sort = operational_sort_of thy sort
- in map_index (fn (n, class) => (Lookup ([], (v, (n, length op_sort))), class)) op_sort end;
- in
- Sorts.of_sort_derivation pp algebra
- {classrel = classrel, constructor = constructor, variable = variable}
- (Type.no_tvars typ_ctxt, operational_sort_of thy sort_decl)
- end;
+ val _ = if is_operational_class thy class then () else error ("no operational class: " ^ quote class);
+ val asorts = Sign.arity_sorts thy tyco [class];
+ val (clsvar, const_sign) = the_consts_sign thy class;
+ fun add_var sort used =
+ let val v = hd (Name.invents used "'a" 1);
+ in ((v, sort), Name.declare v used) end;
+ val (vsorts, _) =
+ Name.context
+ |> Name.declare clsvar
+ |> fold (fn (_, ty) => fold Name.declare
+ ((map (fst o fst) o typ_tvars) ty @ map fst (Term.add_tfreesT ty []))) const_sign
+ |> fold_map add_var asorts;
+ val ty_inst = Type (tyco, map TFree vsorts);
+ val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
+ in (vsorts, inst_signs) end;
-(* toplevel interface *)
+
+(** toplevel interface **)
local
@@ -665,6 +610,6 @@
val _ = OuterSyntax.add_parsers [classP, instanceP, print_classesP];
-end; (* local *)
+end; (*local*)
-end; (* struct *)
+end;