25519
|
1 |
(* Title: Pure/Isar/overloading.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Overloaded definitions without any discipline.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature OVERLOADING =
|
|
9 |
sig
|
|
10 |
val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
|
|
11 |
val conclude: local_theory -> local_theory
|
|
12 |
val declare: string * typ -> theory -> term * theory
|
|
13 |
val confirm: string -> local_theory -> local_theory
|
|
14 |
val define: bool -> string -> string * term -> theory -> thm * theory
|
|
15 |
val operation: Proof.context -> string -> (string * bool) option
|
25606
|
16 |
val pretty: Proof.context -> Pretty.T
|
25519
|
17 |
end;
|
|
18 |
|
|
19 |
structure Overloading: OVERLOADING =
|
|
20 |
struct
|
|
21 |
|
|
22 |
(* bookkeeping *)
|
|
23 |
|
|
24 |
structure OverloadingData = ProofDataFun
|
|
25 |
(
|
|
26 |
type T = ((string * typ) * (string * bool)) list;
|
|
27 |
fun init _ = [];
|
|
28 |
);
|
|
29 |
|
|
30 |
val get_overloading = OverloadingData.get o LocalTheory.target_of;
|
|
31 |
val map_overloading = LocalTheory.target o OverloadingData.map;
|
|
32 |
|
|
33 |
fun operation lthy v = get_overloading lthy
|
|
34 |
|> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
|
|
35 |
|
|
36 |
fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
|
|
37 |
|
|
38 |
|
|
39 |
(* overloaded declarations and definitions *)
|
|
40 |
|
|
41 |
fun declare c_ty = pair (Const c_ty);
|
|
42 |
|
|
43 |
fun define checked name (c, t) =
|
|
44 |
Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
|
|
45 |
|
|
46 |
|
|
47 |
(* syntax *)
|
|
48 |
|
25536
|
49 |
fun subst_operation overloading = map_aterms (fn t as Const (c, ty) =>
|
|
50 |
(case AList.lookup (op =) overloading (c, ty)
|
|
51 |
of SOME (v, _) => Free (v, ty)
|
|
52 |
| NONE => t)
|
|
53 |
| t => t);
|
|
54 |
|
25519
|
55 |
fun term_check ts lthy =
|
|
56 |
let
|
|
57 |
val overloading = get_overloading lthy;
|
25536
|
58 |
val ts' = map (subst_operation overloading) ts;
|
25519
|
59 |
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
|
|
60 |
|
|
61 |
fun term_uncheck ts lthy =
|
|
62 |
let
|
|
63 |
val overloading = get_overloading lthy;
|
25606
|
64 |
fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) =>
|
|
65 |
if v = v' then SOME c else NONE) overloading
|
25519
|
66 |
of SOME c => Const (c, ty)
|
|
67 |
| NONE => t)
|
|
68 |
| subst t = t;
|
|
69 |
val ts' = (map o map_aterms) subst ts;
|
|
70 |
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
|
|
71 |
|
|
72 |
|
|
73 |
(* target *)
|
|
74 |
|
|
75 |
fun init overloading thy =
|
|
76 |
let
|
|
77 |
val _ = if null overloading then error "At least one parameter must be given" else ();
|
25606
|
78 |
fun declare ((_, ty), (v, _ )) = Variable.declare_term (Free (v, ty));
|
25519
|
79 |
in
|
|
80 |
thy
|
|
81 |
|> ProofContext.init
|
|
82 |
|> OverloadingData.put overloading
|
25606
|
83 |
|> fold declare overloading
|
25519
|
84 |
|> Context.proof_map (
|
|
85 |
Syntax.add_term_check 0 "overloading" term_check
|
|
86 |
#> Syntax.add_term_uncheck 0 "overloading" term_uncheck)
|
|
87 |
end;
|
|
88 |
|
|
89 |
fun conclude lthy =
|
|
90 |
let
|
|
91 |
val overloading = get_overloading lthy;
|
|
92 |
val _ = if null overloading then () else
|
|
93 |
error ("Missing definition(s) for parameters " ^ commas (map (quote
|
|
94 |
o Syntax.string_of_term lthy o Const o fst) overloading));
|
|
95 |
in
|
|
96 |
lthy
|
|
97 |
end;
|
|
98 |
|
25606
|
99 |
fun pretty lthy =
|
|
100 |
let
|
|
101 |
val thy = ProofContext.theory_of lthy;
|
|
102 |
val overloading = get_overloading lthy;
|
|
103 |
fun pr_operation ((c, ty), (v, _)) =
|
|
104 |
(Pretty.block o Pretty.breaks) [Pretty.str (Sign.extern_const thy c), Pretty.str "::",
|
|
105 |
Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
|
|
106 |
in
|
|
107 |
(Pretty.block o Pretty.fbreaks)
|
|
108 |
(Pretty.str "overloading" :: map pr_operation overloading)
|
|
109 |
end;
|
|
110 |
|
25519
|
111 |
end;
|