more direct Sorts.has_instance;
authorwenzelm
Mon Jul 16 21:20:56 2012 +0200 (2012-07-16)
changeset 48272db75b4005d9a
parent 48271 b28defd0b5a5
child 48273 65233084e9d7
more direct Sorts.has_instance;
tuned Sorts.mg_domain;
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/record.ML
src/HOL/Typerep.thy
src/Pure/sorts.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jul 16 15:57:21 2012 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jul 16 21:20:56 2012 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4      val certs = map (mk_case_cert thy) tycos;
     1.5      val tycos_eq =
     1.6        filter_out
     1.7 -        (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
     1.8 +        (fn tyco => Sorts.has_instance (Sign.classes_of thy) tyco [HOLogic.class_equal]) tycos;
     1.9    in
    1.10      if null css then thy
    1.11      else
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 15:57:21 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 21:20:56 2012 +0200
     2.3 @@ -60,8 +60,8 @@
     2.4  
     2.5  fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
     2.6    let
     2.7 -    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of})
     2.8 -      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
     2.9 +    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of})
    2.10 +      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
    2.11    in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
    2.12  
    2.13  
    2.14 @@ -111,7 +111,7 @@
    2.15  
    2.16  fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
    2.17    let
    2.18 -    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of};
    2.19 +    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of};
    2.20    in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
    2.21  
    2.22  
     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 16 15:57:21 2012 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 16 21:20:56 2012 +0200
     3.3 @@ -449,7 +449,7 @@
     3.4        (Datatype_Aux.interpret_construction descr vs constr)
     3.5      val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
     3.6        @ insts_of aux_sort { atyp = K [], dtyp = K o K }
     3.7 -    val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
     3.8 +    val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
     3.9    in if has_inst then thy
    3.10      else case perhaps_constrain thy insts vs
    3.11       of SOME constrain => instantiate config descr
     4.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 16 15:57:21 2012 +0200
     4.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Jul 16 21:20:56 2012 +0200
     4.3 @@ -47,8 +47,8 @@
     4.4  
     4.5  fun ensure_term_of (tyco, (raw_vs, _)) thy =
     4.6    let
     4.7 -    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
     4.8 -      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
     4.9 +    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
    4.10 +      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
    4.11    in if need_inst then add_term_of tyco raw_vs thy else thy end;
    4.12  
    4.13  
    4.14 @@ -88,7 +88,7 @@
    4.15  
    4.16  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    4.17    let
    4.18 -    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    4.19 +    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of};
    4.20    in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    4.21  
    4.22  
    4.23 @@ -125,7 +125,7 @@
    4.24  
    4.25  fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
    4.26    let
    4.27 -    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    4.28 +    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of};
    4.29    in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
    4.30  
    4.31  
     5.1 --- a/src/HOL/Tools/record.ML	Mon Jul 16 15:57:21 2012 +0200
     5.2 +++ b/src/HOL/Tools/record.ML	Mon Jul 16 21:20:56 2012 +0200
     5.3 @@ -1722,7 +1722,7 @@
     5.4  fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
     5.5    let
     5.6      val algebra = Sign.classes_of thy;
     5.7 -    val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
     5.8 +    val has_inst = Sorts.has_instance algebra ext_tyco sort;
     5.9    in
    5.10      if has_inst then thy
    5.11      else
     6.1 --- a/src/HOL/Typerep.thy	Mon Jul 16 15:57:21 2012 +0200
     6.2 +++ b/src/HOL/Typerep.thy	Mon Jul 16 21:20:56 2012 +0200
     6.3 @@ -64,8 +64,8 @@
     6.4    end;
     6.5  
     6.6  fun ensure_typerep tyco thy =
     6.7 -  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
     6.8 -    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
     6.9 +  if not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep})
    6.10 +    andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort type}
    6.11    then add_typerep tyco thy else thy;
    6.12  
    6.13  in
     7.1 --- a/src/Pure/sorts.ML	Mon Jul 16 15:57:21 2012 +0200
     7.2 +++ b/src/Pure/sorts.ML	Mon Jul 16 21:20:56 2012 +0200
     7.3 @@ -48,6 +48,7 @@
     7.4    type class_error
     7.5    val class_error: Context.pretty -> class_error -> string
     7.6    exception CLASS_ERROR of class_error
     7.7 +  val has_instance: algebra -> string -> sort -> bool
     7.8    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
     7.9    val meet_sort: algebra -> typ * sort
    7.10      -> sort Vartab.table -> sort Vartab.table   (*exception CLASS_ERROR*)
    7.11 @@ -337,13 +338,16 @@
    7.12  exception CLASS_ERROR of class_error;
    7.13  
    7.14  
    7.15 -(* mg_domain *)
    7.16 +(* instances *)
    7.17 +
    7.18 +fun has_instance algebra a =
    7.19 +  forall (AList.defined (op =) (Symtab.lookup_list (arities_of algebra) a));
    7.20  
    7.21  fun mg_domain algebra a S =
    7.22    let
    7.23 -    val arities = arities_of algebra;
    7.24 +    val ars = Symtab.lookup_list (arities_of algebra) a;
    7.25      fun dom c =
    7.26 -      (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
    7.27 +      (case AList.lookup (op =) ars c of
    7.28          NONE => raise CLASS_ERROR (No_Arity (a, c))
    7.29        | SOME Ss => Ss);
    7.30      fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);