src/HOL/Library/adhoc_overloading.ML
changeset 37789 93f6dcf9ec02
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/adhoc_overloading.ML	Tue Jul 13 00:15:37 2010 +0200
     1.3 @@ -0,0 +1,140 @@
     1.4 +(* Author: Alexander Krauss, TU Muenchen
     1.5 +   Author: Christian Sternagel, University of Innsbruck
     1.6 +
     1.7 +Ad-hoc overloading of constants based on their types.
     1.8 +*)
     1.9 +
    1.10 +signature ADHOC_OVERLOADING =
    1.11 +sig
    1.12 +
    1.13 +  val add_overloaded: string -> theory -> theory
    1.14 +  val add_variant: string -> string -> theory -> theory
    1.15 +
    1.16 +  val show_variants: bool Unsynchronized.ref
    1.17 +  val setup: theory -> theory
    1.18 +
    1.19 +end
    1.20 +
    1.21 +
    1.22 +structure Adhoc_Overloading: ADHOC_OVERLOADING =
    1.23 +struct
    1.24 +
    1.25 +val show_variants = Unsynchronized.ref false;
    1.26 +
    1.27 +
    1.28 +(* errors *)
    1.29 +
    1.30 +fun duplicate_variant_err int_name ext_name =
    1.31 +  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
    1.32 +
    1.33 +fun not_overloaded_err name =
    1.34 +  error ("Constant " ^ quote name ^ " is not declared as overloaded");
    1.35 +
    1.36 +fun already_overloaded_err name =
    1.37 +  error ("Constant " ^ quote name ^ " is already declared as overloaded");
    1.38 +
    1.39 +fun unresolved_err ctxt (c, T) t reason =
    1.40 +  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
    1.41 +    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
    1.42 +    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
    1.43 +
    1.44 +
    1.45 +(* theory data *)
    1.46 +
    1.47 +structure Overload_Data = Theory_Data
    1.48 +(
    1.49 +  type T =
    1.50 +    { internalize : (string * typ) list Symtab.table,
    1.51 +      externalize : string Symtab.table };
    1.52 +  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
    1.53 +  val extend = I;
    1.54 +
    1.55 +  fun merge_ext int_name (ext_name1, ext_name2) =
    1.56 +    if ext_name1 = ext_name2 then ext_name1
    1.57 +    else duplicate_variant_err int_name ext_name1;
    1.58 +
    1.59 +  fun merge ({internalize=int1, externalize=ext1},
    1.60 +      {internalize=int2, externalize=ext2}) =
    1.61 +    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
    1.62 +     externalize=Symtab.join merge_ext (ext1, ext2)};
    1.63 +);
    1.64 +
    1.65 +fun map_tables f g =
    1.66 +  Overload_Data.map (fn {internalize=int, externalize=ext} =>
    1.67 +    {internalize=f int, externalize=g ext});
    1.68 +
    1.69 +val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
    1.70 +val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
    1.71 +val get_external = Symtab.lookup o #externalize o Overload_Data.get;
    1.72 +
    1.73 +fun add_overloaded ext_name thy =
    1.74 +  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
    1.75 +  in map_tables (Symtab.update (ext_name, [])) I thy end;
    1.76 +
    1.77 +fun add_variant ext_name name thy =
    1.78 +  let
    1.79 +    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
    1.80 +    val _ = case get_external thy name of
    1.81 +              NONE => ()
    1.82 +            | SOME gen' => duplicate_variant_err name gen';
    1.83 +    val T = Sign.the_const_type thy name;
    1.84 +  in
    1.85 +    map_tables (Symtab.cons_list (ext_name, (name, T)))
    1.86 +      (Symtab.update (name, ext_name)) thy    
    1.87 +  end
    1.88 +
    1.89 +
    1.90 +(* check / uncheck *)
    1.91 +
    1.92 +fun unifiable_with ctxt T1 (c, T2) =
    1.93 +  let
    1.94 +    val thy = ProofContext.theory_of ctxt;
    1.95 +    val maxidx1 = Term.maxidx_of_typ T1;
    1.96 +    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
    1.97 +    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
    1.98 +  in
    1.99 +    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
   1.100 +    handle Type.TUNIFY => NONE
   1.101 +  end;
   1.102 +
   1.103 +fun insert_internal_same ctxt t (Const (c, T)) =
   1.104 +  (case map_filter (unifiable_with ctxt T) 
   1.105 +     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
   1.106 +      [] => unresolved_err ctxt (c, T) t "no instances"
   1.107 +    | [c'] => Const (c', dummyT)
   1.108 +    | _ => raise Same.SAME)
   1.109 +  | insert_internal_same _ _ _ = raise Same.SAME;
   1.110 +
   1.111 +fun insert_external_same ctxt _ (Const (c, T)) =
   1.112 +    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
   1.113 +  | insert_external_same _ _ _ = raise Same.SAME;
   1.114 +
   1.115 +fun gen_check_uncheck replace ts ctxt =
   1.116 +  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
   1.117 +  |> Option.map (rpair ctxt);
   1.118 +
   1.119 +val check = gen_check_uncheck insert_internal_same;
   1.120 +fun uncheck ts ctxt = 
   1.121 +  if !show_variants then NONE
   1.122 +  else gen_check_uncheck insert_external_same ts ctxt;
   1.123 +
   1.124 +fun reject_unresolved ts ctxt =
   1.125 +  let
   1.126 +    val thy = ProofContext.theory_of ctxt;
   1.127 +    fun check_unresolved t =
   1.128 +      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
   1.129 +          [] => ()
   1.130 +        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
   1.131 +
   1.132 +    val _ = map check_unresolved ts;
   1.133 +  in NONE end;
   1.134 +
   1.135 +
   1.136 +(* setup *)
   1.137 +
   1.138 +val setup = Context.theory_map 
   1.139 +  (Syntax.add_term_check 0 "adhoc_overloading" check
   1.140 +   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
   1.141 +   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
   1.142 +
   1.143 +end