added explicit query function for arities to subalgebra projection
authorhaftmann
Thu Jan 25 09:32:46 2007 +0100 (2007-01-25)
changeset 2218139104d1c43ca
parent 22180 65e26e893818
child 22182 05ed4080cbd7
added explicit query function for arities to subalgebra projection
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Thu Jan 25 09:32:45 2007 +0100
     1.2 +++ b/src/Pure/sorts.ML	Thu Jan 25 09:32:46 2007 +0100
     1.3 @@ -44,7 +44,8 @@
     1.4    val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
     1.5    val empty_algebra: algebra
     1.6    val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
     1.7 -  val subalgebra: Pretty.pp -> (class -> bool) -> algebra -> (sort -> sort) * algebra
     1.8 +  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
     1.9 +    -> algebra -> (sort -> sort) * algebra
    1.10    type class_error
    1.11    val class_error: Pretty.pp -> class_error -> 'a
    1.12    exception CLASS_ERROR of class_error
    1.13 @@ -285,13 +286,16 @@
    1.14  
    1.15  (* subalgebra *)
    1.16  
    1.17 -fun subalgebra pp P (algebra as Algebra {classes, arities}) =
    1.18 +fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.19    let
    1.20      val restrict_sort = norm_sort algebra o filter P o Graph.all_succs classes;
    1.21 -    fun restrict_arity (c, (_, Ss)) =
    1.22 -      if P c then SOME (c, (c, map restrict_sort Ss)) else NONE;
    1.23 +    fun restrict_arity tyco (c, (_, Ss)) =
    1.24 +      if P c then
    1.25 +        SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
    1.26 +          |> map restrict_sort))
    1.27 +      else NONE;
    1.28      val classes' = classes |> Graph.subgraph P;
    1.29 -    val arities' = arities |> (Symtab.map o map_filter) restrict_arity;
    1.30 +    val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
    1.31    in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
    1.32  
    1.33