--- a/src/Pure/axclass.ML Thu Mar 25 17:56:31 2010 +0100
+++ b/src/Pure/axclass.ML Thu Mar 25 23:18:42 2010 +0100
@@ -37,9 +37,6 @@
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val thynames_of_arity: theory -> class * string -> string list
- type cache
- val of_sort: theory -> typ * sort -> cache -> thm list * cache (*exception Sorts.CLASS_ERROR*)
- val cache: cache
val introN: string
val axiomsN: string
end;
@@ -190,7 +187,7 @@
Sign.super_classes thy c
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
- val completions = map (fn c1 => (Sorts.weaken algebra
+ val completions = map (fn c1 => (Sorts.classrel_derivation algebra
(fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
|> Thm.close_derivation, c1)) super_class_completions;
val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
@@ -564,59 +561,4 @@
end;
-
-
-(** explicit derivations -- cached **)
-
-datatype cache = Types of (class * thm) list Typtab.table;
-
-local
-
-fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache;
-fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache);
-
-fun derive_type _ (_, []) = []
- | derive_type thy (typ, sort) =
- let
- val certT = Thm.ctyp_of thy;
- val vars = Term.fold_atyps
- (fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
- | T as TVar (_, S) => insert (eq_fst op =) (T, S)
- | _ => I) typ [];
- val hyps = vars
- |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
- val ths = (typ, sort)
- |> Sorts.of_sort_derivation (Sign.classes_of thy)
- {class_relation =
- fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
- type_constructor =
- fn a => fn dom => fn c =>
- let val Ss = map (map snd) dom and ths = maps (map fst) dom
- in ths MRS the_arity thy a (c, Ss) end,
- type_variable =
- the_default [] o AList.lookup (op =) hyps};
- in ths end;
-
-in
-
-fun of_sort thy (typ, sort) cache =
- let
- val sort' = filter (is_none o lookup_type cache typ) sort;
- val ths' = derive_type thy (typ, sort')
- handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
- Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
- val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
- val ths =
- sort |> map (fn c =>
- Goal.finish
- (Syntax.init_pretty_global thy)
- (the (lookup_type cache' typ c) RS
- Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
- |> Thm.adjust_maxidx_thm ~1);
- in (ths, cache') end;
-
end;
-
-val cache = Types Typtab.empty;
-
-end;
--- a/src/Pure/sorts.ML Thu Mar 25 17:56:31 2010 +0100
+++ b/src/Pure/sorts.ML Thu Mar 25 23:18:42 2010 +0100
@@ -56,12 +56,13 @@
-> sort Vartab.table -> sort Vartab.table (*exception CLASS_ERROR*)
val meet_sort_typ: algebra -> typ * sort -> typ -> typ (*exception CLASS_ERROR*)
val of_sort: algebra -> typ * sort -> bool
- val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
val of_sort_derivation: algebra ->
{class_relation: 'a * class -> class -> 'a,
type_constructor: string -> ('a * class) list list -> class -> 'a,
type_variable: typ -> ('a * class) list} ->
typ * sort -> 'a list (*exception CLASS_ERROR*)
+ val classrel_derivation: algebra ->
+ ('a * class -> class -> 'a) -> 'a * class -> class -> 'a (*exception CLASS_ERROR*)
val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
end;
@@ -317,7 +318,7 @@
(** sorts of types **)
-(* errors -- delayed message composition *)
+(* errors -- performance tuning via delayed message composition *)
datatype class_error =
NoClassrel of class * class |
@@ -391,24 +392,13 @@
(* animating derivations *)
-fun weaken algebra class_relation =
- let
- fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
- | path (x, _) = x;
- in fn (x, c1) => fn c2 =>
- (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
- [] => raise CLASS_ERROR (NoClassrel (c1, c2))
- | cs :: _ => path (x, cs))
- end;
-
fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
let
- val weaken = weaken algebra class_relation;
val arities = arities_of algebra;
- fun weakens S1 S2 = S2 |> map (fn c2 =>
+ fun weaken S1 S2 = S2 |> map (fn c2 =>
(case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
- SOME d1 => weaken d1 c2
+ SOME d1 => class_relation d1 c2
| NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
fun derive _ [] = []
@@ -420,12 +410,23 @@
S |> map (fn c =>
let
val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
- val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
- in weaken (type_constructor a dom' c0, c0) c end)
+ val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
+ in class_relation (type_constructor a dom' c0, c0) c end)
end
- | derive T S = weakens (type_variable T) S;
+ | derive T S = weaken (type_variable T) S;
in uncurry derive end;
+fun classrel_derivation algebra class_relation =
+ let
+ fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
+ | path (x, _) = x;
+ in
+ fn (x, c1) => fn c2 =>
+ (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
+ [] => raise CLASS_ERROR (NoClassrel (c1, c2))
+ | cs :: _ => path (x, cs))
+ end;
+
(* witness_sorts *)
--- a/src/Tools/Code/code_thingol.ML Thu Mar 25 17:56:31 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Thu Mar 25 23:18:42 2010 +0100
@@ -774,7 +774,8 @@
val sort' = proj_sort sort;
in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
val typargs = Sorts.of_sort_derivation algebra
- {class_relation = class_relation, type_constructor = type_constructor,
+ {class_relation = Sorts.classrel_derivation algebra class_relation,
+ type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
fun mk_dict (Global (inst, yss)) =