src/Pure/sorts.ML
changeset 20454 7e948db7e42d
parent 20391 d079804d3b82
child 20465 95f6d354b0ed
     1.1 --- a/src/Pure/sorts.ML	Fri Sep 01 08:36:51 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Fri Sep 01 08:36:53 2006 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4      arities: (class * (class * sort list)) list Symtab.table}
     1.5    val classes: algebra -> class list
     1.6    val super_classes: algebra -> class -> class list
     1.7 -  val all_super_classes: algebra -> class -> class list
     1.8    val class_less: algebra -> class * class -> bool
     1.9    val class_le: algebra -> class * class -> bool
    1.10    val sort_eq: algebra -> sort * sort -> bool
    1.11 @@ -44,7 +43,7 @@
    1.12    val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
    1.13    val empty_algebra: algebra
    1.14    val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
    1.15 -  val project_algebra: Pretty.pp -> (class -> bool) -> algebra -> algebra
    1.16 +  val project_algebra: Pretty.pp -> (class -> bool) -> algebra -> algebra * (sort -> sort)
    1.17    type class_error
    1.18    val class_error: Pretty.pp -> class_error -> 'a
    1.19    exception CLASS_ERROR of class_error
    1.20 @@ -58,7 +57,7 @@
    1.21    val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
    1.22  end;
    1.23  
    1.24 -structure Sorts: SORTS =
    1.25 +structure Sorts (*: SORTS *) =
    1.26  struct
    1.27  
    1.28  
    1.29 @@ -123,7 +122,6 @@
    1.30  
    1.31  val classes = Graph.keys o classes_of;
    1.32  val super_classes = Graph.imm_succs o classes_of;
    1.33 -fun all_super_classes algebra class = Graph.all_succs (classes_of algebra) [class];
    1.34  
    1.35  
    1.36  (* class relations *)
    1.37 @@ -283,13 +281,21 @@
    1.38  
    1.39  fun project_algebra pp proj (algebra as Algebra {classes, arities}) =
    1.40    let
    1.41 -    val proj_sort = norm_sort algebra o filter proj o Graph.all_succs classes;
    1.42 +    val classes' = classes |> Graph.project proj;
    1.43 +    val proj' = can (Graph.get_node classes');
    1.44 +    fun proj_classes class =
    1.45 +      if proj' class
    1.46 +      then [class]
    1.47 +      else (norm_sort algebra o maps proj_classes o super_classes algebra) class;
    1.48 +    val class_subst = fold (fn class => Symtab.update (class, proj_classes class))
    1.49 +      (Graph.keys classes) Symtab.empty;
    1.50      fun proj_arity (c, (_, Ss)) =
    1.51 -      if proj c then SOME (c, (c, map proj_sort Ss)) else NONE;
    1.52 -    val classes' = classes |> Graph.project proj;
    1.53 +      if proj' c then SOME (c,
    1.54 +        (c, map (norm_sort algebra o filter proj' o Graph.all_succs classes) Ss)) else NONE;
    1.55      val arities' = arities |> (Symtab.map o map_filter) proj_arity;
    1.56 -  in rebuild_arities pp (make_algebra (classes', arities')) end;
    1.57 -
    1.58 +    val algebra' = rebuild_arities pp (make_algebra (classes', arities'));
    1.59 +    val proj_sort = norm_sort algebra' o maps (the o Symtab.lookup class_subst);
    1.60 +  in (rebuild_arities pp (make_algebra (classes', arities')), proj_sort) end;
    1.61  
    1.62  
    1.63  (** sorts of types **)