src/Pure/sorts.ML
changeset 30240 5b25fee0362c
parent 29269 5c25a2012975
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/sorts.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/Pure/sorts.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -46,9 +46,7 @@
     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 classrels_of: algebra -> (class * class list) list
     1.8 -  val instances_of: algebra -> (string * class) list
     1.9 -  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
    1.10 +  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
    1.11      -> algebra -> (sort -> sort) * algebra
    1.12    type class_error
    1.13    val class_error: Pretty.pp -> class_error -> string
    1.14 @@ -302,19 +300,14 @@
    1.15  
    1.16  (* algebra projections *)
    1.17  
    1.18 -fun classrels_of (Algebra {classes, ...}) =
    1.19 -  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
    1.20 -
    1.21 -fun instances_of (Algebra {arities, ...}) =
    1.22 -  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
    1.23 -
    1.24  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.25    let
    1.26      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    1.27      fun restrict_arity tyco (c, (_, Ss)) =
    1.28 -      if P c then
    1.29 -        SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
    1.30 +      if P c then case sargs (c, tyco)
    1.31 +       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
    1.32            |> map restrict_sort))
    1.33 +        | NONE => NONE
    1.34        else NONE;
    1.35      val classes' = classes |> Graph.subgraph P;
    1.36      val arities' = arities |> Symtab.map' (map_filter o restrict_arity);