src/Pure/sorts.ML
changeset 37248 8e8e5f9d1441
parent 36429 9d6b3be996d4
child 39020 ac0f24f850c9
     1.1 --- a/src/Pure/sorts.ML	Tue Jun 01 17:36:53 2010 +0200
     1.2 +++ b/src/Pure/sorts.ML	Tue Jun 01 22:19:17 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
     1.5    type algebra
     1.6    val classes_of: algebra -> serial Graph.T
     1.7 -  val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
     1.8 +  val arities_of: algebra -> (class * sort list) list Symtab.table
     1.9    val all_classes: algebra -> class list
    1.10    val super_classes: algebra -> class -> class list
    1.11    val class_less: algebra -> class * class -> bool
    1.12 @@ -105,15 +105,14 @@
    1.13  
    1.14    arities: table of association lists of all type arities; (t, ars)
    1.15      means that type constructor t has the arities ars; an element
    1.16 -    (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
    1.17 -    via c0 <= c.  "Coregularity" of the arities structure requires
    1.18 -    that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
    1.19 -    c1 <= c2 holds Ss1 <= Ss2.
    1.20 +    (c, Ss) of ars represents the arity t::(Ss)c.  "Coregularity" of
    1.21 +    the arities structure requires that for any two declarations
    1.22 +    t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
    1.23  *)
    1.24  
    1.25  datatype algebra = Algebra of
    1.26   {classes: serial Graph.T,
    1.27 -  arities: (class * (class * sort list)) list Symtab.table};
    1.28 +  arities: (class * sort list) list Symtab.table};
    1.29  
    1.30  fun classes_of (Algebra {classes, ...}) = classes;
    1.31  fun arities_of (Algebra {arities, ...}) = arities;
    1.32 @@ -225,9 +224,9 @@
    1.33      Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
    1.34      Pretty.string_of_arity pp (t, Ss', [c']));
    1.35  
    1.36 -fun coregular pp algebra t (c, (c0, Ss)) ars =
    1.37 +fun coregular pp algebra t (c, Ss) ars =
    1.38    let
    1.39 -    fun conflict (c', (_, Ss')) =
    1.40 +    fun conflict (c', Ss') =
    1.41        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
    1.42          SOME ((c, c'), (c', Ss'))
    1.43        else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
    1.44 @@ -236,19 +235,18 @@
    1.45    in
    1.46      (case get_first conflict ars of
    1.47        SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
    1.48 -    | NONE => (c, (c0, Ss)) :: ars)
    1.49 +    | NONE => (c, Ss) :: ars)
    1.50    end;
    1.51  
    1.52 -fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
    1.53 +fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
    1.54  
    1.55 -fun insert pp algebra t (c, (c0, Ss)) ars =
    1.56 +fun insert pp algebra t (c, Ss) ars =
    1.57    (case AList.lookup (op =) ars c of
    1.58 -    NONE => coregular pp algebra t (c, (c0, Ss)) ars
    1.59 -  | SOME (_, Ss') =>
    1.60 +    NONE => coregular pp algebra t (c, Ss) ars
    1.61 +  | SOME Ss' =>
    1.62        if sorts_le algebra (Ss, Ss') then ars
    1.63 -      else if sorts_le algebra (Ss', Ss) then
    1.64 -        coregular pp algebra t (c, (c0, Ss))
    1.65 -          (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
    1.66 +      else if sorts_le algebra (Ss', Ss)
    1.67 +      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
    1.68        else err_conflict pp t NONE (c, Ss) (c, Ss'));
    1.69  
    1.70  in
    1.71 @@ -265,7 +263,7 @@
    1.72    algebra |> map_arities (insert_complete_ars pp algebra arg);
    1.73  
    1.74  fun add_arities_table pp algebra =
    1.75 -  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
    1.76 +  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
    1.77  
    1.78  end;
    1.79  
    1.80 @@ -310,16 +308,17 @@
    1.81    in make_algebra (classes', arities') end;
    1.82  
    1.83  
    1.84 -(* algebra projections *)
    1.85 +(* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
    1.86  
    1.87  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.88    let
    1.89      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    1.90 -    fun restrict_arity tyco (c, (_, Ss)) =
    1.91 -      if P c then case sargs (c, tyco)
    1.92 -       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
    1.93 -          |> map restrict_sort))
    1.94 -        | NONE => NONE
    1.95 +    fun restrict_arity t (c, Ss) =
    1.96 +      if P c then
    1.97 +        (case sargs (c, t) of
    1.98 +          SOME sorts =>
    1.99 +            SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
   1.100 +        | NONE => NONE)
   1.101        else NONE;
   1.102      val classes' = classes |> Graph.subgraph P;
   1.103      val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
   1.104 @@ -355,7 +354,7 @@
   1.105      fun dom c =
   1.106        (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
   1.107          NONE => raise CLASS_ERROR (No_Arity (a, c))
   1.108 -      | SOME (_, Ss) => Ss);
   1.109 +      | SOME Ss => Ss);
   1.110      fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
   1.111    in
   1.112      (case S of
   1.113 @@ -380,11 +379,8 @@
   1.114    in uncurry meet end;
   1.115  
   1.116  fun meet_sort_typ algebra (T, S) =
   1.117 -  let
   1.118 -    val tab = meet_sort algebra (T, S) Vartab.empty;
   1.119 -  in Term.map_type_tvar (fn (v, _) =>
   1.120 -    TVar (v, (the o Vartab.lookup tab) v))
   1.121 -  end;
   1.122 +  let val tab = meet_sort algebra (T, S) Vartab.empty;
   1.123 +  in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
   1.124  
   1.125  
   1.126  (* of_sort *)
   1.127 @@ -425,9 +421,9 @@
   1.128            in
   1.129              S |> map (fn c =>
   1.130                let
   1.131 -                val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
   1.132 +                val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
   1.133                  val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
   1.134 -              in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
   1.135 +              in type_constructor (a, Us) dom' c end)
   1.136            end
   1.137        | derive (T, S) = weaken T (type_variable T) S;
   1.138    in derive end;