exported weaken combinator
authorhaftmann
Tue Jul 08 18:13:11 2008 +0200 (2008-07-08)
changeset 2749880d0de398339
parent 27497 c683836fe908
child 27499 150558266831
exported weaken combinator
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Tue Jul 08 18:13:10 2008 +0200
     1.2 +++ b/src/Pure/sorts.ML	Tue Jul 08 18:13:11 2008 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
     1.5    val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
     1.6    val of_sort: algebra -> typ * sort -> bool
     1.7 +  
     1.8 +val weaken: 'b Graph.T -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a;
     1.9    val of_sort_derivation: Pretty.pp -> algebra ->
    1.10      {class_relation: 'a * class -> class -> 'a,
    1.11       type_constructor: string -> ('a * class) list list -> class -> 'a,
    1.12 @@ -368,18 +370,21 @@
    1.13    in ofS end;
    1.14  
    1.15  
    1.16 -(* of_sort_derivation *)
    1.17 +(* animating derivations *)
    1.18 +
    1.19 +fun weaken classes class_relation (x, c1) c2 =
    1.20 +  (case Graph.irreducible_paths classes (c1, c2) of
    1.21 +    [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    1.22 +    | cs :: _ => let
    1.23 +        fun weaken_path (x, c1 :: c2 :: cs) =
    1.24 +            weaken_path (class_relation (x, c1) c2, c2 :: cs)
    1.25 +          | weaken_path (x, _) = x;
    1.26 +      in weaken_path (x, cs) end);
    1.27  
    1.28  fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
    1.29    let
    1.30      val {classes, arities} = rep_algebra algebra;
    1.31 -    fun weaken_path (x, c1 :: c2 :: cs) =
    1.32 -          weaken_path (class_relation (x, c1) c2, c2 :: cs)
    1.33 -      | weaken_path (x, _) = x;
    1.34 -    fun weaken (x, c1) c2 =
    1.35 -      (case Graph.irreducible_paths classes (c1, c2) of
    1.36 -        [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    1.37 -      | cs :: _ => weaken_path (x, cs));
    1.38 +    val weaken = weaken classes class_relation;
    1.39  
    1.40      fun weakens S1 S2 = S2 |> map (fn c2 =>
    1.41        (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of