canonical meet_sort operation
authorhaftmann
Wed Apr 02 15:58:40 2008 +0200 (2008-04-02)
changeset 26517ef036a63f6e9
parent 26516 1bf210ac0a90
child 26518 3db6a46d8460
canonical meet_sort operation
src/Pure/sorts.ML
src/Pure/type.ML
src/Tools/code/code_funcgr.ML
     1.1 --- a/src/Pure/sorts.ML	Wed Apr 02 15:58:38 2008 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Apr 02 15:58:40 2008 +0200
     1.3 @@ -50,10 +50,10 @@
     1.4    type class_error
     1.5    val msg_class_error: Pretty.pp -> class_error -> string
     1.6    val class_error: Pretty.pp -> class_error -> 'a
     1.7 -  val NoSubsort: sort * sort -> class_error
     1.8    exception CLASS_ERROR of class_error
     1.9    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.10    val of_sort: algebra -> typ * sort -> bool
    1.11 +  val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
    1.12    val of_sort_derivation: Pretty.pp -> algebra ->
    1.13      {class_relation: 'a * class -> class -> 'a,
    1.14       type_constructor: string -> ('a * class) list list -> class -> 'a,
    1.15 @@ -355,6 +355,20 @@
    1.16    in ofS end;
    1.17  
    1.18  
    1.19 +(* meet_sort *)
    1.20 +
    1.21 +fun meet_sort algebra =
    1.22 +  let
    1.23 +    fun meet _ [] = I
    1.24 +      | meet (TFree (_, S)) S' = if sort_le algebra (S, S') then I
    1.25 +          else raise CLASS_ERROR (NoSubsort (S, S'))
    1.26 +      | meet (TVar (v, S)) S' = if sort_le algebra (S, S') then I
    1.27 +          else Vartab.map_default (v, S) (curry (inter_sort algebra) S')
    1.28 +      | meet (Type (a, Ts)) S =
    1.29 +          fold2 meet Ts (mg_domain algebra a S)
    1.30 +  in uncurry meet end;
    1.31 +
    1.32 +
    1.33  (* of_sort_derivation *)
    1.34  
    1.35  fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
     2.1 --- a/src/Pure/type.ML	Wed Apr 02 15:58:38 2008 +0200
     2.2 +++ b/src/Pure/type.ML	Wed Apr 02 15:58:40 2008 +0200
     2.3 @@ -59,8 +59,6 @@
     2.4    val lookup: tyenv -> indexname * sort -> typ option
     2.5    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     2.6    val typ_instance: tsig -> typ * typ -> bool
     2.7 -  val typ_of_sort: Sorts.algebra -> typ -> sort
     2.8 -    -> sort Vartab.table -> sort Vartab.table
     2.9    val raw_match: typ * typ -> tyenv -> tyenv
    2.10    val raw_matches: typ list * typ list -> tyenv -> tyenv
    2.11    val raw_instance: typ * typ -> bool
    2.12 @@ -349,18 +347,6 @@
    2.13  
    2.14  exception TYPE_MATCH;
    2.15  
    2.16 -fun typ_of_sort algebra =
    2.17 -  let
    2.18 -    val inters = Sorts.inter_sort algebra;
    2.19 -    fun of_sort _ [] = I
    2.20 -      | of_sort (TVar (v, S)) S' = Vartab.map_default (v, [])
    2.21 -          (fn S'' => inters (S, inters (S', S'')))
    2.22 -      | of_sort (TFree (_, S)) S' = if Sorts.sort_le algebra (S, S') then I
    2.23 -          else raise Sorts.CLASS_ERROR (Sorts.NoSubsort (S, S'))
    2.24 -      | of_sort (Type (a, Ts)) S =
    2.25 -          fold2 of_sort Ts (Sorts.mg_domain algebra a S)
    2.26 -  in of_sort end;
    2.27 -
    2.28  fun typ_match tsig =
    2.29    let
    2.30      fun match (TVar (v, S), T) subs =
     3.1 --- a/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:38 2008 +0200
     3.2 +++ b/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:40 2008 +0200
     3.3 @@ -76,7 +76,7 @@
     3.4        Sorts.of_sort_derivation (Sign.pp thy) algebra
     3.5          { class_relation = class_relation, type_constructor = type_constructor,
     3.6            type_variable = type_variable }
     3.7 -        (ty, sort)
     3.8 +        (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
     3.9    in
    3.10      flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
    3.11    end;
    3.12 @@ -110,20 +110,18 @@
    3.13          val thy = Thm.theory_of_thm thm;
    3.14          val pp = Sign.pp thy;
    3.15          val cs = fold_consts (insert (op =)) thms [];
    3.16 -        fun class_error (c, ty_decl) e =
    3.17 -          error ;
    3.18          fun match_const c (ty, ty_decl) =
    3.19            let
    3.20              val tys = Sign.const_typargs thy (c, ty);
    3.21              val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
    3.22 -          in fn tab => fold2 (Type.typ_of_sort algebra) tys sorts tab 
    3.23 +          in fn tab => fold2 (curry (Sorts.meet_sort algebra)) tys sorts tab
    3.24              handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.msg_class_error pp e ^ ",\n"
    3.25                ^ "for constant " ^ CodeUnit.string_of_const thy c
    3.26                ^ "\nin defining equations(s)\n"
    3.27                ^ (cat_lines o map string_of_thm) thms)
    3.28 +            (*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*)
    3.29            end;
    3.30 -        fun match (c, ty) =
    3.31 -          case tap_typ c
    3.32 +        fun match (c, ty) = case tap_typ c
    3.33             of SOME ty_decl => match_const c (ty, ty_decl)
    3.34              | NONE => I;
    3.35          val tvars = fold match cs Vartab.empty;
    3.36 @@ -161,7 +159,7 @@
    3.37      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
    3.38      fun all_classparams tyco class =
    3.39        these (try (#params o AxClass.get_info thy) class)
    3.40 -      |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
    3.41 +      |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
    3.42    in
    3.43      Symtab.empty
    3.44      |> fold (fn (tyco, class) =>
    3.45 @@ -173,7 +171,7 @@
    3.46  fun instances_of_consts thy algebra funcgr consts =
    3.47    let
    3.48      fun inst (cexpr as (c, ty)) = insts_of thy algebra c
    3.49 -      ((fst o Graph.get_node funcgr) c) ty handle Sorts.CLASS_ERROR _ => [];
    3.50 +      ((fst o Graph.get_node funcgr) c) ty;
    3.51    in
    3.52      []
    3.53      |> fold (fold (insert (op =)) o inst) consts