generic ad-hoc overloading via check/uncheck
authorkrauss
Tue Jul 13 00:15:37 2010 +0200 (2010-07-13)
changeset 3778993f6dcf9ec02
parent 37788 261c61fabc98
child 37790 7fea92005066
generic ad-hoc overloading via check/uncheck
src/HOL/IsaMakefile
src/HOL/Library/Adhoc_Overloading.thy
src/HOL/Library/Library.thy
src/HOL/Library/adhoc_overloading.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 13 11:38:04 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 13 00:15:37 2010 +0200
     1.3 @@ -397,7 +397,7 @@
     1.4  
     1.5  $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
     1.6    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
     1.7 -  Library/Abstract_Rat.thy Library/AssocList.thy			\
     1.8 +  Library/Abstract_Rat.thy Library/Adhoc_Overloading.thy Library/AssocList.thy	\
     1.9    Library/BigO.thy Library/Binomial.thy Library/Bit.thy			\
    1.10    Library/Boolean_Algebra.thy Library/Cardinality.thy			\
    1.11    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    1.12 @@ -434,8 +434,8 @@
    1.13    Library/Sum_Of_Squares/sum_of_squares.ML				\
    1.14    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    1.15    Library/While_Combinator.thy Library/Zorn.thy				\
    1.16 -  Library/positivstellensatz.ML Library/reflection.ML			\
    1.17 -  Library/reify_data.ML							\
    1.18 +  Library/adhoc_overloading.ML Library/positivstellensatz.ML		\
    1.19 +  Library/reflection.ML Library/reify_data.ML				\
    1.20    Library/document/root.bib Library/document/root.tex
    1.21  	@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
    1.22  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Adhoc_Overloading.thy	Tue Jul 13 00:15:37 2010 +0200
     2.3 @@ -0,0 +1,14 @@
     2.4 +(* Author: Alexander Krauss, TU Muenchen
     2.5 +   Author: Christian Sternagel, University of Innsbruck
     2.6 +*)
     2.7 +
     2.8 +header {* Ad-hoc overloading of constants based on their types *}
     2.9 +
    2.10 +theory Adhoc_Overloading
    2.11 +imports Main
    2.12 +uses "adhoc_overloading.ML"
    2.13 +begin
    2.14 +
    2.15 +setup Adhoc_Overloading.setup
    2.16 +
    2.17 +end
     3.1 --- a/src/HOL/Library/Library.thy	Tue Jul 13 11:38:04 2010 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Tue Jul 13 00:15:37 2010 +0200
     3.3 @@ -2,6 +2,7 @@
     3.4  theory Library
     3.5  imports
     3.6    Abstract_Rat
     3.7 +  Adhoc_Overloading
     3.8    AssocList
     3.9    BigO
    3.10    Binomial
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/adhoc_overloading.ML	Tue Jul 13 00:15:37 2010 +0200
     4.3 @@ -0,0 +1,140 @@
     4.4 +(* Author: Alexander Krauss, TU Muenchen
     4.5 +   Author: Christian Sternagel, University of Innsbruck
     4.6 +
     4.7 +Ad-hoc overloading of constants based on their types.
     4.8 +*)
     4.9 +
    4.10 +signature ADHOC_OVERLOADING =
    4.11 +sig
    4.12 +
    4.13 +  val add_overloaded: string -> theory -> theory
    4.14 +  val add_variant: string -> string -> theory -> theory
    4.15 +
    4.16 +  val show_variants: bool Unsynchronized.ref
    4.17 +  val setup: theory -> theory
    4.18 +
    4.19 +end
    4.20 +
    4.21 +
    4.22 +structure Adhoc_Overloading: ADHOC_OVERLOADING =
    4.23 +struct
    4.24 +
    4.25 +val show_variants = Unsynchronized.ref false;
    4.26 +
    4.27 +
    4.28 +(* errors *)
    4.29 +
    4.30 +fun duplicate_variant_err int_name ext_name =
    4.31 +  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
    4.32 +
    4.33 +fun not_overloaded_err name =
    4.34 +  error ("Constant " ^ quote name ^ " is not declared as overloaded");
    4.35 +
    4.36 +fun already_overloaded_err name =
    4.37 +  error ("Constant " ^ quote name ^ " is already declared as overloaded");
    4.38 +
    4.39 +fun unresolved_err ctxt (c, T) t reason =
    4.40 +  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
    4.41 +    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
    4.42 +    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
    4.43 +
    4.44 +
    4.45 +(* theory data *)
    4.46 +
    4.47 +structure Overload_Data = Theory_Data
    4.48 +(
    4.49 +  type T =
    4.50 +    { internalize : (string * typ) list Symtab.table,
    4.51 +      externalize : string Symtab.table };
    4.52 +  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
    4.53 +  val extend = I;
    4.54 +
    4.55 +  fun merge_ext int_name (ext_name1, ext_name2) =
    4.56 +    if ext_name1 = ext_name2 then ext_name1
    4.57 +    else duplicate_variant_err int_name ext_name1;
    4.58 +
    4.59 +  fun merge ({internalize=int1, externalize=ext1},
    4.60 +      {internalize=int2, externalize=ext2}) =
    4.61 +    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
    4.62 +     externalize=Symtab.join merge_ext (ext1, ext2)};
    4.63 +);
    4.64 +
    4.65 +fun map_tables f g =
    4.66 +  Overload_Data.map (fn {internalize=int, externalize=ext} =>
    4.67 +    {internalize=f int, externalize=g ext});
    4.68 +
    4.69 +val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
    4.70 +val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
    4.71 +val get_external = Symtab.lookup o #externalize o Overload_Data.get;
    4.72 +
    4.73 +fun add_overloaded ext_name thy =
    4.74 +  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
    4.75 +  in map_tables (Symtab.update (ext_name, [])) I thy end;
    4.76 +
    4.77 +fun add_variant ext_name name thy =
    4.78 +  let
    4.79 +    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
    4.80 +    val _ = case get_external thy name of
    4.81 +              NONE => ()
    4.82 +            | SOME gen' => duplicate_variant_err name gen';
    4.83 +    val T = Sign.the_const_type thy name;
    4.84 +  in
    4.85 +    map_tables (Symtab.cons_list (ext_name, (name, T)))
    4.86 +      (Symtab.update (name, ext_name)) thy    
    4.87 +  end
    4.88 +
    4.89 +
    4.90 +(* check / uncheck *)
    4.91 +
    4.92 +fun unifiable_with ctxt T1 (c, T2) =
    4.93 +  let
    4.94 +    val thy = ProofContext.theory_of ctxt;
    4.95 +    val maxidx1 = Term.maxidx_of_typ T1;
    4.96 +    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
    4.97 +    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
    4.98 +  in
    4.99 +    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
   4.100 +    handle Type.TUNIFY => NONE
   4.101 +  end;
   4.102 +
   4.103 +fun insert_internal_same ctxt t (Const (c, T)) =
   4.104 +  (case map_filter (unifiable_with ctxt T) 
   4.105 +     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
   4.106 +      [] => unresolved_err ctxt (c, T) t "no instances"
   4.107 +    | [c'] => Const (c', dummyT)
   4.108 +    | _ => raise Same.SAME)
   4.109 +  | insert_internal_same _ _ _ = raise Same.SAME;
   4.110 +
   4.111 +fun insert_external_same ctxt _ (Const (c, T)) =
   4.112 +    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
   4.113 +  | insert_external_same _ _ _ = raise Same.SAME;
   4.114 +
   4.115 +fun gen_check_uncheck replace ts ctxt =
   4.116 +  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
   4.117 +  |> Option.map (rpair ctxt);
   4.118 +
   4.119 +val check = gen_check_uncheck insert_internal_same;
   4.120 +fun uncheck ts ctxt = 
   4.121 +  if !show_variants then NONE
   4.122 +  else gen_check_uncheck insert_external_same ts ctxt;
   4.123 +
   4.124 +fun reject_unresolved ts ctxt =
   4.125 +  let
   4.126 +    val thy = ProofContext.theory_of ctxt;
   4.127 +    fun check_unresolved t =
   4.128 +      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
   4.129 +          [] => ()
   4.130 +        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
   4.131 +
   4.132 +    val _ = map check_unresolved ts;
   4.133 +  in NONE end;
   4.134 +
   4.135 +
   4.136 +(* setup *)
   4.137 +
   4.138 +val setup = Context.theory_map 
   4.139 +  (Syntax.add_term_check 0 "adhoc_overloading" check
   4.140 +   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
   4.141 +   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
   4.142 +
   4.143 +end