src/Tools/adhoc_overloading.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 56002 2028467b4df4
child 59414 eb3d8e7b4b21
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
     1
(*  Author:     Alexander Krauss, TU Muenchen
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
     2
    Author:     Christian Sternagel, University of Innsbruck
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     3
52893
aa2afbafd983 use uniform spelling of "adhoc"
Christian Sternagel
parents: 52892
diff changeset
     4
Adhoc overloading of constants based on their types.
37789
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
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
     9
  val is_overloaded: Proof.context -> string -> bool
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    10
  val generic_add_overloaded: string -> Context.generic -> Context.generic
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    11
  val generic_remove_overloaded: string -> Context.generic -> Context.generic
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    12
  val generic_add_variant: string -> term -> Context.generic -> Context.generic
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    13
  (*If the list of variants is empty at the end of "generic_remove_variant", then
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    14
  "generic_remove_overloaded" is called implicitly.*)
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    15
  val generic_remove_variant: string -> term -> Context.generic -> Context.generic
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    16
  val show_variants: bool Config.T
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    17
end
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    18
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    19
structure Adhoc_Overloading: ADHOC_OVERLOADING =
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    20
struct
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    21
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
    22
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
    23
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
    24
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    25
(* errors *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    26
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
    27
fun err_duplicate_variant oconst =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    28
  error ("Duplicate variant of " ^ quote oconst);
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    29
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
    30
fun err_not_a_variant oconst =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    31
  error ("Not a variant of " ^  quote oconst);
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    32
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
    33
fun err_not_overloaded oconst =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    34
  error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    35
53540
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    36
fun err_unresolved_overloading ctxt0 (c, T) t instances =
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    37
  let
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    38
    val ctxt = Config.put show_variants true ctxt0
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    39
    val const_space = Proof_Context.const_space ctxt
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    40
    val prt_const =
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    41
      Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1,
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    42
        Pretty.quote (Syntax.pretty_typ ctxt T)]
52688
1e13b2515e2b show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents: 52687
diff changeset
    43
  in
53537
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    44
    error (Pretty.string_of (Pretty.chunks [
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    45
      Pretty.block [
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    46
        Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
53540
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    47
        prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    48
        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]],
53537
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    49
      Pretty.block (
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    50
        (if null instances then [Pretty.str "no instances"]
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    51
        else Pretty.fbreaks (
addbc2387c61 tuned message;
wenzelm
parents: 53008
diff changeset
    52
          Pretty.str "multiple instances:" ::
53540
7903fe2c271b prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents: 53538
diff changeset
    53
          map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))]))
52688
1e13b2515e2b show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents: 52687
diff changeset
    54
  end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    55
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
    56
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    57
(* generic data *)
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    58
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    59
fun variants_eq ((v1, T1), (v2, T2)) =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    60
  Term.aconv_untyped (v1, v2) andalso T1 = T2;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    61
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    62
structure Overload_Data = Generic_Data
37789
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
  type T =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    65
    {variants : (term * typ) list Symtab.table,
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    66
     oconsts : string Termtab.table};
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    67
  val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    68
  val extend = I;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    69
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 37818
diff changeset
    70
  fun merge
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    71
    ({variants = vtab1, oconsts = otab1},
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    72
     {variants = vtab2, oconsts = otab2}) : T =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    73
    let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    74
      fun merge_oconsts _ (oconst1, oconst2) =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    75
        if oconst1 = oconst2 then oconst1
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
    76
        else err_duplicate_variant oconst1;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    77
    in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    78
      {variants = Symtab.merge_list variants_eq (vtab1, vtab2),
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    79
       oconsts = Termtab.join merge_oconsts (otab1, otab2)}
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    80
    end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    81
);
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    82
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    83
fun map_tables f g =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    84
  Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    85
    {variants = f vtab, oconsts = g otab});
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    86
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    87
val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    88
val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    89
val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    90
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    91
fun generic_add_overloaded oconst context =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    92
  if is_overloaded (Context.proof_of context) oconst then context
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    93
  else map_tables (Symtab.update (oconst, [])) I context;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    94
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    95
fun generic_remove_overloaded oconst context =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    96
  let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    97
    fun remove_oconst_and_variants context oconst =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    98
      let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
    99
        val remove_variants =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   100
          (case get_variants (Context.proof_of context) oconst of
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   101
            NONE => I
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   102
          | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs);
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   103
      in map_tables (Symtab.delete_safe oconst) remove_variants context end;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   104
  in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   105
    if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   106
    else err_not_overloaded oconst
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   107
  end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   108
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   109
local
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   110
  fun generic_variant add oconst t context =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   111
    let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   112
      val ctxt = Context.proof_of context;
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   113
      val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst;
53005
47db379a6cf9 move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents: 53004
diff changeset
   114
      val T = t |> fastype_of;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   115
      val t' = Term.map_types (K dummyT) t;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   116
    in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   117
      if add then
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   118
        let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   119
          val _ =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   120
            (case get_overloaded ctxt t' of
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   121
              NONE => ()
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   122
            | SOME oconst' => err_duplicate_variant oconst');
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   123
        in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   124
          map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   125
        end
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   126
      else
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   127
        let
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   128
          val _ =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   129
            if member variants_eq (the (get_variants ctxt oconst)) (t', T) then ()
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   130
            else err_not_a_variant oconst;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   131
        in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   132
          map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   133
            (Termtab.delete_safe t') context
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   134
          |> (fn context =>
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   135
            (case get_variants (Context.proof_of context) oconst of
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   136
              SOME [] => generic_remove_overloaded oconst context
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   137
            | _ => context))
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   138
        end
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   139
    end;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   140
in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   141
  val generic_add_variant = generic_variant true;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   142
  val generic_remove_variant = generic_variant false;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   143
end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   144
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
   145
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   146
(* check / uncheck *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   147
53004
38165b99562e clarify function;
Christian Sternagel
parents: 52893
diff changeset
   148
fun unifiable_with thy T1 T2 =
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   149
  let
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   150
    val maxidx1 = Term.maxidx_of_typ T1;
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   151
    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   152
    val maxidx2 = Term.maxidx_typ T2' maxidx1;
53004
38165b99562e clarify function;
Christian Sternagel
parents: 52893
diff changeset
   153
  in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   154
53006
83d9984ee639 avoid misleading "instances" in function name;
Christian Sternagel
parents: 53005
diff changeset
   155
fun get_candidates ctxt (c, T) =
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   156
  get_variants ctxt c
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   157
  |> Option.map (map_filter (fn (t, T') =>
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   158
    if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   159
    else NONE));
52687
72cda5eb5a39 refactoring
Christian Sternagel
parents: 52622
diff changeset
   160
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   161
fun insert_variants ctxt t (oconst as Const (c, T)) =
53006
83d9984ee639 avoid misleading "instances" in function name;
Christian Sternagel
parents: 53005
diff changeset
   162
      (case get_candidates ctxt (c, T) of
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   163
        SOME [] => err_unresolved_overloading ctxt (c, T) t []
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   164
      | SOME [variant] => variant
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   165
      | _ => oconst)
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   166
  | insert_variants _ _ oconst = oconst;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   167
54004
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   168
fun insert_overloaded ctxt =
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   169
  let
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   170
    fun proc t =
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   171
      Term.map_types (K dummyT) t
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   172
      |> get_overloaded ctxt
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   173
      |> Option.map (Const o rpair (Term.type_of t));
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   174
  in
55237
1e341728bae9 prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
wenzelm
parents: 54468
diff changeset
   175
    Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
54004
e13b0c88c798 preserve types during rewriting
Christian Sternagel
parents: 53540
diff changeset
   176
  end;
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   177
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   178
fun check ctxt =
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   179
  map (fn t => Term.map_aterms (insert_variants ctxt t) t);
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   180
54468
f6ffe53387ef reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents: 54004
diff changeset
   181
fun uncheck ctxt ts =
f6ffe53387ef reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents: 54004
diff changeset
   182
  if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
f6ffe53387ef reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents: 54004
diff changeset
   183
  else map (insert_overloaded ctxt) ts;
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   184
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   185
fun reject_unresolved ctxt =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   186
  let
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   187
    val the_candidates = the o get_candidates ctxt;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   188
    fun check_unresolved t =
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   189
      (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   190
        [] => t
53008
128bec4e3fca indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents: 53007
diff changeset
   191
      | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   192
  in map check_unresolved end;
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   193
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
   194
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   195
(* setup *)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   196
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   197
val _ = Context.>>
53007
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   198
  (Syntax_Phases.term_check 0 "adhoc_overloading" check
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   199
   #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
54e290da6da8 avoid low-level Same structure;
Christian Sternagel
parents: 53006
diff changeset
   200
   #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
   201
53538
4e9e150422d5 tuned whitespace;
wenzelm
parents: 53537
diff changeset
   202
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   203
(* commands *)
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   204
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   205
fun generic_adhoc_overloading_cmd add =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   206
  if add then
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   207
    fold (fn (oconst, ts) =>
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   208
      generic_add_overloaded oconst
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   209
      #> fold (generic_add_variant oconst) ts)
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   210
  else
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   211
    fold (fn (oconst, ts) =>
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   212
      fold (generic_remove_variant oconst) ts);
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   213
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   214
fun adhoc_overloading_cmd' add args phi =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   215
  let val args' = args
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   216
    |> map (apsnd (map_filter (fn t =>
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   217
         let val t' = Morphism.term phi t;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   218
         in if Term.aconv_untyped (t, t') then SOME t' else NONE end)));
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   219
  in generic_adhoc_overloading_cmd add args' end;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   220
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   221
fun adhoc_overloading_cmd add raw_args lthy =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   222
  let
55954
a29aefc88c8d more uniform check_const/read_const;
wenzelm
parents: 55237
diff changeset
   223
    fun const_name ctxt =
56002
2028467b4df4 tuned signature;
wenzelm
parents: 55958
diff changeset
   224
      fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt;  (* FIXME {proper = true, strict = true} (!?) *)
53005
47db379a6cf9 move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents: 53004
diff changeset
   225
    fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   226
    val args =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   227
      raw_args
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   228
      |> map (apfst (const_name lthy))
53005
47db379a6cf9 move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents: 53004
diff changeset
   229
      |> map (apsnd (map (read_term lthy)));
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   230
  in
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   231
    Local_Theory.declaration {syntax = true, pervasive = false}
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   232
      (adhoc_overloading_cmd' add args) lthy
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   233
  end;
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   234
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   235
val _ =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   236
  Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
52893
aa2afbafd983 use uniform spelling of "adhoc"
Christian Sternagel
parents: 52892
diff changeset
   237
    "add adhoc overloading for constants / fixed variables"
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   238
    (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   239
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   240
val _ =
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   241
  Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
52893
aa2afbafd983 use uniform spelling of "adhoc"
Christian Sternagel
parents: 52892
diff changeset
   242
    "add adhoc overloading for constants / fixed variables"
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   243
    (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   244
45422
711dac69111b proper configuration option;
wenzelm
parents: 42402
diff changeset
   245
end;
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 50768
diff changeset
   246