src/Tools/adhoc_overloading.ML
author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 50768 2172f82de515
child 52622 e0ff1625e96d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     1
(* Author: Alexander Krauss, TU Muenchen
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     2
   Author: Christian Sternagel, University of Innsbruck
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     3
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     4
Ad-hoc overloading of constants based on their types.
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     5
*)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     6
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     7
signature ADHOC_OVERLOADING =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     8
sig
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     9
  val add_overloaded: string -> theory -> theory
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    10
  val add_variant: string -> string -> theory -> theory
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    11
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    12
  val show_variants: bool Config.T
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    13
  val setup: theory -> theory
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    14
end
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    15
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    16
structure Adhoc_Overloading: ADHOC_OVERLOADING =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    17
struct
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    18
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    19
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    20
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    21
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    22
(* errors *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    23
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    24
fun duplicate_variant_err int_name ext_name =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    25
  error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    26
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    27
fun not_overloaded_err name =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    28
  error ("Constant " ^ quote name ^ " is not declared as overloaded");
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    29
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    30
fun already_overloaded_err name =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    31
  error ("Constant " ^ quote name ^ " is already declared as overloaded");
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    32
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    33
fun unresolved_err ctxt (c, T) t reason =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    34
  error ("Unresolved overloading of  " ^ quote c ^ " :: " ^
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    35
    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    36
    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    37
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    38
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    39
(* theory data *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    40
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    41
structure Overload_Data = Theory_Data
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    42
(
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    43
  type T =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    44
    { internalize : (string * typ) list Symtab.table,
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    45
      externalize : string Symtab.table };
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    46
  val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    47
  val extend = I;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    48
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    49
  fun merge_ext int_name (ext_name1, ext_name2) =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    50
    if ext_name1 = ext_name2 then ext_name1
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    51
    else duplicate_variant_err int_name ext_name1;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    52
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 37818
diff changeset
    53
  fun merge
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 37818
diff changeset
    54
    ({internalize = int1, externalize = ext1},
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 37818
diff changeset
    55
      {internalize = int2, externalize = ext2}) : T =
50768
2172f82de515 tuned -- prefer high-level Table.merge with its slightly more conservative update;
wenzelm
parents: 45444
diff changeset
    56
    {internalize = Symtab.merge_list (op =) (int1, int2),
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 37818
diff changeset
    57
      externalize = Symtab.join merge_ext (ext1, ext2)};
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    58
);
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    59
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    60
fun map_tables f g =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    61
  Overload_Data.map (fn {internalize=int, externalize=ext} =>
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    62
    {internalize=f int, externalize=g ext});
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    63
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    64
val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    65
val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    66
val get_external = Symtab.lookup o #externalize o Overload_Data.get;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    67
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    68
fun add_overloaded ext_name thy =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    69
  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    70
  in map_tables (Symtab.update (ext_name, [])) I thy end;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    71
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    72
fun add_variant ext_name name thy =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    73
  let
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    74
    val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    75
    val _ =
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    76
      (case get_external thy name of
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    77
        NONE => ()
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    78
      | SOME gen' => duplicate_variant_err name gen');
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    79
    val T = Sign.the_const_type thy name;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    80
  in
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    81
    map_tables (Symtab.cons_list (ext_name, (name, T)))
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    82
      (Symtab.update (name, ext_name)) thy
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    83
  end
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    84
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    85
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    86
(* check / uncheck *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    87
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    88
fun unifiable_with ctxt T1 (c, T2) =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    89
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41472
diff changeset
    90
    val thy = Proof_Context.theory_of ctxt;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    91
    val maxidx1 = Term.maxidx_of_typ T1;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    92
    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    93
    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    94
  in
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    95
    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    96
    handle Type.TUNIFY => NONE
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    97
  end;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    98
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    99
fun insert_internal_same ctxt t (Const (c, T)) =
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   100
      (case map_filter (unifiable_with ctxt T)
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   101
         (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   102
        [] => unresolved_err ctxt (c, T) t "no instances"
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   103
      | [c'] => Const (c', dummyT)
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   104
      | _ => raise Same.SAME)
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   105
  | insert_internal_same _ _ _ = raise Same.SAME;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   106
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   107
fun insert_external_same ctxt _ (Const (c, T)) =
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   108
      Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T)
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   109
  | insert_external_same _ _ _ = raise Same.SAME;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   110
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   111
fun gen_check_uncheck replace ts ctxt =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   112
  Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   113
  |> Option.map (rpair ctxt);
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   114
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   115
val check = gen_check_uncheck insert_internal_same;
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   116
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   117
fun uncheck ts ctxt =
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   118
  if Config.get ctxt show_variants then NONE
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   119
  else gen_check_uncheck insert_external_same ts ctxt;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   120
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   121
fun reject_unresolved ts ctxt =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   122
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41472
diff changeset
   123
    val thy = Proof_Context.theory_of ctxt;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   124
    fun check_unresolved t =
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   125
      (case filter (is_overloaded thy o fst) (Term.add_consts t []) of
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   126
        [] => ()
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   127
      | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances");
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   128
    val _ = map check_unresolved ts;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   129
  in NONE end;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   130
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   131
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   132
(* setup *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   133
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   134
val setup = Context.theory_map
45444
ac069060e08a tuned signature;
wenzelm
parents: 45429
diff changeset
   135
  (Syntax_Phases.term_check' 0 "adhoc_overloading" check
ac069060e08a tuned signature;
wenzelm
parents: 45429
diff changeset
   136
   #> Syntax_Phases.term_check' 1 "adhoc_overloading_unresolved_check" reject_unresolved
ac069060e08a tuned signature;
wenzelm
parents: 45429
diff changeset
   137
   #> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck);
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   138
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   139
end;