1.1 --- a/src/Pure/display.ML	Tue Jun 01 17:36:53 2010 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Jun 01 22:19:17 2010 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4  
     1.5      fun prt_cls c = Syntax.pretty_sort ctxt [c];
     1.6      fun prt_sort S = Syntax.pretty_sort ctxt S;
     1.7 -    fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     1.8 +    fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     1.9      fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
    1.10      val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
    1.11      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);

     2.1 --- a/src/Pure/sorts.ML	Tue Jun 01 17:36:53 2010 +0200
     2.2 +++ b/src/Pure/sorts.ML	Tue Jun 01 22:19:17 2010 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
     2.5    type algebra
     2.6    val classes_of: algebra -> serial Graph.T
     2.7 -  val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
     2.8 +  val arities_of: algebra -> (class * sort list) list Symtab.table
     2.9    val all_classes: algebra -> class list
    2.10    val super_classes: algebra -> class -> class list
    2.11    val class_less: algebra -> class * class -> bool
    2.12 @@ -105,15 +105,14 @@
    2.13  
    2.14    arities: table of association lists of all type arities; (t, ars)
    2.15      means that type constructor t has the arities ars; an element
    2.16 -    (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
    2.17 -    via c0 <= c.  "Coregularity" of the arities structure requires
    2.18 -    that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
    2.19 -    c1 <= c2 holds Ss1 <= Ss2.
    2.20 +    (c, Ss) of ars represents the arity t::(Ss)c.  "Coregularity" of
    2.21 +    the arities structure requires that for any two declarations
    2.22 +    t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
    2.23  *)
    2.24  
    2.25  datatype algebra = Algebra of
    2.26   {classes: serial Graph.T,
    2.27 -  arities: (class * (class * sort list)) list Symtab.table};
    2.28 +  arities: (class * sort list) list Symtab.table};
    2.29  
    2.30  fun classes_of (Algebra {classes, ...}) = classes;
    2.31  fun arities_of (Algebra {arities, ...}) = arities;
    2.32 @@ -225,9 +224,9 @@
    2.33      Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
    2.34      Pretty.string_of_arity pp (t, Ss', [c']));
    2.35  
    2.36 -fun coregular pp algebra t (c, (c0, Ss)) ars =
    2.37 +fun coregular pp algebra t (c, Ss) ars =
    2.38    let
    2.39 -    fun conflict (c', (_, Ss')) =
    2.40 +    fun conflict (c', Ss') =
    2.41        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
    2.42          SOME ((c, c'), (c', Ss'))
    2.43        else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
    2.44 @@ -236,19 +235,18 @@
    2.45    in
    2.46      (case get_first conflict ars of
    2.47        SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
    2.48 -    | NONE => (c, (c0, Ss)) :: ars)
    2.49 +    | NONE => (c, Ss) :: ars)
    2.50    end;
    2.51  
    2.52 -fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
    2.53 +fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
    2.54  
    2.55 -fun insert pp algebra t (c, (c0, Ss)) ars =
    2.56 +fun insert pp algebra t (c, Ss) ars =
    2.57    (case AList.lookup (op =) ars c of
    2.58 -    NONE => coregular pp algebra t (c, (c0, Ss)) ars
    2.59 -  | SOME (_, Ss') =>
    2.60 +    NONE => coregular pp algebra t (c, Ss) ars
    2.61 +  | SOME Ss' =>
    2.62        if sorts_le algebra (Ss, Ss') then ars
    2.63 -      else if sorts_le algebra (Ss', Ss) then
    2.64 -        coregular pp algebra t (c, (c0, Ss))
    2.65 -          (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
    2.66 +      else if sorts_le algebra (Ss', Ss)
    2.67 +      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    2.68        else err_conflict pp t NONE (c, Ss) (c, Ss'));
    2.69  
    2.70  in
    2.71 @@ -265,7 +263,7 @@
    2.72    algebra |> map_arities (insert_complete_ars pp algebra arg);
    2.73  
    2.74  fun add_arities_table pp algebra =
    2.75 -  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
    2.76 +  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
    2.77  
    2.78  end;
    2.79  
    2.80 @@ -310,16 +308,17 @@
    2.81    in make_algebra (classes', arities') end;
    2.82  
    2.83  
    2.84 -(* algebra projections *)
    2.85 +(* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
    2.86  
    2.87  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    2.88    let
    2.89      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    2.90 -    fun restrict_arity tyco (c, (_, Ss)) =
    2.91 -      if P c then case sargs (c, tyco)
    2.92 -       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
    2.93 -          |> map restrict_sort))
    2.94 -        | NONE => NONE
    2.95 +    fun restrict_arity t (c, Ss) =
    2.96 +      if P c then
    2.97 +        (case sargs (c, t) of
    2.98 +          SOME sorts =>
    2.99 +            SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
   2.100 +        | NONE => NONE)
   2.101        else NONE;
   2.102      val classes' = classes |> Graph.subgraph P;
   2.103      val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
   2.104 @@ -355,7 +354,7 @@
   2.105      fun dom c =
   2.106        (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
   2.107          NONE => raise CLASS_ERROR (No_Arity (a, c))
   2.108 -      | SOME (_, Ss) => Ss);
   2.109 +      | SOME Ss => Ss);
   2.110      fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
   2.111    in
   2.112      (case S of
   2.113 @@ -380,11 +379,8 @@
   2.114    in uncurry meet end;
   2.115  
   2.116  fun meet_sort_typ algebra (T, S) =
   2.117 -  let
   2.118 -    val tab = meet_sort algebra (T, S) Vartab.empty;
   2.119 -  in Term.map_type_tvar (fn (v, _) =>
   2.120 -    TVar (v, (the o Vartab.lookup tab) v))
   2.121 -  end;
   2.122 +  let val tab = meet_sort algebra (T, S) Vartab.empty;
   2.123 +  in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
   2.124  
   2.125  
   2.126  (* of_sort *)
   2.127 @@ -425,9 +421,9 @@
   2.128            in
   2.129              S |> map (fn c =>
   2.130                let
   2.131 -                val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
   2.132 +                val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
   2.133                  val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
   2.134 -              in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
   2.135 +              in type_constructor (a, Us) dom' c end)
   2.136            end
   2.137        | derive (T, S) = weaken T (type_variable T) S;
   2.138    in derive end;