walther@59960
|
1 |
(* Title: Specify/refine.sml
|
walther@59960
|
2 |
Author: Walther Neuper 110226
|
walther@59960
|
3 |
(c) due to copyright terms
|
walther@59960
|
4 |
|
Walther@60555
|
5 |
Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close>
|
Walther@60586
|
6 |
better fitting the respective where_-condition.
|
Walther@60555
|
7 |
|
Walther@60658
|
8 |
The search on the tree given by @{term Know_Store.get_pbls} is costly such that
|
Walther@60658
|
9 |
\<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type.
|
Walther@60658
|
10 |
|
Walther@60658
|
11 |
On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type
|
Walther@60658
|
12 |
(and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)
|
Walther@60658
|
13 |
according to the current context.
|
Walther@60555
|
14 |
|
Walther@60555
|
15 |
Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
|
Walther@60555
|
16 |
are adapted for "adapt_to_type on the fly" until further clarification.
|
Walther@60556
|
17 |
|
Walther@60556
|
18 |
timing (from evaluating imports to use-cases.sml) for Test_Isac_Short
|
Walther@60556
|
19 |
before adapt_to_type: 01:05 sec:sec
|
Walther@60556
|
20 |
after adapt_to_type:
|
Walther@60556
|
21 |
timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ...
|
Walther@60556
|
22 |
before adapt_to_type: 1.5 sec
|
Walther@60556
|
23 |
after adapt_to_type:
|
Walther@60556
|
24 |
timing for test/../refine.sml --- refine ad-hoc equation for timing: ...
|
Walther@60556
|
25 |
before adapt_to_type: 0.05 sec
|
Walther@60556
|
26 |
after adapt_to_type:
|
Walther@60556
|
27 |
*)
|
walther@59960
|
28 |
|
walther@59960
|
29 |
signature REFINE_PROBLEM =
|
walther@59960
|
30 |
sig
|
Walther@60556
|
31 |
(**)
|
walther@59968
|
32 |
val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
|
walther@59968
|
33 |
|
Walther@60742
|
34 |
val by_o_model : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
|
Walther@60742
|
35 |
val by_o_model' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
|
Walther@60742
|
36 |
val by_formalise: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list
|
walther@59960
|
37 |
|
Walther@60729
|
38 |
(*from isac_test for Minisubpbl*)
|
Walther@60742
|
39 |
datatype match_model_prec = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;
|
Walther@60742
|
40 |
val find_match: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node -> match_model_prec list
|
Walther@60742
|
41 |
val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
|
Walther@60742
|
42 |
val check_match: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
|
Walther@60736
|
43 |
|
Walther@60736
|
44 |
\<^isac_test>\<open>
|
Walther@60742
|
45 |
val match_found: match_model_prec list -> match_model_prec option
|
Walther@60742
|
46 |
val find_matchs: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list
|
wenzelm@60223
|
47 |
\<close>
|
walther@59960
|
48 |
end
|
walther@59960
|
49 |
|
walther@59965
|
50 |
(**)
|
walther@59960
|
51 |
structure Refine(**) : REFINE_PROBLEM(**) =
|
walther@59960
|
52 |
struct
|
walther@59965
|
53 |
(**)
|
walther@59960
|
54 |
|
Walther@60742
|
55 |
datatype match_model_prec =
|
walther@59963
|
56 |
Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
|
walther@59960
|
57 |
| NoMatch_;
|
walther@59960
|
58 |
|
walther@59960
|
59 |
fun is_matches_ (Match_ _) = true
|
walther@59960
|
60 |
| is_matches_ _ = false;
|
walther@59960
|
61 |
|
Walther@60742
|
62 |
fun match_found ms = ((find_first is_matches_) o rev) ms;
|
walther@59960
|
63 |
|
walther@59960
|
64 |
fun eq1 d (_, (d', _)) = (d = d');
|
walther@59960
|
65 |
|
Walther@60478
|
66 |
(* chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
|
walther@59960
|
67 |
fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
|
walther@59960
|
68 |
(case find_first (eq1 d) pbt of
|
Walther@60478
|
69 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
|
walther@59960
|
70 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
71 |
| chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
|
walther@59960
|
72 |
(case find_first (eq1 d) pbt of
|
Walther@60478
|
73 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
|
walther@59960
|
74 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
75 |
| chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
|
walther@59960
|
76 |
| chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
|
walther@59960
|
77 |
| chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
|
walther@59960
|
78 |
(case find_first (eq1 d) pbt of
|
Walther@60478
|
79 |
SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
|
walther@59960
|
80 |
| NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
|
walther@59960
|
81 |
| chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
|
walther@59960
|
82 |
(case find_first (eq1 d) pbt of
|
Walther@60478
|
83 |
SOME _ =>
|
Walther@60478
|
84 |
raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
|
walther@59960
|
85 |
| NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
|
walther@59960
|
86 |
| chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
|
walther@59960
|
87 |
|
Walther@60477
|
88 |
fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
|
walther@59960
|
89 |
fun eq0 (0, _, _, _, _) = true
|
walther@59960
|
90 |
| eq0 _ = false;
|
walther@59960
|
91 |
fun max_i i [] = i
|
walther@59960
|
92 |
| max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
|
walther@59960
|
93 |
fun max_id [] = 0
|
walther@59960
|
94 |
| max_id ((id, _, _, _, _) :: is) = max_i id is;
|
walther@59960
|
95 |
fun add_idvat itms _ _ [] = itms
|
walther@59960
|
96 |
| add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
|
walther@59960
|
97 |
add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
|
walther@59960
|
98 |
|
walther@59960
|
99 |
(* find elements of pbt not contained in itms;
|
walther@59960
|
100 |
if such one is untouched, return this one, otherwise create new itm *)
|
walther@59960
|
101 |
fun chk_m itms untouched (p as (f, (d, id))) =
|
walther@59960
|
102 |
case find_first (eq2 p) itms of
|
walther@59960
|
103 |
SOME _ => []
|
walther@59960
|
104 |
| NONE =>
|
walther@59960
|
105 |
(case find_first (eq2 p) untouched of
|
walther@59960
|
106 |
SOME itm => [itm]
|
walther@59960
|
107 |
| NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
|
walther@59960
|
108 |
|
walther@59960
|
109 |
fun chk_mis mvat itms untouched pbt =
|
walther@59960
|
110 |
let val mis = (flat o (map (chk_m itms untouched))) pbt;
|
walther@59960
|
111 |
val mid = max_id itms;
|
walther@59960
|
112 |
in add_idvat [] (mid + 1) mvat mis end;
|
walther@59960
|
113 |
|
walther@59960
|
114 |
(* check a problem (ie. itm list) for matching a problemtype,
|
Walther@60705
|
115 |
takes the Pre_Conds.max_variant for concluding completeness (could be another!) *)
|
Walther@60729
|
116 |
(*T_TESTold* )
|
Walther@60586
|
117 |
fun match_itms thy itms (pbt, where_, where_rls) =
|
walther@59960
|
118 |
let
|
walther@59960
|
119 |
fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
|
walther@59960
|
120 |
val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
|
Walther@60705
|
121 |
val mvat = Pre_Conds.max_variant itms';
|
walther@59960
|
122 |
val itms'' = filter (okv mvat) itms';
|
walther@59960
|
123 |
val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
|
walther@59960
|
124 |
val mis = chk_mis mvat itms'' untouched pbt;
|
Walther@60590
|
125 |
val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms'' mvat
|
Walther@60586
|
126 |
in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
|
Walther@60729
|
127 |
( *T_TEST**)
|
Walther@60729
|
128 |
fun match_itms thy itms (pbt, where_, where_rls) =
|
Walther@60729
|
129 |
let
|
Walther@60729
|
130 |
fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
|
Walther@60729
|
131 |
val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
|
Walther@60729
|
132 |
val mvat = Pre_Conds.max_variant itms';
|
Walther@60729
|
133 |
val itms'' = filter (okv mvat) itms';
|
Walther@60729
|
134 |
val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
|
Walther@60729
|
135 |
val mis = chk_mis mvat itms'' untouched pbt;
|
Walther@60741
|
136 |
val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_
|
Walther@60729
|
137 |
(pbt, I_Model.OLD_to_TEST itms'')
|
Walther@60729
|
138 |
in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
|
Walther@60729
|
139 |
(*T_TESTnew*)
|
walther@59960
|
140 |
|
walther@59960
|
141 |
(* refine a problem; version for tactic Refine_Problem *)
|
Walther@60742
|
142 |
fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
|
walther@59960
|
143 |
let
|
Walther@60585
|
144 |
val {thy, model, where_, where_rls, ...} = py
|
Walther@60556
|
145 |
(*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
|
Walther@60586
|
146 |
val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
|
walther@59960
|
147 |
in
|
walther@59960
|
148 |
if b
|
Walther@60586
|
149 |
then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))]
|
walther@59960
|
150 |
else pbls @ [NoMatch_]
|
walther@59960
|
151 |
end
|
Walther@60742
|
152 |
| find_match _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
|
walther@59960
|
153 |
let
|
Walther@60585
|
154 |
val {thy, model, where_, where_rls, ...} = py
|
Walther@60586
|
155 |
val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
|
walther@59960
|
156 |
in if b
|
Walther@60586
|
157 |
then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_'))
|
Walther@60742
|
158 |
in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
|
walther@59960
|
159 |
else (pbls @ [NoMatch_])
|
Walther@60556
|
160 |
end
|
Walther@60742
|
161 |
| find_match _ _ _ _ _ = raise ERROR "find_match: uncovered fun def."
|
Walther@60742
|
162 |
and find_matchs _ _ _ pbls [] = pbls
|
Walther@60742
|
163 |
| find_matchs thy pblRD itms pbls ((p as Store.Node _) :: pts) =
|
walther@59960
|
164 |
let
|
Walther@60742
|
165 |
val pbls' = find_match thy pblRD itms pbls p
|
walther@59960
|
166 |
in case last_elem pbls' of
|
walther@59960
|
167 |
Match_ _ => pbls'
|
Walther@60742
|
168 |
| NoMatch_ => find_matchs thy pblRD itms pbls' pts
|
walther@59960
|
169 |
end;
|
walther@59960
|
170 |
|
walther@59960
|
171 |
fun problem thy pblID itms =
|
Walther@60742
|
172 |
case match_found ((Store.apply (get_pbls ())) (find_match thy ((rev o tl) pblID) itms [])
|
walther@60324
|
173 |
pblID (rev pblID)) of
|
walther@59960
|
174 |
NONE => NONE
|
Walther@60556
|
175 |
| SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
|
walther@59960
|
176 |
|
Walther@60556
|
177 |
(*
|
Walther@60729
|
178 |
refine a problem; construct pblRD while scanning Problem.T Store.T
|
Walther@60742
|
179 |
TODO: as \<open>check_match: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.
|
Walther@60556
|
180 |
*)
|
Walther@60742
|
181 |
fun check_match ctxt pblRD ori (Store.Node (pI, [py], [])) =
|
Walther@60556
|
182 |
let
|
Walther@60742
|
183 |
val _ = writeln ("check_match 1: " ^ strs2str pblRD)
|
Walther@60585
|
184 |
val {where_rls, model, where_, ...} = py: Problem.T
|
Walther@60585
|
185 |
val model = map (Model_Pattern.adapt_to_type ctxt) model
|
Walther@60660
|
186 |
val where_ = map (ParseC.adapt_term_to_type ctxt) where_
|
Walther@60556
|
187 |
in
|
Walther@60590
|
188 |
if M_Match.match_oris ctxt where_rls ori (model, where_)
|
Walther@60729
|
189 |
then SOME (pblRD(**) @ [pI](**))
|
Walther@60556
|
190 |
else NONE
|
Walther@60556
|
191 |
end
|
Walther@60742
|
192 |
| check_match ctxt pblRD ori (Store.Node (pI, [py], pys)) =
|
Walther@60556
|
193 |
let
|
Walther@60742
|
194 |
val _ = writeln ("check_match 2: " ^ strs2str pblRD)
|
Walther@60585
|
195 |
val {where_rls, model, where_, ...} = py: Problem.T
|
Walther@60585
|
196 |
val model = map (Model_Pattern.adapt_to_type ctxt) model
|
Walther@60660
|
197 |
val where_ = map (ParseC.adapt_term_to_type ctxt) where_
|
Walther@60556
|
198 |
in
|
Walther@60590
|
199 |
if M_Match.match_oris ctxt where_rls ori (model, where_)
|
Walther@60575
|
200 |
then (case refins ctxt (pblRD @ [pI]) ori pys of
|
Walther@60556
|
201 |
SOME pblRD' => SOME pblRD'
|
Walther@60729
|
202 |
| NONE => SOME (pblRD (**)@ [pI](**)))
|
Walther@60556
|
203 |
else NONE
|
Walther@60556
|
204 |
end
|
Walther@60742
|
205 |
| check_match _ _ _ _ = raise ERROR "check_match: uncovered fun def."
|
Walther@60575
|
206 |
and refins _ _ _ [] = NONE
|
Walther@60575
|
207 |
| refins ctxt pblRD ori ((p as Store.Node _) :: pts) =
|
Walther@60729
|
208 |
(writeln ("refins: " ^ strs2str pblRD);
|
Walther@60742
|
209 |
(case check_match ctxt pblRD ori p of
|
Walther@60729
|
210 |
SOME pblRD' => SOME (pblRD')
|
Walther@60729
|
211 |
| NONE => refins ctxt pblRD ori pts)
|
Walther@60729
|
212 |
);
|
Walther@60556
|
213 |
|
Walther@60556
|
214 |
\<^isac_test>\<open>
|
Walther@60738
|
215 |
(**)
|
Walther@60738
|
216 |
\<close>
|
Walther@60738
|
217 |
|
Walther@60729
|
218 |
(* refine a problem; version providing output for math authors *)
|
Walther@60575
|
219 |
(*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list ->
|
Walther@60556
|
220 |
Probl_Def.T Store.node -> M_Match.T list*)
|
Walther@60575
|
221 |
fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
|
Walther@60556
|
222 |
let
|
Walther@60556
|
223 |
val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
|
Walther@60585
|
224 |
val {thy, model, where_, where_rls, ...} = py
|
Walther@60585
|
225 |
val model = map (Model_Pattern.adapt_to_type ctxt) model
|
Walther@60660
|
226 |
val where_ = map (ParseC.adapt_term_to_type ctxt) where_
|
Walther@60653
|
227 |
val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
|
Walther@60586
|
228 |
val (b, (itms, where_')) =
|
Walther@60585
|
229 |
M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
|
Walther@60653
|
230 |
in
|
Walther@60556
|
231 |
if b
|
Walther@60586
|
232 |
then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
|
Walther@60586
|
233 |
else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
|
Walther@60556
|
234 |
end
|
Walther@60575
|
235 |
| refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
|
Walther@60556
|
236 |
let
|
Walther@60556
|
237 |
val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
|
Walther@60585
|
238 |
val {thy, model, where_, where_rls, ...} = py
|
Walther@60585
|
239 |
val model = map (Model_Pattern.adapt_to_type ctxt) model
|
Walther@60660
|
240 |
val where_ = map (ParseC.adapt_term_to_type ctxt) where_
|
Walther@60653
|
241 |
val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
|
Walther@60586
|
242 |
val (b, (itms, where_')) =
|
Walther@60585
|
243 |
M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
|
Walther@60556
|
244 |
in
|
Walther@60556
|
245 |
if b
|
Walther@60556
|
246 |
then
|
Walther@60586
|
247 |
let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
|
Walther@60575
|
248 |
in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
|
Walther@60586
|
249 |
else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
|
Walther@60556
|
250 |
end
|
Walther@60575
|
251 |
| refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
|
Walther@60575
|
252 |
and refins' _ _ _ pbls [] = pbls
|
Walther@60575
|
253 |
| refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) =
|
Walther@60556
|
254 |
let
|
Walther@60575
|
255 |
val pbls' = refin' ctxt pblRD fmz pbls p
|
Walther@60556
|
256 |
in
|
Walther@60556
|
257 |
case last_elem pbls' of
|
Walther@60556
|
258 |
M_Match.Matches _ => pbls'
|
Walther@60575
|
259 |
| M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
|
Walther@60556
|
260 |
end;
|
walther@59968
|
261 |
|
Walther@60556
|
262 |
(*
|
Walther@60556
|
263 |
TODO: rename \<rightarrow> apply_to_node
|
Walther@60556
|
264 |
apply a fun to a ptyps node.
|
Walther@60742
|
265 |
val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
|
Walther@60729
|
266 |
TODO: Store.apply scans Store.T only to the first hit; see Store.apply.
|
Walther@60556
|
267 |
*)
|
Walther@60742
|
268 |
fun find_node_elem x = Store.apply (get_pbls ()) x;
|
walther@59968
|
269 |
|
Walther@60742
|
270 |
(*for tactic Refine_Tacitly; oris are already created wrt. some pbt; ctxt overrides thy in pbt*)
|
Walther@60742
|
271 |
fun by_o_model ctxt oris pblID =
|
walther@59968
|
272 |
let
|
Walther@60742
|
273 |
val opt = find_node_elem (check_match ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
|
Walther@60556
|
274 |
in case opt of
|
walther@59968
|
275 |
SOME pblRD =>
|
walther@59968
|
276 |
let val pblID': Problem.id = rev pblRD
|
walther@59968
|
277 |
in if pblID' = pblID then NONE else SOME pblID' end
|
walther@59968
|
278 |
| NONE => NONE
|
walther@59968
|
279 |
end;
|
Walther@60742
|
280 |
fun by_o_model' ctxt oris pI = perhaps (by_o_model ctxt oris) pI;
|
Walther@60742
|
281 |
|
Walther@60742
|
282 |
(*specifically for tests*)
|
Walther@60742
|
283 |
fun by_formalise ctxt fmz pblID =
|
Walther@60742
|
284 |
find_node_elem (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);
|
walther@59968
|
285 |
|
walther@60268
|
286 |
\<^isac_test>\<open>
|
Walther@60738
|
287 |
(**)
|
walther@60268
|
288 |
\<close>
|
walther@59968
|
289 |
|
walther@59965
|
290 |
(**)end(**)
|