# HG changeset patch # User wenzelm # Date 1269555522 -3600 # Node ID 71620f11dbbbb1b4ed447518f8174d99ac88a3fd # Parent 142c3784a42b26674292417f404e9972b24d0c51# Parent 00e48e1d9afd867155e46ed17102e52442c0cd68 merged diff -r 142c3784a42b -r 71620f11dbbb src/Pure/axclass.ML --- 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; diff -r 142c3784a42b -r 71620f11dbbb src/Pure/sorts.ML --- 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 *) diff -r 142c3784a42b -r 71620f11dbbb src/Tools/Code/code_thingol.ML --- 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)) =