1(*  Title:      HOL/Types_To_Sets/unoverloading.ML
2    Author:     Ond��ej Kun��ar, TU M��nchen
3
4The Unoverloading Rule (extension of the logic).
5*)
6
7signature UNOVERLOADING =
8sig
9  val unoverload: cterm -> thm -> thm
10  val unoverload_attr: cterm -> attribute
11end;
12
13structure Unoverloading : UNOVERLOADING =
14struct
15
16(*
17Unoverloading Rule (UO)
18
19      \<turnstile> \<phi>[c::\<sigma> / x::\<sigma>]
20---------------------------- [no type or constant or type class in \<phi>
21        \<turnstile> \<And>x::\<sigma>. \<phi>           depends on c::\<sigma>; c::\<sigma> is undefined]
22*)
23
24(* The following functions match_args, reduction and entries_of were
25   cloned from defs.ML and theory.ML because the functions are not public.
26   Notice that these functions already belong to the critical code.
27*)
28
29(* >= *)
30fun match_args (Ts, Us) =
31  if Type.could_matches (Ts, Us) then
32    Option.map Envir.subst_type
33      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
34  else NONE;
35
36fun reduction defs (deps : Defs.entry list) : Defs.entry list option =
37  let
38    fun reduct Us (Ts, rhs) =
39      (case match_args (Ts, Us) of
40        NONE => NONE
41      | SOME subst => SOME (map (apsnd (map subst)) rhs));
42    fun reducts (d, Us) = get_first (reduct Us) (Defs.get_deps defs d);
43
44    val reds = map (`reducts) deps;
45    val deps' =
46      if forall (is_none o #1) reds then NONE
47      else SOME (fold_rev
48        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
49  in deps' end;
50
51fun const_and_typ_entries_of thy tm =
52 let
53   val consts =
54     fold_aterms (fn Const const => insert (op =) (Theory.const_dep thy const) | _ => I) tm [];
55   val types =
56     (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) tm [];
57 in
58   consts @ types
59 end;
60
61
62(* The actual implementation *)
63
64(** BEGINNING OF THE CRITICAL CODE **)
65
66fun fold_atyps_classes f =
67  fold_atyps (fn T as TFree (_, S) => fold (pair T #> f) S
68    | T as TVar (_, S) => fold (pair T #> f) S
69    (* just to avoid a warning about incomplete patterns *)
70    | _ => raise TERM ("fold_atyps_classes", []));
71
72fun class_entries_of thy tm =
73  let
74    val var_classes = (fold_types o fold_atyps_classes) (insert op=) tm [];
75  in
76    map (Logic.mk_of_class #> Term.head_of #> Term.dest_Const #> Theory.const_dep thy) var_classes
77  end;
78
79fun unoverload_impl cconst thm =
80  let
81    fun err msg = raise THM ("unoverloading: " ^ msg, 0, [thm]);
82
83    val _ = null (Thm.hyps_of thm) orelse err "the theorem has meta hypotheses";
84    val _ = null (Thm.tpairs_of thm) orelse err "the theorem contains unresolved flex-flex pairs";
85
86    val prop = Thm.prop_of thm;
87    val prop_tfrees = rev (Term.add_tfree_names prop []);
88    val _ = null prop_tfrees orelse err ("the theorem contains free type variables "
89      ^ commas_quote prop_tfrees);
90
91    val const = Thm.term_of cconst;
92    val _ = Term.is_Const const orelse err "the parameter is is not a constant";
93    val const_tfrees = rev (Term.add_tfree_names const []);
94    val _ = null const_tfrees orelse err ("the constant contains free type variables "
95      ^ commas_quote const_tfrees);
96
97    val thy = Thm.theory_of_thm thm;
98    val defs = Theory.defs_of thy;
99
100    val const_entry = Theory.const_dep thy (Term.dest_Const const);
101
102    val Uss = Defs.specifications_of defs (fst const_entry);
103    val _ = forall (fn spec => is_none (match_args (#lhs spec, snd const_entry))) Uss
104      orelse err "the constant instance has already a specification";
105
106    val context = Defs.global_context thy;
107    val prt_entry = Pretty.string_of o Defs.pretty_entry context;
108
109    fun dep_err (c, Ts) (d, Us) =
110      err (prt_entry (c, Ts) ^ " depends on " ^ prt_entry (d, Us));
111    fun deps_of entry = perhaps_loop (reduction defs) [entry] |> these;
112    fun not_depends_on_const prop_entry = forall (not_equal const_entry) (deps_of prop_entry)
113      orelse dep_err prop_entry const_entry;
114    val prop_entries = const_and_typ_entries_of thy prop @ class_entries_of thy prop;
115    val _ = forall not_depends_on_const prop_entries;
116  in
117    Thm.global_cterm_of thy (Logic.all const prop) |> Thm.weaken_sorts (Thm.shyps_of thm)
118  end;
119
120(** END OF THE CRITICAL CODE **)
121
122val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
123  (Thm.add_oracle (\<^binding>\<open>unoverload\<close>,
124  fn (const, thm) => unoverload_impl const  thm)));
125
126fun unoverload const thm = unoverload_oracle (const, thm);
127
128fun unoverload_attr const =
129  Thm.rule_attribute [] (fn _ => fn thm => (unoverload const thm));
130
131val const = Args.context -- Args.term  >>
132  (fn (ctxt, tm) =>
133    if not (Term.is_Const tm)
134    then error ("The term is not a constant: " ^ Syntax.string_of_term ctxt tm)
135    else tm |> Logic.varify_types_global |> Thm.cterm_of ctxt);
136
137val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload\<close>
138  (const >> unoverload_attr) "unoverload an uninterpreted constant"));
139
140end;
141