src/Tools/adhoc_overloading.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 37818 dd65033fed78
child 41472 f6ab14e61604
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
krauss@37789
     1
(* Author: Alexander Krauss, TU Muenchen
krauss@37789
     2
   Author: Christian Sternagel, University of Innsbruck
krauss@37789
     3
krauss@37789
     4
Ad-hoc overloading of constants based on their types.
krauss@37789
     5
*)
krauss@37789
     6
krauss@37789
     7
signature ADHOC_OVERLOADING =
krauss@37789
     8
sig
krauss@37789
     9
krauss@37789
    10
  val add_overloaded: string -> theory -> theory
krauss@37789
    11
  val add_variant: string -> string -> theory -> theory
krauss@37789
    12
krauss@37789
    13
  val show_variants: bool Unsynchronized.ref
krauss@37789
    14
  val setup: theory -> theory
krauss@37789
    15
krauss@37789
    16
end
krauss@37789
    17
krauss@37789
    18
krauss@37789
    19
structure Adhoc_Overloading: ADHOC_OVERLOADING =
krauss@37789
    20
struct
krauss@37789
    21
krauss@37789
    22
val show_variants = Unsynchronized.ref false;
krauss@37789
    23
krauss@37789
    24
krauss@37789
    25
(* errors *)
krauss@37789
    26
krauss@37789
    27
fun duplicate_variant_err int_name ext_name =
krauss@37789
    28
  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
krauss@37789
    29
krauss@37789
    30
fun not_overloaded_err name =
krauss@37789
    31
  error ("Constant " ^ quote name ^ " is not declared as overloaded");
krauss@37789
    32
krauss@37789
    33
fun already_overloaded_err name =
krauss@37789
    34
  error ("Constant " ^ quote name ^ " is already declared as overloaded");
krauss@37789
    35
krauss@37789
    36
fun unresolved_err ctxt (c, T) t reason =
krauss@37789
    37
  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
krauss@37789
    38
    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
krauss@37789
    39
    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
krauss@37789
    40
krauss@37789
    41
krauss@37789
    42
(* theory data *)
krauss@37789
    43
krauss@37789
    44
structure Overload_Data = Theory_Data
krauss@37789
    45
(
krauss@37789
    46
  type T =
krauss@37789
    47
    { internalize : (string * typ) list Symtab.table,
krauss@37789
    48
      externalize : string Symtab.table };
krauss@37789
    49
  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
krauss@37789
    50
  val extend = I;
krauss@37789
    51
krauss@37789
    52
  fun merge_ext int_name (ext_name1, ext_name2) =
krauss@37789
    53
    if ext_name1 = ext_name2 then ext_name1
krauss@37789
    54
    else duplicate_variant_err int_name ext_name1;
krauss@37789
    55
krauss@37789
    56
  fun merge ({internalize=int1, externalize=ext1},
krauss@37789
    57
      {internalize=int2, externalize=ext2}) =
krauss@37789
    58
    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
krauss@37789
    59
     externalize=Symtab.join merge_ext (ext1, ext2)};
krauss@37789
    60
);
krauss@37789
    61
krauss@37789
    62
fun map_tables f g =
krauss@37789
    63
  Overload_Data.map (fn {internalize=int, externalize=ext} =>
krauss@37789
    64
    {internalize=f int, externalize=g ext});
krauss@37789
    65
krauss@37789
    66
val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
krauss@37789
    67
val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
krauss@37789
    68
val get_external = Symtab.lookup o #externalize o Overload_Data.get;
krauss@37789
    69
krauss@37789
    70
fun add_overloaded ext_name thy =
krauss@37789
    71
  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
krauss@37789
    72
  in map_tables (Symtab.update (ext_name, [])) I thy end;
krauss@37789
    73
krauss@37789
    74
fun add_variant ext_name name thy =
krauss@37789
    75
  let
krauss@37789
    76
    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
krauss@37789
    77
    val _ = case get_external thy name of
krauss@37789
    78
              NONE => ()
krauss@37789
    79
            | SOME gen' => duplicate_variant_err name gen';
krauss@37789
    80
    val T = Sign.the_const_type thy name;
krauss@37789
    81
  in
krauss@37789
    82
    map_tables (Symtab.cons_list (ext_name, (name, T)))
krauss@37789
    83
      (Symtab.update (name, ext_name)) thy    
krauss@37789
    84
  end
krauss@37789
    85
krauss@37789
    86
krauss@37789
    87
(* check / uncheck *)
krauss@37789
    88
krauss@37789
    89
fun unifiable_with ctxt T1 (c, T2) =
krauss@37789
    90
  let
krauss@37789
    91
    val thy = ProofContext.theory_of ctxt;
krauss@37789
    92
    val maxidx1 = Term.maxidx_of_typ T1;
krauss@37789
    93
    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
krauss@37789
    94
    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
krauss@37789
    95
  in
krauss@37789
    96
    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
krauss@37789
    97
    handle Type.TUNIFY => NONE
krauss@37789
    98
  end;
krauss@37789
    99
krauss@37789
   100
fun insert_internal_same ctxt t (Const (c, T)) =
krauss@37789
   101
  (case map_filter (unifiable_with ctxt T) 
krauss@37789
   102
     (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
krauss@37789
   103
      [] => unresolved_err ctxt (c, T) t "no instances"
krauss@37789
   104
    | [c'] => Const (c', dummyT)
krauss@37789
   105
    | _ => raise Same.SAME)
krauss@37789
   106
  | insert_internal_same _ _ _ = raise Same.SAME;
krauss@37789
   107
krauss@37789
   108
fun insert_external_same ctxt _ (Const (c, T)) =
krauss@37789
   109
    Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
krauss@37789
   110
  | insert_external_same _ _ _ = raise Same.SAME;
krauss@37789
   111
krauss@37789
   112
fun gen_check_uncheck replace ts ctxt =
krauss@37789
   113
  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
krauss@37789
   114
  |> Option.map (rpair ctxt);
krauss@37789
   115
krauss@37789
   116
val check = gen_check_uncheck insert_internal_same;
krauss@37789
   117
fun uncheck ts ctxt = 
krauss@37789
   118
  if !show_variants then NONE
krauss@37789
   119
  else gen_check_uncheck insert_external_same ts ctxt;
krauss@37789
   120
krauss@37789
   121
fun reject_unresolved ts ctxt =
krauss@37789
   122
  let
krauss@37789
   123
    val thy = ProofContext.theory_of ctxt;
krauss@37789
   124
    fun check_unresolved t =
krauss@37789
   125
      case filter (is_overloaded thy o fst) (Term.add_consts t []) of
krauss@37789
   126
          [] => ()
krauss@37789
   127
        | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
krauss@37789
   128
krauss@37789
   129
    val _ = map check_unresolved ts;
krauss@37789
   130
  in NONE end;
krauss@37789
   131
krauss@37789
   132
krauss@37789
   133
(* setup *)
krauss@37789
   134
krauss@37789
   135
val setup = Context.theory_map 
krauss@37789
   136
  (Syntax.add_term_check 0 "adhoc_overloading" check
krauss@37789
   137
   #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
krauss@37789
   138
   #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
krauss@37789
   139
krauss@37789
   140
end