19 structure Overloading: OVERLOADING = |
19 structure Overloading: OVERLOADING = |
20 struct |
20 struct |
21 |
21 |
22 (* generic check/uncheck combinators for improvable constants *) |
22 (* generic check/uncheck combinators for improvable constants *) |
23 |
23 |
24 type improvable_syntax = ((((string * typ) list * (string * typ) list) * |
24 type improvable_syntax = { |
25 ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) * |
25 primary_constraints: (string * typ) list, |
26 (term * term) list)) * bool); |
26 secondary_constraints: (string * typ) list, |
|
27 improve: string * typ -> (typ * typ) option, |
|
28 subst: string * typ -> (typ * term) option, |
|
29 no_subst_in_abbrev_mode: bool, |
|
30 unchecks: (term * term) list |
|
31 } |
27 |
32 |
28 structure Improvable_Syntax = Proof_Data |
33 structure Improvable_Syntax = Proof_Data |
29 ( |
34 ( |
30 type T = { |
35 type T = {syntax: improvable_syntax, secondary_pass: bool} |
31 primary_constraints: (string * typ) list, |
36 fun init _ = {syntax = { |
32 secondary_constraints: (string * typ) list, |
37 primary_constraints = [], |
33 improve: string * typ -> (typ * typ) option, |
38 secondary_constraints = [], |
34 subst: string * typ -> (typ * term) option, |
39 improve = K NONE, |
35 consider_abbrevs: bool, |
40 subst = K NONE, |
36 unchecks: (term * term) list, |
41 no_subst_in_abbrev_mode = false, |
37 passed: bool |
42 unchecks = [] |
38 }; |
43 }, secondary_pass = false}: T; |
39 val empty: T = { |
|
40 primary_constraints = [], |
|
41 secondary_constraints = [], |
|
42 improve = K NONE, |
|
43 subst = K NONE, |
|
44 consider_abbrevs = false, |
|
45 unchecks = [], |
|
46 passed = true |
|
47 }; |
|
48 fun init _ = empty; |
|
49 ); |
44 ); |
50 |
45 |
51 fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints, |
46 fun map_improvable_syntax f = |
52 secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} => |
47 Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass}); |
53 let |
48 |
54 val (((primary_constraints', secondary_constraints'), |
49 val mark_passed = |
55 (((improve', subst'), consider_abbrevs'), unchecks')), passed') |
50 Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true}); |
56 = f (((primary_constraints, secondary_constraints), |
|
57 (((improve, subst), consider_abbrevs), unchecks)), passed) |
|
58 in |
|
59 {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints', |
|
60 improve = improve', subst = subst', consider_abbrevs = consider_abbrevs', |
|
61 unchecks = unchecks', passed = passed'} |
|
62 end); |
|
63 |
|
64 val mark_passed = (map_improvable_syntax o apsnd) (K true); |
|
65 |
51 |
66 fun improve_term_check ts ctxt = |
52 fun improve_term_check ts ctxt = |
67 let |
53 let |
68 val thy = Proof_Context.theory_of ctxt; |
54 val thy = Proof_Context.theory_of ctxt; |
69 |
55 |
70 val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} = |
56 val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} = |
71 Improvable_Syntax.get ctxt; |
57 Improvable_Syntax.get ctxt; |
72 val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt; |
58 val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode; |
73 val passed_or_abbrev = passed orelse is_abbrev; |
|
74 fun accumulate_improvements (Const (c, ty)) = |
59 fun accumulate_improvements (Const (c, ty)) = |
75 (case improve (c, ty) of |
60 (case improve (c, ty) of |
76 SOME ty_ty' => Sign.typ_match thy ty_ty' |
61 SOME ty_ty' => Sign.typ_match thy ty_ty' |
77 | _ => I) |
62 | _ => I) |
78 | accumulate_improvements _ = I; |
63 | accumulate_improvements _ = I; |
79 val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; |
|
80 val ts' = (map o map_types) (Envir.subst_type improvements) ts; |
|
81 fun apply_subst t = |
64 fun apply_subst t = |
82 Envir.expand_term |
65 Envir.expand_term |
83 (fn Const (c, ty) => |
66 (fn Const (c, ty) => |
84 (case subst (c, ty) of |
67 (case subst (c, ty) of |
85 SOME (ty', t') => |
68 SOME (ty', t') => |
86 if Sign.typ_instance thy (ty, ty') |
69 if Sign.typ_instance thy (ty, ty') |
87 then SOME (ty', apply_subst t') else NONE |
70 then SOME (ty', apply_subst t') else NONE |
88 | NONE => NONE) |
71 | NONE => NONE) |
89 | _ => NONE) t; |
72 | _ => NONE) t; |
90 val ts'' = if is_abbrev then ts' else map apply_subst ts'; |
73 val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; |
|
74 val ts' = |
|
75 ts |
|
76 |> (map o map_types) (Envir.subst_type improvements) |
|
77 |> not no_subst ? map apply_subst; |
91 in |
78 in |
92 if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE |
79 if secondary_pass orelse no_subst then |
93 else if passed_or_abbrev then SOME (ts'', ctxt) |
80 if eq_list (op aconv) (ts, ts') then NONE |
|
81 else SOME (ts', ctxt) |
94 else |
82 else |
95 SOME (ts'', ctxt |
83 SOME (ts', ctxt |
96 |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints |
84 |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints |
97 |> mark_passed) |
85 |> mark_passed) |
98 end; |
86 end; |
99 |
87 |
100 fun rewrite_liberal thy unchecks t = |
88 fun rewrite_liberal thy unchecks t = |
103 | SOME t' => if t aconv t' then NONE else SOME t'); |
91 | SOME t' => if t aconv t' then NONE else SOME t'); |
104 |
92 |
105 fun improve_term_uncheck ts ctxt = |
93 fun improve_term_uncheck ts ctxt = |
106 let |
94 let |
107 val thy = Proof_Context.theory_of ctxt; |
95 val thy = Proof_Context.theory_of ctxt; |
108 val {unchecks, ...} = Improvable_Syntax.get ctxt; |
96 val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt; |
109 val ts' = map (rewrite_liberal thy unchecks) ts; |
97 val ts' = map (rewrite_liberal thy unchecks) ts; |
110 in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
98 in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
111 |
99 |
112 fun set_primary_constraints ctxt = |
100 fun set_primary_constraints ctxt = |
113 let val {primary_constraints, ...} = Improvable_Syntax.get ctxt; |
101 let |
|
102 val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt; |
114 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
103 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
115 |
104 |
116 val activate_improvable_syntax = |
105 val activate_improvable_syntax = |
117 Context.proof_map |
106 Context.proof_map |
118 (Syntax_Phases.term_check' 0 "improvement" improve_term_check |
107 (Syntax_Phases.term_check' 0 "improvement" improve_term_check |
145 | NONE => NONE); |
134 | NONE => NONE); |
146 val unchecks = |
135 val unchecks = |
147 map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; |
136 map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; |
148 in |
137 in |
149 ctxt |
138 ctxt |
150 |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) |
139 |> map_improvable_syntax (K {primary_constraints = [], |
|
140 secondary_constraints = [], improve = K NONE, subst = subst, |
|
141 no_subst_in_abbrev_mode = false, unchecks = unchecks}) |
151 end; |
142 end; |
152 |
143 |
153 fun define_overloaded (c, U) (v, checked) (b_def, rhs) = |
144 fun define_overloaded (c, U) (v, checked) (b_def, rhs) = |
154 Local_Theory.background_theory_result |
145 Local_Theory.background_theory_result |
155 (Thm.add_def_global (not checked) true |
146 (Thm.add_def_global (not checked) true |