64431
|
1 |
(* Title: internalize_sort.ML
|
|
2 |
Author: Ondřej Kunčar, TU München
|
|
3 |
|
|
4 |
Implements a derived rule (by using Thm.unconstrainT) that internalizes
|
|
5 |
type class annotations.
|
|
6 |
*)
|
|
7 |
|
|
8 |
|
|
9 |
(*
|
|
10 |
\<phi>['a::{c_1, ..., c_n} / 'a]
|
|
11 |
---------------------------------------------------------------------
|
|
12 |
class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
|
|
13 |
|
|
14 |
where class.c is the locale predicate associated with type class c and
|
|
15 |
ops are operations associated with type class c. For example:
|
|
16 |
If c = semigroup_add, then ops = op-, op+, 0, uminus.
|
|
17 |
If c = finite, then ops = TYPE('a::type).
|
|
18 |
*)
|
|
19 |
|
|
20 |
signature INTERNALIZE_SORT =
|
|
21 |
sig
|
|
22 |
val internalize_sort: ctyp -> thm -> typ * thm
|
|
23 |
val internalize_sort_attr: typ -> attribute
|
|
24 |
end;
|
|
25 |
|
|
26 |
structure Internalize_Sort : INTERNALIZE_SORT =
|
|
27 |
struct
|
|
28 |
|
|
29 |
fun internalize_sort ctvar thm =
|
|
30 |
let
|
|
31 |
val thy = Thm.theory_of_thm thm;
|
|
32 |
val tvar = Thm.typ_of ctvar;
|
|
33 |
|
|
34 |
val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
|
|
35 |
|
|
36 |
fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
|
|
37 |
fun reduce_to_non_proper_sort (TVar (name, sort)) =
|
|
38 |
TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
|
|
39 |
| reduce_to_non_proper_sort _ = error "not supported";
|
|
40 |
|
|
41 |
val data = (map fst classes) ~~ assms;
|
|
42 |
|
|
43 |
val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
|
|
44 |
then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
|
|
45 |
|> the_default tvar;
|
|
46 |
|
|
47 |
fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
|
|
48 |
|
|
49 |
fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
|
|
50 |
|
|
51 |
val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
|
|
52 |
then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
|
|
53 |
else discharge_of_class ren_tvar class) data;
|
|
54 |
in
|
|
55 |
(new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
|
|
56 |
end;
|
|
57 |
|
|
58 |
val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
|
|
59 |
| (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
|
|
60 |
|
|
61 |
fun internalize_sort_attr tvar =
|
|
62 |
Thm.rule_attribute [] (fn context => fn thm =>
|
|
63 |
(snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
|
|
64 |
|
|
65 |
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
|
|
66 |
(tvar >> internalize_sort_attr) "internalize a sort"));
|
|
67 |
|
|
68 |
end; |