Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
authorwenzelm
Thu Mar 25 21:27:04 2010 +0100 (2010-03-25 ago)
changeset 3596100e48e1d9afd
parent 35960 536c07a2a0bc
child 35973 71620f11dbbb
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
officially export weaken as Sorts.classrel_derivation;
tuned comments;
src/Pure/axclass.ML
src/Pure/sorts.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/axclass.ML	Thu Mar 25 21:14:15 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 25 21:27:04 2010 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4        Sign.super_classes thy c
     1.5        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
     1.6            andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
     1.7 -    val completions = map (fn c1 => (Sorts.weaken algebra
     1.8 +    val completions = map (fn c1 => (Sorts.classrel_derivation algebra
     1.9        (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
    1.10          |> Thm.close_derivation, c1)) super_class_completions;
    1.11      val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
     2.1 --- a/src/Pure/sorts.ML	Thu Mar 25 21:14:15 2010 +0100
     2.2 +++ b/src/Pure/sorts.ML	Thu Mar 25 21:27:04 2010 +0100
     2.3 @@ -56,12 +56,13 @@
     2.4      -> sort Vartab.table -> sort Vartab.table   (*exception CLASS_ERROR*)
     2.5    val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
     2.6    val of_sort: algebra -> typ * sort -> bool
     2.7 -  val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
     2.8    val of_sort_derivation: algebra ->
     2.9      {class_relation: 'a * class -> class -> 'a,
    2.10       type_constructor: string -> ('a * class) list list -> class -> 'a,
    2.11       type_variable: typ -> ('a * class) list} ->
    2.12      typ * sort -> 'a list   (*exception CLASS_ERROR*)
    2.13 +  val classrel_derivation: algebra ->
    2.14 +    ('a * class -> class -> 'a) -> 'a * class -> class -> 'a  (*exception CLASS_ERROR*)
    2.15    val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
    2.16  end;
    2.17  
    2.18 @@ -317,7 +318,7 @@
    2.19  
    2.20  (** sorts of types **)
    2.21  
    2.22 -(* errors -- delayed message composition *)
    2.23 +(* errors -- performance tuning via delayed message composition *)
    2.24  
    2.25  datatype class_error =
    2.26    NoClassrel of class * class |
    2.27 @@ -391,24 +392,13 @@
    2.28  
    2.29  (* animating derivations *)
    2.30  
    2.31 -fun weaken algebra class_relation =
    2.32 -  let
    2.33 -    fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
    2.34 -      | path (x, _) = x;
    2.35 -  in fn (x, c1) => fn c2 =>
    2.36 -    (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
    2.37 -      [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    2.38 -    | cs :: _ => path (x, cs))
    2.39 -  end;
    2.40 -
    2.41  fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
    2.42    let
    2.43 -    val weaken = weaken algebra class_relation;
    2.44      val arities = arities_of algebra;
    2.45  
    2.46 -    fun weakens S1 S2 = S2 |> map (fn c2 =>
    2.47 +    fun weaken S1 S2 = S2 |> map (fn c2 =>
    2.48        (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
    2.49 -        SOME d1 => weaken d1 c2
    2.50 +        SOME d1 => class_relation d1 c2
    2.51        | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
    2.52  
    2.53      fun derive _ [] = []
    2.54 @@ -420,12 +410,23 @@
    2.55              S |> map (fn c =>
    2.56                let
    2.57                  val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
    2.58 -                val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
    2.59 -              in weaken (type_constructor a dom' c0, c0) c end)
    2.60 +                val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
    2.61 +              in class_relation (type_constructor a dom' c0, c0) c end)
    2.62            end
    2.63 -      | derive T S = weakens (type_variable T) S;
    2.64 +      | derive T S = weaken (type_variable T) S;
    2.65    in uncurry derive end;
    2.66  
    2.67 +fun classrel_derivation algebra class_relation =
    2.68 +  let
    2.69 +    fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
    2.70 +      | path (x, _) = x;
    2.71 +  in
    2.72 +    fn (x, c1) => fn c2 =>
    2.73 +      (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
    2.74 +        [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    2.75 +      | cs :: _ => path (x, cs))
    2.76 +  end;
    2.77 +
    2.78  
    2.79  (* witness_sorts *)
    2.80  
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu Mar 25 21:14:15 2010 +0100
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Mar 25 21:27:04 2010 +0100
     3.3 @@ -774,7 +774,8 @@
     3.4          val sort' = proj_sort sort;
     3.5        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
     3.6      val typargs = Sorts.of_sort_derivation algebra
     3.7 -      {class_relation = class_relation, type_constructor = type_constructor,
     3.8 +      {class_relation = Sorts.classrel_derivation algebra class_relation,
     3.9 +       type_constructor = type_constructor,
    3.10         type_variable = type_variable} (ty, proj_sort sort)
    3.11        handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
    3.12      fun mk_dict (Global (inst, yss)) =