1 (* Title: Specify/refine.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close>
6 better fitting the respective pre-condition.
8 The search on the tree got by @{term KEStore_Elems.get_pbls} is costly such that
9 \<open>ML_structure KEStore_Elems\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, pre-condition (and cas).
10 The terms are pre-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
11 according to the type suggested by the current \<open>ML_structure Context\<close>.
13 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
14 are adapted for "adapt_to_type on the fly" until further clarification.
16 timing (from evaluating imports to use-cases.sml) for Test_Isac_Short
17 before adapt_to_type: 01:05 sec:sec
19 timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ...
20 before adapt_to_type: 1.5 sec
22 timing for test/../refine.sml --- refine ad-hoc equation for timing: ...
23 before adapt_to_type: 0.05 sec
27 signature REFINE_PROBLEM =
30 val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
33 val refine_ori : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
35 val refine_ori' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
38 (*val test : Formalise.model -> Problem.id -> M_Match.T list*)
39 (*val refine : Formalise.model -> Problem.id -> M_Match.T list*)
40 val xxxxx: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list
42 datatype match_ = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;
44 val refined_: match_ list -> match_ option
46 val refin'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node -> match_ list
48 val refins'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node list -> match_ list
50 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
51 val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
56 structure Refine(**) : REFINE_PROBLEM(**) =
61 Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
64 fun is_matches_ (Match_ _) = true
65 | is_matches_ _ = false;
67 fun refined_ ms = ((find_first is_matches_) o rev) ms;
69 fun eq1 d (_, (d', _)) = (d = d');
71 (* chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
72 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
73 (case find_first (eq1 d) pbt of
74 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
75 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
76 | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
77 (case find_first (eq1 d) pbt of
78 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
79 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
80 | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
81 | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
82 | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
83 (case find_first (eq1 d) pbt of
84 SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
85 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
86 | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
87 (case find_first (eq1 d) pbt of
89 raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
90 | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
91 | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
93 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
94 fun eq0 (0, _, _, _, _) = true
97 | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
99 | max_id ((id, _, _, _, _) :: is) = max_i id is;
100 fun add_idvat itms _ _ [] = itms
101 | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
102 add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
104 (* find elements of pbt not contained in itms;
105 if such one is untouched, return this one, otherwise create new itm *)
106 fun chk_m itms untouched (p as (f, (d, id))) =
107 case find_first (eq2 p) itms of
110 (case find_first (eq2 p) untouched of
112 | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
114 fun chk_mis mvat itms untouched pbt =
115 let val mis = (flat o (map (chk_m itms untouched))) pbt;
116 val mid = max_id itms;
117 in add_idvat [] (mid + 1) mvat mis end;
119 (* check a problem (ie. itm list) for matching a problemtype,
120 takes the I_Model.max_variant for concluding completeness (could be another!) *)
121 fun match_itms thy itms (pbt, pre, where_rls) =
123 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
124 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
125 val mvat = I_Model.max_variant itms';
126 val itms'' = filter (okv mvat) itms';
127 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
128 val mis = chk_mis mvat itms'' untouched pbt;
129 val (pb, pre') = Pre_Conds.check where_rls pre itms'' mvat
130 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
132 (* refine a problem; version for tactic Refine_Problem *)
133 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
135 val {thy, model, where_, where_rls, ...} = py
136 (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
137 val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
140 then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
141 else pbls @ [NoMatch_]
143 | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
145 val {thy, model, where_, where_rls, ...} = py
146 val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
148 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
149 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
150 else (pbls @ [NoMatch_])
152 | refin'' _ _ _ _ _ = raise ERROR "refin'': uncovered fun def."
153 and refins'' _ _ _ pbls [] = pbls
154 | refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
156 val pbls' = refin'' thy pblRD itms pbls p
157 in case last_elem pbls' of
159 | NoMatch_ => refins'' thy pblRD itms pbls' pts
162 fun problem thy pblID itms =
163 case refined_ ((Store.apply (get_pbls ())) (refin'' thy ((rev o tl) pblID) itms [])
164 pblID (rev pblID)) of
166 | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
169 refine a problem; construct pblRD while scanning
170 val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
173 fun refin pblRD ori (Store.Node (pI, [py], [])) =
174 if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py)
175 then SOME (pblRD @ [pI])
177 | refin pblRD ori (Store.Node (pI, [py], pys)) =
178 if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py)
179 then (case refins (pblRD @ [pI]) ori pys of
180 SOME pblRD' => SOME pblRD'
181 | NONE => SOME (pblRD @ [pI]))
183 | refin _ _ _ = raise ERROR "refin: uncovered fun def."
184 and refins _ _ [] = NONE
185 | refins pblRD ori ((p as Store.Node _) :: pts) =
186 (case refin pblRD ori p of
187 SOME pblRD' => SOME pblRD'
188 | NONE => refins pblRD ori pts);
189 ( ** )TODO clean up after "... "adapt to current ctxt"( **)
191 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
192 (*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
193 fun refin ctxt pblRD ori (Store.Node (pI, [py], [])) =
195 val {where_rls, model, where_, ...} = py: Problem.T
196 val model = map (Model_Pattern.adapt_to_type ctxt) model
197 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
199 if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_)
200 then SOME (pblRD @ [pI])
203 | refin ctxt pblRD ori (Store.Node (pI, [py], pys)) =
205 val {where_rls, model, where_, ...} = py: Problem.T
206 val model = map (Model_Pattern.adapt_to_type ctxt) model
207 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
209 if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_)
210 then (case refins ctxt (pblRD @ [pI]) ori pys of
211 SOME pblRD' => SOME pblRD'
212 | NONE => SOME (pblRD @ [pI]))
215 | refin _ _ _ _ = raise ERROR "refin: uncovered fun def."
216 and refins _ _ _ [] = NONE
217 | refins ctxt pblRD ori ((p as Store.Node _) :: pts) =
218 (case refin ctxt pblRD ori p of
219 SOME pblRD' => SOME pblRD'
220 | NONE => refins ctxt pblRD ori pts);
223 (* refine a problem; version providing output for math-experts *)
225 fun refin' pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
227 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
228 val {thy, model, where_, where_rls, ...} = py
229 val oris = O_Model.init thy fmz model(* |> #1*);
230 (* WN020803: itms!: oris might _not_ be complete here *)
231 val (b, (itms, pre')) = M_Match.match_oris' thy oris (model, where_, where_rls)
234 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
235 else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
237 | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
239 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
240 val {thy, model, where_, where_rls, ...} = py
241 val oris = O_Model.init thy fmz model(* |> #1*);
242 (* WN020803: itms!: oris might _not_ be complete here *)
243 val(b, (itms, pre')) = M_Match.match_oris' thy oris (model,where_,where_rls);
247 let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
248 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
249 else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
251 | refin' _ _ _ _ = raise ERROR "refin': uncovered fun def."
252 and refins' _ _ pbls [] = pbls
253 | refins' pblRD fmz pbls ((p as Store.Node _) :: pts) =
255 val pbls' = refin' pblRD fmz pbls p
257 case last_elem pbls' of
258 M_Match.Matches _ => pbls'
259 | M_Match.NoMatch _ => refins' pblRD fmz pbls' pts
262 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list ->
263 Probl_Def.T Store.node -> M_Match.T list*)
264 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
266 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
267 val {thy, model, where_, where_rls, ...} = py
268 val model = map (Model_Pattern.adapt_to_type ctxt) model
269 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
270 val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
271 val (b, (itms, pre')) =
272 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
275 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
276 else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
278 | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
280 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
281 val {thy, model, where_, where_rls, ...} = py
282 val model = map (Model_Pattern.adapt_to_type ctxt) model
283 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
284 val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
285 val (b, (itms, pre')) =
286 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
290 let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
291 in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
292 else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
294 | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
295 and refins' _ _ _ pbls [] = pbls
296 | refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) =
298 val pbls' = refin' ctxt pblRD fmz pbls p
300 case last_elem pbls' of
301 M_Match.Matches _ => pbls'
302 | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
307 TODO: rename \<rightarrow> apply_to_node
308 apply a fun to a ptyps node.
309 val app_ptyp: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
311 fun app_ptyp x = Store.apply (get_pbls ()) x;
313 (* TODO rename \<rightarrow> by_oris
314 for tactic Refine_Tacitly
315 oris are already created wrt. some pbt; ctxt overrides thy in pbt *)
316 fun refine_ori ctxt oris pblID =
318 val opt = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
321 let val pblID': Problem.id = rev pblRD
322 in if pblID' = pblID then NONE else SOME pblID' end
325 fun refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;
328 fun xxxxx ctxt fmz pblID =
329 app_ptyp (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);