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
|
25861
|
10 |
val init: (string * (string * typ) * bool) list -> theory -> local_theory
|
25519
|
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
|
26238
|
17 |
|
|
18 |
type improvable_syntax
|
|
19 |
val add_improvable_syntax: Proof.context -> Proof.context
|
|
20 |
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
|
|
21 |
-> Proof.context -> Proof.context
|
26259
|
22 |
val set_local_constraints: Proof.context -> Proof.context
|
25519
|
23 |
end;
|
|
24 |
|
|
25 |
structure Overloading: OVERLOADING =
|
|
26 |
struct
|
|
27 |
|
26259
|
28 |
(** generic check/uncheck combinators for improvable constants **)
|
26238
|
29 |
|
26249
|
30 |
type improvable_syntax = ((((string * typ) list * (string * typ) list) *
|
|
31 |
(((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) *
|
|
32 |
(term * term) list)) * bool);
|
25519
|
33 |
|
26238
|
34 |
structure ImprovableSyntax = ProofDataFun(
|
26249
|
35 |
type T = {
|
|
36 |
local_constraints: (string * typ) list,
|
|
37 |
global_constraints: (string * typ) list,
|
|
38 |
improve: string * typ -> (typ * typ) option,
|
|
39 |
subst: string * typ -> (typ * term) option,
|
|
40 |
unchecks: (term * term) list,
|
|
41 |
passed: bool
|
|
42 |
};
|
26238
|
43 |
fun init _ = {
|
|
44 |
local_constraints = [],
|
|
45 |
global_constraints = [],
|
|
46 |
improve = K NONE,
|
|
47 |
subst = K NONE,
|
|
48 |
unchecks = [],
|
|
49 |
passed = true
|
|
50 |
};
|
|
51 |
);
|
25536
|
52 |
|
26249
|
53 |
fun map_improvable_syntax f = ImprovableSyntax.map (fn { local_constraints,
|
|
54 |
global_constraints, improve, subst, unchecks, passed } => let
|
|
55 |
val (((local_constraints', global_constraints'), ((improve', subst'), unchecks')), passed')
|
|
56 |
= f (((local_constraints, global_constraints), ((improve, subst), unchecks)), passed)
|
|
57 |
in { local_constraints = local_constraints', global_constraints = global_constraints',
|
|
58 |
improve = improve', subst = subst', unchecks = unchecks', passed = passed'
|
|
59 |
} end);
|
26238
|
60 |
|
26249
|
61 |
val mark_passed = (map_improvable_syntax o apsnd) (K true);
|
26238
|
62 |
|
|
63 |
fun improve_term_check ts ctxt =
|
25519
|
64 |
let
|
26238
|
65 |
val { local_constraints, global_constraints, improve, subst, passed, ... } =
|
|
66 |
ImprovableSyntax.get ctxt;
|
|
67 |
val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
|
|
68 |
fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
|
|
69 |
of SOME ty_ty' => (perhaps o try o Type.typ_match tsig) ty_ty'
|
|
70 |
| _ => I)
|
|
71 |
| accumulate_improvements _ = I;
|
|
72 |
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
|
|
73 |
val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts;
|
|
74 |
fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
|
26259
|
75 |
of SOME (ty', t') =>
|
26238
|
76 |
if Type.typ_instance tsig (ty, ty')
|
|
77 |
then SOME (ty', apply_subst t') else NONE
|
|
78 |
| NONE => NONE)
|
26259
|
79 |
| _ => NONE) t;
|
26238
|
80 |
val ts'' = map apply_subst ts';
|
|
81 |
in if eq_list (op aconv) (ts, ts'') andalso passed then NONE else
|
|
82 |
if passed then SOME (ts'', ctxt)
|
|
83 |
else SOME (ts'', ctxt
|
|
84 |
|> fold (ProofContext.add_const_constraint o apsnd SOME) global_constraints
|
|
85 |
|> mark_passed)
|
|
86 |
end;
|
25519
|
87 |
|
26238
|
88 |
fun improve_term_uncheck ts ctxt =
|
25519
|
89 |
let
|
26238
|
90 |
val thy = ProofContext.theory_of ctxt;
|
|
91 |
val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
|
|
92 |
val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
|
|
93 |
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
|
|
94 |
|
26259
|
95 |
fun set_local_constraints ctxt =
|
|
96 |
let
|
|
97 |
val { local_constraints, ... } = ImprovableSyntax.get ctxt;
|
|
98 |
in fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints ctxt end;
|
|
99 |
|
|
100 |
val add_improvable_syntax =
|
|
101 |
Context.proof_map
|
26238
|
102 |
(Syntax.add_term_check 0 "improvement" improve_term_check
|
|
103 |
#> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
|
26259
|
104 |
#> set_local_constraints;
|
|
105 |
|
|
106 |
|
|
107 |
(** overloading target **)
|
|
108 |
|
|
109 |
(* bookkeeping *)
|
|
110 |
|
|
111 |
structure OverloadingData = ProofDataFun
|
|
112 |
(
|
|
113 |
type T = ((string * typ) * (string * bool)) list;
|
|
114 |
fun init _ = [];
|
|
115 |
);
|
|
116 |
|
|
117 |
val get_overloading = OverloadingData.get o LocalTheory.target_of;
|
|
118 |
val map_overloading = LocalTheory.target o OverloadingData.map;
|
|
119 |
|
|
120 |
fun operation lthy v = get_overloading lthy
|
|
121 |
|> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
|
|
122 |
|
|
123 |
fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
|
|
124 |
|
|
125 |
|
|
126 |
(* overloaded declarations and definitions *)
|
|
127 |
|
|
128 |
fun declare c_ty = pair (Const c_ty);
|
|
129 |
|
|
130 |
fun define checked name (c, t) =
|
|
131 |
Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
|
25519
|
132 |
|
|
133 |
|
|
134 |
(* target *)
|
|
135 |
|
26238
|
136 |
fun init raw_overloading thy =
|
25519
|
137 |
let
|
26238
|
138 |
val _ = if null raw_overloading then error "At least one parameter must be given" else ();
|
|
139 |
val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
|
|
140 |
fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
|
|
141 |
of SOME (v, _) => SOME (ty, Free (v, ty))
|
|
142 |
| NONE => NONE;
|
|
143 |
val unchecks =
|
|
144 |
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
|
25519
|
145 |
in
|
|
146 |
thy
|
|
147 |
|> ProofContext.init
|
26238
|
148 |
|> OverloadingData.put overloading
|
26259
|
149 |
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
|
26249
|
150 |
|> map_improvable_syntax (K ((([], []), ((K NONE, subst), unchecks)), false))
|
26238
|
151 |
|> add_improvable_syntax
|
25519
|
152 |
end;
|
|
153 |
|
|
154 |
fun conclude lthy =
|
|
155 |
let
|
|
156 |
val overloading = get_overloading lthy;
|
|
157 |
val _ = if null overloading then () else
|
26259
|
158 |
error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
|
25519
|
159 |
o Syntax.string_of_term lthy o Const o fst) overloading));
|
|
160 |
in
|
|
161 |
lthy
|
|
162 |
end;
|
|
163 |
|
25606
|
164 |
fun pretty lthy =
|
|
165 |
let
|
|
166 |
val thy = ProofContext.theory_of lthy;
|
|
167 |
val overloading = get_overloading lthy;
|
|
168 |
fun pr_operation ((c, ty), (v, _)) =
|
25861
|
169 |
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
|
|
170 |
Pretty.str (Sign.extern_const thy c), Pretty.str "::", Sign.pretty_typ thy ty];
|
25606
|
171 |
in
|
|
172 |
(Pretty.block o Pretty.fbreaks)
|
|
173 |
(Pretty.str "overloading" :: map pr_operation overloading)
|
|
174 |
end;
|
|
175 |
|
25519
|
176 |
end;
|